(* Title: the calctree, which holds a calculation

   Author: Walther Neuper 1999

   (c) due to copyright terms

*)

signature BASIC_CALC_TREE =

sig (* vvv--- *.sml require these typs incrementally, with these exception -----------------vvv *)

  (*===\<Longrightarrow> other ?mstools.sml? =================================================================*)

  type state

  type con

  eqtype posel

  type pos = posel list

  val pos2str : int list -> string                                         (* for datatypes.sml *)

  datatype pos_ = Frm | Met | Pbl | Res | Und

  val pos_2str : pos_ -> string

  type pos'

  val pos'2str : pos' -> string

  val str2pos_ : string -> pos_                                            (* for datatypes.sml *)

  val e_pos' : pos'

  (* for generate.sml ?!? ca.*)

  eqtype cellID

  datatype branch  = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB

  datatype ostate = Complete | Incomplete | Inconsistent

  datatype ppobj =

    PblObj of

     {branch: branch,

      cell: Celem.lrd option,

      loc: (Selem.istate * Proof.context) option * (Selem.istate * Proof.context) option,

      ostate: ostate,

      result: Selem.result,

      fmz: Selem.fmz,

      origin: Model.ori list * Celem.spec * term,

      probl: Model.itm list,

      meth: Model.itm list,

      spec: Celem.spec,

      ctxt: Proof.context,

      env: (Selem.istate * Proof.context) option}

  | PrfObj of

     {branch: branch,

      cell: Celem.lrd option,

      loc: (Selem.istate * Proof.context) option * (Selem.istate * Proof.context) option,

      ostate: ostate,

      result: Selem.result,

      form: term,

      tac: Tac.tac}

  datatype ctree = EmptyPtree | Nd of ppobj * ctree list

  val e_ctree : ctree (* TODO: replace by EmptyPtree*)

  val existpt' : pos' -> ctree -> bool                                     (* for interface.sml *)

  val is_interpos : pos' -> bool                                           (* for interface.sml *)

  val lev_pred' : ctree -> pos' -> pos'                                    (* for interface.sml *)

  val ins_chn : ctree list -> ctree -> pos -> ctree                       (* for solve.sml *)

  val children : ctree -> ctree list                                           (* for solve.sml *)

  val get_nd : ctree -> pos -> ctree                                           (* for solve.sml *)

  val just_created_ : ppobj -> bool                                       (* for mathengine.sml *)

  val just_created : state -> bool                                        (* for mathengine.sml *)

  val e_origin : Model.ori list * Celem.spec * term                       (* for mathengine.sml *)

  val is_pblobj : ppobj -> bool

  val is_pblobj' : ctree -> pos -> bool

  val is_pblnd : ctree -> bool

  val g_spec : ppobj -> Celem.spec

  val g_loc : ppobj -> (Selem.istate * Proof.context) option * (Selem.istate * Proof.context) option

  val g_form : ppobj -> term

  val g_pbl : ppobj -> Model.itm list

  val g_met : ppobj -> Model.itm list

  val g_metID : ppobj -> Celem.metID

  val g_result : ppobj -> Selem.result

  val g_tac : ppobj -> Tac.tac

  val g_domID : ppobj -> Celem.domID                     (* for appl.sml TODO: replace by thyID *)

  val g_env : ppobj -> (Selem.istate * Proof.context) option                    (* for appl.sml *)

  val g_origin : ppobj -> Model.ori list * Celem.spec * term                  (* for script.sml *)

  val get_loc : ctree -> pos' -> Selem.istate * Proof.context                 (* for script.sml *)

  val get_istate : ctree -> pos' -> Selem.istate                              (* for script.sml *)

  val get_ctxt : ctree -> pos' -> Proof.context

  val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a

  val get_curr_formula : state -> term

  val get_assumptions_ : ctree -> pos' -> term list                             (* for appl.sml *)

  val is_e_ctxt : Proof.context -> bool                                         (* for appl.sml *)

  val new_val : term -> Selem.istate -> Selem.istate

  (* for calchead.sml *)

  type cid = cellID list

  type ocalhd = bool * pos_ * term * Model.itm list * (bool * term) list * Celem.spec

  datatype ptform = Form of term | ModSpec of ocalhd

  val get_somespec' : Celem.spec -> Celem.spec -> Celem.spec

  exception PTREE of string;

  val par_pbl_det : ctree -> pos -> bool * pos * Celem.rls                      (* for appl.sml *)

  val rootthy : ctree -> theory                                               (* for script.sml *)

