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 "thy-write.sml"
52 section \<open>Knowledge elements for problems and methods\<close>
54 (* Knowledge (and Exercises) are held by "Know_Store" in Isac's Java front-end.
55 In the front-end Knowledge comprises theories, problems and methods.
56 Elements of problems and methods are defined in theories alongside
57 the development of respective language elements.
58 However, the structure of methods and problems is independent from theories'
59 deductive structure. Thus respective structures are built in Build_Thydata.thy.
61 Most elements of problems and methods are implemented in "Knowledge/", but some
62 of them are implemented in "ProgLang/" already; thus "Know_Store.thy" got this
63 location in the directory structure.
65 get_* retrieves all * of the respective theory PLUS of all ancestor theories.
67 signature KESTORE_ELEMS =
69 val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
70 val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
71 val get_calcs: theory -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list
72 val add_calcs: (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list -> theory -> theory
73 val get_cas: theory -> CAS_Def.T list
74 val add_cas: CAS_Def.T list -> theory -> theory
75 val get_pbls: theory -> Probl_Def.store
76 val add_pbls: Proof.context -> (Probl_Def.T * References_Def.id) list -> theory -> theory
77 val get_mets: theory -> Meth_Def.store
78 val add_mets: Proof.context -> (Meth_Def.T * References_Def.id) list -> theory -> theory
79 val get_thes: theory -> (Thy_Write.thydata Store.node) list
80 val add_thes: (Thy_Write.thydata * Thy_Write.theID) list -> theory -> theory (* thydata dropped at existing elems *)
81 val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory
82 val get_ref_thy: unit -> theory
83 val set_ref_thy: theory -> unit
86 structure KEStore_Elems: KESTORE_ELEMS =
88 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
90 structure Data = Theory_Data (
91 type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
94 val merge = Rule_Set.to_kestore;
96 fun get_rlss thy = Data.get thy
97 fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
99 structure Data = Theory_Data (
100 type T = (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list;
103 val merge = merge Eval_Def.calc_eq;
105 fun get_calcs thy = Data.get thy
106 fun add_calcs calcs = Data.map (union_overwrite Eval_Def.calc_eq calcs)
108 structure Data = Theory_Data (
109 type T = (term * (References_Def.T * (term list -> (term * term list) list))) list;
112 val merge = merge CAS_Def.equal;
114 fun get_cas thy = Data.get thy
115 fun add_cas cas = Data.map (union_overwrite CAS_Def.equal cas)
117 structure Data = Theory_Data (
118 type T = Probl_Def.store;
119 val empty = [Probl_Def.empty_store];
121 val merge = Store.merge;
123 fun get_pbls thy = Data.get thy;
124 fun add_pbls ctxt pbts thy =
126 fun add_pbt (pbt as {guh,...}, pblID) =
127 (* the pblID has the leaf-element as first; better readability achieved *)
128 (if (Config.get ctxt check_unique) then Probl_Def.check_unique guh (Data.get thy) else ();
129 rev pblID |> Store.insert pblID pbt);
130 in Data.map (fold add_pbt pbts) thy end;
132 structure Data = Theory_Data (
133 type T = Meth_Def.store;
134 val empty = [Meth_Def.empty_store];
136 val merge = Store.merge;
138 val get_mets = Data.get;
139 fun add_mets ctxt mets thy =
141 fun add_met (met as {guh,...}, metID) =
142 (if (Config.get ctxt check_unique) then Meth_Def.check_unique guh (Data.get thy) else ();
143 Store.insert metID met metID);
144 in Data.map (fold add_met mets) thy end;
146 structure Data = Theory_Data (
147 type T = (Thy_Write.thydata Store.node) list;
150 val merge = Store.merge; (* relevant for store_thm, store_rls *)
152 fun get_thes thy = Data.get thy
153 fun add_thes thes thy = let
154 fun add_the (thydata, theID) = Thy_Write.add_thydata ([], theID) thydata
155 in Data.map (fold add_the thes) thy end;
156 fun insert_fillpats fis thy =
158 fun update_elem (theID, fillpats) =
160 val hthm = Store.get (Data.get thy) theID theID
161 val hthm' = Thy_Write.update_hthm hthm fillpats
163 raise ERROR ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
164 in Store.update theID theID hthm' end
165 in Data.map (fold update_elem fis) thy end
167 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
168 fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)
169 fun get_ref_thy () = Synchronized.value cur_thy;
174 subsection \<open>Isar command syntax\<close>
179 val parse_rule = Parse.name -- Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source);
181 val ml = ML_Lex.read;
183 fun ml_rule thy (name, source) =
184 ml "(" @ ml (ML_Syntax.print_string name) @ ml ", " @
185 ml "(" @ ml (ML_Syntax.print_string (Context.theory_name thy)) @ ml ", " @
186 ML_Lex.read_source source @ ml "))";
188 fun ml_rules thy args =
189 ml "Theory.setup (KEStore_Elems.add_rlss [" @
190 flat (separate (ml ",") (map (ml_rule thy) args)) @ ml "])";
193 Outer_Syntax.command \<^command_keyword>\<open>rule_set_knowledge\<close> "register ISAC rule set to Knowledge Store"
194 (Parse.and_list1 parse_rule >> (fn args => Toplevel.theory (fn thy =>
195 thy |> Context.theory_map
196 (ML_Context.expression (Position.thread_data ()) (ml_rules thy args)))));
199 Parse.name -- (\<^keyword>\<open>(\<close> |-- Parse.const --| \<^keyword>\<open>)\<close>) ||
200 Scan.ahead Parse.name -- Parse.const;
203 Outer_Syntax.command \<^command_keyword>\<open>calculation\<close>
204 "prepare ISAC calculation and register it to Knowledge Store"
205 (calc_name -- (\<^keyword>\<open>=\<close> |-- Parse.!!! Parse.ML_source) >> (fn ((calcID, const), source) =>
206 Toplevel.theory (fn thy =>
208 val ctxt = Proof_Context.init_global thy;
209 val Const (c, _) = Proof_Context.read_const {proper = true, strict = true} ctxt const;
211 ML_Context.expression (Input.pos_of source)
212 (ml "Theory.setup (Eval_Def.set_data (" @ ML_Lex.read_source source @ ml "))")
213 |> Context.theory_map;
214 val eval = Eval_Def.the_data (set_data thy);
215 in KEStore_Elems.add_calcs [(calcID, (c, eval))] thy end)))
221 section \<open>Re-use existing access functions for knowledge elements\<close>
223 The independence of problems' and methods' structure enforces the accesse
224 functions to use "Isac_Knowledge", the final theory which comprises all knowledge defined.
227 val get_ref_thy = KEStore_Elems.get_ref_thy;
229 fun assoc_rls (rls' : Rule_Set.id) =
230 case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
232 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
233 "TODO exception hierarchy needs to be established.")
235 fun assoc_rls' thy (rls' : Rule_Set.id) =
236 case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
238 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
239 "TODO exception hierarchy needs to be established.")
241 fun assoc_calc thy calID = let
243 raise ERROR ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
244 | ass ((calc, (keyi, _)) :: pairs, key) =
245 if key = keyi then calc else ass (pairs, key);
246 in ass (thy |> KEStore_Elems.get_calcs, calID) end;
248 fun assoc_calc' thy key = let
250 raise ERROR ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
251 | ass ((all as (keyi, _)) :: pairs, key') =
252 if key' = keyi then all else ass (pairs, key');
253 in ass (KEStore_Elems.get_calcs thy, key) end;
255 fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
257 fun get_pbls () = get_ref_thy () |> KEStore_Elems.get_pbls;
258 fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
259 fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
263 empty = \<open>Rule_Set.empty\<close> and
264 e_rrls = \<open>Rule_Set.e_rrls\<close>
266 section \<open>determine sequence of main parts in thehier\<close>
268 KEStore_Elems.add_thes
269 [(Thy_Write.Html {guh = Thy_Write.part2guh ["IsacKnowledge"], html = "",
270 mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
271 (Thy_Write.Html {guh = Thy_Write.part2guh ["Isabelle"], html = "",
272 mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
273 (Thy_Write.Html {guh = Thy_Write.part2guh ["IsacScripts"], html = "",
274 mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
277 section \<open>Functions for checking KEStore_Elems\<close>
279 fun short_string_of_rls Rule_Set.Empty = "Erls"
280 | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
281 "Rls {#calc = " ^ string_of_int (length calc) ^
282 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
283 | short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) =
284 "Seq {#calc = " ^ string_of_int (length calc) ^
285 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
286 | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
287 fun check_kestore_rls (rls', (thyID, rls)) =
288 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
290 fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
292 (* we avoid term_to_string''' defined later *)
293 fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) =
294 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
295 (Proof_Context.init_global @{theory})))) t ^ ", " ^ References_Def.to_string s ^ ")";
297 fun count_kestore_ptyps [] = 0
298 | count_kestore_ptyps ((Store.Node (_, _, ps)) :: ps') =
299 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
300 fun check_kestore_ptyp' strfun (Store.Node (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
301 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
302 val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.s_to_string;
303 fun ptyp_ord ((Store.Node (s1, _, _)), (Store.Node (s2, _, _))) = string_ord (s1, s2);
304 fun pbt_ord ({guh = guh'1, ...} : Probl_Def.T, {guh = guh'2, ...} : Probl_Def.T) = string_ord (guh'1, guh'2);
305 fun sort_kestore_ptyp' _ [] = []
306 | sort_kestore_ptyp' ordfun ((Store.Node (key, pbts, ps)) :: ps') =
307 ((Store.Node (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
308 :: sort_kestore_ptyp' ordfun ps');
309 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
311 fun metguh2str ({guh,...} : Meth_Def.T) = guh : string;
312 fun check_kestore_met (mp: Meth_Def.T Store.node) =
313 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
314 fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = string_ord (guh'1, guh'2);
315 val sort_kestore_met = sort_kestore_ptyp' met_ord;
317 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Write.thes2str))) thes
318 fun write_thes thydata_list =
320 |> map (fn (id, the) => (Thy_Write.theID2str id, Thy_Write.the2str the))