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"
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_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list
76 val add_calcs: (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) 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_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list;
116 val merge = merge Eval_Def.equal;
118 fun get_calcs thy = Data.get thy
119 fun add_calcs calcs = Data.map (curry (Library.merge Eval_Def.equal) 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;
200 subsection \<open>Isar command syntax\<close>
205 val parse_rule = Parse.name -- Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source);
207 val ml = ML_Lex.read;
209 fun ml_rule thy (name, source) =
210 ml "(" @ ml (ML_Syntax.print_string name) @ ml ", " @
211 ml "(" @ ml (ML_Syntax.print_string (Context.theory_name thy)) @ ml ", " @
212 ML_Lex.read_source source @ ml "))";
214 fun ml_rules thy args =
215 ml "Theory.setup (KEStore_Elems.add_rlss [" @
216 flat (separate (ml ",") (map (ml_rule thy) args)) @ ml "])";
219 Outer_Syntax.command \<^command_keyword>\<open>rule_set_knowledge\<close> "register ISAC rule set to Knowledge Store"
220 (Parse.and_list1 parse_rule >> (fn args => Toplevel.theory (fn thy =>
221 thy |> Context.theory_map
222 (ML_Context.expression (Position.thread_data ()) (ml_rules thy args)))));
225 Parse.name -- (\<^keyword>\<open>(\<close> |-- Parse.const --| \<^keyword>\<open>)\<close>) ||
226 Scan.ahead Parse.name -- Parse.const;
229 Outer_Syntax.command \<^command_keyword>\<open>calculation\<close>
230 "prepare ISAC calculation and register it to Knowledge Store"
231 (calc_name -- (\<^keyword>\<open>=\<close> |-- Parse.!!! Parse.ML_source) >> (fn ((calcID, const), source) =>
232 Toplevel.theory (fn thy =>
234 val ctxt = Proof_Context.init_global thy;
235 val Const (c, _) = Proof_Context.read_const {proper = true, strict = true} ctxt const;
237 ML_Context.expression (Input.pos_of source)
238 (ml "Theory.setup (Eval_Def.ml_fun_to_store (" @ ML_Lex.read_source source @ ml "))")
239 |> Context.theory_map;
240 val eval = Eval_Def.ml_fun_from_store (set_data thy);
241 in KEStore_Elems.add_calcs [(calcID, (c, eval))] thy end)))
247 section \<open>Re-use existing access functions for knowledge elements\<close>
249 The independence of problems' and methods' structure from theory dependency structure
250 enforces the access functions to use "Isac_Knowledge",
251 the final theory which comprises all knowledge defined.
254 val get_ref_thy = KEStore_Elems.get_ref_thy;
256 fun assoc' ([], key) = raise ERROR ("ME_Isa: rew_ord \"" ^ key ^ "\" not in system 2")
257 | assoc' ((keyi, xi) :: pairs, key) =
258 if key = keyi then SOME xi else assoc' (pairs, key);
259 fun assoc_rew_ord thy ro = ((the o assoc') (KEStore_Elems.get_rew_ord thy, ro))
260 handle ERROR _ => raise ERROR ("ME_Isa: rew_ord \"" ^ ro ^ "\" not in system 1");
262 fun assoc_rls (rls' : Rule_Set.id) =
263 case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
265 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
266 "TODO exception hierarchy needs to be established.")
268 fun get_rls ctxt (rls' : Rule_Set.id) =
269 case AList.lookup (op =) (KEStore_Elems.get_rlss (Proof_Context.theory_of ctxt )) rls' of
271 | NONE => raise ERROR ("rls \"" ^ rls' ^ "\" missing in theory \"" ^
272 (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^
273 "\nTODO exception hierarchy needs to be established.")
275 fun assoc_rls' thy (rls' : Rule_Set.id) =
276 case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
278 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
279 "TODO exception hierarchy needs to be established.")
281 fun assoc_calc thy calID = let
283 raise ERROR ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
284 | ass ((calc, (keyi, _)) :: pairs, key) =
285 if key = keyi then calc else ass (pairs, key);
286 in ass (thy |> KEStore_Elems.get_calcs, calID) end;
288 fun assoc_calc' thy key = let
290 raise ERROR ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
291 | ass ((all as (keyi, _)) :: pairs, key') =
292 if key' = keyi then all else ass (pairs, key');
293 in ass (KEStore_Elems.get_calcs thy, key) end;
295 fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
297 fun get_pbls () = get_ref_thy () |> KEStore_Elems.get_pbls;
298 fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
299 fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
300 fun get_expls () = get_ref_thy () |> KEStore_Elems.get_expls;
304 empty = \<open>Rule_Set.empty\<close> and
305 e_rrls = \<open>Rule_Set.e_rrls\<close>
307 section \<open>determine sequence of main parts in thehier\<close>
309 KEStore_Elems.add_thes
310 [(Thy_Write.Html {guh = Thy_Write.part2guh ["IsacKnowledge"], html = "",
311 mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
312 (Thy_Write.Html {guh = Thy_Write.part2guh ["Isabelle"], html = "",
313 mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
314 (Thy_Write.Html {guh = Thy_Write.part2guh ["IsacScripts"], html = "",
315 mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
318 section \<open>Functions for checking KEStore_Elems\<close>
320 fun short_string_of_rls Rule_Set.Empty = "Erls"
321 | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
322 "Rls {#calc = " ^ string_of_int (length calc) ^
323 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
324 | short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) =
325 "Seq {#calc = " ^ string_of_int (length calc) ^
326 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
327 | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
328 fun check_kestore_rls (rls', (thyID, rls)) =
329 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
331 fun check_kestore_calc ((id, (c, _)) : Rule_Def.eval_ml_from_prog) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
333 (* we avoid term_to_string''' defined later *)
334 fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) =
335 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
336 (Proof_Context.init_global @{theory})))) t ^ ", " ^ References_Def.to_string s ^ ")";
338 fun count_kestore_ptyps [] = 0
339 | count_kestore_ptyps ((Store.Node (_, _, ps)) :: ps') =
340 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
341 fun check_kestore_ptyp' strfun (Store.Node (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
342 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
343 val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.s_to_string;
344 fun ptyp_ord ((Store.Node (s1, _, _)), (Store.Node (s2, _, _))) = string_ord (s1, s2);
345 fun pbt_ord ({guh = guh'1, ...} : Probl_Def.T, {guh = guh'2, ...} : Probl_Def.T) = string_ord (guh'1, guh'2);
346 fun sort_kestore_ptyp' _ [] = []
347 | sort_kestore_ptyp' ordfun ((Store.Node (key, pbts, ps)) :: ps') =
348 ((Store.Node (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
349 :: sort_kestore_ptyp' ordfun ps');
350 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
352 fun metguh2str ({guh,...} : Meth_Def.T) = guh : string;
353 fun check_kestore_met (mp: Meth_Def.T Store.node) =
354 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
355 fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = string_ord (guh'1, guh'2);
356 val sort_kestore_met = sort_kestore_ptyp' met_ord;
358 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Write.thes2str))) thes
359 fun write_thes thydata_list =
361 |> map (fn (id, the) => (Thy_Write.theID2str id, Thy_Write.the2str the))
367 get_rls: Proof.context -> Rule_Set.id -> Rule_Def.rule_set
369 get_rls: Proof.context -> Rule_Set.id -> Rule_Set.T
371 @{context} |> Proof_Context.theory_of |> Context.theory_name