removed box from ThunkLang

compiler/backend/languages/semantics/thunkLangPropsScript.sml

@@ -17,9 +17,9 @@ val _ = set_grammar_ancestry ["thunkLang", "pure_misc", "thunk_semantics"];
 val _ = numLib.prefer_num ();
 
 Theorem exp_size_lemma:
-  (∀x xs. MEM x xs ⇒ exp_size x ≤ exp4_size xs) ∧
+  (∀x xs. MEM x xs ⇒ exp_size x ≤ exp3_size xs) ∧
   (∀x y xs. MEM (x,y) xs ⇒ exp_size y ≤ exp1_size xs) ∧
-  (∀x xs. MEM x xs ⇒ v_size x < exp5_size xs)
+  (∀x xs. MEM x xs ⇒ v_size x < exp4_size xs)
 Proof
   rpt conj_tac
   \\ Induct_on ‘xs’ \\ rw []
@@ -41,7 +41,6 @@ Definition no_value_def:
   (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) ∧
@@ -125,7 +124,6 @@ Theorem exp_ind:
     (∀v x y. P x ∧ P y ⇒ P (Let v x y)) ∧
     (∀f x. (∀n x'. MEM (n,x') f ⇒ P x') ∧ P x ⇒ P (Letrec f x)) ∧
     (∀x. P x ⇒ P (Delay x)) ∧
-    (∀x. P x ⇒ P (Box x)) ∧
     (∀x. P x ⇒ P (Force x)) ∧
     (∀v. P (Value v)) ∧
     (∀x. P x ⇒ P (MkTick x)) ⇒
@@ -263,7 +261,6 @@ Theorem closed_simps[simp]:
   (∀mop xs. closed (Monad mop xs) ⇔ EVERY closed xs) ∧
   (∀x. closed (Force x) ⇔ closed x)  ∧
   (∀x. closed (Delay x) ⇔ closed x)  ∧
-  (∀x. closed (Box x) ⇔ closed x)  ∧
   (∀v. closed (Value v) ⇔ T)  ∧
   (∀x. closed (MkTick x) ⇔ closed x) ∧
   (∀v. closed (Var v) ⇔ F)
@@ -360,8 +357,6 @@ Proof
     \\ simp [AC CONJ_COMM CONJ_ASSOC, SF DNF_ss])
   >- ((* Delay *)
     gs [freevars_def, subst_def])
-  >- ((* Box *)
-    gs [freevars_def, subst_def])
   >- ((* Force *)
     gs [freevars_def, subst_def])
   >- ((* Value *)
@@ -1186,10 +1181,8 @@ Theorem eval_Force:
     case dest_Tick v of
       NONE =>
         do
-          (wx,binds) <- dest_anyThunk v;
-          case wx of
-            INL v => return v
-          | INR y => eval (subst_funs binds y)
+          (y,binds) <- dest_anyThunk v;
+          eval (subst_funs binds y)
         od
     | SOME w => eval (Force (Value w))
 Proof
@@ -1204,7 +1197,6 @@ Proof
     >- (
       Cases_on ‘dest_anyThunk v’ \\ gs []
       \\ pairarg_tac \\ gvs []
-      \\ CASE_TAC \\ gs []
       \\ irule eval_to_equals_eval \\ gs [])
     \\ irule eval_to_equals_eval \\ gs [])
   \\ Cases_on ‘dest_Tick v’ \\ gs []
@@ -1216,7 +1208,6 @@ Proof
       first_x_assum (qspec_then ‘1’ assume_tac)
       \\ Cases_on ‘v’ \\ gs [])
     \\ pairarg_tac \\ gvs []
-    \\ CASE_TAC \\ gs []
     \\ simp [eval_def]
     \\ DEEP_INTRO_TAC some_intro \\ rw []
     \\ first_x_assum (qspec_then ‘x + 1’ assume_tac) \\ gs [])

