(* generated by Ott 0.10.10 from: caml_typedef_syntax.ott caml_typedef_typing.ott caml_typedef_reduction.ott *) Require Import Arith. Require Import Bool. Require Import List. Require Import ott_list_core. Require Import BinInt. Require Import caml_lib_misc. (** syntax *) Definition index := nat. Lemma eq_index: forall (x y : index), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_index : ott_coq_equality. Definition ident := nat. Lemma eq_ident: forall (x y : ident), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_ident : ott_coq_equality. Definition integer_literal := Z. Lemma eq_integer_literal: forall (x y : integer_literal), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_integer_literal : ott_coq_equality. Definition float_literal := nat. Lemma eq_float_literal: forall (x y : float_literal), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_float_literal : ott_coq_equality. Definition char_literal := nat. Lemma eq_char_literal: forall (x y : char_literal), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_char_literal : ott_coq_equality. Definition string_literal := nat. Lemma eq_string_literal: forall (x y : string_literal), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_string_literal : ott_coq_equality. Definition infix_symbol := nat. Lemma eq_infix_symbol: forall (x y : infix_symbol), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_infix_symbol : ott_coq_equality. Definition prefix_symbol := nat. Lemma eq_prefix_symbol: forall (x y : prefix_symbol), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_prefix_symbol : ott_coq_equality. Definition location := nat. Lemma eq_location: forall (x y : location), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_location : ott_coq_equality. Definition lowercase_ident := nat. Lemma eq_lowercase_ident: forall (x y : lowercase_ident), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_lowercase_ident : ott_coq_equality. Definition capitalized_ident := nat. Lemma eq_capitalized_ident: forall (x y : capitalized_ident), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_capitalized_ident : ott_coq_equality. Inductive typeconstr_name : Set := TCN_id : lowercase_ident -> typeconstr_name . Inductive typeconstr : Set := TC_name : typeconstr_name -> typeconstr | TC_int : typeconstr | TC_char : typeconstr | TC_string : typeconstr | TC_float : typeconstr | TC_bool : typeconstr | TC_unit : typeconstr | TC_exn : typeconstr | TC_list : typeconstr | TC_option : typeconstr | TC_ref : typeconstr . Inductive idx : Set := N : index -> idx | Add : idx -> idx -> idx . Inductive typevar : Set := TV_ident : ident -> typevar . Inductive constr_name : Set := CN_id : capitalized_ident -> constr_name . Inductive typexpr : Set := TE_var : typevar -> typexpr | TE_idxvar : idx -> idx -> typexpr | TE_any : typexpr | TE_arrow : typexpr -> typexpr -> typexpr | TE_tuple : list typexpr -> typexpr | TE_constr : list typexpr -> typeconstr -> typexpr . Inductive field_name : Set := FN_id : lowercase_ident -> field_name . Inductive infix_op : Set := IO_symbol : infix_symbol -> infix_op | IO_star : infix_op | IO_equal : infix_op | IO_colonequal : infix_op . Inductive constr_decl : Set := CD_nullary : constr_name -> constr_decl | CD_nary : constr_name -> list typexpr -> constr_decl . Inductive field_decl : Set := FD_immutable : field_name -> typexpr -> field_decl . Inductive operator_name : Set := ON_symbol : prefix_symbol -> operator_name | ON_infix : infix_op -> operator_name . Inductive constr : Set := C_name : constr_name -> constr | C_invalidargument : constr | C_notfound : constr | C_assertfailure : constr | C_matchfailure : constr | C_div_by_0 : constr | C_none : constr | C_some : constr . Definition intn : Set := Z . Inductive type_equation : Set := TE_te : typexpr -> type_equation . Inductive type_representation : Set := TR_variant : list constr_decl -> type_representation | TR_record : list field_decl -> type_representation . Inductive type_param : Set := TP_var : typevar -> type_param . Inductive value_name : Set := VN_id : lowercase_ident -> value_name | VN_op : operator_name -> value_name . Inductive field : Set := F_name : field_name -> field . Inductive constant : Set := CONST_int : intn -> constant | CONST_float : float_literal -> constant | CONST_char : char_literal -> constant | CONST_string : string_literal -> constant | CONST_constr : constr -> constant | CONST_false : constant | CONST_true : constant | CONST_nil : constant | CONST_unit : constant . Inductive type_information : Set := TI_eq : type_equation -> type_information | TI_def : type_representation -> type_information . Inductive type_params_opt : Set := TPS_nary : list type_param -> type_params_opt . Inductive pattern : Set := P_var : value_name -> pattern | P_any : pattern | P_constant : constant -> pattern | P_alias : pattern -> value_name -> pattern | P_typed : pattern -> typexpr -> pattern | P_or : pattern -> pattern -> pattern | P_construct : constr -> list pattern -> pattern | P_construct_any : constr -> pattern | P_tuple : list pattern -> pattern | P_record : list (field*pattern) -> pattern | P_cons : pattern -> pattern -> pattern . Inductive unary_prim : Set := Uprim_raise : unary_prim | Uprim_not : unary_prim | Uprim_minus : unary_prim | Uprim_ref : unary_prim | Uprim_deref : unary_prim . Inductive binary_prim : Set := Bprim_equal : binary_prim | Bprim_plus : binary_prim | Bprim_minus : binary_prim | Bprim_times : binary_prim | Bprim_div : binary_prim | Bprim_assign : binary_prim . Inductive for_dirn : Set := FD_upto : for_dirn | FD_downto : for_dirn . Inductive typedef : Set := TD_td : type_params_opt -> typeconstr_name -> type_information -> typedef . Inductive letrec_binding : Set := LRB_simple : value_name -> pattern_matching -> letrec_binding with letrec_bindings : Set := LRBs_inj : list letrec_binding -> letrec_bindings with let_binding : Set := LB_simple : pattern -> expr -> let_binding with pat_exp : Set := PE_inj : pattern -> expr -> pat_exp with pattern_matching : Set := PM_pm : list pat_exp -> pattern_matching with expr : Set := Expr_uprim : unary_prim -> expr | Expr_bprim : binary_prim -> expr | Expr_ident : value_name -> expr | Expr_constant : constant -> expr | Expr_typed : expr -> typexpr -> expr | Expr_tuple : list expr -> expr | Expr_construct : constr -> list expr -> expr | Expr_cons : expr -> expr -> expr | Expr_record : list (field*expr) -> expr | Expr_override : expr -> list (field*expr) -> expr | Expr_apply : expr -> expr -> expr | Expr_and : expr -> expr -> expr | Expr_or : expr -> expr -> expr | Expr_field : expr -> field -> expr | Expr_ifthenelse : expr -> expr -> expr -> expr | Expr_while : expr -> expr -> expr | Expr_for : value_name -> expr -> for_dirn -> expr -> expr -> expr | Expr_sequence : expr -> expr -> expr | Expr_match : expr -> pattern_matching -> expr | Expr_function : pattern_matching -> expr | Expr_try : expr -> pattern_matching -> expr | Expr_let : let_binding -> expr -> expr | Expr_letrec : letrec_bindings -> expr -> expr | Expr_assert : expr -> expr | Expr_location : location -> expr . Inductive type_definition : Set := TDF_tdf : list typedef -> type_definition . Inductive exception_definition : Set := ED_def : constr_decl -> exception_definition . Inductive definition : Set := D_let : let_binding -> definition | D_letrec : letrec_bindings -> definition | D_type : type_definition -> definition | D_exception : exception_definition -> definition . Inductive typescheme : Set := TS_forall : typexpr -> typescheme . Definition kind : Set := nat . Inductive typexprs : Set := typexprs_inj : list typexpr -> typexprs . Inductive trans_label : Set := Lab_nil : trans_label | Lab_alloc : expr -> location -> trans_label | Lab_deref : location -> expr -> trans_label | Lab_assign : location -> expr -> trans_label . Inductive definitions : Set := Ds_nil : definitions | Ds_cons : definition -> definitions -> definitions . Inductive name : Set := name_tv : name | name_vn : value_name -> name | name_cn : constr_name -> name | name_tcn : typeconstr_name -> name | name_fn : field_name -> name | name_l : location -> name . Inductive environment_binding : Set := EB_tv : environment_binding | EB_vn : value_name -> typescheme -> environment_binding | EB_cc : constr_name -> typeconstr -> environment_binding | EB_pc : constr_name -> type_params_opt -> typexprs -> typeconstr -> environment_binding | EB_fn : field_name -> type_params_opt -> typeconstr_name -> typexpr -> environment_binding | EB_td : typeconstr_name -> kind -> environment_binding | EB_tr : typeconstr_name -> kind -> list field_name -> environment_binding | EB_ta : type_params_opt -> typeconstr_name -> typexpr -> environment_binding | EB_l : location -> typexpr -> environment_binding . Definition labelled_arrow : Set := trans_label . Inductive program : Set := Prog_defs : definitions -> program | Prog_raise : expr -> program . Definition store : Set := . Inductive names : Set := names_inj : list name -> names . Definition environment : Set := (list environment_binding) . Inductive Tsigma : Set := Tsigma_substs : list (typevar*typexpr) -> Tsigma . Inductive substs_x : Set := substs_x_xs : list (value_name*expr) -> substs_x . Inductive value_path : Set := VP_name : value_name -> value_path . Lemma eq_typeconstr_name: forall (x y : typeconstr_name), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_typeconstr_name : ott_coq_equality. Lemma eq_typeconstr: forall (x y : typeconstr), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_typeconstr : ott_coq_equality. Lemma eq_typevar: forall (x y : typevar), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_typevar : ott_coq_equality. Lemma eq_constr_name: forall (x y : constr_name), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_constr_name : ott_coq_equality. Lemma eq_field_name: forall (x y : field_name), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_field_name : ott_coq_equality. Lemma eq_infix_op: forall (x y : infix_op), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_infix_op : ott_coq_equality. Lemma eq_operator_name: forall (x y : operator_name), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_operator_name : ott_coq_equality. Lemma eq_constr: forall (x y : constr), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_constr : ott_coq_equality. Lemma eq_type_param: forall (x y : type_param), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_type_param : ott_coq_equality. Lemma eq_value_name: forall (x y : value_name), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_value_name : ott_coq_equality. Lemma eq_field: forall (x y : field), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_field : ott_coq_equality. Lemma eq_constant: forall (x y : constant), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_constant : ott_coq_equality. Lemma eq_for_dirn: forall (x y : for_dirn), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_for_dirn : ott_coq_equality. Lemma eq_name: forall (x y : name), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_name : ott_coq_equality. Lemma eq_value_path: forall (x y : value_path), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_value_path : ott_coq_equality. (** library functions *) Fixpoint list_assoc (A B:Set) (eq:forall a b:A,{a=b}+{a<>b}) (x:A) (l:list (A*B)) {struct l} : option B := match l with | nil => None | cons (a,b) t => if (eq a x) then Some b else list_assoc A B eq x t end. Implicit Arguments list_assoc. Fixpoint list_filter (A B:Set) (f:(A*B)->bool) (l:list (A*B)) {struct l} : list (A*B) := match l with | nil => nil | cons h t => if (f h) then cons h (list_filter A B f t) else (list_filter A B f t) end. Implicit Arguments list_filter. (** subrules *) Definition is_binary_prim_app_value_of_expr (e5:expr) : bool := match e5 with | (Expr_uprim unary_prim5) => false | (Expr_bprim binary_prim5) => (true) | (Expr_ident value_name5) => false | (Expr_constant constant5) => false | (Expr_typed expr5 typexpr5) => false | (Expr_tuple expr_list) => false | (Expr_construct constr5 expr_list) => false | (Expr_cons expr1 expr2) => false | (Expr_record field_expr_list) => false | (Expr_override expr_5 field_expr_list) => false | (Expr_apply expr1 expr2) => false | (Expr_and expr1 expr2) => false | (Expr_or expr1 expr2) => false | (Expr_field expr5 field5) => false | (Expr_ifthenelse expr0 expr1 expr2) => false | (Expr_while expr1 expr2) => false | (Expr_for x expr1 for_dirn5 expr2 expr3) => false | (Expr_sequence expr1 expr2) => false | (Expr_match expr5 pattern_matching5) => false | (Expr_function pattern_matching5) => false | (Expr_try expr5 pattern_matching5) => false | (Expr_let let_binding5 expr5) => false | (Expr_letrec letrec_bindings5 expr5) => false | (Expr_assert expr5) => false | (Expr_location location5) => false end. Definition is_definition_value_of_definition (d5:definition) : bool := match d5 with | (D_let let_binding5) => false | (D_letrec letrec_bindings5) => false | (D_type type_definition5) => (true) | (D_exception exception_definition5) => (true) end. Fixpoint is_value_of_expr (e5:expr) : bool := match e5 with | (Expr_uprim unary_prim5) => (true) | (Expr_bprim binary_prim5) => (true) | (Expr_ident value_name5) => false | (Expr_constant constant5) => (true) | (Expr_typed expr5 typexpr5) => false | (Expr_tuple expr_list) => ((forall_list (fun (expr_:expr) => (is_value_of_expr expr_)) expr_list)) | (Expr_construct constr5 expr_list) => ((forall_list (fun (expr_:expr) => (is_value_of_expr expr_)) expr_list)) | (Expr_cons expr1 expr2) => ((is_value_of_expr expr1) && (is_value_of_expr expr2)) | (Expr_record field_expr_list) => ((forall_list (fun (pat_:(field*expr)) => match pat_ with (field_,expr_) => (is_value_of_expr expr_) end) field_expr_list)) | (Expr_override expr_5 field_expr_list) => false | (Expr_apply expr1 expr2) => ((is_binary_prim_app_value_of_expr expr1) && (is_value_of_expr expr2)) | (Expr_and expr1 expr2) => false | (Expr_or expr1 expr2) => false | (Expr_field expr5 field5) => false | (Expr_ifthenelse expr0 expr1 expr2) => false | (Expr_while expr1 expr2) => false | (Expr_for x expr1 for_dirn5 expr2 expr3) => false | (Expr_sequence expr1 expr2) => false | (Expr_match expr5 pattern_matching5) => false | (Expr_function pattern_matching5) => (true) | (Expr_try expr5 pattern_matching5) => false | (Expr_let let_binding5 expr5) => false | (Expr_letrec letrec_bindings5 expr5) => false | (Expr_assert expr5) => false | (Expr_location location5) => (true) end. Fixpoint is_non_expansive_of_expr (e5:expr) : bool := match e5 with | (Expr_uprim unary_prim5) => (true) | (Expr_bprim binary_prim5) => (true) | (Expr_ident value_name5) => (true) | (Expr_constant constant5) => (true) | (Expr_typed expr5 typexpr5) => ((is_non_expansive_of_expr expr5)) | (Expr_tuple expr_list) => ((forall_list (fun (expr_:expr) => (is_non_expansive_of_expr expr_)) expr_list)) | (Expr_construct constr5 expr_list) => ((forall_list (fun (expr_:expr) => (is_non_expansive_of_expr expr_)) expr_list)) | (Expr_cons expr1 expr2) => ((is_non_expansive_of_expr expr1) && (is_non_expansive_of_expr expr2)) | (Expr_record field_expr_list) => ((forall_list (fun (pat_:(field*expr)) => match pat_ with (field_,expr_) => (is_non_expansive_of_expr expr_) end) field_expr_list)) | (Expr_override expr_5 field_expr_list) => false | (Expr_apply expr1 expr2) => ((is_binary_prim_app_value_of_expr expr1) && (is_non_expansive_of_expr expr2)) | (Expr_and expr1 expr2) => false | (Expr_or expr1 expr2) => false | (Expr_field expr5 field5) => false | (Expr_ifthenelse expr0 expr1 expr2) => false | (Expr_while expr1 expr2) => false | (Expr_for x expr1 for_dirn5 expr2 expr3) => false | (Expr_sequence expr1 expr2) => false | (Expr_match expr5 pattern_matching5) => false | (Expr_function pattern_matching5) => (true) | (Expr_try expr5 pattern_matching5) => false | (Expr_let let_binding5 expr5) => false | (Expr_letrec letrec_bindings5 expr5) => ((is_non_expansive_of_expr expr5)) | (Expr_assert expr5) => false | (Expr_location location5) => (true) end. Fixpoint is_src_typexpr_of_typexpr (t_5:typexpr) : bool := match t_5 with | (TE_var typevar5) => (true) | (TE_idxvar idx5 num) => false | TE_any => (true) | (TE_arrow typexpr1 typexpr2) => ((is_src_typexpr_of_typexpr typexpr1) && (is_src_typexpr_of_typexpr typexpr2)) | (TE_tuple typexpr_list) => ((forall_list (fun (typexpr_:typexpr) => (is_src_typexpr_of_typexpr typexpr_)) typexpr_list)) | (TE_constr typexpr_list typeconstr5) => ((forall_list (fun (typexpr_:typexpr) => (is_src_typexpr_of_typexpr typexpr_)) typexpr_list)) end. Fixpoint is_definitions_value_of_definitions (ds5:definitions) : bool := match ds5 with | Ds_nil => (true) | (Ds_cons definition5 definitions5) => ((is_definition_value_of_definition definition5) && (is_definitions_value_of_definitions definitions5)) end. Definition is_trans_label_of_trans_label (L5:trans_label) : bool := match L5 with | Lab_nil => (true) | (Lab_alloc v location5) => ((is_value_of_expr v)) | (Lab_deref location5 v) => ((is_value_of_expr v)) | (Lab_assign location5 v) => ((is_value_of_expr v)) end. (** auxiliary functions *) Definition aux_constr_names_constr_decl_of_constr_decl (constr_decl5:constr_decl) : list constr_name := match constr_decl5 with | (CD_nullary constr_name5) => (cons constr_name5 nil) | (CD_nary constr_name5 typexpr_list) => (cons constr_name5 nil) end. Definition aux_constr_names_type_representation_of_type_representation (type_representation5:type_representation) : list constr_name := match type_representation5 with | (TR_variant constr_decl_list) => (flat_map (fun (constr_decl_:constr_decl) => aux_constr_names_constr_decl_of_constr_decl constr_decl_) constr_decl_list) | (TR_record field_decl_list) => nil end. Definition aux_constr_names_type_information_of_type_information (type_information5:type_information) : list constr_name := match type_information5 with | (TI_eq type_equation5) => nil | (TI_def type_representation5) => (aux_constr_names_type_representation_of_type_representation type_representation5) end. Definition aux_field_names_field_decl_of_field_decl (field_decl5:field_decl) : list field_name := match field_decl5 with | (FD_immutable field_name5 typexpr5) => (cons field_name5 nil) end. Fixpoint aux_xs_pattern_of_pattern (pat5:pattern) : list value_name := match pat5 with | (P_var value_name5) => (cons value_name5 nil) | P_any => nil | (P_constant constant5) => nil | (P_alias pattern5 value_name5) => (app (aux_xs_pattern_of_pattern pattern5) (cons value_name5 nil)) | (P_typed pattern5 typexpr5) => (aux_xs_pattern_of_pattern pattern5) | (P_or pattern1 pattern2) => (aux_xs_pattern_of_pattern pattern1) | (P_construct constr5 pattern_list) => (flat_map (fun (pattern_:pattern) => aux_xs_pattern_of_pattern pattern_) pattern_list) | (P_construct_any constr5) => nil | (P_tuple pattern_list) => (flat_map (fun (pattern_:pattern) => aux_xs_pattern_of_pattern pattern_) pattern_list) | (P_record field_pattern_list) => (flat_map (fun (pat_:(field*pattern)) => match pat_ with (field_,pattern_) => aux_xs_pattern_of_pattern pattern_ end ) field_pattern_list) | (P_cons pattern1 pattern2) => (app (aux_xs_pattern_of_pattern pattern1) (aux_xs_pattern_of_pattern pattern2)) end. Definition aux_xs_letrec_binding_of_letrec_binding (letrec_binding5:letrec_binding) : list value_name := match letrec_binding5 with | (LRB_simple value_name5 pattern_matching5) => (cons value_name5 nil) end. Definition aux_constr_names_typedef_of_typedef (typedef5:typedef) : list constr_name := match typedef5 with | (TD_td type_params_opt5 typeconstr_name5 type_information5) => (aux_constr_names_type_information_of_type_information type_information5) end. Definition aux_field_names_type_representation_of_type_representation (type_representation5:type_representation) : list field_name := match type_representation5 with | (TR_variant constr_decl_list) => nil | (TR_record field_decl_list) => (flat_map (fun (field_decl_:field_decl) => aux_field_names_field_decl_of_field_decl field_decl_) field_decl_list) end. Definition aux_type_names_typedef_of_typedef (typedef5:typedef) : list typeconstr_name := match typedef5 with | (TD_td type_params_opt5 typeconstr_name5 type_information5) => (cons typeconstr_name5 nil) end. Definition aux_typevars_type_param_of_type_param (tp5:type_param) : list typevar := match tp5 with | (TP_var typevar5) => (cons typevar5 nil) end. Definition aux_xs_let_binding_of_let_binding (let_binding_6:let_binding) : list value_name := match let_binding_6 with | (LB_simple pattern5 expr5) => (aux_xs_pattern_of_pattern pattern5) end. Definition aux_xs_letrec_bindings_of_letrec_bindings (letrec_bindings_6:letrec_bindings) : list value_name := match letrec_bindings_6 with | (LRBs_inj letrec_binding_list) => (flat_map (fun (letrec_binding_:letrec_binding) => aux_xs_letrec_binding_of_letrec_binding letrec_binding_) letrec_binding_list) end. Definition aux_constr_names_type_definition_of_type_definition (type_definition5:type_definition) : list constr_name := match type_definition5 with | (TDF_tdf typedef_list) => (flat_map (fun (typedef_:typedef) => aux_constr_names_typedef_of_typedef typedef_) typedef_list) end. Definition aux_field_names_type_information_of_type_information (type_information5:type_information) : list field_name := match type_information5 with | (TI_eq type_equation5) => nil | (TI_def type_representation5) => (aux_field_names_type_representation_of_type_representation type_representation5) end. Definition aux_type_names_type_definition_of_type_definition (type_definition5:type_definition) : list typeconstr_name := match type_definition5 with | (TDF_tdf typedef_list) => (flat_map (fun (typedef_:typedef) => aux_type_names_typedef_of_typedef typedef_) typedef_list) end. Definition aux_typevars_type_params_opt_of_type_params_opt (type_params_opt5:type_params_opt) : list typevar := match type_params_opt5 with | (TPS_nary type_param_list) => (flat_map (fun (type_param_:type_param) => aux_typevars_type_param_of_type_param type_param_) type_param_list) end. Definition aux_xs_definition_of_definition (d5:definition) : list value_name := match d5 with | (D_let let_binding5) => (aux_xs_let_binding_of_let_binding let_binding5) | (D_letrec letrec_bindings5) => (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings5) | (D_type type_definition5) => nil | (D_exception exception_definition5) => nil end. (** free variables *) Fixpoint ftv_typexpr (t_5:typexpr) : list typevar := match t_5 with | (TE_var typevar5) => (cons typevar5 nil) | (TE_idxvar idx5 num) => nil | TE_any => nil | (TE_arrow typexpr1 typexpr2) => (app (ftv_typexpr typexpr1) (ftv_typexpr typexpr2)) | (TE_tuple typexpr_list) => ((flat_map (fun (typexpr_:typexpr) => (ftv_typexpr typexpr_)) typexpr_list)) | (TE_constr typexpr_list typeconstr5) => ((flat_map (fun (typexpr_:typexpr) => (ftv_typexpr typexpr_)) typexpr_list)) end. Definition ftv_constr_decl (constr_decl5:constr_decl) : list typevar := match constr_decl5 with | (CD_nullary constr_name5) => nil | (CD_nary constr_name5 typexpr_list) => ((flat_map (fun (typexpr_:typexpr) => (ftv_typexpr typexpr_)) typexpr_list)) end. Definition ftv_field_decl (field_decl5:field_decl) : list typevar := match field_decl5 with | (FD_immutable field_name5 typexpr5) => ((ftv_typexpr typexpr5)) end. Definition ftv_type_equation (type_equation5:type_equation) : list typevar := match type_equation5 with | (TE_te typexpr5) => ((ftv_typexpr typexpr5)) end. Definition ftv_type_representation (type_representation5:type_representation) : list typevar := match type_representation5 with | (TR_variant constr_decl_list) => ((flat_map (fun (constr_decl_:constr_decl) => (ftv_constr_decl constr_decl_)) constr_decl_list)) | (TR_record field_decl_list) => ((flat_map (fun (field_decl_:field_decl) => (ftv_field_decl field_decl_)) field_decl_list)) end. Definition ftv_type_information (type_information5:type_information) : list typevar := match type_information5 with | (TI_eq type_equation5) => ((ftv_type_equation type_equation5)) | (TI_def type_representation5) => ((ftv_type_representation type_representation5)) end. Fixpoint ftv_pattern (pat5:pattern) : list typevar := match pat5 with | (P_var value_name5) => nil | P_any => nil | (P_constant constant5) => nil | (P_alias pattern5 value_name5) => ((ftv_pattern pattern5)) | (P_typed pattern5 typexpr5) => (app (ftv_pattern pattern5) (ftv_typexpr typexpr5)) | (P_or pattern1 pattern2) => (app (ftv_pattern pattern1) (ftv_pattern pattern2)) | (P_construct constr5 pattern_list) => ((flat_map (fun (pattern_:pattern) => (ftv_pattern pattern_)) pattern_list)) | (P_construct_any constr5) => nil | (P_tuple pattern_list) => ((flat_map (fun (pattern_:pattern) => (ftv_pattern pattern_)) pattern_list)) | (P_record field_pattern_list) => ((flat_map (fun (pat_:(field*pattern)) => match pat_ with (field_,pattern_) => (ftv_pattern pattern_) end) field_pattern_list)) | (P_cons pattern1 pattern2) => (app (ftv_pattern pattern1) (ftv_pattern pattern2)) end. Definition ftv_typedef (typedef5:typedef) : list typevar := match typedef5 with | (TD_td type_params_opt5 typeconstr_name5 type_information5) => ((list_minus eq_typevar (ftv_type_information type_information5) (aux_typevars_type_params_opt_of_type_params_opt type_params_opt5))) end. Fixpoint ftv_letrec_binding (letrec_binding5:letrec_binding) : list typevar := match letrec_binding5 with | (LRB_simple value_name5 pattern_matching5) => ((ftv_pattern_matching pattern_matching5)) end with ftv_letrec_bindings (letrec_bindings_6:letrec_bindings) : list typevar := match letrec_bindings_6 with | (LRBs_inj letrec_binding_list) => ((flat_map (fun (letrec_binding_:letrec_binding) => (ftv_letrec_binding letrec_binding_)) letrec_binding_list)) end with ftv_let_binding (let_binding_6:let_binding) : list typevar := match let_binding_6 with | (LB_simple pattern5 expr5) => (app (ftv_pattern pattern5) (ftv_expr expr5)) end with ftv_pat_exp (pat_exp5:pat_exp) : list typevar := match pat_exp5 with | (PE_inj pattern5 expr5) => (app (ftv_pattern pattern5) (ftv_expr expr5)) end with ftv_pattern_matching (pm5:pattern_matching) : list typevar := match pm5 with | (PM_pm pat_exp_list) => ((flat_map (fun (pat_exp_:pat_exp) => (ftv_pat_exp pat_exp_)) pat_exp_list)) end with ftv_expr (e5:expr) : list typevar := match e5 with | (Expr_uprim unary_prim5) => nil | (Expr_bprim binary_prim5) => nil | (Expr_ident value_name5) => nil | (Expr_constant constant5) => nil | (Expr_typed expr5 typexpr5) => (app (ftv_expr expr5) (ftv_typexpr typexpr5)) | (Expr_tuple expr_list) => ((flat_map (fun (expr_:expr) => (ftv_expr expr_)) expr_list)) | (Expr_construct constr5 expr_list) => ((flat_map (fun (expr_:expr) => (ftv_expr expr_)) expr_list)) | (Expr_cons expr1 expr2) => (app (ftv_expr expr1) (ftv_expr expr2)) | (Expr_record field_expr_list) => ((flat_map (fun (pat_:(field*expr)) => match pat_ with (field_,expr_) => (ftv_expr expr_) end) field_expr_list)) | (Expr_override expr_5 field_expr_list) => (app (ftv_expr expr_5) (flat_map (fun (pat_:(field*expr)) => match pat_ with (field_,expr_) => (ftv_expr expr_) end) field_expr_list)) | (Expr_apply expr1 expr2) => (app (ftv_expr expr1) (ftv_expr expr2)) | (Expr_and expr1 expr2) => (app (ftv_expr expr1) (ftv_expr expr2)) | (Expr_or expr1 expr2) => (app (ftv_expr expr1) (ftv_expr expr2)) | (Expr_field expr5 field5) => ((ftv_expr expr5)) | (Expr_ifthenelse expr0 expr1 expr2) => (app (ftv_expr expr0) (app (ftv_expr expr1) (ftv_expr expr2))) | (Expr_while expr1 expr2) => (app (ftv_expr expr1) (ftv_expr expr2)) | (Expr_for x expr1 for_dirn5 expr2 expr3) => (app (ftv_expr expr1) (app (ftv_expr expr2) (ftv_expr expr3))) | (Expr_sequence expr1 expr2) => (app (ftv_expr expr1) (ftv_expr expr2)) | (Expr_match expr5 pattern_matching5) => (app (ftv_expr expr5) (ftv_pattern_matching pattern_matching5)) | (Expr_function pattern_matching5) => ((ftv_pattern_matching pattern_matching5)) | (Expr_try expr5 pattern_matching5) => (app (ftv_expr expr5) (ftv_pattern_matching pattern_matching5)) | (Expr_let let_binding5 expr5) => (app (ftv_let_binding let_binding5) (ftv_expr expr5)) | (Expr_letrec letrec_bindings5 expr5) => (app (ftv_letrec_bindings letrec_bindings5) (ftv_expr expr5)) | (Expr_assert expr5) => ((ftv_expr expr5)) | (Expr_location location5) => nil end. Definition ftv_type_definition (type_definition5:type_definition) : list typevar := match type_definition5 with | (TDF_tdf typedef_list) => ((flat_map (fun (typedef_:typedef) => (ftv_typedef typedef_)) typedef_list)) end. Definition ftv_exception_definition (exception_definition5:exception_definition) : list typevar := match exception_definition5 with | (ED_def constr_decl5) => ((ftv_constr_decl constr_decl5)) end. Fixpoint fv_letrec_binding (letrec_binding5:letrec_binding) : list value_name := match letrec_binding5 with | (LRB_simple value_name5 pattern_matching5) => ((fv_pattern_matching pattern_matching5)) end with fv_letrec_bindings (letrec_bindings_6:letrec_bindings) : list value_name := match letrec_bindings_6 with | (LRBs_inj letrec_binding_list) => ((flat_map (fun (letrec_binding_:letrec_binding) => (fv_letrec_binding letrec_binding_)) letrec_binding_list)) end with fv_let_binding (let_binding_6:let_binding) : list value_name := match let_binding_6 with | (LB_simple pattern5 expr5) => ((fv_expr expr5)) end with fv_pat_exp (pat_exp5:pat_exp) : list value_name := match pat_exp5 with | (PE_inj pattern5 expr5) => ((list_minus eq_value_name (fv_expr expr5) (aux_xs_pattern_of_pattern pattern5))) end with fv_pattern_matching (pm5:pattern_matching) : list value_name := match pm5 with | (PM_pm pat_exp_list) => ((flat_map (fun (pat_exp_:pat_exp) => (fv_pat_exp pat_exp_)) pat_exp_list)) end with fv_expr (e5:expr) : list value_name := match e5 with | (Expr_uprim unary_prim5) => nil | (Expr_bprim binary_prim5) => nil | (Expr_ident value_name5) => (cons value_name5 nil) | (Expr_constant constant5) => nil | (Expr_typed expr5 typexpr5) => ((fv_expr expr5)) | (Expr_tuple expr_list) => ((flat_map (fun (expr_:expr) => (fv_expr expr_)) expr_list)) | (Expr_construct constr5 expr_list) => ((flat_map (fun (expr_:expr) => (fv_expr expr_)) expr_list)) | (Expr_cons expr1 expr2) => (app (fv_expr expr1) (fv_expr expr2)) | (Expr_record field_expr_list) => ((flat_map (fun (pat_:(field*expr)) => match pat_ with (field_,expr_) => (fv_expr expr_) end) field_expr_list)) | (Expr_override expr_5 field_expr_list) => (app (fv_expr expr_5) (flat_map (fun (pat_:(field*expr)) => match pat_ with (field_,expr_) => (fv_expr expr_) end) field_expr_list)) | (Expr_apply expr1 expr2) => (app (fv_expr expr1) (fv_expr expr2)) | (Expr_and expr1 expr2) => (app (fv_expr expr1) (fv_expr expr2)) | (Expr_or expr1 expr2) => (app (fv_expr expr1) (fv_expr expr2)) | (Expr_field expr5 field5) => ((fv_expr expr5)) | (Expr_ifthenelse expr0 expr1 expr2) => (app (fv_expr expr0) (app (fv_expr expr1) (fv_expr expr2))) | (Expr_while expr1 expr2) => (app (fv_expr expr1) (fv_expr expr2)) | (Expr_for x expr1 for_dirn5 expr2 expr3) => (app (fv_expr expr1) (app (fv_expr expr2) (list_minus eq_value_name (fv_expr expr3) (cons x nil)))) | (Expr_sequence expr1 expr2) => (app (fv_expr expr1) (fv_expr expr2)) | (Expr_match expr5 pattern_matching5) => (app (fv_expr expr5) (fv_pattern_matching pattern_matching5)) | (Expr_function pattern_matching5) => ((fv_pattern_matching pattern_matching5)) | (Expr_try expr5 pattern_matching5) => (app (fv_expr expr5) (fv_pattern_matching pattern_matching5)) | (Expr_let let_binding5 expr5) => (app (fv_let_binding let_binding5) (list_minus eq_value_name (fv_expr expr5) (aux_xs_let_binding_of_let_binding let_binding5))) | (Expr_letrec letrec_bindings5 expr5) => (app (list_minus eq_value_name (fv_letrec_bindings letrec_bindings5) (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings5)) (list_minus eq_value_name (fv_expr expr5) (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings5))) | (Expr_assert expr5) => ((fv_expr expr5)) | (Expr_location location5) => nil end. Fixpoint fl_letrec_binding (letrec_binding5:letrec_binding) : list location := match letrec_binding5 with | (LRB_simple value_name5 pattern_matching5) => ((fl_pattern_matching pattern_matching5)) end with fl_letrec_bindings (letrec_bindings_6:letrec_bindings) : list location := match letrec_bindings_6 with | (LRBs_inj letrec_binding_list) => ((flat_map (fun (letrec_binding_:letrec_binding) => (fl_letrec_binding letrec_binding_)) letrec_binding_list)) end with fl_let_binding (let_binding_6:let_binding) : list location := match let_binding_6 with | (LB_simple pattern5 expr5) => ((fl_expr expr5)) end with fl_pat_exp (pat_exp5:pat_exp) : list location := match pat_exp5 with | (PE_inj pattern5 expr5) => ((fl_expr expr5)) end with fl_pattern_matching (pm5:pattern_matching) : list location := match pm5 with | (PM_pm pat_exp_list) => ((flat_map (fun (pat_exp_:pat_exp) => (fl_pat_exp pat_exp_)) pat_exp_list)) end with fl_expr (e5:expr) : list location := match e5 with | (Expr_uprim unary_prim5) => nil | (Expr_bprim binary_prim5) => nil | (Expr_ident value_name5) => nil | (Expr_constant constant5) => nil | (Expr_typed expr5 typexpr5) => ((fl_expr expr5)) | (Expr_tuple expr_list) => ((flat_map (fun (expr_:expr) => (fl_expr expr_)) expr_list)) | (Expr_construct constr5 expr_list) => ((flat_map (fun (expr_:expr) => (fl_expr expr_)) expr_list)) | (Expr_cons expr1 expr2) => (app (fl_expr expr1) (fl_expr expr2)) | (Expr_record field_expr_list) => ((flat_map (fun (pat_:(field*expr)) => match pat_ with (field_,expr_) => (fl_expr expr_) end) field_expr_list)) | (Expr_override expr_5 field_expr_list) => (app (fl_expr expr_5) (flat_map (fun (pat_:(field*expr)) => match pat_ with (field_,expr_) => (fl_expr expr_) end) field_expr_list)) | (Expr_apply expr1 expr2) => (app (fl_expr expr1) (fl_expr expr2)) | (Expr_and expr1 expr2) => (app (fl_expr expr1) (fl_expr expr2)) | (Expr_or expr1 expr2) => (app (fl_expr expr1) (fl_expr expr2)) | (Expr_field expr5 field5) => ((fl_expr expr5)) | (Expr_ifthenelse expr0 expr1 expr2) => (app (fl_expr expr0) (app (fl_expr expr1) (fl_expr expr2))) | (Expr_while expr1 expr2) => (app (fl_expr expr1) (fl_expr expr2)) | (Expr_for x expr1 for_dirn5 expr2 expr3) => (app (fl_expr expr1) (app (fl_expr expr2) (fl_expr expr3))) | (Expr_sequence expr1 expr2) => (app (fl_expr expr1) (fl_expr expr2)) | (Expr_match expr5 pattern_matching5) => (app (fl_expr expr5) (fl_pattern_matching pattern_matching5)) | (Expr_function pattern_matching5) => ((fl_pattern_matching pattern_matching5)) | (Expr_try expr5 pattern_matching5) => (app (fl_expr expr5) (fl_pattern_matching pattern_matching5)) | (Expr_let let_binding5 expr5) => (app (fl_let_binding let_binding5) (fl_expr expr5)) | (Expr_letrec letrec_bindings5 expr5) => (app (fl_letrec_bindings letrec_bindings5) (fl_expr expr5)) | (Expr_assert expr5) => ((fl_expr expr5)) | (Expr_location location5) => (cons location5 nil) end. Definition ftv_definition (d5:definition) : list typevar := match d5 with | (D_let let_binding5) => ((ftv_let_binding let_binding5)) | (D_letrec letrec_bindings5) => ((ftv_letrec_bindings letrec_bindings5)) | (D_type type_definition5) => ((ftv_type_definition type_definition5)) | (D_exception exception_definition5) => ((ftv_exception_definition exception_definition5)) end. Definition fv_definition (d5:definition) : list value_name := match d5 with | (D_let let_binding5) => ((fv_let_binding let_binding5)) | (D_letrec letrec_bindings5) => ((list_minus eq_value_name (fv_letrec_bindings letrec_bindings5) (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings5))) | (D_type type_definition5) => nil | (D_exception exception_definition5) => nil end. Definition fl_definition (d5:definition) : list location := match d5 with | (D_let let_binding5) => ((fl_let_binding let_binding5)) | (D_letrec letrec_bindings5) => ((fl_letrec_bindings letrec_bindings5)) | (D_type type_definition5) => nil | (D_exception exception_definition5) => nil end. Fixpoint ftv_definitions (ds5:definitions) : list typevar := match ds5 with | Ds_nil => nil | (Ds_cons definition5 definitions5) => (app (ftv_definition definition5) (ftv_definitions definitions5)) end. Definition ftv_typescheme (ts5:typescheme) : list typevar := match ts5 with | (TS_forall typexpr5) => ((ftv_typexpr typexpr5)) end. Definition ftv_typexprs (typexprs_6:typexprs) : list typevar := match typexprs_6 with | (typexprs_inj typexpr_list) => ((flat_map (fun (typexpr_:typexpr) => (ftv_typexpr typexpr_)) typexpr_list)) end. Fixpoint fv_definitions (ds5:definitions) : list value_name := match ds5 with | Ds_nil => nil | (Ds_cons definition5 definitions5) => (app (fv_definition definition5) (list_minus eq_value_name (fv_definitions definitions5) (aux_xs_definition_of_definition definition5))) end. Fixpoint fl_definitions (ds5:definitions) : list location := match ds5 with | Ds_nil => nil | (Ds_cons definition5 definitions5) => (app (fl_definition definition5) (fl_definitions definitions5)) end. Definition ftv_Tsigma (Tsigma_6:Tsigma) : list typevar := match Tsigma_6 with | typevar_typexpr_list => ((flat_map (fun (pat_:(typevar*typexpr)) => match pat_ with (typevar_,typexpr_) => (ftv_typexpr typexpr_) end) typevar_typexpr_list)) end. Definition ftv_substs_x (substs_x_5:substs_x) : list typevar := match substs_x_5 with | (substs_x_xs value_name_expr_list) => ((flat_map (fun (pat_:(value_name*expr)) => match pat_ with (value_name_,expr_) => (ftv_expr expr_) end) value_name_expr_list)) end. Definition ftv_program (program5:program) : list typevar := match program5 with | (Prog_defs definitions5) => ((ftv_definitions definitions5)) | (Prog_raise expr5) => ((ftv_expr expr5)) end. Definition ftv_environment_binding (EB5:environment_binding) : list typevar := match EB5 with | EB_tv => nil | (EB_vn value_name5 typescheme5) => ((ftv_typescheme typescheme5)) | (EB_cc constr_name5 typeconstr5) => nil | (EB_pc constr_name5 type_params_opt5 typexprs5 typeconstr5) => ((list_minus eq_typevar (ftv_typexprs typexprs5) (aux_typevars_type_params_opt_of_type_params_opt type_params_opt5))) | (EB_fn field_name5 type_params_opt5 typeconstr_name5 typexpr5) => ((list_minus eq_typevar (ftv_typexpr typexpr5) (aux_typevars_type_params_opt_of_type_params_opt type_params_opt5))) | (EB_td typeconstr_name5 kind5) => nil | (EB_tr typeconstr_name5 kind5 field_name_list) => (nil) | (EB_ta type_params_opt5 typeconstr_name5 typexpr5) => ((list_minus eq_typevar (ftv_typexpr typexpr5) (aux_typevars_type_params_opt_of_type_params_opt type_params_opt5))) | (EB_l location5 typexpr5) => ((ftv_typexpr typexpr5)) end. Definition ftv_trans_label (L5:trans_label) : list typevar := match L5 with | Lab_nil => nil | (Lab_alloc v location5) => nil | (Lab_deref location5 v) => nil | (Lab_assign location5 v) => nil end. Definition fv_substs_x (substs_x_5:substs_x) : list value_name := match substs_x_5 with | (substs_x_xs value_name_expr_list) => ((flat_map (fun (pat_:(value_name*expr)) => match pat_ with (value_name_,expr_) => (fv_expr expr_) end) value_name_expr_list)) end. Definition fv_program (program5:program) : list value_name := match program5 with | (Prog_defs definitions5) => ((fv_definitions definitions5)) | (Prog_raise expr5) => ((fv_expr expr5)) end. Definition fv_trans_label (L5:trans_label) : list value_name := match L5 with | Lab_nil => nil | (Lab_alloc v location5) => nil | (Lab_deref location5 v) => nil | (Lab_assign location5 v) => nil end. Definition fl_substs_x (substs_x_5:substs_x) : list location := match substs_x_5 with | (substs_x_xs value_name_expr_list) => ((flat_map (fun (pat_:(value_name*expr)) => match pat_ with (value_name_,expr_) => (fl_expr expr_) end) value_name_expr_list)) end. Definition fl_program (program5:program) : list location := match program5 with | (Prog_defs definitions5) => ((fl_definitions definitions5)) | (Prog_raise expr5) => ((fl_expr expr5)) end. Definition fl_trans_label (L5:trans_label) : list location := match L5 with | Lab_nil => nil | (Lab_alloc v location5) => nil | (Lab_deref location5 v) => nil | (Lab_assign location5 v) => nil end. (** substitutions *) Fixpoint substs_typevar_typexpr (sub:list (typevar*typexpr)) (t__6:typexpr) {struct t__6} : typexpr := match t__6 with | (TE_var typevar5) => (match list_assoc eq_typevar typevar5 sub with None => (TE_var typevar5) | Some t_5 => t_5 end) | (TE_idxvar idx5 num) => TE_idxvar idx5 num | TE_any => TE_any | (TE_arrow typexpr1 typexpr2) => TE_arrow (substs_typevar_typexpr sub typexpr1) (substs_typevar_typexpr sub typexpr2) | (TE_tuple typexpr_list) => TE_tuple (map (fun (typexpr_:typexpr) => (substs_typevar_typexpr sub typexpr_)) typexpr_list) | (TE_constr typexpr_list typeconstr5) => TE_constr (map (fun (typexpr_:typexpr) => (substs_typevar_typexpr sub typexpr_)) typexpr_list) typeconstr5 end. Definition substs_typevar_constr_decl (sub:list (typevar*typexpr)) (constr_decl5:constr_decl) : constr_decl := match constr_decl5 with | (CD_nullary constr_name5) => CD_nullary constr_name5 | (CD_nary constr_name5 typexpr_list) => CD_nary constr_name5 (map (fun (typexpr_:typexpr) => (substs_typevar_typexpr sub typexpr_)) typexpr_list) end. Definition substs_typevar_field_decl (sub:list (typevar*typexpr)) (field_decl5:field_decl) : field_decl := match field_decl5 with | (FD_immutable field_name5 typexpr5) => FD_immutable field_name5 (substs_typevar_typexpr sub typexpr5) end. Definition substs_typevar_type_equation (sub:list (typevar*typexpr)) (type_equation5:type_equation) : type_equation := match type_equation5 with | (TE_te typexpr5) => TE_te (substs_typevar_typexpr sub typexpr5) end. Definition substs_typevar_type_representation (sub:list (typevar*typexpr)) (type_representation5:type_representation) : type_representation := match type_representation5 with | (TR_variant constr_decl_list) => TR_variant (map (fun (constr_decl_:constr_decl) => (substs_typevar_constr_decl sub constr_decl_)) constr_decl_list) | (TR_record field_decl_list) => TR_record (map (fun (field_decl_:field_decl) => (substs_typevar_field_decl sub field_decl_)) field_decl_list) end. Definition substs_typevar_type_information (sub:list (typevar*typexpr)) (type_information5:type_information) : type_information := match type_information5 with | (TI_eq type_equation5) => TI_eq (substs_typevar_type_equation sub type_equation5) | (TI_def type_representation5) => TI_def (substs_typevar_type_representation sub type_representation5) end. Fixpoint substs_typevar_pattern (sub:list (typevar*typexpr)) (pat5:pattern) {struct pat5} : pattern := match pat5 with | (P_var value_name5) => P_var value_name5 | P_any => P_any | (P_constant constant5) => P_constant constant5 | (P_alias pattern5 value_name5) => P_alias (substs_typevar_pattern sub pattern5) value_name5 | (P_typed pattern5 typexpr5) => P_typed (substs_typevar_pattern sub pattern5) (substs_typevar_typexpr sub typexpr5) | (P_or pattern1 pattern2) => P_or (substs_typevar_pattern sub pattern1) (substs_typevar_pattern sub pattern2) | (P_construct constr5 pattern_list) => P_construct constr5 (map (fun (pattern_:pattern) => (substs_typevar_pattern sub pattern_)) pattern_list) | (P_construct_any constr5) => P_construct_any constr5 | (P_tuple pattern_list) => P_tuple (map (fun (pattern_:pattern) => (substs_typevar_pattern sub pattern_)) pattern_list) | (P_record field_pattern_list) => P_record (map (fun (pat_:(field*pattern)) => match pat_ with (field_,pattern_) => (field_,(substs_typevar_pattern sub pattern_)) end) field_pattern_list) | (P_cons pattern1 pattern2) => P_cons (substs_typevar_pattern sub pattern1) (substs_typevar_pattern sub pattern2) end. Definition substs_typevar_typedef (sub:list (typevar*typexpr)) (typedef5:typedef) : typedef := match typedef5 with | (TD_td type_params_opt5 typeconstr_name5 type_information5) => TD_td type_params_opt5 typeconstr_name5 (substs_typevar_type_information (list_filter (fun (tmp:typevar*typexpr) => match tmp with (tv5,t5) => negb (list_mem eq_typevar tv5 (aux_typevars_type_params_opt_of_type_params_opt type_params_opt5)) end) sub) type_information5) end. Fixpoint substs_typevar_letrec_binding (sub:list (typevar*typexpr)) (letrec_binding5:letrec_binding) {struct letrec_binding5} : letrec_binding := match letrec_binding5 with | (LRB_simple value_name5 pattern_matching5) => LRB_simple value_name5 (substs_typevar_pattern_matching sub pattern_matching5) end with substs_typevar_letrec_bindings (sub:list (typevar*typexpr)) (letrec_bindings_6:letrec_bindings) {struct letrec_bindings_6} : letrec_bindings := match letrec_bindings_6 with | (LRBs_inj letrec_binding_list) => LRBs_inj (map (fun (letrec_binding_:letrec_binding) => (substs_typevar_letrec_binding sub letrec_binding_)) letrec_binding_list) end with substs_typevar_let_binding (sub:list (typevar*typexpr)) (let_binding_6:let_binding) {struct let_binding_6} : let_binding := match let_binding_6 with | (LB_simple pattern5 expr5) => LB_simple (substs_typevar_pattern sub pattern5) (substs_typevar_expr sub expr5) end with substs_typevar_pat_exp (sub:list (typevar*typexpr)) (pat_exp5:pat_exp) {struct pat_exp5} : pat_exp := match pat_exp5 with | (PE_inj pattern5 expr5) => PE_inj (substs_typevar_pattern sub pattern5) (substs_typevar_expr sub expr5) end with substs_typevar_pattern_matching (sub:list (typevar*typexpr)) (pm5:pattern_matching) {struct pm5} : pattern_matching := match pm5 with | (PM_pm pat_exp_list) => PM_pm (map (fun (pat_exp_:pat_exp) => (substs_typevar_pat_exp sub pat_exp_)) pat_exp_list) end with substs_typevar_expr (sub:list (typevar*typexpr)) (e5:expr) {struct e5} : expr := match e5 with | (Expr_uprim unary_prim5) => Expr_uprim unary_prim5 | (Expr_bprim binary_prim5) => Expr_bprim binary_prim5 | (Expr_ident value_name5) => Expr_ident value_name5 | (Expr_constant constant5) => Expr_constant constant5 | (Expr_typed expr5 typexpr5) => Expr_typed (substs_typevar_expr sub expr5) (substs_typevar_typexpr sub typexpr5) | (Expr_tuple expr_list) => Expr_tuple (map (fun (expr_:expr) => (substs_typevar_expr sub expr_)) expr_list) | (Expr_construct constr5 expr_list) => Expr_construct constr5 (map (fun (expr_:expr) => (substs_typevar_expr sub expr_)) expr_list) | (Expr_cons expr1 expr2) => Expr_cons (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2) | (Expr_record field_expr_list) => Expr_record (map (fun (pat_:(field*expr)) => match pat_ with (field_,expr_) => (field_,(substs_typevar_expr sub expr_)) end) field_expr_list) | (Expr_override expr_5 field_expr_list) => Expr_override (substs_typevar_expr sub expr_5) (map (fun (pat_:(field*expr)) => match pat_ with (field_,expr_) => (field_,(substs_typevar_expr sub expr_)) end) field_expr_list) | (Expr_apply expr1 expr2) => Expr_apply (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2) | (Expr_and expr1 expr2) => Expr_and (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2) | (Expr_or expr1 expr2) => Expr_or (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2) | (Expr_field expr5 field5) => Expr_field (substs_typevar_expr sub expr5) field5 | (Expr_ifthenelse expr0 expr1 expr2) => Expr_ifthenelse (substs_typevar_expr sub expr0) (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2) | (Expr_while expr1 expr2) => Expr_while (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2) | (Expr_for x expr1 for_dirn5 expr2 expr3) => Expr_for x (substs_typevar_expr sub expr1) for_dirn5 (substs_typevar_expr sub expr2) (substs_typevar_expr sub expr3) | (Expr_sequence expr1 expr2) => Expr_sequence (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2) | (Expr_match expr5 pattern_matching5) => Expr_match (substs_typevar_expr sub expr5) (substs_typevar_pattern_matching sub pattern_matching5) | (Expr_function pattern_matching5) => Expr_function (substs_typevar_pattern_matching sub pattern_matching5) | (Expr_try expr5 pattern_matching5) => Expr_try (substs_typevar_expr sub expr5) (substs_typevar_pattern_matching sub pattern_matching5) | (Expr_let let_binding5 expr5) => Expr_let (substs_typevar_let_binding sub let_binding5) (substs_typevar_expr sub expr5) | (Expr_letrec letrec_bindings5 expr5) => Expr_letrec (substs_typevar_letrec_bindings sub letrec_bindings5) (substs_typevar_expr sub expr5) | (Expr_assert expr5) => Expr_assert (substs_typevar_expr sub expr5) | (Expr_location location5) => Expr_location location5 end. Definition substs_typevar_type_definition (sub:list (typevar*typexpr)) (type_definition5:type_definition) : type_definition := match type_definition5 with | (TDF_tdf typedef_list) => TDF_tdf (map (fun (typedef_:typedef) => (substs_typevar_typedef sub typedef_)) typedef_list) end. Definition substs_typevar_exception_definition (sub:list (typevar*typexpr)) (exception_definition5:exception_definition) : exception_definition := match exception_definition5 with | (ED_def constr_decl5) => ED_def (substs_typevar_constr_decl sub constr_decl5) end. Fixpoint substs_value_name_letrec_binding (sub:list (value_name*expr)) (letrec_binding5:letrec_binding) {struct letrec_binding5} : letrec_binding := match letrec_binding5 with | (LRB_simple value_name5 pattern_matching5) => LRB_simple value_name5 (substs_value_name_pattern_matching sub pattern_matching5) end with substs_value_name_letrec_bindings (sub:list (value_name*expr)) (letrec_bindings_6:letrec_bindings) {struct letrec_bindings_6} : letrec_bindings := match letrec_bindings_6 with | (LRBs_inj letrec_binding_list) => LRBs_inj (map (fun (letrec_binding_:letrec_binding) => (substs_value_name_letrec_binding sub letrec_binding_)) letrec_binding_list) end with substs_value_name_let_binding (sub:list (value_name*expr)) (let_binding_6:let_binding) {struct let_binding_6} : let_binding := match let_binding_6 with | (LB_simple pattern5 expr5) => LB_simple pattern5 (substs_value_name_expr sub expr5) end with substs_value_name_pat_exp (sub:list (value_name*expr)) (pat_exp5:pat_exp) {struct pat_exp5} : pat_exp := match pat_exp5 with | (PE_inj pattern5 expr5) => PE_inj pattern5 (substs_value_name_expr (list_filter (fun (tmp:value_name*expr) => match tmp with (x5,e5) => negb (list_mem eq_value_name x5 (aux_xs_pattern_of_pattern pattern5)) end) sub) expr5) end with substs_value_name_pattern_matching (sub:list (value_name*expr)) (pm5:pattern_matching) {struct pm5} : pattern_matching := match pm5 with | (PM_pm pat_exp_list) => PM_pm (map (fun (pat_exp_:pat_exp) => (substs_value_name_pat_exp sub pat_exp_)) pat_exp_list) end with substs_value_name_expr (sub:list (value_name*expr)) (e_6:expr) {struct e_6} : expr := match e_6 with | (Expr_uprim unary_prim5) => Expr_uprim unary_prim5 | (Expr_bprim binary_prim5) => Expr_bprim binary_prim5 | (Expr_ident value_name5) => (match list_assoc eq_value_name value_name5 sub with None => (Expr_ident value_name5) | Some e5 => e5 end) | (Expr_constant constant5) => Expr_constant constant5 | (Expr_typed expr5 typexpr5) => Expr_typed (substs_value_name_expr sub expr5) typexpr5 | (Expr_tuple expr_list) => Expr_tuple (map (fun (expr_:expr) => (substs_value_name_expr sub expr_)) expr_list) | (Expr_construct constr5 expr_list) => Expr_construct constr5 (map (fun (expr_:expr) => (substs_value_name_expr sub expr_)) expr_list) | (Expr_cons expr1 expr2) => Expr_cons (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2) | (Expr_record field_expr_list) => Expr_record (map (fun (pat_:(field*expr)) => match pat_ with (field_,expr_) => (field_,(substs_value_name_expr sub expr_)) end) field_expr_list) | (Expr_override expr_5 field_expr_list) => Expr_override (substs_value_name_expr sub expr_5) (map (fun (pat_:(field*expr)) => match pat_ with (field_,expr_) => (field_,(substs_value_name_expr sub expr_)) end) field_expr_list) | (Expr_apply expr1 expr2) => Expr_apply (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2) | (Expr_and expr1 expr2) => Expr_and (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2) | (Expr_or expr1 expr2) => Expr_or (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2) | (Expr_field expr5 field5) => Expr_field (substs_value_name_expr sub expr5) field5 | (Expr_ifthenelse expr0 expr1 expr2) => Expr_ifthenelse (substs_value_name_expr sub expr0) (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2) | (Expr_while expr1 expr2) => Expr_while (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2) | (Expr_for x expr1 for_dirn5 expr2 expr3) => Expr_for x (substs_value_name_expr sub expr1) for_dirn5 (substs_value_name_expr sub expr2) (substs_value_name_expr (list_filter (fun (tmp:value_name*expr) => match tmp with (x5,e5) => negb (list_mem eq_value_name x5 (cons x nil)) end) sub) expr3) | (Expr_sequence expr1 expr2) => Expr_sequence (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2) | (Expr_match expr5 pattern_matching5) => Expr_match (substs_value_name_expr sub expr5) (substs_value_name_pattern_matching sub pattern_matching5) | (Expr_function pattern_matching5) => Expr_function (substs_value_name_pattern_matching sub pattern_matching5) | (Expr_try expr5 pattern_matching5) => Expr_try (substs_value_name_expr sub expr5) (substs_value_name_pattern_matching sub pattern_matching5) | (Expr_let let_binding5 expr5) => Expr_let (substs_value_name_let_binding sub let_binding5) (substs_value_name_expr (list_filter (fun (tmp:value_name*expr) => match tmp with (x5,e5) => negb (list_mem eq_value_name x5 (aux_xs_let_binding_of_let_binding let_binding5)) end) sub) expr5) | (Expr_letrec letrec_bindings5 expr5) => Expr_letrec (substs_value_name_letrec_bindings (list_filter (fun (tmp:value_name*expr) => match tmp with (x5,e5) => negb (list_mem eq_value_name x5 (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings5)) end) sub) letrec_bindings5) (substs_value_name_expr (list_filter (fun (tmp:value_name*expr) => match tmp with (x5,e5) => negb (list_mem eq_value_name x5 (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings5)) end) sub) expr5) | (Expr_assert expr5) => Expr_assert (substs_value_name_expr sub expr5) | (Expr_location location5) => Expr_location location5 end. Fixpoint subst_value_name_letrec_binding (e5:expr) (x5:value_name) (letrec_binding5:letrec_binding) {struct letrec_binding5} : letrec_binding := match letrec_binding5 with | (LRB_simple value_name5 pattern_matching5) => LRB_simple value_name5 (subst_value_name_pattern_matching e5 x5 pattern_matching5) end with subst_value_name_letrec_bindings (e5:expr) (x5:value_name) (letrec_bindings_6:letrec_bindings) {struct letrec_bindings_6} : letrec_bindings := match letrec_bindings_6 with | (LRBs_inj letrec_binding_list) => LRBs_inj (map (fun (letrec_binding_:letrec_binding) => (subst_value_name_letrec_binding e5 x5 letrec_binding_)) letrec_binding_list) end with subst_value_name_let_binding (e5:expr) (x5:value_name) (let_binding_6:let_binding) {struct let_binding_6} : let_binding := match let_binding_6 with | (LB_simple pattern5 expr5) => LB_simple pattern5 (subst_value_name_expr e5 x5 expr5) end with subst_value_name_pat_exp (e5:expr) (x5:value_name) (pat_exp5:pat_exp) {struct pat_exp5} : pat_exp := match pat_exp5 with | (PE_inj pattern5 expr5) => PE_inj pattern5 (if list_mem eq_value_name x5 (aux_xs_pattern_of_pattern pattern5) then expr5 else (subst_value_name_expr e5 x5 expr5)) end with subst_value_name_pattern_matching (e5:expr) (x5:value_name) (pm5:pattern_matching) {struct pm5} : pattern_matching := match pm5 with | (PM_pm pat_exp_list) => PM_pm (map (fun (pat_exp_:pat_exp) => (subst_value_name_pat_exp e5 x5 pat_exp_)) pat_exp_list) end with subst_value_name_expr (e5:expr) (x5:value_name) (e_6:expr) {struct e_6} : expr := match e_6 with | (Expr_uprim unary_prim5) => Expr_uprim unary_prim5 | (Expr_bprim binary_prim5) => Expr_bprim binary_prim5 | (Expr_ident value_name5) => (if eq_value_name value_name5 x5 then e5 else (Expr_ident value_name5)) | (Expr_constant constant5) => Expr_constant constant5 | (Expr_typed expr5 typexpr5) => Expr_typed (subst_value_name_expr e5 x5 expr5) typexpr5 | (Expr_tuple expr_list) => Expr_tuple (map (fun (expr_:expr) => (subst_value_name_expr e5 x5 expr_)) expr_list) | (Expr_construct constr5 expr_list) => Expr_construct constr5 (map (fun (expr_:expr) => (subst_value_name_expr e5 x5 expr_)) expr_list) | (Expr_cons expr1 expr2) => Expr_cons (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2) | (Expr_record field_expr_list) => Expr_record (map (fun (pat_:(field*expr)) => match pat_ with (field_,expr_) => (field_,(subst_value_name_expr e5 x5 expr_)) end) field_expr_list) | (Expr_override expr_5 field_expr_list) => Expr_override (subst_value_name_expr e5 x5 expr_5) (map (fun (pat_:(field*expr)) => match pat_ with (field_,expr_) => (field_,(subst_value_name_expr e5 x5 expr_)) end) field_expr_list) | (Expr_apply expr1 expr2) => Expr_apply (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2) | (Expr_and expr1 expr2) => Expr_and (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2) | (Expr_or expr1 expr2) => Expr_or (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2) | (Expr_field expr5 field5) => Expr_field (subst_value_name_expr e5 x5 expr5) field5 | (Expr_ifthenelse expr0 expr1 expr2) => Expr_ifthenelse (subst_value_name_expr e5 x5 expr0) (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2) | (Expr_while expr1 expr2) => Expr_while (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2) | (Expr_for x expr1 for_dirn5 expr2 expr3) => Expr_for x (subst_value_name_expr e5 x5 expr1) for_dirn5 (subst_value_name_expr e5 x5 expr2) (if list_mem eq_value_name x5 (cons x nil) then expr3 else (subst_value_name_expr e5 x5 expr3)) | (Expr_sequence expr1 expr2) => Expr_sequence (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2) | (Expr_match expr5 pattern_matching5) => Expr_match (subst_value_name_expr e5 x5 expr5) (subst_value_name_pattern_matching e5 x5 pattern_matching5) | (Expr_function pattern_matching5) => Expr_function (subst_value_name_pattern_matching e5 x5 pattern_matching5) | (Expr_try expr5 pattern_matching5) => Expr_try (subst_value_name_expr e5 x5 expr5) (subst_value_name_pattern_matching e5 x5 pattern_matching5) | (Expr_let let_binding5 expr5) => Expr_let (subst_value_name_let_binding e5 x5 let_binding5) (if list_mem eq_value_name x5 (aux_xs_let_binding_of_let_binding let_binding5) then expr5 else (subst_value_name_expr e5 x5 expr5)) | (Expr_letrec letrec_bindings5 expr5) => Expr_letrec (if list_mem eq_value_name x5 (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings5) then letrec_bindings5 else (subst_value_name_letrec_bindings e5 x5 letrec_bindings5)) (if list_mem eq_value_name x5 (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings5) then expr5 else (subst_value_name_expr e5 x5 expr5)) | (Expr_assert expr5) => Expr_assert (subst_value_name_expr e5 x5 expr5) | (Expr_location location5) => Expr_location location5 end. Definition substs_typevar_definition (sub:list (typevar*typexpr)) (d5:definition) : definition := match d5 with | (D_let let_binding5) => D_let (substs_typevar_let_binding sub let_binding5) | (D_letrec letrec_bindings5) => D_letrec (substs_typevar_letrec_bindings sub letrec_bindings5) | (D_type type_definition5) => D_type (substs_typevar_type_definition sub type_definition5) | (D_exception exception_definition5) => D_exception (substs_typevar_exception_definition sub exception_definition5) end. Definition substs_value_name_definition (sub:list (value_name*expr)) (d5:definition) : definition := match d5 with | (D_let let_binding5) => D_let (substs_value_name_let_binding sub let_binding5) | (D_letrec letrec_bindings5) => D_letrec (substs_value_name_letrec_bindings (list_filter (fun (tmp:value_name*expr) => match tmp with (x5,e5) => negb (list_mem eq_value_name x5 (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings5)) end) sub) letrec_bindings5) | (D_type type_definition5) => D_type type_definition5 | (D_exception exception_definition5) => D_exception exception_definition5 end. Definition subst_value_name_definition (e5:expr) (x5:value_name) (d5:definition) : definition := match d5 with | (D_let let_binding5) => D_let (subst_value_name_let_binding e5 x5 let_binding5) | (D_letrec letrec_bindings5) => D_letrec (if list_mem eq_value_name x5 (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings5) then letrec_bindings5 else (subst_value_name_letrec_bindings e5 x5 letrec_bindings5)) | (D_type type_definition5) => D_type type_definition5 | (D_exception exception_definition5) => D_exception exception_definition5 end. Fixpoint substs_typevar_definitions (sub:list (typevar*typexpr)) (ds5:definitions) {struct ds5} : definitions := match ds5 with | Ds_nil => Ds_nil | (Ds_cons definition5 definitions5) => Ds_cons (substs_typevar_definition sub definition5) (substs_typevar_definitions sub definitions5) end. Definition substs_typevar_typescheme (sub:list (typevar*typexpr)) (ts5:typescheme) : typescheme := match ts5 with | (TS_forall typexpr5) => TS_forall (substs_typevar_typexpr sub typexpr5) end. Definition substs_typevar_typexprs (sub:list (typevar*typexpr)) (typexprs_6:typexprs) : typexprs := match typexprs_6 with | (typexprs_inj typexpr_list) => typexprs_inj (map (fun (typexpr_:typexpr) => (substs_typevar_typexpr sub typexpr_)) typexpr_list) end. Fixpoint substs_value_name_definitions (sub:list (value_name*expr)) (ds5:definitions) {struct ds5} : definitions := match ds5 with | Ds_nil => Ds_nil | (Ds_cons definition5 definitions5) => Ds_cons (substs_value_name_definition sub definition5) (substs_value_name_definitions (list_filter (fun (tmp:value_name*expr) => match tmp with (x5,e5) => negb (list_mem eq_value_name x5 (aux_xs_definition_of_definition definition5)) end) sub) definitions5) end. Fixpoint subst_value_name_definitions (e5:expr) (x5:value_name) (ds5:definitions) {struct ds5} : definitions := match ds5 with | Ds_nil => Ds_nil | (Ds_cons definition5 definitions5) => Ds_cons (subst_value_name_definition e5 x5 definition5) (if list_mem eq_value_name x5 (aux_xs_definition_of_definition definition5) then definitions5 else (subst_value_name_definitions e5 x5 definitions5)) end. Definition substs_typevar_Tsigma (sub:list (typevar*typexpr)) (Tsigma_6:Tsigma) : Tsigma := match Tsigma_6 with | typevar_typexpr_list => Tsigma_substs (map (fun (pat_:(typevar*typexpr)) => match pat_ with (typevar_,typexpr_) => (typevar_,(substs_typevar_typexpr sub typexpr_)) end) typevar_typexpr_list) end. Definition substs_typevar_substs_x (sub:list (typevar*typexpr)) (substs_x_5:substs_x) : substs_x := match substs_x_5 with | (substs_x_xs value_name_expr_list) => substs_x_xs (map (fun (pat_:(value_name*expr)) => match pat_ with (value_name_,expr_) => (value_name_,(substs_typevar_expr sub expr_)) end) value_name_expr_list) end. Definition substs_typevar_program (sub:list (typevar*typexpr)) (program5:program) : program := match program5 with | (Prog_defs definitions5) => Prog_defs (substs_typevar_definitions sub definitions5) | (Prog_raise expr5) => Prog_raise (substs_typevar_expr sub expr5) end. Definition substs_typevar_environment_binding (sub:list (typevar*typexpr)) (EB5:environment_binding) : environment_binding := match EB5 with | EB_tv => EB_tv | (EB_vn value_name5 typescheme5) => EB_vn value_name5 (substs_typevar_typescheme sub typescheme5) | (EB_cc constr_name5 typeconstr5) => EB_cc constr_name5 typeconstr5 | (EB_pc constr_name5 type_params_opt5 typexprs5 typeconstr5) => EB_pc constr_name5 type_params_opt5 (substs_typevar_typexprs (list_filter (fun (tmp:typevar*typexpr) => match tmp with (tv5,t5) => negb (list_mem eq_typevar tv5 (aux_typevars_type_params_opt_of_type_params_opt type_params_opt5)) end) sub) typexprs5) typeconstr5 | (EB_fn field_name5 type_params_opt5 typeconstr_name5 typexpr5) => EB_fn field_name5 type_params_opt5 typeconstr_name5 (substs_typevar_typexpr (list_filter (fun (tmp:typevar*typexpr) => match tmp with (tv5,t5) => negb (list_mem eq_typevar tv5 (aux_typevars_type_params_opt_of_type_params_opt type_params_opt5)) end) sub) typexpr5) | (EB_td typeconstr_name5 kind5) => EB_td typeconstr_name5 kind5 | (EB_tr typeconstr_name5 kind5 field_name_list) => EB_tr typeconstr_name5 kind5 field_name_list | (EB_ta type_params_opt5 typeconstr_name5 typexpr5) => EB_ta type_params_opt5 typeconstr_name5 (substs_typevar_typexpr (list_filter (fun (tmp:typevar*typexpr) => match tmp with (tv5,t5) => negb (list_mem eq_typevar tv5 (aux_typevars_type_params_opt_of_type_params_opt type_params_opt5)) end) sub) typexpr5) | (EB_l location5 typexpr5) => EB_l location5 (substs_typevar_typexpr sub typexpr5) end. Definition substs_typevar_trans_label (sub:list (typevar*typexpr)) (L5:trans_label) : trans_label := match L5 with | Lab_nil => Lab_nil | (Lab_alloc v location5) => Lab_alloc v location5 | (Lab_deref location5 v) => Lab_deref location5 v | (Lab_assign location5 v) => Lab_assign location5 v end. Definition substs_value_name_substs_x (sub:list (value_name*expr)) (substs_x_5:substs_x) : substs_x := match substs_x_5 with | (substs_x_xs value_name_expr_list) => substs_x_xs (map (fun (pat_:(value_name*expr)) => match pat_ with (value_name_,expr_) => (value_name_,(substs_value_name_expr sub expr_)) end) value_name_expr_list) end. Definition substs_value_name_program (sub:list (value_name*expr)) (program5:program) : program := match program5 with | (Prog_defs definitions5) => Prog_defs (substs_value_name_definitions sub definitions5) | (Prog_raise expr5) => Prog_raise (substs_value_name_expr sub expr5) end. Definition substs_value_name_trans_label (sub:list (value_name*expr)) (L5:trans_label) : trans_label := match L5 with | Lab_nil => Lab_nil | (Lab_alloc v location5) => Lab_alloc v location5 | (Lab_deref location5 v) => Lab_deref location5 v | (Lab_assign location5 v) => Lab_assign location5 v end. Definition subst_value_name_substs_x (e5:expr) (x5:value_name) (substs_x_5:substs_x) : substs_x := match substs_x_5 with | (substs_x_xs value_name_expr_list) => substs_x_xs (map (fun (pat_:(value_name*expr)) => match pat_ with (value_name_,expr_) => (value_name_,(subst_value_name_expr e5 x5 expr_)) end) value_name_expr_list) end. Definition subst_value_name_program (e5:expr) (x5:value_name) (program5:program) : program := match program5 with | (Prog_defs definitions5) => Prog_defs (subst_value_name_definitions e5 x5 definitions5) | (Prog_raise expr5) => Prog_raise (subst_value_name_expr e5 x5 expr5) end. Definition subst_value_name_trans_label (e5:expr) (x5:value_name) (L5:trans_label) : trans_label := match L5 with | Lab_nil => Lab_nil | (Lab_alloc v location5) => Lab_alloc v location5 | (Lab_deref location5 v) => Lab_deref location5 v | (Lab_assign location5 v) => Lab_assign location5 v end. Section Definitions_for_homs_and_syntactic_sugar. Set Implicit Arguments. (* Names *) Coercion name_tv : typevar >-> name. Coercion name_vn : value_name >-> name. Coercion name_cn : constr_name >-> name. Coercion name_tcn : typeconstr_name >-> name. Coercion name_fn : field_name >-> name. Coercion name_l : location >-> name. Coercion VP_name : value_name >-> value_path. Coercion C_name : constr_name >-> constr. Coercion TC_name : typeconstr_name >-> typeconstr. Definition names_proj (names:names) := let (l) := names in l. (*-oldlists-*) Coercion names_proj : names >-> list. (*+oldlists+ Coercion names_proj : names >-> list_name. *) (* Integers *) Definition for_dirn_times_intn fd nn := match fd with | FD_upto => nn | FD_downto => (-nn)%Z end. (* Constants *) Coercion CONST_int : intn >-> constant. Definition CONST_int' : Z -> constant := CONST_int. Coercion CONST_int' : Z >-> constant. Definition CONST_bool (b:bool) := if b then CONST_true else CONST_false. Coercion CONST_bool : bool >-> constant. Definition CONST_unit' (_:unit) := CONST_unit. Coercion CONST_unit' : unit >-> constant. (* Types *) Definition TPS_proj (tpo:type_params_opt) := let (tvs) := tpo in tvs. (*-oldlists-*) Coercion TPS_proj : type_params_opt >-> list. (*+oldlists+ Coercion TPS_proj : type_params_opt >-> list_type_param. *) Coercion TE_var : typevar >-> typexpr. Definition TE_constr0 := TE_constr Nil_list_typexpr. Coercion TE_constr0 : typeconstr >-> typexpr. Definition TE_arrown tl t0 := fold_right (fun ti t => TE_arrow ti t) t0 tl. Definition typexprs_proj (tes:typexprs) := let (ts) := tes in ts. (*-oldlists-*) Coercion typexprs_proj : typexprs >-> list. (*+oldlists+ Coercion typexprs_proj : typexprs >-> list_typexpr. *) (* Patterns *) Coercion P_var : value_name >-> pattern. Coercion P_constant : constant >-> pattern. Definition P_list : list pattern -> pattern := fold_right P_cons CONST_nil. (* Expressions *) Coercion Expr_uprim : unary_prim >-> expr. Coercion Expr_bprim : binary_prim >-> expr. Coercion Expr_ident : value_name >-> expr. Coercion Expr_constant : constant >-> expr. Definition Expr_fun (patterns:list pattern) (body:expr) : expr := fold_right (fun p e => Expr_function (PM_pm (make_list_pat_exp (PE_inj p e :: nil)))) body patterns. Definition Expr_multiand : list expr -> expr := fold_right Expr_and (Expr_constant CONST_true). Definition Expr_list : list expr -> expr := fold_right Expr_cons CONST_nil. Definition subst_x x e := substs_x_xs (Cons_list_value_name_expr x e Nil_list_value_name_expr). Definition substs_x_proj (z:substs_x) := let (y) := z in y. (*-oldlists-*) Coercion substs_x_proj : substs_x >-> list. (*+oldlists+ Coercion substs_x_proj : substs_x >-> list_value_name_expr. *) Coercion TE_te : typexpr >-> type_equation. Coercion TI_eq : type_equation >-> type_information. Coercion TI_def : type_representation >-> type_information. Fixpoint STORE_proj (st:store) : list (location*expr) := match st with | STORE_empty => nil | STORE_map st loc e => (loc,e)::(STORE_proj st) end. Coercion STORE_proj : store >-> list. End Definitions_for_homs_and_syntactic_sugar. Notation Expr_applyn := (fun f args => fold_left Expr_apply args f) (only parsing). Notation Expr_apply2 := (fun f arg1 arg2 => Expr_apply (Expr_apply f arg1) arg2) (only parsing). (** definitions *) (**** begin AUTOMATICALLY ADDED DECLARATIONS ****) (**** end AUTOMATICALLY ADDED DECLARATIONS ****) (* * Local Variables: * revert-without-query: ("") * End: *)