Fix alt_semantics

Author: HeikoBecker

semantics/alt_semantics/proofs/bigSmallEquivScript.sml

@@ -20,32 +20,79 @@ Inductive evaluate_ctxt:
   (evaluate_list ck env s1 es (s2, Rval vs2) ∧
    do_opapp (REVERSE vs2 ++ [v] ++ vs1) = SOME (env',e) ∧
    (ck ⇒ s2.clock ≠ 0) ∧
+   (opClass op FunApp) ∧
    evaluate ck env' (if ck then s2 with clock := s2.clock - 1 else s2) e bv
-      ⇒ evaluate_ctxt ck env s1 (Capp Opapp vs1 () es) v bv) ∧
+      ⇒ evaluate_ctxt ck env s1 (Capp op vs1 () es) v bv) ∧
 
   (evaluate_list T env s1 es (s2, Rval vs2) ∧
    do_opapp (REVERSE vs2 ++ [v] ++ vs1) = SOME (env',e) ∧
-   s2.clock = 0
-      ⇒ evaluate_ctxt T env s1 (Capp Opapp vs1 () es) v
+   s2.clock = 0 ∧
+   (opClass op FunApp)
+      ⇒ evaluate_ctxt T env s1 (Capp op vs1 () es) v
           (s2, Rerr (Rabort Rtimeout_error))) ∧
 
   (evaluate_list ck env s1 es (s2, Rval vs2) ∧
-   do_opapp (REVERSE vs2 ++ [v] ++ vs1) = NONE
-      ⇒ evaluate_ctxt ck env s1 (Capp Opapp vs1 () es) v
+   (do_opapp (REVERSE vs2 ++ [v] ++ vs1) = NONE) ∧
+   (opClass op FunApp)
+      ⇒ evaluate_ctxt ck env s1 (Capp op vs1 () es) v
           (s2, Rerr (Rabort Rtype_error))) ∧
 
-  (op ≠ Opapp ∧
+  (opClass op Simple ∧
    evaluate_list ck env s1 es (s2, Rval vs2) ∧
    do_app (s2.refs,s2.ffi) op (REVERSE vs2 ++ [v] ++ vs1) =
     SOME ((new_refs, new_ffi) ,res)
       ⇒ evaluate_ctxt ck env s1 (Capp op vs1 () es) v
           (s2 with <| ffi := new_ffi; refs := new_refs |>, res)) ∧
 
-  (op ≠ Opapp ∧
+  (opClass op Icing ∧
+   evaluate_list ck env s1 es (s2, Rval vs2) ∧
+   do_app (s2.refs,s2.ffi) op (REVERSE vs2 ++ [v] ++ vs1) =
+   SOME ((new_refs, new_ffi) ,vFp) ∧
+   s2.fp_state.canOpt ≠ FPScope Opt ∧
+   compress_if_bool op vFp = res
+      ⇒ evaluate_ctxt ck env s1 (Capp op vs1 () es) v
+          (s2 with <| ffi := new_ffi; refs := new_refs |>, res)) ∧
+
+  (opClass op Icing ∧
+   evaluate_list ck env s1 es (s2, Rval vs2) ∧
+   do_app (s2.refs,s2.ffi) op (REVERSE vs2 ++ [v] ++ vs1) =
+   SOME ((new_refs, new_ffi) ,vFp) ∧
+   s2.fp_state.canOpt = FPScope Opt ∧
+   do_fprw vFp (s2.fp_state.opts 0) s2.fp_state.rws = NONE ∧
+   compress_if_bool op vFp = res
+      ⇒ evaluate_ctxt ck env s1 (Capp op vs1 () es) v
+          ((shift_fp_opts s2) with <| ffi := new_ffi; refs := new_refs |>, res)) ∧
+
+  (opClass op Icing ∧
+   evaluate_list ck env s1 es (s2, Rval vs2) ∧
+   do_app (s2.refs,s2.ffi) op (REVERSE vs2 ++ [v] ++ vs1) =
+   SOME ((new_refs, new_ffi) ,vFp) ∧
+   s2.fp_state.canOpt = FPScope Opt ∧
+   do_fprw vFp (s2.fp_state.opts 0) s2.fp_state.rws = SOME rOpt ∧
+   compress_if_bool op rOpt = res
+      ⇒ evaluate_ctxt ck env s1 (Capp op vs1 () es) v
+          ((shift_fp_opts s2) with <| ffi := new_ffi; refs := new_refs |>, res)) ∧
+
+  (opClass op Reals ∧
+   evaluate_list ck env s1 es (s2, Rval vs2) ∧
+   do_app (s2.refs,s2.ffi) op (REVERSE vs2 ++ [v] ++ vs1) =
+   SOME ((new_refs, new_ffi) ,res) ∧
+   s2.fp_state.real_sem
+      ⇒ evaluate_ctxt ck env s1 (Capp op vs1 () es) v
+          (s2 with <| ffi := new_ffi; refs := new_refs |>, res)) ∧
+
+  (opClass op Reals ∧
+   evaluate_list ck env s1 es (s2, Rval vs2) ∧
+   ~s2.fp_state.real_sem
+      ⇒ evaluate_ctxt ck env s1 (Capp op vs1 () es) v
+          (shift_fp_opts s2, Rerr (Rabort Rtype_error))) ∧
+
+  ((~opClass op FunApp) ∧
+   (opClass op Reals ⇒ s2.fp_state.real_sem) ∧
    evaluate_list ck env s1 es (s2, Rval vs2) ∧
    do_app (s2.refs, s2.ffi) op (REVERSE vs2 ++ [v] ++ vs1) = NONE
       ⇒ evaluate_ctxt ck env s1 (Capp op vs1 () es) v
-          (s2, Rerr (Rabort Rtype_error))) ∧
+                      (s2, Rerr (Rabort Rtype_error))) ∧
 
   (evaluate_list ck env s es (s', Rerr err)
       ⇒ evaluate_ctxt ck env s (Capp op vs () es) v (s', Rerr err)) ∧
@@ -97,7 +144,15 @@ Inductive evaluate_ctxt:
 
   evaluate_ctxt ck env s (Ctannot () t) v (s, Rval v) ∧
 
-  evaluate_ctxt ck env s (Clannot () l) v (s, Rval v)
+  evaluate_ctxt ck env s (Clannot () l) v (s, Rval v) ∧
+
+  (oldSc = Strict ⇒
+   evaluate_ctxt ck env s (Coptimise oldSc sc ()) v (s with fp_state := s.fp_state with canOpt := oldSc,
+                                                     Rval (HD (do_fpoptimise sc [v])))) ∧
+
+  (oldSc ≠ Strict ⇒
+   evaluate_ctxt ck env s (Coptimise oldSc sc ()) v (s with fp_state := s.fp_state with canOpt := oldSc,
+                                                     Rval (HD (do_fpoptimise sc [v]))))
 End
 
 Inductive evaluate_ctxts:
@@ -108,9 +163,13 @@ Inductive evaluate_ctxts:
       ⇒ evaluate_ctxts ck s1 ((c,env)::cs) (Rval v) bv) ∧
 
   (evaluate_ctxts ck s cs (Rerr err) bv ∧
-  ((∀pes. c ≠ Chandle () pes) ∨ (∀v. err ≠ Rraise v))
+  ((∀pes. c ≠ Chandle () pes) ∨ (∀v. err ≠ Rraise v)) ∧
+   (∀ oldSc sc. c ≠ Coptimise oldSc sc ())
       ⇒ evaluate_ctxts ck s ((c,env)::cs) (Rerr err) bv) ∧
 
+  (evaluate_ctxts ck (s with fp_state := s.fp_state with canOpt := oldSc) cs (Rerr err) bv ⇒
+   evaluate_ctxts ck s ((Coptimise oldSc sc (),env)::cs) (Rerr err) bv) ∧
+
   (¬can_pmatch_all env.c s.refs (MAP FST pes) v ∧
    evaluate_ctxts ck s cs (Rerr (Rabort Rtype_error)) res2
       ⇒ evaluate_ctxts ck s ((Chandle () pes,env)::cs) (Rerr (Rraise v)) res2) ∧

semantics/alt_semantics/proofs/bigSmallInvariantsScript.sml

@@ -147,20 +147,21 @@ Theorem RTC_decl_step_determ = RTC_functional_deterministic |>
   Lib.C MATCH_MP (Q.SPEC `env` decl_step_reln_functional) |> GEN_ALL
 
 Definition Rerr_to_decl_step_result_def[simp]:
-  Rerr_to_decl_step_result (Rraise v) = Draise v ∧
-  Rerr_to_decl_step_result (Rabort v) = Dabort v
+  Rerr_to_decl_step_result fps (Rraise v) = Draise (fps, v) ∧
+  Rerr_to_decl_step_result fps (Rabort v) = Dabort (fps, v)
 End
 
 Theorem small_eval_dec_def:
   (∀benv dst st e. small_eval_dec benv dst (st, Rval e) =
     (decl_step_reln benv)꙳ dst (st, Env e, [])) ∧
   (∀benv dst st err. small_eval_dec benv dst (st, Rerr err) =
-    ∃dst'.
-      (decl_step_reln benv)꙳ dst (st, dst') ∧
-      decl_step benv (st, dst') = Rerr_to_decl_step_result err)
+    ∃fp dst'.
+      (decl_step_reln benv)꙳ dst (st with fp_state := fp, dst') ∧
+      decl_step benv (st with fp_state := fp, dst') = Rerr_to_decl_step_result (st.fp_state) err)
 Proof
   rw[small_eval_dec_def] >>
-  Cases_on `err` >> rw[small_eval_dec_def, EXISTS_PROD]
+  Cases_on `err` >> rw[small_eval_dec_def, EXISTS_PROD] >>
+  metis_tac[]
 QED
 
 Theorem small_eval_dec_cases:
@@ -169,14 +170,14 @@ Theorem small_eval_dec_cases:
       ∃dev'.
         (decl_step_reln env)꙳ dev dev' ∧
         ((∃env'. SND res = Rval env' ∧ dev' = (FST res, Env env', [])) ∨
-         (∃err. SND res = Rerr err ∧ FST dev' = FST res ∧
-            decl_step env dev' = Rerr_to_decl_step_result err))
+         (∃err fp. SND res = Rerr err ∧ FST dev' = FST res with fp_state := fp ∧
+            decl_step env dev' = Rerr_to_decl_step_result (FST res).fp_state err))
 Proof
   rw[] >> reverse eq_tac >> rw[] >> gvs[small_eval_dec_def] >>
   PairCases_on `res` >> gvs[small_eval_dec_def]
-  >- (PairCases_on `dev'` >> simp[] >> goal_assum drule >> simp[]) >>
+  >- (PairCases_on `dev'` >> gs[] >> goal_assum drule >> simp[]) >>
   Cases_on `res1` >> gvs[small_eval_dec_def] >>
-  goal_assum drule >> simp[]
+  goal_assum drule >> simp[] >> metis_tac[]
 QED
 
 Theorem small_eval_dec_determ:
@@ -211,7 +212,7 @@ Proof
     qspecl_then [`env`,`dev`,`a`,`b`] assume_tac RTC_decl_step_determ >> gvs[] >>
     unabbrev_all_tac >> Cases_on `err` >> Cases_on `err'` >>
     gvs[decl_step_reln_def, decl_step_def, decl_continue_def] >>
-    metis_tac[PAIR]
+    Cases_on ‘r1’ >> Cases_on ‘r2’ >> gs[state_component_equality]
     )
 QED
 

semantics/alt_semantics/proofs/determScript.sml

@@ -136,7 +136,8 @@ val _ = temp_delsimps["getOpClass_def"]
 Theorem getOpClass_opClass:
   (getOpClass op = FunApp ⇔ opClass op FunApp) ∧
   (getOpClass op = Simple ⇔ opClass op Simple) ∧
-  (getOpClass op = Icing ⇔ opClass op Icing)
+  (getOpClass op = Icing ⇔ opClass op Icing) ∧
+  (getOpClass op = Reals ⇔ opClass op Reals)
 Proof
   Cases_on ‘op’ >> gs[getOpClass_def, opClass_cases]
 QED