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_rew_ord: theory -> Rewrite_Ord.rew_ord list
72 val add_rew_ord: Rewrite_Ord.rew_ord list -> theory -> theory
73 val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
74 val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
75 val get_calcs: theory -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list
76 val add_calcs: (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list -> theory -> theory
77 val get_cas: theory -> CAS_Def.T list
78 val add_cas: CAS_Def.T list -> theory -> theory
79 val get_pbls: theory -> Probl_Def.store
80 val add_pbls: Proof.context -> (Probl_Def.T * References_Def.id) list -> theory -> theory
81 val get_mets: theory -> Meth_Def.store
82 val add_mets: Proof.context -> (Meth_Def.T * References_Def.id) list -> theory -> theory
83 val get_expls: theory -> Example.store
84 val add_expls: (Example.T * Store.key) list -> theory -> theory
85 val get_thes: theory -> (Thy_Write.thydata Store.node) list
86 val add_thes: (Thy_Write.thydata * Thy_Write.theID) list -> theory -> theory (* thydata dropped at existing elems *)
87 val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory
88 val get_ref_thy: unit -> theory
89 val set_ref_thy: theory -> unit
92 structure KEStore_Elems(**): KESTORE_ELEMS(**) =
94 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
96 structure Data = Theory_Data (
97 type T = (string * (LibraryC.subst -> term * term -> bool)) list;
100 val merge = merge Rewrite_Ord.equal;
102 fun get_rew_ord thy = Data.get thy
103 fun add_rew_ord rlss = Data.map (union_overwrite Rewrite_Ord.equal rlss)
105 structure Data = Theory_Data (
106 type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
109 val merge = Rule_Set.to_kestore;
111 fun get_rlss thy = Data.get thy
112 fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
114 structure Data = Theory_Data (
115 type T = (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list;
118 val merge = merge Eval_Def.calc_eq;
120 fun get_calcs thy = Data.get thy
121 fun add_calcs calcs = Data.map (union_overwrite Eval_Def.calc_eq calcs)
123 structure Data = Theory_Data (
124 type T = (term * (References_Def.T * (term list -> (term * term list) list))) list;
127 val merge = merge CAS_Def.equal;
129 fun get_cas thy = Data.get thy
130 fun add_cas cas = Data.map (union_overwrite CAS_Def.equal cas)
132 structure Data = Theory_Data (
133 type T = Probl_Def.store;
134 val empty = [Probl_Def.empty_store];
136 val merge = Store.merge;
138 fun get_pbls thy = Data.get thy;
139 fun add_pbls ctxt pbts thy =
141 fun add_pbt (pbt as {guh,...}, pblID) =
142 (* the pblID has the leaf-element as first; better readability achieved *)
143 (if (Config.get ctxt check_unique) then Probl_Def.check_unique guh (Data.get thy) else ();
144 rev pblID |> Store.insert pblID pbt);
145 in Data.map (fold add_pbt pbts) thy end;
147 structure Data = Theory_Data (
148 type T = Meth_Def.store;
149 val empty = [Meth_Def.empty_store];
151 val merge = Store.merge;
153 val get_mets = Data.get;
154 fun add_mets ctxt mets thy =
156 fun add_met (met as {guh,...}, metID) =
157 (if (Config.get ctxt check_unique) then Meth_Def.check_unique guh (Data.get thy) else ();
158 Store.insert metID met metID);
159 in Data.map (fold add_met mets) thy end;
161 structure Data = Theory_Data (
162 type T = Example.store;
163 val empty = [Example.empty_store];
165 val merge = Store.merge;
167 val get_expls = Data.get;
168 fun add_expls expls thy =
170 fun add_expl (expl, expl_id) = Store.insert expl_id expl expl_id;
171 in Data.map (fold add_expl expls) thy end;
173 structure Data = Theory_Data (
174 type T = (Thy_Write.thydata Store.node) list;
177 val merge = Store.merge; (* relevant for store_thm, store_rls *)
179 fun get_thes thy = Data.get thy
180 fun add_thes thes thy = let
181 fun add_the (thydata, theID) = Thy_Write.add_thydata ([], theID) thydata
182 in Data.map (fold add_the thes) thy end;
183 fun insert_fillpats fis thy =
185 fun update_elem (theID, fillpats) =
187 val hthm = Store.get (Data.get thy) theID theID
188 val hthm' = Thy_Write.update_hthm hthm fillpats
190 raise ERROR ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
191 in Store.update theID theID hthm' end
192 in Data.map (fold update_elem fis) thy end
194 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
195 fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)
196 fun get_ref_thy () = Synchronized.value cur_thy;
201 subsection \<open>Isar command syntax\<close>
206 val parse_rule = Parse.name -- Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source);
208 val ml = ML_Lex.read;
210 fun ml_rule thy (name, source) =
211 ml "(" @ ml (ML_Syntax.print_string name) @ ml ", " @
212 ml "(" @ ml (ML_Syntax.print_string (Context.theory_name thy)) @ ml ", " @
213 ML_Lex.read_source source @ ml "))";
215 fun ml_rules thy args =
216 ml "Theory.setup (KEStore_Elems.add_rlss [" @
217 flat (separate (ml ",") (map (ml_rule thy) args)) @ ml "])";
220 Outer_Syntax.command \<^command_keyword>\<open>rule_set_knowledge\<close> "register ISAC rule set to Knowledge Store"
221 (Parse.and_list1 parse_rule >> (fn args => Toplevel.theory (fn thy =>
222 thy |> Context.theory_map
223 (ML_Context.expression (Position.thread_data ()) (ml_rules thy args)))));
226 Parse.name -- (\<^keyword>\<open>(\<close> |-- Parse.const --| \<^keyword>\<open>)\<close>) ||
227 Scan.ahead Parse.name -- Parse.const;
230 Outer_Syntax.command \<^command_keyword>\<open>calculation\<close>
231 "prepare ISAC calculation and register it to Knowledge Store"
232 (calc_name -- (\<^keyword>\<open>=\<close> |-- Parse.!!! Parse.ML_source) >> (fn ((calcID, const), source) =>
233 Toplevel.theory (fn thy =>
235 val ctxt = Proof_Context.init_global thy;
236 val Const (c, _) = Proof_Context.read_const {proper = true, strict = true} ctxt const;
238 ML_Context.expression (Input.pos_of source)
239 (ml "Theory.setup (Eval_Def.set_data (" @ ML_Lex.read_source source @ ml "))")
240 |> Context.theory_map;
241 val eval = Eval_Def.the_data (set_data thy);
242 in KEStore_Elems.add_calcs [(calcID, (c, eval))] thy end)))
248 section \<open>Re-use existing access functions for knowledge elements\<close>
250 The independence of problems' and methods' structure from theory dependency structure
251 enforces the access functions to use "Isac_Knowledge",
252 the final theory which comprises all knowledge defined.
255 val get_ref_thy = KEStore_Elems.get_ref_thy;
257 fun assoc' ([], key) = raise ERROR ("ME_Isa: rew_ord \"" ^ key ^ "\" not in system 2")
258 | assoc' ((keyi, xi) :: pairs, key) =
259 if key = keyi then SOME xi else assoc' (pairs, key);
260 fun assoc_rew_ord thy ro = ((the o assoc') (KEStore_Elems.get_rew_ord thy, ro))
261 handle ERROR _ => raise ERROR ("ME_Isa: rew_ord \"" ^ ro ^ "\" not in system 1");
263 fun assoc_rls (rls' : Rule_Set.id) =
264 case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
266 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
267 "TODO exception hierarchy needs to be established.")
269 fun assoc_rls' thy (rls' : Rule_Set.id) =
270 case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
272 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
273 "TODO exception hierarchy needs to be established.")
275 fun assoc_calc thy calID = let
277 raise ERROR ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
278 | ass ((calc, (keyi, _)) :: pairs, key) =
279 if key = keyi then calc else ass (pairs, key);
280 in ass (thy |> KEStore_Elems.get_calcs, calID) end;
282 fun assoc_calc' thy key = let
284 raise ERROR ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
285 | ass ((all as (keyi, _)) :: pairs, key') =
286 if key' = keyi then all else ass (pairs, key');
287 in ass (KEStore_Elems.get_calcs thy, key) end;
289 fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
291 fun get_pbls () = get_ref_thy () |> KEStore_Elems.get_pbls;
292 fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
293 fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
294 fun get_expls () = get_ref_thy () |> KEStore_Elems.get_expls;
298 empty = \<open>Rule_Set.empty\<close> and
299 e_rrls = \<open>Rule_Set.e_rrls\<close>
301 section \<open>determine sequence of main parts in thehier\<close>
303 KEStore_Elems.add_thes
304 [(Thy_Write.Html {guh = Thy_Write.part2guh ["IsacKnowledge"], html = "",
305 mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
306 (Thy_Write.Html {guh = Thy_Write.part2guh ["Isabelle"], html = "",
307 mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
308 (Thy_Write.Html {guh = Thy_Write.part2guh ["IsacScripts"], html = "",
309 mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
312 section \<open>Functions for checking KEStore_Elems\<close>
314 fun short_string_of_rls Rule_Set.Empty = "Erls"
315 | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
316 "Rls {#calc = " ^ string_of_int (length calc) ^
317 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
318 | short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) =
319 "Seq {#calc = " ^ string_of_int (length calc) ^
320 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
321 | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
322 fun check_kestore_rls (rls', (thyID, rls)) =
323 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
325 fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
327 (* we avoid term_to_string''' defined later *)
328 fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) =
329 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
330 (Proof_Context.init_global @{theory})))) t ^ ", " ^ References_Def.to_string s ^ ")";
332 fun count_kestore_ptyps [] = 0
333 | count_kestore_ptyps ((Store.Node (_, _, ps)) :: ps') =
334 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
335 fun check_kestore_ptyp' strfun (Store.Node (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
336 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
337 val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.s_to_string;
338 fun ptyp_ord ((Store.Node (s1, _, _)), (Store.Node (s2, _, _))) = string_ord (s1, s2);
339 fun pbt_ord ({guh = guh'1, ...} : Probl_Def.T, {guh = guh'2, ...} : Probl_Def.T) = string_ord (guh'1, guh'2);
340 fun sort_kestore_ptyp' _ [] = []
341 | sort_kestore_ptyp' ordfun ((Store.Node (key, pbts, ps)) :: ps') =
342 ((Store.Node (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
343 :: sort_kestore_ptyp' ordfun ps');
344 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
346 fun metguh2str ({guh,...} : Meth_Def.T) = guh : string;
347 fun check_kestore_met (mp: Meth_Def.T Store.node) =
348 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
349 fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = string_ord (guh'1, guh'2);
350 val sort_kestore_met = sort_kestore_ptyp' met_ord;
352 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Write.thes2str))) thes
353 fun write_thes thydata_list =
355 |> map (fn (id, the) => (Thy_Write.theID2str id, Thy_Write.the2str the))