Retire Env_id

On writing the Eval paper, it becomes clear that Env_id is an extra feature that isn't actually needed anywhere.
CakeML · Nov 7, 2022 · e4fea61 · e4fea61
1 parent 1c30998
commit e4fea61
Show file tree

Hide file tree

Showing 13 changed files with 4 additions and 64 deletions.
diff --git a/candle/prover/candle_prover_evaluateScript.sml b/candle/prover/candle_prover_evaluateScript.sml
@@ -287,11 +287,6 @@ Theorem do_app_ok:
 Proof
   strip_tac
   \\ qpat_x_assum ‘do_app _ _ _ = _’ mp_tac
-  \\ Cases_on ‘op = Env_id’ \\ gs []
-  >- (
-    rw [do_app_cases] \\ gs []
-    \\ simp [v_ok_def, nat_to_v_def]
-    \\ first_assum (irule_at Any) \\ gs [SF SFY_ss])
   \\ Cases_on ‘∃chn. op = FFI chn’ \\ gs []
   >- (
     rw [do_app_cases] \\ gs []

diff --git a/candle/prover/permsScript.sml b/candle/prover/permsScript.sml
@@ -322,10 +322,6 @@ Theorem do_app_perms:
 Proof
   strip_tac
   \\ qpat_x_assum ‘do_app _ _ _ = _’ mp_tac
-  \\ Cases_on ‘op = Env_id’ \\ gs []
-  >- (
-    rw [do_app_cases] \\ gs []
-    \\ simp [perms_ok_def, nat_to_v_def])
   \\ Cases_on ‘∃chn. op = FFI chn’ \\ gs []
   >- (
     rw [do_app_cases] \\ gs []

diff --git a/compiler/backend/proofs/source_to_flatProofScript.sml b/compiler/backend/proofs/source_to_flatProofScript.sml
@@ -922,8 +922,7 @@ val do_app = time Q.prove (
     SND s1 = s1_i1.ffi ∧
     genv_c_ok genv.c ∧
     op ≠ AallocEmpty ∧
-    getOpClass op ≠ Reals ∧
-    op ≠ Env_id
+    getOpClass op ≠ Reals
     ⇒
      ∃r_i1 s2_i1.
        LIST_REL (sv_rel genv) (FST s2) (TL s2_i1.refs) ∧
@@ -4142,24 +4141,7 @@ Proof
     fs [evaluateTheory.dec_clock_def, dec_clock_def] >>
     metis_tac (SUBSET_TRANS :: trans_thms)
   )
-  \\ Cases_on `op = Env_id`
-  >- (
-    fs [option_case_eq, pair_case_eq, result_rel_eqns, astTheory.getOpClass_def]
-    \\ rw []
-    \\ fs [semanticPrimitivesTheory.do_app_def]
-    \\ fs [case_eq_thms, semanticPrimitivesTheory.v_case_eq, pair_case_eq]
-    \\ rveq \\ fs []
-    \\ fs [v_rel_eqns]
-    \\ rveq \\ fs []
-    \\ imp_res_tac evaluate_length
-    \\ fs [compile_exps_length]
-    \\ fs [LENGTH_EQ_NUM_compute]
-    \\ fs [compile_exp_def]
-    \\ rw [result_rel_eqns, v_rel_eqns]
-    \\ asm_exists_tac \\ fs []
-    \\ fs [invariant_def, s_rel_cases]
-  ) >>
-  Cases_on ‘getOpClass op’ >> gs[]
+  >> Cases_on ‘getOpClass op’ >> gs[]
   >- (Cases_on ‘op’ >> gs[astTheory.getOpClass_def])
   >- (Cases_on ‘op’ >> gs[astTheory.getOpClass_def])
   >~ [‘getOpClass op = Reals’]

diff --git a/compiler/backend/source_to_flatScript.sml b/compiler/backend/source_to_flatScript.sml
@@ -191,14 +191,6 @@ Definition compile_exp_def:
                     (MAP (Var_local None) ["bytes"; "words"]))
                 (Let None (SOME "r") (App None (GlobalVarLookup 0) [])
                     (flatLang$App None (El 0) [Var_local None "r"])))]
