Walther@60704: (* Title: the calctree, which holds a calculation Walther@60704: Author: Walther Neuper 1999 Walther@60704: (c) due to copyright terms Walther@60704: Walther@60704: Definitions required for Ctree, renamed later appropriately Walther@60704: -------------------------vvvvv + I_Model.T-TEST are the only difference to Walther@60704: BASIC_CALC_TREE Walther@60704: *) Walther@60704: Walther@60771: signature BASIC_CALC_TREE_POS = Walther@60704: sig Walther@60704: (**** signature ****) Walther@60704: (** the basic datatype **) Walther@60704: type state Walther@60704: val e_state: state Walther@60704: Walther@60704: type con Walther@60704: eqtype cellID Walther@60704: Walther@60704: datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB Walther@60704: datatype ostate = Complete | Incomplete | Inconsistent Walther@60704: type specify_data Walther@60704: type solve_data Walther@60704: datatype ppobj = PblObj of specify_data | PrfObj of solve_data Walther@60704: datatype ctree = EmptyPtree | Nd of ppobj * ctree list Walther@60704: Walther@60704: val rep_solve_data: ppobj -> solve_data Walther@60704: val rep_specify_data: ppobj -> specify_data Walther@60704: Walther@60704: (** basic functions **) Walther@60704: val e_ctree : ctree (* TODO: replace by EmptyPtree*) Walther@60704: val existpt' : Pos.pos' -> ctree -> bool Walther@60704: val is_interpos : Pos.pos' -> bool Walther@60704: val lev_pred' : ctree -> Pos.pos' -> Pos.pos' Walther@60704: val ins_chn : ctree list -> ctree -> Pos.pos -> ctree Walther@60704: val children : ctree -> ctree list Walther@60704: val get_nd : ctree -> Pos.pos -> ctree Walther@60704: val just_created_ : ppobj -> bool Walther@60704: val just_created : state -> bool Walther@60704: val e_origin : Model_Def.o_model * References_Def.T * term Walther@60704: Walther@60704: val is_pblobj : ppobj -> bool Walther@60704: val is_pblobj' : ctree -> Pos.pos -> bool Walther@60704: val is_pblnd : ctree -> bool Walther@60704: Walther@60704: val g_spec : ppobj -> References_Def.T Walther@60704: val g_loc : ppobj -> (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option Walther@60704: val g_form : ppobj -> term Walther@60771: val g_pbl : ppobj -> Model_Def.i_model_POS Walther@60771: val g_met : ppobj -> Model_Def.i_model_POS Walther@60704: val g_metID : ppobj -> MethodC.id Walther@60704: val g_result : ppobj -> Celem.result Walther@60704: val g_tac : ppobj -> Tactic.input Walther@60704: val g_domID : ppobj -> ThyC.id Walther@60704: Walther@60704: val g_origin : ppobj -> Model_Def.o_model * References_Def.T * term Walther@60704: val get_loc : ctree -> Pos.pos' -> Istate_Def.T * Proof.context Walther@60704: val get_istate_LI : ctree -> Pos.pos' -> Istate_Def.T Walther@60704: val get_ctxt_LI: ctree -> Pos.pos' -> Proof.context Walther@60704: val get_ctxt : ctree -> Pos.pos' -> Proof.context (*DEPRECATED*) Walther@60704: val get_obj : (ppobj -> 'a) -> ctree -> Pos.pos -> 'a Walther@60704: val get_curr_formula : state -> term Walther@60704: val get_assumptions : ctree -> Pos.pos' -> term list Walther@60704: Walther@60704: val new_val : term -> Istate_Def.T -> Istate_Def.T Walther@60704: Walther@60704: type cid = cellID list Walther@60704: datatype ptform = Form of term | ModSpec of Specification_Def.T Walther@60704: val get_somespec' : References_Def.T -> References_Def.T -> References_Def.T Walther@60704: exception PTREE of string; Walther@60704: Walther@60704: val root_thy : ctree -> theory Walther@60704: (* ---- made visible ONLY for structure CTaccess : CALC_TREE_ACCESS --------------------------- *) Walther@60704: val appl_obj : (ppobj -> ppobj) -> ctree -> Pos.pos -> ctree Walther@60704: val existpt : Pos.pos -> ctree -> bool Walther@60704: val cut_tree : ctree -> Pos.pos * 'a -> ctree * Pos.pos' list Walther@60704: val insert_pt : ppobj -> ctree -> int list -> ctree Walther@60704: (* ---- made visible ONLY for structure CTnavi : CALC_TREE_NAVIGATION ------------------------- *) Walther@60704: val g_branch : ppobj -> branch Walther@60704: val g_form' : ctree -> term Walther@60704: val g_ostate : ppobj -> ostate Walther@60704: val g_ostate' : ctree -> ostate Walther@60704: val g_res : ppobj -> term Walther@60704: val g_res' : ctree -> term Walther@60704: (*/---- duplicates in CTnavi, reconsider structs ----------------------------------------------- Walther@60704: val lev_dn : CTbasic.Pos.pos -> Pos.pos (* duplicate in ctree-navi.sml *) Walther@60704: val par_pblobj : CTbasic.ctree -> Pos.pos -> Pos.pos (* duplicate in ctree-navi.sml *) Walther@60704: ---- duplicates in CTnavi, reconsider structs ----------------------------------------------/*) Walther@60704: (*from isac_test for Minisubpbl*) Walther@60704: val pr_ctree: Proof.context -> (Proof.context -> int list -> ppobj -> string) -> ctree -> string Walther@60704: val pr_short: Proof.context -> Pos.pos -> ppobj -> string Walther@60704: Walther@60704: \<^isac_test>\ Walther@60704: val g_ctxt : ppobj -> Proof.context Walther@60704: val g_fmz : ppobj -> Model_Def.form_T Walther@60704: val get_allp : Pos.pos' list -> Pos.pos * (int list * Pos.pos_) -> ctree -> Pos.pos' list Walther@60704: val get_allps : (Pos.pos * Pos.pos_) list -> Pos.posel list -> ctree list -> Pos.pos' list Walther@60704: val get_allpos' : Pos.pos * Pos.posel -> ctree -> Pos.pos' list Walther@60704: val get_allpos's : Pos.pos * Pos.posel -> ctree list -> (Pos.pos * Pos.pos_) list Walther@60704: val cut_bottom : Pos.pos * Pos.posel -> ctree -> (ctree * Pos.pos' list) * bool Walther@60704: val cut_level : Pos.pos' list -> Pos.pos -> ctree -> int list * Pos.pos_ -> ctree * Pos.pos' list Walther@60704: val cut_level__ : Pos.pos' list -> Pos.pos -> ctree -> int list * Pos.pos_ -> ctree * Pos.pos' list Walther@60704: val get_trace : ctree -> int list -> int list -> int list list Walther@60704: val branch2str : branch -> string Walther@60704: \ Walther@60704: end Walther@60704: Walther@60704: (**) Walther@60771: structure CTbasic_POS(**): BASIC_CALC_TREE_POS(**) = Walther@60704: struct Walther@60704: (**) Walther@60704: open Pos Walther@60704: Walther@60704: (**** Ctree ****) Walther@60704: Walther@60704: (*** general types* **) Walther@60704: Walther@60704: datatype branch = Walther@60704: NoBranch | AndB | OrB Walther@60704: | TransitiveB (* FIXXXME.0308: set branch from met in Apply_Method Walther@60704: FIXXXME.0402: -"- in Begin_Trans'*) Walther@60704: | SequenceB | IntersectB | CollectB | MapB; Walther@60704: Walther@60704: \<^isac_test>\ Walther@60704: fun branch2str NoBranch = "NoBranch" Walther@60704: | branch2str AndB = "AndB" Walther@60704: | branch2str OrB = "OrB" Walther@60704: | branch2str TransitiveB = "TransitiveB" Walther@60704: | branch2str SequenceB = "SequenceB" Walther@60704: | branch2str IntersectB = "IntersectB" Walther@60704: | branch2str CollectB = "CollectB" Walther@60704: | branch2str MapB = "MapB"; Walther@60704: \ Walther@60704: Walther@60704: datatype ostate = Walther@60704: Incomplete | Complete | Inconsistent (* WN041020 latter still unused *); Walther@60704: \<^isac_test>\ Walther@60704: fun ostate2str Incomplete = "Incomplete" Walther@60704: | ostate2str Complete = "Complete" Walther@60704: | ostate2str Inconsistent = "Inconsistent"; Walther@60704: \ Walther@60704: Walther@60704: type cellID = int; Walther@60704: type cid = cellID list; Walther@60704: Walther@60704: Walther@60704: type iist = Istate_Def.T option * Istate_Def.T option; Walther@60704: (*val e_iist = (empty, empty); --- sinnlos f"ur NICHT-equality-type*) Walther@60704: Walther@60704: Walther@60704: fun new_val v (Istate_Def.Pstate pst) = Walther@60704: (Istate_Def.Pstate (Istate_Def.set_act v pst)) Walther@60704: | new_val _ _ = raise ERROR "new_val: only for Pstate"; Walther@60704: Walther@60704: datatype con = land | lor; Walther@60704: Walther@60704: (* executed tactics (tac_s) with local environment etc.; Walther@60704: used for continuing eval script + for generate *) Walther@60704: type ets = Walther@60704: (TermC.path *(* of tactic in program, tactic (weakly) associated with tac_ *) Walther@60704: (Tactic.T * (* (for generate) *) Walther@60704: Env.T * (* with 'tactic=result' as rule, tactic ev. _not_ ready for 'parallel let' *) Walther@60704: Env.T * (* with results of (ready) tacs *) Walther@60704: term * (* itr_arg of tactic, for upd. env at Repeat, Try *) Walther@60704: term * (* result value of the tac *) Walther@60704: Celem.safe)) Walther@60704: list; Walther@60704: Walther@60704: type envp =(*9.5.03: unused, delete with field in ctree.PblObj FIXXXME*) Walther@60704: (int * term list) list * (* assoc-list: args of met*) Walther@60704: (int * Rule_Set.T) list * (* assoc-list: tacs already done ///15.9.00*) Walther@60704: (int * ets) list * (* assoc-list: tacs etc. already done*) Walther@60704: (string * pos) list; (* asms * from where*) Walther@60704: Walther@60704: Walther@60704: (*** type Ctree ***) Walther@60704: Walther@60704: type specify_data = Walther@60704: {fmz : Model_Def.form_T, (* for uniformity also created/used for/by Subproblem *) Walther@60704: origin: (Model_Def.o_model) *(* = O_Model.T for efficiently checking input to I_Model *) Walther@60704: References_Def.T * (* updated by Refine_Tacitly *) Walther@60704: term, (* headline of calc-head, as calculated initially(!) *) Walther@60704: spec : References_Def.T, (* explicitly input *) Walther@60771: probl : Model_Def.i_model_POS,(* = I_Model.T for interactive input to a Problem *) Walther@60771: meth : Model_Def.i_model_POS,(* = I_Model.T for interactive input to a MethodC *) Walther@60704: ctxt : Proof.context, (* used while specifying this (Sub-)Problem and MethodC *) Walther@60704: loc : (Istate_Def.T * Proof.context) option (* like in PrfObj, calling this SubProblem *) Walther@60704: * (Istate_Def.T * Proof.context) option, (* like in PrfObj, finishing the SubProblem *) Walther@60704: branch: branch, (* like PrfObj *) Walther@60704: result: Celem.result, (* like PrfObj *) Walther@60704: ostate: ostate}; (* like PrfObj *) Walther@60704: type solve_data = (* TODO: arrange according to signature *) Walther@60704: {form : term, (* where tactic is applied to *) Walther@60704: tac : Tactic.input, (* tactic as presented to users *) Walther@60704: loc : (Istate_Def.T * (* program interpreter state *) Walther@60704: Proof.context) (* context for provers, type inference *) Walther@60704: option * (* both for interpreter location on Frm, Pbl, Met *) Walther@60704: (Istate_Def.T * (* script interpreter state *) Walther@60704: Proof.context) (* context for provers, type inference *) Walther@60704: option, (* both for interpreter location on Res, (NONE,NONE) == empty *) Walther@60704: branch: branch, (* only rudimentary *) Walther@60704: result: Celem.result, (* result and assumptions *) Walther@60704: ostate: ostate} (* Complete <=> result is OK *) Walther@60704: Walther@60704: datatype ppobj = Walther@60704: PblObj of specify_data (* data serving a whole specification-phase *) Walther@60704: | PrfObj of solve_data; (* data for a proof step triggered by a tactic *) Walther@60704: Walther@60704: (* this tree contains isac's calculations; Walther@60704: the tree's structure has been copied from an early version of Theorema(c); Walther@60704: it has the disadvantage, that there is no space Walther@60704: for the first tactic in a script generating the first formula at (p,Frm); Walther@60704: this trouble has been covered by 'implicit_take' and 'Take' so far, Walther@60704: but it is crucial if the first tactic in a script is eg. 'Subproblem'; Walther@60704: see 'type tac', Apply_Method. Walther@60704: *) Walther@60704: datatype ctree = Walther@60704: EmptyPtree Walther@60704: | Nd of ppobj * (ctree list); Walther@60704: val e_ctree = EmptyPtree; Walther@60704: type state = ctree * pos' Walther@60704: val e_state = (EmptyPtree , e_pos') Walther@60704: Walther@60704: fun rep_solve_data (PrfObj solve_data) = solve_data Walther@60704: | rep_solve_data _ = raise ERROR "rep_solve_data ONLY for solve_data" Walther@60704: fun rep_specify_data (PblObj specify_data) = specify_data Walther@60704: | rep_specify_data _ = raise ERROR "rep_solve_data ONLY for solve_data" Walther@60704: Walther@60704: Walther@60704: (*** minimal set of functions on Ctree* **) Walther@60704: Walther@60704: fun is_pblobj (PblObj _) = true Walther@60704: | is_pblobj _ = false; Walther@60704: Walther@60704: exception PTREE of string; Walther@60704: fun nth _ [] = raise PTREE "nth _ []" Walther@60704: | nth 1 (x :: _) = x Walther@60704: | nth n (_ :: xs) = nth (n - 1) xs; Walther@60704: (*> nth 2 [11,22,33]; -->> val it = 22 : int*) Walther@60704: Walther@60704: Walther@60704: (** convert ctree to a string **) Walther@60704: Walther@60704: (* convert a pos from list to string *) Walther@60704: fun pr_pos ps = (space_implode "." (map string_of_int ps)) ^ ". "; Walther@60704: (* show hd origin or form only *) Walther@60704: (**) Walther@60704: fun pr_short _ p (PblObj _) = pr_pos p ^ " ----- pblobj -----\n" Walther@60704: | pr_short ctxt p (PrfObj {form = form, ...}) = pr_pos p ^ UnparseC.term ctxt form ^ "\n"; Walther@60704: fun pr_ctree ctxt f pt = Walther@60704: let Walther@60704: fun pr_pt _ _ EmptyPtree = "" Walther@60704: | pr_pt pfn ps (Nd (b, [])) = pfn ps b Walther@60704: | pr_pt pfn ps (Nd (b, ts)) = pfn ps b ^ prts pfn ps 1 ts Walther@60704: and prts _ _ _ [] = "" Walther@60704: | prts pfn ps p (t :: ts) = (pr_pt pfn (ps @ [p]) t)^ Walther@60704: (prts pfn ps (p + 1) ts) Walther@60704: in pr_pt (f ctxt) [] pt end; Walther@60704: Walther@60704: Walther@60704: Walther@60704: (** access the branches of ctree **) Walther@60704: Walther@60704: fun repl [] _ _ = raise PTREE "repl [] _ _" Walther@60704: | repl (_ :: ls) 1 e = e :: ls Walther@60704: | repl (l :: ls) n e = l :: (repl ls (n-1) e); Walther@60704: fun repl_app ls n e = Walther@60704: let Walther@60704: val lim = 1 + length ls Walther@60704: in Walther@60704: if n > lim Walther@60704: then raise PTREE "repl_app: n > lim" Walther@60704: else if n = lim Walther@60704: then ls @ [e] Walther@60704: else repl ls n e end; Walther@60704: Walther@60704: (* get from obj at pos by f : ppobj -> 'a *) Walther@60704: fun get_obj _ EmptyPtree _ = raise PTREE "get_obj f EmptyPtree" Walther@60704: | get_obj f (Nd (b, _)) [] = f b Walther@60704: | get_obj f (Nd (_, bs)) (p :: ps) = Walther@60704: case \<^try>\ get_obj f (nth p bs) ps \ of Walther@60704: SOME obj => obj Walther@60704: | NONE => raise PTREE ("get_obj: pos = " ^ ints2str' (p :: ps) ^ " does not exist"); Walther@60704: fun get_nd EmptyPtree _ = raise PTREE "get_nd EmptyPtree" Walther@60704: | get_nd n [] = n Walther@60704: | get_nd (Nd (_, nds)) (pos as p :: ps) = Walther@60704: case \<^try>\ get_nd (nth p nds) ps \ of Walther@60704: SOME nd => nd Walther@60704: | NONE => raise PTREE ("get_nd: not existent pos = " ^ ints2str' pos); Walther@60704: Walther@60704: (* for use by get_obj *) Walther@60704: fun g_form (PrfObj {form = f,...}) = f Walther@60704: | g_form (PblObj {origin= (_,_,f),...}) = f; Walther@60704: fun g_form' (Nd (PrfObj {form = f, ...}, _)) = f Walther@60704: | g_form' (Nd (PblObj {origin= (_, _, f),...}, _)) = f Walther@60704: | g_form' _ = raise ERROR "g_form': uncovered fun def."; Walther@60704: (* | g_form _ = raise PTREE "g_form not for PblObj";*) Walther@60704: fun g_origin (PblObj {origin = ori, ...}) = ori Walther@60704: | g_origin _ = raise PTREE "g_origin not for PrfObj"; Walther@60704: \<^isac_test>\ Walther@60704: fun g_fmz (PblObj {fmz = f, ...}) = f Walther@60704: | g_fmz _ = raise PTREE "g_fmz not for PrfObj"; Walther@60704: \ Walther@60704: fun g_spec (PblObj {spec = s, ...}) = s Walther@60704: | g_spec _ = raise PTREE "g_spec not for PrfObj"; Walther@60704: fun g_pbl (PblObj {probl = p, ...}) = p Walther@60704: | g_pbl _ = raise PTREE "g_pbl not for PrfObj"; Walther@60704: fun g_met (PblObj {meth = p, ...}) = p Walther@60704: | g_met _ = raise PTREE "g_met not for PrfObj"; Walther@60704: fun g_domID (PblObj {spec = (d, _, _), ...}) = d Walther@60704: | g_domID _ = raise PTREE "g_metID not for PrfObj"; Walther@60704: fun g_metID (PblObj {spec = (_, _, m), ...}) = m Walther@60704: | g_metID _ = raise PTREE "g_metID not for PrfObj"; Walther@60704: fun g_ctxt (PblObj {ctxt, ...}) = ctxt Walther@60704: | g_ctxt _ = raise PTREE "g_ctxt not for PrfObj"; Walther@60704: fun g_loc (PblObj {loc = l, ...}) = l Walther@60704: | g_loc (PrfObj {loc = l, ...}) = l; Walther@60704: fun g_branch (PblObj {branch = b, ...}) = b Walther@60704: | g_branch (PrfObj {branch = b, ...}) = b; Walther@60704: fun g_tac (PblObj {spec = (_, _, m),...}) = Tactic.Apply_Method m Walther@60704: | g_tac (PrfObj {tac = m, ...}) = m; Walther@60704: fun g_result (PblObj {result = r, ...}) = r Walther@60704: | g_result (PrfObj {result = r, ...}) = r; Walther@60704: fun g_res (PblObj {result = (r, _) ,...}) = r Walther@60704: | g_res (PrfObj {result = (r, _),...}) = r; Walther@60704: fun g_res' (Nd (PblObj {result = (r, _), ...}, _)) = r Walther@60704: | g_res' (Nd (PrfObj {result = (r, _),...}, _)) = r Walther@60704: | g_res' _ = raise PTREE "g_res': uncovered fun def."; Walther@60704: fun g_ostate (PblObj {ostate = r, ...}) = r Walther@60704: | g_ostate (PrfObj {ostate = r, ...}) = r; Walther@60704: fun g_ostate' (Nd (PblObj {ostate = r, ...}, _)) = r Walther@60704: | g_ostate' (Nd (PrfObj {ostate = r, ...}, _)) = r Walther@60704: | g_ostate' _ = raise PTREE "g_ostate': uncovered fun def."; Walther@60704: Walther@60704: (* get the formula preceeding the current position in a calculation *) Walther@60704: fun get_curr_formula (pt, (p, p_)) = Walther@60704: case p_ of Walther@60704: Frm => get_obj g_form pt p Walther@60704: | Res => (fst o (get_obj g_result pt)) p Walther@60704: | _ => #3 (get_obj g_origin pt p); (* the headline*) Walther@60704: Walther@60704: (* in CalcTree/Subproblem an 'just_created_' model is created; Walther@60704: this is filled to 'untouched' by Model/Refine_Problem *) Walther@60704: fun just_created_ (PblObj {meth, probl, spec, ...}) = Walther@60704: null meth andalso null probl andalso spec = References_Def.empty Walther@60704: | just_created_ _ = raise PTREE "g_ostate': uncovered fun def."; Walther@60704: val e_origin = ([], References_Def.empty, TermC.empty); Walther@60704: Walther@60704: fun just_created (pt, (p, _)) = Walther@60704: let val ppobj = get_obj I pt p Walther@60704: in is_pblobj ppobj andalso just_created_ ppobj end; Walther@60704: Walther@60704: (* does the pos in the ctree exist ? *) Walther@60704: fun existpt pos pt = can (get_obj I pt) pos; Walther@60704: (* does the pos' in the ctree exist, ie. extra check for result in the node *) Walther@60704: fun existpt' (p, p_) pt = Walther@60704: if can (get_obj I pt) p Walther@60704: then case p_ of Walther@60704: Res => get_obj g_ostate pt p = Complete Walther@60704: | _ => true Walther@60704: else false; Walther@60704: Walther@60704: (* is this position appropriate for calculating intermediate steps? *) Walther@60704: fun is_interpos (_, Res) = true Walther@60704: | is_interpos _ = false; Walther@60704: Walther@60704: (* get the children of a node in ctree *) Walther@60704: fun children (Nd (PblObj _, cn)) = cn Walther@60704: | children (Nd (PrfObj _, cn)) = cn Walther@60704: | children _ = raise ERROR "children: uncovered fun def."; Walther@60704: Walther@60704: (*/--------------- duplicates in ctree-navi.sml: required also here below ---------------\*) Walther@60704: \<^isac_test>\ Walther@60704: fun lev_up [] = raise PTREE "lev_up []" Walther@60704: | lev_up p = (drop_last p):pos; Walther@60704: (* find the position of the next parent which is a PblObj in ctree *) Walther@60704: fun par_pblobj _ [] = [] Walther@60704: | par_pblobj pt p = Walther@60704: let Walther@60704: fun par _ [] = [] Walther@60704: | par pt p = Walther@60704: if is_pblobj (get_obj I pt p) Walther@60704: then p Walther@60704: else par pt (lev_up p) Walther@60704: in par pt (lev_up p) end; Walther@60704: \ Walther@60704: (*\--------------- duplicates in ctree-navi.sml: required also here below ---------------/*) Walther@60704: Walther@60704: (* insert obj b into ctree at pos, ev.overwriting this pos *) Walther@60704: fun insert_pt b EmptyPtree [] = Nd (b, []) Walther@60704: | insert_pt _ EmptyPtree _ = raise PTREE "insert_pt b Empty _" Walther@60704: | insert_pt b _ [] = Nd (b, []) Walther@60704: | insert_pt b (Nd (b', bs)) (p :: []) = Nd (b', repl_app bs p (Nd (b, []))) Walther@60704: | insert_pt b (Nd (b', bs)) (p :: ps) = Nd (b', repl_app bs p (insert_pt b (nth p bs) ps)); Walther@60704: Walther@60704: (* insert children to a node without children. compare: fun insert_pt *) Walther@60704: fun ins_chn _ EmptyPtree _ = raise PTREE "ins_chn: EmptyPtree" Walther@60704: | ins_chn _ (Nd _) [] = raise PTREE "ins_chn: pos = []" Walther@60704: | ins_chn ns (Nd (b, bs)) (p :: []) = Walther@60704: if p > length bs Walther@60704: then raise PTREE "ins_chn: pos not existent" Walther@60704: else Walther@60704: let Walther@60704: val (b', bs') = case nth p bs of Walther@60704: Nd (b', bs') => (b', bs') Walther@60704: | _ => raise ERROR "ins_chn: uncovered case nth" Walther@60704: in Walther@60704: if null bs' Walther@60704: then Nd (b, repl_app bs p (Nd (b', ns))) Walther@60704: else raise PTREE "ins_chn: pos mustNOT be overwritten" Walther@60704: end Walther@60704: | ins_chn ns (Nd (b, bs)) (p::ps) = Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps)); Walther@60704: Walther@60704: (* apply f to obj at pos, f: ppobj -> ppobj *) Walther@60704: fun appl_to_node f (Nd (b, bs)) = Nd (f b, bs) Walther@60704: | appl_to_node _ _ = raise ERROR "appl_to_node: uncovered fun def."; Walther@60704: fun appl_obj _ EmptyPtree [] = EmptyPtree Walther@60704: | appl_obj _ EmptyPtree _ = raise PTREE "appl_obj f Empty _" Walther@60704: | appl_obj f (Nd (b, bs)) [] = Nd (f b, bs) Walther@60704: | appl_obj f (Nd (b, bs)) (p :: []) = Nd (b, repl_app bs p (((appl_to_node f) o (nth p)) bs)) Walther@60704: | appl_obj f (Nd (b, bs)) (p :: ps) = Nd (b, repl_app bs p (appl_obj f (nth p bs) (ps:pos))); Walther@60704: Walther@60704: datatype ptform = Form of term | ModSpec of Specification_Def.T; Walther@60704: Walther@60704: \<^isac_test>\ Walther@60704: fun test_trans (PrfObj {branch, ...}) = true andalso branch = TransitiveB Walther@60704: | test_trans (PblObj {branch, ...}) = true andalso branch = TransitiveB; Walther@60704: \ Walther@60704: Walther@60704: fun is_pblobj' pt p = Walther@60704: let val ppobj = get_obj I pt p Walther@60704: in is_pblobj ppobj end; Walther@60704: Walther@60704: fun del_res (PblObj {fmz, origin, spec, probl, meth, ctxt, loc = (l1, _), branch, ...}) = Walther@60704: PblObj {fmz = fmz, origin = origin, spec = spec, probl = probl, meth = meth, Walther@60704: ctxt = ctxt, loc= (l1, NONE), branch = branch, Walther@60704: result = (TermC.empty, []), ostate = Incomplete} Walther@60704: | del_res (PrfObj {form, tac, loc= (l1, _), branch, ...}) = Walther@60704: PrfObj {form = form, tac = tac, loc = (l1, NONE), branch = branch, Walther@60704: result = (TermC.empty, []), ostate = Incomplete}; Walther@60704: Walther@60704: Walther@60704: fun get_loc EmptyPtree _ = (Istate_Def.empty, ContextC.empty) Walther@60704: | get_loc pt (p, Res) = Walther@60704: (case get_obj g_loc pt p of Walther@60704: (SOME ist_ctxt, NONE) => ist_ctxt Walther@60704: | (NONE , NONE) => (Istate_Def.empty, ContextC.empty) Walther@60704: | (_ , SOME ist_ctxt) => ist_ctxt) Walther@60704: | get_loc pt (p, _) = Walther@60704: (case get_obj g_loc pt p of Walther@60704: (NONE , SOME ist_ctxt) => ist_ctxt (* 020813 too liberal? *) Walther@60704: | (NONE , NONE) => (Istate_Def.empty, ContextC.empty) Walther@60704: | (SOME ist_ctxt, _) => ist_ctxt); Walther@60704: fun get_istate_LI pt p = get_loc pt p |> #1; Walther@60704: fun get_ctxt_LI pt p = get_loc pt p |> #2; Walther@60704: fun get_ctxt pt (pos as (p, p_)) = Walther@60704: if member op = [Frm, Res] p_ Walther@60704: then get_loc pt pos |> #2 (*for program interpretation rely on fun get_loc*) Walther@60704: else (*p = Pbl: for specify phase take ctxt from PblObj *) Walther@60704: if (p |> get_obj g_origin pt |> LibraryC.fst3) = [] (*CAS-command ? *) Walther@60704: then (Know_Store.get_via_last_thy "Isac_Knowledge"(*CAS-command unknown*)) |> Defs.global_context |> fst Walther@60704: else get_obj g_ctxt pt p Walther@60704: Walther@60704: fun get_assumptions pt p = get_ctxt pt p |> ContextC.get_assumptions; Walther@60704: Walther@60704: fun get_somespec' (dI, pI, mI) (dI', pI', mI') = Walther@60704: let Walther@60704: val domID = if dI = ThyC.id_empty then dI' else dI Walther@60704: val pblID = if pI = Problem.id_empty then pI' else pI Walther@60704: val metID = if mI = MethodC.id_empty then mI' else mI Walther@60704: in (domID, pblID, metID) end; Walther@60704: Walther@60704: (**.development for extracting an 'interval' from ptree.**) Walther@60704: Walther@60704: \<^isac_test>\ Walther@60704: (*WN0510 version stopped in favour of get_interval with !!!move_dn, getFormulaeFromTo Walther@60704: actually used (inefficient) version with move_dn: see modspec.sml*) Walther@60704: local Walther@60704: Walther@60704: fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*) Walther@60704: fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*) Walther@60704: fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x; Walther@60704: fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x; Walther@60704: Walther@60704: fun getnd i (b,p) q (Nd (_, nds)) = Walther@60704: (if i <= 0 then [[b]] else []) @ Walther@60704: (getnds (i-1) true (b@[hdp p], tlp p) (tlq q) Walther@60704: (take_fromto (hdp p) (hdq q) nds)) Walther@60704: | getnd _ _ _ _ = raise ERROR "getnd: uncovered case in fun.def." Walther@60704: and getnds _ _ _ _ [] = [] (*no children*) Walther@60704: | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*) Walther@60704: Walther@60704: | getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*) Walther@60704: (getnd i ( b, p ) [99999] n1) @ Walther@60704: (getnd ~99999 (lev_on b,[0]) q n2) Walther@60704: Walther@60704: | getnds i _ (b, _) q [n1, n2] = (*intern, r-margin*) Walther@60704: (getnd i ( b,[0]) [99999] n1) @ Walther@60704: (getnd ~99999 (lev_on b,[0]) q n2) Walther@60704: Walther@60704: | getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*) Walther@60704: (getnd i ( b, p ) [99999] nd) @ Walther@60704: (getnds ~99999 false (lev_on b,[0]) q nds) Walther@60704: Walther@60704: | getnds i _ (b, _) q (nd::(nds as _::_)) = (*intern, ...*) Walther@60704: (getnd i ( b,[0]) [99999] nd) @ Walther@60704: (getnds ~99999 false (lev_on b,[0]) q nds); Walther@60704: in Walther@60704: (*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes Walther@60704: where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous) Walther@60704: (1) the 'f' are given Walther@60704: (1a) by 'from' if 'f' = the respective element of 'from' (left margin) Walther@60704: (1b) -inifinity, if 'f' > the respective element of 'from' (internal node) Walther@60704: (2) the 't' ar given Walther@60704: (2a) by 'to' if 't' = the respective element of 'to' (right margin) Walther@60704: (2b) inifinity, if 't' < the respective element of 'to (internal node)' Walther@60704: the 'f' and 't' are set by hdp,... *) Walther@60704: fun get_trace pt p q = Walther@60704: (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q))) Walther@60704: (take_fromto (hdp p) (hdq q) (children pt)); Walther@60704: end; Walther@60704: Walther@60704: (*extract a formula or model from ctree for itms2itemppc or model2xml*) Walther@60704: fun preconds2str bts = Walther@60704: (strs2str o (map (linefeed o pair2str o Walther@60704: (apsnd (UnparseC.term @{context})) o Walther@60704: (apfst bool2str)))) bts; Walther@60704: Walther@60704: fun ocalhd2str (b, p, hdf, itms, prec, spec) = Walther@60704: "(" ^ bool2str b ^ ", " ^ pos_2str p ^ ", " ^ UnparseC.term @{context} hdf ^ Walther@60704: ", " ^ "\itms2str itms\" (*Model_Def.itms2str_ (ThyC.id_to_ctxt "Isac_Knowledge") itms*) ^ Walther@60704: ", " ^ preconds2str prec ^ ", \n" ^ References_Def.to_string spec ^ " )"; Walther@60704: \ Walther@60704: Walther@60704: Walther@60704: fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj Walther@60704: | is_pblnd _ = raise ERROR "is_pblnd: uncovered fun def."; Walther@60704: Walther@60704: Walther@60704: (* determine the previous pos' on the same level Walther@60704: WN0502 made for interSteps; _only_ works for branch TransitiveB WN120517 compare lev_back *) Walther@60704: fun lev_pred' _ ([], Res) = ([], Pbl) Walther@60704: | lev_pred' pt (p, Res) = Walther@60704: let val (p', last) = split_last p Walther@60704: in Walther@60704: if last = 1 Walther@60704: then if (is_pblobj o (get_obj I pt)) p then (p, Pbl) else (p, Frm) Walther@60704: else if get_obj g_res pt (p' @ [last - 1]) = get_obj g_form pt p Walther@60704: then (p' @ [last - 1], Res) (* TransitiveB *) Walther@60704: else if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm) Walther@60704: end Walther@60704: | lev_pred' _ _ = raise ERROR ""; Walther@60704: Walther@60704: Walther@60704: (**.insert into ctree and cut branches accordingly.**) Walther@60704: Walther@60704: \<^isac_test>\ Walther@60704: (* get all positions of certain intervals on the ctree. Walther@60704: old VERSION without move_dn; kept for occasional redesign Walther@60704: get all pos's to be cut in a ctree Walther@60704: below a pos or from a ctree list after i-th element (NO level_up) *) Walther@60704: fun get_allpos' (_, _) EmptyPtree = [] Walther@60704: | get_allpos' (p, 1) (Nd (b, bs)) = (* p is pos of Nd *) Walther@60704: if g_ostate b = Incomplete Walther@60704: then (p, Frm) :: (get_allpos's (p, 1) bs) Walther@60704: else (p, Frm) :: (get_allpos's (p, 1) bs) @ [(p, Res)] Walther@60704: | get_allpos' (p, _) (Nd (b, bs)) = (* p is pos of Nd *) Walther@60704: if length bs > 0 orelse is_pblobj b Walther@60704: then if g_ostate b = Incomplete Walther@60704: then [(p,Frm)] @ (get_allpos's (p, 1) bs) Walther@60704: else [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p, Res)] Walther@60704: else if g_ostate b = Incomplete then [] else [(p, Res)] Walther@60704: and get_allpos's _ [] = [] Walther@60704: | get_allpos's (p, i) (pt :: pts) = (* p is pos of parent-Nd *) Walther@60704: (get_allpos' (p @ [i], i) pt) @ (get_allpos's (p, i + 1) pts); Walther@60704: Walther@60704: (*WN050106 like cut_level, but deletes exactly 1 node *) Walther@60704: fun cut_level__ _ _ EmptyPtree _ =raise PTREE "cut_level__ Empty _" (* for tests ONLY *) Walther@60704: | cut_level__ _ _ (Nd ( _, _)) ([], _) = raise PTREE "cut_level__ _ []" Walther@60704: | cut_level__ cuts P (Nd (b, bs)) (p :: [], p_) = Walther@60704: if test_trans b Walther@60704: then Walther@60704: (Nd (b, drop_nth [] (p:Pos.posel, bs)), Walther@60704: cuts @ (if p_ = Frm then [(P @ [p], Res)] else []) @ Walther@60704: (get_allpos's (P, p + 1) (drop_nth [] (p, bs)))) Walther@60704: else (Nd (b, bs), cuts) Walther@60704: | cut_level__ cuts P (Nd (b, bs)) ((p :: ps), p_) = Walther@60704: let Walther@60704: val (bs', cuts') = cut_level__ cuts P (nth p bs) (ps, p_) Walther@60704: in (Nd (b, repl_app bs p bs'), cuts @ cuts') end; Walther@60704: Walther@60704: fun cut_level _ _ EmptyPtree _ = raise PTREE "cut_level EmptyPtree _" Walther@60704: | cut_level _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level _ []" Walther@60704: | cut_level cuts P (Nd (b, bs)) (p :: [], p_) = Walther@60704: if test_trans b Walther@60704: then Walther@60704: (Nd (b, take (p:Pos.posel, bs)), Walther@60704: cuts @ Walther@60704: (if p_ = Frm andalso (*#*) g_ostate b = Complete then [(P@[p],Res)] else ([]:pos' list)) @ Walther@60704: (get_allpos's (P, p+1) (takerest (p, bs)))) Walther@60704: else (Nd (b, bs), cuts) Walther@60704: | cut_level cuts P (Nd (b, bs)) ((p :: ps), p_) = Walther@60704: let Walther@60704: val (bs', cuts') = cut_level cuts P (nth p bs) (ps, p_) Walther@60704: in (Nd (b, repl_app bs p bs'), cuts @ cuts') end; Walther@60704: Walther@60704: Walther@60704: (*old version before WN050219, overwritten below*) Walther@60704: fun cut_tree _ ([], _) = raise PTREE "cut_tree _ ([],_)" Walther@60704: | cut_tree pt (pos as ([_], _)) = Walther@60704: let Walther@60704: val (pt', cuts) = cut_level [] [] pt pos Walther@60704: in Walther@60704: (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete then [] else [([], Res)])) Walther@60704: end Walther@60704: | cut_tree pt (p,p_) = Walther@60704: let Walther@60704: fun cutfn pt cuts (p, p_) = Walther@60704: let Walther@60704: val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_) Walther@60704: in Walther@60704: if length cuts' > 0 andalso length p > 1 Walther@60704: then cutfn pt' (cuts @ cuts') (lev_up p, Frm(*-->(p,Res)*)) Walther@60704: else (pt', cuts @ cuts') Walther@60704: end Walther@60704: val (pt', cuts) = cutfn pt [] (p, p_) Walther@60704: in Walther@60704: (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete then [] else [([], Res)])) Walther@60704: end; Walther@60704: \ Walther@60704: Walther@60704: local Walther@60704: fun move_dn _ (Nd (_, ns)) ([],p_) = (* root problem *) Walther@60704: (case p_ of Walther@60704: Res => raise PTREE "move_dn: end of calculation" Walther@60704: | _ => Walther@60704: if null ns (* go down from Pbl + Met *) Walther@60704: then raise PTREE "move_dn: solve problem not started" Walther@60704: else ([1], Frm)) Walther@60704: | move_dn P (Nd (_, ns)) (p :: (ps as (_ :: _)), p_) = (* iterate to end of pos *) Walther@60704: if p > length ns Walther@60704: then raise PTREE "move_dn: pos not existent 2" Walther@60704: else move_dn (P @ [p]) (nth p ns) (ps, p_) Walther@60704: | move_dn P (Nd (c, ns)) ([p], p_) = (* act on last element of pos *) Walther@60704: if p > length ns Walther@60704: then raise PTREE "move_dn: pos not existent 3" Walther@60704: else Walther@60704: (case p_ of Walther@60704: Res => Walther@60704: if p = length ns (* last Res on this level: go a level up *) Walther@60704: then if g_ostate c = Complete Walther@60704: then (P, Res) Walther@60704: else raise PTREE (ints2str' P ^ " not complete 1") Walther@60704: else (* go to the next Nd on this level, or down into the next Nd *) Walther@60704: if is_pblnd (nth (p + 1) ns) then (P@[p + 1], Pbl) Walther@60704: else if g_res' (nth p ns) = g_form' (nth (p + 1) ns) Walther@60704: then if (null o children o (nth (p + 1))) ns Walther@60704: then (* take the Res if Complete *) Walther@60704: if g_ostate' (nth (p + 1) ns) = Complete Walther@60704: then (P@[p + 1], Res) Walther@60704: else raise PTREE (ints2str' (P@[p + 1]) ^ " not complete 2") Walther@60704: else (P@[p + 1, 1], Frm) (* go down into the next PrfObj *) Walther@60704: else (P@[p + 1], Frm) (* take Frm: exists if the Nd exists *) Walther@60704: | Frm => (*go down or to the Res of this Nd*) Walther@60704: if (null o children o (nth p)) ns Walther@60704: then if g_ostate' (nth p ns) = Complete then (P @ [p], Res) Walther@60704: else raise PTREE (ints2str' (P @ [p])^" not complete 3") Walther@60704: else (P @ [p, 1], Frm) Walther@60704: | _ => (* is Pbl or Met *) Walther@60704: if (null o children o (nth p)) ns Walther@60704: then raise PTREE "move_dn:solve subproblem not startd" Walther@60704: else (P @ [p, 1], Walther@60704: if (is_pblnd o hd o children o (nth p)) ns Walther@60704: then Pbl else Frm)) Walther@60704: | move_dn _ _ _ = raise ERROR ""; Walther@60704: in Walther@60704: (* get all positions in a ctree until ([],Res) or ostate=Incomplete Walther@60704: val get_allp = fn : Walther@60704: pos' list -> : accumulated, start with [] Walther@60704: pos -> : the offset for subtrees wrt the root Walther@60704: ctree -> : (sub)tree Walther@60704: pos' : initialization (the last pos' before ...) Walther@60704: -> pos' list : of positions in this (sub) tree (relative to the root) Walther@60704: *) Walther@60704: fun get_allp cuts (P, pos) pt = Walther@60704: (let Walther@60704: val nxt = move_dn [] pt pos (*exn if Incomplete reached*) Walther@60704: in Walther@60704: if nxt <> ([], Res) Walther@60704: then get_allp (cuts @ [nxt]) (P, nxt) pt Walther@60704: else map (apfst (curry op @ P)) (cuts @ [nxt]) Walther@60704: end) Walther@60704: handle PTREE _ => (map (apfst (curry op@ P)) cuts); Walther@60704: end Walther@60704: Walther@60704: (* the pts are assumed to be on the same level *) Walther@60704: fun get_allps cuts _ [] = cuts Walther@60704: | get_allps cuts P (pt :: pts) = Walther@60704: let Walther@60704: val below = get_allp [] (P, ([], Frm)) pt Walther@60704: val levfrm = Walther@60704: if is_pblnd pt Walther@60704: then (P, Pbl) :: below Walther@60704: else if last_elem P = 1 Walther@60704: then (P, Frm) :: below Walther@60704: else (*Trans*) below Walther@60704: val levres = levfrm @ (if null below then [(P, Res)] else []) Walther@60704: in Walther@60704: get_allps (cuts @ levres) (lev_on P) pts Walther@60704: end; Walther@60704: Walther@60704: (** these 2 funs decide on how far cut_tree goes **) Walther@60704: (* shall the nodes _after_ the pos to be inserted at be deleted? Walther@60704: shall cutting be continued on the higher level(s)? the Nd regarded will NOT be changed *) Walther@60704: fun test_trans (PrfObj {branch, ...}) = (branch = TransitiveB orelse branch = NoBranch) Walther@60704: | test_trans (PblObj {branch, ...}) = (branch = TransitiveB orelse branch = NoBranch); Walther@60704: Walther@60704: (* cut_bottom new sml603..608 Walther@60704: cut the level at the bottom of the pos (used by cappend_...) Walther@60704: and handle the parent in order to avoid extra case for root Walther@60704: fn: ctree -> : the _whole_ ctree for cut_levup Walther@60704: pos * Pos.posel -> : the pos after split_last Walther@60704: ctree -> : the parent of the Nd to be cut Walther@60704: return Walther@60704: (ctree * : the updated ctree Walther@60704: pos' list) * : the pos's cut Walther@60704: bool : cutting shall be continued on the higher level(s) Walther@60704: *) Walther@60704: fun cut_bottom _ (pt' as Nd (b, [])) = ((pt', []), test_trans b) Walther@60704: | cut_bottom (P, p) (Nd (b, bs)) = Walther@60704: let (*divide level into 3 parts...*) Walther@60704: val keep = take (p - 1, bs) Walther@60704: val pt' = case nth p bs of Walther@60704: pt' as Nd _ => pt' Walther@60704: | _ => raise ERROR "cut_bottom: uncovered case nth p bs" Walther@60704: (*^^^^^_here_ will be 'insert_pt'ed by 'append_..'*) Walther@60704: val (tail, _) = (takerest (p, bs), if null (takerest (p, bs)) then 0 else p + 1) Walther@60704: val (children, cuts) = Walther@60704: if test_trans b Walther@60704: then Walther@60704: (keep, (if is_pblnd pt' then [(P @ [p], Pbl)] else []) Walther@60704: @ (get_allp [] (P @ [p], (P, Frm)) pt') Walther@60704: @ (get_allps [] (P @ [p + 1]) tail)) Walther@60704: else (keep @ [(*'insert_pt'ed by 'append_..'*)] @ tail, Walther@60704: get_allp [] (P @ [p], (P, Frm)) pt') Walther@60704: val (pt'', cuts) = Walther@60704: if test_trans b Walther@60704: then (Nd (del_res b, children), cuts @ (if g_ostate b = Incomplete then [] else [(P, Res)])) Walther@60704: else (Nd (b, children), cuts) Walther@60704: in ((pt'', cuts), test_trans b) end Walther@60704: | cut_bottom _ _ = raise ERROR "cut_bottom: uncovered fun def."; Walther@60704: Walther@60704: Walther@60704: (* go all levels from the bottom of 'pos' up to the root, Walther@60704: on each level compose the children of a node and accumulate the cut Nds Walther@60704: args Walther@60704: pos' list -> : for accumulation Walther@60704: bool -> : cutting shall be continued on the higher level(s) Walther@60704: ctree -> : the whole ctree for 'get_nd pt P' on each level Walther@60704: ctree -> : the Nd from the lower level for insertion at path Walther@60704: pos * Pos.posel -> : pos=path split for convenience Walther@60704: ctree -> : Nd the children of are under consideration on this call Walther@60704: returns : Walther@60704: ctree * pos' list : the updated parent-Nd and the pos's of the Nds cut Walther@60704: *) Walther@60704: fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:Pos.posel) (Nd (b, bs)) = Walther@60704: let (*divide level into 3 parts...*) Walther@60704: val keep = take (p - 1, bs) Walther@60704: (*val pt' comes as argument from below*) Walther@60704: val (tail, _) = Walther@60704: (takerest (p, bs), if null (takerest (p, bs)) then 0 else p + 1) Walther@60704: val (children, cuts') = Walther@60704: if clevup Walther@60704: then (keep @ [pt'], get_allps [] (P @ [p+1]) tail) Walther@60704: else (keep @ [pt'] @ tail, []) Walther@60704: val clevup' = if clevup then test_trans b else false Walther@60704: (*the first Nd with false stops cutting on all levels above*) Walther@60704: val (pt'', cuts') = Walther@60704: if clevup' Walther@60704: then (Nd (del_res b, children), cuts' @ (if g_ostate b = Incomplete then [] else [(P, Res)])) Walther@60704: else (Nd (b, children), cuts') Walther@60704: in Walther@60704: if null P Walther@60704: then (pt'', cuts @ cuts') Walther@60704: else Walther@60704: let val (P, p) = split_last P Walther@60704: in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P) end Walther@60704: end Walther@60704: | cut_levup _ _ _ _ _ _ = raise ERROR "cut_levup: uncovered fun def."; Walther@60704: Walther@60704: (* cut nodes after and below an inserted node in the ctree; Walther@60704: the cuts range is limited by the predicate 'fun cutlevup' *) Walther@60704: fun cut_tree pt (pos, _) = Walther@60704: if not (existpt pos pt) Walther@60704: then (pt, []) (*appending a formula never cuts anything*) Walther@60704: else Walther@60704: let Walther@60704: val (P, p) = split_last pos Walther@60704: val ((pt', cuts), clevup) = cut_bottom (P, p) (get_nd pt P) Walther@60704: (* pt' is the updated parent of the Nd to cappend_..*) Walther@60704: in Walther@60704: if null P Walther@60704: then (pt', cuts) Walther@60704: else Walther@60704: let val (P, p) = split_last P Walther@60704: in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P) end Walther@60704: end; Walther@60704: Walther@60704: (* get the theory explicitly just for the rootpbl; Walther@60704: thus use this function _after_ finishing specification *) Walther@60704: fun root_thy (Nd (PblObj {spec = (thyID, _, _), ctxt, ...}, _)) = ThyC.get_theory ctxt thyID Walther@60704: | root_thy _ = raise ERROR "root_thy: uncovered fun def."; Walther@60704: Walther@60704: (**) Walther@60704: end; Walther@60704: (**)