diff --git a/compiler/inference/infer_cvScript.sml b/compiler/inference/infer_cvScript.sml index 89ad1eaf3b..b5798f4530 100644 --- a/compiler/inference/infer_cvScript.sml +++ b/compiler/inference/infer_cvScript.sml @@ -56,19 +56,7 @@ val map_t_walkstar_pre = cv_trans_pre map_t_walkstar_def; val apply_subst_list_pre = cv_trans_pre (apply_subst_list_def |> expand |> SRULE [read_def,map_t_walkstar_thm]); -Definition add_parens_list_def: - add_parens_list n [] = [] ∧ - add_parens_list n (x::xs) = add_parens n x :: add_parens_list n xs -End - -Theorem add_parens_list: - MAP (add_parens n) xs = add_parens_list n xs -Proof - Induct_on ‘xs’ \\ gvs [add_parens_list_def] -QED - val _ = cv_trans infer_tTheory.add_parens_def; -val _ = cv_trans add_parens_list_def; val res = cv_trans_pre infer_tTheory.get_tyname_def; @@ -111,7 +99,6 @@ Proof QED val res = expand infer_tTheory.inf_type_to_string_rec_def - |> SRULE [add_parens_list] |> cv_auto_trans; val res = infer_tTheory.inf_type_to_string_def |> cv_trans; @@ -209,57 +196,15 @@ QED val res = cv_trans (check_type_definition_expand |> SRULE [GSYM MAP_MAP_o]) -Definition map_infer_type_subst_def: - map_infer_type_subst s [] = [] ∧ - map_infer_type_subst s (x::xs) = - infer_type_subst s x :: map_infer_type_subst s xs -End - -Triviality map_infer_type_subst_eq: - map_infer_type_subst s xs = MAP (infer_type_subst s) xs -Proof - Induct_on ‘xs’ \\ gvs [map_infer_type_subst_def] -QED - -val _ = cv_trans map_infer_type_subst_def; - -val infer_p_pre = cv_trans_pre - (infer_p_expand |> SRULE [GSYM map_infer_type_subst_eq]); +val infer_p_pre = cv_auto_trans_pre infer_p_expand; val constrain_op_pre = cv_trans_pre constrain_op_expand; -Definition map1_def: - map1 [] = [] ∧ - map1 ((n,t)::xs) = (n,0n,t) :: map1 xs -End - -Triviality map1_eq: - map1 xs = MAP (λ(n,t). (n,0n,t)) xs -Proof - Induct_on ‘xs’ \\ gvs [map1_def,FORALL_PROD] -QED - -val _ = cv_trans map1_def - -Definition map2_def: - map2 ((f,x,e)::xs) (uvar::ys) = (f,0n,uvar) :: map2 xs ys ∧ - map2 _ _ = [] -End - -Triviality map2_eq: - ∀xs ys. map2 xs ys = MAP2 (λ(f,x,e) uvar. (f,0n,uvar)) xs ys -Proof - Induct \\ Cases_on ‘ys’ \\ gvs [map2_def,FORALL_PROD] -QED - -val _ = cv_trans map2_def; val _ = cv_trans nsBind_def; val _ = cv_trans nsOptBind_def; -val infer_e_pre = cv_trans_pre_rec - (infer_e_expand |> SRULE [GSYM map_infer_type_subst_eq, - GSYM map1_eq, GSYM map2_eq, - namespaceTheory.alist_to_ns_def]) +val infer_e_pre = cv_auto_trans_pre_rec + (infer_e_expand |> SRULE [namespaceTheory.alist_to_ns_def]) (WF_REL_TAC ‘measure $ λx. case x of | INL (_,_,e,_) => cv_sum_depth e | INR (INL (_,_,es,_)) => cv_sum_depth es @@ -294,62 +239,6 @@ QED val _ = cv_trans alist_to_ns_def; -Definition infer_d_map_1_def: - infer_d_map_1 y [] = [] ∧ - infer_d_map_1 y (t::ts) = (y,t) :: infer_d_map_1 y ts -End - -val _ = cv_trans infer_d_map_1_def - -Theorem infer_d_map_1_eq: - MAP (λt. (y,t)) ts = infer_d_map_1 y ts -Proof - Induct_on ‘ts’ \\ gvs [infer_d_map_1_def] -QED - -Definition MAP_Tvar_def: - MAP_Tvar [] = [] ∧ - MAP_Tvar (e::es) = Tvar e :: MAP_Tvar es -End - -val _ = cv_trans MAP_Tvar_def - -Theorem MAP_Tvar_eq: - MAP Tvar ts = MAP_Tvar ts -Proof - Induct_on ‘ts’ \\ gvs [MAP_Tvar_def] -QED - -Definition infer_d_map_2_def: - infer_d_map_2 ((tvs,tn,ctors)::xs) (i::ys) = - (tn,tvs,Tapp (MAP_Tvar tvs) i) :: infer_d_map_2 xs ys ∧ - infer_d_map_2 _ _ = [] -End - -val _ = cv_trans infer_d_map_2_def - -Theorem infer_d_map_2_eq: - ∀xs ys. - MAP2 (λ(tvs,tn,ctors) i. (tn,tvs,Tapp (MAP_Tvar tvs) i)) xs ys = - infer_d_map_2 xs ys -Proof - Induct \\ Cases_on ‘ys’ \\ gvs [infer_d_map_2_def,FORALL_PROD] -QED - -Definition infer_d_map_3_def: - infer_d_map_3 y ((f,x,e)::xs) (t::ys) = (f,y,t) :: infer_d_map_3 y xs ys ∧ - infer_d_map_3 y _ _ = [] -End - -val _ = cv_trans infer_d_map_3_def - -Theorem infer_d_map_3_eq: - ∀xs ys. - MAP2 (λ(f,x,e) t. (f,y,t)) xs ys = infer_d_map_3 y xs ys -Proof - Induct \\ Cases_on ‘ys’ \\ gvs [infer_d_map_3_def,FORALL_PROD] -QED - Definition type_name_subst_1_def: type_name_subst_1 tenvT (Atvar tv) = Tvar tv ∧ type_name_subst_1 tenvT (Attup ts) = @@ -370,47 +259,17 @@ End val _ = cv_auto_trans type_name_subst_1_def; Theorem type_name_subst_1_eq: - (∀t. type_name_subst tenvT t = type_name_subst_1 tenvT t) ∧ - (∀ts. MAP (type_name_subst tenvT) ts = type_name_subst_list_1 tenvT ts) + type_name_subst tenvT = type_name_subst_1 tenvT ∧ + MAP (type_name_subst tenvT) = type_name_subst_list_1 tenvT Proof - ho_match_mp_tac ast_t_induction \\ rw [] + simp[FUN_EQ_THM] + \\ ho_match_mp_tac ast_t_induction \\ rw [] \\ gvs [type_name_subst_1_def,GSYM type_subst_alist_to_fmap, typeSystemTheory.type_name_subst_def] \\ gvs [SF ETA_ss] QED -Definition MAP_type_name_subst_def: - MAP_type_name_subst tenvT [] = [] ∧ - MAP_type_name_subst tenvT (x::xs) = - type_name_subst_1 tenvT x :: MAP_type_name_subst tenvT xs -End - -val _ = cv_trans MAP_type_name_subst_def; - -Theorem MAP_type_name_subst_eq: - MAP (type_name_subst tenvT) ts = MAP_type_name_subst tenvT ts -Proof - Induct_on ‘ts’ \\ gvs [MAP_type_name_subst_def,GSYM type_name_subst_1_eq] -QED - -Definition MAP_MAP_type_name_subst_def: - MAP_MAP_type_name_subst id tenvT tvs [] = [] ∧ - MAP_MAP_type_name_subst id tenvT tvs ((cn,ts)::xs) = - (cn,tvs,MAP_type_name_subst tenvT ts,id) :: - MAP_MAP_type_name_subst id tenvT tvs xs -End - -val _ = cv_trans MAP_MAP_type_name_subst_def - -Theorem MAP_MAP_type_name_subst_eq: - MAP (λ(cn,ts). (cn,tvs,MAP_type_name_subst tenvT ts,id)) xs = - MAP_MAP_type_name_subst id tenvT tvs xs -Proof - Induct_on ‘xs’ \\ gvs [FORALL_PROD,MAP_MAP_type_name_subst_def] -QED - -val res = cv_trans_pre (typeSystemTheory.build_ctor_tenv_def - |> SRULE [namespaceTheory.alist_to_ns_def, namespaceTheory.nsEmpty_def, - MAP_type_name_subst_eq,MAP_MAP_type_name_subst_eq]); +val res = cv_auto_trans_pre (typeSystemTheory.build_ctor_tenv_def + |> SRULE [type_name_subst_1_eq, namespaceTheory.alist_to_ns_def, namespaceTheory.nsEmpty_def]) Theorem build_ctor_tenv_pre[cv_pre,local]: ∀a0 a1 a2. build_ctor_tenv_pre a0 a1 a2 @@ -420,12 +279,9 @@ QED val _ = cv_trans namespaceTheory.nsSing_def; -val infer_d_pre = cv_trans_pre - (infer_d_expand - |> SRULE [exp_is_value_eq,infer_d_map_1_eq,nsEmpty_def, - extend_dec_ienv_def, - infer_d_map_2_eq, infer_d_map_3_eq,init_state_def, - GSYM map1_eq, GSYM map2_eq, MAP_Tvar_eq]); +val infer_d_pre = cv_auto_trans_pre + (infer_d_expand |> + SRULE [exp_is_value_eq, nsEmpty_def, extend_dec_ienv_def, init_state_def]); Definition call_infer_def: call_infer ienv prog start_id = @@ -520,7 +376,7 @@ Proof \\ imp_res_tac type_name_check_sub_success \\ gvs [] \\ gvs [type_name_check_subst_success,IMP_infer_p_pre] \\ imp_res_tac infer_p_wfs - \\ gvs [GSYM map1_eq,alist_to_ns_def] + \\ gvs [alist_to_ns_def, LAMBDA_PROD] \\ irule IMP_constrain_op_pre \\ gvs [] QED