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.T list
72 val add_rew_ord: Rewrite_Ord.T 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 structure Data = Theory_Data (
95 type T = (string * (LibraryC.subst -> term * term -> bool)) list;
98 val merge = merge Rewrite_Ord.equal;
100 fun get_rew_ord thy = Data.get thy
101 fun add_rew_ord rlss = Data.map (curry (Library.merge Rewrite_Ord.equal) rlss)
103 structure Data = Theory_Data (
104 type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
107 val merge = Rule_Set.to_kestore;
109 fun get_rlss thy = Data.get thy
110 fun add_rlss rlss = Data.map (curry (Library.merge Rule_Set.equal) rlss)
112 structure Data = Theory_Data (
113 type T = (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list;
116 val merge = merge Eval_Def.calc_eq;
118 fun get_calcs thy = Data.get thy
119 fun add_calcs calcs = Data.map (curry (Library.merge Eval_Def.calc_eq) calcs)
121 structure Data = Theory_Data (
122 type T = (term * (References_Def.T * (term list -> (term * term list) list))) list;
125 val merge = merge CAS_Def.equal;
127 fun get_cas thy = Data.get thy
128 fun add_cas cas = Data.map (curry (Library.merge CAS_Def.equal) cas)
130 structure Data = Theory_Data (
131 type T = Probl_Def.store;
132 val empty = [Probl_Def.empty_store];
134 val merge = Store.merge;
136 fun get_pbls thy = Data.get thy;
137 fun add_pbls ctxt pbts thy =
139 fun add_pbt (pbt as {guh,...}, pblID) =
140 (* the pblID has the leaf-element as first; better readability achieved *)
141 (if (Config.get ctxt check_unique) then Probl_Def.check_unique guh (Data.get thy) else ();
142 rev pblID |> Store.insert pblID pbt);
143 in Data.map (fold add_pbt pbts) thy end;
145 structure Data = Theory_Data (
146 type T = Meth_Def.store;
147 val empty = [Meth_Def.empty_store];
149 val merge = Store.merge;
151 val get_mets = Data.get;
152 fun add_mets ctxt mets thy =
154 fun add_met (met as {guh,...}, metID) =
155 (if (Config.get ctxt check_unique) then Meth_Def.check_unique guh (Data.get thy) else ();
156 Store.insert metID met metID);
157 in Data.map (fold add_met mets) thy end;
159 structure Data = Theory_Data (
160 type T = Example.store;
161 val empty = [Example.empty_store];
163 val merge = Store.merge;
165 val get_expls = Data.get;
166 fun add_expls expls thy =
168 fun add_expl (expl, expl_id) = Store.insert expl_id expl expl_id;
169 in Data.map (fold add_expl expls) thy end;
171 structure Data = Theory_Data (
172 type T = (Thy_Write.thydata Store.node) list;
175 val merge = Store.merge; (* relevant for store_thm, store_rls *)
177 fun get_thes thy = Data.get thy
178 fun add_thes thes thy = let
179 fun add_the (thydata, theID) = Thy_Write.add_thydata ([], theID) thydata
180 in Data.map (fold add_the thes) thy end;
181 fun insert_fillpats fis thy =
183 fun update_elem (theID, fillpats) =
185 val hthm = Store.get (Data.get thy) theID theID
186 val hthm' = Thy_Write.update_hthm hthm fillpats
188 raise ERROR ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
189 in Store.update theID theID hthm' end
190 in Data.map (fold update_elem fis) thy end
192 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
193 fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)
194 fun get_ref_thy () = Synchronized.value cur_thy;
199 subsection \<open>Isar command syntax\<close>
204 val parse_rule = Parse.name -- Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source);
206 val ml = ML_Lex.read;
208 fun ml_rule thy (name, source) =
209 ml "(" @ ml (ML_Syntax.print_string name) @ ml ", " @
210 ml "(" @ ml (ML_Syntax.print_string (Context.theory_name thy)) @ ml ", " @
211 ML_Lex.read_source source @ ml "))";
213 fun ml_rules thy args =
214 ml "Theory.setup (KEStore_Elems.add_rlss [" @
215 flat (separate (ml ",") (map (ml_rule thy) args)) @ ml "])";
218 Outer_Syntax.command \<^command_keyword>\<open>rule_set_knowledge\<close> "register ISAC rule set to Knowledge Store"
219 (Parse.and_list1 parse_rule >> (fn args => Toplevel.theory (fn thy =>
220 thy |> Context.theory_map
221 (ML_Context.expression (Position.thread_data ()) (ml_rules thy args)))));
224 Parse.name -- (\<^keyword>\<open>(\<close> |-- Parse.const --| \<^keyword>\<open>)\<close>) ||
225 Scan.ahead Parse.name -- Parse.const;
228 Outer_Syntax.command \<^command_keyword>\<open>calculation\<close>
229 "prepare ISAC calculation and register it to Knowledge Store"
230 (calc_name -- (\<^keyword>\<open>=\<close> |-- Parse.!!! Parse.ML_source) >> (fn ((calcID, const), source) =>
231 Toplevel.theory (fn thy =>
233 val ctxt = Proof_Context.init_global thy;
234 val Const (c, _) = Proof_Context.read_const {proper = true, strict = true} ctxt const;
236 ML_Context.expression (Input.pos_of source)
237 (ml "Theory.setup (Eval_Def.set_data (" @ ML_Lex.read_source source @ ml "))")
238 |> Context.theory_map;
239 val eval = Eval_Def.the_data (set_data thy);
240 in KEStore_Elems.add_calcs [(calcID, (c, eval))] thy end)))
246 section \<open>Re-use existing access functions for knowledge elements\<close>
248 The independence of problems' and methods' structure from theory dependency structure
249 enforces the access functions to use "Isac_Knowledge",
250 the final theory which comprises all knowledge defined.
253 val get_ref_thy = KEStore_Elems.get_ref_thy;
255 fun assoc' ([], key) = raise ERROR ("ME_Isa: rew_ord \"" ^ key ^ "\" not in system 2")
256 | assoc' ((keyi, xi) :: pairs, key) =
257 if key = keyi then SOME xi else assoc' (pairs, key);
258 fun assoc_rew_ord thy ro = ((the o assoc') (KEStore_Elems.get_rew_ord thy, ro))
259 handle ERROR _ => raise ERROR ("ME_Isa: rew_ord \"" ^ ro ^ "\" not in system 1");
261 fun assoc_rls (rls' : Rule_Set.id) =
262 case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
264 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
265 "TODO exception hierarchy needs to be established.")
267 fun assoc_rls' thy (rls' : Rule_Set.id) =
268 case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
270 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
271 "TODO exception hierarchy needs to be established.")
273 fun assoc_calc thy calID = let
275 raise ERROR ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
276 | ass ((calc, (keyi, _)) :: pairs, key) =
277 if key = keyi then calc else ass (pairs, key);
278 in ass (thy |> KEStore_Elems.get_calcs, calID) end;
280 fun assoc_calc' thy key = let
282 raise ERROR ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
283 | ass ((all as (keyi, _)) :: pairs, key') =
284 if key' = keyi then all else ass (pairs, key');
285 in ass (KEStore_Elems.get_calcs thy, key) end;
287 fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
289 fun get_pbls () = get_ref_thy () |> KEStore_Elems.get_pbls;
290 fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
291 fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
292 fun get_expls () = get_ref_thy () |> KEStore_Elems.get_expls;
296 empty = \<open>Rule_Set.empty\<close> and
297 e_rrls = \<open>Rule_Set.e_rrls\<close>
299 section \<open>determine sequence of main parts in thehier\<close>
301 KEStore_Elems.add_thes
302 [(Thy_Write.Html {guh = Thy_Write.part2guh ["IsacKnowledge"], html = "",
303 mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
304 (Thy_Write.Html {guh = Thy_Write.part2guh ["Isabelle"], html = "",
305 mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
306 (Thy_Write.Html {guh = Thy_Write.part2guh ["IsacScripts"], html = "",
307 mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
310 section \<open>Functions for checking KEStore_Elems\<close>
312 fun short_string_of_rls Rule_Set.Empty = "Erls"
313 | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
314 "Rls {#calc = " ^ string_of_int (length calc) ^
315 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
316 | short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) =
317 "Seq {#calc = " ^ string_of_int (length calc) ^
318 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
319 | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
320 fun check_kestore_rls (rls', (thyID, rls)) =
321 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
323 fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
325 (* we avoid term_to_string''' defined later *)
326 fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) =
327 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
328 (Proof_Context.init_global @{theory})))) t ^ ", " ^ References_Def.to_string s ^ ")";
330 fun count_kestore_ptyps [] = 0
331 | count_kestore_ptyps ((Store.Node (_, _, ps)) :: ps') =
332 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
333 fun check_kestore_ptyp' strfun (Store.Node (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
334 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
335 val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.s_to_string;
336 fun ptyp_ord ((Store.Node (s1, _, _)), (Store.Node (s2, _, _))) = string_ord (s1, s2);
337 fun pbt_ord ({guh = guh'1, ...} : Probl_Def.T, {guh = guh'2, ...} : Probl_Def.T) = string_ord (guh'1, guh'2);
338 fun sort_kestore_ptyp' _ [] = []
339 | sort_kestore_ptyp' ordfun ((Store.Node (key, pbts, ps)) :: ps') =
340 ((Store.Node (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
341 :: sort_kestore_ptyp' ordfun ps');
342 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
344 fun metguh2str ({guh,...} : Meth_Def.T) = guh : string;
345 fun check_kestore_met (mp: Meth_Def.T Store.node) =
346 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
347 fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = string_ord (guh'1, guh'2);
348 val sort_kestore_met = sort_kestore_ptyp' met_ord;
350 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Write.thes2str))) thes
351 fun write_thes thydata_list =
353 |> map (fn (id, the) => (Thy_Write.theID2str id, Thy_Write.the2str the))
359 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
361 union_overwrite: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list;
362 merge : ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
365 val l1 = [1,2,3,4,5];
366 val l2 = [4,5,6,7,8];
368 union_overwrite eq l1 l2 = [8, 7, 6, 1, 2, 3, 4, 5];
369 Library.merge eq (l1, l2) = [6, 7, 8, 1, 2, 3, 4, 5]
372 Library.merge eq (*: _a list * _a list -> _a list*);
373 curry (Library.merge eq)(*: _a list -> _a list -> _a list*)