Skip to content

Commit 3f013f6

Browse files
AnoudAlshnakatAnoudAlshnakat
committed
typo in the function application of cakeml test cases
1 parent c6d9198 commit 3f013f6

11 files changed

+44
-123
lines changed

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

Lines changed: 4 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -428,23 +428,17 @@ val policy_full_order = ``[
428428
]``;
429429

430430

431-
(********************************)
431+
432+
(***********************************************)
432433

433434

434435
(********************)
435436
(* Testing scripts *)
436437
(********************)
437438

438-
(* old BDD alists + EVAL *)
439-
440-
(*
441-
val final_thm_res =
442-
fwd_proofLib.convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
443-
*)
444-
445-
(* new BDD sptrees + EVAL *)
439+
(* Cakeml sptrees *)
446440
(*
447-
val final_thm_res = sptrees_fwd_proof_evalLib.eval_sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
441+
val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
448442
*)
449443

450444

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

Lines changed: 4 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -466,23 +466,17 @@ val policy_full_order = ``[
466466
("77nf" ,["is_dstNAT_le_80";"is_dstNAT_ge_80"])
467467
]``;
468468

469-
(********************************)
469+
470+
(***********************************************)
470471

471472

472473
(********************)
473474
(* Testing scripts *)
474475
(********************)
475476

476-
(* old BDD alists + EVAL *)
477-
478-
(*
479-
val final_thm_res =
480-
fwd_proofLib.convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
481-
*)
482-
483-
(* new BDD sptrees + EVAL *)
477+
(* Cakeml sptrees *)
484478
(*
485-
val final_thm_res = sptrees_fwd_proof_evalLib.eval_sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
479+
val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
486480
*)
487481

488482

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

Lines changed: 4 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -89,16 +89,9 @@ val policy_order = “["is_srcPort_le_57222"; "is_srcPort_ge_57222"; "is_dstPort
8989
(* Testing scripts *)
9090
(********************)
9191

92-
(* old BDD alists + EVAL *)
93-
94-
95-
val final_thm_res =
96-
fwd_proofLib.convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
97-
98-
99-
(* new BDD sptrees + EVAL *)
100-
(*
101-
val final_thm_res = sptrees_fwd_proof_evalLib.eval_sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
102-
*)
92+
(* Cakeml sptrees *)
93+
(*
94+
val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
95+
*)
10396

10497
val _ = export_theory ();

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

Lines changed: 4 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -172,17 +172,10 @@ val policy_full_order = ``[
172172
(* Testing scripts *)
173173
(********************)
174174

175-
(* old BDD alists + EVAL *)
176-
177-
178-
val final_thm_res =
179-
fwd_proofLib.convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
180-
181-
182-
(* new BDD sptrees + EVAL *)
183-
(*
184-
val final_thm_res = sptrees_fwd_proof_evalLib.eval_sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
185-
*)
175+
(* Cakeml sptrees *)
176+
(*
177+
val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
178+
*)
186179

187180

188181
val _ = export_theory ();

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

Lines changed: 4 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -216,17 +216,10 @@ val policy_full_order = ``[
216216
(* Testing scripts *)
217217
(********************)
218218

219-
(* old BDD alists + EVAL *)
220-
221-
222-
val final_thm_res =
223-
fwd_proofLib.convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
224-
225-
226-
(* new BDD sptrees + EVAL *)
227-
(*
228-
val final_thm_res = sptrees_fwd_proof_evalLib.eval_sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
229-
*)
219+
(* Cakeml sptrees *)
220+
(*
221+
val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
222+
*)
230223

231224

232225
val _ = export_theory ();

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

Lines changed: 4 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -248,17 +248,10 @@ val policy_full_order = ``[
248248
(* Testing scripts *)
249249
(********************)
250250

251-
(* old BDD alists + EVAL *)
252-
253-
254-
val final_thm_res =
255-
fwd_proofLib.convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
256-
257-
258-
(* new BDD sptrees + EVAL *)
259-
(*
260-
val final_thm_res = sptrees_fwd_proof_evalLib.eval_sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
261-
*)
251+
(* Cakeml sptrees *)
252+
(*
253+
val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
254+
*)
262255

263256

264257
val _ = export_theory ();

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

Lines changed: 4 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -288,16 +288,9 @@ val policy_full_order = ``[
288288
(* Testing scripts *)
289289
(********************)
290290

291-
(* old BDD alists + EVAL *)
292-
293-
294-
val final_thm_res =
295-
fwd_proofLib.convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
296-
297-
298-
(* new BDD sptrees + EVAL *)
299-
(*
300-
val final_thm_res = sptrees_fwd_proof_evalLib.eval_sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
301-
*)
291+
(* Cakeml sptrees *)
292+
(*
293+
val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
294+
*)
302295

303296
val _ = export_theory ();

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

Lines changed: 4 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -309,31 +309,17 @@ val policy_full_order = ``[
309309

310310

311311

312-
313312
(***********************************************)
314313

315314

316315
(********************)
317316
(* Testing scripts *)
318317
(********************)
319318

320-
(* old BDD alists + EVAL *)
321-
322-
(********************)
323-
(* Testing scripts *)
324-
(********************)
325-
326-
(* old BDD alists + EVAL *)
327-
328-
329-
val final_thm_res =
330-
fwd_proofLib.convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
331-
332-
333-
(* new BDD sptrees + EVAL *)
334-
(*
335-
val final_thm_res = sptrees_fwd_proof_evalLib.eval_sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
336-
*)
319+
(* Cakeml sptrees *)
320+
(*
321+
val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
322+
*)
337323

338324

339325
val _ = export_theory ();

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

Lines changed: 4 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -329,23 +329,17 @@ val policy_full_order = ``[
329329
]``;
330330

331331

332-
(********************************)
332+
333+
(***********************************************)
333334

334335

335336
(********************)
336337
(* Testing scripts *)
337338
(********************)
338339

339-
(* old BDD alists + EVAL *)
340-
341-
(*
342-
val final_thm_res =
343-
fwd_proofLib.convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
344-
*)
345-
346-
(* new BDD sptrees + EVAL *)
340+
(* Cakeml sptrees *)
347341
(*
348-
val final_thm_res = sptrees_fwd_proof_evalLib.eval_sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
342+
val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
349343
*)
350344

351345
val _ = export_theory ();

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

Lines changed: 4 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -356,23 +356,17 @@ val policy_full_order = ``[
356356
("58k" ,["is_srcNAT_le_21285";"is_srcNAT_ge_21285"])
357357
]``;
358358

359-
(********************************)
359+
360+
(***********************************************)
360361

361362

362363
(********************)
363364
(* Testing scripts *)
364365
(********************)
365366

366-
(* old BDD alists + EVAL *)
367-
368-
(*
369-
val final_thm_res =
370-
fwd_proofLib.convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
371-
*)
372-
373-
(* new BDD sptrees + EVAL *)
367+
(* Cakeml sptrees *)
374368
(*
375-
val final_thm_res = sptrees_fwd_proof_evalLib.eval_sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
369+
val final_thm_res = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
376370
*)
377371

378372

0 commit comments

Comments
 (0)