1 (* elements of calculations.
2 they are partially held in association lists as ref's for
3 switching language levels (meta-string, object-values).
4 in order to keep these ref's during re-evaluation of code,
5 they are defined here at the beginning of the code.
6 Author: Walther Neuper 2003
7 (c) copyright due to lincense terms
14 val linefeed = (curry op^) "\n";
15 type authors = string list;
18 val empty_cterm' = "empty_cterm'";
20 type thmID = string; (* identifier for a thm (the shortest possible identifier) *)
21 type thmDeriv = string; (* WN120524 deprecated
22 thyID ^"."^ xxx ^"."^ thmID, see fun thmID_of_derivation_name
23 WN120524: dont use Thm.derivation_name, this is destroyed by num_str;
24 Thm.get_name_hint survives num_str and seems perfectly reliable *)
26 type thm' = thmID * cterm';(*WN060610 deprecated in favour of thm''*)
27 type thm'' = thmID * term;
30 (*.a 'guh'='globally unique handle' is a string unique for each element
31 of isac's KEStore and persistent over time
32 (in particular under shifts within the respective hierarchy);
34 # guh NOT resistant agains shifts from one thy to another
35 (which is the price for Isabelle's design: thy's overwrite ids of subthy's)
36 # requirement for matchTheory: induce guh from tac + current thy
37 (see 'fun thy_containing_thm', 'fun thy_containing_rls' etc.)
38 TODO: introduce to pbl, met.*)
40 val e_guh = "e_guh":guh;
44 (* eval function calling sml code during rewriting.
45 Unifying "type cal" and "type calc" would make Lucas-Interpretation more efficient,
46 see "fun rule2stac": instead of
47 Calc: calID * eval_fn -> rule
49 Calc: prog_calcID * (calID * eval_fn)) -> rule*)
50 type eval_fn = (string -> term -> theory -> (string * term) option);
51 fun e_evalfn (_:'a) (_:term) (_:theory) = NONE:(string * term) option;
52 (*. op in isa-term 'Const(op,_)' .*)
56 type cal = (calID * eval_fn);
57 (*. fun calculate_ fetches the evaluation-function via this list. *)
58 type prog_calcID = string;
59 type calc = (prog_calcID * cal);
61 prog_calcID * (* a simple identifier used in programs *)
62 (calID * (* a long identifier used in Const *)
63 eval_fn) (* an ML function *)
64 fun calc_eq ((pi1, (ci1, _)) : calc_elem, (pi2, (ci2, _)) : calc_elem) =
66 then if ci1 = ci2 then true else error ("calc_eq: " ^ ci1 ^ " <> " ^ ci2)
70 type subs' = (cterm' * cterm') list; (*16.11.00 for FE-KE*)
71 type subst = (term * term) list; (*here for ets2str*)
72 val e_subst = []:(term * term) list;
74 (*TODO.WN060610 make use of "type rew_ord" total*)
75 type rew_ord' = string;
76 val e_rew_ord' = "e_rew_ord" : rew_ord';
77 type rew_ord_ = subst -> Term.term * Term.term -> bool;
78 fun dummy_ord (_:subst) (_:term,_:term) = true;
79 val e_rew_ord_ = dummy_ord;
80 type rew_ord = rew_ord' * rew_ord_;
81 val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)
82 val e_rew_ordX = (e_rew_ord', e_rew_ord_) : rew_ord;
84 (* error patterns and fill patterns *)
85 type errpatID = string
87 errpatID (* one identifier for a list of patterns
88 DESIGN ?TODO: errpatID list for hierarchy of errpats ? *)
89 * term list (* error patterns *)
90 * thm list (* thms related to error patterns; note that respective lhs
91 do not match (which reflects student's error).
92 fillpatterns are stored with these thms. *)
94 (* for (at least) 2 kinds of access:
95 (1) given an errpatID, find the respective fillpats (e.g. in fun find_fill_pats)
96 (2) given a thm, find respective fillpats *)
97 type fillpatID = string
99 fillpatID (* DESIGN ?TODO: give an order w.r.t difficulty ? *)
100 * term (* the pattern with fill-in gaps *)
101 * errpatID; (* which the fillpat would be a help for
102 DESIGN ?TODO: list for several patterns ? *)
105 Erule (*.the empty rule .*)
106 | Thm of (string * Basic_Thm.thm)(*.a theorem, ie (identifier, Thm.thm).*)
107 | Calc of string * (*.sml-code manipulating a (sub)term .*)
108 (string -> term -> theory -> (string * term) option)
109 | Cal1 of string * (*.sml-code applied only to whole term
110 or left/right-hand-side of eqality .*)
111 (string -> term -> theory -> (string * term) option)
112 | Rls_ of rls (*.ie. rule sets may be nested.*)
115 | Prog of term (* for met *)
116 | Rfuns of (* for Rrls, usage see rational.sml ----- reverse rewrite ----- *)
117 {init_state : (* initialise for reverse rewriting by the Interpreter *)
118 term -> (* for this the rrlsstate is initialised: *)
119 term * (* the current formula: goes locate_gen -> next_tac via istate *)
120 term * (* the final formula *)
121 rule list (* of reverse rewrite set (#1#) *)
122 list * (* may be serveral, eg. in norm_rational *)
123 ( rule * (* Thm (+ Thm generated from Calc) resulting in ... *)
124 (term * (* ... rewrite with ... *)
125 term list)) (* ... assumptions *)
126 list, (* derivation from given term to normalform
127 in reverse order with sym_thm;
128 (#1#) could be extracted from here #1 *)
129 normal_form: (* the function which drives the Rrls ##############################*)
130 term -> (term * term list) option,
131 locate_rule: (* checks a rule R for being a cancel-rule, and if it is,
132 then return the list of rules (+ the terms they are rewriting to)
133 which need to be applied before R should be applied.
134 precondition: the rule is applicable to the argument-term. *)
135 rule list list -> (* the reverse rule list *)
136 term -> (* ... to which the rule shall be applied *)
137 rule -> (* ... to be applied to term *)
138 ( rule * (* value: a rule rewriting to ... *)
139 (term * (* ... the resulting term ... *)
140 term list)) (* ... with the assumptions ( //#0) *)
141 list, (* there may be several such rules; the list is empty,
142 if the rule has nothing to do with e.g. cancelation *)
143 next_rule: (* for a given term return the next rules to be done for cancelling *)
144 rule list list->(* the reverse rule list *)
145 term -> (* the term for which ... *)
146 rule option, (* ... this rule is appropriate for cancellation;
147 there may be no such rule (if the term is eg.canceled already*)
148 attach_form: (* checks an input term TI, if it may belong to e.g. a current
149 cancellation, by trying to derive it from the given term TG.
152 term -> (* TG, the last one agreed upon by user + math-eng *)
153 term -> (* TI, the next one input by the user *)
154 ( rule * (* the rule to be applied in order to reach TI *)
155 (term * (* ... obtained by applying the rule ... *)
156 term list)) (* ... and the respective assumptions *)
157 list} (* there may be several such rules; the list is empty, if the
158 users term does not belong to e.g. a cancellation of the term
161 Erls (*for init e_rls*)
163 | Rls of (*a confluent and terminating ruleset, in general *)
164 {id : string, (*for trace_rewrite:=true *)
165 preconds : term list, (*unused WN020820 *)
166 (*WN060616 for efficiency...
167 bdvs : false, (*set in prep_rls' for get_bdvs *)*)
168 rew_ord : rew_ord, (*for rules*)
169 erls : rls, (*for the conditions in rules *)
170 srls : rls, (*for evaluation of list_fns in script *)
171 calc : calc list, (*for Calculate in scr, set by prep_rls' *)
173 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
174 scr : scr} (*Prog term: generating intermed.steps *)
175 | Seq of (*a sequence of rules to be tried only once *)
176 {id : string, (*for trace_rewrite:=true *)
177 preconds : term list, (*unused 20.8.02 *)
178 (*WN060616 for efficiency...
179 bdvs : false, (*set in prep_rls' for get_bdvs *)*)
180 rew_ord : rew_ord, (*for rules *)
181 erls : rls, (*for the conditions in rules *)
182 srls : rls, (*for evaluation of list_fns in script *)
183 calc : calc list, (*for Calculate in scr, set by prep_rls' *)
185 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
186 scr : scr} (*Prog term (how to restrict type ???)*)
188 (*Rrls call SML-code and simulate an rls
189 difference: there is always _ONE_ redex rewritten in 1 call,
190 thus wrap Rrls by: Rls (Rls_ ...)*)
191 | Rrls of (* SML-functions within rewriting; step-wise execution provided;
193 difference: there is always _ONE_ redex rewritten in 1 call,
194 thus wrap Rrls by: Rls (Rls_ ...) *)
195 {id : string, (* for trace_rewrite := true *)
196 prepat : (term list *(* preconds, eval with subst from pattern;
197 if [@{term True}], match decides alone *)
198 term ) (* pattern matched with current (sub)term *)
199 list, (* meta-conjunction is or *)
200 rew_ord : rew_ord, (* for rules *)
201 erls : rls, (* for the conditions in rules and preconds *)
202 calc : calc list, (* for Calculate in scr, set automatic.in prep_rls' *)
203 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
204 scr : scr}; (* Rfuns {...} (how to restrict type ???) *)
206 fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info.get_theory thy');(*FIXXXME thy-ctxt*)
207 fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*)
209 fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac"); (*@{theory "Isac"}*)
211 val e_rule = Thm ("refl", @{thm refl});
212 fun id_of_thm (Thm (id, _)) = id
213 | id_of_thm _ = error "error id_of_thm";
214 fun thm_of_thm (Thm (_, thm)) = thm
215 | thm_of_thm _ = error "error thm_of_thm";
216 fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm);
218 fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
219 fun thyID_of_derivation_name dn = hd (space_explode "." dn);
221 fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
222 (strip_thy thmid1) = (strip_thy thmid2);
223 (*WN120201 weakened*)
224 fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _)) = thmid1 = thmid2;
225 (*version typed weaker WN100910*)
226 fun eq_thmI' ((thmid1, _), (thmid2, _)) =
227 (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2);
229 val string_of_thm = Thm.get_name_hint; (*FIXME.2009*)
230 fun thm'_of_thm thm =
231 ((thmID_of_derivation_name o Thm.get_name_hint) thm, ""): thm'
233 (*check for [.] as caused by "fun assoc_thm'"*)
234 fun string_of_thmI thm =
235 let val ct' = (de_quote o string_of_thm) thm
236 val (a, b) = split_nlast (5, Symbol.explode ct')
238 [" ", " ","[", ".", "]"] => implode a
242 (*.id requested for all, Rls,Seq,Rrls.*)
243 fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs!*)
244 | id_rls (Rls {id,...}) = id
245 | id_rls (Seq {id,...}) = id
246 | id_rls (Rrls {id,...}) = id;
247 val rls2str = id_rls;
248 fun id_rule (Thm (id, _)) = id
249 | id_rule (Calc (id, _)) = id
250 | id_rule (Rls_ rls) = id_rls rls;
252 fun get_rules (Rls {rules,...}) = rules
253 | get_rules (Seq {rules,...}) = rules
254 | get_rules (Rrls _) = [];
256 fun rule2str Erule = "Erule"
257 | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thmI thm)^")"
258 | rule2str (Calc (str,f)) = "Calc (\""^str^"\",fn)"
259 | rule2str (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
260 | rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
261 fun rule2str' Erule = "Erule"
262 | rule2str' (Thm (str, thm)) = "Thm (\""^str^"\",\"\")"
263 | rule2str' (Calc (str,f)) = "Calc (\""^str^"\",fn)"
264 | rule2str' (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
265 | rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
267 (*WN080102 compare eq_rule ?!?*)
268 fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2
269 | eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2
270 | eqrule (Cal1 (id1,_), Cal1 (id2,_)) = id1 = id2
271 | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*)
274 type rrlsstate = (* state for reverse rewriting, comments see type rule and scr | Rfuns *)
275 (term * term * rule list list * (rule * (term * term list)) list);
277 val e_type = Type("empty",[]);
278 val a_type = TFree("'a",[]);
279 val e_term = Const("empty",e_type);
280 val a_term = Free("empty",a_type);
281 val e_rrlsstate = (e_term,e_term,[[e_rule]],[(e_rule,(e_term,[]))]):rrlsstate;
283 val e_term = Const("empty", Type("'a", []));
284 val e_scr = Prog e_term;
287 there are two kinds of theorems ...
288 (1) known by isabelle
289 (2) not known, eg. calc_thm, instantiated rls
290 the latter have a thmid "#..."
291 and thus outside isa we ALWAYS transport both (thmid,string_of_thmI)
292 and have a special assoc_thm / assoc_rls in this interface *)
293 type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)
294 type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*)
295 type thyID = string; (*WN.3.11.03 TODO: replace domID with thyID*)
297 fun string_of_thy thy = Context.theory_name thy: theory';
298 val theory2domID = string_of_thy;
299 val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
300 val theory2theory' = string_of_thy;
301 val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)
302 val theory2str' = implode o (drop_last_n 4) o Symbol.explode o string_of_thy;
303 (* fun theory'2theory = fun thyID2thy ... see fun assoc_thy (...Thy_Info.get_theory string);
304 al it = "Isac" : string
307 fun thyID2theory' (thyID:thyID) = thyID;
309 let val ss = Symbol.explode thyID
310 val ext = implode (takelast (4, ss))
311 in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*)
315 (* thyID2theory' "Isac" (*ok*);
316 val it = "Isac" : theory'
317 > thyID2theory' "Isac" (*abuse, goes ok...*);
318 val it = "Isac" : theory'
321 fun theory'2thyID (theory':theory') = theory';
323 let val ss = Symbol.explode theory'
324 val ext = implode (takelast (4, ss))
325 in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID
326 else theory' (*disarm abuse of theory'*)
329 (* theory'2thyID "Isac";
330 val it = "Isac" : thyID
331 > theory'2thyID "Isac";
332 val it = "Isac" : thyID*)
335 (*. WN0509 discussion:
336 #############################################################################
337 # How to manage theorys in subproblems wrt. the requirement, #
338 # that scripts should be re-usable ? #
339 #############################################################################
341 eg. 'Script Solve_rat_equation' calls 'SubProblem (RatEq',..'
342 which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script
343 because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b
344 is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard
347 Preliminary solution:
348 # the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically,
349 # instead the 'maxthy (rootthy pt) thy' is taken for each subpbl
350 # however, a thy specified by the user in the rootpbl may lead to
351 errors in far-off subpbls (which are not yet reported properly !!!)
352 and interactively specifiying thys in subpbl is not very relevant.
354 Other solutions possible:
355 # always parse and type-check with Thy_Info.get_theory "Isac"
356 (rejected tue to the vague idea eg. to re-use equations for R in C etc.)
357 # regard the subthy-relation in specifying thys of subpbls
358 # specifically handle 'SubProblem (undefined, pbl, arglist)'
361 (*WN0509 TODO "ProtoPure" ... would be more consistent
362 with assoc_thy <--> theory2theory' +FIXME assoc_thy "e_domID" -> Script.thy*)
363 val e_domID = "e_domID":domID;
365 (*the key into the hierarchy ob theory elements*)
366 type theID = string list;
367 val e_theID = ["e_theID"];
368 val theID2str = strs2str;
369 (*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
370 fun theID2thyID (theID:theID) =
371 if length theID >= 3 then (last_elem o (drop_last_n 2)) theID : thyID
372 else error ("theID2thyID called with "^ theID2str theID);
374 (*the key into the hierarchy ob problems*)
375 type pblID = string list; (* domID::...*)
376 val e_pblID = ["e_pblID"]:pblID;
377 val pblID2str = strs2str;
379 (*the key into the hierarchy ob methods*)
380 type metID = string list;
381 val e_metID = ["e_metID"]:metID;
382 val metID2str = strs2str;
385 domID * (*WN.12.03: is replaced by thy from get_met ?FIXME? in:
386 specify (Init_Proof..), nxt_specify_init_calc,
387 assod (.SubProblem...), stac2tac (.SubProblem...)*)
391 fun spec2str ((dom,pbl,met)(*:spec*)) =
392 "(" ^ (quote dom) ^ ", " ^ (strs2str pbl) ^
393 ", " ^ (strs2str met) ^ ")";
394 (*> spec2str empty_spec;
395 val it = "(\"\", [], (\"\", \"\"))" : string *)
396 val empty_spec = (e_domID,e_pblID,e_metID):spec;
397 val e_spec = empty_spec;
399 (*.association list with cas-commands, for generating a complete calc-head.*)
401 (term list -> (* the arguments of the cas-command, eg. (x+1=2, x) *)
402 (term * (* description of an element *)
403 term list) (* value of the element (always put into a list) *)
404 list) (* of elements in the formalization *)
406 (term * (* cas-command, eg. 'solve' *)
407 (spec * (* theory, problem, method *)
409 fun cas_eq ((t1, (_, _)) : cas_elem, (t2, (_, _)) : cas_elem) = t1 = t2
411 (*either theID or pblID or metID*)
412 type kestoreID = string list;
413 val e_kestoreID = ["e_kestoreID"];
414 val kestoreID2str = strs2str;
416 (*for distinction of contexts WN130621: disambiguate with Isabelle's Context !*)
417 datatype ketype = Exp_ | Thy_ | Pbl_ | Met_;
418 fun ketype2str Exp_ = "Exp_"
419 | ketype2str Thy_ = "Thy_"
420 | ketype2str Pbl_ = "Pbl_"
421 | ketype2str Met_ = "Met_";
422 fun ketype2str' Exp_ = "Example"
423 | ketype2str' Thy_ = "Theory"
424 | ketype2str' Pbl_ = "Problem"
425 | ketype2str' Met_ = "Method";
427 (*see 'How to manage theorys in subproblems' at 'type thyID'*)
428 val theory' = Unsynchronized.ref ([]:(theory' * theory) list);
430 (*rewrite orders, also stored in 'type met' and type 'and rls'
431 The association list is required for 'rewrite.."rew_ord"..'
432 WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*)
433 val rew_ord' = Unsynchronized.ref
434 ([]:(rew_ord' * (*the key for the association list *)
435 (subst (*the bound variables - they get high order*)
436 -> (term * term) (*(t1, t2) to be compared *)
437 -> bool)) (*if t1 <= t2 then true else false *)
438 list); (*association list *)
440 rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord),
441 ("dummy_ord", dummy_ord)]);
444 (* A tree for storing data defined in different theories
445 for access from the Interpreter and from dialogue authoring
446 using a string list as key.
447 'a is for pbt | met | thydata; after WN030424 naming became inappropriate *)
449 Ptyp of string * (* element of the key *)
450 'a list * (* several pbts with different domIDs/thy TODO: select by subthy (isaref.p.69)
451 presently only _ONE_ elem FOR ALL KINDS OF CONTENT pbt | met | thydata *)
452 ('a ptyp) list;(* the children nodes *)
454 (*.datatype for collecting thydata for hierarchy.*)
455 (*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
456 (*WN0606 Htxt contains html which does not belong to the sml-kernel*)
457 datatype thydata = Html of {guh: guh,
458 coursedesign: authors,
459 mathauthors: authors,
460 html: string} (*html; for demos before database*)
462 coursedesign: authors,
463 mathauthors: authors,
464 fillpats: fillpat list,
467 coursedesign: authors,
468 mathauthors: authors,
469 thy_rls: (thyID * rls)}
471 coursedesign: authors,
472 mathauthors: authors,
475 coursedesign: authors,
476 mathauthors: authors,
477 ord: (subst -> (term * term) -> bool)};
478 val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""};
479 fun the2str (Html {guh, coursedesign, mathauthors, html}) = guh : string
480 | the2str (Hthm {guh, coursedesign, mathauthors, fillpats, thm}) = guh
481 | the2str (Hrls {guh, coursedesign, mathauthors, thy_rls}) = guh
482 | the2str (Hcal {guh, coursedesign, mathauthors, calc}) = guh
483 | the2str (Hord {guh, coursedesign, mathauthors, ord}) = guh
484 fun thes2str thes = map the2str thes |> list2str;
486 type thehier = (thydata ptyp) list;
487 (* required to determine sequence of main nodes of thehier in KEStore.thy *)
488 fun part2guh ([str]:theID) =
490 "Isabelle" => "thy_isab_" ^ str ^ "-part" : guh
491 | "IsacScripts" => "thy_scri_" ^ str ^ "-part"
492 | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"
493 | str => error ("thy2guh: called with '"^str^"'"))
494 | part2guh theID = error ("part2guh called with theID = " ^ theID2str theID);
496 fun thy2guh ([part, thyID] : theID) = (case part of
497 "Isabelle" => "thy_isab_" ^ thyID : guh
498 | "IsacScripts" => "thy_scri_" ^ thyID
499 | "IsacKnowledge" => "thy_isac_" ^ thyID
500 | str => error ("thy2guh: called with '" ^ str ^ "'"))
501 | thy2guh theID = error ("thy2guh called with '" ^ strs2str' theID ^ "'");
503 fun thypart2guh ([part, thyID, thypart] : theID) = case part of
504 "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : guh
505 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
506 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
507 | str => error ("thypart2guh: called with '" ^ str ^ "'");
509 (* convert the data got via contextToThy to a globally unique handle
510 there is another way to get the guh out of the 'theID' in the hierarchy *)
511 fun thm2guh (isa, thyID:thyID) (thmID:thmID) = case isa of
512 "Isabelle" => "thy_isab_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID : guh
513 | "IsacKnowledge" => "thy_isac_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
514 | "IsacScripts" => "thy_scri_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
515 | str => error ("thm2guh called with isa = '" ^ isa ^ "' for thm = " ^ thmID ^ "'");
517 fun rls2guh (isa, thyID:thyID) (rls':rls') = case isa of
518 "Isabelle" => "thy_isab_" ^ theory'2thyID thyID ^ "-rls-" ^ rls' : guh
519 | "IsacKnowledge" => "thy_isac_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'
520 | "IsacScripts" => "thy_scri_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'
521 | str => error ("rls2guh called with isa = '" ^ isa ^ "' for rls = '" ^ rls' ^ "'");
523 fun cal2guh (isa, thyID:thyID) calID = case isa of
524 "Isabelle" => "thy_isab_" ^ theory'2thyID thyID ^ "-cal-" ^ calID : guh
525 | "IsacKnowledge" => "thy_isac_" ^ theory'2thyID thyID ^ "-cal-" ^ calID
526 | "IsacScripts" => "thy_scri_" ^ theory'2thyID thyID ^ "-cal-" ^ calID
527 | str => error ("cal2guh called with isa = '" ^ isa ^ "' for cal = '" ^ calID ^ "'");
529 fun ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') = case isa of
530 "Isabelle" => "thy_isab_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord' : guh
531 | "IsacKnowledge" => "thy_isac_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'
532 | "IsacScripts" => "thy_scri_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'
533 | str => error ("ord2guh called with isa = '" ^ isa ^ "' for ord = '" ^ rew_ord' ^ "'");
535 (* not only for thydata, but also for thy's etc *)
536 fun theID2guh (theID : theID) = case length theID of
537 0 => error ("theID2guh: called with theID = " ^ strs2str' theID)
538 | 1 => part2guh theID
540 | 3 => thypart2guh theID
542 let val [isa, thyID, typ, elemID] = theID
544 "Theorems" => thm2guh (isa, thyID) elemID
545 | "Rulesets" => rls2guh (isa, thyID) elemID
546 | "Calculations" => cal2guh (isa, thyID) elemID
547 | "Orders" => ord2guh (isa, thyID) elemID
548 | "Theorems" => thy2guh [isa, thyID]
549 | str => error ("theID2guh: called with theID = " ^ strs2str' theID)
551 | n => error ("theID2guh called with theID = " ^ strs2str' theID);
553 (* an association list, gets the value once in Isac.ML.
554 stores Isabelle's thms as terms for compatibility with Theory.axioms_of.
555 WN1-1-28 make this data arguments and del ref ?*)
556 val isab_thm_thy = Unsynchronized.ref ([] : (thmDeriv * term) list);
557 val isabthys = Unsynchronized.ref ([] : theory list);
561 type filename = string;
563 (*val xxx = fn: a b => (a,b); ??? fun-definition ???*)
565 fun ii (_:term) = e_rrlsstate;
566 fun no (_:term) = SOME (e_term,[e_term]);
567 fun lo (_:rule list list) (_:term) (_:rule) = [(e_rule,(e_term,[e_term]))];
568 fun ne (_:rule list list) (_:term) = SOME e_rule;
569 fun fo (_:rule list list) (_:term) (_:term) = [(e_rule,(e_term,[e_term]))];
571 val e_rfuns = Rfuns {init_state=ii,normal_form=no,locate_rule=lo,
572 next_rule=ne,attach_form=fo};
576 Rls {id = "e_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Erls,
577 srls = Erls, calc = [], rules = [], errpatts = [], scr = EmptyScr}: rls;
579 Rrls {id = "e_rrls", prepat = [], rew_ord = ("dummy_ord", dummy_ord), erls = Erls,
580 calc = [], errpatts = [], scr=e_rfuns}:rls;
582 fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,errpatts,rules,scr}) =
583 {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
584 (*asm_thm=asm_thm,*)rules=rules,scr=scr}
585 | rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,errpatts,rules,scr}) =
586 {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
587 (*asm_thm=asm_thm,*)rules=rules,scr=scr}
588 | rep_rls Erls = rep_rls e_rls
589 | rep_rls (Rrls {id,...}) = rep_rls e_rls
590 (*error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*);
591 (*| rep_rls (Seq {id,...}) =
592 error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id);
594 fun rep_rrls (Rrls {id, calc, erls, prepat, rew_ord, errpatts,
595 scr = Rfuns {attach_form, init_state, locate_rule, next_rule, normal_form}}) =
596 {id=id, calc=calc, erls=erls, prepat=prepat,
597 rew_ord=rew_ord, errpatts=errpatts, attach_form=attach_form, init_state=init_state,
598 locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form}
599 | rep_rrls (Rls {id,...}) =
600 error ("rep_rrls doesn't take apart (normal) rule-sets: "^id)
601 | rep_rrls (Seq {id,...}) =
602 error ("rep_rrls doesn't take apart (normal) rule-sets: "^id);
604 fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
605 rules =rs, errpatts=errpatts, scr=sc}) r =
606 (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
607 rules = rs @ r, errpatts=errpatts, scr=sc}:rls)
608 | append_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
609 rules =rs, errpatts=errpatts, scr=sc}) r =
610 (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
611 rules = rs @ r, errpatts=errpatts, scr=sc}:rls)
612 | append_rls id (Rrls _) _ =
613 error ("append_rls: not for reverse-rewrite-rule-set "^id);
615 (*. are _atomic_ rules equal ?.*)
616 (*WN080102 compare eqrule ?!?*)
617 fun eq_rule (Thm (thm1,_), Thm (thm2,_)) = thm1 = thm2
618 | eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2
619 | eq_rule (Rls_ rls1, Rls_ rls2) = id_rls rls1 = id_rls rls2
620 (*id_rls checks for Rls, Seq, Rrls*)
623 fun merge_ids rls1 rls2 =
625 val id1 = (#id o rep_rls) rls1
626 val id2 = (#id o rep_rls) rls2
628 if id1 = id2 then id1
629 else "merged_" ^ id1 ^ "_" ^ id2
631 fun merge_rls _ Erls rls = rls
632 | merge_rls _ rls Erls = rls
633 | merge_rls _ (Rrls x) _ = Rrls x (* required for merging Theory_Data *)
634 | merge_rls _ _ (Rrls x) = Rrls x
636 (Rls {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
637 rules = rs1, errpatts = eps1, scr = sc1, ...})
638 (Rls {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
639 rules = rs2, errpatts = eps2, ...})
641 (Rls {id = id, rew_ord = ro1, scr = sc1,
642 preconds = union (op =) pc1 pc2,
643 erls = merge_rls (merge_ids er1 er2) er1 er2,
644 srls = merge_rls (merge_ids sr1 sr2) sr1 sr2,
645 calc = union calc_eq ca1 ca2,
646 rules = union eq_rule rs1 rs2,
647 errpatts = union (op =) eps1 eps2} : rls)
649 (Seq {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
650 rules = rs1, errpatts = eps1, scr = sc1, ...})
651 (Seq {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
652 rules = rs2, errpatts = eps2, ...})
654 (Seq {id = id, rew_ord = ro1, scr = sc1,
655 preconds = union (op =) pc1 pc2,
656 erls = merge_rls (merge_ids er1 er2) er1 er2,
657 srls = merge_rls (merge_ids sr1 sr2) sr1 sr2,
658 calc = union calc_eq ca1 ca2,
659 rules = union eq_rule rs1 rs2,
660 errpatts = union (op =) eps1 eps2} : rls)
661 | merge_rls id _ _ = error ("merge_rls: \"" ^ id ^
662 "\"; not for reverse-rewrite-rule-sets and not for mixed Rls -- Seq");
664 fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
665 rules=rs, errpatts=eps, scr=sc}) r =
666 (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
667 rules = gen_rems eq_rule (rs, r),
668 errpatts = eps(*gen_rems op= (eps, TODO)*),
670 | remove_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
671 rules =rs, errpatts=eps, scr=sc}) r =
672 (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
673 rules = gen_rems eq_rule (rs, r),
674 errpatts = eps(*gen_rems op= (eps, TODO)*),
676 | remove_rls id (Rrls _) _ = error
677 ("remove_rls: not for reverse-rewrite-rule-set "^id);
679 (* datastructure for KEStore_Elems, intermediate for thehier *)
681 (rls' * (* identifier unique within Isac *)
682 (theory' * (* just for assignment in thehier, not appropriate for parsing etc *)
683 rls)) (* ((#id o rep_rls) rls) = rls' by coding discipline *)
684 fun rls_eq ((id1, (_, _)), (id2, (_, _))) = id1 = id2
686 fun insert_merge_rls (re as (id, (thyID, r1)) : rlss_elem) ys =
687 case get_index (fn y => if curry rls_eq re y then SOME y else NONE) ys of
689 | SOME (i, (_, (_, r2))) =>
691 val r12 = merge_rls id r1 r2
692 in list_update ys i (id, (thyID, r12)) end
694 fun merge_rlss (s1, s2) = fold insert_merge_rls s1 s2;
697 fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules)
698 | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules)
699 | memrls r _ = error ("memrls: incomplete impl. r= "^(rule2str r));
701 fun assoc' ([], key) = error ("ME_Isa: '"^key^"' not known")
702 | assoc' ((keyi, xi) :: pairs, key) =
703 if key = keyi then SOME xi else assoc' (pairs, key);
705 (*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
706 handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*)
707 fun assoc_thy (thy:theory') =
708 if thy = "e_domID" then (Thy_Info.get_theory "Script") (*lower bound of Knowledge*)
709 else (Thy_Info.get_theory thy)
710 handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system");
712 (*.overwrite an element in an association list and pair it with a thyID
713 in order to create the thy_hierarchy;
714 overwrites existing rls' even if they are defined in a different thy;
715 this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc;.*)
716 (*WN060120 ...these are NOT compatible to "fun assoc_thm'" in that
717 they do NOT handle overlays by re-using an identifier in different thys;
718 "thyID.rlsID" would be a good solution, if the "." would be possible
720 actually a hack to get alltogether run again with minimal effort*)
721 fun insthy thy' (rls', rls) = (rls', (thy', rls));
722 fun overwritelthy thy (al, bl:(rls' * rls) list) =
723 let val bl' = map (insthy ((get_thy o theory2theory') thy)) bl
724 in overwritel (al, bl') end;
726 fun assoc_rew_ord ro = ((the o assoc') (!rew_ord',ro))
727 handle _ => error ("ME_Isa: rew_ord '"^ro^"' not in system");
728 (*get the string for stac from rule*)
730 fun term_to_string' ctxt t =
732 val ctxt' = Config.put show_markup false ctxt
733 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
734 fun term_to_string'' (thyID : thyID) t =
736 val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info.get_theory thyID))
737 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
738 fun term_to_string''' thy t =
740 val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
741 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
743 fun term2str t = term_to_string' (assoc_thy "Isac" |> thy2ctxt) t;
744 fun terms2strs ts = map term2str ts;
745 (*terms2strs [t1,t2] = ["1 + 2", "abc"];*)
746 val terms2str = strs2str o terms2strs;
747 (*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*)
748 val terms2str' = strs2str' o terms2strs;
749 (*terms2str' [t1,t2] = "[1 + 2,abc]";*)
751 fun termopt2str (SOME t) = "(SOME " ^ term2str t ^ ")"
752 | termopt2str NONE = "NONE";
754 fun type_to_string' ctxt t =
756 val ctxt' = Config.put show_markup false ctxt
757 in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
758 fun type_to_string'' (thyID : thyID) t =
760 val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info.get_theory thyID))
761 in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
762 fun type_to_string''' thy t =
764 val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
765 in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
767 fun type2str typ = type_to_string'' "Isac" typ; (*legacy*)
768 val string_of_typ = type2str; (*legacy*)
769 fun string_of_typ_thy thy typ = type_to_string'' thy typ; (*legacy*)
771 fun subst2str (s:subst) =
773 (map (linefeed o pair2str o
775 (apfst term2str)))) s;
776 fun subst2str' (s:subst) =
780 (apfst term2str)))) s;
781 (*> subst2str' [(str2term "bdv", str2term "x"),
782 (str2term "bdv_2", str2term "y")];
783 val it = "[(bdv, x)]" : string
785 val env2str = subst2str;
789 fun scr2str (Prog s) = "Prog " ^ term2str s
790 | scr2str (Rfuns _) = "Rfuns";
793 fun maxthy thy1 thy2 = if Theory.subthy (thy1, thy2) then thy2 else thy1;
796 (*.trace internal steps of isac's rewriter*)
797 val trace_rewrite = Unsynchronized.ref false;
798 (*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*)
799 val depth = Unsynchronized.ref 99999;
800 (*.no of rewrites exceeding this int -> NO rewrite.*)
801 (*WN060829 still unused...*)
802 val lim_rewrite = Unsynchronized.ref 99999;
803 (*.no of derivation-elements exceeding this int -> SOME derivation-elements.*)
804 val lim_deriv = Unsynchronized.ref 100;
805 (*.switch for checking guhs unique before storing a pbl or met;
806 set true at startup (done at begin of ROOT.ML)
807 set false for editing IsacKnowledge (done at end of ROOT.ML).*)
808 val check_guhs_unique = Unsynchronized.ref true;
811 datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)
813 | R (*go right at $*)
814 | D; (*go down at Abs*)
815 type loc_ = lrd list;
819 fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k;
822 (* the pattern for an item of a problems model or a methods guard *)
824 (string * (* field *)
825 (term * (* description *)
826 term)) (* id | arbitrary term *);
827 fun pat2str ((field, (dsc, id)) : pat) =
828 pair2str (field, pair2str (term2str dsc, term2str id))
829 fun pats2str pats = (strs2str o (map pat2str)) pats
831 (* types for problems models (TODO rename to specification models) *)
833 (string * (* field "#Given",..*)(*deprecated due to 'type pat'*)
834 (term * (* description *)
835 term)); (* id | struct-var *)
836 val e_pbt_ = ("#Undef", (e_term, e_term)) : pbt_
838 {guh : guh, (* unique within this isac-knowledge *)
839 mathauthors : string list, (* copyright *)
840 init : pblID, (* to start refinement with *)
841 thy : theory, (* which allows to compile that pbt
842 TODO: search generalized for subthy (ref.p.69*)
843 (*^^^ WN050912 NOT used during application of the problem,
844 because applied terms may be from 'subthy' as well as from super;
845 thus we take 'maxthy'; see match_ags !*)
846 cas : term option, (* 'CAS-command'*)
847 prls : rls, (* for preds in where_*)
848 where_ : term list, (* where - predicates*)
849 ppc : pat list, (* this is the model-pattern;
850 it contains "#Given","#Where","#Find","#Relate"-patterns
851 for constraints on identifiers see "fun cpy_nam" *)
852 met : metID list} (* methods solving the pbt*)
854 val e_pbt = {guh = "pbl_empty", mathauthors = [], init = e_pblID, thy = Thy_Info.get_theory "Pure",
855 cas = NONE, prls = Erls, where_ = [], ppc = [], met = []} : pbt
857 ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc',
858 prls = prls', thy = thy', where_ = w'} : pbt) =
859 "{cas = " ^ (termopt2str cas') ^ ", guh = \"" ^ guh' ^ "\", init = "
860 ^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", met = "
861 ^ (strslist2strs met') ^ ", ppc = " ^ pats2str ppc' ^ ", prls = "
862 ^ (rls2str prls' |> quote) ^ ", thy = {" ^ (theory2str thy') ^ "}, where_ = "
863 ^ (terms2str w') ^ "}" |> linefeed;
864 fun pbts2str pbts = map pbt2str pbts |> list2str;
866 val e_Ptyp = Ptyp ("e_pblID",[e_pbt],[])
867 type ptyps = (pbt ptyp) list
869 fun coll_pblguhs pbls =
870 let fun node coll (Ptyp (_,[n],ns)) =
871 [(#guh : pbt -> guh) n] @ (nodes coll ns)
872 and nodes coll [] = coll
873 | nodes coll (n::ns) = (node coll n) @ (nodes coll ns);
874 in nodes [] pbls end;
875 fun check_pblguh_unique (guh:guh) (pbls: (pbt ptyp) list) =
876 if member op = (coll_pblguhs pbls) guh
877 then error ("check_guh_unique failed with '"^guh^"';\n"^
878 "use 'sort_pblguhs()' for a list of guhs;\n"^
879 "consider setting 'check_guhs_unique := false'")
882 fun insrt _ pbt [k] [] = [Ptyp (k, [pbt],[])]
883 | insrt d pbt [k] ((Ptyp (k', [p], ps))::pys) =
884 ((*tracing("### insert 1: ks = "^(strs2str [k])^" k'= "^k');*)
886 then ((Ptyp (k', [pbt], ps))::pys)
887 else (*ev.newly added pbt is free _only_ with 'last_elem pblID'*)
888 ((Ptyp (k', [p], ps))::(insrt d pbt [k] pys))
890 | insrt d pbt (k::ks) ((Ptyp (k', [p], ps))::pys) =
891 ((*tracing("### insert 2: ks = "^(strs2str (k::ks))^" k'= "^k');*)
893 then ((Ptyp (k', [p], insrt d pbt ks ps))::pys)
896 then error ("insert: not found "^(strs2str (d:pblID)))
897 else ((Ptyp (k', [p], ps))::(insrt d pbt (k::ks) pys))
900 fun update_ptyps ID _ _ [] =
901 error ("update_ptyps: " ^ strs2str' ID ^ " does not exist")
902 | update_ptyps ID [i] data ((py as Ptyp (key, _, pys)) :: pyss) =
906 then ((Ptyp (key, [data], [])) :: pyss)
907 else error ("update_ptyps: " ^ strs2str' ID ^ " has descendants")
908 else py :: update_ptyps ID [i] data pyss
909 | update_ptyps ID (i :: is) data ((py as Ptyp (key, d, pys)) :: pyss) =
911 then ((Ptyp (key, d, update_ptyps ID is data pys)) :: pyss)
912 else (py :: (update_ptyps ID (i :: is) data pyss))
914 (* this function only works wrt. the way Isabelle evaluates Theories and is not a general merge
915 function for trees / ptyps *)
916 fun merge_ptyps ([], pt) = pt
917 | merge_ptyps (pt, []) = pt
918 | merge_ptyps ((x' as Ptyp (k, x, ps)) :: xs, (xs' as Ptyp (k', y, ps') :: ys)) =
920 then Ptyp (k, y, merge_ptyps (ps, ps')) :: merge_ptyps (xs, ys)
921 else x' :: merge_ptyps (xs, xs');
922 fun merge_ptyps' pt1 pt2 = merge_ptyps (pt1, pt2)
924 (* data for methods stored in 'methods'-database*)
926 {guh : guh, (*unique within this isac-knowledge *)
927 mathauthors: string list,(*copyright *)
928 init : pblID, (*WN060721 introduced mistakenly--TODO.REMOVE!*)
929 rew_ord' : rew_ord', (*for rules in Detail
930 TODO.WN0509 store fun itself, see 'type pbt'*)
931 erls : rls, (*the eval_rls for cond. in rules FIXME "rls'
932 instead erls in "fun prep_met" *)
933 srls : rls, (*for evaluating list expressions in scr *)
934 prls : rls, (*for evaluating predicates in modelpattern *)
935 crls : rls, (*for check_elementwise, ie. formulae in calc.*)
936 nrls : rls, (*canonical simplifier specific for this met *)
937 errpats : errpat list,(*error patterns expected in this method *)
938 calc : calc list, (*Theory_Data in fun prep_met *)
939 (*branch : TransitiveB set in append_problem at generation ob pblobj
940 FIXXXME.0308: set branch from met in Apply_Method ? *)
941 ppc : pat list, (*.items in given, find, relate;
942 items (in "#Find") which need not occur in the arg-list of a SubProblem
943 are 'copy-named' with an identifier "*'.'".
944 copy-named items are 'generating' if they are NOT "*'''" ?WN120516??
945 see ME/calchead.sml 'fun is_copy_named'. *)
946 pre : term list, (*preconditions in where *)
947 scr : scr (*prep_met gets progam or string "empty_script"*)
949 val e_met = {guh="met_empty",mathauthors=[],init=e_metID,
950 rew_ord' = "e_rew_ord'": rew_ord',
951 erls = e_rls, srls = e_rls, prls = e_rls,
952 calc = [], crls = e_rls, errpats = [], nrls= e_rls,
953 ppc = []: (string * (term * term)) list,
955 scr = EmptyScr: scr}:met;
958 val e_Mets = Ptyp ("e_metID",[e_met],[]);
960 type mets = (met ptyp) list;
962 fun coll_metguhs mets =
963 let fun node coll (Ptyp (_,[n],ns)) =
964 [(#guh : met -> guh) n] @ (nodes coll ns)
965 and nodes coll [] = coll
966 | nodes coll (n::ns) = (node coll n) @ (nodes coll ns);
967 in nodes [] mets end;
969 (* val (guh, mets) = ("met_test", !mets);
971 fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) =
972 if member op = (coll_metguhs mets) guh
973 then error ("check_guh_unique failed with '"^guh^"';\n"^
974 "use 'sort_metguhs()' for a list of guhs;\n"^
975 "consider setting 'check_guhs_unique := false'")
978 (* for preserving elements created by 'fun store_thy' *)
979 fun exist_the (theID : theID) (thy_hie : thehier) =
981 fun node theID ids (Ptyp (id, _, ns)) =
982 if theID = ids @ [id] then true else nodes theID (ids @ [id]) ns
983 and nodes _ _ [] = false
984 | nodes theID ids (n::ns) =
985 if node theID ids n then true else nodes theID ids ns
986 in nodes theID [] thy_hie end;
988 (* insrt requires a parent; see 'fun fill_parents' *)
989 fun can_insert (theID : theID) (thy_hie : thehier) =
990 (insrt theID e_thydata theID thy_hie; true)
993 (* cut 'theID', the ID of theory elements from tail to head
994 until insertion into the hierarchy of theory elements 'th' is possible
995 (the hierarchy requires the parentnode to exist for insertion) *)
996 fun cut_theID th ([] : theID) = error "could not insert into thy-hierarchy"
997 | cut_theID th theID =
998 if can_insert theID th
999 then theID else cut_theID th (drop_last theID);
1001 (* insert empty parents 'Html' into the hierarchy of theory elements 'th'
1002 until the actual node can be inserted with key 'theID' *)
1003 fun fill_parents th cutID theID =
1004 let val cutID' = cut_theID th cutID
1005 in if cutID' = theID
1009 val th' = insrt cutID' (Html {guh=theID2guh theID, coursedesign = ["isac team 2006"],
1010 mathauthors = [], html = ""}) cutID' th
1011 val cutID_ = cutID' @ [nth ((length cutID') + 1) theID]
1012 in fill_parents th' cutID_ theID end
1015 (* argument 1 "th : thehier": contains some thydata from "setup {* KEStore_Elems.add_thes ..."
1016 argument 1 "th : thehier": contains some thydata from "store_thes ..."
1017 already in some "ProgLang/*.thy" or "Knowledge/*.thy"
1018 argument 2 "(theID, thydata)::_ : (theID * thydata) list: contains thydata collected
1019 automatically in Build_Thydata.thy finally.
1020 parents of thydata in list, missing in thehier, are inserted
1021 (causing msgs '*** insert: not found');
1022 (1) is kept in case (2) contains same theID (causing msgs '*** insert: preserved ') *)
1023 fun (*KEStore_Elems.*)add_thes th thes = (* for tests bypassing setup KEStore_Elems *)
1025 fun add_the th ((thydata, theID)) =
1026 if can_insert theID th
1028 if exist_the theID th
1029 then (writeln ("*** insert: preserved " ^ strs2str theID); (fn x => x))
1030 else insrt theID thydata theID
1033 val th' = fill_parents th theID theID (*..*** insert: not found*)
1034 val th' = insrt theID thydata theID th'
1035 in merge_ptyps' th' end;
1036 in fold (add_the th) thes end
1038 fun Html_default exist = (Html {guh = theID2guh exist,
1039 coursedesign = ["isac team 2006"], mathauthors = [], html = ""})
1041 fun fill_parents (exist, [i]) thydata = Ptyp (i, [thydata], [])
1042 | fill_parents (exist, i :: is) thydata =
1043 Ptyp (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])
1044 | fill_parents _ _ = error "Html_default: avoid ML warning: Matches are not exhaustive"
1046 fun add_thydata (exist, is) thydata [] = [fill_parents (exist, is) thydata]
1047 | add_thydata (exist, [i]) data (pys as (py as Ptyp (key, _, _)) :: pyss) =
1049 then pys (* preserve existing thydata *)
1050 else py :: add_thydata (exist, [i]) data pyss
1051 | add_thydata (exist, iss as (i :: is)) data ((py as Ptyp (key, d, pys)) :: pyss) =
1055 then Ptyp (key, d, [fill_parents (exist @ [i], is) data]) :: pyss
1056 else Ptyp (key, d, add_thydata (exist @ [i], is) data pys) :: pyss
1057 else py :: add_thydata (exist, iss) data pyss
1058 | add_thydata _ _ _ = error "add_thydata: avoid ML warning: Matches are not exhaustive"
1060 fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' =
1061 Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
1062 fillpats = fillpats', thm = thm}
1063 | update_hthm _ _ = raise ERROR "wrong data";
1065 (* for interface for dialog-authoring *)
1066 fun update_hrls (Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =
1070 Rls {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...} =>
1071 Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
1072 calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
1073 | Seq {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...} =>
1074 Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
1075 calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
1076 | Rrls {id, prepat, rew_ord, erls, calc, scr, ...} =>
1077 Rrls {id = id, prepat = prepat, rew_ord = rew_ord, erls = erls, calc = calc,
1078 scr = scr, errpatts = errpatIDs}
1081 Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
1082 thy_rls = (thyID, rls')}
1084 | update_hrls _ _ = raise ERROR "wrong data";
1086 fun app_py p f (d:pblID) (k(*:pblRD*)) = let
1088 error ("app_py: not found: " ^ (strs2str d));
1089 fun app_py' _ [] = py_err ()
1090 | app_py' [] _ = py_err ()
1091 | app_py' [k0] ((p' as Ptyp (k', _, _ ))::ps) =
1092 if k0 = k' then f p' else app_py' [k0] ps
1093 | app_py' (k' as (k0::ks)) (Ptyp (k'', _, ps)::ps') =
1094 if k0 = k'' then app_py' ks ps else app_py' k' ps';
1098 fun extract_py (Ptyp (_, [py], _)) = py
1099 | extract_py _ = error ("extract_py: Ptyp has wrong format.");
1100 in app_py p extract_py end;
1103 fun (*KEStore_Elems.*)insert_fillpats th fis = (* for tests bypassing setup KEStore_Elems *)
1105 fun update_elem th (theID, fillpats) =
1107 val hthm = get_py th theID theID
1108 val hthm' = update_hthm hthm fillpats
1109 handle ERROR _ => error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
1110 in update_ptyps theID theID hthm' end
1111 in fold (update_elem th) fis end