Skip to content

Commit f7041a2

Browse files
AnoudAlshnakatAnoudAlshnakat
committed
edited the cakeML files, and the test cases according to the renaming of the previous commit
1 parent 8d59cce commit f7041a2

26 files changed

+1045
-1130
lines changed

‎hol/policy_to_table/bdd_cake_trans/apply_trans_to_IOLib.sml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ structure apply_trans_to_IOLib :> apply_trans_to_IOLib = struct
22

33

44
open HolKernel Parse boolLib bossLib;
5-
open optionTheory bdd_sptrees_genTheory pairTheory bdd_genTheory tables_specTheory tables_spec_oldTheory policy_specTheory pred_specTheory;
5+
open optionTheory pairTheory bdd_genTheory tables_specTheory tables_spec_oldTheory policy_specTheory pred_specTheory;
66

77
open bdd_trans_ProgTheory;
88
open preamble basis ml_translatorLib ;

‎hol/policy_to_table/bdd_cake_trans/bdd_trans_ProgScript.sml‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,9 @@
11
open HolKernel Parse boolLib bossLib;
2-
open optionTheory bdd_sptrees_genTheory pairTheory bdd_genTheory tables_specTheory tables_spec_oldTheory policy_specTheory pred_specTheory;
2+
open optionTheory pairTheory bdd_genTheory tables_specTheory tables_spec_oldTheory policy_specTheory pred_specTheory;
33

44
open preamble basis ml_translatorLib ;
55

66
open miscTheory ml_translatorTheory ListProgTheory ;
7-
open fromSexpTheory;
87

98

109

‎hol/policy_to_table/bdd_cake_trans/common_parse_cakeml_ProgScript.sml‎

