implemented new optimisation pass, still needs to be integrated and tested

Author: samsa1

compiler/backend/languages/semantics/thunkLangPropsScript.sml

@@ -28,6 +28,43 @@ Proof
   \\ simp []
 QED
 
+(* -------------------------------------------------------------------------
+ * Property about terms stating they do not contain a value
+ * ------------------------------------------------------------------------- *)
+
+Definition no_value_def:
+  (no_value (Var n) = T) ∧
+  (no_value (Force x) = no_value x) ∧
+  (no_value (Prim op xs) = EVERY no_value xs) ∧
+  (no_value (If x y z) = (no_value x ∧ no_value y ∧ no_value z)) ∧
+  (no_value (App x y) = (no_value x ∧ no_value y)) ∧
+  (no_value (Lam s x) = no_value x) ∧
+  (no_value (Let opt x y) = (no_value x ∧ no_value y)) ∧
+  (no_value (Box x) = no_value x) ∧
+  (no_value (MkTick x) = no_value x) ∧
+  (no_value (Letrec f x) = (no_value x ∧ EVERY no_value (MAP SND f) ∧ EVERY ok_bind (MAP SND f))) ∧
+  (no_value (Value v) = F) ∧
+  (no_value (Delay x) = no_value x)
+Termination
+  WF_REL_TAC ‘measure $ exp_size’ \\ rw [MEM_MAP, SND_THM]
+  \\ assume_tac exp_size_lemma
+  \\ pairarg_tac \\ gvs []
+  \\ first_x_assum $ dxrule_then assume_tac \\ gvs []
+End
+
+Theorem no_value_Lams:
+  ∀l x. no_value (Lams l x) = no_value x
+Proof
+  Induct >> gs [no_value_def]
+QED
+
+Theorem no_value_Apps:
+  ∀l x. no_value (Apps x l) = (no_value x ∧ EVERY no_value l)
+Proof
+  Induct >> gs [no_value_def] >>
+  metis_tac []
+QED
+
 (* -------------------------------------------------------------------------
  * Lemmas about Lams and Apps
  * ------------------------------------------------------------------------- *)

compiler/backend/languages/semantics/thunkLangScript.sml

@@ -569,6 +569,16 @@ Definition is_Lam_def[simp]:
   (is_Lam _ = F)
 End
 
+Definition is_Delay_def[simp]:
+  (is_Delay (Delay x) = T) ∧
+  (is_Delay _ = F)
+End
+
+Definition is_Box_def[simp]:
+  (is_Box (Box x) = T) ∧
+  (is_Box _ = F)
+End
+
 Definition ok_bind_def[simp]:
   (ok_bind (Lam _ _) = T) ∧
   (ok_bind (Delay _) = T) ∧
@@ -583,6 +593,16 @@ Proof
   \\ gs []
 QED
 
+Theorem FINITE_freevars:
+  ∀e. FINITE (freevars e)
+Proof
+  Induct using freevars_ind
+  \\ gs [freevars_def, MEM_MAP, PULL_EXISTS, FORALL_PROD]
+  \\ irule FINITE_DIFF
+  \\ simp [MEM_MAP, PULL_EXISTS, FORALL_PROD]
+  \\ rw [] \\ last_x_assum $ dxrule_then irule
+QED
+
 Theorem boundvars_Lams:
   ∀vL e. boundvars (Lams vL e) = set vL ∪ boundvars e
 Proof

compiler/backend/languages/semantics/thunk_exp_ofScript.sml

@@ -111,4 +111,10 @@ Definition is_Delay_def:
   (is_Delay _ = F)
 End
 
+Theorem lets_for_APPEND:
+  lets_for l m n (l1 ++ l2) e = lets_for l m n l1 (lets_for l m n l2 e)
+Proof
+  Induct_on ‘l1’ \\ gvs [lets_for_def, FORALL_PROD]
+QED
+
 val _ = export_theory ();