Skip to content

Commit eb7d336

Browse files
AnoudAlshnakatAnoudAlshnakat
committed
edited the terminal printing of cakeml bin
1 parent 7c2b0dd commit eb7d336

File tree

1 file changed

+101
-177
lines changed

1 file changed

+101
-177
lines changed

‎hol/policy_to_table/bdd_cake_trans/sptrees_bdd_trans_ProgScript.sml‎

Lines changed: 101 additions & 177 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ open fromSexpTheory;
77

88

99

10-
val _ = new_theory "bdd_trans_Prog";
10+
val _ = new_theory "sptrees_bdd_trans_Prog";
1111

1212

1313

@@ -86,13 +86,16 @@ val r = translate rich_listTheory.SEG;
8686
val r = translate pre_are_fail_def;
8787
val r = translate final_policy_def;
8888

89+
90+
8991
Theorem final_policy_cake_trans:
9092
final_policy_side v4
9193
Proof
94+
Induct_on ‘v4’ >>
9295
rw [fetch "-" "final_policy_side_def"] >>
9396
rw [fetch "-" "pre_are_fail_side_def"] >>
9497
rw [Once (fetch "-" "seg_side_def")] >>
95-
fs[min_idx_till_def] >> cheat
98+
fs[min_idx_till_def, INDEX_FIND_def] >> cheat
9699
QED
97100

98101

@@ -122,171 +125,8 @@ val r = translate sp_mk_BDD_policy_def;
122125

123126
(*****************************************************)
124127

