Fix some repl proofs

CakeML · Oct 7, 2022 · e63dc62 · e63dc62
1 parent 9f02fb9
commit e63dc62
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 0 deletions.
diff --git a/compiler/repl/evaluate_initScript.sml b/compiler/repl/evaluate_initScript.sml
@@ -675,6 +675,11 @@ Proof
     \\ ‘s with <| refs := s.refs; ffi := s.ffi |> = s’ suffices_by gs[]
     \\ gs[state_component_equality])
   \\ Cases_on ‘op = RealFromFP’ \\ gs[]
+  >- (
+    gvs[do_app_cases, v_ok_thm]
+    \\ ‘s with <| refs := s.refs; ffi := s.ffi |> = s’ suffices_by gs[]
+    \\ gs[state_component_equality])
+  \\ Cases_on ‘op = RealFromIntProd’ \\ gs[]
   >- (
     gvs[do_app_cases, v_ok_thm]
     \\ ‘s with <| refs := s.refs; ffi := s.ffi |> = s’ suffices_by gs[]

diff --git a/compiler/repl/evaluate_skipScript.sml b/compiler/repl/evaluate_skipScript.sml
@@ -1790,6 +1790,13 @@ Proof
     \\ rpt (irule_at Any SUBMAP_REFL) \\ gs []
     \\ first_assum (irule_at Any) \\ gs [])
   \\ Cases_on ‘op = RealFromFP’ \\ gs[]
+  >- (
+    Cases_on ‘res’ \\ gvs [do_app_def, v_rel_def, OPTREL_def,
+                           CaseEqs ["list", "v", "option", "prod", "lit",
+                                    "store_v", "v"]]
+    \\ rpt (irule_at Any SUBMAP_REFL) \\ gs []
+    \\ first_assum (irule_at Any) \\ gs [])
+  \\ Cases_on ‘op = RealFromIntProd’ \\ gs[]
   >- (
     Cases_on ‘res’ \\ gvs [do_app_def, v_rel_def, OPTREL_def,
                            CaseEqs ["list", "v", "option", "prod", "lit",