test files in examples/arm_cm0/balrob

examples/arm_cm0/balrob/balrob_ftop_test2Script.sml

@@ -0,0 +1,53 @@
+open HolKernel Parse boolLib bossLib;
+
+open balrob_supportLib;
+open birsSyntax;
+open birs_utilsLib;
+
+open balrob_ftop_testTheory;
+
+val _ = new_theory "balrob_ftop_test2";
+
+(*
+val symb_exec_thm = balrob_test_ftop_thm3;
+val symb_exec_thm = balrob_test_ftop_thm2;
+val symb_exec_thm = balrob_test_ftop_thm4;
+*)
+val symb_exec_thm = balrob_test_ftop_thm;
+
+fun print_mem sys =
+  let
+    val env = dest_birs_state_env sys;
+    val mappings = get_env_mappings env;
+    val mappings_ = List.filter ((fn x => x = "MEM") o stringSyntax.fromHOLstring o fst) mappings;
+    val mem_exp = (snd o hd) mappings_;
+    (*val _ = print_term mem_exp;*)
+    val (mexp, stores) = birs_simp_instancesLib.dest_BExp_Store_list mem_exp [];
+    val _ = print ("MEM " ^ (term_to_string mexp) ^ " [\n");
+    fun print_store (expad, _, expv) =
+      let
+        val expad_s = term_to_string expad;
+        val expv_s = term_to_string expv;
+        val expv_s = if String.size expv_s > 100 then "(...)" else expv_s;
+        val _ = print ("  " ^ expad_s ^ "\n    -> " ^ expv_s ^ "\n");
+      in () end;
+    val _ = map (print_store) stores;
+    val _ = print ("]\n");
+  in () end;
+
+(*
+val Pis = (get_birs_Pi_list o concl) symb_exec_thm;
+val _ = List.map
+  (fn sys =>
+    let
+      val _ = print_mem sys;
+    in () end)
+  Pis;
+*)
+
+val proc_thm = balrob_supportLib.birs_basic_merge symb_exec_thm;
+
+val entry_name = "ftop";
+val _ = save_thm("balrob_summary_" ^ entry_name ^ "_thm", proc_thm);
+
+val _ = export_theory ();

examples/arm_cm0/balrob/balrob_top_test2Script.sml

@@ -0,0 +1,53 @@
+open HolKernel Parse boolLib bossLib;
+
+open balrob_supportLib;
+open birsSyntax;
+open birs_utilsLib;
+
+open balrob_top_testTheory;
+
+val _ = new_theory "balrob_top_test2";
+
+(*
+val symb_exec_thm = balrob_test_top_thm3;
+val symb_exec_thm = balrob_test_top_thm2;
+val symb_exec_thm = balrob_test_top_thm4;
+*)
+val symb_exec_thm = balrob_test_top_thm;
+
+fun print_mem sys =
+  let
+    val env = dest_birs_state_env sys;
+    val mappings = get_env_mappings env;
+    val mappings_ = List.filter ((fn x => x = "MEM") o stringSyntax.fromHOLstring o fst) mappings;
+    val mem_exp = (snd o hd) mappings_;
+    (*val _ = print_term mem_exp;*)
+    val (mexp, stores) = birs_simp_instancesLib.dest_BExp_Store_list mem_exp [];
+    val _ = print ("MEM " ^ (term_to_string mexp) ^ " [\n");
+    fun print_store (expad, _, expv) =
+      let
+        val expad_s = term_to_string expad;
+        val expv_s = term_to_string expv;
+        val expv_s = if String.size expv_s > 100 then "(...)" else expv_s;
+        val _ = print ("  " ^ expad_s ^ "\n    -> " ^ expv_s ^ "\n");
+      in () end;
+    val _ = map (print_store) stores;
+    val _ = print ("]\n");
+  in () end;
+
+(*
+val Pis = (get_birs_Pi_list o concl) symb_exec_thm;
+val _ = List.map
+  (fn sys =>
+    let
+      val _ = print_mem sys;
+    in () end)
+  Pis;
+*)
+
+val proc_thm = balrob_supportLib.birs_basic_merge symb_exec_thm;
+
+val entry_name = "top";
+val _ = save_thm("balrob_summary_" ^ entry_name ^ "_thm", proc_thm);
+
+val _ = export_theory ();