From 72a59e5e4feeebed27a3368055087aa2ab56242c Mon Sep 17 00:00:00 2001
From: Hrutvik Kanabar <hrutvikkanabar@yahoo.co.uk>
Date: Tue, 5 Mar 2024 21:44:40 +0000
Subject: [PATCH] Update some more proofs

Progress towards #73
---
 .../proofs/pure_dead_letProofScript.sml       |  6 ++++
 .../pure_demands_analysisProofScript.sml      |  7 ++--
 .../passes/proofs/pure_freshenProofScript.sml | 15 ++++++++-
 .../proofs/pure_inline_cexpProofScript.sml    | 21 ++++++++++++
 .../proofs/pure_letrec_cexpProofScript.sml    | 10 +++++-
 .../backend/passes/pure_dead_letScript.sml    |  5 ++-
 .../passes/pure_demands_analysisScript.sml    |  2 ++
 .../backend/passes/pure_freshenScript.sml     |  8 ++++-
 .../backend/passes/pure_inline_cexpScript.sml |  7 +++-
 .../backend/passes/pure_letrec_cexpScript.sml | 33 +++++++++++--------
 .../backend/passes/pure_to_thunkScript.sml    |  1 +
 11 files changed, 94 insertions(+), 21 deletions(-)

diff --git a/compiler/backend/passes/proofs/pure_dead_letProofScript.sml b/compiler/backend/passes/proofs/pure_dead_letProofScript.sml
index 0149bbc9..5e857c9d 100644
--- a/compiler/backend/passes/proofs/pure_dead_letProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_dead_letProofScript.sml
@@ -285,6 +285,9 @@ Proof
       gvs[cepat_vars_l_correct] >> metis_tac[neq_some_unit]
       )
     )
+  >- ( (* Annot fvs_ok *)
+    imp_res_tac fvs_ok_imp >> gvs[fvs_ok_def, fv_set_ok_def]
+    )
 QED
 
 Theorem dead_let_cns_arities:
@@ -440,6 +443,9 @@ Proof
       gvs[EVERY_MAP, EVERY_MEM, FORALL_PROD] >> metis_tac[]
       )
     )
+  >- (
+    once_rewrite_tac[type_tcexp_cases] >> simp[]
+    )
 QED
 
 
diff --git a/compiler/backend/passes/proofs/pure_demands_analysisProofScript.sml b/compiler/backend/passes/proofs/pure_demands_analysisProofScript.sml
index 4e85c892..95463e04 100644
--- a/compiler/backend/passes/proofs/pure_demands_analysisProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_demands_analysisProofScript.sml
@@ -1778,8 +1778,11 @@ Proof
   >- (rw [empty_thm, TotOrd_compare]
       \\ irule find_fixpoint_refl)
   >~[‘Annot _ _ _’]
-  >- (rw [empty_thm, TotOrd_compare]
-      \\ irule find_fixpoint_refl)
+  >- (
+    simp[exp_of_def, cexp_size_def] >> strip_tac >>
+    first_x_assum $ qspec_then `cexp_size (K 0) c` mp_tac >> simp[] >>
+    disch_then $ qspec_then `c` mp_tac >> simp[]
+    )
 QED
 
 Theorem test_list_rel_soundness:
diff --git a/compiler/backend/passes/proofs/pure_freshenProofScript.sml b/compiler/backend/passes/proofs/pure_freshenProofScript.sml
index 7c2bd8f1..8479c6e1 100644
--- a/compiler/backend/passes/proofs/pure_freshenProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_freshenProofScript.sml
@@ -1154,7 +1154,8 @@ Theorem avoid_ok_simps[simp]:
     avoid_ok avoid ce ∧
     explode x ∈ set_of avoid ∧
     EVERY (λ(cn,pvs,ce). set (MAP explode pvs) ⊆ set_of avoid ∧ avoid_ok avoid ce) css ∧
