wneuper@59292: (* Title: the calctree, which holds a calculation wneuper@59292: Author: Walther Neuper 1999 wneuper@59292: (c) due to copyright terms wneuper@59292: *) wneuper@59292: wneuper@59292: signature BASIC_CALC_TREE = wneuper@59292: sig (* vvv--- *.sml require these typs incrementally, with these exception -----------------vvv *) wneuper@59294: (*===\ other ?mstools.sml? =================================================================*) wneuper@59292: type state wneuper@59292: type con wneuper@59292: wneuper@59292: eqtype posel wneuper@59292: type pos = posel list wneuper@59292: val pos2str : int list -> string (* for datatypes.sml *) wneuper@59292: datatype pos_ = Frm | Met | Pbl | Res | Und wneuper@59292: val pos_2str : pos_ -> string wneuper@59292: type pos' wneuper@59292: val pos'2str : pos' -> string wneuper@59292: val str2pos_ : string -> pos_ (* for datatypes.sml *) wneuper@59292: val e_pos' : pos' wneuper@59292: (* for generate.sml ?!? ca.*) wneuper@59292: eqtype cellID wneuper@59292: wneuper@59292: datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB wneuper@59292: datatype ostate = Complete | Incomplete | Inconsistent wneuper@59292: datatype ppobj = wneuper@59292: PblObj of wneuper@59292: {branch: branch, wneuper@59405: cell: Celem.lrd option, wneuper@59300: loc: (Selem.istate * Proof.context) option * (Selem.istate * Proof.context) option, wneuper@59292: ostate: ostate, wneuper@59299: result: Selem.result, wneuper@59292: wneuper@59298: fmz: Selem.fmz, wneuper@59405: origin: Model.ori list * Celem.spec * term, wneuper@59316: probl: Model.itm list, wneuper@59316: meth: Model.itm list, wneuper@59405: spec: Celem.spec, wneuper@59292: ctxt: Proof.context, wneuper@59300: env: (Selem.istate * Proof.context) option} wneuper@59292: | PrfObj of wneuper@59292: {branch: branch, wneuper@59405: cell: Celem.lrd option, wneuper@59300: loc: (Selem.istate * Proof.context) option * (Selem.istate * Proof.context) option, wneuper@59292: ostate: ostate, wneuper@59299: result: Selem.result, wneuper@59292: wneuper@59292: form: term, wneuper@59302: tac: Tac.tac} wneuper@59292: wneuper@59292: datatype ctree = EmptyPtree | Nd of ppobj * ctree list wneuper@59292: val e_ctree : ctree (* TODO: replace by EmptyPtree*) wneuper@59292: val existpt' : pos' -> ctree -> bool (* for interface.sml *) wneuper@59292: val is_interpos : pos' -> bool (* for interface.sml *) wneuper@59292: val lev_pred' : ctree -> pos' -> pos' (* for interface.sml *) wneuper@59292: val ins_chn : ctree list -> ctree -> pos -> ctree (* for solve.sml *) wneuper@59292: val children : ctree -> ctree list (* for solve.sml *) wneuper@59292: val get_nd : ctree -> pos -> ctree (* for solve.sml *) wneuper@59292: val just_created_ : ppobj -> bool (* for mathengine.sml *) wneuper@59405: val just_created : state -> bool (* for mathengine.sml *) wneuper@59405: val e_origin : Model.ori list * Celem.spec * term (* for mathengine.sml *) wneuper@59292: wneuper@59292: val is_pblobj : ppobj -> bool wneuper@59292: val is_pblobj' : ctree -> pos -> bool wneuper@59292: val is_pblnd : ctree -> bool wneuper@59292: wneuper@59405: val g_spec : ppobj -> Celem.spec wneuper@59300: val g_loc : ppobj -> (Selem.istate * Proof.context) option * (Selem.istate * Proof.context) option wneuper@59292: val g_form : ppobj -> term wneuper@59316: val g_pbl : ppobj -> Model.itm list wneuper@59316: val g_met : ppobj -> Model.itm list wneuper@59405: val g_metID : ppobj -> Celem.metID wneuper@59299: val g_result : ppobj -> Selem.result wneuper@59302: val g_tac : ppobj -> Tac.tac wneuper@59405: val g_domID : ppobj -> Celem.domID (* for appl.sml TODO: replace by thyID *) wneuper@59405: val g_env : ppobj -> (Selem.istate * Proof.context) option (* for appl.sml *) wneuper@59292: wneuper@59405: val g_origin : ppobj -> Model.ori list * Celem.spec * term (* for script.sml *) wneuper@59405: val get_loc : ctree -> pos' -> Selem.istate * Proof.context (* for script.sml *) wneuper@59405: val get_istate : ctree -> pos' -> Selem.istate (* for script.sml *) wneuper@59292: val get_ctxt : ctree -> pos' -> Proof.context wneuper@59292: val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a wneuper@59292: val get_curr_formula : state -> term wneuper@59292: val get_assumptions_ : ctree -> pos' -> term list (* for appl.sml *) wneuper@59292: wneuper@59292: val is_e_ctxt : Proof.context -> bool (* for appl.sml *) wneuper@59300: val new_val : term -> Selem.istate -> Selem.istate wneuper@59292: (* for calchead.sml *) wneuper@59292: type cid = cellID list wneuper@59405: type ocalhd = bool * pos_ * term * Model.itm list * (bool * term) list * Celem.spec wneuper@59292: datatype ptform = Form of term | ModSpec of ocalhd wneuper@59405: val get_somespec' : Celem.spec -> Celem.spec -> Celem.spec wneuper@59292: exception PTREE of string; wneuper@59296: wneuper@59405: val par_pbl_det : ctree -> pos -> bool * pos * Celem.rls (* for appl.sml *) wneuper@59405: val rootthy : ctree -> theory (* for script.sml *) wneuper@59294: (* ---- made visible ONLY for structure CTaccess : CALC_TREE_ACCESS --------------------------- *) wneuper@59294: val appl_obj : (ppobj -> ppobj) -> ctree -> pos -> ctree wneuper@59294: val existpt : pos -> ctree -> bool (* also for tests *) wneuper@59294: val cut_tree : ctree -> pos * 'a -> ctree * pos' list (* also for tests *) wneuper@59294: val insert_pt : ppobj -> ctree -> int list -> ctree wneuper@59294: (* ---- made visible ONLY for structure CTnavi : CALC_TREE_NAVIGATION ------------------------- *) wneuper@59296: val g_branch : ppobj -> branch wneuper@59296: val g_form' : ctree -> term wneuper@59296: val g_ostate : ppobj -> ostate wneuper@59296: val g_ostate' : ctree -> ostate wneuper@59296: val g_res : ppobj -> term wneuper@59296: val g_res' : ctree -> term wneuper@59296: (*/---- duplicates in CTnavi, reconsider structs ----------------------------------------------- wneuper@59296: val lev_on : CTbasic.pos -> CTbasic.pos (* duplicate in ctree-navi.sml *) wneuper@59296: val lev_dn : CTbasic.pos -> CTbasic.pos (* duplicate in ctree-navi.sml *) wneuper@59296: val par_pblobj : CTbasic.ctree -> CTbasic.pos -> CTbasic.pos (* duplicate in ctree-navi.sml *) wneuper@59296: ---- duplicates in CTnavi, reconsider structs ----------------------------------------------/*) wneuper@59294: wneuper@59299: (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) wneuper@59292: val pr_ctree : (pos -> ppobj -> string) -> ctree -> string wneuper@59292: val pr_short : pos -> ppobj -> string wneuper@59292: val g_ctxt : ppobj -> Proof.context wneuper@59298: val g_fmz : ppobj -> Selem.fmz wneuper@59292: val get_allp : pos' list -> pos * (int list * pos_) -> ctree -> pos' list wneuper@59292: val get_allps : (pos * pos_) list -> posel list -> ctree list -> pos' list wneuper@59292: val get_allpos' : pos * posel -> ctree -> pos' list wneuper@59292: val get_allpos's : pos * posel -> ctree list -> (pos * pos_) list wneuper@59292: val cut_bottom : pos * posel -> ctree -> (ctree * pos' list) * bool wneuper@59292: val cut_level : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list wneuper@59292: val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list wneuper@59292: val get_trace : ctree -> int list -> int list -> int list list wneuper@59292: val branch2str : branch -> string wneuper@59299: ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) wneuper@59310: wneuper@59310: (*----- unused code, kept as hints to design ideas ---------------------------------------------*) wneuper@59310: (* NONE *) wneuper@59292: end wneuper@59292: wneuper@59292: (**) wneuper@59292: structure CTbasic(**): BASIC_CALC_TREE(**) = wneuper@59292: struct wneuper@59292: (**) wneuper@59292: type env = (term * term) list; wneuper@59292: wneuper@59292: datatype branch = wneuper@59292: NoBranch | AndB | OrB wneuper@59292: | TransitiveB (* FIXXXME.0308: set branch from met in Apply_Method wneuper@59292: FIXXXME.0402: -"- in Begin_Trans'*) wneuper@59292: | SequenceB | IntersectB | CollectB | MapB; wneuper@59292: wneuper@59292: fun branch2str NoBranch = "NoBranch" (* for tests only *) wneuper@59292: | branch2str AndB = "AndB" wneuper@59292: | branch2str OrB = "OrB" wneuper@59292: | branch2str TransitiveB = "TransitiveB" wneuper@59292: | branch2str SequenceB = "SequenceB" wneuper@59292: | branch2str IntersectB = "IntersectB" wneuper@59292: | branch2str CollectB = "CollectB" wneuper@59292: | branch2str MapB = "MapB"; wneuper@59292: wneuper@59292: datatype ostate = wneuper@59292: Incomplete | Complete | Inconsistent (* WN041020 latter still unused *); wneuper@59292: fun ostate2str Incomplete = "Incomplete" (* for tests only *) wneuper@59292: | ostate2str Complete = "Complete" wneuper@59292: | ostate2str Inconsistent = "Inconsistent"; wneuper@59292: wneuper@59292: type cellID = int; wneuper@59292: type cid = cellID list; wneuper@59292: wneuper@59292: type posel = int; (* for readability in funs accessing Ctree *) wneuper@59292: type pos = int list; wneuper@59292: val pos2str = ints2str'; wneuper@59292: datatype pos_ = wneuper@59292: Pbl (* PblObj-position: problem-type *) wneuper@59292: | Met (* PblObj-position: method *) wneuper@59292: | Frm (* PblObj-position: -> Pbl in ME (not by moveDown !) wneuper@59299: | PrfObj-position: formula *) wneuper@59292: | Res (* PblObj | PrfObj-position: result *) wneuper@59292: | Und; (* undefined*) wneuper@59292: fun pos_2str Pbl = "Pbl" wneuper@59292: | pos_2str Met = "Met" wneuper@59292: | pos_2str Frm = "Frm" wneuper@59292: | pos_2str Res = "Res" wneuper@59292: | pos_2str Und = "Und"; wneuper@59292: fun str2pos_ "Pbl" = Pbl wneuper@59292: | str2pos_ "Met" = Met wneuper@59292: | str2pos_ "Frm" = Frm wneuper@59292: | str2pos_ "Res" = Res wneuper@59292: | str2pos_ "Und" = Und wneuper@59292: | str2pos_ str = error ("str2pos_: wrong argument = " ^ str) wneuper@59292: wneuper@59292: type pos' = pos * pos_; wneuper@59292: (*WN0312 remembering interator (pos * pos_) for ctree wneuper@59292: pos : lev_on, lev_dn, lev_up wneuper@59292: pos_: wneuper@59292: # generate1 sets pos_ if possible ...?WN0502?NOT... wneuper@59292: # generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn wneuper@59292: exceptions: Begin/End_Trans wneuper@59292: # thus generate(1) called in wneuper@59292: .# assy, locate_gen wneuper@59292: .# nxt_solv (tac_ -cases); general case: wneuper@59292: val pos' = case pos' of (p,Res) => (lev_on p',Res) | _ => pos' wneuper@59292: # WN050220, S(604): wneuper@59292: generate1...(Rewrite(f,..,res))..(pos, pos_) wneuper@59292: cappend_atomic.................pos ////// gets f+res always!!! wneuper@59292: cut_tree....................pos, pos_ wneuper@59292: *) wneuper@59292: fun pos'2str (p, p_) = pair2str (ints2str' p, pos_2str p_); wneuper@59292: fun pos's2str ps = (strs2str' o (map pos'2str)) ps; (* for tests only *) wneuper@59292: val e_pos' = ([], Und); wneuper@59292: wneuper@59292: (* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*) wneuper@59397: fun is_e_ctxt ctxt = Context.eq_thy (Proof_Context.theory_of ctxt, @{theory "Pure"}); wneuper@59292: wneuper@59300: type iist = Selem.istate option * Selem.istate option; wneuper@59292: (*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*) wneuper@59292: wneuper@59292: wneuper@59300: fun new_val v (Selem.ScrState (env, loc_, topt, _, safe, bool)) = wneuper@59300: (Selem.ScrState (env, loc_, topt, v, safe, bool)) wneuper@59292: | new_val _ _ = error "new_val: only for ScrState"; wneuper@59292: wneuper@59292: datatype con = land | lor; wneuper@59292: wneuper@59292: (* executed tactics (tac_s) with local environment etc.; wneuper@59292: used for continuing eval script + for generate *) wneuper@59292: type ets = wneuper@59405: (Celem.loc_ *(* of tactic in scr, tactic (weakly) associated with tac_ *) wneuper@59302: (Tac.tac_ * (* (for generate) *) wneuper@59302: env * (* with 'tactic=result' as rule, tactic ev. _not_ ready for 'parallel let' *) wneuper@59302: env * (* with results of (ready) tacs *) wneuper@59302: term * (* itr_arg of tactic, for upd. env at Repeat, Try *) wneuper@59302: term * (* result value of the tac *) wneuper@59299: Selem.safe)) wneuper@59292: list; wneuper@59292: wneuper@59292: fun ets2s (l,(m,eno,env,iar,res,s)) = wneuper@59405: "\n(" ^ Celem.loc_2str l ^ ",(" ^ Tac.tac_2str m ^ wneuper@59405: ",\n ens= " ^ Celem.subst2str eno ^ wneuper@59405: ",\n env= " ^ Celem.subst2str env ^ wneuper@59405: ",\n iar= " ^ Celem.term2str iar ^ wneuper@59405: ",\n res= " ^ Celem.term2str res ^ wneuper@59299: ",\n " ^ Selem.safe2str s ^ "))"; wneuper@59292: fun ets2str (ets: ets) = (strs2str o (map ets2s)) ets; (* for tests only *) wneuper@59292: wneuper@59292: type envp =(*9.5.03: unused, delete with field in ctree.PblObj FIXXXME*) wneuper@59292: (int * term list) list * (* assoc-list: args of met*) wneuper@59292: (int * rls) list * (* assoc-list: tacs already done ///15.9.00*) wneuper@59292: (int * ets) list * (* assoc-list: tacs etc. already done*) wneuper@59292: (string * pos) list; (* asms * from where*) wneuper@59292: wneuper@59292: datatype ppobj = (* TODO: arrange according to signature *) wneuper@59292: PrfObj of wneuper@59405: {cell : Celem.lrd option, (* where in form tac has been applied, FIXME.WN0607 rename field *) wneuper@59292: form : term, (* where tac is applied to *) wneuper@59302: tac : Tac.tac, (* also in istate *) wneuper@59300: loc : (Selem.istate * (* script interpreter state *) wneuper@59292: Proof.context) (* context for provers, type inference *) wneuper@59292: option * (* both for interpreter location on Frm, Pbl, Met *) wneuper@59300: (Selem.istate * (* script interpreter state *) wneuper@59292: Proof.context) (* context for provers, type inference *) wneuper@59292: option, (* both for interpreter location on Res *) wneuper@59292: (*(NONE,NONE) <==> e_istate ! see update_loc, get_loc *) wneuper@59292: branch: branch, (* only rudimentary *) wneuper@59299: result: Selem.result, (* result and assumptions *) wneuper@59292: ostate: ostate} (* Complete <=> result is OK *) wneuper@59292: | PblObj of wneuper@59405: {cell : Celem.lrd option, (* unused: meaningful only for some _Prf_Obj *) wneuper@59298: fmz : Selem.fmz, (* from init:FIXME never use this spec;-drop *) wneuper@59316: origin: (Model.ori list) * (* representation from fmz+pbt wneuper@59292: for efficiently adding items in probl, meth *) wneuper@59405: Celem.spec * (* updated by Refine_Tacitly *) wneuper@59292: term, (* headline of calc-head, as calculated initially(!) *) wneuper@59405: spec : Celem.spec, (* explicitly input *) wneuper@59405: probl : Model.itm list, (* itms explicitly input *) wneuper@59405: meth : Model.itm list, (* itms automatically added to copy of probl *) wneuper@59292: ctxt : Proof.context, (* WN110513 introduced to avoid [*] [**] *) wneuper@59300: env : (Selem.istate * Proof.context) option, (* istate only for initac in script wneuper@59292: context for specify phase on this node NO.. wneuper@59292: ..NO: this conflicts with init_form/initac: see Apply_Method without init_form *) wneuper@59300: loc : (Selem.istate * Proof.context) option * (Selem.istate * (* like PrfObj *) wneuper@59292: Proof.context) option, (* for spec-phase [*], NO.. wneuper@59292: ..NO: raises errors not tracable on WN110513 [**] *) wneuper@59292: branch: branch, (* like PrfObj *) wneuper@59299: result: Selem.result, (* like PrfObj *) wneuper@59292: ostate: ostate}; (* like PrfObj *) wneuper@59292: wneuper@59292: (* this tree contains isac's calculations; wneuper@59292: the tree's structure has been copied from an early version of Theorema(c); wneuper@59292: it has the disadvantage, that there is no space wneuper@59292: for the first tactic in a script generating the first formula at (p,Frm); wneuper@59292: this trouble has been covered by 'init_form' and 'Take' so far, wneuper@59292: but it is crucial if the first tactic in a script is eg. 'Subproblem'; wneuper@59292: see 'type tac', Apply_Method. wneuper@59292: *) wneuper@59292: datatype ctree = wneuper@59292: EmptyPtree wneuper@59292: | Nd of ppobj * (ctree list); wneuper@59292: val e_ctree = EmptyPtree; wneuper@59292: type state = ctree * pos' wneuper@59292: wneuper@59292: fun is_pblobj (PblObj _) = true wneuper@59292: | is_pblobj _ = false; wneuper@59292: wneuper@59292: exception PTREE of string; wneuper@59292: fun nth _ [] = raise PTREE "nth _ []" wneuper@59292: | nth 1 (x :: _) = x wneuper@59292: | nth n (_ :: xs) = nth (n - 1) xs; wneuper@59292: (*> nth 2 [11,22,33]; -->> val it = 22 : int*) wneuper@59292: wneuper@59292: wneuper@59292: (** convert ctree to a string **) wneuper@59292: wneuper@59292: (* convert a pos from list to string *) wneuper@59292: fun pr_pos ps = (space_implode "." (map string_of_int ps))^". "; wneuper@59292: (* show hd origin or form only *) wneuper@59292: fun pr_short p (PblObj _) = pr_pos p ^ " ----- pblobj -----\n" (* for tests only *) wneuper@59405: | pr_short p (PrfObj {form = form, ...}) = pr_pos p ^ Celem.term2str form ^ "\n"; wneuper@59292: fun pr_ctree f pt = (* for tests only *) wneuper@59292: let wneuper@59292: fun pr_pt _ _ EmptyPtree = "" wneuper@59292: | pr_pt pfn ps (Nd (b, [])) = pfn ps b wneuper@59292: | pr_pt pfn ps (Nd (b, ts)) = pfn ps b ^ prts pfn ps 1 ts wneuper@59292: and prts _ _ _ [] = "" wneuper@59292: | prts pfn ps p (t :: ts) = (pr_pt pfn (ps @ [p]) t)^ wneuper@59292: (prts pfn ps (p + 1) ts) wneuper@59292: in pr_pt f [] pt end; wneuper@59292: wneuper@59292: (** access the branches of ctree **) wneuper@59292: wneuper@59292: fun repl [] _ _ = raise PTREE "repl [] _ _" wneuper@59292: | repl (_ :: ls) 1 e = e :: ls wneuper@59292: | repl (l :: ls) n e = l :: (repl ls (n-1) e); wneuper@59292: fun repl_app ls n e = wneuper@59292: let wneuper@59292: val lim = 1 + length ls wneuper@59292: in wneuper@59292: if n > lim wneuper@59292: then raise PTREE "repl_app: n > lim" wneuper@59292: else if n = lim wneuper@59292: then ls @ [e] wneuper@59292: else repl ls n e end; wneuper@59292: wneuper@59292: (* get from obj at pos by f : ppobj -> 'a *) wneuper@59292: fun get_obj _ EmptyPtree _ = raise PTREE "get_obj f EmptyPtree" wneuper@59292: | get_obj f (Nd (b, _)) [] = f b wneuper@59292: | get_obj f (Nd (_, bs)) (p :: ps) = wneuper@59292: let wneuper@59292: val _ = (nth p bs) wneuper@59292: handle _ => raise PTREE ("get_obj: pos = " ^ ints2str' (p::ps) ^ " does not exist"); wneuper@59292: in wneuper@59292: (get_obj f (nth p bs) ps) wneuper@59292: handle _ => raise PTREE ("get_obj: pos = " ^ ints2str' (p::ps) ^ " does not exist") wneuper@59292: end; wneuper@59292: fun get_nd EmptyPtree _ = raise PTREE "get_nd EmptyPtree" wneuper@59292: | get_nd n [] = n wneuper@59292: | get_nd (Nd (_, nds)) (pos as p :: ps) = (get_nd (nth p nds) ps) wneuper@59292: handle _ => raise PTREE ("get_nd: not existent pos = " ^ ints2str' pos); wneuper@59292: wneuper@59292: (* for use by get_obj *) wneuper@59292: fun g_form (PrfObj {form = f,...}) = f wneuper@59292: | g_form (PblObj {origin= (_,_,f),...}) = f; wneuper@59292: fun g_form' (Nd (PrfObj {form = f, ...}, _)) = f wneuper@59292: | g_form' (Nd (PblObj {origin= (_, _, f),...}, _)) = f wneuper@59292: | g_form' _ = error "g_form': uncovered fun def."; wneuper@59292: (* | g_form _ = raise PTREE "g_form not for PblObj";*) wneuper@59292: fun g_origin (PblObj {origin = ori, ...}) = ori wneuper@59292: | g_origin _ = raise PTREE "g_origin not for PrfObj"; wneuper@59292: fun g_fmz (PblObj {fmz = f, ...}) = f (* for tests only *) wneuper@59292: | g_fmz _ = raise PTREE "g_fmz not for PrfObj"; wneuper@59292: fun g_spec (PblObj {spec = s, ...}) = s wneuper@59292: | g_spec _ = raise PTREE "g_spec not for PrfObj"; wneuper@59292: fun g_pbl (PblObj {probl = p, ...}) = p wneuper@59292: | g_pbl _ = raise PTREE "g_pbl not for PrfObj"; wneuper@59292: fun g_met (PblObj {meth = p, ...}) = p wneuper@59292: | g_met _ = raise PTREE "g_met not for PrfObj"; wneuper@59292: fun g_domID (PblObj {spec = (d, _, _), ...}) = d wneuper@59292: | g_domID _ = raise PTREE "g_metID not for PrfObj"; wneuper@59292: fun g_metID (PblObj {spec = (_, _, m), ...}) = m wneuper@59292: | g_metID _ = raise PTREE "g_metID not for PrfObj"; wneuper@59292: fun g_ctxt (PblObj {ctxt, ...}) = ctxt wneuper@59292: | g_ctxt _ = raise PTREE "g_ctxt not for PrfObj"; wneuper@59292: fun g_env (PblObj {env, ...}) = env wneuper@59292: | g_env _ = raise PTREE "g_env not for PrfObj"; wneuper@59292: fun g_loc (PblObj {loc = l, ...}) = l wneuper@59292: | g_loc (PrfObj {loc = l, ...}) = l; wneuper@59292: fun g_branch (PblObj {branch = b, ...}) = b wneuper@59292: | g_branch (PrfObj {branch = b, ...}) = b; wneuper@59302: fun g_tac (PblObj {spec = (_, _, m),...}) = Tac.Apply_Method m wneuper@59292: | g_tac (PrfObj {tac = m, ...}) = m; wneuper@59292: fun g_result (PblObj {result = r, ...}) = r wneuper@59292: | g_result (PrfObj {result = r, ...}) = r; wneuper@59292: fun g_res (PblObj {result = (r, _) ,...}) = r wneuper@59299: | g_res (PrfObj {result = (r, _),...}) = r; wneuper@59292: fun g_res' (Nd (PblObj {result = (r, _), ...}, _)) = r wneuper@59292: | g_res' (Nd (PrfObj {result = (r, _),...}, _)) = r wneuper@59292: | g_res' _ = raise PTREE "g_res': uncovered fun def."; wneuper@59292: fun g_ostate (PblObj {ostate = r, ...}) = r wneuper@59292: | g_ostate (PrfObj {ostate = r, ...}) = r; wneuper@59292: fun g_ostate' (Nd (PblObj {ostate = r, ...}, _)) = r wneuper@59292: | g_ostate' (Nd (PrfObj {ostate = r, ...}, _)) = r wneuper@59292: | g_ostate' _ = raise PTREE "g_ostate': uncovered fun def."; wneuper@59292: wneuper@59292: (* get the formula preceeding the current position in a calculation *) wneuper@59292: fun get_curr_formula (pt, (p, p_)) = wneuper@59292: case p_ of wneuper@59292: Frm => get_obj g_form pt p wneuper@59292: | Res => (fst o (get_obj g_result pt)) p wneuper@59292: | _ => #3 (get_obj g_origin pt p); wneuper@59292: wneuper@59292: (* in CalcTree/Subproblem an 'just_created_' model is created; wneuper@59292: this is filled to 'untouched' by Model/Refine_Problem *) wneuper@59292: fun just_created_ (PblObj {meth, probl, spec, ...}) = wneuper@59405: null meth andalso null probl andalso spec = Celem.e_spec wneuper@59292: | just_created_ _ = raise PTREE "g_ostate': uncovered fun def."; wneuper@59405: val e_origin = ([], Celem.e_spec, Celem.e_term); wneuper@59292: wneuper@59292: fun just_created (pt, (p, _)) = wneuper@59292: let val ppobj = get_obj I pt p wneuper@59292: in is_pblobj ppobj andalso just_created_ ppobj end; wneuper@59292: wneuper@59292: (* does the pos in the ctree exist ? *) wneuper@59292: fun existpt pos pt = can (get_obj I pt) pos; wneuper@59292: (* does the pos' in the ctree exist, ie. extra check for result in the node *) wneuper@59299: fun existpt' (p, p_) pt = wneuper@59292: if can (get_obj I pt) p wneuper@59292: then case p_ of wneuper@59292: Res => get_obj g_ostate pt p = Complete wneuper@59292: | _ => true wneuper@59292: else false; wneuper@59292: wneuper@59292: (* is this position appropriate for calculating intermediate steps? *) wneuper@59292: fun is_interpos (_, Res) = true wneuper@59292: | is_interpos _ = false; wneuper@59292: wneuper@59296: (* get the children of a node in ctree *) wneuper@59296: fun children (Nd (PblObj _, cn)) = cn wneuper@59296: | children (Nd (PrfObj _, cn)) = cn wneuper@59296: | children _ = error "children: uncovered fun def."; wneuper@59292: wneuper@59296: (*/--------------- duplicates in ctree-navi.sml: required also here below ---------------\*) wneuper@59296: fun lev_on [] = raise PTREE "lev_on []" wneuper@59296: | lev_on pos = wneuper@59296: let val len = length pos wneuper@59296: in (drop_last pos) @ [(nth len pos)+1] end; wneuper@59296: fun lev_up [] = raise PTREE "lev_up []" wneuper@59296: | lev_up p = (drop_last p):pos; wneuper@59292: (* find the position of the next parent which is a PblObj in ctree *) wneuper@59292: fun par_pblobj _ [] = [] wneuper@59292: | par_pblobj pt p = wneuper@59292: let wneuper@59292: fun par _ [] = [] wneuper@59292: | par pt p = wneuper@59292: if is_pblobj (get_obj I pt p) wneuper@59292: then p wneuper@59292: else par pt (lev_up p) wneuper@59292: in par pt (lev_up p) end; wneuper@59296: (*\--------------- duplicates in ctree-navi.sml: required also here below ---------------/*) wneuper@59292: wneuper@59292: (* find the next parent, which is either a PblObj (return true) wneuper@59292: or a PrfObj with tac = Detail_Set (return false) wneuper@59292: FIXME.030403: re-organize par_pbl_det after rls' --> rls*) wneuper@59405: fun par_pbl_det pt [] = (true, [], Celem.Erls) wneuper@59292: | par_pbl_det pt p = wneuper@59292: let wneuper@59405: fun par _ [] = (true, [], Celem.Erls) wneuper@59292: | par pt p = wneuper@59292: if is_pblobj (get_obj I pt p) wneuper@59405: then (true, p, Celem.Erls) wneuper@59292: else case get_obj g_tac pt p of wneuper@59302: Tac.Rewrite_Set rls' => (false, p, assoc_rls rls') wneuper@59302: | Tac.Rewrite_Set_Inst (_, rls') => (false, p, assoc_rls rls') wneuper@59292: | _ => par pt (lev_up p) wneuper@59292: in par pt (lev_up p) end; wneuper@59292: wneuper@59292: (* insert obj b into ctree at pos, ev.overwriting this pos *) wneuper@59292: fun insert_pt b EmptyPtree [] = Nd (b, []) wneuper@59292: | insert_pt _ EmptyPtree _ = raise PTREE "insert_pt b Empty _" wneuper@59292: | insert_pt _ (Nd ( _, _)) [] = raise PTREE "insert_pt b _ []" wneuper@59292: | insert_pt b (Nd (b', bs)) (p :: []) = Nd (b', repl_app bs p (Nd (b, []))) wneuper@59292: | insert_pt b (Nd (b', bs)) (p :: ps) = Nd (b', repl_app bs p (insert_pt b (nth p bs) ps)); wneuper@59292: wneuper@59292: (* insert children to a node without children. compare: fun insert_pt *) wneuper@59292: fun ins_chn _ EmptyPtree _ = raise PTREE "ins_chn: EmptyPtree" wneuper@59292: | ins_chn _ (Nd _) [] = raise PTREE "ins_chn: pos = []" wneuper@59292: | ins_chn ns (Nd (b, bs)) (p :: []) = wneuper@59292: if p > length bs wneuper@59292: then raise PTREE "ins_chn: pos not existent" wneuper@59292: else wneuper@59292: let wneuper@59292: val (b', bs') = case nth p bs of wneuper@59292: Nd (b', bs') => (b', bs') wneuper@59292: | _ => error "ins_chn: uncovered case nth" wneuper@59292: in wneuper@59292: if null bs' wneuper@59292: then Nd (b, repl_app bs p (Nd (b', ns))) wneuper@59292: else raise PTREE "ins_chn: pos mustNOT be overwritten" wneuper@59292: end wneuper@59292: | ins_chn ns (Nd (b, bs)) (p::ps) = Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps)); wneuper@59292: wneuper@59292: (* apply f to obj at pos, f: ppobj -> ppobj *) wneuper@59292: fun appl_to_node f (Nd (b, bs)) = Nd (f b, bs) wneuper@59292: | appl_to_node _ _ = error "appl_to_node: uncovered fun def."; wneuper@59292: fun appl_obj _ EmptyPtree [] = EmptyPtree wneuper@59292: | appl_obj _ EmptyPtree _ = raise PTREE "appl_obj f Empty _" wneuper@59292: | appl_obj f (Nd (b, bs)) [] = Nd (f b, bs) wneuper@59292: | appl_obj f (Nd (b, bs)) (p :: []) = Nd (b, repl_app bs p (((appl_to_node f) o (nth p)) bs)) wneuper@59292: | appl_obj f (Nd (b, bs)) (p :: ps) = Nd (b, repl_app bs p (appl_obj f (nth p bs) (ps:pos))); wneuper@59292: wneuper@59292: wneuper@59292: type ocalhd = wneuper@59292: bool * (* ALL itms+preconds true *) wneuper@59292: pos_ * (* model belongs to Problem | Method *) wneuper@59292: term * (* header: Problem... or Cas FIXME.0312: item for marking syntaxerrors *) wneuper@59405: Model.itm list * (* model: given, find, relate *) wneuper@59292: ((bool * term) list) *(* model: preconds *) wneuper@59405: Celem.spec; (* specification *) wneuper@59405: val e_ocalhd = (false, Und, Celem.e_term, [Model.e_itm], [(false, Celem.e_term)], Celem.e_spec); wneuper@59292: wneuper@59292: datatype ptform = Form of term | ModSpec of ocalhd; wneuper@59292: wneuper@59292: (* for cut_level; (deprecated) *) wneuper@59292: fun test_trans (PrfObj {branch, ...}) = true andalso branch = TransitiveB wneuper@59292: | test_trans (PblObj {branch, ...}) = true andalso branch = TransitiveB; wneuper@59292: wneuper@59292: fun is_pblobj' pt p = wneuper@59292: let val ppobj = get_obj I pt p wneuper@59292: in is_pblobj ppobj end; wneuper@59292: wneuper@59292: fun del_res (PblObj {cell, fmz, origin, spec, probl, meth, ctxt, env, loc= (l1, _), branch, ...}) = wneuper@59292: PblObj {cell = cell, fmz = fmz, origin = origin, spec = spec, probl = probl, meth = meth, wneuper@59292: ctxt = ctxt, env = env, loc= (l1, NONE), branch = branch, wneuper@59405: result = (Celem.e_term, []), ostate = Incomplete} wneuper@59292: | del_res (PrfObj {cell, form, tac, loc= (l1, _), branch, ...}) = wneuper@59292: PrfObj {cell = cell, form = form, tac = tac, loc = (l1, NONE), branch = branch, wneuper@59405: result = (Celem.e_term, []), ostate = Incomplete}; wneuper@59292: wneuper@59292: wneuper@59301: fun get_loc EmptyPtree _ = (Selem.e_istate, Selem.e_ctxt) wneuper@59292: | get_loc pt (p, Res) = wneuper@59292: (case get_obj g_loc pt p of wneuper@59292: (SOME i, NONE) => i wneuper@59301: | (NONE , NONE) => (Selem.e_istate, Selem.e_ctxt) wneuper@59292: | (_ , SOME i) => i) wneuper@59292: | get_loc pt (p, _) = wneuper@59292: (case get_obj g_loc pt p of wneuper@59292: (NONE , SOME i) => i (*13.8.02 just copied from ^^^: too liberal ?*) wneuper@59301: | (NONE , NONE) => (Selem.e_istate, Selem.e_ctxt) wneuper@59292: | (SOME i, _) => i); wneuper@59292: fun get_istate pt p = get_loc pt p |> #1; wneuper@59292: fun get_ctxt pt (pos as (p, p_)) = wneuper@59292: if member op = [Frm, Res] p_ wneuper@59292: then get_loc pt pos |> #2 (*for script interpretation rely on fun get_loc*) wneuper@59292: else get_obj g_ctxt pt p (*for specify phase take ctx from PblObj*) wneuper@59292: wneuper@59308: fun get_assumptions_ pt p = get_ctxt pt p |> Stool.get_assumptions; wneuper@59292: wneuper@59292: fun get_somespec' (dI, pI, mI) (dI', pI', mI') = wneuper@59292: let wneuper@59405: val domID = if dI = Celem.e_domID then dI' else dI wneuper@59405: val pblID = if pI = Celem.e_pblID then pI' else pI wneuper@59405: val metID = if mI = Celem.e_metID then mI' else mI wneuper@59292: in (domID, pblID, metID) end; wneuper@59292: wneuper@59292: (**.development for extracting an 'interval' from ptree.**) wneuper@59292: wneuper@59292: (*WN0510 version stopped in favour of get_interval with !!!move_dn, getFormulaeFromTo wneuper@59292: actually used (inefficient) version with move_dn: see modspec.sml*) wneuper@59292: local wneuper@59292: wneuper@59292: fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*) wneuper@59292: fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*) wneuper@59292: fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x; wneuper@59292: fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x; wneuper@59292: wneuper@59292: fun getnd i (b,p) q (Nd (po, nds)) = wneuper@59292: (if i <= 0 then [[b]] else []) @ wneuper@59292: (getnds (i-1) true (b@[hdp p], tlp p) (tlq q) wneuper@59292: (take_fromto (hdp p) (hdq q) nds)) wneuper@59292: wneuper@59292: and getnds _ _ _ _ [] = [] (*no children*) wneuper@59292: | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*) wneuper@59292: wneuper@59292: | getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*) wneuper@59292: (getnd i ( b, p ) [99999] n1) @ wneuper@59292: (getnd ~99999 (lev_on b,[0]) q n2) wneuper@59292: wneuper@59292: | getnds i _ (b,p) q [n1, n2] = (*intern, r-margin*) wneuper@59292: (getnd i ( b,[0]) [99999] n1) @ wneuper@59292: (getnd ~99999 (lev_on b,[0]) q n2) wneuper@59292: wneuper@59292: | getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*) wneuper@59292: (getnd i ( b, p ) [99999] nd) @ wneuper@59292: (getnds ~99999 false (lev_on b,[0]) q nds) wneuper@59292: wneuper@59292: | getnds i _ (b,p) q (nd::(nds as _::_)) = (*intern, ...*) wneuper@59292: (getnd i ( b,[0]) [99999] nd) @ wneuper@59292: (getnds ~99999 false (lev_on b,[0]) q nds); wneuper@59292: in wneuper@59292: (*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes wneuper@59292: where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous) wneuper@59292: (1) the 'f' are given wneuper@59292: (1a) by 'from' if 'f' = the respective element of 'from' (left margin) wneuper@59292: (1b) -inifinity, if 'f' > the respective element of 'from' (internal node) wneuper@59292: (2) the 't' ar given wneuper@59292: (2a) by 'to' if 't' = the respective element of 'to' (right margin) wneuper@59292: (2b) inifinity, if 't' < the respective element of 'to (internal node)' wneuper@59292: the 'f' and 't' are set by hdp,... *) wneuper@59292: fun get_trace pt p q = wneuper@59292: (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q))) wneuper@59292: (take_fromto (hdp p) (hdq q) (children pt)); wneuper@59292: end; wneuper@59292: wneuper@59292: (*extract a formula or model from ctree for itms2itemppc or model2xml*) wneuper@59292: fun preconds2str bts = wneuper@59405: (strs2str o (map (Celem.linefeed o pair2str o wneuper@59405: (apsnd Celem.term2str) o wneuper@59292: (apfst bool2str)))) bts; wneuper@59292: fun ocalhd2str (b, p, hdf, itms, prec, spec) = (* for tests only *) wneuper@59405: "(" ^ bool2str b ^ ", " ^ pos_2str p ^ ", " ^ Celem.term2str hdf ^ wneuper@59405: ", " ^ Model.itms2str_ (Celem.thy2ctxt' "Isac") itms ^ wneuper@59405: ", " ^ preconds2str prec ^ ", \n" ^ Celem.spec2str spec ^ " )"; wneuper@59292: wneuper@59292: fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj wneuper@59292: | is_pblnd _ = error "is_pblnd: uncovered fun def."; wneuper@59292: wneuper@59292: wneuper@59292: (* determine the previous pos' on the same level wneuper@59292: WN0502 made for interSteps; _only_ works for branch TransitiveB WN120517 compare lev_back *) wneuper@59292: fun lev_pred' _ ([], Res) = ([], Pbl) wneuper@59292: | lev_pred' pt (p, Res) = wneuper@59292: let val (p', last) = split_last p wneuper@59292: in wneuper@59292: if last = 1 wneuper@59292: then if (is_pblobj o (get_obj I pt)) p then (p, Pbl) else (p, Frm) wneuper@59292: else if get_obj g_res pt (p' @ [last - 1]) = get_obj g_form pt p wneuper@59292: then (p' @ [last - 1], Res) (* TransitiveB *) wneuper@59292: else if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm) wneuper@59292: end wneuper@59292: | lev_pred' _ _ = error ""; wneuper@59292: wneuper@59292: wneuper@59292: (**.insert into ctree and cut branches accordingly.**) wneuper@59292: wneuper@59292: (* get all positions of certain intervals on the ctree. wneuper@59292: OLD VERSION without move_dn; kept for occasional redesign wneuper@59292: get all pos's to be cut in a ctree wneuper@59292: below a pos or from a ctree list after i-th element (NO level_up) *) wneuper@59292: fun get_allpos' (_, _) EmptyPtree = [] wneuper@59292: | get_allpos' (p, 1) (Nd (b, bs)) = (* p is pos of Nd *) wneuper@59292: if g_ostate b = Incomplete wneuper@59292: then (p, Frm) :: (get_allpos's (p, 1) bs) wneuper@59292: else (p, Frm) :: (get_allpos's (p, 1) bs) @ [(p, Res)] wneuper@59292: | get_allpos' (p, i) (Nd (b, bs)) = (* p is pos of Nd *) wneuper@59292: if length bs > 0 orelse is_pblobj b wneuper@59292: then if g_ostate b = Incomplete wneuper@59292: then [(p,Frm)] @ (get_allpos's (p, 1) bs) wneuper@59292: else [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p, Res)] wneuper@59292: else if g_ostate b = Incomplete then [] else [(p, Res)] wneuper@59292: and get_allpos's _ [] = [] wneuper@59292: | get_allpos's (p, i) (pt :: pts) = (* p is pos of parent-Nd *) wneuper@59292: (get_allpos' (p @ [i], i) pt) @ (get_allpos's (p, i + 1) pts); wneuper@59292: wneuper@59292: (*WN050106 like cut_level, but deletes exactly 1 node *) wneuper@59292: fun cut_level_'_ _ _ EmptyPtree _ =raise PTREE "cut_level_'_ Empty _" (* for tests ONLY *) wneuper@59292: | cut_level_'_ _ _ (Nd ( _, _)) ([], _) = raise PTREE "cut_level_'_ _ []" wneuper@59292: | cut_level_'_ cuts P (Nd (b, bs)) (p :: [], p_) = wneuper@59292: if test_trans b wneuper@59292: then wneuper@59292: (Nd (b, drop_nth [] (p:posel, bs)), wneuper@59292: cuts @ (if p_ = Frm then [(P @ [p], Res)] else []) @ wneuper@59292: (get_allpos's (P, p + 1) (drop_nth [] (p, bs)))) wneuper@59292: else (Nd (b, bs), cuts) wneuper@59292: | cut_level_'_ cuts P (Nd (b, bs)) ((p :: ps), p_) = wneuper@59292: let wneuper@59292: val (bs', cuts') = cut_level_'_ cuts P (nth p bs) (ps, p_) wneuper@59292: in (Nd (b, repl_app bs p bs'), cuts @ cuts') end; wneuper@59292: wneuper@59292: fun cut_level _ _ EmptyPtree _ = raise PTREE "cut_level EmptyPtree _" wneuper@59292: | cut_level _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level _ []" wneuper@59292: | cut_level cuts P (Nd (b, bs)) (p :: [], p_) = wneuper@59292: if test_trans b wneuper@59292: then wneuper@59292: (Nd (b, take (p:posel, bs)), wneuper@59292: cuts @ wneuper@59292: (if p_ = Frm andalso (*#*) g_ostate b = Complete then [(P@[p],Res)] else ([]:pos' list)) @ wneuper@59292: (get_allpos's (P, p+1) (takerest (p, bs)))) wneuper@59292: else (Nd (b, bs), cuts) wneuper@59292: | cut_level cuts P (Nd (b, bs)) ((p :: ps), p_) = wneuper@59292: let wneuper@59292: val (bs', cuts') = cut_level cuts P (nth p bs) (ps, p_) wneuper@59292: in (Nd (b, repl_app bs p bs'), cuts @ cuts') end; wneuper@59292: wneuper@59292: (*OLD version before WN050219, overwritten below*) wneuper@59292: fun cut_tree _ ([], _) = raise PTREE "cut_tree _ ([],_)" (* for test only *) wneuper@59292: | cut_tree pt (pos as ([_], _)) = wneuper@59292: let wneuper@59292: val (pt', cuts) = cut_level [] [] pt pos wneuper@59292: in wneuper@59292: (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete then [] else [([], Res)])) wneuper@59292: end wneuper@59292: | cut_tree pt (p,p_) = wneuper@59292: let wneuper@59292: fun cutfn pt cuts (p, p_) = wneuper@59292: let wneuper@59292: val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_) wneuper@59292: in wneuper@59292: if length cuts' > 0 andalso length p > 1 wneuper@59292: then cutfn pt' (cuts @ cuts') (lev_up p, Frm(*-->(p,Res)*)) wneuper@59292: else (pt', cuts @ cuts') wneuper@59292: end wneuper@59292: val (pt', cuts) = cutfn pt [] (p, p_) wneuper@59292: in wneuper@59292: (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete then [] else [([], Res)])) wneuper@59292: end; wneuper@59292: wneuper@59296: local wneuper@59296: fun move_dn _ (Nd (_, ns)) ([],p_) = (* root problem *) wneuper@59296: (case p_ of wneuper@59296: Res => raise PTREE "move_dn: end of calculation" wneuper@59296: | _ => wneuper@59296: if null ns (* go down from Pbl + Met *) wneuper@59296: then raise PTREE "move_dn: solve problem not started" wneuper@59296: else ([1], Frm)) wneuper@59296: | move_dn P (Nd (_, ns)) (p :: (ps as (_ :: _)), p_) = (* iterate to end of pos *) wneuper@59296: if p > length ns wneuper@59296: then raise PTREE "move_dn: pos not existent 2" wneuper@59296: else move_dn (P @ [p]) (nth p ns) (ps, p_) wneuper@59296: | move_dn P (Nd (c, ns)) ([p], p_) = (* act on last element of pos *) wneuper@59296: if p > length ns wneuper@59296: then raise PTREE "move_dn: pos not existent 3" wneuper@59296: else wneuper@59296: (case p_ of wneuper@59296: Res => wneuper@59296: if p = length ns (* last Res on this level: go a level up *) wneuper@59296: then if g_ostate c = Complete wneuper@59296: then (P, Res) wneuper@59296: else raise PTREE (ints2str' P ^ " not complete 1") wneuper@59296: else (* go to the next Nd on this level, or down into the next Nd *) wneuper@59296: if is_pblnd (nth (p + 1) ns) then (P@[p + 1], Pbl) wneuper@59296: else if g_res' (nth p ns) = g_form' (nth (p + 1) ns) wneuper@59296: then if (null o children o (nth (p + 1))) ns wneuper@59296: then (* take the Res if Complete *) wneuper@59296: if g_ostate' (nth (p + 1) ns) = Complete wneuper@59296: then (P@[p + 1], Res) wneuper@59296: else raise PTREE (ints2str' (P@[p + 1]) ^ " not complete 2") wneuper@59296: else (P@[p + 1, 1], Frm) (* go down into the next PrfObj *) wneuper@59296: else (P@[p + 1], Frm) (* take Frm: exists if the Nd exists *) wneuper@59296: | Frm => (*go down or to the Res of this Nd*) wneuper@59296: if (null o children o (nth p)) ns wneuper@59296: then if g_ostate' (nth p ns) = Complete then (P @ [p], Res) wneuper@59296: else raise PTREE (ints2str' (P @ [p])^" not complete 3") wneuper@59296: else (P @ [p, 1], Frm) wneuper@59296: | _ => (* is Pbl or Met *) wneuper@59296: if (null o children o (nth p)) ns wneuper@59296: then raise PTREE "move_dn:solve subproblem not startd" wneuper@59296: else (P @ [p, 1], wneuper@59296: if (is_pblnd o hd o children o (nth p)) ns wneuper@59296: then Pbl else Frm)) wneuper@59296: | move_dn _ _ _ = error ""; wneuper@59296: in wneuper@59292: (* get all positions in a ctree until ([],Res) or ostate=Incomplete wneuper@59292: val get_allp = fn : wneuper@59292: pos' list -> : accumulated, start with [] wneuper@59292: pos -> : the offset for subtrees wrt the root wneuper@59292: ctree -> : (sub)tree wneuper@59292: pos' : initialization (the last pos' before ...) wneuper@59292: -> pos' list : of positions in this (sub) tree (relative to the root) wneuper@59292: *) wneuper@59292: fun get_allp cuts (P, pos) pt = wneuper@59292: (let wneuper@59292: val nxt = move_dn [] pt pos (*exn if Incomplete reached*) wneuper@59292: in wneuper@59292: if nxt <> ([], Res) wneuper@59292: then get_allp (cuts @ [nxt]) (P, nxt) pt wneuper@59292: else map (apfst (curry op @ P)) (cuts @ [nxt]) wneuper@59292: end) wneuper@59292: handle PTREE _ => (map (apfst (curry op@ P)) cuts); wneuper@59296: end wneuper@59292: wneuper@59292: (* the pts are assumed to be on the same level *) wneuper@59292: fun get_allps cuts _ [] = cuts wneuper@59292: | get_allps cuts P (pt :: pts) = wneuper@59292: let wneuper@59292: val below = get_allp [] (P, ([], Frm)) pt wneuper@59292: val levfrm = wneuper@59292: if is_pblnd pt wneuper@59292: then (P, Pbl) :: below wneuper@59292: else if last_elem P = 1 wneuper@59292: then (P, Frm) :: below wneuper@59292: else (*Trans*) below wneuper@59292: val levres = levfrm @ (if null below then [(P, Res)] else []) wneuper@59292: in wneuper@59292: get_allps (cuts @ levres) (lev_on P) pts wneuper@59292: end; wneuper@59292: wneuper@59292: (** these 2 funs decide on how far cut_tree goes **) wneuper@59292: (* shall the nodes _after_ the pos to be inserted at be deleted? wneuper@59292: shall cutting be continued on the higher level(s)? the Nd regarded will NOT be changed *) wneuper@59292: fun test_trans (PrfObj {branch, ...}) = (branch = TransitiveB orelse branch = NoBranch) wneuper@59292: | test_trans (PblObj {branch, ...}) = (branch = TransitiveB orelse branch = NoBranch); wneuper@59292: wneuper@59292: (* cut_bottom new sml603..608 wneuper@59292: cut the level at the bottom of the pos (used by cappend_...) wneuper@59292: and handle the parent in order to avoid extra case for root wneuper@59292: fn: ctree -> : the _whole_ ctree for cut_levup wneuper@59292: pos * posel -> : the pos after split_last wneuper@59292: ctree -> : the parent of the Nd to be cut wneuper@59292: return wneuper@59292: (ctree * : the updated ctree wneuper@59292: pos' list) * : the pos's cut wneuper@59292: bool : cutting shall be continued on the higher level(s) wneuper@59292: *) wneuper@59292: fun cut_bottom _ (pt' as Nd (b, [])) = ((pt', []), test_trans b) wneuper@59292: | cut_bottom (P, p) (Nd (b, bs)) = wneuper@59292: let (*divide level into 3 parts...*) wneuper@59292: val keep = take (p - 1, bs) wneuper@59292: val pt' = case nth p bs of wneuper@59292: pt' as Nd _ => pt' wneuper@59292: | _ => error "cut_bottom: uncovered case nth p bs" wneuper@59292: (*^^^^^_here_ will be 'insert_pt'ed by 'append_..'*) wneuper@59292: val (tail, _) = (takerest (p, bs), if null (takerest (p, bs)) then 0 else p + 1) wneuper@59292: val (children, cuts) = wneuper@59292: if test_trans b wneuper@59292: then wneuper@59292: (keep, (if is_pblnd pt' then [(P @ [p], Pbl)] else []) wneuper@59292: @ (get_allp [] (P @ [p], (P, Frm)) pt') wneuper@59292: @ (get_allps [] (P @ [p + 1]) tail)) wneuper@59292: else (keep @ [(*'insert_pt'ed by 'append_..'*)] @ tail, wneuper@59292: get_allp [] (P @ [p], (P, Frm)) pt') wneuper@59292: val (pt'', cuts) = wneuper@59292: if test_trans b wneuper@59292: then (Nd (del_res b, children), cuts @ (if g_ostate b = Incomplete then [] else [(P, Res)])) wneuper@59292: else (Nd (b, children), cuts) wneuper@59292: in ((pt'', cuts), test_trans b) end wneuper@59292: | cut_bottom _ _ = error "cut_bottom: uncovered fun def."; wneuper@59292: wneuper@59292: wneuper@59292: (* go all levels from the bottom of 'pos' up to the root, wneuper@59292: on each level compose the children of a node and accumulate the cut Nds wneuper@59292: args wneuper@59292: pos' list -> : for accumulation wneuper@59292: bool -> : cutting shall be continued on the higher level(s) wneuper@59292: ctree -> : the whole ctree for 'get_nd pt P' on each level wneuper@59292: ctree -> : the Nd from the lower level for insertion at path wneuper@59292: pos * posel -> : pos=path split for convenience wneuper@59292: ctree -> : Nd the children of are under consideration on this call wneuper@59292: returns : wneuper@59292: ctree * pos' list : the updated parent-Nd and the pos's of the Nds cut wneuper@59292: *) wneuper@59292: fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) = wneuper@59292: let (*divide level into 3 parts...*) wneuper@59292: val keep = take (p - 1, bs) wneuper@59292: (*val pt' comes as argument from below*) wneuper@59292: val (tail, _) = wneuper@59292: (takerest (p, bs), if null (takerest (p, bs)) then 0 else p + 1) wneuper@59292: val (children, cuts') = wneuper@59292: if clevup wneuper@59292: then (keep @ [pt'], get_allps [] (P @ [p+1]) tail) wneuper@59292: else (keep @ [pt'] @ tail, []) wneuper@59292: val clevup' = if clevup then test_trans b else false wneuper@59292: (*the first Nd with false stops cutting on all levels above*) wneuper@59292: val (pt'', cuts') = wneuper@59292: if clevup' wneuper@59292: then (Nd (del_res b, children), cuts' @ (if g_ostate b = Incomplete then [] else [(P, Res)])) wneuper@59292: else (Nd (b, children), cuts') wneuper@59292: in wneuper@59292: if null P wneuper@59292: then (pt'', cuts @ cuts') wneuper@59292: else wneuper@59292: let val (P, p) = split_last P wneuper@59292: in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P) end wneuper@59292: end wneuper@59292: | cut_levup _ _ _ _ _ _ = error "cut_levup: uncovered fun def."; wneuper@59292: wneuper@59292: (* cut nodes after and below an inserted node in the ctree; wneuper@59292: the cuts range is limited by the predicate 'fun cutlevup' *) wneuper@59292: fun cut_tree pt (pos, _) = wneuper@59292: if not (existpt pos pt) wneuper@59292: then (pt,[]) (*appending a formula never cuts anything*) wneuper@59292: else wneuper@59292: let wneuper@59292: val (P, p) = split_last pos wneuper@59292: val ((pt', cuts), clevup) = cut_bottom (P, p) (get_nd pt P) wneuper@59292: (* pt' is the updated parent of the Nd to cappend_..*) wneuper@59292: in wneuper@59292: if null P wneuper@59292: then (pt', cuts) wneuper@59292: else wneuper@59292: let val (P, p) = split_last P wneuper@59292: in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P) end wneuper@59292: end; wneuper@59292: wneuper@59292: (* get the theory explicitly specified for the rootpbl; wneuper@59292: thus use this function _after_ finishing specification *) wneuper@59405: fun rootthy (Nd (PblObj {spec = (thyID, _, _), ...}, _)) = Celem.assoc_thy thyID wneuper@59292: | rootthy _ = error "rootthy: uncovered fun def."; wneuper@59292: wneuper@59292: (**) wneuper@59292: end; wneuper@59292: (**)