4 ML_file "~~/src/Tools/isac/library.sml"
5 ML_file "~~/src/Tools/isac/calcelems.sml"
7 section {* Knowledge elements for problems and methods *}
9 (* Knowledge (and Exercises) are held by "KEStore" in Isac's Java front-end.
10 In the front-end Knowledge comprises theories, problems and methods.
11 Elements of problems and methods are defined in theories alongside
12 the development of respective language elements.
13 However, the structure of methods and problems is independent from theories'
14 deductive structure. Thus respective structures are built in Build_Thydata.thy.
16 Most elements of problems and methods are implemented in "Knowledge/", but some
17 of them are implemented in "ProgLang/" already; thus "KEStore.thy" got this
18 location in the directory structure.
20 signature KESTORE_ELEMS =
22 val get_rlss: theory -> (rls' * (theory' * rls)) list
23 val add_rlss: (rls' * (theory' * rls)) list -> theory -> theory
24 val get_calcs: theory -> (prog_calcID * (calID * eval_fn)) list
25 val add_calcs: (prog_calcID * (calID * eval_fn)) list -> theory -> theory
26 val get_cas: theory -> cas_elem list
27 val add_cas: cas_elem list -> theory -> theory
31 structure KEStore_Elems: KESTORE_ELEMS =
33 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
35 structure Data = Theory_Data (
36 type T = (rls' * (theory' * rls)) list;
39 val merge = merge_rlss;
41 fun get_rlss thy = Data.get thy
42 fun add_rlss rlss = Data.map (union_overwrite rls_eq rlss)
44 structure Data = Theory_Data (
45 type T = (prog_calcID * (calID * eval_fn)) list;
48 val merge = merge calc_eq;
50 fun get_calcs thy = Data.get thy
51 fun add_calcs calcs = Data.map (union_overwrite calc_eq calcs)
53 structure Data = Theory_Data (
54 type T = (term * (spec * (term list -> (term * term list) list))) list;
57 val merge = merge cas_eq;
59 fun get_cas thy = Data.get thy
60 fun add_cas cas = Data.map (union_overwrite cas_eq cas)
66 section {* Re-use existing access functions for knowledge elements *}
68 The independence of problems' and methods' structure enforces the accesse
69 functions to use "Isac", the final theory which comprises all knowledge defined.
72 (* in this phase of removing Unsynchornized.ref we do NOT overwrite the existing function! *)
73 fun assoc_rls (rls' : rls') = (*SWITCH outcommented*)
74 case AList.lookup (op =) (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) rls' of
76 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
77 "TODO exception hierarchy needs to be established.")
79 fun assoc_rls' thy (rls' : rls') = (*SWITCH outcommented*)
80 case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
82 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
83 "TODO exception hierarchy needs to be established.")
85 fun assoc_calc thy calID = let
87 error ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
88 | ass ((calc, (keyi, _)) :: pairs, key) =
89 if key = keyi then calc else ass (pairs, key);
90 in ass (thy |> KEStore_Elems.get_calcs, calID) end;
92 fun assoc_calc' thy key = let
94 error ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
95 | ass ((all as (keyi, _)) :: pairs, key') =
96 if key' = keyi then all else ass (pairs, key');
97 in ass (KEStore_Elems.get_calcs thy, key) end;
100 case AList.lookup (op =) (Thy_Info.get_theory "Isac" |> KEStore_Elems.get_rlss) cas' of
102 | NONE => raise ERROR ("cas \""^ cas' ^ "\" missing in KEStore.\n" ^
103 "TODO exception hierarchy needs to be established.")
105 setup {* KEStore_Elems.add_rlss
106 [("e_rls", (Context.theory_name @{theory}, e_rls)),
107 ("e_rrls", (Context.theory_name @{theory}, e_rrls))] *}
109 section {* Functions for checking KEStore_Elems *}
111 fun short_string_of_rls Erls = "Erls"
112 | short_string_of_rls (Rls {calc, rules, ...}) =
113 "Rls {#calc = " ^ string_of_int (length calc) ^
114 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
115 | short_string_of_rls (Seq {calc, rules, ...}) =
116 "Seq {#calc = " ^ string_of_int (length calc) ^
117 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
118 | short_string_of_rls (Rrls _) = "Rrls {...}";
120 fun check_kestore_rls (rls', (thyID, rls)) =
121 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
123 fun check_kestore_calc ((id, (c, _)) : calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
125 fun check_kestore_cas ((t, (s, _)):cas_elem) =
126 "(" ^ (term_to_string''' @{theory} t) ^ ", " ^ (spec2str s) ^ ")";