6 "-----------------------------------------------------------------------------"; |
6 "-----------------------------------------------------------------------------"; |
7 "-----------------------------------------------------------------------------"; |
7 "-----------------------------------------------------------------------------"; |
8 "table of contents -----------------------------------------------------------"; |
8 "table of contents -----------------------------------------------------------"; |
9 "-----------------------------------------------------------------------------"; |
9 "-----------------------------------------------------------------------------"; |
10 "-------- fun check_kestore_rls ----------------------------------------------"; |
10 "-------- fun check_kestore_rls ----------------------------------------------"; |
11 "-------- fun KEStore_Elems.add_rlss overwrites earlier data -----------------"; |
11 "-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data ------------"; |
12 "-----------------------------------------------------------------------------"; |
12 "-----------------------------------------------------------------------------"; |
13 "-----------------------------------------------------------------------------"; |
13 "-----------------------------------------------------------------------------"; |
14 |
14 |
15 "-------- fun check_kestore_rls ----------------------------------------------"; |
15 "-------- fun check_kestore_rls ----------------------------------------------"; |
16 "-------- fun check_kestore_rls ----------------------------------------------"; |
16 "-------- fun check_kestore_rls ----------------------------------------------"; |
17 "-------- fun check_kestore_rls ----------------------------------------------"; |
17 "-------- fun check_kestore_rls ----------------------------------------------"; |
18 if check_kestore_rls ("e_rls", ("KEStore", e_rls)) = |
18 if check_kestore_rls ("e_rls", ("KEStore", e_rls)) = |
19 "(e_rls, (KEStore, Rls {#calc = 0, #rules = 0, ...))" |
19 "(e_rls, (KEStore, Rls {#calc = 0, #rules = 0, ...))" |
20 then () else error "check_kestore_rls changed" |
20 then () else error "check_kestore_rls changed" |
21 ; |
21 ; |
22 KEStore_Elems.get_rlss @{theory Isac} |
22 Test_KEStore_Elems.get_rlss @{theory Isac} |
23 |> map check_kestore_rls |
23 |> map check_kestore_rls |
24 |> enumerate_strings |
24 |> enumerate_strings |
25 |> sort string_ord |
25 |> sort string_ord |
26 (*|> map writeln*) |
26 (*|> map writeln*) |
27 ; |
27 ; |
28 |
28 |
29 "-------- fun KEStore_Elems.add_rlss overwrites earlier data -----------------"; |
29 "-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------"; |
30 "-------- fun KEStore_Elems.add_rlss overwrites earlier data -----------------"; |
30 "-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------"; |
31 "-------- fun KEStore_Elems.add_rlss overwrites earlier data -----------------"; |
31 "-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------"; |
32 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1; |
32 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1; |
33 fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*) |
33 fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*) |
34 |
34 |
35 val data1 = [("test", ("theory-1", Erls)), |
35 val data1 = [("test", ("theory-1", Erls)), |
36 ("test_rls", ("theory-1", |
36 ("test_rls", ("theory-1", |