-    (∀cnars ce. usopt = SOME (cnars,ce) ⇒ avoid_ok avoid ce))
+    (∀cnars ce. usopt = SOME (cnars,ce) ⇒ avoid_ok avoid ce)) ∧
+  (avoid_ok avoid (Annot c annot ce) ⇔ avoid_ok avoid ce)
 Proof
   rw[avoid_ok_def, exp_of_def, EVERY_MEM, allvars_Apps, allvars_Lams, allvars_rows_of]
   >- (simp[BIGUNION_SUBSET, MEM_MAP, PULL_EXISTS] >> metis_tac[])
@@ -1325,6 +1326,9 @@ Proof
     >- (strip_tac >> gvs[SUBSET_DEF, avoid_ok_def]) >>
     gvs[EVERY_MEM, FORALL_PROD, avoid_ok_def, SUBSET_DEF, EXTENSION] >> metis_tac[]
     )
+  >- (
+    rpt (pairarg_tac >> gvs[]) >> res_tac
+    )
   >- ( (* list case *)
     rpt (pairarg_tac >> gvs[]) >>
     last_x_assum drule_all >> strip_tac >> drule $ cj 1 freshen_aux_mono >>
@@ -2055,6 +2059,9 @@ Proof
       metis_tac[]
       )
     )
+  >- (
+    rpt (pairarg_tac >> gvs[]) >> gvs[exp_of_def, cexp_wf_def]
+    )
   >- ( (* list case *)
     rpt (pairarg_tac >> gvs[]) >>
     rename1 `freshen_aux_list _ ces1 avoid1' = (ces2,_)` >>
@@ -2489,6 +2496,12 @@ Proof
         )
       )
     )
+  >- ( (* Annot *)
+    rpt (pairarg_tac >> gvs[]) >> gvs[tcexp_of_def] >>
+    qpat_x_assum `type_tcexp _ _ _ _ _ _` mp_tac >>
+    once_rewrite_tac[type_tcexp_cases] >> rw[] >>
+    first_x_assum irule >> simp[PULL_EXISTS] >> rpt $ goal_assum $ drule_at Any
+    )
   >- ( (* NestedCase *)
     qpat_x_assum `type_tcexp _ _ _ _ _ _` mp_tac >>
     simp[Once type_tcexp_cases]
diff --git a/compiler/backend/passes/proofs/pure_inline_cexpProofScript.sml b/compiler/backend/passes/proofs/pure_inline_cexpProofScript.sml
index b93a90e1..b4da62c4 100644
--- a/compiler/backend/passes/proofs/pure_inline_cexpProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_inline_cexpProofScript.sml
@@ -697,6 +697,12 @@ Proof
   \\ gvs [SUBSET_DEF]
 QED
 
+Theorem avoid_set_ok_Annot:
+  avoid_set_ok ns (Annot c annot e) ⇔ avoid_set_ok ns e
+Proof
+  rw[avoid_set_ok_def, exp_of_def]
+QED
+
 fun avoid_set_ok_lemma () = inline_ind
   |> Q.SPEC ‘λm ns cl h x. ∀t ns1.
     (inline m ns cl h x) = (t, ns1) ∧
@@ -823,6 +829,11 @@ Proof
     \\ irule Case_lemma \\ gvs []
     \\ last_x_assum $ irule_at $ Pos hd
     \\ fs [] \\ metis_tac [SUBSET_TRANS])
+  >~ [`Annot`]
+  >- (
+    rpt (pairarg_tac >> gvs[]) >>
+    gvs[fake_avoid_set_ok_def, avoid_set_ok_Annot]
+    )
   \\ rpt (pairarg_tac \\ gvs [AllCaseEqs()])
   \\ gvs [fake_avoid_set_ok_def]
   \\ last_x_assum $ irule_at Any
@@ -1330,6 +1341,11 @@ Proof
       (rpt $ pop_assum kall_tac \\ gvs [LAMBDA_PROD])
     \\ gvs [MAP_MAP_o,o_DEF]
     \\ gvs [SUBSET_DEF] \\ metis_tac [])
