Skip to content

Commit

Permalink
Streamline inference cv translation
Browse files Browse the repository at this point in the history 
Co-authored-by: Magnus Myreen <myreen@chalmers.se>
  • Loading branch information
@hrutvik @myreen
hrutvik and myreen committed Mar 14, 2024
1 parent 52dfd30 commit b02d95b
Showing 1 changed file with 13 additions and 157 deletions.
170 changes: 13 additions & 157 deletions compiler/inference/infer_cvScript.sml
View file
Expand Up @@ -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;

Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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) =
Expand All @@ -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
Expand All @@ -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 =
Expand Down Expand Up @@ -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

Expand Down

0 comments on commit b02d95b

Please sign in to comment.