(* ---- made visible ONLY for structure CTaccess : CALC_TREE_ACCESS --------------------------- *)

  val appl_obj : (ppobj -> ppobj) -> ctree -> pos -> ctree

  val existpt : pos -> ctree -> bool                                          (* also for tests *)

  val cut_tree : ctree -> pos * 'a -> ctree * pos' list                       (* also for tests *)

  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_on : CTbasic.pos -> CTbasic.pos                        (* duplicate in ctree-navi.sml *)

  val lev_dn : CTbasic.pos -> CTbasic.pos                        (* duplicate in ctree-navi.sml *)

  val par_pblobj : CTbasic.ctree -> CTbasic.pos -> CTbasic.pos   (* duplicate in ctree-navi.sml *)

   ---- duplicates in CTnavi, reconsider structs ----------------------------------------------/*)

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

  val pr_ctree : (pos -> ppobj -> string) -> ctree -> string

  val pr_short : pos -> ppobj -> string

  val g_ctxt : ppobj -> Proof.context

  val g_fmz : ppobj -> Selem.fmz

  val get_allp : pos' list -> pos * (int list * pos_) -> ctree -> pos' list

  val get_allps : (pos * pos_) list -> posel list -> ctree list -> pos' list

  val get_allpos' : pos * posel -> ctree -> pos' list

  val get_allpos's : pos * posel -> ctree list -> (pos * pos_) list

  val cut_bottom : pos * posel -> ctree -> (ctree * pos' list) * bool

  val cut_level : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list

  val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list

  val get_trace : ctree -> int list -> int list -> int list list

  val branch2str : branch -> string

( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

(*----- unused code, kept as hints to design ideas ---------------------------------------------*)

  (* NONE *)

end

(**)

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

struct

(**)

type env = (term * term) list;

datatype branch = 

	NoBranch | AndB | OrB 

| TransitiveB  (* FIXXXME.0308: set branch from met in Apply_Method

                  FIXXXME.0402: -"- in Begin_Trans'*)

| SequenceB | IntersectB | CollectB | MapB;

fun branch2str NoBranch = "NoBranch" (* for tests only *)

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

fun ostate2str Incomplete = "Incomplete" (* for tests only *)

  | ostate2str Complete = "Complete"

  | ostate2str Inconsistent = "Inconsistent";

type cellID = int;     

type cid = cellID list;

type posel = int; (* for readability in funs accessing Ctree *)

type pos = int list;

val pos2str = ints2str';

datatype pos_ = 

  Pbl    (* PblObj-position: problem-type                   *)

| Met    (* PblObj-position: method                         *)

| Frm    (* PblObj-position: -> Pbl in ME (not by moveDown !)

         |  PrfObj-position: formula                        *)

| Res    (* PblObj | PrfObj-position: result                *)

| Und;   (* undefined*)

fun pos_2str Pbl = "Pbl"

  | pos_2str Met = "Met"

  | pos_2str Frm = "Frm"

  | pos_2str Res = "Res"

  | pos_2str Und = "Und";

fun str2pos_ "Pbl" = Pbl

  | str2pos_ "Met" = Met

  | str2pos_ "Frm" = Frm

  | str2pos_ "Res" = Res

  | str2pos_ "Und" = Und

  | str2pos_ str = error ("str2pos_: wrong argument = " ^ str)

type pos' = pos * pos_;

(*WN0312 remembering interator (pos * pos_) for ctree 

	   pos : lev_on, lev_dn, lev_up

     pos_:

# generate1 sets pos_ if possible  ...?WN0502?NOT...

# generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn

                     exceptions: Begin/End_Trans

# thus generate(1) called in

.# assy, locate_gen 

.# nxt_solv (tac_ -cases); general case: 

  val pos' = case pos' of (p,Res) => (lev_on p',Res) | _ => pos'

# WN050220, S(604):

  generate1...(Rewrite(f,..,res))..(pos, pos_)

     cappend_atomic.................pos //////  gets f+res always!!!

        cut_tree....................pos, pos_ 

*)

fun pos'2str (p, p_) = pair2str (ints2str' p, pos_2str p_);

fun pos's2str ps = (strs2str' o (map pos'2str)) ps; (* for tests only *)

val e_pos' = ([], Und);

(* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*)

fun is_e_ctxt ctxt = Context.eq_thy (Proof_Context.theory_of ctxt, @{theory "Pure"});

type iist = Selem.istate option * Selem.istate option;

(*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*) 

fun new_val v (Selem.ScrState (env, loc_, topt, _, safe, bool)) =

    (Selem.ScrState (env, loc_, topt, v, safe, bool))

  | new_val _ _ = error "new_val: only for ScrState";

datatype con = land | lor;

(* executed tactics (tac_s) with local environment etc.;

  used for continuing eval script + for generate *)

type ets =

  (Celem.loc_ *(* of tactic in scr, tactic (weakly) associated with tac_                   *)

   (Tac.tac_ * (* (for generate)                                                           *)

    env *      (* with 'tactic=result' as  rule, tactic ev. _not_ ready for 'parallel let' *)

    env *      (* with results of (ready) tacs                                             *)

    term *     (* itr_arg of tactic, for upd. env at Repeat, Try                           *)

    term *     (* result value of the tac                                                  *)

    Selem.safe))

  list;

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

  "\n(" ^ Celem.loc_2str l ^ ",(" ^ Tac.tac_2str m ^

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

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

  ",\n  iar= " ^ Celem.term2str iar ^

  ",\n  res= " ^ Celem.term2str res ^

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

fun ets2str (ets: ets) = (strs2str o (map ets2s)) ets; (* for tests only *)

type envp =(*9.5.03: unused, delete with field in ctree.PblObj FIXXXME*)

  (int * term list) list * (* assoc-list: args of met*)

  (int * rls) list *       (* assoc-list: tacs already done ///15.9.00*)

  (int * ets) list *       (* assoc-list: tacs etc. already done*)

  (string * pos) list;     (* asms * from where*)

datatype ppobj = (* TODO: arrange according to signature *)

  PrfObj of 

   {cell  : Celem.lrd option, (* where in form tac has been applied, FIXME.WN0607 rename field *)

	  form  : term,             (* where tac is applied to                                       *)

	  tac   : Tac.tac,           (* also in istate                                                *)

	  loc   : (Selem.istate *   (* script interpreter state                                      *)

	           Proof.context)   (* context for provers, type inference                           *)

            option *          (* both for interpreter location on Frm, Pbl, Met                *)

            (Selem.istate *   (* script interpreter state                                      *)

             Proof.context)   (* context for provers, type inference                           *)

            option,           (* both for interpreter location on Res                          *)

                              (*(NONE,NONE) <==> e_istate ! see update_loc, get_loc            *)

	  branch: branch,           (* only rudimentary                                              *)

	  result: Selem.result,     (* result and assumptions                                        *)

	  ostate: ostate}           (* Complete <=> result is OK                                     *)

| PblObj of 

   {cell  : Celem.lrd option, (* unused: meaningful only for some _Prf_Obj                     *)

    fmz   : Selem.fmz,        (* from init:FIXME never use this spec;-drop                     *)

    origin: (Model.ori list) *      (* representation from fmz+pbt

                                 for efficiently adding items in probl, meth                   *)

	           Celem.spec *     (* updated by Refine_Tacitly                                     *)

	           term,            (* headline of calc-head, as calculated initially(!)             *)

    spec  : Celem.spec,       (* explicitly input                                              *)

    probl : Model.itm list,   (* itms explicitly input                                         *)

    meth  : Model.itm list,   (* itms automatically added to copy of probl                     *)

    ctxt  : Proof.context,    (* WN110513 introduced to avoid [*] [**]                         *)

    env   : (Selem.istate * Proof.context) option, (* istate only for initac in script              

                                 context for specify phase on this node NO..                  

..NO: this conflicts with init_form/initac: see Apply_Method without init_form                 *)

    loc   : (Selem.istate * Proof.context) option * (Selem.istate * (* like PrfObj                         *)

              Proof.context) option, (* for spec-phase [*], NO..

..NO: raises errors not tracable on WN110513 [**]                                              *)                               

    branch: branch,           (* like PrfObj                                                   *)

    result: Selem.result,     (* like PrfObj                                                   *)

    ostate: ostate};          (* like PrfObj                                                   *)

(* 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 'init_form' 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'

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"               (* for tests only *)

  | pr_short p (PrfObj {form = form, ...}) = pr_pos p ^ Celem.term2str form ^ "\n";

fun pr_ctree f pt =                                                            (* for tests only *)

  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 [] 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) =

    let

      val _ = (nth p bs)

      handle _ => raise PTREE ("get_obj: pos = " ^ ints2str' (p::ps) ^ " does not exist");

    in

      (get_obj f (nth p bs) ps) 

      handle _ => raise PTREE ("get_obj: pos = " ^ ints2str' (p::ps) ^ " does not exist")

    end;

fun get_nd EmptyPtree _ = raise PTREE "get_nd EmptyPtree"

  | get_nd n [] = n

  | get_nd (Nd (_, nds)) (pos as p :: ps) = (get_nd (nth p nds) ps)

    handle _ => 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' _ = 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";

fun g_fmz (PblObj {fmz = f, ...}) = f                                        (* for tests only *)

  | 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_env    (PblObj {env, ...}) = env

  | g_env    _ = raise PTREE "g_env 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),...}) = Tac.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);

(* 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 = Celem.e_spec

  | just_created_ _ = raise PTREE "g_ostate': uncovered fun def.";

val e_origin = ([], Celem.e_spec, Celem.e_term);

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 _ = error "children: uncovered fun def.";

(*/--------------- duplicates in ctree-navi.sml: required also here below ---------------\*)

