Move state_cexp to the right place

Author: myreen

compiler/backend/languages/Holmakefile

@@ -1 +1,2 @@
-INCLUDES = $(PUREDIR)/misc $(PUREDIR)/language
+INCLUDES = $(PUREDIR)/misc $(PUREDIR)/language \
+           $(CAKEMLDIR)/basis/pure

compiler/backend/languages/semantics/Holmakefile

@@ -1 +1,2 @@
-INCLUDES = ../ $(PUREDIR)/language $(PUREDIR)/misc
+INCLUDES = ../ $(PUREDIR)/language $(PUREDIR)/misc \
+           $(CAKEMLDIR)/basis/pure

compiler/backend/languages/semantics/stateLangScript.sml

@@ -12,11 +12,12 @@
 
 open HolKernel Parse boolLib bossLib BasicProvers dep_rewrite;
 open stringTheory optionTheory sumTheory pairTheory listTheory alistTheory
-     pure_expTheory pure_semanticsTheory arithmeticTheory;
+     pure_expTheory pure_semanticsTheory arithmeticTheory
+     state_cexpTheory mlstringTheory;
 
 val _ = new_theory "stateLang";
 
-val _ = set_grammar_ancestry ["pure_semantics"];
+val _ = set_grammar_ancestry ["pure_semantics","state_cexp"];
 
 val _ = numLib.prefer_num();
 
@@ -40,6 +41,8 @@ Datatype:
       | FFI string         (* make an FFI call                         *)
 End
 
+Type vname = “:string”
+
 Datatype:
   exp = (* stateLang expressions *)
       | Var vname                           (* variable                *)
@@ -846,4 +849,40 @@ Proof
   cheat
 QED
 
+(* meaning of cexp *)
+
+Definition sop_of_def[simp]:
+  sop_of (AppOp:csop) = (AppOp:sop) ∧
+  sop_of (Cons n) = Cons (explode n) ∧
+  sop_of (AtomOp m) = AtomOp m ∧
+  sop_of Alloc = Alloc ∧
+  sop_of Ref = Ref ∧
+  sop_of Length = Length ∧
+  sop_of Sub = Sub ∧
+  sop_of UnsafeSub = UnsafeSub ∧
+  sop_of Length = Length ∧
+  sop_of Update = Update ∧
+  sop_of UnsafeUpdate = UnsafeUpdate ∧
+  sop_of (FFI s) = FFI (explode s)
+End
+
+Definition exp_of_def:
+  exp_of ((Var n):cexp) = (Var (explode n)):exp ∧
+  exp_of (App op xs) = App (sop_of op) (MAP exp_of xs) ∧
+  exp_of (Lam vn x) = Lam (OPTION_MAP explode vn) (exp_of x) ∧
+  exp_of (Letrec funs x) =
+    Letrec (MAP (λ(f,v,y). (explode f,Lam (SOME (explode v)) (exp_of y))) funs) (exp_of x) ∧
+  exp_of (Let vn x y) = Let (OPTION_MAP explode vn) (exp_of x) (exp_of y) ∧
+  exp_of (If x y z) = If (exp_of x) (exp_of y) (exp_of z) ∧
+  exp_of (Case x v rows) =
+    Case (exp_of x) (explode v) (MAP (λ(v,vs,y). (explode v,MAP explode vs,exp_of y)) rows) ∧
+  exp_of (Raise x) = Raise (exp_of x) ∧
+  exp_of (Handle x v y) = Handle (exp_of x) (explode v) (exp_of y) ∧
+  exp_of (HandleApp x y) = HandleApp (exp_of x) (exp_of y)
+Termination
+  WF_REL_TAC ‘measure cexp_size’
+End
+
+Theorem exp_of_def[simp] = exp_of_def |> CONV_RULE (DEPTH_CONV ETA_CONV);
+
 val _ = export_theory ();

compiler/backend/passes/proofs/state_cexpScript.sml renamed to compiler/backend/languages/state_cexpScript.sml

