1 (* Title: the calctree, which holds a calculation
2 Author: Walther Neuper 1999
3 (c) due to copyright terms
6 signature BASIC_CALC_TREE =
8 (** definitions required for datatype ctree, renamed later appropriately **)
10 (** the basic datatype **)
14 (* for generate.sml ?!? ca.*)
20 datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB
21 datatype ostate = Complete | Incomplete | Inconsistent
25 cell: TermC.lrd option,
26 loc: (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option,
31 origin: Model.ori list * Celem.spec * term,
32 probl: Model.itm list,
36 env: (Istate_Def.T * Proof.context) option}
39 cell: TermC.lrd option,
40 loc: (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option,
46 datatype ctree = EmptyPtree | Nd of ppobj * ctree list
48 (** basic functions **)
49 val e_ctree : ctree (* TODO: replace by EmptyPtree*)
50 val existpt' : pos' -> ctree -> bool (* for interface.sml *)
51 val is_interpos : pos' -> bool (* for interface.sml *)
52 val lev_pred' : ctree -> pos' -> pos' (* for interface.sml *)
53 val ins_chn : ctree list -> ctree -> pos -> ctree (* for solve.sml *)
54 val children : ctree -> ctree list (* for solve.sml *)
55 val get_nd : ctree -> pos -> ctree (* for solve.sml *)
56 val just_created_ : ppobj -> bool (* for mathengine.sml *)
57 val just_created : state -> bool (* for mathengine.sml *)
58 val e_origin : Model.ori list * Celem.spec * term (* for mathengine.sml *)
60 val is_pblobj : ppobj -> bool
61 val is_pblobj' : ctree -> pos -> bool
62 val is_pblnd : ctree -> bool
64 val g_spec : ppobj -> Celem.spec
65 val g_loc : ppobj -> (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option
66 val g_form : ppobj -> term
67 val g_pbl : ppobj -> Model.itm list
68 val g_met : ppobj -> Model.itm list
69 val g_metID : ppobj -> Celem.metID
70 val g_result : ppobj -> Selem.result
71 val g_tac : ppobj -> Tactic.input
72 val g_domID : ppobj -> Rule.domID (* for appl.sml TODO: replace by thyID *)
73 val g_env : ppobj -> (Istate_Def.T * Proof.context) option (* for appl.sml *)
75 val g_origin : ppobj -> Model.ori list * Celem.spec * term (* for script.sml *)
76 val get_loc : ctree -> pos' -> Istate_Def.T * Proof.context (* for script.sml *)
77 val get_istate : ctree -> pos' -> Istate_Def.T (* for script.sml *)
78 val get_ctxt : ctree -> pos' -> Proof.context
79 val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a
80 val get_curr_formula : state -> term
81 val get_assumptions_ : ctree -> pos' -> term list (* for appl.sml *)
83 val new_val : term -> Istate_Def.T -> Istate_Def.T
84 (* for calchead.sml *)
85 type cid = cellID list
86 type ocalhd = bool * pos_ * term * Model.itm list * (bool * term) list * Celem.spec
87 datatype ptform = Form of term | ModSpec of ocalhd
88 val get_somespec' : Celem.spec -> Celem.spec -> Celem.spec
89 exception PTREE of string;
91 val par_pbl_det : ctree -> pos -> bool * pos * Rule.rls (* for appl.sml *)
92 val rootthy : ctree -> theory (* for script.sml *)
93 (* ---- made visible ONLY for structure CTaccess : CALC_TREE_ACCESS --------------------------- *)
94 val appl_obj : (ppobj -> ppobj) -> ctree -> pos -> ctree
95 val existpt : pos -> ctree -> bool (* also for tests *)
96 val cut_tree : ctree -> pos * 'a -> ctree * pos' list (* also for tests *)
97 val insert_pt : ppobj -> ctree -> int list -> ctree
98 (* ---- made visible ONLY for structure CTnavi : CALC_TREE_NAVIGATION ------------------------- *)
99 val g_branch : ppobj -> branch
100 val g_form' : ctree -> term
101 val g_ostate : ppobj -> ostate
102 val g_ostate' : ctree -> ostate
103 val g_res : ppobj -> term
104 val g_res' : ctree -> term
105 (*/---- duplicates in CTnavi, reconsider structs -----------------------------------------------
106 val lev_on : CTbasic.pos -> CTbasic.pos (* duplicate in ctree-navi.sml *)
107 val lev_dn : CTbasic.pos -> CTbasic.pos (* duplicate in ctree-navi.sml *)
108 val par_pblobj : CTbasic.ctree -> CTbasic.pos -> CTbasic.pos (* duplicate in ctree-navi.sml *)
109 ---- duplicates in CTnavi, reconsider structs ----------------------------------------------/*)
111 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
112 val pr_ctree : (pos -> ppobj -> string) -> ctree -> string
113 val pr_short : pos -> ppobj -> string
114 val g_ctxt : ppobj -> Proof.context
115 val g_fmz : ppobj -> Selem.fmz
116 val get_allp : pos' list -> pos * (int list * pos_) -> ctree -> pos' list
117 val get_allps : (pos * pos_) list -> Pos.posel list -> ctree list -> pos' list
118 val get_allpos' : pos * Pos.posel -> ctree -> pos' list
119 val get_allpos's : pos * Pos.posel -> ctree list -> (pos * pos_) list
120 val cut_bottom : pos * Pos.posel -> ctree -> (ctree * pos' list) * bool
121 val cut_level : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
122 val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
123 val get_trace : ctree -> int list -> int list -> int list list
124 val branch2str : branch -> string
125 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
127 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
132 structure CTbasic(**): BASIC_CALC_TREE(**) =
138 NoBranch | AndB | OrB
139 | TransitiveB (* FIXXXME.0308: set branch from met in Apply_Method
140 FIXXXME.0402: -"- in Begin_Trans'*)
141 | SequenceB | IntersectB | CollectB | MapB;
143 fun branch2str NoBranch = "NoBranch" (* for tests only *)
144 | branch2str AndB = "AndB"
145 | branch2str OrB = "OrB"
146 | branch2str TransitiveB = "TransitiveB"
147 | branch2str SequenceB = "SequenceB"
148 | branch2str IntersectB = "IntersectB"
149 | branch2str CollectB = "CollectB"
150 | branch2str MapB = "MapB";
153 Incomplete | Complete | Inconsistent (* WN041020 latter still unused *);
154 fun ostate2str Incomplete = "Incomplete" (* for tests only *)
155 | ostate2str Complete = "Complete"
156 | ostate2str Inconsistent = "Inconsistent";
159 type cid = cellID list;
162 type iist = Istate_Def.T option * Istate_Def.T option;
163 (*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*)
166 fun new_val v (Istate_Def.Pstate pst) =
167 (Istate_Def.Pstate (Istate_Def.set_act v pst))
168 | new_val _ _ = error "new_val: only for Pstate";
170 datatype con = land | lor;
172 (* executed tactics (tac_s) with local environment etc.;
173 used for continuing eval script + for generate *)
175 (TermC.path *(* of tactic in scr, tactic (weakly) associated with tac_ *)
176 (Tactic.T * (* (for generate) *)
177 Env.T * (* with 'tactic=result' as rule, tactic ev. _not_ ready for 'parallel let' *)
178 Env.T * (* with results of (ready) tacs *)
179 term * (* itr_arg of tactic, for upd. env at Repeat, Try *)
180 term * (* result value of the tac *)
184 fun ets2s (l,(m,eno,env,iar,res,s)) =
185 "\n(" ^ TermC.path2str l ^ ",(" ^ Tactic.string_of m ^
186 ",\n ens= " ^ Env.subst2str eno ^
187 ",\n env= " ^ Env.subst2str env ^
188 ",\n iar= " ^ Rule.term2str iar ^
189 ",\n res= " ^ Rule.term2str res ^
190 ",\n " ^ Telem.safe2str s ^ "))";
191 fun ets2str (ets: ets) = (strs2str o (map ets2s)) ets; (* for tests only *)
193 type envp =(*9.5.03: unused, delete with field in ctree.PblObj FIXXXME*)
194 (int * term list) list * (* assoc-list: args of met*)
195 (int * Rule.rls) list * (* assoc-list: tacs already done ///15.9.00*)
196 (int * ets) list * (* assoc-list: tacs etc. already done*)
197 (string * pos) list; (* asms * from where*)
199 datatype ppobj = (* TODO: arrange according to signature *)
201 {cell : TermC.lrd option, (* where in form tac has been applied, FIXME.WN0607 rename field *)
202 form : term, (* where tac is applied to *)
203 tac : Tactic.input, (* also in istate *)
204 loc : (Istate_Def.T * (* script interpreter state *)
205 Proof.context) (* context for provers, type inference *)
206 option * (* both for interpreter location on Frm, Pbl, Met *)
207 (Istate_Def.T * (* script interpreter state *)
208 Proof.context) (* context for provers, type inference *)
209 option, (* both for interpreter location on Res *)
210 (*(NONE,NONE) <==> e_istate ! see update_loc, get_loc *)
211 branch: branch, (* only rudimentary *)
212 result: Selem.result, (* result and assumptions *)
213 ostate: ostate} (* Complete <=> result is OK *)
215 {cell : TermC.lrd option, (* unused: meaningful only for some _Prf_Obj *)
216 fmz : Selem.fmz, (* from init:FIXME never use this spec;-drop *)
217 origin: (Model.ori list) *(* representation from fmz+pbt+met
218 for efficiently adding items in probl, meth *)
219 Celem.spec * (* updated by Refine_Tacitly *)
220 term, (* headline of calc-head, as calculated initially(!) *)
221 spec : Celem.spec, (* explicitly input *)
222 probl : Model.itm list, (* itms explicitly input *)
223 meth : Model.itm list, (* itms automatically added to copy of probl *)
224 ctxt : Proof.context, (* WN110513 introduced to avoid [*] [**] *)
225 env : (Istate_Def.T * Proof.context) option, (* istate only for initac in script
226 context for specify phase on this node NO..
227 ..NO: this conflicts with init_form/initac: see Apply_Method without init_form *)
228 loc : (Istate_Def.T * Proof.context) option * (Istate_Def.T * (* like PrfObj *)
229 Proof.context) option, (* for spec-phase [*], NO..
230 ..NO: raises errors not tracable on WN110513 [**] *)
231 branch: branch, (* like PrfObj *)
232 result: Selem.result, (* like PrfObj *)
233 ostate: ostate}; (* like PrfObj *)
235 (* this tree contains isac's calculations;
236 the tree's structure has been copied from an early version of Theorema(c);
237 it has the disadvantage, that there is no space
238 for the first tactic in a script generating the first formula at (p,Frm);
239 this trouble has been covered by 'init_form' and 'Take' so far,
240 but it is crucial if the first tactic in a script is eg. 'Subproblem';
241 see 'type tac', Apply_Method.
245 | Nd of ppobj * (ctree list);
246 val e_ctree = EmptyPtree;
247 type state = ctree * pos'
249 fun is_pblobj (PblObj _) = true
250 | is_pblobj _ = false;
252 exception PTREE of string;
253 fun nth _ [] = raise PTREE "nth _ []"
255 | nth n (_ :: xs) = nth (n - 1) xs;
256 (*> nth 2 [11,22,33]; -->> val it = 22 : int*)
259 (** convert ctree to a string **)
261 (* convert a pos from list to string *)
262 fun pr_pos ps = (space_implode "." (map string_of_int ps))^". ";
263 (* show hd origin or form only *)
264 fun pr_short p (PblObj _) = pr_pos p ^ " ----- pblobj -----\n" (* for tests only *)
265 | pr_short p (PrfObj {form = form, ...}) = pr_pos p ^ Rule.term2str form ^ "\n";
266 fun pr_ctree f pt = (* for tests only *)
268 fun pr_pt _ _ EmptyPtree = ""
269 | pr_pt pfn ps (Nd (b, [])) = pfn ps b
270 | pr_pt pfn ps (Nd (b, ts)) = pfn ps b ^ prts pfn ps 1 ts
271 and prts _ _ _ [] = ""
272 | prts pfn ps p (t :: ts) = (pr_pt pfn (ps @ [p]) t)^
273 (prts pfn ps (p + 1) ts)
274 in pr_pt f [] pt end;
276 (** access the branches of ctree **)
278 fun repl [] _ _ = raise PTREE "repl [] _ _"
279 | repl (_ :: ls) 1 e = e :: ls
280 | repl (l :: ls) n e = l :: (repl ls (n-1) e);
281 fun repl_app ls n e =
283 val lim = 1 + length ls
286 then raise PTREE "repl_app: n > lim"
289 else repl ls n e end;
291 (* get from obj at pos by f : ppobj -> 'a *)
292 fun get_obj _ EmptyPtree _ = raise PTREE "get_obj f EmptyPtree"
293 | get_obj f (Nd (b, _)) [] = f b
294 | get_obj f (Nd (_, bs)) (p :: ps) =
297 handle _ => raise PTREE ("get_obj: pos = " ^ ints2str' (p::ps) ^ " does not exist");
299 (get_obj f (nth p bs) ps)
300 handle _ => raise PTREE ("get_obj: pos = " ^ ints2str' (p::ps) ^ " does not exist")
302 fun get_nd EmptyPtree _ = raise PTREE "get_nd EmptyPtree"
304 | get_nd (Nd (_, nds)) (pos as p :: ps) = (get_nd (nth p nds) ps)
305 handle _ => raise PTREE ("get_nd: not existent pos = " ^ ints2str' pos);
307 (* for use by get_obj *)
308 fun g_form (PrfObj {form = f,...}) = f
309 | g_form (PblObj {origin= (_,_,f),...}) = f;
310 fun g_form' (Nd (PrfObj {form = f, ...}, _)) = f
311 | g_form' (Nd (PblObj {origin= (_, _, f),...}, _)) = f
312 | g_form' _ = error "g_form': uncovered fun def.";
313 (* | g_form _ = raise PTREE "g_form not for PblObj";*)
314 fun g_origin (PblObj {origin = ori, ...}) = ori
315 | g_origin _ = raise PTREE "g_origin not for PrfObj";
316 fun g_fmz (PblObj {fmz = f, ...}) = f (* for tests only *)
317 | g_fmz _ = raise PTREE "g_fmz not for PrfObj";
318 fun g_spec (PblObj {spec = s, ...}) = s
319 | g_spec _ = raise PTREE "g_spec not for PrfObj";
320 fun g_pbl (PblObj {probl = p, ...}) = p
321 | g_pbl _ = raise PTREE "g_pbl not for PrfObj";
322 fun g_met (PblObj {meth = p, ...}) = p
323 | g_met _ = raise PTREE "g_met not for PrfObj";
324 fun g_domID (PblObj {spec = (d, _, _), ...}) = d
325 | g_domID _ = raise PTREE "g_metID not for PrfObj";
326 fun g_metID (PblObj {spec = (_, _, m), ...}) = m
327 | g_metID _ = raise PTREE "g_metID not for PrfObj";
328 fun g_ctxt (PblObj {ctxt, ...}) = ctxt
329 | g_ctxt _ = raise PTREE "g_ctxt not for PrfObj";
330 fun g_env (PblObj {env, ...}) = env
331 | g_env _ = raise PTREE "g_env not for PrfObj";
332 fun g_loc (PblObj {loc = l, ...}) = l
333 | g_loc (PrfObj {loc = l, ...}) = l;
334 fun g_branch (PblObj {branch = b, ...}) = b
335 | g_branch (PrfObj {branch = b, ...}) = b;
336 fun g_tac (PblObj {spec = (_, _, m),...}) = Tactic.Apply_Method m
337 | g_tac (PrfObj {tac = m, ...}) = m;
338 fun g_result (PblObj {result = r, ...}) = r
339 | g_result (PrfObj {result = r, ...}) = r;
340 fun g_res (PblObj {result = (r, _) ,...}) = r
341 | g_res (PrfObj {result = (r, _),...}) = r;
342 fun g_res' (Nd (PblObj {result = (r, _), ...}, _)) = r
343 | g_res' (Nd (PrfObj {result = (r, _),...}, _)) = r
344 | g_res' _ = raise PTREE "g_res': uncovered fun def.";
345 fun g_ostate (PblObj {ostate = r, ...}) = r
346 | g_ostate (PrfObj {ostate = r, ...}) = r;
347 fun g_ostate' (Nd (PblObj {ostate = r, ...}, _)) = r
348 | g_ostate' (Nd (PrfObj {ostate = r, ...}, _)) = r
349 | g_ostate' _ = raise PTREE "g_ostate': uncovered fun def.";
351 (* get the formula preceeding the current position in a calculation *)
352 fun get_curr_formula (pt, (p, p_)) =
354 Frm => get_obj g_form pt p
355 | Res => (fst o (get_obj g_result pt)) p
356 | _ => #3 (get_obj g_origin pt p);
358 (* in CalcTree/Subproblem an 'just_created_' model is created;
359 this is filled to 'untouched' by Model/Refine_Problem *)
360 fun just_created_ (PblObj {meth, probl, spec, ...}) =
361 null meth andalso null probl andalso spec = Celem.e_spec
362 | just_created_ _ = raise PTREE "g_ostate': uncovered fun def.";
363 val e_origin = ([], Celem.e_spec, Rule.e_term);
365 fun just_created (pt, (p, _)) =
366 let val ppobj = get_obj I pt p
367 in is_pblobj ppobj andalso just_created_ ppobj end;
369 (* does the pos in the ctree exist ? *)
370 fun existpt pos pt = can (get_obj I pt) pos;
371 (* does the pos' in the ctree exist, ie. extra check for result in the node *)
372 fun existpt' (p, p_) pt =
373 if can (get_obj I pt) p
375 Res => get_obj g_ostate pt p = Complete
379 (* is this position appropriate for calculating intermediate steps? *)
380 fun is_interpos (_, Res) = true
381 | is_interpos _ = false;
383 (* get the children of a node in ctree *)
384 fun children (Nd (PblObj _, cn)) = cn
385 | children (Nd (PrfObj _, cn)) = cn
386 | children _ = error "children: uncovered fun def.";
388 (*/--------------- duplicates in ctree-navi.sml: required also here below ---------------\*)
389 fun lev_on [] = raise PTREE "lev_on []"
391 let val len = length pos
392 in (drop_last pos) @ [(nth len pos)+1] end;
393 fun lev_up [] = raise PTREE "lev_up []"
394 | lev_up p = (drop_last p):pos;
395 (* find the position of the next parent which is a PblObj in ctree *)
396 fun par_pblobj _ [] = []
401 if is_pblobj (get_obj I pt p)
403 else par pt (lev_up p)
404 in par pt (lev_up p) end;
405 (*\--------------- duplicates in ctree-navi.sml: required also here below ---------------/*)
407 (* find the next parent, which is either a PblObj (return true)
408 or a PrfObj with tac = Detail_Set (return false)
409 FIXME.030403: re-organize par_pbl_det after rls' --> rls*)
410 fun par_pbl_det pt [] = (true, [], Rule.Erls)
413 fun par _ [] = (true, [], Rule.Erls)
415 if is_pblobj (get_obj I pt p)
416 then (true, p, Rule.Erls)
417 else case get_obj g_tac pt p of
418 Tactic.Rewrite_Set rls' => (false, p, assoc_rls rls')
419 | Tactic.Rewrite_Set_Inst (_, rls') => (false, p, assoc_rls rls')
420 | _ => par pt (lev_up p)
421 in par pt (lev_up p) end;
423 (* insert obj b into ctree at pos, ev.overwriting this pos *)
424 fun insert_pt b EmptyPtree [] = Nd (b, [])
425 | insert_pt _ EmptyPtree _ = raise PTREE "insert_pt b Empty _"
426 | insert_pt _ (Nd ( _, _)) [] = raise PTREE "insert_pt b _ []"
427 | insert_pt b (Nd (b', bs)) (p :: []) = Nd (b', repl_app bs p (Nd (b, [])))
428 | insert_pt b (Nd (b', bs)) (p :: ps) = Nd (b', repl_app bs p (insert_pt b (nth p bs) ps));
430 (* insert children to a node without children. compare: fun insert_pt *)
431 fun ins_chn _ EmptyPtree _ = raise PTREE "ins_chn: EmptyPtree"
432 | ins_chn _ (Nd _) [] = raise PTREE "ins_chn: pos = []"
433 | ins_chn ns (Nd (b, bs)) (p :: []) =
435 then raise PTREE "ins_chn: pos not existent"
438 val (b', bs') = case nth p bs of
439 Nd (b', bs') => (b', bs')
440 | _ => error "ins_chn: uncovered case nth"
443 then Nd (b, repl_app bs p (Nd (b', ns)))
444 else raise PTREE "ins_chn: pos mustNOT be overwritten"
446 | ins_chn ns (Nd (b, bs)) (p::ps) = Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps));
448 (* apply f to obj at pos, f: ppobj -> ppobj *)
449 fun appl_to_node f (Nd (b, bs)) = Nd (f b, bs)
450 | appl_to_node _ _ = error "appl_to_node: uncovered fun def.";
451 fun appl_obj _ EmptyPtree [] = EmptyPtree
452 | appl_obj _ EmptyPtree _ = raise PTREE "appl_obj f Empty _"
453 | appl_obj f (Nd (b, bs)) [] = Nd (f b, bs)
454 | appl_obj f (Nd (b, bs)) (p :: []) = Nd (b, repl_app bs p (((appl_to_node f) o (nth p)) bs))
455 | appl_obj f (Nd (b, bs)) (p :: ps) = Nd (b, repl_app bs p (appl_obj f (nth p bs) (ps:pos)));
459 bool * (* ALL itms+preconds true *)
460 pos_ * (* model belongs to Problem | Method *)
461 term * (* header: Problem... or Cas FIXME.0312: item for marking syntaxerrors *)
462 Model.itm list * (* model: given, find, relate *)
463 ((bool * term) list) *(* model: preconds *)
464 Celem.spec; (* specification *)
465 val e_ocalhd = (false, Und, Rule.e_term, [Model.e_itm], [(false, Rule.e_term)], Celem.e_spec);
467 datatype ptform = Form of term | ModSpec of ocalhd;
469 (* for cut_level; (deprecated) *)
470 fun test_trans (PrfObj {branch, ...}) = true andalso branch = TransitiveB
471 | test_trans (PblObj {branch, ...}) = true andalso branch = TransitiveB;
473 fun is_pblobj' pt p =
474 let val ppobj = get_obj I pt p
475 in is_pblobj ppobj end;
477 fun del_res (PblObj {cell, fmz, origin, spec, probl, meth, ctxt, env, loc= (l1, _), branch, ...}) =
478 PblObj {cell = cell, fmz = fmz, origin = origin, spec = spec, probl = probl, meth = meth,
479 ctxt = ctxt, env = env, loc= (l1, NONE), branch = branch,
480 result = (Rule.e_term, []), ostate = Incomplete}
481 | del_res (PrfObj {cell, form, tac, loc= (l1, _), branch, ...}) =
482 PrfObj {cell = cell, form = form, tac = tac, loc = (l1, NONE), branch = branch,
483 result = (Rule.e_term, []), ostate = Incomplete};
486 fun get_loc EmptyPtree _ = (Istate_Def.e_istate, ContextC.e_ctxt)
487 | get_loc pt (p, Res) =
488 (case get_obj g_loc pt p of
490 | (NONE , NONE) => (Istate_Def.e_istate, ContextC.e_ctxt)
492 | get_loc pt (p, _) =
493 (case get_obj g_loc pt p of
494 (NONE , SOME i) => i (*13.8.02 just copied from ^^^: too liberal ?*)
495 | (NONE , NONE) => (Istate_Def.e_istate, ContextC.e_ctxt)
497 fun get_istate pt p = get_loc pt p |> #1;
498 fun get_ctxt pt (pos as (p, p_)) =
499 if member op = [Frm, Res] p_
500 then get_loc pt pos |> #2 (*for script interpretation rely on fun get_loc*)
501 else get_obj g_ctxt pt p (*for specify phase take ctx from PblObj*)
503 fun get_assumptions_ pt p = get_ctxt pt p |> ContextC.get_assumptions;
505 fun get_somespec' (dI, pI, mI) (dI', pI', mI') =
507 val domID = if dI = Rule.e_domID then dI' else dI
508 val pblID = if pI = Celem.e_pblID then pI' else pI
509 val metID = if mI = Celem.e_metID then mI' else mI
510 in (domID, pblID, metID) end;
512 (**.development for extracting an 'interval' from ptree.**)
514 (*WN0510 version stopped in favour of get_interval with !!!move_dn, getFormulaeFromTo
515 actually used (inefficient) version with move_dn: see modspec.sml*)
518 fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*)
519 fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)
520 fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x;
521 fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
523 fun getnd i (b,p) q (Nd (po, nds)) =
524 (if i <= 0 then [[b]] else []) @
525 (getnds (i-1) true (b@[hdp p], tlp p) (tlq q)
526 (take_fromto (hdp p) (hdq q) nds))
528 and getnds _ _ _ _ [] = [] (*no children*)
529 | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)
531 | getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*)
532 (getnd i ( b, p ) [99999] n1) @
533 (getnd ~99999 (lev_on b,[0]) q n2)
535 | getnds i _ (b,p) q [n1, n2] = (*intern, r-margin*)
536 (getnd i ( b,[0]) [99999] n1) @
537 (getnd ~99999 (lev_on b,[0]) q n2)
539 | getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*)
540 (getnd i ( b, p ) [99999] nd) @
541 (getnds ~99999 false (lev_on b,[0]) q nds)
543 | getnds i _ (b,p) q (nd::(nds as _::_)) = (*intern, ...*)
544 (getnd i ( b,[0]) [99999] nd) @
545 (getnds ~99999 false (lev_on b,[0]) q nds);
547 (*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes
548 where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
549 (1) the 'f' are given
550 (1a) by 'from' if 'f' = the respective element of 'from' (left margin)
551 (1b) -inifinity, if 'f' > the respective element of 'from' (internal node)
553 (2a) by 'to' if 't' = the respective element of 'to' (right margin)
554 (2b) inifinity, if 't' < the respective element of 'to (internal node)'
555 the 'f' and 't' are set by hdp,... *)
556 fun get_trace pt p q =
557 (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q)))
558 (take_fromto (hdp p) (hdq q) (children pt));
561 (*extract a formula or model from ctree for itms2itemppc or model2xml*)
562 fun preconds2str bts =
563 (strs2str o (map (Celem.linefeed o pair2str o
564 (apsnd Rule.term2str) o
565 (apfst bool2str)))) bts;
566 fun ocalhd2str (b, p, hdf, itms, prec, spec) = (* for tests only *)
567 "(" ^ bool2str b ^ ", " ^ pos_2str p ^ ", " ^ Rule.term2str hdf ^
568 ", " ^ Model.itms2str_ (Rule.thy2ctxt' "Isac_Knowledge") itms ^
569 ", " ^ preconds2str prec ^ ", \n" ^ Celem.spec2str spec ^ " )";
571 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj
572 | is_pblnd _ = error "is_pblnd: uncovered fun def.";
575 (* determine the previous pos' on the same level
576 WN0502 made for interSteps; _only_ works for branch TransitiveB WN120517 compare lev_back *)
577 fun lev_pred' _ ([], Res) = ([], Pbl)
578 | lev_pred' pt (p, Res) =
579 let val (p', last) = split_last p
582 then if (is_pblobj o (get_obj I pt)) p then (p, Pbl) else (p, Frm)
583 else if get_obj g_res pt (p' @ [last - 1]) = get_obj g_form pt p
584 then (p' @ [last - 1], Res) (* TransitiveB *)
585 else if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm)
587 | lev_pred' _ _ = error "";
590 (**.insert into ctree and cut branches accordingly.**)
592 (* get all positions of certain intervals on the ctree.
593 old VERSION without move_dn; kept for occasional redesign
594 get all pos's to be cut in a ctree
595 below a pos or from a ctree list after i-th element (NO level_up) *)
596 fun get_allpos' (_, _) EmptyPtree = []
597 | get_allpos' (p, 1) (Nd (b, bs)) = (* p is pos of Nd *)
598 if g_ostate b = Incomplete
599 then (p, Frm) :: (get_allpos's (p, 1) bs)
600 else (p, Frm) :: (get_allpos's (p, 1) bs) @ [(p, Res)]
601 | get_allpos' (p, i) (Nd (b, bs)) = (* p is pos of Nd *)
602 if length bs > 0 orelse is_pblobj b
603 then if g_ostate b = Incomplete
604 then [(p,Frm)] @ (get_allpos's (p, 1) bs)
605 else [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p, Res)]
606 else if g_ostate b = Incomplete then [] else [(p, Res)]
607 and get_allpos's _ [] = []
608 | get_allpos's (p, i) (pt :: pts) = (* p is pos of parent-Nd *)
609 (get_allpos' (p @ [i], i) pt) @ (get_allpos's (p, i + 1) pts);
611 (*WN050106 like cut_level, but deletes exactly 1 node *)
612 fun cut_level_'_ _ _ EmptyPtree _ =raise PTREE "cut_level_'_ Empty _" (* for tests ONLY *)
613 | cut_level_'_ _ _ (Nd ( _, _)) ([], _) = raise PTREE "cut_level_'_ _ []"
614 | cut_level_'_ cuts P (Nd (b, bs)) (p :: [], p_) =
617 (Nd (b, drop_nth [] (p:Pos.posel, bs)),
618 cuts @ (if p_ = Frm then [(P @ [p], Res)] else []) @
619 (get_allpos's (P, p + 1) (drop_nth [] (p, bs))))
620 else (Nd (b, bs), cuts)
621 | cut_level_'_ cuts P (Nd (b, bs)) ((p :: ps), p_) =
623 val (bs', cuts') = cut_level_'_ cuts P (nth p bs) (ps, p_)
624 in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
626 fun cut_level _ _ EmptyPtree _ = raise PTREE "cut_level EmptyPtree _"
627 | cut_level _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level _ []"
628 | cut_level cuts P (Nd (b, bs)) (p :: [], p_) =
631 (Nd (b, take (p:Pos.posel, bs)),
633 (if p_ = Frm andalso (*#*) g_ostate b = Complete then [(P@[p],Res)] else ([]:pos' list)) @
634 (get_allpos's (P, p+1) (takerest (p, bs))))
635 else (Nd (b, bs), cuts)
636 | cut_level cuts P (Nd (b, bs)) ((p :: ps), p_) =
638 val (bs', cuts') = cut_level cuts P (nth p bs) (ps, p_)
639 in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
641 (*old version before WN050219, overwritten below*)
642 fun cut_tree _ ([], _) = raise PTREE "cut_tree _ ([],_)" (* for test only *)
643 | cut_tree pt (pos as ([_], _)) =
645 val (pt', cuts) = cut_level [] [] pt pos
647 (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete then [] else [([], Res)]))
649 | cut_tree pt (p,p_) =
651 fun cutfn pt cuts (p, p_) =
653 val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_)
655 if length cuts' > 0 andalso length p > 1
656 then cutfn pt' (cuts @ cuts') (lev_up p, Frm(*-->(p,Res)*))
657 else (pt', cuts @ cuts')
659 val (pt', cuts) = cutfn pt [] (p, p_)
661 (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete then [] else [([], Res)]))
665 fun move_dn _ (Nd (_, ns)) ([],p_) = (* root problem *)
667 Res => raise PTREE "move_dn: end of calculation"
669 if null ns (* go down from Pbl + Met *)
670 then raise PTREE "move_dn: solve problem not started"
672 | move_dn P (Nd (_, ns)) (p :: (ps as (_ :: _)), p_) = (* iterate to end of pos *)
674 then raise PTREE "move_dn: pos not existent 2"
675 else move_dn (P @ [p]) (nth p ns) (ps, p_)
676 | move_dn P (Nd (c, ns)) ([p], p_) = (* act on last element of pos *)
678 then raise PTREE "move_dn: pos not existent 3"
682 if p = length ns (* last Res on this level: go a level up *)
683 then if g_ostate c = Complete
685 else raise PTREE (ints2str' P ^ " not complete 1")
686 else (* go to the next Nd on this level, or down into the next Nd *)
687 if is_pblnd (nth (p + 1) ns) then (P@[p + 1], Pbl)
688 else if g_res' (nth p ns) = g_form' (nth (p + 1) ns)
689 then if (null o children o (nth (p + 1))) ns
690 then (* take the Res if Complete *)
691 if g_ostate' (nth (p + 1) ns) = Complete
692 then (P@[p + 1], Res)
693 else raise PTREE (ints2str' (P@[p + 1]) ^ " not complete 2")
694 else (P@[p + 1, 1], Frm) (* go down into the next PrfObj *)
695 else (P@[p + 1], Frm) (* take Frm: exists if the Nd exists *)
696 | Frm => (*go down or to the Res of this Nd*)
697 if (null o children o (nth p)) ns
698 then if g_ostate' (nth p ns) = Complete then (P @ [p], Res)
699 else raise PTREE (ints2str' (P @ [p])^" not complete 3")
700 else (P @ [p, 1], Frm)
701 | _ => (* is Pbl or Met *)
702 if (null o children o (nth p)) ns
703 then raise PTREE "move_dn:solve subproblem not startd"
705 if (is_pblnd o hd o children o (nth p)) ns
707 | move_dn _ _ _ = error "";
709 (* get all positions in a ctree until ([],Res) or ostate=Incomplete
711 pos' list -> : accumulated, start with []
712 pos -> : the offset for subtrees wrt the root
714 pos' : initialization (the last pos' before ...)
715 -> pos' list : of positions in this (sub) tree (relative to the root)
717 fun get_allp cuts (P, pos) pt =
719 val nxt = move_dn [] pt pos (*exn if Incomplete reached*)
722 then get_allp (cuts @ [nxt]) (P, nxt) pt
723 else map (apfst (curry op @ P)) (cuts @ [nxt])
725 handle PTREE _ => (map (apfst (curry op@ P)) cuts);
728 (* the pts are assumed to be on the same level *)
729 fun get_allps cuts _ [] = cuts
730 | get_allps cuts P (pt :: pts) =
732 val below = get_allp [] (P, ([], Frm)) pt
735 then (P, Pbl) :: below
736 else if last_elem P = 1
737 then (P, Frm) :: below
739 val levres = levfrm @ (if null below then [(P, Res)] else [])
741 get_allps (cuts @ levres) (lev_on P) pts
744 (** these 2 funs decide on how far cut_tree goes **)
745 (* shall the nodes _after_ the pos to be inserted at be deleted?
746 shall cutting be continued on the higher level(s)? the Nd regarded will NOT be changed *)
747 fun test_trans (PrfObj {branch, ...}) = (branch = TransitiveB orelse branch = NoBranch)
748 | test_trans (PblObj {branch, ...}) = (branch = TransitiveB orelse branch = NoBranch);
750 (* cut_bottom new sml603..608
751 cut the level at the bottom of the pos (used by cappend_...)
752 and handle the parent in order to avoid extra case for root
753 fn: ctree -> : the _whole_ ctree for cut_levup
754 pos * Pos.posel -> : the pos after split_last
755 ctree -> : the parent of the Nd to be cut
757 (ctree * : the updated ctree
758 pos' list) * : the pos's cut
759 bool : cutting shall be continued on the higher level(s)
761 fun cut_bottom _ (pt' as Nd (b, [])) = ((pt', []), test_trans b)
762 | cut_bottom (P, p) (Nd (b, bs)) =
763 let (*divide level into 3 parts...*)
764 val keep = take (p - 1, bs)
765 val pt' = case nth p bs of
767 | _ => error "cut_bottom: uncovered case nth p bs"
768 (*^^^^^_here_ will be 'insert_pt'ed by 'append_..'*)
769 val (tail, _) = (takerest (p, bs), if null (takerest (p, bs)) then 0 else p + 1)
770 val (children, cuts) =
773 (keep, (if is_pblnd pt' then [(P @ [p], Pbl)] else [])
774 @ (get_allp [] (P @ [p], (P, Frm)) pt')
775 @ (get_allps [] (P @ [p + 1]) tail))
776 else (keep @ [(*'insert_pt'ed by 'append_..'*)] @ tail,
777 get_allp [] (P @ [p], (P, Frm)) pt')
780 then (Nd (del_res b, children), cuts @ (if g_ostate b = Incomplete then [] else [(P, Res)]))
781 else (Nd (b, children), cuts)
782 in ((pt'', cuts), test_trans b) end
783 | cut_bottom _ _ = error "cut_bottom: uncovered fun def.";
786 (* go all levels from the bottom of 'pos' up to the root,
787 on each level compose the children of a node and accumulate the cut Nds
789 pos' list -> : for accumulation
790 bool -> : cutting shall be continued on the higher level(s)
791 ctree -> : the whole ctree for 'get_nd pt P' on each level
792 ctree -> : the Nd from the lower level for insertion at path
793 pos * Pos.posel -> : pos=path split for convenience
794 ctree -> : Nd the children of are under consideration on this call
796 ctree * pos' list : the updated parent-Nd and the pos's of the Nds cut
798 fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:Pos.posel) (Nd (b, bs)) =
799 let (*divide level into 3 parts...*)
800 val keep = take (p - 1, bs)
801 (*val pt' comes as argument from below*)
803 (takerest (p, bs), if null (takerest (p, bs)) then 0 else p + 1)
804 val (children, cuts') =
806 then (keep @ [pt'], get_allps [] (P @ [p+1]) tail)
807 else (keep @ [pt'] @ tail, [])
808 val clevup' = if clevup then test_trans b else false
809 (*the first Nd with false stops cutting on all levels above*)
812 then (Nd (del_res b, children), cuts' @ (if g_ostate b = Incomplete then [] else [(P, Res)]))
813 else (Nd (b, children), cuts')
816 then (pt'', cuts @ cuts')
818 let val (P, p) = split_last P
819 in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P) end
821 | cut_levup _ _ _ _ _ _ = error "cut_levup: uncovered fun def.";
823 (* cut nodes after and below an inserted node in the ctree;
824 the cuts range is limited by the predicate 'fun cutlevup' *)
825 fun cut_tree pt (pos, _) =
826 if not (existpt pos pt)
827 then (pt,[]) (*appending a formula never cuts anything*)
830 val (P, p) = split_last pos
831 val ((pt', cuts), clevup) = cut_bottom (P, p) (get_nd pt P)
832 (* pt' is the updated parent of the Nd to cappend_..*)
837 let val (P, p) = split_last P
838 in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P) end
841 (* get the theory explicitly specified for the rootpbl;
842 thus use this function _after_ finishing specification *)
843 fun rootthy (Nd (PblObj {spec = (thyID, _, _), ...}, _)) = Celem.assoc_thy thyID
844 | rootthy _ = error "rootthy: uncovered fun def.";