Merge pull request #66 from CakeML/clean-up-moves

Clean up moves

compiler/backend/languages/env_cexpScript.sml

@@ -80,4 +80,24 @@ Termination
   WF_REL_TAC `measure cexp_size`
 End
 
+Definition Lams_def:
+  Lams [] x = x ∧
+  Lams (y::ys) x = Lam y (Lams ys x)
+End
+
+Definition Apps_def:
+  Apps x [] = x ∧
+  Apps x (y::ys) = Apps (App x y) ys
+End
+
+Definition dest_Delay_def:
+  dest_Delay (Delay x) = SOME x ∧
+  dest_Delay _ = NONE
+End
+
+Definition dest_Lam_def:
+  dest_Lam (Lam v x) = SOME (v,x) ∧
+  dest_Lam _ = NONE
+End
+
 val _ = export_theory();

compiler/backend/languages/properties/env_cexp_lemmasScript.sml

@@ -7,6 +7,8 @@ open pure_miscTheory env_cexpTheory ;
 val _ = new_theory "env_cexp_lemmas";
 
 val freevars_def = envLangTheory.freevars_def;
+val Lams_def = envLangTheory.Lams_def;
+val Apps_def = envLangTheory.Apps_def;
 
 Theorem freevars_Lams[simp]:
   ∀vs e. freevars (Lams vs e) = freevars e DIFF set vs
@@ -106,4 +108,3 @@ QED
  *)
 
 val _ = export_theory();
-

compiler/backend/languages/pure_cexpScript.sml

@@ -105,11 +105,31 @@ Theorem better_cexp_induction =
 
 val _ = TypeBase.update_induction better_cexp_induction
 
-Definition dest_var_def[simp]:
+Definition is_Lam_def:
+  is_Lam (Lam a vs e) = T ∧
+  is_Lam _ = F
+End
+
+Definition Lets_def:
+  Lets a ((v,e)::xs) e1 = Let a v e (Lets a xs e1) ∧
+  Lets a _ e = e
+End
+
+Definition dest_var_def[simp]: (* TODO: uppercase var *)
   dest_var (Var _ vnm) = SOME vnm ∧
   dest_var _ = NONE
 End
 
+Definition get_Var_name_def: (* TODO: replace by dest_var *)
+  get_Var_name (Var a v) = (SOME v) ∧
+  get_Var_name _ = NONE
+End
+
+Definition eq_Var_def:
+  eq_Var f (Var a v) = (f = v:mlstring) ∧
+  eq_Var f _ = F
+End
+
 Definition dest_nestedcase_def[simp]:
   dest_nestedcase (NestedCase _ g gv p e pes) = SOME (g, gv, (p,e)::pes) ∧
   dest_nestedcase _ = NONE

compiler/backend/languages/relations/pure_presScript.sml

@@ -16,7 +16,6 @@ open pure_expTheory pure_valueTheory pure_evalTheory pure_eval_lemmasTheory
      pure_tcexpTheory pure_tcexp_lemmasTheory
      pure_typingTheory pure_typingPropsTheory;
 
-
 val exp_of_def = pureLangTheory.exp_of_def;
 val rows_of_def = pureLangTheory.rows_of_def;
 val lets_for_def = pureLangTheory.lets_for_def;
@@ -155,9 +154,11 @@ Inductive bidir:
   (* typing: => direction proved
              <= direction has mismatching free variables *)
 [~App_Lam:]