125-
126-
val arith_policy_eval = EVAL “convert_arith_to_var_policy ^arith_policy ^policy_me”;
127-
val var_policy = optionSyntax.dest_some (rhs (concl arith_policy_eval));
128-
129-
130-
131-
132-
Definition policy_order_test_def:
133-
policy_order_test = ["x";"y";"z"]
134-
End
135-
136-
val r = translate policy_order_test_def;
137-
138-
Definition policy_content_test_def:
139-
policy_content_test = [
140-
(Var "x", action ("allow",[1]));
141-
(And (Var "y") (Var "z"), action ("allow",[2]));
142-
(True, action ("drop",[]))
143-
]:action_policy_type
144-
End
145-
146-
val r = translate policy_content_test_def;
147-
148-
149-
Definition main_hol4_def:
150-
main_hol4 =
151-
sp_mk_BDD_policy policy_content_test policy_order_test
152-
End
153-
154-
155-
val r = translate main_hol4_def;
156-
157-
val res = append_prog o process_topdecs $
158-
‘fun main () =
159-
let
160-
val args = CommandLine.arguments()
161-
in
162-
(case main_hol4 of
163-
None => TextIO.print "No BDD can be created \n"
164-
| Some bdd => TextIO.print "SOME \n")
165-
end ;’
166-
;
167-
168-
169-
val prog =
170-
``SNOC
171-
(Dlet unknown_loc (Pcon NONE [])
172-
(App Opapp [Var (Short "main"); Con NONE []]))
173-
^(get_ml_prog_state() |> get_prog)
174-
`` |> EVAL |> concl |> rhs
175-
176-
177-
178-
val _ = astToSexprLib.write_ast_to_file "test_bdd.sexp" prog;
179-
180-
181-
182-
183-
184-
185-
186-
187-
188-
189-
(************************)
190-
191-
val _ = astPP.enable_astPP ();
192-
val _ = (max_print_depth := 200);
193-
194-
195-
196-
val var_pred = “ Or (And (Var "x") (Not (Var "y"))) (And (Not (Var "a")) (Var "b")) ”;
197-
val var_pred2 = “ Or (And (Var "c") (Not (Var "d"))) (And (Not (Var "e")) (Var "f")) ”;
198-
val var_pred3 = “ Or ^var_pred ^var_pred2 ”;
199-
200-
201-
202-
EVAL “sp_mk_BDDPred_opt pred_structure (0n,LN,insert 0 (non_termn (NONE, ^var_pred)) LN) [] ["a";"b";"c"; "d"; "f"; "g"; "x"; "y"] 1”;
203-
204-
EVAL “sp_mk_BDDPred_opt pred_structure (0n,LN,insert 0 (non_termn (NONE, ^var_pred)) LN) [] ["a";"b";"c"; "d"; "x"; "y"; "f"; "e"] 1”;
205-
206-
val _ = type_abbrev("action_rule_type", “:((string# num list) action_expr) rule”);
207-
val _ = type_abbrev("action_policy_type", “:((string# num list) action_expr) policy”);
208-
209-
val rule1 = “(^var_pred3 , action ("allow",[1]: num list)):action_rule_type”;
210-
val rule2 = “((Var "k") , action ("allow",[2]: num list)):action_rule_type”;
211-
val rule3 = “((Var "o") , action ("allow",[3]: num list)):action_rule_type”;
212-
213-
val arith_policy_rule_default = “(True, action ("drop", []: num list)):action_rule_type”;
214-
215-
216-
val arith_policy = “[
217-
^rule1;
218-
^rule2;
219-
^arith_policy_rule_default
220-
]: action_policy_type”;
221-
222-
223-
224-
225-
Definition toAList_BDD_edges_def:
226-
toAList_BDD_edges (r,edges,labels) = toSortedAList edges
227-
End
228-
229-
Definition toAList_BDD_labels_def:
230-
toAList_BDD_labels (r,edges,labels) = toSortedAList labels
231-
End
232-
233-
Definition BDD_root_is_def:
234-
BDD_root_is (r,edges,labels) = r
235-
End
236-
237-
238-
val a = (optionSyntax.dest_some (rhs ( concl (EVAL “ (sp_mk_BDDPred_opt policy_structure (0n,LN,insert 0 (non_termn (NONE, ^arith_policy)) LN) []
239-
["o";"k";"x";"y";"a";"b";"c";"d"]
240-
1)”))));
241-
242-
243-
val edges_list = rhs ( concl (EVAL “ toAList_BDD_edges ^a ”));
244-
val labels_list = rhs ( concl (EVAL “ toAList_BDD_labels ^a ”));
245-
246-
247-
248-
249-
250-
251-
252-
253-
254-
Definition test_bdd_def:
255-
test_bdd = SOME ^edges_list
256-
End
257-
258-
259-
val r = translate test_bdd_def;
260-
261-
val _ = (max_print_depth := 200);
262-
263-
264-
265-
(************************************************)
266-
267-
open HolKernel Parse boolLib bossLib;
268-
open optionTheory bdd_sptrees_genTheory pairTheory bdd_genTheory policy_specTheory pred_specTheory;
269-
open preamble basis ml_translatorLib ;
270-
271-
open miscTheory ml_translatorTheory ListProgTheory ;
272-
open fromSexpTheory;
273-
274-
275-
val _ = translation_extends "basisProg"
276-
val _ = intLib.deprecate_int();
277-
278128

279129
(* print edges *)
280-
281-
(*
282-
283-
Definition test_list_edges_def:
284-
test_list_edges = SOME ([(1,2,3);(4,5,6)]:edges)
285-
End
286-
287-
val r = translate test_list_edges_def;
288-
*)
289-
290130

291131
val res = append_prog o process_topdecs $
292132
‘fun print_tuple_list xs =
@@ -311,17 +151,22 @@ val res = append_prog o process_topdecs $
311151
| [x] => print_elem x
312152
| x::rest =>
313153
(print_elem x;
314-
TextIO.print ", ";
154+
TextIO.print "; ";
315155
loop rest)
316156
in
317157
TextIO.print "[";
318158
loop xs;
319159
TextIO.print "]"
320160
end’;
321161

162+
163+
(*
322164
165+
Definition test_list_edges_def:
166+
test_list_edges = SOME ([(1,2,3);(4,5,6)]:edges)
167+
End
323168
324-
(*
169+
val r = translate test_list_edges_def;
325170
326171
val res = append_prog o process_topdecs $
327172
‘fun main () =
@@ -331,7 +176,7 @@ val res = append_prog o process_topdecs $
331176
(case test_list_edges of
332177
None => TextIO.print "No BDD can be created \n"
333178
| Some l => print_tuple_list l;
334-
TextIO.print "\n";
179+
TextIO.print "\n"
335180
)
336181
end ;’
337182
;
@@ -350,14 +195,6 @@ val _ = astToSexprLib.write_ast_to_file "test_bdd.sexp" prog;
350195
*)
351196

352197

353-
(*(((string#num list) action_expr) policy, (string#num list) action_expr) labelings)*)
354-
355-
(*
356-
val _ = astPP.enable_astPP ();
357-
val _ = (max_print_depth := 200);
358-
*)
359-
360-
361198

362199

363200
(* print labels *)
@@ -505,7 +342,7 @@ val res = append_prog o process_topdecs $
505342
TextIO.print (Int.toString (fst x));
506343
TextIO.print ", ";
507344
print_label (snd x);
508-
TextIO.print "); ";
345+
TextIO.print "); \n ";
509346
loop rest)
510347
in
511348
TextIO.print "[";
@@ -561,6 +398,93 @@ val _ = astToSexprLib.write_ast_to_file "test_bdd.sexp" prog;
561398

562399

563400

401+
val r = translate spts_to_alist_add_pause_def;
402+
val r = translate spt_left_def;
403+
val r = translate spt_right_def;
404+
val r = translate spt_center_def;
405+
406+
val r = translate spts_to_alist_aux_def;
407+
val r = translate spts_to_alist_def;
408+
val r = translate toSortedAList_def;
409+
410+
411+
(***************************************)
412+
413+
(* EXAMPLE OF USAGE *)
414+
415+
(*
416+
417+
Definition policy_order_test_def:
418+
policy_order_test = ["x";"y";"z"]
419+
End
420+
421+
val r = translate policy_order_test_def;
422+
423+
Definition policy_content_test_def:
424+
policy_content_test = [
425+
(Var "x", action ("allow",[1]));
426+
(And (Var "y") (Var "z"), action ("allow",[2]));
427+
(True, action ("drop",[]))
428+
]:action_policy_type
429+
End
430+
431+
val r = translate policy_content_test_def;
432+
433+
434+
Definition main_hol4_def:
435+
main_hol4 =
436+
case sp_mk_BDD_policy policy_content_test policy_order_test of
437+
| NONE => NONE
438+
| SOME (r,sp_edges,sp_labels) => SOME (r,
439+
((toSortedAList sp_edges):edges),
440+
((toSortedAList sp_labels): (((string#num list) action_expr) policy, (string#num list) action_expr) labelings) )
441+
End
442+
443+
444+
445+
446+
447+
val r = translate main_hol4_def;
448+
449+
450+
val res = append_prog o process_topdecs $
451+
‘fun main () =
452+
let
453+
val args = CommandLine.arguments()
454+
in
455+
(case main_hol4 of
456+
None => (TextIO.print "No BDD can be created \n")
457+
| Some bdd =>
458+
(
459+
TextIO.print "(" ;
460+
TextIO.print (Int.toString (fst bdd));
461+
(TextIO.print ", \n");
462+
print_tuple_list (fst (snd (bdd))) ;
463+
(TextIO.print ", \n");
464+
print_list_label (snd (snd (bdd))) ;
465+
TextIO.print ")"
466+
)
467+
468+
)
469+
end ;’
470+
;
471+
472+
473+
val prog =
474+
``SNOC
475+
(Dlet unknown_loc (Pcon NONE [])
476+
(App Opapp [Var (Short "main"); Con NONE []]))
477+
^(get_ml_prog_state() |> get_prog)
478+
`` |> EVAL |> concl |> rhs
479+
480+
481+
482+
val _ = astToSexprLib.write_ast_to_file "test_bdd.sexp" prog;
483+
484+
485+
486+
*)
487+
564488

565489

566490
val _ = export_theory ();

0 commit comments

Comments
 (0)