1 (* use"../ME/ctree.sml";
6 writeln (pr_ptree pr_short pt);
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 test_trans : ppobj -> bool
101 val uni__asm : (string * pos) list -> ppobj -> ppobj
102 val uni__cid : cellID list -> ppobj -> ppobj *)
103 val union_asm : ptree -> pos -> (string * pos) list -> ptree
104 val union_cid : ptree -> pos -> cellID list -> ptree
105 val update_branch : ptree -> pos -> branch -> ptree
106 val update_domID : ptree -> pos -> domID -> ptree
107 val update_met : ptree -> pos -> meth -> ptree
108 val update_metppc : ptree -> pos -> item ppc -> ptree
109 val update_metID : ptree -> pos -> metID -> ptree
110 val update_tac : ptree -> pos -> tac -> ptree
111 val update_pbl : ptree -> pos -> pblID * item ppc -> ptree
112 val update_pblppc : ptree -> pos -> item ppc -> ptree
113 val update_pblID : ptree -> pos -> pblID -> ptree
114 val update_spec : ptree -> pos -> spec -> ptree
115 val update_subs : ptree -> pos -> (string * string) list -> ptree
117 val rep_pblobj : ppobj
118 -> {branch:branch, cell:cid, env:envp, loc:loc, meth:meth, model:cterm' ppc,
119 origin:cterm' list * spec, ostate:ostate, probl:pblID * item ppc,
120 result:cterm', spec:spec}
121 val rep_prfobj : ppobj
122 -> {branch:branch, cell:cid, form:cterm', loc:loc, tac:tac,
123 ostate:ostate, result:cterm'}
127 structure Ptree (**): PTREE (**) =
131 type env = (term * term) list;
135 NoBranch | AndB | OrB
136 | TransitiveB (* FIXXXME.8.03: set branch from met in Apply_Method
137 FIXXXME.0402: -"- in Begin_Trans'*)
138 | SequenceB | IntersectB | CollectB | MapB;
139 fun branch2str NoBranch = "NoBranch"
140 | branch2str AndB = "AndB"
141 | branch2str OrB = "OrB"
142 | branch2str TransitiveB = "TransitiveB"
143 | branch2str SequenceB = "SequenceB"
144 | branch2str IntersectB = "IntersectB"
145 | branch2str CollectB = "CollectB"
146 | branch2str MapB = "MapB";
149 Incomplete | Complete | Inconsistent(*WN041020 latter unused*);
152 type cid = cellID list;
154 type posel = int; (* roundabout for (some of) nice signatures *)
155 type pos = posel list;
156 val pos2str = ints2str';
158 Pbl (*PblObj-position: problem-type*)
159 | Met (*PblObj-position: method*)
160 | Frm (*PblObj-position: -> Pbl in ME (not by moveDown !)
161 | PrfObj-position: formula*)
162 | Res (*PblObj | PrfObj-position: result*)
164 fun pos_2str Pbl = "Pbl"
165 | pos_2str Met = "Met"
166 | pos_2str Frm = "Frm"
167 | pos_2str Res = "Res"
168 | pos_2str Und = "Und";
170 type pos' = pos * pos_;
171 (*WN.12.03 remembering interator (pos * pos_) for ptree
172 pos : lev_on, lev_dn, lev_up,
173 lev_onFrm, lev_dnRes (..see solve Apply_Method !)
175 # generate1 sets pos_ if possible ...?WN0502?NOT...
176 # generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn
177 exceptions: Begin/End_Trans
178 # thus generate(1) called in
180 .# nxt_solv (tac_ -cases); general case:
181 val pos' = case pos' of (p,Res) => (lev_on p',Res) | _ => pos'
183 generate1...(Rewrite(f,..,res))..(pos, pos_)
184 cappend_atomic.................pos ////// gets f+res always!!!
185 cut_tree....................pos, pos_
187 fun pos'2str (p,p_) = pair2str (ints2str' p, pos_2str p_);
188 fun pos's2str ps = (strs2str' o (map pos'2str)) ps;
189 val e_pos' = ([],Und):pos';
191 fun res2str (t, ts) = pair2str (term2str t, terms2str ts);
192 fun asm2str (t, p:pos) = pair2str (term2str t, ints2str' p);
193 fun asms2str asms = (strs2str' o (map asm2str)) asms;
197 datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)
199 | R (*go right at $*)
200 | D; (*go down at Abs*)
201 type loc_ = lrd list;
205 fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k;
207 (*26.4.02: never used after introduction of scripts !!!
208 type loc = loc_ * (* + interpreter-state *)
209 (loc_ * rls') (* -"- for script of the ruleset*)
211 val e_loc = ([],None):loc;
212 val ee_loc = (e_loc,e_loc);*)
215 datatype safe = Sundef | Safe | Unsafe | Helpless;
216 fun safe2str Sundef = "Sundef"
217 | safe2str Safe = "Safe"
218 | safe2str Unsafe = "Unsafe"
219 | safe2str Helpless = "Helpless";
221 type subs = cterm' list; (*16.11.00 for FE-KE*)
222 fun subst2str' thy' (s:subst) =
225 (apsnd (Sign.string_of_term (sign_of (assoc_thy thy')))) o
226 (apfst (Sign.string_of_term (sign_of (assoc_thy thy'))))))) s;
228 type scrstate = (*state for script interpreter*)
229 env(*stack*) (*used to instantiate tac for checking assod
230 12.03.noticed: e_ not updated during execution ?!?*)
231 * loc_ (*location of tac in script*)
232 * term option(*argument of curried functions*)
233 * term (*value obtained by tac executed
234 updated also after a derivation by 'new_val'*)
235 * safe (*estimation of how result will be obtained*)
236 * bool; (*true = strongly .., false = weakly associated:
237 only used during ass_dn/up*)
238 val e_scrstate = ([],[],None,e_term,Sundef,false):scrstate;
241 (*21.8.02 ---> definitions.sml for datatype scr
242 type rrlsstate = (*state for reverse rewriting*)
243 (term * (*the current formula*)
244 rule list (*of reverse rewrite set (#1#)*)
245 list * (*may be serveral, eg. in norm_rational*)
246 (rule * (*Thm (+ Thm generated from Calc) resulting in ...*)
247 (term * (*... rewrite with ...*)
248 term list)) (*... assumptions*)
249 list); (*derivation from given term to normalform
250 in reverse order with sym_thm;
251 (#1#) could be extracted from here #1*) --------*)
253 datatype istate = (*interpreter state*)
254 Uistate (*undefined in modspec, in '_deriv'ation*)
255 | ScrState of scrstate (*for script interpreter*)
256 | RrlsState of rrlsstate; (*for reverse rewriting*)
257 type iist = istate option * istate option;
258 val e_istate = (ScrState ([],[],None,e_term,Sundef,false)):istate;
259 (*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*)
260 fun rta2str (r,(t,a)) = "\n("^(rule2str r)^",("^(term2str t)^", "^
262 fun istate2str Uistate = "Uistate"
263 | istate2str (ScrState (e,l,to,t,s,b):istate) =
264 "ScrState ("^ subst2str e ^",\n "^
265 loc_2str l ^", "^ termopt2str to ^",\n "^
266 term2str t ^", "^ safe2str s ^", "^ bool2str b ^")"
267 | istate2str (RrlsState (t,t1,rss,rtas)) =
268 "RrlsState ("^(term2str t)^", "^(term2str t1)^", "^
269 ((strs2str o (map (strs2str o (map rule2str)))) rss)^", "^
270 ((strs2str o (map rta2str)) rtas)^")";
271 fun istates2str (None, None) = "(#None, #None)"
272 | istates2str (None, Some ist) = "(#None,\n#Some "^istate2str ist^")"
273 | istates2str (Some ist, None) = "(#Some "^istate2str ist^",\n #None)"
274 | istates2str (Some i1, Some i2) = "(#Some "^istate2str i1^",\n #Some "^
277 fun new_val v (ScrState (env, loc_, topt, _, safe, bool)) =
278 (ScrState (env, loc_, topt, v, safe, bool))
279 | new_val _ _ = raise error "new_val: only for ScrState";
281 datatype con = land | lor;
284 fun subst2subs s = map (pair2str o
285 (apfst (Sign.string_of_term (sign_of thy))) o
286 (apsnd (Sign.string_of_term (sign_of thy)))) s;
287 fun subst2subs' s = map ((apfst (Sign.string_of_term (sign_of thy))) o
288 (apsnd (Sign.string_of_term (sign_of thy)))) s;
292 fun isapair2pair (Const ("Pair",_) $ a $ b) = (a,b);
293 fun subs2subst thy s = map (isapair2pair o term_of o the o (parse thy)) s;
294 (*> subs2subst thy ["(bdv,x)","(err,#0)"];
296 [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real")),
297 (Free ("err","RealDef.real"),Free ("#0","RealDef.real"))]
298 : (term * term) list*)
305 (*FE <-> KE: strings*)
307 Init_Proof of ((cterm' list) * spec)
308 (*Init_Proo_Hid of (dgmode * (cterm' list) * spec)
309 | Init_Proof 7.6.02java-sml*)
310 | Model_Problem of pblID
311 | Refine_Problem of pblID | Refine_Tacitly of pblID
312 (*| Match_Problem of pblID*)
313 | Add_Given of cterm' | Del_Given of cterm'
314 | Add_Find of cterm' | Del_Find of cterm'
315 | Add_Relation of cterm' | Del_Relation of cterm'
317 | Specify_Theory of domID | Specify_Problem of pblID
318 | Specify_Method of metID
319 | Apply_Method of metID | Check_Postcond of pblID
322 | Rewrite_Inst of ( subs * thm') | Rewrite of thm'
323 | Rewrite_Asm of thm'
324 | Rewrite_Set_Inst of ( subs * rls') | Rewrite_Set of rls'
325 | Detail_Set_Inst of ( subs * rls') | Detail_Set of rls'
326 | End_Detail (*end of script from next_tac,
327 in solve: switches back to parent script*)
328 | Derive of rls' (*an input formula using rls*)
329 | Calculate of string | End_Ruleset
330 (* plus | minus | times | cancel | pow | sqrt *)
331 | Substitute of subs | Apply_Assumption of cterm' list
333 | Take of cterm' | Take_Inst of cterm'
334 | Group of (con * int list )
335 (*| Subproblem_Full of (spec * (cterm' list)) *)
336 | Subproblem of (domID * pblID)
337 | CAScmd of cterm' (*6.6.02 URD: Function formula *)
340 | Split_And | Conclude_And
341 | Split_Or | Conclude_Or
342 | Begin_Trans | End_Trans
343 | Begin_Sequ | End_Sequ(* substitute root.env *)
344 | Split_Intersect | End_Intersect
345 | Check_elementwise of cterm' | Collect_Trues
348 | Empty_Tac (*TODO.11.6.03 ... of string: could carry msg of (Notappl msg)
350 | Tac of string(* eg.'repeat'*)
351 | User (*internal, for ets*) | End_Proof';(* inout*)
354 (* tac2str /--> library.sml: needed in dialog.sml for 'separable *)
355 fun tac2str (ma:tac) = case ma of
356 Init_Proof (ppc, spec) =>
357 "Init_Proof "^(pair2str (strs2str ppc, spec2str spec))
358 | Model_Problem pblID => "Model_Problem "^(strs2str pblID)
359 | Refine_Tacitly pblID => "Refine_Tacitly "^(strs2str pblID)
360 | Refine_Problem pblID => "Refine_Problem "^(strs2str pblID)
361 (*| Match_Problem pblID => "Match_Problem "^(strs2str pblID)*)
362 | Add_Given cterm' => "Add_Given "^cterm'
363 | Del_Given cterm' => "Del_Given "^cterm'
364 | Add_Find cterm' => "Add_Find "^cterm'
365 | Del_Find cterm' => "Del_Find "^cterm'
366 | Add_Relation cterm' => "Add_Relation "^cterm'
367 | Del_Relation cterm' => "Del_Relation "^cterm'
369 | Specify_Theory domID => "Specify_Theory "^(quote domID )
370 | Specify_Problem pblID => "Specify_Problem "^(strs2str pblID )
371 | Specify_Method metID => "Specify_Method "^(strs2str metID)
372 | Apply_Method metID => "Apply_Method "^(strs2str metID)
373 | Check_Postcond pblID => "Check_Postcond "^(strs2str pblID)
374 | Free_Solve => "Free_Solve"
376 | Rewrite_Inst (subs,thm')=>
377 "Rewrite_Inst "^(pair2str (subs2str subs, spair2str thm'))
378 | Rewrite thm' => "Rewrite "^(spair2str thm')
379 | Rewrite_Asm thm' => "Rewrite_Asm "^(spair2str thm')
380 | Rewrite_Set_Inst (subs, rls) =>
381 "Rewrite_Set_Inst "^(pair2str (subs2str subs, quote rls))
382 | Rewrite_Set rls => "Rewrite_Set "^(quote rls )
383 | Detail_Set rls => "Detail_Set "^(quote rls )
384 | Detail_Set_Inst (subs, rls) =>
385 "Detail_Set_Inst "^(pair2str (subs2str subs, quote rls))
386 | End_Detail => "End_Detail"
387 | Derive rls' => "Derive "^rls'
388 | Calculate op_ => "Calculate "^op_
389 | Substitute subs => "Substitute "^(subs2str subs)
390 | Apply_Assumption ct's => "Apply_Assumption "^(strs2str ct's)
392 | Take cterm' => "Take "^(quote cterm' )
393 | Take_Inst cterm' => "Take_Inst "^(quote cterm' )
394 | Group (con, ints) =>
395 "Group "^(pair2str (con2str con, ints2str ints))
396 | Subproblem (domID, pblID) =>
397 "Subproblem "^(pair2str (domID, strs2str pblID))
398 (*| Subproblem_Full (spec, cts') =>
399 "Subproblem_Full "^(pair2str (spec2str spec, strs2str cts'))*)
400 | End_Subproblem => "End_Subproblem"
401 | CAScmd cterm' => "CAScmd "^(quote cterm')
403 | Check_elementwise cterm'=> "Check_elementwise "^(quote cterm')
404 | Or_to_List => "Or_to_List "
405 | Collect_Trues => "Collect_Trues"
407 | Empty_Tac => "Empty_Tac"
408 | Tac string => "Tac "^string
410 | End_Proof' => "tac End_Proof'"
411 | _ => "tac2str not impl. for ?!";
413 fun is_rewset (Rewrite_Set_Inst _) = true
414 | is_rewset (Rewrite_Set _) = true
415 | is_rewset _ = false;
417 fun tac2IDstr (ma:tac) = case ma of
418 Model_Problem _ => "Model_Problem"
419 | Refine_Tacitly pblID => "Refine_Tacitly"
420 | Refine_Problem pblID => "Refine_Problem"
421 | Add_Given cterm' => "Add_Given"
422 | Del_Given cterm' => "Del_Given"
423 | Add_Find cterm' => "Add_Find"
424 | Del_Find cterm' => "Del_Find"
425 | Add_Relation cterm' => "Add_Relation"
426 | Del_Relation cterm' => "Del_Relation"
428 | Specify_Theory domID => "Specify_Theory"
429 | Specify_Problem pblID => "Specify_Problem"
430 | Specify_Method metID => "Specify_Method"
431 | Apply_Method metID => "Apply_Method"
432 | Check_Postcond pblID => "Check_Postcond"
433 | Free_Solve => "Free_Solve"
435 | Rewrite_Inst (subs,thm')=> "Rewrite_Inst"
436 | Rewrite thm' => "Rewrite"
437 | Rewrite_Asm thm' => "Rewrite_Asm"
438 | Rewrite_Set_Inst (subs, rls) => "Rewrite_Set_Inst"
439 | Rewrite_Set rls => "Rewrite_Set"
440 | Detail_Set rls => "Detail_Set"
441 | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst"
442 | Derive rls' => "Derive "
443 | Calculate op_ => "Calculate "
444 | Substitute subs => "Substitute"
445 | Apply_Assumption ct's => "Apply_Assumption"
447 | Take cterm' => "Take"
448 | Take_Inst cterm' => "Take_Inst"
449 | Group (con, ints) => "Group"
450 | Subproblem (domID, pblID) => "Subproblem"
451 | End_Subproblem => "End_Subproblem"
452 | CAScmd cterm' => "CAScmd"
454 | Check_elementwise cterm'=> "Check_elementwise"
455 | Or_to_List => "Or_to_List "
456 | Collect_Trues => "Collect_Trues"
458 | Empty_Tac => "Empty_Tac"
459 | Tac string => "Tac "
461 | End_Proof' => "End_Proof'"
462 | _ => "tac2str not impl. for ?!";
465 type fmz_ = cterm' list;
466 type fmz = fmz_ * spec;
467 val e_fmz = ([],e_spec);
469 (*tac_ is made from tac in applicable_in,
470 and carries all data necessary for generate;*)
473 Init_Proof' of ((cterm' list) * spec)
474 (* ori list !: code specify -> applicable*)
475 | Model_Problem' of pblID *
476 itm list (*the 'untouched' pbl*)
477 | Refine_Tacitly' of pblID * (*input*)
478 pblID * (*the refined from applicable_in*)
479 domID * (*from new pbt?! filled in specify*)
480 metID * (*from new pbt?! filled in specify*)
481 itm list (*drop ! 9.03: remains [] for
482 Model_Problem recognizing its activation*)
483 | Refine_Problem' of (pblID * (itm list * (bool * Term.term) list))
484 (*FIXME?040215 drop: done automatically in init_proof + Subproblem'*)
485 | Add_Given' of cterm' *
486 itm list (*updated with input in fun specify_additem*)
487 | Add_Find' of cterm' *
488 itm list (*updated with input in fun specify_additem*)
489 | Add_Relation' of cterm' *
490 itm list (*updated with input in fun specify_additem*)
491 | Del_Given' of cterm' | Del_Find' of cterm' | Del_Relation' of cterm'
492 (*4.00.: all.. term: in applicable_in ..? Syn ?only for FormFK?*)
494 | Specify_Theory' of domID
495 | Specify_Problem' of (pblID * (* *)
496 (bool * (* matches *)
497 (itm list * (* ppc *)
498 (bool * term) list))) (* preconditions *)
499 | Specify_Method' of metID *
500 ori list * (*repl. "#undef"*)
501 itm list (*... updated from pbl to met*)
502 | Apply_Method' of metID *
503 (term option) * (*init_form*)
507 (term * (*returnvalue of script in solve*)
508 cterm' list)(*collect by get_assumptions_ in applicable_in, except if
509 butlast tac is Check_elementwise: take only these asms*)
512 | Rewrite_Inst' of theory' * rew_ord' * rls
513 * bool * subst * thm' * term * (term * term list)
514 (*... form * (result* asumpts ), saves time*)
515 | Rewrite' of theory' * rew_ord' * rls * bool * thm' *
516 term * (term * term list)
517 | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm' *
518 term * (term * term list)
519 | Rewrite_Set_Inst' of theory' * bool * subst * rls *
520 term * (term * term list)
521 | Detail_Set_Inst' of theory' * bool * subst * rls *
522 term * (term * term list)
523 | Rewrite_Set' of theory' * bool * rls * term * (term * term list)
524 | Detail_Set' of theory' * bool * rls * term * (term * term list)
525 | End_Detail' of (term * (term list)) (*see End_Trans'*)
526 | End_Ruleset' of term
528 | Calculate' of theory' * string * term * (term * thm')
529 (*WN.29.4.03 asm?: * term list??*)
530 | Substitute' of subst * term (*10.8.00+..*)* term
531 | Apply_Assumption' of term list * term
533 | Take' of term | Take_Inst' of term
534 | Group' of (con * int list * term)
535 | Subproblem' of (spec *
536 (ori list) * (*filled in assod Subproblem'*)
537 term * (*-"-, headline of calc-head *)
539 term) (*Subproblem(dom,pbl)*)
541 | End_Subproblem' of term (*???*)
542 | Split_And' of term | Conclude_And' of term
543 | Split_Or' of term | Conclude_Or' of term
544 | Begin_Trans' of term | End_Trans' of (term * (term list))
545 | Begin_Sequ' | End_Sequ'(* substitute root.env*)
546 | Split_Intersect' of term | End_Intersect' of term
547 | Check_elementwise' of (*special case:*)
548 term * (*(1)the current formula: [x=1,x=...]*)
549 string * (*(2)the pred from Check_elementwise *)
550 (term * (*(3)composed from (1) and (2): {x. pred}*)
551 term list) (*20.5.03 assumptions*)
553 | Or_to_List' of term * term (* (a | b, [a,b]) *)
554 | Collect_Trues' of term
556 | Empty_Tac_ | Tac_ of (*for dummies*)
560 string (*result of Tac".."*)
561 | User' (*internal for ets*) | End_Proof'';(*End_Proof:inout*)
562 (*TODO?: done partially for tests*)
563 fun tac_2str ma = case ma of
564 Init_Proof' (ppc, spec) =>
565 "Init_Proof' "^(pair2str (strs2str ppc, spec2str spec))
566 | Model_Problem' (pblID,_) => "Model_Problem' "^(strs2str pblID )
567 | Refine_Tacitly'(p,prefin,domID,metID,itms)=>
569 ^(strs2str p)^", "^(strs2str prefin)^", "
570 ^domID^", "^(strs2str metID)^", pbl-itms)"
571 | Refine_Problem' ms => "Refine_Problem' ("^(*matchs2str ms*)"..."^")"
572 (*| Match_Problem' (pI, (ok, (itms, pre))) =>
573 "Match_Problem' "^(spair2str (strs2str pI,
574 spair2str (bool2str ok,
575 spair2str ("itms2str itms",
576 "items2str pre"))))*)
577 | Add_Given' cterm' => "Add_Given' "(*^cterm'*)
578 | Del_Given' cterm' => "Del_Given' "(*^cterm'*)
579 | Add_Find' cterm' => "Add_Find' "(*^cterm'*)
580 | Del_Find' cterm' => "Del_Find' "(*^cterm'*)
581 | Add_Relation' cterm' => "Add_Relation' "(*^cterm'*)
582 | Del_Relation' cterm' => "Del_Relation' "(*^cterm'*)
584 | Specify_Theory' domID => "Specify_Theory' "^(quote domID )
585 | Specify_Problem' (pI, (ok, (itms, pre))) =>
586 "Specify_Problem' "^(spair2str (strs2str pI,
587 spair2str (bool2str ok,
588 spair2str ("itms2str itms",
590 | Specify_Method' (pI,oris,itms) =>
591 "Specify_Method' ("^metID2str pI^", "^oris2str oris^", )"
593 | Apply_Method' (metID,_,_) => "Apply_Method' "^(strs2str metID)
594 | Check_Postcond' (pblID,(scval,asm)) =>
595 "Check_Postcond' "^(spair2str(strs2str pblID,
596 spair2str (term2str scval, strs2str asm)))
598 | Free_Solve' => "Free_Solve'"
600 | Rewrite_Inst' (*subs,thm'*) _ =>
601 "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
602 | Rewrite' thm' => "Rewrite' "(*^(spair2str thm')*)
603 | Rewrite_Asm' thm' => "Rewrite_Asm' "(*^(spair2str thm')*)
604 | Rewrite_Set_Inst' (*subs,thm'*) _ =>
605 "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
606 | Rewrite_Set'(thy',pasm,rls',f,(f',asm))
607 => "Rewrite_Set' ("^thy'^","^(bool2str pasm)^","^(id_rls rls')^","
608 ^(Sign.string_of_term (sign_of thy) f)^",("^(Sign.string_of_term (sign_of thy) f')
609 ^","^((strs2str o (map (Sign.string_of_term (sign_of thy)))) asm)^"))"
611 | End_Detail' _ => "End_Detail' xxx"
612 | Detail_Set' _ => "Detail_Set' xxx"
613 | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
615 | Derive' rls => "Derive' "^id_rls rls
616 | Calculate' _ => "Calculate' "
617 | Substitute' subs => "Substitute' "(*^(subs2str subs)*)
618 | Apply_Assumption' ct's => "Apply_Assumption' "(*^(strs2str ct's)*)
620 | Take' cterm' => "Take' "(*^(quote cterm' )*)
621 | Take_Inst' cterm' => "Take_Inst' "(*^(quote cterm' )*)
622 | Group' (con, ints, _) =>
623 "Group' "^(pair2str (con2str con, ints2str ints))
624 | Subproblem' (spec, oris, _,_,pbl_form) =>
625 "Subproblem' "(*^(pair2str (domID, strs2str ,...))*)
626 | End_Subproblem' _ => "End_Subproblem'"
627 | CAScmd' cterm' => "CAScmd' "(*^(quote cterm')*)
629 | Empty_Tac_ => "Empty_Tac_"
631 | Tac_ (_,form,id,result) => "Tac_ (thy,"^form^","^id^","^result^")"
632 | _ => "tac_2str not impl. for arg";
634 (*'executed tactics' (tac_s) with local environment etc.;
635 used for continuing eval script + for generate*)
637 (loc_ * (* of tactic in scr, tactic (weakly) associated with tac_*)
638 (tac_ * (* (for generate) *)
639 env * (* with 'tactic=result' as a rule, tactic ev. _not_ ready:
640 for handling 'parallel let'*)
641 env * (* with results of (ready) tacs *)
642 term * (* itr_arg of tactic, for upd. env at Repeat, Try*)
643 term * (* result value of the tac *)
649 fun ets2s (l,(m,eno,env,iar,res,s)) =
650 "\n("^(loc_2str l)^",("^(tac_2str m)^
651 ",\n ens= "^(subst2str eno)^
652 ",\n env= "^(subst2str env)^
653 ",\n iar= "^(Sign.string_of_term (sign_of thy) iar)^
654 ",\n res= "^(Sign.string_of_term (sign_of thy) res)^
655 ",\n "^(safe2str s)^"))";
656 fun ets2str (ets:ets) = (strs2str o (map ets2s)) ets;
659 type envp =(*9.5.03: unused, delete with field in ptree.PblObj FIXXXME*)
660 (int * term list) list * (*assoc-list: args of met*)
661 (int * rls) list * (*assoc-list: tacs already done ///15.9.00*)
662 (int * ets) list * (*assoc-list: tacs etc. already done*)
663 (string * pos) list; (*asms * from where*)
664 val empty_envp = ([],[],[],[]):envp;
667 PrfObj of {cell : cid, (* 4.00 superfluous: use cid in DG only!!*)
669 tac : tac, (* also in istate*)
670 loc : istate option * istate option, (*for form, result
671 13.8.02: (None,None) <==> e_istate ! see update_loc, get_loc*)
673 result: term * term list,
674 (*FIXX@ME result:term * term list
675 => applicable_in =..rewrite_set_
676 => rls = {erls: rls (NOT rls'),...}*)
677 ostate: ostate} (*Complete <=> result is OK*)
678 | PblObj of {cell : cid, (*unused*)
679 fmz : fmz, (*from init:FIXME never use this spec;-drop*)
680 origin: (ori list) * (*representation from fmz+pbt
681 for efficiently adding items in probl, meth*)
682 spec * (*updated by Refine_Tacitly*)
683 term, (*headline of calc-head*)
684 spec : spec, (*explicitly input*)
685 probl : itm list, (*itms explicitly input*)
686 meth : itm list, (*itms automatically added to copy of probl*)
687 env : istate option,(*for _sub_problem, if no init_form*)
688 loc : istate option * istate option, (*for pbl+met, result*)
690 result: term * term list,
691 ostate: ostate}; (*Complete <=> result is _proven_ OK*)
694 | Nd of ppobj * (ptree list);
695 val e_ptree = EmptyPtree;
697 fun rep_prfobj (PrfObj {cell,form,tac,loc,branch,result,ostate}) =
698 {cell=cell,form=form,tac=tac,loc=loc,branch=branch,result=result,ostate=ostate};
699 fun rep_pblobj (PblObj {cell,origin,fmz,spec,probl,meth,env,
700 loc,branch,result,ostate}) =
701 {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,
702 env=env,loc=loc,branch=branch,result=result,ostate=ostate};
703 fun is_prfobj (PrfObj _) = true
704 | is_prfobj _ =false;
705 (*val is_prfobj' = get_obj is_prfobj; *)
706 fun is_pblobj (PblObj _) = true
707 | is_pblobj _ = false;
708 (*val is_pblobj' = get_obj is_pblobj; 'Error: unbound constructor get_obj'*)
711 exception PTREE of string;
712 fun nth _ [] = raise PTREE "nth _ []"
714 | nth n (x::xs) = nth (n-1) xs;
715 (*> nth 2 [11,22,33]; -->> val it = 22 : int*)
717 fun lev_up ([]:pos) = raise PTREE "lev_up []"
718 | lev_up p = (drop_last p):pos;
719 fun lev_on ([]:pos) = raise PTREE "lev_on []"
721 let val len = length pos
722 in (drop_last pos) @ [(nth len pos)+1] end;
723 fun lev_onFrm ((p,_):pos') = (lev_on p,Frm):pos'
724 | lev_onFrm p = raise PTREE ("*** lev_onFrm: pos'="^(pos'2str p));
725 (*040216: for inform --> embed_deriv: remains on same level*)
726 fun lev_back (([],_):pos') = raise PTREE "lev_on_back: called by ([],_)"
728 if last_elem p <= 1 then (p, Frm):pos'
729 else ((drop_last p) @ [(nth (length p) p) - 1], Res);
730 (*.increase pos by n within a level.*)
731 fun pos_plus 0 pos = pos
732 | pos_plus n ((p,Frm):pos') = pos_plus (n-1) (p, Res)
733 | pos_plus n ((p, _):pos') = pos_plus (n-1) (lev_on p, Res);
737 fun lev_pred ([]:pos) = raise PTREE "lev_pred []"
738 | lev_pred (pos:pos) =
739 let val len = length pos
740 in ((drop_last pos) @ [(nth len pos)-1]):pos end;
742 val it = [1,2,2] : pos
744 val it = [0] : pos *)
746 fun lev_dn p = p @ [0];
747 (*> (lev_dn o lev_on) [1,2,3];
748 val it = [1,2,4,0] : pos *)
749 (*fun lev_dn' ((p,p_):pos') = (lev_dn p, Frm):pos'; WN.3.12.03: never used*)
750 fun lev_dnRes ((p,_):pos') = (lev_dn p, Res):pos';
753 fun lev_up_ ((p,Res):pos') = (lev_up p,Res):pos'
754 | lev_up_ p' = raise error ("lev_up_: called for "^(pos'2str p'));
755 fun lev_dn_ ((p,_):pos') = (lev_dn p,Res):pos'
756 fun ind ((p,_):pos') = length p; (*WN050108 deprecated in favour of lev_of*)
757 fun lev_of ((p,_):pos') = length p;
760 (** convert ptree to a string **)
762 (* convert a pos from list to string *)
763 fun pr_pos ps = (space_implode "." (map string_of_int ps))^". ";
764 (* show hd origin or form only *)
765 fun pr_short (p:pos) (PblObj {origin = (ori,_,_),...}) =
766 ((pr_pos p) ^ " ----- pblobj -----\n")
767 (* ((((Sign.string_of_term (sign_of thy)) o #4 o hd) ori)^" "^
768 (((Sign.string_of_term (sign_of thy)) o hd(*!?!*) o #5 o hd) ori))^
770 | pr_short p (PrfObj {form = form,...}) =
771 ((pr_pos p) ^ (term2str form) ^ "\n");
772 fun pr_cell (p:pos) (PblObj {cell = c, origin = (ori,_,_),...}) =
774 ((((Sign.string_of_term (sign_of thy)) o #4 o hd) ori)^" "^
775 (((Sign.string_of_term (sign_of thy)) o hd(*!?!*) o #5 o hd) ori))^
777 | pr_cell p (PrfObj {cell = c, form = form,...}) =
778 ((ints2str c) ^" "^ (term2str form) ^ "\n");
784 fun pr_pt pfn _ EmptyPtree = ""
785 | pr_pt pfn ps (Nd (b, [])) = pfn ps b
786 | pr_pt pfn ps (Nd (b, ts)) = (pfn ps b)^
787 (prts pfn (ps:pos) 1 ts)
788 and prts pfn ps p [] = ""
789 | prts pfn ps p (t::ts) = (pr_pt pfn (ps @ [p]) t)^
790 (prts pfn ps (p+1) ts)
791 in pr_pt f [] pt end;
793 > fun prfn ps b = (pr_pos ps)^" "^b(*TODO*)^"\n";
794 > val pt = ref EmptyPtree;
801 > writeln (pr_ptree prfn (!pt));
805 (** access the branches of ptree **)
807 fun ins_nth 1 e l = e::l
808 | ins_nth n e [] = raise PTREE "ins_nth n e []"
809 | ins_nth n e (l::ls) = l::(ins_nth (n-1) e ls);
810 fun repl [] _ _ = raise PTREE "repl [] _ _"
811 | repl (l::ls) 1 e = e::ls
812 | repl (l::ls) n e = l::(repl ls (n-1) e);
813 fun repl_app ls n e =
814 let val lim = 1 + length ls
815 in if n > lim then raise PTREE "repl_app: n > lim"
816 else if n = lim then ls @ [e]
817 else repl ls n e end;
819 > repl [1,2,3] 2 22222;
820 val it = [1,22222,3] : int list
821 > repl_app [1,2,3,4] 5 5555;
822 val it = [1,2,3,4,5555] : int list
823 > repl_app [1,2,3] 2 22222;
824 val it = [1,22222,3] : int list
825 > repl_app [1] 2 22222 ;
826 val it = [1,22222] : int list
830 (*.get from obj at pos by f : ppobj -> 'a.*)
831 fun get_obj f EmptyPtree _ = raise PTREE "get_obj f EmptyPtree"
832 | get_obj f (Nd (b, _)) [] = f b
833 | get_obj f (Nd (b, bs)) (p::ps) =
834 (* val (f, Nd (b, bs), (p::ps)) = (I, pt, p);
836 let val _ = (nth p bs) handle _ => raise PTREE ("get_obj: pos = "^
837 (ints2str' (p::ps))^" does not exist");
838 in (get_obj f (nth p bs) (ps:pos))
839 (*before WN050419: 'wrong type..' raised also if pos doesn't exist*)
840 handle _ => raise PTREE (*"get_obj: at pos = "^
841 (ints2str' (p::ps))^" wrong type of ppobj"*)
843 (ints2str' (p::ps))^" does not exist")
845 fun get_nd EmptyPtree _ = raise PTREE "get_nd EmptyPtree"
847 | get_nd (Nd (_,nds)) (pos as p::(ps:pos)) = (get_nd (nth p nds) ps)
848 handle _ => raise PTREE ("get_nd: not existent pos = "^(ints2str' pos));
851 (* for use by get_obj *)
852 fun g_cell (PblObj {cell = c,...}) = c
853 | g_cell (PrfObj {cell = c,...}) = c;
854 fun g_form (PrfObj {form = f,...}) = f
855 | g_form (PblObj {origin=(_,_,f),...}) = f;
856 (* | g_form _ = raise PTREE "g_form not for PblObj";*)
857 fun g_origin (PblObj {origin = ori,...}) = ori
858 | g_origin _ = raise PTREE "g_origin not for PrfObj";
859 fun g_fmz (PblObj {fmz = f,...}) = f
860 | g_fmz _ = raise PTREE "g_fmz not for PrfObj";
861 fun g_spec (PblObj {spec = s,...}) = s
862 | g_spec _ = raise PTREE "g_spec not for PrfObj";
863 fun g_pbl (PblObj {probl = p,...}) = p
864 | g_pbl _ = raise PTREE "g_pbl not for PrfObj";
865 fun g_met (PblObj {meth = p,...}) = p
866 | g_met _ = raise PTREE "g_met not for PrfObj";
867 fun g_domID (PblObj {spec = (d,_,_),...}) = d
868 | g_domID _ = raise PTREE "g_metID not for PrfObj";
869 fun g_metID (PblObj {spec = (_,_,m),...}) = m
870 | g_metID _ = raise PTREE "g_metID not for PrfObj";
871 fun g_env (PblObj {env,...}) = env
872 | g_env _ = raise PTREE "g_env not for PrfObj";
873 fun g_loc (PblObj {loc = l,...}) = l
874 | g_loc (PrfObj {loc = l,...}) = l;
875 fun g_branch (PblObj {branch = b,...}) = b
876 | g_branch (PrfObj {branch = b,...}) = b;
877 fun g_tac (PblObj {spec = (d,p,m),...}) = Apply_Method m
878 | g_tac (PrfObj {tac = m,...}) = m;
879 fun g_result (PblObj {result = r,...}) = r
880 | g_result (PrfObj {result = r,...}) = r;
881 fun g_ostate (PblObj {ostate = r,...}) = r
882 | g_ostate (PrfObj {ostate = r,...}) = r;
883 fun g_ostate' (Nd (PblObj {ostate = r,...}, _)) = r
884 | g_ostate' (Nd (PrfObj {ostate = r,...}, _)) = r;
886 fun gpt_cell (Nd (PblObj {cell = c,...},_)) = c
887 | gpt_cell (Nd (PrfObj {cell = c,...},_)) = c;
889 (*in CalcTree/Subproblem an 'just_created_' model is created;
890 this is filled to 'untouched' by Model/Refine_Problem*)
891 fun just_created_ (PblObj {meth, probl, spec, ...}) =
892 null meth andalso null probl andalso spec = e_spec;
893 val e_origin = ([],e_spec,e_term): (ori list) * spec * term;
895 fun just_created (pt,(p,_):pos') =
896 let val ppobj = get_obj I pt p
897 in is_pblobj ppobj andalso just_created_ ppobj end;
899 fun existpt pos pt = can (get_obj I pt) pos;
900 fun existpt' ((p,p_):pos') pt =
901 if can (get_obj I pt) p
903 Res => get_obj g_ostate pt p = Complete
907 fun fst_onlev (([], Frm):pos') = true
908 | fst_onlev (([], Pbl):pos') = true
909 | fst_onlev (([], Met):pos') = true
910 | fst_onlev (pos, Frm) = last_elem pos = 1
911 | fst_onlev _ = false;
912 fun last_onlev pt pos = not (existpt (lev_on pos) pt);
915 (*.find the position of the next parent which is a PblObj in ptree.*)
916 fun par_pblobj pt ([]:pos) = ([]:pos)
918 let fun par pt [] = []
919 | par pt p = if is_pblobj (get_obj I pt p) then p
920 else par pt (lev_up p)
921 in par pt (lev_up p) end;
922 (* lev_up for hard_gen operating with pos = [...,0] *)
924 (*.find the position and the children of the next parent which is a PblObj.*)
925 fun par_children (Nd (PblObj _, children)) ([]:pos) = (children, []:pos)
926 | par_children (pt as Nd (PblObj _, children)) p =
927 let fun par [] = (children, [])
928 | par p = let val Nd (obj, children) = get_nd pt p
929 in if is_pblobj obj then (children, p) else par (lev_up p)
931 in par (lev_up p) end;
933 (*.get the children of a node in ptree.*)
934 fun children (Nd (PblObj _, cn)) = cn
935 | children (Nd (PrfObj _, cn)) = cn;
938 (*.find the next parent, which is either a PblObj (return true)
939 or a PrfObj with tac = Detail_Set (return false).*)
940 (*FIXME.3.4.03:re-organize par_pbl_det after rls' --> rls*)
941 fun par_pbl_det pt ([]:pos) = (true, []:pos, Erls)
943 let fun par pt [] = (true, [], Erls)
944 | par pt p = if is_pblobj (get_obj I pt p) then (true, p, Erls)
945 else case get_obj g_tac pt p of
946 (*Detail_Set rls' => (false, p, assoc_rls rls')
947 (*^^^--- before 040206 after ---vvv*)
948 |*)Rewrite_Set rls' => (false, p, assoc_rls rls')
949 | Rewrite_Set_Inst (_, rls') =>
950 (false, p, assoc_rls rls')
951 | _ => par pt (lev_up p)
952 in par pt (lev_up p) end;
957 (*.get from the whole ptree by f : ppobj -> 'a.*)
958 fun get_all f EmptyPtree = []
959 | get_all f (Nd (b, [])) = [f b]
960 | get_all f (Nd (b, bs)) = [f b] @ (get_alls f bs)
961 and get_alls f [] = []
962 | get_alls f pts = flat (map (get_all f) pts);
965 (*.insert obj b into ptree at pos, ev.overwriting this pos.*)
966 fun insert b EmptyPtree ([]:pos) = Nd (b, [])
967 | insert b EmptyPtree _ = raise PTREE "insert b Empty _"
968 | insert b (Nd ( _, _)) [] = raise PTREE "insert b _ []"
969 | insert b (Nd (b', bs)) (p::[]) =
970 Nd (b', repl_app bs p (Nd (b,[])))
971 | insert b (Nd (b', bs)) (p::ps) =
972 Nd (b', repl_app bs p (insert b (nth p bs) ps));
974 > type ppobj = string;
975 > writeln (pr_ptree prfn (!pt));
977 pt:= insert ("root":ppobj) EmptyPtree [];
978 pt:= insert ("xx1":ppobj) (!pt) [1];
979 pt:= insert ("xx2":ppobj) (!pt) [2];
980 pt:= insert ("xx3":ppobj) (!pt) [3];
981 pt:= insert ("xx2.1":ppobj) (!pt) [2,1];
982 pt:= insert ("xx2.2":ppobj) (!pt) [2,2];
983 pt:= insert ("xx2.1.1":ppobj) (!pt) [2,1,1];
984 pt:= insert ("xx2.1.2":ppobj) (!pt) [2,1,2];
985 pt:= insert ("xx2.1.3":ppobj) (!pt) [2,1,3];
988 (*.insert children to a node without children.*)
989 (*compare: fun insert*)
990 fun ins_chn _ EmptyPtree (_:pos) = raise PTREE "ins_chn: EmptyPtree"
991 | ins_chn ns (Nd _) [] = raise PTREE "ins_chn: pos = []"
992 | ins_chn ns (Nd (b, bs)) (p::[]) =
993 if p > length bs then raise PTREE "ins_chn: pos not existent"
994 else let val Nd (b', bs') = nth p bs
995 in if null bs' then Nd (b, repl_app bs p (Nd (b', ns)))
996 else raise PTREE "ins_chn: pos mustNOT be overwritten" end
997 | ins_chn ns (Nd (b, bs)) (p::ps) =
998 Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps));
1000 print_depth 11;ins_chn;print_depth 3 (*###insert#########################*);
1003 (** apply f to obj at pos, f: ppobj -> ppobj **)
1005 fun appl_to_node f (Nd (b,bs)) = Nd (f b, bs);
1006 fun appl_obj f EmptyPtree [] = EmptyPtree
1007 | appl_obj f EmptyPtree _ = raise PTREE "appl_obj f Empty _"
1008 | appl_obj f (Nd (b, bs)) [] = Nd (f b, bs)
1009 | appl_obj f (Nd (b, bs)) (p::[]) =
1010 Nd (b, repl_app bs p (((appl_to_node f) o (nth p)) bs))
1011 | appl_obj f (Nd (b, bs)) (p::ps) =
1012 Nd (b, repl_app bs p (appl_obj f (nth p bs) (ps:pos)));
1014 (* for use by appl_obj *)
1015 fun repl_form f (PrfObj {cell=c,form= _,tac=tac,loc=loc,
1016 branch=branch,result=result,ostate=ostate}) =
1017 PrfObj {cell=c,form= f,tac=tac,loc=loc,
1018 branch=branch,result=result,ostate=ostate}
1019 | repl_form _ _ = raise PTREE "repl_form takes no PblObj";
1020 fun repl_pbl x (PblObj {cell=cell,origin=origin,fmz=fmz,
1021 spec=spec,probl=_,meth=meth,env=env,loc=loc,
1022 branch=branch,result=result,ostate=ostate}) =
1023 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl= x,
1024 meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1025 | repl_pbl _ _ = raise PTREE "repl_pbl takes no PrfObj";
1026 fun repl_met x (PblObj {cell=cell,origin=origin,fmz=fmz,
1027 spec=spec,probl=probl,meth=_,env=env,loc=loc,
1028 branch=branch,result=result,ostate=ostate}) =
1029 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
1030 meth= x,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1031 | repl_met _ _ = raise PTREE "repl_pbl takes no PrfObj";
1033 fun repl_spec x (PblObj {cell=cell,origin=origin,fmz=fmz,
1034 spec= _,probl=probl,meth=meth,env=env,loc=loc,
1035 branch=branch,result=result,ostate=ostate}) =
1036 PblObj {cell=cell,origin=origin,fmz=fmz,spec= x,probl=probl,
1037 meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1038 | repl_spec _ _ = raise PTREE "repl_domID takes no PrfObj";
1039 fun repl_domID x (PblObj {cell=cell,origin=origin,fmz=fmz,
1040 spec=(_,p,m),probl=probl,meth=meth,env=env,loc=loc,
1041 branch=branch,result=result,ostate=ostate}) =
1042 PblObj {cell=cell,origin=origin,fmz=fmz,spec=(x,p,m),probl=probl,
1043 meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1044 | repl_domID _ _ = raise PTREE "repl_domID takes no PrfObj";
1045 fun repl_pblID x (PblObj {cell=cell,origin=origin,fmz=fmz,
1046 spec=(d,_,m),probl=probl,meth=meth,env=env,loc=loc,
1047 branch=branch,result=result,ostate=ostate}) =
1048 PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,x,m),probl=probl,
1049 meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1050 | repl_pblID _ _ = raise PTREE "repl_pblID takes no PrfObj";
1051 fun repl_metID x (PblObj {cell=cell,origin=origin,fmz=fmz,
1052 spec=(d,p,_),probl=probl,meth=meth,env=env,loc=loc,
1053 branch=branch,result=result,ostate=ostate}) =
1054 PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,p,x),probl=probl,
1055 meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1056 | repl_metID _ _ = raise PTREE "repl_metID takes no PrfObj";
1058 fun repl_result l f' s (PrfObj {cell=cell,form=form,tac=tac,loc=_,
1059 branch=branch,result = _ ,ostate = _}) =
1060 PrfObj {cell=cell,form=form,tac=tac,loc= l,
1061 branch=branch,result = f',ostate = s}
1062 | repl_result l f' s (PblObj {cell=cell,origin=origin,fmz=fmz,
1063 spec=spec,probl=probl,meth=meth,env=env,loc=_,
1064 branch=branch,result= _ ,ostate= _}) =
1065 PblObj {cell=cell,origin=origin,fmz=fmz,
1066 spec=spec,probl=probl,meth=meth,env=env,loc= l,
1067 branch=branch,result= f',ostate= s};
1069 fun repl_tac x (PrfObj {cell=cell,form=form,tac= _,loc=loc,
1070 branch=branch,result=result,ostate=ostate}) =
1071 PrfObj {cell=cell,form=form,tac= x,loc=loc,
1072 branch=branch,result=result,ostate=ostate}
1073 | repl_tac _ _ = raise PTREE "repl_tac takes no PblObj";
1075 fun repl_branch b (PblObj {cell=cell,origin=origin,fmz=fmz,
1076 spec=spec,probl=probl,meth=meth,env=env,loc=loc,
1077 branch= _,result=result,ostate=ostate}) =
1078 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
1079 meth=meth,env=env,loc=loc,branch= b,result=result,ostate=ostate}
1080 | repl_branch b (PrfObj {cell=cell,form=form,tac=tac,loc=loc,
1081 branch= _,result=result,ostate=ostate}) =
1082 PrfObj {cell=cell,form=form,tac=tac,loc=loc,
1083 branch= b,result=result,ostate=ostate};
1086 (PblObj {cell=cell,origin=origin,fmz=fmz,
1087 spec=spec,probl=probl,meth=meth,env=_,loc=loc,
1088 branch=branch,result=result,ostate=ostate}) =
1089 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
1090 meth=meth,env=e,loc=loc,branch=branch,
1091 result=result,ostate=ostate}
1092 | repl_env _ _ = raise PTREE "repl_ets takes no PrfObj";
1095 (PblObj {cell=cell,origin=(_,spe,hdf),fmz=fmz,
1096 spec=spec,probl=probl,meth=meth,env=env,loc=loc,
1097 branch=branch,result=result,ostate=ostate}) =
1098 PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,
1099 meth=meth,env=env,loc=loc,branch=branch,
1100 result=result,ostate=ostate}
1101 | repl_oris _ _ = raise PTREE "repl_oris takes no PrfObj";
1102 fun repl_orispec spe
1103 (PblObj {cell=cell,origin=(oris,_,hdf),fmz=fmz,
1104 spec=spec,probl=probl,meth=meth,env=env,loc=loc,
1105 branch=branch,result=result,ostate=ostate}) =
1106 PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,
1107 meth=meth,env=env,loc=loc,branch=branch,
1108 result=result,ostate=ostate}
1109 | repl_orispec _ _ = raise PTREE "repl_orispec takes no PrfObj";
1111 fun repl_loc l (PblObj {cell=cell,origin=origin,fmz=fmz,
1112 spec=spec,probl=probl,meth=meth,env=env,loc=_,
1113 branch=branch,result=result,ostate=ostate}) =
1114 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
1115 meth=meth,env=env,loc=l,branch=branch,result=result,ostate=ostate}
1116 | repl_loc l (PrfObj {cell=cell,form=form,tac=tac,loc=_,
1117 branch=branch,result=result,ostate=ostate}) =
1118 PrfObj {cell=cell,form=form,tac=tac,loc= l,
1119 branch=branch,result=result,ostate=ostate};
1122 (PblObj {cell=cell,origin=origin,fmz=fmz,
1123 spec=spec,probl=probl,meth=meth,env=env,loc=loc,
1124 branch=branch,result=result,ostate=ostate}) =
1125 PblObj {cell=cell union cell',origin=origin,fmz=fmz,spec=spec,probl=probl,
1126 meth=meth,env=env,loc=loc,branch=branch,
1127 result=result,ostate=ostate}
1129 (PrfObj {cell=cell,form=form,tac=tac,loc=loc,
1130 branch=branch,result=result,ostate=ostate}) =
1131 PrfObj {cell=cell union cell',form=form,tac=tac,loc=loc,
1132 branch=branch,result=result,ostate=ostate};
1134 (*WN050219 put here for interpreting code for cut_tree below...*)
1136 bool * (*ALL itms+preconds true*)
1137 pos_ * (*model belongs to Problem | Method*)
1138 term * (*header: Problem... or Cas
1139 FIXXXME.12.03: item! for marking syntaxerrors*)
1140 itm list * (*model: given, find, relate*)
1141 ((bool * term) list) *(*model: preconds*)
1142 spec; (*specification*)
1143 val e_ocalhd = (false, Und, e_term, [e_itm], [(false, e_term)], e_spec);
1147 | ModSpec of ocalhd;
1148 val e_ptform = Form e_term;
1149 val e_ptform' = ModSpec e_ocalhd;
1153 (*.applies (snd f) to the branches at a pos if ((fst f) b),
1154 f : (ppobj -> bool) * (int -> ptree list -> ptree list).*)
1156 fun appl_branch f EmptyPtree [] = (EmptyPtree, false)
1157 | appl_branch f EmptyPtree _ = raise PTREE "appl_branch f Empty _"
1158 | appl_branch f (Nd ( _, _)) [] = raise PTREE "appl_branch f _ []"
1159 | appl_branch f (Nd (b, bs)) (p::[]) =
1160 if (fst f) b then (Nd (b, (snd f) (p:posel) bs), true)
1161 else (Nd (b, bs), false)
1162 | appl_branch f (Nd (b, bs)) (p::ps) =
1163 let val (b',bool) = appl_branch f (nth p bs) ps
1164 in (Nd (b, repl_app bs p b'), bool) end;
1166 (* for cut_level; appl_branch(deprecated) *)
1167 fun test_trans (PrfObj{branch = Transitive,...}) = true
1168 | test_trans (PblObj{branch = Transitive,...}) = true
1169 | test_trans _ = false;
1171 fun is_pblobj' pt (p:pos) =
1172 let val ppobj = get_obj I pt p
1173 in is_pblobj ppobj end;
1176 fun delete_result pt (p:pos) =
1177 (appl_obj (repl_result (fst (get_obj g_loc pt p), None)
1178 (e_term,[]) Incomplete) pt p);
1180 fun del_res (PblObj {cell, fmz, origin, spec, probl, meth,
1181 env, loc=(l1,_), branch, result, ostate}) =
1182 PblObj {cell=cell,fmz=fmz,origin=origin,spec=spec,probl=probl,meth=meth,
1183 env=env, loc=(l1,None), branch=branch, result=(e_term,[]),
1186 | del_res (PrfObj {cell, form, tac, loc=(l1,_), branch, result, ostate}) =
1187 PrfObj {cell=cell,form=form,tac=tac, loc=(l1,None), branch=branch,
1188 result=(e_term,[]), ostate=Incomplete};
1192 fun update_fmz pt pos x = appl_obj (repl_fmz x) pt pos;
1193 1.00 not used anymore*)
1195 (*FIXME.WN.12.03: update_X X pos pt -> pt could be chained by o (efficiency?)*)
1196 fun update_env pt pos x = appl_obj (repl_env x) pt pos;
1197 fun update_domID pt pos x = appl_obj (repl_domID x) pt pos;
1198 fun update_pblID pt pos x = appl_obj (repl_pblID x) pt pos;
1199 fun update_metID pt pos x = appl_obj (repl_metID x) pt pos;
1200 fun update_spec pt pos x = appl_obj (repl_spec x) pt pos;
1202 fun update_pbl pt pos x = appl_obj (repl_pbl x) pt pos;
1203 fun update_pblppc pt pos x = appl_obj (repl_pbl x) pt pos;
1205 fun update_met pt pos x = appl_obj (repl_met x) pt pos;
1207 fun update_metppc pt pos x =
1208 let val {rew_ord'=od,rls'=rs,asm_thm=at,asm_rls=ar,...} =
1209 get_obj g_met pt pos
1210 in appl_obj (repl_met
1211 {rew_ord'=od,rls'=rs,asm_thm=at,asm_rls=ar,ppc=x})
1213 fun update_metppc pt pos x = appl_obj (repl_met x) pt pos;
1215 fun union_cid pt pos x = appl_obj (uni__cid x) pt pos;
1217 fun update_branch pt pos x = appl_obj (repl_branch x) pt pos;
1218 fun update_tac pt pos x = appl_obj (repl_tac x) pt pos;
1220 fun update_oris pt pos x = appl_obj (repl_oris x) pt pos;
1221 fun update_orispec pt pos x = appl_obj (repl_orispec x) pt pos;
1223 (*done by append_* !! 3.5.02*)
1224 fun update_loc pt (p,_) (ScrState ([],[],None,
1225 Const ("empty",_),Sundef,false)) =
1226 appl_obj (repl_loc (None,None)) pt p
1227 | update_loc pt (p,Res) x =
1228 let val (lform,_) = get_obj g_loc pt p
1229 in appl_obj (repl_loc (lform,Some x)) pt p end
1231 | update_loc pt (p,_) x =
1232 let val (_,lres) = get_obj g_loc pt p
1233 in appl_obj (repl_loc (Some x,lres)) pt p end;
1234 (*WN050305 for handling cut_tree in cappend_atomic -- TODO redesign !*)
1235 fun update_loc' pt p iss = appl_obj (repl_loc iss) pt p;
1237 (*13.8.02---------------------------
1238 fun get_loc EmptyPtree _ = None
1239 | get_loc pt (p,Res) =
1240 let val (lfrm,lres) = get_obj g_loc pt p
1241 in if lres = e_istate then lfrm else lres end
1242 | get_loc pt (p,_) =
1243 let val (lfrm,lres) = get_obj g_loc pt p
1244 in if lfrm = e_istate then lres else lfrm end; 5.10.00: too liberal ?*)
1245 (*13.8.02: options, because istate is no equalitype any more*)
1246 fun get_loc EmptyPtree _ = e_istate
1247 | get_loc pt (p,Res) =
1248 (case get_obj g_loc pt p of
1250 | (None , None) => e_istate
1251 | (_ , Some i) => i)
1252 | get_loc pt (p,_) =
1253 (case get_obj g_loc pt p of
1254 (None , Some i) => i (*13.8.02 just copied from ^^^: too liberal ?*)
1255 | (None , None) => e_istate
1256 | (Some i, _) => i);
1257 val get_istate = get_loc; (*3.5.02*)
1259 (*.collect the assumptions within a problem up to a certain position.*)
1260 type asms = (term * pos) list;(*WN0502 should be (pos' * term) list
1261 ...........===^===*)
1263 fun get_asm (b:pos, p:pos) (Nd (PblObj {result=(_,asm),...},_)) =
1264 ((*writeln ("### get_asm PblObj:(b,p)= "^
1265 (pair2str(ints2str b, ints2str p)));*)
1266 (map (rpair b) asm):asms)
1267 | get_asm (b, p) (Nd (PrfObj {result=(_,asm),...}, [])) =
1268 ((*writeln ("### get_asm PrfObj []:(b,p)= "^
1269 (pair2str(ints2str b, ints2str p)));*)
1270 (map (rpair b) asm))
1271 | get_asm (b, p:pos) (Nd (PrfObj _, nds)) =
1272 let (*val _= writeln ("### get_asm PrfObj nds:(b,p)= "^
1273 (pair2str(ints2str b, ints2str p)));*)
1275 if p <> [] then (b @ [hd p]:pos, tl p:pos)
1276 else (b @ [1], [99999]) (*_deeper_ nesting is always _before_ p*)
1277 in gets_asm levdn 1 nds end
1278 and gets_asm _ _ [] = []
1279 | gets_asm (b, p' as p::ps) i (nd::nds) =
1281 else ((*writeln ("### gets_asm: (b,p')= "^(pair2str(ints2str b,
1283 (get_asm (b @ [i], ps) nd) @ (gets_asm (b, p') (i + 1) nds));
1285 fun get_assumptions_ (Nd (PblObj {result=(r,asm),...}, cn)) (([], _):pos') =
1286 if r = e_term then gets_asm ([], [99999]) 1 cn
1287 else map (rpair []) asm
1288 | get_assumptions_ pt (p,p_) =
1289 let val (cn, base) = par_children pt p
1290 val offset = drop (length base, p)
1291 val base' = replicate (length base) 1
1292 val offset' = case p_ of
1293 Frm => let val (qs,q) = split_last offset
1296 (*val _= writeln ("... get_assumptions: (b,o)= "^
1297 (pair2str(ints2str base',ints2str offset)))*)
1298 in gets_asm (base', offset) 1 cn end;
1307 (*pos of the formula on FE relative to the current pos,
1308 which is the next writepos*)
1309 fun pre_pos ([]:pos) = []:pos
1311 let val (ps,p) = split_last pp
1312 in case p of 1 => ps | n => ps @ [n-1] end;
1314 (*WN.20.5.03 ... but not used*)
1315 fun posless [] (_::_) = true
1316 | posless (_::_) [] = false
1317 | posless (p::ps) (q::qs) = if p = q then posless ps qs else p < q;
1318 (* posless [2,3,4] [3,4,5];
1320 > posless [2,3,4] [1,2,3];
1322 > posless [2,3] [2,3,4];
1324 > posless [2,3,4] [2,3];
1326 > posless [6] [6,5,2];
1328 +++ see Isabelle/../library.ML*)
1331 (**.development for extracting an 'interval' from ptree.**)
1333 (*version 1 stopped 8.03 in favour of get_interval with !!!move_dn
1334 actually used (inefficient) version with move_dn: see modspec.sml*)
1337 fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*)
1338 fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)
1339 fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x;
1340 fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
1342 fun getnd i (b,p) q (Nd (po, nds)) =
1343 (if i <= 0 then [[b]] else []) @
1344 (getnds (i-1) true (b@[hdp p], tlp p) (tlq q)
1345 (take_fromto (hdp p) (hdq q) nds))
1347 and getnds _ _ _ _ [] = [] (*no children*)
1348 | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)
1350 | getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*)
1351 (getnd i ( b, p ) [99999] n1) @
1352 (getnd ~99999 (lev_on b,[0]) q n2)
1354 | getnds i _ (b,p) q [n1, n2] = (*intern, r-margin*)
1355 (getnd i ( b,[0]) [99999] n1) @
1356 (getnd ~99999 (lev_on b,[0]) q n2)
1358 | getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*)
1359 (getnd i ( b, p ) [99999] nd) @
1360 (getnds ~99999 false (lev_on b,[0]) q nds)
1362 | getnds i _ (b,p) q (nd::(nds as _::_)) = (*intern, ...*)
1363 (getnd i ( b,[0]) [99999] nd) @
1364 (getnds ~99999 false (lev_on b,[0]) q nds);
1366 (*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes
1367 where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
1368 (1) the 'f' are given
1369 (1a) by 'from' if 'f' = the respective element of 'from' (left margin)
1370 (1b) -inifinity, if 'f' > the respective element of 'from' (internal node)
1371 (2) the 't' ar given
1372 (2a) by 'to' if 't' = the respective element of 'to' (right margin)
1373 (2b) inifinity, if 't' < the respective element of 'to (internal node)'
1374 the 'f' and 't' are set by hdp,... *)
1375 fun get_trace pt p q =
1376 (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q)))
1377 (take_fromto (hdp p) (hdq q) (children pt));
1379 (*WN0510 stoppde this development;
1380 actually used (inefficient) version with move_dn: getElementsFromTo*)
1385 fun get_somespec ((dI,pI,mI):spec) ((dI',pI',mI'):spec) =
1386 let val domID = if dI = e_domID
1387 then if dI' = e_domID
1388 then raise error"pt_extract: no domID in probl,origin"
1391 val pblID = if pI = e_pblID
1392 then if pI' = e_pblID
1393 then raise error"pt_extract: no pblID in probl,origin"
1396 val metID = if mI = e_metID
1397 then if pI' = e_metID
1398 then raise error"pt_extract: no metID in probl,origin"
1401 in (domID, pblID, metID):spec end;
1402 fun get_somespec' ((dI,pI,mI):spec) ((dI',pI',mI'):spec) =
1403 let val domID = if dI = e_domID then dI' else dI
1404 val pblID = if pI = e_pblID then pI' else pI
1405 val metID = if mI = e_metID then mI' else mI
1406 in (domID, pblID, metID):spec end;
1408 (*extract a formula or model from ptree for itms2itemppc or model2xml*)
1409 fun preconds2str bts =
1410 (strs2str o (map (linefeed o pair2str o
1412 (apfst bool2str)))) bts;
1413 fun ocalhd2str ((b, p, hdf, itms, prec, spec):ocalhd) =
1414 "("^bool2str b^", "^pos_2str p^", "^term2str hdf^
1415 ", "^itms2str (assoc_thy "Isac.thy") itms^
1416 ", "^preconds2str prec^", \n"^spec2str spec^" )";
1420 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj;
1423 (**.functions for the 'ptree iterator' as seen from the FE-Kernel interface.**)
1425 (*.move one step down into existing nodes of ptree; regard TransitiveB.*)
1426 fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*)
1427 (* val (Nd (c, ns), ([],p_)) = (pt, get_pos cI uI);
1430 then case p_ of (*Frm => ([], Pbl) 1.12.03
1431 |*) Res => raise PTREE "move_dn: end of calculation"
1432 | _ => if null ns (*go down from Pbl + Met*)
1433 then raise PTREE "move_dn: solve problem not started"
1435 else (case p_ of Res => raise PTREE "move_dn: end of (sub-)tree"
1437 then raise PTREE "move_dn: pos not existent 1"
1440 (*iterate towards end of pos*)
1441 (* val (P,(Nd (_, ns)),(p::(ps as (_::_)),p_)) = ([]:pos, pt, get_pos cI uI);
1442 val (P,(Nd (_, ns)),(p::(ps as (_::_)),p_)) = ((P@[p]),(nth p ns),(ps, p_));
1444 | move_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
1445 if p > length ns then raise PTREE "move_dn: pos not existent 2"
1446 else move_dn ((P@[p]): pos) (nth p ns) (ps, p_)
1447 (* val (P, (Nd (c, ns)), ([p], p_)) = ((P@[p]), (nth p ns), (ps, p_));
1448 val (P, (Nd (c, ns)), ([p], p_)) = ([],pt,get_pos cI uI);
1450 | move_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1451 if p > length ns then raise PTREE "move_dn: pos not existent 3"
1452 else if is_pblnd (nth p ns) then
1453 ((*writeln("### move_dn: is_pblnd (nth p ns), P= "^ints2str' P^", \n"^
1454 "length ns= "^((string_of_int o length) ns)^
1455 ", p= "^string_of_int p^", p_= "^pos_2str p_);*)
1456 case p_ of Res => if p = length ns
1457 then if g_ostate c = Complete then (P, Res)
1458 else raise PTREE (ints2str' P^" not complete")
1459 (*FIXME here handle not-sequent-branches*)
1460 else if g_branch c = TransitiveB
1461 andalso (not o is_pblnd o (nth (p+1))) ns
1463 else (P@[p+1], if is_pblnd (nth (p+1) ns)
1465 | _ => if (null o children o (nth p)) ns (*go down from Pbl*)
1466 then raise PTREE "move_dn: solve subproblem not started"
1468 if (is_pblnd o hd o children o (nth p)) ns
1471 (* val (P, Nd (c, ns), ([p], p_)) = ([], pt, ([1], Frm));
1473 else case p_ of Frm => if (null o children o (nth p)) ns
1474 (*then if g_ostate c = Complete then (P@[p],Res)*)
1475 then if g_ostate' (nth p ns) = Complete
1477 else raise PTREE "move_dn: pos not existent 4"
1478 else (P @ [p, 1], (*go down*)
1479 if (is_pblnd o hd o children o (nth p)) ns
1481 | Res => if p = length ns
1483 if g_ostate c = Complete then (P, Res)
1484 else raise PTREE (ints2str' P^" not complete")
1486 if g_branch c = TransitiveB
1487 andalso (not o is_pblnd o (nth (p+1))) ns
1488 then if (null o children o (nth (p+1))) ns
1490 else (P@[p+1,1], Frm)(*040221*)
1491 else (P@[p+1], if is_pblnd (nth (p+1) ns)
1496 (*.go one level down into ptree.*)
1497 fun movelevel_dn [] (Nd (c, ns)) ([],p_) = (*root problem*)
1500 then raise PTREE "solve problem not started"
1501 else ([1], if (is_pblnd o hd) ns then Pbl else Frm)
1502 else raise PTREE "pos not existent 1"
1504 (*iterate towards end of pos*)
1505 | movelevel_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
1506 if p > length ns then raise PTREE "pos not existent 2"
1507 else movelevel_dn (P@[p]) (nth p ns) (ps, p_)
1509 | movelevel_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1510 if p > length ns then raise PTREE "pos not existent 3" else
1513 then raise PTREE "no children"
1515 if g_branch c = TransitiveB
1516 then if (null o children o (nth (p+1))) ns
1517 then raise PTREE "no children"
1519 if (is_pblnd o hd o children o (nth (p+1))) ns
1521 else if (null o children o (nth p)) ns
1522 then raise PTREE "no children"
1523 else (P @ [p, 1], if (is_pblnd o hd o children o (nth p)) ns
1525 | _ => if (null o children o (nth p)) ns
1526 then raise PTREE "no children"
1527 else (P @ [p, 1], (*go down*)
1528 if (is_pblnd o hd o children o (nth p)) ns
1533 (*.go to the previous position in ptree; regard TransitiveB.*)
1534 fun move_up _ (Nd (c, ns)) (([],p_):pos') = (*root problem*)
1536 then case p_ of Res => if null ns then ([], Pbl) (*Res -> Pbl (not Met)!*)
1537 else ([length ns], Res)
1538 | _ => raise PTREE "begin of calculation"
1539 else raise PTREE "pos not existent"
1541 | move_up P (Nd (_, ns)) (p::(ps as (_::_)),p_) = (*iterate to end of pos*)
1542 if p > length ns then raise PTREE "pos not existent"
1543 else move_up (P@[p]) (nth p ns) (ps,p_)
1545 | move_up P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1546 if p > length ns then raise PTREE "pos not existent"
1547 else if is_pblnd (nth p ns) then
1549 let val nc = (length o children o (nth p)) ns
1550 in if nc = 0 then (P@[p], Pbl) (*Res -> Pbl (not Met)!*)
1551 else (P @ [p, nc], Res) end (*go down*)
1552 | _ => if p = 1 then (P, Pbl) else (P@[p-1], Res)
1553 else case p_ of Frm => if p <> 1 then (P, Frm)
1554 else if is_pblobj c then (P, Pbl) else (P, Frm)
1556 let val nc = (length o children o (nth p)) ns
1557 in if nc = 0 (*cannot go down*)
1558 then if g_branch c = TransitiveB andalso p <> 1
1559 then (P@[p-1], Res) else (P@[p], Frm)
1560 else (P @ [p, nc], Res) end; (*go down*)
1564 (*.go one level up in ptree; sets the position on Frm.*)
1565 fun movelevel_up _ (Nd (c, ns)) (([],p_):pos') = (*root problem*)
1566 raise PTREE "pos not existent"
1568 (*iterate towards end of pos*)
1569 | movelevel_up P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
1570 if p > length ns then raise PTREE "pos not existent"
1571 else movelevel_up (P@[p]) (nth p ns) (ps,p_)
1573 | movelevel_up P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1574 if p > length ns then raise PTREE "pos not existent"
1575 else if is_pblobj c then (P, Pbl) else (P, Frm);
1578 (*.go to the next calc-head up in the calc-tree.*)
1579 fun movecalchd_up pt ((p, Res):pos') =
1580 (par_pblobj pt p, Pbl):pos'
1581 | movecalchd_up pt (p, _) =
1582 if is_pblobj (get_obj I pt p)
1583 then (p, Pbl) else (par_pblobj pt p, Pbl);
1585 (*WN0502 made for interSteps; _only_ works for branch TransitiveB*)
1586 fun lev_pred' pt (pos:pos' as (p,Res)) =
1587 if (is_pblobj o (get_obj I pt)) p then (p,Pbl):pos' else move_up [] pt pos
1588 | lev_pred' pt p = move_up [] pt p;
1591 (**.insert into ctree and cut branches accordingly.**)
1593 (*.get all positions of certain intervals on the ctree.*)
1594 (*OLD VERSION without move_dn; kept for occasional redesign
1595 get all pos's to be cut in a ptree
1596 below a pos or from a ptree list after i-th element (NO level_up).*)
1597 fun get_allpos' (_:pos, _:posel) EmptyPtree = ([]:pos' list)
1598 | get_allpos' (p, 1) (Nd (b, bs)) = (*p is pos of Nd*)
1599 if g_ostate b = Incomplete
1600 then (writeln("get_allpos' (p, 1) Incomplete: p="^ints2str' p);
1601 [(p,Frm)] @ (get_allpos's (p, 1) bs)
1603 else (writeln("get_allpos' (p, 1) else: p="^ints2str' p);
1604 [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)]
1606 (*WN041020 here we assume what is presented on the worksheet ?!*)
1607 | get_allpos' (p, i) (Nd (b, bs)) = (*p is pos of Nd*)
1608 if length bs > 0 orelse is_pblobj b
1609 then if g_ostate b = Incomplete
1610 then [(p,Frm)] @ (get_allpos's (p, 1) bs)
1611 else [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)]
1613 if g_ostate b = Incomplete
1616 (*WN041020 here we assume what is presented on the worksheet ?!*)
1617 and get_allpos's _ [] = []
1618 | get_allpos's (p, i) (pt::pts) = (*p is pos of parent-Nd*)
1619 (get_allpos' (p@[i], i) pt) @ (get_allpos's (p, i+1) pts);
1621 (*.get all positions of certain intervals on the ctree.*)
1622 (*NEW version WN050225*)
1626 (*before WN041019......
1627 val cut_branch = (test_trans, curry take):
1628 (ppobj -> bool) * (int -> ptree list -> ptree list);
1629 .. formlery used for ...
1630 fun cut_tree''' _ [] = EmptyPtree
1631 | cut_tree''' pt pos =
1632 let val (pt',cut) = appl_branch cut_branch pt pos
1633 in if cut andalso length pos > 1 then cut_tree''' pt' (lev_up pos)
1636 (*OLD version before WN050225*)
1637 (*WN050106 like cut_level, but deletes exactly 1 node --- for tests ONLY*)
1638 fun cut_level_'_ (_:pos' list) (_:pos) EmptyPtree (_:pos') =
1639 raise PTREE "cut_level_'_ Empty _"
1640 | cut_level_'_ _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level_'_ _ []"
1641 | cut_level_'_ cuts P (Nd (b, bs)) (p::[],p_) =
1643 then (Nd (b, drop_nth [] (p:posel, bs)),
1646 (if p_ = Frm then [(P@[p],Res)] else ([]:pos' list)) @
1647 (*WN041020 here we assume what is presented on the worksheet ?!*)
1648 (get_allpos's (P, p+1) (drop_nth [] (p, bs))))
1650 else (Nd (b, bs), cuts)
1651 | cut_level_'_ cuts P (Nd (b, bs)) ((p::ps),p_) =
1652 let val (bs',cuts') = cut_level_'_ cuts P (nth p bs) (ps, p_)
1653 in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
1656 fun cut_level (_:pos' list) (_:pos) EmptyPtree (_:pos') =
1657 raise PTREE "cut_level EmptyPtree _"
1658 | cut_level _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level _ []"
1660 | cut_level cuts P (Nd (b, bs)) (p::[],p_) =
1662 then (Nd (b, take (p:posel, bs)),
1664 (if p_ = Frm andalso (*#*) g_ostate b = Complete
1665 then [(P@[p],Res)] else ([]:pos' list)) @
1666 (*WN041020 here we assume what is presented on the worksheet ?!*)
1667 (get_allpos's (P, p+1) (takerest (p, bs))))
1668 else (Nd (b, bs), cuts)
1670 | cut_level cuts P (Nd (b, bs)) ((p::ps),p_) =
1671 let val (bs',cuts') = cut_level cuts P (nth p bs) (ps, p_)
1672 in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
1674 (*OLD version before WN050219, overwritten below*)
1675 fun cut_tree _ (([],_):pos') = raise PTREE "cut_tree _ ([],_)"
1676 | cut_tree pt (pos as ([p],_)) =
1677 let val (pt', cuts) = cut_level ([]:pos' list) [] pt pos
1678 in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
1679 then [] else [([],Res)])) end
1680 | cut_tree pt (p,p_) =
1682 fun cutfn pt cuts (p,p_) =
1683 let val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_)
1684 val cuts'' = if get_obj g_ostate pt (lev_up p) = Incomplete
1685 then [] else [(lev_up p, Res)]
1686 in if length cuts' > 0 andalso length p > 1
1687 then cutfn pt' (cuts @ cuts') (lev_up p, Frm(*-->(p,Res)*))
1688 else (pt',cuts @ cuts') end
1689 val (pt', cuts) = cutfn pt [] (p,p_)
1690 in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
1691 then [] else [([], Res)])) end;
1694 (*########/ inserted from ctreeNEW.sml \#################################(**)
1696 (*.get all positions in a ptree until ([],Res) or ostate=Incomplete
1698 pos' list -> : accumulated, start with []
1699 pos -> : the offset for subtrees wrt the root
1700 ptree -> : (sub)tree
1701 pos' : initialization (the last pos' before ...)
1702 -> pos' list : of positions in this (sub) tree (relative to the root)
1704 (* val (cuts, P, pt, pos) = ([], [3], get_nd pt [3], ([], Frm):pos');
1705 val (cuts, P, pt, pos) = ([], [2], get_nd pt [2], ([], Frm):pos');
1706 length (children pt);
1708 fun get_allp (cuts:pos' list) (P:pos, pos:pos') pt =
1709 (let val nxt = move_dn [] pt pos (*exn if Incomplete reached*)
1710 in if nxt <> ([],Res)
1711 then get_allp (cuts @ [nxt]) (P, nxt) pt
1712 else (map (apfst (curry op@ P)) (cuts @ [nxt])): pos' list
1713 end) handle PTREE _ => (map (apfst (curry op@ P)) cuts);
1716 (*the pts are assumed to be on the same level*)
1717 fun get_allps (cuts: pos' list) (P:pos) [] = cuts
1718 | get_allps cuts P (pt::pts) =
1719 let val below = get_allp [] (P, ([], Frm)) pt
1722 then (P, Pbl)::below
1723 else if last_elem P = 1
1724 then (P, Frm)::below
1725 else (*Trans*) below
1726 val levres = levfrm @ (if null below then [(P, Res)] else [])
1727 in get_allps (cuts @ levres) (lev_on P) pts end;
1730 (**.these 2 funs decide on how far cut_tree goes.**)
1731 (*.shall the nodes _after_ the pos to be inserted at be deleted?.*)
1732 fun test_trans (PrfObj{branch = Transitive,...}) = true
1733 | test_trans (PrfObj{branch = NoBranch,...}) = true
1734 | test_trans (PblObj{branch = Transitive,...}) = true
1735 | test_trans (PblObj{branch = NoBranch,...}) = true
1736 | test_trans _ = false;
1737 (*.shall cutting be continued on the higher level(s)?
1738 the Nd regarded will NOT be changed.*)
1739 fun cutlevup (PblObj _) = false (*for tests of LK0502*)
1740 | cutlevup _ = true;
1742 (*cut_bottom new S(603)..(608)
1743 cut the level at the bottom of the pos (used by cappend_...)
1744 and handle the parent in order to avoid extra case for root
1745 fn: ptree -> : the _whole_ ptree for cut_levup
1746 pos * posel -> : the pos after split_last
1747 ptree -> : the parent of the Nd to be cut
1749 (ptree * : the updated ptree
1750 pos' list) * : the pos's cut
1751 bool : cutting shall be continued on the higher level(s)
1753 fun cut_bottom _ (pt' as Nd (b, [])) = ((pt', []), cutlevup b)
1754 | cut_bottom (P:pos, p:posel) (Nd (b, bs)) =
1755 let (*divide level into 3 parts...*)
1756 val keep = take (p - 1, bs)
1757 val pt' as Nd (_,bs') = nth p bs
1758 (*^^^^^_here_ will be 'insert'ed by 'append_..'*)
1759 val (tail, tp) = (takerest (p, bs),
1760 if null (takerest (p, bs)) then 0 else p + 1)
1761 val (children, cuts) =
1764 (if is_pblnd pt' then [(P @ [p], Pbl)] else [])
1765 @ (get_allp [] (P @ [p], (P, Frm)) pt')
1766 @ (get_allps [] (P @ [p+1]) tail))
1767 else (keep @ [(*'insert'ed by 'append_..'*)] @ tail,
1768 get_allp [] (P @ [p], (P, Frm)) pt')
1771 then (Nd (del_res b, children),
1772 cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
1773 else (Nd (b, children), cuts)
1774 (*val _= writeln("####cut_bottom (P, p)="^pos2str (P @ [p])^
1775 ", Nd=.............................................")
1777 val _= writeln("####cut_bottom form='"^
1778 term2str (get_obj g_form pt'' []))
1779 val _= writeln("####cut_bottom cuts#="^string_of_int (length cuts)^
1780 ", cuts="^pos's2str cuts)*)
1781 in ((pt'', cuts:pos' list), cutlevup b) end;
1785 (*.go all levels from the bottom of 'pos' up to the root,
1786 on each level compose the children of a node and accumulate the cut Nds
1788 pos' list -> : for accumulation
1789 bool -> : cutting shall be continued on the higher level(s)
1790 ptree -> : the whole ptree for 'get_nd pt P' on each level
1791 ptree -> : the Nd from the lower level for insertion at path
1792 pos * posel -> : pos=path split for convenience
1793 ptree -> : Nd the children of are under consideration on this call
1795 ptree * pos' list : the updated parent-Nd and the pos's of the Nds cut
1798 fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) =
1799 let (*divide level into 3 parts...*)
1800 val keep = take (p - 1, bs)
1801 (*val pt' comes as argument from below*)
1802 val (tail, tp) = (takerest (p, bs),
1803 if null (takerest (p, bs)) then 0 else p + 1)
1804 val (children, cuts') =
1806 then (keep @ [pt'], get_allps [] (P @ [p+1]) tail)
1807 else (keep @ [pt'] @ tail, [])
1808 val clevup' = if clevup then cutlevup b else false
1809 (*the first Nd with false stops cutting on all levels above*)
1812 then (Nd (del_res b, children),
1813 cuts' @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
1814 else (Nd (b, children), cuts')
1815 (*val _= writeln("#####cut_levup clevup= "^bool2str clevup)
1816 val _= writeln("#####cut_levup cutlevup b= "^bool2str (cutlevup b))
1817 val _= writeln("#####cut_levup (P, p)="^pos2str (P @ [p])^
1818 ", Nd=.............................................")
1820 val _= writeln("#####cut_levup form='"^
1821 term2str (get_obj g_form pt'' []))
1822 val _= writeln("#####cut_levup cuts#="^string_of_int (length cuts)^
1823 ", cuts="^pos's2str cuts)*)
1824 in if null P then (pt'', (cuts @ cuts'):pos' list)
1825 else let val (P, p) = split_last P
1826 in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P)
1831 fun cut_tree pt (pos,_) =
1832 if not (existpt pos pt)
1833 then (pt,[]) (*appending a formula never cuts anything*)
1834 else let val (P, p) = split_last pos
1835 val ((pt', cuts), clevup) = cut_bottom (P, p) (get_nd pt P)
1836 (* pt' is the updated parent of the Nd to cappend_..*)
1837 in if null P then (pt', cuts)
1838 else let val (P, p) = split_last P
1839 in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P)
1843 (**)########\ inserted from ctreeNEW.sml /#################################**)
1845 fun append_atomic p l f r f' s pt =
1846 let (**)val _= writeln("#@append_atomic: pos ="^pos2str p)(**)
1847 val (iss, f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
1849 ((fst (get_obj g_loc pt p), Some l),
1850 get_obj g_form pt p)
1851 (*040223 else ((Some l, None), f)*)
1852 else ((None, Some l), f)
1853 in insert (PrfObj {cell = [(*3.00. unused*)],
1859 ostate= s}) pt p end;
1861 (*20.8.02: cappend_* FIXXXXME cut branches below cannot be decided here:
1862 detail - generate - cappend: inserted, not appended !!!
1864 cut decided in applicable_in !?!
1866 fun cappend_atomic pt p loc f r f' s =
1867 (* val (pt, p, loc, f, r, f', s) =
1868 (pt,p,l,f,Rewrite_Set_Inst (subst2subs subs',id_rls rls'),
1871 (writeln("##@cappend_atomic: pos ="^pos2str p);
1872 apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm))
1874 fun cappend_atomic pt p loc f r f' s =
1875 let val _= writeln("##@cappend_atomic: pos ="^pos2str p);
1876 val _= writeln("##@cappend_atomic arg loc ="^istate2str loc);
1877 val _= if existpt p pt
1878 then writeln("##@cappend_atomic before cut_ loc ="^
1879 istates2str (get_obj g_loc pt p))
1880 else writeln("##@cappend_atomic pos not existent before cut_");
1881 val (pt', cs) = cut_tree pt (p,Frm);
1882 val _= if existpt p pt'
1883 then writeln("##@cappend_atomic after cut_ loc ="^
1884 istates2str (get_obj g_loc pt' p))
1885 else writeln("##@cappend_atomic pos not existent after cut_");
1886 val pt'' = append_atomic p loc f r f' s pt';
1887 val _= writeln("##@cappend_atomic after append: loc ="^
1888 istates2str (get_obj g_loc pt'' p));
1891 fun cappend_atomic pt p loc f r f' s =
1892 let val (pt', cs) = cut_tree pt (p,Frm)
1893 val pt'' = append_atomic p loc f r f' s pt'
1896 fun cappend_atomic pt p ist_res f r f' s =
1897 if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
1898 then (*after Take: transfer Frm and respective istate*)
1899 let val (ist_form, f) = (get_loc pt (p,Frm),
1900 get_obj g_form pt p)
1901 val (pt, cs) = cut_tree pt (p,Frm)
1902 val pt = append_atomic p e_istate f r f' s pt
1903 val pt = update_loc' pt p (Some ist_form, Some ist_res)
1905 else apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
1908 (* called by Take *)
1909 fun append_form p l f pt =
1910 (writeln("##@append_form: pos ="^pos2str p);
1911 insert (PrfObj {cell = [(*3.00. unused*)],
1912 form = (*if existpt p pt
1913 andalso get_obj g_tac pt p = Empty_Tac
1914 (*distinction from 'old' (+complete!) pobjs*)
1915 then get_obj g_form pt p else*) f,
1917 loc = (Some l, None),
1919 result= (e_term,[]),
1920 ostate= Incomplete}) pt p
1922 (* val (p,loc,f) = ([1], e_istate, str2term "x + 1 = 2");
1923 val (p,loc,f) = (fst p, e_istate, str2term "-1 + x = 0");
1925 fun cappend_form pt p loc f =
1926 (writeln("##@cappend_form: pos ="^pos2str p);
1927 apfst (append_form p loc f) (cut_tree pt (p,Frm))
1929 fun cappend_form pt p loc f =
1930 let val _= writeln("##@cappend_form: pos ="^pos2str p)
1931 val _= writeln("##@cappend_form before cut_tree: loc ="^istate2str loc)
1932 val (pt', cs) = cut_tree pt (p,Frm)
1933 val pt'' = append_form p loc f pt'
1934 val _= writeln("##@cappend_form after append: loc ="^
1935 istates2str (get_obj g_loc pt'' p))
1940 fun append_result pt p l f s =
1941 (writeln("##@append_result: pos ="^pos2str p);
1942 (appl_obj (repl_result (fst (get_obj g_loc pt p),
1943 Some l) f s) pt p, [])
1947 (*WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml*)
1948 fun append_parent p l f r b pt =
1949 let val _= writeln("###append_parent: pos ="^pos2str p);
1950 val (ll,f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
1951 then ((fst (get_obj g_loc pt p), Some l),
1952 get_obj g_form pt p)
1953 else ((Some l, None), f)
1955 {cell = [(*unused*)],
1960 result= (e_term,[]),
1961 ostate= Incomplete}) pt p end;
1962 fun cappend_parent pt p loc f r b =
1963 (writeln("###cappend_parent: pos ="^pos2str p);
1964 apfst (append_parent p loc f r b) (cut_tree pt (p,Und))
1968 fun append_problem [] l fmz (strs,spec,hdf) _ =
1969 (writeln("###append_problem: pos = []");
1971 {cell = [(*3.00. unused*)],
1972 origin= (strs,spec,hdf),
1975 probl = []:itm list,
1978 loc = (Some l, None),
1979 branch= TransitiveB,(*FIXXXXXME.27.8.03: for equations only*)
1980 result= (e_term,[]),
1981 ostate= Incomplete},[]))
1983 | append_problem p l fmz (strs,spec,hdf) pt =
1984 (writeln("###append_problem: pos ="^pos2str p);
1986 {cell = [(*3.00. unused*)],
1987 origin= (strs,spec,hdf),
1990 probl = []:itm list,
1993 loc = (Some l, None),
1994 branch= TransitiveB,
1995 result= (e_term,[]),
1996 ostate= Incomplete}) pt p
1998 fun cappend_problem _ [] loc fmz ori =
1999 (writeln("###cappend_problem: pos = []");
2000 (append_problem [] loc fmz ori EmptyPtree,[])
2002 | cappend_problem pt p loc fmz ori =
2003 (writeln("###cappend_problem: pos ="^pos2str p);
2004 apfst (append_problem p (loc:istate) fmz ori) (cut_tree pt (p,Frm))