1 (* Title: src/Tools/isac/KEStore.thy
2 Author: Mathias Lehnfeld
5 theory KEStore imports Complex_Main
11 ML_file "rule-set.sml"
17 section \<open>Knowledge elements for problems and methods\<close>
19 (* Knowledge (and Exercises) are held by "KEStore" in Isac's Java front-end.
20 In the front-end Knowledge comprises theories, problems and methods.
21 Elements of problems and methods are defined in theories alongside
22 the development of respective language elements.
23 However, the structure of methods and problems is independent from theories'
24 deductive structure. Thus respective structures are built in Build_Thydata.thy.
26 Most elements of problems and methods are implemented in "Knowledge/", but some
27 of them are implemented in "ProgLang/" already; thus "KEStore.thy" got this
28 location in the directory structure.
30 get_* retrieves all * of the respective theory PLUS of all ancestor theories.
32 signature KESTORE_ELEMS =
34 val get_rlss: theory -> (Rule_Set.rls' * (Rule.theory' * Rule_Set.T)) list
35 val add_rlss: (Rule_Set.rls' * (Rule.theory' * Rule_Set.T)) list -> theory -> theory
36 val get_calcs: theory -> (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list
37 val add_calcs: (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list -> theory -> theory
38 val get_cas: theory -> Celem.cas_elem list
39 val add_cas: Celem.cas_elem list -> theory -> theory
40 val get_ptyps: theory -> Celem.ptyps
41 val add_pbts: (Celem.pbt * Celem.pblID) list -> theory -> theory
42 val get_mets: theory -> Celem.mets
43 val add_mets: (Celem.met * Celem.metID) list -> theory -> theory
44 val get_thes: theory -> (Celem.thydata Celem.ptyp) list
45 val add_thes: (Celem.thydata * Celem.theID) list -> theory -> theory (* thydata dropped at existing elems *)
46 val insert_fillpats: (Celem.theID * Celem.fillpat list) list -> theory -> theory
47 val get_ref_thy: unit -> theory
48 val set_ref_thy: theory -> unit
51 structure KEStore_Elems: KESTORE_ELEMS =
53 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
55 structure Data = Theory_Data (
56 type T = (Rule_Set.rls' * (Rule.theory' * Rule_Set.T)) list;
59 val merge = Rule_Set.merge_rlss;
61 fun get_rlss thy = Data.get thy
62 fun add_rlss rlss = Data.map (union_overwrite Rule_Set.rls_eq rlss)
64 structure Data = Theory_Data (
65 type T = (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list;
68 val merge = merge Rule_Set.calc_eq;
70 fun get_calcs thy = Data.get thy
71 fun add_calcs calcs = Data.map (union_overwrite Rule_Set.calc_eq calcs)
73 structure Data = Theory_Data (
74 type T = (term * (Celem.spec * (term list -> (term * term list) list))) list;
77 val merge = merge Celem.cas_eq;
79 fun get_cas thy = Data.get thy
80 fun add_cas cas = Data.map (union_overwrite Celem.cas_eq cas)
82 structure Data = Theory_Data (
84 val empty = [Celem.e_Ptyp];
86 val merge = Celem.merge_ptyps;
88 fun get_ptyps thy = Data.get thy;
89 fun add_pbts pbts thy = let
90 fun add_pbt (pbt as {guh,...}, pblID) =
91 (* the pblID has the leaf-element as first; better readability achieved *)
92 (if (!Celem.check_guhs_unique) then Celem.check_pblguh_unique guh (Data.get thy) else ();
93 rev pblID |> Celem.insrt pblID pbt);
94 in Data.map (fold add_pbt pbts) thy end;
96 structure Data = Theory_Data (
98 val empty = [Celem.e_Mets];
100 val merge = Celem.merge_ptyps;
102 val get_mets = Data.get;
103 fun add_mets mets thy = let
104 fun add_met (met as {guh,...}, metID) =
105 (if (!Celem.check_guhs_unique) then Celem.check_metguh_unique guh (Data.get thy) else ();
106 Celem.insrt metID met metID);
107 in Data.map (fold add_met mets) thy end;
109 structure Data = Theory_Data (
110 type T = (Celem.thydata Celem.ptyp) list;
113 val merge = Celem.merge_ptyps; (* relevant for store_thm, store_rls *)
115 fun get_thes thy = Data.get thy
116 fun add_thes thes thy = let
117 fun add_the (thydata, theID) = Celem.add_thydata ([], theID) thydata
118 in Data.map (fold add_the thes) thy end;
119 fun insert_fillpats fis thy =
121 fun update_elem (theID, fillpats) =
123 val hthm = Celem.get_py (Data.get thy) theID theID
124 val hthm' = Celem.update_hthm hthm fillpats
126 error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
127 in Celem.update_ptyps theID theID hthm' end
128 in Data.map (fold update_elem fis) thy end
130 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
131 fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)
132 fun get_ref_thy () = Synchronized.value cur_thy;
136 section \<open>Re-use existing access functions for knowledge elements\<close>
138 The independence of problems' and methods' structure enforces the accesse
139 functions to use "Isac_Knowledge", the final theory which comprises all knowledge defined.
142 val get_ref_thy = KEStore_Elems.get_ref_thy;
144 fun assoc_rls (rls' : Rule_Set.rls') =
145 case AList.lookup (op =) (KEStore_Elems.get_rlss (Rule.Thy_Info_get_theory "Isac_Knowledge")) rls' of
147 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
148 "TODO exception hierarchy needs to be established.")
150 fun assoc_rls' thy (rls' : Rule_Set.rls') =
151 case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
153 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
154 "TODO exception hierarchy needs to be established.")
156 fun assoc_calc thy calID = let
158 error ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
159 | ass ((calc, (keyi, _)) :: pairs, key) =
160 if key = keyi then calc else ass (pairs, key);
161 in ass (thy |> KEStore_Elems.get_calcs, calID) end;
163 fun assoc_calc' thy key = let
165 error ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
166 | ass ((all as (keyi, _)) :: pairs, key') =
167 if key' = keyi then all else ass (pairs, key');
168 in ass (KEStore_Elems.get_calcs thy, key) end;
170 fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
172 fun get_ptyps () = get_ref_thy () |> KEStore_Elems.get_ptyps;
173 fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
174 fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
176 setup \<open>KEStore_Elems.add_rlss
177 [("e_rls", (Context.theory_name @{theory}, Rule_Set.e_rls)),
178 ("e_rrls", (Context.theory_name @{theory}, Rule_Set.e_rrls))]\<close>
180 section \<open>determine sequence of main parts in thehier\<close>
182 KEStore_Elems.add_thes
183 [(Celem.Html {guh = Celem.part2guh ["IsacKnowledge"], html = "",
184 mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
185 (Celem.Html {guh = Celem.part2guh ["Isabelle"], html = "",
186 mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
187 (Celem.Html {guh = Celem.part2guh ["IsacScripts"], html = "",
188 mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
191 section \<open>Functions for checking KEStore_Elems\<close>
193 fun short_string_of_rls Rule_Set.Empty = "Erls"
194 | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
195 "Rls {#calc = " ^ string_of_int (length calc) ^
196 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
197 | short_string_of_rls (Rule_Set.Seqence {calc, rules, ...}) =
198 "Seq {#calc = " ^ string_of_int (length calc) ^
199 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
200 | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
201 fun check_kestore_rls (rls', (thyID, rls)) =
202 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
204 fun check_kestore_calc ((id, (c, _)) : Rule_Set.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
206 (* we avoid term_to_string''' defined later *)
207 fun check_kestore_cas ((t, (s, _)) : Celem.cas_elem) =
208 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
209 (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem.spec2str s ^ ")";
211 fun count_kestore_ptyps [] = 0
212 | count_kestore_ptyps ((Celem.Ptyp (_, _, ps)) :: ps') =
213 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
214 fun check_kestore_ptyp' strfun (Celem.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
215 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> Celem.linefeed;
216 val check_kestore_ptyp = check_kestore_ptyp' Celem.pbts2str;
217 fun ptyp_ord ((Celem.Ptyp (s1, _, _)), (Celem.Ptyp (s2, _, _))) = string_ord (s1, s2);
218 fun pbt_ord ({guh = guh'1, ...} : Celem.pbt, {guh = guh'2, ...} : Celem.pbt) = string_ord (guh'1, guh'2);
219 fun sort_kestore_ptyp' _ [] = []
220 | sort_kestore_ptyp' ordfun ((Celem.Ptyp (key, pbts, ps)) :: ps') =
221 ((Celem.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
222 :: sort_kestore_ptyp' ordfun ps');
223 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
225 fun metguh2str ({guh,...} : Celem.met) = guh : string;
226 fun check_kestore_met (mp: Celem.met Celem.ptyp) =
227 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
228 fun met_ord ({guh = guh'1, ...} : Celem.met, {guh = guh'2, ...} : Celem.met) = string_ord (guh'1, guh'2);
229 val sort_kestore_met = sort_kestore_ptyp' met_ord;
231 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem.thes2str))) thes
232 fun write_thes thydata_list =
234 |> map (fn (id, the) => (Celem.theID2str id, Celem.the2str the))