Lines changed: 131 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,131 @@
1+
open HolKernel Parse boolLib bossLib;
2+
open preamble basis ml_translatorLib ;
3+
4+
open bdd_trans_ProgTheory;
5+
6+
7+
8+
val _ = new_theory "common_parse_cakeml_Prog";
9+
10+
11+
12+
val _ = translation_extends "bdd_trans_Prog"
13+
val _ = intLib.deprecate_int();
14+
15+
16+
17+
val res = append_prog o process_topdecs $
18+
‘
19+
(* Helper function to check if character is whitespace *)
20+
fun is_whitespace c = c = #" " orelse c = #"\n" orelse c = #"\t" orelse c = #"\r";
21+
22+
23+
(* Skip whitespace and return remaining string *)
24+
fun skip_ws s =
25+
case s of
26+
[] => []
27+
| c::rest => if is_whitespace c then skip_ws rest else c::rest;
28+
29+
30+
(* Helper to check if character is a digit *)
31+
fun is_digit c = (c = #"0") orelse (c = #"1") orelse (c = #"2") orelse (c = #"3")
32+
orelse (c = #"4") orelse (c = #"5") orelse (c = #"6")
33+
orelse (c = #"7") orelse (c = #"8") orelse (c = #"9");
34+
(* Convert character digit to int *)
35+
fun char_to_digit c =
36+
if c = #"0" then 0
37+
else if c = #"1" then 1
38+
else if c = #"2" then 2
39+
else if c = #"3" then 3
40+
else if c = #"4" then 4
41+
else if c = #"5" then 5
42+
else if c = #"6" then 6
43+
else if c = #"7" then 7
44+
else if c = #"8" then 8
45+
else if c = #"9" then 9
46+
else 0;
47+
(* Parse a variable name (quoted) - returns char list and remaining *)
48+
fun parse_var_name s =
49+
case s of
50+
#"\"" :: rest =>
51+
let fun read_until_quote acc s =
52+
case s of
53+
[] => (List.rev acc, [])
54+
| #"\"" :: rest => (List.rev acc, rest)
55+
| c :: rest => read_until_quote (c :: acc) rest
56+
in read_until_quote [] rest
57+
end
58+
| _ => ([], s);
59+
(* Parse an integer - returns int and remaining *)
60+
fun parse_int s =
61+
let fun read_digits acc s =
62+
case s of
63+
[] => (acc, [])
64+
| c::rest => if is_digit c
65+
then read_digits (acc * 10 + char_to_digit c) rest
66+
else (acc, c::rest)
67+
in
68+
case s of
69+
#"-"::rest =>
70+
let val (num, rest) = read_digits 0 rest
71+
in (~num, rest)
72+
end
73+
| _ => read_digits 0 s
74+
end;
75+
(* Parse a list of integers: [1;2;3] *)
76+
fun parse_int_list s =
77+
let val s = skip_ws s in
78+
case s of
79+
#"[" :: rest =>
80+
let val s = skip_ws rest
81+
fun parse_list acc s =
82+
let val s = skip_ws s in
83+
case s of
84+
#"]" :: rest => (List.rev acc, skip_ws rest)
85+
| _ =>
86+
let val (n, s) = parse_int s
87+
val s = skip_ws s
88+
in case s of
89+
#";" :: rest => parse_list (n :: acc) (skip_ws rest)
90+
| #"]" :: rest => (List.rev (n :: acc), skip_ws rest)
91+
| _ => (List.rev (n :: acc), s)
92+
end
93+
end
94+
in parse_list [] s
95+
end
96+
| _ => ([], s)
97+
end;
98+
(* Helper to convert int list to string *)
99+
fun int_list_to_string nums =
100+
case nums of
101+
[] => ""
102+
| n::rest =>
103+
case rest of
104+
[] => Int.toString n
105+
| _ => Int.toString n ^ ";" ^ int_list_to_string rest;
106+
(* Skip closing parentheses *)
107+
fun skip_close_parens s =
108+
let val s = skip_ws s in
109+
case s of
110+
#")" :: rest => skip_close_parens (skip_ws rest)
111+
| _ => s
112+
end;
113+
114+
(* Skip opening parentheses *)
115+
fun skip_open_parens s =
116+
let val s = skip_ws s in
117+
case s of
118+
#"(" :: rest => skip_open_parens (skip_ws rest)
119+
| _ => s
120+
end;
121+
122+
’;
123+
124+
125+
(*
126+
val _ = astPP.enable_astPP ();
127+
val _ = (max_print_depth := 700);
128+
*)
129+
130+
131+
val _ = export_theory ();

‎hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_10Script.sml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -435,9 +435,9 @@ val policy_full_order = ``[
435435
(* Testing scripts *)
436436
(********************)
437437

438-
(* Cakeml sptrees *)
438+
(* Test CakeML + compiling the input with the ML script *)
439439

440-
val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
440+
val final_thm_res = fwd_proof_w_IOcakeLib.convert_arith_policy_to_interval_tables_cake_w_IO (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
441441

442442

443443

‎hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_11Script.sml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -474,9 +474,9 @@ val policy_full_order = ``[
474474
(* Testing scripts *)
475475
(********************)
476476

477-
(* Cakeml sptrees *)
477+
(* Test CakeML + compiling the input with the ML script *)
478478

479-
val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
479+
val final_thm_res = fwd_proof_w_IOcakeLib.convert_arith_policy_to_interval_tables_cake_w_IO (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
480480

481481

482482

‎hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_12Script.sml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -498,9 +498,9 @@ val policy_full_order = ``[
498498
(* Testing scripts *)
499499
(********************)
500500

501-
(* Cakeml sptrees *)
501+
(* Test CakeML + compiling the input with the ML script *)
502502

503-
val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
503+
val final_thm_res = fwd_proof_w_IOcakeLib.convert_arith_policy_to_interval_tables_cake_w_IO (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
504504

505505

506506
val _ = export_theory ();

‎hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_13Script.sml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -528,9 +528,9 @@ val policy_full_order = ``[
528528
(* Testing scripts *)
529529
(********************)
530530

531-
(* Cakeml sptrees *)
531+
(* Test CakeML + compiling the input with the ML script *)
532532

533-
val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
533+
val final_thm_res = fwd_proof_w_IOcakeLib.convert_arith_policy_to_interval_tables_cake_w_IO (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
534534

535535

536536

‎hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_14Script.sml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -556,9 +556,9 @@ val policy_full_order = ``[
556556
(* Testing scripts *)
557557
(********************)
558558

559-
(* Cakeml sptrees *)
559+
(* Test CakeML + compiling the input with the ML script *)
560560

561-
val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
561+
val final_thm_res = fwd_proof_w_IOcakeLib.convert_arith_policy_to_interval_tables_cake_w_IO (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
562562

563563

564564

‎hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_15Script.sml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -584,9 +584,9 @@ val policy_full_order = ``[
584584
(* Testing scripts *)
585585
(********************)
586586

587-
(* Cakeml sptrees *)
587+
(* Test CakeML + compiling the input with the ML script *)
588588

589-
val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
589+
val final_thm_res = fwd_proof_w_IOcakeLib.convert_arith_policy_to_interval_tables_cake_w_IO (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
590590

591591

592592

‎hol/policy_to_table/bdd_cake_trans/internet_firewall_policies/internet_firewall_16Script.sml‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -607,14 +607,13 @@ val policy_full_order = ``[
607607

608608
(***********************************************)
609609

610-
611610
(********************)
612611
(* Testing scripts *)
613612
(********************)
614613

615-
(* Cakeml sptrees *)
614+
(* Test CakeML + compiling the input with the ML script *)
616615

617-
val final_thm_res = fwd_proof_cakeLib.convert_arith_policy_to_interval_tables_cake (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
616+
val final_thm_res = fwd_proof_w_IOcakeLib.convert_arith_policy_to_interval_tables_cake_w_IO (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
618617

619618

620619

0 commit comments

Comments
 (0)