1 (* Title: the calctree, which holds a calculation
2 Author: Walther Neuper 1999
3 (c) due to copyright terms
7 sig (* vvv--- *.sml require these typs incrementally, with these exception -----------------vvv *)
10 type fmz_ = cterm' list
11 type fmz = fmz_ * spec;
12 val e_fmz : fmz_ * spec (* for datatypes.sml *)
15 datatype istate = RrlsState of rrlsstate | ScrState of scrstate | Uistate
16 val istate2str : istate -> string
20 val sube2str : cterm' list -> string
22 val sube2subst : theory -> cterm' list -> (term * term) list
23 val sube2subte : cterm' list -> term list
24 val subs2subst : theory -> cterm' list -> (term * term) list
25 val subst2sube : (term * term) list -> cterm' list (* for datatypes.sml *)
26 val subst2subs : (term * term) list -> cterm' list
27 val subst2subs' : (term * term) list -> (string * string) list
28 val subte2sube : term list -> cterm' list
31 datatype tac_ = (* TODO.WN161219: replace *every* cterm' by term *)
32 Add_Find' of cterm' * itm list | Add_Given' of cterm' * itm list | Add_Relation' of cterm' * itm list
33 | Apply_Assumption' of term list * term
34 | Apply_Method' of metID * term option * istate * Proof.context
35 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
36 | Begin_Sequ' | Begin_Trans' of term
37 | Split_And' of term | Split_Or' of term | Split_Intersect' of term
38 | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
39 | End_Sequ' | End_Trans' of result
40 | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''
41 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
43 | Calculate' of theory' * string * term * (term * thm')
44 | Check_Postcond' of pblID * result
45 | Check_elementwise' of term * cterm' * result
46 | Del_Find' of cterm' | Del_Given' of cterm' | Del_Relation' of cterm'
49 | Detail_Set' of theory' * bool * rls * term * result
50 | Detail_Set_Inst' of theory' * bool * subst * rls * term * result
51 | End_Detail' of result
56 | Init_Proof' of cterm' list * spec
57 | Model_Problem' of pblID * itm list * itm list
58 | Or_to_List' of term * term
59 | Refine_Problem' of pblID * (itm list * (bool * term) list)
60 | Refine_Tacitly' of pblID * pblID * domID * metID * itm list
62 | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * result
63 | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * result
64 | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * result
65 | Rewrite_Set' of theory' * bool * rls * term * result
66 | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * result
68 | Specify_Method' of metID * ori list * itm list
69 | Specify_Problem' of pblID * (bool * (itm list * (bool * term) list))
70 | Specify_Theory' of domID
71 | Subproblem' of spec * ori list * term * fmz_ * Proof.context * term
72 | Substitute' of rew_ord_ * rls * subte * term * term
73 | Tac_ of theory * string * string * string
74 | Take' of term | Take_Inst' of term
76 Add_Find of cterm' | Add_Given of cterm' | Add_Relation of cterm'
77 | Apply_Assumption of cterm' list
78 | Apply_Method of metID
80 | Begin_Sequ | Begin_Trans
81 | Split_And | Split_Or | Split_Intersect
82 | Conclude_And | Conclude_Or | Collect_Trues
83 | End_Sequ | End_Trans
84 | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
88 | Check_Postcond of pblID
89 | Check_elementwise of cterm'
90 | Del_Find of cterm' | Del_Given of cterm' | Del_Relation of cterm'
94 | Detail_Set_Inst of subs * rls'
99 | Group of con * int list
101 | Init_Proof of cterm' list * spec
104 | Refine_Problem of pblID
105 | Refine_Tacitly of pblID
108 | Rewrite_Asm of thm''
109 | Rewrite_Inst of subs * thm''
110 | Rewrite_Set of rls'
111 | Rewrite_Set_Inst of subs * rls'
113 | Specify_Method of metID
114 | Specify_Problem of pblID
115 | Specify_Theory of domID
116 | Subproblem of domID * pblID
120 | Take of cterm' | Take_Inst of cterm'
121 val tac2str : tac -> string
122 val rls_of : tac -> rls' (* for solve.sml *)
123 val tac2IDstr : tac -> string
124 val is_rewset : tac -> bool (* for mathengine.sml *)
125 val is_rewtac : tac -> bool (* for interface.sml *)
128 type pos = posel list
129 val pos2str : int list -> string (* for datatypes.sml *)
130 datatype pos_ = Frm | Met | Pbl | Res | Und
131 val pos_2str : pos_ -> string
133 val pos'2str : pos' -> string
134 val str2pos_ : string -> pos_ (* for datatypes.sml *)
137 (* for generate.sml ?!? ca.*)
138 datatype safe = Helpless | Safe | Sundef | Unsafe
139 val tac_2str : tac_ -> string
142 datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB
143 datatype ostate = Complete | Incomplete | Inconsistent
148 loc: (istate * Proof.context) option * (istate * Proof.context) option,
153 origin: ori list * spec * term,
158 env: (istate * Proof.context) option}
162 loc: (istate * Proof.context) option * (istate * Proof.context) option,
168 val lev_on : pos -> pos
169 val lev_dn : pos -> pos
170 val lev_dn_ : pos' -> pos'
171 val lev_up : pos -> pos
172 val lev_of : pos' -> int
173 val pos_plus : int -> pos' -> pos'
174 val lev_back' : pos' -> pos' (* for inform.sml *)
176 datatype ctree = EmptyPtree | Nd of ppobj * ctree list
177 val e_ctree : ctree (* TODO: replace by EmptyPtree*)
178 val existpt' : pos' -> ctree -> bool (* for interface.sml *)
179 val exist_lev_on' : ctree -> pos' -> bool (* for interface.sml *)
180 val is_interpos : pos' -> bool (* for interface.sml *)
181 val lev_on' : ctree -> pos' -> pos' (* for interface.sml *)
182 val lev_pred' : ctree -> pos' -> pos' (* for interface.sml *)
183 val move_up : pos -> ctree -> pos' -> pos' (* for interface.sml *)
184 val movelevel_dn : pos -> ctree -> pos' -> pos' (* for interface.sml *)
185 val movelevel_up : pos -> ctree -> pos' -> pos' (* for interface.sml *)
186 val movecalchd_up : ctree -> pos' -> pos' (* for interface.sml *)
187 val par_pblobj : ctree -> pos -> pos
188 val ins_chn : ctree list -> ctree -> pos -> ctree (* for solve.sml *)
189 val children : ctree -> ctree list (* for solve.sml *)
190 val get_nd : ctree -> pos -> ctree (* for solve.sml *)
191 val just_created_ : ppobj -> bool (* for mathengine.sml *)
192 val just_created : state -> bool (* for mathengine.sml *)
193 val is_curr_endof_calc : ctree -> pos' -> bool (* for interface.sml *)
194 val e_origin : ori list * spec * term (* for mathengine.sml *)
196 val move_dn : pos -> ctree -> pos' -> pos'
197 val is_pblobj : ppobj -> bool
198 val is_pblobj' : ctree -> pos -> bool
199 val is_pblnd : ctree -> bool
200 val last_onlev : ctree -> pos -> bool
202 val g_spec : ppobj -> spec
203 val g_loc : ppobj -> (istate * Proof.context) option * (istate * Proof.context) option
204 val g_form : ppobj -> term
205 val g_pbl : ppobj -> itm list
206 val g_met : ppobj -> itm list
207 val g_metID : ppobj -> metID
208 val g_result : ppobj -> result
209 val g_tac : ppobj -> tac
210 val g_domID : ppobj -> domID (* for appl.sml TODO: replace by thyID *)
211 val g_env : ppobj -> (istate * Proof.context) option (* for appl.sml *)
213 val g_origin : ppobj -> ori list * spec * term (* for script.sml *)
214 val get_loc : ctree -> pos' -> istate * Proof.context (* for script.sml *)
215 val get_istate : ctree -> pos' -> istate (* for script.sml *)
216 val get_ctxt : ctree -> pos' -> Proof.context
217 val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a
218 val get_curr_formula : state -> term
219 val get_assumptions_ : ctree -> pos' -> term list (* for appl.sml *)
221 val append_result : ctree -> pos -> istate * Proof.context -> result ->
222 ostate -> ctree * 'a list
223 val append_atomic : (* for solve.sml *)
224 pos -> istate * Proof.context -> term -> tac -> result -> ostate -> ctree -> ctree
225 val cappend_atomic : ctree -> pos -> istate * Proof.context -> term -> tac -> result ->
226 ostate -> ctree * pos' list
227 val cappend_form : ctree -> pos -> istate * Proof.context -> term -> ctree * pos' list
228 val cappend_problem : ctree -> pos -> istate * Proof.context -> fmz ->
229 ori list * spec * term -> ctree * pos' list
231 val update_branch : ctree -> pos -> branch -> ctree
232 val update_ctxt : ctree -> pos -> Proof.context -> ctree
233 val update_env : ctree -> pos -> (istate * Proof.context) option -> ctree
234 val update_oris : ctree -> pos -> ori list -> ctree
235 val update_orispec : ctree -> pos -> spec -> ctree
236 val update_pbl : ctree -> pos -> itm list -> ctree
237 val update_pblppc : ctree -> pos -> itm list -> ctree (* =vvv= ? *)
238 val update_pblID : ctree -> pos -> pblID -> ctree (* =^^^= ? *)
239 val update_met : ctree -> pos -> itm list -> ctree (* =vvv= ? *)
240 val update_metppc : ctree -> pos -> itm list -> ctree (* =^^^= ? *)
241 val update_metID : ctree -> pos -> metID -> ctree
242 val update_domID : ctree -> pos -> domID -> ctree
243 val update_spec : ctree -> pos -> spec -> ctree
244 val update_tac : ctree -> pos -> tac -> ctree
246 val e_ctxt : Proof.context
247 val is_e_ctxt : Proof.context -> bool (* for appl.sml *)
248 val new_val : term -> istate -> istate
249 (* for calchead.sml *)
250 type cid = cellID list
251 type ocalhd = bool * pos_ * term * itm list * (bool * term) list * spec
252 datatype ptform = Form of term | ModSpec of ocalhd
253 val get_somespec' : spec -> spec -> spec
254 exception PTREE of string;
256 val par_pbl_det : ctree -> pos -> bool * pos * rls
257 (* for rewtools.sml *)
258 val rule2tac : theory -> (term * term) list -> rule -> tac
259 val eq_tac : tac * tac -> bool
261 val rootthy : ctree -> theory
262 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
263 val update_loc' : ctree -> pos -> (istate * Proof.context) option * (istate * Proof.context) option -> ctree
264 val append_problem : int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree -> ctree
265 val g_res : ppobj -> term
266 val pr_ctree : (pos -> ppobj -> string) -> ctree -> string
267 val pr_short : pos -> ppobj -> string
268 val existpt : pos -> ctree -> bool
269 val is_empty_tac : tac -> bool
270 val e_subs : string list
271 val e_sube : cterm' list
272 val g_branch : ppobj -> branch
273 val g_ctxt : ppobj -> Proof.context
274 val g_fmz : ppobj -> fmz
275 val get_allp : pos' list -> pos * (int list * pos_) -> ctree -> pos' list
276 val get_allps : (pos * pos_) list -> posel list -> ctree list -> pos' list
277 val get_allpos' : pos * posel -> ctree -> pos' list
278 val get_allpos's : pos * posel -> ctree list -> (pos * pos_) list
279 val cut_bottom : pos * posel -> ctree -> (ctree * pos' list) * bool
280 val cut_tree : ctree -> pos * 'a -> ctree * pos' list
281 val cut_level : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
282 val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
283 val get_trace : ctree -> int list -> int list -> int list list
284 val subte2subst : term list -> (term * term) list
285 val branch2str : branch -> string
286 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
290 structure Ctree(**): CALC_TREEE(**) =
293 type result = term * term list
294 type env = (term * term) list;
297 NoBranch | AndB | OrB
298 | TransitiveB (* FIXXXME.0308: set branch from met in Apply_Method
299 FIXXXME.0402: -"- in Begin_Trans'*)
300 | SequenceB | IntersectB | CollectB | MapB;
302 fun branch2str NoBranch = "NoBranch" (* for tests only *)
303 | branch2str AndB = "AndB"
304 | branch2str OrB = "OrB"
305 | branch2str TransitiveB = "TransitiveB"
306 | branch2str SequenceB = "SequenceB"
307 | branch2str IntersectB = "IntersectB"
308 | branch2str CollectB = "CollectB"
309 | branch2str MapB = "MapB";
312 Incomplete | Complete | Inconsistent (* WN041020 latter still unused *);
313 fun ostate2str Incomplete = "Incomplete" (* for tests only *)
314 | ostate2str Complete = "Complete"
315 | ostate2str Inconsistent = "Inconsistent";
318 type cid = cellID list;
320 type posel = int; (* for readability in funs accessing Ctree *)
322 val pos2str = ints2str';
324 Pbl (* PblObj-position: problem-type *)
325 | Met (* PblObj-position: method *)
326 | Frm (* PblObj-position: -> Pbl in ME (not by moveDown !)
327 | PrfObj-position: formula *)
328 | Res (* PblObj | PrfObj-position: result *)
329 | Und; (* undefined*)
330 fun pos_2str Pbl = "Pbl"
331 | pos_2str Met = "Met"
332 | pos_2str Frm = "Frm"
333 | pos_2str Res = "Res"
334 | pos_2str Und = "Und";
335 fun str2pos_ "Pbl" = Pbl
336 | str2pos_ "Met" = Met
337 | str2pos_ "Frm" = Frm
338 | str2pos_ "Res" = Res
339 | str2pos_ "Und" = Und
340 | str2pos_ str = error ("str2pos_: wrong argument = " ^ str)
342 type pos' = pos * pos_;
343 (*WN0312 remembering interator (pos * pos_) for ctree
344 pos : lev_on, lev_dn, lev_up,
345 lev_onFrm, lev_dnRes (..see solve Apply_Method !)
347 # generate1 sets pos_ if possible ...?WN0502?NOT...
348 # generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn
349 exceptions: Begin/End_Trans
350 # thus generate(1) called in
352 .# nxt_solv (tac_ -cases); general case:
353 val pos' = case pos' of (p,Res) => (lev_on p',Res) | _ => pos'
355 generate1...(Rewrite(f,..,res))..(pos, pos_)
356 cappend_atomic.................pos ////// gets f+res always!!!
357 cut_tree....................pos, pos_
359 fun pos'2str (p, p_) = pair2str (ints2str' p, pos_2str p_);
360 fun pos's2str ps = (strs2str' o (map pos'2str)) ps; (* for tests only *)
361 val e_pos' = ([], Und);
363 fun res2str (t, ts) = pair2str (term2str t, terms2str ts);
367 (*26.4.02: never used after introduction of scripts !!!
368 type loc = loc_ * (* + interpreter-state *)
369 (loc_ * rls') (* -"- for script of the ruleset*)
371 val e_loc = ([],NONE):loc;
372 val ee_loc = (e_loc,e_loc);*)
375 datatype safe = Sundef | Safe | Unsafe | Helpless;
376 fun safe2str Sundef = "Sundef"
377 | safe2str Safe = "Safe"
378 | safe2str Unsafe = "Unsafe"
379 | safe2str Helpless = "Helpless";
381 type subs = cterm' list; (*16.11.00 for FE-KE*)
382 val e_subs = ["(bdv, x)"];
384 (* argument type of tac Rewrite_Inst *)
385 type sube = cterm' list;
386 val e_sube = []: cterm' list;
387 fun sube2str s = strs2str s;
389 (*._sub_stitution as _t_erms of _e_qualities.*)
390 type subte = term list;
391 val e_subte = []: term list;
392 fun subte2str ss = terms2str ss;
394 val subte2sube = map term2str;
395 val subst2subs = map (pair2str o (apfst term2str) o (apsnd term2str));
396 fun subst2sube subst = map term2str (map HOLogic.mk_eq subst)
397 val subst2subs' = map ((apfst term2str) o (apsnd term2str));
398 fun subs2subst thy s = map (isapair2pair o (parse_patt thy)) s;
399 fun sube2subst thy s = map (dest_equals' o (parse_patt thy)) s;
400 val sube2subte = map str2term;
401 val subte2subst = map HOLogic.dest_eq;
403 fun isasub2subst isasub = ((map isapair2pair) o isalist2list) isasub;
405 type scrstate = (*state for script interpreter*)
406 env(*stack*) (*used to instantiate tac for checking assod
407 12.03.noticed: e_ not updated during execution ?!?*)
408 * loc_ (*location of tac in script*)
409 * term option(*argument of curried functions*)
410 * term (*value obtained by tac executed
411 updated also after a derivation by 'new_val'*)
412 * safe (*estimation of how result will be obtained*)
413 * bool; (*true = strongly .., false = weakly associated:
414 only used during ass_dn/up*)
415 val e_scrstate = ([],[],NONE,e_term,Sundef,false): scrstate;
416 fun topt2str NONE = "NONE"
417 | topt2str (SOME t) = "SOME" ^ term2str t;
418 fun scrstate2str (env, loc_, topt, t, safe, bool) =
419 "(" ^ env2str env ^ ", " ^ loc_2str loc_ ^ ", " ^ topt2str topt ^ ", \n" ^
420 term2str t ^ ", " ^ safe2str safe ^ ", " ^ bool2str bool ^ ")";
422 (* for handling type istate see fun from_pblobj_or_detail', +? *)
423 datatype istate = (*interpreter state*)
424 Uistate (*undefined in modspec, in '_deriv'ation*)
425 | ScrState of scrstate (*for script interpreter*)
426 | RrlsState of rrlsstate; (*for reverse rewriting*)
427 val e_istate = (ScrState ([],[],NONE,e_term,Sundef,false));
428 val e_ctxt = Proof_Context.init_global @{theory "Pure"};
430 (* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*)
431 fun is_e_ctxt ctxt = Theory.eq_thy (Proof_Context.theory_of ctxt, @{theory "Pure"});
433 type iist = istate option * istate option;
434 (*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*)
437 fun rta2str (r,(t,a)) = "\n("^(rule2str r)^",("^(term2str t)^", "^
439 fun istate2str Uistate = "Uistate"
440 | istate2str (ScrState (e, l, to, t, s, b)) =
441 "ScrState ("^ subst2str e ^",\n "^
442 loc_2str l ^", "^ termopt2str to ^",\n "^
443 term2str t ^", "^ safe2str s ^", "^ bool2str b ^")"
444 | istate2str (RrlsState (t,t1,rss,rtas)) =
445 "RrlsState ("^(term2str t)^", "^(term2str t1)^", "^
446 ((strs2str o (map (strs2str o (map rule2str)))) rss)^", "^
447 ((strs2str o (map rta2str)) rtas)^")";
448 fun istates2str (NONE, NONE) = "(#NONE, #NONE)"
449 | istates2str (NONE, SOME ist) = "(#NONE,\n#SOME "^istate2str ist^")"
450 | istates2str (SOME ist, NONE) = "(#SOME "^istate2str ist^",\n #NONE)"
451 | istates2str (SOME i1, SOME i2) = "(#SOME "^istate2str i1^",\n #SOME "^
454 fun new_val v (ScrState (env, loc_, topt, _, safe, bool)) =
455 (ScrState (env, loc_, topt, v, safe, bool))
456 | new_val _ _ = error "new_val: only for ScrState";
458 datatype con = land | lor;
462 (*.tactics propagate the construction of the calc-tree;
464 (a) 'specsteps' for the specify-phase, and others for the solve-phase
465 (b) those of the solve-phase are 'initac's and others;
466 initacs start with a formula different from the preceding formula.
467 see 'type tac_' for the internal representation of tactics.*)
468 datatype tac = (* TODO: arrange according to signature *)
469 Init_Proof of ((cterm' list) * spec)
472 | Refine_Problem of pblID | Refine_Tacitly of pblID
474 | Add_Given of cterm' | Del_Given of cterm'
475 | Add_Find of cterm' | Del_Find of cterm'
476 | Add_Relation of cterm' | Del_Relation of cterm'
478 | Specify_Theory of domID | Specify_Problem of pblID
479 | Specify_Method of metID
481 | Apply_Method of metID
482 (*.creates an 'istate' in PblObj.env; in case of 'init_form'
483 creates a formula at ((lev_on o lev_dn) p, Frm) and in this ppobj.'loc'
484 'SOME istate' (at fst of 'loc').
485 As each step (in the solve-phase) has a resulting formula (at the front-end)
486 Apply_Method also does the 1st step in the script (an 'initac') if there
487 is no 'init_form' .*)
488 | Check_Postcond of pblID
491 (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
492 because there all the thms are present with both (thmID, thm)
493 (where user-views can show both or only one of (thmID, thm)),
494 and thm is created from ThmID by assoc_thm'' when entering isabisac *)
495 | Rewrite_Inst of ( subs * thm'') | Rewrite of thm'' | Rewrite_Asm of thm''
496 | Rewrite_Set_Inst of ( subs * rls') | Rewrite_Set of rls'
497 | Detail_Set_Inst of ( subs * rls') | Detail_Set of rls'
498 | End_Detail (*end of script from next_tac,
499 in solve: switches back to parent script WN0509 drop!*)
500 | Derive of rls' (*an input formula using rls WN0509 drop!*)
501 | Calculate of string (* plus | minus | times | cancel | pow | sqrt *)
503 | Substitute of sube | Apply_Assumption of cterm' list
505 | Take of cterm' (*an 'initac'*)
506 | Take_Inst of cterm'
507 | Group of (con * int list )
508 | Subproblem of (domID * pblID) (*an 'initac'*)
509 | CAScmd of cterm' (*6.6.02 URD: Function formula; WN0509 drop!*)
510 | End_Subproblem (*WN0509 drop!*)
512 | Split_And | Conclude_And
513 | Split_Or | Conclude_Or
514 | Begin_Trans | End_Trans
515 | Begin_Sequ | End_Sequ(* substitute root.env *)
516 | Split_Intersect | End_Intersect
517 | Check_elementwise of cterm' | Collect_Trues
518 | Or_to_List (*WN120315 ~ @{thm d2_prescind1},2,3,4 in PolyEq.thy *)
520 | Empty_Tac (* TODO.11.6.03 ... of string: could carry msg of (Notappl msg)
522 | Tac of string (* eg.'repeat'*WN0509 drop! (ab)used to report syntaxerror *)
523 | End_Proof'; (* inout *)
525 (* tac2str /--> library.sml: needed in dialog.sml for 'separable *)
526 fun tac2str ma = case ma of
527 Init_Proof (ppc, spec) =>
528 "Init_Proof "^(pair2str (strs2str ppc, spec2str spec))
529 | Model_Problem => "Model_Problem "
530 | Refine_Tacitly pblID => "Refine_Tacitly "^(strs2str pblID)
531 | Refine_Problem pblID => "Refine_Problem "^(strs2str pblID)
532 | Add_Given cterm' => "Add_Given "^cterm'
533 | Del_Given cterm' => "Del_Given "^cterm'
534 | Add_Find cterm' => "Add_Find "^cterm'
535 | Del_Find cterm' => "Del_Find "^cterm'
536 | Add_Relation cterm' => "Add_Relation "^cterm'
537 | Del_Relation cterm' => "Del_Relation "^cterm'
539 | Specify_Theory domID => "Specify_Theory "^(quote domID )
540 | Specify_Problem pblID => "Specify_Problem "^(strs2str pblID )
541 | Specify_Method metID => "Specify_Method "^(strs2str metID)
542 | Apply_Method metID => "Apply_Method "^(strs2str metID)
543 | Check_Postcond pblID => "Check_Postcond "^(strs2str pblID)
544 | Free_Solve => "Free_Solve"
546 | Rewrite_Inst (subs, (id, thm)) =>
547 "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> term2str)))
548 | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> term2str)
549 | Rewrite_Asm (id, thm) => "Rewrite_Asm " ^ spair2str (id, thm |> Thm.prop_of |> term2str)
550 | Rewrite_Set_Inst (subs, rls) =>
551 "Rewrite_Set_Inst "^(pair2str (subs2str subs, quote rls))
552 | Rewrite_Set rls => "Rewrite_Set "^(quote rls )
553 | Detail_Set rls => "Detail_Set "^(quote rls )
554 | Detail_Set_Inst (subs, rls) =>
555 "Detail_Set_Inst "^(pair2str (subs2str subs, quote rls))
556 | End_Detail => "End_Detail"
557 | Derive rls' => "Derive "^rls'
558 | Calculate op_ => "Calculate "^op_
559 | Substitute sube => "Substitute "^sube2str sube
560 | Apply_Assumption ct's => "Apply_Assumption "^(strs2str ct's)
562 | Take cterm' => "Take "^(quote cterm' )
563 | Take_Inst cterm' => "Take_Inst "^(quote cterm' )
564 | Group (con, ints) =>
565 "Group "^(pair2str (con2str con, ints2str ints))
566 | Subproblem (domID, pblID) =>
567 "Subproblem "^(pair2str (domID, strs2str pblID))
568 (*| Subproblem_Full (spec, cts') =>
569 "Subproblem_Full "^(pair2str (spec2str spec, strs2str cts'))*)
570 | End_Subproblem => "End_Subproblem"
571 | CAScmd cterm' => "CAScmd "^(quote cterm')
573 | Check_elementwise cterm'=> "Check_elementwise "^(quote cterm')
574 | Or_to_List => "Or_to_List "
575 | Collect_Trues => "Collect_Trues"
577 | Empty_Tac => "Empty_Tac"
578 | Tac string => "Tac "^string
579 | End_Proof' => "tac End_Proof'"
580 | _ => "tac2str not impl. for ?!";
582 fun is_empty_tac tac = case tac of Empty_Tac => true | _ => false
584 fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
585 | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
586 | eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2
587 | eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2
588 | eq_tac (Calculate id1, Calculate id2) = id1 = id2
591 fun is_rewset (Rewrite_Set_Inst _) = true
592 | is_rewset (Rewrite_Set _) = true
593 | is_rewset _ = false;
594 fun is_rewtac (Rewrite _) = true
595 | is_rewtac (Rewrite_Inst _) = true
596 | is_rewtac (Rewrite_Asm _) = true
597 | is_rewtac tac = is_rewset tac;
599 fun tac2IDstr ma = case ma of
600 Model_Problem => "Model_Problem"
601 | Refine_Tacitly pblID => "Refine_Tacitly"
602 | Refine_Problem pblID => "Refine_Problem"
603 | Add_Given cterm' => "Add_Given"
604 | Del_Given cterm' => "Del_Given"
605 | Add_Find cterm' => "Add_Find"
606 | Del_Find cterm' => "Del_Find"
607 | Add_Relation cterm' => "Add_Relation"
608 | Del_Relation cterm' => "Del_Relation"
610 | Specify_Theory domID => "Specify_Theory"
611 | Specify_Problem pblID => "Specify_Problem"
612 | Specify_Method metID => "Specify_Method"
613 | Apply_Method metID => "Apply_Method"
614 | Check_Postcond pblID => "Check_Postcond"
615 | Free_Solve => "Free_Solve"
617 | Rewrite_Inst (subs,thm')=> "Rewrite_Inst"
618 | Rewrite thm' => "Rewrite"
619 | Rewrite_Asm thm' => "Rewrite_Asm"
620 | Rewrite_Set_Inst (subs, rls) => "Rewrite_Set_Inst"
621 | Rewrite_Set rls => "Rewrite_Set"
622 | Detail_Set rls => "Detail_Set"
623 | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst"
624 | Derive rls' => "Derive "
625 | Calculate op_ => "Calculate "
626 | Substitute subs => "Substitute"
627 | Apply_Assumption ct's => "Apply_Assumption"
629 | Take cterm' => "Take"
630 | Take_Inst cterm' => "Take_Inst"
631 | Group (con, ints) => "Group"
632 | Subproblem (domID, pblID) => "Subproblem"
633 | End_Subproblem => "End_Subproblem"
634 | CAScmd cterm' => "CAScmd"
636 | Check_elementwise cterm'=> "Check_elementwise"
637 | Or_to_List => "Or_to_List "
638 | Collect_Trues => "Collect_Trues"
640 | Empty_Tac => "Empty_Tac"
641 | Tac string => "Tac "
642 | End_Proof' => "End_Proof'"
643 | _ => "tac2str not impl. for ?!";
645 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
646 | rls_of (Rewrite_Set rls) = rls
647 | rls_of tac = error ("rls_of: called with tac '"^tac2IDstr tac^"'");
649 fun thm_of_rew (Rewrite_Inst (subs,(thmID,_))) =
650 (thmID, SOME ((subs2subst (assoc_thy "Isac") subs)))
651 | thm_of_rew (Rewrite (thmID,_)) = (thmID, NONE)
652 | thm_of_rew (Rewrite_Asm (thmID,_)) = (thmID, NONE);
654 fun rls_of_rewset (Rewrite_Set_Inst (subs,rls)) =
655 (rls, SOME ((subs2subst (assoc_thy "Isac") subs)))
656 | rls_of_rewset (Rewrite_Set rls) = (rls, NONE)
657 | rls_of_rewset (Detail_Set rls) = (rls, NONE)
658 | rls_of_rewset (Detail_Set_Inst (subs, rls)) =
659 (rls, SOME ((subs2subst (assoc_thy "Isac") subs)));
661 fun rule2tac thy _ (Calc (opID, thm)) = Calculate (assoc_calc thy opID)
662 | rule2tac _ [] (Thm thm'') = Rewrite thm''
663 | rule2tac _ subst (Thm thm'') =
664 Rewrite_Inst (subst2subs subst, thm'')
665 | rule2tac _ [] (Rls_ rls) = Rewrite_Set (id_rls rls)
666 | rule2tac _ subst (Rls_ rls) =
667 Rewrite_Set_Inst (subst2subs subst, (id_rls rls))
668 | rule2tac _ _ rule =
669 error ("rule2tac: called with '" ^ rule2str rule ^ "'");
671 type fmz_ = cterm' list;
673 (*.a formalization of an example containing data
674 sufficient for mechanically finding the solution for the example.*)
675 (*FIXME.WN051014: dont store fmz = (_,spec) in the PblObj,
676 this is done in origin*)
677 type fmz = fmz_ * spec;
678 val e_fmz = ([],e_spec);
680 (* tac_ contains results from check in 'fun applicable_in'.
681 This is useful for costly results, e.g. from rewriting;
682 however, these results might be changed by Scripts like
683 " eq = (Rewrite_Set ansatz_rls False) eql;" ^
684 " eq = drop_questionmarks eq;" ^
685 " eq = (Rewrite_Set equival_trans False) eq;" ^
686 WN120106 TODO ANALOGOUSLY TO Substitute':
687 So tac_ contains the term t the result was calculated from
688 in order to compare t with t' possibly changed by "Expr "
689 and re-calculate result if t<>t'*)
690 datatype tac_ = (* TODO: arrange according to signature *)
691 Init_Proof' of ((cterm' list) * spec)
694 itm list * (*the 'untouched' pbl*)
695 itm list (*the casually completed met*)
698 pblID * (*the refined from applicable_in*)
699 domID * (*from new pbt?! filled in specify*)
700 metID * (*from new pbt?! filled in specify*)
701 itm list (*drop ! 9.03: remains [] for
702 Model_Problem recognizing its activation*)
703 | Refine_Problem' of (pblID * (itm list * (bool * Term.term) list))
704 (*FIXME?040215 drop: done automatically in init_proof + Subproblem'*)
707 itm list (*updated with input in fun specify_additem*)
708 | Add_Find' of cterm' * itm list (* see Add_Given' *)
709 | Add_Relation' of cterm' * itm list (* see Add_Given' *)
710 | Del_Given' of cterm' | Del_Find' of cterm' | Del_Relation' of cterm'
711 (*4.00.: all.. term: in applicable_in ..? Syn ?only for FormFK?*)
712 | Specify_Theory' of domID
713 | Specify_Problem' of
715 (bool * (* matches *)
716 (itm list * (* ppc *)
717 (bool * term) list))) (* preconditions *)
720 ori list * (*repl. "#undef"*)
721 itm list (*... updated from pbl to met*)
724 (term option) * (*init_form*)
725 istate * Proof.context
728 (term * (*returnvalue of script in solve*)
729 term list) (*collect by get_assumptions_ in applicable_in, except if
730 butlast tac is Check_elementwise: take only these asms*)
732 (* context_thy would be simpler if instead thm' woudl be thm *)
733 | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * (term * term list)
734 | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * result
735 | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * result
736 | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * result
737 | Detail_Set_Inst' of theory' * bool * subst * rls * term * result
738 | Rewrite_Set' of theory' * bool * rls * term * result
739 | Detail_Set' of theory' * bool * rls * term * result
740 | End_Detail' of (term * (term list)) (*see End_Trans'*)
741 | End_Ruleset' of term
743 | Calculate' of theory' * string * term * (term * thm')
745 rew_ord_ * (*for re-calculation *)
746 rls * (*for re-calculation *)
747 subte * (*the 'substitution': terms of type bool*)
748 term * (*to be substituted in *)
749 term (*resulting from the substitution *)
750 | Apply_Assumption' of term list * term
755 (ori list) * (* filled in assod Subproblem' *)
756 term * (*-"-, headline of calc-head *)
758 Proof.context *(* transported from assod to generate1 *)
759 term) (* Subproblem(dom,pbl) OR cascmd*)
761 | End_Subproblem' of term (*???*)
762 | Split_And' of term | Conclude_And' of term
763 | Split_Or' of term | Conclude_Or' of term
764 | Begin_Trans' of term | End_Trans' of (term * (term list))
765 | Begin_Sequ' | End_Sequ'(* substitute root.env*)
766 | Split_Intersect' of term | End_Intersect' of term
767 | Check_elementwise' of (*special case:*)
768 term * (*(1)the current formula: [x=1,x=...]*)
769 string * (*(2)the pred from Check_elementwise *)
770 (term * (*(3)composed from (1) and (2): {x. pred}*)
771 term list) (*20.5.03 assumptions*)
772 | Or_to_List' of term * term (* (a | b, [a,b]) *)
773 | Collect_Trues' of term
775 | Tac_ of (*for dummies*)
779 string (*result of Tac".."*)
780 | End_Proof'';(*End_Proof:inout*)
782 fun tac_2str ma = case ma of
783 Init_Proof' (ppc, spec) =>
784 "Init_Proof' "^(pair2str (strs2str ppc, spec2str spec))
785 | Model_Problem' (pblID,_,_) => "Model_Problem' "^(strs2str pblID )
786 | Refine_Tacitly'(p,prefin,domID,metID,itms)=>
788 ^(strs2str p)^", "^(strs2str prefin)^", "
789 ^domID^", "^(strs2str metID)^", pbl-itms)"
790 | Refine_Problem' ms => "Refine_Problem' ("^(*matchs2str ms*)"..."^")"
791 (*| Match_Problem' (pI, (ok, (itms, pre))) =>
792 "Match_Problem' "^(spair2str (strs2str pI,
793 spair2str (bool2str ok,
794 spair2str ("itms2str_ itms",
795 "items2str pre"))))*)
796 | Add_Given' cterm' => "Add_Given' "(*^cterm'*)
797 | Del_Given' cterm' => "Del_Given' "(*^cterm'*)
798 | Add_Find' cterm' => "Add_Find' "(*^cterm'*)
799 | Del_Find' cterm' => "Del_Find' "(*^cterm'*)
800 | Add_Relation' cterm' => "Add_Relation' "(*^cterm'*)
801 | Del_Relation' cterm' => "Del_Relation' "(*^cterm'*)
803 | Specify_Theory' domID => "Specify_Theory' "^(quote domID )
804 | Specify_Problem' (pI, (ok, (itms, pre))) =>
805 "Specify_Problem' "^(spair2str (strs2str pI,
806 spair2str (bool2str ok,
807 spair2str ("itms2str_ itms",
809 | Specify_Method' (pI,oris,itms) =>
810 "Specify_Method' ("^metID2str pI^", "^oris2str oris^", )"
812 | Apply_Method' (metID,_,_,_) => "Apply_Method' "^(strs2str metID)
813 | Check_Postcond' (pblID,(scval,asm)) =>
815 (spair2str (strs2str pblID, spair2str (term2str scval, terms2str asm)))
817 | Free_Solve' => "Free_Solve'"
819 | Rewrite_Inst' (*subs,thm'*) _ =>
820 "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
821 | Rewrite' thm' => "Rewrite' "(*^(spair2str thm')*)
822 | Rewrite_Asm' thm' => "Rewrite_Asm' "(*^(spair2str thm')*)
823 | Rewrite_Set_Inst' (*subs,thm'*) _ =>
824 "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
825 | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) =>
826 "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^ "," ^ id_rls rls' ^ "," ^
827 term2str f ^ ",(" ^ term2str f' ^ "," ^ terms2str asm ^ "))"
828 | End_Detail' _ => "End_Detail' xxx"
829 | Detail_Set' _ => "Detail_Set' xxx"
830 | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
832 | Derive' rls => "Derive' "^id_rls rls
833 | Calculate' _ => "Calculate' "
834 | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
835 | Apply_Assumption' ct's => "Apply_Assumption' "(*^(strs2str ct's)*)
837 | Take' cterm' => "Take' "(*^(quote cterm' )*)
838 | Take_Inst' cterm' => "Take_Inst' "(*^(quote cterm' )*)
839 | Subproblem' (spec, oris, _, _, _, pbl_form) =>
840 "Subproblem' "(*^(pair2str (domID, strs2str ,...))*)
841 | End_Subproblem' _ => "End_Subproblem'"
842 | CAScmd' cterm' => "CAScmd' "(*^(quote cterm')*)
844 | Empty_Tac_ => "Empty_Tac_"
845 | Tac_ (_,form,id,result) => "Tac_ (thy,"^form^","^id^","^result^")"
846 | _ => "tac_2str not impl. for arg";
848 (*'executed tactics' (tac_s) with local environment etc.;
849 used for continuing eval script + for generate*)
851 (loc_ * (* of tactic in scr, tactic (weakly) associated with tac_*)
852 (tac_ * (* (for generate) *)
853 env * (* with 'tactic=result' as a rule, tactic ev. _not_ ready:
854 for handling 'parallel let'*)
855 env * (* with results of (ready) tacs *)
856 term * (* itr_arg of tactic, for upd. env at Repeat, Try*)
857 term * (* result value of the tac *)
863 fun ets2s (l,(m,eno,env,iar,res,s)) =
864 "\n(" ^ loc_2str l ^ ",(" ^ tac_2str m ^
865 ",\n ens= " ^ subst2str eno ^
866 ",\n env= " ^ subst2str env ^
867 ",\n iar= " ^ term2str iar ^
868 ",\n res= " ^ term2str res ^
869 ",\n " ^ safe2str s ^ "))";
870 fun ets2str (ets: ets) = (strs2str o (map ets2s)) ets;
873 type envp =(*9.5.03: unused, delete with field in ctree.PblObj FIXXXME*)
874 (int * term list) list * (*assoc-list: args of met*)
875 (int * rls) list * (*assoc-list: tacs already done ///15.9.00*)
876 (int * ets) list * (*assoc-list: tacs etc. already done*)
877 (string * pos) list; (*asms * from where*)
878 val empty_envp = ([], [], [], []): envp;
880 datatype ppobj = (* TODO: arrange according to signature *)
882 {cell : lrd option, (* where in form tac has been applied *)
883 (*^^^FIXME.WN0607 rename this field*)
884 form : term, (* where tac is applied to *)
885 tac : tac, (* also in istate *)
886 loc : (istate * (* script interpreter state *)
887 Proof.context) (* context for provers, type inference *)
888 option * (* both for interpreter location on Frm, Pbl, Met *)
889 (istate * (* script interpreter state *)
890 Proof.context) (* context for provers, type inference *)
891 option, (* both for interpreter location on Res *)
892 (*(NONE,NONE) <==> e_istate ! see update_loc, get_loc*)
893 branch: branch, (* only rudimentary *)
894 result: result, (* result and assumptions *)
895 ostate: ostate} (* Complete <=> result is OK *)
897 {cell : lrd option, (* unused: meaningful only for some _Prf_Obj *)
898 fmz : fmz, (* from init:FIXME never use this spec;-drop *)
899 origin: (ori list) * (* representation from fmz+pbt
900 for efficiently adding items in probl, meth *)
901 spec * (* updated by Refine_Tacitly *)
902 term, (* headline of calc-head, as calculated initially(!)*)
903 spec : spec, (* explicitly input *)
904 probl : itm list, (* itms explicitly input *)
905 meth : itm list, (* itms automatically added to copy of probl *)
906 ctxt : Proof.context, (* WN110513 introduced to avoid [*] [**]*)
907 env : (istate * Proof.context) option,
908 (* istate only for initac in script
909 context for specify phase on this node NO..
910 ..NO: this conflicts with init_form/initac: see Apply_Method without init_form *)
911 loc : (istate * Proof.context) option * (istate * (* like PrfObj *)
912 Proof.context) option, (* for spec-phase [*], NO..
913 ..NO: raises errors not tracable on WN110513 [**]*)
914 branch: branch, (* like PrfObj *)
915 result: result, (* like PrfObj *)
916 ostate: ostate}; (* like PrfObj *)
918 (*.this tree contains isac's calculations; TODO.WN03 rename to ctree;
919 the tree's structure has been copied from an early version of Theorema(c);
920 it has the disadvantage, that there is no space
921 for the first tactic in a script generating the first formula at (p,Frm);
922 this trouble has been covered by 'init_form' and 'Take' so far,
923 but it is crucial if the first tactic in a script is eg. 'Subproblem';
924 see 'type tac ', Apply_Method.
928 | Nd of ppobj * (ctree list);
929 val e_ctree = EmptyPtree;
930 type state = ctree * pos
932 fun rep_prfobj (PrfObj {cell,form,tac,loc,branch,result,ostate}) =
933 {cell=cell,form=form,tac=tac,loc=loc,branch=branch,result=result,ostate=ostate};
934 fun rep_pblobj (PblObj {cell,origin,fmz,spec,probl,meth,ctxt,
935 env,loc,branch,result,ostate}) =
936 {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,ctxt=ctxt,
937 env=env,loc=loc,branch=branch,result=result,ostate=ostate};
938 fun is_prfobj (PrfObj _) = true
939 | is_prfobj _ =false;
940 (*val is_prfobj' = get_obj is_prfobj; *)
941 fun is_pblobj (PblObj _) = true
942 | is_pblobj _ = false;
943 (*val is_pblobj' = get_obj is_pblobj; 'Error: unbound constructor get_obj'*)
945 type state = ctree * pos'
947 exception PTREE of string;
948 fun nth _ [] = raise PTREE "nth _ []"
950 | nth n (x::xs) = nth (n-1) xs;
951 (*> nth 2 [11,22,33]; -->> val it = 22 : int*)
953 fun lev_up [] = raise PTREE "lev_up []"
954 | lev_up p = (drop_last p):pos;
955 fun lev_on [] = raise PTREE "lev_on []"
957 let val len = length pos
958 in (drop_last pos) @ [(nth len pos)+1] end;
959 fun lev_onFrm (p,_) = (lev_on p,Frm):pos'
960 | lev_onFrm p = raise PTREE ("*** lev_onFrm: pos'="^(pos'2str p));
961 (*040216: for inform --> embed_deriv: remains on same level TODO.WN120517 compare lev_pred*)
962 fun lev_back' ([],_) = raise PTREE "lev_back': called by ([],_)"
964 if last_elem p <= 1 then (p, Frm):pos'
965 else ((drop_last p) @ [(nth (length p) p) - 1], Res);
966 (*.increase pos by n within a level.*)
967 fun pos_plus 0 pos = pos
968 | pos_plus n (p,Frm) = pos_plus (n-1) (p, Res)
969 | pos_plus n (p, _) = pos_plus (n-1) (lev_on p, Res);
971 fun lev_pred [] = raise PTREE "lev_pred []"
973 let val len = length pos
974 in ((drop_last pos) @ [(nth len pos)-1]) end;
976 val it = [1,2,2] : pos
978 val it = [0] : pos *)
980 fun lev_dn p = p @ [0];
981 (*> (lev_dn o lev_on) [1,2,3];
982 val it = [1,2,4,0] : pos *)
983 (*fun lev_dn' ((p,p_):pos') = (lev_dn p, Frm):pos'; WN.3.12.03: never used*)
984 fun lev_dnRes (p,_) = (lev_dn p, Res);
987 fun lev_up_ (p,Res) = (lev_up p,Res):pos'
988 | lev_up_ p' = error ("lev_up_: called for "^(pos'2str p'));
989 fun lev_dn_ (p, _) = (lev_dn p, Res)
990 fun ind (p,_) = length p; (*WN050108 deprecated in favour of lev_of*)
991 fun lev_of (p,_) = length p;
994 (** convert ctree to a string **)
996 (* convert a pos from list to string *)
997 fun pr_pos ps = (space_implode "." (map string_of_int ps))^". ";
998 (* show hd origin or form only *)
999 fun pr_short p (PblObj {origin = (ori,_,_),...}) =
1000 ((pr_pos p) ^ " ----- pblobj -----\n")
1001 (* ((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^
1002 (((Syntax.string_of_term (thy2ctxt' "Isac")) o hd(*!?!*) o #5 o hd) ori))^
1004 | pr_short p (PrfObj {form = form,...}) =
1005 ((pr_pos p) ^ (term2str form) ^ "\n");
1007 fun pr_cell (p:pos) (PblObj {cell = c, origin = (ori,_,_),...}) =
1009 ((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^
1010 (((Syntax.string_of_term (thy2ctxt' "Isac")) o hd(*!?!*) o #5 o hd) ori))^
1012 | pr_cell p (PrfObj {cell = c, form = form,...}) =
1013 ((ints2str c) ^" "^ (term2str form) ^ "\n");
1019 fun pr_pt pfn _ EmptyPtree = ""
1020 | pr_pt pfn ps (Nd (b, [])) = pfn ps b
1021 | pr_pt pfn ps (Nd (b, ts)) = (pfn ps b)^
1023 and prts pfn ps p [] = ""
1024 | prts pfn ps p (t::ts) = (pr_pt pfn (ps @ [p]) t)^
1025 (prts pfn ps (p+1) ts)
1026 in pr_pt f [] pt end;
1028 > fun prfn ps b = (pr_pos ps)^" "^b(*TODO*)^"\n";
1029 (*val pt = Unsynchronized.ref EmptyPtree;*)
1036 > tracing (pr_ctree prfn (!pt));
1040 (** access the branches of ctree **)
1042 fun ins_nth 1 e l = e::l
1043 | ins_nth n e [] = raise PTREE "ins_nth n e []"
1044 | ins_nth n e (l::ls) = l::(ins_nth (n-1) e ls);
1045 fun repl [] _ _ = raise PTREE "repl [] _ _"
1046 | repl (l::ls) 1 e = e::ls
1047 | repl (l::ls) n e = l::(repl ls (n-1) e);
1048 fun repl_app ls n e =
1049 let val lim = 1 + length ls
1050 in if n > lim then raise PTREE "repl_app: n > lim"
1051 else if n = lim then ls @ [e]
1052 else repl ls n e end;
1054 > repl [1,2,3] 2 22222;
1055 val it = [1,22222,3] : int list
1056 > repl_app [1,2,3,4] 5 5555;
1057 val it = [1,2,3,4,5555] : int list
1058 > repl_app [1,2,3] 2 22222;
1059 val it = [1,22222,3] : int list
1060 > repl_app [1] 2 22222 ;
1061 val it = [1,22222] : int list
1065 (*.get from obj at pos by f : ppobj -> 'a.*)
1066 fun get_obj f EmptyPtree _ = raise PTREE "get_obj f EmptyPtree"
1067 | get_obj f (Nd (b, _)) [] = f b
1068 | get_obj f (Nd (b, bs)) (p::ps) =
1069 (* val (f, Nd (b, bs), (p::ps)) = (I, pt, p);
1071 let val _ = (nth p bs) handle _ => raise PTREE ("get_obj: pos = "^
1072 (ints2str' (p::ps))^" does not exist");
1073 in (get_obj f (nth p bs) ps)
1074 (*before WN050419: 'wrong type..' raised also if pos doesn't exist*)
1075 handle _ => raise PTREE (*"get_obj: at pos = "^
1076 (ints2str' (p::ps))^" wrong type of ppobj"*)
1078 (ints2str' (p::ps))^" does not exist")
1080 fun get_nd EmptyPtree _ = raise PTREE "get_nd EmptyPtree"
1082 | get_nd (Nd (_,nds)) (pos as p :: ps) = (get_nd (nth p nds) ps)
1083 handle _ => raise PTREE ("get_nd: not existent pos = "^(ints2str' pos));
1085 (* for use by get_obj *)
1086 fun g_cell (PblObj {cell = c,...}) = NONE
1087 | g_cell (PrfObj {cell = c,...}) = c;(*WN0607 hack for quick introduction of lrd + rewrite-at (thms, calcs)*)
1088 fun g_form (PrfObj {form = f,...}) = f
1089 | g_form (PblObj {origin=(_,_,f),...}) = f;
1090 fun g_form' (Nd (PrfObj {form = f,...}, _)) = f
1091 | g_form' (Nd (PblObj {origin=(_,_,f),...}, _)) = f;
1092 (* | g_form _ = raise PTREE "g_form not for PblObj";*)
1093 fun g_origin (PblObj {origin = ori,...}) = ori
1094 | g_origin _ = raise PTREE "g_origin not for PrfObj";
1095 fun g_fmz (PblObj {fmz = f,...}) = f
1096 | g_fmz _ = raise PTREE "g_fmz not for PrfObj";
1097 fun g_spec (PblObj {spec = s,...}) = s
1098 | g_spec _ = raise PTREE "g_spec not for PrfObj";
1099 fun g_pbl (PblObj {probl = p,...}) = p
1100 | g_pbl _ = raise PTREE "g_pbl not for PrfObj";
1101 fun g_met (PblObj {meth = p,...}) = p
1102 | g_met _ = raise PTREE "g_met not for PrfObj";
1103 fun g_domID (PblObj {spec = (d,_,_),...}) = d
1104 | g_domID _ = raise PTREE "g_metID not for PrfObj";
1105 fun g_metID (PblObj {spec = (_,_,m),...}) = m
1106 | g_metID _ = raise PTREE "g_metID not for PrfObj";
1107 fun g_ctxt (PblObj {ctxt, ...}) = ctxt
1108 | g_ctxt _ = raise PTREE "g_ctxt not for PrfObj";
1109 fun g_env (PblObj {env,...}) = env
1110 | g_env _ = raise PTREE "g_env not for PrfObj";
1111 fun g_loc (PblObj {loc = l,...}) = l
1112 | g_loc (PrfObj {loc = l,...}) = l;
1113 fun g_branch (PblObj {branch = b,...}) = b
1114 | g_branch (PrfObj {branch = b,...}) = b;
1115 fun g_tac (PblObj {spec = (d,p,m),...}) = Apply_Method m
1116 | g_tac (PrfObj {tac = m,...}) = m;
1117 fun g_result (PblObj {result = r,...}) = r
1118 | g_result (PrfObj {result = r,...}) = r;
1119 fun g_res (PblObj {result = (r,_),...}) = r
1120 | g_res (PrfObj {result = (r,_),...}) = r;
1121 fun g_res' (Nd (PblObj {result = (r,_),...}, _)) = r
1122 | g_res' (Nd (PrfObj {result = (r,_),...}, _)) = r;
1123 fun g_ostate (PblObj {ostate = r,...}) = r
1124 | g_ostate (PrfObj {ostate = r,...}) = r;
1125 fun g_ostate' (Nd (PblObj {ostate = r,...}, _)) = r
1126 | g_ostate' (Nd (PrfObj {ostate = r,...}, _)) = r;
1128 fun gpt_cell (Nd (PblObj {cell = c,...},_)) = NONE
1129 | gpt_cell (Nd (PrfObj {cell = c,...},_)) = c;
1131 (* get the formula preceeding the current position in a calculation *)
1132 fun get_curr_formula (pt, pos as (p, p_)) =
1134 Frm => get_obj g_form pt p
1135 | Res => (fst o (get_obj g_result pt)) p
1136 | _ => #3 (get_obj g_origin pt p);
1138 (*in CalcTree/Subproblem an 'just_created_' model is created;
1139 this is filled to 'untouched' by Model/Refine_Problem*)
1140 fun just_created_ (PblObj {meth, probl, spec, ...}) =
1141 null meth andalso null probl andalso spec = e_spec;
1142 val e_origin = ([],e_spec,e_term);
1144 fun just_created (pt, (p, _)) =
1145 let val ppobj = get_obj I pt p
1146 in is_pblobj ppobj andalso just_created_ ppobj end;
1148 (*.does the pos in the ctree exist ?.*)
1149 fun existpt pos pt = can (get_obj I pt) pos;
1150 (*.does the pos' in the ctree exist, ie. extra check for result in the node.*)
1151 fun existpt' (p,p_) pt =
1152 if can (get_obj I pt) p
1154 Res => get_obj g_ostate pt p = Complete
1158 (*.is this position appropriate for calculating intermediate steps?.*)
1159 fun is_interpos (_, Res) = true
1160 | is_interpos _ = false;
1162 fun last_onlev pt pos = not (existpt (lev_on pos) pt);
1165 (*.find the position of the next parent which is a PblObj in ctree.*)
1166 fun par_pblobj pt [] = []
1168 let fun par pt [] = []
1169 | par pt p = if is_pblobj (get_obj I pt p) then p
1170 else par pt (lev_up p)
1171 in par pt (lev_up p) end;
1172 (* lev_up for hard_gen operating with pos = [...,0] *)
1174 (*.find the position and the children of the next parent which is a PblObj.*)
1175 fun par_children (Nd (PblObj _, children)) [] = (children, [])
1176 | par_children (pt as Nd (PblObj _, children)) p =
1177 let fun par [] = (children, [])
1178 | par p = let val Nd (obj, children) = get_nd pt p
1179 in if is_pblobj obj then (children, p) else par (lev_up p)
1181 in par (lev_up p) end;
1183 (*.get the children of a node in ctree.*)
1184 fun children (Nd (PblObj _, cn)) = cn
1185 | children (Nd (PrfObj _, cn)) = cn;
1188 (*.find the next parent, which is either a PblObj (return true)
1189 or a PrfObj with tac = Detail_Set (return false).*)
1190 (*FIXME.3.4.03:re-organize par_pbl_det after rls' --> rls*)
1191 fun par_pbl_det pt [] = (true, [], Erls)
1192 | par_pbl_det pt p =
1193 let fun par pt [] = (true, [], Erls)
1194 | par pt p = if is_pblobj (get_obj I pt p) then (true, p, Erls)
1195 else case get_obj g_tac pt p of
1196 (*Detail_Set rls' => (false, p, assoc_rls rls')
1197 (*^^^--- before 040206 after ---vvv*)
1198 |*)Rewrite_Set rls' => (false, p, assoc_rls rls')
1199 | Rewrite_Set_Inst (_, rls') =>
1200 (false, p, assoc_rls rls')
1201 | _ => par pt (lev_up p)
1202 in par pt (lev_up p) end;
1207 (*.get from the whole ctree by f : ppobj -> 'a.*)
1208 fun get_all f EmptyPtree = []
1209 | get_all f (Nd (b, [])) = [f b]
1210 | get_all f (Nd (b, bs)) = [f b] @ (get_alls f bs)
1211 and get_alls f [] = []
1212 | get_alls f pts = flat (map (get_all f) pts);
1215 (*.insert obj b into ctree at pos, ev.overwriting this pos.
1216 covers library.ML TODO.WN110315 rename*)
1217 fun insert_pt b EmptyPtree [] = Nd (b, [])
1218 | insert_pt b EmptyPtree _ = raise PTREE "insert_pt b Empty _"
1219 | insert_pt b (Nd ( _, _)) [] = raise PTREE "insert_pt b _ []"
1220 | insert_pt b (Nd (b', bs)) (p::[]) =
1221 Nd (b', repl_app bs p (Nd (b,[])))
1222 | insert_pt b (Nd (b', bs)) (p::ps) =
1223 Nd (b', repl_app bs p (insert_pt b (nth p bs) ps));
1225 > type ppobj = string;
1226 > tracing (pr_ctree prfn (!pt));
1227 (*val pt = Unsynchronized.ref Empty;*)
1228 pt:= insert_pt ("root'":ppobj) EmptyPtree [];
1229 pt:= insert_pt ("xx1":ppobj) (!pt) [1];
1230 pt:= insert_pt ("xx2":ppobj) (!pt) [2];
1231 pt:= insert_pt ("xx3":ppobj) (!pt) [3];
1232 pt:= insert_pt ("xx2.1":ppobj) (!pt) [2,1];
1233 pt:= insert_pt ("xx2.2":ppobj) (!pt) [2,2];
1234 pt:= insert_pt ("xx2.1.1":ppobj) (!pt) [2,1,1];
1235 pt:= insert_pt ("xx2.1.2":ppobj) (!pt) [2,1,2];
1236 pt:= insert_pt ("xx2.1.3":ppobj) (!pt) [2,1,3];
1239 (*.insert children to a node without children.*)
1240 (*compare: fun insert_pt*)
1241 fun ins_chn _ EmptyPtree _ = raise PTREE "ins_chn: EmptyPtree"
1242 | ins_chn ns (Nd _) [] = raise PTREE "ins_chn: pos = []"
1243 | ins_chn ns (Nd (b, bs)) (p::[]) =
1244 if p > length bs then raise PTREE "ins_chn: pos not existent"
1245 else let val Nd (b', bs') = nth p bs
1246 in if null bs' then Nd (b, repl_app bs p (Nd (b', ns)))
1247 else raise PTREE "ins_chn: pos mustNOT be overwritten" end
1248 | ins_chn ns (Nd (b, bs)) (p::ps) =
1249 Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps));
1251 (* print_depth 11;ins_chn;print_depth 3; ###insert_pt#########################*);
1254 (** apply f to obj at pos, f: ppobj -> ppobj **)
1256 fun appl_to_node f (Nd (b,bs)) = Nd (f b, bs);
1257 fun appl_obj f EmptyPtree [] = EmptyPtree
1258 | appl_obj f EmptyPtree _ = raise PTREE "appl_obj f Empty _"
1259 | appl_obj f (Nd (b, bs)) [] = Nd (f b, bs)
1260 | appl_obj f (Nd (b, bs)) (p::[]) =
1261 Nd (b, repl_app bs p (((appl_to_node f) o (nth p)) bs))
1262 | appl_obj f (Nd (b, bs)) (p::ps) =
1263 Nd (b, repl_app bs p (appl_obj f (nth p bs) (ps:pos)));
1265 (* for use by appl_obj *)
1266 fun repl_form f (PrfObj {cell=c,form= _,tac=tac,loc=loc,
1267 branch=branch,result=result,ostate=ostate}) =
1268 PrfObj {cell=c,form= f,tac=tac,loc=loc,
1269 branch=branch,result=result,ostate=ostate}
1270 | repl_form _ _ = raise PTREE "repl_form takes no PblObj";
1271 fun repl_pbl x (PblObj {cell=cell,origin=origin,fmz=fmz,
1272 spec=spec,probl=_,meth=meth,ctxt=ctxt,env=env,loc=loc,
1273 branch=branch,result=result,ostate=ostate}) =
1274 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl= x,
1275 meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1276 | repl_pbl _ _ = raise PTREE "repl_pbl takes no PrfObj";
1277 fun repl_met x (PblObj {cell=cell,origin=origin,fmz=fmz,
1278 spec=spec,probl=probl,meth=_,ctxt=ctxt,env=env,loc=loc,
1279 branch=branch,result=result,ostate=ostate}) =
1280 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
1281 meth= x,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1282 | repl_met _ _ = raise PTREE "repl_pbl takes no PrfObj";
1284 fun repl_spec x (PblObj {cell=cell,origin=origin,fmz=fmz,
1285 spec= _,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
1286 branch=branch,result=result,ostate=ostate}) =
1287 PblObj {cell=cell,origin=origin,fmz=fmz,spec= x,probl=probl,
1288 meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1289 | repl_spec _ _ = raise PTREE "repl_domID takes no PrfObj";
1290 fun repl_domID x (PblObj {cell=cell,origin=origin,fmz=fmz,
1291 spec=(_,p,m),probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
1292 branch=branch,result=result,ostate=ostate}) =
1293 PblObj {cell=cell,origin=origin,fmz=fmz,spec=(x,p,m),probl=probl,
1294 meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1295 | repl_domID _ _ = raise PTREE "repl_domID takes no PrfObj";
1296 fun repl_pblID x (PblObj {cell=cell,origin=origin,fmz=fmz,
1297 spec=(d,_,m),probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
1298 branch=branch,result=result,ostate=ostate}) =
1299 PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,x,m),probl=probl,
1300 meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1301 | repl_pblID _ _ = raise PTREE "repl_pblID takes no PrfObj";
1302 fun repl_metID x (PblObj {cell=cell,origin=origin,fmz=fmz,
1303 spec=(d,p,_),probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
1304 branch=branch,result=result,ostate=ostate}) =
1305 PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,p,x),probl=probl,
1306 meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1307 | repl_metID _ _ = raise PTREE "repl_metID takes no PrfObj";
1309 fun repl_result l f' s (PrfObj {cell=cell,form=form,tac=tac,loc=_,
1310 branch=branch,result = _ ,ostate = _}) =
1311 PrfObj {cell=cell,form=form,tac=tac,loc= l,
1312 branch=branch,result = f',ostate = s}
1313 | repl_result l f' s (PblObj {cell=cell,origin=origin,fmz=fmz,
1314 spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=_,
1315 branch=branch,result= _ ,ostate= _}) =
1316 PblObj {cell=cell,origin=origin,fmz=fmz,
1317 spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc= l,
1318 branch=branch,result= f',ostate= s};
1320 fun repl_tac x (PrfObj {cell=cell,form=form,tac= _,loc=loc,
1321 branch=branch,result=result,ostate=ostate}) =
1322 PrfObj {cell=cell,form=form,tac= x,loc=loc,
1323 branch=branch,result=result,ostate=ostate}
1324 | repl_tac _ _ = raise PTREE "repl_tac takes no PblObj";
1326 fun repl_branch b (PblObj {cell=cell,origin=origin,fmz=fmz,
1327 spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
1328 branch= _,result=result,ostate=ostate}) =
1329 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
1330 meth=meth,ctxt=ctxt,env=env,loc=loc,branch= b,result=result,ostate=ostate}
1331 | repl_branch b (PrfObj {cell=cell,form=form,tac=tac,loc=loc,
1332 branch= _,result=result,ostate=ostate}) =
1333 PrfObj {cell=cell,form=form,tac=tac,loc=loc,
1334 branch= b,result=result,ostate=ostate};
1337 (PblObj {cell, origin, fmz, spec, probl, meth,
1338 ctxt=_, env, loc, branch, result, ostate}) =
1339 PblObj {cell=cell, origin=origin, fmz=fmz, spec=spec, probl=probl, meth=meth,
1340 ctxt=x, env=env, loc=loc, branch=branch, result=result, ostate=ostate}
1341 | repl_ctxt _ _ = raise PTREE "repl_env takes no PrfObj";
1344 (PblObj {cell=cell, origin=origin, fmz=fmz, spec=spec, probl=probl, meth=meth,
1345 ctxt=ctxt, env=_, loc=loc, branch=branch, result=result, ostate=ostate}) =
1346 PblObj {cell=cell, origin=origin, fmz=fmz, spec=spec, probl=probl, meth=meth,
1347 ctxt=ctxt, env=e, loc=loc, branch=branch, result=result, ostate=ostate}
1348 | repl_env _ _ = raise PTREE "repl_env takes no PrfObj";
1351 (PblObj {cell=cell,origin=(_,spe,hdf),fmz=fmz,
1352 spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
1353 branch=branch,result=result,ostate=ostate}) =
1354 PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,
1355 meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,
1356 result=result,ostate=ostate}
1357 | repl_oris _ _ = raise PTREE "repl_oris takes no PrfObj";
1358 fun repl_orispec spe
1359 (PblObj {cell=cell,origin=(oris,_,hdf),fmz=fmz,
1360 spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
1361 branch=branch,result=result,ostate=ostate}) =
1362 PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,
1363 meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,
1364 result=result,ostate=ostate}
1365 | repl_orispec _ _ = raise PTREE "repl_orispec takes no PrfObj";
1367 fun repl_loc l (PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,
1368 ctxt=ctxt,env=env,loc=_,branch=branch,result=result,ostate=ostate}) =
1369 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,
1370 ctxt=ctxt,env=env,loc=l,branch=branch,result=result,ostate=ostate}
1371 | repl_loc l (PrfObj {cell=cell,form=form,tac=tac,
1372 loc=_,branch=branch,result=result,ostate=ostate}) =
1373 PrfObj {cell=cell,form=form,tac=tac,
1374 loc= l,branch=branch,result=result,ostate=ostate};
1376 (*WN050219 put here for interpreting code for cut_tree below...*)
1378 bool * (*ALL itms+preconds true*)
1379 pos_ * (*model belongs to Problem | Method*)
1380 term * (*header: Problem... or Cas
1381 FIXXXME.12.03: item! for marking syntaxerrors*)
1382 itm list * (*model: given, find, relate*)
1383 ((bool * term) list) *(*model: preconds*)
1384 spec; (*specification*)
1385 val e_ocalhd = (false, Und, e_term, [e_itm], [(false, e_term)], e_spec);
1387 datatype ptform = Form of term | ModSpec of ocalhd;
1388 val e_ptform = Form e_term;
1389 val e_ptform' = ModSpec e_ocalhd;
1391 (*.applies (snd f) to the branches at a pos if ((fst f) b),
1392 f : (ppobj -> bool) * (int -> ctree list -> ctree list).*)
1394 fun appl_branch f EmptyPtree [] = (EmptyPtree, false)
1395 | appl_branch f EmptyPtree _ = raise PTREE "appl_branch f Empty _"
1396 | appl_branch f (Nd ( _, _)) [] = raise PTREE "appl_branch f _ []"
1397 | appl_branch f (Nd (b, bs)) (p::[]) =
1398 if (fst f) b then (Nd (b, (snd f) p bs), true)
1399 else (Nd (b, bs), false)
1400 | appl_branch f (Nd (b, bs)) (p::ps) =
1401 let val (b',bool) = appl_branch f (nth p bs) ps
1402 in (Nd (b, repl_app bs p b'), bool) end;
1404 (* for cut_level; appl_branch(deprecated) *)
1405 fun test_trans (PrfObj{branch = Transitive,...}) = true
1406 | test_trans (PblObj{branch = Transitive,...}) = true
1407 | test_trans _ = false;
1409 fun is_pblobj' pt p =
1410 let val ppobj = get_obj I pt p
1411 in is_pblobj ppobj end;
1413 fun delete_result pt p =
1414 (appl_obj (repl_result (fst (get_obj g_loc pt p), NONE)
1415 (e_term,[]) Incomplete) pt p);
1417 fun del_res (PblObj {cell, fmz, origin, spec, probl, meth,
1418 ctxt, env, loc=(l1,_), branch, result, ostate}) =
1419 PblObj {cell=cell,fmz=fmz,origin=origin,spec=spec,probl=probl,meth=meth,
1420 ctxt=ctxt,env=env, loc=(l1,NONE), branch=branch, result=(e_term,[]),
1423 | del_res (PrfObj {cell, form, tac, loc=(l1,_), branch, result, ostate}) =
1424 PrfObj {cell=cell,form=form,tac=tac, loc=(l1,NONE), branch=branch,
1425 result=(e_term,[]), ostate=Incomplete};
1427 (*FIXME.WN0312 update_X X pos pt -> pt could be chained by o (efficiency?)*)
1428 (*fun update_fmz pt pos x = appl_obj (repl_fmz x) pt pos; WN01xx *)
1429 fun update_ctxt pt pos x = appl_obj (repl_ctxt x) pt pos; (*for use on PblObj,
1430 otherwise use fun generate1; compare fun get_ctxt*)
1431 fun update_env pt pos x = appl_obj (repl_env x) pt pos;
1432 fun update_domID pt pos x = appl_obj (repl_domID x) pt pos;
1433 fun update_pblID pt pos x = appl_obj (repl_pblID x) pt pos;
1434 fun update_metID pt pos x = appl_obj (repl_metID x) pt pos;
1435 fun update_spec pt pos x = appl_obj (repl_spec x) pt pos;
1436 fun update_pbl pt pos x = appl_obj (repl_pbl x) pt pos;
1437 fun update_pblppc pt pos x = appl_obj (repl_pbl x) pt pos;
1438 fun update_met pt pos x = appl_obj (repl_met x) pt pos;
1439 fun update_metppc pt pos x = appl_obj (repl_met x) pt pos;
1440 fun update_branch pt pos x = appl_obj (repl_branch x) pt pos;
1441 fun update_tac pt pos x = appl_obj (repl_tac x) pt pos;
1442 fun update_oris pt pos x = appl_obj (repl_oris x) pt pos;
1443 fun update_orispec pt pos x = appl_obj (repl_orispec x) pt pos;
1445 (*WN050305 for handling cut_tree in cappend_atomic + for testing*)
1446 fun update_loc' pt pos x = appl_obj (repl_loc x) pt pos;
1448 (*13.8.02: options, because istate is no equalitype any more*)
1449 fun get_loc EmptyPtree _ = (e_istate, e_ctxt)
1450 | get_loc pt (p,Res) =
1451 (case get_obj g_loc pt p of
1453 | (NONE , NONE) => (e_istate, e_ctxt)
1454 | (_ , SOME i) => i)
1455 | get_loc pt (p,_) =
1456 (case get_obj g_loc pt p of
1457 (NONE , SOME i) => i (*13.8.02 just copied from ^^^: too liberal ?*)
1458 | (NONE , NONE) => (e_istate, e_ctxt)
1459 | (SOME i, _) => i);
1460 fun get_istate pt p = get_loc pt p |> #1;
1461 fun get_ctxt pt (pos as (p, p_)) =
1462 if member op = [Frm, Res] p_
1463 then get_loc pt pos |> #2 (*for script interpretation rely on fun get_loc*)
1464 else get_obj g_ctxt pt p (*for specify phase take ctx from PblObj*)
1466 fun get_assumptions_ pt p = get_ctxt pt p |> get_assumptions;
1468 (*pos of the formula on FE relative to the current pos,
1469 which is the next writepos*)
1472 let val (ps,p) = split_last pp
1473 in case p of 1 => ps | n => ps @ [n-1] end;
1475 (*WN.20.5.03 ... but not used*)
1476 fun posless [] (_::_) = true
1477 | posless (_::_) [] = false
1478 | posless (p::ps) (q::qs) = if p = q then posless ps qs else p < q;
1479 (* posless [2,3,4] [3,4,5];
1481 > posless [2,3,4] [1,2,3];
1483 > posless [2,3] [2,3,4];
1485 > posless [2,3,4] [2,3];
1487 > posless [6] [6,5,2];
1489 +++ see Isabelle/../library.ML*)
1492 (**.development for extracting an 'interval' from ctree.**)
1494 (*WN0510 version stopped in favour of get_interval with !!!move_dn, getFormulaeFromTo
1495 actually used (inefficient) version with move_dn: see modspec.sml*)
1498 fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*)
1499 fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)
1500 fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x;
1501 fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
1503 fun getnd i (b,p) q (Nd (po, nds)) =
1504 (if i <= 0 then [[b]] else []) @
1505 (getnds (i-1) true (b@[hdp p], tlp p) (tlq q)
1506 (take_fromto (hdp p) (hdq q) nds))
1508 and getnds _ _ _ _ [] = [] (*no children*)
1509 | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)
1511 | getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*)
1512 (getnd i ( b, p ) [99999] n1) @
1513 (getnd ~99999 (lev_on b,[0]) q n2)
1515 | getnds i _ (b,p) q [n1, n2] = (*intern, r-margin*)
1516 (getnd i ( b,[0]) [99999] n1) @
1517 (getnd ~99999 (lev_on b,[0]) q n2)
1519 | getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*)
1520 (getnd i ( b, p ) [99999] nd) @
1521 (getnds ~99999 false (lev_on b,[0]) q nds)
1523 | getnds i _ (b,p) q (nd::(nds as _::_)) = (*intern, ...*)
1524 (getnd i ( b,[0]) [99999] nd) @
1525 (getnds ~99999 false (lev_on b,[0]) q nds);
1527 (*get an 'interval from to' from a ctree as 'intervals f t' of respective nodes
1528 where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
1529 (1) the 'f' are given
1530 (1a) by 'from' if 'f' = the respective element of 'from' (left margin)
1531 (1b) -inifinity, if 'f' > the respective element of 'from' (internal node)
1532 (2) the 't' ar given
1533 (2a) by 'to' if 't' = the respective element of 'to' (right margin)
1534 (2b) inifinity, if 't' < the respective element of 'to (internal node)'
1535 the 'f' and 't' are set by hdp,... *)
1536 fun get_trace pt p q =
1537 (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q)))
1538 (take_fromto (hdp p) (hdq q) (children pt));
1541 fun get_somespec (dI,pI,mI) (dI',pI',mI') =
1542 let val domID = if dI = e_domID
1543 then if dI' = e_domID
1544 then error"pt_extract: no domID in probl,origin"
1547 val pblID = if pI = e_pblID
1548 then if pI' = e_pblID
1549 then error"pt_extract: no pblID in probl,origin"
1552 val metID = if mI = e_metID
1553 then if pI' = e_metID
1554 then error"pt_extract: no metID in probl,origin"
1557 in (domID, pblID, metID) end;
1558 fun get_somespec' (dI,pI,mI) (dI',pI',mI') =
1559 let val domID = if dI = e_domID then dI' else dI
1560 val pblID = if pI = e_pblID then pI' else pI
1561 val metID = if mI = e_metID then mI' else mI
1562 in (domID, pblID, metID) end;
1564 (*extract a formula or model from ctree for itms2itemppc or model2xml*)
1565 fun preconds2str bts =
1566 (strs2str o (map (linefeed o pair2str o
1568 (apfst bool2str)))) bts;
1569 fun ocalhd2str (b, p, hdf, itms, prec, spec) =
1570 "("^bool2str b^", "^pos_2str p^", "^term2str hdf^
1571 ", "^itms2str_ (thy2ctxt' "Isac") itms^
1572 ", "^preconds2str prec^", \n"^spec2str spec^" )";
1576 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj;
1579 (**.functions for the 'ctree iterator' as seen from the FE-Kernel interface.**)
1581 (*move one step down into existing nodes of ctree; regard TransitiveB
1582 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~##################
1583 fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*)
1584 (* val (Nd (c, ns), ([],p_)) = (pt, get_pos cI uI);
1587 then case p_ of (*Frm => ([], Pbl) 1.12.03
1588 |*) Res => raise PTREE "move_dn: end of calculation"
1589 | _ => if null ns (*go down from Pbl + Met*)
1590 then raise PTREE "move_dn: solve problem not started"
1592 else (case p_ of Res => raise PTREE "move_dn: end of (sub-)tree"
1594 then raise PTREE "move_dn: pos not existent 1"
1597 (*iterate towards end of pos*)
1598 (* val (P,(Nd (_, ns)),(p::(ps as (_::_)),p_)) = ([]:pos, pt, get_pos cI uI);
1599 val (P,(Nd (_, ns)),(p::(ps as (_::_)),p_)) = ((P@[p]),(nth p ns),(ps, p_));
1601 | move_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
1602 if p > length ns then raise PTREE "move_dn: pos not existent 2"
1603 else move_dn ((P@[p]): pos) (nth p ns) (ps, p_)
1604 (* val (P, (Nd (c, ns)), ([p], p_)) = ((P@[p]), (nth p ns), (ps, p_));
1605 val (P, (Nd (c, ns)), ([p], p_)) = ([],pt,get_pos cI uI);
1607 | move_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1608 if p > length ns then raise PTREE "move_dn: pos not existent 3"
1609 else if is_pblnd (nth p ns) then
1610 ((*tracing("### move_dn: is_pblnd (nth p ns), P= "^ints2str' P^", \n"^
1611 "length ns= "^((string_of_int o length) ns)^
1612 ", p= "^string_of_int p^", p_= "^pos_2str p_);*)
1613 case p_ of Res => if p = length ns
1614 then if g_ostate c = Complete then (P, Res)
1615 else raise PTREE (ints2str' P^" not complete")
1616 (*FIXME here handle not-sequent-branches*)
1617 else if g_branch c = TransitiveB
1618 andalso (not o is_pblnd o (nth (p+1))) ns
1620 else (P@[p+1], if is_pblnd (nth (p+1) ns)
1622 | _ => if (null o children o (nth p)) ns (*go down from Pbl*)
1623 then raise PTREE "move_dn: solve subproblem not started"
1625 if (is_pblnd o hd o children o (nth p)) ns
1628 (* val (P, Nd (c, ns), ([p], p_)) = ([], pt, ([1], Frm));
1630 else case p_ of Frm => if (null o children o (nth p)) ns
1631 (*then if g_ostate c = Complete then (P@[p],Res)*)
1632 then if g_ostate' (nth p ns) = Complete
1634 else raise PTREE "move_dn: pos not existent 4"
1635 else (P @ [p, 1], (*go down*)
1636 if (is_pblnd o hd o children o (nth p)) ns
1638 | Res => if p = length ns
1640 if g_ostate c = Complete then (P, Res)
1641 else raise PTREE (ints2str' P^" not complete")
1643 if g_branch c = TransitiveB
1644 andalso (not o is_pblnd o (nth (p+1))) ns
1645 then if (null o children o (nth (p+1))) ns
1647 else (P@[p+1,1], Frm)(*040221*)
1648 else (P@[p+1], if is_pblnd (nth (p+1) ns)
1651 (*.move one step down into existing nodes of ctree; skip Res = Frm.nxt;
1652 move_dn at the end of the calc-tree raises PTREE.*)
1653 fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*)
1655 Res => raise PTREE "move_dn: end of calculation"
1656 | _ => if null ns (*go down from Pbl + Met*)
1657 then raise PTREE "move_dn: solve problem not started"
1659 | move_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =(*iterate to end of pos*)
1660 if p > length ns then raise PTREE "move_dn: pos not existent 2"
1661 else move_dn (P@[p]) (nth p ns) (ps, p_)
1663 | move_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1664 if p > length ns then raise PTREE "move_dn: pos not existent 3"
1667 if p = length ns (*last Res on this level: go a level up*)
1668 then if g_ostate c = Complete then (P, Res)
1669 else raise PTREE (ints2str' P^" not complete 1")
1670 else (*go to the next Nd on this level, or down into the next Nd*)
1671 if is_pblnd (nth (p+1) ns) then (P@[p+1], Pbl)
1673 if g_res' (nth p ns) = g_form' (nth (p+1) ns)
1674 then if (null o children o (nth (p+1))) ns
1675 then (*take the Res if Complete*)
1676 if g_ostate' (nth (p+1) ns) = Complete
1678 else raise PTREE (ints2str' (P@[p+1])^
1680 else (P@[p+1,1], Frm)(*go down into the next PrfObj*)
1681 else (P@[p+1], Frm)(*take Frm: exists if the Nd exists*)
1682 | Frm => (*go down or to the Res of this Nd*)
1683 if (null o children o (nth p)) ns
1684 then if g_ostate' (nth p ns) = Complete then (P @ [p], Res)
1685 else raise PTREE (ints2str' (P @ [p])^" not complete 3")
1686 else (P @ [p, 1], Frm)
1687 | _ => (*is Pbl or Met*)
1688 if (null o children o (nth p)) ns
1689 then raise PTREE "move_dn:solve subproblem not startd"
1691 if (is_pblnd o hd o children o (nth p)) ns
1695 (*.go one level down into ctree.*)
1696 fun movelevel_dn [] (Nd (c, ns)) ([],p_) = (*root problem*)
1699 then raise PTREE "solve problem not started"
1700 else ([1], if (is_pblnd o hd) ns then Pbl else Frm)
1701 else raise PTREE "pos not existent 1"
1703 (*iterate towards end of pos*)
1704 | movelevel_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
1705 if p > length ns then raise PTREE "pos not existent 2"
1706 else movelevel_dn (P@[p]) (nth p ns) (ps, p_)
1708 | movelevel_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1709 if p > length ns then raise PTREE "pos not existent 3" else
1712 then raise PTREE "no children"
1714 if g_branch c = TransitiveB
1715 then if (null o children o (nth (p+1))) ns
1716 then raise PTREE "no children"
1718 if (is_pblnd o hd o children o (nth (p+1))) ns
1720 else if (null o children o (nth p)) ns
1721 then raise PTREE "no children"
1722 else (P @ [p, 1], if (is_pblnd o hd o children o (nth p)) ns
1724 | _ => if (null o children o (nth p)) ns
1725 then raise PTREE "no children"
1726 else (P @ [p, 1], (*go down*)
1727 if (is_pblnd o hd o children o (nth p)) ns
1732 (*.go to the previous position in ctree; regard TransitiveB.*)
1733 fun move_up _ (Nd (c, ns)) ([],p_) = (*root problem*)
1735 then case p_ of Res => if null ns then ([], Pbl) (*Res -> Pbl (not Met)!*)
1736 else ([length ns], Res)
1737 | _ => raise PTREE "begin of calculation"
1738 else raise PTREE "pos not existent"
1740 | move_up P (Nd (_, ns)) (p::(ps as (_::_)),p_) = (*iterate to end of pos*)
1741 if p > length ns then raise PTREE "pos not existent"
1742 else move_up (P@[p]) (nth p ns) (ps,p_)
1744 | move_up P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1745 if p > length ns then raise PTREE "pos not existent"
1746 else if is_pblnd (nth p ns) then
1748 let val nc = (length o children o (nth p)) ns
1749 in if nc = 0 then (P@[p], Pbl) (*Res -> Pbl (not Met)!*)
1750 else (P @ [p, nc], Res) end (*go down*)
1751 | _ => if p = 1 then (P, Pbl) else (P@[p-1], Res)
1752 else case p_ of Frm => if p <> 1 then (P, Frm)
1753 else if is_pblobj c then (P, Pbl) else (P, Frm)
1755 let val nc = (length o children o (nth p)) ns
1756 in if nc = 0 (*cannot go down*)
1757 then if g_branch c = TransitiveB andalso p <> 1
1758 then (P@[p-1], Res) else (P@[p], Frm)
1759 else (P @ [p, nc], Res) end; (*go down*)
1763 (*.go one level up in ctree; sets the position on Frm.*)
1764 fun movelevel_up _ (Nd (c, ns)) (([],p_):pos') = (*root problem*)
1765 raise PTREE "pos not existent"
1767 (*iterate towards end of pos*)
1768 | movelevel_up P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
1769 if p > length ns then raise PTREE "pos not existent"
1770 else movelevel_up (P@[p]) (nth p ns) (ps,p_)
1772 | movelevel_up P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1773 if p > length ns then raise PTREE "pos not existent"
1774 else if is_pblobj c then (P, Pbl) else (P, Frm);
1777 (*.go to the next calc-head up in the calc-tree.*)
1778 fun movecalchd_up pt ((p, Res):pos') =
1779 (par_pblobj pt p, Pbl):pos'
1780 | movecalchd_up pt (p, _) =
1781 if is_pblobj (get_obj I pt p)
1782 then (p, Pbl) else (par_pblobj pt p, Pbl);
1784 (*.determine the previous pos' on the same level.*)
1785 (*WN0502 made for interSteps; _only_ works for branch TransitiveB WN120517 compare lev_back*)
1786 fun lev_pred' pt (pos:pos' as ([],Res)) = ([],Pbl):pos'
1787 | lev_pred' pt (pos:pos' as (p, Res)) =
1788 let val (p', last) = split_last p
1790 then if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm)
1791 else if get_obj g_res pt (p' @ [last - 1]) = get_obj g_form pt p
1792 then (p' @ [last - 1], Res) (*TransitiveB*)
1793 else if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm)
1797 (*.determine the next pos' on the same level.*)
1798 fun lev_on' pt (([],Pbl):pos') = ([],Res):pos'
1799 | lev_on' pt (p, Res) =
1800 if get_obj g_res pt p = get_obj g_form pt (lev_on p)(*TransitiveB*)
1801 then if existpt' (lev_on p, Res) pt then (lev_on p, Res)
1802 else error ("lev_on': (p, Res) -> (p, Res) not existent, \
1803 \p = "^ints2str' (lev_on p))
1804 else (lev_on p, Frm)
1805 | lev_on' pt (p, _) =
1806 if existpt' (p, Res) pt then (p, Res)
1807 else error ("lev_on': (p, Frm) -> (p, Res) not existent, \
1808 \p = "^ints2str' p);
1810 fun exist_lev_on' pt p = (lev_on' pt p; true) handle _ => false;
1812 (*.is the pos' at the last element of a calulation _AND_ can be continued.*)
1813 (* val (pt, pos as (p,p_)) = (pt, ([1],Frm));
1815 fun is_curr_endof_calc pt (([],Res) : pos') = false
1816 | is_curr_endof_calc pt (pos as (p,_)) =
1817 not (exist_lev_on' pt pos)
1818 andalso get_obj g_ostate pt (lev_up p) = Incomplete;
1821 (**.insert into ctree and cut branches accordingly.**)
1823 (*.get all positions of certain intervals on the ctree.*)
1824 (*OLD VERSION without move_dn; kept for occasional redesign
1825 get all pos's to be cut in a ctree
1826 below a pos or from a ctree list after i-th element (NO level_up).*)
1827 fun get_allpos' (_:pos, _:posel) EmptyPtree = ([]:pos' list)
1828 | get_allpos' (p, 1) (Nd (b, bs)) = (*p is pos of Nd*)
1829 if g_ostate b = Incomplete
1830 then ((*tracing("get_allpos' (p, 1) Incomplete: p="^ints2str' p);*)
1831 [(p,Frm)] @ (get_allpos's (p, 1) bs)
1833 else ((*tracing("get_allpos' (p, 1) else: p="^ints2str' p);*)
1834 [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)]
1836 (*WN041020 here we assume what is presented on the worksheet ?!*)
1837 | get_allpos' (p, i) (Nd (b, bs)) = (*p is pos of Nd*)
1838 if length bs > 0 orelse is_pblobj b
1839 then if g_ostate b = Incomplete
1840 then [(p,Frm)] @ (get_allpos's (p, 1) bs)
1841 else [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)]
1843 if g_ostate b = Incomplete
1846 (*WN041020 here we assume what is presented on the worksheet ?!*)
1847 and get_allpos's _ [] = []
1848 | get_allpos's (p, i) (pt::pts) = (*p is pos of parent-Nd*)
1849 (get_allpos' (p@[i], i) pt) @ (get_allpos's (p, i+1) pts);
1851 (*.get all positions of certain intervals on the ctree.*)
1852 (*NEW version WN050225*)
1856 (*before WN041019......
1857 val cut_branch = (test_trans, curry take):
1858 (ppobj -> bool) * (int -> ctree list -> ctree list);
1859 .. formlery used for ...
1860 fun cut_tree''' _ [] = EmptyPtree
1861 | cut_tree''' pt pos =
1862 let val (pt',cut) = appl_branch cut_branch pt pos
1863 in if cut andalso length pos > 1 then cut_tree''' pt' (lev_up pos)
1866 (*OLD version before WN050225*)
1867 (*WN050106 like cut_level, but deletes exactly 1 node --- for tests ONLY*)
1868 fun cut_level_'_ (_:pos' list) (_:pos) EmptyPtree (_:pos') =
1869 raise PTREE "cut_level_'_ Empty _"
1870 | cut_level_'_ _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level_'_ _ []"
1871 | cut_level_'_ cuts P (Nd (b, bs)) (p::[],p_) =
1873 then (Nd (b, drop_nth [] (p:posel, bs)),
1876 (if p_ = Frm then [(P@[p],Res)] else ([]:pos' list)) @
1877 (*WN041020 here we assume what is presented on the worksheet ?!*)
1878 (get_allpos's (P, p+1) (drop_nth [] (p, bs))))
1880 else (Nd (b, bs), cuts)
1881 | cut_level_'_ cuts P (Nd (b, bs)) ((p::ps),p_) =
1882 let val (bs',cuts') = cut_level_'_ cuts P (nth p bs) (ps, p_)
1883 in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
1886 fun cut_level (_:pos' list) (_:pos) EmptyPtree (_:pos') =
1887 raise PTREE "cut_level EmptyPtree _"
1888 | cut_level _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level _ []"
1890 | cut_level cuts P (Nd (b, bs)) (p::[],p_) =
1892 then (Nd (b, take (p:posel, bs)),
1894 (if p_ = Frm andalso (*#*) g_ostate b = Complete
1895 then [(P@[p],Res)] else ([]:pos' list)) @
1896 (*WN041020 here we assume what is presented on the worksheet ?!*)
1897 (get_allpos's (P, p+1) (takerest (p, bs))))
1898 else (Nd (b, bs), cuts)
1900 | cut_level cuts P (Nd (b, bs)) ((p::ps),p_) =
1901 let val (bs',cuts') = cut_level cuts P (nth p bs) (ps, p_)
1902 in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
1904 (*OLD version before WN050219, overwritten below*)
1905 fun cut_tree _ (([],_):pos') = raise PTREE "cut_tree _ ([],_)"
1906 | cut_tree pt (pos as ([p],_)) =
1907 let val (pt', cuts) = cut_level ([]:pos' list) [] pt pos
1908 in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
1909 then [] else [([],Res)])) end
1910 | cut_tree pt (p,p_) =
1912 fun cutfn pt cuts (p,p_) =
1913 let val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_)
1914 val cuts'' = if get_obj g_ostate pt (lev_up p) = Incomplete
1915 then [] else [(lev_up p, Res)]
1916 in if length cuts' > 0 andalso length p > 1
1917 then cutfn pt' (cuts @ cuts') (lev_up p, Frm(*-->(p,Res)*))
1918 else (pt',cuts @ cuts') end
1919 val (pt', cuts) = cutfn pt [] (p,p_)
1920 in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
1921 then [] else [([], Res)])) end;
1924 (*########/ inserted from ctreeNEW.sml \#################################**)
1926 (*.get all positions in a ctree until ([],Res) or ostate=Incomplete
1928 pos' list -> : accumulated, start with []
1929 pos -> : the offset for subtrees wrt the root
1930 ctree -> : (sub)tree
1931 pos' : initialization (the last pos' before ...)
1932 -> pos' list : of positions in this (sub) tree (relative to the root)
1934 (* val (cuts, P, pt, pos) = ([], [3], get_nd pt [3], ([], Frm):pos');
1935 val (cuts, P, pt, pos) = ([], [2], get_nd pt [2], ([], Frm):pos');
1936 length (children pt);
1938 fun get_allp (cuts:pos' list) (P:pos, pos:pos') pt =
1939 (let val nxt = move_dn [] pt pos (*exn if Incomplete reached*)
1940 in if nxt <> ([],Res)
1941 then get_allp (cuts @ [nxt]) (P, nxt) pt
1942 else (map (apfst (curry op@ P)) (cuts @ [nxt])): pos' list
1943 end) handle PTREE _ => (map (apfst (curry op@ P)) cuts);
1946 (*the pts are assumed to be on the same level*)
1947 fun get_allps (cuts: pos' list) (P:pos) [] = cuts
1948 | get_allps cuts P (pt::pts) =
1949 let val below = get_allp [] (P, ([], Frm)) pt
1952 then (P, Pbl)::below
1953 else if last_elem P = 1
1954 then (P, Frm)::below
1955 else (*Trans*) below
1956 val levres = levfrm @ (if null below then [(P, Res)] else [])
1957 in get_allps (cuts @ levres) (lev_on P) pts end;
1960 (**.these 2 funs decide on how far cut_tree goes.**)
1961 (*.shall the nodes _after_ the pos to be inserted at be deleted?.*)
1962 fun test_trans (PrfObj{branch = Transitive,...}) = true
1963 | test_trans (PrfObj{branch = NoBranch,...}) = true
1964 | test_trans (PblObj{branch = Transitive,...}) = true
1965 | test_trans (PblObj{branch = NoBranch,...}) = true
1966 | test_trans _ = false;
1967 (*.shall cutting be continued on the higher level(s)?
1968 the Nd regarded will NOT be changed.*)
1969 fun cutlevup (PblObj _) = false (*for tests of LK0502*)
1970 | cutlevup _ = true;
1971 val cutlevup = test_trans;(*WN060727 after summerterm tests.LK0502 withdrawn*)
1973 (*cut_bottom new sml603..608
1974 cut the level at the bottom of the pos (used by cappend_...)
1975 and handle the parent in order to avoid extra case for root
1976 fn: ctree -> : the _whole_ ctree for cut_levup
1977 pos * posel -> : the pos after split_last
1978 ctree -> : the parent of the Nd to be cut
1980 (ctree * : the updated ctree
1981 pos' list) * : the pos's cut
1982 bool : cutting shall be continued on the higher level(s)
1984 fun cut_bottom _ (pt' as Nd (b, [])) = ((pt', []), cutlevup b)
1985 | cut_bottom (P:pos, p:posel) (Nd (b, bs)) =
1986 let (*divide level into 3 parts...*)
1987 val keep = take (p - 1, bs)
1988 val pt' as Nd (_,bs') = nth p bs
1989 (*^^^^^_here_ will be 'insert_pt'ed by 'append_..'*)
1990 val (tail, tp) = (takerest (p, bs),
1991 if null (takerest (p, bs)) then 0 else p + 1)
1992 val (children, cuts) =
1995 (if is_pblnd pt' then [(P @ [p], Pbl)] else [])
1996 @ (get_allp [] (P @ [p], (P, Frm)) pt')
1997 @ (get_allps [] (P @ [p+1]) tail))
1998 else (keep @ [(*'insert_pt'ed by 'append_..'*)] @ tail,
1999 get_allp [] (P @ [p], (P, Frm)) pt')
2002 then (Nd (del_res b, children),
2003 cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
2004 else (Nd (b, children), cuts)
2005 (*val _= tracing("####cut_bottom (P, p)="^pos2str (P @ [p])^
2006 ", Nd=.............................................")
2008 val _= tracing("####cut_bottom form='"^
2009 term2str (get_obj g_form pt'' []))
2010 val _= tracing("####cut_bottom cuts#="^string_of_int (length cuts)^
2011 ", cuts="^pos's2str cuts)*)
2012 in ((pt'', cuts:pos' list), cutlevup b) end;
2015 (*.go all levels from the bottom of 'pos' up to the root,
2016 on each level compose the children of a node and accumulate the cut Nds
2018 pos' list -> : for accumulation
2019 bool -> : cutting shall be continued on the higher level(s)
2020 ctree -> : the whole ctree for 'get_nd pt P' on each level
2021 ctree -> : the Nd from the lower level for insertion at path
2022 pos * posel -> : pos=path split for convenience
2023 ctree -> : Nd the children of are under consideration on this call
2025 ctree * pos' list : the updated parent-Nd and the pos's of the Nds cut
2027 fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) =
2028 let (*divide level into 3 parts...*)
2029 val keep = take (p - 1, bs)
2030 (*val pt' comes as argument from below*)
2031 val (tail, tp) = (takerest (p, bs),
2032 if null (takerest (p, bs)) then 0 else p + 1)
2033 val (children, cuts') =
2035 then (keep @ [pt'], get_allps [] (P @ [p+1]) tail)
2036 else (keep @ [pt'] @ tail, [])
2037 val clevup' = if clevup then cutlevup b else false
2038 (*the first Nd with false stops cutting on all levels above*)
2041 then (Nd (del_res b, children),
2042 cuts' @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
2043 else (Nd (b, children), cuts')
2044 (*val _= tracing("#####cut_levup clevup= "^bool2str clevup)
2045 val _= tracing("#####cut_levup cutlevup b= "^bool2str (cutlevup b))
2046 val _= tracing("#####cut_levup (P, p)="^pos2str (P @ [p])^
2047 ", Nd=.............................................")
2049 val _= tracing("#####cut_levup form='"^
2050 term2str (get_obj g_form pt'' []))
2051 val _= tracing("#####cut_levup cuts#="^string_of_int (length cuts)^
2052 ", cuts="^pos's2str cuts)*)
2053 in if null P then (pt'', (cuts @ cuts'):pos' list)
2054 else let val (P, p) = split_last P
2055 in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P)
2059 (*.cut nodes after and below an inserted node in the ctree;
2060 the cuts range is limited by the predicate 'fun cutlevup'.*)
2061 fun cut_tree pt (pos,_) =
2062 if not (existpt pos pt)
2063 then (pt,[]) (*appending a formula never cuts anything*)
2064 else let val (P, p) = split_last pos
2065 val ((pt', cuts), clevup) = cut_bottom (P, p) (get_nd pt P)
2066 (* pt' is the updated parent of the Nd to cappend_..*)
2067 in if null P then (pt', cuts)
2068 else let val (P, p) = split_last P
2069 in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P)
2073 fun append_atomic p l f r f' s pt =
2074 let (**val _= tracing("#@append_atomic: pos ="^pos2str p)**)
2075 val (iss, f) = if existpt p pt andalso is_empty_tac (get_obj g_tac pt p)
2077 ((fst (get_obj g_loc pt p), SOME l),
2078 get_obj g_form pt p)
2079 else ((NONE, SOME l), f)
2080 in insert_pt (PrfObj {cell = NONE,
2086 ostate= s}) pt p end;
2089 (*20.8.02: cappend_* FIXXXXME cut branches below cannot be decided here:
2090 detail - generate - cappend: inserted, not appended !!!
2092 cut decided in applicable_in !?!
2094 fun cappend_atomic pt p loc f r f' s =
2095 (* val (pt, p, loc, f, r, f', s) =
2096 (pt,p,l,f,Rewrite_Set_Inst (subst2subs subs',id_rls rls'),
2099 ((*tracing("##@cappend_atomic: pos ="^pos2str p);*)
2100 apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm))
2102 (*TODO.WN050305 redesign the handling of istates*)
2103 fun cappend_atomic pt p ist_res f r f' s =
2104 if existpt p pt andalso is_empty_tac (get_obj g_tac pt p)
2105 then (*after Take: transfer Frm and respective istate*)
2108 (get_loc pt (p,Frm), get_obj g_form pt p)
2109 val (pt, cs) = cut_tree pt (p,Frm)
2110 val pt = append_atomic p (e_istate, e_ctxt) f r f' s pt
2111 val pt = update_loc' pt p (SOME ist_form, SOME ist_res)
2113 else apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
2115 (* called by Take *)
2116 fun append_form p l f pt =
2117 ((*tracing("##@append_form: pos ="^pos2str p);*)
2118 insert_pt (PrfObj {cell = NONE,
2119 form = (*if existpt p pt
2120 andalso get_obj g_tac pt p = Empty_Tac
2121 (*distinction from 'old' (+complete!) pobjs*)
2122 then get_obj g_form pt p else*) f,
2124 loc = (SOME l, NONE),
2126 result= (e_term,[]),
2127 ostate= Incomplete}) pt p
2129 (* val (p,loc,f) = ([1], e_istate, str2term "x + 1 = 2");
2130 val (p,loc,f) = (fst p, e_istate, str2term "-1 + x = 0");
2132 fun cappend_form pt p loc f =
2133 ((*tracing("##@cappend_form: pos ="^pos2str p);*)
2134 apfst (append_form p loc f) (cut_tree pt (p,Frm))
2136 fun cappend_form pt p loc f =
2137 let (*val _= tracing("##@cappend_form: pos ="^pos2str p)
2138 val _= tracing("##@cappend_form before cut_tree: loc ="^istate2str loc)*)
2139 val (pt', cs) = cut_tree pt (p,Frm)
2140 val pt'' = append_form p loc f pt'
2141 (*val _= tracing("##@cappend_form after append: loc ="^
2142 istates2str (get_obj g_loc pt'' p))*)
2147 fun append_result pt p l f s =
2148 (appl_obj (repl_result (fst (get_obj g_loc pt p), SOME l) f s) pt p, []);
2151 (*WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml*)
2152 fun append_parent p l f r b pt =
2153 let (*val _= tracing("###append_parent: pos ="^pos2str p);*)
2154 val (ll,f) = if existpt p pt andalso is_empty_tac (get_obj g_tac pt p)
2155 then ((fst (get_obj g_loc pt p), SOME l),
2156 get_obj g_form pt p)
2157 else ((SOME l, NONE), f)
2158 in insert_pt (PrfObj
2164 result= (e_term,[]),
2165 ostate= Incomplete}) pt p end;
2166 fun cappend_parent pt p loc f r b =
2167 ((*tracing("###cappend_parent: pos ="^pos2str p);*)
2168 apfst (append_parent p loc f r b) (cut_tree pt (p,Und))
2172 fun append_problem [] l fmz (strs,spec,hdf) _ =
2173 ((*tracing("###append_problem: pos = []");*)
2176 origin= (strs,spec,hdf),
2179 probl = []:itm list,
2183 loc = (SOME l, NONE),
2184 branch= TransitiveB,(*FIXXXXXME.27.8.03: for equations only*)
2185 result= (e_term,[]),
2186 ostate= Incomplete},[]))
2188 | append_problem p l fmz (strs,spec,hdf) pt =
2189 ((*tracing("###append_problem: pos ="^pos2str p);*)
2192 origin= (strs,spec,hdf),
2195 probl = []:itm list,
2199 loc = (SOME l, NONE),
2200 branch= TransitiveB,
2201 result= (e_term,[]),
2202 ostate= Incomplete}) pt p
2204 fun cappend_problem _ [] loc fmz ori =
2205 ((*tracing("###cappend_problem: pos = []");*)
2206 (append_problem [] loc fmz ori EmptyPtree,[])
2208 | cappend_problem pt p loc fmz ori =
2209 ((*tracing("###cappend_problem: pos ="^pos2str p);*)
2210 apfst (append_problem p (loc:(istate * Proof.context)) fmz ori) (cut_tree pt (p,Frm))
2213 (*.get the theory explicitly specified for the rootpbl;
2214 thus use this function _after_ finishing specification.*)
2215 fun rootthy (Nd (PblObj {spec=(thyID, _, _), ...}, _)) = assoc_thy thyID
2216 | rootthy _ = error "rootthy";
2221 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2223 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2225 (* policy for "open" structures:
2226 --------------------------------
2227 The above "open Ctree" creates an unclear situation with structures, in particular in test/.
2228 This is work in progress, but urges to make policy explicit:
2230 (1) All structures are closed with a signature; this for prepares re-arrangement of structures.
2231 (2) Some structures are pervasive (e.g. Ctree) such, that an "open" ensures readability locally.
2232 (3) test/ is preceeded by "open" for all structures, in order to ease copy&paste from scr/ to test/
2234 ad (1) Presently this point is under construction.
2235 ad (2) Such local "open" are kept to a minimum (with the goal to reach Isabelle's state).
2236 ad (3) See https://intra.ist.tugraz.at/hg/isa/file/2ba35efb07b7/test/Tools/isac/Test_Isac.thy#l70