-    else
-    if op = Env_id then (case es of
-      | [_] => (case compile_exps t env es of
-                | x::xs => x
-                | _ => Var_local None "" (* Can't happen *))
-      (* possible only if one of es raises an exception *)
-      | _ => App None (El 0) (compile_exps t env es)
-      )
     else
       flatLang$App None (astOp_to_flatOp op) (compile_exps t env es)) ∧
   (compile_exp t env (Log lop e1 e2) =

diff --git a/compiler/inference/inferScript.sml b/compiler/inference/inferScript.sml
@@ -417,7 +417,6 @@ val op_to_string_def = Define `
 (op_to_string Aupdate_unsafe = (implode "Aupdate_unsafe", 3)) ∧
 (op_to_string ConfigGC = (implode "ConfigGC", 2)) ∧
 (op_to_string Eval = (implode "Eval", 6)) ∧
-(op_to_string Env_id = (implode "Env_id", 1)) ∧
 (op_to_string ListAppend = (implode "ListAppend", 2)) ∧
 (op_to_string (FFI _) = (implode "FFI", 2))`;
 
@@ -558,7 +557,6 @@ constrain_op l op ts =
    | (RealFromFP, _) => failwith l (implode "Reals do not have a type")
    | (AallocFixed, _) => failwith l (implode "Unsafe ops do not have a type") (* not actually unsafe *)
    | (Eval, _) => failwith l (implode "Unsafe ops do not have a type")
-   | (Env_id, _) => failwith l (implode "Unsafe ops do not have a type")
    | _ => failwith l (op_n_args_msg op (LENGTH ts))
 End
 

diff --git a/compiler/parsing/fromSexpScript.sml b/compiler/parsing/fromSexpScript.sml
@@ -730,8 +730,7 @@ val sexpop_def = Define`
   if s = "Asub_unsafe" then SOME Asub_unsafe else
   if s = "Aupdate_unsafe" then SOME Aupdate_unsafe else
   if s = "ConfigGC" then SOME ConfigGC else
-  if s = "Eval" then SOME Eval else
-  if s = "Env_id" then SOME Env_id else NONE) ∧
+  if s = "Eval" then SOME Eval else NONE) ∧
   (sexpop (SX_CONS (SX_SYM s) (SX_STR s')) =
      if s = "FFI" then OPTION_MAP FFI (decode_control s') else NONE
    ) ∧
@@ -1378,7 +1377,6 @@ val opsexp_def = Define`
   (opsexp Aupdate_unsafe = SX_SYM "Aupdate_unsafe") ∧
   (opsexp ConfigGC = SX_SYM "ConfigGC") ∧
   (opsexp Eval = SX_SYM "Eval") ∧
-  (opsexp Env_id = SX_SYM "Env_id") ∧
   (opsexp (FFI s) = SX_CONS (SX_SYM "FFI") (SEXSTR s))`;
 
 Theorem sexpop_opsexp[simp]:

diff --git a/compiler/repl/evaluate_initScript.sml b/compiler/repl/evaluate_initScript.sml
@@ -357,9 +357,6 @@ Proof
     gs [state_ok_def, state_rel_def, EVERY_EL, ref_ok_def]
     \\ rw [] \\ gs [FLOOKUP_FUN_FMAP])
   \\ simp [Once CONJ_COMM]
-  \\ Cases_on ‘op = Env_id’ \\ gs []
-  >- (
-    gvs [do_app_cases, v_ok_thm, nat_to_v_def, with_same_refs_and_ffi])
   \\ Cases_on ‘∃chn. op = FFI chn’ \\ gs []
   >- (
     gvs [do_app_cases, v_ok_thm, ffiTheory.call_FFI_def, store_assign_def,

diff --git a/compiler/repl/evaluate_skipScript.sml b/compiler/repl/evaluate_skipScript.sml
@@ -849,12 +849,6 @@ Theorem do_app_update:
               res res1
 Proof
   strip_tac
-  \\ Cases_on ‘op = Env_id’ \\ gs []
-  >- (
-    Cases_on ‘res’ \\ gvs [do_app_def, CaseEqs ["list", "v", "option", "prod"],
-                           v_rel_def, OPTREL_def]
-    \\ rpt (irule_at Any SUBMAP_REFL) \\ gs [v_rel_def, nat_to_v_def]
-    \\ first_assum (irule_at Any) \\ gs [])
   \\ Cases_on ‘∃chn. op = FFI chn’ \\ gs []
   >- (
     Cases_on ‘res’ \\ gvs [do_app_def, v_rel_def, OPTREL_def,

diff --git a/semantics/alt_semantics/bigStepScript.sml b/semantics/alt_semantics/bigStepScript.sml
@@ -31,7 +31,7 @@ Inductive opClass:
        op = Vlength ∨ op = Aalloc ∨ op = AallocEmpty ∨ op = Asub ∨
        op = Alength ∨ op = Aupdate ∨ op = Asub_unsafe ∨ op = Aupdate_unsafe ∨
        op = Aw8sub_unsafe ∨ op = Aw8update_unsafe ∨ op = ListAppend ∨
-       op = ConfigGC ∨ op = Env_id ∨ op = Opderef ∨ op = AallocFixed
+       op = ConfigGC ∨ op = Opderef ∨ op = AallocFixed
        ⇒
        opClass op Simple) ∧
 (* FunApp *)

diff --git a/semantics/alt_semantics/itree_semanticsScript.sml b/semantics/alt_semantics/itree_semanticsScript.sml
@@ -368,10 +368,6 @@ Definition do_app_def:
       )
     | (ConfigGC, [Litv (IntLit i); Litv (IntLit j)]) =>
         SOME (s, Rval (Conv NONE []))
-    | (Env_id, [Env env (gen, id)]) => SOME (s,
-            Rval (Conv NONE [nat_to_v gen; nat_to_v id]))
-    | (Env_id, [Conv NONE [gen; id]]) => SOME (s,
-            Rval (Conv NONE [gen; id]))
     | _ => NONE
 End
 

diff --git a/semantics/astScript.sml b/semantics/astScript.sml
@@ -132,8 +132,6 @@ Datatype:
   | FFI string
   (* Evaluate new code in a given env *)
   | Eval
-  (* Get the identifier of an env object *)
-  | Env_id
 End
 
 (* Define operator classes, that allow to group their behavior later *)

diff --git a/semantics/semanticPrimitivesScript.sml b/semantics/semanticPrimitivesScript.sml
@@ -1181,10 +1181,6 @@ Definition do_app_def:
             )
         | _ => NONE
         )
-    | (Env_id, [Env env (gen, id)]) => SOME ((s, t),
-            Rval (Conv NONE [nat_to_v gen; nat_to_v id]))
-    | (Env_id, [Conv NONE [gen; id]]) => SOME ((s, t),
-            Rval (Conv NONE [gen; id]))
     | _ => NONE
 End
 

diff --git a/unverified/lem/ast.lem b/unverified/lem/ast.lem
@@ -115,8 +115,6 @@ type op =
   | FFI of string
   (* Evaluate new code in a given env *)
   | Eval
-  (* Get the identifier of an env object *)
-  | Env_id
 
 (* Define operator classes, that allow to group their behavior later *)
 type op_class =