(* use"../ME/ctreeNEW.sml";

    use"ME/ctreeNEW.sml";

    use"ctreeNEW.sml";

    *)

 (*.get all positions in a ptree until ([],Res) or ostate=Incomplete

 val get_allp = fn : 

   pos' list -> : accumulated, start with []

   pos ->       : the offset for subtrees wrt the root

   ptree ->     : (sub)tree

   pos'         : initialization (the last pos' before ...)

   -> pos' list : of positions in this (sub) tree (relative to the root)

 .*)

 (*###################################################################*)

 (* val (cuts, P, pt, pos) = ([], [3], get_nd pt [3], ([], Frm):pos');

    val (cuts, P, pt, pos) = ([], [2], get_nd pt [2], ([], Frm):pos');

    length (children pt);

    *)

 fun get_allp (cuts:pos' list) (P:pos, pos: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])): pos' list

      end) handle PTREE _ => (map (apfst (curry op@ P)) cuts);

 (*###################################################################*)

 (*----OLD-----*)

 fun get_allps (cuts: pos' list) (P:pos) [] = cuts

   | get_allps cuts P (pt::pts) =

     let val cuts' = 

 	    get_allp [] (P, ([], Frm)) pt

     in get_allps (cuts @ cuts') (lev_on P) pts end;

 print_depth 11;

 (* val (cuts: pos' list, P, pt::pts) = ([], [1], children pt);

    val cuts' = get_allp [] P pt ([], Frm);

    val (cuts: pos' list, P, pt::pts) = (cuts @ cuts', lev_on P, pts);

    val cuts' = get_allp [] P pt ([], Frm);

    length (children pt);

    *)

 (*the pts are assumed to be on the same level*)

 fun get_allps (cuts: pos' list) (P:pos) [] = 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;

 print_depth 11; move_dn; print_depth 3;

 print_depth 11; get_allpos'; print_depth 3;

 (**.these 2 funs decide on how far cut_tree goes.**)

 (*.shall the nodes _after_ the pos to be inserted at be deleted?.*)

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

   | test_trans (PrfObj{branch = NoBranch,...}) = true

   | test_trans (PblObj{branch = Transitive,...}) = true 

   | test_trans (PblObj{branch = NoBranch,...}) = true 

   | test_trans _ = false;

 (*.shall cutting be continued on the higher level(s)?

    the Nd regarded will NOT be changed.*)

 fun cutlevup (PblObj _) = false (*for tests of LK0502*)

   | cutlevup _ = true;

 (*cut_bottom new S(603)..(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: ptree ->         : the _whole_ ptree for cut_levup

     pos * posel ->   : the pos after split_last

     ptree ->         : the parent of the Nd to be cut

 return

     (ptree *         : the updated ptree

      pos' list) *    : the pos's cut

      bool            : cutting shall be continued on the higher level(s)

 *)

 (**############# 2nd get_allp finished############################**)

 print_depth 99;

 fun cut_bottom _ (pt' as Nd (b, [])) = ((pt', []), cutlevup b)

   | cut_bottom (P:pos, p:posel) (Nd (b, bs)) =

     let (*divide level into 3 parts...*)

 	val keep = take (p - 1, bs)

 	val pt' as Nd (_,bs') = nth p bs

 	(*^^^^^_here_ will be 'insert'ed by 'append_..'*)

 	val (tail, tp) = (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'ed by 'append_..'*)] @ tail,

 		  get_allp  [] (P @ [p], (P, Frm)) pt')

 	val (pt'', cuts) = 

 	    if cutlevup b

 	    then (Nd (del_res b, children), 

 		  cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)]))

 	    else (Nd (b, children), cuts)

 	(*val _= writeln("####cut_bottom (P, p)="^pos2str (P @ [p])^

 		       ", Nd=.............................................")

 	val _= show_pt pt''

 	val _= writeln("####cut_bottom form='"^

 		       term2str (get_obj g_form pt'' []))

 	val _= writeln("####cut_bottom cuts#="^string_of_int (length cuts)^

 		       ", cuts="^pos's2str cuts)*)

     in ((pt'', cuts:pos' list), cutlevup b) end;

 print_depth 3;

 (**######################################################################**);

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

    ptree -> 	     : the whole ptree for 'get_nd pt P' on each level

    ptree -> 	     : the Nd from the lower level for insertion at path

    pos * posel ->    : pos=path split for convenience

    ptree -> 	     : Nd the children of are under consideration on this call 

 returns		     :

    ptree * pos' list : the updated parent-Nd and the pos's of the Nds cut

 .*)

 print_depth 99;

 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, tp) = (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 cutlevup 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')

 	(*val _= writeln("#####cut_levup clevup= "^bool2str clevup)

 	val _= writeln("#####cut_levup cutlevup b= "^bool2str (cutlevup b))

 	val _= writeln("#####cut_levup (P, p)="^pos2str (P @ [p])^

 		       ", Nd=.............................................")

 	val _= show_pt pt''

 	val _= writeln("#####cut_levup form='"^

 		       term2str (get_obj g_form pt'' []))

 	val _= writeln("#####cut_levup cuts#="^string_of_int (length cuts)^

 		       ", cuts="^pos's2str cuts)*)

     in if null P then (pt'', (cuts @ cuts'):pos' list)

        else let val (P, p) = split_last P

 	    in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P)

 	    end

     end;

 print_depth 3;

 (**######################################################################**);

 (* use"../ME/ctreeNEW.sml";

    use"ME/ctreeNEW.sml";

    use"ctreeNEW.sml";

    *)

 print_depth 99;

 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;

 print_depth 3;

 (*######## eval from here ##########################################**)

 (*######## eval from here ##########################################**)

 (*######## eval from here ##########################################**)

 fun append_atomic p l f r f' s pt = 

     let (*val _= writeln("##append_atomic: pos ="^pos2str p^

 	       ", Nd=.............................................")

 	val _= show_pt pt*)

 	val (iss, f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac

 		       then (*after Take*)

 			   ((fst (get_obj g_loc pt p), Some l), 

 			    get_obj g_form pt p) 

 		       (*040223	     else ((Some l, None), f)*)

 		       else ((None, Some l), f)

     in insert (PrfObj {cell = [(*3.00. unused*)],

 		       form  = f,

 		       tac  = r,

 		       loc   = iss,

 		       branch= NoBranch,

 		       result= f',

 		       ostate= s}) pt p end;

 (*20.8.02: cappend_* FIXXXXME cut branches below cannot be decided here:

   detail - generate - cappend: inserted, not appended !!!

   cut decided in applicable_in !?!

 *)

 fun cappend_atomic pt p loc f r f' s = 

     let val _= writeln("#cappend_atomic: pos ="^pos2str p)

 	val (pt',c) = cut_tree pt (p,Frm)

 	val _= writeln("#cappend_atomic: after cut")

 	val pt'' = append_atomic p loc f r f' s pt'

     in (pt'',c) end;

 fun cappend_atomic pt p loc f r f' s = 

 (* val (pt, p, loc, f, r, f', s) = 

        (pt,p,l,f,Rewrite_Set_Inst (subst2subs subs',id_rls rls'),

 	(f',asm),Complete);

    *)

 ((*writeln("###cappend_atomic: pos ="^pos2str p);*)

   apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm))

 );

 (* called by Take *)

 fun append_form p l f pt = 

 ((*writeln("###append_form: pos ="^pos2str p);*)

   insert (PrfObj {cell = [(*3.00. unused*)],

 		  form  = (*if existpt p pt 

 		  andalso get_obj g_tac pt p = Empty_Tac 

 			    (*distinction from 'old' (+complete!) pobjs*)

 			    then get_obj g_form pt p else*) f,

 		  tac  = Empty_Tac,

 		  loc   = (Some l, None),

 		  branch= NoBranch,

 		  result= (e_term,[]),

 		  ostate= Incomplete}) pt p

 );

 (* val (p,loc,f) = ([1], e_istate, str2term "x + 1 = 2");

    val (p,loc,f) = (fst p, e_istate, str2term "-1 + x = 0");

    *)

 fun cappend_form pt p loc f =

 ((*writeln("###cappend_form: pos ="^pos2str p);*)

   apfst (append_form p loc f) (cut_tree pt (p,Frm))

 );

 fun append_result pt p l f s =

 ((*writeln("###append_result: pos ="^pos2str p);*)

     (appl_obj (repl_result (fst (get_obj g_loc pt p),

 			    Some l) f s) pt p, [])

 );

 (*WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml*)

 fun append_parent p l f r b pt = 

   let (*val _= writeln("###append_parent: pos ="^pos2str p);*)

     val (ll,f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac

 		  then ((fst (get_obj g_loc pt p), Some l), 

 			get_obj g_form pt p) 

 		 else ((Some l, None), f)

   in insert (PrfObj 

 	  {cell = [(*unused*)],

 	   form  = f,

 	   tac  = r,

 	   loc   = ll,

 	   branch= b,

 	   result= (e_term,[]),

 	   ostate= Incomplete}) pt p end;

 fun cappend_parent pt p loc f r b =

 ((*writeln("###cappend_parent: pos ="^pos2str p);*)

   apfst (append_parent p loc f r b) (cut_tree pt (p,Und))

 );

 fun append_problem [] l fmz (strs,spec,hdf) _ =

 ((*writeln("###append_problem: pos = []");*)

   (Nd (PblObj 

 	       {cell  = [(*3.00. unused*)],

 		origin= (strs,spec,hdf),

 		fmz   = fmz,

 		spec  = empty_spec,

 		probl = []:itm list,

 		meth  = []:itm list,

 		env   = None,

 		loc   = (Some l, None),

 		branch= TransitiveB,(*FIXXXXXME.27.8.03: for equations only*)

 		result= (e_term,[]),

 		ostate= Incomplete},[]))

 )

   | append_problem p l fmz (strs,spec,hdf) pt =

 ((*writeln("###append_problem: pos ="^pos2str p);*)

   insert (PblObj 

 	  {cell  = [(*3.00. unused*)],

 	   origin= (strs,spec,hdf),

 	   fmz   = fmz,

 	   spec  = empty_spec,

 	   probl = []:itm list,

 	   meth  = []:itm list,

 	   env   = None,

 	   loc   = (Some l, None),

 	   branch= TransitiveB,

 	   result= (e_term,[]),

 	   ostate= Incomplete}) pt p

 );

 fun cappend_problem _ [] loc fmz ori =

 ((*writeln("###cappend_problem: pos = []");*)

   (append_problem [] loc fmz ori EmptyPtree,[])

 )

   | cappend_problem pt p loc fmz ori = 

 ((*writeln("###cappend_problem: pos ="^pos2str p);*)

   apfst (append_problem p (loc:istate) fmz ori) (cut_tree pt (p,Frm))

 );

 (* use"ME/ctreeNEW.sml";

    use"ctreeNEW.sml";

    *)