compiler/backend/languages/semantics/thunkLangScript.sml

@@ -5,12 +5,11 @@
    thunkLang is the next language in the compiler after pureLang.
    - It has a call-by-value semantics.
    - It extends the pureLang syntax with explicit syntax for delaying and
-     forcing computations (“Delay” and “Force”) and “Thunk” values. Non-
-     suspended thunks can be created with “Box”.
+     forcing computations (“Delay” and “Force”) and “Thunk” values.
    - Suspended computations can be wrapped in “MkTick” to cause the suspended
      evaluation to consume one extra clock tick by producing a value wrapped in
      “DoTick”.
-   - Any expression bound by a Letrec must be one of “Lam”, “Delay” or “Box”.
+   - Any expression bound by a Letrec must be one of “Lam”, “Delay”.
    - thunkLang has a substitution-based semantics. See [envLangScript.sml]
      for the next language in the compiler, which has an environment-based
      semantics.
@@ -36,7 +35,6 @@ Datatype:
       | Let (vname option) exp exp               (* non-recursive let       *)
       | If exp exp exp                           (* if-then-else            *)
       | Delay exp                                (* suspend in a Thunk      *)
-      | Box exp                                  (* wrap result in a Thunk  *)
       | Force exp                                (* evaluates a Thunk       *)
       | Value v                                  (* for substitution        *)
       | MkTick exp;                              (* creates a delayed Tick  *)
