1 (* Title: the calctree, which holds a calculation
2 Author: Walther Neuper 1999
3 (c) due to copyright terms
6 signature BASIC_CALC_TREE =
7 sig (* vvv--- *.sml require these typs incrementally, with these exception -----------------vvv *)
8 (*===\<Longrightarrow> other ?mstools.sml? =================================================================*)
13 Add_Find' of cterm' * itm list | Add_Given' of cterm' * itm list | Add_Relation' of cterm' * itm list
14 | Apply_Assumption' of term list * term
15 | Apply_Method' of metID * term option * Selem.istate * Proof.context
17 | Begin_Sequ' | Begin_Trans' of term
18 | Split_And' of term | Split_Or' of term | Split_Intersect' of term
19 | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
20 | End_Sequ' | End_Trans' of Selem.result
21 | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''
24 | Calculate' of theory' * string * term * (term * thm')
25 | Check_Postcond' of pblID * Selem.result
26 | Check_elementwise' of term * cterm' * Selem.result
27 | Del_Find' of cterm' | Del_Given' of cterm' | Del_Relation' of cterm'
30 | Detail_Set' of theory' * bool * rls * term * Selem.result
31 | Detail_Set_Inst' of theory' * bool * subst * rls * term * Selem.result
32 | End_Detail' of Selem.result
37 | Init_Proof' of cterm' list * spec
38 | Model_Problem' of pblID * itm list * itm list
39 | Or_to_List' of term * term
40 | Refine_Problem' of pblID * (itm list * (bool * term) list)
41 | Refine_Tacitly' of pblID * pblID * domID * metID * itm list
43 | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * Selem.result
44 | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * Selem.result
45 | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * Selem.result
46 | Rewrite_Set' of theory' * bool * rls * term * Selem.result
47 | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * Selem.result
49 | Specify_Method' of metID * ori list * itm list
50 | Specify_Problem' of pblID * (bool * (itm list * (bool * term) list))
51 | Specify_Theory' of domID
52 | Subproblem' of spec * ori list * term * Selem.fmz_ * Proof.context * term
53 | Substitute' of rew_ord_ * rls * Selem.subte * term * term
54 | Tac_ of theory * string * string * string
55 | Take' of term | Take_Inst' of term
58 Add_Find of cterm' | Add_Given of cterm' | Add_Relation of cterm'
59 | Apply_Assumption of cterm' list
60 | Apply_Method of metID
61 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
62 | Begin_Sequ | Begin_Trans
63 | Split_And | Split_Or | Split_Intersect
64 | Conclude_And | Conclude_Or | Collect_Trues
65 | End_Sequ | End_Trans
66 | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
67 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
70 | Check_Postcond of pblID
71 | Check_elementwise of cterm'
72 | Del_Find of cterm' | Del_Given of cterm' | Del_Relation of cterm'
76 | Detail_Set_Inst of Selem.subs * rls'
82 | Init_Proof of cterm' list * spec
85 | Refine_Problem of pblID
86 | Refine_Tacitly of pblID
89 | Rewrite_Asm of thm''
90 | Rewrite_Inst of Selem.subs * thm''
92 | Rewrite_Set_Inst of Selem.subs * rls'
94 | Specify_Method of metID
95 | Specify_Problem of pblID
96 | Specify_Theory of domID
97 | Subproblem of domID * pblID
99 | Substitute of Selem.sube
101 | Take of cterm' | Take_Inst of cterm'
103 val tac2str : tac -> string
104 val rls_of : tac -> rls' (* for solve.sml *)
105 val tac2IDstr : tac -> string
106 val is_rewset : tac -> bool (* for mathengine.sml *)
107 val is_rewtac : tac -> bool (* for interface.sml *)
110 type pos = posel list
111 val pos2str : int list -> string (* for datatypes.sml *)
112 datatype pos_ = Frm | Met | Pbl | Res | Und
113 val pos_2str : pos_ -> string
115 val pos'2str : pos' -> string
116 val str2pos_ : string -> pos_ (* for datatypes.sml *)
118 (* for generate.sml ?!? ca.*)
119 val tac_2str : tac_ -> string
122 datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB
123 datatype ostate = Complete | Incomplete | Inconsistent
128 loc: (Selem.istate * Proof.context) option * (Selem.istate * Proof.context) option,
130 result: Selem.result,
133 origin: ori list * spec * term,
138 env: (Selem.istate * Proof.context) option}
142 loc: (Selem.istate * Proof.context) option * (Selem.istate * Proof.context) option,
144 result: Selem.result,
149 datatype ctree = EmptyPtree | Nd of ppobj * ctree list
150 val e_ctree : ctree (* TODO: replace by EmptyPtree*)
151 val existpt' : pos' -> ctree -> bool (* for interface.sml *)
152 val is_interpos : pos' -> bool (* for interface.sml *)
153 val lev_pred' : ctree -> pos' -> pos' (* for interface.sml *)
154 val ins_chn : ctree list -> ctree -> pos -> ctree (* for solve.sml *)
155 val children : ctree -> ctree list (* for solve.sml *)
156 val get_nd : ctree -> pos -> ctree (* for solve.sml *)
157 val just_created_ : ppobj -> bool (* for mathengine.sml *)
158 val just_created : state -> bool (* for mathengine.sml *)
159 val e_origin : ori list * spec * term (* for mathengine.sml *)
161 val is_pblobj : ppobj -> bool
162 val is_pblobj' : ctree -> pos -> bool
163 val is_pblnd : ctree -> bool
165 val g_spec : ppobj -> spec
166 val g_loc : ppobj -> (Selem.istate * Proof.context) option * (Selem.istate * Proof.context) option
167 val g_form : ppobj -> term
168 val g_pbl : ppobj -> itm list
169 val g_met : ppobj -> itm list
170 val g_metID : ppobj -> metID
171 val g_result : ppobj -> Selem.result
172 val g_tac : ppobj -> tac
173 val g_domID : ppobj -> domID (* for appl.sml TODO: replace by thyID *)
174 val g_env : ppobj -> (Selem.istate * Proof.context) option (* for appl.sml *)
176 val g_origin : ppobj -> ori list * spec * term (* for script.sml *)
177 val get_loc : ctree -> pos' -> Selem.istate * Proof.context (* for script.sml *)
178 val get_istate : ctree -> pos' -> Selem.istate (* for script.sml *)
179 val get_ctxt : ctree -> pos' -> Proof.context
180 val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a
181 val get_curr_formula : state -> term
182 val get_assumptions_ : ctree -> pos' -> term list (* for appl.sml *)
184 val is_e_ctxt : Proof.context -> bool (* for appl.sml *)
185 val new_val : term -> Selem.istate -> Selem.istate
186 (* for calchead.sml *)
187 type cid = cellID list
188 type ocalhd = bool * pos_ * term * itm list * (bool * term) list * spec
189 datatype ptform = Form of term | ModSpec of ocalhd
190 val get_somespec' : spec -> spec -> spec
191 exception PTREE of string;
193 val par_pbl_det : ctree -> pos -> bool * pos * rls (* for appl.sml *)
194 val rule2tac : theory -> (term * term) list -> rule -> tac (* for rewtools.sml *)
195 val eq_tac : tac * tac -> bool (* for script.sml *)
196 val rootthy : ctree -> theory (* for script.sml *)
197 (* ---- made visible ONLY for structure CTaccess : CALC_TREE_ACCESS --------------------------- *)
198 val appl_obj : (ppobj -> ppobj) -> ctree -> pos -> ctree
199 val existpt : pos -> ctree -> bool (* also for tests *)
200 val is_empty_tac : tac -> bool (* also for tests *)
201 val cut_tree : ctree -> pos * 'a -> ctree * pos' list (* also for tests *)
202 val insert_pt : ppobj -> ctree -> int list -> ctree
203 (* ---- made visible ONLY for structure CTnavi : CALC_TREE_NAVIGATION ------------------------- *)
204 val g_branch : ppobj -> branch
205 val g_form' : ctree -> term
206 val g_ostate : ppobj -> ostate
207 val g_ostate' : ctree -> ostate
208 val g_res : ppobj -> term
209 val g_res' : ctree -> term
210 (*/---- duplicates in CTnavi, reconsider structs -----------------------------------------------
211 val lev_on : CTbasic.pos -> CTbasic.pos (* duplicate in ctree-navi.sml *)
212 val lev_dn : CTbasic.pos -> CTbasic.pos (* duplicate in ctree-navi.sml *)
213 val par_pblobj : CTbasic.ctree -> CTbasic.pos -> CTbasic.pos (* duplicate in ctree-navi.sml *)
214 ---- duplicates in CTnavi, reconsider structs ----------------------------------------------/*)
216 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
217 val pr_ctree : (pos -> ppobj -> string) -> ctree -> string
218 val pr_short : pos -> ppobj -> string
219 val g_ctxt : ppobj -> Proof.context
220 val g_fmz : ppobj -> Selem.fmz
221 val get_allp : pos' list -> pos * (int list * pos_) -> ctree -> pos' list
222 val get_allps : (pos * pos_) list -> posel list -> ctree list -> pos' list
223 val get_allpos' : pos * posel -> ctree -> pos' list
224 val get_allpos's : pos * posel -> ctree list -> (pos * pos_) list
225 val cut_bottom : pos * posel -> ctree -> (ctree * pos' list) * bool
226 val cut_level : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
227 val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
228 val get_trace : ctree -> int list -> int list -> int list list
229 val branch2str : branch -> string
230 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
235 sig exception PTREE of string val appl_obj : (ppobj -> ppobj) -> ctree -> pos -> ctree
236 val appl_to_node : (ppobj -> ppobj) -> ctree -> ctree
237 datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB
238 val branch2str : branch -> string eqtype cellID val children : ctree -> ctree list type cid = cellID list
239 datatype con = land | lor datatype ctree = EmptyPtree | Nd of ppobj * ctree list
240 val cut_bottom : int list * int -> ctree -> (ctree * (int list * pos_) list) * bool
242 (posel list * pos_) list -> posel list -> ctree -> int list * pos_ -> ctree * (posel list * pos_) list
244 (posel list * pos_) list -> posel list -> ctree -> int list * pos_ -> ctree * (posel list * pos_) list
245 val cut_levup : pos' list -> bool -> ctree -> ctree -> int list * int -> ctree -> ctree * pos' list
246 val cut_tree : ctree -> int list * 'a -> ctree * (int list * pos_) list val del_res : ppobj -> ppobj
247 val e_ctree : ctree val e_ctxt : Proof.context val e_fmz : 'a list * spec val e_istate : istate
248 val e_ocalhd : bool * pos_ * term * itm list * (bool * term) list * spec
249 val e_origin : 'a list * spec * term val e_pos' : 'a list * pos_ val e_sube : cterm' list
250 val e_subs : string list type env = (term * term) list
251 type envp = (int * term list) list * (int * rls) list * (int * ets) list * (string * pos) list
252 val eq_tac : tac * tac -> bool type ets = (loc_ * (tac_ * env * env * term * term * safe)) list
253 val ets2s : loc_ * (tac_ * subst * subst * term * term * safe) -> string val ets2str : ets -> string
254 val existpt : int list -> ctree -> bool val existpt' : int list * pos_ -> ctree -> bool
255 val g_branch : ppobj -> branch
256 val g_ctxt : ppobj -> Proof.context val g_domID : ppobj -> domID
257 val g_env : ppobj -> (istate * Proof.context) option val g_fmz : ppobj -> fmz val g_form : ppobj -> term
258 val g_loc : ppobj -> (istate * Proof.context) option * (istate * Proof.context) option
259 val g_met : ppobj -> itm list val g_metID : ppobj -> metID val g_origin : ppobj -> ori list * spec * term
260 val g_res : ppobj -> term val g_result : ppobj -> Selem.result
261 val g_spec : ppobj -> spec val g_tac : ppobj -> tac
262 val get_allp : (int list * pos_) list -> int list * (int list * pos_) -> ctree -> (int list * pos_) list
263 val get_allpos' : posel list * posel -> ctree -> (posel list * pos_) list
264 val get_allpos's : posel list * posel -> ctree list -> (posel list * pos_) list
265 val get_allps : (int list * pos_) list -> int list -> ctree list -> (int list * pos_) list
266 val get_assumptions_ : ctree -> int list * pos_ -> term list
267 val get_ctxt : ctree -> int list * pos_ -> Proof.context
268 val get_curr_formula : ctree * (int list * pos_) -> term
269 val get_istate : ctree -> int list * pos_ -> istate
270 val get_loc : ctree -> int list * pos_ -> istate * Proof.context val get_nd : ctree -> int list -> ctree
271 val get_obj : (ppobj -> 'a) -> ctree -> int list -> 'a
272 val get_somespec' : domID * pblID * metID -> domID * pblID * metID -> domID * pblID * metID
273 val get_trace : ctree -> int list -> int list -> int list list type iist = istate option * istate option
274 val ins_chn : ctree list -> ctree -> int list -> ctree
275 val insert_pt : ppobj -> ctree -> int list -> ctree val is_e_ctxt : Proof.context -> bool
276 val is_empty_tac : tac -> bool val is_interpos : 'a * pos_ -> bool val is_pblnd : ctree -> bool
277 val is_pblobj : ppobj -> bool val is_pblobj' : ctree -> int list -> bool val is_rewset : tac -> bool
278 val is_rewtac : tac -> bool datatype istate = RrlsState of rrlsstate | ScrState of scrstate | Uistate
279 val istate2str : istate -> string
280 val just_created : ctree * (int list * 'a) -> bool val just_created_ : ppobj -> bool
281 val lev_on : int list -> int list val lev_pred' : ctree -> int list * pos_ -> int list * pos_
282 val lev_up : int list -> pos val move_dn : int list -> ctree -> int list * pos_ -> int list * pos_
283 val move_up : int list -> ctree -> int list * pos_ -> int list * pos_
284 val movecalchd_up : ctree -> int list * pos_ -> int list * pos_
285 val movelevel_dn : int list -> ctree -> int list * pos_ -> int list * pos_
286 val movelevel_up : int list -> ctree -> int list * 'a -> int list * pos_
287 val new_val : term -> istate -> istate val nth : int -> 'a list -> 'a
288 type ocalhd = bool * pos_ * term * itm list * (bool * term) list * spec
290 bool * pos_ * term * itm list * (bool * term) list * (string * string list * string list) -> string
291 datatype ostate = Complete | Incomplete | Inconsistent val ostate2str : ostate -> string
292 val par_pbl_det : ctree -> int list -> bool * int list * rls
293 val par_pblobj : ctree -> int list -> int list type pos = int list type pos' = pos * pos_
294 val pos'2str : int list * pos_ -> string val pos's2str : (int list * pos_) list -> string
295 val pos2str : int list -> string datatype pos_ = Frm | Met | Pbl | Res | Und
296 val pos_2str : pos_ -> string eqtype posel
302 env: (istate * Proof.context) option,
304 loc: (istate * Proof.context) option * (istate * Proof.context) option,
306 origin: ori list * spec * term, ostate: ostate, probl: itm list, Selem.result: Selem.result, spec: spec}
311 loc: (istate * Proof.context) option * (istate * Proof.context) option,
312 ostate: ostate, Selem.result: Selem.result, tac: tac}
313 val pr_ctree : (int list -> ppobj -> string) -> ctree -> string val pr_pos : int list -> string
314 val pr_short : int list -> ppobj -> string val preconds2str : (bool * term) list -> string
315 datatype ptform = Form of term | ModSpec of ocalhd val repl : 'a list -> int -> 'a -> 'a list
316 val repl_app : 'a list -> int -> 'a -> 'a list
317 type result = term * term list val rls_of : tac -> rls' val rootthy : ctree -> theory
318 val rta2str : rule * (term * term list) -> string
319 val rule2tac : theory -> (term * term) list -> rule -> tac
320 datatype safe = Helpless | Safe | Selem.Sundef | Unsafe
321 val safe2str : safe -> string
322 type scrstate = env * loc_ * term option * term * safe * bool
323 type state = ctree * pos'
324 val str2pos_ : string -> pos_ type sube = cterm' list
325 val sube2subst : theory -> string list -> (term * term) list val sube2subte : string list -> term list
326 type subs = cterm' list val subs2subst : theory -> string list -> (term * term) list
327 val subst2sube : (term * term) list -> string list val subst2subs : (term * term) list -> string list
328 val subst2subs' : (term * term) list -> (string * string) list type subte = term list
329 val subte2sube : term list -> string list val subte2subst : term list -> (term * term) list
331 = Add_Find of cterm' | Add_Given of cterm' | Add_Relation of cterm' | Apply_Assumption of cterm' list
332 | Apply_Method of metID | Begin_Sequ | Begin_Trans | CAScmd of cterm' | Calculate of string
333 | Check_Postcond of pblID | Check_elementwise of cterm' | Collect_Trues | Conclude_And | Conclude_Or
334 | Del_Find of cterm' | Del_Given of cterm' | Del_Relation of cterm' | Derive of rls'
335 | Detail_Set of rls' | Detail_Set_Inst of subs * rls' | Empty_Tac | End_Detail | End_Intersect
336 | End_Proof' | End_Ruleset | End_Sequ | End_Subproblem | End_Trans | Free_Solve
337 | Init_Proof of cterm' list * spec | Model_Problem | Or_to_List | Refine_Problem of pblID
338 | Refine_Tacitly of pblID | Rewrite of thm'' | Rewrite_Asm of thm'' | Rewrite_Inst of subs * thm''
339 | Rewrite_Set of rls' | Rewrite_Set_Inst of subs * rls' | Specify_Method of metID
340 | Specify_Problem of pblID | Specify_Theory of domID | Split_And | Split_Intersect | Split_Or
341 | Subproblem of domID * pblID | Substitute of sube | Tac of string | Take of cterm'
342 | Take_Inst of cterm'
343 val tac2IDstr : tac -> string val tac2str : tac -> string
345 = Add_Find' of cterm' * itm list | Add_Given' of cterm' * itm list | Add_Relation' of cterm' * itm list
346 | Apply_Assumption' of term list * term
347 | Apply_Method' of metID * term option * istate * Proof.context | Begin_Sequ' | Begin_Trans' of term
348 | CAScmd' of term | Calculate' of theory' * string * term * (term * thm')
349 | Check_Postcond' of pblID * Selem.result | Check_elementwise' of term * string * Selem.result
350 | Collect_Trues' of term | Conclude_And' of term | Conclude_Or' of term | Del_Find' of cterm'
351 | Del_Given' of cterm' | Del_Relation' of cterm' | Derive' of rls
352 | Detail_Set' of theory' * bool * rls * term * Selem.result
353 | Detail_Set_Inst' of theory' * bool * subst * rls * term * Selem.result | Empty_Tac_
354 | End_Detail' of Selem.result | End_Intersect' of term | End_Proof'' | End_Ruleset' of term | End_Sequ'
355 | End_Subproblem' of term | End_Trans' of Selem.result | Free_Solve' | Init_Proof' of cterm' list * spec
356 | Model_Problem' of pblID * itm list * itm list | Or_to_List' of term * term
357 | Refine_Problem' of pblID * (itm list * (bool * term) list)
358 | Refine_Tacitly' of pblID * pblID * domID * metID * itm list
359 | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * Selem.result
360 | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * Selem.result
361 | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * Selem.result
362 | Rewrite_Set' of theory' * bool * rls * term * Selem.result
363 | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * Selem.result
364 | Specify_Method' of metID * ori list * itm list
365 | Specify_Problem' of pblID * (bool * (itm list * (bool * term) list)) | Specify_Theory' of domID
366 | Split_And' of term | Split_Intersect' of term | Split_Or' of term
367 | Subproblem' of spec * ori list * term * fmz_ * Proof.context * term
368 | Substitute' of rew_ord_ * rls * subte * term * term | Tac_ of theory * string * string * string
369 | Take' of term | Take_Inst' of term
370 val tac_2str : tac_ -> string val test_trans : ppobj -> bool val topt2str : term option -> string end*)
373 structure CTbasic(**): BASIC_CALC_TREE(**) =
376 type env = (term * term) list;
379 NoBranch | AndB | OrB
380 | TransitiveB (* FIXXXME.0308: set branch from met in Apply_Method
381 FIXXXME.0402: -"- in Begin_Trans'*)
382 | SequenceB | IntersectB | CollectB | MapB;
384 fun branch2str NoBranch = "NoBranch" (* for tests only *)
385 | branch2str AndB = "AndB"
386 | branch2str OrB = "OrB"
387 | branch2str TransitiveB = "TransitiveB"
388 | branch2str SequenceB = "SequenceB"
389 | branch2str IntersectB = "IntersectB"
390 | branch2str CollectB = "CollectB"
391 | branch2str MapB = "MapB";
394 Incomplete | Complete | Inconsistent (* WN041020 latter still unused *);
395 fun ostate2str Incomplete = "Incomplete" (* for tests only *)
396 | ostate2str Complete = "Complete"
397 | ostate2str Inconsistent = "Inconsistent";
400 type cid = cellID list;
402 type posel = int; (* for readability in funs accessing Ctree *)
404 val pos2str = ints2str';
406 Pbl (* PblObj-position: problem-type *)
407 | Met (* PblObj-position: method *)
408 | Frm (* PblObj-position: -> Pbl in ME (not by moveDown !)
409 | PrfObj-position: formula *)
410 | Res (* PblObj | PrfObj-position: result *)
411 | Und; (* undefined*)
412 fun pos_2str Pbl = "Pbl"
413 | pos_2str Met = "Met"
414 | pos_2str Frm = "Frm"
415 | pos_2str Res = "Res"
416 | pos_2str Und = "Und";
417 fun str2pos_ "Pbl" = Pbl
418 | str2pos_ "Met" = Met
419 | str2pos_ "Frm" = Frm
420 | str2pos_ "Res" = Res
421 | str2pos_ "Und" = Und
422 | str2pos_ str = error ("str2pos_: wrong argument = " ^ str)
424 type pos' = pos * pos_;
425 (*WN0312 remembering interator (pos * pos_) for ctree
426 pos : lev_on, lev_dn, lev_up
428 # generate1 sets pos_ if possible ...?WN0502?NOT...
429 # generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn
430 exceptions: Begin/End_Trans
431 # thus generate(1) called in
433 .# nxt_solv (tac_ -cases); general case:
434 val pos' = case pos' of (p,Res) => (lev_on p',Res) | _ => pos'
436 generate1...(Rewrite(f,..,res))..(pos, pos_)
437 cappend_atomic.................pos ////// gets f+res always!!!
438 cut_tree....................pos, pos_
440 fun pos'2str (p, p_) = pair2str (ints2str' p, pos_2str p_);
441 fun pos's2str ps = (strs2str' o (map pos'2str)) ps; (* for tests only *)
442 val e_pos' = ([], Und);
444 (* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*)
445 fun is_e_ctxt ctxt = Theory.eq_thy (Proof_Context.theory_of ctxt, @{theory "Pure"});
447 type iist = Selem.istate option * Selem.istate option;
448 (*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*)
451 fun new_val v (Selem.ScrState (env, loc_, topt, _, safe, bool)) =
452 (Selem.ScrState (env, loc_, topt, v, safe, bool))
453 | new_val _ _ = error "new_val: only for ScrState";
455 datatype con = land | lor;
457 (* tactics for user at front-end.
458 tac propagates the construction of the calc-tree;
460 (a) 'specsteps' for the specify-phase, and others for the solve-phase
461 (b) those of the solve-phase are 'initac's and others;
462 initacs start with a formula different from the preceding formula.
463 see 'type tac_' for the internal representation of tactics
464 TODO.WN161219: replace *every* cterm' by term
467 Add_Find of cterm' | Add_Given of cterm' | Add_Relation of cterm'
468 | Apply_Assumption of cterm' list
469 | Apply_Method of metID
470 (* creates an "istate" in PblObj.env; in case of "init_form"
471 creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
472 a "SOME istate" at fst of "loc".
473 As each step (in the solve-phase) has a resulting formula (at the front-end)
474 Apply_Method also does the 1st step in the script (an "initac") if there is no "init_form" *)
475 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
476 | Begin_Sequ | Begin_Trans
477 | Split_And | Split_Or | Split_Intersect
478 | Conclude_And | Conclude_Or | Collect_Trues
479 | End_Sequ | End_Trans
480 | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'
481 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
483 | Calculate of string
484 | Check_Postcond of pblID
485 | Check_elementwise of cterm'
486 | Del_Find of cterm' | Del_Given of cterm' | Del_Relation of cterm'
488 | Derive of rls' (* WN0509 drop *)
489 | Detail_Set of rls' (* WN0509 drop *)
490 | Detail_Set_Inst of Selem.subs * rls' (* WN0509 drop *)
491 | End_Detail (* WN0509 drop *)
496 | Init_Proof of cterm' list * spec
499 | Refine_Problem of pblID
500 | Refine_Tacitly of pblID
502 (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
503 because there all the thms are present with both (thmID, thm)
504 (where user-views can show both or only one of (thmID, thm)),
505 and thm is created from ThmID by assoc_thm'' when entering isabisac *)
507 | Rewrite_Asm of thm''
508 | Rewrite_Inst of Selem.subs * thm''
509 | Rewrite_Set of rls'
510 | Rewrite_Set_Inst of Selem.subs * rls'
512 | Specify_Method of metID
513 | Specify_Problem of pblID
514 | Specify_Theory of domID
515 | Subproblem of domID * pblID (* WN0509 drop *)
517 | Substitute of Selem.sube
518 | Tac of string (* WN0509 drop *)
519 | Take of cterm' | Take_Inst of cterm'
521 fun tac2str ma = case ma of
522 Init_Proof (ppc, spec) =>
523 "Init_Proof "^(pair2str (strs2str ppc, spec2str spec))
524 | Model_Problem => "Model_Problem "
525 | Refine_Tacitly pblID => "Refine_Tacitly " ^ strs2str pblID
526 | Refine_Problem pblID => "Refine_Problem " ^ strs2str pblID
527 | Add_Given cterm' => "Add_Given " ^ cterm'
528 | Del_Given cterm' => "Del_Given " ^ cterm'
529 | Add_Find cterm' => "Add_Find " ^ cterm'
530 | Del_Find cterm' => "Del_Find " ^ cterm'
531 | Add_Relation cterm' => "Add_Relation " ^ cterm'
532 | Del_Relation cterm' => "Del_Relation " ^ cterm'
534 | Specify_Theory domID => "Specify_Theory " ^ quote domID
535 | Specify_Problem pblID => "Specify_Problem " ^ strs2str pblID
536 | Specify_Method metID => "Specify_Method " ^ strs2str metID
537 | Apply_Method metID => "Apply_Method " ^ strs2str metID
538 | Check_Postcond pblID => "Check_Postcond " ^ strs2str pblID
539 | Free_Solve => "Free_Solve"
541 | Rewrite_Inst (subs, (id, thm)) =>
542 "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> term2str)))
543 | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> term2str)
544 | Rewrite_Asm (id, thm) => "Rewrite_Asm " ^ spair2str (id, thm |> Thm.prop_of |> term2str)
545 | Rewrite_Set_Inst (subs, rls) =>
546 "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
547 | Rewrite_Set rls => "Rewrite_Set " ^ quote rls
548 | Detail_Set rls => "Detail_Set " ^ quote rls
549 | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls)
550 | End_Detail => "End_Detail"
551 | Derive rls' => "Derive " ^ rls'
552 | Calculate op_ => "Calculate " ^ op_
553 | Substitute sube => "Substitute " ^ Selem.sube2str sube
554 | Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's
556 | Take cterm' => "Take " ^ quote cterm'
557 | Take_Inst cterm' => "Take_Inst " ^ quote cterm'
558 | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
559 | End_Subproblem => "End_Subproblem"
560 | CAScmd cterm' => "CAScmd " ^ quote cterm'
562 | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
563 | Or_to_List => "Or_to_List "
564 | Collect_Trues => "Collect_Trues"
566 | Empty_Tac => "Empty_Tac"
567 | Tac string => "Tac " ^ string
568 | End_Proof' => "tac End_Proof'"
569 | _ => "tac2str not impl. for ?!";
571 fun is_empty_tac tac = case tac of Empty_Tac => true | _ => false
573 fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
574 | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
575 | eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2
576 | eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2
577 | eq_tac (Calculate id1, Calculate id2) = id1 = id2
580 fun is_rewset (Rewrite_Set_Inst _) = true
581 | is_rewset (Rewrite_Set _) = true
582 | is_rewset _ = false;
583 fun is_rewtac (Rewrite _) = true
584 | is_rewtac (Rewrite_Inst _) = true
585 | is_rewtac (Rewrite_Asm _) = true
586 | is_rewtac tac = is_rewset tac;
588 fun tac2IDstr ma = case ma of
589 Model_Problem => "Model_Problem"
590 | Refine_Tacitly _ => "Refine_Tacitly"
591 | Refine_Problem _ => "Refine_Problem"
592 | Add_Given _ => "Add_Given"
593 | Del_Given _ => "Del_Given"
594 | Add_Find _ => "Add_Find"
595 | Del_Find _ => "Del_Find"
596 | Add_Relation _ => "Add_Relation"
597 | Del_Relation _ => "Del_Relation"
599 | Specify_Theory _ => "Specify_Theory"
600 | Specify_Problem _ => "Specify_Problem"
601 | Specify_Method _ => "Specify_Method"
602 | Apply_Method _ => "Apply_Method"
603 | Check_Postcond _ => "Check_Postcond"
604 | Free_Solve => "Free_Solve"
606 | Rewrite_Inst _ => "Rewrite_Inst"
607 | Rewrite _ => "Rewrite"
608 | Rewrite_Asm _ => "Rewrite_Asm"
609 | Rewrite_Set_Inst _ => "Rewrite_Set_Inst"
610 | Rewrite_Set _ => "Rewrite_Set"
611 | Detail_Set _ => "Detail_Set"
612 | Detail_Set_Inst _ => "Detail_Set_Inst"
613 | Derive _ => "Derive "
614 | Calculate _ => "Calculate "
615 | Substitute _ => "Substitute"
616 | Apply_Assumption _ => "Apply_Assumption"
619 | Take_Inst _ => "Take_Inst"
620 | Subproblem _ => "Subproblem"
621 | End_Subproblem => "End_Subproblem"
622 | CAScmd _ => "CAScmd"
624 | Check_elementwise _ => "Check_elementwise"
625 | Or_to_List => "Or_to_List "
626 | Collect_Trues => "Collect_Trues"
628 | Empty_Tac => "Empty_Tac"
630 | End_Proof' => "End_Proof'"
631 | _ => "tac2str not impl. for ?!";
633 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
634 | rls_of (Rewrite_Set rls) = rls
635 | rls_of tac = error ("rls_of: called with tac \"" ^ tac2IDstr tac ^ "\"");
637 fun rule2tac thy _ (Calc (opID, thm)) = Calculate (assoc_calc thy opID)
638 | rule2tac _ [] (Thm thm'') = Rewrite thm''
639 | rule2tac _ subst (Thm thm'') =
640 Rewrite_Inst (Selem.subst2subs subst, thm'')
641 | rule2tac _ [] (Rls_ rls) = Rewrite_Set (id_rls rls)
642 | rule2tac _ subst (Rls_ rls) =
643 Rewrite_Set_Inst (Selem.subst2subs subst, (id_rls rls))
644 | rule2tac _ _ rule =
645 error ("rule2tac: called with \"" ^ rule2str rule ^ "\"");
647 (* tactics for for internal use, compare "tac" for user at the front-end.
648 tac_ contains results from check in 'fun applicable_in'.
649 This is useful for costly results, e.g. from rewriting;
650 however, these results might be changed by Scripts like
651 " eq = (Rewrite_Set ansatz_rls False) eql;" ^
652 " eq = drop_questionmarks eq;" ^
653 " eq = (Rewrite_Set equival_trans False) eq;" ^
654 TODO.WN120106 ANALOGOUSLY TO Substitute':
655 So tac_ contains the term t the result was calculated from
656 in order to compare t with t' possibly changed by "Expr "
657 and re-calculate result if t<>t'
658 TODO.WN161219: replace *every* cterm' by term
661 Add_Find' of cterm' * itm list | Add_Given' of cterm' * itm list | Add_Relation' of cterm' * itm list
662 | Apply_Assumption' of term list * term
663 | Apply_Method' of metID * term option * Selem.istate * Proof.context
664 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
665 | Begin_Sequ' | Begin_Trans' of term
666 | Split_And' of term | Split_Or' of term | Split_Intersect' of term
667 | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
668 | End_Sequ' | End_Trans' of Selem.result
669 | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''
670 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
672 | Calculate' of theory' * string * term * (term * thm')
673 | Check_Postcond' of pblID *
674 Selem.result (* returnvalue of script in solve *)
675 | Check_elementwise' of (*special case:*)
676 term * (* (1) the current formula: [x=1,x=...] *)
677 string * (* (2) the pred from Check_elementwise *)
678 Selem.result (* (3) composed from (1) and (2): {x. pred} *)
679 | Del_Find' of cterm' | Del_Given' of cterm' | Del_Relation' of cterm'
682 | Detail_Set' of theory' * bool * rls * term * Selem.result
683 | Detail_Set_Inst' of theory' * bool * subst * rls * term * Selem.result
684 | End_Detail' of Selem.result
689 | Init_Proof' of cterm' list * spec
690 | Model_Problem' of pblID *
691 itm list * (* the 'untouched' pbl *)
692 itm list (* the casually completed met *)
693 | Or_to_List' of term * term
694 | Refine_Problem' of pblID * (itm list * (bool * term) list)
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 Model_Problem recognizing its activation *)
701 | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * Selem.result
702 | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * Selem.result
703 | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * Selem.result
704 | Rewrite_Set' of theory' * bool * rls * term * Selem.result
705 | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * Selem.result
707 | Specify_Method' of metID * ori list * itm list
708 | Specify_Problem' of pblID *
709 (bool * (* matches *)
710 (itm list * (* ppc *)
711 (bool * term) list)) (* preconditions *)
712 | Specify_Theory' of domID
715 (ori list) * (* filled in assod Subproblem' *)
716 term * (* -"-, headline of calc-head *)
718 Proof.context * (* transported from assod to generate1*)
719 term (* Subproblem(dom,pbl) OR cascmd *)
721 rew_ord_ * (* for re-calculation *)
722 rls * (* for re-calculation *)
723 Selem.subte * (* the 'substitution': terms of type bool *)
724 term * (* to be substituted in *)
725 term (* resulting from the substitution *)
726 | Tac_ of theory * string * string * string
727 | Take' of term | Take_Inst' of term
729 fun tac_2str ma = case ma of
730 Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, spec2str spec)
731 | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
732 | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
733 strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
734 | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"
735 | Add_Given' _ => "Add_Given' "(*^cterm'*)
736 | Del_Given' _ => "Del_Given' "(*^cterm'*)
737 | Add_Find' _ => "Add_Find' "(*^cterm'*)
738 | Del_Find' _ => "Del_Find' "(*^cterm'*)
739 | Add_Relation' _ => "Add_Relation' "(*^cterm'*)
740 | Del_Relation' _ => "Del_Relation' "(*^cterm'*)
742 | Specify_Theory' domID => "Specify_Theory' " ^ quote domID
743 | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
744 spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
745 | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
746 metID2str pI ^ ", " ^ oris2str oris ^ ", )"
748 | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
749 | Check_Postcond' (pblID, (scval, asm)) => "Check_Postcond' " ^
750 (spair2str (strs2str pblID, spair2str (term2str scval, terms2str asm)))
752 | Free_Solve' => "Free_Solve'"
754 | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
755 | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
756 | Rewrite_Asm' _(*thm'*) => "Rewrite_Asm' "(*^(spair2str thm')*)
757 | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
758 | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
759 "," ^ id_rls rls' ^ "," ^ term2str f ^ ",(" ^ term2str f' ^ "," ^ terms2str asm ^ "))"
760 | End_Detail' _ => "End_Detail' xxx"
761 | Detail_Set' _ => "Detail_Set' xxx"
762 | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
764 | Derive' rls => "Derive' " ^ id_rls rls
765 | Calculate' _ => "Calculate' "
766 | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
767 | Apply_Assumption' _(* ct's*) => "Apply_Assumption' "(*^(strs2str ct's)*)
769 | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*)
770 | Take_Inst' _(*cterm'*) => "Take_Inst' "(*^(quote cterm' )*)
771 | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) =>
772 "Subproblem' "(*^(pair2str (domID, strs2str ,))*)
773 | End_Subproblem' _ => "End_Subproblem'"
774 | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*)
776 | Empty_Tac_ => "Empty_Tac_"
777 | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"
778 | _ => "tac_2str not impl. for arg";
780 (* executed tactics (tac_s) with local environment etc.;
781 used for continuing eval script + for generate *)
783 (loc_ * (* of tactic in scr, tactic (weakly) associated with tac_ *)
784 (tac_ * (* (for generate) *)
785 env * (* with 'tactic=result' as rule, tactic ev. _not_ ready: for handling 'parallel let'*)
786 env * (* with results of (ready) tacs *)
787 term * (* itr_arg of tactic, for upd. env at Repeat, Try *)
788 term * (* result value of the tac *)
792 fun ets2s (l,(m,eno,env,iar,res,s)) =
793 "\n(" ^ loc_2str l ^ ",(" ^ tac_2str m ^
794 ",\n ens= " ^ subst2str eno ^
795 ",\n env= " ^ subst2str env ^
796 ",\n iar= " ^ term2str iar ^
797 ",\n res= " ^ term2str res ^
798 ",\n " ^ Selem.safe2str s ^ "))";
799 fun ets2str (ets: ets) = (strs2str o (map ets2s)) ets; (* for tests only *)
801 type envp =(*9.5.03: unused, delete with field in ctree.PblObj FIXXXME*)
802 (int * term list) list * (* assoc-list: args of met*)
803 (int * rls) list * (* assoc-list: tacs already done ///15.9.00*)
804 (int * ets) list * (* assoc-list: tacs etc. already done*)
805 (string * pos) list; (* asms * from where*)
807 datatype ppobj = (* TODO: arrange according to signature *)
809 {cell : lrd option, (* where in form tac has been applied, FIXME.WN0607 rename field *)
810 form : term, (* where tac is applied to *)
811 tac : tac, (* also in istate *)
812 loc : (Selem.istate * (* script interpreter state *)
813 Proof.context) (* context for provers, type inference *)
814 option * (* both for interpreter location on Frm, Pbl, Met *)
815 (Selem.istate * (* script interpreter state *)
816 Proof.context) (* context for provers, type inference *)
817 option, (* both for interpreter location on Res *)
818 (*(NONE,NONE) <==> e_istate ! see update_loc, get_loc *)
819 branch: branch, (* only rudimentary *)
820 result: Selem.result, (* result and assumptions *)
821 ostate: ostate} (* Complete <=> result is OK *)
823 {cell : lrd option, (* unused: meaningful only for some _Prf_Obj *)
824 fmz : Selem.fmz, (* from init:FIXME never use this spec;-drop *)
825 origin: (ori list) * (* representation from fmz+pbt
826 for efficiently adding items in probl, meth *)
827 spec * (* updated by Refine_Tacitly *)
828 term, (* headline of calc-head, as calculated initially(!) *)
829 spec : spec, (* explicitly input *)
830 probl : itm list, (* itms explicitly input *)
831 meth : itm list, (* itms automatically added to copy of probl *)
832 ctxt : Proof.context, (* WN110513 introduced to avoid [*] [**] *)
833 env : (Selem.istate * Proof.context) option, (* istate only for initac in script
834 context for specify phase on this node NO..
835 ..NO: this conflicts with init_form/initac: see Apply_Method without init_form *)
836 loc : (Selem.istate * Proof.context) option * (Selem.istate * (* like PrfObj *)
837 Proof.context) option, (* for spec-phase [*], NO..
838 ..NO: raises errors not tracable on WN110513 [**] *)
839 branch: branch, (* like PrfObj *)
840 result: Selem.result, (* like PrfObj *)
841 ostate: ostate}; (* like PrfObj *)
843 (* this tree contains isac's calculations;
844 the tree's structure has been copied from an early version of Theorema(c);
845 it has the disadvantage, that there is no space
846 for the first tactic in a script generating the first formula at (p,Frm);
847 this trouble has been covered by 'init_form' and 'Take' so far,
848 but it is crucial if the first tactic in a script is eg. 'Subproblem';
849 see 'type tac', Apply_Method.
853 | Nd of ppobj * (ctree list);
854 val e_ctree = EmptyPtree;
855 type state = ctree * pos'
857 fun is_pblobj (PblObj _) = true
858 | is_pblobj _ = false;
860 exception PTREE of string;
861 fun nth _ [] = raise PTREE "nth _ []"
863 | nth n (_ :: xs) = nth (n - 1) xs;
864 (*> nth 2 [11,22,33]; -->> val it = 22 : int*)
867 (** convert ctree to a string **)
869 (* convert a pos from list to string *)
870 fun pr_pos ps = (space_implode "." (map string_of_int ps))^". ";
871 (* show hd origin or form only *)
872 fun pr_short p (PblObj _) = pr_pos p ^ " ----- pblobj -----\n" (* for tests only *)
873 | pr_short p (PrfObj {form = form, ...}) = pr_pos p ^ term2str form ^ "\n";
874 fun pr_ctree f pt = (* for tests only *)
876 fun pr_pt _ _ EmptyPtree = ""
877 | pr_pt pfn ps (Nd (b, [])) = pfn ps b
878 | pr_pt pfn ps (Nd (b, ts)) = pfn ps b ^ prts pfn ps 1 ts
879 and prts _ _ _ [] = ""
880 | prts pfn ps p (t :: ts) = (pr_pt pfn (ps @ [p]) t)^
881 (prts pfn ps (p + 1) ts)
882 in pr_pt f [] pt end;
884 (** access the branches of ctree **)
886 fun repl [] _ _ = raise PTREE "repl [] _ _"
887 | repl (_ :: ls) 1 e = e :: ls
888 | repl (l :: ls) n e = l :: (repl ls (n-1) e);
889 fun repl_app ls n e =
891 val lim = 1 + length ls
894 then raise PTREE "repl_app: n > lim"
897 else repl ls n e end;
899 (* get from obj at pos by f : ppobj -> 'a *)
900 fun get_obj _ EmptyPtree _ = raise PTREE "get_obj f EmptyPtree"
901 | get_obj f (Nd (b, _)) [] = f b
902 | get_obj f (Nd (_, bs)) (p :: ps) =
905 handle _ => raise PTREE ("get_obj: pos = " ^ ints2str' (p::ps) ^ " does not exist");
907 (get_obj f (nth p bs) ps)
908 handle _ => raise PTREE ("get_obj: pos = " ^ ints2str' (p::ps) ^ " does not exist")
910 fun get_nd EmptyPtree _ = raise PTREE "get_nd EmptyPtree"
912 | get_nd (Nd (_, nds)) (pos as p :: ps) = (get_nd (nth p nds) ps)
913 handle _ => raise PTREE ("get_nd: not existent pos = " ^ ints2str' pos);
915 (* for use by get_obj *)
916 fun g_form (PrfObj {form = f,...}) = f
917 | g_form (PblObj {origin= (_,_,f),...}) = f;
918 fun g_form' (Nd (PrfObj {form = f, ...}, _)) = f
919 | g_form' (Nd (PblObj {origin= (_, _, f),...}, _)) = f
920 | g_form' _ = error "g_form': uncovered fun def.";
921 (* | g_form _ = raise PTREE "g_form not for PblObj";*)
922 fun g_origin (PblObj {origin = ori, ...}) = ori
923 | g_origin _ = raise PTREE "g_origin not for PrfObj";
924 fun g_fmz (PblObj {fmz = f, ...}) = f (* for tests only *)
925 | g_fmz _ = raise PTREE "g_fmz not for PrfObj";
926 fun g_spec (PblObj {spec = s, ...}) = s
927 | g_spec _ = raise PTREE "g_spec not for PrfObj";
928 fun g_pbl (PblObj {probl = p, ...}) = p
929 | g_pbl _ = raise PTREE "g_pbl not for PrfObj";
930 fun g_met (PblObj {meth = p, ...}) = p
931 | g_met _ = raise PTREE "g_met not for PrfObj";
932 fun g_domID (PblObj {spec = (d, _, _), ...}) = d
933 | g_domID _ = raise PTREE "g_metID not for PrfObj";
934 fun g_metID (PblObj {spec = (_, _, m), ...}) = m
935 | g_metID _ = raise PTREE "g_metID not for PrfObj";
936 fun g_ctxt (PblObj {ctxt, ...}) = ctxt
937 | g_ctxt _ = raise PTREE "g_ctxt not for PrfObj";
938 fun g_env (PblObj {env, ...}) = env
939 | g_env _ = raise PTREE "g_env not for PrfObj";
940 fun g_loc (PblObj {loc = l, ...}) = l
941 | g_loc (PrfObj {loc = l, ...}) = l;
942 fun g_branch (PblObj {branch = b, ...}) = b
943 | g_branch (PrfObj {branch = b, ...}) = b;
944 fun g_tac (PblObj {spec = (_, _, m),...}) = Apply_Method m
945 | g_tac (PrfObj {tac = m, ...}) = m;
946 fun g_result (PblObj {result = r, ...}) = r
947 | g_result (PrfObj {result = r, ...}) = r;
948 fun g_res (PblObj {result = (r, _) ,...}) = r
949 | g_res (PrfObj {result = (r, _),...}) = r;
950 fun g_res' (Nd (PblObj {result = (r, _), ...}, _)) = r
951 | g_res' (Nd (PrfObj {result = (r, _),...}, _)) = r
952 | g_res' _ = raise PTREE "g_res': uncovered fun def.";
953 fun g_ostate (PblObj {ostate = r, ...}) = r
954 | g_ostate (PrfObj {ostate = r, ...}) = r;
955 fun g_ostate' (Nd (PblObj {ostate = r, ...}, _)) = r
956 | g_ostate' (Nd (PrfObj {ostate = r, ...}, _)) = r
957 | g_ostate' _ = raise PTREE "g_ostate': uncovered fun def.";
959 (* get the formula preceeding the current position in a calculation *)
960 fun get_curr_formula (pt, (p, p_)) =
962 Frm => get_obj g_form pt p
963 | Res => (fst o (get_obj g_result pt)) p
964 | _ => #3 (get_obj g_origin pt p);
966 (* in CalcTree/Subproblem an 'just_created_' model is created;
967 this is filled to 'untouched' by Model/Refine_Problem *)
968 fun just_created_ (PblObj {meth, probl, spec, ...}) =
969 null meth andalso null probl andalso spec = e_spec
970 | just_created_ _ = raise PTREE "g_ostate': uncovered fun def.";
971 val e_origin = ([],e_spec,e_term);
973 fun just_created (pt, (p, _)) =
974 let val ppobj = get_obj I pt p
975 in is_pblobj ppobj andalso just_created_ ppobj end;
977 (* does the pos in the ctree exist ? *)
978 fun existpt pos pt = can (get_obj I pt) pos;
979 (* does the pos' in the ctree exist, ie. extra check for result in the node *)
980 fun existpt' (p, p_) pt =
981 if can (get_obj I pt) p
983 Res => get_obj g_ostate pt p = Complete
987 (* is this position appropriate for calculating intermediate steps? *)
988 fun is_interpos (_, Res) = true
989 | is_interpos _ = false;
991 (* get the children of a node in ctree *)
992 fun children (Nd (PblObj _, cn)) = cn
993 | children (Nd (PrfObj _, cn)) = cn
994 | children _ = error "children: uncovered fun def.";
996 (*/--------------- duplicates in ctree-navi.sml: required also here below ---------------\*)
997 fun lev_on [] = raise PTREE "lev_on []"
999 let val len = length pos
1000 in (drop_last pos) @ [(nth len pos)+1] end;
1001 fun lev_up [] = raise PTREE "lev_up []"
1002 | lev_up p = (drop_last p):pos;
1003 (* find the position of the next parent which is a PblObj in ctree *)
1004 fun par_pblobj _ [] = []
1009 if is_pblobj (get_obj I pt p)
1011 else par pt (lev_up p)
1012 in par pt (lev_up p) end;
1013 (*\--------------- duplicates in ctree-navi.sml: required also here below ---------------/*)
1015 (* find the next parent, which is either a PblObj (return true)
1016 or a PrfObj with tac = Detail_Set (return false)
1017 FIXME.030403: re-organize par_pbl_det after rls' --> rls*)
1018 fun par_pbl_det pt [] = (true, [], Erls)
1019 | par_pbl_det pt p =
1021 fun par _ [] = (true, [], Erls)
1023 if is_pblobj (get_obj I pt p)
1024 then (true, p, Erls)
1025 else case get_obj g_tac pt p of
1026 Rewrite_Set rls' => (false, p, assoc_rls rls')
1027 | Rewrite_Set_Inst (_, rls') => (false, p, assoc_rls rls')
1028 | _ => par pt (lev_up p)
1029 in par pt (lev_up p) end;
1031 (* insert obj b into ctree at pos, ev.overwriting this pos *)
1032 fun insert_pt b EmptyPtree [] = Nd (b, [])
1033 | insert_pt _ EmptyPtree _ = raise PTREE "insert_pt b Empty _"
1034 | insert_pt _ (Nd ( _, _)) [] = raise PTREE "insert_pt b _ []"
1035 | insert_pt b (Nd (b', bs)) (p :: []) = Nd (b', repl_app bs p (Nd (b, [])))
1036 | insert_pt b (Nd (b', bs)) (p :: ps) = Nd (b', repl_app bs p (insert_pt b (nth p bs) ps));
1038 (* insert children to a node without children. compare: fun insert_pt *)
1039 fun ins_chn _ EmptyPtree _ = raise PTREE "ins_chn: EmptyPtree"
1040 | ins_chn _ (Nd _) [] = raise PTREE "ins_chn: pos = []"
1041 | ins_chn ns (Nd (b, bs)) (p :: []) =
1043 then raise PTREE "ins_chn: pos not existent"
1046 val (b', bs') = case nth p bs of
1047 Nd (b', bs') => (b', bs')
1048 | _ => error "ins_chn: uncovered case nth"
1051 then Nd (b, repl_app bs p (Nd (b', ns)))
1052 else raise PTREE "ins_chn: pos mustNOT be overwritten"
1054 | ins_chn ns (Nd (b, bs)) (p::ps) = Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps));
1056 (* apply f to obj at pos, f: ppobj -> ppobj *)
1057 fun appl_to_node f (Nd (b, bs)) = Nd (f b, bs)
1058 | appl_to_node _ _ = error "appl_to_node: uncovered fun def.";
1059 fun appl_obj _ EmptyPtree [] = EmptyPtree
1060 | appl_obj _ EmptyPtree _ = raise PTREE "appl_obj f Empty _"
1061 | appl_obj f (Nd (b, bs)) [] = Nd (f b, bs)
1062 | appl_obj f (Nd (b, bs)) (p :: []) = Nd (b, repl_app bs p (((appl_to_node f) o (nth p)) bs))
1063 | appl_obj f (Nd (b, bs)) (p :: ps) = Nd (b, repl_app bs p (appl_obj f (nth p bs) (ps:pos)));
1067 bool * (* ALL itms+preconds true *)
1068 pos_ * (* model belongs to Problem | Method *)
1069 term * (* header: Problem... or Cas FIXME.0312: item for marking syntaxerrors *)
1070 itm list * (* model: given, find, relate *)
1071 ((bool * term) list) *(* model: preconds *)
1072 spec; (* specification *)
1073 val e_ocalhd = (false, Und, e_term, [e_itm], [(false, e_term)], e_spec);
1075 datatype ptform = Form of term | ModSpec of ocalhd;
1077 (* for cut_level; (deprecated) *)
1078 fun test_trans (PrfObj {branch, ...}) = true andalso branch = TransitiveB
1079 | test_trans (PblObj {branch, ...}) = true andalso branch = TransitiveB;
1081 fun is_pblobj' pt p =
1082 let val ppobj = get_obj I pt p
1083 in is_pblobj ppobj end;
1085 fun del_res (PblObj {cell, fmz, origin, spec, probl, meth, ctxt, env, loc= (l1, _), branch, ...}) =
1086 PblObj {cell = cell, fmz = fmz, origin = origin, spec = spec, probl = probl, meth = meth,
1087 ctxt = ctxt, env = env, loc= (l1, NONE), branch = branch,
1088 result = (e_term, []), ostate = Incomplete}
1089 | del_res (PrfObj {cell, form, tac, loc= (l1, _), branch, ...}) =
1090 PrfObj {cell = cell, form = form, tac = tac, loc = (l1, NONE), branch = branch,
1091 result = (e_term, []), ostate = Incomplete};
1094 fun get_loc EmptyPtree _ = (Selem.e_istate, Selem.e_ctxt)
1095 | get_loc pt (p, Res) =
1096 (case get_obj g_loc pt p of
1098 | (NONE , NONE) => (Selem.e_istate, Selem.e_ctxt)
1099 | (_ , SOME i) => i)
1100 | get_loc pt (p, _) =
1101 (case get_obj g_loc pt p of
1102 (NONE , SOME i) => i (*13.8.02 just copied from ^^^: too liberal ?*)
1103 | (NONE , NONE) => (Selem.e_istate, Selem.e_ctxt)
1104 | (SOME i, _) => i);
1105 fun get_istate pt p = get_loc pt p |> #1;
1106 fun get_ctxt pt (pos as (p, p_)) =
1107 if member op = [Frm, Res] p_
1108 then get_loc pt pos |> #2 (*for script interpretation rely on fun get_loc*)
1109 else get_obj g_ctxt pt p (*for specify phase take ctx from PblObj*)
1111 fun get_assumptions_ pt p = get_ctxt pt p |> get_assumptions;
1113 fun get_somespec' (dI, pI, mI) (dI', pI', mI') =
1115 val domID = if dI = e_domID then dI' else dI
1116 val pblID = if pI = e_pblID then pI' else pI
1117 val metID = if mI = e_metID then mI' else mI
1118 in (domID, pblID, metID) end;
1120 (**.development for extracting an 'interval' from ptree.**)
1122 (*WN0510 version stopped in favour of get_interval with !!!move_dn, getFormulaeFromTo
1123 actually used (inefficient) version with move_dn: see modspec.sml*)
1126 fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*)
1127 fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)
1128 fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x;
1129 fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
1131 fun getnd i (b,p) q (Nd (po, nds)) =
1132 (if i <= 0 then [[b]] else []) @
1133 (getnds (i-1) true (b@[hdp p], tlp p) (tlq q)
1134 (take_fromto (hdp p) (hdq q) nds))
1136 and getnds _ _ _ _ [] = [] (*no children*)
1137 | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)
1139 | getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*)
1140 (getnd i ( b, p ) [99999] n1) @
1141 (getnd ~99999 (lev_on b,[0]) q n2)
1143 | getnds i _ (b,p) q [n1, n2] = (*intern, r-margin*)
1144 (getnd i ( b,[0]) [99999] n1) @
1145 (getnd ~99999 (lev_on b,[0]) q n2)
1147 | getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*)
1148 (getnd i ( b, p ) [99999] nd) @
1149 (getnds ~99999 false (lev_on b,[0]) q nds)
1151 | getnds i _ (b,p) q (nd::(nds as _::_)) = (*intern, ...*)
1152 (getnd i ( b,[0]) [99999] nd) @
1153 (getnds ~99999 false (lev_on b,[0]) q nds);
1155 (*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes
1156 where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
1157 (1) the 'f' are given
1158 (1a) by 'from' if 'f' = the respective element of 'from' (left margin)
1159 (1b) -inifinity, if 'f' > the respective element of 'from' (internal node)
1160 (2) the 't' ar given
1161 (2a) by 'to' if 't' = the respective element of 'to' (right margin)
1162 (2b) inifinity, if 't' < the respective element of 'to (internal node)'
1163 the 'f' and 't' are set by hdp,... *)
1164 fun get_trace pt p q =
1165 (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q)))
1166 (take_fromto (hdp p) (hdq q) (children pt));
1169 (*extract a formula or model from ctree for itms2itemppc or model2xml*)
1170 fun preconds2str bts =
1171 (strs2str o (map (linefeed o pair2str o
1173 (apfst bool2str)))) bts;
1174 fun ocalhd2str (b, p, hdf, itms, prec, spec) = (* for tests only *)
1175 "(" ^ bool2str b ^ ", " ^ pos_2str p ^ ", " ^ term2str hdf ^
1176 ", " ^ itms2str_ (thy2ctxt' "Isac") itms ^
1177 ", " ^ preconds2str prec ^ ", \n" ^ spec2str spec ^ " )";
1179 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj
1180 | is_pblnd _ = error "is_pblnd: uncovered fun def.";
1183 (* determine the previous pos' on the same level
1184 WN0502 made for interSteps; _only_ works for branch TransitiveB WN120517 compare lev_back *)
1185 fun lev_pred' _ ([], Res) = ([], Pbl)
1186 | lev_pred' pt (p, Res) =
1187 let val (p', last) = split_last p
1190 then if (is_pblobj o (get_obj I pt)) p then (p, Pbl) else (p, Frm)
1191 else if get_obj g_res pt (p' @ [last - 1]) = get_obj g_form pt p
1192 then (p' @ [last - 1], Res) (* TransitiveB *)
1193 else if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm)
1195 | lev_pred' _ _ = error "";
1198 (**.insert into ctree and cut branches accordingly.**)
1200 (* get all positions of certain intervals on the ctree.
1201 OLD VERSION without move_dn; kept for occasional redesign
1202 get all pos's to be cut in a ctree
1203 below a pos or from a ctree list after i-th element (NO level_up) *)
1204 fun get_allpos' (_, _) EmptyPtree = []
1205 | get_allpos' (p, 1) (Nd (b, bs)) = (* p is pos of Nd *)
1206 if g_ostate b = Incomplete
1207 then (p, Frm) :: (get_allpos's (p, 1) bs)
1208 else (p, Frm) :: (get_allpos's (p, 1) bs) @ [(p, Res)]
1209 | get_allpos' (p, i) (Nd (b, bs)) = (* p is pos of Nd *)
1210 if length bs > 0 orelse is_pblobj b
1211 then if g_ostate b = Incomplete
1212 then [(p,Frm)] @ (get_allpos's (p, 1) bs)
1213 else [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p, Res)]
1214 else if g_ostate b = Incomplete then [] else [(p, Res)]
1215 and get_allpos's _ [] = []
1216 | get_allpos's (p, i) (pt :: pts) = (* p is pos of parent-Nd *)
1217 (get_allpos' (p @ [i], i) pt) @ (get_allpos's (p, i + 1) pts);
1219 (*WN050106 like cut_level, but deletes exactly 1 node *)
1220 fun cut_level_'_ _ _ EmptyPtree _ =raise PTREE "cut_level_'_ Empty _" (* for tests ONLY *)
1221 | cut_level_'_ _ _ (Nd ( _, _)) ([], _) = raise PTREE "cut_level_'_ _ []"
1222 | cut_level_'_ cuts P (Nd (b, bs)) (p :: [], p_) =
1225 (Nd (b, drop_nth [] (p:posel, bs)),
1226 cuts @ (if p_ = Frm then [(P @ [p], Res)] else []) @
1227 (get_allpos's (P, p + 1) (drop_nth [] (p, bs))))
1228 else (Nd (b, bs), cuts)
1229 | cut_level_'_ cuts P (Nd (b, bs)) ((p :: ps), p_) =
1231 val (bs', cuts') = cut_level_'_ cuts P (nth p bs) (ps, p_)
1232 in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
1234 fun cut_level _ _ EmptyPtree _ = raise PTREE "cut_level EmptyPtree _"
1235 | cut_level _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level _ []"
1236 | cut_level cuts P (Nd (b, bs)) (p :: [], p_) =
1239 (Nd (b, take (p:posel, bs)),
1241 (if p_ = Frm andalso (*#*) g_ostate b = Complete then [(P@[p],Res)] else ([]:pos' list)) @
1242 (get_allpos's (P, p+1) (takerest (p, bs))))
1243 else (Nd (b, bs), cuts)
1244 | cut_level cuts P (Nd (b, bs)) ((p :: ps), p_) =
1246 val (bs', cuts') = cut_level cuts P (nth p bs) (ps, p_)
1247 in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
1249 (*OLD version before WN050219, overwritten below*)
1250 fun cut_tree _ ([], _) = raise PTREE "cut_tree _ ([],_)" (* for test only *)
1251 | cut_tree pt (pos as ([_], _)) =
1253 val (pt', cuts) = cut_level [] [] pt pos
1255 (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete then [] else [([], Res)]))
1257 | cut_tree pt (p,p_) =
1259 fun cutfn pt cuts (p, p_) =
1261 val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_)
1263 if length cuts' > 0 andalso length p > 1
1264 then cutfn pt' (cuts @ cuts') (lev_up p, Frm(*-->(p,Res)*))
1265 else (pt', cuts @ cuts')
1267 val (pt', cuts) = cutfn pt [] (p, p_)
1269 (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete then [] else [([], Res)]))
1273 fun move_dn _ (Nd (_, ns)) ([],p_) = (* root problem *)
1275 Res => raise PTREE "move_dn: end of calculation"
1277 if null ns (* go down from Pbl + Met *)
1278 then raise PTREE "move_dn: solve problem not started"
1280 | move_dn P (Nd (_, ns)) (p :: (ps as (_ :: _)), p_) = (* iterate to end of pos *)
1282 then raise PTREE "move_dn: pos not existent 2"
1283 else move_dn (P @ [p]) (nth p ns) (ps, p_)
1284 | move_dn P (Nd (c, ns)) ([p], p_) = (* act on last element of pos *)
1286 then raise PTREE "move_dn: pos not existent 3"
1290 if p = length ns (* last Res on this level: go a level up *)
1291 then if g_ostate c = Complete
1293 else raise PTREE (ints2str' P ^ " not complete 1")
1294 else (* go to the next Nd on this level, or down into the next Nd *)
1295 if is_pblnd (nth (p + 1) ns) then (P@[p + 1], Pbl)
1296 else if g_res' (nth p ns) = g_form' (nth (p + 1) ns)
1297 then if (null o children o (nth (p + 1))) ns
1298 then (* take the Res if Complete *)
1299 if g_ostate' (nth (p + 1) ns) = Complete
1300 then (P@[p + 1], Res)
1301 else raise PTREE (ints2str' (P@[p + 1]) ^ " not complete 2")
1302 else (P@[p + 1, 1], Frm) (* go down into the next PrfObj *)
1303 else (P@[p + 1], Frm) (* take Frm: exists if the Nd exists *)
1304 | Frm => (*go down or to the Res of this Nd*)
1305 if (null o children o (nth p)) ns
1306 then if g_ostate' (nth p ns) = Complete then (P @ [p], Res)
1307 else raise PTREE (ints2str' (P @ [p])^" not complete 3")
1308 else (P @ [p, 1], Frm)
1309 | _ => (* is Pbl or Met *)
1310 if (null o children o (nth p)) ns
1311 then raise PTREE "move_dn:solve subproblem not startd"
1313 if (is_pblnd o hd o children o (nth p)) ns
1315 | move_dn _ _ _ = error "";
1317 (* get all positions in a ctree until ([],Res) or ostate=Incomplete
1319 pos' list -> : accumulated, start with []
1320 pos -> : the offset for subtrees wrt the root
1321 ctree -> : (sub)tree
1322 pos' : initialization (the last pos' before ...)
1323 -> pos' list : of positions in this (sub) tree (relative to the root)
1325 fun get_allp cuts (P, pos) pt =
1327 val nxt = move_dn [] pt pos (*exn if Incomplete reached*)
1330 then get_allp (cuts @ [nxt]) (P, nxt) pt
1331 else map (apfst (curry op @ P)) (cuts @ [nxt])
1333 handle PTREE _ => (map (apfst (curry op@ P)) cuts);
1336 (* the pts are assumed to be on the same level *)
1337 fun get_allps cuts _ [] = cuts
1338 | get_allps cuts P (pt :: pts) =
1340 val below = get_allp [] (P, ([], Frm)) pt
1343 then (P, Pbl) :: below
1344 else if last_elem P = 1
1345 then (P, Frm) :: below
1346 else (*Trans*) below
1347 val levres = levfrm @ (if null below then [(P, Res)] else [])
1349 get_allps (cuts @ levres) (lev_on P) pts
1352 (** these 2 funs decide on how far cut_tree goes **)
1353 (* shall the nodes _after_ the pos to be inserted at be deleted?
1354 shall cutting be continued on the higher level(s)? the Nd regarded will NOT be changed *)
1355 fun test_trans (PrfObj {branch, ...}) = (branch = TransitiveB orelse branch = NoBranch)
1356 | test_trans (PblObj {branch, ...}) = (branch = TransitiveB orelse branch = NoBranch);
1358 (* cut_bottom new sml603..608
1359 cut the level at the bottom of the pos (used by cappend_...)
1360 and handle the parent in order to avoid extra case for root
1361 fn: ctree -> : the _whole_ ctree for cut_levup
1362 pos * posel -> : the pos after split_last
1363 ctree -> : the parent of the Nd to be cut
1365 (ctree * : the updated ctree
1366 pos' list) * : the pos's cut
1367 bool : cutting shall be continued on the higher level(s)
1369 fun cut_bottom _ (pt' as Nd (b, [])) = ((pt', []), test_trans b)
1370 | cut_bottom (P, p) (Nd (b, bs)) =
1371 let (*divide level into 3 parts...*)
1372 val keep = take (p - 1, bs)
1373 val pt' = case nth p bs of
1375 | _ => error "cut_bottom: uncovered case nth p bs"
1376 (*^^^^^_here_ will be 'insert_pt'ed by 'append_..'*)
1377 val (tail, _) = (takerest (p, bs), if null (takerest (p, bs)) then 0 else p + 1)
1378 val (children, cuts) =
1381 (keep, (if is_pblnd pt' then [(P @ [p], Pbl)] else [])
1382 @ (get_allp [] (P @ [p], (P, Frm)) pt')
1383 @ (get_allps [] (P @ [p + 1]) tail))
1384 else (keep @ [(*'insert_pt'ed by 'append_..'*)] @ tail,
1385 get_allp [] (P @ [p], (P, Frm)) pt')
1388 then (Nd (del_res b, children), cuts @ (if g_ostate b = Incomplete then [] else [(P, Res)]))
1389 else (Nd (b, children), cuts)
1390 in ((pt'', cuts), test_trans b) end
1391 | cut_bottom _ _ = error "cut_bottom: uncovered fun def.";
1394 (* go all levels from the bottom of 'pos' up to the root,
1395 on each level compose the children of a node and accumulate the cut Nds
1397 pos' list -> : for accumulation
1398 bool -> : cutting shall be continued on the higher level(s)
1399 ctree -> : the whole ctree for 'get_nd pt P' on each level
1400 ctree -> : the Nd from the lower level for insertion at path
1401 pos * posel -> : pos=path split for convenience
1402 ctree -> : Nd the children of are under consideration on this call
1404 ctree * pos' list : the updated parent-Nd and the pos's of the Nds cut
1406 fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) =
1407 let (*divide level into 3 parts...*)
1408 val keep = take (p - 1, bs)
1409 (*val pt' comes as argument from below*)
1411 (takerest (p, bs), if null (takerest (p, bs)) then 0 else p + 1)
1412 val (children, cuts') =
1414 then (keep @ [pt'], get_allps [] (P @ [p+1]) tail)
1415 else (keep @ [pt'] @ tail, [])
1416 val clevup' = if clevup then test_trans b else false
1417 (*the first Nd with false stops cutting on all levels above*)
1420 then (Nd (del_res b, children), cuts' @ (if g_ostate b = Incomplete then [] else [(P, Res)]))
1421 else (Nd (b, children), cuts')
1424 then (pt'', cuts @ cuts')
1426 let val (P, p) = split_last P
1427 in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P) end
1429 | cut_levup _ _ _ _ _ _ = error "cut_levup: uncovered fun def.";
1431 (* cut nodes after and below an inserted node in the ctree;
1432 the cuts range is limited by the predicate 'fun cutlevup' *)
1433 fun cut_tree pt (pos, _) =
1434 if not (existpt pos pt)
1435 then (pt,[]) (*appending a formula never cuts anything*)
1438 val (P, p) = split_last pos
1439 val ((pt', cuts), clevup) = cut_bottom (P, p) (get_nd pt P)
1440 (* pt' is the updated parent of the Nd to cappend_..*)
1445 let val (P, p) = split_last P
1446 in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P) end
1449 (* get the theory explicitly specified for the rootpbl;
1450 thus use this function _after_ finishing specification *)
1451 fun rootthy (Nd (PblObj {spec = (thyID, _, _), ...}, _)) = assoc_thy thyID
1452 | rootthy _ = error "rootthy: uncovered fun def.";