CakeML-exportable architectural function for V1Model, wrapper CakeML …

…program for V1Model simulation

hol/cake_export/Holmakefile

@@ -10,7 +10,9 @@ DEPENDENCIES   = .. \
  $(CAKEMLDIR)/basis/pure \
  $(CAKEMLDIR)/basis \
  $(CAKEMLDIR)/translator \
- $(CAKEMLDIR)/characteristic
+ $(CAKEMLDIR)/characteristic \
+ $(CAKEMLDIR)/compiler/parsing \
+ $(CAKEMLDIR)/unverified/sexpr-bootstrap
 
 # configuration
 # ----------------------------------

hol/cake_export/p4_exec_sem_arch_cakeProgScript.sml

@@ -127,6 +127,17 @@ Definition arch_exec'_def:
 (arch_exec' _ _ = NONE)
 End
 
+Definition arch_multi_exec'_def:
+ (arch_multi_exec' actx (aenv, g_scope_list, arch_frame_list, status) 0 =
+  SOME (aenv, g_scope_list, arch_frame_list, status))
+  /\
+ (arch_multi_exec' actx (aenv, g_scope_list, arch_frame_list, status) (SUC fuel) =
+  case arch_exec' actx (aenv, g_scope_list, arch_frame_list, status) of
+  | SOME (aenv', g_scope_list', arch_frame_list', status') =>
+   arch_multi_exec' actx (aenv', g_scope_list', arch_frame_list', status') fuel
+  | NONE => NONE)
+End
+
 
 val _ = translation_extends "p4_exec_sem_frames_cakeProg";
 
@@ -144,6 +155,8 @@ val _ = translate set_fin_status_def;
 
 val _ = translate arch_exec'_def;
 
+val _ = translate arch_multi_exec'_def;
+
 val _ = ml_prog_update (close_module NONE);
 
 val _ = export_theory ();

hol/cake_export/p4_exec_sem_e_cakeProgScript.sml

@@ -136,46 +136,6 @@ Termination
  METIS_TAC [v1_size_mem]
 End
 
-Definition slice'_def:
- slice' (v, n) (vec1, len1) (vec2, len2) =
-  let hi = v2n vec1 in
-  let lo = v2n vec2 in
-  if lo <= hi /\ hi < n /\ LENGTH v = n
-  then
-   SOME $ bitv_bitslice (v, n) (v2n vec1) (v2n vec2)
-  else NONE
-End
-
-Definition slice_lval'_def:
- slice_lval' v e1 e2 =
-  case v of
-  | (v_bit (v, bl)) =>
-   (case e1 of
-    | (e_v (v_bit (v1, bl1))) =>
-     (case e2 of
-      | (e_v (v_bit (v2, bl2))) =>
-       (case slice' (v, bl) (v1, bl1) (v2, bl2) of
-        | SOME bitv => SOME $ v_bit bitv
-        | NONE => NONE)
-      | _ => NONE)
-    | _ => NONE)
-  | _ => NONE
-End
-
-Definition lookup_lval'_def:
- (lookup_lval' (ss:scope list) (lval_varname x) = lookup_v ss x) /\
- (lookup_lval' ss (lval_field lval f) =
-  case lookup_lval' ss lval of
-  | SOME v => acc_f v f
-  | NONE => NONE) /\
- (lookup_lval' ss (lval_slice lval e1 e2) =
-  case lookup_lval' ss lval of
-   | SOME (v_bit (v, bl)) => slice_lval' (v_bit (v, bl)) e1 e2
-   | _ => NONE) /\
- (lookup_lval' ss lval_null = NONE ) /\
- (lookup_lval' ss (lval_paren lval) = lookup_lval' ss lval) 
-End
-
 
 Definition one_arg_val_for_newscope'_def:
  one_arg_val_for_newscope' d e ss =
@@ -1030,25 +990,4 @@ val _ = translate e_exec'_def;
 
 val _ = ml_prog_update (close_module NONE);
 
-(*
-(* To print the resulting CakeML program *)
-fun get_current_prog () =
-  let
-    val state = get_ml_prog_state ()
-    val state_thm =
-     state |> ml_progLib.remove_snocs
-           |> ml_progLib.clean_state
-           |> get_thm
-  in
-    state_thm |> concl |> strip_comb |> #2 |> el 2
-  end
-;
-
-val _ = astPP.enable_astPP();
-
-val _ = print_term (get_current_prog ());
-
-val _ = astPP.disable_astPP();
-*)
-
 val _ = export_theory ();

hol/cake_export/p4_exec_sem_stmt_cakeProgScript.sml

@@ -46,62 +46,6 @@ Definition declare_list_in_fresh_scope'_def:
   MAP (\(x, (t, lvalop)). (x, (init_v_from_tau_cake t, NONE))) t_scope
 End
 
-(* Puts the bits in bl1 between index hi and lo of bl2. *)
-Definition replace_bits_def:
- replace_bits (bl1, (n1:num)) (bl2,n2) hi lo =
-  if lo <= hi /\ hi < n2 /\ LENGTH bl2 = n2
-  then
-   SOME $ (SEG (n2-(hi+1)) 0 bl2) ++ bl1 ++ (SEG lo (n2-lo) bl2)
-  else NONE
-End
-
-Definition assign_to_slice'_def:
- assign_to_slice' vb vb' ev1 ev2 =
-  (case ev1 of
-   | (e_v (v_bit (bl1, n1))) =>
-    (case ev2 of
-     | (e_v (v_bit (bl2, n2))) =>
-      (case replace_bits vb vb' (v2n bl1) (v2n bl2) of
-       | SOME bitv =>
-        SOME $ v_bit (bitv, SND vb')
-       | NONE => NONE)
-     | _ => NONE)
-   | _ => NONE)
-End
-
-Definition assign'_def:
- (assign' ss v (lval_varname x) =
-  case find_topmost_map ss x of
-  | SOME (i, sc) =>
-   (case lookup_out ss x of
-    | SOME str_opt =>
-      SOME (LUPDATE (AUPDATE sc (x, (v, str_opt))) i ss)
-    | NONE => NONE)
-  | _ => NONE) /\
- (assign' ss v (lval_field lval f) =
-  case lookup_lval' ss lval of
-  | SOME (v_struct f_v_l) =>
-   (case INDEX_OF f (MAP FST f_v_l) of
-    | SOME i => assign' ss (v_struct (LUPDATE (f, v) i f_v_l)) lval
-    | NONE => NONE)
-  | SOME (v_header validity f_v_l) =>
-   (case INDEX_OF f (MAP FST f_v_l) of
-    | SOME i => assign' ss (v_header validity (LUPDATE (f, v) i f_v_l)) lval
-    | NONE => NONE)
-   | _ => NONE) /\    
- (assign' ss v (lval_slice lval ev1 ev2) =
-  case v of
-  | v_bit vb =>
-   (case lookup_lval' ss lval of
-    | SOME (v_bit vb') =>
-     (case assign_to_slice' vb vb' ev1 ev2 of
-      | SOME v_res => assign' ss v_res lval
-      | _ => NONE)
-    | _ => NONE)
-  | _ => NONE) /\
- (assign' ss v lval_null = SOME ss) /\
- (assign' ss v (lval_paren lval) = assign' ss v lval)
-End
 
 Definition stmt_exec_ass'_def:
  (stmt_exec_ass' lval (e_v v) ss = assign' ss v lval) /\