+  >~ [`Annot`]
+  >- (
+    gvs[inline_def] >> rpt (pairarg_tac >> gvs[]) >>
+    gvs[avoid_set_ok_Annot, exp_of_def, cexp_wf_def, cns_arities_def]
+    )
   \\ gvs [inline_def]
   \\ rpt (pairarg_tac \\ gvs [AllCaseEqs()])
   \\ gvs [block_def] \\ gvs [SUBSET_DEF]
@@ -2375,6 +2391,11 @@ Proof
   >~ [`NestedCase _ _ _ _ _ _`] >- (
     gvs [NestedCase_free_def]
   )
+  >~ [`Annot`]
+  >- (
+    gvs[inline_def] >> rpt (pairarg_tac >> gvs[]) >>
+    gvs[exp_of_def, cexp_wf_def, letrecs_distinct_def, avoid_set_ok_Annot]
+    )
   >~ [`LIST_REL _ [] _`] >- (
     gvs [inline_def]
   )
diff --git a/compiler/backend/passes/proofs/pure_letrec_cexpProofScript.sml b/compiler/backend/passes/proofs/pure_letrec_cexpProofScript.sml
index d2c9ea88..8c4b37cc 100644
--- a/compiler/backend/passes/proofs/pure_letrec_cexpProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_letrec_cexpProofScript.sml
@@ -215,7 +215,8 @@ Definition fvs_ok_def:
      OPTION_ALL (λ(_,e). fvs_ok e) eopt) ∧
   fvs_ok (NestedCase c g gv p e pes) =
     (fv_set_ok (NestedCase c g gv p e pes) ∧
-     fvs_ok g ∧ fvs_ok e ∧ EVERY (λ(p,e). fvs_ok e) pes)
+     fvs_ok g ∧ fvs_ok e ∧ EVERY (λ(p,e). fvs_ok e) pes) ∧
+  fvs_ok (Annot c annot e) = (fv_set_ok (Annot c annot e) ∧ fvs_ok e)
 Termination
   WF_REL_TAC `measure $ cexp_size (K 0)` >>
   simp[cexp_size_eq, DISJ_IMP_THM, FORALL_AND_THM] >> rpt strip_tac >>
@@ -390,6 +391,10 @@ Proof
       simp[cepat_vars_l_correct] >>
       strip_tac >> disj2_tac >> first_assum $ irule_at Any >>
       simp[lookup_list_delete, cepat_vars_l_correct])
+  >- (
+    imp_res_tac fvs_ok_imp >> gvs[fv_set_ok_def] >>
+    rw[fvs_ok_def, fv_set_ok_def, get_info_def]
+    )
 QED
 
 Triviality letrec_recurse_IfDisj:
@@ -1037,6 +1042,9 @@ Proof
       gvs[EVERY_MAP, EVERY_MEM, FORALL_PROD] >> metis_tac[]
       )
     )
+  >- (
+    once_rewrite_tac[type_tcexp_cases] >> simp[]
+    )
 QED
 
 Theorem clean_all_cexp_cexp_wf:
diff --git a/compiler/backend/passes/pure_dead_letScript.sml b/compiler/backend/passes/pure_dead_letScript.sml
index 9a3dc043..a892f1ba 100644
--- a/compiler/backend/passes/pure_dead_letScript.sml
+++ b/compiler/backend/passes/pure_dead_letScript.sml
@@ -54,7 +54,10 @@ Definition dead_let_def:
         c'    = union (get_info ce') $ combin$C delete x $ list_union $
                   MAP (λ(p,ce). list_delete (get_info ce) (cepat_vars_l p)) $
                     (p,pce')::pces'
-    in NestedCase c' ce' x p pce' pces')
+    in NestedCase c' ce' x p pce' pces') ∧
+  dead_let (Annot c annot ce) =
+    let ce'   = dead_let ce
+    in Annot (get_info ce') annot ce'
 Termination
   WF_REL_TAC `measure $ cexp_size (K 0)`
 End
diff --git a/compiler/backend/passes/pure_demands_analysisScript.sml b/compiler/backend/passes/pure_demands_analysisScript.sml
index 8446c9bc..65b8bd00 100644
--- a/compiler/backend/passes/pure_demands_analysisScript.sml
+++ b/compiler/backend/passes/pure_demands_analysisScript.sml
@@ -207,6 +207,8 @@ Definition fixpoint1_def:
                                               else m) (empty compare) hd in
                 (union demands_e (delete m n), NONE))) ∧
 
