changed the implementation to keep the alists and commented out the sptrees implementation

Author: AnoudAlshnakat

hol/policy_to_table/bdd_cake_trans/apply_trans_to_IOLib.sig

@@ -2,7 +2,7 @@ signature apply_trans_to_IOLib =
 sig
   include Abbrev
 
-   val sptrees_gen_bdds_policy_and_table : term * term * term -> (term * term * term)
+   val gen_bdds_policy_and_table_cake : term * term * term -> (term * term * term)
    val time_stage : string * Timer.cpu_timer * Timer.real_timer -> {sys: Time.time, usr: Time.time} * Time.time
 
 end

hol/policy_to_table/bdd_cake_trans/apply_trans_to_IOLib.sml

@@ -4,23 +4,19 @@ structure apply_trans_to_IOLib :> apply_trans_to_IOLib = struct
 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 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 _ = translation_extends "bdd_trans_Prog";
 
 
 
 val _ = type_abbrev("action_policy_type", “:((string# num list) action_expr) policy”);
 
-
-
 fun time_stage (stage_name, timer_cpu, timer_real) = 
         let
             val cpu_time = Timer.checkCPUTimer timer_cpu
@@ -34,10 +30,7 @@ fun time_stage (stage_name, timer_cpu, timer_real) =
 end
 
 
-
-
-
-fun sptrees_gen_bdds_policy_and_table (var_policy, policy_order, policy_full_order) =
+fun gen_bdds_policy_and_table_cake (var_policy, policy_order, policy_full_order) =
 
 let
 
@@ -61,21 +54,10 @@ 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 
-
-
-(* 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 *)
+End
 
 val r = translate policy_main_hol4_def;
 
@@ -224,21 +206,10 @@ End
 val r = translate table_content_test_def;
 
 
-Definition table_main_hol4_def:
-  table_main_hol4 =
-  case sp_mk_BDD_table table_content_test policy_order_test of
-  | NONE => NONE
-  | SOME (r,sp_edges,sp_labels) => SOME (r,
-                                         ((toSortedAList sp_edges):edges),
-                                         ((toSortedAList sp_labels): (action_table_type, (string#num list) action_expr) labelings) )
-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 *)
+End
 
 
 val r = translate table_main_hol4_def;

…/bdd_cake_trans/sptrees_fwd_proofLib.sig …ble/bdd_cake_trans/fwd_proof_cakeLib.sighol/policy_to_table/bdd_cake_trans/sptrees_fwd_proofLib.sig renamed to hol/policy_to_table/bdd_cake_trans/fwd_proof_cakeLib.sig hol/policy_to_table/bdd_cake_trans/sptrees_fwd_proofLib.sig renamed to hol/policy_to_table/bdd_cake_trans/fwd_proof_cakeLib.sig

@@ -1,9 +1,9 @@
-signature sptrees_fwd_proofLib =
+signature fwd_proof_cakeLib =
 sig
   include Abbrev
 
 
-        val sptrees_convert_arith_policy_to_interval_tables : term * term * term * term * term -> thm
+        val convert_arith_policy_to_interval_tables_cake : term * term * term * term * term -> thm
         val time_stage : string * Timer.cpu_timer * Timer.real_timer -> {sys: Time.time, usr: Time.time} * Time.time
 
 

…/bdd_cake_trans/sptrees_fwd_proofLib.sml …ble/bdd_cake_trans/fwd_proof_cakeLib.smlhol/policy_to_table/bdd_cake_trans/sptrees_fwd_proofLib.sml renamed to hol/policy_to_table/bdd_cake_trans/fwd_proof_cakeLib.sml hol/policy_to_table/bdd_cake_trans/sptrees_fwd_proofLib.sml renamed to hol/policy_to_table/bdd_cake_trans/fwd_proof_cakeLib.sml

@@ -1,4 +1,4 @@
-structure sptrees_fwd_proofLib :> sptrees_fwd_proofLib = struct
+structure fwd_proof_cakeLib :> fwd_proof_cakeLib = struct
 
 
 open HolKernel boolLib liteLib simpLib Parse bossLib pairLib;
@@ -57,7 +57,7 @@ open apply_trans_to_IOLib;
 
 
 
-    fun sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order) =
+    fun convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order) =
 
         let
 
@@ -94,7 +94,7 @@ open apply_trans_to_IOLib;
             val start_real_total_stage2 = Timer.startRealTimer (); 
 
             val (final_policy_bdd, tbl, final_table_bdd) =
-            apply_trans_to_IOLib.sptrees_gen_bdds_policy_and_table (var_policy, policy_order, policy_full_order);
+            apply_trans_to_IOLib.gen_bdds_policy_and_table_cake (var_policy, policy_order, policy_full_order);
 
             val _ = time_stage ("Stage 2 TOTAL BEFORE PROOF", start_cpu_total, start_real_total) 
 

hol/policy_to_table/bdd_cake_trans/sptrees_bdd_trans_ProgScript.sml

@@ -1,14 +1,18 @@
 open HolKernel Parse boolLib bossLib;
+(*
 open optionTheory bdd_sptrees_genTheory pairTheory bdd_genTheory tables_specTheory tables_spec_oldTheory policy_specTheory pred_specTheory;
 open preamble basis ml_translatorLib ;
 
 open miscTheory ml_translatorTheory ListProgTheory ;
 open fromSexpTheory;
-
+*)
 
 
 val _ = new_theory "sptrees_bdd_trans_Prog";
 
+(*
+
+
 (*)
  val _ = ml_prog_update (open_module "cake_sptrees_bdd_trans_Prog");
 *)
@@ -756,6 +760,10 @@ end;
 val _ = ml_prog_update (close_module NONE);
 *)
 
+
+
+*)
+
 val _ = export_theory ();