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