Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
(* generated by Ott 0.10.13 from: caml_typedef_syntax.ott caml_typedef_typing.ott caml_typedef_reduction.ott *) theory caml_typedef imports Main Multiset begin (** syntax *) types index = "nat" types ident = "string" types integer_literal = "int" types float_literal = "nat" types char_literal = "char" types string_literal = "string" types infix_symbol = "string" types prefix_symbol = "string" types location = "nat" types lowercase_ident = "string" types capitalized_ident = "string" datatype typeconstr_name = TCN_id "lowercase_ident" datatype typeconstr = TC_name "typeconstr_name" | TC_int | TC_char | TC_string | TC_float | TC_bool | TC_unit | TC_exn | TC_list | TC_option | TC_ref types idx = "nat" datatype typevar = TV_ident "ident" datatype constr_name = CN_id "capitalized_ident" datatype typexpr = TE_var "typevar" | TE_idxvar "idx" "idx" | TE_any | TE_arrow "typexpr" "typexpr" | TE_tuple "typexpr list" | TE_constr "typexpr list" "typeconstr" datatype field_name = FN_id "lowercase_ident" datatype infix_op = IO_symbol "infix_symbol" | IO_star | IO_equal | IO_colonequal datatype constr_decl = CD_nullary "constr_name" | CD_nary "constr_name" "typexpr list" datatype field_decl = FD_immutable "field_name" "typexpr" datatype operator_name = ON_symbol "prefix_symbol" | ON_infix "infix_op" datatype constr = C_name "constr_name" | C_invalidargument | C_notfound | C_assertfailure | C_matchfailure | C_div_by_0 | C_none | C_some types intn = "int" datatype type_equation = TE_te "typexpr" datatype type_representation = TR_variant "constr_decl list" | TR_record "field_decl list" datatype type_param = TP_var "typevar" datatype value_name = VN_id "lowercase_ident" | VN_op "operator_name" datatype field = F_name "field_name" datatype constant = CONST_int "intn" | CONST_float "float_literal" | CONST_char "char_literal" | CONST_string "string_literal" | CONST_constr "constr" | CONST_false | CONST_true | CONST_nil | CONST_unit datatype type_information = TI_eq "type_equation" | TI_def "type_representation" datatype type_params_opt = TPS_nary "type_param list" datatype pattern = P_var "value_name" | P_any | P_constant "constant" | P_alias "pattern" "value_name" | P_typed "pattern" "typexpr" | P_or "pattern" "pattern" | P_construct "constr" "pattern list" | P_construct_any "constr" | P_tuple "pattern list" | P_record "(field*pattern) list" | P_cons "pattern" "pattern" datatype unary_prim = Uprim_raise | Uprim_not | Uprim_minus | Uprim_ref | Uprim_deref datatype binary_prim = Bprim_equal | Bprim_plus | Bprim_minus | Bprim_times | Bprim_div | Bprim_assign datatype for_dirn = FD_upto | FD_downto datatype caml_typedef = TD_td "type_params_opt" "typeconstr_name" "type_information" datatype letrec_binding = LRB_simple "value_name" "pattern_matching" and letrec_bindings = LRBs_inj "letrec_binding list" and let_binding = LB_simple "pattern" "expr" and pat_exp = PE_inj "pattern" "expr" and pattern_matching = PM_pm "pat_exp list" and expr = Expr_uprim "unary_prim" | Expr_bprim "binary_prim" | Expr_ident "value_name" | Expr_constant "constant" | Expr_typed "expr" "typexpr" | Expr_tuple "expr list" | Expr_construct "constr" "expr list" | Expr_cons "expr" "expr" | Expr_record "(field*expr) list" | Expr_override "expr" "(field*expr) list" | Expr_apply "expr" "expr" | Expr_and "expr" "expr" | Expr_or "expr" "expr" | Expr_field "expr" "field" | Expr_ifthenelse "expr" "expr" "expr" | Expr_while "expr" "expr" | Expr_for "value_name" "expr" "for_dirn" "expr" "expr" | Expr_sequence "expr" "expr" | Expr_match "expr" "pattern_matching" | Expr_function "pattern_matching" | Expr_try "expr" "pattern_matching" | Expr_let "let_binding" "expr" | Expr_letrec "letrec_bindings" "expr" | Expr_assert "expr" | Expr_location "location" datatype caml_type_definition = TDF_tdf "caml_typedef list" datatype exception_definition = ED_def "constr_decl" datatype caml_definition = D_let "let_binding" | D_letrec "letrec_bindings" | D_type "caml_type_definition" | D_exception "exception_definition" datatype typescheme = TS_forall "typexpr" types kind = "nat" datatype typexprs = typexprs_inj "typexpr list" datatype trans_label = Lab_nil | Lab_alloc "expr" "location" | Lab_deref "location" "expr" | Lab_assign "location" "expr" datatype definitions = Ds_nil | Ds_cons "caml_definition" "definitions" datatype name = name_tv | name_vn "value_name" | name_cn "constr_name" | name_tcn "typeconstr_name" | name_fn "field_name" | name_l "location" datatype environment_binding = EB_tv | EB_vn "value_name" "typescheme" | EB_cc "constr_name" "typeconstr" | EB_pc "constr_name" "type_params_opt" "typexprs" "typeconstr" | EB_fn "field_name" "type_params_opt" "typeconstr_name" "typexpr" | EB_td "typeconstr_name" "kind" | EB_tr "typeconstr_name" "kind" "field_name list" | EB_ta "type_params_opt" "typeconstr_name" "typexpr" | EB_l "location" "typexpr" types labelled_arrow = "trans_label" datatype program = Prog_defs "definitions" | Prog_raise "expr" types store = "((location*expr) list)" types names = "(name list)" types environment = "(environment_binding list)" types Tsigma = "(typevar*typexpr) list" datatype substs_x = substs_x_xs "(value_name*expr) list" datatype value_path = VP_name "value_name" (** library functions *) lemma [mono]:" (!! x. f x --> g x) ==> list_all (%b. b) (map f foo_list)--> list_all (%b. b) (map g foo_list) " apply(induct_tac foo_list, auto) done lemma [mono]: "split f p = f (fst p) (snd p)" by (simp add: split_def) consts list_assoc :: "'a => ('a*'b) list => 'b option" primrec "list_assoc x0 Nil = None" "list_assoc x0 (Cons xy xys) = (if x0=fst xy then Some (snd xy) else list_assoc x0 xys)" consts list_minus :: "'a list => 'a list => 'a list" primrec "list_minus Nil ys = Nil" "list_minus (Cons x xs) ys = (if Not(x : set ys) then Cons x (list_minus xs ys) else list_minus xs ys)" (** subrules *) consts is_definition_value_of_definition :: "caml_definition => bool" primrec "is_definition_value_of_definition (D_let let_binding) = (False)" "is_definition_value_of_definition (D_letrec letrec_bindings) = (False)" "is_definition_value_of_definition (D_type caml_type_definition) = ((True))" "is_definition_value_of_definition (D_exception exception_definition) = ((True))" consts is_value_of_field_expr_Expr_record_is_non_expansive_of_field_expr_Expr_record :: "(field*expr) => (bool) * (bool)" is_value_of_field_expr_list_Expr_record_is_non_expansive_of_field_expr_list_Expr_record :: "(field*expr) list => (bool) * (bool)" is_value_of_expr_list_Expr_construct_is_non_expansive_of_expr_list_Expr_construct :: "expr list => (bool) * (bool)" is_value_of_expr_list_Expr_tuple_is_non_expansive_of_expr_list_Expr_tuple :: "expr list => (bool) * (bool)" is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr :: "expr => (bool) * (bool) * (bool)" primrec "is_value_of_field_expr_Expr_record_is_non_expansive_of_field_expr_Expr_record (field_XXX,expr_XXX) = (((%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_value_of_expr) (is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr expr_XXX)) , ((%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_non_expansive_of_expr) (is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr expr_XXX)))" "is_value_of_field_expr_list_Expr_record_is_non_expansive_of_field_expr_list_Expr_record Nil = (True , True)" "is_value_of_field_expr_list_Expr_record_is_non_expansive_of_field_expr_list_Expr_record (field_expr_XXX#field_expr_list_XXX) = ((((%(is_value_of_field_expr_Expr_record,is_non_expansive_of_field_expr_Expr_record).is_value_of_field_expr_Expr_record) (is_value_of_field_expr_Expr_record_is_non_expansive_of_field_expr_Expr_record field_expr_XXX)) & ((%(is_value_of_field_expr_list_Expr_record,is_non_expansive_of_field_expr_list_Expr_record).is_value_of_field_expr_list_Expr_record) (is_value_of_field_expr_list_Expr_record_is_non_expansive_of_field_expr_list_Expr_record field_expr_list_XXX))) , (((%(is_value_of_field_expr_Expr_record,is_non_expansive_of_field_expr_Expr_record).is_non_expansive_of_field_expr_Expr_record) (is_value_of_field_expr_Expr_record_is_non_expansive_of_field_expr_Expr_record field_expr_XXX)) & ((%(is_value_of_field_expr_list_Expr_record,is_non_expansive_of_field_expr_list_Expr_record).is_non_expansive_of_field_expr_list_Expr_record) (is_value_of_field_expr_list_Expr_record_is_non_expansive_of_field_expr_list_Expr_record field_expr_list_XXX))))" "is_value_of_expr_list_Expr_construct_is_non_expansive_of_expr_list_Expr_construct Nil = (True , True)" "is_value_of_expr_list_Expr_construct_is_non_expansive_of_expr_list_Expr_construct (expr_XXX#expr_list_XXX) = ((((%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_value_of_expr) (is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr expr_XXX)) & ((%(is_value_of_expr_list_Expr_construct,is_non_expansive_of_expr_list_Expr_construct).is_value_of_expr_list_Expr_construct) (is_value_of_expr_list_Expr_construct_is_non_expansive_of_expr_list_Expr_construct expr_list_XXX))) , (((%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_non_expansive_of_expr) (is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr expr_XXX)) & ((%(is_value_of_expr_list_Expr_construct,is_non_expansive_of_expr_list_Expr_construct).is_non_expansive_of_expr_list_Expr_construct) (is_value_of_expr_list_Expr_construct_is_non_expansive_of_expr_list_Expr_construct expr_list_XXX))))" "is_value_of_expr_list_Expr_tuple_is_non_expansive_of_expr_list_Expr_tuple Nil = (True , True)" "is_value_of_expr_list_Expr_tuple_is_non_expansive_of_expr_list_Expr_tuple (expr_XXX#expr_list_XXX) = ((((%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_value_of_expr) (is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr expr_XXX)) & ((%(is_value_of_expr_list_Expr_tuple,is_non_expansive_of_expr_list_Expr_tuple).is_value_of_expr_list_Expr_tuple) (is_value_of_expr_list_Expr_tuple_is_non_expansive_of_expr_list_Expr_tuple expr_list_XXX))) , (((%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_non_expansive_of_expr) (is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr expr_XXX)) & ((%(is_value_of_expr_list_Expr_tuple,is_non_expansive_of_expr_list_Expr_tuple).is_non_expansive_of_expr_list_Expr_tuple) (is_value_of_expr_list_Expr_tuple_is_non_expansive_of_expr_list_Expr_tuple expr_list_XXX))))" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_uprim unary_prim) = ((True) , False , (True))" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_bprim binary_prim) = ((True) , (True) , (True))" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_ident value_name) = (False , False , (True))" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_constant constant) = ((True) , False , (True))" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_typed expr typexpr) = (False , False , (((%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_non_expansive_of_expr) (is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr expr))))" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_tuple (expr_list)) = (((%(is_value_of_expr_list_Expr_tuple,is_non_expansive_of_expr_list_Expr_tuple).is_value_of_expr_list_Expr_tuple) (is_value_of_expr_list_Expr_tuple_is_non_expansive_of_expr_list_Expr_tuple expr_list)) , False , ((%(is_value_of_expr_list_Expr_tuple,is_non_expansive_of_expr_list_Expr_tuple).is_non_expansive_of_expr_list_Expr_tuple) (is_value_of_expr_list_Expr_tuple_is_non_expansive_of_expr_list_Expr_tuple expr_list)))" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_construct constr (expr_list)) = (((%(is_value_of_expr_list_Expr_construct,is_non_expansive_of_expr_list_Expr_construct).is_value_of_expr_list_Expr_construct) (is_value_of_expr_list_Expr_construct_is_non_expansive_of_expr_list_Expr_construct expr_list)) , False , ((%(is_value_of_expr_list_Expr_construct,is_non_expansive_of_expr_list_Expr_construct).is_non_expansive_of_expr_list_Expr_construct) (is_value_of_expr_list_Expr_construct_is_non_expansive_of_expr_list_Expr_construct expr_list)))" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_cons expr1 expr2) = ((((%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_value_of_expr) (is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr expr1)) & ((%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_value_of_expr) (is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr expr2))) , False , (((%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_non_expansive_of_expr) (is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr expr1)) & ((%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_non_expansive_of_expr) (is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr expr2))))" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_record (field_expr_list)) = (((%(is_value_of_field_expr_list_Expr_record,is_non_expansive_of_field_expr_list_Expr_record).is_value_of_field_expr_list_Expr_record) (is_value_of_field_expr_list_Expr_record_is_non_expansive_of_field_expr_list_Expr_record field_expr_list)) , False , ((%(is_value_of_field_expr_list_Expr_record,is_non_expansive_of_field_expr_list_Expr_record).is_non_expansive_of_field_expr_list_Expr_record) (is_value_of_field_expr_list_Expr_record_is_non_expansive_of_field_expr_list_Expr_record field_expr_list)))" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_override expr (field_expr_list)) = (False , False , False)" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_apply expr1 expr2) = ((((%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_binary_prim_app_value_of_expr) (is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr expr1)) & ((%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_value_of_expr) (is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr expr2))) , False , (((%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_binary_prim_app_value_of_expr) (is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr expr1)) & ((%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_non_expansive_of_expr) (is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr expr2))))" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_and expr1 expr2) = (False , False , False)" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_or expr1 expr2) = (False , False , False)" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_field expr field) = (False , False , False)" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_ifthenelse expr0 expr1 expr2) = (False , False , False)" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_while expr1 expr2) = (False , False , False)" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_for x expr1 for_dirn expr2 expr3) = (False , False , False)" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_sequence expr1 expr2) = (False , False , False)" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_match expr pattern_matching) = (False , False , False)" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_function pattern_matching) = ((True) , False , (True))" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_try expr pattern_matching) = (False , False , False)" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_let let_binding expr) = (False , False , False)" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_letrec letrec_bindings expr) = (False , False , (((%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_non_expansive_of_expr) (is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr expr))))" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_assert expr) = (False , False , False)" "is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr (Expr_location location) = ((True) , False , (True))" constdefs is_value_of_field_expr_Expr_record :: "(field*expr) => bool" "is_value_of_field_expr_Expr_record == (%(is_value_of_field_expr_Expr_record,is_non_expansive_of_field_expr_Expr_record).is_value_of_field_expr_Expr_record) o is_value_of_field_expr_Expr_record_is_non_expansive_of_field_expr_Expr_record" constdefs is_non_expansive_of_field_expr_Expr_record :: "(field*expr) => bool" "is_non_expansive_of_field_expr_Expr_record == (%(is_value_of_field_expr_Expr_record,is_non_expansive_of_field_expr_Expr_record).is_non_expansive_of_field_expr_Expr_record) o is_value_of_field_expr_Expr_record_is_non_expansive_of_field_expr_Expr_record" constdefs is_value_of_field_expr_list_Expr_record :: "(field*expr) list => bool" "is_value_of_field_expr_list_Expr_record == (%(is_value_of_field_expr_list_Expr_record,is_non_expansive_of_field_expr_list_Expr_record).is_value_of_field_expr_list_Expr_record) o is_value_of_field_expr_list_Expr_record_is_non_expansive_of_field_expr_list_Expr_record" constdefs is_non_expansive_of_field_expr_list_Expr_record :: "(field*expr) list => bool" "is_non_expansive_of_field_expr_list_Expr_record == (%(is_value_of_field_expr_list_Expr_record,is_non_expansive_of_field_expr_list_Expr_record).is_non_expansive_of_field_expr_list_Expr_record) o is_value_of_field_expr_list_Expr_record_is_non_expansive_of_field_expr_list_Expr_record" constdefs is_value_of_expr_list_Expr_construct :: "expr list => bool" "is_value_of_expr_list_Expr_construct == (%(is_value_of_expr_list_Expr_construct,is_non_expansive_of_expr_list_Expr_construct).is_value_of_expr_list_Expr_construct) o is_value_of_expr_list_Expr_construct_is_non_expansive_of_expr_list_Expr_construct" constdefs is_non_expansive_of_expr_list_Expr_construct :: "expr list => bool" "is_non_expansive_of_expr_list_Expr_construct == (%(is_value_of_expr_list_Expr_construct,is_non_expansive_of_expr_list_Expr_construct).is_non_expansive_of_expr_list_Expr_construct) o is_value_of_expr_list_Expr_construct_is_non_expansive_of_expr_list_Expr_construct" constdefs is_value_of_expr_list_Expr_tuple :: "expr list => bool" "is_value_of_expr_list_Expr_tuple == (%(is_value_of_expr_list_Expr_tuple,is_non_expansive_of_expr_list_Expr_tuple).is_value_of_expr_list_Expr_tuple) o is_value_of_expr_list_Expr_tuple_is_non_expansive_of_expr_list_Expr_tuple" constdefs is_non_expansive_of_expr_list_Expr_tuple :: "expr list => bool" "is_non_expansive_of_expr_list_Expr_tuple == (%(is_value_of_expr_list_Expr_tuple,is_non_expansive_of_expr_list_Expr_tuple).is_non_expansive_of_expr_list_Expr_tuple) o is_value_of_expr_list_Expr_tuple_is_non_expansive_of_expr_list_Expr_tuple" constdefs is_value_of_expr :: "expr => bool" "is_value_of_expr == (%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_value_of_expr) o is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr" constdefs is_binary_prim_app_value_of_expr :: "expr => bool" "is_binary_prim_app_value_of_expr == (%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_binary_prim_app_value_of_expr) o is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr" constdefs is_non_expansive_of_expr :: "expr => bool" "is_non_expansive_of_expr == (%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_non_expansive_of_expr) o is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr" consts is_src_typexpr_of_typexpr_list_TE_constr :: "typexpr list => bool" is_src_typexpr_of_typexpr_list_TE_tuple :: "typexpr list => bool" is_src_typexpr_of_typexpr :: "typexpr => bool" primrec "is_src_typexpr_of_typexpr_list_TE_constr Nil = (True)" "is_src_typexpr_of_typexpr_list_TE_constr (typexpr_XXX#typexpr_list_XXX) = (((is_src_typexpr_of_typexpr typexpr_XXX) & (is_src_typexpr_of_typexpr_list_TE_constr typexpr_list_XXX)))" "is_src_typexpr_of_typexpr_list_TE_tuple Nil = (True)" "is_src_typexpr_of_typexpr_list_TE_tuple (typexpr_XXX#typexpr_list_XXX) = (((is_src_typexpr_of_typexpr typexpr_XXX) & (is_src_typexpr_of_typexpr_list_TE_tuple typexpr_list_XXX)))" "is_src_typexpr_of_typexpr (TE_var typevar) = ((True))" "is_src_typexpr_of_typexpr (TE_idxvar idx num) = (False)" "is_src_typexpr_of_typexpr TE_any = ((True))" "is_src_typexpr_of_typexpr (TE_arrow typexpr1 typexpr2) = (((is_src_typexpr_of_typexpr typexpr1) & (is_src_typexpr_of_typexpr typexpr2)))" "is_src_typexpr_of_typexpr (TE_tuple (typexpr_list)) = ((is_src_typexpr_of_typexpr_list_TE_tuple typexpr_list))" "is_src_typexpr_of_typexpr (TE_constr (typexpr_list) typeconstr) = ((is_src_typexpr_of_typexpr_list_TE_constr typexpr_list))" consts is_definitions_value_of_definitions :: "definitions => bool" primrec "is_definitions_value_of_definitions Ds_nil = ((True))" "is_definitions_value_of_definitions (Ds_cons caml_definition definitions) = (((is_definition_value_of_definition caml_definition) & (is_definitions_value_of_definitions definitions)))" consts is_trans_label_of_trans_label :: "trans_label => bool" primrec "is_trans_label_of_trans_label Lab_nil = ((True))" "is_trans_label_of_trans_label (Lab_alloc v location) = ((((%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_value_of_expr) (is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr v))))" "is_trans_label_of_trans_label (Lab_deref location v) = ((((%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_value_of_expr) (is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr v))))" "is_trans_label_of_trans_label (Lab_assign location v) = ((((%(is_value_of_expr,is_binary_prim_app_value_of_expr,is_non_expansive_of_expr).is_value_of_expr) (is_value_of_expr_is_binary_prim_app_value_of_expr_is_non_expansive_of_expr v))))" (** auxiliary functions *) consts aux_constr_names_constr_decl_of_constr_decl :: "constr_decl => constr_name list" primrec "aux_constr_names_constr_decl_of_constr_decl (CD_nullary constr_name) = ([constr_name])" "aux_constr_names_constr_decl_of_constr_decl (CD_nary constr_name (typexpr_list)) = ([constr_name])" consts aux_field_names_field_decl_of_field_decl :: "field_decl => field_name list" primrec "aux_field_names_field_decl_of_field_decl (FD_immutable field_name typexpr) = ([field_name])" consts aux_constr_names_constr_decl_of_constr_decl_list :: "constr_decl list => constr_name list" primrec "aux_constr_names_constr_decl_of_constr_decl_list Nil = ([])" "aux_constr_names_constr_decl_of_constr_decl_list (constr_decl_XXX#constr_decl_list_XXX) = ((aux_constr_names_constr_decl_of_constr_decl constr_decl_XXX) @ (aux_constr_names_constr_decl_of_constr_decl_list constr_decl_list_XXX))" consts aux_field_names_field_decl_of_field_decl_list :: "field_decl list => field_name list" primrec "aux_field_names_field_decl_of_field_decl_list Nil = ([])" "aux_field_names_field_decl_of_field_decl_list (field_decl_XXX#field_decl_list_XXX) = ((aux_field_names_field_decl_of_field_decl field_decl_XXX) @ (aux_field_names_field_decl_of_field_decl_list field_decl_list_XXX))" consts aux_constr_names_type_representation_of_type_representation_aux_field_names_type_representation_of_type_representation :: "type_representation => (constr_name list) * (field_name list)" primrec "aux_constr_names_type_representation_of_type_representation_aux_field_names_type_representation_of_type_representation (TR_variant (constr_decl_list)) = ((aux_constr_names_constr_decl_of_constr_decl_list constr_decl_list) , [])" "aux_constr_names_type_representation_of_type_representation_aux_field_names_type_representation_of_type_representation (TR_record (field_decl_list)) = ([] , (aux_field_names_field_decl_of_field_decl_list field_decl_list))" constdefs aux_constr_names_type_representation_of_type_representation :: "type_representation => constr_name list" "aux_constr_names_type_representation_of_type_representation == (%(aux_constr_names_type_representation_of_type_representation,aux_field_names_type_representation_of_type_representation).aux_constr_names_type_representation_of_type_representation) o aux_constr_names_type_representation_of_type_representation_aux_field_names_type_representation_of_type_representation" constdefs aux_field_names_type_representation_of_type_representation :: "type_representation => field_name list" "aux_field_names_type_representation_of_type_representation == (%(aux_constr_names_type_representation_of_type_representation,aux_field_names_type_representation_of_type_representation).aux_field_names_type_representation_of_type_representation) o aux_constr_names_type_representation_of_type_representation_aux_field_names_type_representation_of_type_representation" consts aux_xs_letrec_binding_of_letrec_binding :: "letrec_binding => value_name list" primrec "aux_xs_letrec_binding_of_letrec_binding (LRB_simple value_name pattern_matching) = ([value_name])" consts aux_constr_names_type_information_of_type_information_aux_field_names_type_information_of_type_information :: "type_information => (constr_name list) * (field_name list)" primrec "aux_constr_names_type_information_of_type_information_aux_field_names_type_information_of_type_information (TI_eq type_equation) = ([] , [])" "aux_constr_names_type_information_of_type_information_aux_field_names_type_information_of_type_information (TI_def type_representation) = (((%(aux_constr_names_type_representation_of_type_representation,aux_field_names_type_representation_of_type_representation).aux_constr_names_type_representation_of_type_representation) (aux_constr_names_type_representation_of_type_representation_aux_field_names_type_representation_of_type_representation type_representation)) , ((%(aux_constr_names_type_representation_of_type_representation,aux_field_names_type_representation_of_type_representation).aux_field_names_type_representation_of_type_representation) (aux_constr_names_type_representation_of_type_representation_aux_field_names_type_representation_of_type_representation type_representation)))" constdefs aux_constr_names_type_information_of_type_information :: "type_information => constr_name list" "aux_constr_names_type_information_of_type_information == (%(aux_constr_names_type_information_of_type_information,aux_field_names_type_information_of_type_information).aux_constr_names_type_information_of_type_information) o aux_constr_names_type_information_of_type_information_aux_field_names_type_information_of_type_information" constdefs aux_field_names_type_information_of_type_information :: "type_information => field_name list" "aux_field_names_type_information_of_type_information == (%(aux_constr_names_type_information_of_type_information,aux_field_names_type_information_of_type_information).aux_field_names_type_information_of_type_information) o aux_constr_names_type_information_of_type_information_aux_field_names_type_information_of_type_information" consts aux_xs_pattern_of_field_pattern :: "(field*pattern) => value_name list" aux_xs_pattern_of_field_pattern_list :: "(field*pattern) list => value_name list" aux_xs_pattern_of_pattern_list_P_tuple :: "pattern list => value_name list" aux_xs_pattern_of_pattern_list :: "pattern list => value_name list" aux_xs_pattern_of_pattern :: "pattern => value_name list" primrec "aux_xs_pattern_of_field_pattern (field_XXX,pattern_XXX) = (((aux_xs_pattern_of_pattern pattern_XXX)))" "aux_xs_pattern_of_field_pattern_list Nil = ([])" "aux_xs_pattern_of_field_pattern_list (field_pattern_XXX#field_pattern_list_XXX) = ((aux_xs_pattern_of_field_pattern field_pattern_XXX) @ (aux_xs_pattern_of_field_pattern_list field_pattern_list_XXX))" "aux_xs_pattern_of_pattern_list_P_tuple Nil = ([])" "aux_xs_pattern_of_pattern_list_P_tuple (pattern_XXX#pattern_list_XXX) = ((aux_xs_pattern_of_pattern pattern_XXX) @ (aux_xs_pattern_of_pattern_list_P_tuple pattern_list_XXX))" "aux_xs_pattern_of_pattern_list Nil = ([])" "aux_xs_pattern_of_pattern_list (pattern_XXX#pattern_list_XXX) = ((aux_xs_pattern_of_pattern pattern_XXX) @ (aux_xs_pattern_of_pattern_list pattern_list_XXX))" "aux_xs_pattern_of_pattern (P_var value_name) = ([value_name])" "aux_xs_pattern_of_pattern P_any = ([])" "aux_xs_pattern_of_pattern (P_constant constant) = ([])" "aux_xs_pattern_of_pattern (P_alias pattern value_name) = ((aux_xs_pattern_of_pattern pattern) @ [value_name])" "aux_xs_pattern_of_pattern (P_typed pattern typexpr) = ((aux_xs_pattern_of_pattern pattern))" "aux_xs_pattern_of_pattern (P_or pattern1 pattern2) = ((aux_xs_pattern_of_pattern pattern1))" "aux_xs_pattern_of_pattern (P_construct constr (pattern_list)) = ((aux_xs_pattern_of_pattern_list pattern_list))" "aux_xs_pattern_of_pattern (P_construct_any constr) = ([])" "aux_xs_pattern_of_pattern (P_tuple (pattern_list)) = ((aux_xs_pattern_of_pattern_list_P_tuple pattern_list))" "aux_xs_pattern_of_pattern (P_record (field_pattern_list)) = ((aux_xs_pattern_of_field_pattern_list field_pattern_list))" "aux_xs_pattern_of_pattern (P_cons pattern1 pattern2) = ((aux_xs_pattern_of_pattern pattern1) @ (aux_xs_pattern_of_pattern pattern2))" consts aux_xs_letrec_binding_of_letrec_binding_list :: "letrec_binding list => value_name list" primrec "aux_xs_letrec_binding_of_letrec_binding_list Nil = ([])" "aux_xs_letrec_binding_of_letrec_binding_list (letrec_binding_XXX#letrec_binding_list_XXX) = ((aux_xs_letrec_binding_of_letrec_binding letrec_binding_XXX) @ (aux_xs_letrec_binding_of_letrec_binding_list letrec_binding_list_XXX))" consts aux_constr_names_caml_typedef_of_caml_typedef_aux_type_names_caml_typedef_of_caml_typedef :: "caml_typedef => (constr_name list) * (typeconstr_name list)" primrec "aux_constr_names_caml_typedef_of_caml_typedef_aux_type_names_caml_typedef_of_caml_typedef (TD_td type_params_opt typeconstr_name type_information) = (((%(aux_constr_names_type_information_of_type_information,aux_field_names_type_information_of_type_information).aux_constr_names_type_information_of_type_information) (aux_constr_names_type_information_of_type_information_aux_field_names_type_information_of_type_information type_information)) , [typeconstr_name])" constdefs aux_constr_names_caml_typedef_of_caml_typedef :: "caml_typedef => constr_name list" "aux_constr_names_caml_typedef_of_caml_typedef == (%(aux_constr_names_caml_typedef_of_caml_typedef,aux_type_names_caml_typedef_of_caml_typedef).aux_constr_names_caml_typedef_of_caml_typedef) o aux_constr_names_caml_typedef_of_caml_typedef_aux_type_names_caml_typedef_of_caml_typedef" constdefs aux_type_names_caml_typedef_of_caml_typedef :: "caml_typedef => typeconstr_name list" "aux_type_names_caml_typedef_of_caml_typedef == (%(aux_constr_names_caml_typedef_of_caml_typedef,aux_type_names_caml_typedef_of_caml_typedef).aux_type_names_caml_typedef_of_caml_typedef) o aux_constr_names_caml_typedef_of_caml_typedef_aux_type_names_caml_typedef_of_caml_typedef" consts aux_typevars_type_param_of_type_param :: "type_param => typevar list" primrec "aux_typevars_type_param_of_type_param (TP_var typevar) = ([typevar])" consts aux_xs_let_binding_of_let_binding :: "let_binding => value_name list" primrec "aux_xs_let_binding_of_let_binding (LB_simple pattern expr) = ((aux_xs_pattern_of_pattern pattern))" consts aux_xs_letrec_bindings_of_letrec_bindings :: "letrec_bindings => value_name list" primrec "aux_xs_letrec_bindings_of_letrec_bindings (LRBs_inj (letrec_binding_list)) = ((aux_xs_letrec_binding_of_letrec_binding_list letrec_binding_list))" consts aux_constr_names_caml_typedef_of_caml_typedef_list_aux_type_names_caml_typedef_of_caml_typedef_list :: "caml_typedef list => (constr_name list) * (typeconstr_name list)" primrec "aux_constr_names_caml_typedef_of_caml_typedef_list_aux_type_names_caml_typedef_of_caml_typedef_list Nil = ([] , [])" "aux_constr_names_caml_typedef_of_caml_typedef_list_aux_type_names_caml_typedef_of_caml_typedef_list (caml_typedef_XXX#caml_typedef_list_XXX) = (((%(aux_constr_names_caml_typedef_of_caml_typedef,aux_type_names_caml_typedef_of_caml_typedef).aux_constr_names_caml_typedef_of_caml_typedef) (aux_constr_names_caml_typedef_of_caml_typedef_aux_type_names_caml_typedef_of_caml_typedef caml_typedef_XXX)) @ ((%(aux_constr_names_caml_typedef_of_caml_typedef_list,aux_type_names_caml_typedef_of_caml_typedef_list).aux_constr_names_caml_typedef_of_caml_typedef_list) (aux_constr_names_caml_typedef_of_caml_typedef_list_aux_type_names_caml_typedef_of_caml_typedef_list caml_typedef_list_XXX)) , ((%(aux_constr_names_caml_typedef_of_caml_typedef,aux_type_names_caml_typedef_of_caml_typedef).aux_type_names_caml_typedef_of_caml_typedef) (aux_constr_names_caml_typedef_of_caml_typedef_aux_type_names_caml_typedef_of_caml_typedef caml_typedef_XXX)) @ ((%(aux_constr_names_caml_typedef_of_caml_typedef_list,aux_type_names_caml_typedef_of_caml_typedef_list).aux_type_names_caml_typedef_of_caml_typedef_list) (aux_constr_names_caml_typedef_of_caml_typedef_list_aux_type_names_caml_typedef_of_caml_typedef_list caml_typedef_list_XXX)))" constdefs aux_constr_names_caml_typedef_of_caml_typedef_list :: "caml_typedef list => constr_name list" "aux_constr_names_caml_typedef_of_caml_typedef_list == (%(aux_constr_names_caml_typedef_of_caml_typedef_list,aux_type_names_caml_typedef_of_caml_typedef_list).aux_constr_names_caml_typedef_of_caml_typedef_list) o aux_constr_names_caml_typedef_of_caml_typedef_list_aux_type_names_caml_typedef_of_caml_typedef_list" constdefs aux_type_names_caml_typedef_of_caml_typedef_list :: "caml_typedef list => typeconstr_name list" "aux_type_names_caml_typedef_of_caml_typedef_list == (%(aux_constr_names_caml_typedef_of_caml_typedef_list,aux_type_names_caml_typedef_of_caml_typedef_list).aux_type_names_caml_typedef_of_caml_typedef_list) o aux_constr_names_caml_typedef_of_caml_typedef_list_aux_type_names_caml_typedef_of_caml_typedef_list" consts aux_typevars_type_param_of_type_param_list :: "type_param list => typevar list" primrec "aux_typevars_type_param_of_type_param_list Nil = ([])" "aux_typevars_type_param_of_type_param_list (type_param_XXX#type_param_list_XXX) = ((aux_typevars_type_param_of_type_param type_param_XXX) @ (aux_typevars_type_param_of_type_param_list type_param_list_XXX))" consts aux_xs_caml_definition_of_caml_definition :: "caml_definition => value_name list" primrec "aux_xs_caml_definition_of_caml_definition (D_let let_binding) = ((aux_xs_let_binding_of_let_binding let_binding))" "aux_xs_caml_definition_of_caml_definition (D_letrec letrec_bindings) = ((aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings))" "aux_xs_caml_definition_of_caml_definition (D_type caml_type_definition) = ([])" "aux_xs_caml_definition_of_caml_definition (D_exception exception_definition) = ([])" consts aux_constr_names_caml_type_definition_of_caml_type_definition_aux_type_names_caml_type_definition_of_caml_type_definition :: "caml_type_definition => (constr_name list) * (typeconstr_name list)" primrec "aux_constr_names_caml_type_definition_of_caml_type_definition_aux_type_names_caml_type_definition_of_caml_type_definition (TDF_tdf (caml_typedef_list)) = (((%(aux_constr_names_caml_typedef_of_caml_typedef_list,aux_type_names_caml_typedef_of_caml_typedef_list).aux_constr_names_caml_typedef_of_caml_typedef_list) (aux_constr_names_caml_typedef_of_caml_typedef_list_aux_type_names_caml_typedef_of_caml_typedef_list caml_typedef_list)) , ((%(aux_constr_names_caml_typedef_of_caml_typedef_list,aux_type_names_caml_typedef_of_caml_typedef_list).aux_type_names_caml_typedef_of_caml_typedef_list) (aux_constr_names_caml_typedef_of_caml_typedef_list_aux_type_names_caml_typedef_of_caml_typedef_list caml_typedef_list)))" constdefs aux_constr_names_caml_type_definition_of_caml_type_definition :: "caml_type_definition => constr_name list" "aux_constr_names_caml_type_definition_of_caml_type_definition == (%(aux_constr_names_caml_type_definition_of_caml_type_definition,aux_type_names_caml_type_definition_of_caml_type_definition).aux_constr_names_caml_type_definition_of_caml_type_definition) o aux_constr_names_caml_type_definition_of_caml_type_definition_aux_type_names_caml_type_definition_of_caml_type_definition" constdefs aux_type_names_caml_type_definition_of_caml_type_definition :: "caml_type_definition => typeconstr_name list" "aux_type_names_caml_type_definition_of_caml_type_definition == (%(aux_constr_names_caml_type_definition_of_caml_type_definition,aux_type_names_caml_type_definition_of_caml_type_definition).aux_type_names_caml_type_definition_of_caml_type_definition) o aux_constr_names_caml_type_definition_of_caml_type_definition_aux_type_names_caml_type_definition_of_caml_type_definition" consts aux_typevars_type_params_opt_of_type_params_opt :: "type_params_opt => typevar list" primrec "aux_typevars_type_params_opt_of_type_params_opt (TPS_nary (type_param_list)) = ((aux_typevars_type_param_of_type_param_list type_param_list))" (** free variables *) consts ftv_typexpr_list_TE_constr :: "typexpr list => typevar list" ftv_typexpr_list_TE_tuple :: "typexpr list => typevar list" ftv_typexpr :: "typexpr => typevar list" primrec "ftv_typexpr_list_TE_constr Nil = ([])" "ftv_typexpr_list_TE_constr (typexpr_XXX#typexpr_list_XXX) = ((ftv_typexpr typexpr_XXX) @ (ftv_typexpr_list_TE_constr typexpr_list_XXX))" "ftv_typexpr_list_TE_tuple Nil = ([])" "ftv_typexpr_list_TE_tuple (typexpr_XXX#typexpr_list_XXX) = ((ftv_typexpr typexpr_XXX) @ (ftv_typexpr_list_TE_tuple typexpr_list_XXX))" "ftv_typexpr (TE_var typevar) = ([typevar])" "ftv_typexpr (TE_idxvar idx num) = ([])" "ftv_typexpr TE_any = ([])" "ftv_typexpr (TE_arrow typexpr1 typexpr2) = ((ftv_typexpr typexpr1) @ (ftv_typexpr typexpr2))" "ftv_typexpr (TE_tuple (typexpr_list)) = ((ftv_typexpr_list_TE_tuple typexpr_list))" "ftv_typexpr (TE_constr (typexpr_list) typeconstr) = ((ftv_typexpr_list_TE_constr typexpr_list))" consts ftv_typexpr_list :: "typexpr list => typevar list" primrec "ftv_typexpr_list Nil = ([])" "ftv_typexpr_list (typexpr_XXX#typexpr_list_XXX) = ((ftv_typexpr typexpr_XXX) @ (ftv_typexpr_list typexpr_list_XXX))" consts ftv_constr_decl :: "constr_decl => typevar list" primrec "ftv_constr_decl (CD_nullary constr_name) = ([])" "ftv_constr_decl (CD_nary constr_name (typexpr_list)) = ((ftv_typexpr_list typexpr_list))" consts ftv_field_decl :: "field_decl => typevar list" primrec "ftv_field_decl (FD_immutable field_name typexpr) = ((ftv_typexpr typexpr))" consts ftv_constr_decl_list :: "constr_decl list => typevar list" primrec "ftv_constr_decl_list Nil = ([])" "ftv_constr_decl_list (constr_decl_XXX#constr_decl_list_XXX) = ((ftv_constr_decl constr_decl_XXX) @ (ftv_constr_decl_list constr_decl_list_XXX))" consts ftv_field_decl_list :: "field_decl list => typevar list" primrec "ftv_field_decl_list Nil = ([])" "ftv_field_decl_list (field_decl_XXX#field_decl_list_XXX) = ((ftv_field_decl field_decl_XXX) @ (ftv_field_decl_list field_decl_list_XXX))" consts ftv_type_equation :: "type_equation => typevar list" primrec "ftv_type_equation (TE_te typexpr) = ((ftv_typexpr typexpr))" consts ftv_type_representation :: "type_representation => typevar list" primrec "ftv_type_representation (TR_variant (constr_decl_list)) = ((ftv_constr_decl_list constr_decl_list))" "ftv_type_representation (TR_record (field_decl_list)) = ((ftv_field_decl_list field_decl_list))" consts ftv_type_information :: "type_information => typevar list" primrec "ftv_type_information (TI_eq type_equation) = ((ftv_type_equation type_equation))" "ftv_type_information (TI_def type_representation) = ((ftv_type_representation type_representation))" consts ftv_caml_typedef :: "caml_typedef => typevar list" primrec "ftv_caml_typedef (TD_td type_params_opt typeconstr_name type_information) = ((list_minus (ftv_type_information type_information) (aux_typevars_type_params_opt_of_type_params_opt type_params_opt)))" consts ftv_field_pattern_P_record :: "(field*pattern) => typevar list" ftv_field_pattern_list_P_record :: "(field*pattern) list => typevar list" ftv_pattern_list_P_tuple :: "pattern list => typevar list" ftv_pattern_list_P_construct :: "pattern list => typevar list" ftv_pattern :: "pattern => typevar list" primrec "ftv_field_pattern_P_record (field_XXX,pattern_XXX) = ((ftv_pattern pattern_XXX))" "ftv_field_pattern_list_P_record Nil = ([])" "ftv_field_pattern_list_P_record (field_pattern_XXX#field_pattern_list_XXX) = ((ftv_field_pattern_P_record field_pattern_XXX) @ (ftv_field_pattern_list_P_record field_pattern_list_XXX))" "ftv_pattern_list_P_tuple Nil = ([])" "ftv_pattern_list_P_tuple (pattern_XXX#pattern_list_XXX) = ((ftv_pattern pattern_XXX) @ (ftv_pattern_list_P_tuple pattern_list_XXX))" "ftv_pattern_list_P_construct Nil = ([])" "ftv_pattern_list_P_construct (pattern_XXX#pattern_list_XXX) = ((ftv_pattern pattern_XXX) @ (ftv_pattern_list_P_construct pattern_list_XXX))" "ftv_pattern (P_var value_name) = ([])" "ftv_pattern P_any = ([])" "ftv_pattern (P_constant constant) = ([])" "ftv_pattern (P_alias pattern value_name) = ((ftv_pattern pattern))" "ftv_pattern (P_typed pattern typexpr) = ((ftv_pattern pattern) @ (ftv_typexpr typexpr))" "ftv_pattern (P_or pattern1 pattern2) = ((ftv_pattern pattern1) @ (ftv_pattern pattern2))" "ftv_pattern (P_construct constr (pattern_list)) = ((ftv_pattern_list_P_construct pattern_list))" "ftv_pattern (P_construct_any constr) = ([])" "ftv_pattern (P_tuple (pattern_list)) = ((ftv_pattern_list_P_tuple pattern_list))" "ftv_pattern (P_record (field_pattern_list)) = ((ftv_field_pattern_list_P_record field_pattern_list))" "ftv_pattern (P_cons pattern1 pattern2) = ((ftv_pattern pattern1) @ (ftv_pattern pattern2))" consts ftv_caml_typedef_list :: "caml_typedef list => typevar list" primrec "ftv_caml_typedef_list Nil = ([])" "ftv_caml_typedef_list (caml_typedef_XXX#caml_typedef_list_XXX) = ((ftv_caml_typedef caml_typedef_XXX) @ (ftv_caml_typedef_list caml_typedef_list_XXX))" consts ftv_letrec_binding :: "letrec_binding => typevar list" ftv_letrec_binding_list :: "letrec_binding list => typevar list" ftv_letrec_bindings :: "letrec_bindings => typevar list" ftv_let_binding :: "let_binding => typevar list" ftv_pat_exp :: "pat_exp => typevar list" ftv_pat_exp_list :: "pat_exp list => typevar list" ftv_pattern_matching :: "pattern_matching => typevar list" ftv_field_expr_Expr_override :: "(field*expr) => typevar list" ftv_field_expr_list_Expr_override :: "(field*expr) list => typevar list" ftv_field_expr_Expr_record :: "(field*expr) => typevar list" ftv_field_expr_list_Expr_record :: "(field*expr) list => typevar list" ftv_expr_list_Expr_construct :: "expr list => typevar list" ftv_expr_list_Expr_tuple :: "expr list => typevar list" ftv_expr :: "expr => typevar list" primrec "ftv_letrec_binding (LRB_simple value_name pattern_matching) = ((ftv_pattern_matching pattern_matching))" "ftv_letrec_binding_list Nil = ([])" "ftv_letrec_binding_list (letrec_binding_XXX#letrec_binding_list_XXX) = ((ftv_letrec_binding letrec_binding_XXX) @ (ftv_letrec_binding_list letrec_binding_list_XXX))" "ftv_letrec_bindings (LRBs_inj (letrec_binding_list)) = ((ftv_letrec_binding_list letrec_binding_list))" "ftv_let_binding (LB_simple pattern expr) = ((ftv_pattern pattern) @ (ftv_expr expr))" "ftv_pat_exp (PE_inj pattern expr) = ((ftv_pattern pattern) @ (ftv_expr expr))" "ftv_pat_exp_list Nil = ([])" "ftv_pat_exp_list (pat_exp_XXX#pat_exp_list_XXX) = ((ftv_pat_exp pat_exp_XXX) @ (ftv_pat_exp_list pat_exp_list_XXX))" "ftv_pattern_matching (PM_pm (pat_exp_list)) = ((ftv_pat_exp_list pat_exp_list))" "ftv_field_expr_Expr_override (field_XXX,expr_XXX) = ((ftv_expr expr_XXX))" "ftv_field_expr_list_Expr_override Nil = ([])" "ftv_field_expr_list_Expr_override (field_expr_XXX#field_expr_list_XXX) = ((ftv_field_expr_Expr_override field_expr_XXX) @ (ftv_field_expr_list_Expr_override field_expr_list_XXX))" "ftv_field_expr_Expr_record (field_XXX,expr_XXX) = ((ftv_expr expr_XXX))" "ftv_field_expr_list_Expr_record Nil = ([])" "ftv_field_expr_list_Expr_record (field_expr_XXX#field_expr_list_XXX) = ((ftv_field_expr_Expr_record field_expr_XXX) @ (ftv_field_expr_list_Expr_record field_expr_list_XXX))" "ftv_expr_list_Expr_construct Nil = ([])" "ftv_expr_list_Expr_construct (expr_XXX#expr_list_XXX) = ((ftv_expr expr_XXX) @ (ftv_expr_list_Expr_construct expr_list_XXX))" "ftv_expr_list_Expr_tuple Nil = ([])" "ftv_expr_list_Expr_tuple (expr_XXX#expr_list_XXX) = ((ftv_expr expr_XXX) @ (ftv_expr_list_Expr_tuple expr_list_XXX))" "ftv_expr (Expr_uprim unary_prim) = ([])" "ftv_expr (Expr_bprim binary_prim) = ([])" "ftv_expr (Expr_ident value_name) = ([])" "ftv_expr (Expr_constant constant) = ([])" "ftv_expr (Expr_typed expr typexpr) = ((ftv_expr expr) @ (ftv_typexpr typexpr))" "ftv_expr (Expr_tuple (expr_list)) = ((ftv_expr_list_Expr_tuple expr_list))" "ftv_expr (Expr_construct constr (expr_list)) = ((ftv_expr_list_Expr_construct expr_list))" "ftv_expr (Expr_cons expr1 expr2) = ((ftv_expr expr1) @ (ftv_expr expr2))" "ftv_expr (Expr_record (field_expr_list)) = ((ftv_field_expr_list_Expr_record field_expr_list))" "ftv_expr (Expr_override expr (field_expr_list)) = ((ftv_expr expr) @ (ftv_field_expr_list_Expr_override field_expr_list))" "ftv_expr (Expr_apply expr1 expr2) = ((ftv_expr expr1) @ (ftv_expr expr2))" "ftv_expr (Expr_and expr1 expr2) = ((ftv_expr expr1) @ (ftv_expr expr2))" "ftv_expr (Expr_or expr1 expr2) = ((ftv_expr expr1) @ (ftv_expr expr2))" "ftv_expr (Expr_field expr field) = ((ftv_expr expr))" "ftv_expr (Expr_ifthenelse expr0 expr1 expr2) = ((ftv_expr expr0) @ (ftv_expr expr1) @ (ftv_expr expr2))" "ftv_expr (Expr_while expr1 expr2) = ((ftv_expr expr1) @ (ftv_expr expr2))" "ftv_expr (Expr_for x expr1 for_dirn expr2 expr3) = ((ftv_expr expr1) @ (ftv_expr expr2) @ (ftv_expr expr3))" "ftv_expr (Expr_sequence expr1 expr2) = ((ftv_expr expr1) @ (ftv_expr expr2))" "ftv_expr (Expr_match expr pattern_matching) = ((ftv_expr expr) @ (ftv_pattern_matching pattern_matching))" "ftv_expr (Expr_function pattern_matching) = ((ftv_pattern_matching pattern_matching))" "ftv_expr (Expr_try expr pattern_matching) = ((ftv_expr expr) @ (ftv_pattern_matching pattern_matching))" "ftv_expr (Expr_let let_binding expr) = ((ftv_let_binding let_binding) @ (ftv_expr expr))" "ftv_expr (Expr_letrec letrec_bindings expr) = ((ftv_letrec_bindings letrec_bindings) @ (ftv_expr expr))" "ftv_expr (Expr_assert expr) = ((ftv_expr expr))" "ftv_expr (Expr_location location) = ([])" consts ftv_caml_type_definition :: "caml_type_definition => typevar list" primrec "ftv_caml_type_definition (TDF_tdf (caml_typedef_list)) = ((ftv_caml_typedef_list caml_typedef_list))" consts ftv_exception_definition :: "exception_definition => typevar list" primrec "ftv_exception_definition (ED_def constr_decl) = ((ftv_constr_decl constr_decl))" consts fv_letrec_binding :: "letrec_binding => value_name list" fv_letrec_binding_list :: "letrec_binding list => value_name list" fv_letrec_bindings :: "letrec_bindings => value_name list" fv_let_binding :: "let_binding => value_name list" fv_pat_exp :: "pat_exp => value_name list" fv_pat_exp_list :: "pat_exp list => value_name list" fv_pattern_matching :: "pattern_matching => value_name list" fv_field_expr_Expr_override :: "(field*expr) => value_name list" fv_field_expr_list_Expr_override :: "(field*expr) list => value_name list" fv_field_expr_Expr_record :: "(field*expr) => value_name list" fv_field_expr_list_Expr_record :: "(field*expr) list => value_name list" fv_expr_list_Expr_construct :: "expr list => value_name list" fv_expr_list_Expr_tuple :: "expr list => value_name list" fv_expr :: "expr => value_name list" primrec "fv_letrec_binding (LRB_simple value_name pattern_matching) = ((fv_pattern_matching pattern_matching))" "fv_letrec_binding_list Nil = ([])" "fv_letrec_binding_list (letrec_binding_XXX#letrec_binding_list_XXX) = ((fv_letrec_binding letrec_binding_XXX) @ (fv_letrec_binding_list letrec_binding_list_XXX))" "fv_letrec_bindings (LRBs_inj (letrec_binding_list)) = ((fv_letrec_binding_list letrec_binding_list))" "fv_let_binding (LB_simple pattern expr) = ((fv_expr expr))" "fv_pat_exp (PE_inj pattern expr) = ((list_minus (fv_expr expr) (aux_xs_pattern_of_pattern pattern)))" "fv_pat_exp_list Nil = ([])" "fv_pat_exp_list (pat_exp_XXX#pat_exp_list_XXX) = ((fv_pat_exp pat_exp_XXX) @ (fv_pat_exp_list pat_exp_list_XXX))" "fv_pattern_matching (PM_pm (pat_exp_list)) = ((fv_pat_exp_list pat_exp_list))" "fv_field_expr_Expr_override (field_XXX,expr_XXX) = ((fv_expr expr_XXX))" "fv_field_expr_list_Expr_override Nil = ([])" "fv_field_expr_list_Expr_override (field_expr_XXX#field_expr_list_XXX) = ((fv_field_expr_Expr_override field_expr_XXX) @ (fv_field_expr_list_Expr_override field_expr_list_XXX))" "fv_field_expr_Expr_record (field_XXX,expr_XXX) = ((fv_expr expr_XXX))" "fv_field_expr_list_Expr_record Nil = ([])" "fv_field_expr_list_Expr_record (field_expr_XXX#field_expr_list_XXX) = ((fv_field_expr_Expr_record field_expr_XXX) @ (fv_field_expr_list_Expr_record field_expr_list_XXX))" "fv_expr_list_Expr_construct Nil = ([])" "fv_expr_list_Expr_construct (expr_XXX#expr_list_XXX) = ((fv_expr expr_XXX) @ (fv_expr_list_Expr_construct expr_list_XXX))" "fv_expr_list_Expr_tuple Nil = ([])" "fv_expr_list_Expr_tuple (expr_XXX#expr_list_XXX) = ((fv_expr expr_XXX) @ (fv_expr_list_Expr_tuple expr_list_XXX))" "fv_expr (Expr_uprim unary_prim) = ([])" "fv_expr (Expr_bprim binary_prim) = ([])" "fv_expr (Expr_ident value_name) = ([value_name])" "fv_expr (Expr_constant constant) = ([])" "fv_expr (Expr_typed expr typexpr) = ((fv_expr expr))" "fv_expr (Expr_tuple (expr_list)) = ((fv_expr_list_Expr_tuple expr_list))" "fv_expr (Expr_construct constr (expr_list)) = ((fv_expr_list_Expr_construct expr_list))" "fv_expr (Expr_cons expr1 expr2) = ((fv_expr expr1) @ (fv_expr expr2))" "fv_expr (Expr_record (field_expr_list)) = ((fv_field_expr_list_Expr_record field_expr_list))" "fv_expr (Expr_override expr (field_expr_list)) = ((fv_expr expr) @ (fv_field_expr_list_Expr_override field_expr_list))" "fv_expr (Expr_apply expr1 expr2) = ((fv_expr expr1) @ (fv_expr expr2))" "fv_expr (Expr_and expr1 expr2) = ((fv_expr expr1) @ (fv_expr expr2))" "fv_expr (Expr_or expr1 expr2) = ((fv_expr expr1) @ (fv_expr expr2))" "fv_expr (Expr_field expr field) = ((fv_expr expr))" "fv_expr (Expr_ifthenelse expr0 expr1 expr2) = ((fv_expr expr0) @ (fv_expr expr1) @ (fv_expr expr2))" "fv_expr (Expr_while expr1 expr2) = ((fv_expr expr1) @ (fv_expr expr2))" "fv_expr (Expr_for x expr1 for_dirn expr2 expr3) = ((fv_expr expr1) @ (fv_expr expr2) @ (list_minus (fv_expr expr3) [x]))" "fv_expr (Expr_sequence expr1 expr2) = ((fv_expr expr1) @ (fv_expr expr2))" "fv_expr (Expr_match expr pattern_matching) = ((fv_expr expr) @ (fv_pattern_matching pattern_matching))" "fv_expr (Expr_function pattern_matching) = ((fv_pattern_matching pattern_matching))" "fv_expr (Expr_try expr pattern_matching) = ((fv_expr expr) @ (fv_pattern_matching pattern_matching))" "fv_expr (Expr_let let_binding expr) = ((fv_let_binding let_binding) @ (list_minus (fv_expr expr) (aux_xs_let_binding_of_let_binding let_binding)))" "fv_expr (Expr_letrec letrec_bindings expr) = ((list_minus (fv_letrec_bindings letrec_bindings) (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings)) @ (list_minus (fv_expr expr) (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings)))" "fv_expr (Expr_assert expr) = ((fv_expr expr))" "fv_expr (Expr_location location) = ([])" consts fl_letrec_binding :: "letrec_binding => location list" fl_letrec_binding_list :: "letrec_binding list => location list" fl_letrec_bindings :: "letrec_bindings => location list" fl_let_binding :: "let_binding => location list" fl_pat_exp :: "pat_exp => location list" fl_pat_exp_list :: "pat_exp list => location list" fl_pattern_matching :: "pattern_matching => location list" fl_field_expr_Expr_override :: "(field*expr) => location list" fl_field_expr_list_Expr_override :: "(field*expr) list => location list" fl_field_expr_Expr_record :: "(field*expr) => location list" fl_field_expr_list_Expr_record :: "(field*expr) list => location list" fl_expr_list_Expr_construct :: "expr list => location list" fl_expr_list_Expr_tuple :: "expr list => location list" fl_expr :: "expr => location list" primrec "fl_letrec_binding (LRB_simple value_name pattern_matching) = ((fl_pattern_matching pattern_matching))" "fl_letrec_binding_list Nil = ([])" "fl_letrec_binding_list (letrec_binding_XXX#letrec_binding_list_XXX) = ((fl_letrec_binding letrec_binding_XXX) @ (fl_letrec_binding_list letrec_binding_list_XXX))" "fl_letrec_bindings (LRBs_inj (letrec_binding_list)) = ((fl_letrec_binding_list letrec_binding_list))" "fl_let_binding (LB_simple pattern expr) = ((fl_expr expr))" "fl_pat_exp (PE_inj pattern expr) = ((fl_expr expr))" "fl_pat_exp_list Nil = ([])" "fl_pat_exp_list (pat_exp_XXX#pat_exp_list_XXX) = ((fl_pat_exp pat_exp_XXX) @ (fl_pat_exp_list pat_exp_list_XXX))" "fl_pattern_matching (PM_pm (pat_exp_list)) = ((fl_pat_exp_list pat_exp_list))" "fl_field_expr_Expr_override (field_XXX,expr_XXX) = ((fl_expr expr_XXX))" "fl_field_expr_list_Expr_override Nil = ([])" "fl_field_expr_list_Expr_override (field_expr_XXX#field_expr_list_XXX) = ((fl_field_expr_Expr_override field_expr_XXX) @ (fl_field_expr_list_Expr_override field_expr_list_XXX))" "fl_field_expr_Expr_record (field_XXX,expr_XXX) = ((fl_expr expr_XXX))" "fl_field_expr_list_Expr_record Nil = ([])" "fl_field_expr_list_Expr_record (field_expr_XXX#field_expr_list_XXX) = ((fl_field_expr_Expr_record field_expr_XXX) @ (fl_field_expr_list_Expr_record field_expr_list_XXX))" "fl_expr_list_Expr_construct Nil = ([])" "fl_expr_list_Expr_construct (expr_XXX#expr_list_XXX) = ((fl_expr expr_XXX) @ (fl_expr_list_Expr_construct expr_list_XXX))" "fl_expr_list_Expr_tuple Nil = ([])" "fl_expr_list_Expr_tuple (expr_XXX#expr_list_XXX) = ((fl_expr expr_XXX) @ (fl_expr_list_Expr_tuple expr_list_XXX))" "fl_expr (Expr_uprim unary_prim) = ([])" "fl_expr (Expr_bprim binary_prim) = ([])" "fl_expr (Expr_ident value_name) = ([])" "fl_expr (Expr_constant constant) = ([])" "fl_expr (Expr_typed expr typexpr) = ((fl_expr expr))" "fl_expr (Expr_tuple (expr_list)) = ((fl_expr_list_Expr_tuple expr_list))" "fl_expr (Expr_construct constr (expr_list)) = ((fl_expr_list_Expr_construct expr_list))" "fl_expr (Expr_cons expr1 expr2) = ((fl_expr expr1) @ (fl_expr expr2))" "fl_expr (Expr_record (field_expr_list)) = ((fl_field_expr_list_Expr_record field_expr_list))" "fl_expr (Expr_override expr (field_expr_list)) = ((fl_expr expr) @ (fl_field_expr_list_Expr_override field_expr_list))" "fl_expr (Expr_apply expr1 expr2) = ((fl_expr expr1) @ (fl_expr expr2))" "fl_expr (Expr_and expr1 expr2) = ((fl_expr expr1) @ (fl_expr expr2))" "fl_expr (Expr_or expr1 expr2) = ((fl_expr expr1) @ (fl_expr expr2))" "fl_expr (Expr_field expr field) = ((fl_expr expr))" "fl_expr (Expr_ifthenelse expr0 expr1 expr2) = ((fl_expr expr0) @ (fl_expr expr1) @ (fl_expr expr2))" "fl_expr (Expr_while expr1 expr2) = ((fl_expr expr1) @ (fl_expr expr2))" "fl_expr (Expr_for x expr1 for_dirn expr2 expr3) = ((fl_expr expr1) @ (fl_expr expr2) @ (fl_expr expr3))" "fl_expr (Expr_sequence expr1 expr2) = ((fl_expr expr1) @ (fl_expr expr2))" "fl_expr (Expr_match expr pattern_matching) = ((fl_expr expr) @ (fl_pattern_matching pattern_matching))" "fl_expr (Expr_function pattern_matching) = ((fl_pattern_matching pattern_matching))" "fl_expr (Expr_try expr pattern_matching) = ((fl_expr expr) @ (fl_pattern_matching pattern_matching))" "fl_expr (Expr_let let_binding expr) = ((fl_let_binding let_binding) @ (fl_expr expr))" "fl_expr (Expr_letrec letrec_bindings expr) = ((fl_letrec_bindings letrec_bindings) @ (fl_expr expr))" "fl_expr (Expr_assert expr) = ((fl_expr expr))" "fl_expr (Expr_location location) = ([location])" consts ftv_value_name_expr :: "(value_name*expr) => typevar list" primrec "ftv_value_name_expr (value_name_XXX,expr_XXX) = ((ftv_expr expr_XXX))" consts ftv_caml_definition :: "caml_definition => typevar list" primrec "ftv_caml_definition (D_let let_binding) = ((ftv_let_binding let_binding))" "ftv_caml_definition (D_letrec letrec_bindings) = ((ftv_letrec_bindings letrec_bindings))" "ftv_caml_definition (D_type caml_type_definition) = ((ftv_caml_type_definition caml_type_definition))" "ftv_caml_definition (D_exception exception_definition) = ((ftv_exception_definition exception_definition))" consts fv_value_name_expr :: "(value_name*expr) => value_name list" primrec "fv_value_name_expr (value_name_XXX,expr_XXX) = ((fv_expr expr_XXX))" consts fv_caml_definition :: "caml_definition => value_name list" primrec "fv_caml_definition (D_let let_binding) = ((fv_let_binding let_binding))" "fv_caml_definition (D_letrec letrec_bindings) = ((list_minus (fv_letrec_bindings letrec_bindings) (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings)))" "fv_caml_definition (D_type caml_type_definition) = ([])" "fv_caml_definition (D_exception exception_definition) = ([])" consts fl_value_name_expr :: "(value_name*expr) => location list" primrec "fl_value_name_expr (value_name_XXX,expr_XXX) = ((fl_expr expr_XXX))" consts fl_caml_definition :: "caml_definition => location list" primrec "fl_caml_definition (D_let let_binding) = ((fl_let_binding let_binding))" "fl_caml_definition (D_letrec letrec_bindings) = ((fl_letrec_bindings letrec_bindings))" "fl_caml_definition (D_type caml_type_definition) = ([])" "fl_caml_definition (D_exception exception_definition) = ([])" consts ftv_value_name_expr_list :: "(value_name*expr) list => typevar list" primrec "ftv_value_name_expr_list Nil = ([])" "ftv_value_name_expr_list (value_name_expr_XXX#value_name_expr_list_XXX) = ((ftv_value_name_expr value_name_expr_XXX) @ (ftv_value_name_expr_list value_name_expr_list_XXX))" consts ftv_definitions :: "definitions => typevar list" primrec "ftv_definitions Ds_nil = ([])" "ftv_definitions (Ds_cons caml_definition definitions) = ((ftv_caml_definition caml_definition) @ (ftv_definitions definitions))" consts ftv_typescheme :: "typescheme => typevar list" primrec "ftv_typescheme (TS_forall typexpr) = ((ftv_typexpr typexpr))" consts ftv_typexprs :: "typexprs => typevar list" primrec "ftv_typexprs (typexprs_inj (typexpr_list)) = ((ftv_typexpr_list typexpr_list))" consts fv_value_name_expr_list :: "(value_name*expr) list => value_name list" primrec "fv_value_name_expr_list Nil = ([])" "fv_value_name_expr_list (value_name_expr_XXX#value_name_expr_list_XXX) = ((fv_value_name_expr value_name_expr_XXX) @ (fv_value_name_expr_list value_name_expr_list_XXX))" consts fv_definitions :: "definitions => value_name list" primrec "fv_definitions Ds_nil = ([])" "fv_definitions (Ds_cons caml_definition definitions) = ((fv_caml_definition caml_definition) @ (list_minus (fv_definitions definitions) (aux_xs_caml_definition_of_caml_definition caml_definition)))" consts fl_value_name_expr_list :: "(value_name*expr) list => location list" primrec "fl_value_name_expr_list Nil = ([])" "fl_value_name_expr_list (value_name_expr_XXX#value_name_expr_list_XXX) = ((fl_value_name_expr value_name_expr_XXX) @ (fl_value_name_expr_list value_name_expr_list_XXX))" consts fl_definitions :: "definitions => location list" primrec "fl_definitions Ds_nil = ([])" "fl_definitions (Ds_cons caml_definition definitions) = ((fl_caml_definition caml_definition) @ (fl_definitions definitions))" consts ftv_substs_x :: "substs_x => typevar list" primrec "ftv_substs_x (substs_x_xs (value_name_expr_list)) = ((ftv_value_name_expr_list value_name_expr_list))" consts ftv_program :: "program => typevar list" primrec "ftv_program (Prog_defs definitions) = ((ftv_definitions definitions))" "ftv_program (Prog_raise expr) = ((ftv_expr expr))" consts ftv_environment_binding :: "environment_binding => typevar list" primrec "ftv_environment_binding EB_tv = ([])" "ftv_environment_binding (EB_vn value_name typescheme) = ((ftv_typescheme typescheme))" "ftv_environment_binding (EB_cc constr_name typeconstr) = ([])" "ftv_environment_binding (EB_pc constr_name type_params_opt typexprs typeconstr) = ((list_minus (ftv_typexprs typexprs) (aux_typevars_type_params_opt_of_type_params_opt type_params_opt)))" "ftv_environment_binding (EB_fn field_name type_params_opt typeconstr_name typexpr) = ((list_minus (ftv_typexpr typexpr) (aux_typevars_type_params_opt_of_type_params_opt type_params_opt)))" "ftv_environment_binding (EB_td typeconstr_name kind) = ([])" "ftv_environment_binding (EB_tr typeconstr_name kind (field_name_list)) = ([])" "ftv_environment_binding (EB_ta type_params_opt typeconstr_name typexpr) = ((list_minus (ftv_typexpr typexpr) (aux_typevars_type_params_opt_of_type_params_opt type_params_opt)))" "ftv_environment_binding (EB_l location typexpr) = ((ftv_typexpr typexpr))" consts ftv_trans_label :: "trans_label => typevar list" primrec "ftv_trans_label Lab_nil = ([])" "ftv_trans_label (Lab_alloc v location) = ([])" "ftv_trans_label (Lab_deref location v) = ([])" "ftv_trans_label (Lab_assign location v) = ([])" consts fv_substs_x :: "substs_x => value_name list" primrec "fv_substs_x (substs_x_xs (value_name_expr_list)) = ((fv_value_name_expr_list value_name_expr_list))" consts fv_program :: "program => value_name list" primrec "fv_program (Prog_defs definitions) = ((fv_definitions definitions))" "fv_program (Prog_raise expr) = ((fv_expr expr))" consts fv_trans_label :: "trans_label => value_name list" primrec "fv_trans_label Lab_nil = ([])" "fv_trans_label (Lab_alloc v location) = ([])" "fv_trans_label (Lab_deref location v) = ([])" "fv_trans_label (Lab_assign location v) = ([])" consts fl_substs_x :: "substs_x => location list" primrec "fl_substs_x (substs_x_xs (value_name_expr_list)) = ((fl_value_name_expr_list value_name_expr_list))" consts fl_program :: "program => location list" primrec "fl_program (Prog_defs definitions) = ((fl_definitions definitions))" "fl_program (Prog_raise expr) = ((fl_expr expr))" consts fl_trans_label :: "trans_label => location list" primrec "fl_trans_label Lab_nil = ([])" "fl_trans_label (Lab_alloc v location) = ([])" "fl_trans_label (Lab_deref location v) = ([])" "fl_trans_label (Lab_assign location v) = ([])" (** substitutions *) consts substs_typevar_typexpr_list_TE_constr :: "(typevar*typexpr) list => typexpr list => typexpr list" substs_typevar_typexpr_list_TE_tuple :: "(typevar*typexpr) list => typexpr list => typexpr list" substs_typevar_typexpr :: "(typevar*typexpr) list => typexpr => typexpr" primrec "substs_typevar_typexpr_list_TE_constr sub Nil = (Nil)" "substs_typevar_typexpr_list_TE_constr sub (typexpr_XXX#typexpr_list_XXX) = ((substs_typevar_typexpr sub typexpr_XXX) # (substs_typevar_typexpr_list_TE_constr sub typexpr_list_XXX))" "substs_typevar_typexpr_list_TE_tuple sub Nil = (Nil)" "substs_typevar_typexpr_list_TE_tuple sub (typexpr_XXX#typexpr_list_XXX) = ((substs_typevar_typexpr sub typexpr_XXX) # (substs_typevar_typexpr_list_TE_tuple sub typexpr_list_XXX))" "substs_typevar_typexpr sub (TE_var typevar) = ((case list_assoc typevar sub of None => (TE_var typevar) | Some t_5 => t_5))" "substs_typevar_typexpr sub (TE_idxvar idx num) = (TE_idxvar idx num)" "substs_typevar_typexpr sub TE_any = (TE_any )" "substs_typevar_typexpr sub (TE_arrow typexpr1 typexpr2) = (TE_arrow (substs_typevar_typexpr sub typexpr1) (substs_typevar_typexpr sub typexpr2))" "substs_typevar_typexpr sub (TE_tuple (typexpr_list)) = (TE_tuple (substs_typevar_typexpr_list_TE_tuple sub typexpr_list))" "substs_typevar_typexpr sub (TE_constr (typexpr_list) typeconstr) = (TE_constr (substs_typevar_typexpr_list_TE_constr sub typexpr_list) typeconstr)" consts substs_typevar_typexpr_list :: "(typevar*typexpr) list => typexpr list => typexpr list" primrec "substs_typevar_typexpr_list sub Nil = (Nil)" "substs_typevar_typexpr_list sub (typexpr_XXX#typexpr_list_XXX) = ((substs_typevar_typexpr sub typexpr_XXX) # (substs_typevar_typexpr_list sub typexpr_list_XXX))" consts substs_typevar_constr_decl :: "(typevar*typexpr) list => constr_decl => constr_decl" primrec "substs_typevar_constr_decl sub (CD_nullary constr_name) = (CD_nullary constr_name)" "substs_typevar_constr_decl sub (CD_nary constr_name (typexpr_list)) = (CD_nary constr_name (substs_typevar_typexpr_list sub typexpr_list))" consts substs_typevar_field_decl :: "(typevar*typexpr) list => field_decl => field_decl" primrec "substs_typevar_field_decl sub (FD_immutable field_name typexpr) = (FD_immutable field_name (substs_typevar_typexpr sub typexpr))" consts substs_typevar_constr_decl_list :: "(typevar*typexpr) list => constr_decl list => constr_decl list" primrec "substs_typevar_constr_decl_list sub Nil = (Nil)" "substs_typevar_constr_decl_list sub (constr_decl_XXX#constr_decl_list_XXX) = ((substs_typevar_constr_decl sub constr_decl_XXX) # (substs_typevar_constr_decl_list sub constr_decl_list_XXX))" consts substs_typevar_field_decl_list :: "(typevar*typexpr) list => field_decl list => field_decl list" primrec "substs_typevar_field_decl_list sub Nil = (Nil)" "substs_typevar_field_decl_list sub (field_decl_XXX#field_decl_list_XXX) = ((substs_typevar_field_decl sub field_decl_XXX) # (substs_typevar_field_decl_list sub field_decl_list_XXX))" consts substs_typevar_type_equation :: "(typevar*typexpr) list => type_equation => type_equation" primrec "substs_typevar_type_equation sub (TE_te typexpr) = (TE_te (substs_typevar_typexpr sub typexpr))" consts substs_typevar_type_representation :: "(typevar*typexpr) list => type_representation => type_representation" primrec "substs_typevar_type_representation sub (TR_variant (constr_decl_list)) = (TR_variant (substs_typevar_constr_decl_list sub constr_decl_list))" "substs_typevar_type_representation sub (TR_record (field_decl_list)) = (TR_record (substs_typevar_field_decl_list sub field_decl_list))" consts substs_typevar_type_information :: "(typevar*typexpr) list => type_information => type_information" primrec "substs_typevar_type_information sub (TI_eq type_equation) = (TI_eq (substs_typevar_type_equation sub type_equation))" "substs_typevar_type_information sub (TI_def type_representation) = (TI_def (substs_typevar_type_representation sub type_representation))" consts substs_typevar_caml_typedef :: "(typevar*typexpr) list => caml_typedef => caml_typedef" primrec "substs_typevar_caml_typedef sub (TD_td type_params_opt typeconstr_name type_information) = (TD_td type_params_opt typeconstr_name (substs_typevar_type_information (List.filter (%(tv5,t5).Not(tv5 mem (aux_typevars_type_params_opt_of_type_params_opt type_params_opt))) sub) type_information))" consts substs_typevar_field_pattern_P_record :: "(typevar*typexpr) list => (field*pattern) => (field*pattern)" substs_typevar_field_pattern_list_P_record :: "(typevar*typexpr) list => (field*pattern) list => (field*pattern) list" substs_typevar_pattern_list_P_tuple :: "(typevar*typexpr) list => pattern list => pattern list" substs_typevar_pattern_list_P_construct :: "(typevar*typexpr) list => pattern list => pattern list" substs_typevar_pattern :: "(typevar*typexpr) list => pattern => pattern" primrec "substs_typevar_field_pattern_P_record sub (field1,pattern1) = (field1 , substs_typevar_pattern sub pattern1)" "substs_typevar_field_pattern_list_P_record sub Nil = (Nil)" "substs_typevar_field_pattern_list_P_record sub (field_pattern_XXX#field_pattern_list_XXX) = ((substs_typevar_field_pattern_P_record sub field_pattern_XXX) # (substs_typevar_field_pattern_list_P_record sub field_pattern_list_XXX))" "substs_typevar_pattern_list_P_tuple sub Nil = (Nil)" "substs_typevar_pattern_list_P_tuple sub (pattern_XXX#pattern_list_XXX) = ((substs_typevar_pattern sub pattern_XXX) # (substs_typevar_pattern_list_P_tuple sub pattern_list_XXX))" "substs_typevar_pattern_list_P_construct sub Nil = (Nil)" "substs_typevar_pattern_list_P_construct sub (pattern_XXX#pattern_list_XXX) = ((substs_typevar_pattern sub pattern_XXX) # (substs_typevar_pattern_list_P_construct sub pattern_list_XXX))" "substs_typevar_pattern sub (P_var value_name) = (P_var value_name)" "substs_typevar_pattern sub P_any = (P_any )" "substs_typevar_pattern sub (P_constant constant) = (P_constant constant)" "substs_typevar_pattern sub (P_alias pattern value_name) = (P_alias (substs_typevar_pattern sub pattern) value_name)" "substs_typevar_pattern sub (P_typed pattern typexpr) = (P_typed (substs_typevar_pattern sub pattern) (substs_typevar_typexpr sub typexpr))" "substs_typevar_pattern sub (P_or pattern1 pattern2) = (P_or (substs_typevar_pattern sub pattern1) (substs_typevar_pattern sub pattern2))" "substs_typevar_pattern sub (P_construct constr (pattern_list)) = (P_construct constr (substs_typevar_pattern_list_P_construct sub pattern_list))" "substs_typevar_pattern sub (P_construct_any constr) = (P_construct_any constr)" "substs_typevar_pattern sub (P_tuple (pattern_list)) = (P_tuple (substs_typevar_pattern_list_P_tuple sub pattern_list))" "substs_typevar_pattern sub (P_record (field_pattern_list)) = (P_record (substs_typevar_field_pattern_list_P_record sub field_pattern_list))" "substs_typevar_pattern sub (P_cons pattern1 pattern2) = (P_cons (substs_typevar_pattern sub pattern1) (substs_typevar_pattern sub pattern2))" consts substs_typevar_caml_typedef_list :: "(typevar*typexpr) list => caml_typedef list => caml_typedef list" primrec "substs_typevar_caml_typedef_list sub Nil = (Nil)" "substs_typevar_caml_typedef_list sub (caml_typedef_XXX#caml_typedef_list_XXX) = ((substs_typevar_caml_typedef sub caml_typedef_XXX) # (substs_typevar_caml_typedef_list sub caml_typedef_list_XXX))" consts substs_typevar_letrec_binding :: "(typevar*typexpr) list => letrec_binding => letrec_binding" substs_typevar_letrec_binding_list :: "(typevar*typexpr) list => letrec_binding list => letrec_binding list" substs_typevar_letrec_bindings :: "(typevar*typexpr) list => letrec_bindings => letrec_bindings" substs_typevar_let_binding :: "(typevar*typexpr) list => let_binding => let_binding" substs_typevar_pat_exp :: "(typevar*typexpr) list => pat_exp => pat_exp" substs_typevar_pat_exp_list :: "(typevar*typexpr) list => pat_exp list => pat_exp list" substs_typevar_pattern_matching :: "(typevar*typexpr) list => pattern_matching => pattern_matching" substs_typevar_field_expr_Expr_override :: "(typevar*typexpr) list => (field*expr) => (field*expr)" substs_typevar_field_expr_list_Expr_override :: "(typevar*typexpr) list => (field*expr) list => (field*expr) list" substs_typevar_field_expr_Expr_record :: "(typevar*typexpr) list => (field*expr) => (field*expr)" substs_typevar_field_expr_list_Expr_record :: "(typevar*typexpr) list => (field*expr) list => (field*expr) list" substs_typevar_expr_list_Expr_construct :: "(typevar*typexpr) list => expr list => expr list" substs_typevar_expr_list_Expr_tuple :: "(typevar*typexpr) list => expr list => expr list" substs_typevar_expr :: "(typevar*typexpr) list => expr => expr" primrec "substs_typevar_letrec_binding sub (LRB_simple value_name pattern_matching) = (LRB_simple value_name (substs_typevar_pattern_matching sub pattern_matching))" "substs_typevar_letrec_binding_list sub Nil = (Nil)" "substs_typevar_letrec_binding_list sub (letrec_binding_XXX#letrec_binding_list_XXX) = ((substs_typevar_letrec_binding sub letrec_binding_XXX) # (substs_typevar_letrec_binding_list sub letrec_binding_list_XXX))" "substs_typevar_letrec_bindings sub (LRBs_inj (letrec_binding_list)) = (LRBs_inj (substs_typevar_letrec_binding_list sub letrec_binding_list))" "substs_typevar_let_binding sub (LB_simple pattern expr) = (LB_simple (substs_typevar_pattern sub pattern) (substs_typevar_expr sub expr))" "substs_typevar_pat_exp sub (PE_inj pattern expr) = (PE_inj (substs_typevar_pattern sub pattern) (substs_typevar_expr sub expr))" "substs_typevar_pat_exp_list sub Nil = (Nil)" "substs_typevar_pat_exp_list sub (pat_exp_XXX#pat_exp_list_XXX) = ((substs_typevar_pat_exp sub pat_exp_XXX) # (substs_typevar_pat_exp_list sub pat_exp_list_XXX))" "substs_typevar_pattern_matching sub (PM_pm (pat_exp_list)) = (PM_pm (substs_typevar_pat_exp_list sub pat_exp_list))" "substs_typevar_field_expr_Expr_override sub (field1,expr1) = (field1 , substs_typevar_expr sub expr1)" "substs_typevar_field_expr_list_Expr_override sub Nil = (Nil)" "substs_typevar_field_expr_list_Expr_override sub (field_expr_XXX#field_expr_list_XXX) = ((substs_typevar_field_expr_Expr_override sub field_expr_XXX) # (substs_typevar_field_expr_list_Expr_override sub field_expr_list_XXX))" "substs_typevar_field_expr_Expr_record sub (field1,expr1) = (field1 , substs_typevar_expr sub expr1)" "substs_typevar_field_expr_list_Expr_record sub Nil = (Nil)" "substs_typevar_field_expr_list_Expr_record sub (field_expr_XXX#field_expr_list_XXX) = ((substs_typevar_field_expr_Expr_record sub field_expr_XXX) # (substs_typevar_field_expr_list_Expr_record sub field_expr_list_XXX))" "substs_typevar_expr_list_Expr_construct sub Nil = (Nil)" "substs_typevar_expr_list_Expr_construct sub (expr_XXX#expr_list_XXX) = ((substs_typevar_expr sub expr_XXX) # (substs_typevar_expr_list_Expr_construct sub expr_list_XXX))" "substs_typevar_expr_list_Expr_tuple sub Nil = (Nil)" "substs_typevar_expr_list_Expr_tuple sub (expr_XXX#expr_list_XXX) = ((substs_typevar_expr sub expr_XXX) # (substs_typevar_expr_list_Expr_tuple sub expr_list_XXX))" "substs_typevar_expr sub (Expr_uprim unary_prim) = (Expr_uprim unary_prim)" "substs_typevar_expr sub (Expr_bprim binary_prim) = (Expr_bprim binary_prim)" "substs_typevar_expr sub (Expr_ident value_name) = (Expr_ident value_name)" "substs_typevar_expr sub (Expr_constant constant) = (Expr_constant constant)" "substs_typevar_expr sub (Expr_typed expr typexpr) = (Expr_typed (substs_typevar_expr sub expr) (substs_typevar_typexpr sub typexpr))" "substs_typevar_expr sub (Expr_tuple (expr_list)) = (Expr_tuple (substs_typevar_expr_list_Expr_tuple sub expr_list))" "substs_typevar_expr sub (Expr_construct constr (expr_list)) = (Expr_construct constr (substs_typevar_expr_list_Expr_construct sub expr_list))" "substs_typevar_expr sub (Expr_cons expr1 expr2) = (Expr_cons (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2))" "substs_typevar_expr sub (Expr_record (field_expr_list)) = (Expr_record (substs_typevar_field_expr_list_Expr_record sub field_expr_list))" "substs_typevar_expr sub (Expr_override expr (field_expr_list)) = (Expr_override (substs_typevar_expr sub expr) (substs_typevar_field_expr_list_Expr_override sub field_expr_list))" "substs_typevar_expr sub (Expr_apply expr1 expr2) = (Expr_apply (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2))" "substs_typevar_expr sub (Expr_and expr1 expr2) = (Expr_and (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2))" "substs_typevar_expr sub (Expr_or expr1 expr2) = (Expr_or (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2))" "substs_typevar_expr sub (Expr_field expr field) = (Expr_field (substs_typevar_expr sub expr) field)" "substs_typevar_expr sub (Expr_ifthenelse expr0 expr1 expr2) = (Expr_ifthenelse (substs_typevar_expr sub expr0) (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2))" "substs_typevar_expr sub (Expr_while expr1 expr2) = (Expr_while (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2))" "substs_typevar_expr sub (Expr_for x expr1 for_dirn expr2 expr3) = (Expr_for x (substs_typevar_expr sub expr1) for_dirn (substs_typevar_expr sub expr2) (substs_typevar_expr sub expr3))" "substs_typevar_expr sub (Expr_sequence expr1 expr2) = (Expr_sequence (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2))" "substs_typevar_expr sub (Expr_match expr pattern_matching) = (Expr_match (substs_typevar_expr sub expr) (substs_typevar_pattern_matching sub pattern_matching))" "substs_typevar_expr sub (Expr_function pattern_matching) = (Expr_function (substs_typevar_pattern_matching sub pattern_matching))" "substs_typevar_expr sub (Expr_try expr pattern_matching) = (Expr_try (substs_typevar_expr sub expr) (substs_typevar_pattern_matching sub pattern_matching))" "substs_typevar_expr sub (Expr_let let_binding expr) = (Expr_let (substs_typevar_let_binding sub let_binding) (substs_typevar_expr sub expr))" "substs_typevar_expr sub (Expr_letrec letrec_bindings expr) = (Expr_letrec (substs_typevar_letrec_bindings sub letrec_bindings) (substs_typevar_expr sub expr))" "substs_typevar_expr sub (Expr_assert expr) = (Expr_assert (substs_typevar_expr sub expr))" "substs_typevar_expr sub (Expr_location location) = (Expr_location location)" consts substs_typevar_caml_type_definition :: "(typevar*typexpr) list => caml_type_definition => caml_type_definition" primrec "substs_typevar_caml_type_definition sub (TDF_tdf (caml_typedef_list)) = (TDF_tdf (substs_typevar_caml_typedef_list sub caml_typedef_list))" consts substs_typevar_exception_definition :: "(typevar*typexpr) list => exception_definition => exception_definition" primrec "substs_typevar_exception_definition sub (ED_def constr_decl) = (ED_def (substs_typevar_constr_decl sub constr_decl))" consts substs_value_name_letrec_binding :: "(value_name*expr) list => letrec_binding => letrec_binding" substs_value_name_letrec_binding_list :: "(value_name*expr) list => letrec_binding list => letrec_binding list" substs_value_name_letrec_bindings :: "(value_name*expr) list => letrec_bindings => letrec_bindings" substs_value_name_let_binding :: "(value_name*expr) list => let_binding => let_binding" substs_value_name_pat_exp :: "(value_name*expr) list => pat_exp => pat_exp" substs_value_name_pat_exp_list :: "(value_name*expr) list => pat_exp list => pat_exp list" substs_value_name_pattern_matching :: "(value_name*expr) list => pattern_matching => pattern_matching" substs_value_name_field_expr_Expr_override :: "(value_name*expr) list => (field*expr) => (field*expr)" substs_value_name_field_expr_list_Expr_override :: "(value_name*expr) list => (field*expr) list => (field*expr) list" substs_value_name_field_expr_Expr_record :: "(value_name*expr) list => (field*expr) => (field*expr)" substs_value_name_field_expr_list_Expr_record :: "(value_name*expr) list => (field*expr) list => (field*expr) list" substs_value_name_expr_list_Expr_construct :: "(value_name*expr) list => expr list => expr list" substs_value_name_expr_list_Expr_tuple :: "(value_name*expr) list => expr list => expr list" substs_value_name_expr :: "(value_name*expr) list => expr => expr" primrec "substs_value_name_letrec_binding sub (LRB_simple value_name pattern_matching) = (LRB_simple value_name (substs_value_name_pattern_matching sub pattern_matching))" "substs_value_name_letrec_binding_list sub Nil = (Nil)" "substs_value_name_letrec_binding_list sub (letrec_binding_XXX#letrec_binding_list_XXX) = ((substs_value_name_letrec_binding sub letrec_binding_XXX) # (substs_value_name_letrec_binding_list sub letrec_binding_list_XXX))" "substs_value_name_letrec_bindings sub (LRBs_inj (letrec_binding_list)) = (LRBs_inj (substs_value_name_letrec_binding_list sub letrec_binding_list))" "substs_value_name_let_binding sub (LB_simple pattern expr) = (LB_simple pattern (substs_value_name_expr sub expr))" "substs_value_name_pat_exp sub (PE_inj pattern expr) = (PE_inj pattern (substs_value_name_expr (List.filter (%(x5,e5).Not(x5 mem (aux_xs_pattern_of_pattern pattern))) sub) expr))" "substs_value_name_pat_exp_list sub Nil = (Nil)" "substs_value_name_pat_exp_list sub (pat_exp_XXX#pat_exp_list_XXX) = ((substs_value_name_pat_exp sub pat_exp_XXX) # (substs_value_name_pat_exp_list sub pat_exp_list_XXX))" "substs_value_name_pattern_matching sub (PM_pm (pat_exp_list)) = (PM_pm (substs_value_name_pat_exp_list sub pat_exp_list))" "substs_value_name_field_expr_Expr_override sub (field1,expr1) = (field1 , substs_value_name_expr sub expr1)" "substs_value_name_field_expr_list_Expr_override sub Nil = (Nil)" "substs_value_name_field_expr_list_Expr_override sub (field_expr_XXX#field_expr_list_XXX) = ((substs_value_name_field_expr_Expr_override sub field_expr_XXX) # (substs_value_name_field_expr_list_Expr_override sub field_expr_list_XXX))" "substs_value_name_field_expr_Expr_record sub (field1,expr1) = (field1 , substs_value_name_expr sub expr1)" "substs_value_name_field_expr_list_Expr_record sub Nil = (Nil)" "substs_value_name_field_expr_list_Expr_record sub (field_expr_XXX#field_expr_list_XXX) = ((substs_value_name_field_expr_Expr_record sub field_expr_XXX) # (substs_value_name_field_expr_list_Expr_record sub field_expr_list_XXX))" "substs_value_name_expr_list_Expr_construct sub Nil = (Nil)" "substs_value_name_expr_list_Expr_construct sub (expr_XXX#expr_list_XXX) = ((substs_value_name_expr sub expr_XXX) # (substs_value_name_expr_list_Expr_construct sub expr_list_XXX))" "substs_value_name_expr_list_Expr_tuple sub Nil = (Nil)" "substs_value_name_expr_list_Expr_tuple sub (expr_XXX#expr_list_XXX) = ((substs_value_name_expr sub expr_XXX) # (substs_value_name_expr_list_Expr_tuple sub expr_list_XXX))" "substs_value_name_expr sub (Expr_uprim unary_prim) = (Expr_uprim unary_prim)" "substs_value_name_expr sub (Expr_bprim binary_prim) = (Expr_bprim binary_prim)" "substs_value_name_expr sub (Expr_ident value_name) = ((case list_assoc value_name sub of None => (Expr_ident value_name) | Some e5 => e5))" "substs_value_name_expr sub (Expr_constant constant) = (Expr_constant constant)" "substs_value_name_expr sub (Expr_typed expr typexpr) = (Expr_typed (substs_value_name_expr sub expr) typexpr)" "substs_value_name_expr sub (Expr_tuple (expr_list)) = (Expr_tuple (substs_value_name_expr_list_Expr_tuple sub expr_list))" "substs_value_name_expr sub (Expr_construct constr (expr_list)) = (Expr_construct constr (substs_value_name_expr_list_Expr_construct sub expr_list))" "substs_value_name_expr sub (Expr_cons expr1 expr2) = (Expr_cons (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2))" "substs_value_name_expr sub (Expr_record (field_expr_list)) = (Expr_record (substs_value_name_field_expr_list_Expr_record sub field_expr_list))" "substs_value_name_expr sub (Expr_override expr (field_expr_list)) = (Expr_override (substs_value_name_expr sub expr) (substs_value_name_field_expr_list_Expr_override sub field_expr_list))" "substs_value_name_expr sub (Expr_apply expr1 expr2) = (Expr_apply (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2))" "substs_value_name_expr sub (Expr_and expr1 expr2) = (Expr_and (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2))" "substs_value_name_expr sub (Expr_or expr1 expr2) = (Expr_or (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2))" "substs_value_name_expr sub (Expr_field expr field) = (Expr_field (substs_value_name_expr sub expr) field)" "substs_value_name_expr sub (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))" "substs_value_name_expr sub (Expr_while expr1 expr2) = (Expr_while (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2))" "substs_value_name_expr sub (Expr_for x expr1 for_dirn expr2 expr3) = (Expr_for x (substs_value_name_expr sub expr1) for_dirn (substs_value_name_expr sub expr2) (substs_value_name_expr (List.filter (%(x5,e5).Not(x5 mem [x])) sub) expr3))" "substs_value_name_expr sub (Expr_sequence expr1 expr2) = (Expr_sequence (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2))" "substs_value_name_expr sub (Expr_match expr pattern_matching) = (Expr_match (substs_value_name_expr sub expr) (substs_value_name_pattern_matching sub pattern_matching))" "substs_value_name_expr sub (Expr_function pattern_matching) = (Expr_function (substs_value_name_pattern_matching sub pattern_matching))" "substs_value_name_expr sub (Expr_try expr pattern_matching) = (Expr_try (substs_value_name_expr sub expr) (substs_value_name_pattern_matching sub pattern_matching))" "substs_value_name_expr sub (Expr_let let_binding expr) = (Expr_let (substs_value_name_let_binding sub let_binding) (substs_value_name_expr (List.filter (%(x5,e5).Not(x5 mem (aux_xs_let_binding_of_let_binding let_binding))) sub) expr))" "substs_value_name_expr sub (Expr_letrec letrec_bindings expr) = (Expr_letrec (substs_value_name_letrec_bindings (List.filter (%(x5,e5).Not(x5 mem (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings))) sub) letrec_bindings) (substs_value_name_expr (List.filter (%(x5,e5).Not(x5 mem (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings))) sub) expr))" "substs_value_name_expr sub (Expr_assert expr) = (Expr_assert (substs_value_name_expr sub expr))" "substs_value_name_expr sub (Expr_location location) = (Expr_location location)" consts subst_value_name_letrec_binding :: "expr => value_name => letrec_binding => letrec_binding" subst_value_name_letrec_binding_list :: "expr => value_name => letrec_binding list => letrec_binding list" subst_value_name_letrec_bindings :: "expr => value_name => letrec_bindings => letrec_bindings" subst_value_name_let_binding :: "expr => value_name => let_binding => let_binding" subst_value_name_pat_exp :: "expr => value_name => pat_exp => pat_exp" subst_value_name_pat_exp_list :: "expr => value_name => pat_exp list => pat_exp list" subst_value_name_pattern_matching :: "expr => value_name => pattern_matching => pattern_matching" subst_value_name_field_expr_Expr_override :: "expr => value_name => (field*expr) => (field*expr)" subst_value_name_field_expr_list_Expr_override :: "expr => value_name => (field*expr) list => (field*expr) list" subst_value_name_field_expr_Expr_record :: "expr => value_name => (field*expr) => (field*expr)" subst_value_name_field_expr_list_Expr_record :: "expr => value_name => (field*expr) list => (field*expr) list" subst_value_name_expr_list_Expr_construct :: "expr => value_name => expr list => expr list" subst_value_name_expr_list_Expr_tuple :: "expr => value_name => expr list => expr list" subst_value_name_expr :: "expr => value_name => expr => expr" primrec "subst_value_name_letrec_binding e5 x5 (LRB_simple value_name pattern_matching) = (LRB_simple value_name (subst_value_name_pattern_matching e5 x5 pattern_matching))" "subst_value_name_letrec_binding_list e5 x5 Nil = (Nil)" "subst_value_name_letrec_binding_list e5 x5 (letrec_binding_XXX#letrec_binding_list_XXX) = ((subst_value_name_letrec_binding e5 x5 letrec_binding_XXX) # (subst_value_name_letrec_binding_list e5 x5 letrec_binding_list_XXX))" "subst_value_name_letrec_bindings e5 x5 (LRBs_inj (letrec_binding_list)) = (LRBs_inj (subst_value_name_letrec_binding_list e5 x5 letrec_binding_list))" "subst_value_name_let_binding e5 x5 (LB_simple pattern expr) = (LB_simple pattern (subst_value_name_expr e5 x5 expr))" "subst_value_name_pat_exp e5 x5 (PE_inj pattern expr) = (PE_inj pattern (if x5 mem (aux_xs_pattern_of_pattern pattern) then expr else (subst_value_name_expr e5 x5 expr)))" "subst_value_name_pat_exp_list e5 x5 Nil = (Nil)" "subst_value_name_pat_exp_list e5 x5 (pat_exp_XXX#pat_exp_list_XXX) = ((subst_value_name_pat_exp e5 x5 pat_exp_XXX) # (subst_value_name_pat_exp_list e5 x5 pat_exp_list_XXX))" "subst_value_name_pattern_matching e5 x5 (PM_pm (pat_exp_list)) = (PM_pm (subst_value_name_pat_exp_list e5 x5 pat_exp_list))" "subst_value_name_field_expr_Expr_override e5 x5 (field1,expr1) = (field1 , subst_value_name_expr e5 x5 expr1)" "subst_value_name_field_expr_list_Expr_override e5 x5 Nil = (Nil)" "subst_value_name_field_expr_list_Expr_override e5 x5 (field_expr_XXX#field_expr_list_XXX) = ((subst_value_name_field_expr_Expr_override e5 x5 field_expr_XXX) # (subst_value_name_field_expr_list_Expr_override e5 x5 field_expr_list_XXX))" "subst_value_name_field_expr_Expr_record e5 x5 (field1,expr1) = (field1 , subst_value_name_expr e5 x5 expr1)" "subst_value_name_field_expr_list_Expr_record e5 x5 Nil = (Nil)" "subst_value_name_field_expr_list_Expr_record e5 x5 (field_expr_XXX#field_expr_list_XXX) = ((subst_value_name_field_expr_Expr_record e5 x5 field_expr_XXX) # (subst_value_name_field_expr_list_Expr_record e5 x5 field_expr_list_XXX))" "subst_value_name_expr_list_Expr_construct e5 x5 Nil = (Nil)" "subst_value_name_expr_list_Expr_construct e5 x5 (expr_XXX#expr_list_XXX) = ((subst_value_name_expr e5 x5 expr_XXX) # (subst_value_name_expr_list_Expr_construct e5 x5 expr_list_XXX))" "subst_value_name_expr_list_Expr_tuple e5 x5 Nil = (Nil)" "subst_value_name_expr_list_Expr_tuple e5 x5 (expr_XXX#expr_list_XXX) = ((subst_value_name_expr e5 x5 expr_XXX) # (subst_value_name_expr_list_Expr_tuple e5 x5 expr_list_XXX))" "subst_value_name_expr e5 x5 (Expr_uprim unary_prim) = (Expr_uprim unary_prim)" "subst_value_name_expr e5 x5 (Expr_bprim binary_prim) = (Expr_bprim binary_prim)" "subst_value_name_expr e5 x5 (Expr_ident value_name) = ((if value_name=x5 then e5 else (Expr_ident value_name)))" "subst_value_name_expr e5 x5 (Expr_constant constant) = (Expr_constant constant)" "subst_value_name_expr e5 x5 (Expr_typed expr typexpr) = (Expr_typed (subst_value_name_expr e5 x5 expr) typexpr)" "subst_value_name_expr e5 x5 (Expr_tuple (expr_list)) = (Expr_tuple (subst_value_name_expr_list_Expr_tuple e5 x5 expr_list))" "subst_value_name_expr e5 x5 (Expr_construct constr (expr_list)) = (Expr_construct constr (subst_value_name_expr_list_Expr_construct e5 x5 expr_list))" "subst_value_name_expr e5 x5 (Expr_cons expr1 expr2) = (Expr_cons (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2))" "subst_value_name_expr e5 x5 (Expr_record (field_expr_list)) = (Expr_record (subst_value_name_field_expr_list_Expr_record e5 x5 field_expr_list))" "subst_value_name_expr e5 x5 (Expr_override expr (field_expr_list)) = (Expr_override (subst_value_name_expr e5 x5 expr) (subst_value_name_field_expr_list_Expr_override e5 x5 field_expr_list))" "subst_value_name_expr e5 x5 (Expr_apply expr1 expr2) = (Expr_apply (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2))" "subst_value_name_expr e5 x5 (Expr_and expr1 expr2) = (Expr_and (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2))" "subst_value_name_expr e5 x5 (Expr_or expr1 expr2) = (Expr_or (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2))" "subst_value_name_expr e5 x5 (Expr_field expr field) = (Expr_field (subst_value_name_expr e5 x5 expr) field)" "subst_value_name_expr e5 x5 (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))" "subst_value_name_expr e5 x5 (Expr_while expr1 expr2) = (Expr_while (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2))" "subst_value_name_expr e5 x5 (Expr_for x expr1 for_dirn expr2 expr3) = (Expr_for x (subst_value_name_expr e5 x5 expr1) for_dirn (subst_value_name_expr e5 x5 expr2) (if x5 mem [x] then expr3 else (subst_value_name_expr e5 x5 expr3)))" "subst_value_name_expr e5 x5 (Expr_sequence expr1 expr2) = (Expr_sequence (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2))" "subst_value_name_expr e5 x5 (Expr_match expr pattern_matching) = (Expr_match (subst_value_name_expr e5 x5 expr) (subst_value_name_pattern_matching e5 x5 pattern_matching))" "subst_value_name_expr e5 x5 (Expr_function pattern_matching) = (Expr_function (subst_value_name_pattern_matching e5 x5 pattern_matching))" "subst_value_name_expr e5 x5 (Expr_try expr pattern_matching) = (Expr_try (subst_value_name_expr e5 x5 expr) (subst_value_name_pattern_matching e5 x5 pattern_matching))" "subst_value_name_expr e5 x5 (Expr_let let_binding expr) = (Expr_let (subst_value_name_let_binding e5 x5 let_binding) (if x5 mem (aux_xs_let_binding_of_let_binding let_binding) then expr else (subst_value_name_expr e5 x5 expr)))" "subst_value_name_expr e5 x5 (Expr_letrec letrec_bindings expr) = (Expr_letrec (if x5 mem (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings) then letrec_bindings else (subst_value_name_letrec_bindings e5 x5 letrec_bindings)) (if x5 mem (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings) then expr else (subst_value_name_expr e5 x5 expr)))" "subst_value_name_expr e5 x5 (Expr_assert expr) = (Expr_assert (subst_value_name_expr e5 x5 expr))" "subst_value_name_expr e5 x5 (Expr_location location) = (Expr_location location)" consts substs_typevar_value_name_expr :: "(typevar*typexpr) list => (value_name*expr) => (value_name*expr)" primrec "substs_typevar_value_name_expr sub (value_name1,expr1) = (value_name1 , substs_typevar_expr sub expr1)" consts substs_typevar_caml_definition :: "(typevar*typexpr) list => caml_definition => caml_definition" primrec "substs_typevar_caml_definition sub (D_let let_binding) = (D_let (substs_typevar_let_binding sub let_binding))" "substs_typevar_caml_definition sub (D_letrec letrec_bindings) = (D_letrec (substs_typevar_letrec_bindings sub letrec_bindings))" "substs_typevar_caml_definition sub (D_type caml_type_definition) = (D_type (substs_typevar_caml_type_definition sub caml_type_definition))" "substs_typevar_caml_definition sub (D_exception exception_definition) = (D_exception (substs_typevar_exception_definition sub exception_definition))" consts substs_value_name_value_name_expr :: "(value_name*expr) list => (value_name*expr) => (value_name*expr)" primrec "substs_value_name_value_name_expr sub (value_name1,expr1) = (value_name1 , substs_value_name_expr sub expr1)" consts substs_value_name_caml_definition :: "(value_name*expr) list => caml_definition => caml_definition" primrec "substs_value_name_caml_definition sub (D_let let_binding) = (D_let (substs_value_name_let_binding sub let_binding))" "substs_value_name_caml_definition sub (D_letrec letrec_bindings) = (D_letrec (substs_value_name_letrec_bindings (List.filter (%(x5,e5).Not(x5 mem (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings))) sub) letrec_bindings))" "substs_value_name_caml_definition sub (D_type caml_type_definition) = (D_type caml_type_definition)" "substs_value_name_caml_definition sub (D_exception exception_definition) = (D_exception exception_definition)" consts subst_value_name_value_name_expr :: "expr => value_name => (value_name*expr) => (value_name*expr)" primrec "subst_value_name_value_name_expr e5 x5 (value_name1,expr1) = (value_name1 , subst_value_name_expr e5 x5 expr1)" consts subst_value_name_caml_definition :: "expr => value_name => caml_definition => caml_definition" primrec "subst_value_name_caml_definition e5 x5 (D_let let_binding) = (D_let (subst_value_name_let_binding e5 x5 let_binding))" "subst_value_name_caml_definition e5 x5 (D_letrec letrec_bindings) = (D_letrec (if x5 mem (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings) then letrec_bindings else (subst_value_name_letrec_bindings e5 x5 letrec_bindings)))" "subst_value_name_caml_definition e5 x5 (D_type caml_type_definition) = (D_type caml_type_definition)" "subst_value_name_caml_definition e5 x5 (D_exception exception_definition) = (D_exception exception_definition)" consts substs_typevar_value_name_expr_list :: "(typevar*typexpr) list => (value_name*expr) list => (value_name*expr) list" primrec "substs_typevar_value_name_expr_list sub Nil = (Nil)" "substs_typevar_value_name_expr_list sub (value_name_expr_XXX#value_name_expr_list_XXX) = ((substs_typevar_value_name_expr sub value_name_expr_XXX) # (substs_typevar_value_name_expr_list sub value_name_expr_list_XXX))" consts substs_typevar_definitions :: "(typevar*typexpr) list => definitions => definitions" primrec "substs_typevar_definitions sub Ds_nil = (Ds_nil )" "substs_typevar_definitions sub (Ds_cons caml_definition definitions) = (Ds_cons (substs_typevar_caml_definition sub caml_definition) (substs_typevar_definitions sub definitions))" consts substs_typevar_typescheme :: "(typevar*typexpr) list => typescheme => typescheme" primrec "substs_typevar_typescheme sub (TS_forall typexpr) = (TS_forall (substs_typevar_typexpr sub typexpr))" consts substs_typevar_typexprs :: "(typevar*typexpr) list => typexprs => typexprs" primrec "substs_typevar_typexprs sub (typexprs_inj (typexpr_list)) = (typexprs_inj (substs_typevar_typexpr_list sub typexpr_list))" consts substs_value_name_value_name_expr_list :: "(value_name*expr) list => (value_name*expr) list => (value_name*expr) list" primrec "substs_value_name_value_name_expr_list sub Nil = (Nil)" "substs_value_name_value_name_expr_list sub (value_name_expr_XXX#value_name_expr_list_XXX) = ((substs_value_name_value_name_expr sub value_name_expr_XXX) # (substs_value_name_value_name_expr_list sub value_name_expr_list_XXX))" consts substs_value_name_definitions :: "(value_name*expr) list => definitions => definitions" primrec "substs_value_name_definitions sub Ds_nil = (Ds_nil )" "substs_value_name_definitions sub (Ds_cons caml_definition definitions) = (Ds_cons (substs_value_name_caml_definition sub caml_definition) (substs_value_name_definitions (List.filter (%(x5,e5).Not(x5 mem (aux_xs_caml_definition_of_caml_definition caml_definition))) sub) definitions))" consts subst_value_name_value_name_expr_list :: "expr => value_name => (value_name*expr) list => (value_name*expr) list" primrec "subst_value_name_value_name_expr_list e5 x5 Nil = (Nil)" "subst_value_name_value_name_expr_list e5 x5 (value_name_expr_XXX#value_name_expr_list_XXX) = ((subst_value_name_value_name_expr e5 x5 value_name_expr_XXX) # (subst_value_name_value_name_expr_list e5 x5 value_name_expr_list_XXX))" consts subst_value_name_definitions :: "expr => value_name => definitions => definitions" primrec "subst_value_name_definitions e5 x5 Ds_nil = (Ds_nil )" "subst_value_name_definitions e5 x5 (Ds_cons caml_definition definitions) = (Ds_cons (subst_value_name_caml_definition e5 x5 caml_definition) (if x5 mem (aux_xs_caml_definition_of_caml_definition caml_definition) then definitions else (subst_value_name_definitions e5 x5 definitions)))" consts substs_typevar_substs_x :: "(typevar*typexpr) list => substs_x => substs_x" primrec "substs_typevar_substs_x sub (substs_x_xs (value_name_expr_list)) = (substs_x_xs (substs_typevar_value_name_expr_list sub value_name_expr_list))" consts substs_typevar_program :: "(typevar*typexpr) list => program => program" primrec "substs_typevar_program sub (Prog_defs definitions) = (Prog_defs (substs_typevar_definitions sub definitions))" "substs_typevar_program sub (Prog_raise expr) = (Prog_raise (substs_typevar_expr sub expr))" consts substs_typevar_environment_binding :: "(typevar*typexpr) list => environment_binding => environment_binding" primrec "substs_typevar_environment_binding sub EB_tv = (EB_tv )" "substs_typevar_environment_binding sub (EB_vn value_name typescheme) = (EB_vn value_name (substs_typevar_typescheme sub typescheme))" "substs_typevar_environment_binding sub (EB_cc constr_name typeconstr) = (EB_cc constr_name typeconstr)" "substs_typevar_environment_binding sub (EB_pc constr_name type_params_opt typexprs typeconstr) = (EB_pc constr_name type_params_opt (substs_typevar_typexprs (List.filter (%(tv5,t5).Not(tv5 mem (aux_typevars_type_params_opt_of_type_params_opt type_params_opt))) sub) typexprs) typeconstr)" "substs_typevar_environment_binding sub (EB_fn field_name type_params_opt typeconstr_name typexpr) = (EB_fn field_name type_params_opt typeconstr_name (substs_typevar_typexpr (List.filter (%(tv5,t5).Not(tv5 mem (aux_typevars_type_params_opt_of_type_params_opt type_params_opt))) sub) typexpr))" "substs_typevar_environment_binding sub (EB_td typeconstr_name kind) = (EB_td typeconstr_name kind)" "substs_typevar_environment_binding sub (EB_tr typeconstr_name kind (field_name_list)) = (EB_tr typeconstr_name kind field_name_list)" "substs_typevar_environment_binding sub (EB_ta type_params_opt typeconstr_name typexpr) = (EB_ta type_params_opt typeconstr_name (substs_typevar_typexpr (List.filter (%(tv5,t5).Not(tv5 mem (aux_typevars_type_params_opt_of_type_params_opt type_params_opt))) sub) typexpr))" "substs_typevar_environment_binding sub (EB_l location typexpr) = (EB_l location (substs_typevar_typexpr sub typexpr))" consts substs_typevar_trans_label :: "(typevar*typexpr) list => trans_label => trans_label" primrec "substs_typevar_trans_label sub Lab_nil = (Lab_nil )" "substs_typevar_trans_label sub (Lab_alloc v location) = (Lab_alloc v location)" "substs_typevar_trans_label sub (Lab_deref location v) = (Lab_deref location v)" "substs_typevar_trans_label sub (Lab_assign location v) = (Lab_assign location v)" consts substs_value_name_substs_x :: "(value_name*expr) list => substs_x => substs_x" primrec "substs_value_name_substs_x sub (substs_x_xs (value_name_expr_list)) = (substs_x_xs (substs_value_name_value_name_expr_list sub value_name_expr_list))" consts substs_value_name_program :: "(value_name*expr) list => program => program" primrec "substs_value_name_program sub (Prog_defs definitions) = (Prog_defs (substs_value_name_definitions sub definitions))" "substs_value_name_program sub (Prog_raise expr) = (Prog_raise (substs_value_name_expr sub expr))" consts substs_value_name_trans_label :: "(value_name*expr) list => trans_label => trans_label" primrec "substs_value_name_trans_label sub Lab_nil = (Lab_nil )" "substs_value_name_trans_label sub (Lab_alloc v location) = (Lab_alloc v location)" "substs_value_name_trans_label sub (Lab_deref location v) = (Lab_deref location v)" "substs_value_name_trans_label sub (Lab_assign location v) = (Lab_assign location v)" consts subst_value_name_substs_x :: "expr => value_name => substs_x => substs_x" primrec "subst_value_name_substs_x e5 x5 (substs_x_xs (value_name_expr_list)) = (substs_x_xs (subst_value_name_value_name_expr_list e5 x5 value_name_expr_list))" consts subst_value_name_program :: "expr => value_name => program => program" primrec "subst_value_name_program e5 x5 (Prog_defs definitions) = (Prog_defs (subst_value_name_definitions e5 x5 definitions))" "subst_value_name_program e5 x5 (Prog_raise expr) = (Prog_raise (subst_value_name_expr e5 x5 expr))" consts subst_value_name_trans_label :: "expr => value_name => trans_label => trans_label" primrec "subst_value_name_trans_label e5 x5 Lab_nil = (Lab_nil )" "subst_value_name_trans_label e5 x5 (Lab_alloc v location) = (Lab_alloc v location)" "subst_value_name_trans_label e5 x5 (Lab_deref location v) = (Lab_deref location v)" "subst_value_name_trans_label e5 x5 (Lab_assign location v) = (Lab_assign location v)" constdefs fold_pat :: "pattern list => expr => expr" "fold_pat pats expr == foldr (% p e. Expr_function (PM_pm [PE_inj p e])) pats expr" consts shiftt :: "nat => nat => typexpr => typexpr" (* primrec "( (shiftt m n (TE_var typevar) ) = (TE_var typevar))" " ( (shiftt m n (TE_idxvar idx num) ) = (if ( idx < m ) then (TE_idxvar idx num) else (TE_idxvar ( idx + n ) num)) " " ( (shiftt m n TE_any ) = TE_any)) " " ( (shiftt m n (TE_arrow typexpr1 typexpr2) ) = (TE_arrow (shiftt m n typexpr1 ) (shiftt m n typexpr2 ) )) " " (shiftt m n (TE_tuple typexprs) = TE_tuple (map (shiftt m n) typexprs)) " " (shiftt m n (TE_constr typexprs tc) = TE_constr (map (shiftt m n) typexprs) tc)" FIXMEdoesn't like recursive call in last clause *) consts shifttes :: "nat => nat => typexprs => typexprs" (* primrec "(shifttes m n (typexprs_inj tes) == typexprs_inj (map (shiftt m n) tes))" FIXME doesn't like rec call *) consts shiftts :: "nat => nat => typescheme => typescheme" (* primrec "( (shiftts m n (TS_forall typexpr) ) = (TS_forall (shiftt ( m + 1 ) n typexpr ) ))" FIXME *) consts shiftEB :: "nat => nat => environment_binding => environment_binding" primrec "( (shiftEB m n EB_tv ) = EB_tv)" "( (shiftEB m n (EB_vn value_name typescheme) ) = (EB_vn value_name (shiftts m n typescheme ) ))" " ( (shiftEB m n (EB_cc constr_name typeconstr) ) = (EB_cc constr_name typeconstr)) " " ( (shiftEB m n (EB_pc constr_name type_params_opt typexprs typeconstr) ) = (EB_pc constr_name type_params_opt (shifttes m n typexprs ) typeconstr)) " " ( (shiftEB m n (EB_fn field_name type_params_opt typeconstr_name typexpr) ) = (EB_fn field_name type_params_opt typeconstr_name (shiftt m n typexpr ) )) " " ( (shiftEB m n (EB_td typeconstr_name kind) ) = (EB_td typeconstr_name kind)) " " (shiftEB m n (EB_tr tcn k field_names) = EB_tr tcn k field_names) " " ( (shiftEB m n (EB_ta type_params_opt typeconstr_name typexpr) ) = (EB_ta type_params_opt typeconstr_name (shiftt m n typexpr ) )) " " ( (shiftEB m n (EB_l location typexpr) ) = (EB_l location (shiftt m n typexpr ) ))" consts num_tv :: "environment => nat" primrec "(num_tv [] = (0::nat)) " "(num_tv (eb#e) = (if eb = EB_tv then 1 else 0) + num_tv e)" consts shiftE :: "nat => nat => environment => environment" primrec "(shiftE m n [] = []) " " (shiftE m n (EB#E) = shiftEB (m + num_tv E) n EB#shiftE m n E)" constdefs shiftTsig :: "nat => nat => ('a * typexpr) list => ('a * typexpr) list" "(shiftTsig m n Tsig == map (%(tv, t). (tv, shiftt m n t)) Tsig)" consts definitions_snoc :: "definitions => caml_definition => definitions" primrec "(definitions_snoc Ds_nil d = Ds_cons d Ds_nil) " "(definitions_snoc (Ds_cons d ds) d' = Ds_cons d (definitions_snoc ds d'))" consts remv_tyvar_typexpr :: "typexpr => typexpr" (* val _ = ottDefine "remv_tyvar_typexpr" `(remv_tyvar_typexpr (TE_var typevar) = TE_any) /\ (remv_tyvar_typexpr (TE_idxvar idx num) = TE_idxvar idx num) /\ (remv_tyvar_typexpr TE_any = TE_any) /\ (remv_tyvar_typexpr (TE_arrow typexpr1 typexpr2) = TE_arrow (remv_tyvar_typexpr typexpr1) (remv_tyvar_typexpr typexpr2)) /\ (remv_tyvar_typexpr (TE_tuple (typexpr_list)) = TE_tuple (MAP (\typexpr_. (remv_tyvar_typexpr typexpr_)) typexpr_list)) /\ (remv_tyvar_typexpr (TE_constr (typexpr_list) typeconstr) = TE_constr (MAP (\typexpr_. (remv_tyvar_typexpr typexpr_)) typexpr_list) typeconstr)`; *) consts remv_tyvar_pattern :: "pattern => pattern" (* `(remv_tyvar_pattern (P_var value_name) = P_var value_name) /\ (remv_tyvar_pattern P_any = P_any) /\ (remv_tyvar_pattern (P_constant constant) = P_constant constant) /\ (remv_tyvar_pattern (P_alias pattern value_name) = P_alias (remv_tyvar_pattern pattern) value_name) /\ (remv_tyvar_pattern (P_typed pattern typexpr) = P_typed (remv_tyvar_pattern pattern) (remv_tyvar_typexpr typexpr)) /\ (remv_tyvar_pattern (P_or pattern1 pattern2) = P_or (remv_tyvar_pattern pattern1) (remv_tyvar_pattern pattern2)) /\ (remv_tyvar_pattern (P_construct constr (pattern_list)) = P_construct constr (MAP (\pattern_. (remv_tyvar_pattern pattern_)) pattern_list)) /\ (remv_tyvar_pattern (P_construct_any constr) = P_construct_any constr) /\ (remv_tyvar_pattern (P_tuple (pattern_list)) = P_tuple (MAP (\pattern_. (remv_tyvar_pattern pattern_)) pattern_list)) /\ (remv_tyvar_pattern (P_record (field_pattern_list)) = P_record (MAP (\(field_,pattern_). (field_,(remv_tyvar_pattern pattern_))) field_pattern_list)) /\ (remv_tyvar_pattern (P_cons pattern1 pattern2) = P_cons (remv_tyvar_pattern pattern1) (remv_tyvar_pattern pattern2))`; *) consts remv_tyvar_letrec_binding :: "letrec_binding => letrec_binding" (* `(remv_tyvar_letrec_binding (LRB_simple value_name pattern_matching) = LRB_simple value_name (remv_tyvar_pattern_matching pattern_matching)) /\ (remv_tyvar_letrec_bindings (LRBs_inj (letrec_binding_list)) = LRBs_inj (MAP (\letrec_binding_. (remv_tyvar_letrec_binding letrec_binding_)) letrec_binding_list)) /\ (remv_tyvar_let_binding (LB_simple pattern expr) = LB_simple (remv_tyvar_pattern pattern) (remv_tyvar_expr expr)) /\ (remv_tyvar_pat_exp (PE_inj pattern expr) = PE_inj (remv_tyvar_pattern pattern) (remv_tyvar_expr expr)) /\ (remv_tyvar_pattern_matching (PM_pm (pat_exp_list)) = PM_pm (MAP (\pat_exp_. (remv_tyvar_pat_exp pat_exp_)) pat_exp_list)) /\ (remv_tyvar_expr (Expr_uprim unary_prim) = Expr_uprim unary_prim) /\ (remv_tyvar_expr (Expr_bprim binary_prim) = Expr_bprim binary_prim) /\ (remv_tyvar_expr (Expr_ident value_name) = Expr_ident value_name) /\ (remv_tyvar_expr (Expr_constant constant) = Expr_constant constant) /\ (remv_tyvar_expr (Expr_typed expr typexpr) = Expr_typed (remv_tyvar_expr expr) (remv_tyvar_typexpr typexpr)) /\ (remv_tyvar_expr (Expr_tuple (expr_list)) = Expr_tuple (MAP (\expr_. (remv_tyvar_expr expr_)) expr_list)) /\ (remv_tyvar_expr (Expr_construct constr (expr_list)) = Expr_construct constr (MAP (\expr_. (remv_tyvar_expr expr_)) expr_list)) /\ (remv_tyvar_expr (Expr_cons expr1 expr2) = Expr_cons (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\ (remv_tyvar_expr (Expr_record (field_expr_list)) = Expr_record (MAP (\(field_,expr_). (field_,(remv_tyvar_expr expr_))) field_expr_list)) /\ (remv_tyvar_expr (Expr_override expr (field_expr_list)) = Expr_override (remv_tyvar_expr expr) (MAP (\(field_,expr_). (field_,(remv_tyvar_expr expr_))) field_expr_list)) /\ (remv_tyvar_expr (Expr_apply expr1 expr2) = Expr_apply (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\ (remv_tyvar_expr (Expr_and expr1 expr2) = Expr_and (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\ (remv_tyvar_expr (Expr_or expr1 expr2) = Expr_or (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\ (remv_tyvar_expr (Expr_field expr field) = Expr_field (remv_tyvar_expr expr) field) /\ (remv_tyvar_expr (Expr_ifthenelse expr0 expr1 expr2) = Expr_ifthenelse (remv_tyvar_expr expr0) (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\ (remv_tyvar_expr (Expr_while expr1 expr2) = Expr_while (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\ (remv_tyvar_expr (Expr_for x expr1 for_dirn expr2 expr3) = Expr_for x (remv_tyvar_expr expr1) for_dirn (remv_tyvar_expr expr2) (remv_tyvar_expr expr3))/\ (remv_tyvar_expr (Expr_sequence expr1 expr2) = Expr_sequence (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\ (remv_tyvar_expr (Expr_match expr pattern_matching) = Expr_match (remv_tyvar_expr expr) (remv_tyvar_pattern_matching pattern_matching)) /\ (remv_tyvar_expr (Expr_function pattern_matching) = Expr_function (remv_tyvar_pattern_matching pattern_matching)) /\ (remv_tyvar_expr (Expr_try expr pattern_matching) = Expr_try (remv_tyvar_expr expr) (remv_tyvar_pattern_matching pattern_matching)) /\ (remv_tyvar_expr (Expr_let let_binding expr) = Expr_let (remv_tyvar_let_binding let_binding) (remv_tyvar_expr expr)) /\ (remv_tyvar_expr (Expr_letrec letrec_bindings expr) = Expr_letrec (remv_tyvar_letrec_bindings letrec_bindings) (remv_tyvar_expr expr)) /\ (remv_tyvar_expr (Expr_assert expr) = Expr_assert (remv_tyvar_expr expr)) /\ (remv_tyvar_expr (Expr_location location) = Expr_location location)`; *) (** definitions *) (*defns JdomEB *) consts JdomEB :: "(environment_binding*name) set" inductive JdomEB intros (* defn domEB *) JdomEB_type_paramI: " ( EB_tv , name_tv ) : JdomEB" JdomEB_value_nameI: " ( (EB_vn value_name typescheme) , (name_vn value_name) ) : JdomEB" JdomEB_const_constr_nameI: " ( (EB_cc constr_name typeconstr) , (name_cn constr_name) ) : JdomEB" JdomEB_constr_nameI: " ( (EB_pc constr_name type_params_opt (typexprs_inj (t_list)) typeconstr) , (name_cn constr_name) ) : JdomEB" JdomEB_opaque_typeconstr_nameI: " ( (EB_td typeconstr_name kind) , (name_tcn typeconstr_name) ) : JdomEB" JdomEB_trans_typeconstr_nameI: " ( (EB_ta type_params_opt typeconstr_name t) , (name_tcn typeconstr_name) ) : JdomEB" JdomEB_record_typeconstr_nameI: " ( (EB_tr typeconstr_name kind (field_name_list)) , (name_tcn typeconstr_name) ) : JdomEB" JdomEB_record_field_nameI: " ( (EB_fn field_name type_params_opt typeconstr_name typexpr) , (name_fn field_name) ) : JdomEB" JdomEB_locationI: " ( (EB_l location t) , (name_l location) ) : JdomEB" (*defns JdomE *) consts JdomE :: "(environment*names) set" inductive JdomE intros (* defn domE *) JdomE_emptyI: " ( [] , [] ) : JdomE" JdomE_consI: "[| ( E , (name_list) ) : JdomE ; ( EB , name ) : JdomEB|] ==> ( ( EB # E ) , ([(name)] @ name_list) ) : JdomE" (*defns Jlookup *) consts Jlookup_EB :: "(environment*name*environment_binding) set" inductive Jlookup_EB intros (* defn EB *) Jlookup_EB_rec1I: "[| ( EB , name' ) : JdomEB ; (~( name = name' )) ; (~( name' = name_tv )) ; ( E , name , EB' ) : Jlookup_EB|] ==> ( ( EB # E ) , name , EB' ) : Jlookup_EB" Jlookup_EB_rec2I: "[| (~( name = name_tv )) ; ( E , name , EB' ) : Jlookup_EB|] ==> ( ( EB_tv # E ) , name , (shiftEB 0 1 EB' ) ) : Jlookup_EB" Jlookup_EB_headI: "[| ( EB , name ) : JdomEB|] ==> ( ( EB # E ) , name , EB ) : Jlookup_EB" (*defns Jidx *) consts Jidx_bound :: "(environment*idx) set" inductive Jidx_bound intros (* defn bound *) Jidx_bound_skip1I: "[| ( E , idx ) : Jidx_bound ; ( EB , name ) : JdomEB ; (~( name = name_tv )) |] ==> ( ( EB # E ) , idx ) : Jidx_bound" Jidx_bound_skip2I: "[| ( E , idx ) : Jidx_bound|] ==> ( ( EB_tv # E ) , ( idx + 1 ) ) : Jidx_bound" Jidx_bound_foundI: " ( ( EB_tv # E ) , 0 ) : Jidx_bound" (*defns JTtps_kind *) consts JTtps_kind :: "(type_params_opt*kind) set" inductive JTtps_kind intros (* defn tps_kind *) JTtps_kind_kindI: "[| (distinct ( (tp_list) )) ; ( n = length ( (tp_list) )) |] ==> ( (TPS_nary (tp_list)) , n ) : JTtps_kind" (*defns JTEok *) consts JTEok :: "environment set" JTtypeconstr :: "(environment*typeconstr*kind) set" JTts :: "(environment*typescheme*kind) set" JTtsnamed :: "(environment*type_params_opt*typexpr*kind) set" JTt :: "(environment*typexpr*kind) set" inductive JTEok JTtypeconstr JTts JTtsnamed JTt intros (* defn Eok *) JTEok_emptyI: " ( [] ) : JTEok" JTEok_typevarI: "[| ( E ) : JTEok|] ==> ( ( EB_tv # E ) ) : JTEok" JTEok_value_nameI: "[| ( E , (TS_forall t) , 0 ) : JTts|] ==> ( ( (EB_vn value_name (TS_forall t)) # E ) ) : JTEok" JTEok_constr_name_cI: "[| ( E ) : JTEok ; ( E , (name_tcn typeconstr_name) , (EB_td typeconstr_name kind) ) : Jlookup_EB ; ( E , names ) : JdomE ; (~( (name_cn constr_name) mem names )) |] ==> ( ( (EB_cc constr_name (TC_name typeconstr_name)) # E ) ) : JTEok" JTEok_exn_constr_name_cI: "[| ( E ) : JTEok ; ( E , names ) : JdomE ; (~( (name_cn constr_name) mem names )) |] ==> ( ( (EB_cc constr_name TC_exn) # E ) ) : JTEok" JTEok_constr_name_pI: "[| ( type_params_opt = (TPS_nary ((List.map (%(tv_XXX::typevar).(TP_var tv_XXX)) tv_list))) ) ; (List.list_all (% b . b) ((List.map (%(t_XXX::typexpr). ( E , type_params_opt , t_XXX , 0 ) : JTtsnamed) t_list))) ; ( E , (name_tcn typeconstr_name) , (EB_td typeconstr_name m ) ) : Jlookup_EB ; ( E , names ) : JdomE ; (~( (name_cn constr_name) mem names )) ; (length ( (t_list) ) >= 1 ) ; ( m = length ( ((List.map (%(tv_XXX::typevar).(TP_var tv_XXX)) tv_list)) )) |] ==> ( ( (EB_pc constr_name (TPS_nary ((List.map (%(tv_XXX::typevar).(TP_var tv_XXX)) tv_list))) (typexprs_inj (t_list)) (TC_name typeconstr_name)) # E ) ) : JTEok" JTEok_exn_constr_name_pI: "[|(List.list_all (% b . b) ((List.map (%(t_XXX::typexpr). ( E , t_XXX , 0 ) : JTt) t_list))) ; ( E , names ) : JdomE ; (~( (name_cn constr_name) mem names )) ; (length ( (t_list) ) >= 1 ) |] ==> ( ( (EB_pc constr_name (TPS_nary []) (typexprs_inj (t_list)) TC_exn) # E ) ) : JTEok" JTEok_record_destrI: "[| ( E , (TPS_nary ((List.map (%(tv_XXX::typevar).(TP_var tv_XXX)) tv_list))) , t , 0 ) : JTtsnamed ; ( E , names ) : JdomE ; (~( (name_fn field_name) mem names )) ; ( E , (name_tcn typeconstr_name) , (EB_tr typeconstr_name m (field_name_list)) ) : Jlookup_EB ; ( m = length ( ((List.map (%(tv_XXX::typevar).(TP_var tv_XXX)) tv_list)) )) ; ( field_name mem (field_name_list) ) |] ==> ( ( (EB_fn field_name (TPS_nary ((List.map (%(tv_XXX::typevar).(TP_var tv_XXX)) tv_list))) typeconstr_name t) # E ) ) : JTEok" JTEok_typeconstr_nameI: "[| ( E ) : JTEok ; ( E , names ) : JdomE ; (~( (name_tcn typeconstr_name) mem names )) |] ==> ( ( (EB_td typeconstr_name kind) # E ) ) : JTEok" JTEok_typeconstr_eqnI: "[| ( E , names ) : JdomE ; (~( (name_tcn typeconstr_name) mem names )) ; ( E , (TPS_nary ((List.map (%(tv_XXX::typevar).(TP_var tv_XXX)) tv_list))) , t , 0 ) : JTtsnamed|] ==> ( ( (EB_ta (TPS_nary ((List.map (%(tv_XXX::typevar).(TP_var tv_XXX)) tv_list))) typeconstr_name t) # E ) ) : JTEok" JTEok_typeconstr_recordI: "[| ( E ) : JTEok ; ( E , names ) : JdomE ; (~( (name_tcn typeconstr_name) mem names )) ; (distinct ( ((List.map (%(field_name_XXX::field_name).(name_fn field_name_XXX)) field_name_list)) )) |] ==> ( ( (EB_tr typeconstr_name kind (field_name_list)) # E ) ) : JTEok" JTEok_locationI: "[| ( E , t , 0 ) : JTt ; ( E , names ) : JdomE ; (~( (name_l location) mem names )) |] ==> ( ( (EB_l location t) # E ) ) : JTEok" (* defn typeconstr *) JTtypeconstr_abstractI: "[| ( E ) : JTEok ; ( E , (name_tcn typeconstr_name) , (EB_td typeconstr_name kind) ) : Jlookup_EB|] ==> ( E , (TC_name typeconstr_name) , kind ) : JTtypeconstr" JTtypeconstr_concreteI: "[| ( E ) : JTEok ; ( E , (name_tcn typeconstr_name) , (EB_ta type_params_opt typeconstr_name t) ) : Jlookup_EB ; ( type_params_opt , kind ) : JTtps_kind|] ==> ( E , (TC_name typeconstr_name) , kind ) : JTtypeconstr" JTtypeconstr_recordI: "[| ( E ) : JTEok ; ( E , (name_tcn typeconstr_name) , (EB_tr typeconstr_name kind (field_name_list)) ) : Jlookup_EB|] ==> ( E , (TC_name typeconstr_name) , kind ) : JTtypeconstr" JTtypeconstr_intI: "[| ( E ) : JTEok|] ==> ( E , TC_int , 0 ) : JTtypeconstr" JTtypeconstr_charI: "[| ( E ) : JTEok|] ==> ( E , TC_char , 0 ) : JTtypeconstr" JTtypeconstr_stringI: "[| ( E ) : JTEok|] ==> ( E , TC_string , 0 ) : JTtypeconstr" JTtypeconstr_floatI: "[| ( E ) : JTEok|] ==> ( E , TC_float , 0 ) : JTtypeconstr" JTtypeconstr_boolI: "[| ( E ) : JTEok|] ==> ( E , TC_bool , 0 ) : JTtypeconstr" JTtypeconstr_unitI: "[| ( E ) : JTEok|] ==> ( E , TC_unit , 0 ) : JTtypeconstr" JTtypeconstr_exnI: "[| ( E ) : JTEok|] ==> ( E , TC_exn , 0 ) : JTtypeconstr" JTtypeconstr_listI: "[| ( E ) : JTEok|] ==> ( E , TC_list , 1 ) : JTtypeconstr" JTtypeconstr_optionI: "[| ( E ) : JTEok|] ==> ( E , TC_option , 1 ) : JTtypeconstr" JTtypeconstr_refI: "[| ( E ) : JTEok|] ==> ( E , TC_ref , 1 ) : JTtypeconstr" (* defn ts *) JTts_forallI: "[| ( ( EB_tv # E ) , t , 0 ) : JTt|] ==> ( E , (TS_forall t) , 0 ) : JTts" (* defn tsnamed *) JTtsnamed_forallI: "[| ( E , (substs_typevar_typexpr ((List.map (%(tv_XXX::typevar).(tv_XXX, (TE_constr [] TC_unit ) )) tv_list)) t ) , 0 ) : JTt ; (distinct ( ((List.map (%(tv_XXX::typevar).(TP_var tv_XXX)) tv_list)) )) |] ==> ( E , (TPS_nary ((List.map (%(tv_XXX::typevar).(TP_var tv_XXX)) tv_list))) , t , 0 ) : JTtsnamed" (* defn t *) JTt_varI: "[| ( E ) : JTEok ; ( E , idx ) : Jidx_bound|] ==> ( E , (TE_idxvar idx num) , 0 ) : JTt" JTt_arrowI: "[| ( E , t , 0 ) : JTt ; ( E , t' , 0 ) : JTt|] ==> ( E , (TE_arrow t t') , 0 ) : JTt" JTt_tupleI: "[|(List.list_all (% b . b) ((List.map (%(t_XXX::typexpr). ( E , t_XXX , 0 ) : JTt) t_list))) ; (length ( (t_list) ) >= 2 ) |] ==> ( E , (TE_tuple (t_list)) , 0 ) : JTt" JTt_constrI: "[| ( E , typeconstr , n ) : JTtypeconstr ; (List.list_all (% b . b) ((List.map (%(t_XXX::typexpr). ( E , t_XXX , 0 ) : JTt) t_list))) ; ( n = length ( (t_list) )) |] ==> ( E , (TE_constr (t_list) typeconstr) , 0 ) : JTt" (*defns JTeq *) consts JTeq :: "(environment*typexpr*typexpr) set" inductive JTeq intros (* defn eq *) JTeq_reflI: "[| ( E , t , 0 ) : JTt|] ==> ( E , t , t ) : JTeq" JTeq_symI: "[| ( E , t' , t ) : JTeq|] ==> ( E , t , t' ) : JTeq" JTeq_transI: "[| ( E , t , t' ) : JTeq ; ( E , t' , t'' ) : JTeq|] ==> ( E , t , t'' ) : JTeq" JTeq_expandI: "[| ( E ) : JTEok ; ( E , (name_tcn typeconstr_name) , (EB_ta (TPS_nary ((List.map (%((t_XXX::typexpr),(typevar_XXX::typevar)).(TP_var typevar_XXX)) t_typevar_list))) typeconstr_name t) ) : Jlookup_EB ; (List.list_all (% b . b) ((List.map (%((t_XXX::typexpr),(typevar_XXX::typevar)). ( E , t_XXX , 0 ) : JTt) t_typevar_list)))|] ==> ( E , (TE_constr ((List.map (%((t_XXX::typexpr),(typevar_XXX::typevar)).t_XXX) t_typevar_list)) (TC_name typeconstr_name)) , (substs_typevar_typexpr ((List.map (%((t_XXX::typexpr),(typevar_XXX::typevar)).(typevar_XXX,t_XXX)) t_typevar_list)) t ) ) : JTeq" JTeq_arrowI: "[| ( E , t1 , t1' ) : JTeq ; ( E , t2 , t2' ) : JTeq|] ==> ( E , (TE_arrow t1 t2) , (TE_arrow t1' t2') ) : JTeq" JTeq_tupleI: "[|(List.list_all (% b . b) ((List.map (%((t_XXX::typexpr),(t_'::typexpr)). ( E , t_XXX , t_' ) : JTeq) t_t'_list))) ; (length ( ((List.map (%((t_XXX::typexpr),(t_'::typexpr)).t_XXX) t_t'_list)) ) >= 2 ) |] ==> ( E , (TE_tuple ((List.map (%((t_XXX::typexpr),(t_'::typexpr)).t_XXX) t_t'_list))) , (TE_tuple ((List.map (%((t_XXX::typexpr),(t_'::typexpr)).t_') t_t'_list))) ) : JTeq" JTeq_constrI: "[| ( E , typeconstr , n ) : JTtypeconstr ; (List.list_all (% b . b) ((List.map (%((t_XXX::typexpr),(t_'::typexpr)). ( E , t_XXX , t_' ) : JTeq) t_t'_list))) ; ( n = length ( ((List.map (%((t_XXX::typexpr),(t_'::typexpr)).t_XXX) t_t'_list)) )) |] ==> ( E , (TE_constr ((List.map (%((t_XXX::typexpr),(t_'::typexpr)).t_XXX) t_t'_list)) typeconstr) , (TE_constr ((List.map (%((t_XXX::typexpr),(t_'::typexpr)).t_') t_t'_list)) typeconstr) ) : JTeq" (*defns JTidxsub *) consts JTidxsub :: "(typexpr list*typexpr*typexpr) set" inductive JTidxsub intros (* defn idxsub *) JTinxsub_alphaI: " ( (t_list) , (TE_var typevar) , (TE_var typevar) ) : JTidxsub" JTinxsub_idx0I: "[| ( num = length ( (t_list) )) |] ==> ( (t_list @ [(t')] @ t''_list) , (TE_idxvar 0 num) , t' ) : JTidxsub" JTinxsub_idx1I: "[| (length ( (t_list) ) <= num ) |] ==> ( (t_list) , (TE_idxvar 0 num) , (TE_constr [] TC_unit ) ) : JTidxsub" JTinxsub_idx2I: " ( (t_list) , (TE_idxvar ( idx + 1 ) num) , (TE_idxvar idx num) ) : JTidxsub" JTinxsub_anyI: " ( (t_list) , TE_any , TE_any ) : JTidxsub" JTinxsub_arrowI: "[| ( (t_list) , t1' , t1'' ) : JTidxsub ; ( (t_list) , t2' , t2'' ) : JTidxsub|] ==> ( (t_list) , (TE_arrow t1' t2') , (TE_arrow t1'' t2'') ) : JTidxsub" JTinxsub_tupleI: "[|(List.list_all (% b . b) ((List.map (%((t_'::typexpr),(t_''::typexpr)). ( (t_list) , t_' , t_'' ) : JTidxsub) t'_t''_list)))|] ==> ( (t_list) , (TE_tuple ((List.map (%((t_'::typexpr),(t_''::typexpr)).t_') t'_t''_list))) , (TE_tuple ((List.map (%((t_'::typexpr),(t_''::typexpr)).t_'') t'_t''_list))) ) : JTidxsub" JTinxsub_tcI: "[|(List.list_all (% b . b) ((List.map (%((t_'::typexpr),(t_''::typexpr)). ( (t_list) , t_' , t_'' ) : JTidxsub) t'_t''_list)))|] ==> ( (t_list) , (TE_constr ((List.map (%((t_'::typexpr),(t_''::typexpr)).t_') t'_t''_list)) typeconstr) , (TE_constr ((List.map (%((t_'::typexpr),(t_''::typexpr)).t_'') t'_t''_list)) typeconstr) ) : JTidxsub" (*defns JTinst *) consts JTinst :: "(environment*typexpr*typescheme) set" inductive JTinst intros (* defn inst *) JTinst_idxI: "[| ( E , (TS_forall t') , 0 ) : JTts ; (List.list_all (% b . b) ((List.map (%(t_XXX::typexpr). ( E , t_XXX , 0 ) : JTt) t_list))) ; ( (t_list) , t' , t'' ) : JTidxsub|] ==> ( E , t'' , (TS_forall t') ) : JTinst" (*defns JTinst_named *) consts JTinst_named :: "(environment*typexpr*type_params_opt*typexpr) set" inductive JTinst_named intros (* defn inst_named *) JTinst_named_namedI: "[| ( E , (TPS_nary ((List.map (%((typevar_XXX::typevar),(t_XXX::typexpr)).(TP_var typevar_XXX)) typevar_t_list))) , t , 0 ) : JTtsnamed ; (List.list_all (% b . b) ((List.map (%((typevar_XXX::typevar),(t_XXX::typexpr)). ( E , t_XXX , 0 ) : JTt) typevar_t_list)))|] ==> ( E , (substs_typevar_typexpr (typevar_t_list) t ) , (TPS_nary ((List.map (%((typevar_XXX::typevar),(t_XXX::typexpr)).(TP_var typevar_XXX)) typevar_t_list))) , t ) : JTinst_named" (*defns JTinst_any *) consts JTinst_any :: "(environment*typexpr*typexpr) set" inductive JTinst_any intros (* defn inst_any *) JTinst_any_tyvarI: "[| ( E , (TE_idxvar idx num) , 0 ) : JTt|] ==> ( E , (TE_idxvar idx num) , (TE_idxvar idx num) ) : JTinst_any" JTinst_any_anyI: "[| ( E , t , 0 ) : JTt|] ==> ( E , t , TE_any ) : JTinst_any" JTinst_any_arrowI: "[| ( E , t1 , t1' ) : JTinst_any ; ( E , t2 , t2' ) : JTinst_any|] ==> ( E , (TE_arrow t1 t2) , (TE_arrow t1' t2') ) : JTinst_any" JTinst_any_tupleI: "[|(List.list_all (% b . b) ((List.map (%((t_XXX::typexpr),(t_'::typexpr)). ( E , t_XXX , t_' ) : JTinst_any) t_t'_list))) ; (length ( ((List.map (%((t_XXX::typexpr),(t_'::typexpr)).t_XXX) t_t'_list)) ) >= 2 ) |] ==> ( E , (TE_tuple ((List.map (%((t_XXX::typexpr),(t_'::typexpr)).t_XXX) t_t'_list))) , (TE_tuple ((List.map (%((t_XXX::typexpr),(t_'::typexpr)).t_') t_t'_list))) ) : JTinst_any" JTinst_any_ctorI: "[|(List.list_all (% b . b) ((List.map (%((t_XXX::typexpr),(t_'::typexpr)). ( E , t_XXX , t_' ) : JTinst_any) t_t'_list))) ; ( E , typeconstr , n ) : JTtypeconstr ; ( n = length ( ((List.map (%((t_XXX::typexpr),(t_'::typexpr)).t_XXX) t_t'_list)) )) |] ==> ( E , (TE_constr ((List.map (%((t_XXX::typexpr),(t_'::typexpr)).t_XXX) t_t'_list)) typeconstr) , (TE_constr ((List.map (%((t_XXX::typexpr),(t_'::typexpr)).t_') t_t'_list)) typeconstr) ) : JTinst_any" (*defns JTval *) consts JTvalue_name :: "(environment*value_name*typexpr) set" inductive JTvalue_name intros (* defn value_name *) JTvalue_name_value_nameI: "[| ( E , (name_vn value_name) , (EB_vn value_name ts) ) : Jlookup_EB ; ( E , t , ts ) : JTinst|] ==> ( E , value_name , t ) : JTvalue_name" (*defns JTfield *) consts JTfield :: "(environment*field_name*typexpr*typexpr) set" inductive JTfield intros (* defn field *) JTfield_nameI: "[| ( E , (name_fn field_name) , (EB_fn field_name (TPS_nary ((List.map (%((t_'::typexpr),(tv_XXX::typevar)).(TP_var tv_XXX)) t'_tv_list))) typeconstr_name t) ) : Jlookup_EB ; ( E , (TE_arrow (TE_constr ((List.map (%((t_'::typexpr),(tv_XXX::typevar)).t_') t'_tv_list)) (TC_name typeconstr_name)) t'') , (TPS_nary ((List.map (%((t_'::typexpr),(tv_XXX::typevar)).(TP_var tv_XXX)) t'_tv_list))) , (TE_arrow (TE_constr ((List.map (%((t_'::typexpr),(tv_XXX::typevar)).(TE_var tv_XXX)) t'_tv_list)) (TC_name typeconstr_name)) t) ) : JTinst_named|] ==> ( E , field_name , (TE_constr ((List.map (%((t_'::typexpr),(tv_XXX::typevar)).t_') t'_tv_list)) (TC_name typeconstr_name)) , t'' ) : JTfield" (*defns JTconstr_p *) consts JTconstr_p :: "(environment*constr*typexpr list*typexpr) set" inductive JTconstr_p intros (* defn constr_p *) JTconstr_p_nameI: "[| ( E , (name_cn constr_name) , (EB_pc constr_name (TPS_nary ((List.map (%((t_''::typexpr),(tv_XXX::typevar)).(TP_var tv_XXX)) t''_tv_list))) (typexprs_inj ((List.map (%((t_'::typexpr),(t_XXX::typexpr)).t_XXX) t'_t_list))) typeconstr) ) : Jlookup_EB ; ( E , (TE_arrow (TE_tuple ((List.map (%((t_'::typexpr),(t_XXX::typexpr)).t_') t'_t_list))) (TE_constr ((List.map (%((t_''::typexpr),(tv_XXX::typevar)).t_'') t''_tv_list)) typeconstr)) , (TPS_nary ((List.map (%((t_''::typexpr),(tv_XXX::typevar)).(TP_var tv_XXX)) t''_tv_list))) , (TE_arrow (TE_tuple ((List.map (%((t_'::typexpr),(t_XXX::typexpr)).t_XXX) t'_t_list))) (TE_constr ((List.map (%((t_''::typexpr),(tv_XXX::typevar)).(TE_var tv_XXX)) t''_tv_list)) typeconstr)) ) : JTinst_named|] ==> ( E , (C_name constr_name) , ((List.map (%((t_'::typexpr),(t_XXX::typexpr)).t_') t'_t_list)) , (TE_constr ((List.map (%((t_''::typexpr),(tv_XXX::typevar)).t_'') t''_tv_list)) typeconstr) ) : JTconstr_p" JTconstr_p_invargI: "[| ( E ) : JTEok|] ==> ( E , C_invalidargument , ([( (TE_constr [] TC_string ) )]) , (TE_constr [] TC_exn ) ) : JTconstr_p" JTconstr_p_someI: "[| ( E , t , 0 ) : JTt|] ==> ( E , C_some , ([(t)]) , (TE_constr ([ t ]) TC_option ) ) : JTconstr_p" (*defns JTconstr_c *) consts JTconstr_c :: "(environment*constr*typexpr) set" inductive JTconstr_c intros (* defn constr_c *) JTconstr_c_constrI: "[| ( E ) : JTEok ; ( E , (name_cn constr_name) , (EB_cc constr_name (TC_name typeconstr_name)) ) : Jlookup_EB ; ( E , (name_tcn typeconstr_name) , (EB_td typeconstr_name n ) ) : Jlookup_EB ; (List.list_all (% b . b) ((List.map (%(t_XXX::typexpr). ( E , t_XXX , 0 ) : JTt) t_list))) ; ( n = length ( (t_list) )) |] ==> ( E , (C_name constr_name) , (TE_constr (t_list) (TC_name typeconstr_name)) ) : JTconstr_c" JTconstr_c_exn_constrI: "[| ( E ) : JTEok ; ( E , (name_cn constr_name) , (EB_cc constr_name TC_exn) ) : Jlookup_EB|] ==> ( E , (C_name constr_name) , (TE_constr [] TC_exn ) ) : JTconstr_c" JTconstr_c_notfoundI: "[| ( E ) : JTEok|] ==> ( E , C_notfound , (TE_constr [] TC_exn ) ) : JTconstr_c" JTconstr_c_assert_failI: "[| ( E ) : JTEok|] ==> ( E , C_assertfailure , (TE_constr [] TC_exn ) ) : JTconstr_c" JTconstr_c_match_failI: "[| ( E ) : JTEok|] ==> ( E , C_matchfailure , (TE_constr [] TC_exn ) ) : JTconstr_c" JTconstr_c_div_by_0I: "[| ( E ) : JTEok|] ==> ( E , C_div_by_0 , (TE_constr [] TC_exn ) ) : JTconstr_c" JTconstr_c_noneI: "[| ( E , t , 0 ) : JTt|] ==> ( E , C_none , (TE_constr ([ t ]) TC_option ) ) : JTconstr_c" (*defns JTconst *) consts JTconst :: "(environment*constant*typexpr) set" inductive JTconst intros (* defn const *) JTconst_intI: "[| ( E ) : JTEok|] ==> ( E , (CONST_int ( integer_literal ) ) , (TE_constr [] TC_int ) ) : JTconst" JTconst_floatI: "[| ( E ) : JTEok|] ==> ( E , (CONST_float float_literal) , (TE_constr [] TC_float ) ) : JTconst" JTconst_charI: "[| ( E ) : JTEok|] ==> ( E , (CONST_char char_literal) , (TE_constr [] TC_char ) ) : JTconst" JTconst_stringI: "[| ( E ) : JTEok|] ==> ( E , (CONST_string string_literal) , (TE_constr [] TC_string ) ) : JTconst" JTconst_constrI: "[| ( E , constr , t ) : JTconstr_c|] ==> ( E , (CONST_constr constr) , t ) : JTconst" JTconst_falseI: "[| ( E ) : JTEok|] ==> ( E , CONST_false , (TE_constr [] TC_bool ) ) : JTconst" JTconst_trueI: "[| ( E ) : JTEok|] ==> ( E , CONST_true , (TE_constr [] TC_bool ) ) : JTconst" JTconst_unitI: "[| ( E ) : JTEok|] ==> ( E , CONST_unit , (TE_constr [] TC_unit ) ) : JTconst" JTconst_nilI: "[| ( E , t , 0 ) : JTt|] ==> ( E , CONST_nil , (TE_constr ([ t ]) TC_list ) ) : JTconst" (*defns JTpat *) consts JTpat :: "(Tsigma*environment*pattern*typexpr*environment) set" inductive JTpat intros (* defn pat *) JTpat_varI: "[| ( E , t , 0 ) : JTt|] ==> ( Tsigma , E , (P_var x) , t , ( (EB_vn x (TS_forall (shiftt 0 1 t ))) # [] ) ) : JTpat" JTpat_anyI: "[| ( E , t , 0 ) : JTt|] ==> ( Tsigma , E , P_any , t , [] ) : JTpat" JTpat_constantI: "[| ( E , constant , t ) : JTconst|] ==> ( Tsigma , E , (P_constant constant) , t , [] ) : JTpat" JTpat_aliasI: "[| ( Tsigma , E , pattern , t , E' ) : JTpat ; ( ( (EB_vn x (TS_forall (shiftt 0 1 t ))) # E' ) , (name_list) ) : JdomE ; (distinct ( (name_list) )) |] ==> ( Tsigma , E , (P_alias pattern x) , t , ( (EB_vn x (TS_forall (shiftt 0 1 t ))) # E' ) ) : JTpat" JTpat_typedI: "[|is_src_typexpr_of_typexpr src_t ; ( Tsigma , E , pattern , t , E' ) : JTpat ; ( E , t' , (substs_typevar_typexpr Tsigma src_t ) ) : JTinst_any ; ( E , t , t' ) : JTeq|] ==> ( Tsigma , E , (P_typed pattern src_t) , t , E' ) : JTpat" JTpat_orI: "[| ( Tsigma , E , pattern , t , E' ) : JTpat ; ( Tsigma , E , pattern' , t , E'' ) : JTpat ; (perm ( E' ) ( E'' )) |] ==> ( Tsigma , E , (P_or pattern pattern') , t , E' ) : JTpat" JTpat_constructI: "[| ( E , constr , ((List.map (%((pattern_XXX::pattern),(E_XXX::environment),(t_XXX::typexpr)).t_XXX) pattern_E_t_list)) , t ) : JTconstr_p ; (List.list_all (% b . b) ((List.map (%((pattern_XXX::pattern),(E_XXX::environment),(t_XXX::typexpr)). ( Tsigma , E , pattern_XXX , t_XXX , E_XXX ) : JTpat) pattern_E_t_list))) ; ( (concat (rev ((List.map (%((pattern_XXX::pattern),(E_XXX::environment),(t_XXX::typexpr)).E_XXX) pattern_E_t_list)) )) , (name_list) ) : JdomE ; (distinct ( (name_list) )) |] ==> ( Tsigma , E , (P_construct constr ((List.map (%((pattern_XXX::pattern),(E_XXX::environment),(t_XXX::typexpr)).pattern_XXX) pattern_E_t_list))) , t , (concat (rev ((List.map (%((pattern_XXX::pattern),(E_XXX::environment),(t_XXX::typexpr)).E_XXX) pattern_E_t_list)) )) ) : JTpat" JTpat_construct_anyI: "[| ( E , constr , (t_list) , t ) : JTconstr_p|] ==> ( Tsigma , E , (P_construct_any constr) , t , [] ) : JTpat" JTpat_tupleI: "[|(List.list_all (% b . b) ((List.map (%((pattern_XXX::pattern),(t_XXX::typexpr),(E_XXX::environment)). ( Tsigma , E , pattern_XXX , t_XXX , E_XXX ) : JTpat) pattern_t_E_list))) ; (length ( ((List.map (%((pattern_XXX::pattern),(t_XXX::typexpr),(E_XXX::environment)).pattern_XXX) pattern_t_E_list)) ) >= 2 ) ; ( (concat (rev ((List.map (%((pattern_XXX::pattern),(t_XXX::typexpr),(E_XXX::environment)).E_XXX) pattern_t_E_list)) )) , (name_list) ) : JdomE ; (distinct ( (name_list) )) |] ==> ( Tsigma , E , (P_tuple ((List.map (%((pattern_XXX::pattern),(t_XXX::typexpr),(E_XXX::environment)).pattern_XXX) pattern_t_E_list))) , (TE_tuple ((List.map (%((pattern_XXX::pattern),(t_XXX::typexpr),(E_XXX::environment)).t_XXX) pattern_t_E_list))) , (concat (rev ((List.map (%((pattern_XXX::pattern),(t_XXX::typexpr),(E_XXX::environment)).E_XXX) pattern_t_E_list)) )) ) : JTpat" JTpat_recordI: "[|(List.list_all (% b . b) ((List.map (%((field_name_XXX::field_name),(pattern_XXX::pattern),(E_XXX::environment),(t_XXX::typexpr)). ( Tsigma , E , pattern_XXX , t_XXX , E_XXX ) : JTpat) field_name_pattern_E_t_list))) ; (List.list_all (% b . b) ((List.map (%((field_name_XXX::field_name),(pattern_XXX::pattern),(E_XXX::environment),(t_XXX::typexpr)). ( E , field_name_XXX , t , t_XXX ) : JTfield) field_name_pattern_E_t_list))) ; (length ( ((List.map (%((field_name_XXX::field_name),(pattern_XXX::pattern),(E_XXX::environment),(t_XXX::typexpr)).pattern_XXX) field_name_pattern_E_t_list)) ) >= 1 ) ; ( (concat (rev ((List.map (%((field_name_XXX::field_name),(pattern_XXX::pattern),(E_XXX::environment),(t_XXX::typexpr)).E_XXX) field_name_pattern_E_t_list)) )) , (name_list) ) : JdomE ; (distinct ( (name_list) )) |] ==> ( Tsigma , E , (P_record ((List.map (%((field_name_XXX::field_name),(pattern_XXX::pattern),(E_XXX::environment),(t_XXX::typexpr)).((F_name field_name_XXX),pattern_XXX)) field_name_pattern_E_t_list))) , t , (concat (rev ((List.map (%((field_name_XXX::field_name),(pattern_XXX::pattern),(E_XXX::environment),(t_XXX::typexpr)).E_XXX) field_name_pattern_E_t_list)) )) ) : JTpat" JTpat_consI: "[| ( Tsigma , E , pattern , t , E' ) : JTpat ; ( Tsigma , E , pattern' , (TE_constr ([ t ]) TC_list ) , E'' ) : JTpat ; ( E' , (name_list) ) : JdomE ; ( E'' , (name'_list) ) : JdomE ; (distinct ( (name_list @ name'_list) )) |] ==> ( Tsigma , E , (P_cons pattern pattern') , (TE_constr ([ t ]) TC_list ) , (concat (rev ([(E')] @ [(E'')]) )) ) : JTpat" (*defns JTuprim *) consts JTuprim :: "(environment*unary_prim*typexpr) set" inductive JTuprim intros (* defn uprim *) JTuprim_raiseI: "[| ( E , t , 0 ) : JTt|] ==> ( E , Uprim_raise , (TE_arrow (TE_constr [] TC_exn ) t) ) : JTuprim" JTuprim_notI: "[| ( E ) : JTEok|] ==> ( E , Uprim_not , (TE_arrow (TE_constr [] TC_bool ) (TE_constr [] TC_bool ) ) ) : JTuprim" JTuprim_uminusI: "[| ( E ) : JTEok|] ==> ( E , Uprim_minus , (TE_arrow (TE_constr [] TC_int ) (TE_constr [] TC_int ) ) ) : JTuprim" JTuprim_refI: "[| ( E , t , 0 ) : JTt|] ==> ( E , Uprim_ref , (TE_arrow t (TE_constr ([ t ]) TC_ref ) ) ) : JTuprim" JTuprim_derefI: "[| ( E , t , 0 ) : JTt|] ==> ( E , Uprim_deref , (TE_arrow (TE_constr ([ t ]) TC_ref ) t) ) : JTuprim" (*defns JTbprim *) consts JTbprim :: "(environment*binary_prim*typexpr) set" inductive JTbprim intros (* defn bprim *) JTbprim_equalI: "[| ( E , t , 0 ) : JTt|] ==> ( E , Bprim_equal , (TE_arrow t (TE_arrow t (TE_constr [] TC_bool ) ) ) ) : JTbprim" JTbprim_plusI: "[| ( E ) : JTEok|] ==> ( E , Bprim_plus , (TE_arrow (TE_constr [] TC_int ) (TE_arrow (TE_constr [] TC_int ) (TE_constr [] TC_int ) ) ) ) : JTbprim" JTbprim_minusI: "[| ( E ) : JTEok|] ==> ( E , Bprim_minus , (TE_arrow (TE_constr [] TC_int ) (TE_arrow (TE_constr [] TC_int ) (TE_constr [] TC_int ) ) ) ) : JTbprim" JTbprim_timesI: "[| ( E ) : JTEok|] ==> ( E , Bprim_times , (TE_arrow (TE_constr [] TC_int ) (TE_arrow (TE_constr [] TC_int ) (TE_constr [] TC_int ) ) ) ) : JTbprim" JTbprim_divI: "[| ( E ) : JTEok|] ==> ( E , Bprim_div , (TE_arrow (TE_constr [] TC_int ) (TE_arrow (TE_constr [] TC_int ) (TE_constr [] TC_int ) ) ) ) : JTbprim" JTbprim_assignI: "[| ( E , t , 0 ) : JTt|] ==> ( E , Bprim_assign , (TE_arrow (TE_constr ([ t ]) TC_ref ) (TE_arrow t (TE_constr [] TC_unit ) ) ) ) : JTbprim" (*defns JTe *) consts JTe :: "(Tsigma*environment*expr*typexpr) set" JTpat_matching :: "(Tsigma*environment*pattern_matching*typexpr*typexpr) set" JTlet_binding :: "(Tsigma*environment*let_binding*environment) set" JTletrec_binding :: "(Tsigma*environment*letrec_bindings*environment) set" inductive JTe JTpat_matching JTlet_binding JTletrec_binding intros (* defn e *) JTe_uprimI: "[| ( E , unary_prim , t ) : JTuprim ; ( E , t , t' ) : JTeq|] ==> ( Tsigma , E , (Expr_uprim unary_prim) , t' ) : JTe" JTe_bprimI: "[| ( E , binary_prim , t ) : JTbprim ; ( E , t , t' ) : JTeq|] ==> ( Tsigma , E , (Expr_bprim binary_prim) , t' ) : JTe" JTe_identI: "[| ( E , value_name , t ) : JTvalue_name ; ( E , t , t' ) : JTeq|] ==> ( Tsigma , E , (Expr_ident value_name) , t' ) : JTe" JTe_constantI: "[| ( E , constant , t ) : JTconst ; ( E , t , t' ) : JTeq|] ==> ( Tsigma , E , (Expr_constant constant) , t' ) : JTe" JTe_typedI: "[|is_src_typexpr_of_typexpr src_t ; ( Tsigma , E , e , t ) : JTe ; ( E , t' , (substs_typevar_typexpr Tsigma src_t ) ) : JTinst_any ; ( E , t , t' ) : JTeq|] ==> ( Tsigma , E , (Expr_typed e src_t) , t ) : JTe" JTe_tupleI: "[|(List.list_all (% b . b) ((List.map (%((e_XXX::expr),(t_XXX::typexpr)). ( Tsigma , E , e_XXX , t_XXX ) : JTe) e_t_list))) ; (length ( ((List.map (%((e_XXX::expr),(t_XXX::typexpr)).e_XXX) e_t_list)) ) >= 2 ) ; ( E , (TE_tuple ((List.map (%((e_XXX::expr),(t_XXX::typexpr)).t_XXX) e_t_list))) , t' ) : JTeq|] ==> ( Tsigma , E , (Expr_tuple ((List.map (%((e_XXX::expr),(t_XXX::typexpr)).e_XXX) e_t_list))) , t' ) : JTe" JTe_constructI: "[| ( E , constr , ((List.map (%((e_XXX::expr),(t_XXX::typexpr)).t_XXX) e_t_list)) , t ) : JTconstr_p ; (List.list_all (% b . b) ((List.map (%((e_XXX::expr),(t_XXX::typexpr)). ( Tsigma , E , e_XXX , t_XXX ) : JTe) e_t_list))) ; ( E , t , t' ) : JTeq|] ==> ( Tsigma , E , (Expr_construct constr ((List.map (%((e_XXX::expr),(t_XXX::typexpr)).e_XXX) e_t_list))) , t' ) : JTe" JTe_consI: "[| ( Tsigma , E , e1 , t ) : JTe ; ( Tsigma , E , e2 , (TE_constr ([ t ]) TC_list ) ) : JTe ; ( E , (TE_constr ([ t ]) TC_list ) , t' ) : JTeq|] ==> ( Tsigma , E , (Expr_cons e1 e2) , t' ) : JTe" JTe_record_constrI: "[|(List.list_all (% b . b) ((List.map (%((field_name_XXX::field_name),(e_XXX::expr),(t_XXX::typexpr)). ( Tsigma , E , e_XXX , t_XXX ) : JTe) field_name_e_t_list))) ; (List.list_all (% b . b) ((List.map (%((field_name_XXX::field_name),(e_XXX::expr),(t_XXX::typexpr)). ( E , field_name_XXX , t , t_XXX ) : JTfield) field_name_e_t_list))) ; ( t = (TE_constr (t'_list) (TC_name typeconstr_name)) ) ; ( E , (name_tcn typeconstr_name) , (EB_tr typeconstr_name kind (field_name'_list)) ) : Jlookup_EB ; (perm ( ((List.map (%((field_name_XXX::field_name),(e_XXX::expr),(t_XXX::typexpr)).field_name_XXX) field_name_e_t_list)) ) ( (field_name'_list) )) ; (length ( ((List.map (%((field_name_XXX::field_name),(e_XXX::expr),(t_XXX::typexpr)).e_XXX) field_name_e_t_list)) ) >= 1 ) ; ( E , t , t' ) : JTeq|] ==> ( Tsigma , E , (Expr_record ((List.map (%((field_name_XXX::field_name),(e_XXX::expr),(t_XXX::typexpr)).((F_name field_name_XXX),e_XXX)) field_name_e_t_list))) , t' ) : JTe" JTe_record_withI: "[| ( Tsigma , E , expr , t ) : JTe ; (List.list_all (% b . b) ((List.map (%((field_name_XXX::field_name),(e_XXX::expr),(t_XXX::typexpr)). ( E , field_name_XXX , t , t_XXX ) : JTfield) field_name_e_t_list))) ; (List.list_all (% b . b) ((List.map (%((field_name_XXX::field_name),(e_XXX::expr),(t_XXX::typexpr)). ( Tsigma , E , e_XXX , t_XXX ) : JTe) field_name_e_t_list))) ; (distinct ( ((List.map (%((field_name_XXX::field_name),(e_XXX::expr),(t_XXX::typexpr)).(name_fn field_name_XXX)) field_name_e_t_list)) )) ; (length ( ((List.map (%((field_name_XXX::field_name),(e_XXX::expr),(t_XXX::typexpr)).e_XXX) field_name_e_t_list)) ) >= 1 ) ; ( E , t , t' ) : JTeq|] ==> ( Tsigma , E , (Expr_override expr ((List.map (%((field_name_XXX::field_name),(e_XXX::expr),(t_XXX::typexpr)).((F_name field_name_XXX),e_XXX)) field_name_e_t_list))) , t' ) : JTe" JTe_applyI: "[| ( Tsigma , E , e , (TE_arrow t1 t) ) : JTe ; ( Tsigma , E , e1 , t1 ) : JTe|] ==> ( Tsigma , E , (Expr_apply e e1) , t ) : JTe" JTe_record_projI: "[| ( Tsigma , E , e , t ) : JTe ; ( E , field_name , t , t' ) : JTfield ; ( E , t' , t'' ) : JTeq|] ==> ( Tsigma , E , (Expr_field e (F_name field_name)) , t'' ) : JTe" JTe_andI: "[| ( Tsigma , E , e1 , (TE_constr [] TC_bool ) ) : JTe ; ( Tsigma , E , e2 , (TE_constr [] TC_bool ) ) : JTe ; ( E , (TE_constr [] TC_bool ) , t ) : JTeq|] ==> ( Tsigma , E , (Expr_and e1 e2) , t ) : JTe" JTe_orI: "[| ( Tsigma , E , e1 , (TE_constr [] TC_bool ) ) : JTe ; ( Tsigma , E , e2 , (TE_constr [] TC_bool ) ) : JTe ; ( E , (TE_constr [] TC_bool ) , t ) : JTeq|] ==> ( Tsigma , E , (Expr_or e1 e2) , t ) : JTe" JTe_ifthenelseI: "[| ( Tsigma , E , e1 , (TE_constr [] TC_bool ) ) : JTe ; ( Tsigma , E , e2 , t ) : JTe ; ( Tsigma , E , e3 , t ) : JTe|] ==> ( Tsigma , E , (Expr_ifthenelse e1 e2 e3) , t ) : JTe" JTe_whileI: "[| ( Tsigma , E , e1 , (TE_constr [] TC_bool ) ) : JTe ; ( Tsigma , E , e2 , (TE_constr [] TC_unit ) ) : JTe ; ( E , (TE_constr [] TC_unit ) , t ) : JTeq|] ==> ( Tsigma , E , (Expr_while e1 e2) , t ) : JTe" JTe_forI: "[| ( Tsigma , E , e1 , (TE_constr [] TC_int ) ) : JTe ; ( Tsigma , E , e2 , (TE_constr [] TC_int ) ) : JTe ; ( Tsigma , ( (EB_vn (VN_id lowercase_ident) (TS_forall (shiftt 0 1 (TE_constr [] TC_int ) ))) # E ) , e3 , (TE_constr [] TC_unit ) ) : JTe ; ( E , (TE_constr [] TC_unit ) , t ) : JTeq|] ==> ( Tsigma , E , (Expr_for (VN_id lowercase_ident) e1 for_dirn e2 e3) , t ) : JTe" JTe_sequenceI: "[| ( Tsigma , E , e1 , (TE_constr [] TC_unit ) ) : JTe ; ( Tsigma , E , e2 , t ) : JTe|] ==> ( Tsigma , E , (Expr_sequence e1 e2) , t ) : JTe" JTe_matchI: "[| ( Tsigma , E , e , t ) : JTe ; ( Tsigma , E , pattern_matching , t , t' ) : JTpat_matching|] ==> ( Tsigma , E , (Expr_match e pattern_matching) , t' ) : JTe" JTe_functionI: "[| ( Tsigma , E , pattern_matching , t , t' ) : JTpat_matching ; ( E , (TE_arrow t t') , t'' ) : JTeq|] ==> ( Tsigma , E , (Expr_function pattern_matching) , t'' ) : JTe" JTe_tryI: "[| ( Tsigma , E , e , t ) : JTe ; ( Tsigma , E , pattern_matching , (TE_constr [] TC_exn ) , t ) : JTpat_matching|] ==> ( Tsigma , E , (Expr_try e pattern_matching) , t ) : JTe" JTe_let_monoI: "[| ( Tsigma , E , (LB_simple pat expr) , (rev ((List.map (%((x_XXX::value_name),(t_XXX::typexpr)). (EB_vn x_XXX (TS_forall (shiftt 0 1 t_XXX ))) ) x_t_list)) ) ) : JTlet_binding ; ( Tsigma , (concat (rev ([(E)] @ [( (rev ((List.map (%((x_XXX::value_name),(t_XXX::typexpr)). (EB_vn x_XXX (TS_forall (shiftt 0 1 t_XXX ))) ) x_t_list)) ) )]) )) , e , t ) : JTe|] ==> ( Tsigma , E , (Expr_let (LB_simple pat expr) e) , t ) : JTe" JTe_let_polyI: "[|is_non_expansive_of_expr nexp ; ( (shiftTsig 0 1 Tsigma ) , ( EB_tv # E ) , (LB_simple pat nexp) , (rev ((List.map (%((x_XXX::value_name),(t_XXX::typexpr)). (EB_vn x_XXX (TS_forall (shiftt 0 1 t_XXX ))) ) x_t_list)) ) ) : JTlet_binding ; ( Tsigma , (concat (rev ([(E)] @ [( (rev ((List.map (%((x_XXX::value_name),(t_XXX::typexpr)).(EB_vn x_XXX (TS_forall t_XXX))) x_t_list)) ) )]) )) , e , t ) : JTe|] ==> ( Tsigma , E , (Expr_let (LB_simple pat nexp) e) , t ) : JTe" JTe_letrecI: "[| ( (shiftTsig 0 1 Tsigma ) , ( EB_tv # E ) , letrec_bindings , (rev ((List.map (%((x_XXX::value_name),(t_XXX::typexpr)). (EB_vn x_XXX (TS_forall (shiftt 0 1 t_XXX ))) ) x_t_list)) ) ) : JTletrec_binding ; ( Tsigma , (concat (rev ([(E)] @ [( (rev ((List.map (%((x_XXX::value_name),(t_XXX::typexpr)). (EB_vn x_XXX (TS_forall t_XXX)) ) x_t_list)) ) )]) )) , e , t ) : JTe|] ==> ( Tsigma , E , (Expr_letrec letrec_bindings e) , t ) : JTe" JTe_assertI: "[| ( Tsigma , E , e , (TE_constr [] TC_bool ) ) : JTe ; ( E , (TE_constr [] TC_unit ) , t ) : JTeq|] ==> ( Tsigma , E , (Expr_assert e) , t ) : JTe" JTe_assertfalseI: "[| ( E , t , 0 ) : JTt|] ==> ( Tsigma , E , (Expr_assert (Expr_constant CONST_false)) , t ) : JTe" JTe_locationI: "[| ( E ) : JTEok ; ( E , (name_l location) , (EB_l location t) ) : Jlookup_EB ; ( E , (TE_constr ([ t ]) TC_ref ) , t' ) : JTeq|] ==> ( Tsigma , E , (Expr_location location) , t' ) : JTe" (* defn pat_matching *) JTpat_matching_pmI: "[|(List.list_all (% b . b) ((List.map (%((pattern_XXX::pattern),(e_XXX::expr),(E_XXX::environment)). ( Tsigma , E , pattern_XXX , t , E_XXX ) : JTpat) pattern_e_E_list))) ; (List.list_all (% b . b) ((List.map (%((pattern_XXX::pattern),(e_XXX::expr),(E_XXX::environment)). ( Tsigma , (concat (rev ([(E)] @ [(E_XXX)]) )) , e_XXX , t' ) : JTe) pattern_e_E_list))) ; (length ( ((List.map (%((pattern_XXX::pattern),(e_XXX::expr),(E_XXX::environment)).pattern_XXX) pattern_e_E_list)) ) >= 1 ) |] ==> ( Tsigma , E , (PM_pm ((List.map (%((pattern_XXX::pattern),(e_XXX::expr),(E_XXX::environment)).(PE_inj pattern_XXX e_XXX)) pattern_e_E_list))) , t , t' ) : JTpat_matching" (* defn let_binding *) JTlet_binding_polyI: "[| ( Tsigma , E , pattern , t , (rev ((List.map (%((x_XXX::value_name),(t_XXX::typexpr)). (EB_vn x_XXX (TS_forall (shiftt 0 1 t_XXX ))) ) x_t_list)) ) ) : JTpat ; ( Tsigma , E , expr , t ) : JTe|] ==> ( Tsigma , E , (LB_simple pattern expr) , (rev ((List.map (%((x_XXX::value_name),(t_XXX::typexpr)). (EB_vn x_XXX (TS_forall (shiftt 0 1 t_XXX ))) ) x_t_list)) ) ) : JTlet_binding" (* defn letrec_binding *) JTletrec_binding_equal_functionI: "[| ( E' = (concat (rev ([(E)] @ [( (rev ((List.map (%((value_name_XXX::value_name),(pattern_matching_XXX::pattern_matching),(t_XXX::typexpr),(t_'::typexpr)). (EB_vn value_name_XXX (TS_forall (shiftt 0 1 (TE_arrow t_XXX t_') ))) ) value_name_pattern_matching_t_t'_list)) ) )]) )) ) ; (List.list_all (% b . b) ((List.map (%((value_name_XXX::value_name),(pattern_matching_XXX::pattern_matching),(t_XXX::typexpr),(t_'::typexpr)). ( Tsigma , E' , pattern_matching_XXX , t_XXX , t_' ) : JTpat_matching) value_name_pattern_matching_t_t'_list))) ; (distinct ( ((List.map (%((value_name_XXX::value_name),(pattern_matching_XXX::pattern_matching),(t_XXX::typexpr),(t_'::typexpr)).(name_vn value_name_XXX)) value_name_pattern_matching_t_t'_list)) )) |] ==> ( Tsigma , E , (LRBs_inj ((List.map (%((value_name_XXX::value_name),(pattern_matching_XXX::pattern_matching),(t_XXX::typexpr),(t_'::typexpr)).(LRB_simple value_name_XXX pattern_matching_XXX)) value_name_pattern_matching_t_t'_list))) , (rev ((List.map (%((value_name_XXX::value_name),(pattern_matching_XXX::pattern_matching),(t_XXX::typexpr),(t_'::typexpr)). (EB_vn value_name_XXX (TS_forall (shiftt 0 1 (TE_arrow t_XXX t_') ))) ) value_name_pattern_matching_t_t'_list)) ) ) : JTletrec_binding" (*defns JTconstr_decl *) consts JTconstr_decl :: "(type_params_opt*typeconstr*constr_decl*environment_binding) set" inductive JTconstr_decl intros (* defn constr_decl *) JTconstr_decl_nullaryI: " ( (TPS_nary ((List.map (%(tv_XXX::typevar).(TP_var tv_XXX)) tv_list))) , typeconstr , (CD_nullary constr_name) , (EB_cc constr_name typeconstr) ) : JTconstr_decl" JTconstr_decl_naryI: " ( (TPS_nary ((List.map (%((tv_XXX::typevar),(t_XXX::typexpr)).(TP_var tv_XXX)) tv_t_list))) , typeconstr , (CD_nary constr_name ((List.map (%((tv_XXX::typevar),(t_XXX::typexpr)).t_XXX) tv_t_list))) , (EB_pc constr_name (TPS_nary ((List.map (%((tv_XXX::typevar),(t_XXX::typexpr)).(TP_var tv_XXX)) tv_t_list))) (typexprs_inj ((List.map (%((tv_XXX::typevar),(t_XXX::typexpr)).t_XXX) tv_t_list))) typeconstr) ) : JTconstr_decl" (*defns JTfield_decl *) consts JTfield_decl :: "(type_params_opt*typeconstr_name*field_decl*environment_binding) set" inductive JTfield_decl intros (* defn field_decl *) JTfield_decl_onlyI: " ( (TPS_nary ((List.map (%(tv_XXX::typevar).(TP_var tv_XXX)) tv_list))) , typeconstr_name , (FD_immutable fn t) , (EB_fn fn (TPS_nary ((List.map (%(tv_XXX::typevar).(TP_var tv_XXX)) tv_list))) typeconstr_name t) ) : JTfield_decl" (*defns JTtypedef *) consts JTtypedef :: "(caml_typedef list*environment*environment*environment) set" inductive JTtypedef intros (* defn typedef *) JTtypedef_emptyI: " ( [] , [] , [] , [] ) : JTtypedef" JTtypedef_eqI: "[| ( (caml_typedef_list) , E , E' , E'' ) : JTtypedef|] ==> ( ([((TD_td type_params_opt typeconstr_name (TI_eq (TE_te t))))] @ caml_typedef_list) , E , ( (EB_ta type_params_opt typeconstr_name t) # E' ) , E'' ) : JTtypedef" JTtypedef_def_sumI: "[| ( (caml_typedef_list) , E , E' , E'' ) : JTtypedef ; ( type_params_opt , kind ) : JTtps_kind ; (List.list_all (% b . b) ((List.map (%((constr_decl_XXX::constr_decl),(EB_XXX::environment_binding)). ( type_params_opt , (TC_name typeconstr_name) , constr_decl_XXX , EB_XXX ) : JTconstr_decl) constr_decl_EB_list)))|] ==> ( ([((TD_td type_params_opt typeconstr_name (TI_def (TR_variant ((List.map (%((constr_decl_XXX::constr_decl),(EB_XXX::environment_binding)).constr_decl_XXX) constr_decl_EB_list))))))] @ caml_typedef_list) , ( (EB_td typeconstr_name kind) # E ) , E' , (concat (rev ([(E'')] @ [( (rev ((List.map (%((constr_decl_XXX::constr_decl),(EB_XXX::environment_binding)).EB_XXX) constr_decl_EB_list)) ) )]) )) ) : JTtypedef" JTtypedef_def_recordI: "[| ( (caml_typedef_list) , E , E' , E'' ) : JTtypedef ; ( type_params_opt , kind ) : JTtps_kind ; (List.list_all (% b . b) ((List.map (%((field_name_XXX::field_name),(t_XXX::typexpr),(EB_XXX::environment_binding)). ( type_params_opt , typeconstr_name , (FD_immutable field_name_XXX t_XXX) , EB_XXX ) : JTfield_decl) field_name_t_EB_list)))|] ==> ( ([((TD_td type_params_opt typeconstr_name (TI_def (TR_record ((List.map (%((field_name_XXX::field_name),(t_XXX::typexpr),(EB_XXX::environment_binding)).(FD_immutable field_name_XXX t_XXX)) field_name_t_EB_list))))))] @ caml_typedef_list) , ( (EB_tr typeconstr_name kind ((List.map (%((field_name_XXX::field_name),(t_XXX::typexpr),(EB_XXX::environment_binding)).field_name_XXX) field_name_t_EB_list))) # E ) , E' , (concat (rev ([(E'')] @ [( (rev ((List.map (%((field_name_XXX::field_name),(t_XXX::typexpr),(EB_XXX::environment_binding)).EB_XXX) field_name_t_EB_list)) ) )]) )) ) : JTtypedef" (*defns JTtype_definition *) consts JTtype_definition :: "(environment*caml_type_definition*environment) set" inductive JTtype_definition intros (* defn type_definition *) JTtype_definition_listI: "[| ( (caml_typedef_list) , E' , E'' , E''' ) : JTtypedef ; ( E'''' = (concat (rev ([(E')] @ [(E'')] @ [(E''')]) )) ) ; ( (concat (rev ([(E)] @ [(E'''')]) )) ) : JTEok|] ==> ( E , (TDF_tdf (caml_typedef_list)) , E'''' ) : JTtype_definition" JTtype_definition_swapI: "[| ( E , (TDF_tdf (caml_typedef_list @ [(caml_typedef')] @ [(caml_typedef)] @ caml_typedef''_list)) , E' ) : JTtype_definition|] ==> ( E , (TDF_tdf (caml_typedef_list @ [(caml_typedef)] @ [(caml_typedef')] @ caml_typedef''_list)) , E' ) : JTtype_definition" (*defns JTdefinition *) consts JTdefinition :: "(environment*caml_definition*environment) set" inductive JTdefinition intros (* defn definition *) JTdefinition_let_polyI: "[|is_non_expansive_of_expr nexp ; ( Tsigma , ( EB_tv # E ) , (LB_simple pat nexp) , (rev ((List.map (%((x_XXX::value_name),(t_'::typexpr)). (EB_vn x_XXX (TS_forall (shiftt 0 1 t_' ))) ) x_t'_list)) ) ) : JTlet_binding|] ==> ( E , (D_let (LB_simple pat nexp)) , (rev ((List.map (%((x_XXX::value_name),(t_'::typexpr)). (EB_vn x_XXX (TS_forall t_')) ) x_t'_list)) ) ) : JTdefinition" JTdefinition_let_monoI: "[| ( Tsigma , E , (LB_simple pat expr) , (rev ((List.map (%((x_XXX::value_name),(t_'::typexpr)). (EB_vn x_XXX (TS_forall (shiftt 0 1 t_' ))) ) x_t'_list)) ) ) : JTlet_binding|] ==> ( E , (D_let (LB_simple pat expr)) , (rev ((List.map (%((x_XXX::value_name),(t_'::typexpr)). (EB_vn x_XXX (TS_forall (shiftt 0 1 t_' ))) ) x_t'_list)) ) ) : JTdefinition" JTdefinition_letrecI: "[| ( Tsigma , ( EB_tv # E ) , letrec_bindings , (rev ((List.map (%((x_XXX::value_name),(t_'::typexpr)). (EB_vn x_XXX (TS_forall (shiftt 0 1 t_' ))) ) x_t'_list)) ) ) : JTletrec_binding|] ==> ( E , (D_letrec letrec_bindings) , (rev ((List.map (%((x_XXX::value_name),(t_'::typexpr)). (EB_vn x_XXX (TS_forall t_')) ) x_t'_list)) ) ) : JTdefinition" JTdefinition_typedefI: "[| ( E , (TDF_tdf (caml_typedef_list)) , E' ) : JTtype_definition|] ==> ( E , (D_type (TDF_tdf (caml_typedef_list))) , E' ) : JTdefinition" JTdefinition_exndefI: "[| ( E ) : JTEok ; ( (TPS_nary []) , TC_exn , constr_decl , EB ) : JTconstr_decl|] ==> ( E , (D_exception (ED_def constr_decl)) , (rev ([(EB)]) ) ) : JTdefinition" (*defns JTdefinitions *) consts JTdefinitions :: "(environment*definitions*environment) set" inductive JTdefinitions intros (* defn definitions *) JTdefinitions_emptyI: "[| ( E ) : JTEok|] ==> ( E , Ds_nil , (rev [] ) ) : JTdefinitions" JTdefinitions_itemI: "[| ( E , caml_definition , E' ) : JTdefinition ; ( (concat (rev ([(E)] @ [(E')]) )) , definitions' , E'' ) : JTdefinitions|] ==> ( E , (Ds_cons caml_definition definitions') , (concat (rev ([(E')] @ [(E'')]) )) ) : JTdefinitions" (*defns JTprog *) consts JTprog :: "(environment*program*environment) set" inductive JTprog intros (* defn prog *) JTprog_defsI: "[| ( E , definitions , E' ) : JTdefinitions|] ==> ( E , (Prog_defs definitions) , E' ) : JTprog" JTprog_raiseI: "[|is_value_of_expr v ; ( Tsigma , E , v , t ) : JTe|] ==> ( E , (Prog_raise v) , (rev [] ) ) : JTprog" (*defns JTstore *) consts JTstore :: "(environment*store*environment) set" inductive JTstore intros (* defn store *) JTstore_emptyI: " ( E , [] , (rev [] ) ) : JTstore" JTstore_mapI: "[|is_value_of_expr v ; ( E , store , E' ) : JTstore ; ( [] , E , v , t ) : JTe|] ==> ( E , (( l , v )# store ) , ( (EB_l l t) # E' ) ) : JTstore" (*defns JTtop *) consts JTtop :: "(environment*program*store*environment) set" inductive JTtop intros (* defn top *) JTtop_defsI: "[| ( (concat (rev ([(E)] @ [(E')]) )) , store , E' ) : JTstore ; ( (concat (rev ([(E)] @ [(E')]) )) , program , E'' ) : JTprog|] ==> ( E , program , store , (concat (rev ([(E')] @ [(E'')]) )) ) : JTtop" (*defns JTLin *) consts JTLin :: "(Tsigma*environment*trans_label) set" inductive JTLin intros (* defn Lin *) JTLin_nilI: " ( Tsigma , E , Lab_nil ) : JTLin" JTLin_allocI: "[| ( E , names ) : JdomE ; (~( (name_l location) mem names )) |] ==> ( Tsigma , E , (Lab_alloc v location) ) : JTLin" JTLin_derefI: "[|is_value_of_expr v ; ( Tsigma , E , v , t ) : JTe ; ( E , (name_l location) , (EB_l location t) ) : Jlookup_EB|] ==> ( Tsigma , E , (Lab_deref location v) ) : JTLin" JTLin_assignI: " ( Tsigma , E , (Lab_assign location v) ) : JTLin" (*defns JTLout *) consts JTLout :: "(Tsigma*environment*trans_label*environment) set" inductive JTLout intros (* defn Lout *) JTLout_nilI: " ( Tsigma , E , Lab_nil , (rev [] ) ) : JTLout" JTLout_allocI: "[|is_value_of_expr v ; ( Tsigma , E , v , t ) : JTe|] ==> ( Tsigma , E , (Lab_alloc v location) , (rev ([( (EB_l location t) )]) ) ) : JTLout" JTLout_derefI: " ( Tsigma , E , (Lab_deref location v) , (rev [] ) ) : JTLout" JTLout_assignI: "[|is_value_of_expr v ; ( Tsigma , E , v , t ) : JTe ; ( E , (name_l location) , (EB_l location t) ) : Jlookup_EB|] ==> ( Tsigma , E , (Lab_assign location v) , (rev [] ) ) : JTLout" (*defns JmatchP *) consts JM_matchP :: "(expr*pattern) set" inductive JM_matchP intros (* defn matchP *) JM_matchP_varI: "[|is_value_of_expr v|] ==> ( v , (P_var x) ) : JM_matchP" JM_matchP_anyI: "[|is_value_of_expr v|] ==> ( v , P_any ) : JM_matchP" JM_matchP_constantI: " ( (Expr_constant constant) , (P_constant constant) ) : JM_matchP" JM_matchP_aliasI: "[|is_value_of_expr v ; ( v , pat ) : JM_matchP|] ==> ( v , (P_alias pat x) ) : JM_matchP" JM_matchP_typedI: "[|is_value_of_expr v ; ( v , pat ) : JM_matchP|] ==> ( v , (P_typed pat t) ) : JM_matchP" JM_matchP_or_leftI: "[|is_value_of_expr v ; ( v , pat1 ) : JM_matchP|] ==> ( v , (P_or pat1 pat2) ) : JM_matchP" JM_matchP_or_rightI: "[|is_value_of_expr v ; ( v , pat2 ) : JM_matchP|] ==> ( v , (P_or pat1 pat2) ) : JM_matchP" JM_matchP_constructI: "[|List.list_all (%(v_XXX,pat_XXX). is_value_of_expr v_XXX) v_pat_list ; (List.list_all (% b . b) ((List.map (%((v_XXX::expr),(pat_XXX::pattern)). ( v_XXX , pat_XXX ) : JM_matchP) v_pat_list)))|] ==> ( (Expr_construct constr ((List.map (%((v_XXX::expr),(pat_XXX::pattern)).v_XXX) v_pat_list))) , (P_construct constr ((List.map (%((v_XXX::expr),(pat_XXX::pattern)).pat_XXX) v_pat_list))) ) : JM_matchP" JM_matchP_construct_anyI: "[|List.list_all (%v_XXX. is_value_of_expr v_XXX) v_list|] ==> ( (Expr_construct constr (v_list)) , (P_construct_any constr) ) : JM_matchP" JM_matchP_tupleI: "[|List.list_all (%(v_XXX,pat_XXX). is_value_of_expr v_XXX) v_pat_list ; (List.list_all (% b . b) ((List.map (%((v_XXX::expr),(pat_XXX::pattern)). ( v_XXX , pat_XXX ) : JM_matchP) v_pat_list)))|] ==> ( (Expr_tuple ((List.map (%((v_XXX::expr),(pat_XXX::pattern)).v_XXX) v_pat_list))) , (P_tuple ((List.map (%((v_XXX::expr),(pat_XXX::pattern)).pat_XXX) v_pat_list))) ) : JM_matchP" JM_matchP_recordI: "[|List.list_all (%(fn_XXX,v_''). is_value_of_expr v_'') fn_v''_list ; List.list_all (%(field_name_',pat_XXX,v_'). is_value_of_expr v_') field_name'_pat_v'_list ; List.list_all (%(field_name_XXX,v_XXX). is_value_of_expr v_XXX) field_name_v_list ; (perm ( ((List.map (%((field_name_'::field_name),(pat_XXX::pattern),(v_'::expr)).(field_name_',v_')) field_name'_pat_v'_list) @ fn_v''_list) ) ( (field_name_v_list) )) ; (List.list_all (% b . b) ((List.map (%((field_name_'::field_name),(pat_XXX::pattern),(v_'::expr)). ( v_' , pat_XXX ) : JM_matchP) field_name'_pat_v'_list))) ; (distinct ( ((List.map (%((field_name_XXX::field_name),(v_XXX::expr)).(name_fn field_name_XXX)) field_name_v_list)) )) |] ==> ( (Expr_record ((List.map (%((field_name_XXX::field_name),(v_XXX::expr)).((F_name field_name_XXX),v_XXX)) field_name_v_list))) , (P_record ((List.map (%((field_name_'::field_name),(pat_XXX::pattern),(v_'::expr)).((F_name field_name_'),pat_XXX)) field_name'_pat_v'_list))) ) : JM_matchP" JM_matchP_consI: "[|is_value_of_expr v1 ; is_value_of_expr v2 ; ( v1 , pat1 ) : JM_matchP ; ( v2 , pat2 ) : JM_matchP|] ==> ( (Expr_cons v1 v2) , (P_cons pat1 pat2) ) : JM_matchP" (*defns Jmatch *) consts JM_match :: "(expr*pattern*substs_x) set" inductive JM_match intros (* defn match *) JM_match_varI: "[|is_value_of_expr v|] ==> ( v , (P_var x) , (substs_x_xs ([(x,v)])) ) : JM_match" JM_match_anyI: "[|is_value_of_expr v|] ==> ( v , P_any , (substs_x_xs []) ) : JM_match" JM_match_constantI: " ( (Expr_constant constant) , (P_constant constant) , (substs_x_xs []) ) : JM_match" JM_match_aliasI: "[|is_value_of_expr v ; List.list_all (%(x_XXX,v_XXX). is_value_of_expr v_XXX) x_v_list ; ( v , pat , (substs_x_xs (x_v_list)) ) : JM_match|] ==> ( v , (P_alias pat x) , (substs_x_xs (x_v_list @ [(x,v)])) ) : JM_match" JM_match_typedI: "[|is_value_of_expr v ; List.list_all (%(x_XXX,v_XXX). is_value_of_expr v_XXX) x_v_list ; ( v , pat , (substs_x_xs (x_v_list)) ) : JM_match|] ==> ( v , (P_typed pat t) , (substs_x_xs (x_v_list)) ) : JM_match" JM_match_or_leftI: "[|is_value_of_expr v ; List.list_all (%(x_XXX,v_XXX). is_value_of_expr v_XXX) x_v_list ; ( v , pat1 , (substs_x_xs (x_v_list)) ) : JM_match|] ==> ( v , (P_or pat1 pat2) , (substs_x_xs (x_v_list)) ) : JM_match" JM_match_or_rightI: "[|is_value_of_expr v ; List.list_all (%(x_XXX,v_XXX). is_value_of_expr v_XXX) x_v_list ; (~(( v , pat1 ) : JM_matchP)) ; ( v , pat2 , (substs_x_xs (x_v_list)) ) : JM_match|] ==> ( v , (P_or pat1 pat2) , (substs_x_xs (x_v_list)) ) : JM_match" JM_match_constructI: "[|List.list_all (%(v_XXX,pat_XXX,substs_x_XXX). is_value_of_expr v_XXX) v_pat_substs_x_list ; (List.list_all (% b . b) ((List.map (%((v_XXX::expr),(pat_XXX::pattern),(substs_x_XXX::substs_x)). ( v_XXX , pat_XXX , substs_x_XXX ) : JM_match) v_pat_substs_x_list)))|] ==> ( (Expr_construct constr ((List.map (%((v_XXX::expr),(pat_XXX::pattern),(substs_x_XXX::substs_x)).v_XXX) v_pat_substs_x_list))) , (P_construct constr ((List.map (%((v_XXX::expr),(pat_XXX::pattern),(substs_x_XXX::substs_x)).pat_XXX) v_pat_substs_x_list))) , (substs_x_xs (concat (map (%x. case x of substs_x_xs l => l) ((List.map (%((v_XXX::expr),(pat_XXX::pattern),(substs_x_XXX::substs_x)).substs_x_XXX) v_pat_substs_x_list)) ))) ) : JM_match" JM_match_construct_anyI: "[|List.list_all (%v_XXX. is_value_of_expr v_XXX) v_list|] ==> ( (Expr_construct constr (v_list)) , (P_construct_any constr) , (substs_x_xs []) ) : JM_match" JM_match_tupleI: "[|List.list_all (%(v_XXX,pat_XXX,substs_x_XXX). is_value_of_expr v_XXX) v_pat_substs_x_list ; (List.list_all (% b . b) ((List.map (%((v_XXX::expr),(pat_XXX::pattern),(substs_x_XXX::substs_x)). ( v_XXX , pat_XXX , substs_x_XXX ) : JM_match) v_pat_substs_x_list)))|] ==> ( (Expr_tuple ((List.map (%((v_XXX::expr),(pat_XXX::pattern),(substs_x_XXX::substs_x)).v_XXX) v_pat_substs_x_list))) , (P_tuple ((List.map (%((v_XXX::expr),(pat_XXX::pattern),(substs_x_XXX::substs_x)).pat_XXX) v_pat_substs_x_list))) , (substs_x_xs (concat (map (%x. case x of substs_x_xs l => l) ((List.map (%((v_XXX::expr),(pat_XXX::pattern),(substs_x_XXX::substs_x)).substs_x_XXX) v_pat_substs_x_list)) ))) ) : JM_match" JM_match_recordI: "[|List.list_all (%(fn_XXX,v_''). is_value_of_expr v_'') fn_v''_list ; List.list_all (%(field_name_',pat_XXX,substs_x_XXX,v_'). is_value_of_expr v_') field_name'_pat_substs_x_v'_list ; List.list_all (%(field_name_XXX,v_XXX). is_value_of_expr v_XXX) field_name_v_list ; (perm ( ((List.map (%((field_name_'::field_name),(pat_XXX::pattern),(substs_x_XXX::substs_x),(v_'::expr)).(field_name_',v_')) field_name'_pat_substs_x_v'_list) @ fn_v''_list) ) ( (field_name_v_list) )) ; (List.list_all (% b . b) ((List.map (%((field_name_'::field_name),(pat_XXX::pattern),(substs_x_XXX::substs_x),(v_'::expr)). ( v_' , pat_XXX , substs_x_XXX ) : JM_match) field_name'_pat_substs_x_v'_list))) ; (distinct ( ((List.map (%((field_name_XXX::field_name),(v_XXX::expr)).(name_fn field_name_XXX)) field_name_v_list)) )) |] ==> ( (Expr_record ((List.map (%((field_name_XXX::field_name),(v_XXX::expr)).((F_name field_name_XXX),v_XXX)) field_name_v_list))) , (P_record ((List.map (%((field_name_'::field_name),(pat_XXX::pattern),(substs_x_XXX::substs_x),(v_'::expr)).((F_name field_name_'),pat_XXX)) field_name'_pat_substs_x_v'_list))) , (substs_x_xs (concat (map (%x. case x of substs_x_xs l => l) ((List.map (%((field_name_'::field_name),(pat_XXX::pattern),(substs_x_XXX::substs_x),(v_'::expr)).substs_x_XXX) field_name'_pat_substs_x_v'_list)) ))) ) : JM_match" JM_match_consI: "[|is_value_of_expr v1 ; is_value_of_expr v2 ; ( v1 , pat1 , substs_x1 ) : JM_match ; ( v2 , pat2 , substs_x2 ) : JM_match|] ==> ( (Expr_cons v1 v2) , (P_cons pat1 pat2) , (substs_x_xs (concat (map (%x. case x of substs_x_xs l => l) ([(substs_x1)] @ [(substs_x2)]) ))) ) : JM_match" (*defns Jrecfun *) consts Jrecfun :: "(letrec_bindings*pattern_matching*expr) set" inductive Jrecfun intros (* defn recfun *) Jrecfun_letrecI: "[| ( letrec_bindings = (LRBs_inj ((List.map (%((x_XXX::value_name),(pattern_matching_XXX::pattern_matching)).(LRB_simple x_XXX pattern_matching_XXX)) x_pattern_matching_list))) ) |] ==> ( letrec_bindings , pattern_matching , (substs_value_name_expr (case (substs_x_xs ((List.map (%((x_XXX::value_name),(pattern_matching_XXX::pattern_matching)).(x_XXX,(Expr_letrec letrec_bindings (Expr_ident x_XXX)))) x_pattern_matching_list))) of substs_x_xs l => l) (Expr_function pattern_matching) ) ) : Jrecfun" (*defns Jfunval *) consts Jfunval :: "expr set" inductive Jfunval intros (* defn funval *) Jfunval_upI: " ( (Expr_uprim unary_prim) ) : Jfunval" Jfunval_bpI: " ( (Expr_bprim binary_prim) ) : Jfunval" Jfunval_bp_appI: "[|is_value_of_expr v|] ==> ( (Expr_apply (Expr_bprim binary_prim) v) ) : Jfunval" Jfunval_funcI: " ( (Expr_function pattern_matching) ) : Jfunval" (*defns JRuprim *) consts JRuprim :: "(unary_prim*expr*labelled_arrow*expr) set" inductive JRuprim intros (* defn Ruprim *) Juprim_not_trueI: " ( Uprim_not , (Expr_constant CONST_true) , Lab_nil , (Expr_constant CONST_false) ) : JRuprim" Juprim_not_falseI: " ( Uprim_not , (Expr_constant CONST_false) , Lab_nil , (Expr_constant CONST_true) ) : JRuprim" Juprim_uminusI: " ( Uprim_minus , (Expr_constant (CONST_int intn)) , Lab_nil , (Expr_constant (CONST_int ( ( 0 ) - intn ) )) ) : JRuprim" Juprim_ref_allocI: "[|is_value_of_expr v|] ==> ( Uprim_ref , v , (Lab_alloc v l) , (Expr_location l) ) : JRuprim" Juprim_derefI: "[|is_value_of_expr v|] ==> ( Uprim_deref , (Expr_location l) , (Lab_deref l v) , v ) : JRuprim" (*defns JRbprim *) consts JRbprim :: "(expr*binary_prim*expr*labelled_arrow*expr) set" inductive JRbprim intros (* defn Rbprim *) Jbprim_equal_funI: "[|is_value_of_expr v ; is_value_of_expr v' ; ( v ) : Jfunval|] ==> ( v , Bprim_equal , v' , Lab_nil , (Expr_apply (Expr_uprim Uprim_raise) (Expr_construct C_invalidargument ([((Expr_constant (CONST_string ''equal: functional value'') ))])) ) ) : JRbprim" Jbprim_equal_const_trueI: " ( (Expr_constant constant) , Bprim_equal , (Expr_constant constant) , Lab_nil , (Expr_constant CONST_true) ) : JRbprim" Jbprim_equal_const_falseI: "[| (~( constant = constant' )) |] ==> ( (Expr_constant constant) , Bprim_equal , (Expr_constant constant') , Lab_nil , (Expr_constant CONST_false) ) : JRbprim" Jbprim_equal_locI: " ( (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')) ) ) : JRbprim" Jbprim_equal_consI: "[|is_value_of_expr v1 ; is_value_of_expr v2 ; is_value_of_expr v1' ; is_value_of_expr v2'|] ==> ( (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') ) ) : JRbprim" Jbprim_equal_cons_nilI: "[|is_value_of_expr v1 ; is_value_of_expr v2|] ==> ( (Expr_cons v1 v2) , Bprim_equal , (Expr_constant CONST_nil) , Lab_nil , (Expr_constant CONST_false) ) : JRbprim" Jbprim_equal_nil_consI: "[|is_value_of_expr v1 ; is_value_of_expr v2|] ==> ( (Expr_constant CONST_nil) , Bprim_equal , (Expr_cons v1 v2) , Lab_nil , (Expr_constant CONST_false) ) : JRbprim" Jbprim_equal_tupleI: "[|List.list_all (%(v_XXX,v_'). is_value_of_expr v_XXX) v_v'_list ; List.list_all (%(v_XXX,v_'). is_value_of_expr v_') v_v'_list ; (length ( ((List.map (%((v_XXX::expr),(v_'::expr)).v_XXX) v_v'_list)) ) >= 2 ) |] ==> ( (Expr_tuple ((List.map (%((v_XXX::expr),(v_'::expr)).v_XXX) v_v'_list))) , Bprim_equal , (Expr_tuple ((List.map (%((v_XXX::expr),(v_'::expr)).v_') v_v'_list))) , Lab_nil , (foldr Expr_and ((List.map (%((v_XXX::expr),(v_'::expr)).(Expr_apply (Expr_apply (Expr_bprim Bprim_equal) v_XXX) v_')) v_v'_list)) (Expr_constant CONST_true)) ) : JRbprim" Jbprim_equal_constrI: "[|List.list_all (%(v_XXX,v_'). is_value_of_expr v_XXX) v_v'_list ; List.list_all (%(v_XXX,v_'). is_value_of_expr v_') v_v'_list|] ==> ( (Expr_construct constr ((List.map (%((v_XXX::expr),(v_'::expr)).v_XXX) v_v'_list))) , Bprim_equal , (Expr_construct constr ((List.map (%((v_XXX::expr),(v_'::expr)).v_') v_v'_list))) , Lab_nil , (foldr Expr_and ((List.map (%((v_XXX::expr),(v_'::expr)).(Expr_apply (Expr_apply (Expr_bprim Bprim_equal) v_XXX) v_')) v_v'_list)) (Expr_constant CONST_true)) ) : JRbprim" Jbprim_equal_constr_falseI: "[|List.list_all (%v_'. is_value_of_expr v_') v'_list ; List.list_all (%v_XXX. is_value_of_expr v_XXX) v_list ; (~( (CONST_constr constr) = (CONST_constr constr') )) |] ==> ( (Expr_construct constr (v_list)) , Bprim_equal , (Expr_construct constr' (v'_list)) , Lab_nil , (Expr_constant CONST_false) ) : JRbprim" Jbprim_equal_const_constr_falseI: "[|List.list_all (%v_XXX. is_value_of_expr v_XXX) v_list|] ==> ( (Expr_constant (CONST_constr constr')) , Bprim_equal , (Expr_construct constr (v_list)) , Lab_nil , (Expr_constant CONST_false) ) : JRbprim" Jbprim_equal_constr_const_falseI: "[|List.list_all (%v_XXX. is_value_of_expr v_XXX) v_list|] ==> ( (Expr_construct constr (v_list)) , Bprim_equal , (Expr_constant (CONST_constr constr')) , Lab_nil , (Expr_constant CONST_false) ) : JRbprim" Jbprim_equal_recI: "[|is_value_of_expr v' ; List.list_all (%(fn_'',v_''). is_value_of_expr v_'') fn''_v''_list ; List.list_all (%(fn_XXX,v_XXX). is_value_of_expr v_XXX) fn_v_list ; ( v' = (Expr_record ((List.map (%((fn_''::field_name),(v_''::expr)).((F_name fn_''),v_'')) fn''_v''_list))) ) ; (perm ( ((List.map (%((fn_XXX::field_name),(v_XXX::expr)).fn_XXX) fn_v_list)) ) ( ((List.map (%((fn_''::field_name),(v_''::expr)).fn_'') fn''_v''_list)) )) |] ==> ( (Expr_record ((List.map (%((fn_XXX::field_name),(v_XXX::expr)).((F_name fn_XXX),v_XXX)) fn_v_list))) , Bprim_equal , v' , Lab_nil , (foldr Expr_and ((List.map (%((fn_XXX::field_name),(v_XXX::expr)).(Expr_apply (Expr_apply (Expr_bprim Bprim_equal) v_XXX) (Expr_field v' (F_name fn_XXX)) )) fn_v_list)) (Expr_constant CONST_true)) ) : JRbprim" Jbprim_plusI: " ( (Expr_constant (CONST_int intn1)) , Bprim_plus , (Expr_constant (CONST_int intn2)) , Lab_nil , (Expr_constant (CONST_int ( intn1 + intn2 ) )) ) : JRbprim" Jbprim_minusI: " ( (Expr_constant (CONST_int intn1)) , Bprim_minus , (Expr_constant (CONST_int intn2)) , Lab_nil , (Expr_constant (CONST_int ( intn1 - intn2 ) )) ) : JRbprim" Jbprim_timesI: " ( (Expr_constant (CONST_int intn1)) , Bprim_times , (Expr_constant (CONST_int intn2)) , Lab_nil , (Expr_constant (CONST_int ( intn1 * intn2 ) )) ) : JRbprim" Jbprim_div0I: " ( (Expr_constant (CONST_int intn)) , Bprim_div , (Expr_constant (CONST_int ( 0 ) )) , Lab_nil , (Expr_apply (Expr_uprim Uprim_raise) (Expr_constant (CONST_constr C_div_by_0))) ) : JRbprim" Jbprim_divI: "[| (~( (CONST_int intn2) = (CONST_int ( 0 ) ) )) |] ==> ( (Expr_constant (CONST_int intn1)) , Bprim_div , (Expr_constant (CONST_int intn2)) , Lab_nil , (Expr_constant (CONST_int ( intn1 div intn2 ) )) ) : JRbprim" Jbprim_assignI: "[|is_value_of_expr v|] ==> ( (Expr_location l) , Bprim_assign , v , (Lab_assign l v) , (Expr_constant CONST_unit) ) : JRbprim" (*defns JRmatching_step *) consts JRmatching_step :: "(expr*pattern_matching*pattern_matching) set" inductive JRmatching_step intros (* defn matching_step *) JRmatching_nextI: "[|is_value_of_expr v ; (~(( v , pat ) : JM_matchP)) ; (length ( ((List.map (%((pat_XXX::pattern),(e_XXX::expr)).e_XXX) pat_e_list)) ) >= 1 ) |] ==> ( v , (PM_pm ([((PE_inj pat e))] @ (List.map (%((pat_XXX::pattern),(e_XXX::expr)).(PE_inj pat_XXX e_XXX)) pat_e_list))) , (PM_pm ((List.map (%((pat_XXX::pattern),(e_XXX::expr)).(PE_inj pat_XXX e_XXX)) pat_e_list))) ) : JRmatching_step" (*defns JRmatching_success *) consts JRmatching_success :: "(expr*pattern_matching*expr) set" inductive JRmatching_success intros (* defn matching_success *) JRmatching_foundI: "[|is_value_of_expr v ; List.list_all (%(x_XXX,v_XXX). is_value_of_expr v_XXX) x_v_list ; ( v , pat , (substs_x_xs (x_v_list)) ) : JM_match|] ==> ( v , (PM_pm ([((PE_inj pat e))] @ (List.map (%((pat_XXX::pattern),(e_XXX::expr)).(PE_inj pat_XXX e_XXX)) pat_e_list))) , (substs_value_name_expr (case (substs_x_xs (x_v_list)) of substs_x_xs l => l) e ) ) : JRmatching_success" JRmatching_failI: "[|is_value_of_expr v ; (~(( v , pat ) : JM_matchP)) |] ==> ( v , (PM_pm ([((PE_inj pat e))])) , (Expr_apply (Expr_uprim Uprim_raise) (Expr_constant (CONST_constr C_matchfailure))) ) : JRmatching_success" (*defns Jred *) consts JR_expr :: "(expr*labelled_arrow*expr) set" inductive JR_expr intros (* defn expr *) JR_expr_uprimI: "[|is_value_of_expr v ; ( unary_prim , v , L , e ) : JRuprim|] ==> ( (Expr_apply (Expr_uprim unary_prim) v) , L , e ) : JR_expr" JR_expr_bprimI: "[|is_value_of_expr v1 ; is_value_of_expr v2 ; ( v1 , binary_prim , v2 , L , e ) : JRbprim|] ==> ( (Expr_apply (Expr_apply (Expr_bprim binary_prim) v1) v2) , L , e ) : JR_expr" JR_expr_typed_ctxI: " ( (Expr_typed e t) , Lab_nil , e ) : JR_expr" JR_expr_apply_ctx_argI: "[| ( e0 , L , e0' ) : JR_expr|] ==> ( (Expr_apply e1 e0) , L , (Expr_apply e1 e0') ) : JR_expr" JR_expr_apply_raise1I: "[|is_value_of_expr v|] ==> ( (Expr_apply e (Expr_apply (Expr_uprim Uprim_raise) v) ) , Lab_nil , (Expr_apply (Expr_uprim Uprim_raise) v) ) : JR_expr" JR_expr_apply_ctx_funI: "[|is_value_of_expr v0 ; ( e1 , L , e1' ) : JR_expr|] ==> ( (Expr_apply e1 v0) , L , (Expr_apply e1' v0) ) : JR_expr" JR_expr_apply_raise2I: "[|is_value_of_expr v ; is_value_of_expr v'|] ==> ( (Expr_apply (Expr_apply (Expr_uprim Uprim_raise) v) v') , Lab_nil , (Expr_apply (Expr_uprim Uprim_raise) v) ) : JR_expr" JR_expr_applyI: "[|is_value_of_expr v0|] ==> ( (Expr_apply (Expr_function pattern_matching) v0) , Lab_nil , (Expr_match v0 pattern_matching) ) : JR_expr" JR_expr_let_ctxI: "[| ( e0 , L , e0' ) : JR_expr|] ==> ( (Expr_let (LB_simple pat e0) e) , L , (Expr_let (LB_simple pat e0') e) ) : JR_expr" JR_expr_let_raiseI: "[|is_value_of_expr v|] ==> ( (Expr_let (LB_simple pat (Expr_apply (Expr_uprim Uprim_raise) v)) e) , Lab_nil , (Expr_apply (Expr_uprim Uprim_raise) v) ) : JR_expr" JR_expr_let_substI: "[|is_value_of_expr v ; List.list_all (%(x_XXX,v_XXX). is_value_of_expr v_XXX) x_v_list ; ( v , pat , (substs_x_xs (x_v_list)) ) : JM_match|] ==> ( (Expr_let (LB_simple pat v) e) , Lab_nil , (substs_value_name_expr (case (substs_x_xs (x_v_list)) of substs_x_xs l => l) e ) ) : JR_expr" JR_expr_let_failI: "[|is_value_of_expr v ; (~(( v , pat ) : JM_matchP)) |] ==> ( (Expr_let (LB_simple pat v) e) , Lab_nil , (Expr_apply (Expr_uprim Uprim_raise) (Expr_constant (CONST_constr C_matchfailure))) ) : JR_expr" JR_expr_letrecI: "[| ( letrec_bindings = (LRBs_inj ((List.map (%((x_XXX::value_name),(e_XXX::expr),(pattern_matching_XXX::pattern_matching)).(LRB_simple x_XXX pattern_matching_XXX)) x_e_pattern_matching_list))) ) ; (List.list_all (% b . b) ((List.map (%((x_XXX::value_name),(e_XXX::expr),(pattern_matching_XXX::pattern_matching)). ( letrec_bindings , pattern_matching_XXX , e_XXX ) : Jrecfun) x_e_pattern_matching_list)))|] ==> ( (Expr_letrec letrec_bindings e) , Lab_nil , (substs_value_name_expr (case (substs_x_xs ((List.map (%((x_XXX::value_name),(e_XXX::expr),(pattern_matching_XXX::pattern_matching)).(x_XXX,e_XXX)) x_e_pattern_matching_list))) of substs_x_xs l => l) e ) ) : JR_expr" JR_expr_sequence_ctx_leftI: "[| ( e1 , L , e1' ) : JR_expr|] ==> ( (Expr_sequence e1 e2) , L , (Expr_sequence e1' e2) ) : JR_expr" JR_expr_sequence_raiseI: "[|is_value_of_expr v|] ==> ( (Expr_sequence (Expr_apply (Expr_uprim Uprim_raise) v) e) , Lab_nil , (Expr_apply (Expr_uprim Uprim_raise) v) ) : JR_expr" JR_expr_sequenceI: "[|is_value_of_expr v|] ==> ( (Expr_sequence v e2) , Lab_nil , e2 ) : JR_expr" JR_expr_ifthenelse_ctxI: "[| ( e1 , L , e1' ) : JR_expr|] ==> ( (Expr_ifthenelse e1 e2 e3) , L , (Expr_ifthenelse e1' e2 e3) ) : JR_expr" JR_expr_if_raiseI: "[|is_value_of_expr v|] ==> ( (Expr_ifthenelse (Expr_apply (Expr_uprim Uprim_raise) v) e1 e2) , Lab_nil , (Expr_apply (Expr_uprim Uprim_raise) v) ) : JR_expr" JR_expr_ifthenelse_trueI: " ( (Expr_ifthenelse (Expr_constant CONST_true) e2 e3) , Lab_nil , e2 ) : JR_expr" JR_expr_ifthenelse_falseI: " ( (Expr_ifthenelse (Expr_constant CONST_false) e2 e3) , Lab_nil , e3 ) : JR_expr" JR_expr_match_ctxI: "[| ( e , L , e' ) : JR_expr|] ==> ( (Expr_match e pattern_matching) , L , (Expr_match e' pattern_matching) ) : JR_expr" JR_expr_match_raiseI: "[|is_value_of_expr v|] ==> ( (Expr_match (Expr_apply (Expr_uprim Uprim_raise) v) pattern_matching) , Lab_nil , (Expr_apply (Expr_uprim Uprim_raise) v) ) : JR_expr" JR_expr_match_stepI: "[|is_value_of_expr v ; ( v , pattern_matching , pattern_matching' ) : JRmatching_step|] ==> ( (Expr_match v pattern_matching) , Lab_nil , (Expr_match v pattern_matching') ) : JR_expr" JR_expr_match_successI: "[|is_value_of_expr v ; ( v , pattern_matching , e' ) : JRmatching_success|] ==> ( (Expr_match v pattern_matching) , Lab_nil , e' ) : JR_expr" JR_expr_andI: " ( (Expr_and e1 e2) , Lab_nil , (Expr_ifthenelse e1 e2 (Expr_constant CONST_false)) ) : JR_expr" JR_expr_orI: " ( (Expr_or e1 e2) , Lab_nil , (Expr_ifthenelse e1 (Expr_constant CONST_true) e2) ) : JR_expr" JR_expr_whileI: " ( (Expr_while e1 e2) , Lab_nil , (Expr_ifthenelse e1 (Expr_sequence e2 (Expr_while e1 e2)) (Expr_constant CONST_unit)) ) : JR_expr" JR_expr_for_ctx1I: "[| ( e1 , L , e1' ) : JR_expr|] ==> ( (Expr_for x e1 for_dirn e2 e3) , L , (Expr_for x e1' for_dirn e2 e3) ) : JR_expr" JR_expr_for_raise1I: "[|is_value_of_expr v|] ==> ( (Expr_for x (Expr_apply (Expr_uprim Uprim_raise) v) for_dirn e2 e3) , Lab_nil , (Expr_apply (Expr_uprim Uprim_raise) v) ) : JR_expr" JR_expr_for_ctx2I: "[|is_value_of_expr v1 ; ( e2 , L , e2' ) : JR_expr|] ==> ( (Expr_for x v1 for_dirn e2 e3) , L , (Expr_for x v1 for_dirn e2' e3) ) : JR_expr" JR_expr_for_raise2I: "[|is_value_of_expr v ; is_value_of_expr v'|] ==> ( (Expr_for x v for_dirn (Expr_apply (Expr_uprim Uprim_raise) v') e3) , Lab_nil , (Expr_apply (Expr_uprim Uprim_raise) v') ) : JR_expr" JR_expr_for_to_doI: "[| ( intn1 <= intn2 ) |] ==> ( (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 ) ) )) FD_upto (Expr_constant (CONST_int intn2)) e)) ) : JR_expr" JR_expr_for_to_doneI: "[| ( intn1 <= intn2 ) |] ==> ( (Expr_for x (Expr_constant (CONST_int intn1)) FD_upto (Expr_constant (CONST_int intn2)) e) , Lab_nil , (Expr_constant CONST_unit) ) : JR_expr" JR_expr_for_downto_doI: "[| ( intn2 <= intn1 ) |] ==> ( (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 ) ) )) FD_downto (Expr_constant (CONST_int intn2)) e)) ) : JR_expr" JR_expr_for_downto_doneI: "[| ( intn2 <= intn1 ) |] ==> ( (Expr_for x (Expr_constant (CONST_int intn1)) FD_downto (Expr_constant (CONST_int intn2)) e) , Lab_nil , (Expr_constant CONST_unit) ) : JR_expr" JR_expr_try_ctxI: "[| ( e , L , e' ) : JR_expr|] ==> ( (Expr_try e pattern_matching) , L , (Expr_try e' pattern_matching) ) : JR_expr" JR_expr_try_returnI: "[|is_value_of_expr v|] ==> ( (Expr_try v pattern_matching) , Lab_nil , v ) : JR_expr" JR_expr_try_catchI: "[|is_value_of_expr v|] ==> ( (Expr_try (Expr_apply (Expr_uprim Uprim_raise) v) (PM_pm (pat_exp_list))) , Lab_nil , (Expr_match v (PM_pm (pat_exp_list @ [((PE_inj P_any (Expr_apply (Expr_uprim Uprim_raise) v) ))]))) ) : JR_expr" JR_expr_tuple_ctxI: "[|List.list_all (%v_XXX. is_value_of_expr v_XXX) v_list ; ( e , L , e' ) : JR_expr|] ==> ( (Expr_tuple (e_list @ [(e)] @ v_list)) , L , (Expr_tuple (e_list @ [(e')] @ v_list)) ) : JR_expr" JR_expr_tuple_raiseI: "[|is_value_of_expr v ; List.list_all (%v_XXX. is_value_of_expr v_XXX) v_list|] ==> ( (Expr_tuple (e_list @ [( (Expr_apply (Expr_uprim Uprim_raise) v) )] @ v_list)) , Lab_nil , (Expr_apply (Expr_uprim Uprim_raise) v) ) : JR_expr" JR_expr_constr_ctxI: "[|List.list_all (%v_XXX. is_value_of_expr v_XXX) v_list ; ( e , L , e' ) : JR_expr|] ==> ( (Expr_construct constr (e_list @ [(e)] @ v_list)) , L , (Expr_construct constr (e_list @ [(e')] @ v_list)) ) : JR_expr" JR_expr_constr_raiseI: "[|is_value_of_expr v ; List.list_all (%v_XXX. is_value_of_expr v_XXX) v_list|] ==> ( (Expr_construct constr (e_list @ [( (Expr_apply (Expr_uprim Uprim_raise) v) )] @ v_list)) , Lab_nil , (Expr_apply (Expr_uprim Uprim_raise) v) ) : JR_expr" JR_expr_cons_ctx1I: "[| ( e , L , e' ) : JR_expr|] ==> ( (Expr_cons e0 e) , L , (Expr_cons e0 e') ) : JR_expr" JR_expr_cons_raise1I: "[|is_value_of_expr v|] ==> ( (Expr_cons e (Expr_apply (Expr_uprim Uprim_raise) v) ) , Lab_nil , (Expr_apply (Expr_uprim Uprim_raise) v) ) : JR_expr" JR_expr_cons_ctx2I: "[|is_value_of_expr v ; ( e , L , e' ) : JR_expr|] ==> ( (Expr_cons e v) , L , (Expr_cons e' v) ) : JR_expr" JR_expr_cons_raise2I: "[|is_value_of_expr v ; is_value_of_expr v'|] ==> ( (Expr_cons (Expr_apply (Expr_uprim Uprim_raise) v) v') , Lab_nil , (Expr_apply (Expr_uprim Uprim_raise) v) ) : JR_expr" JR_expr_record_ctxI: "[|List.list_all (%(fn_',v_XXX). is_value_of_expr v_XXX) fn'_v_list ; ( expr , L , expr' ) : JR_expr|] ==> ( (Expr_record ((List.map (%((fn_XXX::field_name),(e_XXX::expr)).((F_name fn_XXX),e_XXX)) fn_e_list) @ [((F_name field_name),expr)] @ (List.map (%((fn_'::field_name),(v_XXX::expr)).((F_name fn_'),v_XXX)) fn'_v_list))) , L , (Expr_record ((List.map (%((fn_XXX::field_name),(e_XXX::expr)).((F_name fn_XXX),e_XXX)) fn_e_list) @ [((F_name field_name),expr')] @ (List.map (%((fn_'::field_name),(v_XXX::expr)).((F_name fn_'),v_XXX)) fn'_v_list))) ) : JR_expr" JR_expr_record_raiseI: "[|is_value_of_expr v ; List.list_all (%(fn_',v_XXX). is_value_of_expr v_XXX) fn'_v_list|] ==> ( (Expr_record ((List.map (%((fn_XXX::field_name),(e_XXX::expr)).((F_name fn_XXX),e_XXX)) fn_e_list) @ [((F_name fn),(Expr_apply (Expr_uprim Uprim_raise) v))] @ (List.map (%((fn_'::field_name),(v_XXX::expr)).((F_name fn_'),v_XXX)) fn'_v_list))) , Lab_nil , (Expr_apply (Expr_uprim Uprim_raise) v) ) : JR_expr" JR_expr_record_with_ctx1I: "[|is_value_of_expr v ; List.list_all (%(fn_',v_XXX). is_value_of_expr v_XXX) fn'_v_list ; ( e , L , e' ) : JR_expr|] ==> ( (Expr_override v ((List.map (%((fn_XXX::field_name),(e_XXX::expr)).((F_name fn_XXX),e_XXX)) fn_e_list) @ [((F_name field_name),e)] @ (List.map (%((fn_'::field_name),(v_XXX::expr)).((F_name fn_'),v_XXX)) fn'_v_list))) , L , (Expr_override v ((List.map (%((fn_XXX::field_name),(e_XXX::expr)).((F_name fn_XXX),e_XXX)) fn_e_list) @ [((F_name field_name),e')] @ (List.map (%((fn_'::field_name),(v_XXX::expr)).((F_name fn_'),v_XXX)) fn'_v_list))) ) : JR_expr" JR_expr_record_with_raise1I: "[|is_value_of_expr v' ; is_value_of_expr v ; List.list_all (%(fn_',v_XXX). is_value_of_expr v_XXX) fn'_v_list|] ==> ( (Expr_override v' ((List.map (%((fn_XXX::field_name),(e_XXX::expr)).((F_name fn_XXX),e_XXX)) fn_e_list) @ [((F_name fn),(Expr_apply (Expr_uprim Uprim_raise) v))] @ (List.map (%((fn_'::field_name),(v_XXX::expr)).((F_name fn_'),v_XXX)) fn'_v_list))) , Lab_nil , (Expr_apply (Expr_uprim Uprim_raise) v) ) : JR_expr" JR_expr_record_with_ctx2I: "[| ( e , L , e' ) : JR_expr|] ==> ( (Expr_override e ((List.map (%((field_name_XXX::field_name),(e_XXX::expr)).((F_name field_name_XXX),e_XXX)) field_name_e_list))) , L , (Expr_override e' ((List.map (%((field_name_XXX::field_name),(e_XXX::expr)).((F_name field_name_XXX),e_XXX)) field_name_e_list))) ) : JR_expr" JR_expr_record_raise_ctx2I: "[|is_value_of_expr v|] ==> ( (Expr_override (Expr_apply (Expr_uprim Uprim_raise) v) ((List.map (%((field_name_XXX::field_name),(e_XXX::expr)).((F_name field_name_XXX),e_XXX)) field_name_e_list))) , Lab_nil , (Expr_apply (Expr_uprim Uprim_raise) v) ) : JR_expr" JR_expr_record_with_manyI: "[|is_value_of_expr v ; is_value_of_expr v' ; List.list_all (%(fn_'',v_''). is_value_of_expr v_'') fn''_v''_list ; List.list_all (%(fn_',v_'). is_value_of_expr v_') fn'_v'_list ; List.list_all (%(fn_XXX,v_XXX). is_value_of_expr v_XXX) fn_v_list ; (length ( ((List.map (%((fn_''::field_name),(v_''::expr)).v_'') fn''_v''_list)) ) >= 1 ) ; (~( (name_fn field_name) mem ((List.map (%((fn_XXX::field_name),(v_XXX::expr)).(name_fn fn_XXX)) fn_v_list)) )) |] ==> ( (Expr_override (Expr_record ((List.map (%((fn_XXX::field_name),(v_XXX::expr)).((F_name fn_XXX),v_XXX)) fn_v_list) @ [((F_name field_name),v)] @ (List.map (%((fn_'::field_name),(v_'::expr)).((F_name fn_'),v_')) fn'_v'_list))) ([((F_name field_name),v')] @ (List.map (%((fn_''::field_name),(v_''::expr)).((F_name fn_''),v_'')) fn''_v''_list))) , Lab_nil , (Expr_override (Expr_record ((List.map (%((fn_XXX::field_name),(v_XXX::expr)).((F_name fn_XXX),v_XXX)) fn_v_list) @ [((F_name field_name),v')] @ (List.map (%((fn_'::field_name),(v_'::expr)).((F_name fn_'),v_')) fn'_v'_list))) ((List.map (%((fn_''::field_name),(v_''::expr)).((F_name fn_''),v_'')) fn''_v''_list))) ) : JR_expr" JR_expr_record_with_1I: "[|is_value_of_expr v ; is_value_of_expr v' ; List.list_all (%(fn_',v_'). is_value_of_expr v_') fn'_v'_list ; List.list_all (%(fn_XXX,v_XXX). is_value_of_expr v_XXX) fn_v_list ; (~( (name_fn field_name) mem ((List.map (%((fn_XXX::field_name),(v_XXX::expr)).(name_fn fn_XXX)) fn_v_list)) )) |] ==> ( (Expr_override (Expr_record ((List.map (%((fn_XXX::field_name),(v_XXX::expr)).((F_name fn_XXX),v_XXX)) fn_v_list) @ [((F_name field_name),v)] @ (List.map (%((fn_'::field_name),(v_'::expr)).((F_name fn_'),v_')) fn'_v'_list))) ([((F_name field_name),v')])) , Lab_nil , (Expr_record ((List.map (%((fn_XXX::field_name),(v_XXX::expr)).((F_name fn_XXX),v_XXX)) fn_v_list) @ [((F_name field_name),v')] @ (List.map (%((fn_'::field_name),(v_'::expr)).((F_name fn_'),v_')) fn'_v'_list))) ) : JR_expr" JR_expr_record_access_ctxI: "[| ( e , L , e' ) : JR_expr|] ==> ( (Expr_field e (F_name field_name)) , L , (Expr_field e' (F_name field_name)) ) : JR_expr" JR_expr_record_access_raiseI: "[|is_value_of_expr v|] ==> ( (Expr_field (Expr_apply (Expr_uprim Uprim_raise) v) (F_name field_name)) , Lab_nil , (Expr_apply (Expr_uprim Uprim_raise) v) ) : JR_expr" JR_expr_record_accessI: "[|is_value_of_expr v ; List.list_all (%(fn_',v_'). is_value_of_expr v_') fn'_v'_list ; List.list_all (%(fn_XXX,v_XXX). is_value_of_expr v_XXX) fn_v_list ; (~( (name_fn field_name) mem ((List.map (%((fn_XXX::field_name),(v_XXX::expr)).(name_fn fn_XXX)) fn_v_list)) )) |] ==> ( (Expr_field (Expr_record ((List.map (%((fn_XXX::field_name),(v_XXX::expr)).((F_name fn_XXX),v_XXX)) fn_v_list) @ [((F_name field_name),v)] @ (List.map (%((fn_'::field_name),(v_'::expr)).((F_name fn_'),v_')) fn'_v'_list))) (F_name field_name)) , Lab_nil , v ) : JR_expr" JR_expr_assert_ctxI: "[| ( e , L , e' ) : JR_expr|] ==> ( (Expr_assert e) , L , (Expr_assert e') ) : JR_expr" JR_expr_assert_raiseI: "[|is_value_of_expr v|] ==> ( (Expr_assert (Expr_apply (Expr_uprim Uprim_raise) v) ) , Lab_nil , (Expr_apply (Expr_uprim Uprim_raise) v) ) : JR_expr" JR_expr_assert_trueI: " ( (Expr_assert (Expr_constant CONST_true)) , Lab_nil , (Expr_constant CONST_unit) ) : JR_expr" JR_expr_assert_falseI: " ( (Expr_assert (Expr_constant CONST_false)) , Lab_nil , (Expr_apply (Expr_uprim Uprim_raise) (Expr_constant (CONST_constr C_assertfailure))) ) : JR_expr" (*defns JRdefn *) consts JRdefn :: "(definitions*program*labelled_arrow*definitions*program) set" inductive JRdefn intros (* defn Rdefn *) Jdefn_let_ctxI: "[|is_definitions_value_of_definitions ds_value ; ( e , L , e' ) : JR_expr|] ==> ( ds_value , (Prog_defs (Ds_cons (D_let (LB_simple pat e)) definitions ) ) , L , ds_value , (Prog_defs (Ds_cons (D_let (LB_simple pat e')) definitions ) ) ) : JRdefn" Jdefn_let_raiseI: "[|is_definitions_value_of_definitions ds_value ; is_value_of_expr v|] ==> ( ds_value , (Prog_defs (Ds_cons (D_let (LB_simple pat (Expr_apply (Expr_uprim Uprim_raise) v))) definitions ) ) , Lab_nil , ds_value , (Prog_raise v) ) : JRdefn" Jdefn_let_matchI: "[|is_definitions_value_of_definitions ds_value ; is_value_of_expr v ; List.list_all (%(x_XXX,v_XXX). is_value_of_expr v_XXX) x_v_list ; ( v , pat , (substs_x_xs (x_v_list)) ) : JM_match|] ==> ( ds_value , (Prog_defs (Ds_cons (D_let (LB_simple pat v)) definitions ) ) , Lab_nil , ds_value , (Prog_defs (substs_value_name_definitions (case (substs_x_xs ((List.map (%((x_XXX::value_name),(v_XXX::expr)).(x_XXX, (remv_tyvar_expr v_XXX ) )) x_v_list))) of substs_x_xs l => l) definitions ) ) ) : JRdefn" Jdefn_let_not_matchI: "[|is_definitions_value_of_definitions ds_value ; is_value_of_expr v ; (~(( v , pat ) : JM_matchP)) |] ==> ( ds_value , (Prog_defs (Ds_cons (D_let (LB_simple pat v)) definitions ) ) , Lab_nil , ds_value , (Prog_raise (Expr_constant (CONST_constr C_matchfailure))) ) : JRdefn" Jdefn_letrecI: "[|is_definitions_value_of_definitions ds_value ; ( letrec_bindings = (LRBs_inj ((List.map (%((x_XXX::value_name),(e_XXX::expr),(pattern_matching_XXX::pattern_matching)).(LRB_simple x_XXX pattern_matching_XXX)) x_e_pattern_matching_list))) ) ; (List.list_all (% b . b) ((List.map (%((x_XXX::value_name),(e_XXX::expr),(pattern_matching_XXX::pattern_matching)). ( letrec_bindings , pattern_matching_XXX , e_XXX ) : Jrecfun) x_e_pattern_matching_list)))|] ==> ( ds_value , (Prog_defs (Ds_cons (D_letrec letrec_bindings) definitions ) ) , Lab_nil , ds_value , (Prog_defs (substs_value_name_definitions (case (substs_x_xs ((List.map (%((x_XXX::value_name),(e_XXX::expr),(pattern_matching_XXX::pattern_matching)).(x_XXX, (remv_tyvar_expr e_XXX ) )) x_e_pattern_matching_list))) of substs_x_xs l => l) definitions ) ) ) : JRdefn" Jdefn_typeI: "[|is_definitions_value_of_definitions ds_value|] ==> ( ds_value , (Prog_defs (Ds_cons (D_type caml_type_definition) definitions ) ) , Lab_nil , (definitions_snoc ds_value (D_type caml_type_definition) ) , (Prog_defs definitions) ) : JRdefn" Jdefn_exnI: "[|is_definitions_value_of_definitions ds_value|] ==> ( ds_value , (Prog_defs (Ds_cons (D_exception exception_definition) definitions ) ) , Lab_nil , (definitions_snoc ds_value (D_exception exception_definition) ) , (Prog_defs definitions) ) : JRdefn" (*defns JSlookup *) consts JSlookup :: "(store*location*expr) set" inductive JSlookup intros (* defn lookup *) JSstlookup_recI: "[| ( st , l , e' ) : JSlookup ; (~( (name_l l) = (name_l l') )) |] ==> ( (( l' , e )# st ) , l , e' ) : JSlookup" JSstlookup_foundI: " ( (( l , e )# st ) , l , e ) : JSlookup" (*defns JRstore *) consts JRstore :: "(store*labelled_arrow*store) set" inductive JRstore intros (* defn store *) JRstore_emptyI: " ( st , Lab_nil , st ) : JRstore" JRstore_lookupI: "[|is_value_of_expr v ; ( st , l , v ) : JSlookup|] ==> ( st , (Lab_deref l v) , st ) : JRstore" JRstore_assignI: "[|is_value_of_expr v ; (! v8. ~(( st' , l , v8) : JSlookup )) |] ==> ( ( st' @[( l , expr )]@ st ) , (Lab_assign l v) , ( st' @[( l , (remv_tyvar_expr v ) )]@ st ) ) : JRstore" JRstore_allocI: "[|is_value_of_expr v ; (! v8. ~(( st , l , v8) : JSlookup )) |] ==> ( st , (Lab_alloc v l) , (( l , (remv_tyvar_expr v ) )# st ) ) : JRstore" (*defns JRtop *) consts JRtop :: "(definitions*program*store*definitions*program*store) set" inductive JRtop intros (* defn top *) JRtop_defsI: "[|is_definitions_value_of_definitions definitions_value ; ( store , L , store' ) : JRstore ; ( definitions_value , program , L , definitions , program' ) : JRdefn|] ==> ( definitions_value , program , store , definitions , program' , store' ) : JRtop" (*defns Jebehaviour *) consts JRB_ebehaviour :: "expr set" inductive JRB_ebehaviour intros (* defn ebehaviour *) JRB_ebehaviour_valueI: "[|is_value_of_expr v|] ==> ( v ) : JRB_ebehaviour" JRB_ebehaviour_reducesI: "[| ( e , L , e' ) : JR_expr|] ==> ( e ) : JRB_ebehaviour" JRB_ebehaviour_raisesI: "[|is_value_of_expr v|] ==> ( (Expr_apply (Expr_uprim Uprim_raise) v) ) : JRB_ebehaviour" (*defns Jdbehaviour *) consts JRB_dbehaviour :: "(definitions*program*store) set" inductive JRB_dbehaviour intros (* defn dbehaviour *) JRB_behaviour_valueI: "[|is_definitions_value_of_definitions definitions_value|] ==> ( definitions_value , (Prog_defs Ds_nil) , store ) : JRB_dbehaviour" JRB_behaviour_reducesI: "[|is_definitions_value_of_definitions definitions_value ; ( definitions_value , program , store , definitions' , program' , store' ) : JRtop|] ==> ( definitions_value , program , store ) : JRB_dbehaviour" JRB_behaviour_raisesI: "[|is_definitions_value_of_definitions definitions_value ; is_value_of_expr v|] ==> ( definitions_value , (Prog_raise v) , store ) : JRB_dbehaviour" end