Compile a few example timeLang programs

Author: myreen

pancake/README.md

@@ -65,6 +65,9 @@ This is an example compilation of a TA program
 [ta_progs](ta_progs):
 Some sample timed automata (TA) programs.
 
+[temp](temp):
+Temporary files
+
 [timeLangScript.sml](timeLangScript.sml):
 Abstract syntax for timeLang
 

pancake/crepLangScript.sml

@@ -28,6 +28,7 @@ Datatype:
       | Op binop (exp list)
       | Cmp cmp exp exp
       | Shift shift exp num
+      | BaseAddr
 End
 
 Datatype:

pancake/crep_to_loopScript.sml

@@ -42,6 +42,7 @@ End
 
 
 Definition compile_exp_def:
+  (compile_exp ctxt tmp l ((BaseAddr):'a crepLang$exp) = ([], BaseAddr, tmp, l)) /\
   (compile_exp ctxt tmp l ((Const c):'a crepLang$exp) = ([], Const c, tmp, l)) /\
   (compile_exp ctxt tmp l (Var v) = ([], Var (find_var ctxt v), tmp, l)) /\
   (compile_exp ctxt tmp l (Label f) = ([LocValue tmp (find_lab ctxt f)],

pancake/loopLangScript.sml

@@ -16,6 +16,7 @@ Datatype:
       | Load exp
       | Op binop (exp list)
       | Shift shift exp num
+      | BaseAddr
 End
 
 Datatype:

pancake/loop_liveScript.sml

@@ -11,6 +11,7 @@ val _ = new_theory "loop_live";
 Definition vars_of_exp_def:
   vars_of_exp (loopLang$Var v) l = insert v () l ∧
   vars_of_exp (Const _) l = l ∧
+  vars_of_exp (BaseAddr) l = l ∧
   vars_of_exp (Lookup _) l = l ∧
   vars_of_exp (Load a) l = vars_of_exp a l ∧
   vars_of_exp (Op x vs) l = vars_of_exp_list vs l ∧

pancake/loop_to_wordScript.sml

@@ -28,6 +28,7 @@ Definition comp_exp_def :
   (comp_exp ctxt (loopLang$Const w) = wordLang$Const w) /\
   (comp_exp ctxt (Var n) = Var (find_var ctxt n)) /\
   (comp_exp ctxt (Lookup m) = Lookup (Temp m)) /\
+  (comp_exp ctxt (BaseAddr) = Lookup CurrHeap) /\
   (comp_exp ctxt (Load exp) = Load (comp_exp ctxt exp)) /\
   (comp_exp ctxt (Shift s exp n) = Shift s (comp_exp ctxt exp) n) /\
   (comp_exp ctxt (Op op wexps) =

pancake/panLangScript.sml

@@ -44,6 +44,7 @@ Datatype:
       | Op binop (exp list)
       | Cmp cmp exp exp
       | Shift shift exp num
+      | BaseAddr
 End
 
 Datatype:

pancake/pan_to_crepScript.sml

@@ -73,7 +73,8 @@ Definition compile_exp_def:
   (compile_exp ctxt (Shift sh e n) =
    case FST (compile_exp ctxt e) of
    | [] => ([Const 0w], One)
-   | e::es => ([Shift sh e n], One))
+   | e::es => ([Shift sh e n], One)) /\
+  (compile_exp ctxt BaseAddr = ([BaseAddr], One))
 Termination
   wf_rel_tac `measure (\e. panLang$exp_size ARB (SND e))` >>
   rpt strip_tac >>

pancake/temp/README.md

@@ -0,0 +1 @@
+Temporary files