cleanup, naming: 'KEStore_Elems' in Tests now 'Test_KEStore_Elems', 'store_pbts' now 'add_pbts'
1 (* KEStore holds Knowledge and Exercises in Isac's Java front-end.
2 In the front-end knowledge comprises theories, problems and methods.
3 Elements of problems and methods are defined in theories alongside
4 the development of respective language elements.
5 The structure of methods and problems is independent from theories' deductive
6 structure. The respective structures are built in Build_Thydata.thy.
8 signature KESTORE_ELEMS =
10 val get_rlss: theory -> (rls' * (theory' * rls)) list
11 val add_rlss: (rls' * (theory' * rls)) list -> theory -> theory
12 val get_calcs: theory -> (prog_calcID * (calID * eval_fn)) list
13 val add_calcs: (prog_calcID * (calID * eval_fn)) list -> theory -> theory
17 structure Test_KEStore_Elems: KESTORE_ELEMS =
19 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
21 fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*)
22 structure Data = Theory_Data (
23 type T = (rls' * (theory' * rls)) list;
26 val merge = merge rls_eq;
28 fun get_rlss thy = Data.get thy
29 fun add_rlss rlss = Data.map (union_overwrite rls_eq rlss)
32 structure Data = Theory_Data (
33 type T = (prog_calcID * (calID * eval_fn)) list;
36 val merge = merge calc_eq;
38 fun get_calcs thy = Data.get thy
39 fun add_calcs calcs = Data.map (union_overwrite calc_eq calcs)