@@ -3,12 +3,11 @@
 *)
 open HolKernel Parse boolLib bossLib BasicProvers dep_rewrite;
 open stringTheory optionTheory sumTheory pairTheory listTheory alistTheory
-     pure_expTheory pure_semanticsTheory arithmeticTheory stateLangTheory
-     mlstringTheory;
+     pure_expTheory pure_semanticsTheory arithmeticTheory mlstringTheory;
 
 val _ = new_theory "state_cexp";
 
-val _ = set_grammar_ancestry ["stateLang","mlstring"];
+val _ = set_grammar_ancestry ["pure_exp","mlstring"];
 
 val _ = numLib.prefer_num();
 
@@ -52,38 +51,4 @@ Overload "Unit" = “App (Cons (strlit "")) [] :cexp”;
 Overload IntLit = “λi. App (AtomOp (Lit (Int i))) []”
 Overload Eq = “λx y. App (AtomOp Eq) [x; y]”
 
-Definition sop_of_def[simp]:
-  sop_of (AppOp:csop) = (AppOp:sop) ∧
-  sop_of (Cons n) = Cons (explode n) ∧
-  sop_of (AtomOp m) = AtomOp m ∧
-  sop_of Alloc = Alloc ∧
-  sop_of Ref = Ref ∧
-  sop_of Length = Length ∧
-  sop_of Sub = Sub ∧
-  sop_of UnsafeSub = UnsafeSub ∧
-  sop_of Length = Length ∧
-  sop_of Update = Update ∧
-  sop_of UnsafeUpdate = UnsafeUpdate ∧
-  sop_of (FFI s) = FFI (explode s)
-End
-
-Definition exp_of_def:
-  exp_of ((Var n):cexp) = (Var (explode n)):exp ∧
-  exp_of (App op xs) = App (sop_of op) (MAP exp_of xs) ∧
-  exp_of (Lam vn x) = Lam (OPTION_MAP explode vn) (exp_of x) ∧
-  exp_of (Letrec funs x) =
-    Letrec (MAP (λ(f,v,y). (explode f,Lam (SOME (explode v)) (exp_of y))) funs) (exp_of x) ∧
-  exp_of (Let vn x y) = Let (OPTION_MAP explode vn) (exp_of x) (exp_of y) ∧
-  exp_of (If x y z) = If (exp_of x) (exp_of y) (exp_of z) ∧
-  exp_of (Case x v rows) =
-    Case (exp_of x) (explode v) (MAP (λ(v,vs,y). (explode v,MAP explode vs,exp_of y)) rows) ∧
-  exp_of (Raise x) = Raise (exp_of x) ∧
-  exp_of (Handle x v y) = Handle (exp_of x) (explode v) (exp_of y) ∧
-  exp_of (HandleApp x y) = HandleApp (exp_of x) (exp_of y)
-Termination
-  WF_REL_TAC ‘measure cexp_size’
-End
-
-Theorem exp_of_def[simp] = exp_of_def |> CONV_RULE (DEPTH_CONV ETA_CONV);
-
 val _ = export_theory();

compiler/backend/passes/proofs/state_to_cakeProofScript.sml

@@ -2516,8 +2516,8 @@ Proof
   pop_assum SUBST_ALL_TAC >> simp[] >>
   ntac 9 (qrefine `SUC m` >> simp[dstep, cstep, do_app_def]) >>
   simp[store_lookup_def, copy_array_def, integerTheory.INT_ADD_CALCULATE] >>
-  qmatch_goalsub_abbrev_tac `StrLit str` >>
-  `str = s` by (
+  qmatch_goalsub_abbrev_tac `StrLit str1` >>
+  `str1 = s` by (
     unabbrev_all_tac >> simp[TAKE_APPEND, GSYM MAP_TAKE] >>
     simp[ws_to_chars_def, MAP_MAP_o, combinTheory.o_DEF, IMPLODE_EXPLODE_I]) >>
   pop_assum SUBST_ALL_TAC >>