walther@59887
|
1 |
(* Title: src/Tools/isac/Know_Store.thy
|
wneuper@59586
|
2 |
Author: Mathias Lehnfeld
|
walther@59871
|
3 |
|
Walther@60547
|
4 |
Store of Theory_Data of all knowledge required by the Lucas-Interpreter.
|
walther@59890
|
5 |
|
Walther@60547
|
6 |
Types of elements are defined in "xxxxx-def.sml". These files have companion files "xxxxx.sml"
|
Walther@60547
|
7 |
with all further code, located at appropriate positions in the file structure.
|
Walther@60547
|
8 |
(The separation of "xxxxx-def.sml" from "xxxxx.sml" should be overcome by
|
Walther@60547
|
9 |
appropriate use of polymorphic high order functions.)
|
walther@59871
|
10 |
|
Walther@60547
|
11 |
Notable are Problem.T and MethodC.T; these are trees with a structure different from
|
Walther@60547
|
12 |
Isabelle's theories dependencies.
|
wneuper@59586
|
13 |
*)
|
wneuper@59586
|
14 |
|
wenzelm@60286
|
15 |
theory Know_Store
|
wenzelm@60286
|
16 |
imports Complex_Main
|
wenzelm@60313
|
17 |
keywords "rule_set_knowledge" "calculation" :: thy_decl
|
wenzelm@60223
|
18 |
begin
|
wneuper@59586
|
19 |
|
wenzelm@60223
|
20 |
setup \<open>
|
wenzelm@60223
|
21 |
ML_Antiquotation.conditional \<^binding>\<open>isac_test\<close>
|
wenzelm@60223
|
22 |
(fn _ => Options.default_bool \<^system_option>\<open>isac_test\<close>)
|
wenzelm@60223
|
23 |
\<close>
|
wenzelm@60223
|
24 |
|
wneuper@59586
|
25 |
ML_file libraryC.sml
|
walther@59880
|
26 |
ML_file theoryC.sml
|
walther@59868
|
27 |
ML_file unparseC.sml
|
walther@59874
|
28 |
ML_file "rule-def.sml"
|
walther@59875
|
29 |
ML_file "thmC-def.sml"
|
Walther@60557
|
30 |
ML_file "eval-def.sml"
|
Walther@60535
|
31 |
ML_file "rewrite-order.sml"
|
wneuper@59586
|
32 |
ML_file rule.sml
|
Walther@60583
|
33 |
ML_file "references-def.sml"
|
Walther@60602
|
34 |
ML_file "cas-def.sml"
|
Walther@60557
|
35 |
ML_file "model-pattern.sml"
|
walther@59909
|
36 |
ML_file "error-pattern-def.sml"
|
walther@59850
|
37 |
ML_file "rule-set.sml"
|
walther@59882
|
38 |
|
walther@59891
|
39 |
ML_file "store.sml"
|
walther@59892
|
40 |
ML_file "check-unique.sml"
|
walther@59893
|
41 |
ML_file "problem-def.sml"
|
walther@59893
|
42 |
ML_file "method-def.sml"
|
Walther@60505
|
43 |
ML_file "formalise.sml"
|
Walther@60505
|
44 |
ML_file "example.sml"
|
walther@59882
|
45 |
|
wneuper@59586
|
46 |
ML \<open>
|
wneuper@59586
|
47 |
\<close> ML \<open>
|
wneuper@59587
|
48 |
\<close> ML \<open>
|
wneuper@59586
|
49 |
\<close>
|
wneuper@59586
|
50 |
section \<open>Knowledge elements for problems and methods\<close>
|
Walther@60547
|
51 |
text \<open>
|
Walther@60554
|
52 |
\<open>ML_structure Problem\<close>, \<open>ML_structure MethodC\<close> and \<open>Example\<close>s are held by "Know_Store".
|
wneuper@59586
|
53 |
|
Walther@60554
|
54 |
The structure of \<open>ML_structure Problem\<close> and \<open>ML_structure MethodC\<close> is independent from
|
Walther@60554
|
55 |
theories' dependency graph. Thus the respective elements are stored as \<open>TermC.as_string\<close>
|
Walther@60554
|
56 |
and parsed on the fly within the current @{ML_structure Context},
|
Walther@60554
|
57 |
while being loaded into \<open>ML_structure Calc\<close>.
|
wneuper@59586
|
58 |
|
Walther@60555
|
59 |
Note: From the children of eb89f586b0b2 onwards the old functions (\<open>term TermC.typ_a2real\<close> etc)
|
Walther@60555
|
60 |
are adapted for "adapt_to_type on the fly" until further clarification.
|
Walther@60555
|
61 |
Why \<open>ML_structure Problem\<close> and \<open>ML_structure MethodC\<close> are not parsed on the fly
|
Walther@60555
|
62 |
within the current \<open>ML_structure Context\<close> see \<open>ML_structure Refine\<close>
|
Walther@60554
|
63 |
\<open>\<close>
|
Walther@60554
|
64 |
Most elements of \<open>ML_structure Problem\<close> and \<open>ML_structure MethodC\<close> are implemented in
|
Walther@60554
|
65 |
\<open>directory Knowledge/\<close> but some of them are implemented in \<open>directory ProgLang/\<close>already;
|
Walther@60554
|
66 |
thus \<open>theory Know_Store\<close> got this location in the directory structure.
|
Walther@60554
|
67 |
|
Walther@60554
|
68 |
\<open>term Know_Store.get_*\<close> retrieves all * of the respective theory PLUS of all ancestor theories.
|
Walther@60547
|
69 |
\<close> ML \<open>
|
Walther@60609
|
70 |
signature KNOW_STORE =
|
wneuper@59586
|
71 |
sig
|
Walther@60547
|
72 |
val get_rew_ords: theory -> Rewrite_Ord.T list
|
Walther@60547
|
73 |
val add_rew_ords: Rewrite_Ord.T list -> theory -> theory
|
walther@59879
|
74 |
val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
|
walther@59879
|
75 |
val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
|
Walther@60538
|
76 |
val get_calcs: theory -> (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list
|
Walther@60538
|
77 |
val add_calcs: (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list -> theory -> theory
|
Walther@60547
|
78 |
val get_cass: theory -> CAS_Def.T list
|
Walther@60547
|
79 |
val add_cass: CAS_Def.T list -> theory -> theory
|
Walther@60495
|
80 |
val get_pbls: theory -> Probl_Def.store
|
Walther@60502
|
81 |
val add_pbls: Proof.context -> (Probl_Def.T * References_Def.id) list -> theory -> theory
|
walther@59895
|
82 |
val get_mets: theory -> Meth_Def.store
|
Walther@60502
|
83 |
val add_mets: Proof.context -> (Meth_Def.T * References_Def.id) list -> theory -> theory
|
Walther@60505
|
84 |
val get_expls: theory -> Example.store
|
Walther@60505
|
85 |
val add_expls: (Example.T * Store.key) list -> theory -> theory
|
Walther@60608
|
86 |
val get_ref_last_thy: unit -> theory
|
Walther@60608
|
87 |
val set_ref_last_thy: theory -> unit
|
Walther@60639
|
88 |
val get_via_last_thy: ThyC.id -> theory (*only used for * (Sub-)problem retrieving respective thy
|
Walther@60649
|
89 |
* problem refinement
|
Walther@60649
|
90 |
* (test-)code to be deleted *)
|
Walther@60508
|
91 |
end;
|
wneuper@59586
|
92 |
|
Walther@60609
|
93 |
structure Know_Store(**): KNOW_STORE(**) =
|
wneuper@59586
|
94 |
struct
|
wneuper@59586
|
95 |
structure Data = Theory_Data (
|
Walther@60547
|
96 |
type T = Rewrite_Ord.T list;
|
Walther@60506
|
97 |
val empty = [];
|
Walther@60506
|
98 |
val merge = merge Rewrite_Ord.equal;
|
Walther@60506
|
99 |
);
|
Walther@60547
|
100 |
fun get_rew_ords thy = Data.get thy
|
Walther@60547
|
101 |
fun add_rew_ords rlss = Data.map (curry (Library.merge Rewrite_Ord.equal) rlss)
|
Walther@60506
|
102 |
|
Walther@60506
|
103 |
structure Data = Theory_Data (
|
walther@59879
|
104 |
type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
|
Walther@60547
|
105 |
(* ^^^^^ would allow same Rls_Set.id for different thys, NOT impl. *)
|
wneuper@59586
|
106 |
val empty = [];
|
walther@59852
|
107 |
val merge = Rule_Set.to_kestore;
|
wneuper@59586
|
108 |
);
|
wneuper@59586
|
109 |
fun get_rlss thy = Data.get thy
|
Walther@60521
|
110 |
fun add_rlss rlss = Data.map (curry (Library.merge Rule_Set.equal) rlss)
|
wneuper@59586
|
111 |
|
wneuper@59586
|
112 |
structure Data = Theory_Data (
|
Walther@60538
|
113 |
type T = (Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)) list;
|
wneuper@59586
|
114 |
val empty = [];
|
Walther@60538
|
115 |
val merge = merge Eval_Def.equal;
|
wneuper@59586
|
116 |
);
|
wneuper@59586
|
117 |
fun get_calcs thy = Data.get thy
|
Walther@60538
|
118 |
fun add_calcs calcs = Data.map (curry (Library.merge Eval_Def.equal) calcs)
|
wneuper@59586
|
119 |
|
wneuper@59586
|
120 |
structure Data = Theory_Data (
|
Walther@60547
|
121 |
type T = (term * (References_Def.T * CAS_Def.generate_fn)) list;
|
wneuper@59586
|
122 |
val empty = [];
|
walther@59896
|
123 |
val merge = merge CAS_Def.equal;
|
wneuper@59586
|
124 |
);
|
Walther@60547
|
125 |
fun get_cass thy = Data.get thy
|
Walther@60547
|
126 |
fun add_cass cas = Data.map (curry (Library.merge CAS_Def.equal) cas)
|
wneuper@59586
|
127 |
|
wneuper@59586
|
128 |
structure Data = Theory_Data (
|
walther@59894
|
129 |
type T = Probl_Def.store;
|
walther@59894
|
130 |
val empty = [Probl_Def.empty_store];
|
walther@59897
|
131 |
val merge = Store.merge;
|
wneuper@59586
|
132 |
);
|
Walther@60495
|
133 |
fun get_pbls thy = Data.get thy;
|
Walther@60502
|
134 |
fun add_pbls ctxt pbts thy =
|
Walther@60502
|
135 |
let
|
Walther@60502
|
136 |
fun add_pbt (pbt as {guh,...}, pblID) =
|
Walther@60502
|
137 |
(* the pblID has the leaf-element as first; better readability achieved *)
|
Walther@60502
|
138 |
(if (Config.get ctxt check_unique) then Probl_Def.check_unique guh (Data.get thy) else ();
|
Walther@60502
|
139 |
rev pblID |> Store.insert pblID pbt);
|
Walther@60502
|
140 |
in Data.map (fold add_pbt pbts) thy end;
|
wneuper@59586
|
141 |
|
wneuper@59586
|
142 |
structure Data = Theory_Data (
|
walther@59895
|
143 |
type T = Meth_Def.store;
|
walther@59895
|
144 |
val empty = [Meth_Def.empty_store];
|
walther@59897
|
145 |
val merge = Store.merge;
|
wneuper@59586
|
146 |
);
|
wneuper@59586
|
147 |
val get_mets = Data.get;
|
Walther@60502
|
148 |
fun add_mets ctxt mets thy =
|
Walther@60502
|
149 |
let
|
Walther@60502
|
150 |
fun add_met (met as {guh,...}, metID) =
|
Walther@60502
|
151 |
(if (Config.get ctxt check_unique) then Meth_Def.check_unique guh (Data.get thy) else ();
|
Walther@60502
|
152 |
Store.insert metID met metID);
|
Walther@60502
|
153 |
in Data.map (fold add_met mets) thy end;
|
wneuper@59586
|
154 |
|
wneuper@59586
|
155 |
structure Data = Theory_Data (
|
Walther@60505
|
156 |
type T = Example.store;
|
Walther@60505
|
157 |
val empty = [Example.empty_store];
|
Walther@60505
|
158 |
val merge = Store.merge;
|
Walther@60505
|
159 |
);
|
Walther@60505
|
160 |
val get_expls = Data.get;
|
Walther@60505
|
161 |
fun add_expls expls thy =
|
Walther@60505
|
162 |
let
|
Walther@60505
|
163 |
fun add_expl (expl, expl_id) = Store.insert expl_id expl expl_id;
|
Walther@60505
|
164 |
in Data.map (fold add_expl expls) thy end;
|
Walther@60505
|
165 |
|
wneuper@59586
|
166 |
|
Walther@60608
|
167 |
val last_thy = Synchronized.var "finally_knowledge_complete" @{theory};
|
Walther@60608
|
168 |
fun set_ref_last_thy thy = Synchronized.change last_thy (fn _ => thy); (* never RE-set ! *)
|
Walther@60608
|
169 |
fun get_ref_last_thy () = Synchronized.value last_thy;
|
Walther@60608
|
170 |
|
Walther@60608
|
171 |
fun get_via_last_thy thy_id =
|
Walther@60608
|
172 |
let
|
Walther@60608
|
173 |
val last_thy = get_ref_last_thy ()
|
Walther@60608
|
174 |
val known_thys = Theory.nodes_of last_thy
|
Walther@60608
|
175 |
in
|
Walther@60608
|
176 |
(find_first (fn thy => Context.theory_name thy = thy_id) known_thys
|
Walther@60608
|
177 |
|> the)
|
Walther@60608
|
178 |
handle Option.Option => raise ERROR ("get_via_last_thy fails with " ^ quote thy_id)
|
Walther@60608
|
179 |
end
|
Walther@60543
|
180 |
|
Walther@60543
|
181 |
(**)end(*struct*);
|
wneuper@59586
|
182 |
\<close>
|
wneuper@59586
|
183 |
|
wenzelm@60286
|
184 |
|
wenzelm@60286
|
185 |
subsection \<open>Isar command syntax\<close>
|
wenzelm@60286
|
186 |
|
wenzelm@60286
|
187 |
ML \<open>
|
wenzelm@60286
|
188 |
local
|
wenzelm@60286
|
189 |
|
wenzelm@60286
|
190 |
val parse_rule = Parse.name -- Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source);
|
wenzelm@60286
|
191 |
|
wenzelm@60286
|
192 |
val ml = ML_Lex.read;
|
wenzelm@60286
|
193 |
|
wenzelm@60286
|
194 |
fun ml_rule thy (name, source) =
|
wenzelm@60286
|
195 |
ml "(" @ ml (ML_Syntax.print_string name) @ ml ", " @
|
wenzelm@60286
|
196 |
ml "(" @ ml (ML_Syntax.print_string (Context.theory_name thy)) @ ml ", " @
|
wenzelm@60286
|
197 |
ML_Lex.read_source source @ ml "))";
|
wenzelm@60286
|
198 |
|
wenzelm@60286
|
199 |
fun ml_rules thy args =
|
Walther@60588
|
200 |
ml "Theory.setup (Know_Store.add_rlss [" @
|
wenzelm@60286
|
201 |
flat (separate (ml ",") (map (ml_rule thy) args)) @ ml "])";
|
wenzelm@60286
|
202 |
|
wenzelm@60286
|
203 |
val _ =
|
wenzelm@60289
|
204 |
Outer_Syntax.command \<^command_keyword>\<open>rule_set_knowledge\<close> "register ISAC rule set to Knowledge Store"
|
wenzelm@60286
|
205 |
(Parse.and_list1 parse_rule >> (fn args => Toplevel.theory (fn thy =>
|
wenzelm@60286
|
206 |
thy |> Context.theory_map
|
wenzelm@60286
|
207 |
(ML_Context.expression (Position.thread_data ()) (ml_rules thy args)))));
|
wenzelm@60286
|
208 |
|
wenzelm@60313
|
209 |
val calc_name =
|
wenzelm@60313
|
210 |
Parse.name -- (\<^keyword>\<open>(\<close> |-- Parse.const --| \<^keyword>\<open>)\<close>) ||
|
wenzelm@60313
|
211 |
Scan.ahead Parse.name -- Parse.const;
|
wenzelm@60313
|
212 |
|
wenzelm@60313
|
213 |
val _ =
|
wenzelm@60313
|
214 |
Outer_Syntax.command \<^command_keyword>\<open>calculation\<close>
|
wenzelm@60313
|
215 |
"prepare ISAC calculation and register it to Knowledge Store"
|
wenzelm@60313
|
216 |
(calc_name -- (\<^keyword>\<open>=\<close> |-- Parse.!!! Parse.ML_source) >> (fn ((calcID, const), source) =>
|
wenzelm@60313
|
217 |
Toplevel.theory (fn thy =>
|
wenzelm@60313
|
218 |
let
|
wenzelm@60313
|
219 |
val ctxt = Proof_Context.init_global thy;
|
wenzelm@60313
|
220 |
val Const (c, _) = Proof_Context.read_const {proper = true, strict = true} ctxt const;
|
wenzelm@60314
|
221 |
val set_data =
|
wenzelm@60313
|
222 |
ML_Context.expression (Input.pos_of source)
|
Walther@60538
|
223 |
(ml "Theory.setup (Eval_Def.ml_fun_to_store (" @ ML_Lex.read_source source @ ml "))")
|
wenzelm@60313
|
224 |
|> Context.theory_map;
|
Walther@60538
|
225 |
val eval = Eval_Def.ml_fun_from_store (set_data thy);
|
Walther@60588
|
226 |
in Know_Store.add_calcs [(calcID, (c, eval))] thy end)))
|
wenzelm@60313
|
227 |
|
wenzelm@60286
|
228 |
in end;
|
wenzelm@60286
|
229 |
\<close>
|
wenzelm@60286
|
230 |
|
wenzelm@60286
|
231 |
|
wneuper@59586
|
232 |
section \<open>Re-use existing access functions for knowledge elements\<close>
|
wneuper@59586
|
233 |
text \<open>
|
Walther@60508
|
234 |
The independence of problems' and methods' structure from theory dependency structure
|
Walther@60508
|
235 |
enforces the access functions to use "Isac_Knowledge",
|
Walther@60508
|
236 |
the final theory which comprises all knowledge defined.
|
wneuper@59586
|
237 |
\<close>
|
wneuper@59586
|
238 |
ML \<open>
|
Walther@60608
|
239 |
val get_ref_last_thy = Know_Store.get_ref_last_thy;
|
wneuper@59586
|
240 |
|
Walther@60550
|
241 |
(*val get_rew_ord: Proof.context -> string -> Rewrite_Ord.function*)
|
Walther@60547
|
242 |
fun get_rew_ord ctxt (id: Rewrite_Ord.id) =
|
Walther@60588
|
243 |
case AList.lookup (op =) (Know_Store.get_rew_ords (Proof_Context.theory_of ctxt)) id of
|
Walther@60547
|
244 |
SOME function => function: Rewrite_Ord.function
|
Walther@60547
|
245 |
| NONE => raise ERROR ("rewrite-order \"" ^ id ^ "\" missing in theory \"" ^
|
Walther@60547
|
246 |
(ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^
|
Walther@60547
|
247 |
"\nTODO exception hierarchy needs to be established.")
|
Walther@60506
|
248 |
|
Walther@60550
|
249 |
(*val get_rls: Proof.context -> Rule_Set.id -> Rule_Def.rule_set*)
|
Walther@60547
|
250 |
fun get_rls ctxt (id : Rule_Set.id) =
|
Walther@60588
|
251 |
case AList.lookup (op =) (Know_Store.get_rlss (Proof_Context.theory_of ctxt)) id of
|
Walther@60543
|
252 |
SOME (_, rls) => rls
|
Walther@60547
|
253 |
| NONE => raise ERROR ("rls \"" ^ id ^ "\" missing in theory \"" ^
|
Walther@60543
|
254 |
(ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^
|
Walther@60543
|
255 |
"\nTODO exception hierarchy needs to be established.")
|
Walther@60543
|
256 |
|
Walther@60550
|
257 |
(*val get_calc: Proof.context -> Eval_Def.prog_id ->
|
Walther@60550
|
258 |
Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)*)
|
Walther@60550
|
259 |
fun get_calc ctxt (id: Eval_Def.prog_id) =
|
Walther@60588
|
260 |
case AList.lookup (op =) (Know_Store.get_calcs (Proof_Context.theory_of ctxt)) id of
|
Walther@60550
|
261 |
SOME const_id__ml_fun => (id, const_id__ml_fun)
|
Walther@60550
|
262 |
| NONE => raise ERROR ("ml-calculation \"" ^ id ^ "\" missing in theory \"" ^
|
Walther@60550
|
263 |
(ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^
|
Walther@60550
|
264 |
"\nTODO exception hierarchy needs to be established.")
|
Walther@60550
|
265 |
|
Walther@60550
|
266 |
(*val get_calc_prog_id: Proof.context -> Eval_Def.const_id -> Eval_Def.prog_id*)
|
Walther@60550
|
267 |
fun get_calc_prog_id ctxt (const_id: Eval_Def.const_id) =
|
Walther@60550
|
268 |
let
|
Walther@60550
|
269 |
fun assoc ([], prog_id) =
|
Walther@60550
|
270 |
raise ERROR ("ml-calculation \"" ^ prog_id ^ "\" missing in theory \"" ^
|
Walther@60550
|
271 |
(ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)." ^
|
Walther@60550
|
272 |
"\nThus " ^ quote const_id ^ " cannot be retrieved." ^
|
Walther@60550
|
273 |
"\nTODO exception hierarchy needs to be established.")
|
Walther@60550
|
274 |
| assoc ((prog_id, (const_id, _)) :: pairs, key) =
|
Walther@60550
|
275 |
if key = const_id then prog_id else assoc (pairs, key);
|
Walther@60588
|
276 |
in assoc (ctxt |> Proof_Context.theory_of |> Know_Store.get_calcs, const_id) end;
|
wneuper@59586
|
277 |
|
Walther@60550
|
278 |
(*val get_cas: Proof.context -> term -> References_Def.T * CAS_Def.generate_fn*)
|
Walther@60547
|
279 |
fun get_cas ctxt tm =
|
Walther@60588
|
280 |
case AList.lookup (op =) (Know_Store.get_cass (Proof_Context.theory_of ctxt)) tm of
|
Walther@60547
|
281 |
SOME refs__gen_fun => refs__gen_fun: References_Def.T * CAS_Def.generate_fn
|
Walther@60547
|
282 |
| NONE => raise ERROR ("CAS_Cmd \"" ^
|
Walther@60608
|
283 |
UnparseC.term_in_thy (get_ref_last_thy ()) tm ^ "\" missing in theory \"" ^
|
Walther@60547
|
284 |
(ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^
|
Walther@60547
|
285 |
"\nTODO exception hierarchy needs to be established.")
|
Walther@60551
|
286 |
|
Walther@60550
|
287 |
(*for starting an Exmaple by CAS_Cmd*)
|
Walther@60550
|
288 |
(*val get_cas_global: term -> References_Def.T * CAS_Def.generate_fn*)
|
Walther@60550
|
289 |
fun get_cas_global tm =
|
Walther@60550
|
290 |
let
|
Walther@60608
|
291 |
val thy = get_ref_last_thy ()
|
Walther@60550
|
292 |
in
|
Walther@60588
|
293 |
case AList.lookup (op =) (Know_Store.get_cass thy) tm of
|
Walther@60550
|
294 |
NONE => (writeln ("CAS_Cmd \"" ^
|
Walther@60550
|
295 |
UnparseC.term_in_thy thy tm ^ "\" missing in theory \"" ^
|
Walther@60550
|
296 |
(thy |> Context.theory_name) ^ "\" (and ancestors).");
|
Walther@60550
|
297 |
NONE)
|
Walther@60550
|
298 |
| SOME refs__gen_fun => SOME refs__gen_fun
|
Walther@60550
|
299 |
end
|
Walther@60550
|
300 |
|
wneuper@59586
|
301 |
|
Walther@60608
|
302 |
fun get_pbls () = get_ref_last_thy () |> Know_Store.get_pbls;
|
Walther@60608
|
303 |
fun get_mets () = get_ref_last_thy () |> Know_Store.get_mets;
|
Walther@60608
|
304 |
fun get_expls () = get_ref_last_thy () |> Know_Store.get_expls;
|
wneuper@59586
|
305 |
\<close>
|
wenzelm@60286
|
306 |
|
wenzelm@60289
|
307 |
rule_set_knowledge
|
wenzelm@60286
|
308 |
empty = \<open>Rule_Set.empty\<close> and
|
wenzelm@60286
|
309 |
e_rrls = \<open>Rule_Set.e_rrls\<close>
|
wneuper@59586
|
310 |
|
Walther@60588
|
311 |
section \<open>Functions for checking Know_Store\<close>
|
wneuper@59586
|
312 |
ML \<open>
|
walther@59851
|
313 |
fun short_string_of_rls Rule_Set.Empty = "Erls"
|
walther@59851
|
314 |
| short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
|
wneuper@59586
|
315 |
"Rls {#calc = " ^ string_of_int (length calc) ^
|
wneuper@59586
|
316 |
", #rules = " ^ string_of_int (length rules) ^ ", ..."
|
walther@59878
|
317 |
| short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) =
|
wneuper@59586
|
318 |
"Seq {#calc = " ^ string_of_int (length calc) ^
|
wneuper@59586
|
319 |
", #rules = " ^ string_of_int (length rules) ^ ", ..."
|
walther@59850
|
320 |
| short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
|
wneuper@59586
|
321 |
fun check_kestore_rls (rls', (thyID, rls)) =
|
wneuper@59586
|
322 |
"(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
|
wneuper@59586
|
323 |
|
Walther@60537
|
324 |
fun check_kestore_calc ((id, (c, _)) : Rule_Def.eval_ml_from_prog) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
|
wneuper@59586
|
325 |
|
walther@59846
|
326 |
(* we avoid term_to_string''' defined later *)
|
walther@59896
|
327 |
fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) =
|
walther@59846
|
328 |
"(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
|
walther@59985
|
329 |
(Proof_Context.init_global @{theory})))) t ^ ", " ^ References_Def.to_string s ^ ")";
|
wneuper@59586
|
330 |
|
wneuper@59586
|
331 |
fun count_kestore_ptyps [] = 0
|
walther@59897
|
332 |
| count_kestore_ptyps ((Store.Node (_, _, ps)) :: ps') =
|
wneuper@59586
|
333 |
1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
|
walther@59897
|
334 |
fun check_kestore_ptyp' strfun (Store.Node (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
|
walther@59888
|
335 |
(strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
|
walther@59894
|
336 |
val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.s_to_string;
|
walther@59897
|
337 |
fun ptyp_ord ((Store.Node (s1, _, _)), (Store.Node (s2, _, _))) = string_ord (s1, s2);
|
walther@59894
|
338 |
fun pbt_ord ({guh = guh'1, ...} : Probl_Def.T, {guh = guh'2, ...} : Probl_Def.T) = string_ord (guh'1, guh'2);
|
wneuper@59586
|
339 |
fun sort_kestore_ptyp' _ [] = []
|
walther@59897
|
340 |
| sort_kestore_ptyp' ordfun ((Store.Node (key, pbts, ps)) :: ps') =
|
walther@59897
|
341 |
((Store.Node (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
|
wneuper@59586
|
342 |
:: sort_kestore_ptyp' ordfun ps');
|
wneuper@59586
|
343 |
val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
|
wneuper@59586
|
344 |
|
walther@59895
|
345 |
fun metguh2str ({guh,...} : Meth_Def.T) = guh : string;
|
walther@59897
|
346 |
fun check_kestore_met (mp: Meth_Def.T Store.node) =
|
wneuper@59586
|
347 |
check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
|
walther@59895
|
348 |
fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = string_ord (guh'1, guh'2);
|
wneuper@59586
|
349 |
val sort_kestore_met = sort_kestore_ptyp' met_ord;
|
Walther@60636
|
350 |
\<close>
|
wneuper@59586
|
351 |
|
wneuper@59586
|
352 |
ML \<open>
|
wneuper@59586
|
353 |
\<close> ML \<open>
|
wneuper@59586
|
354 |
\<close> ML \<open>
|
wneuper@59586
|
355 |
\<close>
|
wneuper@59586
|
356 |
end
|