changed the names of the files that compiles the input with cakeML

AnoudAlshnakat · AnoudAlshnakat · commit a31b6182e298 · 2025-12-29T00:20:05.000+01:00
diff --git a/hol/policy_to_table/bdd_cake_trans/fwd_proof_cake_w_IOLib.sig b/hol/policy_to_table/bdd_cake_trans/fwd_proof_cake_w_IOLib.sig
@@ -1,4 +1,4 @@
-signature fwd_proof_cakeLib =
+signature fwd_proof_w_IOcakeLib =
 sig
   include Abbrev
 
diff --git a/hol/policy_to_table/bdd_cake_trans/fwd_proof_cake_w_IOLib.sml b/hol/policy_to_table/bdd_cake_trans/fwd_proof_cake_w_IOLib.sml
@@ -1,4 +1,4 @@
-structure fwd_proof_cakeLib :> fwd_proof_cakeLib = struct
+structure fwd_proof_w_IOcakeLib :> fwd_proof_w_IOcakeLib = struct
 
 
 open HolKernel boolLib liteLib simpLib Parse bossLib pairLib;
@@ -57,7 +57,10 @@ open apply_trans_to_IOLib;
 
 
 
-    fun convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order) =
+    fun convert_arith_policy_to_interval_tables_cake_w_IO (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order) =
+
+       (* this compiles the input with cakeML It takes a very longer time, so I created a parser in CakeML, This should be in fwd_proof_cakeLib file*)
+
 
         let
             

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-signature fwd_proof_cakeLib =`
	`1`	`+signature fwd_proof_w_IOcakeLib =`
`2`	`2`	`sig`
`3`	`3`	`include Abbrev`
`4`	`4`