|
neuper@52126
|
1 |
(* Title: tests for KEStore.thy
|
|
neuper@52126
|
2 |
Author: Walther Neuper
|
|
neuper@52126
|
3 |
Use is subject to license terms.
|
|
neuper@52126
|
4 |
*)
|
|
neuper@52126
|
5 |
|
|
neuper@52126
|
6 |
"-----------------------------------------------------------------------------";
|
|
neuper@52126
|
7 |
"-----------------------------------------------------------------------------";
|
|
neuper@52126
|
8 |
"table of contents -----------------------------------------------------------";
|
|
neuper@52126
|
9 |
"-----------------------------------------------------------------------------";
|
|
neuper@52126
|
10 |
"-------- fun check_kestore_rls ----------------------------------------------";
|
|
s1210629013@55359
|
11 |
"-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data ------------";
|
|
neuper@52126
|
12 |
"-----------------------------------------------------------------------------";
|
|
neuper@52126
|
13 |
"-----------------------------------------------------------------------------";
|
|
neuper@52126
|
14 |
|
|
neuper@52126
|
15 |
"-------- fun check_kestore_rls ----------------------------------------------";
|
|
neuper@52126
|
16 |
"-------- fun check_kestore_rls ----------------------------------------------";
|
|
neuper@52126
|
17 |
"-------- fun check_kestore_rls ----------------------------------------------";
|
|
neuper@52126
|
18 |
if check_kestore_rls ("e_rls", ("KEStore", e_rls)) =
|
|
neuper@52126
|
19 |
"(e_rls, (KEStore, Rls {#calc = 0, #rules = 0, ...))"
|
|
neuper@52126
|
20 |
then () else error "check_kestore_rls changed"
|
|
neuper@52126
|
21 |
;
|
|
s1210629013@55359
|
22 |
Test_KEStore_Elems.get_rlss @{theory Isac}
|
|
neuper@52126
|
23 |
|> map check_kestore_rls
|
|
neuper@52126
|
24 |
|> enumerate_strings
|
|
neuper@52126
|
25 |
|> sort string_ord
|
|
neuper@52126
|
26 |
(*|> map writeln*)
|
|
neuper@52126
|
27 |
;
|
|
neuper@52139
|
28 |
|
|
s1210629013@55359
|
29 |
"-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";
|
|
s1210629013@55359
|
30 |
"-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";
|
|
s1210629013@55359
|
31 |
"-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";
|
|
neuper@52139
|
32 |
fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
|
|
neuper@52139
|
33 |
fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*)
|
|
neuper@52139
|
34 |
|
|
neuper@52139
|
35 |
val data1 = [("test", ("theory-1", Erls)),
|
|
neuper@52139
|
36 |
("test_rls", ("theory-1",
|
|
neuper@52139
|
37 |
append_rls "test_rls" e_rls [Thm ("refl", @{thm refl}), Thm ("subst", @{thm subst})]))]
|
|
neuper@52139
|
38 |
val data2 =
|
|
neuper@52139
|
39 |
[("test_rls", ("theory-2",
|
|
neuper@52139
|
40 |
append_rls "test_rls" e_rls [Thm ("not_def", @{thm not_def})]))]
|
|
neuper@52139
|
41 |
val data_3a = union rls_eq data1 data2
|
|
neuper@52139
|
42 |
val data_3b = union_overwrite rls_eq data1 data2
|
|
neuper@52139
|
43 |
|
|
neuper@52139
|
44 |
val SOME (_, Rls {rules, ...}) = AList.lookup op = data_3a "test_rls";
|
|
neuper@52139
|
45 |
case rules of
|
|
neuper@52139
|
46 |
[Thm ("not_def", _)] => ()
|
|
neuper@52139
|
47 |
| _ => error "union rls_eq changed: 1st argument is NOT overwritten anymore"
|
|
neuper@52139
|
48 |
;
|
|
neuper@52139
|
49 |
val SOME (_, Rls {rules, ...}) = AList.lookup op = data_3b "test_rls";
|
|
neuper@52139
|
50 |
case rules of
|
|
neuper@52139
|
51 |
[Thm ("refl", _), Thm ("subst", _)] => ()
|
|
neuper@52139
|
52 |
| _ => error "union_overwrite rls_eq changed: 2nd argument is NOT overwritten anymore"
|
|
neuper@52139
|
53 |
|
|
neuper@52139
|
54 |
(* add_rlss will take union_overwrite due to argument sequence *)
|
|
neuper@52139
|
55 |
|