1 (* Title: src/Tools/isac/KEStore.thy
2 Author: Mathias Lehnfeld
6 imports "~~/src/HOL/Complex_Main"
8 ML_file "~~/src/Tools/isac/library.sml"
9 ML_file "~~/src/Tools/isac/calcelems.sml"
11 section {* Knowledge elements for problems and methods *}
13 (* Knowledge (and Exercises) are held by "KEStore" in Isac's Java front-end.
14 In the front-end Knowledge comprises theories, problems and methods.
15 Elements of problems and methods are defined in theories alongside
16 the development of respective language elements.
17 However, the structure of methods and problems is independent from theories'
18 deductive structure. Thus respective structures are built in Build_Thydata.thy.
20 Most elements of problems and methods are implemented in "Knowledge/", but some
21 of them are implemented in "ProgLang/" already; thus "KEStore.thy" got this
22 location in the directory structure.
24 signature KESTORE_ELEMS =
26 val get_rlss: theory -> (Celem.rls' * (Celem.theory' * Celem.rls)) list
27 val add_rlss: (Celem.rls' * (Celem.theory' * Celem.rls)) list -> theory -> theory
28 val get_calcs: theory -> (Celem.prog_calcID * (Celem.calID * Celem.eval_fn)) list
29 val add_calcs: (Celem.prog_calcID * (Celem.calID * Celem.eval_fn)) list -> theory -> theory
30 val get_cas: theory -> Celem.cas_elem list
31 val add_cas: Celem.cas_elem list -> theory -> theory
32 val get_ptyps: theory -> Celem.ptyps
33 val add_pbts: (Celem.pbt * Celem.pblID) list -> theory -> theory
34 val get_mets: theory -> Celem.mets
35 val add_mets: (Celem.met * Celem.metID) list -> theory -> theory
36 val get_thes: theory -> (Celem.thydata Celem.ptyp) list
37 val add_thes: (Celem.thydata * Celem.theID) list -> theory -> theory (* thydata dropped at existing elems *)
38 val insert_fillpats: (Celem.theID * Celem.fillpat list) list -> theory -> theory
39 val get_ref_thy: unit -> theory
40 val set_ref_thy: theory -> unit
43 structure KEStore_Elems: KESTORE_ELEMS =
45 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
47 structure Data = Theory_Data (
48 type T = (Celem.rls' * (Celem.theory' * Celem.rls)) list;
51 val merge = Celem.merge_rlss;
53 fun get_rlss thy = Data.get thy
54 fun add_rlss rlss = Data.map (union_overwrite Celem.rls_eq rlss)
56 structure Data = Theory_Data (
57 type T = (Celem.prog_calcID * (Celem.calID * Celem.eval_fn)) list;
60 val merge = merge Celem.calc_eq;
62 fun get_calcs thy = Data.get thy
63 fun add_calcs calcs = Data.map (union_overwrite Celem.calc_eq calcs)
65 structure Data = Theory_Data (
66 type T = (term * (Celem.spec * (term list -> (term * term list) list))) list;
69 val merge = merge Celem.cas_eq;
71 fun get_cas thy = Data.get thy
72 fun add_cas cas = Data.map (union_overwrite Celem.cas_eq cas)
74 structure Data = Theory_Data (
76 val empty = [Celem.e_Ptyp];
78 val merge = Celem.merge_ptyps;
80 fun get_ptyps thy = Data.get thy;
81 fun add_pbts pbts thy = let
82 fun add_pbt (pbt as {guh,...}, pblID) =
83 (* the pblID has the leaf-element as first; better readability achieved *)
84 (if (!Celem.check_guhs_unique) then Celem.check_pblguh_unique guh (Data.get thy) else ();
85 rev pblID |> Celem.insrt pblID pbt);
86 in Data.map (fold add_pbt pbts) thy end;
88 structure Data = Theory_Data (
90 val empty = [Celem.e_Mets];
92 val merge = Celem.merge_ptyps;
94 val get_mets = Data.get;
95 fun add_mets mets thy = let
96 fun add_met (met as {guh,...}, metID) =
97 (if (!Celem.check_guhs_unique) then Celem.check_metguh_unique guh (Data.get thy) else ();
98 Celem.insrt metID met metID);
99 in Data.map (fold add_met mets) thy end;
101 structure Data = Theory_Data (
102 type T = (Celem.thydata Celem.ptyp) list;
105 val merge = Celem.merge_ptyps; (* relevant for store_thm, store_rls *)
107 fun get_thes thy = Data.get thy
108 fun add_thes thes thy = let
109 fun add_the (thydata, theID) = Celem.add_thydata ([], theID) thydata
110 in Data.map (fold add_the thes) thy end;
111 fun insert_fillpats fis thy =
113 fun update_elem (theID, fillpats) =
115 val hthm = Celem.get_py (Data.get thy) theID theID
116 val hthm' = Celem.update_hthm hthm fillpats
118 error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
119 in Celem.update_ptyps theID theID hthm' end
120 in Data.map (fold update_elem fis) thy end
122 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
123 fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)
124 fun get_ref_thy () = Synchronized.value cur_thy;
128 section {* Re-use existing access functions for knowledge elements *}
130 The independence of problems' and methods' structure enforces the accesse
131 functions to use "Isac", the final theory which comprises all knowledge defined.
134 val get_ref_thy = KEStore_Elems.get_ref_thy;
136 fun assoc_rls (rls' : Celem.rls') =
137 case AList.lookup (op =) (KEStore_Elems.get_rlss (Celem.Thy_Info_get_theory "Isac")) rls' of
139 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
140 "TODO exception hierarchy needs to be established.")
142 fun assoc_rls' thy (rls' : Celem.rls') =
143 case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
145 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
146 "TODO exception hierarchy needs to be established.")
148 fun assoc_calc thy calID = let
150 error ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
151 | ass ((calc, (keyi, _)) :: pairs, key) =
152 if key = keyi then calc else ass (pairs, key);
153 in ass (thy |> KEStore_Elems.get_calcs, calID) end;
155 fun assoc_calc' thy key = let
157 error ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
158 | ass ((all as (keyi, _)) :: pairs, key') =
159 if key' = keyi then all else ass (pairs, key');
160 in ass (KEStore_Elems.get_calcs thy, key) end;
162 fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
164 fun get_ptyps () = get_ref_thy () |> KEStore_Elems.get_ptyps;
165 fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
166 fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
168 setup {* KEStore_Elems.add_rlss
169 [("e_rls", (Context.theory_name @{theory}, Celem.e_rls)),
170 ("e_rrls", (Context.theory_name @{theory}, Celem.e_rrls))] *}
172 section {* determine sequence of main parts in thehier *}
174 KEStore_Elems.add_thes
175 [(Celem.Html {guh = Celem.part2guh ["IsacKnowledge"], html = "",
176 mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
177 (Celem.Html {guh = Celem.part2guh ["Isabelle"], html = "",
178 mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
179 (Celem.Html {guh = Celem.part2guh ["IsacScripts"], html = "",
180 mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
183 section {* Functions for checking KEStore_Elems *}
185 fun short_string_of_rls Celem.Erls = "Erls"
186 | short_string_of_rls (Celem.Rls {calc, rules, ...}) =
187 "Rls {#calc = " ^ string_of_int (length calc) ^
188 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
189 | short_string_of_rls (Celem.Seq {calc, rules, ...}) =
190 "Seq {#calc = " ^ string_of_int (length calc) ^
191 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
192 | short_string_of_rls (Celem.Rrls _) = "Rrls {...}";
193 fun check_kestore_rls (rls', (thyID, rls)) =
194 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
196 fun check_kestore_calc ((id, (c, _)) : Celem.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
198 fun check_kestore_cas ((t, (s, _)) : Celem.cas_elem) =
199 "(" ^ (Celem.term_to_string''' @{theory} t) ^ ", " ^ (Celem.spec2str s) ^ ")";
201 fun count_kestore_ptyps [] = 0
202 | count_kestore_ptyps ((Celem.Ptyp (_, _, ps)) :: ps') =
203 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
204 fun check_kestore_ptyp' strfun (Celem.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
205 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> Celem.linefeed;
206 val check_kestore_ptyp = check_kestore_ptyp' Celem.pbts2str;
207 fun ptyp_ord ((Celem.Ptyp (s1, _, _)), (Celem.Ptyp (s2, _, _))) = string_ord (s1, s2);
208 fun pbt_ord ({guh = guh'1, ...} : Celem.pbt, {guh = guh'2, ...} : Celem.pbt) = string_ord (guh'1, guh'2);
209 fun sort_kestore_ptyp' _ [] = []
210 | sort_kestore_ptyp' ordfun ((Celem.Ptyp (key, pbts, ps)) :: ps') =
211 ((Celem.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
212 :: sort_kestore_ptyp' ordfun ps');
213 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
215 fun metguh2str ({guh,...} : Celem.met) = guh : string;
216 fun check_kestore_met (mp: Celem.met Celem.ptyp) =
217 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
218 fun met_ord ({guh = guh'1, ...} : Celem.met, {guh = guh'2, ...} : Celem.met) = string_ord (guh'1, guh'2);
219 val sort_kestore_met = sort_kestore_ptyp' met_ord;
221 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem.thes2str))) thes
222 fun write_thes thydata_list =
224 |> map (fn (id, the) => (Celem.theID2str id, Celem.the2str the))