1 (* Title: src/Tools/isac/Know_Store.thy
2 Author: Mathias Lehnfeld
4 Store of Theory_Data of all knowledge required by the Lucas-Interpreter.
6 Types of elements are defined in "xxxxx-def.sml". These files have companion files "xxxxx.sml"
7 with all further code, located at appropriate positions in the file structure.
8 (The separation of "xxxxx-def.sml" from "xxxxx.sml" should be overcome by
9 appropriate use of polymorphic high order functions.)
11 Notable are Problem.T and MethodC.T; these are trees with a structure different from
12 Isabelle's theories dependencies.
17 keywords "rule_set_knowledge" "calculation" :: thy_decl
21 ML_Antiquotation.conditional \<^binding>\<open>isac_test\<close>
22 (fn _ => Options.default_bool \<^system_option>\<open>isac_test\<close>)
29 ML_file "rule-def.sml"
30 ML_file "thmC-def.sml"
31 ML_file "eval-def.sml"
32 ML_file "rewrite-order.sml"
34 ML_file "references-def.sml"
36 ML_file "model-pattern.sml"
37 ML_file "error-pattern-def.sml"
38 ML_file "rule-set.sml"
41 ML_file "check-unique.sml"
42 ML_file "problem-def.sml"
43 ML_file "method-def.sml"
44 ML_file "formalise.sml"
51 section \<open>Knowledge elements for problems and methods\<close>
53 \<open>ML_structure Problem\<close>, \<open>ML_structure MethodC\<close> and \<open>Example\<close>s are held by "Know_Store".
55 The structure of \<open>ML_structure Problem\<close> and \<open>ML_structure MethodC\<close> is independent from
56 theories' dependency graph. Thus the respective elements are stored as \<open>TermC.as_string\<close>
57 and parsed on the fly within the current @{ML_structure Context},
58 while being loaded into \<open>ML_structure Calc\<close>.
60 Note: From the children of eb89f586b0b2 onwards the old functions (\<open>term TermC.typ_a2real\<close> etc)
61 are adapted for "adapt_to_type on the fly" until further clarification.
62 Why \<open>ML_structure Problem\<close> and \<open>ML_structure MethodC\<close> are not parsed on the fly
63 within the current \<open>ML_structure Context\<close> see \<open>ML_structure Refine\<close>
65 Most elements of \<open>ML_structure Problem\<close> and \<open>ML_structure MethodC\<close> are implemented in
66 \<open>directory Knowledge/\<close> but some of them are implemented in \<open>directory ProgLang/\<close>already;
67 thus \<open>theory Know_Store\<close> got this location in the directory structure.
69 \<open>term Know_Store.get_*\<close> retrieves all * of the respective theory PLUS of all ancestor theories.
71 signature KNOW_STORE =
73 val get_rew_ords: theory -> Rewrite_Ord.T list
74 val add_rew_ords: Rewrite_Ord.T list -> theory -> theory
75 val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
76 val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
77 val get_calcs: theory -> (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list
78 val add_calcs: (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list -> theory -> theory
79 val get_cass: theory -> CAS_Def.T list
80 val add_cass: CAS_Def.T list -> theory -> theory
81 val get_pbls: theory -> Probl_Def.store
82 val add_pbls: Proof.context -> (Probl_Def.T * References_Def.id) list -> theory -> theory
83 val get_mets: theory -> Meth_Def.store
84 val add_mets: Proof.context -> (Meth_Def.T * References_Def.id) list -> theory -> theory
85 val get_expls: theory -> Example.store
86 val add_expls: (Example.T * Store.key) list -> theory -> theory
87 val get_ref_last_thy: unit -> theory
88 val set_ref_last_thy: theory -> unit
89 val get_via_last_thy: ThyC.id -> theory (*only used for * (Sub-)problem retrieving respective thy
91 * CAS_Cmd, to be redesigned anyway
92 * Ctree.get_ctxt, ThmC.long_id
93 * in ContextC.for_ERROR *)
96 structure Know_Store(**): KNOW_STORE(**) =
98 structure Data = Theory_Data (
99 type T = Rewrite_Ord.T list;
101 val merge = merge Rewrite_Ord.equal;
103 fun get_rew_ords thy = Data.get thy
104 fun add_rew_ords rlss = Data.map (curry (Library.merge Rewrite_Ord.equal) rlss)
106 structure Data = Theory_Data (
107 type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
108 (* ^^^^^ would allow same Rls_Set.id for different thys, NOT impl. *)
110 val merge = Rule_Set.to_kestore;
112 fun get_rlss thy = Data.get thy
113 fun add_rlss rlss = Data.map (curry (Library.merge Rule_Set.equal) rlss)
115 structure Data = Theory_Data (
116 type T = (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list;
118 val merge = merge Eval_Def.equal;
120 fun get_calcs thy = Data.get thy
121 fun add_calcs calcs = Data.map (curry (Library.merge Eval_Def.equal) calcs)
123 structure Data = Theory_Data (
124 type T = (term * (References_Def.T * CAS_Def.generate_fn)) list;
126 val merge = merge CAS_Def.equal;
128 fun get_cass thy = Data.get thy
129 fun add_cass cas = Data.map (curry (Library.merge CAS_Def.equal) cas)
131 structure Data = Theory_Data (
132 type T = Probl_Def.store;
133 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];
148 val merge = Store.merge;
150 val get_mets = Data.get;
151 fun add_mets ctxt mets thy =
153 fun add_met (met as {guh,...}, metID) =
154 (if (Config.get ctxt check_unique) then Meth_Def.check_unique guh (Data.get thy) else ();
155 Store.insert metID met metID);
156 in Data.map (fold add_met mets) thy end;
158 structure Data = Theory_Data (
159 type T = Example.store;
160 val empty = [Example.empty_store];
161 val merge = Store.merge;
163 val get_expls = Data.get;
164 fun add_expls expls thy =
166 fun add_expl (expl, expl_id) = Store.insert expl_id expl expl_id;
167 in Data.map (fold add_expl expls) thy end;
170 val last_thy = Synchronized.var "finally_knowledge_complete" @{theory};
171 fun set_ref_last_thy thy = Synchronized.change last_thy (fn _ => thy); (* never RE-set ! *)
172 fun get_ref_last_thy () = Synchronized.value last_thy;
174 fun get_via_last_thy thy_id =
176 val last_thy = get_ref_last_thy ()
177 val known_thys = Theory.nodes_of last_thy
179 (find_first (fn thy => Context.theory_name thy = thy_id) known_thys
181 handle Option.Option => raise ERROR ("get_via_last_thy fails with " ^ quote thy_id)
188 subsection \<open>Isar command syntax\<close>
193 val parse_rule = Parse.name -- Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source);
195 val ml = ML_Lex.read;
197 fun ml_rule thy (name, source) =
198 ml "(" @ ml (ML_Syntax.print_string name) @ ml ", " @
199 ml "(" @ ml (ML_Syntax.print_string (Context.theory_name thy)) @ ml ", " @
200 ML_Lex.read_source source @ ml "))";
202 fun ml_rules thy args =
203 ml "Theory.setup (Know_Store.add_rlss [" @
204 flat (separate (ml ",") (map (ml_rule thy) args)) @ ml "])";
207 Outer_Syntax.command \<^command_keyword>\<open>rule_set_knowledge\<close> "register ISAC rule set to Knowledge Store"
208 (Parse.and_list1 parse_rule >> (fn args => Toplevel.theory (fn thy =>
209 thy |> Context.theory_map
210 (ML_Context.expression (Position.thread_data ()) (ml_rules thy args)))));
213 Parse.name -- (\<^keyword>\<open>(\<close> |-- Parse.const --| \<^keyword>\<open>)\<close>) ||
214 Scan.ahead Parse.name -- Parse.const;
217 Outer_Syntax.command \<^command_keyword>\<open>calculation\<close>
218 "prepare ISAC calculation and register it to Knowledge Store"
219 (calc_name -- (\<^keyword>\<open>=\<close> |-- Parse.!!! Parse.ML_source) >> (fn ((calcID, const), source) =>
220 Toplevel.theory (fn thy =>
222 val ctxt = Proof_Context.init_global thy;
223 val Const (c, _) = Proof_Context.read_const {proper = true, strict = true} ctxt const;
225 ML_Context.expression (Input.pos_of source)
226 (ml "Theory.setup (Eval_Def.ml_fun_to_store (" @ ML_Lex.read_source source @ ml "))")
227 |> Context.theory_map;
228 val eval = Eval_Def.ml_fun_from_store (set_data thy);
229 in Know_Store.add_calcs [(calcID, (c, eval))] thy end)))
235 section \<open>Re-use existing access functions for knowledge elements\<close>
237 The independence of problems' and methods' structure from theory dependency structure
238 enforces the access functions to use "Isac_Knowledge",
239 the final theory which comprises all knowledge defined.
242 val get_ref_last_thy = Know_Store.get_ref_last_thy;
244 (*val get_rew_ord: Proof.context -> string -> Rewrite_Ord.function*)
245 fun get_rew_ord ctxt (id: Rewrite_Ord.id) =
246 case AList.lookup (op =) (Know_Store.get_rew_ords (Proof_Context.theory_of ctxt)) id of
247 SOME function => function: Rewrite_Ord.function
248 | NONE => raise ERROR ("rewrite-order \"" ^ id ^ "\" missing in theory \"" ^
249 (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^
250 "\nTODO exception hierarchy needs to be established.")
252 (*val get_rls: Proof.context -> Rule_Set.id -> Rule_Def.rule_set*)
253 fun get_rls ctxt (id : Rule_Set.id) =
254 case AList.lookup (op =) (Know_Store.get_rlss (Proof_Context.theory_of ctxt)) id of
256 | NONE => raise ERROR ("rls \"" ^ id ^ "\" missing in theory \"" ^
257 (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^
258 "\nTODO exception hierarchy needs to be established.")
260 (*val get_calc: Proof.context -> Eval_Def.prog_id ->
261 Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)*)
262 fun get_calc ctxt (id: Eval_Def.prog_id) =
263 case AList.lookup (op =) (Know_Store.get_calcs (Proof_Context.theory_of ctxt)) id of
264 SOME const_id__ml_fun => (id, const_id__ml_fun)
265 | NONE => raise ERROR ("ml-calculation \"" ^ id ^ "\" missing in theory \"" ^
266 (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^
267 "\nTODO exception hierarchy needs to be established.")
269 (*val get_calc_prog_id: Proof.context -> Eval_Def.const_id -> Eval_Def.prog_id*)
270 fun get_calc_prog_id ctxt (const_id: Eval_Def.const_id) =
272 fun assoc ([], prog_id) =
273 raise ERROR ("ml-calculation \"" ^ prog_id ^ "\" missing in theory \"" ^
274 (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)." ^
275 "\nThus " ^ quote const_id ^ " cannot be retrieved." ^
276 "\nTODO exception hierarchy needs to be established.")
277 | assoc ((prog_id, (const_id, _)) :: pairs, key) =
278 if key = const_id then prog_id else assoc (pairs, key);
279 in assoc (ctxt |> Proof_Context.theory_of |> Know_Store.get_calcs, const_id) end;
281 (*val get_cas: Proof.context -> term -> References_Def.T * CAS_Def.generate_fn*)
282 fun get_cas ctxt tm =
283 case AList.lookup (op =) (Know_Store.get_cass (Proof_Context.theory_of ctxt)) tm of
284 SOME refs__gen_fun => refs__gen_fun: References_Def.T * CAS_Def.generate_fn
285 | NONE => raise ERROR ("CAS_Cmd \"" ^
286 UnparseC.term_in_thy (get_ref_last_thy ()) tm ^ "\" missing in theory \"" ^
287 (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^
288 "\nTODO exception hierarchy needs to be established.")
290 (*for starting an Exmaple by CAS_Cmd*)
291 (*val get_cas_global: term -> References_Def.T * CAS_Def.generate_fn*)
292 fun get_cas_global tm =
294 val thy = get_ref_last_thy ()
296 case AList.lookup (op =) (Know_Store.get_cass thy) tm of
297 NONE => (writeln ("CAS_Cmd \"" ^
298 UnparseC.term_in_thy thy tm ^ "\" missing in theory \"" ^
299 (thy |> Context.theory_name) ^ "\" (and ancestors).");
301 | SOME refs__gen_fun => SOME refs__gen_fun
305 fun get_pbls () = get_ref_last_thy () |> Know_Store.get_pbls;
306 fun get_mets () = get_ref_last_thy () |> Know_Store.get_mets;
307 fun get_expls () = get_ref_last_thy () |> Know_Store.get_expls;
311 empty = \<open>Rule_Set.empty\<close> and
312 e_rrls = \<open>Rule_Set.e_rrls\<close>
314 section \<open>Functions for checking Know_Store\<close>
316 fun short_string_of_rls Rule_Set.Empty = "Erls"
317 | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
318 "Rls {#calc = " ^ string_of_int (length calc) ^
319 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
320 | short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) =
321 "Seq {#calc = " ^ string_of_int (length calc) ^
322 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
323 | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
324 fun check_kestore_rls (rls', (thyID, rls)) =
325 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
327 fun check_kestore_calc ((id, (c, _)) : Rule_Def.eval_ml_from_prog) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
329 (* we avoid term_to_string''' defined later *)
330 fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) =
331 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
332 (Proof_Context.init_global @{theory})))) t ^ ", " ^ References_Def.to_string s ^ ")";
334 fun count_kestore_ptyps [] = 0
335 | count_kestore_ptyps ((Store.Node (_, _, ps)) :: ps') =
336 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
337 fun check_kestore_ptyp' strfun (Store.Node (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
338 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
339 fun check_kestore_ptyp ctxt ptyp = check_kestore_ptyp' (Probl_Def.s_to_string ctxt) ptyp;
340 fun ptyp_ord ((Store.Node (s1, _, _)), (Store.Node (s2, _, _))) = string_ord (s1, s2);
341 fun pbt_ord ({guh = guh'1, ...} : Probl_Def.T, {guh = guh'2, ...} : Probl_Def.T) = string_ord (guh'1, guh'2);
342 fun sort_kestore_ptyp' _ [] = []
343 | sort_kestore_ptyp' ordfun ((Store.Node (key, pbts, ps)) :: ps') =
344 ((Store.Node (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
345 :: sort_kestore_ptyp' ordfun ps');
346 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
348 fun metguh2str ({guh,...} : Meth_Def.T) = guh : string;
349 fun check_kestore_met (mp: Meth_Def.T Store.node) =
350 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
351 fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = string_ord (guh'1, guh'2);
352 val sort_kestore_met = sort_kestore_ptyp' met_ord;