1 (* Title: the calctree, which holds a calculation
2 Author: Walther Neuper 1999
3 (c) due to copyright terms
7 sig (* vvv--- *.sml require these typs incrementally, with these exception -----------------vvv *)
9 type fmz_ = cterm' list
10 type fmz = fmz_ * spec;
11 val e_fmz : fmz_ * spec (* for datatypes.sml *)
14 datatype istate = RrlsState of rrlsstate | ScrState of scrstate | Uistate
15 val istate2str : istate -> string
19 val sube2str : cterm' list -> string
21 val sube2subst : theory -> cterm' list -> (term * term) list
22 val sube2subte : cterm' list -> term list
23 val subs2subst : theory -> cterm' list -> (term * term) list
24 val subst2sube : (term * term) list -> cterm' list (* for datatypes.sml *)
25 val subst2subs : (term * term) list -> cterm' list
26 val subst2subs' : (term * term) list -> (string * string) list
27 val subte2sube : term list -> cterm' list
30 datatype tac_ = (* TODO.WN161219: replace *every* cterm' by term *)
31 Add_Find' of cterm' * itm list | Add_Given' of cterm' * itm list | Add_Relation' of cterm' * itm list
32 | Apply_Assumption' of term list * term
33 | Apply_Method' of metID * term option * istate * Proof.context
34 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
35 | Begin_Sequ' | Begin_Trans' of term
36 | Split_And' of term | Split_Or' of term | Split_Intersect' of term
37 | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
38 | End_Sequ' | End_Trans' of result
39 | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''
40 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
42 | Calculate' of theory' * string * term * (term * thm')
43 | Check_Postcond' of pblID * result
44 | Check_elementwise' of term * cterm' * result
45 | Del_Find' of cterm' | Del_Given' of cterm' | Del_Relation' of cterm'
48 | Detail_Set' of theory' * bool * rls * term * result
49 | Detail_Set_Inst' of theory' * bool * subst * rls * term * result
50 | End_Detail' of result
55 | Init_Proof' of cterm' list * spec
56 | Model_Problem' of pblID * itm list * itm list
57 | Or_to_List' of term * term
58 | Refine_Problem' of pblID * (itm list * (bool * term) list)
59 | Refine_Tacitly' of pblID * pblID * domID * metID * itm list
61 | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * result
62 | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * result
63 | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * result
64 | Rewrite_Set' of theory' * bool * rls * term * result
65 | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * result
67 | Specify_Method' of metID * ori list * itm list
68 | Specify_Problem' of pblID * (bool * (itm list * (bool * term) list))
69 | Specify_Theory' of domID
70 | Subproblem' of spec * ori list * term * fmz_ * Proof.context * term
71 | Substitute' of rew_ord_ * rls * subte * term * term
72 | Tac_ of theory * string * string * string
73 | Take' of term | Take_Inst' of term
75 Add_Find of cterm' | Add_Given of cterm' | Add_Relation of cterm'
76 | Apply_Assumption of cterm' list
77 | Apply_Method of metID
79 | Begin_Sequ | Begin_Trans
80 | Split_And | Split_Or | Split_Intersect
81 | Conclude_And | Conclude_Or | Collect_Trues
82 | End_Sequ | End_Trans
83 | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
87 | Check_Postcond of pblID
88 | Check_elementwise of cterm'
89 | Del_Find of cterm' | Del_Given of cterm' | Del_Relation of cterm'
93 | Detail_Set_Inst of subs * rls'
98 | Group of con * int list
100 | Init_Proof of cterm' list * spec
103 | Refine_Problem of pblID
104 | Refine_Tacitly of pblID
107 | Rewrite_Asm of thm''
108 | Rewrite_Inst of subs * thm''
109 | Rewrite_Set of rls'
110 | Rewrite_Set_Inst of subs * rls'
112 | Specify_Method of metID
113 | Specify_Problem of pblID
114 | Specify_Theory of domID
115 | Subproblem of domID * pblID
119 | Take of cterm' | Take_Inst of cterm'
120 val tac2str : tac -> string
121 val rls_of : tac -> rls' (* for solve.sml *)
122 val tac2IDstr : tac -> string
123 val is_rewset : tac -> bool (* for mathengine.sml *)
124 val is_rewtac : tac -> bool (* for interface.sml *)
127 type pos = posel list
128 val pos2str : int list -> string (* for datatypes.sml *)
129 datatype pos_ = Frm | Met | Pbl | Res | Und
130 val pos_2str : pos_ -> string
132 val pos'2str : pos' -> string
133 val str2pos_ : string -> pos_ (* for datatypes.sml *)
136 (* for generate.sml ?!? ca.*)
137 datatype safe = Helpless | Safe | Sundef | Unsafe
138 val tac_2str : tac_ -> string
141 datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB
142 datatype ostate = Complete | Incomplete | Inconsistent
147 loc: (istate * Proof.context) option * (istate * Proof.context) option,
152 origin: ori list * spec * term,
157 env: (istate * Proof.context) option}
161 loc: (istate * Proof.context) option * (istate * Proof.context) option,
167 val lev_on : pos -> pos
168 val lev_dn : pos -> pos
169 val lev_dn_ : pos' -> pos'
170 val lev_up : pos -> pos
171 val lev_of : pos' -> int
172 val pos_plus : int -> pos' -> pos'
173 val lev_back' : pos' -> pos' (* for inform.sml *)
175 datatype ctree = EmptyPtree | Nd of ppobj * ctree list
176 val e_ctree : ctree (* TODO: replace by EmptyPtree*)
177 val existpt' : pos' -> ctree -> bool (* for interface.sml *)
178 val exist_lev_on' : ctree -> pos' -> bool (* for interface.sml *)
179 val is_interpos : pos' -> bool (* for interface.sml *)
180 val lev_on' : ctree -> pos' -> pos' (* for interface.sml *)
181 val lev_pred' : ctree -> pos' -> pos' (* for interface.sml *)
182 val move_up : pos -> ctree -> pos' -> pos' (* for interface.sml *)
183 val movelevel_dn : pos -> ctree -> pos' -> pos' (* for interface.sml *)
184 val movelevel_up : pos -> ctree -> pos' -> pos' (* for interface.sml *)
185 val movecalchd_up : ctree -> pos' -> pos' (* for interface.sml *)
186 val par_pblobj : ctree -> pos -> pos
187 val ins_chn : ctree list -> ctree -> pos -> ctree (* for solve.sml *)
188 val children : ctree -> ctree list (* for solve.sml *)
189 val get_nd : ctree -> pos -> ctree (* for solve.sml *)
190 val just_created_ : ppobj -> bool (* for mathengine.sml *)
191 val just_created : ctree * pos' -> bool (* for mathengine.sml *)
192 val is_curr_endof_calc : ctree -> pos' -> bool (* for interface.sml *)
193 val e_origin : ori list * spec * term (* for mathengine.sml *)
195 val move_dn : pos -> ctree -> pos' -> pos'
196 val is_pblobj : ppobj -> bool
197 val is_pblobj' : ctree -> pos -> bool
198 val is_pblnd : ctree -> bool
199 val last_onlev : ctree -> pos -> bool
201 val g_spec : ppobj -> spec
202 val g_loc : ppobj -> (istate * Proof.context) option * (istate * Proof.context) option
203 val g_form : ppobj -> term
204 val g_pbl : ppobj -> itm list
205 val g_met : ppobj -> itm list
206 val g_metID : ppobj -> metID
207 val g_result : ppobj -> result
208 val g_tac : ppobj -> tac
209 val g_domID : ppobj -> domID (* for appl.sml TODO: replace by thyID *)
210 val g_env : ppobj -> (istate * Proof.context) option (* for appl.sml *)
212 val g_origin : ppobj -> ori list * spec * term (* for script.sml *)
213 val get_loc : ctree -> pos' -> istate * Proof.context (* for script.sml *)
214 val get_istate : ctree -> pos' -> istate (* for script.sml *)
215 val get_ctxt : ctree -> pos' -> Proof.context
216 val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a
217 val get_curr_formula : ctree * pos' -> term
218 val get_assumptions_ : ctree -> pos' -> term list (* for appl.sml *)
220 val append_result : ctree -> pos -> istate * Proof.context -> result ->
221 ostate -> ctree * 'a list
222 val append_atomic : (* for solve.sml *)
223 pos -> istate * Proof.context -> term -> tac -> result -> ostate -> ctree -> ctree
224 val cappend_atomic : ctree -> pos -> istate * Proof.context -> term -> tac -> result ->
225 ostate -> ctree * pos' list
226 val cappend_form : ctree -> pos -> istate * Proof.context -> term -> ctree * pos' list
227 val cappend_problem : ctree -> pos -> istate * Proof.context -> fmz ->
228 ori list * spec * term -> ctree * pos' list
230 val update_branch : ctree -> pos -> branch -> ctree
231 val update_ctxt : ctree -> pos -> Proof.context -> ctree
232 val update_env : ctree -> pos -> (istate * Proof.context) option -> ctree
233 val update_oris : ctree -> pos -> ori list -> ctree
234 val update_orispec : ctree -> pos -> spec -> ctree
235 val update_pbl : ctree -> pos -> itm list -> ctree
236 val update_pblppc : ctree -> pos -> itm list -> ctree (* =vvv= ? *)
237 val update_pblID : ctree -> pos -> pblID -> ctree (* =^^^= ? *)
238 val update_met : ctree -> pos -> itm list -> ctree (* =vvv= ? *)
239 val update_metppc : ctree -> pos -> itm list -> ctree (* =^^^= ? *)
240 val update_metID : ctree -> pos -> metID -> ctree
241 val update_domID : ctree -> pos -> domID -> ctree
242 val update_spec : ctree -> pos -> spec -> ctree
243 val update_tac : ctree -> pos -> tac -> ctree
245 val e_ctxt : Proof.context
246 val is_e_ctxt : Proof.context -> bool (* for appl.sml *)
247 val new_val : term -> istate -> istate
248 (* for calchead.sml *)
249 type cid = cellID list
250 type ocalhd = bool * pos_ * term * itm list * (bool * term) list * spec
251 datatype ptform = Form of term | ModSpec of ocalhd
252 val get_somespec' : spec -> spec -> spec
253 exception PTREE of string;
255 val par_pbl_det : ctree -> pos -> bool * pos * rls
256 (* for rewtools.sml *)
257 val rule2tac : theory -> (term * term) list -> rule -> tac
258 val eq_tac : tac * tac -> bool
260 val rootthy : ctree -> theory
261 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
262 val update_loc' : ctree -> pos -> (istate * Proof.context) option * (istate * Proof.context) option -> ctree
263 val append_problem : int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree -> ctree
264 val g_res : ppobj -> term
265 val pr_ctree : (pos -> ppobj -> string) -> ctree -> string
266 val pr_short : pos -> ppobj -> string
267 val existpt : pos -> ctree -> bool
268 val is_empty_tac : tac -> bool
269 val e_subs : string list
270 val e_sube : cterm' list
271 val g_branch : ppobj -> branch
272 val g_ctxt : ppobj -> Proof.context
273 val g_fmz : ppobj -> fmz
274 val get_allp : pos' list -> pos * (int list * pos_) -> ctree -> pos' list
275 val get_allps : (pos * pos_) list -> posel list -> ctree list -> pos' list
276 val get_allpos' : pos * posel -> ctree -> pos' list
277 val get_allpos's : pos * posel -> ctree list -> (pos * pos_) list
278 val cut_bottom : pos * posel -> ctree -> (ctree * pos' list) * bool
279 val cut_tree : ctree -> pos * 'a -> ctree * pos' list
280 val cut_level : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
281 val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
282 val get_trace : ctree -> int list -> int list -> int list list
283 val subte2subst : term list -> (term * term) list
284 val branch2str : branch -> string
285 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
289 structure Ctree(**): CALC_TREEE(**) =
292 type result = term * term list
293 type env = (term * term) list;
296 NoBranch | AndB | OrB
297 | TransitiveB (* FIXXXME.0308: set branch from met in Apply_Method
298 FIXXXME.0402: -"- in Begin_Trans'*)
299 | SequenceB | IntersectB | CollectB | MapB;
301 fun branch2str NoBranch = "NoBranch" (* for tests only *)
302 | branch2str AndB = "AndB"
303 | branch2str OrB = "OrB"
304 | branch2str TransitiveB = "TransitiveB"
305 | branch2str SequenceB = "SequenceB"
306 | branch2str IntersectB = "IntersectB"
307 | branch2str CollectB = "CollectB"
308 | branch2str MapB = "MapB";
311 Incomplete | Complete | Inconsistent (* WN041020 latter still unused *);
312 fun ostate2str Incomplete = "Incomplete" (* for tests only *)
313 | ostate2str Complete = "Complete"
314 | ostate2str Inconsistent = "Inconsistent";
317 type cid = cellID list;
319 type posel = int; (* for readability in funs accessing Ctree *)
321 val pos2str = ints2str';
323 Pbl (* PblObj-position: problem-type *)
324 | Met (* PblObj-position: method *)
325 | Frm (* PblObj-position: -> Pbl in ME (not by moveDown !)
326 | PrfObj-position: formula *)
327 | Res (* PblObj | PrfObj-position: result *)
328 | Und; (* undefined*)
329 fun pos_2str Pbl = "Pbl"
330 | pos_2str Met = "Met"
331 | pos_2str Frm = "Frm"
332 | pos_2str Res = "Res"
333 | pos_2str Und = "Und";
334 fun str2pos_ "Pbl" = Pbl
335 | str2pos_ "Met" = Met
336 | str2pos_ "Frm" = Frm
337 | str2pos_ "Res" = Res
338 | str2pos_ "Und" = Und
339 | str2pos_ str = error ("str2pos_: wrong argument = " ^ str)
341 type pos' = pos * pos_;
342 (*WN0312 remembering interator (pos * pos_) for ctree
343 pos : lev_on, lev_dn, lev_up,
344 lev_onFrm, lev_dnRes (..see solve Apply_Method !)
346 # generate1 sets pos_ if possible ...?WN0502?NOT...
347 # generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn
348 exceptions: Begin/End_Trans
349 # thus generate(1) called in
351 .# nxt_solv (tac_ -cases); general case:
352 val pos' = case pos' of (p,Res) => (lev_on p',Res) | _ => pos'
354 generate1...(Rewrite(f,..,res))..(pos, pos_)
355 cappend_atomic.................pos ////// gets f+res always!!!
356 cut_tree....................pos, pos_
358 fun pos'2str (p, p_) = pair2str (ints2str' p, pos_2str p_);
359 fun pos's2str ps = (strs2str' o (map pos'2str)) ps; (* for tests only *)
360 val e_pos' = ([], Und);
362 fun res2str (t, ts) = pair2str (term2str t, terms2str ts);
366 (*26.4.02: never used after introduction of scripts !!!
367 type loc = loc_ * (* + interpreter-state *)
368 (loc_ * rls') (* -"- for script of the ruleset*)
370 val e_loc = ([],NONE):loc;
371 val ee_loc = (e_loc,e_loc);*)
374 datatype safe = Sundef | Safe | Unsafe | Helpless;
375 fun safe2str Sundef = "Sundef"
376 | safe2str Safe = "Safe"
377 | safe2str Unsafe = "Unsafe"
378 | safe2str Helpless = "Helpless";
380 type subs = cterm' list; (*16.11.00 for FE-KE*)
381 val e_subs = ["(bdv, x)"];
383 (* argument type of tac Rewrite_Inst *)
384 type sube = cterm' list;
385 val e_sube = []: cterm' list;
386 fun sube2str s = strs2str s;
388 (*._sub_stitution as _t_erms of _e_qualities.*)
389 type subte = term list;
390 val e_subte = []: term list;
391 fun subte2str ss = terms2str ss;
393 val subte2sube = map term2str;
394 val subst2subs = map (pair2str o (apfst term2str) o (apsnd term2str));
395 fun subst2sube subst = map term2str (map HOLogic.mk_eq subst)
396 val subst2subs' = map ((apfst term2str) o (apsnd term2str));
397 fun subs2subst thy s = map (isapair2pair o (parse_patt thy)) s;
398 fun sube2subst thy s = map (dest_equals' o (parse_patt thy)) s;
399 val sube2subte = map str2term;
400 val subte2subst = map HOLogic.dest_eq;
402 fun isasub2subst isasub = ((map isapair2pair) o isalist2list) isasub;
404 type scrstate = (*state for script interpreter*)
405 env(*stack*) (*used to instantiate tac for checking assod
406 12.03.noticed: e_ not updated during execution ?!?*)
407 * loc_ (*location of tac in script*)
408 * term option(*argument of curried functions*)
409 * term (*value obtained by tac executed
410 updated also after a derivation by 'new_val'*)
411 * safe (*estimation of how result will be obtained*)
412 * bool; (*true = strongly .., false = weakly associated:
413 only used during ass_dn/up*)
414 val e_scrstate = ([],[],NONE,e_term,Sundef,false): scrstate;
415 fun topt2str NONE = "NONE"
416 | topt2str (SOME t) = "SOME" ^ term2str t;
417 fun scrstate2str (env, loc_, topt, t, safe, bool) =
418 "(" ^ env2str env ^ ", " ^ loc_2str loc_ ^ ", " ^ topt2str topt ^ ", \n" ^
419 term2str t ^ ", " ^ safe2str safe ^ ", " ^ bool2str bool ^ ")";
421 (* for handling type istate see fun from_pblobj_or_detail', +? *)
422 datatype istate = (*interpreter state*)
423 Uistate (*undefined in modspec, in '_deriv'ation*)
424 | ScrState of scrstate (*for script interpreter*)
425 | RrlsState of rrlsstate; (*for reverse rewriting*)
426 val e_istate = (ScrState ([],[],NONE,e_term,Sundef,false));
427 val e_ctxt = Proof_Context.init_global @{theory "Pure"};
429 (* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*)
430 fun is_e_ctxt ctxt = Theory.eq_thy (Proof_Context.theory_of ctxt, @{theory "Pure"});
432 type iist = istate option * istate option;
433 (*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*)
436 fun rta2str (r,(t,a)) = "\n("^(rule2str r)^",("^(term2str t)^", "^
438 fun istate2str Uistate = "Uistate"
439 | istate2str (ScrState (e, l, to, t, s, b)) =
440 "ScrState ("^ subst2str e ^",\n "^
441 loc_2str l ^", "^ termopt2str to ^",\n "^
442 term2str t ^", "^ safe2str s ^", "^ bool2str b ^")"
443 | istate2str (RrlsState (t,t1,rss,rtas)) =
444 "RrlsState ("^(term2str t)^", "^(term2str t1)^", "^
445 ((strs2str o (map (strs2str o (map rule2str)))) rss)^", "^
446 ((strs2str o (map rta2str)) rtas)^")";
447 fun istates2str (NONE, NONE) = "(#NONE, #NONE)"
448 | istates2str (NONE, SOME ist) = "(#NONE,\n#SOME "^istate2str ist^")"
449 | istates2str (SOME ist, NONE) = "(#SOME "^istate2str ist^",\n #NONE)"
450 | istates2str (SOME i1, SOME i2) = "(#SOME "^istate2str i1^",\n #SOME "^
453 fun new_val v (ScrState (env, loc_, topt, _, safe, bool)) =
454 (ScrState (env, loc_, topt, v, safe, bool))
455 | new_val _ _ = error "new_val: only for ScrState";
457 datatype con = land | lor;
461 (*.tactics propagate the construction of the calc-tree;
463 (a) 'specsteps' for the specify-phase, and others for the solve-phase
464 (b) those of the solve-phase are 'initac's and others;
465 initacs start with a formula different from the preceding formula.
466 see 'type tac_' for the internal representation of tactics.*)
467 datatype tac = (* TODO: arrange according to signature *)
468 Init_Proof of ((cterm' list) * spec)
471 | Refine_Problem of pblID | Refine_Tacitly of pblID
473 | Add_Given of cterm' | Del_Given of cterm'
474 | Add_Find of cterm' | Del_Find of cterm'
475 | Add_Relation of cterm' | Del_Relation of cterm'
477 | Specify_Theory of domID | Specify_Problem of pblID
478 | Specify_Method of metID
480 | Apply_Method of metID
481 (*.creates an 'istate' in PblObj.env; in case of 'init_form'
482 creates a formula at ((lev_on o lev_dn) p, Frm) and in this ppobj.'loc'
483 'SOME istate' (at fst of 'loc').
484 As each step (in the solve-phase) has a resulting formula (at the front-end)
485 Apply_Method also does the 1st step in the script (an 'initac') if there
486 is no 'init_form' .*)
487 | Check_Postcond of pblID
490 (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
491 because there all the thms are present with both (thmID, thm)
492 (where user-views can show both or only one of (thmID, thm)),
493 and thm is created from ThmID by assoc_thm'' when entering isabisac *)
494 | Rewrite_Inst of ( subs * thm'') | Rewrite of thm'' | Rewrite_Asm of thm''
495 | Rewrite_Set_Inst of ( subs * rls') | Rewrite_Set of rls'
496 | Detail_Set_Inst of ( subs * rls') | Detail_Set of rls'
497 | End_Detail (*end of script from next_tac,
498 in solve: switches back to parent script WN0509 drop!*)
499 | Derive of rls' (*an input formula using rls WN0509 drop!*)
500 | Calculate of string (* plus | minus | times | cancel | pow | sqrt *)
502 | Substitute of sube | Apply_Assumption of cterm' list
504 | Take of cterm' (*an 'initac'*)
505 | Take_Inst of cterm'
506 | Group of (con * int list )
507 | Subproblem of (domID * pblID) (*an 'initac'*)
508 | CAScmd of cterm' (*6.6.02 URD: Function formula; WN0509 drop!*)
509 | End_Subproblem (*WN0509 drop!*)
511 | Split_And | Conclude_And
512 | Split_Or | Conclude_Or
513 | Begin_Trans | End_Trans
514 | Begin_Sequ | End_Sequ(* substitute root.env *)
515 | Split_Intersect | End_Intersect
516 | Check_elementwise of cterm' | Collect_Trues
517 | Or_to_List (*WN120315 ~ @{thm d2_prescind1},2,3,4 in PolyEq.thy *)
519 | Empty_Tac (* TODO.11.6.03 ... of string: could carry msg of (Notappl msg)
521 | Tac of string (* eg.'repeat'*WN0509 drop! (ab)used to report syntaxerror *)
522 | End_Proof'; (* inout *)
524 (* tac2str /--> library.sml: needed in dialog.sml for 'separable *)
525 fun tac2str ma = case ma of
526 Init_Proof (ppc, spec) =>
527 "Init_Proof "^(pair2str (strs2str ppc, spec2str spec))
528 | Model_Problem => "Model_Problem "
529 | Refine_Tacitly pblID => "Refine_Tacitly "^(strs2str pblID)
530 | Refine_Problem pblID => "Refine_Problem "^(strs2str pblID)
531 | Add_Given cterm' => "Add_Given "^cterm'
532 | Del_Given cterm' => "Del_Given "^cterm'
533 | Add_Find cterm' => "Add_Find "^cterm'
534 | Del_Find cterm' => "Del_Find "^cterm'
535 | Add_Relation cterm' => "Add_Relation "^cterm'
536 | Del_Relation cterm' => "Del_Relation "^cterm'
538 | Specify_Theory domID => "Specify_Theory "^(quote domID )
539 | Specify_Problem pblID => "Specify_Problem "^(strs2str pblID )
540 | Specify_Method metID => "Specify_Method "^(strs2str metID)
541 | Apply_Method metID => "Apply_Method "^(strs2str metID)
542 | Check_Postcond pblID => "Check_Postcond "^(strs2str pblID)
543 | Free_Solve => "Free_Solve"
545 | Rewrite_Inst (subs, (id, thm)) =>
546 "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> term2str)))
547 | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> term2str)
548 | Rewrite_Asm (id, thm) => "Rewrite_Asm " ^ spair2str (id, thm |> Thm.prop_of |> term2str)
549 | Rewrite_Set_Inst (subs, rls) =>
550 "Rewrite_Set_Inst "^(pair2str (subs2str subs, quote rls))
551 | Rewrite_Set rls => "Rewrite_Set "^(quote rls )
552 | Detail_Set rls => "Detail_Set "^(quote rls )
553 | Detail_Set_Inst (subs, rls) =>
554 "Detail_Set_Inst "^(pair2str (subs2str subs, quote rls))
555 | End_Detail => "End_Detail"
556 | Derive rls' => "Derive "^rls'
557 | Calculate op_ => "Calculate "^op_
558 | Substitute sube => "Substitute "^sube2str sube
559 | Apply_Assumption ct's => "Apply_Assumption "^(strs2str ct's)
561 | Take cterm' => "Take "^(quote cterm' )
562 | Take_Inst cterm' => "Take_Inst "^(quote cterm' )
563 | Group (con, ints) =>
564 "Group "^(pair2str (con2str con, ints2str ints))
565 | Subproblem (domID, pblID) =>
566 "Subproblem "^(pair2str (domID, strs2str pblID))
567 (*| Subproblem_Full (spec, cts') =>
568 "Subproblem_Full "^(pair2str (spec2str spec, strs2str cts'))*)
569 | End_Subproblem => "End_Subproblem"
570 | CAScmd cterm' => "CAScmd "^(quote cterm')
572 | Check_elementwise cterm'=> "Check_elementwise "^(quote cterm')
573 | Or_to_List => "Or_to_List "
574 | Collect_Trues => "Collect_Trues"
576 | Empty_Tac => "Empty_Tac"
577 | Tac string => "Tac "^string
578 | End_Proof' => "tac End_Proof'"
579 | _ => "tac2str not impl. for ?!";
581 fun is_empty_tac tac = case tac of Empty_Tac => true | _ => false
583 fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
584 | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
585 | eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2
586 | eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2
587 | eq_tac (Calculate id1, Calculate id2) = id1 = id2
590 fun is_rewset (Rewrite_Set_Inst _) = true
591 | is_rewset (Rewrite_Set _) = true
592 | is_rewset _ = false;
593 fun is_rewtac (Rewrite _) = true
594 | is_rewtac (Rewrite_Inst _) = true
595 | is_rewtac (Rewrite_Asm _) = true
596 | is_rewtac tac = is_rewset tac;
598 fun tac2IDstr ma = case ma of
599 Model_Problem => "Model_Problem"
600 | Refine_Tacitly pblID => "Refine_Tacitly"
601 | Refine_Problem pblID => "Refine_Problem"
602 | Add_Given cterm' => "Add_Given"
603 | Del_Given cterm' => "Del_Given"
604 | Add_Find cterm' => "Add_Find"
605 | Del_Find cterm' => "Del_Find"
606 | Add_Relation cterm' => "Add_Relation"
607 | Del_Relation cterm' => "Del_Relation"
609 | Specify_Theory domID => "Specify_Theory"
610 | Specify_Problem pblID => "Specify_Problem"
611 | Specify_Method metID => "Specify_Method"
612 | Apply_Method metID => "Apply_Method"
613 | Check_Postcond pblID => "Check_Postcond"
614 | Free_Solve => "Free_Solve"
616 | Rewrite_Inst (subs,thm')=> "Rewrite_Inst"
617 | Rewrite thm' => "Rewrite"
618 | Rewrite_Asm thm' => "Rewrite_Asm"
619 | Rewrite_Set_Inst (subs, rls) => "Rewrite_Set_Inst"
620 | Rewrite_Set rls => "Rewrite_Set"
621 | Detail_Set rls => "Detail_Set"
622 | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst"
623 | Derive rls' => "Derive "
624 | Calculate op_ => "Calculate "
625 | Substitute subs => "Substitute"
626 | Apply_Assumption ct's => "Apply_Assumption"
628 | Take cterm' => "Take"
629 | Take_Inst cterm' => "Take_Inst"
630 | Group (con, ints) => "Group"
631 | Subproblem (domID, pblID) => "Subproblem"
632 | End_Subproblem => "End_Subproblem"
633 | CAScmd cterm' => "CAScmd"
635 | Check_elementwise cterm'=> "Check_elementwise"
636 | Or_to_List => "Or_to_List "
637 | Collect_Trues => "Collect_Trues"
639 | Empty_Tac => "Empty_Tac"
640 | Tac string => "Tac "
641 | End_Proof' => "End_Proof'"
642 | _ => "tac2str not impl. for ?!";
644 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
645 | rls_of (Rewrite_Set rls) = rls
646 | rls_of tac = error ("rls_of: called with tac '"^tac2IDstr tac^"'");
648 fun thm_of_rew (Rewrite_Inst (subs,(thmID,_))) =
649 (thmID, SOME ((subs2subst (assoc_thy "Isac") subs)))
650 | thm_of_rew (Rewrite (thmID,_)) = (thmID, NONE)
651 | thm_of_rew (Rewrite_Asm (thmID,_)) = (thmID, NONE);
653 fun rls_of_rewset (Rewrite_Set_Inst (subs,rls)) =
654 (rls, SOME ((subs2subst (assoc_thy "Isac") subs)))
655 | rls_of_rewset (Rewrite_Set rls) = (rls, NONE)
656 | rls_of_rewset (Detail_Set rls) = (rls, NONE)
657 | rls_of_rewset (Detail_Set_Inst (subs, rls)) =
658 (rls, SOME ((subs2subst (assoc_thy "Isac") subs)));
660 fun rule2tac thy _ (Calc (opID, thm)) = Calculate (assoc_calc thy opID)
661 | rule2tac _ [] (Thm thm'') = Rewrite thm''
662 | rule2tac _ subst (Thm thm'') =
663 Rewrite_Inst (subst2subs subst, thm'')
664 | rule2tac _ [] (Rls_ rls) = Rewrite_Set (id_rls rls)
665 | rule2tac _ subst (Rls_ rls) =
666 Rewrite_Set_Inst (subst2subs subst, (id_rls rls))
667 | rule2tac _ _ rule =
668 error ("rule2tac: called with '" ^ rule2str rule ^ "'");
670 type fmz_ = cterm' list;
672 (*.a formalization of an example containing data
673 sufficient for mechanically finding the solution for the example.*)
674 (*FIXME.WN051014: dont store fmz = (_,spec) in the PblObj,
675 this is done in origin*)
676 type fmz = fmz_ * spec;
677 val e_fmz = ([],e_spec);
679 (* tac_ contains results from check in 'fun applicable_in'.
680 This is useful for costly results, e.g. from rewriting;
681 however, these results might be changed by Scripts like
682 " eq = (Rewrite_Set ansatz_rls False) eql;" ^
683 " eq = drop_questionmarks eq;" ^
684 " eq = (Rewrite_Set equival_trans False) eq;" ^
685 WN120106 TODO ANALOGOUSLY TO Substitute':
686 So tac_ contains the term t the result was calculated from
687 in order to compare t with t' possibly changed by "Expr "
688 and re-calculate result if t<>t'*)
689 datatype tac_ = (* TODO: arrange according to signature *)
690 Init_Proof' of ((cterm' list) * spec)
693 itm list * (*the 'untouched' pbl*)
694 itm list (*the casually completed met*)
697 pblID * (*the refined from applicable_in*)
698 domID * (*from new pbt?! filled in specify*)
699 metID * (*from new pbt?! filled in specify*)
700 itm list (*drop ! 9.03: remains [] for
701 Model_Problem recognizing its activation*)
702 | Refine_Problem' of (pblID * (itm list * (bool * Term.term) list))
703 (*FIXME?040215 drop: done automatically in init_proof + Subproblem'*)
706 itm list (*updated with input in fun specify_additem*)
707 | Add_Find' of cterm' * itm list (* see Add_Given' *)
708 | Add_Relation' of cterm' * itm list (* see Add_Given' *)
709 | Del_Given' of cterm' | Del_Find' of cterm' | Del_Relation' of cterm'
710 (*4.00.: all.. term: in applicable_in ..? Syn ?only for FormFK?*)
711 | Specify_Theory' of domID
712 | Specify_Problem' of
714 (bool * (* matches *)
715 (itm list * (* ppc *)
716 (bool * term) list))) (* preconditions *)
719 ori list * (*repl. "#undef"*)
720 itm list (*... updated from pbl to met*)
723 (term option) * (*init_form*)
724 istate * Proof.context
727 (term * (*returnvalue of script in solve*)
728 term list) (*collect by get_assumptions_ in applicable_in, except if
729 butlast tac is Check_elementwise: take only these asms*)
731 (* context_thy would be simpler if instead thm' woudl be thm *)
732 | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * (term * term list)
733 | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * result
734 | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * result
735 | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * result
736 | Detail_Set_Inst' of theory' * bool * subst * rls * term * result
737 | Rewrite_Set' of theory' * bool * rls * term * result
738 | Detail_Set' of theory' * bool * rls * term * result
739 | End_Detail' of (term * (term list)) (*see End_Trans'*)
740 | End_Ruleset' of term
742 | Calculate' of theory' * string * term * (term * thm')
744 rew_ord_ * (*for re-calculation *)
745 rls * (*for re-calculation *)
746 subte * (*the 'substitution': terms of type bool*)
747 term * (*to be substituted in *)
748 term (*resulting from the substitution *)
749 | Apply_Assumption' of term list * term
754 (ori list) * (* filled in assod Subproblem' *)
755 term * (*-"-, headline of calc-head *)
757 Proof.context *(* transported from assod to generate1 *)
758 term) (* Subproblem(dom,pbl) OR cascmd*)
760 | End_Subproblem' of term (*???*)
761 | Split_And' of term | Conclude_And' of term
762 | Split_Or' of term | Conclude_Or' of term
763 | Begin_Trans' of term | End_Trans' of (term * (term list))
764 | Begin_Sequ' | End_Sequ'(* substitute root.env*)
765 | Split_Intersect' of term | End_Intersect' of term
766 | Check_elementwise' of (*special case:*)
767 term * (*(1)the current formula: [x=1,x=...]*)
768 string * (*(2)the pred from Check_elementwise *)
769 (term * (*(3)composed from (1) and (2): {x. pred}*)
770 term list) (*20.5.03 assumptions*)
771 | Or_to_List' of term * term (* (a | b, [a,b]) *)
772 | Collect_Trues' of term
774 | Tac_ of (*for dummies*)
778 string (*result of Tac".."*)
779 | End_Proof'';(*End_Proof:inout*)
781 fun tac_2str ma = case ma of
782 Init_Proof' (ppc, spec) =>
783 "Init_Proof' "^(pair2str (strs2str ppc, spec2str spec))
784 | Model_Problem' (pblID,_,_) => "Model_Problem' "^(strs2str pblID )
785 | Refine_Tacitly'(p,prefin,domID,metID,itms)=>
787 ^(strs2str p)^", "^(strs2str prefin)^", "
788 ^domID^", "^(strs2str metID)^", pbl-itms)"
789 | Refine_Problem' ms => "Refine_Problem' ("^(*matchs2str ms*)"..."^")"
790 (*| Match_Problem' (pI, (ok, (itms, pre))) =>
791 "Match_Problem' "^(spair2str (strs2str pI,
792 spair2str (bool2str ok,
793 spair2str ("itms2str_ itms",
794 "items2str pre"))))*)
795 | Add_Given' cterm' => "Add_Given' "(*^cterm'*)
796 | Del_Given' cterm' => "Del_Given' "(*^cterm'*)
797 | Add_Find' cterm' => "Add_Find' "(*^cterm'*)
798 | Del_Find' cterm' => "Del_Find' "(*^cterm'*)
799 | Add_Relation' cterm' => "Add_Relation' "(*^cterm'*)
800 | Del_Relation' cterm' => "Del_Relation' "(*^cterm'*)
802 | Specify_Theory' domID => "Specify_Theory' "^(quote domID )
803 | Specify_Problem' (pI, (ok, (itms, pre))) =>
804 "Specify_Problem' "^(spair2str (strs2str pI,
805 spair2str (bool2str ok,
806 spair2str ("itms2str_ itms",
808 | Specify_Method' (pI,oris,itms) =>
809 "Specify_Method' ("^metID2str pI^", "^oris2str oris^", )"
811 | Apply_Method' (metID,_,_,_) => "Apply_Method' "^(strs2str metID)
812 | Check_Postcond' (pblID,(scval,asm)) =>
814 (spair2str (strs2str pblID, spair2str (term2str scval, terms2str asm)))
816 | Free_Solve' => "Free_Solve'"
818 | Rewrite_Inst' (*subs,thm'*) _ =>
819 "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
820 | Rewrite' thm' => "Rewrite' "(*^(spair2str thm')*)
821 | Rewrite_Asm' thm' => "Rewrite_Asm' "(*^(spair2str thm')*)
822 | Rewrite_Set_Inst' (*subs,thm'*) _ =>
823 "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
824 | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) =>
825 "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^ "," ^ id_rls rls' ^ "," ^
826 term2str f ^ ",(" ^ term2str f' ^ "," ^ terms2str asm ^ "))"
827 | End_Detail' _ => "End_Detail' xxx"
828 | Detail_Set' _ => "Detail_Set' xxx"
829 | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
831 | Derive' rls => "Derive' "^id_rls rls
832 | Calculate' _ => "Calculate' "
833 | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
834 | Apply_Assumption' ct's => "Apply_Assumption' "(*^(strs2str ct's)*)
836 | Take' cterm' => "Take' "(*^(quote cterm' )*)
837 | Take_Inst' cterm' => "Take_Inst' "(*^(quote cterm' )*)
838 | Subproblem' (spec, oris, _, _, _, pbl_form) =>
839 "Subproblem' "(*^(pair2str (domID, strs2str ,...))*)
840 | End_Subproblem' _ => "End_Subproblem'"
841 | CAScmd' cterm' => "CAScmd' "(*^(quote cterm')*)
843 | Empty_Tac_ => "Empty_Tac_"
844 | Tac_ (_,form,id,result) => "Tac_ (thy,"^form^","^id^","^result^")"
845 | _ => "tac_2str not impl. for arg";
847 (*'executed tactics' (tac_s) with local environment etc.;
848 used for continuing eval script + for generate*)
850 (loc_ * (* of tactic in scr, tactic (weakly) associated with tac_*)
851 (tac_ * (* (for generate) *)
852 env * (* with 'tactic=result' as a rule, tactic ev. _not_ ready:
853 for handling 'parallel let'*)
854 env * (* with results of (ready) tacs *)
855 term * (* itr_arg of tactic, for upd. env at Repeat, Try*)
856 term * (* result value of the tac *)
862 fun ets2s (l,(m,eno,env,iar,res,s)) =
863 "\n(" ^ loc_2str l ^ ",(" ^ tac_2str m ^
864 ",\n ens= " ^ subst2str eno ^
865 ",\n env= " ^ subst2str env ^
866 ",\n iar= " ^ term2str iar ^
867 ",\n res= " ^ term2str res ^
868 ",\n " ^ safe2str s ^ "))";
869 fun ets2str (ets: ets) = (strs2str o (map ets2s)) ets;
872 type envp =(*9.5.03: unused, delete with field in ctree.PblObj FIXXXME*)
873 (int * term list) list * (*assoc-list: args of met*)
874 (int * rls) list * (*assoc-list: tacs already done ///15.9.00*)
875 (int * ets) list * (*assoc-list: tacs etc. already done*)
876 (string * pos) list; (*asms * from where*)
877 val empty_envp = ([], [], [], []): envp;
879 datatype ppobj = (* TODO: arrange according to signature *)
881 {cell : lrd option, (* where in form tac has been applied *)
882 (*^^^FIXME.WN0607 rename this field*)
883 form : term, (* where tac is applied to *)
884 tac : tac, (* also in istate *)
885 loc : (istate * (* script interpreter state *)
886 Proof.context) (* context for provers, type inference *)
887 option * (* both for interpreter location on Frm, Pbl, Met *)
888 (istate * (* script interpreter state *)
889 Proof.context) (* context for provers, type inference *)
890 option, (* both for interpreter location on Res *)
891 (*(NONE,NONE) <==> e_istate ! see update_loc, get_loc*)
892 branch: branch, (* only rudimentary *)
893 result: result, (* result and assumptions *)
894 ostate: ostate} (* Complete <=> result is OK *)
896 {cell : lrd option, (* unused: meaningful only for some _Prf_Obj *)
897 fmz : fmz, (* from init:FIXME never use this spec;-drop *)
898 origin: (ori list) * (* representation from fmz+pbt
899 for efficiently adding items in probl, meth *)
900 spec * (* updated by Refine_Tacitly *)
901 term, (* headline of calc-head, as calculated initially(!)*)
902 spec : spec, (* explicitly input *)
903 probl : itm list, (* itms explicitly input *)
904 meth : itm list, (* itms automatically added to copy of probl *)
905 ctxt : Proof.context, (* WN110513 introduced to avoid [*] [**]*)
906 env : (istate * Proof.context) option,
907 (* istate only for initac in script
908 context for specify phase on this node NO..
909 ..NO: this conflicts with init_form/initac: see Apply_Method without init_form *)
910 loc : (istate * Proof.context) option * (istate * (* like PrfObj *)
911 Proof.context) option, (* for spec-phase [*], NO..
912 ..NO: raises errors not tracable on WN110513 [**]*)
913 branch: branch, (* like PrfObj *)
914 result: result, (* like PrfObj *)
915 ostate: ostate}; (* like PrfObj *)
917 (*.this tree contains isac's calculations; TODO.WN03 rename to ctree;
918 the tree's structure has been copied from an early version of Theorema(c);
919 it has the disadvantage, that there is no space
920 for the first tactic in a script generating the first formula at (p,Frm);
921 this trouble has been covered by 'init_form' and 'Take' so far,
922 but it is crucial if the first tactic in a script is eg. 'Subproblem';
923 see 'type tac ', Apply_Method.
927 | Nd of ppobj * (ctree list);
928 val e_ctree = EmptyPtree;
929 type state = ctree * pos
931 fun rep_prfobj (PrfObj {cell,form,tac,loc,branch,result,ostate}) =
932 {cell=cell,form=form,tac=tac,loc=loc,branch=branch,result=result,ostate=ostate};
933 fun rep_pblobj (PblObj {cell,origin,fmz,spec,probl,meth,ctxt,
934 env,loc,branch,result,ostate}) =
935 {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,ctxt=ctxt,
936 env=env,loc=loc,branch=branch,result=result,ostate=ostate};
937 fun is_prfobj (PrfObj _) = true
938 | is_prfobj _ =false;
939 (*val is_prfobj' = get_obj is_prfobj; *)
940 fun is_pblobj (PblObj _) = true
941 | is_pblobj _ = false;
942 (*val is_pblobj' = get_obj is_pblobj; 'Error: unbound constructor get_obj'*)
945 exception PTREE of string;
946 fun nth _ [] = raise PTREE "nth _ []"
948 | nth n (x::xs) = nth (n-1) xs;
949 (*> nth 2 [11,22,33]; -->> val it = 22 : int*)
951 fun lev_up [] = raise PTREE "lev_up []"
952 | lev_up p = (drop_last p):pos;
953 fun lev_on [] = raise PTREE "lev_on []"
955 let val len = length pos
956 in (drop_last pos) @ [(nth len pos)+1] end;
957 fun lev_onFrm (p,_) = (lev_on p,Frm):pos'
958 | lev_onFrm p = raise PTREE ("*** lev_onFrm: pos'="^(pos'2str p));
959 (*040216: for inform --> embed_deriv: remains on same level TODO.WN120517 compare lev_pred*)
960 fun lev_back' ([],_) = raise PTREE "lev_back': called by ([],_)"
962 if last_elem p <= 1 then (p, Frm):pos'
963 else ((drop_last p) @ [(nth (length p) p) - 1], Res);
964 (*.increase pos by n within a level.*)
965 fun pos_plus 0 pos = pos
966 | pos_plus n (p,Frm) = pos_plus (n-1) (p, Res)
967 | pos_plus n (p, _) = pos_plus (n-1) (lev_on p, Res);
969 fun lev_pred [] = raise PTREE "lev_pred []"
971 let val len = length pos
972 in ((drop_last pos) @ [(nth len pos)-1]) end;
974 val it = [1,2,2] : pos
976 val it = [0] : pos *)
978 fun lev_dn p = p @ [0];
979 (*> (lev_dn o lev_on) [1,2,3];
980 val it = [1,2,4,0] : pos *)
981 (*fun lev_dn' ((p,p_):pos') = (lev_dn p, Frm):pos'; WN.3.12.03: never used*)
982 fun lev_dnRes (p,_) = (lev_dn p, Res);
985 fun lev_up_ (p,Res) = (lev_up p,Res):pos'
986 | lev_up_ p' = error ("lev_up_: called for "^(pos'2str p'));
987 fun lev_dn_ (p, _) = (lev_dn p, Res)
988 fun ind (p,_) = length p; (*WN050108 deprecated in favour of lev_of*)
989 fun lev_of (p,_) = length p;
992 (** convert ctree to a string **)
994 (* convert a pos from list to string *)
995 fun pr_pos ps = (space_implode "." (map string_of_int ps))^". ";
996 (* show hd origin or form only *)
997 fun pr_short p (PblObj {origin = (ori,_,_),...}) =
998 ((pr_pos p) ^ " ----- pblobj -----\n")
999 (* ((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^
1000 (((Syntax.string_of_term (thy2ctxt' "Isac")) o hd(*!?!*) o #5 o hd) ori))^
1002 | pr_short p (PrfObj {form = form,...}) =
1003 ((pr_pos p) ^ (term2str form) ^ "\n");
1005 fun pr_cell (p:pos) (PblObj {cell = c, origin = (ori,_,_),...}) =
1007 ((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^
1008 (((Syntax.string_of_term (thy2ctxt' "Isac")) o hd(*!?!*) o #5 o hd) ori))^
1010 | pr_cell p (PrfObj {cell = c, form = form,...}) =
1011 ((ints2str c) ^" "^ (term2str form) ^ "\n");
1017 fun pr_pt pfn _ EmptyPtree = ""
1018 | pr_pt pfn ps (Nd (b, [])) = pfn ps b
1019 | pr_pt pfn ps (Nd (b, ts)) = (pfn ps b)^
1021 and prts pfn ps p [] = ""
1022 | prts pfn ps p (t::ts) = (pr_pt pfn (ps @ [p]) t)^
1023 (prts pfn ps (p+1) ts)
1024 in pr_pt f [] pt end;
1026 > fun prfn ps b = (pr_pos ps)^" "^b(*TODO*)^"\n";
1027 (*val pt = Unsynchronized.ref EmptyPtree;*)
1034 > tracing (pr_ctree prfn (!pt));
1038 (** access the branches of ctree **)
1040 fun ins_nth 1 e l = e::l
1041 | ins_nth n e [] = raise PTREE "ins_nth n e []"
1042 | ins_nth n e (l::ls) = l::(ins_nth (n-1) e ls);
1043 fun repl [] _ _ = raise PTREE "repl [] _ _"
1044 | repl (l::ls) 1 e = e::ls
1045 | repl (l::ls) n e = l::(repl ls (n-1) e);
1046 fun repl_app ls n e =
1047 let val lim = 1 + length ls
1048 in if n > lim then raise PTREE "repl_app: n > lim"
1049 else if n = lim then ls @ [e]
1050 else repl ls n e end;
1052 > repl [1,2,3] 2 22222;
1053 val it = [1,22222,3] : int list
1054 > repl_app [1,2,3,4] 5 5555;
1055 val it = [1,2,3,4,5555] : int list
1056 > repl_app [1,2,3] 2 22222;
1057 val it = [1,22222,3] : int list
1058 > repl_app [1] 2 22222 ;
1059 val it = [1,22222] : int list
1063 (*.get from obj at pos by f : ppobj -> 'a.*)
1064 fun get_obj f EmptyPtree _ = raise PTREE "get_obj f EmptyPtree"
1065 | get_obj f (Nd (b, _)) [] = f b
1066 | get_obj f (Nd (b, bs)) (p::ps) =
1067 (* val (f, Nd (b, bs), (p::ps)) = (I, pt, p);
1069 let val _ = (nth p bs) handle _ => raise PTREE ("get_obj: pos = "^
1070 (ints2str' (p::ps))^" does not exist");
1071 in (get_obj f (nth p bs) ps)
1072 (*before WN050419: 'wrong type..' raised also if pos doesn't exist*)
1073 handle _ => raise PTREE (*"get_obj: at pos = "^
1074 (ints2str' (p::ps))^" wrong type of ppobj"*)
1076 (ints2str' (p::ps))^" does not exist")
1078 fun get_nd EmptyPtree _ = raise PTREE "get_nd EmptyPtree"
1080 | get_nd (Nd (_,nds)) (pos as p :: ps) = (get_nd (nth p nds) ps)
1081 handle _ => raise PTREE ("get_nd: not existent pos = "^(ints2str' pos));
1083 (* for use by get_obj *)
1084 fun g_cell (PblObj {cell = c,...}) = NONE
1085 | g_cell (PrfObj {cell = c,...}) = c;(*WN0607 hack for quick introduction of lrd + rewrite-at (thms, calcs)*)
1086 fun g_form (PrfObj {form = f,...}) = f
1087 | g_form (PblObj {origin=(_,_,f),...}) = f;
1088 fun g_form' (Nd (PrfObj {form = f,...}, _)) = f
1089 | g_form' (Nd (PblObj {origin=(_,_,f),...}, _)) = f;
1090 (* | g_form _ = raise PTREE "g_form not for PblObj";*)
1091 fun g_origin (PblObj {origin = ori,...}) = ori
1092 | g_origin _ = raise PTREE "g_origin not for PrfObj";
1093 fun g_fmz (PblObj {fmz = f,...}) = f
1094 | g_fmz _ = raise PTREE "g_fmz not for PrfObj";
1095 fun g_spec (PblObj {spec = s,...}) = s
1096 | g_spec _ = raise PTREE "g_spec not for PrfObj";
1097 fun g_pbl (PblObj {probl = p,...}) = p
1098 | g_pbl _ = raise PTREE "g_pbl not for PrfObj";
1099 fun g_met (PblObj {meth = p,...}) = p
1100 | g_met _ = raise PTREE "g_met not for PrfObj";
1101 fun g_domID (PblObj {spec = (d,_,_),...}) = d
1102 | g_domID _ = raise PTREE "g_metID not for PrfObj";
1103 fun g_metID (PblObj {spec = (_,_,m),...}) = m
1104 | g_metID _ = raise PTREE "g_metID not for PrfObj";
1105 fun g_ctxt (PblObj {ctxt, ...}) = ctxt
1106 | g_ctxt _ = raise PTREE "g_ctxt not for PrfObj";
1107 fun g_env (PblObj {env,...}) = env
1108 | g_env _ = raise PTREE "g_env not for PrfObj";
1109 fun g_loc (PblObj {loc = l,...}) = l
1110 | g_loc (PrfObj {loc = l,...}) = l;
1111 fun g_branch (PblObj {branch = b,...}) = b
1112 | g_branch (PrfObj {branch = b,...}) = b;
1113 fun g_tac (PblObj {spec = (d,p,m),...}) = Apply_Method m
1114 | g_tac (PrfObj {tac = m,...}) = m;
1115 fun g_result (PblObj {result = r,...}) = r
1116 | g_result (PrfObj {result = r,...}) = r;
1117 fun g_res (PblObj {result = (r,_),...}) = r
1118 | g_res (PrfObj {result = (r,_),...}) = r;
1119 fun g_res' (Nd (PblObj {result = (r,_),...}, _)) = r
1120 | g_res' (Nd (PrfObj {result = (r,_),...}, _)) = r;
1121 fun g_ostate (PblObj {ostate = r,...}) = r
1122 | g_ostate (PrfObj {ostate = r,...}) = r;
1123 fun g_ostate' (Nd (PblObj {ostate = r,...}, _)) = r
1124 | g_ostate' (Nd (PrfObj {ostate = r,...}, _)) = r;
1126 fun gpt_cell (Nd (PblObj {cell = c,...},_)) = NONE
1127 | gpt_cell (Nd (PrfObj {cell = c,...},_)) = c;
1129 (* get the formula preceeding the current position in a calculation *)
1130 fun get_curr_formula (pt, pos as (p, p_)) =
1132 Frm => get_obj g_form pt p
1133 | Res => (fst o (get_obj g_result pt)) p
1134 | _ => #3 (get_obj g_origin pt p);
1136 (*in CalcTree/Subproblem an 'just_created_' model is created;
1137 this is filled to 'untouched' by Model/Refine_Problem*)
1138 fun just_created_ (PblObj {meth, probl, spec, ...}) =
1139 null meth andalso null probl andalso spec = e_spec;
1140 val e_origin = ([],e_spec,e_term);
1142 fun just_created (pt, (p, _)) =
1143 let val ppobj = get_obj I pt p
1144 in is_pblobj ppobj andalso just_created_ ppobj end;
1146 (*.does the pos in the ctree exist ?.*)
1147 fun existpt pos pt = can (get_obj I pt) pos;
1148 (*.does the pos' in the ctree exist, ie. extra check for result in the node.*)
1149 fun existpt' (p,p_) pt =
1150 if can (get_obj I pt) p
1152 Res => get_obj g_ostate pt p = Complete
1156 (*.is this position appropriate for calculating intermediate steps?.*)
1157 fun is_interpos (_, Res) = true
1158 | is_interpos _ = false;
1160 fun last_onlev pt pos = not (existpt (lev_on pos) pt);
1163 (*.find the position of the next parent which is a PblObj in ctree.*)
1164 fun par_pblobj pt [] = []
1166 let fun par pt [] = []
1167 | par pt p = if is_pblobj (get_obj I pt p) then p
1168 else par pt (lev_up p)
1169 in par pt (lev_up p) end;
1170 (* lev_up for hard_gen operating with pos = [...,0] *)
1172 (*.find the position and the children of the next parent which is a PblObj.*)
1173 fun par_children (Nd (PblObj _, children)) [] = (children, [])
1174 | par_children (pt as Nd (PblObj _, children)) p =
1175 let fun par [] = (children, [])
1176 | par p = let val Nd (obj, children) = get_nd pt p
1177 in if is_pblobj obj then (children, p) else par (lev_up p)
1179 in par (lev_up p) end;
1181 (*.get the children of a node in ctree.*)
1182 fun children (Nd (PblObj _, cn)) = cn
1183 | children (Nd (PrfObj _, cn)) = cn;
1186 (*.find the next parent, which is either a PblObj (return true)
1187 or a PrfObj with tac = Detail_Set (return false).*)
1188 (*FIXME.3.4.03:re-organize par_pbl_det after rls' --> rls*)
1189 fun par_pbl_det pt [] = (true, [], Erls)
1190 | par_pbl_det pt p =
1191 let fun par pt [] = (true, [], Erls)
1192 | par pt p = if is_pblobj (get_obj I pt p) then (true, p, Erls)
1193 else case get_obj g_tac pt p of
1194 (*Detail_Set rls' => (false, p, assoc_rls rls')
1195 (*^^^--- before 040206 after ---vvv*)
1196 |*)Rewrite_Set rls' => (false, p, assoc_rls rls')
1197 | Rewrite_Set_Inst (_, rls') =>
1198 (false, p, assoc_rls rls')
1199 | _ => par pt (lev_up p)
1200 in par pt (lev_up p) end;
1205 (*.get from the whole ctree by f : ppobj -> 'a.*)
1206 fun get_all f EmptyPtree = []
1207 | get_all f (Nd (b, [])) = [f b]
1208 | get_all f (Nd (b, bs)) = [f b] @ (get_alls f bs)
1209 and get_alls f [] = []
1210 | get_alls f pts = flat (map (get_all f) pts);
1213 (*.insert obj b into ctree at pos, ev.overwriting this pos.
1214 covers library.ML TODO.WN110315 rename*)
1215 fun insert_pt b EmptyPtree [] = Nd (b, [])
1216 | insert_pt b EmptyPtree _ = raise PTREE "insert_pt b Empty _"
1217 | insert_pt b (Nd ( _, _)) [] = raise PTREE "insert_pt b _ []"
1218 | insert_pt b (Nd (b', bs)) (p::[]) =
1219 Nd (b', repl_app bs p (Nd (b,[])))
1220 | insert_pt b (Nd (b', bs)) (p::ps) =
1221 Nd (b', repl_app bs p (insert_pt b (nth p bs) ps));
1223 > type ppobj = string;
1224 > tracing (pr_ctree prfn (!pt));
1225 (*val pt = Unsynchronized.ref Empty;*)
1226 pt:= insert_pt ("root'":ppobj) EmptyPtree [];
1227 pt:= insert_pt ("xx1":ppobj) (!pt) [1];
1228 pt:= insert_pt ("xx2":ppobj) (!pt) [2];
1229 pt:= insert_pt ("xx3":ppobj) (!pt) [3];
1230 pt:= insert_pt ("xx2.1":ppobj) (!pt) [2,1];
1231 pt:= insert_pt ("xx2.2":ppobj) (!pt) [2,2];
1232 pt:= insert_pt ("xx2.1.1":ppobj) (!pt) [2,1,1];
1233 pt:= insert_pt ("xx2.1.2":ppobj) (!pt) [2,1,2];
1234 pt:= insert_pt ("xx2.1.3":ppobj) (!pt) [2,1,3];
1237 (*.insert children to a node without children.*)
1238 (*compare: fun insert_pt*)
1239 fun ins_chn _ EmptyPtree _ = raise PTREE "ins_chn: EmptyPtree"
1240 | ins_chn ns (Nd _) [] = raise PTREE "ins_chn: pos = []"
1241 | ins_chn ns (Nd (b, bs)) (p::[]) =
1242 if p > length bs then raise PTREE "ins_chn: pos not existent"
1243 else let val Nd (b', bs') = nth p bs
1244 in if null bs' then Nd (b, repl_app bs p (Nd (b', ns)))
1245 else raise PTREE "ins_chn: pos mustNOT be overwritten" end
1246 | ins_chn ns (Nd (b, bs)) (p::ps) =
1247 Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps));
1249 (* print_depth 11;ins_chn;print_depth 3; ###insert_pt#########################*);
1252 (** apply f to obj at pos, f: ppobj -> ppobj **)
1254 fun appl_to_node f (Nd (b,bs)) = Nd (f b, bs);
1255 fun appl_obj f EmptyPtree [] = EmptyPtree
1256 | appl_obj f EmptyPtree _ = raise PTREE "appl_obj f Empty _"
1257 | appl_obj f (Nd (b, bs)) [] = Nd (f b, bs)
1258 | appl_obj f (Nd (b, bs)) (p::[]) =
1259 Nd (b, repl_app bs p (((appl_to_node f) o (nth p)) bs))
1260 | appl_obj f (Nd (b, bs)) (p::ps) =
1261 Nd (b, repl_app bs p (appl_obj f (nth p bs) (ps:pos)));
1263 (* for use by appl_obj *)
1264 fun repl_form f (PrfObj {cell=c,form= _,tac=tac,loc=loc,
1265 branch=branch,result=result,ostate=ostate}) =
1266 PrfObj {cell=c,form= f,tac=tac,loc=loc,
1267 branch=branch,result=result,ostate=ostate}
1268 | repl_form _ _ = raise PTREE "repl_form takes no PblObj";
1269 fun repl_pbl x (PblObj {cell=cell,origin=origin,fmz=fmz,
1270 spec=spec,probl=_,meth=meth,ctxt=ctxt,env=env,loc=loc,
1271 branch=branch,result=result,ostate=ostate}) =
1272 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl= x,
1273 meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1274 | repl_pbl _ _ = raise PTREE "repl_pbl takes no PrfObj";
1275 fun repl_met x (PblObj {cell=cell,origin=origin,fmz=fmz,
1276 spec=spec,probl=probl,meth=_,ctxt=ctxt,env=env,loc=loc,
1277 branch=branch,result=result,ostate=ostate}) =
1278 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
1279 meth= x,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1280 | repl_met _ _ = raise PTREE "repl_pbl takes no PrfObj";
1282 fun repl_spec x (PblObj {cell=cell,origin=origin,fmz=fmz,
1283 spec= _,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
1284 branch=branch,result=result,ostate=ostate}) =
1285 PblObj {cell=cell,origin=origin,fmz=fmz,spec= x,probl=probl,
1286 meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1287 | repl_spec _ _ = raise PTREE "repl_domID takes no PrfObj";
1288 fun repl_domID x (PblObj {cell=cell,origin=origin,fmz=fmz,
1289 spec=(_,p,m),probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
1290 branch=branch,result=result,ostate=ostate}) =
1291 PblObj {cell=cell,origin=origin,fmz=fmz,spec=(x,p,m),probl=probl,
1292 meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1293 | repl_domID _ _ = raise PTREE "repl_domID takes no PrfObj";
1294 fun repl_pblID x (PblObj {cell=cell,origin=origin,fmz=fmz,
1295 spec=(d,_,m),probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
1296 branch=branch,result=result,ostate=ostate}) =
1297 PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,x,m),probl=probl,
1298 meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1299 | repl_pblID _ _ = raise PTREE "repl_pblID takes no PrfObj";
1300 fun repl_metID x (PblObj {cell=cell,origin=origin,fmz=fmz,
1301 spec=(d,p,_),probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
1302 branch=branch,result=result,ostate=ostate}) =
1303 PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,p,x),probl=probl,
1304 meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1305 | repl_metID _ _ = raise PTREE "repl_metID takes no PrfObj";
1307 fun repl_result l f' s (PrfObj {cell=cell,form=form,tac=tac,loc=_,
1308 branch=branch,result = _ ,ostate = _}) =
1309 PrfObj {cell=cell,form=form,tac=tac,loc= l,
1310 branch=branch,result = f',ostate = s}
1311 | repl_result l f' s (PblObj {cell=cell,origin=origin,fmz=fmz,
1312 spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=_,
1313 branch=branch,result= _ ,ostate= _}) =
1314 PblObj {cell=cell,origin=origin,fmz=fmz,
1315 spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc= l,
1316 branch=branch,result= f',ostate= s};
1318 fun repl_tac x (PrfObj {cell=cell,form=form,tac= _,loc=loc,
1319 branch=branch,result=result,ostate=ostate}) =
1320 PrfObj {cell=cell,form=form,tac= x,loc=loc,
1321 branch=branch,result=result,ostate=ostate}
1322 | repl_tac _ _ = raise PTREE "repl_tac takes no PblObj";
1324 fun repl_branch b (PblObj {cell=cell,origin=origin,fmz=fmz,
1325 spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
1326 branch= _,result=result,ostate=ostate}) =
1327 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
1328 meth=meth,ctxt=ctxt,env=env,loc=loc,branch= b,result=result,ostate=ostate}
1329 | repl_branch b (PrfObj {cell=cell,form=form,tac=tac,loc=loc,
1330 branch= _,result=result,ostate=ostate}) =
1331 PrfObj {cell=cell,form=form,tac=tac,loc=loc,
1332 branch= b,result=result,ostate=ostate};
1335 (PblObj {cell, origin, fmz, spec, probl, meth,
1336 ctxt=_, env, loc, branch, result, ostate}) =
1337 PblObj {cell=cell, origin=origin, fmz=fmz, spec=spec, probl=probl, meth=meth,
1338 ctxt=x, env=env, loc=loc, branch=branch, result=result, ostate=ostate}
1339 | repl_ctxt _ _ = raise PTREE "repl_env takes no PrfObj";
1342 (PblObj {cell=cell, origin=origin, fmz=fmz, spec=spec, probl=probl, meth=meth,
1343 ctxt=ctxt, env=_, loc=loc, branch=branch, result=result, ostate=ostate}) =
1344 PblObj {cell=cell, origin=origin, fmz=fmz, spec=spec, probl=probl, meth=meth,
1345 ctxt=ctxt, env=e, loc=loc, branch=branch, result=result, ostate=ostate}
1346 | repl_env _ _ = raise PTREE "repl_env takes no PrfObj";
1349 (PblObj {cell=cell,origin=(_,spe,hdf),fmz=fmz,
1350 spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
1351 branch=branch,result=result,ostate=ostate}) =
1352 PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,
1353 meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,
1354 result=result,ostate=ostate}
1355 | repl_oris _ _ = raise PTREE "repl_oris takes no PrfObj";
1356 fun repl_orispec spe
1357 (PblObj {cell=cell,origin=(oris,_,hdf),fmz=fmz,
1358 spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
1359 branch=branch,result=result,ostate=ostate}) =
1360 PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,
1361 meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,
1362 result=result,ostate=ostate}
1363 | repl_orispec _ _ = raise PTREE "repl_orispec takes no PrfObj";
1365 fun repl_loc l (PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,
1366 ctxt=ctxt,env=env,loc=_,branch=branch,result=result,ostate=ostate}) =
1367 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,
1368 ctxt=ctxt,env=env,loc=l,branch=branch,result=result,ostate=ostate}
1369 | repl_loc l (PrfObj {cell=cell,form=form,tac=tac,
1370 loc=_,branch=branch,result=result,ostate=ostate}) =
1371 PrfObj {cell=cell,form=form,tac=tac,
1372 loc= l,branch=branch,result=result,ostate=ostate};
1374 (*WN050219 put here for interpreting code for cut_tree below...*)
1376 bool * (*ALL itms+preconds true*)
1377 pos_ * (*model belongs to Problem | Method*)
1378 term * (*header: Problem... or Cas
1379 FIXXXME.12.03: item! for marking syntaxerrors*)
1380 itm list * (*model: given, find, relate*)
1381 ((bool * term) list) *(*model: preconds*)
1382 spec; (*specification*)
1383 val e_ocalhd = (false, Und, e_term, [e_itm], [(false, e_term)], e_spec);
1385 datatype ptform = Form of term | ModSpec of ocalhd;
1386 val e_ptform = Form e_term;
1387 val e_ptform' = ModSpec e_ocalhd;
1389 (*.applies (snd f) to the branches at a pos if ((fst f) b),
1390 f : (ppobj -> bool) * (int -> ctree list -> ctree list).*)
1392 fun appl_branch f EmptyPtree [] = (EmptyPtree, false)
1393 | appl_branch f EmptyPtree _ = raise PTREE "appl_branch f Empty _"
1394 | appl_branch f (Nd ( _, _)) [] = raise PTREE "appl_branch f _ []"
1395 | appl_branch f (Nd (b, bs)) (p::[]) =
1396 if (fst f) b then (Nd (b, (snd f) p bs), true)
1397 else (Nd (b, bs), false)
1398 | appl_branch f (Nd (b, bs)) (p::ps) =
1399 let val (b',bool) = appl_branch f (nth p bs) ps
1400 in (Nd (b, repl_app bs p b'), bool) end;
1402 (* for cut_level; appl_branch(deprecated) *)
1403 fun test_trans (PrfObj{branch = Transitive,...}) = true
1404 | test_trans (PblObj{branch = Transitive,...}) = true
1405 | test_trans _ = false;
1407 fun is_pblobj' pt p =
1408 let val ppobj = get_obj I pt p
1409 in is_pblobj ppobj end;
1411 fun delete_result pt p =
1412 (appl_obj (repl_result (fst (get_obj g_loc pt p), NONE)
1413 (e_term,[]) Incomplete) pt p);
1415 fun del_res (PblObj {cell, fmz, origin, spec, probl, meth,
1416 ctxt, env, loc=(l1,_), branch, result, ostate}) =
1417 PblObj {cell=cell,fmz=fmz,origin=origin,spec=spec,probl=probl,meth=meth,
1418 ctxt=ctxt,env=env, loc=(l1,NONE), branch=branch, result=(e_term,[]),
1421 | del_res (PrfObj {cell, form, tac, loc=(l1,_), branch, result, ostate}) =
1422 PrfObj {cell=cell,form=form,tac=tac, loc=(l1,NONE), branch=branch,
1423 result=(e_term,[]), ostate=Incomplete};
1425 (*FIXME.WN0312 update_X X pos pt -> pt could be chained by o (efficiency?)*)
1426 (*fun update_fmz pt pos x = appl_obj (repl_fmz x) pt pos; WN01xx *)
1427 fun update_ctxt pt pos x = appl_obj (repl_ctxt x) pt pos; (*for use on PblObj,
1428 otherwise use fun generate1; compare fun get_ctxt*)
1429 fun update_env pt pos x = appl_obj (repl_env x) pt pos;
1430 fun update_domID pt pos x = appl_obj (repl_domID x) pt pos;
1431 fun update_pblID pt pos x = appl_obj (repl_pblID x) pt pos;
1432 fun update_metID pt pos x = appl_obj (repl_metID x) pt pos;
1433 fun update_spec pt pos x = appl_obj (repl_spec x) pt pos;
1434 fun update_pbl pt pos x = appl_obj (repl_pbl x) pt pos;
1435 fun update_pblppc pt pos x = appl_obj (repl_pbl x) pt pos;
1436 fun update_met pt pos x = appl_obj (repl_met x) pt pos;
1437 fun update_metppc pt pos x = appl_obj (repl_met x) pt pos;
1438 fun update_branch pt pos x = appl_obj (repl_branch x) pt pos;
1439 fun update_tac pt pos x = appl_obj (repl_tac x) pt pos;
1440 fun update_oris pt pos x = appl_obj (repl_oris x) pt pos;
1441 fun update_orispec pt pos x = appl_obj (repl_orispec x) pt pos;
1443 (*WN050305 for handling cut_tree in cappend_atomic + for testing*)
1444 fun update_loc' pt pos x = appl_obj (repl_loc x) pt pos;
1446 (*13.8.02: options, because istate is no equalitype any more*)
1447 fun get_loc EmptyPtree _ = (e_istate, e_ctxt)
1448 | get_loc pt (p,Res) =
1449 (case get_obj g_loc pt p of
1451 | (NONE , NONE) => (e_istate, e_ctxt)
1452 | (_ , SOME i) => i)
1453 | get_loc pt (p,_) =
1454 (case get_obj g_loc pt p of
1455 (NONE , SOME i) => i (*13.8.02 just copied from ^^^: too liberal ?*)
1456 | (NONE , NONE) => (e_istate, e_ctxt)
1457 | (SOME i, _) => i);
1458 fun get_istate pt p = get_loc pt p |> #1;
1459 fun get_ctxt pt (pos as (p, p_)) =
1460 if member op = [Frm, Res] p_
1461 then get_loc pt pos |> #2 (*for script interpretation rely on fun get_loc*)
1462 else get_obj g_ctxt pt p (*for specify phase take ctx from PblObj*)
1464 fun get_assumptions_ pt p = get_ctxt pt p |> get_assumptions;
1466 (*pos of the formula on FE relative to the current pos,
1467 which is the next writepos*)
1470 let val (ps,p) = split_last pp
1471 in case p of 1 => ps | n => ps @ [n-1] end;
1473 (*WN.20.5.03 ... but not used*)
1474 fun posless [] (_::_) = true
1475 | posless (_::_) [] = false
1476 | posless (p::ps) (q::qs) = if p = q then posless ps qs else p < q;
1477 (* posless [2,3,4] [3,4,5];
1479 > posless [2,3,4] [1,2,3];
1481 > posless [2,3] [2,3,4];
1483 > posless [2,3,4] [2,3];
1485 > posless [6] [6,5,2];
1487 +++ see Isabelle/../library.ML*)
1490 (**.development for extracting an 'interval' from ctree.**)
1492 (*WN0510 version stopped in favour of get_interval with !!!move_dn, getFormulaeFromTo
1493 actually used (inefficient) version with move_dn: see modspec.sml*)
1496 fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*)
1497 fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)
1498 fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x;
1499 fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
1501 fun getnd i (b,p) q (Nd (po, nds)) =
1502 (if i <= 0 then [[b]] else []) @
1503 (getnds (i-1) true (b@[hdp p], tlp p) (tlq q)
1504 (take_fromto (hdp p) (hdq q) nds))
1506 and getnds _ _ _ _ [] = [] (*no children*)
1507 | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)
1509 | getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*)
1510 (getnd i ( b, p ) [99999] n1) @
1511 (getnd ~99999 (lev_on b,[0]) q n2)
1513 | getnds i _ (b,p) q [n1, n2] = (*intern, r-margin*)
1514 (getnd i ( b,[0]) [99999] n1) @
1515 (getnd ~99999 (lev_on b,[0]) q n2)
1517 | getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*)
1518 (getnd i ( b, p ) [99999] nd) @
1519 (getnds ~99999 false (lev_on b,[0]) q nds)
1521 | getnds i _ (b,p) q (nd::(nds as _::_)) = (*intern, ...*)
1522 (getnd i ( b,[0]) [99999] nd) @
1523 (getnds ~99999 false (lev_on b,[0]) q nds);
1525 (*get an 'interval from to' from a ctree as 'intervals f t' of respective nodes
1526 where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
1527 (1) the 'f' are given
1528 (1a) by 'from' if 'f' = the respective element of 'from' (left margin)
1529 (1b) -inifinity, if 'f' > the respective element of 'from' (internal node)
1530 (2) the 't' ar given
1531 (2a) by 'to' if 't' = the respective element of 'to' (right margin)
1532 (2b) inifinity, if 't' < the respective element of 'to (internal node)'
1533 the 'f' and 't' are set by hdp,... *)
1534 fun get_trace pt p q =
1535 (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q)))
1536 (take_fromto (hdp p) (hdq q) (children pt));
1539 fun get_somespec (dI,pI,mI) (dI',pI',mI') =
1540 let val domID = if dI = e_domID
1541 then if dI' = e_domID
1542 then error"pt_extract: no domID in probl,origin"
1545 val pblID = if pI = e_pblID
1546 then if pI' = e_pblID
1547 then error"pt_extract: no pblID in probl,origin"
1550 val metID = if mI = e_metID
1551 then if pI' = e_metID
1552 then error"pt_extract: no metID in probl,origin"
1555 in (domID, pblID, metID) end;
1556 fun get_somespec' (dI,pI,mI) (dI',pI',mI') =
1557 let val domID = if dI = e_domID then dI' else dI
1558 val pblID = if pI = e_pblID then pI' else pI
1559 val metID = if mI = e_metID then mI' else mI
1560 in (domID, pblID, metID) end;
1562 (*extract a formula or model from ctree for itms2itemppc or model2xml*)
1563 fun preconds2str bts =
1564 (strs2str o (map (linefeed o pair2str o
1566 (apfst bool2str)))) bts;
1567 fun ocalhd2str (b, p, hdf, itms, prec, spec) =
1568 "("^bool2str b^", "^pos_2str p^", "^term2str hdf^
1569 ", "^itms2str_ (thy2ctxt' "Isac") itms^
1570 ", "^preconds2str prec^", \n"^spec2str spec^" )";
1574 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj;
1577 (**.functions for the 'ctree iterator' as seen from the FE-Kernel interface.**)
1579 (*move one step down into existing nodes of ctree; regard TransitiveB
1580 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~##################
1581 fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*)
1582 (* val (Nd (c, ns), ([],p_)) = (pt, get_pos cI uI);
1585 then case p_ of (*Frm => ([], Pbl) 1.12.03
1586 |*) Res => raise PTREE "move_dn: end of calculation"
1587 | _ => if null ns (*go down from Pbl + Met*)
1588 then raise PTREE "move_dn: solve problem not started"
1590 else (case p_ of Res => raise PTREE "move_dn: end of (sub-)tree"
1592 then raise PTREE "move_dn: pos not existent 1"
1595 (*iterate towards end of pos*)
1596 (* val (P,(Nd (_, ns)),(p::(ps as (_::_)),p_)) = ([]:pos, pt, get_pos cI uI);
1597 val (P,(Nd (_, ns)),(p::(ps as (_::_)),p_)) = ((P@[p]),(nth p ns),(ps, p_));
1599 | move_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
1600 if p > length ns then raise PTREE "move_dn: pos not existent 2"
1601 else move_dn ((P@[p]): pos) (nth p ns) (ps, p_)
1602 (* val (P, (Nd (c, ns)), ([p], p_)) = ((P@[p]), (nth p ns), (ps, p_));
1603 val (P, (Nd (c, ns)), ([p], p_)) = ([],pt,get_pos cI uI);
1605 | move_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1606 if p > length ns then raise PTREE "move_dn: pos not existent 3"
1607 else if is_pblnd (nth p ns) then
1608 ((*tracing("### move_dn: is_pblnd (nth p ns), P= "^ints2str' P^", \n"^
1609 "length ns= "^((string_of_int o length) ns)^
1610 ", p= "^string_of_int p^", p_= "^pos_2str p_);*)
1611 case p_ of Res => if p = length ns
1612 then if g_ostate c = Complete then (P, Res)
1613 else raise PTREE (ints2str' P^" not complete")
1614 (*FIXME here handle not-sequent-branches*)
1615 else if g_branch c = TransitiveB
1616 andalso (not o is_pblnd o (nth (p+1))) ns
1618 else (P@[p+1], if is_pblnd (nth (p+1) ns)
1620 | _ => if (null o children o (nth p)) ns (*go down from Pbl*)
1621 then raise PTREE "move_dn: solve subproblem not started"
1623 if (is_pblnd o hd o children o (nth p)) ns
1626 (* val (P, Nd (c, ns), ([p], p_)) = ([], pt, ([1], Frm));
1628 else case p_ of Frm => if (null o children o (nth p)) ns
1629 (*then if g_ostate c = Complete then (P@[p],Res)*)
1630 then if g_ostate' (nth p ns) = Complete
1632 else raise PTREE "move_dn: pos not existent 4"
1633 else (P @ [p, 1], (*go down*)
1634 if (is_pblnd o hd o children o (nth p)) ns
1636 | Res => if p = length ns
1638 if g_ostate c = Complete then (P, Res)
1639 else raise PTREE (ints2str' P^" not complete")
1641 if g_branch c = TransitiveB
1642 andalso (not o is_pblnd o (nth (p+1))) ns
1643 then if (null o children o (nth (p+1))) ns
1645 else (P@[p+1,1], Frm)(*040221*)
1646 else (P@[p+1], if is_pblnd (nth (p+1) ns)
1649 (*.move one step down into existing nodes of ctree; skip Res = Frm.nxt;
1650 move_dn at the end of the calc-tree raises PTREE.*)
1651 fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*)
1653 Res => raise PTREE "move_dn: end of calculation"
1654 | _ => if null ns (*go down from Pbl + Met*)
1655 then raise PTREE "move_dn: solve problem not started"
1657 | move_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =(*iterate to end of pos*)
1658 if p > length ns then raise PTREE "move_dn: pos not existent 2"
1659 else move_dn (P@[p]) (nth p ns) (ps, p_)
1661 | move_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1662 if p > length ns then raise PTREE "move_dn: pos not existent 3"
1665 if p = length ns (*last Res on this level: go a level up*)
1666 then if g_ostate c = Complete then (P, Res)
1667 else raise PTREE (ints2str' P^" not complete 1")
1668 else (*go to the next Nd on this level, or down into the next Nd*)
1669 if is_pblnd (nth (p+1) ns) then (P@[p+1], Pbl)
1671 if g_res' (nth p ns) = g_form' (nth (p+1) ns)
1672 then if (null o children o (nth (p+1))) ns
1673 then (*take the Res if Complete*)
1674 if g_ostate' (nth (p+1) ns) = Complete
1676 else raise PTREE (ints2str' (P@[p+1])^
1678 else (P@[p+1,1], Frm)(*go down into the next PrfObj*)
1679 else (P@[p+1], Frm)(*take Frm: exists if the Nd exists*)
1680 | Frm => (*go down or to the Res of this Nd*)
1681 if (null o children o (nth p)) ns
1682 then if g_ostate' (nth p ns) = Complete then (P @ [p], Res)
1683 else raise PTREE (ints2str' (P @ [p])^" not complete 3")
1684 else (P @ [p, 1], Frm)
1685 | _ => (*is Pbl or Met*)
1686 if (null o children o (nth p)) ns
1687 then raise PTREE "move_dn:solve subproblem not startd"
1689 if (is_pblnd o hd o children o (nth p)) ns
1693 (*.go one level down into ctree.*)
1694 fun movelevel_dn [] (Nd (c, ns)) ([],p_) = (*root problem*)
1697 then raise PTREE "solve problem not started"
1698 else ([1], if (is_pblnd o hd) ns then Pbl else Frm)
1699 else raise PTREE "pos not existent 1"
1701 (*iterate towards end of pos*)
1702 | movelevel_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
1703 if p > length ns then raise PTREE "pos not existent 2"
1704 else movelevel_dn (P@[p]) (nth p ns) (ps, p_)
1706 | movelevel_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1707 if p > length ns then raise PTREE "pos not existent 3" else
1710 then raise PTREE "no children"
1712 if g_branch c = TransitiveB
1713 then if (null o children o (nth (p+1))) ns
1714 then raise PTREE "no children"
1716 if (is_pblnd o hd o children o (nth (p+1))) ns
1718 else if (null o children o (nth p)) ns
1719 then raise PTREE "no children"
1720 else (P @ [p, 1], if (is_pblnd o hd o children o (nth p)) ns
1722 | _ => if (null o children o (nth p)) ns
1723 then raise PTREE "no children"
1724 else (P @ [p, 1], (*go down*)
1725 if (is_pblnd o hd o children o (nth p)) ns
1730 (*.go to the previous position in ctree; regard TransitiveB.*)
1731 fun move_up _ (Nd (c, ns)) ([],p_) = (*root problem*)
1733 then case p_ of Res => if null ns then ([], Pbl) (*Res -> Pbl (not Met)!*)
1734 else ([length ns], Res)
1735 | _ => raise PTREE "begin of calculation"
1736 else raise PTREE "pos not existent"
1738 | move_up P (Nd (_, ns)) (p::(ps as (_::_)),p_) = (*iterate to end of pos*)
1739 if p > length ns then raise PTREE "pos not existent"
1740 else move_up (P@[p]) (nth p ns) (ps,p_)
1742 | move_up P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1743 if p > length ns then raise PTREE "pos not existent"
1744 else if is_pblnd (nth p ns) then
1746 let val nc = (length o children o (nth p)) ns
1747 in if nc = 0 then (P@[p], Pbl) (*Res -> Pbl (not Met)!*)
1748 else (P @ [p, nc], Res) end (*go down*)
1749 | _ => if p = 1 then (P, Pbl) else (P@[p-1], Res)
1750 else case p_ of Frm => if p <> 1 then (P, Frm)
1751 else if is_pblobj c then (P, Pbl) else (P, Frm)
1753 let val nc = (length o children o (nth p)) ns
1754 in if nc = 0 (*cannot go down*)
1755 then if g_branch c = TransitiveB andalso p <> 1
1756 then (P@[p-1], Res) else (P@[p], Frm)
1757 else (P @ [p, nc], Res) end; (*go down*)
1761 (*.go one level up in ctree; sets the position on Frm.*)
1762 fun movelevel_up _ (Nd (c, ns)) (([],p_):pos') = (*root problem*)
1763 raise PTREE "pos not existent"
1765 (*iterate towards end of pos*)
1766 | movelevel_up P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
1767 if p > length ns then raise PTREE "pos not existent"
1768 else movelevel_up (P@[p]) (nth p ns) (ps,p_)
1770 | movelevel_up P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1771 if p > length ns then raise PTREE "pos not existent"
1772 else if is_pblobj c then (P, Pbl) else (P, Frm);
1775 (*.go to the next calc-head up in the calc-tree.*)
1776 fun movecalchd_up pt ((p, Res):pos') =
1777 (par_pblobj pt p, Pbl):pos'
1778 | movecalchd_up pt (p, _) =
1779 if is_pblobj (get_obj I pt p)
1780 then (p, Pbl) else (par_pblobj pt p, Pbl);
1782 (*.determine the previous pos' on the same level.*)
1783 (*WN0502 made for interSteps; _only_ works for branch TransitiveB WN120517 compare lev_back*)
1784 fun lev_pred' pt (pos:pos' as ([],Res)) = ([],Pbl):pos'
1785 | lev_pred' pt (pos:pos' as (p, Res)) =
1786 let val (p', last) = split_last p
1788 then if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm)
1789 else if get_obj g_res pt (p' @ [last - 1]) = get_obj g_form pt p
1790 then (p' @ [last - 1], Res) (*TransitiveB*)
1791 else if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm)
1795 (*.determine the next pos' on the same level.*)
1796 fun lev_on' pt (([],Pbl):pos') = ([],Res):pos'
1797 | lev_on' pt (p, Res) =
1798 if get_obj g_res pt p = get_obj g_form pt (lev_on p)(*TransitiveB*)
1799 then if existpt' (lev_on p, Res) pt then (lev_on p, Res)
1800 else error ("lev_on': (p, Res) -> (p, Res) not existent, \
1801 \p = "^ints2str' (lev_on p))
1802 else (lev_on p, Frm)
1803 | lev_on' pt (p, _) =
1804 if existpt' (p, Res) pt then (p, Res)
1805 else error ("lev_on': (p, Frm) -> (p, Res) not existent, \
1806 \p = "^ints2str' p);
1808 fun exist_lev_on' pt p = (lev_on' pt p; true) handle _ => false;
1810 (*.is the pos' at the last element of a calulation _AND_ can be continued.*)
1811 (* val (pt, pos as (p,p_)) = (pt, ([1],Frm));
1813 fun is_curr_endof_calc pt (([],Res) : pos') = false
1814 | is_curr_endof_calc pt (pos as (p,_)) =
1815 not (exist_lev_on' pt pos)
1816 andalso get_obj g_ostate pt (lev_up p) = Incomplete;
1819 (**.insert into ctree and cut branches accordingly.**)
1821 (*.get all positions of certain intervals on the ctree.*)
1822 (*OLD VERSION without move_dn; kept for occasional redesign
1823 get all pos's to be cut in a ctree
1824 below a pos or from a ctree list after i-th element (NO level_up).*)
1825 fun get_allpos' (_:pos, _:posel) EmptyPtree = ([]:pos' list)
1826 | get_allpos' (p, 1) (Nd (b, bs)) = (*p is pos of Nd*)
1827 if g_ostate b = Incomplete
1828 then ((*tracing("get_allpos' (p, 1) Incomplete: p="^ints2str' p);*)
1829 [(p,Frm)] @ (get_allpos's (p, 1) bs)
1831 else ((*tracing("get_allpos' (p, 1) else: p="^ints2str' p);*)
1832 [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)]
1834 (*WN041020 here we assume what is presented on the worksheet ?!*)
1835 | get_allpos' (p, i) (Nd (b, bs)) = (*p is pos of Nd*)
1836 if length bs > 0 orelse is_pblobj b
1837 then if g_ostate b = Incomplete
1838 then [(p,Frm)] @ (get_allpos's (p, 1) bs)
1839 else [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)]
1841 if g_ostate b = Incomplete
1844 (*WN041020 here we assume what is presented on the worksheet ?!*)
1845 and get_allpos's _ [] = []
1846 | get_allpos's (p, i) (pt::pts) = (*p is pos of parent-Nd*)
1847 (get_allpos' (p@[i], i) pt) @ (get_allpos's (p, i+1) pts);
1849 (*.get all positions of certain intervals on the ctree.*)
1850 (*NEW version WN050225*)
1854 (*before WN041019......
1855 val cut_branch = (test_trans, curry take):
1856 (ppobj -> bool) * (int -> ctree list -> ctree list);
1857 .. formlery used for ...
1858 fun cut_tree''' _ [] = EmptyPtree
1859 | cut_tree''' pt pos =
1860 let val (pt',cut) = appl_branch cut_branch pt pos
1861 in if cut andalso length pos > 1 then cut_tree''' pt' (lev_up pos)
1864 (*OLD version before WN050225*)
1865 (*WN050106 like cut_level, but deletes exactly 1 node --- for tests ONLY*)
1866 fun cut_level_'_ (_:pos' list) (_:pos) EmptyPtree (_:pos') =
1867 raise PTREE "cut_level_'_ Empty _"
1868 | cut_level_'_ _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level_'_ _ []"
1869 | cut_level_'_ cuts P (Nd (b, bs)) (p::[],p_) =
1871 then (Nd (b, drop_nth [] (p:posel, bs)),
1874 (if p_ = Frm then [(P@[p],Res)] else ([]:pos' list)) @
1875 (*WN041020 here we assume what is presented on the worksheet ?!*)
1876 (get_allpos's (P, p+1) (drop_nth [] (p, bs))))
1878 else (Nd (b, bs), cuts)
1879 | cut_level_'_ cuts P (Nd (b, bs)) ((p::ps),p_) =
1880 let val (bs',cuts') = cut_level_'_ cuts P (nth p bs) (ps, p_)
1881 in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
1884 fun cut_level (_:pos' list) (_:pos) EmptyPtree (_:pos') =
1885 raise PTREE "cut_level EmptyPtree _"
1886 | cut_level _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level _ []"
1888 | cut_level cuts P (Nd (b, bs)) (p::[],p_) =
1890 then (Nd (b, take (p:posel, bs)),
1892 (if p_ = Frm andalso (*#*) g_ostate b = Complete
1893 then [(P@[p],Res)] else ([]:pos' list)) @
1894 (*WN041020 here we assume what is presented on the worksheet ?!*)
1895 (get_allpos's (P, p+1) (takerest (p, bs))))
1896 else (Nd (b, bs), cuts)
1898 | cut_level cuts P (Nd (b, bs)) ((p::ps),p_) =
1899 let val (bs',cuts') = cut_level cuts P (nth p bs) (ps, p_)
1900 in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
1902 (*OLD version before WN050219, overwritten below*)
1903 fun cut_tree _ (([],_):pos') = raise PTREE "cut_tree _ ([],_)"
1904 | cut_tree pt (pos as ([p],_)) =
1905 let val (pt', cuts) = cut_level ([]:pos' list) [] pt pos
1906 in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
1907 then [] else [([],Res)])) end
1908 | cut_tree pt (p,p_) =
1910 fun cutfn pt cuts (p,p_) =
1911 let val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_)
1912 val cuts'' = if get_obj g_ostate pt (lev_up p) = Incomplete
1913 then [] else [(lev_up p, Res)]
1914 in if length cuts' > 0 andalso length p > 1
1915 then cutfn pt' (cuts @ cuts') (lev_up p, Frm(*-->(p,Res)*))
1916 else (pt',cuts @ cuts') end
1917 val (pt', cuts) = cutfn pt [] (p,p_)
1918 in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
1919 then [] else [([], Res)])) end;
1922 (*########/ inserted from ctreeNEW.sml \#################################**)
1924 (*.get all positions in a ctree until ([],Res) or ostate=Incomplete
1926 pos' list -> : accumulated, start with []
1927 pos -> : the offset for subtrees wrt the root
1928 ctree -> : (sub)tree
1929 pos' : initialization (the last pos' before ...)
1930 -> pos' list : of positions in this (sub) tree (relative to the root)
1932 (* val (cuts, P, pt, pos) = ([], [3], get_nd pt [3], ([], Frm):pos');
1933 val (cuts, P, pt, pos) = ([], [2], get_nd pt [2], ([], Frm):pos');
1934 length (children pt);
1936 fun get_allp (cuts:pos' list) (P:pos, pos:pos') pt =
1937 (let val nxt = move_dn [] pt pos (*exn if Incomplete reached*)
1938 in if nxt <> ([],Res)
1939 then get_allp (cuts @ [nxt]) (P, nxt) pt
1940 else (map (apfst (curry op@ P)) (cuts @ [nxt])): pos' list
1941 end) handle PTREE _ => (map (apfst (curry op@ P)) cuts);
1944 (*the pts are assumed to be on the same level*)
1945 fun get_allps (cuts: pos' list) (P:pos) [] = cuts
1946 | get_allps cuts P (pt::pts) =
1947 let val below = get_allp [] (P, ([], Frm)) pt
1950 then (P, Pbl)::below
1951 else if last_elem P = 1
1952 then (P, Frm)::below
1953 else (*Trans*) below
1954 val levres = levfrm @ (if null below then [(P, Res)] else [])
1955 in get_allps (cuts @ levres) (lev_on P) pts end;
1958 (**.these 2 funs decide on how far cut_tree goes.**)
1959 (*.shall the nodes _after_ the pos to be inserted at be deleted?.*)
1960 fun test_trans (PrfObj{branch = Transitive,...}) = true
1961 | test_trans (PrfObj{branch = NoBranch,...}) = true
1962 | test_trans (PblObj{branch = Transitive,...}) = true
1963 | test_trans (PblObj{branch = NoBranch,...}) = true
1964 | test_trans _ = false;
1965 (*.shall cutting be continued on the higher level(s)?
1966 the Nd regarded will NOT be changed.*)
1967 fun cutlevup (PblObj _) = false (*for tests of LK0502*)
1968 | cutlevup _ = true;
1969 val cutlevup = test_trans;(*WN060727 after summerterm tests.LK0502 withdrawn*)
1971 (*cut_bottom new sml603..608
1972 cut the level at the bottom of the pos (used by cappend_...)
1973 and handle the parent in order to avoid extra case for root
1974 fn: ctree -> : the _whole_ ctree for cut_levup
1975 pos * posel -> : the pos after split_last
1976 ctree -> : the parent of the Nd to be cut
1978 (ctree * : the updated ctree
1979 pos' list) * : the pos's cut
1980 bool : cutting shall be continued on the higher level(s)
1982 fun cut_bottom _ (pt' as Nd (b, [])) = ((pt', []), cutlevup b)
1983 | cut_bottom (P:pos, p:posel) (Nd (b, bs)) =
1984 let (*divide level into 3 parts...*)
1985 val keep = take (p - 1, bs)
1986 val pt' as Nd (_,bs') = nth p bs
1987 (*^^^^^_here_ will be 'insert_pt'ed by 'append_..'*)
1988 val (tail, tp) = (takerest (p, bs),
1989 if null (takerest (p, bs)) then 0 else p + 1)
1990 val (children, cuts) =
1993 (if is_pblnd pt' then [(P @ [p], Pbl)] else [])
1994 @ (get_allp [] (P @ [p], (P, Frm)) pt')
1995 @ (get_allps [] (P @ [p+1]) tail))
1996 else (keep @ [(*'insert_pt'ed by 'append_..'*)] @ tail,
1997 get_allp [] (P @ [p], (P, Frm)) pt')
2000 then (Nd (del_res b, children),
2001 cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
2002 else (Nd (b, children), cuts)
2003 (*val _= tracing("####cut_bottom (P, p)="^pos2str (P @ [p])^
2004 ", Nd=.............................................")
2006 val _= tracing("####cut_bottom form='"^
2007 term2str (get_obj g_form pt'' []))
2008 val _= tracing("####cut_bottom cuts#="^string_of_int (length cuts)^
2009 ", cuts="^pos's2str cuts)*)
2010 in ((pt'', cuts:pos' list), cutlevup b) end;
2013 (*.go all levels from the bottom of 'pos' up to the root,
2014 on each level compose the children of a node and accumulate the cut Nds
2016 pos' list -> : for accumulation
2017 bool -> : cutting shall be continued on the higher level(s)
2018 ctree -> : the whole ctree for 'get_nd pt P' on each level
2019 ctree -> : the Nd from the lower level for insertion at path
2020 pos * posel -> : pos=path split for convenience
2021 ctree -> : Nd the children of are under consideration on this call
2023 ctree * pos' list : the updated parent-Nd and the pos's of the Nds cut
2025 fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) =
2026 let (*divide level into 3 parts...*)
2027 val keep = take (p - 1, bs)
2028 (*val pt' comes as argument from below*)
2029 val (tail, tp) = (takerest (p, bs),
2030 if null (takerest (p, bs)) then 0 else p + 1)
2031 val (children, cuts') =
2033 then (keep @ [pt'], get_allps [] (P @ [p+1]) tail)
2034 else (keep @ [pt'] @ tail, [])
2035 val clevup' = if clevup then cutlevup b else false
2036 (*the first Nd with false stops cutting on all levels above*)
2039 then (Nd (del_res b, children),
2040 cuts' @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
2041 else (Nd (b, children), cuts')
2042 (*val _= tracing("#####cut_levup clevup= "^bool2str clevup)
2043 val _= tracing("#####cut_levup cutlevup b= "^bool2str (cutlevup b))
2044 val _= tracing("#####cut_levup (P, p)="^pos2str (P @ [p])^
2045 ", Nd=.............................................")
2047 val _= tracing("#####cut_levup form='"^
2048 term2str (get_obj g_form pt'' []))
2049 val _= tracing("#####cut_levup cuts#="^string_of_int (length cuts)^
2050 ", cuts="^pos's2str cuts)*)
2051 in if null P then (pt'', (cuts @ cuts'):pos' list)
2052 else let val (P, p) = split_last P
2053 in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P)
2057 (*.cut nodes after and below an inserted node in the ctree;
2058 the cuts range is limited by the predicate 'fun cutlevup'.*)
2059 fun cut_tree pt (pos,_) =
2060 if not (existpt pos pt)
2061 then (pt,[]) (*appending a formula never cuts anything*)
2062 else let val (P, p) = split_last pos
2063 val ((pt', cuts), clevup) = cut_bottom (P, p) (get_nd pt P)
2064 (* pt' is the updated parent of the Nd to cappend_..*)
2065 in if null P then (pt', cuts)
2066 else let val (P, p) = split_last P
2067 in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P)
2071 fun append_atomic p l f r f' s pt =
2072 let (**val _= tracing("#@append_atomic: pos ="^pos2str p)**)
2073 val (iss, f) = if existpt p pt andalso is_empty_tac (get_obj g_tac pt p)
2075 ((fst (get_obj g_loc pt p), SOME l),
2076 get_obj g_form pt p)
2077 else ((NONE, SOME l), f)
2078 in insert_pt (PrfObj {cell = NONE,
2084 ostate= s}) pt p end;
2087 (*20.8.02: cappend_* FIXXXXME cut branches below cannot be decided here:
2088 detail - generate - cappend: inserted, not appended !!!
2090 cut decided in applicable_in !?!
2092 fun cappend_atomic pt p loc f r f' s =
2093 (* val (pt, p, loc, f, r, f', s) =
2094 (pt,p,l,f,Rewrite_Set_Inst (subst2subs subs',id_rls rls'),
2097 ((*tracing("##@cappend_atomic: pos ="^pos2str p);*)
2098 apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm))
2100 (*TODO.WN050305 redesign the handling of istates*)
2101 fun cappend_atomic pt p ist_res f r f' s =
2102 if existpt p pt andalso is_empty_tac (get_obj g_tac pt p)
2103 then (*after Take: transfer Frm and respective istate*)
2106 (get_loc pt (p,Frm), get_obj g_form pt p)
2107 val (pt, cs) = cut_tree pt (p,Frm)
2108 val pt = append_atomic p (e_istate, e_ctxt) f r f' s pt
2109 val pt = update_loc' pt p (SOME ist_form, SOME ist_res)
2111 else apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
2113 (* called by Take *)
2114 fun append_form p l f pt =
2115 ((*tracing("##@append_form: pos ="^pos2str p);*)
2116 insert_pt (PrfObj {cell = NONE,
2117 form = (*if existpt p pt
2118 andalso get_obj g_tac pt p = Empty_Tac
2119 (*distinction from 'old' (+complete!) pobjs*)
2120 then get_obj g_form pt p else*) f,
2122 loc = (SOME l, NONE),
2124 result= (e_term,[]),
2125 ostate= Incomplete}) pt p
2127 (* val (p,loc,f) = ([1], e_istate, str2term "x + 1 = 2");
2128 val (p,loc,f) = (fst p, e_istate, str2term "-1 + x = 0");
2130 fun cappend_form pt p loc f =
2131 ((*tracing("##@cappend_form: pos ="^pos2str p);*)
2132 apfst (append_form p loc f) (cut_tree pt (p,Frm))
2134 fun cappend_form pt p loc f =
2135 let (*val _= tracing("##@cappend_form: pos ="^pos2str p)
2136 val _= tracing("##@cappend_form before cut_tree: loc ="^istate2str loc)*)
2137 val (pt', cs) = cut_tree pt (p,Frm)
2138 val pt'' = append_form p loc f pt'
2139 (*val _= tracing("##@cappend_form after append: loc ="^
2140 istates2str (get_obj g_loc pt'' p))*)
2145 fun append_result pt p l f s =
2146 (appl_obj (repl_result (fst (get_obj g_loc pt p), SOME l) f s) pt p, []);
2149 (*WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml*)
2150 fun append_parent p l f r b pt =
2151 let (*val _= tracing("###append_parent: pos ="^pos2str p);*)
2152 val (ll,f) = if existpt p pt andalso is_empty_tac (get_obj g_tac pt p)
2153 then ((fst (get_obj g_loc pt p), SOME l),
2154 get_obj g_form pt p)
2155 else ((SOME l, NONE), f)
2156 in insert_pt (PrfObj
2162 result= (e_term,[]),
2163 ostate= Incomplete}) pt p end;
2164 fun cappend_parent pt p loc f r b =
2165 ((*tracing("###cappend_parent: pos ="^pos2str p);*)
2166 apfst (append_parent p loc f r b) (cut_tree pt (p,Und))
2170 fun append_problem [] l fmz (strs,spec,hdf) _ =
2171 ((*tracing("###append_problem: pos = []");*)
2174 origin= (strs,spec,hdf),
2177 probl = []:itm list,
2181 loc = (SOME l, NONE),
2182 branch= TransitiveB,(*FIXXXXXME.27.8.03: for equations only*)
2183 result= (e_term,[]),
2184 ostate= Incomplete},[]))
2186 | append_problem p l fmz (strs,spec,hdf) pt =
2187 ((*tracing("###append_problem: pos ="^pos2str p);*)
2190 origin= (strs,spec,hdf),
2193 probl = []:itm list,
2197 loc = (SOME l, NONE),
2198 branch= TransitiveB,
2199 result= (e_term,[]),
2200 ostate= Incomplete}) pt p
2202 fun cappend_problem _ [] loc fmz ori =
2203 ((*tracing("###cappend_problem: pos = []");*)
2204 (append_problem [] loc fmz ori EmptyPtree,[])
2206 | cappend_problem pt p loc fmz ori =
2207 ((*tracing("###cappend_problem: pos ="^pos2str p);*)
2208 apfst (append_problem p (loc:(istate * Proof.context)) fmz ori) (cut_tree pt (p,Frm))
2211 (*.get the theory explicitly specified for the rootpbl;
2212 thus use this function _after_ finishing specification.*)
2213 fun rootthy (Nd (PblObj {spec=(thyID, _, _), ...}, _)) = assoc_thy thyID
2214 | rootthy _ = error "rootthy";
2219 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2221 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2223 (* policy for "open" structures:
2224 --------------------------------
2225 The above "open Ctree" creates an unclear situation with structures, in particular in test/.
2226 This is work in progress, but urges to make policy explicit:
2228 (1) All structures are closed with a signature; this for prepares re-arrangement of structures.
2229 (2) Some structures are pervasive (e.g. Ctree) such, that an "open" ensures readability locally.
2230 (3) test/ is preceeded by "open" for all structures, in order to ease copy&paste from scr/ to test/
2232 ad (1) Presently this point is under construction.
2233 ad (2) Such local "open" are kept to a minimum (with the goal to reach Isabelle's state).
2234 ad (3) See https://intra.ist.tugraz.at/hg/isa/file/2ba35efb07b7/test/Tools/isac/Test_Isac.thy#l70