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