walther@59887
|
1 |
(* Title: src/Tools/isac/Know_Store.thy
|
wneuper@59586
|
2 |
Author: Mathias Lehnfeld
|
walther@59871
|
3 |
|
walther@60154
|
4 |
Calc work on Problem employing MethodC; both are collected in a respective Store;
|
walther@59890
|
5 |
The collections' structure is independent from the dependency graph of Isabelle's theories
|
walther@59890
|
6 |
in Knowledge.
|
walther@59917
|
7 |
Store is also used by Thy_Write, required for Isac's Java front end, irrelevant for PIDE.
|
walther@59890
|
8 |
|
walther@59887
|
9 |
The files (in "xxxxx-def.sml") contain definitions required for Know_Store;
|
walther@59871
|
10 |
they also include minimal code required for other "xxxxx-def.sml" files.
|
walther@59871
|
11 |
These files have companion files "xxxxx.sml" with all further code,
|
walther@59871
|
12 |
located at appropriate positions in the file structure.
|
walther@59871
|
13 |
|
walther@59871
|
14 |
The separation of "xxxxx-def.sml" from "xxxxx.sml" should be overcome by
|
walther@59871
|
15 |
appropriate use of polymorphic high order functions.
|
wneuper@59586
|
16 |
*)
|
wneuper@59586
|
17 |
|
wenzelm@60286
|
18 |
theory Know_Store
|
wenzelm@60286
|
19 |
imports Complex_Main
|
wenzelm@60313
|
20 |
keywords "rule_set_knowledge" "calculation" :: thy_decl
|
wenzelm@60223
|
21 |
begin
|
wneuper@59586
|
22 |
|
wenzelm@60223
|
23 |
setup \<open>
|
wenzelm@60223
|
24 |
ML_Antiquotation.conditional \<^binding>\<open>isac_test\<close>
|
wenzelm@60223
|
25 |
(fn _ => Options.default_bool \<^system_option>\<open>isac_test\<close>)
|
wenzelm@60223
|
26 |
\<close>
|
wenzelm@60223
|
27 |
|
wneuper@59586
|
28 |
ML_file libraryC.sml
|
walther@59880
|
29 |
ML_file theoryC.sml
|
walther@59868
|
30 |
ML_file unparseC.sml
|
walther@59874
|
31 |
ML_file "rule-def.sml"
|
walther@59875
|
32 |
ML_file "thmC-def.sml"
|
walther@59919
|
33 |
ML_file "eval-def.sml" (*rename identifiers by use of struct.id*)
|
walther@59867
|
34 |
ML_file "rewrite-order.sml" (*rename identifiers by use of struct.id*)
|
wneuper@59586
|
35 |
ML_file rule.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@59985
|
41 |
ML_file "references-def.sml"
|
walther@59945
|
42 |
ML_file "model-pattern.sml"
|
walther@59893
|
43 |
ML_file "problem-def.sml"
|
walther@59893
|
44 |
ML_file "method-def.sml"
|
walther@59893
|
45 |
ML_file "cas-def.sml"
|
walther@59917
|
46 |
ML_file "thy-write.sml"
|
walther@59882
|
47 |
|
wneuper@59586
|
48 |
ML \<open>
|
wneuper@59586
|
49 |
\<close> ML \<open>
|
wneuper@59587
|
50 |
\<close> ML \<open>
|
wneuper@59586
|
51 |
\<close>
|
wneuper@59586
|
52 |
section \<open>Knowledge elements for problems and methods\<close>
|
wneuper@59586
|
53 |
ML \<open>
|
walther@59887
|
54 |
(* Knowledge (and Exercises) are held by "Know_Store" in Isac's Java front-end.
|
wneuper@59586
|
55 |
In the front-end Knowledge comprises theories, problems and methods.
|
wneuper@59586
|
56 |
Elements of problems and methods are defined in theories alongside
|
wneuper@59586
|
57 |
the development of respective language elements.
|
wneuper@59586
|
58 |
However, the structure of methods and problems is independent from theories'
|
wneuper@59586
|
59 |
deductive structure. Thus respective structures are built in Build_Thydata.thy.
|
wneuper@59586
|
60 |
|
wneuper@59586
|
61 |
Most elements of problems and methods are implemented in "Knowledge/", but some
|
walther@59887
|
62 |
of them are implemented in "ProgLang/" already; thus "Know_Store.thy" got this
|
wneuper@59586
|
63 |
location in the directory structure.
|
wneuper@59586
|
64 |
|
wneuper@59586
|
65 |
get_* retrieves all * of the respective theory PLUS of all ancestor theories.
|
wneuper@59586
|
66 |
*)
|
wneuper@59586
|
67 |
signature KESTORE_ELEMS =
|
wneuper@59586
|
68 |
sig
|
walther@59879
|
69 |
val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
|
walther@59879
|
70 |
val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
|
walther@59919
|
71 |
val get_calcs: theory -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list
|
walther@59919
|
72 |
val add_calcs: (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list -> theory -> theory
|
walther@59896
|
73 |
val get_cas: theory -> CAS_Def.T list
|
walther@59896
|
74 |
val add_cas: CAS_Def.T list -> theory -> theory
|
Walther@60495
|
75 |
val get_pbls: theory -> Probl_Def.store
|
Walther@60502
|
76 |
val add_pbls: Proof.context -> (Probl_Def.T * References_Def.id) list -> theory -> theory
|
walther@59895
|
77 |
val get_mets: theory -> Meth_Def.store
|
Walther@60502
|
78 |
val add_mets: Proof.context -> (Meth_Def.T * References_Def.id) list -> theory -> theory
|
walther@59917
|
79 |
val get_thes: theory -> (Thy_Write.thydata Store.node) list
|
walther@59917
|
80 |
val add_thes: (Thy_Write.thydata * Thy_Write.theID) list -> theory -> theory (* thydata dropped at existing elems *)
|
walther@59917
|
81 |
val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory
|
wneuper@59586
|
82 |
val get_ref_thy: unit -> theory
|
wneuper@59586
|
83 |
val set_ref_thy: theory -> unit
|
wneuper@59586
|
84 |
end;
|
wneuper@59586
|
85 |
|
wneuper@59586
|
86 |
structure KEStore_Elems: KESTORE_ELEMS =
|
wneuper@59586
|
87 |
struct
|
wneuper@59586
|
88 |
fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
|
wneuper@59586
|
89 |
|
wneuper@59586
|
90 |
structure Data = Theory_Data (
|
walther@59879
|
91 |
type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
|
wneuper@59586
|
92 |
val empty = [];
|
wneuper@59586
|
93 |
val extend = I;
|
walther@59852
|
94 |
val merge = Rule_Set.to_kestore;
|
wneuper@59586
|
95 |
);
|
wneuper@59586
|
96 |
fun get_rlss thy = Data.get thy
|
walther@59852
|
97 |
fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
|
wneuper@59586
|
98 |
|
wneuper@59586
|
99 |
structure Data = Theory_Data (
|
walther@59919
|
100 |
type T = (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list;
|
wneuper@59586
|
101 |
val empty = [];
|
wneuper@59586
|
102 |
val extend = I;
|
walther@59919
|
103 |
val merge = merge Eval_Def.calc_eq;
|
wneuper@59586
|
104 |
);
|
wneuper@59586
|
105 |
fun get_calcs thy = Data.get thy
|
walther@59919
|
106 |
fun add_calcs calcs = Data.map (union_overwrite Eval_Def.calc_eq calcs)
|
wneuper@59586
|
107 |
|
wneuper@59586
|
108 |
structure Data = Theory_Data (
|
walther@59985
|
109 |
type T = (term * (References_Def.T * (term list -> (term * term list) list))) list;
|
wneuper@59586
|
110 |
val empty = [];
|
wneuper@59586
|
111 |
val extend = I;
|
walther@59896
|
112 |
val merge = merge CAS_Def.equal;
|
wneuper@59586
|
113 |
);
|
wneuper@59586
|
114 |
fun get_cas thy = Data.get thy
|
walther@59896
|
115 |
fun add_cas cas = Data.map (union_overwrite CAS_Def.equal cas)
|
wneuper@59586
|
116 |
|
wneuper@59586
|
117 |
structure Data = Theory_Data (
|
walther@59894
|
118 |
type T = Probl_Def.store;
|
walther@59894
|
119 |
val empty = [Probl_Def.empty_store];
|
wneuper@59586
|
120 |
val extend = I;
|
walther@59897
|
121 |
val merge = Store.merge;
|
wneuper@59586
|
122 |
);
|
Walther@60495
|
123 |
fun get_pbls thy = Data.get thy;
|
Walther@60502
|
124 |
fun add_pbls ctxt pbts thy =
|
Walther@60502
|
125 |
let
|
Walther@60502
|
126 |
fun add_pbt (pbt as {guh,...}, pblID) =
|
Walther@60502
|
127 |
(* the pblID has the leaf-element as first; better readability achieved *)
|
Walther@60502
|
128 |
(if (Config.get ctxt check_unique) then Probl_Def.check_unique guh (Data.get thy) else ();
|
Walther@60502
|
129 |
rev pblID |> Store.insert pblID pbt);
|
Walther@60502
|
130 |
in Data.map (fold add_pbt pbts) thy end;
|
wneuper@59586
|
131 |
|
wneuper@59586
|
132 |
structure Data = Theory_Data (
|
walther@59895
|
133 |
type T = Meth_Def.store;
|
walther@59895
|
134 |
val empty = [Meth_Def.empty_store];
|
wneuper@59586
|
135 |
val extend = I;
|
walther@59897
|
136 |
val merge = Store.merge;
|
wneuper@59586
|
137 |
);
|
wneuper@59586
|
138 |
val get_mets = Data.get;
|
Walther@60502
|
139 |
fun add_mets ctxt mets thy =
|
Walther@60502
|
140 |
let
|
Walther@60502
|
141 |
fun add_met (met as {guh,...}, metID) =
|
Walther@60502
|
142 |
(if (Config.get ctxt check_unique) then Meth_Def.check_unique guh (Data.get thy) else ();
|
Walther@60502
|
143 |
Store.insert metID met metID);
|
Walther@60502
|
144 |
in Data.map (fold add_met mets) thy end;
|
wneuper@59586
|
145 |
|
wneuper@59586
|
146 |
structure Data = Theory_Data (
|
walther@59917
|
147 |
type T = (Thy_Write.thydata Store.node) list;
|
wneuper@59586
|
148 |
val empty = [];
|
wneuper@59586
|
149 |
val extend = I;
|
walther@59897
|
150 |
val merge = Store.merge; (* relevant for store_thm, store_rls *)
|
wneuper@59586
|
151 |
);
|
wneuper@59586
|
152 |
fun get_thes thy = Data.get thy
|
wneuper@59586
|
153 |
fun add_thes thes thy = let
|
walther@59917
|
154 |
fun add_the (thydata, theID) = Thy_Write.add_thydata ([], theID) thydata
|
wneuper@59586
|
155 |
in Data.map (fold add_the thes) thy end;
|
wneuper@59586
|
156 |
fun insert_fillpats fis thy =
|
wneuper@59586
|
157 |
let
|
wneuper@59586
|
158 |
fun update_elem (theID, fillpats) =
|
wneuper@59586
|
159 |
let
|
walther@59897
|
160 |
val hthm = Store.get (Data.get thy) theID theID
|
walther@59917
|
161 |
val hthm' = Thy_Write.update_hthm hthm fillpats
|
wneuper@59586
|
162 |
handle ERROR _ =>
|
walther@59962
|
163 |
raise ERROR ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
|
walther@59897
|
164 |
in Store.update theID theID hthm' end
|
wneuper@59586
|
165 |
in Data.map (fold update_elem fis) thy end
|
wneuper@59586
|
166 |
|
wneuper@59586
|
167 |
val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
|
wneuper@59586
|
168 |
fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)
|
wneuper@59586
|
169 |
fun get_ref_thy () = Synchronized.value cur_thy;
|
wneuper@59586
|
170 |
end;
|
wneuper@59586
|
171 |
\<close>
|
wneuper@59586
|
172 |
|
wenzelm@60286
|
173 |
|
wenzelm@60286
|
174 |
subsection \<open>Isar command syntax\<close>
|
wenzelm@60286
|
175 |
|
wenzelm@60286
|
176 |
ML \<open>
|
wenzelm@60286
|
177 |
local
|
wenzelm@60286
|
178 |
|
wenzelm@60286
|
179 |
val parse_rule = Parse.name -- Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source);
|
wenzelm@60286
|
180 |
|
wenzelm@60286
|
181 |
val ml = ML_Lex.read;
|
wenzelm@60286
|
182 |
|
wenzelm@60286
|
183 |
fun ml_rule thy (name, source) =
|
wenzelm@60286
|
184 |
ml "(" @ ml (ML_Syntax.print_string name) @ ml ", " @
|
wenzelm@60286
|
185 |
ml "(" @ ml (ML_Syntax.print_string (Context.theory_name thy)) @ ml ", " @
|
wenzelm@60286
|
186 |
ML_Lex.read_source source @ ml "))";
|
wenzelm@60286
|
187 |
|
wenzelm@60286
|
188 |
fun ml_rules thy args =
|
wenzelm@60286
|
189 |
ml "Theory.setup (KEStore_Elems.add_rlss [" @
|
wenzelm@60286
|
190 |
flat (separate (ml ",") (map (ml_rule thy) args)) @ ml "])";
|
wenzelm@60286
|
191 |
|
wenzelm@60286
|
192 |
val _ =
|
wenzelm@60289
|
193 |
Outer_Syntax.command \<^command_keyword>\<open>rule_set_knowledge\<close> "register ISAC rule set to Knowledge Store"
|
wenzelm@60286
|
194 |
(Parse.and_list1 parse_rule >> (fn args => Toplevel.theory (fn thy =>
|
wenzelm@60286
|
195 |
thy |> Context.theory_map
|
wenzelm@60286
|
196 |
(ML_Context.expression (Position.thread_data ()) (ml_rules thy args)))));
|
wenzelm@60286
|
197 |
|
wenzelm@60313
|
198 |
val calc_name =
|
wenzelm@60313
|
199 |
Parse.name -- (\<^keyword>\<open>(\<close> |-- Parse.const --| \<^keyword>\<open>)\<close>) ||
|
wenzelm@60313
|
200 |
Scan.ahead Parse.name -- Parse.const;
|
wenzelm@60313
|
201 |
|
wenzelm@60313
|
202 |
val _ =
|
wenzelm@60313
|
203 |
Outer_Syntax.command \<^command_keyword>\<open>calculation\<close>
|
wenzelm@60313
|
204 |
"prepare ISAC calculation and register it to Knowledge Store"
|
wenzelm@60313
|
205 |
(calc_name -- (\<^keyword>\<open>=\<close> |-- Parse.!!! Parse.ML_source) >> (fn ((calcID, const), source) =>
|
wenzelm@60313
|
206 |
Toplevel.theory (fn thy =>
|
wenzelm@60313
|
207 |
let
|
wenzelm@60313
|
208 |
val ctxt = Proof_Context.init_global thy;
|
wenzelm@60313
|
209 |
val Const (c, _) = Proof_Context.read_const {proper = true, strict = true} ctxt const;
|
wenzelm@60314
|
210 |
val set_data =
|
wenzelm@60313
|
211 |
ML_Context.expression (Input.pos_of source)
|
wenzelm@60313
|
212 |
(ml "Theory.setup (Eval_Def.set_data (" @ ML_Lex.read_source source @ ml "))")
|
wenzelm@60313
|
213 |
|> Context.theory_map;
|
wenzelm@60314
|
214 |
val eval = Eval_Def.the_data (set_data thy);
|
wenzelm@60313
|
215 |
in KEStore_Elems.add_calcs [(calcID, (c, eval))] thy end)))
|
wenzelm@60313
|
216 |
|
wenzelm@60286
|
217 |
in end;
|
wenzelm@60286
|
218 |
\<close>
|
wenzelm@60286
|
219 |
|
wenzelm@60286
|
220 |
|
wneuper@59586
|
221 |
section \<open>Re-use existing access functions for knowledge elements\<close>
|
wneuper@59586
|
222 |
text \<open>
|
wneuper@59586
|
223 |
The independence of problems' and methods' structure enforces the accesse
|
wneuper@59592
|
224 |
functions to use "Isac_Knowledge", the final theory which comprises all knowledge defined.
|
wneuper@59586
|
225 |
\<close>
|
wneuper@59586
|
226 |
ML \<open>
|
wneuper@59586
|
227 |
val get_ref_thy = KEStore_Elems.get_ref_thy;
|
wneuper@59586
|
228 |
|
walther@59867
|
229 |
fun assoc_rls (rls' : Rule_Set.id) =
|
walther@59879
|
230 |
case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
|
wneuper@59586
|
231 |
SOME (_, rls) => rls
|
walther@59887
|
232 |
| NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
|
wneuper@59586
|
233 |
"TODO exception hierarchy needs to be established.")
|
wneuper@59586
|
234 |
|
walther@59867
|
235 |
fun assoc_rls' thy (rls' : Rule_Set.id) =
|
wneuper@59586
|
236 |
case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
|
wneuper@59586
|
237 |
SOME (_, rls) => rls
|
walther@59887
|
238 |
| NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
|
wneuper@59586
|
239 |
"TODO exception hierarchy needs to be established.")
|
wneuper@59586
|
240 |
|
wneuper@59586
|
241 |
fun assoc_calc thy calID = let
|
wneuper@59586
|
242 |
fun ass ([], key) =
|
walther@59962
|
243 |
raise ERROR ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
|
wneuper@59586
|
244 |
| ass ((calc, (keyi, _)) :: pairs, key) =
|
wneuper@59586
|
245 |
if key = keyi then calc else ass (pairs, key);
|
wneuper@59586
|
246 |
in ass (thy |> KEStore_Elems.get_calcs, calID) end;
|
wneuper@59586
|
247 |
|
wneuper@59586
|
248 |
fun assoc_calc' thy key = let
|
wneuper@59586
|
249 |
fun ass ([], key') =
|
walther@59962
|
250 |
raise ERROR ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
|
wneuper@59586
|
251 |
| ass ((all as (keyi, _)) :: pairs, key') =
|
wneuper@59586
|
252 |
if key' = keyi then all else ass (pairs, key');
|
wneuper@59586
|
253 |
in ass (KEStore_Elems.get_calcs thy, key) end;
|
wneuper@59586
|
254 |
|
wneuper@59586
|
255 |
fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
|
wneuper@59586
|
256 |
|
Walther@60495
|
257 |
fun get_pbls () = get_ref_thy () |> KEStore_Elems.get_pbls;
|
wneuper@59586
|
258 |
fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
|
wneuper@59586
|
259 |
fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
|
wneuper@59586
|
260 |
\<close>
|
wenzelm@60286
|
261 |
|
wenzelm@60289
|
262 |
rule_set_knowledge
|
wenzelm@60286
|
263 |
empty = \<open>Rule_Set.empty\<close> and
|
wenzelm@60286
|
264 |
e_rrls = \<open>Rule_Set.e_rrls\<close>
|
wneuper@59586
|
265 |
|
wneuper@59586
|
266 |
section \<open>determine sequence of main parts in thehier\<close>
|
wneuper@59586
|
267 |
setup \<open>
|
wneuper@59586
|
268 |
KEStore_Elems.add_thes
|
walther@59917
|
269 |
[(Thy_Write.Html {guh = Thy_Write.part2guh ["IsacKnowledge"], html = "",
|
wneuper@59586
|
270 |
mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
|
walther@59917
|
271 |
(Thy_Write.Html {guh = Thy_Write.part2guh ["Isabelle"], html = "",
|
wneuper@59586
|
272 |
mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
|
walther@59917
|
273 |
(Thy_Write.Html {guh = Thy_Write.part2guh ["IsacScripts"], html = "",
|
wneuper@59586
|
274 |
mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
|
wneuper@59586
|
275 |
\<close>
|
wneuper@59586
|
276 |
|
wneuper@59586
|
277 |
section \<open>Functions for checking KEStore_Elems\<close>
|
wneuper@59586
|
278 |
ML \<open>
|
walther@59851
|
279 |
fun short_string_of_rls Rule_Set.Empty = "Erls"
|
walther@59851
|
280 |
| short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
|
wneuper@59586
|
281 |
"Rls {#calc = " ^ string_of_int (length calc) ^
|
wneuper@59586
|
282 |
", #rules = " ^ string_of_int (length rules) ^ ", ..."
|
walther@59878
|
283 |
| short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) =
|
wneuper@59586
|
284 |
"Seq {#calc = " ^ string_of_int (length calc) ^
|
wneuper@59586
|
285 |
", #rules = " ^ string_of_int (length rules) ^ ", ..."
|
walther@59850
|
286 |
| short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
|
wneuper@59586
|
287 |
fun check_kestore_rls (rls', (thyID, rls)) =
|
wneuper@59586
|
288 |
"(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
|
wneuper@59586
|
289 |
|
walther@59852
|
290 |
fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
|
wneuper@59586
|
291 |
|
walther@59846
|
292 |
(* we avoid term_to_string''' defined later *)
|
walther@59896
|
293 |
fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) =
|
walther@59846
|
294 |
"(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
|
walther@59985
|
295 |
(Proof_Context.init_global @{theory})))) t ^ ", " ^ References_Def.to_string s ^ ")";
|
wneuper@59586
|
296 |
|
wneuper@59586
|
297 |
fun count_kestore_ptyps [] = 0
|
walther@59897
|
298 |
| count_kestore_ptyps ((Store.Node (_, _, ps)) :: ps') =
|
wneuper@59586
|
299 |
1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
|
walther@59897
|
300 |
fun check_kestore_ptyp' strfun (Store.Node (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
|
walther@59888
|
301 |
(strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
|
walther@59894
|
302 |
val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.s_to_string;
|
walther@59897
|
303 |
fun ptyp_ord ((Store.Node (s1, _, _)), (Store.Node (s2, _, _))) = string_ord (s1, s2);
|
walther@59894
|
304 |
fun pbt_ord ({guh = guh'1, ...} : Probl_Def.T, {guh = guh'2, ...} : Probl_Def.T) = string_ord (guh'1, guh'2);
|
wneuper@59586
|
305 |
fun sort_kestore_ptyp' _ [] = []
|
walther@59897
|
306 |
| sort_kestore_ptyp' ordfun ((Store.Node (key, pbts, ps)) :: ps') =
|
walther@59897
|
307 |
((Store.Node (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
|
wneuper@59586
|
308 |
:: sort_kestore_ptyp' ordfun ps');
|
wneuper@59586
|
309 |
val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
|
wneuper@59586
|
310 |
|
walther@59895
|
311 |
fun metguh2str ({guh,...} : Meth_Def.T) = guh : string;
|
walther@59897
|
312 |
fun check_kestore_met (mp: Meth_Def.T Store.node) =
|
wneuper@59586
|
313 |
check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
|
walther@59895
|
314 |
fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = string_ord (guh'1, guh'2);
|
wneuper@59586
|
315 |
val sort_kestore_met = sort_kestore_ptyp' met_ord;
|
wneuper@59586
|
316 |
|
walther@59917
|
317 |
fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Write.thes2str))) thes
|
wneuper@59586
|
318 |
fun write_thes thydata_list =
|
wneuper@59586
|
319 |
thydata_list
|
walther@59917
|
320 |
|> map (fn (id, the) => (Thy_Write.theID2str id, Thy_Write.the2str the))
|
wneuper@59586
|
321 |
|> map pair2str
|
wneuper@59586
|
322 |
|> map writeln
|
wneuper@59586
|
323 |
\<close>
|
wneuper@59586
|
324 |
ML \<open>
|
wneuper@59586
|
325 |
\<close> ML \<open>
|
wneuper@59586
|
326 |
\<close> ML \<open>
|
wneuper@59586
|
327 |
\<close>
|
wneuper@59586
|
328 |
end
|