-  (∀a b c vs x.
-    bidir (App a (Lam b vs x) (MAP (Var c) vs))
-          x) ∧
+  (∀a b c vs x ws.
+    set vs ⊆ set ws ∧ vs ≠ []
+    ⇒
+    bidir (Lam a ws (App b (Lam c vs x) (MAP (Var d) vs)))
+          (Lam a ws x)) ∧
 [~Letrec_Lam:]
   (∀a b c d vs l e.
     EVERY (λ(v,e). DISJOINT (IMAGE explode (set vs)) (freevars (exp_of e)) ∧
@@ -361,7 +362,6 @@ Proof
   >~ [`spec_arg`]
   >- cheat (* TODO specialisation *) >>
   rw[] >> eq_tac >> rw[] >> gvs[EVERY_MEM, FORALL_PROD] >> res_tac
-  >- cheat (* App_Lam - not true due to potentially empty `vs` *)
 QED
 
 Theorem pres_imp_wf_preserved:
@@ -638,6 +638,7 @@ Proof
     \\ irule Letrec_eq_Let_Letrec)
   >-
    (fs [exp_of_def,MAP_MAP_o,o_DEF]
+    \\ irule exp_eq_Lams_cong
     \\ ‘MAP (λx. Var (explode x) : exp) vs = MAP Var (MAP explode vs)’ by
           fs [MAP_MAP_o,o_DEF]
     \\ simp [Apps_Lams_Vars])
@@ -678,15 +679,6 @@ Proof
                   pure_demandTheory.Letrec_unfold \\ fs []
     \\ gvs [EL_MAP] \\ disch_then drule \\ fs []
     \\ disch_then $ qspec_then ‘T’ mp_tac
-    \\ impl_tac
-    >-
-     (gvs [MAP_MAP_o,o_DEF,LAMBDA_PROD]
-      \\ qpat_x_assum `ALL_DISTINCT _` mp_tac
-      \\ qmatch_goalsub_abbrev_tac ‘_ xs ⇒ _ ys’
-      \\ qsuff_tac ‘xs = MAP implode ys’ \\ gvs []
-      >- metis_tac [ALL_DISTINCT_MAP]
-      \\ unabbrev_all_tac \\ rpt $ pop_assum kall_tac
-      \\ Induct_on ‘l’ \\ gvs [] \\ PairCases \\ fs [])
     \\ qpat_x_assum ‘_ = EL _ _’ $ assume_tac o GSYM
     \\ simp [])
   >~ [‘spec_arg’] >-
@@ -826,6 +818,7 @@ Proof
   IF_CASES_TAC >> gvs[]
 QED
 
+(*
 Theorem bidir_preserves_typing:
   ∀x y ns db st env t.
     (x <--> y) ∧ namespace_ok ns
@@ -1253,6 +1246,7 @@ Proof
       )
     )
 QED
+*)
 
 (**********)
 

compiler/backend/languages/relations/pure_pres_lemmasScript.sml

@@ -15,7 +15,7 @@ open pure_expTheory pure_valueTheory pure_evalTheory pure_eval_lemmasTheory
 val _ = new_theory "pure_pres_lemmas";
 
 Theorem bidir_letrec_eta:
-  MEM (f,Lam a vs x) l ∧ ALL_DISTINCT (MAP FST l) ∧
+  MEM (f,Lam a vs x) l ∧ ALL_DISTINCT (MAP FST l) ∧ vs ≠ [] ∧
   EVERY (λ(v,e).
            DISJOINT (IMAGE explode (set vs)) (freevars (exp_of e)) ∧
            ~MEM v vs) l ∧
@@ -34,7 +34,8 @@ Proof
   \\ conj_tac
   >-
    (irule bidir_Letrec \\ fs [LIST_REL_same]
-    \\ irule bidir_Lam \\ simp [Once bidir_sym,bidir_App_Lam])
+    \\ simp [Once bidir_sym]
+    \\ irule bidir_App_Lam \\ fs [])
   \\ irule_at Any bidir_trans
   \\ irule_at (Pos hd) bidir_Letrec_Lam \\ fs []
   \\ simp [Once bidir_sym]
@@ -55,7 +56,7 @@ Proof
 QED
 
 Theorem bidir_letrec_eta_1:
-  ¬MEM f vs
+  ¬MEM f vs ∧ vs ≠ []
   ⇒
   (Letrec a [(f,Lam a vs x)] (Var a f))
   <-->
@@ -67,7 +68,7 @@ Proof
 QED
 
 Theorem bidir_letrec_expand_1:
-  ¬MEM f vs
+  ¬MEM f vs ∧ vs ≠ []
   ⇒
   (Letrec a [(f,Lam a vs x)] x)
   <-->
@@ -91,7 +92,7 @@ Proof
 QED
 
 Theorem bidir_contract_1:
