intermed. ctxt ..: cleanup before start with Add_Given
uncommenting in src/../calchead.sm 2x "update_env" after "prep_ori"
marked with GOON.WN110506
causes errors in most test/../*, all with CalcTreeTEST; me; ..
1 (* use"../ME/ctree.sml";
6 tracing (pr_ptree pr_short pt);
12 (*structure Ptree (**): PTREE (**) = ###### outcommented ######*)
18 exception PTREE of string
37 val ets2str : ets -> string
41 val tac_2str : tac_ -> string
43 val safe2str : safe -> string
46 val cappend_atomic : ptree -> pos -> loc -> cterm' -> tac
47 -> cterm' -> ostate -> cid -> ptree * posel list * cid
48 val cappend_form : ptree
49 -> pos -> loc -> cterm' -> cid -> ptree * pos * cid
50 val cappend_parent : ptree -> pos -> loc -> cterm' -> tac
51 -> branch -> cid -> ptree * int list * cid
52 val cappend_problem : ptree -> posel list(*FIXME*) -> loc
53 -> cterm' list * spec -> cid -> ptree * int list * cellID list
54 val append_result : ptree -> pos -> cterm' -> ostate -> ptree * pos
57 val g_branch : ppobj -> branch
58 val g_cell : ppobj -> cid
59 val g_args : ppobj -> (int * (term list)) list (*args of scr*)
60 val g_form : ppobj -> cterm'
61 val g_loc : ppobj -> loc
62 val g_met : ppobj -> meth
63 val g_domID : ppobj -> domID
64 val g_metID : ppobj -> metID
65 val g_model : ppobj -> cterm' ppc
66 val g_tac : ppobj -> tac
67 val g_origin : ppobj -> cterm' list * spec
68 val g_ostate : ppobj -> ostate
69 val g_pbl : ppobj -> pblID * item ppc
70 val g_result : ppobj -> cterm'
71 val g_spec : ppobj -> spec
72 (* val get_all : (ppobj -> 'a) -> ptree -> 'a list
73 val get_alls : (ppobj -> 'a) -> ptree list -> 'a list *)
74 val get_obj : (ppobj -> 'a) -> ptree -> pos -> 'a
75 val gpt_cell : ptree -> cid
76 val par_pblobj : ptree -> pos -> pos
77 val pre_pos : pos -> pos
78 val lev_dn : int list -> int list
79 val lev_on : pos -> posel list
80 val lev_pred : pos -> pos
81 val lev_up : pos -> pos
82 (* val pr_cell : pos -> ppobj -> string
83 val pr_pos : int list -> string *)
84 val pr_ptree : (pos -> ppobj -> string) -> ptree -> string
85 val pr_short : pos -> ppobj -> string
86 (* val repl : 'a list -> int -> 'a -> 'a list
87 val repl_app : 'a list -> int -> 'a -> 'a list
88 val repl_branch : branch -> ppobj -> ppobj
89 val repl_domID : domID -> ppobj -> ppobj
90 val repl_form : cterm' -> ppobj -> ppobj
91 val repl_met : item ppc -> ppobj -> ppobj
92 val repl_metID : metID -> ppobj -> ppobj
93 val repl_model : cterm' list -> ppobj -> ppobj
94 val repl_tac : tac -> ppobj -> ppobj
95 val repl_pbl : item ppc -> ppobj -> ppobj
96 val repl_pblID : pblID -> ppobj -> ppobj
97 val repl_result : cterm' -> ostate -> ppobj -> ppobj
98 val repl_spec : spec -> ppobj -> ppobj
99 val repl_subs : (string * string) list -> ppobj -> ppobj *)
100 val rootthy : ptree -> domID
101 (* val test_trans : ppobj -> bool
102 val uni__asm : (string * pos) list -> ppobj -> ppobj
103 val uni__cid : cellID list -> ppobj -> ppobj *)
104 val union_asm : ptree -> pos -> (string * pos) list -> ptree
105 val union_cid : ptree -> pos -> cellID list -> ptree
106 val update_branch : ptree -> pos -> branch -> ptree
107 val update_domID : ptree -> pos -> domID -> ptree
108 val update_met : ptree -> pos -> meth -> ptree
109 val update_metppc : ptree -> pos -> item ppc -> ptree
110 val update_metID : ptree -> pos -> metID -> ptree
111 val update_tac : ptree -> pos -> tac -> ptree
112 val update_pbl : ptree -> pos -> pblID * item ppc -> ptree
113 val update_pblppc : ptree -> pos -> item ppc -> ptree
114 val update_pblID : ptree -> pos -> pblID -> ptree
115 val update_spec : ptree -> pos -> spec -> ptree
116 val update_subs : ptree -> pos -> (string * string) list -> ptree
118 val rep_pblobj : ppobj
119 -> {branch:branch, cell:cid, env:envp, loc:loc, meth:meth, model:cterm' ppc,
120 origin:cterm' list * spec, ostate:ostate, probl:pblID * item ppc,
121 result:cterm', spec:spec}
122 val rep_prfobj : ppobj
123 -> {branch:branch, cell:cid, form:cterm', loc:loc, tac:tac,
124 ostate:ostate, result:cterm'}
128 structure Ptree (**): PTREE (**) =
132 type env = (term * term) list;
136 NoBranch | AndB | OrB
137 | TransitiveB (* FIXXXME.8.03: set branch from met in Apply_Method
138 FIXXXME.0402: -"- in Begin_Trans'*)
139 | SequenceB | IntersectB | CollectB | MapB;
140 fun branch2str NoBranch = "NoBranch"
141 | branch2str AndB = "AndB"
142 | branch2str OrB = "OrB"
143 | branch2str TransitiveB = "TransitiveB"
144 | branch2str SequenceB = "SequenceB"
145 | branch2str IntersectB = "IntersectB"
146 | branch2str CollectB = "CollectB"
147 | branch2str MapB = "MapB";
150 Incomplete | Complete | Inconsistent(*WN041020 latter unused*);
151 fun ostate2str Incomplete = "Incomplete"
152 | ostate2str Complete = "Complete"
153 | ostate2str Inconsistent = "Inconsistent";
156 type cid = cellID list;
158 type posel = int; (* roundabout for (some of) nice signatures *)
159 type pos = posel list;
160 val pos2str = ints2str';
162 Pbl (*PblObj-position: problem-type*)
163 | Met (*PblObj-position: method*)
164 | Frm (*PblObj-position: -> Pbl in ME (not by moveDown !)
165 | PrfObj-position: formula*)
166 | Res (*PblObj | PrfObj-position: result*)
168 fun pos_2str Pbl = "Pbl"
169 | pos_2str Met = "Met"
170 | pos_2str Frm = "Frm"
171 | pos_2str Res = "Res"
172 | pos_2str Und = "Und";
174 type pos' = pos * pos_;
175 (*WN.12.03 remembering interator (pos * pos_) for ptree
176 pos : lev_on, lev_dn, lev_up,
177 lev_onFrm, lev_dnRes (..see solve Apply_Method !)
179 # generate1 sets pos_ if possible ...?WN0502?NOT...
180 # generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn
181 exceptions: Begin/End_Trans
182 # thus generate(1) called in
184 .# nxt_solv (tac_ -cases); general case:
185 val pos' = case pos' of (p,Res) => (lev_on p',Res) | _ => pos'
187 generate1...(Rewrite(f,..,res))..(pos, pos_)
188 cappend_atomic.................pos ////// gets f+res always!!!
189 cut_tree....................pos, pos_
191 fun pos'2str (p,p_) = pair2str (ints2str' p, pos_2str p_);
192 fun pos's2str ps = (strs2str' o (map pos'2str)) ps;
193 val e_pos' = ([],Und):pos';
195 fun res2str (t, ts) = pair2str (term2str t, terms2str ts);
199 (*26.4.02: never used after introduction of scripts !!!
200 type loc = loc_ * (* + interpreter-state *)
201 (loc_ * rls') (* -"- for script of the ruleset*)
203 val e_loc = ([],NONE):loc;
204 val ee_loc = (e_loc,e_loc);*)
207 datatype safe = Sundef | Safe | Unsafe | Helpless;
208 fun safe2str Sundef = "Sundef"
209 | safe2str Safe = "Safe"
210 | safe2str Unsafe = "Unsafe"
211 | safe2str Helpless = "Helpless";
213 type subs = cterm' list; (*16.11.00 for FE-KE*)
214 val e_subs = ["(bdv, x)"];
216 (*._sub_stitution as strings of _e_qualities.*)
217 type sube = cterm' list;
218 val e_sube = []:cterm' list;
219 fun sube2str s = strs2str s;
221 (*._sub_stitution as _t_erms of _e_qualities.*)
222 type subte = term list;
223 val e_subte = []:term list;
224 fun subte2str ss = terms2str ss;
226 fun subte2sube ss = map term2str ss;
228 fun subst2subs s = map (pair2str o (apfst term2str) o (apsnd term2str)) s;
229 fun subst2subs' s = map ((apfst term2str) o (apsnd term2str)) s;
230 fun subs2subst thy s = map (isapair2pair o term_of o the o (parse thy)) s;
231 (*> subs2subst thy ["(bdv,x)","(err,#0)"];
233 [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real")),
234 (Free ("err","RealDef.real"),Free ("#0","RealDef.real"))]
235 : (term * term) list*)
236 (*["bdv=x","err=0"] ---> [(bdv,x), (err,0)]*)
237 fun sube2subst thy s = map (dest_equals' o term_of o the o (parse thy)) s;
238 (* val ts = sube2subst thy ["bdv=x","err=0"];
241 fun sube2subte ss = map str2term ss;
244 fun isasub2subst isasub = ((map isapair2pair) o isalist2list) isasub;
247 type scrstate = (*state for script interpreter*)
248 env(*stack*) (*used to instantiate tac for checking assod
249 12.03.noticed: e_ not updated during execution ?!?*)
250 * loc_ (*location of tac in script*)
251 * term option(*argument of curried functions*)
252 * term (*value obtained by tac executed
253 updated also after a derivation by 'new_val'*)
254 * safe (*estimation of how result will be obtained*)
255 * bool; (*true = strongly .., false = weakly associated:
256 only used during ass_dn/up*)
257 val e_scrstate = ([],[],NONE,e_term,Sundef,false):scrstate;
260 (*21.8.02 ---> definitions.sml for datatype scr
261 type rrlsstate = (*state for reverse rewriting*)
262 (term * (*the current formula*)
263 rule list (*of reverse rewrite set (#1#)*)
264 list * (*may be serveral, eg. in norm_rational*)
265 (rule * (*Thm (+ Thm generated from Calc) resulting in ...*)
266 (term * (*... rewrite with ...*)
267 term list)) (*... assumptions*)
268 list); (*derivation from given term to normalform
269 in reverse order with sym_thm;
270 (#1#) could be extracted from here #1*) --------*)
272 datatype istate = (*interpreter state*)
273 Uistate (*undefined in modspec, in '_deriv'ation*)
274 | ScrState of scrstate (*for script interpreter*)
275 | RrlsState of rrlsstate; (*for reverse rewriting*)
276 val e_istate = (ScrState ([],[],NONE,e_term,Sundef,false)):istate;
277 val e_ctxt = ProofContext.init_global @{theory};
279 type iist = istate option * istate option;
280 (*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*)
283 fun rta2str (r,(t,a)) = "\n("^(rule2str r)^",("^(term2str t)^", "^
285 fun istate2str Uistate = "Uistate"
286 | istate2str (ScrState (e,l,to,t,s,b):istate) =
287 "ScrState ("^ subst2str e ^",\n "^
288 loc_2str l ^", "^ termopt2str to ^",\n "^
289 term2str t ^", "^ safe2str s ^", "^ bool2str b ^")"
290 | istate2str (RrlsState (t,t1,rss,rtas)) =
291 "RrlsState ("^(term2str t)^", "^(term2str t1)^", "^
292 ((strs2str o (map (strs2str o (map rule2str)))) rss)^", "^
293 ((strs2str o (map rta2str)) rtas)^")";
294 fun istates2str (NONE, NONE) = "(#NONE, #NONE)"
295 | istates2str (NONE, SOME ist) = "(#NONE,\n#SOME "^istate2str ist^")"
296 | istates2str (SOME ist, NONE) = "(#SOME "^istate2str ist^",\n #NONE)"
297 | istates2str (SOME i1, SOME i2) = "(#SOME "^istate2str i1^",\n #SOME "^
300 fun new_val v (ScrState (env, loc_, topt, _, safe, bool)) =
301 (ScrState (env, loc_, topt, v, safe, bool))
302 | new_val _ _ = error "new_val: only for ScrState";
304 datatype con = land | lor;
308 domID * (*WN.12.03: is replaced by thy from get_met ?FIXME? in:
309 specify (Init_Proof..), nxt_specify_init_calc,
310 assod (.SubProblem...), stac2tac (.SubProblem...)*)
313 fun spec2str ((dom,pbl,met)(*:spec*)) =
314 "(" ^ (quote dom) ^ ", " ^ (strs2str pbl) ^
315 ", " ^ (strs2str met) ^ ")";
316 (*> spec2str empty_spec;
317 val it = "(\"\", [], (\"\", \"\"))" : string *)
318 val empty_spec = (e_domID,e_pblID,e_metID):spec;
319 val e_spec = empty_spec;
323 (*.tactics propagate the construction of the calc-tree;
325 (a) 'specsteps' for the specify-phase, and others for the solve-phase
326 (b) those of the solve-phase are 'initac's and others;
327 initacs start with a formula different from the preceding formula.
328 see 'type tac_' for the internal representation of tactics.*)
330 Init_Proof of ((cterm' list) * spec)
333 | Refine_Problem of pblID | Refine_Tacitly of pblID
335 | Add_Given of cterm' | Del_Given of cterm'
336 | Add_Find of cterm' | Del_Find of cterm'
337 | Add_Relation of cterm' | Del_Relation of cterm'
339 | Specify_Theory of domID | Specify_Problem of pblID
340 | Specify_Method of metID
342 | Apply_Method of metID
343 (*.creates an 'istate' in PblObj.env; in case of 'init_form'
344 creates a formula at ((lev_on o lev_dn) p, Frm) and in this ppobj.'loc'
345 'SOME istate' (at fst of 'loc').
346 As each step (in the solve-phase) has a resulting formula (at the front-end)
347 Apply_Method also does the 1st step in the script (an 'initac') if there
348 is no 'init_form' .*)
349 | Check_Postcond of pblID
352 | Rewrite_Inst of ( subs * thm') | Rewrite of thm'
353 | Rewrite_Asm of thm'
354 | Rewrite_Set_Inst of ( subs * rls') | Rewrite_Set of rls'
355 | Detail_Set_Inst of ( subs * rls') | Detail_Set of rls'
356 | End_Detail (*end of script from next_tac,
357 in solve: switches back to parent script WN0509 drop!*)
358 | Derive of rls' (*an input formula using rls WN0509 drop!*)
359 | Calculate of string (* plus | minus | times | cancel | pow | sqrt *)
361 | Substitute of sube | Apply_Assumption of cterm' list
363 | Take of cterm' (*an 'initac'*)
364 | Take_Inst of cterm'
365 | Group of (con * int list )
366 | Subproblem of (domID * pblID) (*an 'initac'*)
367 | CAScmd of cterm' (*6.6.02 URD: Function formula; WN0509 drop!*)
368 | End_Subproblem (*WN0509 drop!*)
370 | Split_And | Conclude_And
371 | Split_Or | Conclude_Or
372 | Begin_Trans | End_Trans
373 | Begin_Sequ | End_Sequ(* substitute root.env *)
374 | Split_Intersect | End_Intersect
375 | Check_elementwise of cterm' | Collect_Trues
378 | Empty_Tac (* TODO.11.6.03 ... of string: could carry msg of (Notappl msg)
380 | Tac of string (* eg.'repeat'*WN0509 drop! (ab)used to report syntaxerror *)
381 | User (* internal, for ets*WN0509 drop! *)
382 | End_Proof'; (* inout *)
384 (* tac2str /--> library.sml: needed in dialog.sml for 'separable *)
385 fun tac2str (ma:tac) = case ma of
386 Init_Proof (ppc, spec) =>
387 "Init_Proof "^(pair2str (strs2str ppc, spec2str spec))
388 | Model_Problem => "Model_Problem "
389 | Refine_Tacitly pblID => "Refine_Tacitly "^(strs2str pblID)
390 | Refine_Problem pblID => "Refine_Problem "^(strs2str pblID)
391 | Add_Given cterm' => "Add_Given "^cterm'
392 | Del_Given cterm' => "Del_Given "^cterm'
393 | Add_Find cterm' => "Add_Find "^cterm'
394 | Del_Find cterm' => "Del_Find "^cterm'
395 | Add_Relation cterm' => "Add_Relation "^cterm'
396 | Del_Relation cterm' => "Del_Relation "^cterm'
398 | Specify_Theory domID => "Specify_Theory "^(quote domID )
399 | Specify_Problem pblID => "Specify_Problem "^(strs2str pblID )
400 | Specify_Method metID => "Specify_Method "^(strs2str metID)
401 | Apply_Method metID => "Apply_Method "^(strs2str metID)
402 | Check_Postcond pblID => "Check_Postcond "^(strs2str pblID)
403 | Free_Solve => "Free_Solve"
405 | Rewrite_Inst (subs,thm')=>
406 "Rewrite_Inst "^(pair2str (subs2str subs, spair2str thm'))
407 | Rewrite thm' => "Rewrite "^(spair2str thm')
408 | Rewrite_Asm thm' => "Rewrite_Asm "^(spair2str thm')
409 | Rewrite_Set_Inst (subs, rls) =>
410 "Rewrite_Set_Inst "^(pair2str (subs2str subs, quote rls))
411 | Rewrite_Set rls => "Rewrite_Set "^(quote rls )
412 | Detail_Set rls => "Detail_Set "^(quote rls )
413 | Detail_Set_Inst (subs, rls) =>
414 "Detail_Set_Inst "^(pair2str (subs2str subs, quote rls))
415 | End_Detail => "End_Detail"
416 | Derive rls' => "Derive "^rls'
417 | Calculate op_ => "Calculate "^op_
418 | Substitute sube => "Substitute "^sube2str sube
419 | Apply_Assumption ct's => "Apply_Assumption "^(strs2str ct's)
421 | Take cterm' => "Take "^(quote cterm' )
422 | Take_Inst cterm' => "Take_Inst "^(quote cterm' )
423 | Group (con, ints) =>
424 "Group "^(pair2str (con2str con, ints2str ints))
425 | Subproblem (domID, pblID) =>
426 "Subproblem "^(pair2str (domID, strs2str pblID))
427 (*| Subproblem_Full (spec, cts') =>
428 "Subproblem_Full "^(pair2str (spec2str spec, strs2str cts'))*)
429 | End_Subproblem => "End_Subproblem"
430 | CAScmd cterm' => "CAScmd "^(quote cterm')
432 | Check_elementwise cterm'=> "Check_elementwise "^(quote cterm')
433 | Or_to_List => "Or_to_List "
434 | Collect_Trues => "Collect_Trues"
436 | Empty_Tac => "Empty_Tac"
437 | Tac string => "Tac "^string
439 | End_Proof' => "tac End_Proof'"
440 | _ => "tac2str not impl. for ?!";
442 fun is_rewset (Rewrite_Set_Inst _) = true
443 | is_rewset (Rewrite_Set _) = true
444 | is_rewset _ = false;
445 fun is_rewtac (Rewrite _) = true
446 | is_rewtac (Rewrite_Inst _) = true
447 | is_rewtac (Rewrite_Asm _) = true
448 | is_rewtac tac = is_rewset tac;
450 fun tac2IDstr (ma:tac) = case ma of
451 Model_Problem => "Model_Problem"
452 | Refine_Tacitly pblID => "Refine_Tacitly"
453 | Refine_Problem pblID => "Refine_Problem"
454 | Add_Given cterm' => "Add_Given"
455 | Del_Given cterm' => "Del_Given"
456 | Add_Find cterm' => "Add_Find"
457 | Del_Find cterm' => "Del_Find"
458 | Add_Relation cterm' => "Add_Relation"
459 | Del_Relation cterm' => "Del_Relation"
461 | Specify_Theory domID => "Specify_Theory"
462 | Specify_Problem pblID => "Specify_Problem"
463 | Specify_Method metID => "Specify_Method"
464 | Apply_Method metID => "Apply_Method"
465 | Check_Postcond pblID => "Check_Postcond"
466 | Free_Solve => "Free_Solve"
468 | Rewrite_Inst (subs,thm')=> "Rewrite_Inst"
469 | Rewrite thm' => "Rewrite"
470 | Rewrite_Asm thm' => "Rewrite_Asm"
471 | Rewrite_Set_Inst (subs, rls) => "Rewrite_Set_Inst"
472 | Rewrite_Set rls => "Rewrite_Set"
473 | Detail_Set rls => "Detail_Set"
474 | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst"
475 | Derive rls' => "Derive "
476 | Calculate op_ => "Calculate "
477 | Substitute subs => "Substitute"
478 | Apply_Assumption ct's => "Apply_Assumption"
480 | Take cterm' => "Take"
481 | Take_Inst cterm' => "Take_Inst"
482 | Group (con, ints) => "Group"
483 | Subproblem (domID, pblID) => "Subproblem"
484 | End_Subproblem => "End_Subproblem"
485 | CAScmd cterm' => "CAScmd"
487 | Check_elementwise cterm'=> "Check_elementwise"
488 | Or_to_List => "Or_to_List "
489 | Collect_Trues => "Collect_Trues"
491 | Empty_Tac => "Empty_Tac"
492 | Tac string => "Tac "
494 | End_Proof' => "End_Proof'"
495 | _ => "tac2str not impl. for ?!";
497 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
498 | rls_of (Rewrite_Set rls) = rls
499 | rls_of tac = error ("rls_of: called with tac '"^tac2IDstr tac^"'");
501 fun thm_of_rew (Rewrite_Inst (subs,(thmID,_))) =
502 (thmID, SOME ((subs2subst (assoc_thy "Isac") subs):subst))
503 | thm_of_rew (Rewrite (thmID,_)) = (thmID, NONE)
504 | thm_of_rew (Rewrite_Asm (thmID,_)) = (thmID, NONE);
506 fun rls_of_rewset (Rewrite_Set_Inst (subs,rls)) =
507 (rls, SOME ((subs2subst (assoc_thy "Isac") subs):subst))
508 | rls_of_rewset (Rewrite_Set rls) = (rls, NONE)
509 | rls_of_rewset (Detail_Set rls) = (rls, NONE)
510 | rls_of_rewset (Detail_Set_Inst (subs, rls)) =
511 (rls, SOME ((subs2subst (assoc_thy "Isac") subs):subst));
513 fun rule2tac _ (Calc (opID, thm)) = Calculate (calID2calcID opID)
514 | rule2tac [] (Thm (thmID, thm)) = Rewrite (thmID, string_of_thmI thm)
515 | rule2tac subst (Thm (thmID, thm)) =
516 Rewrite_Inst (subst2subs subst, (thmID, string_of_thmI thm))
517 | rule2tac [] (Rls_ rls) = Rewrite_Set (id_rls rls)
518 | rule2tac subst (Rls_ rls) =
519 Rewrite_Set_Inst (subst2subs subst, (id_rls rls))
521 error ("rule2tac: called with '" ^ rule2str rule ^ "'");
523 type fmz_ = cterm' list;
525 (*.a formalization of an example containing data
526 sufficient for mechanically finding the solution for the example.*)
527 (*FIXME.WN051014: dont store fmz = (_,spec) in the PblObj,
528 this is done in origin*)
529 type fmz = fmz_ * spec;
530 val e_fmz = ([],e_spec);
532 (*tac_ is made from tac in applicable_in,
533 and carries all data necessary for generate;*)
536 Init_Proof' of ((cterm' list) * spec)
537 (* ori list !: code specify -> applicable*)
538 | Model_Problem' of pblID *
539 itm list * (*the 'untouched' pbl*)
540 itm list (*the casually completed met*)
541 | Refine_Tacitly' of pblID * (*input*)
542 pblID * (*the refined from applicable_in*)
543 domID * (*from new pbt?! filled in specify*)
544 metID * (*from new pbt?! filled in specify*)
545 itm list (*drop ! 9.03: remains [] for
546 Model_Problem recognizing its activation*)
547 | Refine_Problem' of (pblID * (itm list * (bool * Term.term) list))
548 (*FIXME?040215 drop: done automatically in init_proof + Subproblem'*)
549 | Add_Given' of cterm' *
550 itm list (*updated with input in fun specify_additem*)
551 | Add_Find' of cterm' *
552 itm list (*updated with input in fun specify_additem*)
553 | Add_Relation' of cterm' *
554 itm list (*updated with input in fun specify_additem*)
555 | Del_Given' of cterm' | Del_Find' of cterm' | Del_Relation' of cterm'
556 (*4.00.: all.. term: in applicable_in ..? Syn ?only for FormFK?*)
558 | Specify_Theory' of domID
559 | Specify_Problem' of (pblID * (* *)
560 (bool * (* matches *)
561 (itm list * (* ppc *)
562 (bool * term) list))) (* preconditions *)
563 | Specify_Method' of metID *
564 ori list * (*repl. "#undef"*)
565 itm list (*... updated from pbl to met*)
566 | Apply_Method' of metID *
567 (term option) * (*init_form*)
568 istate * Proof.context
571 (term * (*returnvalue of script in solve*)
572 cterm' list)(*collect by get_assumptions_ in applicable_in, except if
573 butlast tac is Check_elementwise: take only these asms*)
576 | Rewrite_Inst' of theory' * rew_ord' * rls
577 * bool * subst * thm' * term * (term * term list)
578 | Rewrite' of theory' * rew_ord' * rls * bool * thm' *
579 term * (term * term list)
580 | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm' *
581 term * (term * term list)
582 | Rewrite_Set_Inst' of theory' * bool * subst * rls *
583 term * (term * term list)
584 | Detail_Set_Inst' of theory' * bool * subst * rls *
585 term * (term * term list)
586 | Rewrite_Set' of theory' * bool * rls * term * (term * term list)
587 | Detail_Set' of theory' * bool * rls * term * (term * term list)
588 | End_Detail' of (term * (term list)) (*see End_Trans'*)
589 | End_Ruleset' of term
591 | Calculate' of theory' * string * term * (term * thm')
592 (*WN.29.4.03 asm?: * term list??*)
593 | Substitute' of subte (*the 'substitution': terms of type bool*)
594 * term (*to be substituted in*)
595 * term (*resulting from the substitution*)
596 | Apply_Assumption' of term list * term
598 | Take' of term | Take_Inst' of term
599 | Group' of (con * int list * term)
600 | Subproblem' of (spec *
601 (ori list) * (*filled in assod Subproblem'*)
602 term * (*-"-, headline of calc-head *)
604 term) (*Subproblem(dom,pbl)*)
606 | End_Subproblem' of term (*???*)
607 | Split_And' of term | Conclude_And' of term
608 | Split_Or' of term | Conclude_Or' of term
609 | Begin_Trans' of term | End_Trans' of (term * (term list))
610 | Begin_Sequ' | End_Sequ'(* substitute root.env*)
611 | Split_Intersect' of term | End_Intersect' of term
612 | Check_elementwise' of (*special case:*)
613 term * (*(1)the current formula: [x=1,x=...]*)
614 string * (*(2)the pred from Check_elementwise *)
615 (term * (*(3)composed from (1) and (2): {x. pred}*)
616 term list) (*20.5.03 assumptions*)
618 | Or_to_List' of term * term (* (a | b, [a,b]) *)
619 | Collect_Trues' of term
621 | Empty_Tac_ | Tac_ of (*for dummies*)
625 string (*result of Tac".."*)
626 | User' (*internal for ets*) | End_Proof'';(*End_Proof:inout*)
628 fun tac_2str ma = case ma of
629 Init_Proof' (ppc, spec) =>
630 "Init_Proof' "^(pair2str (strs2str ppc, spec2str spec))
631 | Model_Problem' (pblID,_,_) => "Model_Problem' "^(strs2str pblID )
632 | Refine_Tacitly'(p,prefin,domID,metID,itms)=>
634 ^(strs2str p)^", "^(strs2str prefin)^", "
635 ^domID^", "^(strs2str metID)^", pbl-itms)"
636 | Refine_Problem' ms => "Refine_Problem' ("^(*matchs2str ms*)"..."^")"
637 (*| Match_Problem' (pI, (ok, (itms, pre))) =>
638 "Match_Problem' "^(spair2str (strs2str pI,
639 spair2str (bool2str ok,
640 spair2str ("itms2str_ itms",
641 "items2str pre"))))*)
642 | Add_Given' cterm' => "Add_Given' "(*^cterm'*)
643 | Del_Given' cterm' => "Del_Given' "(*^cterm'*)
644 | Add_Find' cterm' => "Add_Find' "(*^cterm'*)
645 | Del_Find' cterm' => "Del_Find' "(*^cterm'*)
646 | Add_Relation' cterm' => "Add_Relation' "(*^cterm'*)
647 | Del_Relation' cterm' => "Del_Relation' "(*^cterm'*)
649 | Specify_Theory' domID => "Specify_Theory' "^(quote domID )
650 | Specify_Problem' (pI, (ok, (itms, pre))) =>
651 "Specify_Problem' "^(spair2str (strs2str pI,
652 spair2str (bool2str ok,
653 spair2str ("itms2str_ itms",
655 | Specify_Method' (pI,oris,itms) =>
656 "Specify_Method' ("^metID2str pI^", "^oris2str oris^", )"
658 | Apply_Method' (metID,_,_,_) => "Apply_Method' "^(strs2str metID)
659 | Check_Postcond' (pblID,(scval,asm)) =>
660 "Check_Postcond' "^(spair2str(strs2str pblID,
661 spair2str (term2str scval, strs2str asm)))
663 | Free_Solve' => "Free_Solve'"
665 | Rewrite_Inst' (*subs,thm'*) _ =>
666 "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
667 | Rewrite' thm' => "Rewrite' "(*^(spair2str thm')*)
668 | Rewrite_Asm' thm' => "Rewrite_Asm' "(*^(spair2str thm')*)
669 | Rewrite_Set_Inst' (*subs,thm'*) _ =>
670 "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
671 | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) =>
672 "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^ "," ^ id_rls rls' ^ "," ^
673 term2str f ^ ",(" ^ term2str f' ^ "," ^ terms2str asm ^ "))"
674 | End_Detail' _ => "End_Detail' xxx"
675 | Detail_Set' _ => "Detail_Set' xxx"
676 | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
678 | Derive' rls => "Derive' "^id_rls rls
679 | Calculate' _ => "Calculate' "
680 | Substitute' subs => "Substitute' "(*^(subs2str subs)*)
681 | Apply_Assumption' ct's => "Apply_Assumption' "(*^(strs2str ct's)*)
683 | Take' cterm' => "Take' "(*^(quote cterm' )*)
684 | Take_Inst' cterm' => "Take_Inst' "(*^(quote cterm' )*)
685 | Group' (con, ints, _) =>
686 "Group' "^(pair2str (con2str con, ints2str ints))
687 | Subproblem' (spec, oris, _,_,pbl_form) =>
688 "Subproblem' "(*^(pair2str (domID, strs2str ,...))*)
689 | End_Subproblem' _ => "End_Subproblem'"
690 | CAScmd' cterm' => "CAScmd' "(*^(quote cterm')*)
692 | Empty_Tac_ => "Empty_Tac_"
694 | Tac_ (_,form,id,result) => "Tac_ (thy,"^form^","^id^","^result^")"
695 | _ => "tac_2str not impl. for arg";
697 (*'executed tactics' (tac_s) with local environment etc.;
698 used for continuing eval script + for generate*)
700 (loc_ * (* of tactic in scr, tactic (weakly) associated with tac_*)
701 (tac_ * (* (for generate) *)
702 env * (* with 'tactic=result' as a rule, tactic ev. _not_ ready:
703 for handling 'parallel let'*)
704 env * (* with results of (ready) tacs *)
705 term * (* itr_arg of tactic, for upd. env at Repeat, Try*)
706 term * (* result value of the tac *)
712 fun ets2s (l,(m,eno,env,iar,res,s)) =
713 "\n(" ^ loc_2str l ^ ",(" ^ tac_2str m ^
714 ",\n ens= " ^ subst2str eno ^
715 ",\n env= " ^ subst2str env ^
716 ",\n iar= " ^ term2str iar ^
717 ",\n res= " ^ term2str res ^
718 ",\n " ^ safe2str s ^ "))";
719 fun ets2str (ets:ets) = (strs2str o (map ets2s)) ets;
722 type envp =(*9.5.03: unused, delete with field in ptree.PblObj FIXXXME*)
723 (int * term list) list * (*assoc-list: args of met*)
724 (int * rls) list * (*assoc-list: tacs already done ///15.9.00*)
725 (int * ets) list * (*assoc-list: tacs etc. already done*)
726 (string * pos) list; (*asms * from where*)
727 val empty_envp = ([],[],[],[]):envp;
731 {cell : lrd option, (* where in form tac has been applied *)
732 (*^^^FIXME.WN0607 rename this field*)
733 form : term, (* where tac is applied to *)
734 tac : tac, (* also in istate *)
735 loc : (istate * (* script interpreter state *)
736 Proof.context) (* context for provers, type inference *)
737 option * (* both for interpreter location on Frm, Pbl, Met *)
738 (istate * (* script interpreter state *)
739 Proof.context) (* context for provers, type inference *)
740 option, (* both for interpreter location on Res *)
741 (*(NONE,NONE) <==> e_istate ! see update_loc, get_loc*)
742 branch: branch, (* only rudimentary *)
743 result: term * term list, (* result and assumptions *)
744 ostate: ostate} (* Complete <=> result is OK *)
746 {cell : lrd option, (* unused: meaningful only for some _Prf_Obj *)
747 fmz : fmz, (* from init:FIXME never use this spec;-drop *)
748 origin: (ori list) * (* representation from fmz+pbt
749 for efficiently adding items in probl, meth *)
750 spec * (* updated by Refine_Tacitly *)
751 term, (* headline of calc-head, as calculated initially(!)*)
752 spec : spec, (* explicitly input *)
753 probl : itm list, (* itms explicitly input *)
754 meth : itm list, (* itms automatically added to copy of probl *)
755 env : (istate * Proof.context) option,
756 (* istate only for initac in script
757 context for specify phase on this node *)
758 loc : (istate * Proof.context) option * (istate * Proof.context) option,
760 branch: branch, (* like PrfObj *)
761 result: term * term list, (* like PrfObj *)
762 ostate: ostate}; (* like PrfObj *)
764 (*.this tree contains isac's calculations; TODO.WN03 rename to ctree;
765 the structure has been copied from an early version of Theorema(c);
766 it has the disadvantage, that there is no space
767 for the first tactic in a script generating the first formula at (p,Frm);
768 this trouble has been covered by 'init_form' and 'Take' so far,
769 but it is crucial if the first tactic in a script is eg. 'Subproblem';
770 see 'type tac ', Apply_Method.
774 | Nd of ppobj * (ptree list);
775 val e_ptree = EmptyPtree;
777 fun rep_prfobj (PrfObj {cell,form,tac,loc,branch,result,ostate}) =
778 {cell=cell,form=form,tac=tac,loc=loc,branch=branch,result=result,ostate=ostate};
779 fun rep_pblobj (PblObj {cell,origin,fmz,spec,probl,meth,env,
780 loc,branch,result,ostate}) =
781 {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,
782 env=env,loc=loc,branch=branch,result=result,ostate=ostate};
783 fun is_prfobj (PrfObj _) = true
784 | is_prfobj _ =false;
785 (*val is_prfobj' = get_obj is_prfobj; *)
786 fun is_pblobj (PblObj _) = true
787 | is_pblobj _ = false;
788 (*val is_pblobj' = get_obj is_pblobj; 'Error: unbound constructor get_obj'*)
791 exception PTREE of string;
792 fun nth _ [] = raise PTREE "nth _ []"
794 | nth n (x::xs) = nth (n-1) xs;
795 (*> nth 2 [11,22,33]; -->> val it = 22 : int*)
797 fun lev_up ([]:pos) = raise PTREE "lev_up []"
798 | lev_up p = (drop_last p):pos;
799 fun lev_on ([]:pos) = raise PTREE "lev_on []"
801 let val len = length pos
802 in (drop_last pos) @ [(nth len pos)+1] end;
803 fun lev_onFrm ((p,_):pos') = (lev_on p,Frm):pos'
804 | lev_onFrm p = raise PTREE ("*** lev_onFrm: pos'="^(pos'2str p));
805 (*040216: for inform --> embed_deriv: remains on same level*)
806 fun lev_back (([],_):pos') = raise PTREE "lev_on_back: called by ([],_)"
808 if last_elem p <= 1 then (p, Frm):pos'
809 else ((drop_last p) @ [(nth (length p) p) - 1], Res);
810 (*.increase pos by n within a level.*)
811 fun pos_plus 0 pos = pos
812 | pos_plus n ((p,Frm):pos') = pos_plus (n-1) (p, Res)
813 | pos_plus n ((p, _):pos') = pos_plus (n-1) (lev_on p, Res);
817 fun lev_pred ([]:pos) = raise PTREE "lev_pred []"
818 | lev_pred (pos:pos) =
819 let val len = length pos
820 in ((drop_last pos) @ [(nth len pos)-1]):pos end;
822 val it = [1,2,2] : pos
824 val it = [0] : pos *)
826 fun lev_dn p = p @ [0];
827 (*> (lev_dn o lev_on) [1,2,3];
828 val it = [1,2,4,0] : pos *)
829 (*fun lev_dn' ((p,p_):pos') = (lev_dn p, Frm):pos'; WN.3.12.03: never used*)
830 fun lev_dnRes ((p,_):pos') = (lev_dn p, Res):pos';
833 fun lev_up_ ((p,Res):pos') = (lev_up p,Res):pos'
834 | lev_up_ p' = error ("lev_up_: called for "^(pos'2str p'));
835 fun lev_dn_ ((p,_):pos') = (lev_dn p,Res):pos'
836 fun ind ((p,_):pos') = length p; (*WN050108 deprecated in favour of lev_of*)
837 fun lev_of ((p,_):pos') = length p;
840 (** convert ptree to a string **)
842 (* convert a pos from list to string *)
843 fun pr_pos ps = (space_implode "." (map string_of_int ps))^". ";
844 (* show hd origin or form only *)
845 fun pr_short (p:pos) (PblObj {origin = (ori,_,_),...}) =
846 ((pr_pos p) ^ " ----- pblobj -----\n")
847 (* ((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^
848 (((Syntax.string_of_term (thy2ctxt' "Isac")) o hd(*!?!*) o #5 o hd) ori))^
850 | pr_short p (PrfObj {form = form,...}) =
851 ((pr_pos p) ^ (term2str form) ^ "\n");
853 fun pr_cell (p:pos) (PblObj {cell = c, origin = (ori,_,_),...}) =
855 ((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^
856 (((Syntax.string_of_term (thy2ctxt' "Isac")) o hd(*!?!*) o #5 o hd) ori))^
858 | pr_cell p (PrfObj {cell = c, form = form,...}) =
859 ((ints2str c) ^" "^ (term2str form) ^ "\n");
865 fun pr_pt pfn _ EmptyPtree = ""
866 | pr_pt pfn ps (Nd (b, [])) = pfn ps b
867 | pr_pt pfn ps (Nd (b, ts)) = (pfn ps b)^
868 (prts pfn (ps:pos) 1 ts)
869 and prts pfn ps p [] = ""
870 | prts pfn ps p (t::ts) = (pr_pt pfn (ps @ [p]) t)^
871 (prts pfn ps (p+1) ts)
872 in pr_pt f [] pt end;
874 > fun prfn ps b = (pr_pos ps)^" "^b(*TODO*)^"\n";
875 > val pt = Unsynchronized.ref EmptyPtree;
882 > tracing (pr_ptree prfn (!pt));
886 (** access the branches of ptree **)
888 fun ins_nth 1 e l = e::l
889 | ins_nth n e [] = raise PTREE "ins_nth n e []"
890 | ins_nth n e (l::ls) = l::(ins_nth (n-1) e ls);
891 fun repl [] _ _ = raise PTREE "repl [] _ _"
892 | repl (l::ls) 1 e = e::ls
893 | repl (l::ls) n e = l::(repl ls (n-1) e);
894 fun repl_app ls n e =
895 let val lim = 1 + length ls
896 in if n > lim then raise PTREE "repl_app: n > lim"
897 else if n = lim then ls @ [e]
898 else repl ls n e end;
900 > repl [1,2,3] 2 22222;
901 val it = [1,22222,3] : int list
902 > repl_app [1,2,3,4] 5 5555;
903 val it = [1,2,3,4,5555] : int list
904 > repl_app [1,2,3] 2 22222;
905 val it = [1,22222,3] : int list
906 > repl_app [1] 2 22222 ;
907 val it = [1,22222] : int list
911 (*.get from obj at pos by f : ppobj -> 'a.*)
912 fun get_obj f EmptyPtree (_:pos) = raise PTREE "get_obj f EmptyPtree"
913 | get_obj f (Nd (b, _)) [] = f b
914 | get_obj f (Nd (b, bs)) (p::ps) =
915 (* val (f, Nd (b, bs), (p::ps)) = (I, pt, p);
917 let val _ = (nth p bs) handle _ => raise PTREE ("get_obj: pos = "^
918 (ints2str' (p::ps))^" does not exist");
919 in (get_obj f (nth p bs) (ps:pos))
920 (*before WN050419: 'wrong type..' raised also if pos doesn't exist*)
921 handle _ => raise PTREE (*"get_obj: at pos = "^
922 (ints2str' (p::ps))^" wrong type of ppobj"*)
924 (ints2str' (p::ps))^" does not exist")
926 fun get_nd EmptyPtree _ = raise PTREE "get_nd EmptyPtree"
928 | get_nd (Nd (_,nds)) (pos as p::(ps:pos)) = (get_nd (nth p nds) ps)
929 handle _ => raise PTREE ("get_nd: not existent pos = "^(ints2str' pos));
932 (* for use by get_obj *)
933 fun g_cell (PblObj {cell = c,...}) = NONE
934 | g_cell (PrfObj {cell = c,...}) = c;(*WN0607 hack for quick introduction of lrd + rewrite-at (thms, calcs)*)
935 fun g_form (PrfObj {form = f,...}) = f
936 | g_form (PblObj {origin=(_,_,f),...}) = f;
937 fun g_form' (Nd (PrfObj {form = f,...}, _)) = f
938 | g_form' (Nd (PblObj {origin=(_,_,f),...}, _)) = f;
939 (* | g_form _ = raise PTREE "g_form not for PblObj";*)
940 fun g_origin (PblObj {origin = ori,...}) = ori
941 | g_origin _ = raise PTREE "g_origin not for PrfObj";
942 fun g_fmz (PblObj {fmz = f,...}) = f
943 | g_fmz _ = raise PTREE "g_fmz not for PrfObj";
944 fun g_spec (PblObj {spec = s,...}) = s
945 | g_spec _ = raise PTREE "g_spec not for PrfObj";
946 fun g_pbl (PblObj {probl = p,...}) = p
947 | g_pbl _ = raise PTREE "g_pbl not for PrfObj";
948 fun g_met (PblObj {meth = p,...}) = p
949 | g_met _ = raise PTREE "g_met not for PrfObj";
950 fun g_domID (PblObj {spec = (d,_,_),...}) = d
951 | g_domID _ = raise PTREE "g_metID not for PrfObj";
952 fun g_metID (PblObj {spec = (_,_,m),...}) = m
953 | g_metID _ = raise PTREE "g_metID not for PrfObj";
954 fun g_env (PblObj {env,...}) = env
955 | g_env _ = raise PTREE "g_env not for PrfObj";
956 fun g_loc (PblObj {loc = l,...}) = l
957 | g_loc (PrfObj {loc = l,...}) = l;
958 fun g_branch (PblObj {branch = b,...}) = b
959 | g_branch (PrfObj {branch = b,...}) = b;
960 fun g_tac (PblObj {spec = (d,p,m),...}) = Apply_Method m
961 | g_tac (PrfObj {tac = m,...}) = m;
962 fun g_result (PblObj {result = r,...}) = r
963 | g_result (PrfObj {result = r,...}) = r;
964 fun g_res (PblObj {result = (r,_),...}) = r
965 | g_res (PrfObj {result = (r,_),...}) = r;
966 fun g_res' (Nd (PblObj {result = (r,_),...}, _)) = r
967 | g_res' (Nd (PrfObj {result = (r,_),...}, _)) = r;
968 fun g_ostate (PblObj {ostate = r,...}) = r
969 | g_ostate (PrfObj {ostate = r,...}) = r;
970 fun g_ostate' (Nd (PblObj {ostate = r,...}, _)) = r
971 | g_ostate' (Nd (PrfObj {ostate = r,...}, _)) = r;
973 fun gpt_cell (Nd (PblObj {cell = c,...},_)) = NONE
974 | gpt_cell (Nd (PrfObj {cell = c,...},_)) = c;
976 (*in CalcTree/Subproblem an 'just_created_' model is created;
977 this is filled to 'untouched' by Model/Refine_Problem*)
978 fun just_created_ (PblObj {meth, probl, spec, ...}) =
979 null meth andalso null probl andalso spec = e_spec;
980 val e_origin = ([],e_spec,e_term): (ori list) * spec * term;
982 fun just_created (pt,(p,_):pos') =
983 let val ppobj = get_obj I pt p
984 in is_pblobj ppobj andalso just_created_ ppobj end;
986 (*.does the pos in the ctree exist ?.*)
987 fun existpt pos pt = can (get_obj I pt) pos;
988 (*.does the pos' in the ctree exist, ie. extra check for result in the node.*)
989 fun existpt' ((p,p_):pos') pt =
990 if can (get_obj I pt) p
992 Res => get_obj g_ostate pt p = Complete
996 (*.is this position appropriate for calculating intermediate steps?.*)
997 fun is_interpos ((_, Res):pos') = true
998 | is_interpos _ = false;
1000 fun last_onlev pt pos = not (existpt (lev_on pos) pt);
1003 (*.find the position of the next parent which is a PblObj in ptree.*)
1004 fun par_pblobj pt ([]:pos) = ([]:pos)
1006 let fun par pt [] = []
1007 | par pt p = if is_pblobj (get_obj I pt p) then p
1008 else par pt (lev_up p)
1009 in par pt (lev_up p) end;
1010 (* lev_up for hard_gen operating with pos = [...,0] *)
1012 (*.find the position and the children of the next parent which is a PblObj.*)
1013 fun par_children (Nd (PblObj _, children)) ([]:pos) = (children, []:pos)
1014 | par_children (pt as Nd (PblObj _, children)) p =
1015 let fun par [] = (children, [])
1016 | par p = let val Nd (obj, children) = get_nd pt p
1017 in if is_pblobj obj then (children, p) else par (lev_up p)
1019 in par (lev_up p) end;
1021 (*.get the children of a node in ptree.*)
1022 fun children (Nd (PblObj _, cn)) = cn
1023 | children (Nd (PrfObj _, cn)) = cn;
1026 (*.find the next parent, which is either a PblObj (return true)
1027 or a PrfObj with tac = Detail_Set (return false).*)
1028 (*FIXME.3.4.03:re-organize par_pbl_det after rls' --> rls*)
1029 fun par_pbl_det pt ([]:pos) = (true, []:pos, Erls)
1030 | par_pbl_det pt p =
1031 let fun par pt [] = (true, [], Erls)
1032 | par pt p = if is_pblobj (get_obj I pt p) then (true, p, Erls)
1033 else case get_obj g_tac pt p of
1034 (*Detail_Set rls' => (false, p, assoc_rls rls')
1035 (*^^^--- before 040206 after ---vvv*)
1036 |*)Rewrite_Set rls' => (false, p, assoc_rls rls')
1037 | Rewrite_Set_Inst (_, rls') =>
1038 (false, p, assoc_rls rls')
1039 | _ => par pt (lev_up p)
1040 in par pt (lev_up p) end;
1045 (*.get from the whole ptree by f : ppobj -> 'a.*)
1046 fun get_all f EmptyPtree = []
1047 | get_all f (Nd (b, [])) = [f b]
1048 | get_all f (Nd (b, bs)) = [f b] @ (get_alls f bs)
1049 and get_alls f [] = []
1050 | get_alls f pts = flat (map (get_all f) pts);
1053 (*.insert obj b into ptree at pos, ev.overwriting this pos.
1054 covers library.ML TODO.WN110315 rename*)
1055 fun insert b EmptyPtree ([]:pos) = Nd (b, [])
1056 | insert b EmptyPtree _ = raise PTREE "insert b Empty _"
1057 | insert b (Nd ( _, _)) [] = raise PTREE "insert b _ []"
1058 | insert b (Nd (b', bs)) (p::[]) =
1059 Nd (b', repl_app bs p (Nd (b,[])))
1060 | insert b (Nd (b', bs)) (p::ps) =
1061 Nd (b', repl_app bs p (insert b (nth p bs) ps));
1063 > type ppobj = string;
1064 > tracing (pr_ptree prfn (!pt));
1065 val pt = Unsynchronized.ref Empty;
1066 pt:= insert ("root'":ppobj) EmptyPtree [];
1067 pt:= insert ("xx1":ppobj) (!pt) [1];
1068 pt:= insert ("xx2":ppobj) (!pt) [2];
1069 pt:= insert ("xx3":ppobj) (!pt) [3];
1070 pt:= insert ("xx2.1":ppobj) (!pt) [2,1];
1071 pt:= insert ("xx2.2":ppobj) (!pt) [2,2];
1072 pt:= insert ("xx2.1.1":ppobj) (!pt) [2,1,1];
1073 pt:= insert ("xx2.1.2":ppobj) (!pt) [2,1,2];
1074 pt:= insert ("xx2.1.3":ppobj) (!pt) [2,1,3];
1077 (*.insert children to a node without children.*)
1078 (*compare: fun insert*)
1079 fun ins_chn _ EmptyPtree (_:pos) = raise PTREE "ins_chn: EmptyPtree"
1080 | ins_chn ns (Nd _) [] = raise PTREE "ins_chn: pos = []"
1081 | ins_chn ns (Nd (b, bs)) (p::[]) =
1082 if p > length bs then raise PTREE "ins_chn: pos not existent"
1083 else let val Nd (b', bs') = nth p bs
1084 in if null bs' then Nd (b, repl_app bs p (Nd (b', ns)))
1085 else raise PTREE "ins_chn: pos mustNOT be overwritten" end
1086 | ins_chn ns (Nd (b, bs)) (p::ps) =
1087 Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps));
1089 (* print_depth 11;ins_chn;print_depth 3; ###insert#########################*);
1092 (** apply f to obj at pos, f: ppobj -> ppobj **)
1094 fun appl_to_node f (Nd (b,bs)) = Nd (f b, bs);
1095 fun appl_obj f EmptyPtree [] = EmptyPtree
1096 | appl_obj f EmptyPtree _ = raise PTREE "appl_obj f Empty _"
1097 | appl_obj f (Nd (b, bs)) [] = Nd (f b, bs)
1098 | appl_obj f (Nd (b, bs)) (p::[]) =
1099 Nd (b, repl_app bs p (((appl_to_node f) o (nth p)) bs))
1100 | appl_obj f (Nd (b, bs)) (p::ps) =
1101 Nd (b, repl_app bs p (appl_obj f (nth p bs) (ps:pos)));
1103 (* for use by appl_obj *)
1104 fun repl_form f (PrfObj {cell=c,form= _,tac=tac,loc=loc,
1105 branch=branch,result=result,ostate=ostate}) =
1106 PrfObj {cell=c,form= f,tac=tac,loc=loc,
1107 branch=branch,result=result,ostate=ostate}
1108 | repl_form _ _ = raise PTREE "repl_form takes no PblObj";
1109 fun repl_pbl x (PblObj {cell=cell,origin=origin,fmz=fmz,
1110 spec=spec,probl=_,meth=meth,env=env,loc=loc,
1111 branch=branch,result=result,ostate=ostate}) =
1112 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl= x,
1113 meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1114 | repl_pbl _ _ = raise PTREE "repl_pbl takes no PrfObj";
1115 fun repl_met x (PblObj {cell=cell,origin=origin,fmz=fmz,
1116 spec=spec,probl=probl,meth=_,env=env,loc=loc,
1117 branch=branch,result=result,ostate=ostate}) =
1118 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
1119 meth= x,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1120 | repl_met _ _ = raise PTREE "repl_pbl takes no PrfObj";
1122 fun repl_spec x (PblObj {cell=cell,origin=origin,fmz=fmz,
1123 spec= _,probl=probl,meth=meth,env=env,loc=loc,
1124 branch=branch,result=result,ostate=ostate}) =
1125 PblObj {cell=cell,origin=origin,fmz=fmz,spec= x,probl=probl,
1126 meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1127 | repl_spec _ _ = raise PTREE "repl_domID takes no PrfObj";
1128 fun repl_domID x (PblObj {cell=cell,origin=origin,fmz=fmz,
1129 spec=(_,p,m),probl=probl,meth=meth,env=env,loc=loc,
1130 branch=branch,result=result,ostate=ostate}) =
1131 PblObj {cell=cell,origin=origin,fmz=fmz,spec=(x,p,m),probl=probl,
1132 meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1133 | repl_domID _ _ = raise PTREE "repl_domID takes no PrfObj";
1134 fun repl_pblID x (PblObj {cell=cell,origin=origin,fmz=fmz,
1135 spec=(d,_,m),probl=probl,meth=meth,env=env,loc=loc,
1136 branch=branch,result=result,ostate=ostate}) =
1137 PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,x,m),probl=probl,
1138 meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1139 | repl_pblID _ _ = raise PTREE "repl_pblID takes no PrfObj";
1140 fun repl_metID x (PblObj {cell=cell,origin=origin,fmz=fmz,
1141 spec=(d,p,_),probl=probl,meth=meth,env=env,loc=loc,
1142 branch=branch,result=result,ostate=ostate}) =
1143 PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,p,x),probl=probl,
1144 meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1145 | repl_metID _ _ = raise PTREE "repl_metID takes no PrfObj";
1147 fun repl_result l f' s (PrfObj {cell=cell,form=form,tac=tac,loc=_,
1148 branch=branch,result = _ ,ostate = _}) =
1149 PrfObj {cell=cell,form=form,tac=tac,loc= l,
1150 branch=branch,result = f',ostate = s}
1151 | repl_result l f' s (PblObj {cell=cell,origin=origin,fmz=fmz,
1152 spec=spec,probl=probl,meth=meth,env=env,loc=_,
1153 branch=branch,result= _ ,ostate= _}) =
1154 PblObj {cell=cell,origin=origin,fmz=fmz,
1155 spec=spec,probl=probl,meth=meth,env=env,loc= l,
1156 branch=branch,result= f',ostate= s};
1158 fun repl_tac x (PrfObj {cell=cell,form=form,tac= _,loc=loc,
1159 branch=branch,result=result,ostate=ostate}) =
1160 PrfObj {cell=cell,form=form,tac= x,loc=loc,
1161 branch=branch,result=result,ostate=ostate}
1162 | repl_tac _ _ = raise PTREE "repl_tac takes no PblObj";
1164 fun repl_branch b (PblObj {cell=cell,origin=origin,fmz=fmz,
1165 spec=spec,probl=probl,meth=meth,env=env,loc=loc,
1166 branch= _,result=result,ostate=ostate}) =
1167 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
1168 meth=meth,env=env,loc=loc,branch= b,result=result,ostate=ostate}
1169 | repl_branch b (PrfObj {cell=cell,form=form,tac=tac,loc=loc,
1170 branch= _,result=result,ostate=ostate}) =
1171 PrfObj {cell=cell,form=form,tac=tac,loc=loc,
1172 branch= b,result=result,ostate=ostate};
1175 (PblObj {cell=cell,origin=origin,fmz=fmz,
1176 spec=spec,probl=probl,meth=meth,env=_,loc=loc,
1177 branch=branch,result=result,ostate=ostate}) =
1178 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
1179 meth=meth,env=e,loc=loc,branch=branch,
1180 result=result,ostate=ostate}
1181 | repl_env _ _ = raise PTREE "repl_ets takes no PrfObj";
1184 (PblObj {cell=cell,origin=(_,spe,hdf),fmz=fmz,
1185 spec=spec,probl=probl,meth=meth,env=env,loc=loc,
1186 branch=branch,result=result,ostate=ostate}) =
1187 PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,
1188 meth=meth,env=env,loc=loc,branch=branch,
1189 result=result,ostate=ostate}
1190 | repl_oris _ _ = raise PTREE "repl_oris takes no PrfObj";
1191 fun repl_orispec spe
1192 (PblObj {cell=cell,origin=(oris,_,hdf),fmz=fmz,
1193 spec=spec,probl=probl,meth=meth,env=env,loc=loc,
1194 branch=branch,result=result,ostate=ostate}) =
1195 PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,
1196 meth=meth,env=env,loc=loc,branch=branch,
1197 result=result,ostate=ostate}
1198 | repl_orispec _ _ = raise PTREE "repl_orispec takes no PrfObj";
1200 fun repl_loc l (PblObj {cell=cell,origin=origin,fmz=fmz,
1201 spec=spec,probl=probl,meth=meth,env=env,loc=_,
1202 branch=branch,result=result,ostate=ostate}) =
1203 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
1204 meth=meth,env=env,loc=l,branch=branch,result=result,ostate=ostate}
1205 | repl_loc l (PrfObj {cell=cell,form=form,tac=tac,loc=_,
1206 branch=branch,result=result,ostate=ostate}) =
1207 PrfObj {cell=cell,form=form,tac=tac,loc= l,
1208 branch=branch,result=result,ostate=ostate};
1211 (PblObj {cell=cell,origin=origin,fmz=fmz,
1212 spec=spec,probl=probl,meth=meth,env=env,loc=loc,
1213 branch=branch,result=result,ostate=ostate}) =
1214 PblObj {cell=cell union cell',origin=origin,fmz=fmz,spec=spec,probl=probl,
1215 meth=meth,env=env,loc=loc,branch=branch,
1216 result=result,ostate=ostate}
1218 (PrfObj {cell=cell,form=form,tac=tac,loc=loc,
1219 branch=branch,result=result,ostate=ostate}) =
1220 PrfObj {cell=cell union cell',form=form,tac=tac,loc=loc,
1221 branch=branch,result=result,ostate=ostate};
1224 (*WN050219 put here for interpreting code for cut_tree below...*)
1226 bool * (*ALL itms+preconds true*)
1227 pos_ * (*model belongs to Problem | Method*)
1228 term * (*header: Problem... or Cas
1229 FIXXXME.12.03: item! for marking syntaxerrors*)
1230 itm list * (*model: given, find, relate*)
1231 ((bool * term) list) *(*model: preconds*)
1232 spec; (*specification*)
1233 val e_ocalhd = (false, Und, e_term, [e_itm], [(false, e_term)], e_spec);
1237 | ModSpec of ocalhd;
1238 val e_ptform = Form e_term;
1239 val e_ptform' = ModSpec e_ocalhd;
1243 (*.applies (snd f) to the branches at a pos if ((fst f) b),
1244 f : (ppobj -> bool) * (int -> ptree list -> ptree list).*)
1246 fun appl_branch f EmptyPtree [] = (EmptyPtree, false)
1247 | appl_branch f EmptyPtree _ = raise PTREE "appl_branch f Empty _"
1248 | appl_branch f (Nd ( _, _)) [] = raise PTREE "appl_branch f _ []"
1249 | appl_branch f (Nd (b, bs)) (p::[]) =
1250 if (fst f) b then (Nd (b, (snd f) (p:posel) bs), true)
1251 else (Nd (b, bs), false)
1252 | appl_branch f (Nd (b, bs)) (p::ps) =
1253 let val (b',bool) = appl_branch f (nth p bs) ps
1254 in (Nd (b, repl_app bs p b'), bool) end;
1256 (* for cut_level; appl_branch(deprecated) *)
1257 fun test_trans (PrfObj{branch = Transitive,...}) = true
1258 | test_trans (PblObj{branch = Transitive,...}) = true
1259 | test_trans _ = false;
1261 fun is_pblobj' pt (p:pos) =
1262 let val ppobj = get_obj I pt p
1263 in is_pblobj ppobj end;
1266 fun delete_result pt (p:pos) =
1267 (appl_obj (repl_result (fst (get_obj g_loc pt p), NONE)
1268 (e_term,[]) Incomplete) pt p);
1270 fun del_res (PblObj {cell, fmz, origin, spec, probl, meth,
1271 env, loc=(l1,_), branch, result, ostate}) =
1272 PblObj {cell=cell,fmz=fmz,origin=origin,spec=spec,probl=probl,meth=meth,
1273 env=env, loc=(l1,NONE), branch=branch, result=(e_term,[]),
1276 | del_res (PrfObj {cell, form, tac, loc=(l1,_), branch, result, ostate}) =
1277 PrfObj {cell=cell,form=form,tac=tac, loc=(l1,NONE), branch=branch,
1278 result=(e_term,[]), ostate=Incomplete};
1282 fun update_fmz pt pos x = appl_obj (repl_fmz x) pt pos;
1283 1.00 not used anymore*)
1285 (*FIXME.WN.12.03: update_X X pos pt -> pt could be chained by o (efficiency?)*)
1286 fun update_env pt pos x = appl_obj (repl_env x) pt pos;
1287 fun update_domID pt pos x = appl_obj (repl_domID x) pt pos;
1288 fun update_pblID pt pos x = appl_obj (repl_pblID x) pt pos;
1289 fun update_metID pt pos x = appl_obj (repl_metID x) pt pos;
1290 fun update_spec pt pos x = appl_obj (repl_spec x) pt pos;
1292 fun update_pbl pt pos x = appl_obj (repl_pbl x) pt pos;
1293 fun update_pblppc pt pos x = appl_obj (repl_pbl x) pt pos;
1295 fun update_met pt pos x = appl_obj (repl_met x) pt pos;
1297 fun update_metppc pt pos x =
1298 let val {rew_ord'=od,rls'=rs,asm_thm=at,asm_rls=ar,...} =
1299 get_obj g_met pt pos
1300 in appl_obj (repl_met
1301 {rew_ord'=od,rls'=rs,asm_thm=at,asm_rls=ar,ppc=x})
1303 fun update_metppc pt pos x = appl_obj (repl_met x) pt pos;
1305 (*fun union_cid pt pos x = appl_obj (uni__cid x) pt pos;*)
1307 fun update_branch pt pos x = appl_obj (repl_branch x) pt pos;
1308 fun update_tac pt pos x = appl_obj (repl_tac x) pt pos;
1310 fun update_oris pt pos x = appl_obj (repl_oris x) pt pos;
1311 fun update_orispec pt pos x = appl_obj (repl_orispec x) pt pos;
1313 (*done by append_* !! 3.5.02; ununsed WN050305 thus outcommented
1314 fun update_loc pt (p,_) (ScrState ([],[],NONE,
1315 Const ("empty",_),Sundef,false)) =
1316 appl_obj (repl_loc (NONE,NONE)) pt p
1317 | update_loc pt (p,Res) x =
1318 let val (lform,_) = get_obj g_loc pt p
1319 in appl_obj (repl_loc (lform,SOME x)) pt p end
1321 | update_loc pt (p,_) x =
1322 let val (_,lres) = get_obj g_loc pt p
1323 in appl_obj (repl_loc (SOME x,lres)) pt p end;-------------*)
1325 (*WN050305 for handling cut_tree in cappend_atomic -- TODO redesign !*)
1326 fun update_loc' pt p iss = appl_obj (repl_loc iss) pt p;
1328 (*13.8.02---------------------------
1329 fun get_loc EmptyPtree _ = NONE
1330 | get_loc pt (p,Res) =
1331 let val (lfrm,lres) = get_obj g_loc pt p
1332 in if lres = e_istate then lfrm else lres end
1333 | get_loc pt (p,_) =
1334 let val (lfrm,lres) = get_obj g_loc pt p
1335 in if lfrm = e_istate then lres else lfrm end; 5.10.00: too liberal ?*)
1336 (*13.8.02: options, because istate is no equalitype any more*)
1337 fun get_loc EmptyPtree _ = (e_istate, e_ctxt)
1338 | get_loc pt (p,Res) =
1339 (case get_obj g_loc pt p of
1341 | (NONE , NONE) => (e_istate, e_ctxt)
1342 | (_ , SOME i) => i)
1343 | get_loc pt (p,_) =
1344 (case get_obj g_loc pt p of
1345 (NONE , SOME i) => i (*13.8.02 just copied from ^^^: too liberal ?*)
1346 | (NONE , NONE) => (e_istate, e_ctxt)
1347 | (SOME i, _) => i);
1348 fun get_istate pt p = get_loc pt p |> #1;
1349 fun get_ctxt pt p = get_loc pt p |> #2;
1351 fun get_assumptions_ pt p = get_ctxt pt p |> get_assumptions;
1359 (*pos of the formula on FE relative to the current pos,
1360 which is the next writepos*)
1361 fun pre_pos ([]:pos) = []:pos
1363 let val (ps,p) = split_last pp
1364 in case p of 1 => ps | n => ps @ [n-1] end;
1366 (*WN.20.5.03 ... but not used*)
1367 fun posless [] (_::_) = true
1368 | posless (_::_) [] = false
1369 | posless (p::ps) (q::qs) = if p = q then posless ps qs else p < q;
1370 (* posless [2,3,4] [3,4,5];
1372 > posless [2,3,4] [1,2,3];
1374 > posless [2,3] [2,3,4];
1376 > posless [2,3,4] [2,3];
1378 > posless [6] [6,5,2];
1380 +++ see Isabelle/../library.ML*)
1383 (**.development for extracting an 'interval' from ptree.**)
1385 (*version 1 stopped 8.03 in favour of get_interval with !!!move_dn
1386 actually used (inefficient) version with move_dn: see modspec.sml*)
1389 fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*)
1390 fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)
1391 fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x;
1392 fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
1394 fun getnd i (b,p) q (Nd (po, nds)) =
1395 (if i <= 0 then [[b]] else []) @
1396 (getnds (i-1) true (b@[hdp p], tlp p) (tlq q)
1397 (take_fromto (hdp p) (hdq q) nds))
1399 and getnds _ _ _ _ [] = [] (*no children*)
1400 | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)
1402 | getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*)
1403 (getnd i ( b, p ) [99999] n1) @
1404 (getnd ~99999 (lev_on b,[0]) q n2)
1406 | getnds i _ (b,p) q [n1, n2] = (*intern, r-margin*)
1407 (getnd i ( b,[0]) [99999] n1) @
1408 (getnd ~99999 (lev_on b,[0]) q n2)
1410 | getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*)
1411 (getnd i ( b, p ) [99999] nd) @
1412 (getnds ~99999 false (lev_on b,[0]) q nds)
1414 | getnds i _ (b,p) q (nd::(nds as _::_)) = (*intern, ...*)
1415 (getnd i ( b,[0]) [99999] nd) @
1416 (getnds ~99999 false (lev_on b,[0]) q nds);
1418 (*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes
1419 where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
1420 (1) the 'f' are given
1421 (1a) by 'from' if 'f' = the respective element of 'from' (left margin)
1422 (1b) -inifinity, if 'f' > the respective element of 'from' (internal node)
1423 (2) the 't' ar given
1424 (2a) by 'to' if 't' = the respective element of 'to' (right margin)
1425 (2b) inifinity, if 't' < the respective element of 'to (internal node)'
1426 the 'f' and 't' are set by hdp,... *)
1427 fun get_trace pt p q =
1428 (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q)))
1429 (take_fromto (hdp p) (hdq q) (children pt));
1431 (*WN0510 stoppde this development;
1432 actually used (inefficient) version with move_dn: getFormulaeFromTo*)
1437 fun get_somespec ((dI,pI,mI):spec) ((dI',pI',mI'):spec) =
1438 let val domID = if dI = e_domID
1439 then if dI' = e_domID
1440 then error"pt_extract: no domID in probl,origin"
1443 val pblID = if pI = e_pblID
1444 then if pI' = e_pblID
1445 then error"pt_extract: no pblID in probl,origin"
1448 val metID = if mI = e_metID
1449 then if pI' = e_metID
1450 then error"pt_extract: no metID in probl,origin"
1453 in (domID, pblID, metID):spec end;
1454 fun get_somespec' ((dI,pI,mI):spec) ((dI',pI',mI'):spec) =
1455 let val domID = if dI = e_domID then dI' else dI
1456 val pblID = if pI = e_pblID then pI' else pI
1457 val metID = if mI = e_metID then mI' else mI
1458 in (domID, pblID, metID):spec end;
1460 (*extract a formula or model from ptree for itms2itemppc or model2xml*)
1461 fun preconds2str bts =
1462 (strs2str o (map (linefeed o pair2str o
1464 (apfst bool2str)))) bts;
1465 fun ocalhd2str ((b, p, hdf, itms, prec, spec):ocalhd) =
1466 "("^bool2str b^", "^pos_2str p^", "^term2str hdf^
1467 ", "^itms2str_ (thy2ctxt' "Isac") itms^
1468 ", "^preconds2str prec^", \n"^spec2str spec^" )";
1472 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj;
1475 (**.functions for the 'ptree iterator' as seen from the FE-Kernel interface.**)
1477 (*move one step down into existing nodes of ptree; regard TransitiveB
1478 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~##################
1479 fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*)
1480 (* val (Nd (c, ns), ([],p_)) = (pt, get_pos cI uI);
1483 then case p_ of (*Frm => ([], Pbl) 1.12.03
1484 |*) Res => raise PTREE "move_dn: end of calculation"
1485 | _ => if null ns (*go down from Pbl + Met*)
1486 then raise PTREE "move_dn: solve problem not started"
1488 else (case p_ of Res => raise PTREE "move_dn: end of (sub-)tree"
1490 then raise PTREE "move_dn: pos not existent 1"
1493 (*iterate towards end of pos*)
1494 (* val (P,(Nd (_, ns)),(p::(ps as (_::_)),p_)) = ([]:pos, pt, get_pos cI uI);
1495 val (P,(Nd (_, ns)),(p::(ps as (_::_)),p_)) = ((P@[p]),(nth p ns),(ps, p_));
1497 | move_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
1498 if p > length ns then raise PTREE "move_dn: pos not existent 2"
1499 else move_dn ((P@[p]): pos) (nth p ns) (ps, p_)
1500 (* val (P, (Nd (c, ns)), ([p], p_)) = ((P@[p]), (nth p ns), (ps, p_));
1501 val (P, (Nd (c, ns)), ([p], p_)) = ([],pt,get_pos cI uI);
1503 | move_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1504 if p > length ns then raise PTREE "move_dn: pos not existent 3"
1505 else if is_pblnd (nth p ns) then
1506 ((*tracing("### move_dn: is_pblnd (nth p ns), P= "^ints2str' P^", \n"^
1507 "length ns= "^((string_of_int o length) ns)^
1508 ", p= "^string_of_int p^", p_= "^pos_2str p_);*)
1509 case p_ of Res => if p = length ns
1510 then if g_ostate c = Complete then (P, Res)
1511 else raise PTREE (ints2str' P^" not complete")
1512 (*FIXME here handle not-sequent-branches*)
1513 else if g_branch c = TransitiveB
1514 andalso (not o is_pblnd o (nth (p+1))) ns
1516 else (P@[p+1], if is_pblnd (nth (p+1) ns)
1518 | _ => if (null o children o (nth p)) ns (*go down from Pbl*)
1519 then raise PTREE "move_dn: solve subproblem not started"
1521 if (is_pblnd o hd o children o (nth p)) ns
1524 (* val (P, Nd (c, ns), ([p], p_)) = ([], pt, ([1], Frm));
1526 else case p_ of Frm => if (null o children o (nth p)) ns
1527 (*then if g_ostate c = Complete then (P@[p],Res)*)
1528 then if g_ostate' (nth p ns) = Complete
1530 else raise PTREE "move_dn: pos not existent 4"
1531 else (P @ [p, 1], (*go down*)
1532 if (is_pblnd o hd o children o (nth p)) ns
1534 | Res => if p = length ns
1536 if g_ostate c = Complete then (P, Res)
1537 else raise PTREE (ints2str' P^" not complete")
1539 if g_branch c = TransitiveB
1540 andalso (not o is_pblnd o (nth (p+1))) ns
1541 then if (null o children o (nth (p+1))) ns
1543 else (P@[p+1,1], Frm)(*040221*)
1544 else (P@[p+1], if is_pblnd (nth (p+1) ns)
1547 (*.move one step down into existing nodes of ptree; skip Res = Frm.nxt;
1548 move_dn at the end of the calc-tree raises PTREE.*)
1549 fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*)
1551 Res => raise PTREE "move_dn: end of calculation"
1552 | _ => if null ns (*go down from Pbl + Met*)
1553 then raise PTREE "move_dn: solve problem not started"
1555 | move_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =(*iterate to end of pos*)
1556 if p > length ns then raise PTREE "move_dn: pos not existent 2"
1557 else move_dn ((P@[p]): pos) (nth p ns) (ps, p_)
1559 | move_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1560 if p > length ns then raise PTREE "move_dn: pos not existent 3"
1563 if p = length ns (*last Res on this level: go a level up*)
1564 then if g_ostate c = Complete then (P, Res)
1565 else raise PTREE (ints2str' P^" not complete 1")
1566 else (*go to the next Nd on this level, or down into the next Nd*)
1567 if is_pblnd (nth (p+1) ns) then (P@[p+1], Pbl)
1569 if g_res' (nth p ns) = g_form' (nth (p+1) ns)
1570 then if (null o children o (nth (p+1))) ns
1571 then (*take the Res if Complete*)
1572 if g_ostate' (nth (p+1) ns) = Complete
1574 else raise PTREE (ints2str' (P@[p+1])^
1576 else (P@[p+1,1], Frm)(*go down into the next PrfObj*)
1577 else (P@[p+1], Frm)(*take Frm: exists if the Nd exists*)
1578 | Frm => (*go down or to the Res of this Nd*)
1579 if (null o children o (nth p)) ns
1580 then if g_ostate' (nth p ns) = Complete then (P @ [p], Res)
1581 else raise PTREE (ints2str' (P @ [p])^" not complete 3")
1582 else (P @ [p, 1], Frm)
1583 | _ => (*is Pbl or Met*)
1584 if (null o children o (nth p)) ns
1585 then raise PTREE "move_dn:solve subproblem not startd"
1587 if (is_pblnd o hd o children o (nth p)) ns
1591 (*.go one level down into ptree.*)
1592 fun movelevel_dn [] (Nd (c, ns)) ([],p_) = (*root problem*)
1595 then raise PTREE "solve problem not started"
1596 else ([1], if (is_pblnd o hd) ns then Pbl else Frm)
1597 else raise PTREE "pos not existent 1"
1599 (*iterate towards end of pos*)
1600 | movelevel_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
1601 if p > length ns then raise PTREE "pos not existent 2"
1602 else movelevel_dn (P@[p]) (nth p ns) (ps, p_)
1604 | movelevel_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1605 if p > length ns then raise PTREE "pos not existent 3" else
1608 then raise PTREE "no children"
1610 if g_branch c = TransitiveB
1611 then if (null o children o (nth (p+1))) ns
1612 then raise PTREE "no children"
1614 if (is_pblnd o hd o children o (nth (p+1))) ns
1616 else if (null o children o (nth p)) ns
1617 then raise PTREE "no children"
1618 else (P @ [p, 1], if (is_pblnd o hd o children o (nth p)) ns
1620 | _ => if (null o children o (nth p)) ns
1621 then raise PTREE "no children"
1622 else (P @ [p, 1], (*go down*)
1623 if (is_pblnd o hd o children o (nth p)) ns
1628 (*.go to the previous position in ptree; regard TransitiveB.*)
1629 fun move_up _ (Nd (c, ns)) (([],p_):pos') = (*root problem*)
1631 then case p_ of Res => if null ns then ([], Pbl) (*Res -> Pbl (not Met)!*)
1632 else ([length ns], Res)
1633 | _ => raise PTREE "begin of calculation"
1634 else raise PTREE "pos not existent"
1636 | move_up P (Nd (_, ns)) (p::(ps as (_::_)),p_) = (*iterate to end of pos*)
1637 if p > length ns then raise PTREE "pos not existent"
1638 else move_up (P@[p]) (nth p ns) (ps,p_)
1640 | move_up P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1641 if p > length ns then raise PTREE "pos not existent"
1642 else if is_pblnd (nth p ns) then
1644 let val nc = (length o children o (nth p)) ns
1645 in if nc = 0 then (P@[p], Pbl) (*Res -> Pbl (not Met)!*)
1646 else (P @ [p, nc], Res) end (*go down*)
1647 | _ => if p = 1 then (P, Pbl) else (P@[p-1], Res)
1648 else case p_ of Frm => if p <> 1 then (P, Frm)
1649 else if is_pblobj c then (P, Pbl) else (P, Frm)
1651 let val nc = (length o children o (nth p)) ns
1652 in if nc = 0 (*cannot go down*)
1653 then if g_branch c = TransitiveB andalso p <> 1
1654 then (P@[p-1], Res) else (P@[p], Frm)
1655 else (P @ [p, nc], Res) end; (*go down*)
1659 (*.go one level up in ptree; sets the position on Frm.*)
1660 fun movelevel_up _ (Nd (c, ns)) (([],p_):pos') = (*root problem*)
1661 raise PTREE "pos not existent"
1663 (*iterate towards end of pos*)
1664 | movelevel_up P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
1665 if p > length ns then raise PTREE "pos not existent"
1666 else movelevel_up (P@[p]) (nth p ns) (ps,p_)
1668 | movelevel_up P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1669 if p > length ns then raise PTREE "pos not existent"
1670 else if is_pblobj c then (P, Pbl) else (P, Frm);
1673 (*.go to the next calc-head up in the calc-tree.*)
1674 fun movecalchd_up pt ((p, Res):pos') =
1675 (par_pblobj pt p, Pbl):pos'
1676 | movecalchd_up pt (p, _) =
1677 if is_pblobj (get_obj I pt p)
1678 then (p, Pbl) else (par_pblobj pt p, Pbl);
1680 (*.determine the previous pos' on the same level.*)
1681 (*WN0502 made for interSteps; _only_ works for branch TransitiveB*)
1682 fun lev_pred' pt (pos:pos' as ([],Res)) = ([],Pbl):pos'
1683 | lev_pred' pt (pos:pos' as (p, Res)) =
1684 let val (p', last) = split_last p
1686 then if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm)
1687 else if get_obj g_res pt (p' @ [last - 1]) = get_obj g_form pt p
1688 then (p' @ [last - 1], Res) (*TransitiveB*)
1689 else if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm)
1692 (*.determine the next pos' on the same level.*)
1693 fun lev_on' pt (([],Pbl):pos') = ([],Res):pos'
1694 | lev_on' pt (p, Res) =
1695 if get_obj g_res pt p = get_obj g_form pt (lev_on p)(*TransitiveB*)
1696 then if existpt' (lev_on p, Res) pt then (lev_on p, Res)
1697 else error ("lev_on': (p, Res) -> (p, Res) not existent, \
1698 \p = "^ints2str' (lev_on p))
1699 else (lev_on p, Frm)
1700 | lev_on' pt (p, _) =
1701 if existpt' (p, Res) pt then (p, Res)
1702 else error ("lev_on': (p, Frm) -> (p, Res) not existent, \
1703 \p = "^ints2str' p);
1705 fun exist_lev_on' pt p = (lev_on' pt p; true) handle _ => false;
1707 (*.is the pos' at the last element of a calulation _AND_ can be continued.*)
1708 (* val (pt, pos as (p,p_)) = (pt, ([1],Frm));
1710 fun is_curr_endof_calc pt (([],Res) : pos') = false
1711 | is_curr_endof_calc pt (pos as (p,_)) =
1712 not (exist_lev_on' pt pos)
1713 andalso get_obj g_ostate pt (lev_up p) = Incomplete;
1716 (**.insert into ctree and cut branches accordingly.**)
1718 (*.get all positions of certain intervals on the ctree.*)
1719 (*OLD VERSION without move_dn; kept for occasional redesign
1720 get all pos's to be cut in a ptree
1721 below a pos or from a ptree list after i-th element (NO level_up).*)
1722 fun get_allpos' (_:pos, _:posel) EmptyPtree = ([]:pos' list)
1723 | get_allpos' (p, 1) (Nd (b, bs)) = (*p is pos of Nd*)
1724 if g_ostate b = Incomplete
1725 then ((*tracing("get_allpos' (p, 1) Incomplete: p="^ints2str' p);*)
1726 [(p,Frm)] @ (get_allpos's (p, 1) bs)
1728 else ((*tracing("get_allpos' (p, 1) else: p="^ints2str' p);*)
1729 [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)]
1731 (*WN041020 here we assume what is presented on the worksheet ?!*)
1732 | get_allpos' (p, i) (Nd (b, bs)) = (*p is pos of Nd*)
1733 if length bs > 0 orelse is_pblobj b
1734 then if g_ostate b = Incomplete
1735 then [(p,Frm)] @ (get_allpos's (p, 1) bs)
1736 else [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)]
1738 if g_ostate b = Incomplete
1741 (*WN041020 here we assume what is presented on the worksheet ?!*)
1742 and get_allpos's _ [] = []
1743 | get_allpos's (p, i) (pt::pts) = (*p is pos of parent-Nd*)
1744 (get_allpos' (p@[i], i) pt) @ (get_allpos's (p, i+1) pts);
1746 (*.get all positions of certain intervals on the ctree.*)
1747 (*NEW version WN050225*)
1751 (*before WN041019......
1752 val cut_branch = (test_trans, curry take):
1753 (ppobj -> bool) * (int -> ptree list -> ptree list);
1754 .. formlery used for ...
1755 fun cut_tree''' _ [] = EmptyPtree
1756 | cut_tree''' pt pos =
1757 let val (pt',cut) = appl_branch cut_branch pt pos
1758 in if cut andalso length pos > 1 then cut_tree''' pt' (lev_up pos)
1761 (*OLD version before WN050225*)
1762 (*WN050106 like cut_level, but deletes exactly 1 node --- for tests ONLY*)
1763 fun cut_level_'_ (_:pos' list) (_:pos) EmptyPtree (_:pos') =
1764 raise PTREE "cut_level_'_ Empty _"
1765 | cut_level_'_ _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level_'_ _ []"
1766 | cut_level_'_ cuts P (Nd (b, bs)) (p::[],p_) =
1768 then (Nd (b, drop_nth [] (p:posel, bs)),
1771 (if p_ = Frm then [(P@[p],Res)] else ([]:pos' list)) @
1772 (*WN041020 here we assume what is presented on the worksheet ?!*)
1773 (get_allpos's (P, p+1) (drop_nth [] (p, bs))))
1775 else (Nd (b, bs), cuts)
1776 | cut_level_'_ cuts P (Nd (b, bs)) ((p::ps),p_) =
1777 let val (bs',cuts') = cut_level_'_ cuts P (nth p bs) (ps, p_)
1778 in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
1781 fun cut_level (_:pos' list) (_:pos) EmptyPtree (_:pos') =
1782 raise PTREE "cut_level EmptyPtree _"
1783 | cut_level _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level _ []"
1785 | cut_level cuts P (Nd (b, bs)) (p::[],p_) =
1787 then (Nd (b, take (p:posel, bs)),
1789 (if p_ = Frm andalso (*#*) g_ostate b = Complete
1790 then [(P@[p],Res)] else ([]:pos' list)) @
1791 (*WN041020 here we assume what is presented on the worksheet ?!*)
1792 (get_allpos's (P, p+1) (takerest (p, bs))))
1793 else (Nd (b, bs), cuts)
1795 | cut_level cuts P (Nd (b, bs)) ((p::ps),p_) =
1796 let val (bs',cuts') = cut_level cuts P (nth p bs) (ps, p_)
1797 in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
1799 (*OLD version before WN050219, overwritten below*)
1800 fun cut_tree _ (([],_):pos') = raise PTREE "cut_tree _ ([],_)"
1801 | cut_tree pt (pos as ([p],_)) =
1802 let val (pt', cuts) = cut_level ([]:pos' list) [] pt pos
1803 in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
1804 then [] else [([],Res)])) end
1805 | cut_tree pt (p,p_) =
1807 fun cutfn pt cuts (p,p_) =
1808 let val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_)
1809 val cuts'' = if get_obj g_ostate pt (lev_up p) = Incomplete
1810 then [] else [(lev_up p, Res)]
1811 in if length cuts' > 0 andalso length p > 1
1812 then cutfn pt' (cuts @ cuts') (lev_up p, Frm(*-->(p,Res)*))
1813 else (pt',cuts @ cuts') end
1814 val (pt', cuts) = cutfn pt [] (p,p_)
1815 in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
1816 then [] else [([], Res)])) end;
1819 (*########/ inserted from ctreeNEW.sml \#################################**)
1821 (*.get all positions in a ptree until ([],Res) or ostate=Incomplete
1823 pos' list -> : accumulated, start with []
1824 pos -> : the offset for subtrees wrt the root
1825 ptree -> : (sub)tree
1826 pos' : initialization (the last pos' before ...)
1827 -> pos' list : of positions in this (sub) tree (relative to the root)
1829 (* val (cuts, P, pt, pos) = ([], [3], get_nd pt [3], ([], Frm):pos');
1830 val (cuts, P, pt, pos) = ([], [2], get_nd pt [2], ([], Frm):pos');
1831 length (children pt);
1833 fun get_allp (cuts:pos' list) (P:pos, pos:pos') pt =
1834 (let val nxt = move_dn [] pt pos (*exn if Incomplete reached*)
1835 in if nxt <> ([],Res)
1836 then get_allp (cuts @ [nxt]) (P, nxt) pt
1837 else (map (apfst (curry op@ P)) (cuts @ [nxt])): pos' list
1838 end) handle PTREE _ => (map (apfst (curry op@ P)) cuts);
1841 (*the pts are assumed to be on the same level*)
1842 fun get_allps (cuts: pos' list) (P:pos) [] = cuts
1843 | get_allps cuts P (pt::pts) =
1844 let val below = get_allp [] (P, ([], Frm)) pt
1847 then (P, Pbl)::below
1848 else if last_elem P = 1
1849 then (P, Frm)::below
1850 else (*Trans*) below
1851 val levres = levfrm @ (if null below then [(P, Res)] else [])
1852 in get_allps (cuts @ levres) (lev_on P) pts end;
1855 (**.these 2 funs decide on how far cut_tree goes.**)
1856 (*.shall the nodes _after_ the pos to be inserted at be deleted?.*)
1857 fun test_trans (PrfObj{branch = Transitive,...}) = true
1858 | test_trans (PrfObj{branch = NoBranch,...}) = true
1859 | test_trans (PblObj{branch = Transitive,...}) = true
1860 | test_trans (PblObj{branch = NoBranch,...}) = true
1861 | test_trans _ = false;
1862 (*.shall cutting be continued on the higher level(s)?
1863 the Nd regarded will NOT be changed.*)
1864 fun cutlevup (PblObj _) = false (*for tests of LK0502*)
1865 | cutlevup _ = true;
1866 val cutlevup = test_trans;(*WN060727 after summerterm tests.LK0502 withdrawn*)
1868 (*cut_bottom new sml603..608
1869 cut the level at the bottom of the pos (used by cappend_...)
1870 and handle the parent in order to avoid extra case for root
1871 fn: ptree -> : the _whole_ ptree for cut_levup
1872 pos * posel -> : the pos after split_last
1873 ptree -> : the parent of the Nd to be cut
1875 (ptree * : the updated ptree
1876 pos' list) * : the pos's cut
1877 bool : cutting shall be continued on the higher level(s)
1879 fun cut_bottom _ (pt' as Nd (b, [])) = ((pt', []), cutlevup b)
1880 | cut_bottom (P:pos, p:posel) (Nd (b, bs)) =
1881 let (*divide level into 3 parts...*)
1882 val keep = take (p - 1, bs)
1883 val pt' as Nd (_,bs') = nth p bs
1884 (*^^^^^_here_ will be 'insert'ed by 'append_..'*)
1885 val (tail, tp) = (takerest (p, bs),
1886 if null (takerest (p, bs)) then 0 else p + 1)
1887 val (children, cuts) =
1890 (if is_pblnd pt' then [(P @ [p], Pbl)] else [])
1891 @ (get_allp [] (P @ [p], (P, Frm)) pt')
1892 @ (get_allps [] (P @ [p+1]) tail))
1893 else (keep @ [(*'insert'ed by 'append_..'*)] @ tail,
1894 get_allp [] (P @ [p], (P, Frm)) pt')
1897 then (Nd (del_res b, children),
1898 cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
1899 else (Nd (b, children), cuts)
1900 (*val _= tracing("####cut_bottom (P, p)="^pos2str (P @ [p])^
1901 ", Nd=.............................................")
1903 val _= tracing("####cut_bottom form='"^
1904 term2str (get_obj g_form pt'' []))
1905 val _= tracing("####cut_bottom cuts#="^string_of_int (length cuts)^
1906 ", cuts="^pos's2str cuts)*)
1907 in ((pt'', cuts:pos' list), cutlevup b) end;
1910 (*.go all levels from the bottom of 'pos' up to the root,
1911 on each level compose the children of a node and accumulate the cut Nds
1913 pos' list -> : for accumulation
1914 bool -> : cutting shall be continued on the higher level(s)
1915 ptree -> : the whole ptree for 'get_nd pt P' on each level
1916 ptree -> : the Nd from the lower level for insertion at path
1917 pos * posel -> : pos=path split for convenience
1918 ptree -> : Nd the children of are under consideration on this call
1920 ptree * pos' list : the updated parent-Nd and the pos's of the Nds cut
1922 fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) =
1923 let (*divide level into 3 parts...*)
1924 val keep = take (p - 1, bs)
1925 (*val pt' comes as argument from below*)
1926 val (tail, tp) = (takerest (p, bs),
1927 if null (takerest (p, bs)) then 0 else p + 1)
1928 val (children, cuts') =
1930 then (keep @ [pt'], get_allps [] (P @ [p+1]) tail)
1931 else (keep @ [pt'] @ tail, [])
1932 val clevup' = if clevup then cutlevup b else false
1933 (*the first Nd with false stops cutting on all levels above*)
1936 then (Nd (del_res b, children),
1937 cuts' @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
1938 else (Nd (b, children), cuts')
1939 (*val _= tracing("#####cut_levup clevup= "^bool2str clevup)
1940 val _= tracing("#####cut_levup cutlevup b= "^bool2str (cutlevup b))
1941 val _= tracing("#####cut_levup (P, p)="^pos2str (P @ [p])^
1942 ", Nd=.............................................")
1944 val _= tracing("#####cut_levup form='"^
1945 term2str (get_obj g_form pt'' []))
1946 val _= tracing("#####cut_levup cuts#="^string_of_int (length cuts)^
1947 ", cuts="^pos's2str cuts)*)
1948 in if null P then (pt'', (cuts @ cuts'):pos' list)
1949 else let val (P, p) = split_last P
1950 in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P)
1954 (*.cut nodes after and below an inserted node in the ctree;
1955 the cuts range is limited by the predicate 'fun cutlevup'.*)
1956 fun cut_tree pt (pos,_) =
1957 if not (existpt pos pt)
1958 then (pt,[]) (*appending a formula never cuts anything*)
1959 else let val (P, p) = split_last pos
1960 val ((pt', cuts), clevup) = cut_bottom (P, p) (get_nd pt P)
1961 (* pt' is the updated parent of the Nd to cappend_..*)
1962 in if null P then (pt', cuts)
1963 else let val (P, p) = split_last P
1964 in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P)
1968 fun append_atomic p l f r f' s pt =
1969 let (**val _= tracing("#@append_atomic: pos ="^pos2str p)**)
1970 val (iss, f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
1972 ((fst (get_obj g_loc pt p), SOME l),
1973 get_obj g_form pt p)
1974 else ((NONE, SOME l), f)
1975 in insert (PrfObj {cell = NONE,
1981 ostate= s}) pt p end;
1984 (*20.8.02: cappend_* FIXXXXME cut branches below cannot be decided here:
1985 detail - generate - cappend: inserted, not appended !!!
1987 cut decided in applicable_in !?!
1989 fun cappend_atomic pt p loc f r f' s =
1990 (* val (pt, p, loc, f, r, f', s) =
1991 (pt,p,l,f,Rewrite_Set_Inst (subst2subs subs',id_rls rls'),
1994 ((*tracing("##@cappend_atomic: pos ="^pos2str p);*)
1995 apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm))
1997 (*TODO.WN050305 redesign the handling of istates*)
1998 fun cappend_atomic pt p ist_res f r f' s =
1999 if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
2000 then (*after Take: transfer Frm and respective istate*)
2001 let val (ist_form, f) = (get_loc pt (p,Frm),
2002 get_obj g_form pt p)
2003 val (pt, cs) = cut_tree pt (p,Frm)
2004 val pt = append_atomic p (e_istate, e_ctxt) f r f' s pt
2005 val pt = update_loc' pt p (SOME ist_form, SOME ist_res)
2007 else apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
2010 (* called by Take *)
2011 fun append_form p l f pt =
2012 ((*tracing("##@append_form: pos ="^pos2str p);*)
2013 insert (PrfObj {cell = NONE,
2014 form = (*if existpt p pt
2015 andalso get_obj g_tac pt p = Empty_Tac
2016 (*distinction from 'old' (+complete!) pobjs*)
2017 then get_obj g_form pt p else*) f,
2019 loc = (SOME l, NONE),
2021 result= (e_term,[]),
2022 ostate= Incomplete}) pt p
2024 (* val (p,loc,f) = ([1], e_istate, str2term "x + 1 = 2");
2025 val (p,loc,f) = (fst p, e_istate, str2term "-1 + x = 0");
2027 fun cappend_form pt p loc f =
2028 ((*tracing("##@cappend_form: pos ="^pos2str p);*)
2029 apfst (append_form p loc f) (cut_tree pt (p,Frm))
2031 fun cappend_form pt p loc f =
2032 let (*val _= tracing("##@cappend_form: pos ="^pos2str p)
2033 val _= tracing("##@cappend_form before cut_tree: loc ="^istate2str loc)*)
2034 val (pt', cs) = cut_tree pt (p,Frm)
2035 val pt'' = append_form p loc f pt'
2036 (*val _= tracing("##@cappend_form after append: loc ="^
2037 istates2str (get_obj g_loc pt'' p))*)
2042 fun append_result pt p l f s =
2043 ((*tracing("##@append_result: pos ="^pos2str p);*)
2044 (appl_obj (repl_result (fst (get_obj g_loc pt p),
2045 SOME l) f s) pt p, [])
2049 (*WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml*)
2050 fun append_parent p l f r b pt =
2051 let (*val _= tracing("###append_parent: pos ="^pos2str p);*)
2052 val (ll,f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
2053 then ((fst (get_obj g_loc pt p), SOME l),
2054 get_obj g_form pt p)
2055 else ((SOME l, NONE), f)
2062 result= (e_term,[]),
2063 ostate= Incomplete}) pt p end;
2064 fun cappend_parent pt p loc f r b =
2065 ((*tracing("###cappend_parent: pos ="^pos2str p);*)
2066 apfst (append_parent p loc f r b) (cut_tree pt (p,Und))
2070 fun append_problem [] l fmz (strs,spec,hdf) _ =
2071 ((*tracing("###append_problem: pos = []");*)
2074 origin= (strs,spec,hdf),
2077 probl = []:itm list,
2080 loc = (SOME l, NONE),
2081 branch= TransitiveB,(*FIXXXXXME.27.8.03: for equations only*)
2082 result= (e_term,[]),
2083 ostate= Incomplete},[]))
2085 | append_problem p l fmz (strs,spec,hdf) pt =
2086 ((*tracing("###append_problem: pos ="^pos2str p);*)
2089 origin= (strs,spec,hdf),
2092 probl = []:itm list,
2095 loc = (SOME l, NONE),
2096 branch= TransitiveB,
2097 result= (e_term,[]),
2098 ostate= Incomplete}) pt p
2100 fun cappend_problem _ [] loc fmz ori =
2101 ((*tracing("###cappend_problem: pos = []");*)
2102 (append_problem [] loc fmz ori EmptyPtree,[])
2104 | cappend_problem pt p loc fmz ori =
2105 ((*tracing("###cappend_problem: pos ="^pos2str p);*)
2106 apfst (append_problem p (loc:(istate * Proof.context)) fmz ori) (cut_tree pt (p,Frm))
2109 (*.get the theory explicitly specified for the rootpbl;
2110 thus use this function _after_ finishing specification.*)
2111 fun rootthy (Nd (PblObj {spec=(thyID, _, _),...}, _)) = assoc_thy thyID
2112 | rootthy _ = error "rootthy";