(* generated by Ott 0.10.13 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 Ascii. Require Import BinInt. Require String. Require Import Zdiv. Require Import ott_list. 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 := Ascii.ascii. 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 := String.string. 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 := String.string. 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 := String.string. 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 := String.string. 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 := String.string. 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 . Definition idx : Set := nat . 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 := integer_literal . 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 := list (location * expr) . Definition names : Set := list name . Definition environment : Set := (list environment_binding) . Definition Tsigma : Set := list (typevar * typexpr) . 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_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_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. (*** Coercions and syntactic sugar ***) (* Names *) Coercion VP_name : value_name >-> value_path. Coercion C_name : constr_name >-> constr. Coercion TC_name : typeconstr_name >-> typeconstr. (* 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. Coercion TPS_proj : type_params_opt >-> list. Coercion TE_var : typevar >-> typexpr. Definition TE_constr0 := TE_constr nil. Coercion TE_constr0 : typeconstr >-> typexpr. Definition typexprs_proj (tes:typexprs) := let (ts) := tes in ts. Coercion typexprs_proj : typexprs >-> list. (* Patterns *) Coercion P_var : value_name >-> pattern. Coercion P_constant : constant >-> pattern. (* 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 subst_x x e := substs_x_xs (cons (x, e) nil). (* Definitions *) Fixpoint Ds_proj (ds:definitions) : list definition := match ds with | Ds_nil => nil | Ds_cons d dt => cons d (Ds_proj dt) end. Coercion Ds_proj : definitions >-> list. Fixpoint Ds_list (ds:list definition) : definitions := match ds with | nil => Ds_nil | cons d dt => Ds_cons d (Ds_list dt) end. (* Semantic objects *) Definition substs_x_proj (z:substs_x) := let (y) := z in y. Coercion substs_x_proj : substs_x >-> list. Coercion TE_te : typexpr >-> type_equation. Coercion TI_eq : type_equation >-> type_information. Coercion TI_def : type_representation >-> type_information. (*** Strings ***) Section string_literals. Import String. Open Local Scope string_scope. Definition string_equal_functional_value := "equal: functional value". End string_literals. (*** Auxiliary functions ***) Definition fold_pats pats e0 := fold_right (fun p e => Expr_function (PM_pm (PE_inj p e :: nil))) e0 pats. Definition definitions_snoc (ds:definitions) (d:definition) : definitions := Ds_list (ds ++ d :: nil). Fixpoint remv_tyvar_typexpr (t:typexpr) : typexpr := match t with | TE_var tv => TE_any | TE_idxvar k p => TE_idxvar k p | TE_any => TE_any | TE_arrow t1 t2 => TE_arrow (remv_tyvar_typexpr t1) (remv_tyvar_typexpr t2) | TE_tuple ts => TE_tuple (map remv_tyvar_typexpr ts) | TE_constr ts tc => TE_constr (map remv_tyvar_typexpr ts) tc end. Fixpoint remv_tyvar_pattern (p:pattern) : pattern := match p with | P_var vn => P_var vn | P_any => P_any | P_constant c => P_constant c | P_alias p vn => P_alias (remv_tyvar_pattern p) vn | P_typed p t => P_typed (remv_tyvar_pattern p) (remv_tyvar_typexpr t) | P_or p1 p2 => P_or (remv_tyvar_pattern p1) (remv_tyvar_pattern p2) | P_construct cr ps => P_construct cr (map remv_tyvar_pattern ps) | P_construct_any cr => P_construct_any cr | P_tuple ps => P_tuple (map remv_tyvar_pattern ps) | P_record fps => P_record (map (fun tmp => match tmp with (fi,pi) => (fi, remv_tyvar_pattern pi) end) fps) | P_cons p1 p2 => P_cons (remv_tyvar_pattern p1) (remv_tyvar_pattern p2) end. Fixpoint remv_tyvar_letrec_binding (lrb:letrec_binding) : letrec_binding := match lrb with | LRB_simple vn pm => LRB_simple vn (remv_tyvar_pattern_matching pm) end with remv_tyvar_letrec_bindings (lrbs:letrec_bindings) : letrec_bindings := match lrbs with | LRBs_inj lrbs => LRBs_inj (map remv_tyvar_letrec_binding lrbs) end with remv_tyvar_let_binding (lb:let_binding) : let_binding := match lb with | LB_simple p e => LB_simple (remv_tyvar_pattern p) (remv_tyvar_expr e) end with remv_tyvar_pat_exp (pe:pat_exp) : pat_exp := match pe with | PE_inj p e => PE_inj (remv_tyvar_pattern p) (remv_tyvar_expr e) end with remv_tyvar_pattern_matching (pm:pattern_matching) : pattern_matching := match pm with | PM_pm pes => PM_pm (map remv_tyvar_pat_exp pes) end with remv_tyvar_expr (e:expr) : expr := match e with | Expr_uprim uprim => Expr_uprim uprim | Expr_bprim bprim => Expr_bprim bprim | Expr_ident vn => Expr_ident vn | Expr_constant c => Expr_constant c | Expr_typed e t => Expr_typed (remv_tyvar_expr e) (remv_tyvar_typexpr t) | Expr_tuple es => Expr_tuple (map remv_tyvar_expr es) | Expr_construct cr es => Expr_construct cr (map remv_tyvar_expr es) | Expr_cons e1 e2 => Expr_cons (remv_tyvar_expr e1) (remv_tyvar_expr e2) | Expr_record fes => Expr_record (map (fun tmp => match tmp with (fi, ei) => (fi, remv_tyvar_expr ei) end) fes) | Expr_override e fes => Expr_override (remv_tyvar_expr e) (map (fun tmp => match tmp with (fi, ei) => (fi, remv_tyvar_expr ei) end) fes) | Expr_apply e1 e2 => Expr_apply (remv_tyvar_expr e1) (remv_tyvar_expr e2) | Expr_and e1 e2 => Expr_and (remv_tyvar_expr e1) (remv_tyvar_expr e2) | Expr_or e1 e2 => Expr_or (remv_tyvar_expr e1) (remv_tyvar_expr e2) | Expr_field e f => Expr_field (remv_tyvar_expr e) f | Expr_ifthenelse e0 e1 e2 => Expr_ifthenelse (remv_tyvar_expr e0) (remv_tyvar_expr e1) (remv_tyvar_expr e2) | Expr_while e1 e2 => Expr_while (remv_tyvar_expr e1) (remv_tyvar_expr e2) | Expr_for x e1 fdn e2 e3 => Expr_for x (remv_tyvar_expr e1) fdn (remv_tyvar_expr e2) (remv_tyvar_expr e3) | Expr_sequence e1 e2 => Expr_sequence (remv_tyvar_expr e1) (remv_tyvar_expr e2) | Expr_match e pm => Expr_match (remv_tyvar_expr e) (remv_tyvar_pattern_matching pm) | Expr_function pm => Expr_function (remv_tyvar_pattern_matching pm) | Expr_try e pm => Expr_try (remv_tyvar_expr e) (remv_tyvar_pattern_matching pm) | Expr_let lb e => Expr_let (remv_tyvar_let_binding lb) (remv_tyvar_expr e) | Expr_letrec lrbs e => Expr_letrec (remv_tyvar_letrec_bindings lrbs) (remv_tyvar_expr e) | Expr_assert e => Expr_assert (remv_tyvar_expr e) | Expr_location loc => Expr_location loc end. (*** De Bruijn indices ***) Fixpoint shiftt (m n:nat) (te:typexpr) {struct te} : typexpr := match te with | TE_var tv => TE_var tv | TE_idxvar k p => TE_idxvar (if le_lt_dec m k then n + k else k) p | TE_any => TE_any | TE_arrow te1 te2 => TE_arrow (shiftt m n te1) (shiftt m n te2) | TE_tuple tes => TE_tuple (map (shiftt m n) tes) | TE_constr tes tc => TE_constr (map (shiftt m n) tes) tc end. Definition shifttes m n (tes:typexprs) := typexprs_inj (map (shiftt m n) tes). Definition shiftts m n (ts:typescheme) := match ts with | TS_forall te => TS_forall (shiftt (S m) n te) end. Definition shiftEB m n (EB:environment_binding) := match EB with | EB_tv => EB_tv | EB_vn vn ts => EB_vn vn (shiftts m n ts) | EB_cc cn tc => EB_cc cn tc | EB_pc cn tpo tes tc => EB_pc cn tpo (shifttes m n tes) tc | EB_fn fn tpo tcn te => EB_fn fn tpo tcn (shiftt m n te) | EB_td tcn K => EB_td tcn K | EB_tr tcn K fns => EB_tr tcn K fns | EB_ta tpo tcn te => EB_ta tpo tcn (shiftt m n te) | EB_l loc te => EB_l loc (shiftt m n te) end. Fixpoint count_E_typevars E := match E with | nil => 0 | EB_tv :: E' => S (count_E_typevars E') | _ :: E' => count_E_typevars E' end. Fixpoint shiftE (m n:nat) (E:environment) {struct E} : environment := match E with | nil => nil | EB :: E' => shiftEB (count_E_typevars E + m) n EB :: shiftE m n E' end. Definition shiftTsig m n (sigma:Tsigma) := map (fun tmp => match tmp with (tv, t) => (tv, shiftt m n t) end) sigma. (** definitions *) (* defns JdomEB *) Inductive (* defn domEB *) JdomEB : environment_binding -> name -> Prop := | JdomEB_type_param : JdomEB EB_tv name_tv | JdomEB_value_name : forall (value_name5:value_name) (typescheme5:typescheme), JdomEB (EB_vn value_name5 typescheme5) (name_vn value_name5) | JdomEB_const_constr_name : forall (constr_name5:constr_name) (typeconstr5:typeconstr), JdomEB (EB_cc constr_name5 typeconstr5) (name_cn constr_name5) | JdomEB_constr_name : forall (t_list:list typexpr) (constr_name5:constr_name) (type_params_opt5:type_params_opt) (typeconstr5:typeconstr), JdomEB (EB_pc constr_name5 type_params_opt5 (typexprs_inj t_list) typeconstr5) (name_cn constr_name5) | JdomEB_opaque_typeconstr_name : forall (typeconstr_name5:typeconstr_name) (kind5:kind), JdomEB (EB_td typeconstr_name5 kind5) (name_tcn typeconstr_name5) | JdomEB_trans_typeconstr_name : forall (type_params_opt5:type_params_opt) (typeconstr_name5:typeconstr_name) (t:typexpr), JdomEB (EB_ta type_params_opt5 typeconstr_name5 t) (name_tcn typeconstr_name5) | JdomEB_record_typeconstr_name : forall (field_name_list:list field_name) (typeconstr_name5:typeconstr_name) (kind5:kind), JdomEB (EB_tr typeconstr_name5 kind5 field_name_list) (name_tcn typeconstr_name5) | JdomEB_record_field_name : forall (field_name5:field_name) (type_params_opt5:type_params_opt) (typeconstr_name5:typeconstr_name) (typexpr5:typexpr), JdomEB (EB_fn field_name5 type_params_opt5 typeconstr_name5 typexpr5) (name_fn field_name5) | JdomEB_location : forall (location5:location) (t:typexpr), JdomEB (EB_l location5 t) (name_l location5) . (* defns JdomE *) Inductive (* defn domE *) JdomE : environment -> names -> Prop := | JdomE_empty : JdomE (@nil environment_binding) nil | JdomE_cons : forall (name_list:list name) (E:environment) (EB:environment_binding) (name_5:name), JdomE E name_list -> JdomEB EB name_5 -> JdomE (cons EB E ) ((app (cons name_5 nil) (app name_list nil))) . (* defns Jlookup *) Inductive (* defn EB *) Jlookup_EB : environment -> name -> environment_binding -> Prop := | Jlookup_EB_rec1 : forall (E:environment) (EB:environment_binding) (name5:name) (EB':environment_binding) (name':name), JdomEB EB name' -> (~( name5 = name' )) -> (~( name' = name_tv )) -> Jlookup_EB E name5 EB' -> Jlookup_EB (cons EB E ) name5 EB' | Jlookup_EB_rec2 : forall (E:environment) (name5:name) (EB':environment_binding), (~( name5 = name_tv )) -> Jlookup_EB E name5 EB' -> Jlookup_EB (cons EB_tv E ) name5 (shiftEB 0 1 EB' ) | Jlookup_EB_head : forall (E:environment) (EB:environment_binding) (name5:name), JdomEB EB name5 -> Jlookup_EB (cons EB E ) name5 EB . (* defns Jidx *) Inductive (* defn bound *) Jidx_bound : environment -> idx -> Prop := | Jidx_bound_skip1 : forall (E:environment) (EB:environment_binding) (idx5:idx) (name5:name), Jidx_bound E idx5 -> JdomEB EB name5 -> (~( name5 = name_tv )) -> Jidx_bound (cons EB E ) idx5 | Jidx_bound_skip2 : forall (E:environment) (idx5:idx), Jidx_bound E idx5 -> Jidx_bound (cons EB_tv E ) ( idx5 + 1 ) | Jidx_bound_found : forall (E:environment), Jidx_bound (cons EB_tv E ) 0 . (* defns JTtps_kind *) Inductive (* defn tps_kind *) JTtps_kind : type_params_opt -> kind -> Prop := | JTtps_kind_kind : forall (tp_list:list type_param) (n:index), (NoDup tp_list ) -> ( n = length tp_list ) -> JTtps_kind (TPS_nary tp_list) n . (* defns JTEok *) Inductive (* defn Eok *) JTEok : environment -> Prop := | JTEok_empty : JTEok (@nil environment_binding) | JTEok_typevar : forall (E:environment), JTEok E -> JTEok (cons EB_tv E ) | JTEok_value_name : forall (E:environment) (value_name5:value_name) (t:typexpr), JTts E (TS_forall t) 0 -> JTEok (cons (EB_vn value_name5 (TS_forall t)) E ) | JTEok_constr_name_c : forall (E:environment) (constr_name5:constr_name) (typeconstr_name5:typeconstr_name) (kind5:kind) (names5:names), JTEok E -> Jlookup_EB E (name_tcn typeconstr_name5) (EB_td typeconstr_name5 kind5) -> JdomE E names5 -> (~In (name_cn constr_name5) names5 ) -> JTEok (cons (EB_cc constr_name5 (TC_name typeconstr_name5)) E ) | JTEok_exn_constr_name_c : forall (E:environment) (constr_name5:constr_name) (names5:names), JTEok E -> JdomE E names5 -> (~In (name_cn constr_name5) names5 ) -> JTEok (cons (EB_cc constr_name5 TC_exn) E ) | JTEok_constr_name_p : forall (t_list:list typexpr) (tv_list:list typevar) (E:environment) (constr_name5:constr_name) (typeconstr_name5:typeconstr_name) (type_params_opt5:type_params_opt) (m:index) (names5:names), ( type_params_opt5 = (TPS_nary (map (fun (tv_:typevar) => (TP_var tv_)) tv_list)) ) -> (forall (t_:typexpr), In (E,type_params_opt5,t_, 0 ) (map (fun (t_:typexpr) => (E,type_params_opt5,t_, 0 )) t_list) -> (JTtsnamed E type_params_opt5 t_ 0 )) -> Jlookup_EB E (name_tcn typeconstr_name5) (EB_td typeconstr_name5 m ) -> JdomE E names5 -> (~In (name_cn constr_name5) names5 ) -> (length t_list >= 1 ) -> ( m = length (map (fun (tv_:typevar) => (TP_var tv_)) tv_list) ) -> JTEok (cons (EB_pc constr_name5 (TPS_nary (map (fun (tv_:typevar) => (TP_var tv_)) tv_list)) (typexprs_inj t_list) (TC_name typeconstr_name5)) E ) | JTEok_exn_constr_name_p : forall (t_list:list typexpr) (E:environment) (constr_name5:constr_name) (names5:names), (forall (t_:typexpr), In (E,t_, 0 ) (map (fun (t_:typexpr) => (E,t_, 0 )) t_list) -> (JTt E t_ 0 )) -> JdomE E names5 -> (~In (name_cn constr_name5) names5 ) -> (length t_list >= 1 ) -> JTEok (cons (EB_pc constr_name5 (TPS_nary nil) (typexprs_inj t_list) TC_exn) E ) | JTEok_record_destr : forall (field_name_list:list field_name) (tv_list:list typevar) (E:environment) (field_name_5:field_name) (typeconstr_name5:typeconstr_name) (t:typexpr) (names5:names) (m:index), JTtsnamed E (TPS_nary (map (fun (tv_:typevar) => (TP_var tv_)) tv_list)) t 0 -> JdomE E names5 -> (~In (name_fn field_name_5) names5 ) -> Jlookup_EB E (name_tcn typeconstr_name5) (EB_tr typeconstr_name5 m field_name_list) -> ( m = length (map (fun (tv_:typevar) => (TP_var tv_)) tv_list) ) -> (In field_name_5 field_name_list ) -> JTEok (cons (EB_fn field_name_5 (TPS_nary (map (fun (tv_:typevar) => (TP_var tv_)) tv_list)) typeconstr_name5 t) E ) | JTEok_typeconstr_name : forall (E:environment) (typeconstr_name5:typeconstr_name) (kind5:kind) (names5:names), JTEok E -> JdomE E names5 -> (~In (name_tcn typeconstr_name5) names5 ) -> JTEok (cons (EB_td typeconstr_name5 kind5) E ) | JTEok_typeconstr_eqn : forall (tv_list:list typevar) (E:environment) (typeconstr_name5:typeconstr_name) (t:typexpr) (names5:names), JdomE E names5 -> (~In (name_tcn typeconstr_name5) names5 ) -> JTtsnamed E (TPS_nary (map (fun (tv_:typevar) => (TP_var tv_)) tv_list)) t 0 -> JTEok (cons (EB_ta (TPS_nary (map (fun (tv_:typevar) => (TP_var tv_)) tv_list)) typeconstr_name5 t) E ) | JTEok_typeconstr_record : forall (field_name_list:list field_name) (E:environment) (typeconstr_name5:typeconstr_name) (kind5:kind) (names5:names), JTEok E -> JdomE E names5 -> (~In (name_tcn typeconstr_name5) names5 ) -> (NoDup (map (fun (field_name_:field_name) => (name_fn field_name_)) field_name_list) ) -> JTEok (cons (EB_tr typeconstr_name5 kind5 field_name_list) E ) | JTEok_location : forall (E:environment) (location5:location) (t:typexpr) (names5:names), JTt E t 0 -> JdomE E names5 -> (~In (name_l location5) names5 ) -> JTEok (cons (EB_l location5 t) E ) with (* defn typeconstr *) JTtypeconstr : environment -> typeconstr -> kind -> Prop := | JTtypeconstr_abstract : forall (E:environment) (typeconstr_name5:typeconstr_name) (kind5:kind), JTEok E -> Jlookup_EB E (name_tcn typeconstr_name5) (EB_td typeconstr_name5 kind5) -> JTtypeconstr E (TC_name typeconstr_name5) kind5 | JTtypeconstr_concrete : forall (E:environment) (typeconstr_name5:typeconstr_name) (kind5:kind) (type_params_opt5:type_params_opt) (t:typexpr), JTEok E -> Jlookup_EB E (name_tcn typeconstr_name5) (EB_ta type_params_opt5 typeconstr_name5 t) -> JTtps_kind type_params_opt5 kind5 -> JTtypeconstr E (TC_name typeconstr_name5) kind5 | JTtypeconstr_record : forall (field_name_list:list field_name) (E:environment) (typeconstr_name5:typeconstr_name) (kind5:kind), JTEok E -> Jlookup_EB E (name_tcn typeconstr_name5) (EB_tr typeconstr_name5 kind5 field_name_list) -> JTtypeconstr E (TC_name typeconstr_name5) kind5 | JTtypeconstr_int : forall (E:environment), JTEok E -> JTtypeconstr E TC_int 0 | JTtypeconstr_char : forall (E:environment), JTEok E -> JTtypeconstr E TC_char 0 | JTtypeconstr_string : forall (E:environment), JTEok E -> JTtypeconstr E TC_string 0 | JTtypeconstr_float : forall (E:environment), JTEok E -> JTtypeconstr E TC_float 0 | JTtypeconstr_bool : forall (E:environment), JTEok E -> JTtypeconstr E TC_bool 0 | JTtypeconstr_unit : forall (E:environment), JTEok E -> JTtypeconstr E TC_unit 0 | JTtypeconstr_exn : forall (E:environment), JTEok E -> JTtypeconstr E TC_exn 0 | JTtypeconstr_list : forall (E:environment), JTEok E -> JTtypeconstr E TC_list 1 | JTtypeconstr_option : forall (E:environment), JTEok E -> JTtypeconstr E TC_option 1 | JTtypeconstr_ref : forall (E:environment), JTEok E -> JTtypeconstr E TC_ref 1 with (* defn ts *) JTts : environment -> typescheme -> kind -> Prop := | JTts_forall : forall (E:environment) (t:typexpr), JTt (cons EB_tv E ) t 0 -> JTts E (TS_forall t) 0 with (* defn tsnamed *) JTtsnamed : environment -> type_params_opt -> typexpr -> kind -> Prop := | JTtsnamed_forall : forall (tv_list:list typevar) (E:environment) (t:typexpr), JTt E (substs_typevar_typexpr (map (fun (tv_:typevar) => (tv_, (TE_constr nil TC_unit ) )) tv_list) t ) 0 -> (NoDup (map (fun (tv_:typevar) => (TP_var tv_)) tv_list) ) -> JTtsnamed E (TPS_nary (map (fun (tv_:typevar) => (TP_var tv_)) tv_list)) t 0 with (* defn t *) JTt : environment -> typexpr -> kind -> Prop := | JTt_var : forall (E:environment) (idx5:idx) (num:idx), JTEok E -> Jidx_bound E idx5 -> JTt E (TE_idxvar idx5 num) 0 | JTt_arrow : forall (E:environment) (t:typexpr) (t':typexpr), JTt E t 0 -> JTt E t' 0 -> JTt E (TE_arrow t t') 0 | JTt_tuple : forall (t_list:list typexpr) (E:environment), (forall (t_:typexpr), In (E,t_, 0 ) (map (fun (t_:typexpr) => (E,t_, 0 )) t_list) -> (JTt E t_ 0 )) -> (length t_list >= 2 ) -> JTt E (TE_tuple t_list) 0 | JTt_constr : forall (t_list:list typexpr) (E:environment) (typeconstr5:typeconstr) (n:index), JTtypeconstr E typeconstr5 n -> (forall (t_:typexpr), In (E,t_, 0 ) (map (fun (t_:typexpr) => (E,t_, 0 )) t_list) -> (JTt E t_ 0 )) -> ( n = length t_list ) -> JTt E (TE_constr t_list typeconstr5) 0 . (* defns JTeq *) Inductive (* defn eq *) JTeq : environment -> typexpr -> typexpr -> Prop := | JTeq_refl : forall (E:environment) (t:typexpr), JTt E t 0 -> JTeq E t t | JTeq_sym : forall (E:environment) (t:typexpr) (t':typexpr), JTeq E t' t -> JTeq E t t' | JTeq_trans : forall (E:environment) (t:typexpr) (t'':typexpr) (t':typexpr), JTeq E t t' -> JTeq E t' t'' -> JTeq E t t'' | JTeq_expand : forall (t_typevar_list:list (typexpr*typevar)) (E:environment) (typeconstr_name5:typeconstr_name) (t:typexpr), JTEok E -> Jlookup_EB E (name_tcn typeconstr_name5) (EB_ta (TPS_nary (map (fun (pat_:(typexpr*typevar)) => match pat_ with (t_,typevar_) => (TP_var typevar_) end ) t_typevar_list)) typeconstr_name5 t) -> (forall (t_:typexpr), In (E,t_, 0 ) (map (fun (pat_:typexpr*typevar) => match pat_ with (t_,typevar_) => (E,t_, 0 ) end) t_typevar_list) -> (JTt E t_ 0 )) -> JTeq E (TE_constr (map (fun (pat_:(typexpr*typevar)) => match pat_ with (t_,typevar_) => t_ end ) t_typevar_list) (TC_name typeconstr_name5)) (substs_typevar_typexpr (map (fun (pat_:(typexpr*typevar)) => match pat_ with (t_,typevar_) => (typevar_,t_) end ) t_typevar_list) t ) | JTeq_arrow : forall (E:environment) (t1:typexpr) (t2:typexpr) (t1':typexpr) (t2':typexpr), JTeq E t1 t1' -> JTeq E t2 t2' -> JTeq E (TE_arrow t1 t2) (TE_arrow t1' t2') | JTeq_tuple : forall (t_t'_list:list (typexpr*typexpr)) (E:environment), (forall (t_:typexpr) (t_':typexpr), In (E,t_,t_') (map (fun (pat_:typexpr*typexpr) => match pat_ with (t_,t_') => (E,t_,t_') end) t_t'_list) -> (JTeq E t_ t_')) -> (length (map (fun (pat_:(typexpr*typexpr)) => match pat_ with (t_,t_') => t_ end ) t_t'_list) >= 2 ) -> JTeq E (TE_tuple (map (fun (pat_:(typexpr*typexpr)) => match pat_ with (t_,t_') => t_ end ) t_t'_list)) (TE_tuple (map (fun (pat_:(typexpr*typexpr)) => match pat_ with (t_,t_') => t_' end ) t_t'_list)) | JTeq_constr : forall (t_t'_list:list (typexpr*typexpr)) (E:environment) (typeconstr5:typeconstr) (n:index), JTtypeconstr E typeconstr5 n -> (forall (t_:typexpr) (t_':typexpr), In (E,t_,t_') (map (fun (pat_:typexpr*typexpr) => match pat_ with (t_,t_') => (E,t_,t_') end) t_t'_list) -> (JTeq E t_ t_')) -> ( n = length (map (fun (pat_:(typexpr*typexpr)) => match pat_ with (t_,t_') => t_ end ) t_t'_list) ) -> JTeq E (TE_constr (map (fun (pat_:(typexpr*typexpr)) => match pat_ with (t_,t_') => t_ end ) t_t'_list) typeconstr5) (TE_constr (map (fun (pat_:(typexpr*typexpr)) => match pat_ with (t_,t_') => t_' end ) t_t'_list) typeconstr5) . (* defns JTidxsub *) Inductive (* defn idxsub *) JTidxsub : list typexpr -> typexpr -> typexpr -> Prop := | JTinxsub_alpha : forall (t_list:list typexpr) (typevar5:typevar), JTidxsub t_list (TE_var typevar5) (TE_var typevar5) | JTinxsub_idx0 : forall (t''_list:list typexpr) (t_list:list typexpr) (t':typexpr) (num:idx), ( num = length t_list ) -> JTidxsub ((app t_list (app (cons t' nil) (app t''_list nil)))) (TE_idxvar 0 num) t' | JTinxsub_idx1 : forall (t_list:list typexpr) (num:idx), (length t_list <= num ) -> JTidxsub t_list (TE_idxvar 0 num) (TE_constr nil TC_unit ) | JTinxsub_idx2 : forall (t_list:list typexpr) (idx5:idx) (num:idx), JTidxsub t_list (TE_idxvar ( idx5 + 1 ) num) (TE_idxvar idx5 num) | JTinxsub_any : forall (t_list:list typexpr), JTidxsub t_list TE_any TE_any | JTinxsub_arrow : forall (t_list:list typexpr) (t1':typexpr) (t2':typexpr) (t1'':typexpr) (t2'':typexpr), JTidxsub t_list t1' t1'' -> JTidxsub t_list t2' t2'' -> JTidxsub t_list (TE_arrow t1' t2') (TE_arrow t1'' t2'') | JTinxsub_tuple : forall (t'_t''_list:list (typexpr*typexpr)) (t_list:list typexpr), (forall (t_':typexpr) (t_'':typexpr), In (t_list,t_',t_'') (map (fun (pat_:typexpr*typexpr) => match pat_ with (t_',t_'') => (t_list,t_',t_'') end) t'_t''_list) -> (JTidxsub t_list t_' t_'')) -> JTidxsub t_list (TE_tuple (map (fun (pat_:(typexpr*typexpr)) => match pat_ with (t_',t_'') => t_' end ) t'_t''_list)) (TE_tuple (map (fun (pat_:(typexpr*typexpr)) => match pat_ with (t_',t_'') => t_'' end ) t'_t''_list)) | JTinxsub_tc : forall (t'_t''_list:list (typexpr*typexpr)) (t_list:list typexpr) (typeconstr5:typeconstr), (forall (t_':typexpr) (t_'':typexpr), In (t_list,t_',t_'') (map (fun (pat_:typexpr*typexpr) => match pat_ with (t_',t_'') => (t_list,t_',t_'') end) t'_t''_list) -> (JTidxsub t_list t_' t_'')) -> JTidxsub t_list (TE_constr (map (fun (pat_:(typexpr*typexpr)) => match pat_ with (t_',t_'') => t_' end ) t'_t''_list) typeconstr5) (TE_constr (map (fun (pat_:(typexpr*typexpr)) => match pat_ with (t_',t_'') => t_'' end ) t'_t''_list) typeconstr5) . (* defns JTinst *) Inductive (* defn inst *) JTinst : environment -> typexpr -> typescheme -> Prop := | JTinst_idx : forall (t_list:list typexpr) (E:environment) (t'':typexpr) (t':typexpr), JTts E (TS_forall t') 0 -> (forall (t_:typexpr), In (E,t_, 0 ) (map (fun (t_:typexpr) => (E,t_, 0 )) t_list) -> (JTt E t_ 0 )) -> JTidxsub t_list t' t'' -> JTinst E t'' (TS_forall t') . (* defns JTinst_named *) Inductive (* defn inst_named *) JTinst_named : environment -> typexpr -> type_params_opt -> typexpr -> Prop := | JTinst_named_named : forall (typevar_t_list:list (typevar*typexpr)) (E:environment) (t:typexpr), JTtsnamed E (TPS_nary (map (fun (pat_:(typevar*typexpr)) => match pat_ with (typevar_,t_) => (TP_var typevar_) end ) typevar_t_list)) t 0 -> (forall (t_:typexpr), In (E,t_, 0 ) (map (fun (pat_:typevar*typexpr) => match pat_ with (typevar_,t_) => (E,t_, 0 ) end) typevar_t_list) -> (JTt E t_ 0 )) -> JTinst_named E (substs_typevar_typexpr typevar_t_list t ) (TPS_nary (map (fun (pat_:(typevar*typexpr)) => match pat_ with (typevar_,t_) => (TP_var typevar_) end ) typevar_t_list)) t . (* defns JTinst_any *) Inductive (* defn inst_any *) JTinst_any : environment -> typexpr -> typexpr -> Prop := | JTinst_any_tyvar : forall (E:environment) (idx5:idx) (num:idx), JTt E (TE_idxvar idx5 num) 0 -> JTinst_any E (TE_idxvar idx5 num) (TE_idxvar idx5 num) | JTinst_any_any : forall (E:environment) (t:typexpr), JTt E t 0 -> JTinst_any E t TE_any | JTinst_any_arrow : forall (E:environment) (t1:typexpr) (t2:typexpr) (t1':typexpr) (t2':typexpr), JTinst_any E t1 t1' -> JTinst_any E t2 t2' -> JTinst_any E (TE_arrow t1 t2) (TE_arrow t1' t2') | JTinst_any_tuple : forall (t_t'_list:list (typexpr*typexpr)) (E:environment), (forall (t_:typexpr) (t_':typexpr), In (E,t_,t_') (map (fun (pat_:typexpr*typexpr) => match pat_ with (t_,t_') => (E,t_,t_') end) t_t'_list) -> (JTinst_any E t_ t_')) -> (length (map (fun (pat_:(typexpr*typexpr)) => match pat_ with (t_,t_') => t_ end ) t_t'_list) >= 2 ) -> JTinst_any E (TE_tuple (map (fun (pat_:(typexpr*typexpr)) => match pat_ with (t_,t_') => t_ end ) t_t'_list)) (TE_tuple (map (fun (pat_:(typexpr*typexpr)) => match pat_ with (t_,t_') => t_' end ) t_t'_list)) | JTinst_any_ctor : forall (t_t'_list:list (typexpr*typexpr)) (E:environment) (typeconstr5:typeconstr) (n:index), (forall (t_:typexpr) (t_':typexpr), In (E,t_,t_') (map (fun (pat_:typexpr*typexpr) => match pat_ with (t_,t_') => (E,t_,t_') end) t_t'_list) -> (JTinst_any E t_ t_')) -> JTtypeconstr E typeconstr5 n -> ( n = length (map (fun (pat_:(typexpr*typexpr)) => match pat_ with (t_,t_') => t_ end ) t_t'_list) ) -> JTinst_any E (TE_constr (map (fun (pat_:(typexpr*typexpr)) => match pat_ with (t_,t_') => t_ end ) t_t'_list) typeconstr5) (TE_constr (map (fun (pat_:(typexpr*typexpr)) => match pat_ with (t_,t_') => t_' end ) t_t'_list) typeconstr5) . (* defns JTval *) Inductive (* defn value_name *) JTvalue_name : environment -> value_name -> typexpr -> Prop := | JTvalue_name_value_name : forall (E:environment) (value_name5:value_name) (t:typexpr) (ts:typescheme), Jlookup_EB E (name_vn value_name5) (EB_vn value_name5 ts) -> JTinst E t ts -> JTvalue_name E value_name5 t . (* defns JTfield *) Inductive (* defn field *) JTfield : environment -> field_name -> typexpr -> typexpr -> Prop := | JTfield_name : forall (t'_tv_list:list (typexpr*typevar)) (E:environment) (field_name5:field_name) (typeconstr_name5:typeconstr_name) (t'':typexpr) (t:typexpr), Jlookup_EB E (name_fn field_name5) (EB_fn field_name5 (TPS_nary (map (fun (pat_:(typexpr*typevar)) => match pat_ with (t_',tv_) => (TP_var tv_) end ) t'_tv_list)) typeconstr_name5 t) -> JTinst_named E (TE_arrow (TE_constr (map (fun (pat_:(typexpr*typevar)) => match pat_ with (t_',tv_) => t_' end ) t'_tv_list) (TC_name typeconstr_name5)) t'') (TPS_nary (map (fun (pat_:(typexpr*typevar)) => match pat_ with (t_',tv_) => (TP_var tv_) end ) t'_tv_list)) (TE_arrow (TE_constr (map (fun (pat_:(typexpr*typevar)) => match pat_ with (t_',tv_) => (TE_var tv_) end ) t'_tv_list) (TC_name typeconstr_name5)) t) -> JTfield E field_name5 (TE_constr (map (fun (pat_:(typexpr*typevar)) => match pat_ with (t_',tv_) => t_' end ) t'_tv_list) (TC_name typeconstr_name5)) t'' . (* defns JTconstr_p *) Inductive (* defn constr_p *) JTconstr_p : environment -> constr -> list typexpr -> typexpr -> Prop := | JTconstr_p_name : forall (t'_t_list:list (typexpr*typexpr)) (t''_tv_list:list (typexpr*typevar)) (E:environment) (constr_name5:constr_name) (typeconstr5:typeconstr), Jlookup_EB E (name_cn constr_name5) (EB_pc constr_name5 (TPS_nary (map (fun (pat_:(typexpr*typevar)) => match pat_ with (t_'',tv_) => (TP_var tv_) end ) t''_tv_list)) (typexprs_inj (map (fun (pat_:(typexpr*typexpr)) => match pat_ with (t_',t_) => t_ end ) t'_t_list)) typeconstr5) -> JTinst_named E (TE_arrow (TE_tuple (map (fun (pat_:(typexpr*typexpr)) => match pat_ with (t_',t_) => t_' end ) t'_t_list)) (TE_constr (map (fun (pat_:(typexpr*typevar)) => match pat_ with (t_'',tv_) => t_'' end ) t''_tv_list) typeconstr5)) (TPS_nary (map (fun (pat_:(typexpr*typevar)) => match pat_ with (t_'',tv_) => (TP_var tv_) end ) t''_tv_list)) (TE_arrow (TE_tuple (map (fun (pat_:(typexpr*typexpr)) => match pat_ with (t_',t_) => t_ end ) t'_t_list)) (TE_constr (map (fun (pat_:(typexpr*typevar)) => match pat_ with (t_'',tv_) => (TE_var tv_) end ) t''_tv_list) typeconstr5)) -> JTconstr_p E (C_name constr_name5) (map (fun (pat_:(typexpr*typexpr)) => match pat_ with (t_',t_) => t_' end ) t'_t_list) (TE_constr (map (fun (pat_:(typexpr*typevar)) => match pat_ with (t_'',tv_) => t_'' end ) t''_tv_list) typeconstr5) | JTconstr_p_invarg : forall (E:environment), JTEok E -> JTconstr_p E C_invalidargument (cons (TE_constr nil TC_string ) nil) (TE_constr nil TC_exn ) | JTconstr_p_some : forall (E:environment) (t:typexpr), JTt E t 0 -> JTconstr_p E C_some (cons t nil) (TE_constr (cons t nil) TC_option ) . (* defns JTconstr_c *) Inductive (* defn constr_c *) JTconstr_c : environment -> constr -> typexpr -> Prop := | JTconstr_c_constr : forall (t_list:list typexpr) (E:environment) (constr_name5:constr_name) (typeconstr_name5:typeconstr_name) (n:index), JTEok E -> Jlookup_EB E (name_cn constr_name5) (EB_cc constr_name5 (TC_name typeconstr_name5)) -> Jlookup_EB E (name_tcn typeconstr_name5) (EB_td typeconstr_name5 n ) -> (forall (t_:typexpr), In (E,t_, 0 ) (map (fun (t_:typexpr) => (E,t_, 0 )) t_list) -> (JTt E t_ 0 )) -> ( n = length t_list ) -> JTconstr_c E (C_name constr_name5) (TE_constr t_list (TC_name typeconstr_name5)) | JTconstr_c_exn_constr : forall (E:environment) (constr_name5:constr_name), JTEok E -> Jlookup_EB E (name_cn constr_name5) (EB_cc constr_name5 TC_exn) -> JTconstr_c E (C_name constr_name5) (TE_constr nil TC_exn ) | JTconstr_c_notfound : forall (E:environment), JTEok E -> JTconstr_c E C_notfound (TE_constr nil TC_exn ) | JTconstr_c_assert_fail : forall (E:environment), JTEok E -> JTconstr_c E C_assertfailure (TE_constr nil TC_exn ) | JTconstr_c_match_fail : forall (E:environment), JTEok E -> JTconstr_c E C_matchfailure (TE_constr nil TC_exn ) | JTconstr_c_div_by_0 : forall (E:environment), JTEok E -> JTconstr_c E C_div_by_0 (TE_constr nil TC_exn ) | JTconstr_c_none : forall (E:environment) (t:typexpr), JTt E t 0 -> JTconstr_c E C_none (TE_constr (cons t nil) TC_option ) . (* defns JTconst *) Inductive (* defn const *) JTconst : environment -> constant -> typexpr -> Prop := | JTconst_int : forall (E:environment) (integer_literal5:integer_literal), JTEok E -> JTconst E (CONST_int ( integer_literal5 )%Z ) (TE_constr nil TC_int ) | JTconst_float : forall (E:environment) (float_literal5:float_literal), JTEok E -> JTconst E (CONST_float float_literal5) (TE_constr nil TC_float ) | JTconst_char : forall (E:environment) (char_literal5:char_literal), JTEok E -> JTconst E (CONST_char char_literal5) (TE_constr nil TC_char ) | JTconst_string : forall (E:environment) (string_literal5:string_literal), JTEok E -> JTconst E (CONST_string string_literal5) (TE_constr nil TC_string ) | JTconst_constr : forall (E:environment) (constr5:constr) (t:typexpr), JTconstr_c E constr5 t -> JTconst E (CONST_constr constr5) t | JTconst_false : forall (E:environment), JTEok E -> JTconst E CONST_false (TE_constr nil TC_bool ) | JTconst_true : forall (E:environment), JTEok E -> JTconst E CONST_true (TE_constr nil TC_bool ) | JTconst_unit : forall (E:environment), JTEok E -> JTconst E CONST_unit (TE_constr nil TC_unit ) | JTconst_nil : forall (E:environment) (t:typexpr), JTt E t 0 -> JTconst E CONST_nil (TE_constr (cons t nil) TC_list ) . (* defns JTpat *) Inductive (* defn pat *) JTpat : Tsigma -> environment -> pattern -> typexpr -> environment -> Prop := | JTpat_var : forall (Tsigma5:Tsigma) (E:environment) (x:value_name) (t:typexpr), JTt E t 0 -> JTpat Tsigma5 E (P_var x) t (cons (EB_vn x (TS_forall (shiftt 0 1 t ))) (@nil environment_binding) ) | JTpat_any : forall (Tsigma5:Tsigma) (E:environment) (t:typexpr), JTt E t 0 -> JTpat Tsigma5 E P_any t (@nil environment_binding) | JTpat_constant : forall (Tsigma5:Tsigma) (E:environment) (constant5:constant) (t:typexpr), JTconst E constant5 t -> JTpat Tsigma5 E (P_constant constant5) t (@nil environment_binding) | JTpat_alias : forall (name_list:list name) (Tsigma5:Tsigma) (E:environment) (pattern5:pattern) (x:value_name) (t:typexpr) (E':environment), JTpat Tsigma5 E pattern5 t E' -> JdomE (cons (EB_vn x (TS_forall (shiftt 0 1 t ))) E' ) name_list -> (NoDup name_list ) -> JTpat Tsigma5 E (P_alias pattern5 x) t (cons (EB_vn x (TS_forall (shiftt 0 1 t ))) E' ) | JTpat_typed : forall (Tsigma5:Tsigma) (E:environment) (pattern5:pattern) (src_t:typexpr) (t:typexpr) (E':environment) (t':typexpr), Is_true (is_src_typexpr_of_typexpr src_t) -> JTpat Tsigma5 E pattern5 t E' -> JTinst_any E t' (substs_typevar_typexpr Tsigma5 src_t ) -> JTeq E t t' -> JTpat Tsigma5 E (P_typed pattern5 src_t) t E' | JTpat_or : forall (Tsigma5:Tsigma) (E:environment) (pattern5:pattern) (pattern':pattern) (t:typexpr) (E':environment) (E'':environment), JTpat Tsigma5 E pattern5 t E' -> JTpat Tsigma5 E pattern' t E'' -> (Permutation E' E'' ) -> JTpat Tsigma5 E (P_or pattern5 pattern') t E' | JTpat_construct : forall (name_list:list name) (pattern_E_t_list:list (pattern*environment*typexpr)) (Tsigma5:Tsigma) (E:environment) (constr5:constr) (t:typexpr), JTconstr_p E constr5 (map (fun (pat_:(pattern*environment*typexpr)) => match pat_ with (pattern_,E_,t_) => t_ end ) pattern_E_t_list) t -> (forall (pattern_:pattern) (t_:typexpr) (E_:environment), In (Tsigma5,E,pattern_,t_,E_) (map (fun (pat_:pattern*environment*typexpr) => match pat_ with (pattern_,E_,t_) => (Tsigma5,E,pattern_,t_,E_) end) pattern_E_t_list) -> (JTpat Tsigma5 E pattern_ t_ E_)) -> JdomE (flatten (rev (map (fun (pat_:(pattern*environment*typexpr)) => match pat_ with (pattern_,E_,t_) => E_ end ) pattern_E_t_list) )) name_list -> (NoDup name_list ) -> JTpat Tsigma5 E (P_construct constr5 (map (fun (pat_:(pattern*environment*typexpr)) => match pat_ with (pattern_,E_,t_) => pattern_ end ) pattern_E_t_list)) t (flatten (rev (map (fun (pat_:(pattern*environment*typexpr)) => match pat_ with (pattern_,E_,t_) => E_ end ) pattern_E_t_list) )) | JTpat_construct_any : forall (t_list:list typexpr) (Tsigma5:Tsigma) (E:environment) (constr5:constr) (t:typexpr), JTconstr_p E constr5 t_list t -> JTpat Tsigma5 E (P_construct_any constr5) t (@nil environment_binding) | JTpat_tuple : forall (name_list:list name) (pattern_t_E_list:list (pattern*typexpr*environment)) (Tsigma5:Tsigma) (E:environment), (forall (pattern_:pattern) (t_:typexpr) (E_:environment), In (Tsigma5,E,pattern_,t_,E_) (map (fun (pat_:pattern*typexpr*environment) => match pat_ with (pattern_,t_,E_) => (Tsigma5,E,pattern_,t_,E_) end) pattern_t_E_list) -> (JTpat Tsigma5 E pattern_ t_ E_)) -> (length (map (fun (pat_:(pattern*typexpr*environment)) => match pat_ with (pattern_,t_,E_) => pattern_ end ) pattern_t_E_list) >= 2 ) -> JdomE (flatten (rev (map (fun (pat_:(pattern*typexpr*environment)) => match pat_ with (pattern_,t_,E_) => E_ end ) pattern_t_E_list) )) name_list -> (NoDup name_list ) -> JTpat Tsigma5 E (P_tuple (map (fun (pat_:(pattern*typexpr*environment)) => match pat_ with (pattern_,t_,E_) => pattern_ end ) pattern_t_E_list)) (TE_tuple (map (fun (pat_:(pattern*typexpr*environment)) => match pat_ with (pattern_,t_,E_) => t_ end ) pattern_t_E_list)) (flatten (rev (map (fun (pat_:(pattern*typexpr*environment)) => match pat_ with (pattern_,t_,E_) => E_ end ) pattern_t_E_list) )) | JTpat_record : forall (name_list:list name) (field_name_pattern_E_t_list:list (field_name*pattern*environment*typexpr)) (Tsigma5:Tsigma) (E:environment) (t:typexpr), (forall (pattern_:pattern) (t_:typexpr) (E_:environment), In (Tsigma5,E,pattern_,t_,E_) (map (fun (pat_:field_name*pattern*environment*typexpr) => match pat_ with (field_name_,pattern_,E_,t_) => (Tsigma5,E,pattern_,t_,E_) end) field_name_pattern_E_t_list) -> (JTpat Tsigma5 E pattern_ t_ E_)) -> (forall (field_name_:field_name) (t_:typexpr), In (E,field_name_,t,t_) (map (fun (pat_:field_name*pattern*environment*typexpr) => match pat_ with (field_name_,pattern_,E_,t_) => (E,field_name_,t,t_) end) field_name_pattern_E_t_list) -> (JTfield E field_name_ t t_)) -> (length (map (fun (pat_:(field_name*pattern*environment*typexpr)) => match pat_ with (field_name_,pattern_,E_,t_) => pattern_ end ) field_name_pattern_E_t_list) >= 1 ) -> JdomE (flatten (rev (map (fun (pat_:(field_name*pattern*environment*typexpr)) => match pat_ with (field_name_,pattern_,E_,t_) => E_ end ) field_name_pattern_E_t_list) )) name_list -> (NoDup name_list ) -> JTpat Tsigma5 E (P_record (map (fun (pat_:(field_name*pattern*environment*typexpr)) => match pat_ with (field_name_,pattern_,E_,t_) => ((F_name field_name_),pattern_) end ) field_name_pattern_E_t_list)) t (flatten (rev (map (fun (pat_:(field_name*pattern*environment*typexpr)) => match pat_ with (field_name_,pattern_,E_,t_) => E_ end ) field_name_pattern_E_t_list) )) | JTpat_cons : forall (name'_list:list name) (name_list:list name) (Tsigma5:Tsigma) (E:environment) (pattern5:pattern) (pattern':pattern) (t:typexpr) (E':environment) (E'':environment), JTpat Tsigma5 E pattern5 t E' -> JTpat Tsigma5 E pattern' (TE_constr (cons t nil) TC_list ) E'' -> JdomE E' name_list -> JdomE E'' name'_list -> (NoDup ((app name_list (app name'_list nil))) ) -> JTpat Tsigma5 E (P_cons pattern5 pattern') (TE_constr (cons t nil) TC_list ) (flatten (rev ((app (cons E' nil) (app (cons E'' nil) nil))) )) . (* defns JTuprim *) Inductive (* defn uprim *) JTuprim : environment -> unary_prim -> typexpr -> Prop := | JTuprim_raise : forall (E:environment) (t:typexpr), JTt E t 0 -> JTuprim E Uprim_raise (TE_arrow (TE_constr nil TC_exn ) t) | JTuprim_not : forall (E:environment), JTEok E -> JTuprim E Uprim_not (TE_arrow (TE_constr nil TC_bool ) (TE_constr nil TC_bool ) ) | JTuprim_uminus : forall (E:environment), JTEok E -> JTuprim E Uprim_minus (TE_arrow (TE_constr nil TC_int ) (TE_constr nil TC_int ) ) | JTuprim_ref : forall (E:environment) (t:typexpr), JTt E t 0 -> JTuprim E Uprim_ref (TE_arrow t (TE_constr (cons t nil) TC_ref ) ) | JTuprim_deref : forall (E:environment) (t:typexpr), JTt E t 0 -> JTuprim E Uprim_deref (TE_arrow (TE_constr (cons t nil) TC_ref ) t) . (* defns JTbprim *) Inductive (* defn bprim *) JTbprim : environment -> binary_prim -> typexpr -> Prop := | JTbprim_equal : forall (E:environment) (t:typexpr), JTt E t 0 -> JTbprim E Bprim_equal (TE_arrow t (TE_arrow t (TE_constr nil TC_bool ) ) ) | JTbprim_plus : forall (E:environment), JTEok E -> JTbprim E Bprim_plus (TE_arrow (TE_constr nil TC_int ) (TE_arrow (TE_constr nil TC_int ) (TE_constr nil TC_int ) ) ) | JTbprim_minus : forall (E:environment), JTEok E -> JTbprim E Bprim_minus (TE_arrow (TE_constr nil TC_int ) (TE_arrow (TE_constr nil TC_int ) (TE_constr nil TC_int ) ) ) | JTbprim_times : forall (E:environment), JTEok E -> JTbprim E Bprim_times (TE_arrow (TE_constr nil TC_int ) (TE_arrow (TE_constr nil TC_int ) (TE_constr nil TC_int ) ) ) | JTbprim_div : forall (E:environment), JTEok E -> JTbprim E Bprim_div (TE_arrow (TE_constr nil TC_int ) (TE_arrow (TE_constr nil TC_int ) (TE_constr nil TC_int ) ) ) | JTbprim_assign : forall (E:environment) (t:typexpr), JTt E t 0 -> JTbprim E Bprim_assign (TE_arrow (TE_constr (cons t nil) TC_ref ) (TE_arrow t (TE_constr nil TC_unit ) ) ) . (* defns JTe *) Inductive (* defn e *) JTe : Tsigma -> environment -> expr -> typexpr -> Prop := | JTe_uprim : forall (Tsigma5:Tsigma) (E:environment) (unary_prim5:unary_prim) (t':typexpr) (t:typexpr), JTuprim E unary_prim5 t -> JTeq E t t' -> JTe Tsigma5 E (Expr_uprim unary_prim5) t' | JTe_bprim : forall (Tsigma5:Tsigma) (E:environment) (binary_prim5:binary_prim) (t':typexpr) (t:typexpr), JTbprim E binary_prim5 t -> JTeq E t t' -> JTe Tsigma5 E (Expr_bprim binary_prim5) t' | JTe_ident : forall (Tsigma5:Tsigma) (E:environment) (value_name5:value_name) (t':typexpr) (t:typexpr), JTvalue_name E value_name5 t -> JTeq E t t' -> JTe Tsigma5 E (Expr_ident value_name5) t' | JTe_constant : forall (Tsigma5:Tsigma) (E:environment) (constant5:constant) (t':typexpr) (t:typexpr), JTconst E constant5 t -> JTeq E t t' -> JTe Tsigma5 E (Expr_constant constant5) t' | JTe_typed : forall (Tsigma5:Tsigma) (E:environment) (e:expr) (src_t:typexpr) (t:typexpr) (t':typexpr), Is_true (is_src_typexpr_of_typexpr src_t) -> JTe Tsigma5 E e t -> JTinst_any E t' (substs_typevar_typexpr Tsigma5 src_t ) -> JTeq E t t' -> JTe Tsigma5 E (Expr_typed e src_t) t | JTe_tuple : forall (e_t_list:list (expr*typexpr)) (Tsigma5:Tsigma) (E:environment) (t':typexpr), (forall (e_:expr) (t_:typexpr), In (Tsigma5,E,e_,t_) (map (fun (pat_:expr*typexpr) => match pat_ with (e_,t_) => (Tsigma5,E,e_,t_) end) e_t_list) -> (JTe Tsigma5 E e_ t_)) -> (length (map (fun (pat_:(expr*typexpr)) => match pat_ with (e_,t_) => e_ end ) e_t_list) >= 2 ) -> JTeq E (TE_tuple (map (fun (pat_:(expr*typexpr)) => match pat_ with (e_,t_) => t_ end ) e_t_list)) t' -> JTe Tsigma5 E (Expr_tuple (map (fun (pat_:(expr*typexpr)) => match pat_ with (e_,t_) => e_ end ) e_t_list)) t' | JTe_construct : forall (e_t_list:list (expr*typexpr)) (Tsigma5:Tsigma) (E:environment) (constr5:constr) (t':typexpr) (t:typexpr), JTconstr_p E constr5 (map (fun (pat_:(expr*typexpr)) => match pat_ with (e_,t_) => t_ end ) e_t_list) t -> (forall (e_:expr) (t_:typexpr), In (Tsigma5,E,e_,t_) (map (fun (pat_:expr*typexpr) => match pat_ with (e_,t_) => (Tsigma5,E,e_,t_) end) e_t_list) -> (JTe Tsigma5 E e_ t_)) -> JTeq E t t' -> JTe Tsigma5 E (Expr_construct constr5 (map (fun (pat_:(expr*typexpr)) => match pat_ with (e_,t_) => e_ end ) e_t_list)) t' | JTe_cons : forall (Tsigma5:Tsigma) (E:environment) (e1:expr) (e2:expr) (t':typexpr) (t:typexpr), JTe Tsigma5 E e1 t -> JTe Tsigma5 E e2 (TE_constr (cons t nil) TC_list ) -> JTeq E (TE_constr (cons t nil) TC_list ) t' -> JTe Tsigma5 E (Expr_cons e1 e2) t' | JTe_record_constr : forall (field_name'_list:list field_name) (t'_list:list typexpr) (field_name_e_t_list:list (field_name*expr*typexpr)) (Tsigma5:Tsigma) (E:environment) (t':typexpr) (t:typexpr) (typeconstr_name5:typeconstr_name) (kind5:kind), (forall (e_:expr) (t_:typexpr), In (Tsigma5,E,e_,t_) (map (fun (pat_:field_name*expr*typexpr) => match pat_ with (field_name_,e_,t_) => (Tsigma5,E,e_,t_) end) field_name_e_t_list) -> (JTe Tsigma5 E e_ t_)) -> (forall (field_name_:field_name) (t_:typexpr), In (E,field_name_,t,t_) (map (fun (pat_:field_name*expr*typexpr) => match pat_ with (field_name_,e_,t_) => (E,field_name_,t,t_) end) field_name_e_t_list) -> (JTfield E field_name_ t t_)) -> ( t = (TE_constr t'_list (TC_name typeconstr_name5)) ) -> Jlookup_EB E (name_tcn typeconstr_name5) (EB_tr typeconstr_name5 kind5 field_name'_list) -> (Permutation (map (fun (pat_:(field_name*expr*typexpr)) => match pat_ with (field_name_,e_,t_) => field_name_ end ) field_name_e_t_list) field_name'_list ) -> (length (map (fun (pat_:(field_name*expr*typexpr)) => match pat_ with (field_name_,e_,t_) => e_ end ) field_name_e_t_list) >= 1 ) -> JTeq E t t' -> JTe Tsigma5 E (Expr_record (map (fun (pat_:(field_name*expr*typexpr)) => match pat_ with (field_name_,e_,t_) => ((F_name field_name_),e_) end ) field_name_e_t_list)) t' | JTe_record_with : forall (field_name_e_t_list:list (field_name*expr*typexpr)) (Tsigma5:Tsigma) (E:environment) (expr5:expr) (t':typexpr) (t:typexpr), JTe Tsigma5 E expr5 t -> (forall (field_name_:field_name) (t_:typexpr), In (E,field_name_,t,t_) (map (fun (pat_:field_name*expr*typexpr) => match pat_ with (field_name_,e_,t_) => (E,field_name_,t,t_) end) field_name_e_t_list) -> (JTfield E field_name_ t t_)) -> (forall (e_:expr) (t_:typexpr), In (Tsigma5,E,e_,t_) (map (fun (pat_:field_name*expr*typexpr) => match pat_ with (field_name_,e_,t_) => (Tsigma5,E,e_,t_) end) field_name_e_t_list) -> (JTe Tsigma5 E e_ t_)) -> (NoDup (map (fun (pat_:(field_name*expr*typexpr)) => match pat_ with (field_name_,e_,t_) => (name_fn field_name_) end ) field_name_e_t_list) ) -> (length (map (fun (pat_:(field_name*expr*typexpr)) => match pat_ with (field_name_,e_,t_) => e_ end ) field_name_e_t_list) >= 1 ) -> JTeq E t t' -> JTe Tsigma5 E (Expr_override expr5 (map (fun (pat_:(field_name*expr*typexpr)) => match pat_ with (field_name_,e_,t_) => ((F_name field_name_),e_) end ) field_name_e_t_list)) t' | JTe_apply : forall (Tsigma5:Tsigma) (E:environment) (e:expr) (e1:expr) (t:typexpr) (t1:typexpr), JTe Tsigma5 E e (TE_arrow t1 t) -> JTe Tsigma5 E e1 t1 -> JTe Tsigma5 E (Expr_apply e e1) t | JTe_record_proj : forall (Tsigma5:Tsigma) (E:environment) (e:expr) (field_name5:field_name) (t'':typexpr) (t:typexpr) (t':typexpr), JTe Tsigma5 E e t -> JTfield E field_name5 t t' -> JTeq E t' t'' -> JTe Tsigma5 E (Expr_field e (F_name field_name5)) t'' | JTe_and : forall (Tsigma5:Tsigma) (E:environment) (e1:expr) (e2:expr) (t:typexpr), JTe Tsigma5 E e1 (TE_constr nil TC_bool ) -> JTe Tsigma5 E e2 (TE_constr nil TC_bool ) -> JTeq E (TE_constr nil TC_bool ) t -> JTe Tsigma5 E (Expr_and e1 e2) t | JTe_or : forall (Tsigma5:Tsigma) (E:environment) (e1:expr) (e2:expr) (t:typexpr), JTe Tsigma5 E e1 (TE_constr nil TC_bool ) -> JTe Tsigma5 E e2 (TE_constr nil TC_bool ) -> JTeq E (TE_constr nil TC_bool ) t -> JTe Tsigma5 E (Expr_or e1 e2) t | JTe_ifthenelse : forall (Tsigma5:Tsigma) (E:environment) (e1:expr) (e2:expr) (e3:expr) (t:typexpr), JTe Tsigma5 E e1 (TE_constr nil TC_bool ) -> JTe Tsigma5 E e2 t -> JTe Tsigma5 E e3 t -> JTe Tsigma5 E (Expr_ifthenelse e1 e2 e3) t | JTe_while : forall (Tsigma5:Tsigma) (E:environment) (e1:expr) (e2:expr) (t:typexpr), JTe Tsigma5 E e1 (TE_constr nil TC_bool ) -> JTe Tsigma5 E e2 (TE_constr nil TC_unit ) -> JTeq E (TE_constr nil TC_unit ) t -> JTe Tsigma5 E (Expr_while e1 e2) t | JTe_for : forall (Tsigma5:Tsigma) (E:environment) (lowercase_ident5:lowercase_ident) (e1:expr) (for_dirn5:for_dirn) (e2:expr) (e3:expr) (t:typexpr), JTe Tsigma5 E e1 (TE_constr nil TC_int ) -> JTe Tsigma5 E e2 (TE_constr nil TC_int ) -> JTe Tsigma5 (cons (EB_vn (VN_id lowercase_ident5) (TS_forall (shiftt 0 1 (TE_constr nil TC_int ) ))) E ) e3 (TE_constr nil TC_unit ) -> JTeq E (TE_constr nil TC_unit ) t -> JTe Tsigma5 E (Expr_for (VN_id lowercase_ident5) e1 for_dirn5 e2 e3) t | JTe_sequence : forall (Tsigma5:Tsigma) (E:environment) (e1:expr) (e2:expr) (t:typexpr), JTe Tsigma5 E e1 (TE_constr nil TC_unit ) -> JTe Tsigma5 E e2 t -> JTe Tsigma5 E (Expr_sequence e1 e2) t | JTe_match : forall (Tsigma5:Tsigma) (E:environment) (e:expr) (pattern_matching5:pattern_matching) (t':typexpr) (t:typexpr), JTe Tsigma5 E e t -> JTpat_matching Tsigma5 E pattern_matching5 t t' -> JTe Tsigma5 E (Expr_match e pattern_matching5) t' | JTe_function : forall (Tsigma5:Tsigma) (E:environment) (pattern_matching5:pattern_matching) (t'':typexpr) (t:typexpr) (t':typexpr), JTpat_matching Tsigma5 E pattern_matching5 t t' -> JTeq E (TE_arrow t t') t'' -> JTe Tsigma5 E (Expr_function pattern_matching5) t'' | JTe_try : forall (Tsigma5:Tsigma) (E:environment) (e:expr) (pattern_matching5:pattern_matching) (t:typexpr), JTe Tsigma5 E e t -> JTpat_matching Tsigma5 E pattern_matching5 (TE_constr nil TC_exn ) t -> JTe Tsigma5 E (Expr_try e pattern_matching5) t | JTe_let_mono : forall (x_t_list:list (value_name*typexpr)) (Tsigma5:Tsigma) (E:environment) (pat:pattern) (expr5:expr) (e:expr) (t:typexpr), JTlet_binding Tsigma5 E (LB_simple pat expr5) (rev (map (fun (pat_:(value_name*typexpr)) => match pat_ with (x_,t_) => (EB_vn x_ (TS_forall (shiftt 0 1 t_ ))) end ) x_t_list) ) -> JTe Tsigma5 (flatten (rev ((app (cons E nil) (app (cons (rev (map (fun (pat_:(value_name*typexpr)) => match pat_ with (x_,t_) => (EB_vn x_ (TS_forall (shiftt 0 1 t_ ))) end ) x_t_list) ) nil) nil))) )) e t -> JTe Tsigma5 E (Expr_let (LB_simple pat expr5) e) t | JTe_let_poly : forall (x_t_list:list (value_name*typexpr)) (Tsigma5:Tsigma) (E:environment) (pat:pattern) (nexp:expr) (e:expr) (t:typexpr), Is_true (is_non_expansive_of_expr nexp) -> JTlet_binding (shiftTsig 0 1 Tsigma5 ) (cons EB_tv E ) (LB_simple pat nexp) (rev (map (fun (pat_:(value_name*typexpr)) => match pat_ with (x_,t_) => (EB_vn x_ (TS_forall (shiftt 0 1 t_ ))) end ) x_t_list) ) -> JTe Tsigma5 (flatten (rev ((app (cons E nil) (app (cons (rev (map (fun (pat_:(value_name*typexpr)) => match pat_ with (x_,t_) => (EB_vn x_ (TS_forall t_)) end ) x_t_list) ) nil) nil))) )) e t -> JTe Tsigma5 E (Expr_let (LB_simple pat nexp) e) t | JTe_letrec : forall (x_t_list:list (value_name*typexpr)) (Tsigma5:Tsigma) (E:environment) (letrec_bindings5:letrec_bindings) (e:expr) (t:typexpr), JTletrec_binding (shiftTsig 0 1 Tsigma5 ) (cons EB_tv E ) letrec_bindings5 (rev (map (fun (pat_:(value_name*typexpr)) => match pat_ with (x_,t_) => (EB_vn x_ (TS_forall (shiftt 0 1 t_ ))) end ) x_t_list) ) -> JTe Tsigma5 (flatten (rev ((app (cons E nil) (app (cons (rev (map (fun (pat_:(value_name*typexpr)) => match pat_ with (x_,t_) => (EB_vn x_ (TS_forall t_)) end ) x_t_list) ) nil) nil))) )) e t -> JTe Tsigma5 E (Expr_letrec letrec_bindings5 e) t | JTe_assert : forall (Tsigma5:Tsigma) (E:environment) (e:expr) (t:typexpr), JTe Tsigma5 E e (TE_constr nil TC_bool ) -> JTeq E (TE_constr nil TC_unit ) t -> JTe Tsigma5 E (Expr_assert e) t | JTe_assertfalse : forall (Tsigma5:Tsigma) (E:environment) (t:typexpr), JTt E t 0 -> JTe Tsigma5 E (Expr_assert (Expr_constant CONST_false)) t | JTe_location : forall (Tsigma5:Tsigma) (E:environment) (location5:location) (t':typexpr) (t:typexpr), JTEok E -> Jlookup_EB E (name_l location5) (EB_l location5 t) -> JTeq E (TE_constr (cons t nil) TC_ref ) t' -> JTe Tsigma5 E (Expr_location location5) t' with (* defn pat_matching *) JTpat_matching : Tsigma -> environment -> pattern_matching -> typexpr -> typexpr -> Prop := | JTpat_matching_pm : forall (pattern_e_E_list:list (pattern*expr*environment)) (Tsigma5:Tsigma) (E:environment) (t:typexpr) (t':typexpr), (forall (pattern_:pattern) (E_:environment), In (Tsigma5,E,pattern_,t,E_) (map (fun (pat_:pattern*expr*environment) => match pat_ with (pattern_,e_,E_) => (Tsigma5,E,pattern_,t,E_) end) pattern_e_E_list) -> (JTpat Tsigma5 E pattern_ t E_)) -> (forall (E_:environment) (e_:expr), In (Tsigma5, (flatten (rev ((app (cons E nil) (app (cons E_ nil) nil))) )) ,e_,t') (map (fun (pat_:pattern*expr*environment) => match pat_ with (pattern_,e_,E_) => (Tsigma5, (flatten (rev ((app (cons E nil) (app (cons E_ nil) nil))) )) ,e_,t') end) pattern_e_E_list) -> (JTe Tsigma5 (flatten (rev ((app (cons E nil) (app (cons E_ nil) nil))) )) e_ t')) -> (length (map (fun (pat_:(pattern*expr*environment)) => match pat_ with (pattern_,e_,E_) => pattern_ end ) pattern_e_E_list) >= 1 ) -> JTpat_matching Tsigma5 E (PM_pm (map (fun (pat_:(pattern*expr*environment)) => match pat_ with (pattern_,e_,E_) => (PE_inj pattern_ e_) end ) pattern_e_E_list)) t t' with (* defn let_binding *) JTlet_binding : Tsigma -> environment -> let_binding -> environment -> Prop := | JTlet_binding_poly : forall (x_t_list:list (value_name*typexpr)) (Tsigma5:Tsigma) (E:environment) (pattern5:pattern) (expr5:expr) (t:typexpr), JTpat Tsigma5 E pattern5 t (rev (map (fun (pat_:(value_name*typexpr)) => match pat_ with (x_,t_) => (EB_vn x_ (TS_forall (shiftt 0 1 t_ ))) end ) x_t_list) ) -> JTe Tsigma5 E expr5 t -> JTlet_binding Tsigma5 E (LB_simple pattern5 expr5) (rev (map (fun (pat_:(value_name*typexpr)) => match pat_ with (x_,t_) => (EB_vn x_ (TS_forall (shiftt 0 1 t_ ))) end ) x_t_list) ) with (* defn letrec_binding *) JTletrec_binding : Tsigma -> environment -> letrec_bindings -> environment -> Prop := | JTletrec_binding_equal_function : forall (value_name_pattern_matching_t_t'_list:list (value_name*pattern_matching*typexpr*typexpr)) (Tsigma5:Tsigma) (E:environment) (E':environment), ( E' = (flatten (rev ((app (cons E nil) (app (cons (rev (map (fun (pat_:(value_name*pattern_matching*typexpr*typexpr)) => match pat_ with (value_name_,pattern_matching_,t_,t_') => (EB_vn value_name_ (TS_forall (shiftt 0 1 (TE_arrow t_ t_') ))) end ) value_name_pattern_matching_t_t'_list) ) nil) nil))) )) ) -> (forall (pattern_matching_:pattern_matching) (t_:typexpr) (t_':typexpr), In (Tsigma5,E',pattern_matching_,t_,t_') (map (fun (pat_:value_name*pattern_matching*typexpr*typexpr) => match pat_ with (value_name_,pattern_matching_,t_,t_') => (Tsigma5,E',pattern_matching_,t_,t_') end) value_name_pattern_matching_t_t'_list) -> (JTpat_matching Tsigma5 E' pattern_matching_ t_ t_')) -> (NoDup (map (fun (pat_:(value_name*pattern_matching*typexpr*typexpr)) => match pat_ with (value_name_,pattern_matching_,t_,t_') => (name_vn value_name_) end ) value_name_pattern_matching_t_t'_list) ) -> JTletrec_binding Tsigma5 E (LRBs_inj (map (fun (pat_:(value_name*pattern_matching*typexpr*typexpr)) => match pat_ with (value_name_,pattern_matching_,t_,t_') => (LRB_simple value_name_ pattern_matching_) end ) value_name_pattern_matching_t_t'_list)) (rev (map (fun (pat_:(value_name*pattern_matching*typexpr*typexpr)) => match pat_ with (value_name_,pattern_matching_,t_,t_') => (EB_vn value_name_ (TS_forall (shiftt 0 1 (TE_arrow t_ t_') ))) end ) value_name_pattern_matching_t_t'_list) ) . (* defns JTconstr_decl *) Inductive (* defn constr_decl *) JTconstr_decl : type_params_opt -> typeconstr -> constr_decl -> environment_binding -> Prop := | JTconstr_decl_nullary : forall (tv_list:list typevar) (typeconstr5:typeconstr) (constr_name5:constr_name), JTconstr_decl (TPS_nary (map (fun (tv_:typevar) => (TP_var tv_)) tv_list)) typeconstr5 (CD_nullary constr_name5) (EB_cc constr_name5 typeconstr5) | JTconstr_decl_nary : forall (tv_t_list:list (typevar*typexpr)) (typeconstr5:typeconstr) (constr_name5:constr_name), JTconstr_decl (TPS_nary (map (fun (pat_:(typevar*typexpr)) => match pat_ with (tv_,t_) => (TP_var tv_) end ) tv_t_list)) typeconstr5 (CD_nary constr_name5 (map (fun (pat_:(typevar*typexpr)) => match pat_ with (tv_,t_) => t_ end ) tv_t_list)) (EB_pc constr_name5 (TPS_nary (map (fun (pat_:(typevar*typexpr)) => match pat_ with (tv_,t_) => (TP_var tv_) end ) tv_t_list)) (typexprs_inj (map (fun (pat_:(typevar*typexpr)) => match pat_ with (tv_,t_) => t_ end ) tv_t_list)) typeconstr5) . (* defns JTfield_decl *) Inductive (* defn field_decl *) JTfield_decl : type_params_opt -> typeconstr_name -> field_decl -> environment_binding -> Prop := | JTfield_decl_only : forall (tv_list:list typevar) (typeconstr_name5:typeconstr_name) (fn:field_name) (t:typexpr), JTfield_decl (TPS_nary (map (fun (tv_:typevar) => (TP_var tv_)) tv_list)) typeconstr_name5 (FD_immutable fn t) (EB_fn fn (TPS_nary (map (fun (tv_:typevar) => (TP_var tv_)) tv_list)) typeconstr_name5 t) . (* defns JTtypedef *) Inductive (* defn typedef *) JTtypedef : list typedef -> environment -> environment -> environment -> Prop := | JTtypedef_empty : JTtypedef nil (@nil environment_binding) (@nil environment_binding) (@nil environment_binding) | JTtypedef_eq : forall (typedef_list:list typedef) (type_params_opt5:type_params_opt) (typeconstr_name5:typeconstr_name) (t:typexpr) (E:environment) (E':environment) (E'':environment), JTtypedef typedef_list E E' E'' -> JTtypedef ((app (cons (TD_td type_params_opt5 typeconstr_name5 (TI_eq (TE_te t))) nil) (app typedef_list nil))) E (cons (EB_ta type_params_opt5 typeconstr_name5 t) E' ) E'' | JTtypedef_def_sum : forall (constr_decl_EB_list:list (constr_decl*environment_binding)) (typedef_list:list typedef) (type_params_opt5:type_params_opt) (typeconstr_name5:typeconstr_name) (E:environment) (kind5:kind) (E':environment) (E'':environment), JTtypedef typedef_list E E' E'' -> JTtps_kind type_params_opt5 kind5 -> (forall (constr_decl_:constr_decl) (EB_:environment_binding), In (type_params_opt5,(TC_name typeconstr_name5),constr_decl_,EB_) (map (fun (pat_:constr_decl*environment_binding) => match pat_ with (constr_decl_,EB_) => (type_params_opt5,(TC_name typeconstr_name5),constr_decl_,EB_) end) constr_decl_EB_list) -> (JTconstr_decl type_params_opt5 (TC_name typeconstr_name5) constr_decl_ EB_)) -> JTtypedef ((app (cons (TD_td type_params_opt5 typeconstr_name5 (TI_def (TR_variant (map (fun (pat_:(constr_decl*environment_binding)) => match pat_ with (constr_decl_,EB_) => constr_decl_ end ) constr_decl_EB_list)))) nil) (app typedef_list nil))) (cons (EB_td typeconstr_name5 kind5) E ) E' (flatten (rev ((app (cons E'' nil) (app (cons (rev (map (fun (pat_:(constr_decl*environment_binding)) => match pat_ with (constr_decl_,EB_) => EB_ end ) constr_decl_EB_list) ) nil) nil))) )) | JTtypedef_def_record : forall (field_name_t_EB_list:list (field_name*typexpr*environment_binding)) (typedef_list:list typedef) (type_params_opt5:type_params_opt) (typeconstr_name5:typeconstr_name) (E:environment) (kind5:kind) (E':environment) (E'':environment), JTtypedef typedef_list E E' E'' -> JTtps_kind type_params_opt5 kind5 -> (forall (field_name_:field_name) (t_:typexpr) (EB_:environment_binding), In (type_params_opt5,typeconstr_name5,(FD_immutable field_name_ t_),EB_) (map (fun (pat_:field_name*typexpr*environment_binding) => match pat_ with (field_name_,t_,EB_) => (type_params_opt5,typeconstr_name5,(FD_immutable field_name_ t_),EB_) end) field_name_t_EB_list) -> (JTfield_decl type_params_opt5 typeconstr_name5 (FD_immutable field_name_ t_) EB_)) -> JTtypedef ((app (cons (TD_td type_params_opt5 typeconstr_name5 (TI_def (TR_record (map (fun (pat_:(field_name*typexpr*environment_binding)) => match pat_ with (field_name_,t_,EB_) => (FD_immutable field_name_ t_) end ) field_name_t_EB_list)))) nil) (app typedef_list nil))) (cons (EB_tr typeconstr_name5 kind5 (map (fun (pat_:(field_name*typexpr*environment_binding)) => match pat_ with (field_name_,t_,EB_) => field_name_ end ) field_name_t_EB_list)) E ) E' (flatten (rev ((app (cons E'' nil) (app (cons (rev (map (fun (pat_:(field_name*typexpr*environment_binding)) => match pat_ with (field_name_,t_,EB_) => EB_ end ) field_name_t_EB_list) ) nil) nil))) )) . (* defns JTtype_definition *) Inductive (* defn type_definition *) JTtype_definition : environment -> type_definition -> environment -> Prop := | JTtype_definition_list : forall (typedef_list:list typedef) (E:environment) (E'''':environment) (E':environment) (E'':environment) (E''':environment), JTtypedef typedef_list E' E'' E''' -> ( E'''' = (flatten (rev ((app (cons E' nil) (app (cons E'' nil) (app (cons E''' nil) nil)))) )) ) -> JTEok (flatten (rev ((app (cons E nil) (app (cons E'''' nil) nil))) )) -> JTtype_definition E (TDF_tdf typedef_list) E'''' | JTtype_definition_swap : forall (typedef''_list:list typedef) (typedef_list:list typedef) (E:environment) (typedef_5:typedef) (typedef':typedef) (E':environment), JTtype_definition E (TDF_tdf ((app typedef_list (app (cons typedef' nil) (app (cons typedef_5 nil) (app typedef''_list nil)))))) E' -> JTtype_definition E (TDF_tdf ((app typedef_list (app (cons typedef_5 nil) (app (cons typedef' nil) (app typedef''_list nil)))))) E' . (* defns JTdefinition *) Inductive (* defn definition *) JTdefinition : environment -> definition -> environment -> Prop := | JTdefinition_let_poly : forall (x_t'_list:list (value_name*typexpr)) (E:environment) (pat:pattern) (nexp:expr) (Tsigma5:Tsigma), Is_true (is_non_expansive_of_expr nexp) -> JTlet_binding Tsigma5 (cons EB_tv E ) (LB_simple pat nexp) (rev (map (fun (pat_:(value_name*typexpr)) => match pat_ with (x_,t_') => (EB_vn x_ (TS_forall (shiftt 0 1 t_' ))) end ) x_t'_list) ) -> JTdefinition E (D_let (LB_simple pat nexp)) (rev (map (fun (pat_:(value_name*typexpr)) => match pat_ with (x_,t_') => (EB_vn x_ (TS_forall t_')) end ) x_t'_list) ) | JTdefinition_let_mono : forall (x_t'_list:list (value_name*typexpr)) (E:environment) (pat:pattern) (expr5:expr) (Tsigma5:Tsigma), JTlet_binding Tsigma5 E (LB_simple pat expr5) (rev (map (fun (pat_:(value_name*typexpr)) => match pat_ with (x_,t_') => (EB_vn x_ (TS_forall (shiftt 0 1 t_' ))) end ) x_t'_list) ) -> JTdefinition E (D_let (LB_simple pat expr5)) (rev (map (fun (pat_:(value_name*typexpr)) => match pat_ with (x_,t_') => (EB_vn x_ (TS_forall (shiftt 0 1 t_' ))) end ) x_t'_list) ) | JTdefinition_letrec : forall (x_t'_list:list (value_name*typexpr)) (E:environment) (letrec_bindings5:letrec_bindings) (Tsigma5:Tsigma), JTletrec_binding Tsigma5 (cons EB_tv E ) letrec_bindings5 (rev (map (fun (pat_:(value_name*typexpr)) => match pat_ with (x_,t_') => (EB_vn x_ (TS_forall (shiftt 0 1 t_' ))) end ) x_t'_list) ) -> JTdefinition E (D_letrec letrec_bindings5) (rev (map (fun (pat_:(value_name*typexpr)) => match pat_ with (x_,t_') => (EB_vn x_ (TS_forall t_')) end ) x_t'_list) ) | JTdefinition_typedef : forall (typedef_list:list typedef) (E:environment) (E':environment), JTtype_definition E (TDF_tdf typedef_list) E' -> JTdefinition E (D_type (TDF_tdf typedef_list)) E' | JTdefinition_exndef : forall (E:environment) (constr_decl5:constr_decl) (EB:environment_binding), JTEok E -> JTconstr_decl (TPS_nary nil) TC_exn constr_decl5 EB -> JTdefinition E (D_exception (ED_def constr_decl5)) (rev (cons EB nil) ) . (* defns JTdefinitions *) Inductive (* defn definitions *) JTdefinitions : environment -> definitions -> environment -> Prop := | JTdefinitions_empty : forall (E:environment), JTEok E -> JTdefinitions E Ds_nil (rev nil ) | JTdefinitions_item : forall (E:environment) (definition5:definition) (definitions':definitions) (E':environment) (E'':environment), JTdefinition E definition5 E' -> JTdefinitions (flatten (rev ((app (cons E nil) (app (cons E' nil) nil))) )) definitions' E'' -> JTdefinitions E (Ds_cons definition5 definitions') (flatten (rev ((app (cons E' nil) (app (cons E'' nil) nil))) )) . (* defns JTprog *) Inductive (* defn prog *) JTprog : environment -> program -> environment -> Prop := | JTprog_defs : forall (E:environment) (definitions5:definitions) (E':environment), JTdefinitions E definitions5 E' -> JTprog E (Prog_defs definitions5) E' | JTprog_raise : forall (E:environment) (v:expr) (Tsigma5:Tsigma) (t:typexpr), Is_true (is_value_of_expr v) -> JTe Tsigma5 E v t -> JTprog E (Prog_raise v) (rev nil ) . (* defns JTstore *) Inductive (* defn store *) JTstore : environment -> store -> environment -> Prop := | JTstore_empty : forall (E:environment), JTstore E (@nil (location*expr)) (rev nil ) | JTstore_map : forall (E:environment) (store5:store) (l:index) (v:expr) (E':environment) (t:typexpr), Is_true (is_value_of_expr v) -> JTstore E store5 E' -> JTe nil E v t -> JTstore E (cons ( l , v ) store5 ) (cons (EB_l l t) E' ) . (* defns JTtop *) Inductive (* defn top *) JTtop : environment -> program -> store -> environment -> Prop := | JTtop_defs : forall (E:environment) (program5:program) (store5:store) (E':environment) (E'':environment), JTstore (flatten (rev ((app (cons E nil) (app (cons E' nil) nil))) )) store5 E' -> JTprog (flatten (rev ((app (cons E nil) (app (cons E' nil) nil))) )) program5 E'' -> JTtop E program5 store5 (flatten (rev ((app (cons E' nil) (app (cons E'' nil) nil))) )) . (* defns JTLin *) Inductive (* defn Lin *) JTLin : Tsigma -> environment -> trans_label -> Prop := | JTLin_nil : forall (Tsigma5:Tsigma) (E:environment), JTLin Tsigma5 E Lab_nil | JTLin_alloc : forall (Tsigma5:Tsigma) (E:environment) (v:expr) (location5:location) (names5:names), JdomE E names5 -> (~In (name_l location5) names5 ) -> JTLin Tsigma5 E (Lab_alloc v location5) | JTLin_deref : forall (Tsigma5:Tsigma) (E:environment) (location5:location) (v:expr) (t:typexpr), Is_true (is_value_of_expr v) -> JTe Tsigma5 E v t -> Jlookup_EB E (name_l location5) (EB_l location5 t) -> JTLin Tsigma5 E (Lab_deref location5 v) | JTLin_assign : forall (Tsigma5:Tsigma) (E:environment) (location5:location) (v:expr), JTLin Tsigma5 E (Lab_assign location5 v) . (* defns JTLout *) Inductive (* defn Lout *) JTLout : Tsigma -> environment -> trans_label -> environment -> Prop := | JTLout_nil : forall (Tsigma5:Tsigma) (E:environment), JTLout Tsigma5 E Lab_nil (rev nil ) | JTLout_alloc : forall (Tsigma5:Tsigma) (E:environment) (location5:location) (t:typexpr) (v:expr), Is_true (is_value_of_expr v) -> JTe Tsigma5 E v t -> JTLout Tsigma5 E (Lab_alloc v location5) (rev (cons (EB_l location5 t) nil) ) | JTLout_deref : forall (Tsigma5:Tsigma) (E:environment) (location5:location) (v:expr), JTLout Tsigma5 E (Lab_deref location5 v) (rev nil ) | JTLout_assign : forall (Tsigma5:Tsigma) (E:environment) (location5:location) (v:expr) (t:typexpr), Is_true (is_value_of_expr v) -> JTe Tsigma5 E v t -> Jlookup_EB E (name_l location5) (EB_l location5 t) -> JTLout Tsigma5 E (Lab_assign location5 v) (rev nil ) . (* defns JmatchP *) Inductive (* defn matchP *) JM_matchP : expr -> pattern -> Prop := | JM_matchP_var : forall (v:expr) (x:value_name), Is_true (is_value_of_expr v) -> JM_matchP v (P_var x) | JM_matchP_any : forall (v:expr), Is_true (is_value_of_expr v) -> JM_matchP v P_any | JM_matchP_constant : forall (constant5:constant), JM_matchP (Expr_constant constant5) (P_constant constant5) | JM_matchP_alias : forall (v:expr) (pat:pattern) (x:value_name), Is_true (is_value_of_expr v) -> JM_matchP v pat -> JM_matchP v (P_alias pat x) | JM_matchP_typed : forall (v:expr) (pat:pattern) (t:typexpr), Is_true (is_value_of_expr v) -> JM_matchP v pat -> JM_matchP v (P_typed pat t) | JM_matchP_or_left : forall (v:expr) (pat1:pattern) (pat2:pattern), Is_true (is_value_of_expr v) -> JM_matchP v pat1 -> JM_matchP v (P_or pat1 pat2) | JM_matchP_or_right : forall (v:expr) (pat1:pattern) (pat2:pattern), Is_true (is_value_of_expr v) -> JM_matchP v pat2 -> JM_matchP v (P_or pat1 pat2) | JM_matchP_construct : forall (v_pat_list:list (expr*pattern)) (constr5:constr), (Forall_list (fun (tmp_:(expr*pattern)) => match tmp_ with (v_,pat_) => Is_true (is_value_of_expr v_) end) v_pat_list) -> (forall (v_:expr) (pat_:pattern), In (v_,pat_) v_pat_list -> (JM_matchP v_ pat_)) -> JM_matchP (Expr_construct constr5 (map (fun (pat_:(expr*pattern)) => match pat_ with (v_,pat_) => v_ end ) v_pat_list)) (P_construct constr5 (map (fun (pat_:(expr*pattern)) => match pat_ with (v_,pat_) => pat_ end ) v_pat_list)) | JM_matchP_construct_any : forall (v_list:list expr) (constr5:constr), (Forall_list (fun (v_:expr) => Is_true (is_value_of_expr v_)) v_list) -> JM_matchP (Expr_construct constr5 v_list) (P_construct_any constr5) | JM_matchP_tuple : forall (v_pat_list:list (expr*pattern)), (Forall_list (fun (tmp_:(expr*pattern)) => match tmp_ with (v_,pat_) => Is_true (is_value_of_expr v_) end) v_pat_list) -> (forall (v_:expr) (pat_:pattern), In (v_,pat_) v_pat_list -> (JM_matchP v_ pat_)) -> JM_matchP (Expr_tuple (map (fun (pat_:(expr*pattern)) => match pat_ with (v_,pat_) => v_ end ) v_pat_list)) (P_tuple (map (fun (pat_:(expr*pattern)) => match pat_ with (v_,pat_) => pat_ end ) v_pat_list)) | JM_matchP_record : forall (fn_v''_list:list (field_name*expr)) (field_name'_pat_v'_list:list (field_name*pattern*expr)) (field_name_v_list:list (field_name*expr)), (Forall_list (fun (tmp_:(field_name*expr)) => match tmp_ with (fn_,v_'') => Is_true (is_value_of_expr v_'') end) fn_v''_list) -> (Forall_list (fun (tmp_:(field_name*pattern*expr)) => match tmp_ with (field_name_',pat_,v_') => Is_true (is_value_of_expr v_') end) field_name'_pat_v'_list) -> (Forall_list (fun (tmp_:(field_name*expr)) => match tmp_ with (field_name_,v_) => Is_true (is_value_of_expr v_) end) field_name_v_list) -> (Permutation ((app (map (fun (pat_:(field_name*pattern*expr)) => match pat_ with (field_name_',pat_,v_') => (field_name_',v_') end ) field_name'_pat_v'_list) (app fn_v''_list nil))) field_name_v_list ) -> (forall (v_':expr) (pat_:pattern), In (v_',pat_) (map (fun (pat_:field_name*pattern*expr) => match pat_ with (field_name_',pat_,v_') => (v_',pat_) end) field_name'_pat_v'_list) -> (JM_matchP v_' pat_)) -> (NoDup (map (fun (pat_:(field_name*expr)) => match pat_ with (field_name_,v_) => (name_fn field_name_) end ) field_name_v_list) ) -> JM_matchP (Expr_record (map (fun (pat_:(field_name*expr)) => match pat_ with (field_name_,v_) => ((F_name field_name_),v_) end ) field_name_v_list)) (P_record (map (fun (pat_:(field_name*pattern*expr)) => match pat_ with (field_name_',pat_,v_') => ((F_name field_name_'),pat_) end ) field_name'_pat_v'_list)) | JM_matchP_cons : forall (v1:expr) (v2:expr) (pat1:pattern) (pat2:pattern), Is_true (is_value_of_expr v1) -> Is_true (is_value_of_expr v2) -> JM_matchP v1 pat1 -> JM_matchP v2 pat2 -> JM_matchP (Expr_cons v1 v2) (P_cons pat1 pat2) . (* defns Jmatch *) Inductive (* defn match *) JM_match : expr -> pattern -> substs_x -> Prop := | JM_match_var : forall (v:expr) (x:value_name), Is_true (is_value_of_expr v) -> JM_match v (P_var x) (substs_x_xs (cons (x,v) nil)) | JM_match_any : forall (v:expr), Is_true (is_value_of_expr v) -> JM_match v P_any (substs_x_xs nil) | JM_match_constant : forall (constant5:constant), JM_match (Expr_constant constant5) (P_constant constant5) (substs_x_xs nil) | JM_match_alias : forall (x_v_list:list (value_name*expr)) (v:expr) (pat:pattern) (x:value_name), Is_true (is_value_of_expr v) -> (Forall_list (fun (tmp_:(value_name*expr)) => match tmp_ with (x_,v_) => Is_true (is_value_of_expr v_) end) x_v_list) -> JM_match v pat (substs_x_xs x_v_list) -> JM_match v (P_alias pat x) (substs_x_xs ((app x_v_list (app (cons (x,v) nil) nil)))) | JM_match_typed : forall (x_v_list:list (value_name*expr)) (v:expr) (pat:pattern) (t:typexpr), Is_true (is_value_of_expr v) -> (Forall_list (fun (tmp_:(value_name*expr)) => match tmp_ with (x_,v_) => Is_true (is_value_of_expr v_) end) x_v_list) -> JM_match v pat (substs_x_xs x_v_list) -> JM_match v (P_typed pat t) (substs_x_xs x_v_list) | JM_match_or_left : forall (x_v_list:list (value_name*expr)) (v:expr) (pat1:pattern) (pat2:pattern), Is_true (is_value_of_expr v) -> (Forall_list (fun (tmp_:(value_name*expr)) => match tmp_ with (x_,v_) => Is_true (is_value_of_expr v_) end) x_v_list) -> JM_match v pat1 (substs_x_xs x_v_list) -> JM_match v (P_or pat1 pat2) (substs_x_xs x_v_list) | JM_match_or_right : forall (x_v_list:list (value_name*expr)) (pat1:pattern) (pat2:pattern) (v:expr), Is_true (is_value_of_expr v) -> (Forall_list (fun (tmp_:(value_name*expr)) => match tmp_ with (x_,v_) => Is_true (is_value_of_expr v_) end) x_v_list) -> (~JM_matchP v pat1 ) -> JM_match v pat2 (substs_x_xs x_v_list) -> JM_match v (P_or pat1 pat2) (substs_x_xs x_v_list) | JM_match_construct : forall (v_pat_substs_x_list:list (expr*pattern*substs_x)) (constr5:constr), (Forall_list (fun (tmp_:(expr*pattern*substs_x)) => match tmp_ with (v_,pat_,substs_x_) => Is_true (is_value_of_expr v_) end) v_pat_substs_x_list) -> (forall (v_:expr) (pat_:pattern) (substs_x_:substs_x), In (v_,pat_,substs_x_) v_pat_substs_x_list -> (JM_match v_ pat_ substs_x_)) -> JM_match (Expr_construct constr5 (map (fun (pat_:(expr*pattern*substs_x)) => match pat_ with (v_,pat_,substs_x_) => v_ end ) v_pat_substs_x_list)) (P_construct constr5 (map (fun (pat_:(expr*pattern*substs_x)) => match pat_ with (v_,pat_,substs_x_) => pat_ end ) v_pat_substs_x_list)) (substs_x_xs (flat_map substs_x_proj (map (fun (pat_:(expr*pattern*substs_x)) => match pat_ with (v_,pat_,substs_x_) => substs_x_ end ) v_pat_substs_x_list) )) | JM_match_construct_any : forall (v_list:list expr) (constr5:constr), (Forall_list (fun (v_:expr) => Is_true (is_value_of_expr v_)) v_list) -> JM_match (Expr_construct constr5 v_list) (P_construct_any constr5) (substs_x_xs nil) | JM_match_tuple : forall (v_pat_substs_x_list:list (expr*pattern*substs_x)), (Forall_list (fun (tmp_:(expr*pattern*substs_x)) => match tmp_ with (v_,pat_,substs_x_) => Is_true (is_value_of_expr v_) end) v_pat_substs_x_list) -> (forall (v_:expr) (pat_:pattern) (substs_x_:substs_x), In (v_,pat_,substs_x_) v_pat_substs_x_list -> (JM_match v_ pat_ substs_x_)) -> JM_match (Expr_tuple (map (fun (pat_:(expr*pattern*substs_x)) => match pat_ with (v_,pat_,substs_x_) => v_ end ) v_pat_substs_x_list)) (P_tuple (map (fun (pat_:(expr*pattern*substs_x)) => match pat_ with (v_,pat_,substs_x_) => pat_ end ) v_pat_substs_x_list)) (substs_x_xs (flat_map substs_x_proj (map (fun (pat_:(expr*pattern*substs_x)) => match pat_ with (v_,pat_,substs_x_) => substs_x_ end ) v_pat_substs_x_list) )) | JM_match_record : forall (fn_v''_list:list (field_name*expr)) (field_name'_pat_substs_x_v'_list:list (field_name*pattern*substs_x*expr)) (field_name_v_list:list (field_name*expr)), (Forall_list (fun (tmp_:(field_name*expr)) => match tmp_ with (fn_,v_'') => Is_true (is_value_of_expr v_'') end) fn_v''_list) -> (Forall_list (fun (tmp_:(field_name*pattern*substs_x*expr)) => match tmp_ with (field_name_',pat_,substs_x_,v_') => Is_true (is_value_of_expr v_') end) field_name'_pat_substs_x_v'_list) -> (Forall_list (fun (tmp_:(field_name*expr)) => match tmp_ with (field_name_,v_) => Is_true (is_value_of_expr v_) end) field_name_v_list) -> (Permutation ((app (map (fun (pat_:(field_name*pattern*substs_x*expr)) => match pat_ with (field_name_',pat_,substs_x_,v_') => (field_name_',v_') end ) field_name'_pat_substs_x_v'_list) (app fn_v''_list nil))) field_name_v_list ) -> (forall (v_':expr) (pat_:pattern) (substs_x_:substs_x), In (v_',pat_,substs_x_) (map (fun (pat_:field_name*pattern*substs_x*expr) => match pat_ with (field_name_',pat_,substs_x_,v_') => (v_',pat_,substs_x_) end) field_name'_pat_substs_x_v'_list) -> (JM_match v_' pat_ substs_x_)) -> (NoDup (map (fun (pat_:(field_name*expr)) => match pat_ with (field_name_,v_) => (name_fn field_name_) end ) field_name_v_list) ) -> JM_match (Expr_record (map (fun (pat_:(field_name*expr)) => match pat_ with (field_name_,v_) => ((F_name field_name_),v_) end ) field_name_v_list)) (P_record (map (fun (pat_:(field_name*pattern*substs_x*expr)) => match pat_ with (field_name_',pat_,substs_x_,v_') => ((F_name field_name_'),pat_) end ) field_name'_pat_substs_x_v'_list)) (substs_x_xs (flat_map substs_x_proj (map (fun (pat_:(field_name*pattern*substs_x*expr)) => match pat_ with (field_name_',pat_,substs_x_,v_') => substs_x_ end ) field_name'_pat_substs_x_v'_list) )) | JM_match_cons : forall (v1:expr) (v2:expr) (pat1:pattern) (pat2:pattern) (substs_x1:substs_x) (substs_x2:substs_x), Is_true (is_value_of_expr v1) -> Is_true (is_value_of_expr v2) -> JM_match v1 pat1 substs_x1 -> JM_match v2 pat2 substs_x2 -> JM_match (Expr_cons v1 v2) (P_cons pat1 pat2) (substs_x_xs (flat_map substs_x_proj ((app (cons substs_x1 nil) (app (cons substs_x2 nil) nil))) )) . (* defns Jrecfun *) Inductive (* defn recfun *) Jrecfun : letrec_bindings -> pattern_matching -> expr -> Prop := | Jrecfun_letrec : forall (x_pattern_matching_list:list (value_name*pattern_matching)) (letrec_bindings5:letrec_bindings) (pattern_matching_5:pattern_matching), ( letrec_bindings5 = (LRBs_inj (map (fun (pat_:(value_name*pattern_matching)) => match pat_ with (x_,pattern_matching_) => (LRB_simple x_ pattern_matching_) end ) x_pattern_matching_list)) ) -> Jrecfun letrec_bindings5 pattern_matching_5 (substs_value_name_expr (substs_x_proj (substs_x_xs (map (fun (pat_:(value_name*pattern_matching)) => match pat_ with (x_,pattern_matching_) => (x_,(Expr_letrec letrec_bindings5 (Expr_ident x_))) end ) x_pattern_matching_list)) ) (Expr_function pattern_matching_5) ) . (* defns Jfunval *) Inductive (* defn funval *) Jfunval : expr -> Prop := | Jfunval_up : forall (unary_prim5:unary_prim), Jfunval (Expr_uprim unary_prim5) | Jfunval_bp : forall (binary_prim5:binary_prim), Jfunval (Expr_bprim binary_prim5) | Jfunval_bp_app : forall (binary_prim5:binary_prim) (v:expr), Is_true (is_value_of_expr v) -> Jfunval (Expr_apply (Expr_bprim binary_prim5) v) | Jfunval_func : forall (pattern_matching5:pattern_matching), Jfunval (Expr_function pattern_matching5) . (* defns JRuprim *) Inductive (* defn Ruprim *) JRuprim : unary_prim -> expr -> labelled_arrow -> expr -> Prop := | Juprim_not_true : JRuprim Uprim_not (Expr_constant CONST_true) Lab_nil (Expr_constant CONST_false) | Juprim_not_false : JRuprim Uprim_not (Expr_constant CONST_false) Lab_nil (Expr_constant CONST_true) | Juprim_uminus : forall (intn5:intn), JRuprim Uprim_minus (Expr_constant (CONST_int intn5)) Lab_nil (Expr_constant (CONST_int (( ( 0 )%Z - intn5 )%Z) )) | Juprim_ref_alloc : forall (v:expr) (l:index), Is_true (is_value_of_expr v) -> JRuprim Uprim_ref v (Lab_alloc v l) (Expr_location l) | Juprim_deref : forall (l:index) (v:expr), Is_true (is_value_of_expr v) -> JRuprim Uprim_deref (Expr_location l) (Lab_deref l v) v . (* defns JRbprim *) Inductive (* defn Rbprim *) JRbprim : expr -> binary_prim -> expr -> labelled_arrow -> expr -> Prop := | Jbprim_equal_fun : forall (v:expr) (v':expr), Is_true (is_value_of_expr v) -> Is_true (is_value_of_expr v') -> Jfunval v -> JRbprim v Bprim_equal v' Lab_nil (Expr_apply (Expr_uprim Uprim_raise) (Expr_construct C_invalidargument (cons (Expr_constant (CONST_string string_equal_functional_value) ) nil)) ) | Jbprim_equal_const_true : forall (constant5:constant), JRbprim (Expr_constant constant5) Bprim_equal (Expr_constant constant5) Lab_nil (Expr_constant CONST_true) | Jbprim_equal_const_false : forall (constant5:constant) (constant':constant), (~( constant5 = constant' )) -> JRbprim (Expr_constant constant5) Bprim_equal (Expr_constant constant') Lab_nil (Expr_constant CONST_false) | Jbprim_equal_loc : forall (l:index) (l':index), JRbprim (Expr_location l) Bprim_equal (Expr_location l') Lab_nil (Expr_apply (Expr_apply (Expr_bprim Bprim_equal) (Expr_apply (Expr_uprim Uprim_deref) (Expr_location l)) ) (Expr_apply (Expr_uprim Uprim_deref) (Expr_location l')) ) | Jbprim_equal_cons : forall (v1:expr) (v2:expr) (v1':expr) (v2':expr), Is_true (is_value_of_expr v1) -> Is_true (is_value_of_expr v2) -> Is_true (is_value_of_expr v1') -> Is_true (is_value_of_expr v2') -> JRbprim (Expr_cons v1 v2) Bprim_equal (Expr_cons v1' v2') Lab_nil (Expr_and (Expr_apply (Expr_apply (Expr_bprim Bprim_equal) v1) v1') (Expr_apply (Expr_apply (Expr_bprim Bprim_equal) v2) v2') ) | Jbprim_equal_cons_nil : forall (v1:expr) (v2:expr), Is_true (is_value_of_expr v1) -> Is_true (is_value_of_expr v2) -> JRbprim (Expr_cons v1 v2) Bprim_equal (Expr_constant CONST_nil) Lab_nil (Expr_constant CONST_false) | Jbprim_equal_nil_cons : forall (v1:expr) (v2:expr), Is_true (is_value_of_expr v1) -> Is_true (is_value_of_expr v2) -> JRbprim (Expr_constant CONST_nil) Bprim_equal (Expr_cons v1 v2) Lab_nil (Expr_constant CONST_false) | Jbprim_equal_tuple : forall (v_v'_list:list (expr*expr)), (Forall_list (fun (tmp_:(expr*expr)) => match tmp_ with (v_,v_') => Is_true (is_value_of_expr v_) end) v_v'_list) -> (Forall_list (fun (tmp_:(expr*expr)) => match tmp_ with (v_,v_') => Is_true (is_value_of_expr v_') end) v_v'_list) -> (length (map (fun (pat_:(expr*expr)) => match pat_ with (v_,v_') => v_ end ) v_v'_list) >= 2 ) -> JRbprim (Expr_tuple (map (fun (pat_:(expr*expr)) => match pat_ with (v_,v_') => v_ end ) v_v'_list)) Bprim_equal (Expr_tuple (map (fun (pat_:(expr*expr)) => match pat_ with (v_,v_') => v_' end ) v_v'_list)) Lab_nil (fold_right Expr_and CONST_true (map (fun (pat_:(expr*expr)) => match pat_ with (v_,v_') => (Expr_apply (Expr_apply (Expr_bprim Bprim_equal) v_) v_') end ) v_v'_list) ) | Jbprim_equal_constr : forall (v_v'_list:list (expr*expr)) (constr5:constr), (Forall_list (fun (tmp_:(expr*expr)) => match tmp_ with (v_,v_') => Is_true (is_value_of_expr v_) end) v_v'_list) -> (Forall_list (fun (tmp_:(expr*expr)) => match tmp_ with (v_,v_') => Is_true (is_value_of_expr v_') end) v_v'_list) -> JRbprim (Expr_construct constr5 (map (fun (pat_:(expr*expr)) => match pat_ with (v_,v_') => v_ end ) v_v'_list)) Bprim_equal (Expr_construct constr5 (map (fun (pat_:(expr*expr)) => match pat_ with (v_,v_') => v_' end ) v_v'_list)) Lab_nil (fold_right Expr_and CONST_true (map (fun (pat_:(expr*expr)) => match pat_ with (v_,v_') => (Expr_apply (Expr_apply (Expr_bprim Bprim_equal) v_) v_') end ) v_v'_list) ) | Jbprim_equal_constr_false : forall (v'_list:list expr) (v_list:list expr) (constr5:constr) (constr':constr), (Forall_list (fun (v_':expr) => Is_true (is_value_of_expr v_')) v'_list) -> (Forall_list (fun (v_:expr) => Is_true (is_value_of_expr v_)) v_list) -> (~( (CONST_constr constr5) = (CONST_constr constr') )) -> JRbprim (Expr_construct constr5 v_list) Bprim_equal (Expr_construct constr' v'_list) Lab_nil (Expr_constant CONST_false) | Jbprim_equal_const_constr_false : forall (v_list:list expr) (constr':constr) (constr5:constr), (Forall_list (fun (v_:expr) => Is_true (is_value_of_expr v_)) v_list) -> JRbprim (Expr_constant (CONST_constr constr')) Bprim_equal (Expr_construct constr5 v_list) Lab_nil (Expr_constant CONST_false) | Jbprim_equal_constr_const_false : forall (v_list:list expr) (constr5:constr) (constr':constr), (Forall_list (fun (v_:expr) => Is_true (is_value_of_expr v_)) v_list) -> JRbprim (Expr_construct constr5 v_list) Bprim_equal (Expr_constant (CONST_constr constr')) Lab_nil (Expr_constant CONST_false) | Jbprim_equal_rec : forall (fn''_v''_list:list (field_name*expr)) (fn_v_list:list (field_name*expr)) (v':expr), Is_true (is_value_of_expr v') -> (Forall_list (fun (tmp_:(field_name*expr)) => match tmp_ with (fn_'',v_'') => Is_true (is_value_of_expr v_'') end) fn''_v''_list) -> (Forall_list (fun (tmp_:(field_name*expr)) => match tmp_ with (fn_,v_) => Is_true (is_value_of_expr v_) end) fn_v_list) -> ( v' = (Expr_record (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_'',v_'') => ((F_name fn_''),v_'') end ) fn''_v''_list)) ) -> (Permutation (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_,v_) => fn_ end ) fn_v_list) (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_'',v_'') => fn_'' end ) fn''_v''_list) ) -> JRbprim (Expr_record (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_,v_) => ((F_name fn_),v_) end ) fn_v_list)) Bprim_equal v' Lab_nil (fold_right Expr_and CONST_true (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_,v_) => (Expr_apply (Expr_apply (Expr_bprim Bprim_equal) v_) (Expr_field v' (F_name fn_)) ) end ) fn_v_list) ) | Jbprim_plus : forall (intn1:intn) (intn2:intn), JRbprim (Expr_constant (CONST_int intn1)) Bprim_plus (Expr_constant (CONST_int intn2)) Lab_nil (Expr_constant (CONST_int (( intn1 + intn2 )%Z) )) | Jbprim_minus : forall (intn1:intn) (intn2:intn), JRbprim (Expr_constant (CONST_int intn1)) Bprim_minus (Expr_constant (CONST_int intn2)) Lab_nil (Expr_constant (CONST_int (( intn1 - intn2 )%Z) )) | Jbprim_times : forall (intn1:intn) (intn2:intn), JRbprim (Expr_constant (CONST_int intn1)) Bprim_times (Expr_constant (CONST_int intn2)) Lab_nil (Expr_constant (CONST_int (( intn1 * intn2 )%Z) )) | Jbprim_div0 : forall (intn5:intn), JRbprim (Expr_constant (CONST_int intn5)) Bprim_div (Expr_constant (CONST_int ( 0 )%Z )) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) (Expr_constant (CONST_constr C_div_by_0))) | Jbprim_div : forall (intn1:intn) (intn2:intn), (~( (CONST_int intn2) = (CONST_int ( 0 )%Z ) )) -> JRbprim (Expr_constant (CONST_int intn1)) Bprim_div (Expr_constant (CONST_int intn2)) Lab_nil (Expr_constant (CONST_int (( intn1 / intn2 )%Z) )) | Jbprim_assign : forall (l:index) (v:expr), Is_true (is_value_of_expr v) -> JRbprim (Expr_location l) Bprim_assign v (Lab_assign l v) (Expr_constant CONST_unit) . (* defns JRmatching_step *) Inductive (* defn matching_step *) JRmatching_step : expr -> pattern_matching -> pattern_matching -> Prop := | JRmatching_next : forall (pat_e_list:list (pattern*expr)) (pat:pattern) (e:expr) (v:expr), Is_true (is_value_of_expr v) -> (~JM_matchP v pat ) -> (length (map (fun (pat_:(pattern*expr)) => match pat_ with (pat_,e_) => e_ end ) pat_e_list) >= 1 ) -> JRmatching_step v (PM_pm ((app (cons (PE_inj pat e) nil) (app (map (fun (pat_:(pattern*expr)) => match pat_ with (pat_,e_) => (PE_inj pat_ e_) end ) pat_e_list) nil)))) (PM_pm (map (fun (pat_:(pattern*expr)) => match pat_ with (pat_,e_) => (PE_inj pat_ e_) end ) pat_e_list)) . (* defns JRmatching_success *) Inductive (* defn matching_success *) JRmatching_success : expr -> pattern_matching -> expr -> Prop := | JRmatching_found : forall (x_v_list:list (value_name*expr)) (pat_e_list:list (pattern*expr)) (v:expr) (pat:pattern) (e:expr), Is_true (is_value_of_expr v) -> (Forall_list (fun (tmp_:(value_name*expr)) => match tmp_ with (x_,v_) => Is_true (is_value_of_expr v_) end) x_v_list) -> JM_match v pat (substs_x_xs x_v_list) -> JRmatching_success v (PM_pm ((app (cons (PE_inj pat e) nil) (app (map (fun (pat_:(pattern*expr)) => match pat_ with (pat_,e_) => (PE_inj pat_ e_) end ) pat_e_list) nil)))) (substs_value_name_expr (substs_x_proj (substs_x_xs x_v_list) ) e ) | JRmatching_fail : forall (pat:pattern) (e:expr) (v:expr), Is_true (is_value_of_expr v) -> (~JM_matchP v pat ) -> JRmatching_success v (PM_pm (cons (PE_inj pat e) nil)) (Expr_apply (Expr_uprim Uprim_raise) (Expr_constant (CONST_constr C_matchfailure))) . (* defns Jred *) Inductive (* defn expr *) JR_expr : expr -> labelled_arrow -> expr -> Prop := | JR_expr_uprim : forall (unary_prim5:unary_prim) (v:expr) (L:trans_label) (e:expr), Is_true (is_value_of_expr v) -> JRuprim unary_prim5 v L e -> JR_expr (Expr_apply (Expr_uprim unary_prim5) v) L e | JR_expr_bprim : forall (binary_prim5:binary_prim) (v1:expr) (v2:expr) (L:trans_label) (e:expr), Is_true (is_value_of_expr v1) -> Is_true (is_value_of_expr v2) -> JRbprim v1 binary_prim5 v2 L e -> JR_expr (Expr_apply (Expr_apply (Expr_bprim binary_prim5) v1) v2) L e | JR_expr_typed_ctx : forall (e:expr) (t:typexpr), JR_expr (Expr_typed e t) Lab_nil e | JR_expr_apply_ctx_arg : forall (e1:expr) (e0:expr) (L:trans_label) (e0':expr), JR_expr e0 L e0' -> JR_expr (Expr_apply e1 e0) L (Expr_apply e1 e0') | JR_expr_apply_raise1 : forall (e:expr) (v:expr), Is_true (is_value_of_expr v) -> JR_expr (Expr_apply e (Expr_apply (Expr_uprim Uprim_raise) v) ) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) | JR_expr_apply_ctx_fun : forall (e1:expr) (v0:expr) (L:trans_label) (e1':expr), Is_true (is_value_of_expr v0) -> JR_expr e1 L e1' -> JR_expr (Expr_apply e1 v0) L (Expr_apply e1' v0) | JR_expr_apply_raise2 : forall (v:expr) (v':expr), Is_true (is_value_of_expr v) -> Is_true (is_value_of_expr v') -> JR_expr (Expr_apply (Expr_apply (Expr_uprim Uprim_raise) v) v') Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) | JR_expr_apply : forall (pattern_matching5:pattern_matching) (v0:expr), Is_true (is_value_of_expr v0) -> JR_expr (Expr_apply (Expr_function pattern_matching5) v0) Lab_nil (Expr_match v0 pattern_matching5) | JR_expr_let_ctx : forall (pat:pattern) (e0:expr) (e:expr) (L:trans_label) (e0':expr), JR_expr e0 L e0' -> JR_expr (Expr_let (LB_simple pat e0) e) L (Expr_let (LB_simple pat e0') e) | JR_expr_let_raise : forall (pat:pattern) (v:expr) (e:expr), Is_true (is_value_of_expr v) -> JR_expr (Expr_let (LB_simple pat (Expr_apply (Expr_uprim Uprim_raise) v)) e) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) | JR_expr_let_subst : forall (x_v_list:list (value_name*expr)) (pat:pattern) (v:expr) (e:expr), Is_true (is_value_of_expr v) -> (Forall_list (fun (tmp_:(value_name*expr)) => match tmp_ with (x_,v_) => Is_true (is_value_of_expr v_) end) x_v_list) -> JM_match v pat (substs_x_xs x_v_list) -> JR_expr (Expr_let (LB_simple pat v) e) Lab_nil (substs_value_name_expr (substs_x_proj (substs_x_xs x_v_list) ) e ) | JR_expr_let_fail : forall (pat:pattern) (e:expr) (v:expr), Is_true (is_value_of_expr v) -> (~JM_matchP v pat ) -> JR_expr (Expr_let (LB_simple pat v) e) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) (Expr_constant (CONST_constr C_matchfailure))) | JR_expr_letrec : forall (x_e_pattern_matching_list:list (value_name*expr*pattern_matching)) (letrec_bindings5:letrec_bindings) (e:expr), ( letrec_bindings5 = (LRBs_inj (map (fun (pat_:(value_name*expr*pattern_matching)) => match pat_ with (x_,e_,pattern_matching_) => (LRB_simple x_ pattern_matching_) end ) x_e_pattern_matching_list)) ) -> (forall (pattern_matching_:pattern_matching) (e_:expr), In (letrec_bindings5,pattern_matching_,e_) (map (fun (pat_:value_name*expr*pattern_matching) => match pat_ with (x_,e_,pattern_matching_) => (letrec_bindings5,pattern_matching_,e_) end) x_e_pattern_matching_list) -> (Jrecfun letrec_bindings5 pattern_matching_ e_)) -> JR_expr (Expr_letrec letrec_bindings5 e) Lab_nil (substs_value_name_expr (substs_x_proj (substs_x_xs (map (fun (pat_:(value_name*expr*pattern_matching)) => match pat_ with (x_,e_,pattern_matching_) => (x_,e_) end ) x_e_pattern_matching_list)) ) e ) | JR_expr_sequence_ctx_left : forall (e1:expr) (e2:expr) (L:trans_label) (e1':expr), JR_expr e1 L e1' -> JR_expr (Expr_sequence e1 e2) L (Expr_sequence e1' e2) | JR_expr_sequence_raise : forall (v:expr) (e:expr), Is_true (is_value_of_expr v) -> JR_expr (Expr_sequence (Expr_apply (Expr_uprim Uprim_raise) v) e) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) | JR_expr_sequence : forall (v:expr) (e2:expr), Is_true (is_value_of_expr v) -> JR_expr (Expr_sequence v e2) Lab_nil e2 | JR_expr_ifthenelse_ctx : forall (e1:expr) (e2:expr) (e3:expr) (L:trans_label) (e1':expr), JR_expr e1 L e1' -> JR_expr (Expr_ifthenelse e1 e2 e3) L (Expr_ifthenelse e1' e2 e3) | JR_expr_if_raise : forall (v:expr) (e1:expr) (e2:expr), Is_true (is_value_of_expr v) -> JR_expr (Expr_ifthenelse (Expr_apply (Expr_uprim Uprim_raise) v) e1 e2) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) | JR_expr_ifthenelse_true : forall (e2:expr) (e3:expr), JR_expr (Expr_ifthenelse (Expr_constant CONST_true) e2 e3) Lab_nil e2 | JR_expr_ifthenelse_false : forall (e2:expr) (e3:expr), JR_expr (Expr_ifthenelse (Expr_constant CONST_false) e2 e3) Lab_nil e3 | JR_expr_match_ctx : forall (e:expr) (pattern_matching5:pattern_matching) (L:trans_label) (e':expr), JR_expr e L e' -> JR_expr (Expr_match e pattern_matching5) L (Expr_match e' pattern_matching5) | JR_expr_match_raise : forall (v:expr) (pattern_matching5:pattern_matching), Is_true (is_value_of_expr v) -> JR_expr (Expr_match (Expr_apply (Expr_uprim Uprim_raise) v) pattern_matching5) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) | JR_expr_match_step : forall (v:expr) (pattern_matching5:pattern_matching) (pattern_matching':pattern_matching), Is_true (is_value_of_expr v) -> JRmatching_step v pattern_matching5 pattern_matching' -> JR_expr (Expr_match v pattern_matching5) Lab_nil (Expr_match v pattern_matching') | JR_expr_match_success : forall (v:expr) (pattern_matching5:pattern_matching) (e':expr), Is_true (is_value_of_expr v) -> JRmatching_success v pattern_matching5 e' -> JR_expr (Expr_match v pattern_matching5) Lab_nil e' | JR_expr_and : forall (e1:expr) (e2:expr), JR_expr (Expr_and e1 e2) Lab_nil (Expr_ifthenelse e1 e2 (Expr_constant CONST_false)) | JR_expr_or : forall (e1:expr) (e2:expr), JR_expr (Expr_or e1 e2) Lab_nil (Expr_ifthenelse e1 (Expr_constant CONST_true) e2) | JR_expr_while : forall (e1:expr) (e2:expr), JR_expr (Expr_while e1 e2) Lab_nil (Expr_ifthenelse e1 (Expr_sequence e2 (Expr_while e1 e2)) (Expr_constant CONST_unit)) | JR_expr_for_ctx1 : forall (x:value_name) (e1:expr) (for_dirn5:for_dirn) (e2:expr) (e3:expr) (L:trans_label) (e1':expr), JR_expr e1 L e1' -> JR_expr (Expr_for x e1 for_dirn5 e2 e3) L (Expr_for x e1' for_dirn5 e2 e3) | JR_expr_for_raise1 : forall (x:value_name) (v:expr) (for_dirn5:for_dirn) (e2:expr) (e3:expr), Is_true (is_value_of_expr v) -> JR_expr (Expr_for x (Expr_apply (Expr_uprim Uprim_raise) v) for_dirn5 e2 e3) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) | JR_expr_for_ctx2 : forall (x:value_name) (v1:expr) (for_dirn5:for_dirn) (e2:expr) (e3:expr) (L:trans_label) (e2':expr), Is_true (is_value_of_expr v1) -> JR_expr e2 L e2' -> JR_expr (Expr_for x v1 for_dirn5 e2 e3) L (Expr_for x v1 for_dirn5 e2' e3) | JR_expr_for_raise2 : forall (x:value_name) (v:expr) (for_dirn5:for_dirn) (v':expr) (e3:expr), Is_true (is_value_of_expr v) -> Is_true (is_value_of_expr v') -> JR_expr (Expr_for x v for_dirn5 (Expr_apply (Expr_uprim Uprim_raise) v') e3) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v') | JR_expr_for_to_do : forall (x:value_name) (intn1:intn) (intn2:intn) (e:expr), (( intn1 <= intn2 )%Z) -> JR_expr (Expr_for x (Expr_constant (CONST_int intn1)) FD_upto (Expr_constant (CONST_int intn2)) e) Lab_nil (Expr_sequence (Expr_let (LB_simple (P_var x) (Expr_constant (CONST_int intn1))) e) (Expr_for x (Expr_constant (CONST_int (( intn1 + ( 1 )%Z )%Z) )) FD_upto (Expr_constant (CONST_int intn2)) e)) | JR_expr_for_to_done : forall (x:value_name) (intn1:intn) (intn2:intn) (e:expr), (( intn1 > intn2 )%Z) -> JR_expr (Expr_for x (Expr_constant (CONST_int intn1)) FD_upto (Expr_constant (CONST_int intn2)) e) Lab_nil (Expr_constant CONST_unit) | JR_expr_for_downto_do : forall (x:value_name) (intn1:intn) (intn2:intn) (e:expr), (( intn2 <= intn1 )%Z) -> JR_expr (Expr_for x (Expr_constant (CONST_int intn1)) FD_downto (Expr_constant (CONST_int intn2)) e) Lab_nil (Expr_sequence (Expr_let (LB_simple (P_var x) (Expr_constant (CONST_int intn1))) e) (Expr_for x (Expr_constant (CONST_int (( intn1 - ( 1 )%Z )%Z) )) FD_downto (Expr_constant (CONST_int intn2)) e)) | JR_expr_for_downto_done : forall (x:value_name) (intn1:intn) (intn2:intn) (e:expr), (( intn2 > intn1 )%Z) -> JR_expr (Expr_for x (Expr_constant (CONST_int intn1)) FD_downto (Expr_constant (CONST_int intn2)) e) Lab_nil (Expr_constant CONST_unit) | JR_expr_try_ctx : forall (e:expr) (pattern_matching5:pattern_matching) (L:trans_label) (e':expr), JR_expr e L e' -> JR_expr (Expr_try e pattern_matching5) L (Expr_try e' pattern_matching5) | JR_expr_try_return : forall (v:expr) (pattern_matching5:pattern_matching), Is_true (is_value_of_expr v) -> JR_expr (Expr_try v pattern_matching5) Lab_nil v | JR_expr_try_catch : forall (pat_exp_list:list pat_exp) (v:expr), Is_true (is_value_of_expr v) -> JR_expr (Expr_try (Expr_apply (Expr_uprim Uprim_raise) v) (PM_pm pat_exp_list)) Lab_nil (Expr_match v (PM_pm ((app pat_exp_list (app (cons (PE_inj P_any (Expr_apply (Expr_uprim Uprim_raise) v) ) nil) nil))))) | JR_expr_tuple_ctx : forall (v_list:list expr) (e_list:list expr) (e:expr) (L:trans_label) (e':expr), (Forall_list (fun (v_:expr) => Is_true (is_value_of_expr v_)) v_list) -> JR_expr e L e' -> JR_expr (Expr_tuple ((app e_list (app (cons e nil) (app v_list nil))))) L (Expr_tuple ((app e_list (app (cons e' nil) (app v_list nil))))) | JR_expr_tuple_raise : forall (v_list:list expr) (e_list:list expr) (v:expr), Is_true (is_value_of_expr v) -> (Forall_list (fun (v_:expr) => Is_true (is_value_of_expr v_)) v_list) -> JR_expr (Expr_tuple ((app e_list (app (cons (Expr_apply (Expr_uprim Uprim_raise) v) nil) (app v_list nil))))) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) | JR_expr_constr_ctx : forall (v_list:list expr) (e_list:list expr) (constr5:constr) (e:expr) (L:trans_label) (e':expr), (Forall_list (fun (v_:expr) => Is_true (is_value_of_expr v_)) v_list) -> JR_expr e L e' -> JR_expr (Expr_construct constr5 ((app e_list (app (cons e nil) (app v_list nil))))) L (Expr_construct constr5 ((app e_list (app (cons e' nil) (app v_list nil))))) | JR_expr_constr_raise : forall (v_list:list expr) (e_list:list expr) (constr5:constr) (v:expr), Is_true (is_value_of_expr v) -> (Forall_list (fun (v_:expr) => Is_true (is_value_of_expr v_)) v_list) -> JR_expr (Expr_construct constr5 ((app e_list (app (cons (Expr_apply (Expr_uprim Uprim_raise) v) nil) (app v_list nil))))) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) | JR_expr_cons_ctx1 : forall (e0:expr) (e:expr) (L:trans_label) (e':expr), JR_expr e L e' -> JR_expr (Expr_cons e0 e) L (Expr_cons e0 e') | JR_expr_cons_raise1 : forall (e:expr) (v:expr), Is_true (is_value_of_expr v) -> JR_expr (Expr_cons e (Expr_apply (Expr_uprim Uprim_raise) v) ) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) | JR_expr_cons_ctx2 : forall (e:expr) (v:expr) (L:trans_label) (e':expr), Is_true (is_value_of_expr v) -> JR_expr e L e' -> JR_expr (Expr_cons e v) L (Expr_cons e' v) | JR_expr_cons_raise2 : forall (v:expr) (v':expr), Is_true (is_value_of_expr v) -> Is_true (is_value_of_expr v') -> JR_expr (Expr_cons (Expr_apply (Expr_uprim Uprim_raise) v) v') Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) | JR_expr_record_ctx : forall (fn'_v_list:list (field_name*expr)) (fn_e_list:list (field_name*expr)) (field_name5:field_name) (expr5:expr) (L:trans_label) (expr':expr), (Forall_list (fun (tmp_:(field_name*expr)) => match tmp_ with (fn_',v_) => Is_true (is_value_of_expr v_) end) fn'_v_list) -> JR_expr expr5 L expr' -> JR_expr (Expr_record ((app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_,e_) => ((F_name fn_),e_) end ) fn_e_list) (app (cons ((F_name field_name5),expr5) nil) (app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_',v_) => ((F_name fn_'),v_) end ) fn'_v_list) nil))))) L (Expr_record ((app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_,e_) => ((F_name fn_),e_) end ) fn_e_list) (app (cons ((F_name field_name5),expr') nil) (app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_',v_) => ((F_name fn_'),v_) end ) fn'_v_list) nil))))) | JR_expr_record_raise : forall (fn'_v_list:list (field_name*expr)) (fn_e_list:list (field_name*expr)) (fn:field_name) (v:expr), Is_true (is_value_of_expr v) -> (Forall_list (fun (tmp_:(field_name*expr)) => match tmp_ with (fn_',v_) => Is_true (is_value_of_expr v_) end) fn'_v_list) -> JR_expr (Expr_record ((app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_,e_) => ((F_name fn_),e_) end ) fn_e_list) (app (cons ((F_name fn),(Expr_apply (Expr_uprim Uprim_raise) v)) nil) (app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_',v_) => ((F_name fn_'),v_) end ) fn'_v_list) nil))))) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) | JR_expr_record_with_ctx1 : forall (fn'_v_list:list (field_name*expr)) (fn_e_list:list (field_name*expr)) (v:expr) (field_name5:field_name) (e:expr) (L:trans_label) (e':expr), Is_true (is_value_of_expr v) -> (Forall_list (fun (tmp_:(field_name*expr)) => match tmp_ with (fn_',v_) => Is_true (is_value_of_expr v_) end) fn'_v_list) -> JR_expr e L e' -> JR_expr (Expr_override v ((app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_,e_) => ((F_name fn_),e_) end ) fn_e_list) (app (cons ((F_name field_name5),e) nil) (app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_',v_) => ((F_name fn_'),v_) end ) fn'_v_list) nil))))) L (Expr_override v ((app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_,e_) => ((F_name fn_),e_) end ) fn_e_list) (app (cons ((F_name field_name5),e') nil) (app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_',v_) => ((F_name fn_'),v_) end ) fn'_v_list) nil))))) | JR_expr_record_with_raise1 : forall (fn'_v_list:list (field_name*expr)) (fn_e_list:list (field_name*expr)) (v':expr) (fn:field_name) (v:expr), Is_true (is_value_of_expr v') -> Is_true (is_value_of_expr v) -> (Forall_list (fun (tmp_:(field_name*expr)) => match tmp_ with (fn_',v_) => Is_true (is_value_of_expr v_) end) fn'_v_list) -> JR_expr (Expr_override v' ((app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_,e_) => ((F_name fn_),e_) end ) fn_e_list) (app (cons ((F_name fn),(Expr_apply (Expr_uprim Uprim_raise) v)) nil) (app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_',v_) => ((F_name fn_'),v_) end ) fn'_v_list) nil))))) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) | JR_expr_record_with_ctx2 : forall (field_name_e_list:list (field_name*expr)) (e:expr) (L:trans_label) (e':expr), JR_expr e L e' -> JR_expr (Expr_override e (map (fun (pat_:(field_name*expr)) => match pat_ with (field_name_,e_) => ((F_name field_name_),e_) end ) field_name_e_list)) L (Expr_override e' (map (fun (pat_:(field_name*expr)) => match pat_ with (field_name_,e_) => ((F_name field_name_),e_) end ) field_name_e_list)) | JR_expr_record_raise_ctx2 : forall (field_name_e_list:list (field_name*expr)) (v:expr), Is_true (is_value_of_expr v) -> JR_expr (Expr_override (Expr_apply (Expr_uprim Uprim_raise) v) (map (fun (pat_:(field_name*expr)) => match pat_ with (field_name_,e_) => ((F_name field_name_),e_) end ) field_name_e_list)) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) | JR_expr_record_with_many : forall (fn''_v''_list:list (field_name*expr)) (fn'_v'_list:list (field_name*expr)) (fn_v_list:list (field_name*expr)) (field_name5:field_name) (v:expr) (v':expr), Is_true (is_value_of_expr v) -> Is_true (is_value_of_expr v') -> (Forall_list (fun (tmp_:(field_name*expr)) => match tmp_ with (fn_'',v_'') => Is_true (is_value_of_expr v_'') end) fn''_v''_list) -> (Forall_list (fun (tmp_:(field_name*expr)) => match tmp_ with (fn_',v_') => Is_true (is_value_of_expr v_') end) fn'_v'_list) -> (Forall_list (fun (tmp_:(field_name*expr)) => match tmp_ with (fn_,v_) => Is_true (is_value_of_expr v_) end) fn_v_list) -> (length (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_'',v_'') => v_'' end ) fn''_v''_list) >= 1 ) -> (~In (name_fn field_name5) (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_,v_) => (name_fn fn_) end ) fn_v_list) ) -> JR_expr (Expr_override (Expr_record ((app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_,v_) => ((F_name fn_),v_) end ) fn_v_list) (app (cons ((F_name field_name5),v) nil) (app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_',v_') => ((F_name fn_'),v_') end ) fn'_v'_list) nil))))) ((app (cons ((F_name field_name5),v') nil) (app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_'',v_'') => ((F_name fn_''),v_'') end ) fn''_v''_list) nil)))) Lab_nil (Expr_override (Expr_record ((app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_,v_) => ((F_name fn_),v_) end ) fn_v_list) (app (cons ((F_name field_name5),v') nil) (app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_',v_') => ((F_name fn_'),v_') end ) fn'_v'_list) nil))))) (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_'',v_'') => ((F_name fn_''),v_'') end ) fn''_v''_list)) | JR_expr_record_with_1 : forall (fn'_v'_list:list (field_name*expr)) (fn_v_list:list (field_name*expr)) (field_name5:field_name) (v:expr) (v':expr), Is_true (is_value_of_expr v) -> Is_true (is_value_of_expr v') -> (Forall_list (fun (tmp_:(field_name*expr)) => match tmp_ with (fn_',v_') => Is_true (is_value_of_expr v_') end) fn'_v'_list) -> (Forall_list (fun (tmp_:(field_name*expr)) => match tmp_ with (fn_,v_) => Is_true (is_value_of_expr v_) end) fn_v_list) -> (~In (name_fn field_name5) (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_,v_) => (name_fn fn_) end ) fn_v_list) ) -> JR_expr (Expr_override (Expr_record ((app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_,v_) => ((F_name fn_),v_) end ) fn_v_list) (app (cons ((F_name field_name5),v) nil) (app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_',v_') => ((F_name fn_'),v_') end ) fn'_v'_list) nil))))) (cons ((F_name field_name5),v') nil)) Lab_nil (Expr_record ((app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_,v_) => ((F_name fn_),v_) end ) fn_v_list) (app (cons ((F_name field_name5),v') nil) (app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_',v_') => ((F_name fn_'),v_') end ) fn'_v'_list) nil))))) | JR_expr_record_access_ctx : forall (e:expr) (field_name5:field_name) (L:trans_label) (e':expr), JR_expr e L e' -> JR_expr (Expr_field e (F_name field_name5)) L (Expr_field e' (F_name field_name5)) | JR_expr_record_access_raise : forall (v:expr) (field_name5:field_name), Is_true (is_value_of_expr v) -> JR_expr (Expr_field (Expr_apply (Expr_uprim Uprim_raise) v) (F_name field_name5)) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) | JR_expr_record_access : forall (fn'_v'_list:list (field_name*expr)) (fn_v_list:list (field_name*expr)) (field_name5:field_name) (v:expr), Is_true (is_value_of_expr v) -> (Forall_list (fun (tmp_:(field_name*expr)) => match tmp_ with (fn_',v_') => Is_true (is_value_of_expr v_') end) fn'_v'_list) -> (Forall_list (fun (tmp_:(field_name*expr)) => match tmp_ with (fn_,v_) => Is_true (is_value_of_expr v_) end) fn_v_list) -> (~In (name_fn field_name5) (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_,v_) => (name_fn fn_) end ) fn_v_list) ) -> JR_expr (Expr_field (Expr_record ((app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_,v_) => ((F_name fn_),v_) end ) fn_v_list) (app (cons ((F_name field_name5),v) nil) (app (map (fun (pat_:(field_name*expr)) => match pat_ with (fn_',v_') => ((F_name fn_'),v_') end ) fn'_v'_list) nil))))) (F_name field_name5)) Lab_nil v | JR_expr_assert_ctx : forall (e:expr) (L:trans_label) (e':expr), JR_expr e L e' -> JR_expr (Expr_assert e) L (Expr_assert e') | JR_expr_assert_raise : forall (v:expr), Is_true (is_value_of_expr v) -> JR_expr (Expr_assert (Expr_apply (Expr_uprim Uprim_raise) v) ) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) v) | JR_expr_assert_true : JR_expr (Expr_assert (Expr_constant CONST_true)) Lab_nil (Expr_constant CONST_unit) | JR_expr_assert_false : JR_expr (Expr_assert (Expr_constant CONST_false)) Lab_nil (Expr_apply (Expr_uprim Uprim_raise) (Expr_constant (CONST_constr C_assertfailure))) . (* defns JRdefn *) Inductive (* defn Rdefn *) JRdefn : definitions -> program -> labelled_arrow -> definitions -> program -> Prop := | Jdefn_let_ctx : forall (ds_value:definitions) (pat:pattern) (e:expr) (definitions5:definitions) (L:trans_label) (e':expr), Is_true (is_definitions_value_of_definitions ds_value) -> JR_expr e L e' -> JRdefn ds_value (Prog_defs (Ds_cons (D_let (LB_simple pat e)) definitions5 ) ) L ds_value (Prog_defs (Ds_cons (D_let (LB_simple pat e')) definitions5 ) ) | Jdefn_let_raise : forall (ds_value:definitions) (pat:pattern) (v:expr) (definitions5:definitions), Is_true (is_definitions_value_of_definitions ds_value) -> Is_true (is_value_of_expr v) -> JRdefn ds_value (Prog_defs (Ds_cons (D_let (LB_simple pat (Expr_apply (Expr_uprim Uprim_raise) v))) definitions5 ) ) Lab_nil ds_value (Prog_raise v) | Jdefn_let_match : forall (x_v_list:list (value_name*expr)) (ds_value:definitions) (pat:pattern) (v:expr) (definitions5:definitions), Is_true (is_definitions_value_of_definitions ds_value) -> Is_true (is_value_of_expr v) -> (Forall_list (fun (tmp_:(value_name*expr)) => match tmp_ with (x_,v_) => Is_true (is_value_of_expr v_) end) x_v_list) -> JM_match v pat (substs_x_xs x_v_list) -> JRdefn ds_value (Prog_defs (Ds_cons (D_let (LB_simple pat v)) definitions5 ) ) Lab_nil ds_value (Prog_defs (substs_value_name_definitions (substs_x_proj (substs_x_xs (map (fun (pat_:(value_name*expr)) => match pat_ with (x_,v_) => (x_, (remv_tyvar_expr v_ ) ) end ) x_v_list)) ) definitions5 ) ) | Jdefn_let_not_match : forall (ds_value:definitions) (pat:pattern) (definitions5:definitions) (v:expr), Is_true (is_definitions_value_of_definitions ds_value) -> Is_true (is_value_of_expr v) -> (~JM_matchP v pat ) -> JRdefn ds_value (Prog_defs (Ds_cons (D_let (LB_simple pat v)) definitions5 ) ) Lab_nil ds_value (Prog_raise (Expr_constant (CONST_constr C_matchfailure))) | Jdefn_letrec : forall (x_e_pattern_matching_list:list (value_name*expr*pattern_matching)) (ds_value:definitions) (letrec_bindings5:letrec_bindings) (definitions5:definitions), Is_true (is_definitions_value_of_definitions ds_value) -> ( letrec_bindings5 = (LRBs_inj (map (fun (pat_:(value_name*expr*pattern_matching)) => match pat_ with (x_,e_,pattern_matching_) => (LRB_simple x_ pattern_matching_) end ) x_e_pattern_matching_list)) ) -> (forall (pattern_matching_:pattern_matching) (e_:expr), In (letrec_bindings5,pattern_matching_,e_) (map (fun (pat_:value_name*expr*pattern_matching) => match pat_ with (x_,e_,pattern_matching_) => (letrec_bindings5,pattern_matching_,e_) end) x_e_pattern_matching_list) -> (Jrecfun letrec_bindings5 pattern_matching_ e_)) -> JRdefn ds_value (Prog_defs (Ds_cons (D_letrec letrec_bindings5) definitions5 ) ) Lab_nil ds_value (Prog_defs (substs_value_name_definitions (substs_x_proj (substs_x_xs (map (fun (pat_:(value_name*expr*pattern_matching)) => match pat_ with (x_,e_,pattern_matching_) => (x_, (remv_tyvar_expr e_ ) ) end ) x_e_pattern_matching_list)) ) definitions5 ) ) | Jdefn_type : forall (ds_value:definitions) (type_definition5:type_definition) (definitions5:definitions), Is_true (is_definitions_value_of_definitions ds_value) -> JRdefn ds_value (Prog_defs (Ds_cons (D_type type_definition5) definitions5 ) ) Lab_nil (definitions_snoc ds_value (D_type type_definition5) ) (Prog_defs definitions5) | Jdefn_exn : forall (ds_value:definitions) (exception_definition5:exception_definition) (definitions5:definitions), Is_true (is_definitions_value_of_definitions ds_value) -> JRdefn ds_value (Prog_defs (Ds_cons (D_exception exception_definition5) definitions5 ) ) Lab_nil (definitions_snoc ds_value (D_exception exception_definition5) ) (Prog_defs definitions5) . (* defns JSlookup *) Inductive (* defn lookup *) JSlookup : store -> location -> expr -> Prop := | JSstlookup_rec : forall (st:store) (l':index) (e:expr) (l:index) (e':expr), JSlookup st l e' -> (~( (name_l l) = (name_l l') )) -> JSlookup (cons ( l' , e ) st ) l e' | JSstlookup_found : forall (st:store) (l:index) (e:expr), JSlookup (cons ( l , e ) st ) l e . (* defns JRstore *) Inductive (* defn store *) JRstore : store -> labelled_arrow -> store -> Prop := | JRstore_empty : forall (st:store), JRstore st Lab_nil st | JRstore_lookup : forall (st:store) (l:index) (v:expr), Is_true (is_value_of_expr v) -> JSlookup st l v -> JRstore st (Lab_deref l v) st | JRstore_assign : forall (st:store) (l:index) (expr5:expr) (st':store) (v:expr), Is_true (is_value_of_expr v) -> (forall v8, ~JSlookup st' l v8) -> JRstore (app st' (cons ( l , expr5 ) st )) (Lab_assign l v) (app st' (cons ( l , (remv_tyvar_expr v ) ) st )) | JRstore_alloc : forall (st:store) (l:index) (v:expr), Is_true (is_value_of_expr v) -> (forall v8, ~JSlookup st l v8) -> JRstore st (Lab_alloc v l) (cons ( l , (remv_tyvar_expr v ) ) st ) . (* defns JRtop *) Inductive (* defn top *) JRtop : definitions -> program -> store -> definitions -> program -> store -> Prop := | JRtop_defs : forall (definitions_value5:definitions) (program5:program) (store5:store) (definitions5:definitions) (program':program) (store':store) (L:trans_label), Is_true (is_definitions_value_of_definitions definitions_value5) -> JRstore store5 L store' -> JRdefn definitions_value5 program5 L definitions5 program' -> JRtop definitions_value5 program5 store5 definitions5 program' store' . (* defns Jebehaviour *) Inductive (* defn ebehaviour *) JRB_ebehaviour : expr -> Prop := | JRB_ebehaviour_value : forall (v:expr), Is_true (is_value_of_expr v) -> JRB_ebehaviour v | JRB_ebehaviour_reduces : forall (e:expr) (L:trans_label) (e':expr), JR_expr e L e' -> JRB_ebehaviour e | JRB_ebehaviour_raises : forall (v:expr), Is_true (is_value_of_expr v) -> JRB_ebehaviour (Expr_apply (Expr_uprim Uprim_raise) v) . (* defns Jdbehaviour *) Inductive (* defn dbehaviour *) JRB_dbehaviour : definitions -> program -> store -> Prop := | JRB_behaviour_value : forall (definitions_value5:definitions) (store5:store), Is_true (is_definitions_value_of_definitions definitions_value5) -> JRB_dbehaviour definitions_value5 (Prog_defs Ds_nil) store5 | JRB_behaviour_reduces : forall (definitions_value5:definitions) (program5:program) (store5:store) (definitions':definitions) (program':program) (store':store), Is_true (is_definitions_value_of_definitions definitions_value5) -> JRtop definitions_value5 program5 store5 definitions' program' store' -> JRB_dbehaviour definitions_value5 program5 store5 | JRB_behaviour_raises : forall (definitions_value5:definitions) (v:expr) (store5:store), Is_true (is_definitions_value_of_definitions definitions_value5) -> Is_true (is_value_of_expr v) -> JRB_dbehaviour definitions_value5 (Prog_raise v) store5 . Hint Constructors JdomEB JdomE Jlookup_EB Jidx_bound JTtps_kind JTEok JTtypeconstr JTts JTtsnamed JTt JTeq JTidxsub JTinst JTinst_named JTinst_any JTvalue_name JTfield JTconstr_p JTconstr_c JTconst JTpat JTuprim JTbprim JTe JTpat_matching JTlet_binding JTletrec_binding JTstore JTLin JTLout : rules. Hint Constructors JTconstr_decl JTfield_decl JTtypedef JTtype_definition JTdefinition JTdefinitions JTprog JTtop : rules. Hint Constructors JM_matchP JM_match Jrecfun Jfunval JRuprim JRbprim JRmatching_step JRmatching_success JR_expr JRdefn JSlookup JRstore JRB_ebehaviour : rules. Hint Constructors JRdefn JRtop JRB_dbehaviour : rules. (** induction principles *) Section typexpr_rect. Variables (P_typexpr : typexpr -> Prop) (P_list_typexpr : list typexpr -> Prop). Hypothesis (H_TE_var : forall (typevar5:typevar), P_typexpr (TE_var typevar5)) (H_TE_idxvar : forall (idx5:idx), forall (num:idx), P_typexpr (TE_idxvar idx5 num)) (H_TE_any : P_typexpr TE_any) (H_TE_arrow : forall (typexpr1:typexpr), P_typexpr typexpr1 -> forall (typexpr2:typexpr), P_typexpr typexpr2 -> P_typexpr (TE_arrow typexpr1 typexpr2)) (H_TE_tuple : forall (typexpr_list:list typexpr), P_list_typexpr typexpr_list -> P_typexpr (TE_tuple typexpr_list)) (H_TE_constr : forall (typexpr_list:list typexpr), P_list_typexpr typexpr_list -> forall (typeconstr5:typeconstr), P_typexpr (TE_constr typexpr_list typeconstr5)) (H_list_typexpr_nil : P_list_typexpr nil) (H_list_typexpr_cons : forall (typexpr0:typexpr), P_typexpr typexpr0 -> forall (typexpr_l:list typexpr), P_list_typexpr typexpr_l -> P_list_typexpr (cons typexpr0 typexpr_l)). Fixpoint typexpr_ott_ind (n:typexpr) : P_typexpr n := match n as x return P_typexpr x with | (TE_var typevar5) => H_TE_var typevar5 | (TE_idxvar idx5 num) => H_TE_idxvar idx5 num | TE_any => H_TE_any | (TE_arrow typexpr1 typexpr2) => H_TE_arrow typexpr1 (typexpr_ott_ind typexpr1) typexpr2 (typexpr_ott_ind typexpr2) | (TE_tuple typexpr_list) => H_TE_tuple typexpr_list (((fix typexpr_list_ott_ind (typexpr_l:list typexpr) : P_list_typexpr typexpr_l := match typexpr_l as x return P_list_typexpr x with nil => H_list_typexpr_nil | cons typexpr1 xl => H_list_typexpr_cons typexpr1(typexpr_ott_ind typexpr1)xl (typexpr_list_ott_ind xl) end)) typexpr_list) | (TE_constr typexpr_list typeconstr5) => H_TE_constr typexpr_list (((fix typexpr_list_ott_ind (typexpr_l:list typexpr) : P_list_typexpr typexpr_l := match typexpr_l as x return P_list_typexpr x with nil => H_list_typexpr_nil | cons typexpr2 xl => H_list_typexpr_cons typexpr2(typexpr_ott_ind typexpr2)xl (typexpr_list_ott_ind xl) end)) typexpr_list) typeconstr5 end. End typexpr_rect. Section pattern_rect. Variables (P_list_pattern : list pattern -> Prop) (P_list_field_pattern : list (field*pattern) -> Prop) (P_pattern : pattern -> Prop). Hypothesis (H_P_var : forall (value_name5:value_name), P_pattern (P_var value_name5)) (H_P_any : P_pattern P_any) (H_P_constant : forall (constant5:constant), P_pattern (P_constant constant5)) (H_P_alias : forall (pattern5:pattern), P_pattern pattern5 -> forall (value_name5:value_name), P_pattern (P_alias pattern5 value_name5)) (H_P_typed : forall (pattern5:pattern), P_pattern pattern5 -> forall (typexpr5:typexpr), P_pattern (P_typed pattern5 typexpr5)) (H_P_or : forall (pattern1:pattern), P_pattern pattern1 -> forall (pattern2:pattern), P_pattern pattern2 -> P_pattern (P_or pattern1 pattern2)) (H_P_construct : forall (pattern_list:list pattern), P_list_pattern pattern_list -> forall (constr5:constr), P_pattern (P_construct constr5 pattern_list)) (H_P_construct_any : forall (constr5:constr), P_pattern (P_construct_any constr5)) (H_P_tuple : forall (pattern_list:list pattern), P_list_pattern pattern_list -> P_pattern (P_tuple pattern_list)) (H_P_record : forall (field_pattern_list:list (field*pattern)), P_list_field_pattern field_pattern_list -> P_pattern (P_record field_pattern_list)) (H_P_cons : forall (pattern1:pattern), P_pattern pattern1 -> forall (pattern2:pattern), P_pattern pattern2 -> P_pattern (P_cons pattern1 pattern2)) (H_list_pattern_nil : P_list_pattern nil) (H_list_pattern_cons : forall (pattern0:pattern), P_pattern pattern0 -> forall (pattern_l:list pattern), P_list_pattern pattern_l -> P_list_pattern (cons pattern0 pattern_l)) (H_list_field_pattern_nil : P_list_field_pattern nil) (H_list_field_pattern_cons : forall (field0:field), forall (pattern1:pattern), P_pattern pattern1 -> forall (field_pattern_l:list (field*pattern)), P_list_field_pattern field_pattern_l -> P_list_field_pattern (cons (field0,pattern1) field_pattern_l)). Fixpoint pattern_ott_ind (n:pattern) : P_pattern n := match n as x return P_pattern x with | (P_var value_name5) => H_P_var value_name5 | P_any => H_P_any | (P_constant constant5) => H_P_constant constant5 | (P_alias pattern5 value_name5) => H_P_alias pattern5 (pattern_ott_ind pattern5) value_name5 | (P_typed pattern5 typexpr5) => H_P_typed pattern5 (pattern_ott_ind pattern5) typexpr5 | (P_or pattern1 pattern2) => H_P_or pattern1 (pattern_ott_ind pattern1) pattern2 (pattern_ott_ind pattern2) | (P_construct constr5 pattern_list) => H_P_construct pattern_list (((fix pattern_list_ott_ind (pattern_l:list pattern) : P_list_pattern pattern_l := match pattern_l as x return P_list_pattern x with nil => H_list_pattern_nil | cons pattern2 xl => H_list_pattern_cons pattern2(pattern_ott_ind pattern2)xl (pattern_list_ott_ind xl) end)) pattern_list) constr5 | (P_construct_any constr5) => H_P_construct_any constr5 | (P_tuple pattern_list) => H_P_tuple pattern_list (((fix pattern_list_ott_ind (pattern_l:list pattern) : P_list_pattern pattern_l := match pattern_l as x return P_list_pattern x with nil => H_list_pattern_nil | cons pattern3 xl => H_list_pattern_cons pattern3(pattern_ott_ind pattern3)xl (pattern_list_ott_ind xl) end)) pattern_list) | (P_record field_pattern_list) => H_P_record field_pattern_list (((fix field_pattern_list_ott_ind (field_pattern_l:list (field*pattern)) : P_list_field_pattern field_pattern_l := match field_pattern_l as x return P_list_field_pattern x with nil => H_list_field_pattern_nil | cons (field1,pattern4) xl => H_list_field_pattern_cons field1 pattern4(pattern_ott_ind pattern4)xl (field_pattern_list_ott_ind xl) end)) field_pattern_list) | (P_cons pattern1 pattern2) => H_P_cons pattern1 (pattern_ott_ind pattern1) pattern2 (pattern_ott_ind pattern2) end. End pattern_rect. Section substs_x_rect. Variables (P_substs_x : substs_x -> Prop). Hypothesis (H_substs_x_xs : forall (value_name_expr_list:list (value_name*expr)), P_substs_x (substs_x_xs value_name_expr_list)) . Fixpoint substs_x_ott_ind (n:substs_x) : P_substs_x n := match n as x return P_substs_x x with | (substs_x_xs value_name_expr_list) => H_substs_x_xs value_name_expr_list end. End substs_x_rect. Section letrec_binding_letrec_bindings_let_binding_pat_exp_pattern_matching_expr_rect. Variables (P_letrec_binding : letrec_binding -> Prop) (P_pat_exp : pat_exp -> Prop) (P_list_letrec_binding : list letrec_binding -> Prop) (P_list_pat_exp : list pat_exp -> Prop) (P_list_expr : list expr -> Prop) (P_list_field_expr : list (field*expr) -> Prop) (P_pattern_matching : pattern_matching -> Prop) (P_let_binding : let_binding -> Prop) (P_letrec_bindings : letrec_bindings -> Prop) (P_expr : expr -> Prop). Hypothesis (H_LRB_simple : forall (value_name5:value_name), forall (pattern_matching5:pattern_matching), P_pattern_matching pattern_matching5 -> P_letrec_binding (LRB_simple value_name5 pattern_matching5)) (H_LRBs_inj : forall (letrec_binding_list:list letrec_binding), P_list_letrec_binding letrec_binding_list -> P_letrec_bindings (LRBs_inj letrec_binding_list)) (H_LB_simple : forall (pattern5:pattern), forall (expr5:expr), P_expr expr5 -> P_let_binding (LB_simple pattern5 expr5)) (H_PE_inj : forall (pattern5:pattern), forall (expr5:expr), P_expr expr5 -> P_pat_exp (PE_inj pattern5 expr5)) (H_PM_pm : forall (pat_exp_list:list pat_exp), P_list_pat_exp pat_exp_list -> P_pattern_matching (PM_pm pat_exp_list)) (H_Expr_uprim : forall (unary_prim5:unary_prim), P_expr (Expr_uprim unary_prim5)) (H_Expr_bprim : forall (binary_prim5:binary_prim), P_expr (Expr_bprim binary_prim5)) (H_Expr_ident : forall (value_name5:value_name), P_expr (Expr_ident value_name5)) (H_Expr_constant : forall (constant5:constant), P_expr (Expr_constant constant5)) (H_Expr_typed : forall (expr5:expr), P_expr expr5 -> forall (typexpr5:typexpr), P_expr (Expr_typed expr5 typexpr5)) (H_Expr_tuple : forall (expr_list:list expr), P_list_expr expr_list -> P_expr (Expr_tuple expr_list)) (H_Expr_construct : forall (expr_list:list expr), P_list_expr expr_list -> forall (constr5:constr), P_expr (Expr_construct constr5 expr_list)) (H_Expr_cons : forall (expr1:expr), P_expr expr1 -> forall (expr2:expr), P_expr expr2 -> P_expr (Expr_cons expr1 expr2)) (H_Expr_record : forall (field_expr_list:list (field*expr)), P_list_field_expr field_expr_list -> P_expr (Expr_record field_expr_list)) (H_Expr_override : forall (field_expr_list:list (field*expr)), P_list_field_expr field_expr_list -> forall (expr_5:expr), P_expr expr_5 -> P_expr (Expr_override expr_5 field_expr_list)) (H_Expr_apply : forall (expr1:expr), P_expr expr1 -> forall (expr2:expr), P_expr expr2 -> P_expr (Expr_apply expr1 expr2)) (H_Expr_and : forall (expr1:expr), P_expr expr1 -> forall (expr2:expr), P_expr expr2 -> P_expr (Expr_and expr1 expr2)) (H_Expr_or : forall (expr1:expr), P_expr expr1 -> forall (expr2:expr), P_expr expr2 -> P_expr (Expr_or expr1 expr2)) (H_Expr_field : forall (expr5:expr), P_expr expr5 -> forall (field5:field), P_expr (Expr_field expr5 field5)) (H_Expr_ifthenelse : forall (expr0:expr), P_expr expr0 -> forall (expr1:expr), P_expr expr1 -> forall (expr2:expr), P_expr expr2 -> P_expr (Expr_ifthenelse expr0 expr1 expr2)) (H_Expr_while : forall (expr1:expr), P_expr expr1 -> forall (expr2:expr), P_expr expr2 -> P_expr (Expr_while expr1 expr2)) (H_Expr_for : forall (x:value_name), forall (expr1:expr), P_expr expr1 -> forall (for_dirn5:for_dirn), forall (expr2:expr), P_expr expr2 -> forall (expr3:expr), P_expr expr3 -> P_expr (Expr_for x expr1 for_dirn5 expr2 expr3)) (H_Expr_sequence : forall (expr1:expr), P_expr expr1 -> forall (expr2:expr), P_expr expr2 -> P_expr (Expr_sequence expr1 expr2)) (H_Expr_match : forall (expr5:expr), P_expr expr5 -> forall (pattern_matching5:pattern_matching), P_pattern_matching pattern_matching5 -> P_expr (Expr_match expr5 pattern_matching5)) (H_Expr_function : forall (pattern_matching5:pattern_matching), P_pattern_matching pattern_matching5 -> P_expr (Expr_function pattern_matching5)) (H_Expr_try : forall (expr5:expr), P_expr expr5 -> forall (pattern_matching5:pattern_matching), P_pattern_matching pattern_matching5 -> P_expr (Expr_try expr5 pattern_matching5)) (H_Expr_let : forall (let_binding5:let_binding), P_let_binding let_binding5 -> forall (expr5:expr), P_expr expr5 -> P_expr (Expr_let let_binding5 expr5)) (H_Expr_letrec : forall (letrec_bindings5:letrec_bindings), P_letrec_bindings letrec_bindings5 -> forall (expr5:expr), P_expr expr5 -> P_expr (Expr_letrec letrec_bindings5 expr5)) (H_Expr_assert : forall (expr5:expr), P_expr expr5 -> P_expr (Expr_assert expr5)) (H_Expr_location : forall (location5:location), P_expr (Expr_location location5)) (H_list_letrec_binding_nil : P_list_letrec_binding nil) (H_list_letrec_binding_cons : forall (letrec_binding0:letrec_binding), P_letrec_binding letrec_binding0 -> forall (letrec_binding_l:list letrec_binding), P_list_letrec_binding letrec_binding_l -> P_list_letrec_binding (cons letrec_binding0 letrec_binding_l)) (H_list_pat_exp_nil : P_list_pat_exp nil) (H_list_pat_exp_cons : forall (pat_exp0:pat_exp), P_pat_exp pat_exp0 -> forall (pat_exp_l:list pat_exp), P_list_pat_exp pat_exp_l -> P_list_pat_exp (cons pat_exp0 pat_exp_l)) (H_list_expr_nil : P_list_expr nil) (H_list_expr_cons : forall (expr0:expr), P_expr expr0 -> forall (expr_l:list expr), P_list_expr expr_l -> P_list_expr (cons expr0 expr_l)) (H_list_field_expr_nil : P_list_field_expr nil) (H_list_field_expr_cons : forall (field0:field), forall (expr1:expr), P_expr expr1 -> forall (field_expr_l:list (field*expr)), P_list_field_expr field_expr_l -> P_list_field_expr (cons (field0,expr1) field_expr_l)). Fixpoint expr_ott_ind (n:expr) : P_expr n := match n as x return P_expr x with | (Expr_uprim unary_prim5) => H_Expr_uprim unary_prim5 | (Expr_bprim binary_prim5) => H_Expr_bprim binary_prim5 | (Expr_ident value_name5) => H_Expr_ident value_name5 | (Expr_constant constant5) => H_Expr_constant constant5 | (Expr_typed expr5 typexpr5) => H_Expr_typed expr5 (expr_ott_ind expr5) typexpr5 | (Expr_tuple expr_list) => H_Expr_tuple expr_list (((fix expr_list_ott_ind (expr_l:list expr) : P_list_expr expr_l := match expr_l as x return P_list_expr x with nil => H_list_expr_nil | cons expr2 xl => H_list_expr_cons expr2(expr_ott_ind expr2)xl (expr_list_ott_ind xl) end)) expr_list) | (Expr_construct constr5 expr_list) => H_Expr_construct expr_list (((fix expr_list_ott_ind (expr_l:list expr) : P_list_expr expr_l := match expr_l as x return P_list_expr x with nil => H_list_expr_nil | cons expr3 xl => H_list_expr_cons expr3(expr_ott_ind expr3)xl (expr_list_ott_ind xl) end)) expr_list) constr5 | (Expr_cons expr1 expr2) => H_Expr_cons expr1 (expr_ott_ind expr1) expr2 (expr_ott_ind expr2) | (Expr_record field_expr_list) => H_Expr_record field_expr_list (((fix field_expr_list_ott_ind (field_expr_l:list (field*expr)) : P_list_field_expr field_expr_l := match field_expr_l as x return P_list_field_expr x with nil => H_list_field_expr_nil | cons (field1,expr4) xl => H_list_field_expr_cons field1 expr4(expr_ott_ind expr4)xl (field_expr_list_ott_ind xl) end)) field_expr_list) | (Expr_override expr_5 field_expr_list) => H_Expr_override field_expr_list (((fix field_expr_list_ott_ind (field_expr_l:list (field*expr)) : P_list_field_expr field_expr_l := match field_expr_l as x return P_list_field_expr x with nil => H_list_field_expr_nil | cons (field2,expr5) xl => H_list_field_expr_cons field2 expr5(expr_ott_ind expr5)xl (field_expr_list_ott_ind xl) end)) field_expr_list) expr_5 (expr_ott_ind expr_5) | (Expr_apply expr1 expr2) => H_Expr_apply expr1 (expr_ott_ind expr1) expr2 (expr_ott_ind expr2) | (Expr_and expr1 expr2) => H_Expr_and expr1 (expr_ott_ind expr1) expr2 (expr_ott_ind expr2) | (Expr_or expr1 expr2) => H_Expr_or expr1 (expr_ott_ind expr1) expr2 (expr_ott_ind expr2) | (Expr_field expr5 field5) => H_Expr_field expr5 (expr_ott_ind expr5) field5 | (Expr_ifthenelse expr0 expr1 expr2) => H_Expr_ifthenelse expr0 (expr_ott_ind expr0) expr1 (expr_ott_ind expr1) expr2 (expr_ott_ind expr2) | (Expr_while expr1 expr2) => H_Expr_while expr1 (expr_ott_ind expr1) expr2 (expr_ott_ind expr2) | (Expr_for x expr1 for_dirn5 expr2 expr3) => H_Expr_for x expr1 (expr_ott_ind expr1) for_dirn5 expr2 (expr_ott_ind expr2) expr3 (expr_ott_ind expr3) | (Expr_sequence expr1 expr2) => H_Expr_sequence expr1 (expr_ott_ind expr1) expr2 (expr_ott_ind expr2) | (Expr_match expr5 pattern_matching5) => H_Expr_match expr5 (expr_ott_ind expr5) pattern_matching5 (pattern_matching_ott_ind pattern_matching5) | (Expr_function pattern_matching5) => H_Expr_function pattern_matching5 (pattern_matching_ott_ind pattern_matching5) | (Expr_try expr5 pattern_matching5) => H_Expr_try expr5 (expr_ott_ind expr5) pattern_matching5 (pattern_matching_ott_ind pattern_matching5) | (Expr_let let_binding5 expr5) => H_Expr_let let_binding5 (let_binding_ott_ind let_binding5) expr5 (expr_ott_ind expr5) | (Expr_letrec letrec_bindings5 expr5) => H_Expr_letrec letrec_bindings5 (letrec_bindings_ott_ind letrec_bindings5) expr5 (expr_ott_ind expr5) | (Expr_assert expr5) => H_Expr_assert expr5 (expr_ott_ind expr5) | (Expr_location location5) => H_Expr_location location5 end with pattern_matching_ott_ind (n:pattern_matching) : P_pattern_matching n := match n as x return P_pattern_matching x with | (PM_pm pat_exp_list) => H_PM_pm pat_exp_list (((fix pat_exp_list_ott_ind (pat_exp_l:list pat_exp) : P_list_pat_exp pat_exp_l := match pat_exp_l as x return P_list_pat_exp x with nil => H_list_pat_exp_nil | cons pat_exp1 xl => H_list_pat_exp_cons pat_exp1(pat_exp_ott_ind pat_exp1)xl (pat_exp_list_ott_ind xl) end)) pat_exp_list) end with pat_exp_ott_ind (n:pat_exp) : P_pat_exp n := match n as x return P_pat_exp x with | (PE_inj pattern5 expr5) => H_PE_inj pattern5 expr5 (expr_ott_ind expr5) end with let_binding_ott_ind (n:let_binding) : P_let_binding n := match n as x return P_let_binding x with | (LB_simple pattern5 expr5) => H_LB_simple pattern5 expr5 (expr_ott_ind expr5) end with letrec_bindings_ott_ind (n:letrec_bindings) : P_letrec_bindings n := match n as x return P_letrec_bindings x with | (LRBs_inj letrec_binding_list) => H_LRBs_inj letrec_binding_list (((fix letrec_binding_list_ott_ind (letrec_binding_l:list letrec_binding) : P_list_letrec_binding letrec_binding_l := match letrec_binding_l as x return P_list_letrec_binding x with nil => H_list_letrec_binding_nil | cons letrec_binding1 xl => H_list_letrec_binding_cons letrec_binding1(letrec_binding_ott_ind letrec_binding1)xl (letrec_binding_list_ott_ind xl) end)) letrec_binding_list) end with letrec_binding_ott_ind (n:letrec_binding) : P_letrec_binding n := match n as x return P_letrec_binding x with | (LRB_simple value_name5 pattern_matching5) => H_LRB_simple value_name5 pattern_matching5 (pattern_matching_ott_ind pattern_matching5) end. End letrec_binding_letrec_bindings_let_binding_pat_exp_pattern_matching_expr_rect.