+  (fixpoint1 c (Annot d annot e) fds = fixpoint1 c e fds) ∧
+
   (fixpoint1 c e fds = (mlmap$empty mlstring$compare, NONE))
 Termination
   WF_REL_TAC ‘measure $ (cexp_size (K 0)) o (FST o SND)’ \\ rw []
diff --git a/compiler/backend/passes/pure_freshenScript.sml b/compiler/backend/passes/pure_freshenScript.sml
index 6a5e04ce..3ea8a4e0 100644
--- a/compiler/backend/passes/pure_freshenScript.sml
+++ b/compiler/backend/passes/pure_freshenScript.sml
@@ -180,6 +180,11 @@ Definition freshen_aux_def:
     return (Case d ce' v' css' usopt')
   od ∧
 
+  freshen_aux varmap (Annot d annot ce) = do
+    ce' <- freshen_aux varmap ce;
+    return (Annot d annot ce')
+  od ∧
+
   freshen_aux _ ce = return ce ∧ (* NestedCase not handled *)
 
   (* List form *)
@@ -222,7 +227,8 @@ Definition boundvars_of_def:
     var_union (insert_var (boundvars_of ce) x) $
     var_union (insert_vars (boundvars_of pce) (cepat_vars_l p)) $
     FOLDR (λ(p,ce) s. var_union s $ insert_vars (boundvars_of ce) (cepat_vars_l p))
-      empty_vars pces
+      empty_vars pces ∧
+  boundvars_of (Annot d annot ce) = boundvars_of ce
 Termination
   WF_REL_TAC `measure $ cexp_size (K 0)`
 End
diff --git a/compiler/backend/passes/pure_inline_cexpScript.sml b/compiler/backend/passes/pure_inline_cexpScript.sml
index 4fb53578..b9a84c52 100644
--- a/compiler/backend/passes/pure_inline_cexpScript.sml
+++ b/compiler/backend/passes/pure_inline_cexpScript.sml
@@ -147,6 +147,9 @@ Definition inline_def:
      in (Case a e1 v (MAP2 (λ(v, vs, _) e. (v, vs, e)) bs bs2) f3, ns3)) ∧
   inline m ns cl h (NestedCase a e v p e' bs) =
     (NestedCase a e v p e' bs, ns) ∧
+  inline m ns cl h (Annot a annot e) =
+    (let (e1, ns1) = inline m ns cl h e
+     in (Annot a annot e1, ns1)) ∧
   inline_list m ns cl h [] = ([], ns) ∧
   inline_list m ns cl h (e::es) =
     (let (e1, ns1) = inline m ns cl h e in
@@ -198,7 +201,9 @@ Definition tree_size_heuristic_rec_def:
       | SOME (vs, e) => tree_size_heuristic_rec n1 e) ∧
   tree_size_heuristic_rec n (NestedCase a e v p e' bs) =
     (let n1 = FOLDL (λa (p, e). if a < 0 then a else tree_size_heuristic_rec a e) (n - 1) bs
-    in if n1 < 0 then n1 else tree_size_heuristic_rec n1 e')
+    in if n1 < 0 then n1 else tree_size_heuristic_rec n1 e') ∧
+  tree_size_heuristic_rec n (Annot a annot e) =
+    tree_size_heuristic_rec (n - 1) e
 Termination
   WF_REL_TAC ‘measure (λx. case x of
     | (n, e) => cexp_size (K 0) e)’
diff --git a/compiler/backend/passes/pure_letrec_cexpScript.sml b/compiler/backend/passes/pure_letrec_cexpScript.sml
index fdabee4e..7a7cc317 100644
--- a/compiler/backend/passes/pure_letrec_cexpScript.sml
+++ b/compiler/backend/passes/pure_letrec_cexpScript.sml
@@ -28,7 +28,8 @@ Definition letrec_recurse_cexp_def:
   letrec_recurse_cexp f (NestedCase c g gv p e pes) =
     NestedCase c (letrec_recurse_cexp f g) gv p
                (letrec_recurse_cexp f e)
-               (MAP (λ(p,e). (p, letrec_recurse_cexp f e)) pes)
+               (MAP (λ(p,e). (p, letrec_recurse_cexp f e)) pes) ∧
+  letrec_recurse_cexp f (Annot c annot e) = Annot c annot (letrec_recurse_cexp f e)
 Termination
   WF_REL_TAC `measure $ cexp_size (K 0) o SND`
 End
@@ -72,18 +73,21 @@ Definition letrec_recurse_fvs_def:
                     MAP (λ(cn,vs,e). list_delete (get_info e) vs) ys')) n)
     in Case c' e' n ys' eopt') ∧
   letrec_recurse_fvs f (NestedCase c g gv p e pes) =
-    let g' = letrec_recurse_fvs f g ;
-        e' = letrec_recurse_fvs f e ;
-        pes' = MAP (λ(p,e). (p, letrec_recurse_fvs f e)) pes ;
-        c' = union (get_info g')
-                   (delete
-                    (list_union
-                     (MAP (λ(p,e).
-                             list_delete (get_info e) (cepat_vars_l p))
-                          ((p,e')::pes')))
-                    gv)
-    in
-      NestedCase c' g' gv p e' pes'
+    (let g' = letrec_recurse_fvs f g ;
+         e' = letrec_recurse_fvs f e ;
+         pes' = MAP (λ(p,e). (p, letrec_recurse_fvs f e)) pes ;
+         c' = union (get_info g')
+                    (delete
+                     (list_union
+                      (MAP (λ(p,e).
+                              list_delete (get_info e) (cepat_vars_l p))
+                           ((p,e')::pes')))
+                     gv)
+     in
+       NestedCase c' g' gv p e' pes') ∧
+  letrec_recurse_fvs f (Annot c annot e) =
+    (let e' = letrec_recurse_fvs f e in Annot (get_info e') annot e')
+
 Termination
   WF_REL_TAC `measure $ cexp_size (K 0) o SND`
 End
@@ -176,7 +180,8 @@ Definition init_sets_def:
   init_sets (NestedCase c g gv p e pes) =
     NestedCase empty (init_sets g) gv p
                (init_sets e)
-               (MAP (λ(p,e). (p, init_sets e)) pes)
+               (MAP (λ(p,e). (p, init_sets e)) pes) ∧
+  init_sets (Annot c annot e) = Annot empty annot (init_sets e)
 Termination
   WF_REL_TAC `measure $ cexp_size (K 0)`
 End
diff --git a/compiler/backend/passes/pure_to_thunkScript.sml b/compiler/backend/passes/pure_to_thunkScript.sml
index 1ff55ec6..d7529699 100644
--- a/compiler/backend/passes/pure_to_thunkScript.sml
+++ b/compiler/backend/passes/pure_to_thunkScript.sml
@@ -125,6 +125,7 @@ Definition to_thunk_def:
             ((Let (SOME v) (mk_delay flag x) $
               Let (SOME w) (Force (Var v)) $
                Case w (MAP2 (λ(c,n,_) y. (c,n,y)) ys rs) (SOME (a,y))),s)) ∧
+  to_thunk flag s (Annot c annot e) = to_thunk flag s e ∧
   to_thunk flag s (NestedCase c g gv p e pes) = to_thunk flag s e ∧
   to_thunk_list flag s [] = ([],s) ∧
   to_thunk_list flag s (x::xs) =