(* Title: the calctree, which holds a calculation

    Author: Walther Neuper 1999

    (c) due to copyright terms

 Definitions required for Ctree, renamed later appropriately

 *)

 signature BASIC_CALC_TREE =

 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

   val g_met : ppobj -> Model_Def.i_model

   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>\<open>

   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

 \<close>

 end

 (**)

 structure CTbasic(**): BASIC_CALC_TREE(**) =

 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>\<open>

 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";

 \<close>

 datatype ostate = 

     Incomplete | Complete | Inconsistent (* WN041020 latter still unused *);

 \<^isac_test>\<open>

 fun ostate2str Incomplete = "Incomplete"

   | ostate2str Complete = "Complete"

   | ostate2str Inconsistent = "Inconsistent";

 \<close>

 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;

 \<^isac_test>\<open>

 fun ets2s (l,(m,eno,env,iar,res,s)) = 

   "\n(" ^ TermC.string_of_path l ^ ",(" ^ Tactic.string_of m ^

   ",\n  ens= " ^ Env.subst2str eno ^

   ",\n  env= " ^ Env.subst2str env ^

   ",\n  iar= " ^ UnparseC.term iar ^

   ",\n  res= " ^ UnparseC.term res ^

   ",\n  " ^ Celem.safe2str s ^ "))";

 fun ets2str (ets: ets) = (strs2str o (map ets2s)) ets;

 \<close>

 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, (* from init:FIXME never use this spec;-drop                     *)

     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,(* = I_Model.T for interactive input to a Problem                *)

     meth  : Model_Def.i_model,(* = 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_in_ctxt 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>\<open> get_obj f (nth p bs) ps \<close> 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>\<open> get_nd (nth p nds) ps \<close> 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>\<open>

 fun g_fmz (PblObj {fmz = f, ...}) = f

   | g_fmz _ = raise PTREE "g_fmz not for PrfObj";

 \<close>

 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>\<open>

 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;

 \<close>

 (*\--------------- 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>\<open>

 fun test_trans (PrfObj {branch, ...}) = true andalso branch = TransitiveB

   | test_trans (PblObj {branch, ...}) = true andalso branch = TransitiveB;

 \<close>

 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 (ThyC.get_theory "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>\<open>

 (*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) o 

 	  (apfst bool2str)))) bts;

 fun ocalhd2str (b, p, hdf, itms, prec, spec) =

     "(" ^ bool2str b ^ ", " ^ pos_2str p ^ ", " ^ UnparseC.term hdf ^

     ", " ^ "\<forall>itms2str itms\<forall>" (*Model_Def.itms2str_ (ThyC.id_to_ctxt "Isac_Knowledge") itms*) ^

     ", " ^ preconds2str prec ^ ", \n" ^ References_Def.to_string spec ^ " )";

 \<close>

 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>\<open>

 (* 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;

 \<close>

 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_PIDE ctxt thyID

   | root_thy _ = raise ERROR "root_thy: uncovered fun def.";

 (**)

 end;

 (**)