@@ -45,7 +43,7 @@ Datatype:
     | Monadic mop (exp list)
     | Closure vname exp
     | Recclosure ((vname # exp) list) vname
-    | Thunk (v + exp)
+    | Thunk exp
     | Atom lit
     | DoTick v                                   (* extra clock when forced *)
 End
@@ -83,7 +81,6 @@ Definition subst_def:
     (let m1 = FILTER (λ(n, v). ¬MEM n (MAP FST f)) m in
        Letrec (MAP (λ(n, x). (n, subst m1 x)) f) (subst m1 x)) ∧
   subst m (Delay x) = Delay (subst m x) ∧
-  subst m (Box x) = Box (subst m x) ∧
   subst m (Force x) = Force (subst m x) ∧
   subst m (Value v) = Value v ∧
   subst m (MkTick x) = MkTick (subst m x)
@@ -124,7 +121,6 @@ Theorem subst1_def:
      else
        Letrec (MAP (λ(f, x). (f, subst1 n v x)) f) (subst1 n v x)) ∧
   subst1 n v (Delay x) = Delay (subst1 n v x) ∧
-  subst1 n v (Box x) = Box (subst1 n v x) ∧
   subst1 n v (Force x) = Force (subst1 n v x) ∧
   subst1 n v (Value w) = Value w ∧
   subst1 n v (MkTick x) = MkTick (subst1 n v x)
@@ -179,7 +175,7 @@ Definition dest_anyThunk_def:
     do
       (f, n) <- dest_Recclosure v;
       case ALOOKUP (REVERSE f) n of
-        SOME (Delay x) => return (INR x, f)
+        SOME (Delay x) => return (x, f)
       | _ => fail Type_error
     od
 End
@@ -202,7 +198,6 @@ Definition freevars_def:
     ((freevars x ∪ BIGUNION (set (MAP (λ(n, x). freevars x) f))) DIFF
      set (MAP FST f)) ∧
   freevars (Delay x) = freevars x ∧
-  freevars (Box x) = freevars x ∧
   freevars (Force x) = freevars x ∧
   freevars (Value v) = ∅ ∧
   freevars (MkTick x) = freevars x
@@ -227,7 +222,6 @@ Definition boundvars_def:
     ((boundvars x ∪ BIGUNION (set (MAP (λ(n, x). boundvars x) f))) ∪
      set (MAP FST f)) ∧
   boundvars (Delay x) = boundvars x ∧
-  boundvars (Box x) = boundvars x ∧
   boundvars (Force x) = boundvars x ∧
   boundvars (Value v) = ∅ ∧
   boundvars (MkTick x) = boundvars x
@@ -281,23 +275,16 @@ Definition eval_to_def:
   eval_to k (Letrec funs x) =
     (if k = 0 then fail Diverge else
        eval_to (k - 1) (subst_funs funs x)) ∧
-  eval_to k (Delay x) = return (Thunk (INR x)) ∧
-  eval_to k (Box x) =
-    (do
-       v <- eval_to k x;
-       return (Thunk (INL v))
-     od) ∧
+  eval_to k (Delay x) = return (Thunk x) ∧
   eval_to k (Force x) =
     (if k = 0 then fail Diverge else
        do
          v <- eval_to k x;
          case dest_Tick v of
            SOME w => eval_to (k - 1) (Force (Value w))
          | NONE =>
-             do (wx, binds) <- dest_anyThunk v;
-                case wx of
-                  INL v => return v
-                | INR y => eval_to (k - 1) (subst_funs binds y)
+             do (y, binds) <- dest_anyThunk v;
+                eval_to (k - 1) (subst_funs binds y)
              od
        od) ∧
   eval_to k (MkTick x) =
@@ -377,7 +364,6 @@ Theorem eval_to_ind:
     (∀k funs x.
       (k ≠ 0 ⇒ P (k − 1) (subst_funs funs x)) ⇒ P k (Letrec funs x)) ∧
     (∀k x. P k (Delay x)) ∧
-    (∀k x. P k x ⇒ P k (Box x)) ∧
     (∀k x.
       (∀y binds.
          k ≠ 0 ⇒
@@ -476,9 +462,6 @@ Proof
     rw [eval_to_def, subst_funs_def])
   >- ((* Delay *)
     rw [eval_to_def])
-  >- ((* Box *)
-    rw [eval_to_def]
-    \\ Cases_on ‘eval_to k x’ \\ fs [])
   >- ((* Force *)
     rw []
     \\ rgs [Once eval_to_def]
@@ -488,8 +471,8 @@ Proof
     \\ Cases_on ‘eval_to k x’ \\ fs []
     \\ BasicProvers.TOP_CASE_TAC \\ gs []
     \\ Cases_on ‘dest_anyThunk y’ \\ gs []
-    \\ pairarg_tac \\ gvs []
-    \\ BasicProvers.TOP_CASE_TAC \\ gs [])
+    \\ pairarg_tac \\ gvs [])
+    (* \\ BasicProvers.TOP_CASE_TAC \\ gs []) *)
   >- ((* MkTick *)
     rw [eval_to_def]
     \\ Cases_on ‘eval_to k x’ \\ fs [])
@@ -585,11 +568,6 @@ Definition is_Delay_def[simp]:
   (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) ∧

compiler/backend/languages/semantics/thunk_exp_ofScript.sml

