1 (* Title: src/Tools/isac/Know_Store.thy
2 Author: Mathias Lehnfeld
4 Calc work on Problem employing MethodC; both are collected in a respective Store;
5 The collections' structure is independent from the dependency graph of Isabelle's theories
7 Store is also used by Thy_Write, required for Isac's Java front end, irrelevant for PIDE.
9 The files (in "xxxxx-def.sml") contain definitions required for Know_Store;
10 they also include minimal code required for other "xxxxx-def.sml" files.
11 These files have companion files "xxxxx.sml" with all further code,
12 located at appropriate positions in the file structure.
14 The separation of "xxxxx-def.sml" from "xxxxx.sml" should be overcome by
15 appropriate use of polymorphic high order functions.
20 keywords "rule_set_knowledge" "calculation" :: thy_decl
24 ML_Antiquotation.conditional \<^binding>\<open>isac_test\<close>
25 (fn _ => Options.default_bool \<^system_option>\<open>isac_test\<close>)
31 ML_file "rule-def.sml"
32 ML_file "thmC-def.sml"
33 ML_file "eval-def.sml" (*rename identifiers by use of struct.id*)
34 ML_file "rewrite-order.sml" (*rename identifiers by use of struct.id*)
36 ML_file "error-pattern-def.sml"
37 ML_file "rule-set.sml"
40 ML_file "check-unique.sml"
41 ML_file "references-def.sml"
42 ML_file "model-pattern.sml"
43 ML_file "problem-def.sml"
44 ML_file "method-def.sml"
46 ML_file "formalise.sml"
48 ML_file "thy-write.sml"
54 section \<open>Knowledge elements for problems and methods\<close>
56 (* Knowledge (and Exercises) are held by "Know_Store" in Isac's Java front-end.
57 In the front-end Knowledge comprises theories, problems and methods.
58 Elements of problems and methods are defined in theories alongside
59 the development of respective language elements.
60 However, the structure of methods and problems is independent from theories'
61 deductive structure. Thus respective structures are built in Build_Thydata.thy.
63 Most elements of problems and methods are implemented in "Knowledge/", but some
64 of them are implemented in "ProgLang/" already; thus "Know_Store.thy" got this
65 location in the directory structure.
67 get_* retrieves all * of the respective theory PLUS of all ancestor theories.
69 signature KESTORE_ELEMS =
71 val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
72 val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
73 val get_calcs: theory -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list
74 val add_calcs: (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list -> theory -> theory
75 val get_cas: theory -> CAS_Def.T list
76 val add_cas: CAS_Def.T list -> theory -> theory
77 val get_pbls: theory -> Probl_Def.store
78 val add_pbls: Proof.context -> (Probl_Def.T * References_Def.id) list -> theory -> theory
79 val get_mets: theory -> Meth_Def.store
80 val add_mets: Proof.context -> (Meth_Def.T * References_Def.id) list -> theory -> theory
81 val get_expls: theory -> Example.store
82 val add_expls: (Example.T * Store.key) list -> theory -> theory
83 val get_thes: theory -> (Thy_Write.thydata Store.node) list
84 val add_thes: (Thy_Write.thydata * Thy_Write.theID) list -> theory -> theory (* thydata dropped at existing elems *)
85 val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory
86 val get_ref_thy: unit -> theory
87 val set_ref_thy: theory -> unit
90 structure KEStore_Elems: KESTORE_ELEMS =
92 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
94 structure Data = Theory_Data (
95 type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
98 val merge = Rule_Set.to_kestore;
100 fun get_rlss thy = Data.get thy
101 fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
103 structure Data = Theory_Data (
104 type T = (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list;
107 val merge = merge Eval_Def.calc_eq;
109 fun get_calcs thy = Data.get thy
110 fun add_calcs calcs = Data.map (union_overwrite Eval_Def.calc_eq calcs)
112 structure Data = Theory_Data (
113 type T = (term * (References_Def.T * (term list -> (term * term list) list))) list;
116 val merge = merge CAS_Def.equal;
118 fun get_cas thy = Data.get thy
119 fun add_cas cas = Data.map (union_overwrite CAS_Def.equal cas)
121 structure Data = Theory_Data (
122 type T = Probl_Def.store;
123 val empty = [Probl_Def.empty_store];
125 val merge = Store.merge;
127 fun get_pbls thy = Data.get thy;
128 fun add_pbls ctxt pbts thy =
130 fun add_pbt (pbt as {guh,...}, pblID) =
131 (* the pblID has the leaf-element as first; better readability achieved *)
132 (if (Config.get ctxt check_unique) then Probl_Def.check_unique guh (Data.get thy) else ();
133 rev pblID |> Store.insert pblID pbt);
134 in Data.map (fold add_pbt pbts) thy end;
136 structure Data = Theory_Data (
137 type T = Meth_Def.store;
138 val empty = [Meth_Def.empty_store];
140 val merge = Store.merge;
142 val get_mets = Data.get;
143 fun add_mets ctxt mets thy =
145 fun add_met (met as {guh,...}, metID) =
146 (if (Config.get ctxt check_unique) then Meth_Def.check_unique guh (Data.get thy) else ();
147 Store.insert metID met metID);
148 in Data.map (fold add_met mets) thy end;
150 structure Data = Theory_Data (
151 type T = Example.store;
152 val empty = [Example.empty_store];
154 val merge = Store.merge;
156 val get_expls = Data.get;
157 fun add_expls expls thy =
159 fun add_expl (expl, expl_id) = Store.insert expl_id expl expl_id;
160 in Data.map (fold add_expl expls) thy end;
162 structure Data = Theory_Data (
163 type T = (Thy_Write.thydata Store.node) list;
166 val merge = Store.merge; (* relevant for store_thm, store_rls *)
168 fun get_thes thy = Data.get thy
169 fun add_thes thes thy = let
170 fun add_the (thydata, theID) = Thy_Write.add_thydata ([], theID) thydata
171 in Data.map (fold add_the thes) thy end;
172 fun insert_fillpats fis thy =
174 fun update_elem (theID, fillpats) =
176 val hthm = Store.get (Data.get thy) theID theID
177 val hthm' = Thy_Write.update_hthm hthm fillpats
179 raise ERROR ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
180 in Store.update theID theID hthm' end
181 in Data.map (fold update_elem fis) thy end
183 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
184 fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)
185 fun get_ref_thy () = Synchronized.value cur_thy;
190 subsection \<open>Isar command syntax\<close>
195 val parse_rule = Parse.name -- Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source);
197 val ml = ML_Lex.read;
199 fun ml_rule thy (name, source) =
200 ml "(" @ ml (ML_Syntax.print_string name) @ ml ", " @
201 ml "(" @ ml (ML_Syntax.print_string (Context.theory_name thy)) @ ml ", " @
202 ML_Lex.read_source source @ ml "))";
204 fun ml_rules thy args =
205 ml "Theory.setup (KEStore_Elems.add_rlss [" @
206 flat (separate (ml ",") (map (ml_rule thy) args)) @ ml "])";
209 Outer_Syntax.command \<^command_keyword>\<open>rule_set_knowledge\<close> "register ISAC rule set to Knowledge Store"
210 (Parse.and_list1 parse_rule >> (fn args => Toplevel.theory (fn thy =>
211 thy |> Context.theory_map
212 (ML_Context.expression (Position.thread_data ()) (ml_rules thy args)))));
215 Parse.name -- (\<^keyword>\<open>(\<close> |-- Parse.const --| \<^keyword>\<open>)\<close>) ||
216 Scan.ahead Parse.name -- Parse.const;
219 Outer_Syntax.command \<^command_keyword>\<open>calculation\<close>
220 "prepare ISAC calculation and register it to Knowledge Store"
221 (calc_name -- (\<^keyword>\<open>=\<close> |-- Parse.!!! Parse.ML_source) >> (fn ((calcID, const), source) =>
222 Toplevel.theory (fn thy =>
224 val ctxt = Proof_Context.init_global thy;
225 val Const (c, _) = Proof_Context.read_const {proper = true, strict = true} ctxt const;
227 ML_Context.expression (Input.pos_of source)
228 (ml "Theory.setup (Eval_Def.set_data (" @ ML_Lex.read_source source @ ml "))")
229 |> Context.theory_map;
230 val eval = Eval_Def.the_data (set_data thy);
231 in KEStore_Elems.add_calcs [(calcID, (c, eval))] thy end)))
237 section \<open>Re-use existing access functions for knowledge elements\<close>
239 The independence of problems' and methods' structure enforces the accesse
240 functions to use "Isac_Knowledge", the final theory which comprises all knowledge defined.
243 val get_ref_thy = KEStore_Elems.get_ref_thy;
245 fun assoc_rls (rls' : Rule_Set.id) =
246 case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
248 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
249 "TODO exception hierarchy needs to be established.")
251 fun assoc_rls' thy (rls' : Rule_Set.id) =
252 case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
254 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
255 "TODO exception hierarchy needs to be established.")
257 fun assoc_calc thy calID = let
259 raise ERROR ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
260 | ass ((calc, (keyi, _)) :: pairs, key) =
261 if key = keyi then calc else ass (pairs, key);
262 in ass (thy |> KEStore_Elems.get_calcs, calID) end;
264 fun assoc_calc' thy key = let
266 raise ERROR ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
267 | ass ((all as (keyi, _)) :: pairs, key') =
268 if key' = keyi then all else ass (pairs, key');
269 in ass (KEStore_Elems.get_calcs thy, key) end;
271 fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
273 fun get_pbls () = get_ref_thy () |> KEStore_Elems.get_pbls;
274 fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
275 fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
276 fun get_expls () = get_ref_thy () |> KEStore_Elems.get_expls;
280 empty = \<open>Rule_Set.empty\<close> and
281 e_rrls = \<open>Rule_Set.e_rrls\<close>
283 section \<open>determine sequence of main parts in thehier\<close>
285 KEStore_Elems.add_thes
286 [(Thy_Write.Html {guh = Thy_Write.part2guh ["IsacKnowledge"], html = "",
287 mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
288 (Thy_Write.Html {guh = Thy_Write.part2guh ["Isabelle"], html = "",
289 mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
290 (Thy_Write.Html {guh = Thy_Write.part2guh ["IsacScripts"], html = "",
291 mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
294 section \<open>Functions for checking KEStore_Elems\<close>
296 fun short_string_of_rls Rule_Set.Empty = "Erls"
297 | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
298 "Rls {#calc = " ^ string_of_int (length calc) ^
299 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
300 | short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) =
301 "Seq {#calc = " ^ string_of_int (length calc) ^
302 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
303 | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
304 fun check_kestore_rls (rls', (thyID, rls)) =
305 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
307 fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
309 (* we avoid term_to_string''' defined later *)
310 fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) =
311 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
312 (Proof_Context.init_global @{theory})))) t ^ ", " ^ References_Def.to_string s ^ ")";
314 fun count_kestore_ptyps [] = 0
315 | count_kestore_ptyps ((Store.Node (_, _, ps)) :: ps') =
316 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
317 fun check_kestore_ptyp' strfun (Store.Node (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
318 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
319 val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.s_to_string;
320 fun ptyp_ord ((Store.Node (s1, _, _)), (Store.Node (s2, _, _))) = string_ord (s1, s2);
321 fun pbt_ord ({guh = guh'1, ...} : Probl_Def.T, {guh = guh'2, ...} : Probl_Def.T) = string_ord (guh'1, guh'2);
322 fun sort_kestore_ptyp' _ [] = []
323 | sort_kestore_ptyp' ordfun ((Store.Node (key, pbts, ps)) :: ps') =
324 ((Store.Node (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
325 :: sort_kestore_ptyp' ordfun ps');
326 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
328 fun metguh2str ({guh,...} : Meth_Def.T) = guh : string;
329 fun check_kestore_met (mp: Meth_Def.T Store.node) =
330 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
331 fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = string_ord (guh'1, guh'2);
332 val sort_kestore_met = sort_kestore_ptyp' met_ord;
334 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Write.thes2str))) thes
335 fun write_thes thydata_list =
337 |> map (fn (id, the) => (Thy_Write.theID2str id, Thy_Write.the2str the))