fun lev_on [] = raise PTREE "lev_on []"

  | lev_on pos = 

    let val len = length pos

    in (drop_last pos) @ [(nth len pos)+1] end;

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 ---------------/*)

(* find the next parent, which is either a PblObj (return true)

  or a PrfObj with tac = Detail_Set (return false)

  FIXME.030403: re-organize par_pbl_det after rls' --> rls*)

fun par_pbl_det pt [] = (true, [], Celem.Erls)

  | par_pbl_det pt p =

    let

      fun par _ [] = (true, [], Celem.Erls)

        | par pt p =

          if is_pblobj (get_obj I pt p)

          then (true, p, Celem.Erls)

		      else case get_obj g_tac pt p of

				    Tac.Rewrite_Set rls' => (false, p, assoc_rls rls')

			    | Tac.Rewrite_Set_Inst (_, rls') => (false, p, assoc_rls rls')

			    | _ => par pt (lev_up p)

    in par pt (lev_up p) end; 

(* 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 _ (Nd ( _,  _)) [] = raise PTREE "insert_pt 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')

        | _ => 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 _ _ = 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)));

type ocalhd =

  bool *                (* ALL itms+preconds true                                              *)

  pos_ *                (* model belongs to Problem | Method                                   *)

  term *                (* header: Problem... or Cas FIXME.0312: item for marking syntaxerrors *)

  Model.itm list *      (* model: given, find, relate                                          *)

  ((bool * term) list) *(* model: preconds                                                     *)

  Celem.spec;           (* specification                                                       *)

val e_ocalhd = (false, Und, Celem.e_term, [Model.e_itm], [(false, Celem.e_term)], Celem.e_spec);

datatype ptform = Form of term | ModSpec of ocalhd;

(* for cut_level;   (deprecated) *)

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 {cell, fmz, origin, spec, probl, meth, ctxt, env, loc= (l1, _), branch, ...}) =

    PblObj {cell = cell, fmz = fmz, origin = origin, spec = spec, probl = probl, meth = meth,

	    ctxt = ctxt, env = env, loc= (l1, NONE), branch = branch,

	    result = (Celem.e_term, []), ostate = Incomplete}

  | del_res (PrfObj {cell, form, tac, loc= (l1, _), branch, ...}) =

    PrfObj {cell = cell, form = form, tac = tac, loc = (l1, NONE), branch = branch, 

	    result = (Celem.e_term, []), ostate = Incomplete};

fun get_loc EmptyPtree _ = (Selem.e_istate, Selem.e_ctxt)

  | get_loc pt (p, Res) =

    (case get_obj g_loc pt p of

      (SOME i, NONE) => i

    | (NONE  , NONE) => (Selem.e_istate, Selem.e_ctxt)

    | (_     , SOME i) => i)

  | get_loc pt (p, _) =

    (case get_obj g_loc pt p of

      (NONE  , SOME i) => i (*13.8.02 just copied from ^^^: too liberal ?*)

    | (NONE  , NONE) => (Selem.e_istate, Selem.e_ctxt)

    | (SOME i, _) => i);

fun get_istate pt p = get_loc pt p |> #1;

fun get_ctxt pt (pos as (p, p_)) =

  if member op = [Frm, Res] p_

  then get_loc pt pos |> #2 (*for script interpretation rely on fun get_loc*)

  else get_obj g_ctxt pt p (*for specify phase take ctx from PblObj*)

fun get_assumptions_ pt p = get_ctxt pt p |> Stool.get_assumptions;

fun get_somespec' (dI, pI, mI) (dI', pI', mI') =

  let

    val domID = if dI = Celem.e_domID then dI' else dI

  	val pblID = if pI = Celem.e_pblID then pI' else pI

  	val metID = if mI = Celem.e_metID then mI' else mI

  in (domID, pblID, metID) end;

(**.development for extracting an 'interval' from ptree.**)

(*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 (po, 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))

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,p) 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,p) 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 (Celem.linefeed o pair2str o

	  (apsnd Celem.term2str) o 

	  (apfst bool2str)))) bts;

fun ocalhd2str (b, p, hdf, itms, prec, spec) =                              (* for tests only *)

    "(" ^ bool2str b ^ ", " ^ pos_2str p ^ ", " ^ Celem.term2str hdf ^

    ", " ^ Model.itms2str_ (Celem.thy2ctxt' "Isac") itms ^

    ", " ^ preconds2str prec ^ ", \n" ^ Celem.spec2str spec ^ " )";

fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj

  | is_pblnd _ = 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' _ _ = error "";

(**.insert into ctree and cut branches accordingly.**)

(* 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, i) (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: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: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 _ ([],_)"                      (* for test only *)

  | 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 _ _ _ = 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 * 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'

    	| _ => 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 _ _ = 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 * 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: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 _ _ _ _ _ _ = 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 specified for the rootpbl;

   thus use this function _after_ finishing specification *)

fun rootthy (Nd (PblObj {spec = (thyID, _, _), ...}, _)) = Celem.assoc_thy thyID

  | rootthy _ = error "rootthy: uncovered fun def.";

(**)

end;

(**)