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? =================================================================*)
14 val sube2str : cterm' list -> string
15 val sube2subst : theory -> cterm' list -> (term * term) list
16 val sube2subte : cterm' list -> term list
17 val subs2subst : theory -> cterm' list -> (term * term) list
18 val subst2sube : (term * term) list -> cterm' list (* for datatypes.sml *)
19 val subst2subs : (term * term) list -> cterm' list
20 val subst2subs' : (term * term) list -> (string * string) list
21 val subte2sube : term list -> cterm' list
24 Add_Find' of cterm' * itm list | Add_Given' of cterm' * itm list | Add_Relation' of cterm' * itm list
25 | Apply_Assumption' of term list * term
26 | Apply_Method' of metID * term option * Selem.istate * Proof.context
28 | Begin_Sequ' | Begin_Trans' of term
29 | Split_And' of term | Split_Or' of term | Split_Intersect' of term
30 | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
31 | End_Sequ' | End_Trans' of Selem.result
32 | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''
35 | Calculate' of theory' * string * term * (term * thm')
36 | Check_Postcond' of pblID * Selem.result
37 | Check_elementwise' of term * cterm' * Selem.result
38 | Del_Find' of cterm' | Del_Given' of cterm' | Del_Relation' of cterm'
41 | Detail_Set' of theory' * bool * rls * term * Selem.result
42 | Detail_Set_Inst' of theory' * bool * subst * rls * term * Selem.result
43 | End_Detail' of Selem.result
48 | Init_Proof' of cterm' list * spec
49 | Model_Problem' of pblID * itm list * itm list
50 | Or_to_List' of term * term
51 | Refine_Problem' of pblID * (itm list * (bool * term) list)
52 | Refine_Tacitly' of pblID * pblID * domID * metID * itm list
54 | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * Selem.result
55 | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * Selem.result
56 | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * Selem.result
57 | Rewrite_Set' of theory' * bool * rls * term * Selem.result
58 | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * Selem.result
60 | Specify_Method' of metID * ori list * itm list
61 | Specify_Problem' of pblID * (bool * (itm list * (bool * term) list))
62 | Specify_Theory' of domID
63 | Subproblem' of spec * ori list * term * Selem.fmz_ * Proof.context * term
64 | Substitute' of rew_ord_ * rls * subte * term * term
65 | Tac_ of theory * string * string * string
66 | Take' of term | Take_Inst' of term
69 Add_Find of cterm' | Add_Given of cterm' | Add_Relation of cterm'
70 | Apply_Assumption of cterm' list
71 | Apply_Method of metID
72 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
73 | Begin_Sequ | Begin_Trans
74 | Split_And | Split_Or | Split_Intersect
75 | Conclude_And | Conclude_Or | Collect_Trues
76 | End_Sequ | End_Trans
77 | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
78 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
81 | Check_Postcond of pblID
82 | Check_elementwise of cterm'
83 | Del_Find of cterm' | Del_Given of cterm' | Del_Relation of cterm'
87 | Detail_Set_Inst of subs * rls'
93 | Init_Proof of cterm' list * spec
96 | Refine_Problem of pblID
97 | Refine_Tacitly of pblID
100 | Rewrite_Asm of thm''
101 | Rewrite_Inst of subs * thm''
102 | Rewrite_Set of rls'
103 | Rewrite_Set_Inst of subs * rls'
105 | Specify_Method of metID
106 | Specify_Problem of pblID
107 | Specify_Theory of domID
108 | Subproblem of domID * pblID
112 | Take of cterm' | Take_Inst of cterm'
114 val tac2str : tac -> string
115 val rls_of : tac -> rls' (* for solve.sml *)
116 val tac2IDstr : tac -> string
117 val is_rewset : tac -> bool (* for mathengine.sml *)
118 val is_rewtac : tac -> bool (* for interface.sml *)
121 type pos = posel list
122 val pos2str : int list -> string (* for datatypes.sml *)
123 datatype pos_ = Frm | Met | Pbl | Res | Und
124 val pos_2str : pos_ -> string
126 val pos'2str : pos' -> string
127 val str2pos_ : string -> pos_ (* for datatypes.sml *)
129 (* for generate.sml ?!? ca.*)
130 val tac_2str : tac_ -> string
133 datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB
134 datatype ostate = Complete | Incomplete | Inconsistent
139 loc: (Selem.istate * Proof.context) option * (Selem.istate * Proof.context) option,
141 result: Selem.result,
144 origin: ori list * spec * term,
149 env: (Selem.istate * Proof.context) option}
153 loc: (Selem.istate * Proof.context) option * (Selem.istate * Proof.context) option,
155 result: Selem.result,
160 datatype ctree = EmptyPtree | Nd of ppobj * ctree list
161 val e_ctree : ctree (* TODO: replace by EmptyPtree*)
162 val existpt' : pos' -> ctree -> bool (* for interface.sml *)
163 val is_interpos : pos' -> bool (* for interface.sml *)
164 val lev_pred' : ctree -> pos' -> pos' (* for interface.sml *)
165 val ins_chn : ctree list -> ctree -> pos -> ctree (* for solve.sml *)
166 val children : ctree -> ctree list (* for solve.sml *)
167 val get_nd : ctree -> pos -> ctree (* for solve.sml *)
168 val just_created_ : ppobj -> bool (* for mathengine.sml *)
169 val just_created : state -> bool (* for mathengine.sml *)
170 val e_origin : ori list * spec * term (* for mathengine.sml *)
172 val is_pblobj : ppobj -> bool
173 val is_pblobj' : ctree -> pos -> bool
174 val is_pblnd : ctree -> bool
176 val g_spec : ppobj -> spec
177 val g_loc : ppobj -> (Selem.istate * Proof.context) option * (Selem.istate * Proof.context) option
178 val g_form : ppobj -> term
179 val g_pbl : ppobj -> itm list
180 val g_met : ppobj -> itm list
181 val g_metID : ppobj -> metID
182 val g_result : ppobj -> Selem.result
183 val g_tac : ppobj -> tac
184 val g_domID : ppobj -> domID (* for appl.sml TODO: replace by thyID *)
185 val g_env : ppobj -> (Selem.istate * Proof.context) option (* for appl.sml *)
187 val g_origin : ppobj -> ori list * spec * term (* for script.sml *)
188 val get_loc : ctree -> pos' -> Selem.istate * Proof.context (* for script.sml *)
189 val get_istate : ctree -> pos' -> Selem.istate (* for script.sml *)
190 val get_ctxt : ctree -> pos' -> Proof.context
191 val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a
192 val get_curr_formula : state -> term
193 val get_assumptions_ : ctree -> pos' -> term list (* for appl.sml *)
195 val e_ctxt : Proof.context
196 val is_e_ctxt : Proof.context -> bool (* for appl.sml *)
197 val new_val : term -> Selem.istate -> Selem.istate
198 (* for calchead.sml *)
199 type cid = cellID list
200 type ocalhd = bool * pos_ * term * itm list * (bool * term) list * spec
201 datatype ptform = Form of term | ModSpec of ocalhd
202 val get_somespec' : spec -> spec -> spec
203 exception PTREE of string;
205 val par_pbl_det : ctree -> pos -> bool * pos * rls (* for appl.sml *)
206 val rule2tac : theory -> (term * term) list -> rule -> tac (* for rewtools.sml *)
207 val eq_tac : tac * tac -> bool (* for script.sml *)
208 val rootthy : ctree -> theory (* for script.sml *)
209 (* ---- made visible ONLY for structure CTaccess : CALC_TREE_ACCESS --------------------------- *)
210 val appl_obj : (ppobj -> ppobj) -> ctree -> pos -> ctree
211 val existpt : pos -> ctree -> bool (* also for tests *)
212 val is_empty_tac : tac -> bool (* also for tests *)
213 val cut_tree : ctree -> pos * 'a -> ctree * pos' list (* also for tests *)
214 val insert_pt : ppobj -> ctree -> int list -> ctree
215 (* ---- made visible ONLY for structure CTnavi : CALC_TREE_NAVIGATION ------------------------- *)
216 val g_branch : ppobj -> branch
217 val g_form' : ctree -> term
218 val g_ostate : ppobj -> ostate
219 val g_ostate' : ctree -> ostate
220 val g_res : ppobj -> term
221 val g_res' : ctree -> term
222 (*/---- duplicates in CTnavi, reconsider structs -----------------------------------------------
223 val lev_on : CTbasic.pos -> CTbasic.pos (* duplicate in ctree-navi.sml *)
224 val lev_dn : CTbasic.pos -> CTbasic.pos (* duplicate in ctree-navi.sml *)
225 val par_pblobj : CTbasic.ctree -> CTbasic.pos -> CTbasic.pos (* duplicate in ctree-navi.sml *)
226 ---- duplicates in CTnavi, reconsider structs ----------------------------------------------/*)
228 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
229 val pr_ctree : (pos -> ppobj -> string) -> ctree -> string
230 val pr_short : pos -> ppobj -> string
231 val e_subs : string list
232 val e_sube : cterm' list
233 val g_ctxt : ppobj -> Proof.context
234 val g_fmz : ppobj -> Selem.fmz
235 val get_allp : pos' list -> pos * (int list * pos_) -> ctree -> pos' list
236 val get_allps : (pos * pos_) list -> posel list -> ctree list -> pos' list
237 val get_allpos' : pos * posel -> ctree -> pos' list
238 val get_allpos's : pos * posel -> ctree list -> (pos * pos_) list
239 val cut_bottom : pos * posel -> ctree -> (ctree * pos' list) * bool
240 val cut_level : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
241 val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
242 val get_trace : ctree -> int list -> int list -> int list list
243 val subte2subst : term list -> (term * term) list
244 val branch2str : branch -> string
245 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
250 sig exception PTREE of string val appl_obj : (ppobj -> ppobj) -> ctree -> pos -> ctree
251 val appl_to_node : (ppobj -> ppobj) -> ctree -> ctree
252 datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB
253 val branch2str : branch -> string eqtype cellID val children : ctree -> ctree list type cid = cellID list
254 datatype con = land | lor datatype ctree = EmptyPtree | Nd of ppobj * ctree list
255 val cut_bottom : int list * int -> ctree -> (ctree * (int list * pos_) list) * bool
257 (posel list * pos_) list -> posel list -> ctree -> int list * pos_ -> ctree * (posel list * pos_) list
259 (posel list * pos_) list -> posel list -> ctree -> int list * pos_ -> ctree * (posel list * pos_) list
260 val cut_levup : pos' list -> bool -> ctree -> ctree -> int list * int -> ctree -> ctree * pos' list
261 val cut_tree : ctree -> int list * 'a -> ctree * (int list * pos_) list val del_res : ppobj -> ppobj
262 val e_ctree : ctree val e_ctxt : Proof.context val e_fmz : 'a list * spec val e_istate : istate
263 val e_ocalhd : bool * pos_ * term * itm list * (bool * term) list * spec
264 val e_origin : 'a list * spec * term val e_pos' : 'a list * pos_ val e_sube : cterm' list
265 val e_subs : string list type env = (term * term) list
266 type envp = (int * term list) list * (int * rls) list * (int * ets) list * (string * pos) list
267 val eq_tac : tac * tac -> bool type ets = (loc_ * (tac_ * env * env * term * term * safe)) list
268 val ets2s : loc_ * (tac_ * subst * subst * term * term * safe) -> string val ets2str : ets -> string
269 val existpt : int list -> ctree -> bool val existpt' : int list * pos_ -> ctree -> bool
270 val g_branch : ppobj -> branch
271 val g_ctxt : ppobj -> Proof.context val g_domID : ppobj -> domID
272 val g_env : ppobj -> (istate * Proof.context) option val g_fmz : ppobj -> fmz val g_form : ppobj -> term
273 val g_loc : ppobj -> (istate * Proof.context) option * (istate * Proof.context) option
274 val g_met : ppobj -> itm list val g_metID : ppobj -> metID val g_origin : ppobj -> ori list * spec * term
275 val g_res : ppobj -> term val g_result : ppobj -> Selem.result
276 val g_spec : ppobj -> spec val g_tac : ppobj -> tac
277 val get_allp : (int list * pos_) list -> int list * (int list * pos_) -> ctree -> (int list * pos_) list
278 val get_allpos' : posel list * posel -> ctree -> (posel list * pos_) list
279 val get_allpos's : posel list * posel -> ctree list -> (posel list * pos_) list
280 val get_allps : (int list * pos_) list -> int list -> ctree list -> (int list * pos_) list
281 val get_assumptions_ : ctree -> int list * pos_ -> term list
282 val get_ctxt : ctree -> int list * pos_ -> Proof.context
283 val get_curr_formula : ctree * (int list * pos_) -> term
284 val get_istate : ctree -> int list * pos_ -> istate
285 val get_loc : ctree -> int list * pos_ -> istate * Proof.context val get_nd : ctree -> int list -> ctree
286 val get_obj : (ppobj -> 'a) -> ctree -> int list -> 'a
287 val get_somespec' : domID * pblID * metID -> domID * pblID * metID -> domID * pblID * metID
288 val get_trace : ctree -> int list -> int list -> int list list type iist = istate option * istate option
289 val ins_chn : ctree list -> ctree -> int list -> ctree
290 val insert_pt : ppobj -> ctree -> int list -> ctree val is_e_ctxt : Proof.context -> bool
291 val is_empty_tac : tac -> bool val is_interpos : 'a * pos_ -> bool val is_pblnd : ctree -> bool
292 val is_pblobj : ppobj -> bool val is_pblobj' : ctree -> int list -> bool val is_rewset : tac -> bool
293 val is_rewtac : tac -> bool datatype istate = RrlsState of rrlsstate | ScrState of scrstate | Uistate
294 val istate2str : istate -> string val istates2str : istate option * istate option -> string
295 val just_created : ctree * (int list * 'a) -> bool val just_created_ : ppobj -> bool
296 val lev_on : int list -> int list val lev_pred' : ctree -> int list * pos_ -> int list * pos_
297 val lev_up : int list -> pos val move_dn : int list -> ctree -> int list * pos_ -> int list * pos_
298 val move_up : int list -> ctree -> int list * pos_ -> int list * pos_
299 val movecalchd_up : ctree -> int list * pos_ -> int list * pos_
300 val movelevel_dn : int list -> ctree -> int list * pos_ -> int list * pos_
301 val movelevel_up : int list -> ctree -> int list * 'a -> int list * pos_
302 val new_val : term -> istate -> istate val nth : int -> 'a list -> 'a
303 type ocalhd = bool * pos_ * term * itm list * (bool * term) list * spec
305 bool * pos_ * term * itm list * (bool * term) list * (string * string list * string list) -> string
306 datatype ostate = Complete | Incomplete | Inconsistent val ostate2str : ostate -> string
307 val par_pbl_det : ctree -> int list -> bool * int list * rls
308 val par_pblobj : ctree -> int list -> int list type pos = int list type pos' = pos * pos_
309 val pos'2str : int list * pos_ -> string val pos's2str : (int list * pos_) list -> string
310 val pos2str : int list -> string datatype pos_ = Frm | Met | Pbl | Res | Und
311 val pos_2str : pos_ -> string eqtype posel
317 env: (istate * Proof.context) option,
319 loc: (istate * Proof.context) option * (istate * Proof.context) option,
321 origin: ori list * spec * term, ostate: ostate, probl: itm list, Selem.result: Selem.result, spec: spec}
326 loc: (istate * Proof.context) option * (istate * Proof.context) option,
327 ostate: ostate, Selem.result: Selem.result, tac: tac}
328 val pr_ctree : (int list -> ppobj -> string) -> ctree -> string val pr_pos : int list -> string
329 val pr_short : int list -> ppobj -> string val preconds2str : (bool * term) list -> string
330 datatype ptform = Form of term | ModSpec of ocalhd val repl : 'a list -> int -> 'a -> 'a list
331 val repl_app : 'a list -> int -> 'a -> 'a list
332 type result = term * term list val rls_of : tac -> rls' val rootthy : ctree -> theory
333 val rta2str : rule * (term * term list) -> string
334 val rule2tac : theory -> (term * term) list -> rule -> tac
335 datatype safe = Helpless | Safe | Selem.Sundef | Unsafe
336 val safe2str : safe -> string
337 type scrstate = env * loc_ * term option * term * safe * bool
338 type state = ctree * pos'
339 val str2pos_ : string -> pos_ type sube = cterm' list val sube2str : string list -> string
340 val sube2subst : theory -> string list -> (term * term) list val sube2subte : string list -> term list
341 type subs = cterm' list val subs2subst : theory -> string list -> (term * term) list
342 val subst2sube : (term * term) list -> string list val subst2subs : (term * term) list -> string list
343 val subst2subs' : (term * term) list -> (string * string) list type subte = term list
344 val subte2sube : term list -> string list val subte2subst : term list -> (term * term) list
346 = Add_Find of cterm' | Add_Given of cterm' | Add_Relation of cterm' | Apply_Assumption of cterm' list
347 | Apply_Method of metID | Begin_Sequ | Begin_Trans | CAScmd of cterm' | Calculate of string
348 | Check_Postcond of pblID | Check_elementwise of cterm' | Collect_Trues | Conclude_And | Conclude_Or
349 | Del_Find of cterm' | Del_Given of cterm' | Del_Relation of cterm' | Derive of rls'
350 | Detail_Set of rls' | Detail_Set_Inst of subs * rls' | Empty_Tac | End_Detail | End_Intersect
351 | End_Proof' | End_Ruleset | End_Sequ | End_Subproblem | End_Trans | Free_Solve
352 | Init_Proof of cterm' list * spec | Model_Problem | Or_to_List | Refine_Problem of pblID
353 | Refine_Tacitly of pblID | Rewrite of thm'' | Rewrite_Asm of thm'' | Rewrite_Inst of subs * thm''
354 | Rewrite_Set of rls' | Rewrite_Set_Inst of subs * rls' | Specify_Method of metID
355 | Specify_Problem of pblID | Specify_Theory of domID | Split_And | Split_Intersect | Split_Or
356 | Subproblem of domID * pblID | Substitute of sube | Tac of string | Take of cterm'
357 | Take_Inst of cterm'
358 val tac2IDstr : tac -> string val tac2str : tac -> string
360 = Add_Find' of cterm' * itm list | Add_Given' of cterm' * itm list | Add_Relation' of cterm' * itm list
361 | Apply_Assumption' of term list * term
362 | Apply_Method' of metID * term option * istate * Proof.context | Begin_Sequ' | Begin_Trans' of term
363 | CAScmd' of term | Calculate' of theory' * string * term * (term * thm')
364 | Check_Postcond' of pblID * Selem.result | Check_elementwise' of term * string * Selem.result
365 | Collect_Trues' of term | Conclude_And' of term | Conclude_Or' of term | Del_Find' of cterm'
366 | Del_Given' of cterm' | Del_Relation' of cterm' | Derive' of rls
367 | Detail_Set' of theory' * bool * rls * term * Selem.result
368 | Detail_Set_Inst' of theory' * bool * subst * rls * term * Selem.result | Empty_Tac_
369 | End_Detail' of Selem.result | End_Intersect' of term | End_Proof'' | End_Ruleset' of term | End_Sequ'
370 | End_Subproblem' of term | End_Trans' of Selem.result | Free_Solve' | Init_Proof' of cterm' list * spec
371 | Model_Problem' of pblID * itm list * itm list | Or_to_List' of term * term
372 | Refine_Problem' of pblID * (itm list * (bool * term) list)
373 | Refine_Tacitly' of pblID * pblID * domID * metID * itm list
374 | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * Selem.result
375 | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * Selem.result
376 | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * Selem.result
377 | Rewrite_Set' of theory' * bool * rls * term * Selem.result
378 | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * Selem.result
379 | Specify_Method' of metID * ori list * itm list
380 | Specify_Problem' of pblID * (bool * (itm list * (bool * term) list)) | Specify_Theory' of domID
381 | Split_And' of term | Split_Intersect' of term | Split_Or' of term
382 | Subproblem' of spec * ori list * term * fmz_ * Proof.context * term
383 | Substitute' of rew_ord_ * rls * subte * term * term | Tac_ of theory * string * string * string
384 | Take' of term | Take_Inst' of term
385 val tac_2str : tac_ -> string val test_trans : ppobj -> bool val topt2str : term option -> string end*)
388 structure CTbasic(**): BASIC_CALC_TREE(**) =
391 type env = (term * term) list;
394 NoBranch | AndB | OrB
395 | TransitiveB (* FIXXXME.0308: set branch from met in Apply_Method
396 FIXXXME.0402: -"- in Begin_Trans'*)
397 | SequenceB | IntersectB | CollectB | MapB;
399 fun branch2str NoBranch = "NoBranch" (* for tests only *)
400 | branch2str AndB = "AndB"
401 | branch2str OrB = "OrB"
402 | branch2str TransitiveB = "TransitiveB"
403 | branch2str SequenceB = "SequenceB"
404 | branch2str IntersectB = "IntersectB"
405 | branch2str CollectB = "CollectB"
406 | branch2str MapB = "MapB";
409 Incomplete | Complete | Inconsistent (* WN041020 latter still unused *);
410 fun ostate2str Incomplete = "Incomplete" (* for tests only *)
411 | ostate2str Complete = "Complete"
412 | ostate2str Inconsistent = "Inconsistent";
415 type cid = cellID list;
417 type posel = int; (* for readability in funs accessing Ctree *)
419 val pos2str = ints2str';
421 Pbl (* PblObj-position: problem-type *)
422 | Met (* PblObj-position: method *)
423 | Frm (* PblObj-position: -> Pbl in ME (not by moveDown !)
424 | PrfObj-position: formula *)
425 | Res (* PblObj | PrfObj-position: result *)
426 | Und; (* undefined*)
427 fun pos_2str Pbl = "Pbl"
428 | pos_2str Met = "Met"
429 | pos_2str Frm = "Frm"
430 | pos_2str Res = "Res"
431 | pos_2str Und = "Und";
432 fun str2pos_ "Pbl" = Pbl
433 | str2pos_ "Met" = Met
434 | str2pos_ "Frm" = Frm
435 | str2pos_ "Res" = Res
436 | str2pos_ "Und" = Und
437 | str2pos_ str = error ("str2pos_: wrong argument = " ^ str)
439 type pos' = pos * pos_;
440 (*WN0312 remembering interator (pos * pos_) for ctree
441 pos : lev_on, lev_dn, lev_up
443 # generate1 sets pos_ if possible ...?WN0502?NOT...
444 # generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn
445 exceptions: Begin/End_Trans
446 # thus generate(1) called in
448 .# nxt_solv (tac_ -cases); general case:
449 val pos' = case pos' of (p,Res) => (lev_on p',Res) | _ => pos'
451 generate1...(Rewrite(f,..,res))..(pos, pos_)
452 cappend_atomic.................pos ////// gets f+res always!!!
453 cut_tree....................pos, pos_
455 fun pos'2str (p, p_) = pair2str (ints2str' p, pos_2str p_);
456 fun pos's2str ps = (strs2str' o (map pos'2str)) ps; (* for tests only *)
457 val e_pos' = ([], Und);
459 type subs = cterm' list; (*16.11.00 for FE-KE*)
460 val e_subs = ["(bdv, x)"]; (* for tests only *)
462 (* argument type of tac Rewrite_Inst *)
463 type sube = cterm' list;
464 val e_sube = []: cterm' list; (* for tests only *)
465 fun sube2str s = strs2str s;
467 (* _sub_stitution as _t_erms of _e_qualities *)
468 type subte = term list;
470 val subte2sube = map term2str;
471 val subst2subs = map (pair2str o (apfst term2str) o (apsnd term2str));
472 fun subst2sube subst = map term2str (map HOLogic.mk_eq subst)
473 val subst2subs' = map ((apfst term2str) o (apsnd term2str));
474 fun subs2subst thy s = map (isapair2pair o (parse_patt thy)) s;
475 fun sube2subst thy s = map (dest_equals' o (parse_patt thy)) s;
476 val sube2subte = map str2term;
477 val subte2subst = map HOLogic.dest_eq;
478 val e_ctxt = Proof_Context.init_global @{theory "Pure"};
480 (* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*)
481 fun is_e_ctxt ctxt = Theory.eq_thy (Proof_Context.theory_of ctxt, @{theory "Pure"});
483 type iist = Selem.istate option * Selem.istate option;
484 (*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*)
487 fun new_val v (Selem.ScrState (env, loc_, topt, _, safe, bool)) =
488 (Selem.ScrState (env, loc_, topt, v, safe, bool))
489 | new_val _ _ = error "new_val: only for ScrState";
491 datatype con = land | lor;
493 (* tactics for user at front-end.
494 tac propagates the construction of the calc-tree;
496 (a) 'specsteps' for the specify-phase, and others for the solve-phase
497 (b) those of the solve-phase are 'initac's and others;
498 initacs start with a formula different from the preceding formula.
499 see 'type tac_' for the internal representation of tactics
500 TODO.WN161219: replace *every* cterm' by term
503 Add_Find of cterm' | Add_Given of cterm' | Add_Relation of cterm'
504 | Apply_Assumption of cterm' list
505 | Apply_Method of metID
506 (* creates an "istate" in PblObj.env; in case of "init_form"
507 creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
508 a "SOME istate" at fst of "loc".
509 As each step (in the solve-phase) has a resulting formula (at the front-end)
510 Apply_Method also does the 1st step in the script (an "initac") if there is no "init_form" *)
511 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
512 | Begin_Sequ | Begin_Trans
513 | Split_And | Split_Or | Split_Intersect
514 | Conclude_And | Conclude_Or | Collect_Trues
515 | End_Sequ | End_Trans
516 | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'
517 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
519 | Calculate of string
520 | Check_Postcond of pblID
521 | Check_elementwise of cterm'
522 | Del_Find of cterm' | Del_Given of cterm' | Del_Relation of cterm'
524 | Derive of rls' (* WN0509 drop *)
525 | Detail_Set of rls' (* WN0509 drop *)
526 | Detail_Set_Inst of subs * rls' (* WN0509 drop *)
527 | End_Detail (* WN0509 drop *)
532 | Init_Proof of cterm' list * spec
535 | Refine_Problem of pblID
536 | Refine_Tacitly of pblID
538 (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
539 because there all the thms are present with both (thmID, thm)
540 (where user-views can show both or only one of (thmID, thm)),
541 and thm is created from ThmID by assoc_thm'' when entering isabisac *)
543 | Rewrite_Asm of thm''
544 | Rewrite_Inst of subs * thm''
545 | Rewrite_Set of rls'
546 | Rewrite_Set_Inst of subs * rls'
548 | Specify_Method of metID
549 | Specify_Problem of pblID
550 | Specify_Theory of domID
551 | Subproblem of domID * pblID (* WN0509 drop *)
554 | Tac of string (* WN0509 drop *)
555 | Take of cterm' | Take_Inst of cterm'
557 fun tac2str ma = case ma of
558 Init_Proof (ppc, spec) =>
559 "Init_Proof "^(pair2str (strs2str ppc, spec2str spec))
560 | Model_Problem => "Model_Problem "
561 | Refine_Tacitly pblID => "Refine_Tacitly " ^ strs2str pblID
562 | Refine_Problem pblID => "Refine_Problem " ^ strs2str pblID
563 | Add_Given cterm' => "Add_Given " ^ cterm'
564 | Del_Given cterm' => "Del_Given " ^ cterm'
565 | Add_Find cterm' => "Add_Find " ^ cterm'
566 | Del_Find cterm' => "Del_Find " ^ cterm'
567 | Add_Relation cterm' => "Add_Relation " ^ cterm'
568 | Del_Relation cterm' => "Del_Relation " ^ cterm'
570 | Specify_Theory domID => "Specify_Theory " ^ quote domID
571 | Specify_Problem pblID => "Specify_Problem " ^ strs2str pblID
572 | Specify_Method metID => "Specify_Method " ^ strs2str metID
573 | Apply_Method metID => "Apply_Method " ^ strs2str metID
574 | Check_Postcond pblID => "Check_Postcond " ^ strs2str pblID
575 | Free_Solve => "Free_Solve"
577 | Rewrite_Inst (subs, (id, thm)) =>
578 "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> term2str)))
579 | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> term2str)
580 | Rewrite_Asm (id, thm) => "Rewrite_Asm " ^ spair2str (id, thm |> Thm.prop_of |> term2str)
581 | Rewrite_Set_Inst (subs, rls) =>
582 "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
583 | Rewrite_Set rls => "Rewrite_Set " ^ quote rls
584 | Detail_Set rls => "Detail_Set " ^ quote rls
585 | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls)
586 | End_Detail => "End_Detail"
587 | Derive rls' => "Derive " ^ rls'
588 | Calculate op_ => "Calculate " ^ op_
589 | Substitute sube => "Substitute " ^ sube2str sube
590 | Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's
592 | Take cterm' => "Take " ^ quote cterm'
593 | Take_Inst cterm' => "Take_Inst " ^ quote cterm'
594 | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
595 | End_Subproblem => "End_Subproblem"
596 | CAScmd cterm' => "CAScmd " ^ quote cterm'
598 | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
599 | Or_to_List => "Or_to_List "
600 | Collect_Trues => "Collect_Trues"
602 | Empty_Tac => "Empty_Tac"
603 | Tac string => "Tac " ^ string
604 | End_Proof' => "tac End_Proof'"
605 | _ => "tac2str not impl. for ?!";
607 fun is_empty_tac tac = case tac of Empty_Tac => true | _ => false
609 fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
610 | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
611 | eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2
612 | eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2
613 | eq_tac (Calculate id1, Calculate id2) = id1 = id2
616 fun is_rewset (Rewrite_Set_Inst _) = true
617 | is_rewset (Rewrite_Set _) = true
618 | is_rewset _ = false;
619 fun is_rewtac (Rewrite _) = true
620 | is_rewtac (Rewrite_Inst _) = true
621 | is_rewtac (Rewrite_Asm _) = true
622 | is_rewtac tac = is_rewset tac;
624 fun tac2IDstr ma = case ma of
625 Model_Problem => "Model_Problem"
626 | Refine_Tacitly _ => "Refine_Tacitly"
627 | Refine_Problem _ => "Refine_Problem"
628 | Add_Given _ => "Add_Given"
629 | Del_Given _ => "Del_Given"
630 | Add_Find _ => "Add_Find"
631 | Del_Find _ => "Del_Find"
632 | Add_Relation _ => "Add_Relation"
633 | Del_Relation _ => "Del_Relation"
635 | Specify_Theory _ => "Specify_Theory"
636 | Specify_Problem _ => "Specify_Problem"
637 | Specify_Method _ => "Specify_Method"
638 | Apply_Method _ => "Apply_Method"
639 | Check_Postcond _ => "Check_Postcond"
640 | Free_Solve => "Free_Solve"
642 | Rewrite_Inst _ => "Rewrite_Inst"
643 | Rewrite _ => "Rewrite"
644 | Rewrite_Asm _ => "Rewrite_Asm"
645 | Rewrite_Set_Inst _ => "Rewrite_Set_Inst"
646 | Rewrite_Set _ => "Rewrite_Set"
647 | Detail_Set _ => "Detail_Set"
648 | Detail_Set_Inst _ => "Detail_Set_Inst"
649 | Derive _ => "Derive "
650 | Calculate _ => "Calculate "
651 | Substitute _ => "Substitute"
652 | Apply_Assumption _ => "Apply_Assumption"
655 | Take_Inst _ => "Take_Inst"
656 | Subproblem _ => "Subproblem"
657 | End_Subproblem => "End_Subproblem"
658 | CAScmd _ => "CAScmd"
660 | Check_elementwise _ => "Check_elementwise"
661 | Or_to_List => "Or_to_List "
662 | Collect_Trues => "Collect_Trues"
664 | Empty_Tac => "Empty_Tac"
666 | End_Proof' => "End_Proof'"
667 | _ => "tac2str not impl. for ?!";
669 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
670 | rls_of (Rewrite_Set rls) = rls
671 | rls_of tac = error ("rls_of: called with tac \"" ^ tac2IDstr tac ^ "\"");
673 fun rule2tac thy _ (Calc (opID, thm)) = Calculate (assoc_calc thy opID)
674 | rule2tac _ [] (Thm thm'') = Rewrite thm''
675 | rule2tac _ subst (Thm thm'') =
676 Rewrite_Inst (subst2subs subst, thm'')
677 | rule2tac _ [] (Rls_ rls) = Rewrite_Set (id_rls rls)
678 | rule2tac _ subst (Rls_ rls) =
679 Rewrite_Set_Inst (subst2subs subst, (id_rls rls))
680 | rule2tac _ _ rule =
681 error ("rule2tac: called with \"" ^ rule2str rule ^ "\"");
683 (* tactics for for internal use, compare "tac" for user at the front-end.
684 tac_ contains results from check in 'fun applicable_in'.
685 This is useful for costly results, e.g. from rewriting;
686 however, these results might be changed by Scripts like
687 " eq = (Rewrite_Set ansatz_rls False) eql;" ^
688 " eq = drop_questionmarks eq;" ^
689 " eq = (Rewrite_Set equival_trans False) eq;" ^
690 TODO.WN120106 ANALOGOUSLY TO Substitute':
691 So tac_ contains the term t the result was calculated from
692 in order to compare t with t' possibly changed by "Expr "
693 and re-calculate result if t<>t'
694 TODO.WN161219: replace *every* cterm' by term
697 Add_Find' of cterm' * itm list | Add_Given' of cterm' * itm list | Add_Relation' of cterm' * itm list
698 | Apply_Assumption' of term list * term
699 | Apply_Method' of metID * term option * Selem.istate * Proof.context
700 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
701 | Begin_Sequ' | Begin_Trans' of term
702 | Split_And' of term | Split_Or' of term | Split_Intersect' of term
703 | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
704 | End_Sequ' | End_Trans' of Selem.result
705 | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''
706 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
708 | Calculate' of theory' * string * term * (term * thm')
709 | Check_Postcond' of pblID *
710 Selem.result (* returnvalue of script in solve *)
711 | Check_elementwise' of (*special case:*)
712 term * (* (1) the current formula: [x=1,x=...] *)
713 string * (* (2) the pred from Check_elementwise *)
714 Selem.result (* (3) composed from (1) and (2): {x. pred} *)
715 | Del_Find' of cterm' | Del_Given' of cterm' | Del_Relation' of cterm'
718 | Detail_Set' of theory' * bool * rls * term * Selem.result
719 | Detail_Set_Inst' of theory' * bool * subst * rls * term * Selem.result
720 | End_Detail' of Selem.result
725 | Init_Proof' of cterm' list * spec
726 | Model_Problem' of pblID *
727 itm list * (* the 'untouched' pbl *)
728 itm list (* the casually completed met *)
729 | Or_to_List' of term * term
730 | Refine_Problem' of pblID * (itm list * (bool * term) list)
733 pblID * (* the refined from applicable_in *)
734 domID * (* from new pbt?! filled in specify *)
735 metID * (* from new pbt?! filled in specify *)
736 itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
737 | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * Selem.result
738 | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * Selem.result
739 | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * Selem.result
740 | Rewrite_Set' of theory' * bool * rls * term * Selem.result
741 | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * Selem.result
743 | Specify_Method' of metID * ori list * itm list
744 | Specify_Problem' of pblID *
745 (bool * (* matches *)
746 (itm list * (* ppc *)
747 (bool * term) list)) (* preconditions *)
748 | Specify_Theory' of domID
751 (ori list) * (* filled in assod Subproblem' *)
752 term * (* -"-, headline of calc-head *)
754 Proof.context * (* transported from assod to generate1*)
755 term (* Subproblem(dom,pbl) OR cascmd *)
757 rew_ord_ * (* for re-calculation *)
758 rls * (* for re-calculation *)
759 subte * (* the 'substitution': terms of type bool *)
760 term * (* to be substituted in *)
761 term (* resulting from the substitution *)
762 | Tac_ of theory * string * string * string
763 | Take' of term | Take_Inst' of term
765 fun tac_2str ma = case ma of
766 Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, spec2str spec)
767 | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
768 | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
769 strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
770 | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"
771 | Add_Given' _ => "Add_Given' "(*^cterm'*)
772 | Del_Given' _ => "Del_Given' "(*^cterm'*)
773 | Add_Find' _ => "Add_Find' "(*^cterm'*)
774 | Del_Find' _ => "Del_Find' "(*^cterm'*)
775 | Add_Relation' _ => "Add_Relation' "(*^cterm'*)
776 | Del_Relation' _ => "Del_Relation' "(*^cterm'*)
778 | Specify_Theory' domID => "Specify_Theory' " ^ quote domID
779 | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
780 spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
781 | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
782 metID2str pI ^ ", " ^ oris2str oris ^ ", )"
784 | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
785 | Check_Postcond' (pblID, (scval, asm)) => "Check_Postcond' " ^
786 (spair2str (strs2str pblID, spair2str (term2str scval, terms2str asm)))
788 | Free_Solve' => "Free_Solve'"
790 | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
791 | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
792 | Rewrite_Asm' _(*thm'*) => "Rewrite_Asm' "(*^(spair2str thm')*)
793 | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
794 | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
795 "," ^ id_rls rls' ^ "," ^ term2str f ^ ",(" ^ term2str f' ^ "," ^ terms2str asm ^ "))"
796 | End_Detail' _ => "End_Detail' xxx"
797 | Detail_Set' _ => "Detail_Set' xxx"
798 | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
800 | Derive' rls => "Derive' " ^ id_rls rls
801 | Calculate' _ => "Calculate' "
802 | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
803 | Apply_Assumption' _(* ct's*) => "Apply_Assumption' "(*^(strs2str ct's)*)
805 | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*)
806 | Take_Inst' _(*cterm'*) => "Take_Inst' "(*^(quote cterm' )*)
807 | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) =>
808 "Subproblem' "(*^(pair2str (domID, strs2str ,))*)
809 | End_Subproblem' _ => "End_Subproblem'"
810 | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*)
812 | Empty_Tac_ => "Empty_Tac_"
813 | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"
814 | _ => "tac_2str not impl. for arg";
816 (* executed tactics (tac_s) with local environment etc.;
817 used for continuing eval script + for generate *)
819 (loc_ * (* of tactic in scr, tactic (weakly) associated with tac_ *)
820 (tac_ * (* (for generate) *)
821 env * (* with 'tactic=result' as rule, tactic ev. _not_ ready: for handling 'parallel let'*)
822 env * (* with results of (ready) tacs *)
823 term * (* itr_arg of tactic, for upd. env at Repeat, Try *)
824 term * (* result value of the tac *)
828 fun ets2s (l,(m,eno,env,iar,res,s)) =
829 "\n(" ^ loc_2str l ^ ",(" ^ tac_2str m ^
830 ",\n ens= " ^ subst2str eno ^
831 ",\n env= " ^ subst2str env ^
832 ",\n iar= " ^ term2str iar ^
833 ",\n res= " ^ term2str res ^
834 ",\n " ^ Selem.safe2str s ^ "))";
835 fun ets2str (ets: ets) = (strs2str o (map ets2s)) ets; (* for tests only *)
837 type envp =(*9.5.03: unused, delete with field in ctree.PblObj FIXXXME*)
838 (int * term list) list * (* assoc-list: args of met*)
839 (int * rls) list * (* assoc-list: tacs already done ///15.9.00*)
840 (int * ets) list * (* assoc-list: tacs etc. already done*)
841 (string * pos) list; (* asms * from where*)
843 datatype ppobj = (* TODO: arrange according to signature *)
845 {cell : lrd option, (* where in form tac has been applied, FIXME.WN0607 rename field *)
846 form : term, (* where tac is applied to *)
847 tac : tac, (* also in istate *)
848 loc : (Selem.istate * (* script interpreter state *)
849 Proof.context) (* context for provers, type inference *)
850 option * (* both for interpreter location on Frm, Pbl, Met *)
851 (Selem.istate * (* script interpreter state *)
852 Proof.context) (* context for provers, type inference *)
853 option, (* both for interpreter location on Res *)
854 (*(NONE,NONE) <==> e_istate ! see update_loc, get_loc *)
855 branch: branch, (* only rudimentary *)
856 result: Selem.result, (* result and assumptions *)
857 ostate: ostate} (* Complete <=> result is OK *)
859 {cell : lrd option, (* unused: meaningful only for some _Prf_Obj *)
860 fmz : Selem.fmz, (* from init:FIXME never use this spec;-drop *)
861 origin: (ori list) * (* representation from fmz+pbt
862 for efficiently adding items in probl, meth *)
863 spec * (* updated by Refine_Tacitly *)
864 term, (* headline of calc-head, as calculated initially(!) *)
865 spec : spec, (* explicitly input *)
866 probl : itm list, (* itms explicitly input *)
867 meth : itm list, (* itms automatically added to copy of probl *)
868 ctxt : Proof.context, (* WN110513 introduced to avoid [*] [**] *)
869 env : (Selem.istate * Proof.context) option, (* istate only for initac in script
870 context for specify phase on this node NO..
871 ..NO: this conflicts with init_form/initac: see Apply_Method without init_form *)
872 loc : (Selem.istate * Proof.context) option * (Selem.istate * (* like PrfObj *)
873 Proof.context) option, (* for spec-phase [*], NO..
874 ..NO: raises errors not tracable on WN110513 [**] *)
875 branch: branch, (* like PrfObj *)
876 result: Selem.result, (* like PrfObj *)
877 ostate: ostate}; (* like PrfObj *)
879 (* this tree contains isac's calculations;
880 the tree's structure has been copied from an early version of Theorema(c);
881 it has the disadvantage, that there is no space
882 for the first tactic in a script generating the first formula at (p,Frm);
883 this trouble has been covered by 'init_form' and 'Take' so far,
884 but it is crucial if the first tactic in a script is eg. 'Subproblem';
885 see 'type tac', Apply_Method.
889 | Nd of ppobj * (ctree list);
890 val e_ctree = EmptyPtree;
891 type state = ctree * pos'
893 fun is_pblobj (PblObj _) = true
894 | is_pblobj _ = false;
896 exception PTREE of string;
897 fun nth _ [] = raise PTREE "nth _ []"
899 | nth n (_ :: xs) = nth (n - 1) xs;
900 (*> nth 2 [11,22,33]; -->> val it = 22 : int*)
903 (** convert ctree to a string **)
905 (* convert a pos from list to string *)
906 fun pr_pos ps = (space_implode "." (map string_of_int ps))^". ";
907 (* show hd origin or form only *)
908 fun pr_short p (PblObj _) = pr_pos p ^ " ----- pblobj -----\n" (* for tests only *)
909 | pr_short p (PrfObj {form = form, ...}) = pr_pos p ^ term2str form ^ "\n";
910 fun pr_ctree f pt = (* for tests only *)
912 fun pr_pt _ _ EmptyPtree = ""
913 | pr_pt pfn ps (Nd (b, [])) = pfn ps b
914 | pr_pt pfn ps (Nd (b, ts)) = pfn ps b ^ prts pfn ps 1 ts
915 and prts _ _ _ [] = ""
916 | prts pfn ps p (t :: ts) = (pr_pt pfn (ps @ [p]) t)^
917 (prts pfn ps (p + 1) ts)
918 in pr_pt f [] pt end;
920 (** access the branches of ctree **)
922 fun repl [] _ _ = raise PTREE "repl [] _ _"
923 | repl (_ :: ls) 1 e = e :: ls
924 | repl (l :: ls) n e = l :: (repl ls (n-1) e);
925 fun repl_app ls n e =
927 val lim = 1 + length ls
930 then raise PTREE "repl_app: n > lim"
933 else repl ls n e end;
935 (* get from obj at pos by f : ppobj -> 'a *)
936 fun get_obj _ EmptyPtree _ = raise PTREE "get_obj f EmptyPtree"
937 | get_obj f (Nd (b, _)) [] = f b
938 | get_obj f (Nd (_, bs)) (p :: ps) =
941 handle _ => raise PTREE ("get_obj: pos = " ^ ints2str' (p::ps) ^ " does not exist");
943 (get_obj f (nth p bs) ps)
944 handle _ => raise PTREE ("get_obj: pos = " ^ ints2str' (p::ps) ^ " does not exist")
946 fun get_nd EmptyPtree _ = raise PTREE "get_nd EmptyPtree"
948 | get_nd (Nd (_, nds)) (pos as p :: ps) = (get_nd (nth p nds) ps)
949 handle _ => raise PTREE ("get_nd: not existent pos = " ^ ints2str' pos);
951 (* for use by get_obj *)
952 fun g_form (PrfObj {form = f,...}) = f
953 | g_form (PblObj {origin= (_,_,f),...}) = f;
954 fun g_form' (Nd (PrfObj {form = f, ...}, _)) = f
955 | g_form' (Nd (PblObj {origin= (_, _, f),...}, _)) = f
956 | g_form' _ = error "g_form': uncovered fun def.";
957 (* | g_form _ = raise PTREE "g_form not for PblObj";*)
958 fun g_origin (PblObj {origin = ori, ...}) = ori
959 | g_origin _ = raise PTREE "g_origin not for PrfObj";
960 fun g_fmz (PblObj {fmz = f, ...}) = f (* for tests only *)
961 | g_fmz _ = raise PTREE "g_fmz not for PrfObj";
962 fun g_spec (PblObj {spec = s, ...}) = s
963 | g_spec _ = raise PTREE "g_spec not for PrfObj";
964 fun g_pbl (PblObj {probl = p, ...}) = p
965 | g_pbl _ = raise PTREE "g_pbl not for PrfObj";
966 fun g_met (PblObj {meth = p, ...}) = p
967 | g_met _ = raise PTREE "g_met not for PrfObj";
968 fun g_domID (PblObj {spec = (d, _, _), ...}) = d
969 | g_domID _ = raise PTREE "g_metID not for PrfObj";
970 fun g_metID (PblObj {spec = (_, _, m), ...}) = m
971 | g_metID _ = raise PTREE "g_metID not for PrfObj";
972 fun g_ctxt (PblObj {ctxt, ...}) = ctxt
973 | g_ctxt _ = raise PTREE "g_ctxt not for PrfObj";
974 fun g_env (PblObj {env, ...}) = env
975 | g_env _ = raise PTREE "g_env not for PrfObj";
976 fun g_loc (PblObj {loc = l, ...}) = l
977 | g_loc (PrfObj {loc = l, ...}) = l;
978 fun g_branch (PblObj {branch = b, ...}) = b
979 | g_branch (PrfObj {branch = b, ...}) = b;
980 fun g_tac (PblObj {spec = (_, _, m),...}) = Apply_Method m
981 | g_tac (PrfObj {tac = m, ...}) = m;
982 fun g_result (PblObj {result = r, ...}) = r
983 | g_result (PrfObj {result = r, ...}) = r;
984 fun g_res (PblObj {result = (r, _) ,...}) = r
985 | g_res (PrfObj {result = (r, _),...}) = r;
986 fun g_res' (Nd (PblObj {result = (r, _), ...}, _)) = r
987 | g_res' (Nd (PrfObj {result = (r, _),...}, _)) = r
988 | g_res' _ = raise PTREE "g_res': uncovered fun def.";
989 fun g_ostate (PblObj {ostate = r, ...}) = r
990 | g_ostate (PrfObj {ostate = r, ...}) = r;
991 fun g_ostate' (Nd (PblObj {ostate = r, ...}, _)) = r
992 | g_ostate' (Nd (PrfObj {ostate = r, ...}, _)) = r
993 | g_ostate' _ = raise PTREE "g_ostate': uncovered fun def.";
995 (* get the formula preceeding the current position in a calculation *)
996 fun get_curr_formula (pt, (p, p_)) =
998 Frm => get_obj g_form pt p
999 | Res => (fst o (get_obj g_result pt)) p
1000 | _ => #3 (get_obj g_origin pt p);
1002 (* in CalcTree/Subproblem an 'just_created_' model is created;
1003 this is filled to 'untouched' by Model/Refine_Problem *)
1004 fun just_created_ (PblObj {meth, probl, spec, ...}) =
1005 null meth andalso null probl andalso spec = e_spec
1006 | just_created_ _ = raise PTREE "g_ostate': uncovered fun def.";
1007 val e_origin = ([],e_spec,e_term);
1009 fun just_created (pt, (p, _)) =
1010 let val ppobj = get_obj I pt p
1011 in is_pblobj ppobj andalso just_created_ ppobj end;
1013 (* does the pos in the ctree exist ? *)
1014 fun existpt pos pt = can (get_obj I pt) pos;
1015 (* does the pos' in the ctree exist, ie. extra check for result in the node *)
1016 fun existpt' (p, p_) pt =
1017 if can (get_obj I pt) p
1019 Res => get_obj g_ostate pt p = Complete
1023 (* is this position appropriate for calculating intermediate steps? *)
1024 fun is_interpos (_, Res) = true
1025 | is_interpos _ = false;
1027 (* get the children of a node in ctree *)
1028 fun children (Nd (PblObj _, cn)) = cn
1029 | children (Nd (PrfObj _, cn)) = cn
1030 | children _ = error "children: uncovered fun def.";
1032 (*/--------------- duplicates in ctree-navi.sml: required also here below ---------------\*)
1033 fun lev_on [] = raise PTREE "lev_on []"
1035 let val len = length pos
1036 in (drop_last pos) @ [(nth len pos)+1] end;
1037 fun lev_up [] = raise PTREE "lev_up []"
1038 | lev_up p = (drop_last p):pos;
1039 (* find the position of the next parent which is a PblObj in ctree *)
1040 fun par_pblobj _ [] = []
1045 if is_pblobj (get_obj I pt p)
1047 else par pt (lev_up p)
1048 in par pt (lev_up p) end;
1049 (*\--------------- duplicates in ctree-navi.sml: required also here below ---------------/*)
1051 (* find the next parent, which is either a PblObj (return true)
1052 or a PrfObj with tac = Detail_Set (return false)
1053 FIXME.030403: re-organize par_pbl_det after rls' --> rls*)
1054 fun par_pbl_det pt [] = (true, [], Erls)
1055 | par_pbl_det pt p =
1057 fun par _ [] = (true, [], Erls)
1059 if is_pblobj (get_obj I pt p)
1060 then (true, p, Erls)
1061 else case get_obj g_tac pt p of
1062 Rewrite_Set rls' => (false, p, assoc_rls rls')
1063 | Rewrite_Set_Inst (_, rls') => (false, p, assoc_rls rls')
1064 | _ => par pt (lev_up p)
1065 in par pt (lev_up p) end;
1067 (* insert obj b into ctree at pos, ev.overwriting this pos *)
1068 fun insert_pt b EmptyPtree [] = Nd (b, [])
1069 | insert_pt _ EmptyPtree _ = raise PTREE "insert_pt b Empty _"
1070 | insert_pt _ (Nd ( _, _)) [] = raise PTREE "insert_pt b _ []"
1071 | insert_pt b (Nd (b', bs)) (p :: []) = Nd (b', repl_app bs p (Nd (b, [])))
1072 | insert_pt b (Nd (b', bs)) (p :: ps) = Nd (b', repl_app bs p (insert_pt b (nth p bs) ps));
1074 (* insert children to a node without children. compare: fun insert_pt *)
1075 fun ins_chn _ EmptyPtree _ = raise PTREE "ins_chn: EmptyPtree"
1076 | ins_chn _ (Nd _) [] = raise PTREE "ins_chn: pos = []"
1077 | ins_chn ns (Nd (b, bs)) (p :: []) =
1079 then raise PTREE "ins_chn: pos not existent"
1082 val (b', bs') = case nth p bs of
1083 Nd (b', bs') => (b', bs')
1084 | _ => error "ins_chn: uncovered case nth"
1087 then Nd (b, repl_app bs p (Nd (b', ns)))
1088 else raise PTREE "ins_chn: pos mustNOT be overwritten"
1090 | ins_chn ns (Nd (b, bs)) (p::ps) = Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps));
1092 (* apply f to obj at pos, f: ppobj -> ppobj *)
1093 fun appl_to_node f (Nd (b, bs)) = Nd (f b, bs)
1094 | appl_to_node _ _ = error "appl_to_node: uncovered fun def.";
1095 fun appl_obj _ EmptyPtree [] = EmptyPtree
1096 | appl_obj _ EmptyPtree _ = raise PTREE "appl_obj f Empty _"
1097 | appl_obj f (Nd (b, bs)) [] = Nd (f b, bs)
1098 | appl_obj f (Nd (b, bs)) (p :: []) = Nd (b, repl_app bs p (((appl_to_node f) o (nth p)) bs))
1099 | appl_obj f (Nd (b, bs)) (p :: ps) = Nd (b, repl_app bs p (appl_obj f (nth p bs) (ps:pos)));
1103 bool * (* ALL itms+preconds true *)
1104 pos_ * (* model belongs to Problem | Method *)
1105 term * (* header: Problem... or Cas FIXME.0312: item for marking syntaxerrors *)
1106 itm list * (* model: given, find, relate *)
1107 ((bool * term) list) *(* model: preconds *)
1108 spec; (* specification *)
1109 val e_ocalhd = (false, Und, e_term, [e_itm], [(false, e_term)], e_spec);
1111 datatype ptform = Form of term | ModSpec of ocalhd;
1113 (* for cut_level; (deprecated) *)
1114 fun test_trans (PrfObj {branch, ...}) = true andalso branch = TransitiveB
1115 | test_trans (PblObj {branch, ...}) = true andalso branch = TransitiveB;
1117 fun is_pblobj' pt p =
1118 let val ppobj = get_obj I pt p
1119 in is_pblobj ppobj end;
1121 fun del_res (PblObj {cell, fmz, origin, spec, probl, meth, ctxt, env, loc= (l1, _), branch, ...}) =
1122 PblObj {cell = cell, fmz = fmz, origin = origin, spec = spec, probl = probl, meth = meth,
1123 ctxt = ctxt, env = env, loc= (l1, NONE), branch = branch,
1124 result = (e_term, []), ostate = Incomplete}
1125 | del_res (PrfObj {cell, form, tac, loc= (l1, _), branch, ...}) =
1126 PrfObj {cell = cell, form = form, tac = tac, loc = (l1, NONE), branch = branch,
1127 result = (e_term, []), ostate = Incomplete};
1130 fun get_loc EmptyPtree _ = (Selem.e_istate, e_ctxt)
1131 | get_loc pt (p, Res) =
1132 (case get_obj g_loc pt p of
1134 | (NONE , NONE) => (Selem.e_istate, e_ctxt)
1135 | (_ , SOME i) => i)
1136 | get_loc pt (p, _) =
1137 (case get_obj g_loc pt p of
1138 (NONE , SOME i) => i (*13.8.02 just copied from ^^^: too liberal ?*)
1139 | (NONE , NONE) => (Selem.e_istate, e_ctxt)
1140 | (SOME i, _) => i);
1141 fun get_istate pt p = get_loc pt p |> #1;
1142 fun get_ctxt pt (pos as (p, p_)) =
1143 if member op = [Frm, Res] p_
1144 then get_loc pt pos |> #2 (*for script interpretation rely on fun get_loc*)
1145 else get_obj g_ctxt pt p (*for specify phase take ctx from PblObj*)
1147 fun get_assumptions_ pt p = get_ctxt pt p |> get_assumptions;
1149 fun get_somespec' (dI, pI, mI) (dI', pI', mI') =
1151 val domID = if dI = e_domID then dI' else dI
1152 val pblID = if pI = e_pblID then pI' else pI
1153 val metID = if mI = e_metID then mI' else mI
1154 in (domID, pblID, metID) end;
1156 (**.development for extracting an 'interval' from ptree.**)
1158 (*WN0510 version stopped in favour of get_interval with !!!move_dn, getFormulaeFromTo
1159 actually used (inefficient) version with move_dn: see modspec.sml*)
1162 fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*)
1163 fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)
1164 fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x;
1165 fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
1167 fun getnd i (b,p) q (Nd (po, nds)) =
1168 (if i <= 0 then [[b]] else []) @
1169 (getnds (i-1) true (b@[hdp p], tlp p) (tlq q)
1170 (take_fromto (hdp p) (hdq q) nds))
1172 and getnds _ _ _ _ [] = [] (*no children*)
1173 | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)
1175 | getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*)
1176 (getnd i ( b, p ) [99999] n1) @
1177 (getnd ~99999 (lev_on b,[0]) q n2)
1179 | getnds i _ (b,p) q [n1, n2] = (*intern, r-margin*)
1180 (getnd i ( b,[0]) [99999] n1) @
1181 (getnd ~99999 (lev_on b,[0]) q n2)
1183 | getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*)
1184 (getnd i ( b, p ) [99999] nd) @
1185 (getnds ~99999 false (lev_on b,[0]) q nds)
1187 | getnds i _ (b,p) q (nd::(nds as _::_)) = (*intern, ...*)
1188 (getnd i ( b,[0]) [99999] nd) @
1189 (getnds ~99999 false (lev_on b,[0]) q nds);
1191 (*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes
1192 where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
1193 (1) the 'f' are given
1194 (1a) by 'from' if 'f' = the respective element of 'from' (left margin)
1195 (1b) -inifinity, if 'f' > the respective element of 'from' (internal node)
1196 (2) the 't' ar given
1197 (2a) by 'to' if 't' = the respective element of 'to' (right margin)
1198 (2b) inifinity, if 't' < the respective element of 'to (internal node)'
1199 the 'f' and 't' are set by hdp,... *)
1200 fun get_trace pt p q =
1201 (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q)))
1202 (take_fromto (hdp p) (hdq q) (children pt));
1205 (*extract a formula or model from ctree for itms2itemppc or model2xml*)
1206 fun preconds2str bts =
1207 (strs2str o (map (linefeed o pair2str o
1209 (apfst bool2str)))) bts;
1210 fun ocalhd2str (b, p, hdf, itms, prec, spec) = (* for tests only *)
1211 "(" ^ bool2str b ^ ", " ^ pos_2str p ^ ", " ^ term2str hdf ^
1212 ", " ^ itms2str_ (thy2ctxt' "Isac") itms ^
1213 ", " ^ preconds2str prec ^ ", \n" ^ spec2str spec ^ " )";
1215 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj
1216 | is_pblnd _ = error "is_pblnd: uncovered fun def.";
1219 (* determine the previous pos' on the same level
1220 WN0502 made for interSteps; _only_ works for branch TransitiveB WN120517 compare lev_back *)
1221 fun lev_pred' _ ([], Res) = ([], Pbl)
1222 | lev_pred' pt (p, Res) =
1223 let val (p', last) = split_last p
1226 then if (is_pblobj o (get_obj I pt)) p then (p, Pbl) else (p, Frm)
1227 else if get_obj g_res pt (p' @ [last - 1]) = get_obj g_form pt p
1228 then (p' @ [last - 1], Res) (* TransitiveB *)
1229 else if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm)
1231 | lev_pred' _ _ = error "";
1234 (**.insert into ctree and cut branches accordingly.**)
1236 (* get all positions of certain intervals on the ctree.
1237 OLD VERSION without move_dn; kept for occasional redesign
1238 get all pos's to be cut in a ctree
1239 below a pos or from a ctree list after i-th element (NO level_up) *)
1240 fun get_allpos' (_, _) EmptyPtree = []
1241 | get_allpos' (p, 1) (Nd (b, bs)) = (* p is pos of Nd *)
1242 if g_ostate b = Incomplete
1243 then (p, Frm) :: (get_allpos's (p, 1) bs)
1244 else (p, Frm) :: (get_allpos's (p, 1) bs) @ [(p, Res)]
1245 | get_allpos' (p, i) (Nd (b, bs)) = (* p is pos of Nd *)
1246 if length bs > 0 orelse is_pblobj b
1247 then if g_ostate b = Incomplete
1248 then [(p,Frm)] @ (get_allpos's (p, 1) bs)
1249 else [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p, Res)]
1250 else if g_ostate b = Incomplete then [] else [(p, Res)]
1251 and get_allpos's _ [] = []
1252 | get_allpos's (p, i) (pt :: pts) = (* p is pos of parent-Nd *)
1253 (get_allpos' (p @ [i], i) pt) @ (get_allpos's (p, i + 1) pts);
1255 (*WN050106 like cut_level, but deletes exactly 1 node *)
1256 fun cut_level_'_ _ _ EmptyPtree _ =raise PTREE "cut_level_'_ Empty _" (* for tests ONLY *)
1257 | cut_level_'_ _ _ (Nd ( _, _)) ([], _) = raise PTREE "cut_level_'_ _ []"
1258 | cut_level_'_ cuts P (Nd (b, bs)) (p :: [], p_) =
1261 (Nd (b, drop_nth [] (p:posel, bs)),
1262 cuts @ (if p_ = Frm then [(P @ [p], Res)] else []) @
1263 (get_allpos's (P, p + 1) (drop_nth [] (p, bs))))
1264 else (Nd (b, bs), cuts)
1265 | cut_level_'_ cuts P (Nd (b, bs)) ((p :: ps), p_) =
1267 val (bs', cuts') = cut_level_'_ cuts P (nth p bs) (ps, p_)
1268 in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
1270 fun cut_level _ _ EmptyPtree _ = raise PTREE "cut_level EmptyPtree _"
1271 | cut_level _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level _ []"
1272 | cut_level cuts P (Nd (b, bs)) (p :: [], p_) =
1275 (Nd (b, take (p:posel, bs)),
1277 (if p_ = Frm andalso (*#*) g_ostate b = Complete then [(P@[p],Res)] else ([]:pos' list)) @
1278 (get_allpos's (P, p+1) (takerest (p, bs))))
1279 else (Nd (b, bs), cuts)
1280 | cut_level cuts P (Nd (b, bs)) ((p :: ps), p_) =
1282 val (bs', cuts') = cut_level cuts P (nth p bs) (ps, p_)
1283 in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
1285 (*OLD version before WN050219, overwritten below*)
1286 fun cut_tree _ ([], _) = raise PTREE "cut_tree _ ([],_)" (* for test only *)
1287 | cut_tree pt (pos as ([_], _)) =
1289 val (pt', cuts) = cut_level [] [] pt pos
1291 (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete then [] else [([], Res)]))
1293 | cut_tree pt (p,p_) =
1295 fun cutfn pt cuts (p, p_) =
1297 val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_)
1299 if length cuts' > 0 andalso length p > 1
1300 then cutfn pt' (cuts @ cuts') (lev_up p, Frm(*-->(p,Res)*))
1301 else (pt', cuts @ cuts')
1303 val (pt', cuts) = cutfn pt [] (p, p_)
1305 (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete then [] else [([], Res)]))
1309 fun move_dn _ (Nd (_, ns)) ([],p_) = (* root problem *)
1311 Res => raise PTREE "move_dn: end of calculation"
1313 if null ns (* go down from Pbl + Met *)
1314 then raise PTREE "move_dn: solve problem not started"
1316 | move_dn P (Nd (_, ns)) (p :: (ps as (_ :: _)), p_) = (* iterate to end of pos *)
1318 then raise PTREE "move_dn: pos not existent 2"
1319 else move_dn (P @ [p]) (nth p ns) (ps, p_)
1320 | move_dn P (Nd (c, ns)) ([p], p_) = (* act on last element of pos *)
1322 then raise PTREE "move_dn: pos not existent 3"
1326 if p = length ns (* last Res on this level: go a level up *)
1327 then if g_ostate c = Complete
1329 else raise PTREE (ints2str' P ^ " not complete 1")
1330 else (* go to the next Nd on this level, or down into the next Nd *)
1331 if is_pblnd (nth (p + 1) ns) then (P@[p + 1], Pbl)
1332 else if g_res' (nth p ns) = g_form' (nth (p + 1) ns)
1333 then if (null o children o (nth (p + 1))) ns
1334 then (* take the Res if Complete *)
1335 if g_ostate' (nth (p + 1) ns) = Complete
1336 then (P@[p + 1], Res)
1337 else raise PTREE (ints2str' (P@[p + 1]) ^ " not complete 2")
1338 else (P@[p + 1, 1], Frm) (* go down into the next PrfObj *)
1339 else (P@[p + 1], Frm) (* take Frm: exists if the Nd exists *)
1340 | Frm => (*go down or to the Res of this Nd*)
1341 if (null o children o (nth p)) ns
1342 then if g_ostate' (nth p ns) = Complete then (P @ [p], Res)
1343 else raise PTREE (ints2str' (P @ [p])^" not complete 3")
1344 else (P @ [p, 1], Frm)
1345 | _ => (* is Pbl or Met *)
1346 if (null o children o (nth p)) ns
1347 then raise PTREE "move_dn:solve subproblem not startd"
1349 if (is_pblnd o hd o children o (nth p)) ns
1351 | move_dn _ _ _ = error "";
1353 (* get all positions in a ctree until ([],Res) or ostate=Incomplete
1355 pos' list -> : accumulated, start with []
1356 pos -> : the offset for subtrees wrt the root
1357 ctree -> : (sub)tree
1358 pos' : initialization (the last pos' before ...)
1359 -> pos' list : of positions in this (sub) tree (relative to the root)
1361 fun get_allp cuts (P, pos) pt =
1363 val nxt = move_dn [] pt pos (*exn if Incomplete reached*)
1366 then get_allp (cuts @ [nxt]) (P, nxt) pt
1367 else map (apfst (curry op @ P)) (cuts @ [nxt])
1369 handle PTREE _ => (map (apfst (curry op@ P)) cuts);
1372 (* the pts are assumed to be on the same level *)
1373 fun get_allps cuts _ [] = cuts
1374 | get_allps cuts P (pt :: pts) =
1376 val below = get_allp [] (P, ([], Frm)) pt
1379 then (P, Pbl) :: below
1380 else if last_elem P = 1
1381 then (P, Frm) :: below
1382 else (*Trans*) below
1383 val levres = levfrm @ (if null below then [(P, Res)] else [])
1385 get_allps (cuts @ levres) (lev_on P) pts
1388 (** these 2 funs decide on how far cut_tree goes **)
1389 (* shall the nodes _after_ the pos to be inserted at be deleted?
1390 shall cutting be continued on the higher level(s)? the Nd regarded will NOT be changed *)
1391 fun test_trans (PrfObj {branch, ...}) = (branch = TransitiveB orelse branch = NoBranch)
1392 | test_trans (PblObj {branch, ...}) = (branch = TransitiveB orelse branch = NoBranch);
1394 (* cut_bottom new sml603..608
1395 cut the level at the bottom of the pos (used by cappend_...)
1396 and handle the parent in order to avoid extra case for root
1397 fn: ctree -> : the _whole_ ctree for cut_levup
1398 pos * posel -> : the pos after split_last
1399 ctree -> : the parent of the Nd to be cut
1401 (ctree * : the updated ctree
1402 pos' list) * : the pos's cut
1403 bool : cutting shall be continued on the higher level(s)
1405 fun cut_bottom _ (pt' as Nd (b, [])) = ((pt', []), test_trans b)
1406 | cut_bottom (P, p) (Nd (b, bs)) =
1407 let (*divide level into 3 parts...*)
1408 val keep = take (p - 1, bs)
1409 val pt' = case nth p bs of
1411 | _ => error "cut_bottom: uncovered case nth p bs"
1412 (*^^^^^_here_ will be 'insert_pt'ed by 'append_..'*)
1413 val (tail, _) = (takerest (p, bs), if null (takerest (p, bs)) then 0 else p + 1)
1414 val (children, cuts) =
1417 (keep, (if is_pblnd pt' then [(P @ [p], Pbl)] else [])
1418 @ (get_allp [] (P @ [p], (P, Frm)) pt')
1419 @ (get_allps [] (P @ [p + 1]) tail))
1420 else (keep @ [(*'insert_pt'ed by 'append_..'*)] @ tail,
1421 get_allp [] (P @ [p], (P, Frm)) pt')
1424 then (Nd (del_res b, children), cuts @ (if g_ostate b = Incomplete then [] else [(P, Res)]))
1425 else (Nd (b, children), cuts)
1426 in ((pt'', cuts), test_trans b) end
1427 | cut_bottom _ _ = error "cut_bottom: uncovered fun def.";
1430 (* go all levels from the bottom of 'pos' up to the root,
1431 on each level compose the children of a node and accumulate the cut Nds
1433 pos' list -> : for accumulation
1434 bool -> : cutting shall be continued on the higher level(s)
1435 ctree -> : the whole ctree for 'get_nd pt P' on each level
1436 ctree -> : the Nd from the lower level for insertion at path
1437 pos * posel -> : pos=path split for convenience
1438 ctree -> : Nd the children of are under consideration on this call
1440 ctree * pos' list : the updated parent-Nd and the pos's of the Nds cut
1442 fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) =
1443 let (*divide level into 3 parts...*)
1444 val keep = take (p - 1, bs)
1445 (*val pt' comes as argument from below*)
1447 (takerest (p, bs), if null (takerest (p, bs)) then 0 else p + 1)
1448 val (children, cuts') =
1450 then (keep @ [pt'], get_allps [] (P @ [p+1]) tail)
1451 else (keep @ [pt'] @ tail, [])
1452 val clevup' = if clevup then test_trans b else false
1453 (*the first Nd with false stops cutting on all levels above*)
1456 then (Nd (del_res b, children), cuts' @ (if g_ostate b = Incomplete then [] else [(P, Res)]))
1457 else (Nd (b, children), cuts')
1460 then (pt'', cuts @ cuts')
1462 let val (P, p) = split_last P
1463 in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P) end
1465 | cut_levup _ _ _ _ _ _ = error "cut_levup: uncovered fun def.";
1467 (* cut nodes after and below an inserted node in the ctree;
1468 the cuts range is limited by the predicate 'fun cutlevup' *)
1469 fun cut_tree pt (pos, _) =
1470 if not (existpt pos pt)
1471 then (pt,[]) (*appending a formula never cuts anything*)
1474 val (P, p) = split_last pos
1475 val ((pt', cuts), clevup) = cut_bottom (P, p) (get_nd pt P)
1476 (* pt' is the updated parent of the Nd to cappend_..*)
1481 let val (P, p) = split_last P
1482 in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P) end
1485 (* get the theory explicitly specified for the rootpbl;
1486 thus use this function _after_ finishing specification *)
1487 fun rootthy (Nd (PblObj {spec = (thyID, _, _), ...}, _)) = assoc_thy thyID
1488 | rootthy _ = error "rootthy: uncovered fun def.";