-  ~MEM f ps ∧ ~MEM f ws ∧ vs ≠ [] ∧ ws ≠ []
+  ~MEM f ps ∧ ~MEM f ws ∧ vs ≠ [] ∧ ws ≠ [] ∧ set ws ⊆ set vs
   ⇒
   (Lam a (vs ++ ps)
      (Letrec a [(f,Lam a (ws ++ ps) x)]
@@ -103,53 +104,60 @@ Theorem bidir_contract_1:
 Proof
   Cases_on ‘ps = []’ >- fs []
   \\ rw []
-  \\ irule bidir_trans
-  \\ irule_at Any bidir_Lam_append \\ fs []
-  \\ irule bidir_Lam
-  \\ irule bidir_trans
-  \\ qabbrev_tac ‘y = Letrec a [(f,Lam a (ws ++ ps) x)] x’
-  \\ qexists_tac ‘Lam a ps
-                   (App a (Lam a (ws ++ ps) y) (MAP (Var a) ws ++ MAP (Var a) ps))’
-  \\ conj_tac >-
-   (irule bidir_Lam
-    \\ irule bidir_trans
-    \\ irule_at Any bidir_Letrec_App_forget
-    \\ irule_at Any bidir_App
-    \\ fs [LIST_REL_same,EVERY_MAP,exp_of_def]
-    \\ gvs [EVERY_MEM]
-    \\ irule bidir_trans
-    \\ irule_at (Pos hd) bidir_Letrec_unroll \\ fs []
-    \\ unabbrev_all_tac
-    \\ irule bidir_Letrec_Lam
-    \\ fs [exp_of_def,IN_DISJOINT,MEM_MAP]
-    \\ metis_tac [])
-  \\ simp [Once bidir_sym]
-  \\ irule bidir_trans
-  \\ qexists_tac ‘App a (Lam a (ws ++ ps) y) (MAP (Var a) ws)’
-  \\ conj_tac >-
+  \\ qabbrev_tac ‘z = Letrec a [(f,Lam a (ws ++ ps) x)] x’
+  \\ ‘Letrec a [(f,Lam a (ws ++ ps) x)] (Var a f) <--> Lam a (ws ++ ps) z’ by
    (irule bidir_trans
-    \\ irule_at Any bidir_Letrec_App_forget
-    \\ irule_at Any bidir_App
-    \\ fs [LIST_REL_same,EVERY_MAP,exp_of_def]
-    \\ gvs [EVERY_MEM]
-    \\ irule bidir_trans
     \\ irule_at (Pos hd) bidir_Letrec_unroll \\ fs []
     \\ unabbrev_all_tac
-    \\ irule bidir_Letrec_Lam
-    \\ fs [exp_of_def,IN_DISJOINT,MEM_MAP]
+    \\ irule_at (Pos hd) bidir_Letrec_Lam \\ gvs []
+    \\ gvs [exp_of_def,IN_DISJOINT,MEM_MAP]
     \\ metis_tac [])
-  \\ irule bidir_trans
-  \\ qexists_tac ‘Lam a ps y’
-  \\ conj_tac >-
-   (irule bidir_trans
+  \\ qsuff_tac ‘
+      Lam a (vs ++ ps)
+        (App a (Lam a (ws ++ ps) z) (MAP (Var a) ws ++ MAP (Var a) ps)) <-->
+      Lam a vs
+        (App a (Lam a (ws ++ ps) z) (MAP (Var a) ws))’
+  >-
+   (strip_tac
+    \\ irule_at (Pos hd) bidir_trans
+    \\ irule_at (Pos last) bidir_trans
+    \\ pop_assum $ irule_at $ Pos hd
+    \\ irule_at Any bidir_Lam
+    \\ irule_at Any bidir_Lam
+    \\ unabbrev_all_tac
+    \\ irule_at (Pos hd) bidir_trans
+    \\ irule_at Any bidir_Letrec_App_forget
+    \\ gvs [EVERY_MAP,exp_of_def] \\ gvs [EVERY_MEM]
+    \\ irule_at (Pos hd) bidir_App
+    \\ gvs [LIST_REL_same]
+    \\ simp [Once bidir_sym]
+    \\ irule_at (Pos hd) bidir_trans
+    \\ irule_at Any bidir_Letrec_App_forget
+    \\ gvs [EVERY_MAP,exp_of_def] \\ gvs [EVERY_MEM]
     \\ irule_at (Pos hd) bidir_App
+    \\ gvs [LIST_REL_same])
+  \\ irule_at Any bidir_trans
+  \\ qexists_tac ‘Lam a (vs ++ ps) z’
+  \\ conj_tac >-
+   (rewrite_tac [GSYM MAP_APPEND]
+    \\ irule bidir_App_Lam \\ fs []
+    \\ gvs [SUBSET_DEF])
+  \\ qsuff_tac ‘
+      Lam a vs (Lam a ps z) <-->
+      Lam a vs (App a (Lam a ws (Lam a ps z)) (MAP (Var a) ws))’
+  >-
+   (strip_tac
+    \\ irule bidir_trans
     \\ irule_at (Pos hd) bidir_Lam_append \\ fs []
-    \\ qexists_tac ‘MAP (Var a) ws’ \\ fs []
+    \\ irule bidir_trans
+    \\ pop_assum $ irule_at $ Pos hd
+    \\ irule bidir_Lam
+    \\ irule bidir_App
     \\ gvs [LIST_REL_same]
-    \\ metis_tac [bidir_App_Lam])
-  \\ irule bidir_Lam
+    \\ simp [Once bidir_sym]
+    \\ irule_at (Pos hd) bidir_Lam_append \\ fs [])
   \\ simp [Once bidir_sym]
-  \\ rewrite_tac [GSYM MAP_APPEND,bidir_App_Lam]
+  \\ irule bidir_App_Lam \\ fs []
 QED
 
 val _ = export_theory ();

compiler/backend/languages/semantics/thunkLangScript.sml

@@ -568,6 +568,11 @@ Definition is_Delay_def[simp]:
   (is_Delay _ = F)
 End
 
+Definition is_delay_def[simp]: (* TODO: delete, replace by above *)
+  is_delay (Delay x) = T ∧
+  is_delay _ = F
+End
+
 Definition ok_bind_def[simp]:
   (ok_bind (Lam _ _) = T) ∧
   (ok_bind (Delay _) = T) ∧
@@ -606,4 +611,10 @@ Proof
   \\ simp [SET_EQ_SUBSET, SUBSET_DEF]
 QED
 
+Definition ok_binder_def[simp]:
+  ok_binder (Lam s x) = T ∧
+  ok_binder (Delay x) = T ∧
+  ok_binder _ = F
+End
+
 val _ = export_theory ();

compiler/backend/languages/state_cexpScript.sml

@@ -53,6 +53,11 @@ Overload IntLit = “λi. App (AtomOp (Lit (Int i))) []”
 Overload StrLit = “λs. App (AtomOp (Lit (Str s))) []”
 Overload Eq = “λx y. App (AtomOp Eq) [x; y]”
 
+Definition Lets_def:
+  Lets [] x = (x:state_cexp$cexp) ∧
+  Lets ((v,y)::ys) x = Let v y (Lets ys x)
+End
+
 (* We require the correct number of arguments to be passed to the following.
    We could specify this for all operations, but it isn't necessary *)
 Definition op_args_ok_def:

compiler/backend/languages/thunk_cexpScript.sml

@@ -65,4 +65,14 @@ Termination
   WF_REL_TAC `measure cexp_size`
 End
 
+Definition is_Lam_def:
+  is_Lam (Lam s e) = T ∧
+  is_Lam _ = F
+End
+
+Definition dest_Var_def:
+  dest_Var (Var v) = SOME v ∧
+  dest_Var _ = NONE
+End
+
 val _ = export_theory();

compiler/backend/passes/env_to_stateScript.sml

@@ -14,32 +14,12 @@ val _ = new_theory "env_to_state";
 
 val _ = set_grammar_ancestry ["env_cexp", "state_cexp", "pure_comp_conf"];
 
-Definition dest_Message_def:
-  dest_Message (Message s) = SOME s ∧
-  dest_Message _ = NONE
-End
-
-Definition Lets_def:
-  Lets [] x = (x:state_cexp$cexp) ∧
-  Lets ((v,y)::ys) x = Let v y (Lets ys x)
-End
-
 Definition Letrec_imm_def:
   (Letrec_imm vs ((Var v):env_cexp$cexp) ⇔ MEM v vs) ∧
   (Letrec_imm vs (Lam _ _) ⇔ T) ∧
   (Letrec_imm vs _ ⇔ F)
 End
 
-Definition dest_Delay_def:
-  dest_Delay (Delay x) = SOME (x:env_cexp$cexp) ∧
-  dest_Delay _ = NONE
-End
-
-Definition dest_Lam_def:
-  dest_Lam (Lam v x) = SOME (v,x:env_cexp$cexp) ∧
-  dest_Lam _ = NONE
-End
-
 Definition Letrec_split_def:
   Letrec_split vs [] = ([],[]) ∧
   Letrec_split vs ((v:mlstring,x)::fns) =