From e4fea61ca1f326967c3e20175cf210f2a08800aa Mon Sep 17 00:00:00 2001 From: Thomas Sewell Date: Fri, 4 Nov 2022 22:31:39 +0000 Subject: [PATCH] Retire Env_id On writing the Eval paper, it becomes clear that Env_id is an extra feature that isn't actually needed anywhere. --- .../prover/candle_prover_evaluateScript.sml | 5 ----- candle/prover/permsScript.sml | 4 ---- .../proofs/source_to_flatProofScript.sml | 22 ++----------------- compiler/backend/source_to_flatScript.sml | 8 ------- compiler/inference/inferScript.sml | 2 -- compiler/parsing/fromSexpScript.sml | 4 +--- compiler/repl/evaluate_initScript.sml | 3 --- compiler/repl/evaluate_skipScript.sml | 6 ----- semantics/alt_semantics/bigStepScript.sml | 2 +- .../alt_semantics/itree_semanticsScript.sml | 4 ---- semantics/astScript.sml | 2 -- semantics/semanticPrimitivesScript.sml | 4 ---- unverified/lem/ast.lem | 2 -- 13 files changed, 4 insertions(+), 64 deletions(-) diff --git a/candle/prover/candle_prover_evaluateScript.sml b/candle/prover/candle_prover_evaluateScript.sml index b92b47cf54..ec6c2ac38d 100644 --- 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 index 5bee8e1b0a..3b98c2d3cd 100644 --- 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 index 996b87129f..81eee09c48 100644 --- 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 index 030c775075..62b73c0107 100644 --- 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 index a66eb5a70c..9562e97e27 100644 --- 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 index 60c3962fb6..e7acbed571 100644 --- 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 index 36b7fddda7..a23650aba8 100644 --- 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 index b264fb198a..dc981e65de 100644 --- 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 index e257797e8b..38acdd7ecb 100644 --- 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 index 5587fd4ec9..cbe0abfb12 100644 --- 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 index f59e7db0b9..16e00eea77 100644 --- 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 index 4d2e602911..3a9ed0524a 100644 --- 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 index b665d41ddd..7202b34871 100644 --- 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 =