according to this commit, we decided to ignore the sptrees implementation and focus on alists

Author: AnoudAlshnakat

hol/policy_to_table/bdd_cake_trans/apply_trans_to_IOLib.sml

@@ -5,13 +5,16 @@ open HolKernel Parse boolLib bossLib;
 open optionTheory bdd_sptrees_genTheory pairTheory bdd_genTheory tables_specTheory tables_spec_oldTheory policy_specTheory pred_specTheory;
 
 open sptrees_bdd_trans_ProgTheory;
+(* open bdd_trans_ProgTheory; *)
 open preamble basis ml_translatorLib ;
 
 open miscTheory ;
 open fromSexpTheory;
 
 
 val _ = translation_extends "sptrees_bdd_trans_Prog";
+(* val _ = translation_extends "bdd_trans_Prog";  *)
+
 
 
 val _ = type_abbrev("action_policy_type", “:((string# num list) action_expr) policy”);
@@ -41,6 +44,9 @@ let
 val start_cpu_stage2_io = Timer.startCPUTimer ();
 val start_real_stage2_io = Timer.startRealTimer (); 
 
+(**********************************************************)
+(*         prepp policy:  translation to CakeML           *)
+(**********************************************************)
 
 Definition policy_order_test_def:
  policy_order_test = (^policy_order:string list)
@@ -55,18 +61,21 @@ End
 val r = translate policy_content_test_def;
 
 
+
 Definition policy_main_hol4_def:
   policy_main_hol4 =
   case sp_mk_BDD_policy policy_content_test  policy_order_test of
   | NONE => NONE
   | SOME (r,sp_edges,sp_labels) => SOME (r,
                                          ((toSortedAList sp_edges):edges),
                                          ((toSortedAList sp_labels): (((string#num list) action_expr) policy, (string#num list) action_expr) labelings) )
-End
-
-
+End 
 
 
+(* Definition policy_main_hol4_def:
+  policy_main_hol4   =
+  mk_BDDPred_opt (policy_structure) (0,[],[(0, non_termn (NONE, policy_content_test))]) [] (policy_order_test) 1n
+End *)
 
 val r = translate policy_main_hol4_def;
 
@@ -108,12 +117,11 @@ val prog =
   `` |> EVAL |> concl |> rhs;
 
 
-
+(* write the translation to an sexp file *)
 val _ = astToSexprLib.write_ast_to_file "../../bdd_cake_test/test_bdd_policy.sexp" prog;
 
-val _ = time_stage ("Stage 2 from var policy to sexp - cakeML trans ", start_cpu_stage2_io, start_real_stage2_io);
-val start_cpu_stage2_io2 = Timer.startCPUTimer ();
-val start_real_stage2_io2 = Timer.startRealTimer (); 
+val _ = print "AA:finished trans \n";
+
 
 val status_compile_sexp = OS.Process.system  "cd ../../bdd_cake_test/ && CML_STACK_SIZE=2048 CML_HEAP_SIZE=8192 ./cake --sexp=true --exclude_prelude=true --skip_type_inference=false --jump=false --reg_alg=0 < test_bdd_policy.sexp > test_bdd_policy.cake.S"
 
@@ -129,42 +137,46 @@ val _ = if OS.Process.isSuccess status_cc
         else (print "Nej, policy cc compilation failed\n";
               OS.Process.exit OS.Process.failure)
 
+val _ = time_stage ("Stage 2 translate var POLICY term to sexp, cc compile, link for cakeML prepp ", start_cpu_stage2_io, start_real_stage2_io);
+val start_cpu_stage2_io2 = Timer.startCPUTimer ();
+val start_real_stage2_io2 = Timer.startRealTimer (); 
+
+(************************************************************)
+(*    Compile policy's translation using CakeML compiler    *)
+(************************************************************)
+
+
 val status_exec = OS.Process.system  "cd ../../bdd_cake_test/ && time ./test_bdd_policy.cake > bdd_policy_cakeml_export.txt";
 
 val _ = if OS.Process.isSuccess status_exec 
-        then print "Ja, policy cc compilation completed\n"
-        else (print "Nej, policy cc compilation failed\n";
+        then print "Ja, policy BDD compilation completed\n"
+        else (print "Nej, policy NDD compilation failed\n";
               OS.Process.exit OS.Process.failure)
 
-val _ = time_stage ("Stage 2 cakeML compiliation var policy to bdd ", start_cpu_stage2_io2, start_real_stage2_io2);
+
+
+val _ = time_stage ("Stage 2 cakeML compilation var policy to BDD ", start_cpu_stage2_io2, start_real_stage2_io2);
+
 val start_cpu_stage2_io3 = Timer.startCPUTimer ();
 val start_real_stage2_io3 = Timer.startRealTimer (); 
 
 (*
-
+Individual commands:
 cp test_bdd_policy.sexp ../../bdd_cake_test
-
 CML_STACK_SIZE=2048 CML_HEAP_SIZE=8192 ./cake --sexp=true --exclude_prelude=true --skip_type_inference=false --jump=false --reg_alg=0 < test_bdd_policy.sexp > test_bdd_policy.cake.S
-
 cc test_bdd_policy.cake.S basis_ffi.c -lm -o test_bdd_policy.cake -lm
-
 time ./test_bdd_policy.cake > bdd_policy_cakeml_export.txt
-
-
 *)
 
 
-
-
-
-
-
+(************************************************************)
+(*       Fetch policy's BDD from the output text file       *)
+(************************************************************)
 
 val ins = TextIO.openIn "../../bdd_cake_test/bdd_policy_cakeml_export.txt";
 val policy_content_str = TextIO.inputAll ins;
 val _ = TextIO.closeIn ins;
 
-val _ = time_stage ("Stage 2 from Policy to var BDD total ", start_cpu_stage2_io, start_real_stage2_io);
 
 (*open Term;*)
 
@@ -187,15 +199,24 @@ val policy_bdd_content_term =
         parsed
 end;
 
+val _ = print "AA:finished cleaning input \n";
 
 
 
+(************************************************************)
+(*            Generate a table using sml function           *)
+(************************************************************)
 
 val test_groupings = rhs(concl(EVAL policy_full_order));
 val gen_var_table_auto = bdd_utilsLib.bdd_to_tables_iterative policy_bdd_content_term test_groupings;
 
+val _ = print "AA:finished creating table \n";
 
 
+(**********************************************************)
+(*          prepp table:  translation to CakeML           *)
+(**********************************************************)
+
 Definition table_content_test_def:
   table_content_test = (^gen_var_table_auto : action_table_type)
 End
@@ -213,6 +234,13 @@ Definition table_main_hol4_def:
 End
 
 
+(* 
+Definition table_main_hol4_def:
+  table_main_hol4 =
+  mk_BDDPred_opt (table_structure) (0,[],[(0, non_termn (NONE, table_content_test))]) [] (policy_order_test) 1n
+End *)
+
+
 val r = translate table_main_hol4_def;
 
 
@@ -254,33 +282,44 @@ val prog =
 
 val _ = astToSexprLib.write_ast_to_file "../../bdd_cake_test/test_bdd_table.sexp" prog;
 
-val _ = time_stage ("Stage 2 prepp out table and recompile cakeml translation ", start_cpu_stage2_io3, start_real_stage2_io3);
-val start_cpu_stage2_io4 = Timer.startCPUTimer ();
-val start_real_stage2_io4 = Timer.startRealTimer (); 
+val _ = print "AA:finished translating table \n";
 
 
+val status = OS.Process.system  "cd ../../bdd_cake_test/ && CML_STACK_SIZE=2048 CML_HEAP_SIZE=8192 ./cake --sexp=true --exclude_prelude=true --skip_type_inference=false --jump=false --reg_alg=0 < test_bdd_table.sexp > test_bdd_table.cake.S && cc test_bdd_table.cake.S basis_ffi.c -lm -o test_bdd_table.cake -lm"
 
-val status = OS.Process.system  "cd ../../bdd_cake_test/ && CML_STACK_SIZE=2048 CML_HEAP_SIZE=8192 ./cake --sexp=true --exclude_prelude=true --skip_type_inference=false --jump=false --reg_alg=0 < test_bdd_table.sexp > test_bdd_table.cake.S && cc test_bdd_table.cake.S basis_ffi.c -lm -o test_bdd_table.cake -lm && time ./test_bdd_table.cake > bdd_table_cakeml_export.txt"
+val _ = time_stage ("Stage 2 translate var TABLE term to sexp, cc compile, link for cakeML prepp ", start_cpu_stage2_io3, start_real_stage2_io3);
+val start_cpu_stage2_io4 = Timer.startCPUTimer ();
+val start_real_stage2_io4 = Timer.startRealTimer (); 
 
 val _ = if OS.Process.isSuccess status
-        then print "Ja, table cakeML compilation completed\n"
-        else (print "Nej, table cakeML compilation failed\n";
+        then print "Ja, table BDD compilation completed\n"
+        else (print "Nej, table BDD compilation failed\n";
               OS.Process.exit OS.Process.failure)
 
+(************************************************************)
+(*    Compile table's translation using CakeML compiler     *)
+(************************************************************)
+
+val status = OS.Process.system  "cd ../../bdd_cake_test/ && time ./test_bdd_table.cake > bdd_table_cakeml_export.txt"
+
+val _ = time_stage ("Stage 2 cakeML compilation var TABLE to BDD ", start_cpu_stage2_io4, start_real_stage2_io4);
+
 
+(************************************************************)
+(*       Fetch table's BDD from the output text file        *)
+(************************************************************)
 
 (*
 reset_translation
 val _ = astPP.enable_astPP ();
 val _ = (max_print_depth := 200);
 *)
 
-
-
 val ins = TextIO.openIn "../../bdd_cake_test/bdd_table_cakeml_export.txt";
 val tbl_content_str = TextIO.inputAll ins;
 val _ = TextIO.closeIn ins;
 
+val _ = print "AA:finished getting sexp table to hol4 \n";
 
 
 
@@ -303,11 +342,7 @@ val table_bdd_content_term =
         parsed
 end;
 
-
-
-val _ = time_stage ("Stage 2 cakeML compiliation var table to BDD ", start_cpu_stage2_io4, start_real_stage2_io4);
-
-val _ = time_stage ("Stage 2 from TABLE to var BDD total ", start_cpu_stage2_io3, start_real_stage2_io3);
+val _ = print "AA:finished cleaning sexp table in hol4 \n";
 
 in 
 (policy_bdd_content_term, gen_var_table_auto, table_bdd_content_term)