@@ -56,8 +56,7 @@ Definition exp_of_def[simp]:
         (MAP (λ(c,vs,x). (explode c,MAP explode vs,exp_of x)) rs)
         (OPTION_MAP (λ(a,e). (MAP (explode ## I) a, exp_of e)) d) ∧
   exp_of (Force x)       = Force (exp_of x) ∧
-  exp_of (Delay x)       = Delay (exp_of x) ∧
-  exp_of (Box x)         = Box (exp_of x)
+  exp_of (Delay x)       = Delay (exp_of x)
 Termination
   WF_REL_TAC ‘measure cexp_size’ >> rw [cexp_size_eq]
 End
@@ -83,7 +82,6 @@ Definition cexp_wf_def:
   cexp_wf (App e es) = (cexp_wf e ∧ EVERY cexp_wf es ∧ es ≠ []) ∧
   cexp_wf (Force e) = cexp_wf e ∧
   cexp_wf (Delay e) = cexp_wf e ∧
-  cexp_wf (Box e) = cexp_wf e ∧
   cexp_wf (Lam vs e) = (cexp_wf e ∧ vs ≠ []) ∧
   cexp_wf (Let v e1 e2) = (cexp_wf e1 ∧ cexp_wf e2) ∧
   cexp_wf (Letrec fns e) = (EVERY (λ(_,x). cexp_ok_bind x ∧ cexp_wf x) fns ∧ cexp_wf e

compiler/backend/languages/thunk_cexpScript.sml

@@ -25,7 +25,6 @@ Datatype:
        | Case name ((name # (name list) # cexp) list)    (* pattern match        *)
                     (((name # num) list # cexp) option)  (* optional fallthrough *)
        | Delay cexp                   (* delay a computation as a thunk          *)
-       | Box cexp                     (* eagerly compute, but wrap as a thunk    *)
        | Force cexp                   (* force a thunk                           *)
 End
 
@@ -60,7 +59,6 @@ Definition cns_arities_def:
       | SOME (a,e) =>
         (set (MAP (λ(cn,ar). explode cn, ar) a) ∪ css_cn_ars) INSERT cns_arities e) ∪
     BIGUNION (set (MAP (λ(cn,vs,e). cns_arities e) css))) ∧
-  cns_arities (Box e) = cns_arities e ∧
   cns_arities (Delay e) = cns_arities e ∧
   cns_arities (Force e) = cns_arities e
 Termination

compiler/backend/passes/proofs/pure_to_thunk_1ProofScript.sml

@@ -24,9 +24,8 @@ val _ = numLib.prefer_num ();
 
   As pureLang is lazy it allows non-functional value declarations that are
   mutually recursive, and lazy value declarations. All such computations are
-  suspended thunkLang-side by Lam, Box or Delay. This relation (exp_rel) acts as
-  if the compiler inserted Delay everywhere, but the compiler can insert Box
-  for things that do not require a thunk to be allocated, such as a lambda.
+  suspended thunkLang-side by Lam or Delay. This relation (exp_rel) acts as
+  if the compiler inserted Delay everywhere.
 
   * [Var]
     - All variables are wrapped in ‘Force’ as if they were suspended either by
@@ -71,10 +70,10 @@ val _ = numLib.prefer_num ();
     - `Bind`/`Handle` are straightforwardly compiled
   * [Letrec]
     - We expect all expressions in the list of bindings to be suspended by
-      something (either Lam or Delay or Box), so we insert Delay everywhere.
+      something (either Lam or Delay), so we insert Delay everywhere.
  *)
 
-Overload Suspend[local] = “λx. Force (Value (Thunk (INR x)))”;
+Overload Suspend[local] = “λx. Force (Value (Thunk x))”;
 
 Overload Rec[local] = “λf n. Force (Value (Recclosure f n))”;
 
@@ -218,7 +217,7 @@ End
 
 Definition thunk_rel_def:
   thunk_rel x v ⇔
-    ∃y. v = Thunk (INR y) ∧
+    ∃y. v = Thunk y ∧
         exp_rel x y ∧
         closed x
 End
@@ -464,7 +463,7 @@ Theorem exp_rel_subst:
     exp_rel a b ∧
     closed a ⇒
       exp_rel (subst1 n (Tick a) x)
-              (subst1 n (Thunk (INR b)) y)
+              (subst1 n (Thunk b) y)
 Proof
   ho_match_mp_tac exp_ind_alt \\ rw []
   >- ((* Var *)
@@ -2610,7 +2609,7 @@ Proof
 QED
 
 Triviality eval_simps[simp]:
-  eval (Delay e) = INR (Thunk (INR e)) ∧
+  eval (Delay e) = INR (Thunk e) ∧
   eval (Lit l) = INR (Atom l) ∧
   eval (Monad mop es) = INR (Monadic mop es) ∧
   eval (Lam x body) = INR (Closure x body) ∧