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

    use"ME/ctree.sml";

    use"ctree.sml";

    W.N.26.10.99

 writeln (pr_ptree pr_short pt); 

 val Nd ( _, ns) = pt;

 *)

 (*structure Ptree (**): PTREE (**) = ###### outcommented ######*)

 signature PTREE =

 sig

   type ptree

   type envp

   val e_ptree : ptree

   exception PTREE of string

   type branch

   type ostate

   type cellID

   type cid

   type posel

   type pos

   type pos'

   type loc

   type domID

   type pblID

   type metID

   type spec

   type 'a ppc

   type con

   type subs

   type subst

   type env

   type ets

   val ets2str : ets -> string

   type item

   type tac

   type tac_

   val tac_2str : tac_ -> string

   type safe

   val safe2str : safe -> string

   type meth

   val cappend_atomic : ptree -> pos -> loc -> cterm' -> tac

     -> cterm' -> ostate -> cid -> ptree * posel list * cid

   val cappend_form : ptree

     -> pos -> loc -> cterm' -> cid -> ptree * pos * cid

   val cappend_parent : ptree -> pos -> loc -> cterm' -> tac

     -> branch -> cid -> ptree * int list * cid

   val cappend_problem : ptree -> posel list(*FIXME*) -> loc

     -> cterm' list * spec -> cid -> ptree * int list * cellID list

   val append_result : ptree -> pos -> cterm' -> ostate -> ptree * pos

   type ppobj

   val g_branch : ppobj -> branch

   val g_cell : ppobj -> cid

   val g_args : ppobj -> (int * (term list)) list (*args of scr*)

   val g_form : ppobj -> cterm'

   val g_loc : ppobj -> loc

   val g_met : ppobj -> meth

   val g_domID : ppobj -> domID

   val g_metID : ppobj -> metID

   val g_model : ppobj -> cterm' ppc

   val g_tac : ppobj -> tac

   val g_origin : ppobj -> cterm' list * spec

   val g_ostate : ppobj -> ostate

   val g_pbl : ppobj -> pblID * item ppc

   val g_result : ppobj -> cterm'

   val g_spec : ppobj -> spec

 (*  val get_all : (ppobj -> 'a) -> ptree -> 'a list

   val get_alls : (ppobj -> 'a) -> ptree list -> 'a list *)

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

   val gpt_cell : ptree -> cid

   val par_pblobj : ptree -> pos -> pos

   val pre_pos : pos -> pos

   val lev_dn : int list -> int list

   val lev_on : pos -> posel list

   val lev_pred : pos -> pos

   val lev_up : pos -> pos

 (*  val pr_cell : pos -> ppobj -> string

   val pr_pos : int list -> string        *)

   val pr_ptree : (pos -> ppobj -> string) -> ptree -> string

   val pr_short : pos -> ppobj -> string

 (*  val repl : 'a list -> int -> 'a -> 'a list

   val repl_app : 'a list -> int -> 'a -> 'a list

   val repl_branch : branch -> ppobj -> ppobj

   val repl_domID : domID -> ppobj -> ppobj

   val repl_form : cterm' -> ppobj -> ppobj

   val repl_met : item ppc -> ppobj -> ppobj

   val repl_metID : metID -> ppobj -> ppobj

   val repl_model : cterm' list -> ppobj -> ppobj

   val repl_tac : tac -> ppobj -> ppobj

   val repl_pbl : item ppc -> ppobj -> ppobj

   val repl_pblID : pblID -> ppobj -> ppobj

   val repl_result : cterm' -> ostate -> ppobj -> ppobj

   val repl_spec : spec -> ppobj -> ppobj

   val repl_subs : (string * string) list -> ppobj -> ppobj     *)

   val rootthy : ptree -> domID

 (*  val test_trans : ppobj -> bool

   val uni__asm : (string * pos) list -> ppobj -> ppobj

   val uni__cid : cellID list -> ppobj -> ppobj                 *)

   val union_asm : ptree -> pos -> (string * pos) list -> ptree

   val union_cid : ptree -> pos -> cellID list -> ptree

   val update_branch : ptree -> pos -> branch -> ptree

   val update_domID : ptree -> pos -> domID -> ptree

   val update_met : ptree -> pos -> meth -> ptree

   val update_metppc : ptree -> pos -> item ppc -> ptree

   val update_metID : ptree -> pos -> metID -> ptree

   val update_tac : ptree -> pos -> tac -> ptree

   val update_pbl : ptree -> pos -> pblID * item ppc -> ptree

   val update_pblppc : ptree -> pos -> item ppc -> ptree

   val update_pblID : ptree -> pos -> pblID -> ptree

   val update_spec : ptree -> pos -> spec -> ptree

   val update_subs : ptree -> pos -> (string * string) list -> ptree

   val rep_pblobj : ppobj

     -> {branch:branch, cell:cid, env:envp, loc:loc, meth:meth, model:cterm' ppc,

         origin:cterm' list * spec, ostate:ostate, probl:pblID * item ppc,

         result:cterm', spec:spec}

   val rep_prfobj : ppobj

     -> {branch:branch, cell:cid, form:cterm', loc:loc, tac:tac,

         ostate:ostate, result:cterm'}

 end 

 (* -------------- 

 structure Ptree (**): PTREE (**) =

 struct

  -------------- *)

 type env = (term * term) list;

 datatype branch = 

 	 NoBranch | AndB | OrB 

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

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

        | SequenceB | IntersectB | CollectB | MapB;

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

 fun ostate2str Incomplete = "Incomplete"

   | ostate2str Complete = "Complete"

   | ostate2str Inconsistent = "Inconsistent";

 type cellID = int;     

 type cid = cellID list;

 type posel = int;     (* roundabout for (some of) nice signatures *)

 type pos = posel 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";

 type pos' = pos * pos_;

 (*WN.12.03 remembering interator (pos * pos_) for ptree 

 	   pos : lev_on, lev_dn, lev_up, 

                  lev_onFrm, lev_dnRes (..see solve Apply_Method !) 

            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;

 val e_pos' = ([],Und):pos';

 fun res2str (t, ts) = pair2str (term2str t, terms2str ts);

 fun asm2str (t, p:pos) = pair2str (term2str t, ints2str' p);

 fun asms2str asms = (strs2str' o (map asm2str)) asms;

 (*26.4.02: never used after introduction of scripts !!!

 type loc =  loc_ *        (* + interpreter-state          *)

 	    (loc_ * rls') (* -"- for script of the ruleset*)

 		option;

 val e_loc = ([],NONE):loc;

 val ee_loc = (e_loc,e_loc);*)

 datatype safe = Sundef | Safe | Unsafe | Helpless;

 fun safe2str Sundef   = "Sundef"

   | safe2str Safe     = "Safe"

   | safe2str Unsafe   = "Unsafe" 

   | safe2str Helpless = "Helpless";

 type subs = cterm' list; (*16.11.00 for FE-KE*)

 val e_subs = ["(bdv, x)"];

 (*._sub_stitution as strings of _e_qualities.*)

 type sube = cterm' list;

 val e_sube = []:cterm' list;

 fun sube2str s = strs2str s;

 (*._sub_stitution as _t_erms of _e_qualities.*)

 type subte = term list;

 val e_subte = []:term list;

 fun subte2str ss = terms2str ss;

 fun subte2sube ss = map term2str ss;

 fun subst2subs s = map (pair2str o 

 			(apfst (Syntax.string_of_term (thy2ctxt' "Isac"))) o

 			(apsnd (Syntax.string_of_term (thy2ctxt' "Isac")))) s;

 fun subst2subs' s = map ((apfst (Syntax.string_of_term (thy2ctxt' "Isac"))) o

 			 (apsnd (Syntax.string_of_term (thy2ctxt' "Isac")))) s;

 fun subs2subst thy s = map (isapair2pair o term_of o the o (parse thy)) s;

 (*> subs2subst thy ["(bdv,x)","(err,#0)"];

 val it =

   [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real")),

    (Free ("err","RealDef.real"),Free ("#0","RealDef.real"))] 

    : (term * term) list*)

 (*["bdv=x","err=0"] ---> [(bdv,x), (err,0)]*)

 fun sube2subst thy s = map (dest_equals' o term_of o the o (parse thy)) s;

 (* val ts = sube2subst thy ["bdv=x","err=0"];

    subst2str' ts;

    *)

 fun sube2subte ss = map str2term ss;

 fun isasub2subst isasub = ((map isapair2pair) o isalist2list) isasub;

 type scrstate =       (*state for script interpreter*)

 	 env(*stack*) (*used to instantiate tac for checking assod

 		       12.03.noticed: e_ not updated during execution ?!?*)

 	 * loc_       (*location of tac in script*)

 	 * term option(*argument of curried functions*)

 	 * term       (*value obtained by tac executed

 		       updated also after a derivation by 'new_val'*)

 	 * safe       (*estimation of how result will be obtained*)

 	 * bool;      (*true = strongly .., false = weakly associated: 

 					    only used during ass_dn/up*)

 val e_scrstate = ([],[],NONE,e_term,Sundef,false):scrstate;

 (*21.8.02 ---> definitions.sml for datatype scr 

 type rrlsstate =      (*state for reverse rewriting*)

      (term *          (*the current formula*)

       rule list      (*of reverse rewrite set (#1#)*)

 	    list *    (*may be serveral, eg. in norm_rational*)

       (rule *         (*Thm (+ Thm generated from Calc) resulting in ...*)

        (term *        (*... rewrite with ...*)

 	term list))   (*... assumptions*)

 	  list);      (*derivation from given term to normalform

 		       in reverse order with sym_thm; 

                        (#1#) could be extracted from here #1*) --------*)

 datatype istate =     (*interpreter state*)

 	 Uistate                 (*undefined in modspec, in '_deriv'ation*)

        | ScrState of scrstate    (*for script interpreter*)

        | RrlsState of rrlsstate; (*for reverse rewriting*)

 val e_istate = (ScrState ([],[],NONE,e_term,Sundef,false)):istate;

 type iist = istate option * istate option;

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

 fun rta2str (r,(t,a)) = "\n("^(rule2str r)^",("^(term2str t)^", "^

 		      (terms2str a)^"))";

 fun istate2str Uistate = "Uistate"

   | istate2str (ScrState (e,l,to,t,s,b):istate) =

     "ScrState ("^ subst2str e ^",\n "^ 

     loc_2str l ^", "^ termopt2str to ^",\n "^

     term2str t ^", "^ safe2str s ^", "^ bool2str b ^")"

   | istate2str (RrlsState (t,t1,rss,rtas)) = 

     "RrlsState ("^(term2str t)^", "^(term2str t1)^", "^

     ((strs2str o (map (strs2str o (map rule2str)))) rss)^", "^

     ((strs2str o (map rta2str)) rtas)^")";

 fun istates2str (NONE, NONE) = "(#NONE, #NONE)"

   | istates2str (NONE, SOME ist) = "(#NONE,\n#SOME "^istate2str ist^")"

   | istates2str (SOME ist, NONE) = "(#SOME "^istate2str ist^",\n #NONE)"

   | istates2str (SOME i1, SOME i2) = "(#SOME "^istate2str i1^",\n #SOME "^

 				     istate2str i2^")";

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

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

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

 datatype con = land | lor;

 type spec = 

      domID * (*WN.12.03: is replaced by thy from get_met ?FIXME? in:

 	      specify (Init_Proof..), nxt_specify_init_calc,

 	      assod (.SubProblem...), stac2tac (.SubProblem...)*)

      pblID * 

      metID;

 fun spec2str ((dom,pbl,met)(*:spec*)) = 

   "(" ^ (quote dom) ^ ", " ^ (strs2str pbl) ^ 

   ", " ^ (strs2str met) ^ ")";

 (*> spec2str empty_spec;

 val it = "(\"\", [], (\"\", \"\"))" : string *)

 val empty_spec = (e_domID,e_pblID,e_metID):spec;

 val e_spec = empty_spec;

 (*.tactics propagate the construction of the calc-tree;

    there are

    (a) 'specsteps' for the specify-phase, and others for the solve-phase

    (b) those of the solve-phase are 'initac's and others;

        initacs start with a formula different from the preceding formula.

    see 'type tac_' for the internal representation of tactics.*)

 datatype tac = 

   Init_Proof of ((cterm' list) * spec)

 (*'specsteps'...*)

 | Model_Problem

 | Refine_Problem of pblID              | Refine_Tacitly of pblID

 | Add_Given of cterm'                  | Del_Given of cterm'

 | Add_Find of cterm'                   | Del_Find of cterm'

 | Add_Relation of cterm'               | Del_Relation of cterm'

 | Specify_Theory of domID              | Specify_Problem of pblID

 | Specify_Method of metID

 (*...'specsteps'*)

 | Apply_Method of metID 

 (*.creates an 'istate' in PblObj.env; in case of 'init_form' 

    creates a formula at ((lev_on o lev_dn) p, Frm) and in this ppobj.'loc' 

    'SOME istate' (at fst of 'loc').

    As each step (in the solve-phase) has a resulting formula (at the front-end)

    Apply_Method also does the 1st step in the script (an 'initac') if there

    is no 'init_form' .*)

 | Check_Postcond of pblID

 | Free_Solve

 | Rewrite_Inst of ( subs * thm')       | Rewrite of thm'

                                        | Rewrite_Asm of thm'

 | Rewrite_Set_Inst of ( subs * rls')   | Rewrite_Set of rls'        

 | Detail_Set_Inst of ( subs * rls')    | Detail_Set of rls'

 | End_Detail  (*end of script from next_tac, 

                 in solve: switches back to parent script WN0509 drop!*)

 | Derive of rls' (*an input formula using rls WN0509 drop!*)

 | Calculate of string (* plus | minus | times | cancel | pow | sqrt *)

 | End_Ruleset

 | Substitute of sube                   | Apply_Assumption of cterm' list

 | Take of cterm'      (*an 'initac'*)

 | Take_Inst of cterm'  

 | Group of (con * int list ) 

 | Subproblem of (domID * pblID) (*an 'initac'*)

 | CAScmd of cterm'  (*6.6.02 URD: Function formula; WN0509 drop!*)

 | End_Subproblem    (*WN0509 drop!*)

 | Split_And                            | Conclude_And

 | Split_Or                             | Conclude_Or

 | Begin_Trans                          | End_Trans

 | Begin_Sequ                           | End_Sequ(* substitute root.env *)

 | Split_Intersect                      | End_Intersect

 | Check_elementwise of cterm'          | Collect_Trues

 | Or_to_List

 | Empty_Tac (*TODO.11.6.03 ... of string: could carry msg of (Notappl msg)

 	       in 'helpless'*)

 | Tac of string(* eg.'repeat'*WN0509 drop!*)

 | User                                 (*internal, for ets*WN0509 drop!*)

 | End_Proof';(* inout*)

 (* tac2str /--> library.sml: needed in dialog.sml for 'separable *)

 fun tac2str (ma:tac) = case ma of

     Init_Proof (ppc, spec)  => 

       "Init_Proof "^(pair2str (strs2str ppc, spec2str spec))

   | Model_Problem           => "Model_Problem "

   | Refine_Tacitly pblID    => "Refine_Tacitly "^(strs2str pblID)

   | Refine_Problem pblID    => "Refine_Problem "^(strs2str pblID)

   | Add_Given cterm'        => "Add_Given "^cterm'

   | Del_Given cterm'        => "Del_Given "^cterm'

   | Add_Find cterm'         => "Add_Find "^cterm'

   | Del_Find cterm'         => "Del_Find "^cterm'

   | Add_Relation cterm'     => "Add_Relation "^cterm'

   | Del_Relation cterm'     => "Del_Relation "^cterm'

   | Specify_Theory domID    => "Specify_Theory "^(quote domID    )

   | Specify_Problem pblID   => "Specify_Problem "^(strs2str pblID )

   | Specify_Method metID    => "Specify_Method "^(strs2str metID)

   | Apply_Method metID      => "Apply_Method "^(strs2str metID)

   | Check_Postcond pblID    => "Check_Postcond "^(strs2str pblID)

   | Free_Solve              => "Free_Solve"

   | Rewrite_Inst (subs,thm')=> 

       "Rewrite_Inst "^(pair2str (subs2str subs, spair2str thm'))

   | Rewrite thm'            => "Rewrite "^(spair2str thm')

   | Rewrite_Asm thm'        => "Rewrite_Asm "^(spair2str thm')

   | Rewrite_Set_Inst (subs, rls) => 

       "Rewrite_Set_Inst "^(pair2str (subs2str subs, quote rls))

   | Rewrite_Set rls         => "Rewrite_Set "^(quote rls    )

   | Detail_Set rls          => "Detail_Set "^(quote rls    )

   | Detail_Set_Inst (subs, rls) => 

       "Detail_Set_Inst "^(pair2str (subs2str subs, quote rls))

   | End_Detail              => "End_Detail"

   | Derive rls'             => "Derive "^rls' 

   | Calculate op_           => "Calculate "^op_ 

   | Substitute sube         => "Substitute "^sube2str sube	     

   | Apply_Assumption ct's   => "Apply_Assumption "^(strs2str ct's)

   | Take cterm'             => "Take "^(quote cterm'	)

   | Take_Inst cterm'        => "Take_Inst "^(quote cterm' )

   | Group (con, ints)       => 

       "Group "^(pair2str (con2str con, ints2str ints))

   | Subproblem (domID, pblID) => 

       "Subproblem "^(pair2str (domID, strs2str pblID))

 (*| Subproblem_Full (spec, cts') => 

       "Subproblem_Full "^(pair2str (spec2str spec, strs2str cts'))*)

   | End_Subproblem          => "End_Subproblem"

   | CAScmd cterm'           => "CAScmd "^(quote cterm')

   | Check_elementwise cterm'=> "Check_elementwise "^(quote cterm') 

   | Or_to_List              => "Or_to_List "

   | Collect_Trues           => "Collect_Trues"

   | Empty_Tac             => "Empty_Tac"

   | Tac string            => "Tac "^string

   | User                    => "User"

   | End_Proof'              => "tac End_Proof'"

   | _                       => "tac2str not impl. for ?!";

 fun is_rewset (Rewrite_Set_Inst _) = true

   | is_rewset (Rewrite_Set _) = true 

   | is_rewset _ = false;

 fun is_rewtac (Rewrite _) = true

   | is_rewtac (Rewrite_Inst _) = true

   | is_rewtac (Rewrite_Asm _) = true

   | is_rewtac tac = is_rewset tac;

 fun tac2IDstr (ma:tac) = case ma of

     Model_Problem           => "Model_Problem"

   | Refine_Tacitly pblID    => "Refine_Tacitly"

   | Refine_Problem pblID    => "Refine_Problem"

   | Add_Given cterm'        => "Add_Given"

   | Del_Given cterm'        => "Del_Given"

   | Add_Find cterm'         => "Add_Find"

   | Del_Find cterm'         => "Del_Find"

   | Add_Relation cterm'     => "Add_Relation"

   | Del_Relation cterm'     => "Del_Relation"

   | Specify_Theory domID    => "Specify_Theory"

   | Specify_Problem pblID   => "Specify_Problem"

   | Specify_Method metID    => "Specify_Method"

   | Apply_Method metID      => "Apply_Method"

   | Check_Postcond pblID    => "Check_Postcond"

   | Free_Solve              => "Free_Solve"

   | Rewrite_Inst (subs,thm')=> "Rewrite_Inst"

   | Rewrite thm'            => "Rewrite"

   | Rewrite_Asm thm'        => "Rewrite_Asm"

   | Rewrite_Set_Inst (subs, rls) => "Rewrite_Set_Inst"

   | Rewrite_Set rls         => "Rewrite_Set"

   | Detail_Set rls          => "Detail_Set"

   | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst"

   | Derive rls'             => "Derive "

   | Calculate op_           => "Calculate "

   | Substitute subs         => "Substitute" 

   | Apply_Assumption ct's   => "Apply_Assumption"

   | Take cterm'             => "Take"

   | Take_Inst cterm'        => "Take_Inst"

   | Group (con, ints)       => "Group"

   | Subproblem (domID, pblID) => "Subproblem"

   | End_Subproblem          => "End_Subproblem"

   | CAScmd cterm'           => "CAScmd"

   | Check_elementwise cterm'=> "Check_elementwise"

   | Or_to_List              => "Or_to_List "

   | Collect_Trues           => "Collect_Trues"

   | Empty_Tac             => "Empty_Tac"

   | Tac string            => "Tac "

   | User                    => "User"

   | End_Proof'              => "End_Proof'"

   | _                       => "tac2str not impl. for ?!";

 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls

   | rls_of (Rewrite_Set rls) = rls

   | rls_of tac = raise error ("rls_of: called with tac '"^tac2IDstr tac^"'");

 fun thm_of_rew (Rewrite_Inst (subs,(thmID,_))) = 

     (thmID, SOME ((subs2subst (assoc_thy "Isac.thy") subs):subst))

   | thm_of_rew (Rewrite  (thmID,_)) = (thmID, NONE)

   | thm_of_rew (Rewrite_Asm (thmID,_)) = (thmID, NONE);

 fun rls_of_rewset (Rewrite_Set_Inst (subs,rls)) = 

     (rls, SOME ((subs2subst (assoc_thy "Isac.thy") subs):subst))

   | rls_of_rewset (Rewrite_Set rls) = (rls, NONE)

   | rls_of_rewset (Detail_Set rls) = (rls, NONE)

   | rls_of_rewset (Detail_Set_Inst (subs, rls)) = 

     (rls, SOME ((subs2subst (assoc_thy "Isac.thy") subs):subst));

 fun rule2tac _ (Calc (opID, thm)) = Calculate (calID2calcID opID)

   | rule2tac [] (Thm (thmID, thm)) = Rewrite (thmID, string_of_thmI thm)

   | rule2tac subst (Thm (thmID, thm)) = 

     Rewrite_Inst (subst2subs subst, (thmID, string_of_thmI thm))

   | rule2tac [] (Rls_ rls) = Rewrite_Set (id_rls rls)

   | rule2tac subst (Rls_ rls) = 

     Rewrite_Set_Inst (subst2subs subst, (id_rls rls))

   | rule2tac _ rule = 

     raise error ("rule2tac: called with '" ^ rule2str rule ^ "'");

 type fmz_ = cterm' list;

 (*.a formalization of an example containing data 

    sufficient for mechanically finding the solution for the example.*)

 (*FIXME.WN051014: dont store fmz = (_,spec) in the PblObj, 

   this is done in origin*)

 type fmz = fmz_ * spec;

 val e_fmz = ([],e_spec);

 (*tac_ is made from tac in applicable_in,

   and carries all data necessary for generate;*)

 datatype tac_ = 

 (* datatype tac = *)

   Init_Proof' of ((cterm' list) * spec)

                 (* ori list !: code specify -> applicable*)

 | Model_Problem' of pblID * 

 		    itm list *  (*the 'untouched' pbl*)

 		    itm list    (*the casually completed met*)

 | Refine_Tacitly' of pblID *    (*input*)

 		     pblID *    (*the refined from applicable_in*)

 		     domID *    (*from new pbt?! filled in specify*)

 		     metID *    (*from new pbt?! filled in specify*)

 		     itm list   (*drop ! 9.03: remains [] for

                                   Model_Problem recognizing its activation*)

 | Refine_Problem' of (pblID * (itm list * (bool * Term.term) list))

  (*FIXME?040215 drop: done automatically in init_proof + Subproblem'*)

 | Add_Given'    of cterm' *

 		   itm list (*updated with input in fun specify_additem*)

 | Add_Find'     of cterm' *

 		   itm list (*updated with input in fun specify_additem*)

 | Add_Relation' of cterm' *

 		 itm list (*updated with input in fun specify_additem*)

 | Del_Given' of cterm'   | Del_Find' of cterm'   | Del_Relation' of cterm'

   (*4.00.: all..    term: in applicable_in ..? Syn ?only for FormFK?*)

 | Specify_Theory' of domID              

 | Specify_Problem' of (pblID *        (*               *)

 		       (bool *        (* matches	     *)

 			(itm list *   (* ppc	     *)

 			 (bool * term) list))) (* preconditions *)

 | Specify_Method' of metID *

 		     ori list * (*repl. "#undef"*)

 		     itm list   (*... updated from pbl to met*)

 | Apply_Method' of metID * 

 		   (term option) * (*init_form*)

 		   istate		        

 | Check_Postcond' of 

   pblID * 

   (term *      (*returnvalue of script in solve*)

    cterm' list)(*collect by get_assumptions_ in applicable_in, except if 

                  butlast tac is Check_elementwise: take only these asms*)

 | Free_Solve'

 | Rewrite_Inst' of theory' * rew_ord' * rls

 		   * bool * subst * thm' * term * (term  * term list)

 | Rewrite' of theory' * rew_ord' * rls * bool * thm' * 

 	      term * (term * term list)

 | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm' * 

   term * (term * term list)

 | Rewrite_Set_Inst' of theory' * bool * subst * rls * 

 		       term * (term * term list)

 | Detail_Set_Inst' of theory' * bool * subst * rls * 

 		      term * (term * term list)

 | Rewrite_Set' of theory' * bool * rls * term * (term * term list)

 | Detail_Set' of theory' * bool * rls * term * (term * term list)

 | End_Detail' of (term * (term list)) (*see End_Trans'*)

 | End_Ruleset' of term

 | Derive' of rls

 | Calculate' of theory' * string * term * (term * thm') 

 	      (*WN.29.4.03 asm?: * term list??*)

 | Substitute' of subte  (*the 'substitution': terms of type bool*) 

 		 * term (*to be substituted in*)

 		 * term (*resulting from the substitution*)

 | Apply_Assumption' of term list * term

 | Take' of term                         | Take_Inst' of term  

 | Group' of (con * int list * term)

 | Subproblem' of (spec * 

 		  (ori list) * (*filled in assod Subproblem'*)

 		  term *       (*-"-, headline of calc-head *)

 		  fmz_ * 

 		  term)        (*Subproblem(dom,pbl)*)  

 | CAScmd' of term

 | End_Subproblem' of term (*???*)

 | Split_And' of term                    | Conclude_And' of term

 | Split_Or' of term                     | Conclude_Or' of term

 | Begin_Trans' of term                  | End_Trans' of (term * (term list))

 | Begin_Sequ'                           | End_Sequ'(* substitute root.env*)

 | Split_Intersect' of term              | End_Intersect' of term

 | Check_elementwise' of (*special case:*)

   term *   (*(1)the current formula: [x=1,x=...]*)

   string * (*(2)the pred from Check_elementwise   *)

   (term *  (*(3)composed from (1) and (2): {x. pred}*)

    term list) (*20.5.03 assumptions*)

 | Or_to_List' of term * term            (* (a | b, [a,b]) *)

 | Collect_Trues' of term

 | Empty_Tac_                          | Tac_ of  (*for dummies*)

                                             theory *

                                             string * (*form*)

 					    string * (*in Tac*)

 					    string   (*result of Tac".."*)

 | User' (*internal for ets*)            | End_Proof'';(*End_Proof:inout*)

 fun tac_2str ma = case ma of

     Init_Proof' (ppc, spec)  => 

       "Init_Proof' "^(pair2str (strs2str ppc, spec2str spec))

   | Model_Problem' (pblID,_,_)     => "Model_Problem' "^(strs2str pblID )

   | Refine_Tacitly'(p,prefin,domID,metID,itms)=> 

     "Refine_Tacitly' ("

     ^(strs2str p)^", "^(strs2str prefin)^", "

     ^domID^", "^(strs2str metID)^", pbl-itms)"

   | Refine_Problem' ms       => "Refine_Problem' ("^(*matchs2str ms*)"..."^")"

 (*| Match_Problem' (pI, (ok, (itms, pre))) => 

     "Match_Problem' "^(spair2str (strs2str pI,

 				  spair2str (bool2str ok,

 					     spair2str ("itms2str_ itms", 

 							"items2str pre"))))*)

   | Add_Given' cterm'        => "Add_Given' "(*^cterm'*)

   | Del_Given' cterm'        => "Del_Given' "(*^cterm'*)

   | Add_Find' cterm'         => "Add_Find' "(*^cterm'*)

   | Del_Find' cterm'         => "Del_Find' "(*^cterm'*)

   | Add_Relation' cterm'     => "Add_Relation' "(*^cterm'*)

   | Del_Relation' cterm'     => "Del_Relation' "(*^cterm'*)

   | Specify_Theory' domID    => "Specify_Theory' "^(quote domID    )

   | Specify_Problem' (pI, (ok, (itms, pre))) => 

     "Specify_Problem' "^(spair2str (strs2str pI,

 				  spair2str (bool2str ok,

 					     spair2str ("itms2str_ itms", 

 							"items2str pre"))))

   | Specify_Method' (pI,oris,itms) => 

     "Specify_Method' ("^metID2str pI^", "^oris2str oris^", )"

   | Apply_Method' (metID,_,_)      => "Apply_Method' "^(strs2str metID)

   | Check_Postcond' (pblID,(scval,asm)) => 

       "Check_Postcond' "^(spair2str(strs2str pblID, 

 				    spair2str (term2str scval, strs2str asm)))

   | Free_Solve'              => "Free_Solve'"

   | Rewrite_Inst' (*subs,thm'*) _ => 

       "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)

   | Rewrite' thm'            => "Rewrite' "(*^(spair2str thm')*)

   | Rewrite_Asm' thm'        => "Rewrite_Asm' "(*^(spair2str thm')*)

   | Rewrite_Set_Inst' (*subs,thm'*) _ => 

       "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)

   | Rewrite_Set'(thy',pasm,rls',f,(f',asm))          

     => "Rewrite_Set' ("^thy'^","^(bool2str pasm)^","^(id_rls rls')^","

     ^(Syntax.string_of_term (thy2ctxt' "Isac") f)^",("^(Syntax.string_of_term (thy2ctxt' "Isac") f')

     ^","^((strs2str o (map (Syntax.string_of_term (thy2ctxt' "Isac")))) asm)^"))"

   | End_Detail' _             => "End_Detail' xxx"

   | Detail_Set' _             => "Detail_Set' xxx"

   | Detail_Set_Inst' _        => "Detail_Set_Inst' xxx"

   | Derive' rls              => "Derive' "^id_rls rls

   | Calculate'  _            => "Calculate' "

   | Substitute' subs         => "Substitute' "(*^(subs2str subs)*)    

   | Apply_Assumption' ct's   => "Apply_Assumption' "(*^(strs2str ct's)*)

   | Take' cterm'             => "Take' "(*^(quote cterm'	)*)

   | Take_Inst' cterm'        => "Take_Inst' "(*^(quote cterm' )*)

   | Group' (con, ints, _)     => 

       "Group' "^(pair2str (con2str con, ints2str ints))

   | Subproblem' (spec, oris, _,_,pbl_form) => 

       "Subproblem' "(*^(pair2str (domID, strs2str ,...))*)

   | End_Subproblem'  _       => "End_Subproblem'"

   | CAScmd' cterm'           => "CAScmd' "(*^(quote cterm')*)

   | Empty_Tac_             => "Empty_Tac_"

   | User'                    => "User'"

   | Tac_ (_,form,id,result) => "Tac_ (thy,"^form^","^id^","^result^")"

   | _                       => "tac_2str not impl. for arg";

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

   used for continuing eval script + for generate*)

 type ets =

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

      (tac_ * 	 (* (for generate)  *)

       env *      (* with 'tactic=result' as a rule, tactic ev. _not_ ready:

 		  for handling '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         *)

       safe))

     list;

 val Ets = []:ets;

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

   "\n("^(loc_2str l)^",("^(tac_2str m)^

   ",\n  ens= "^(subst2str eno)^

   ",\n  env= "^(subst2str env)^

   ",\n  iar= "^(Syntax.string_of_term (thy2ctxt' "Isac") iar)^

   ",\n  res= "^(Syntax.string_of_term (thy2ctxt' "Isac") res)^

   ",\n  "^(safe2str s)^"))";

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

 type envp =(*9.5.03: unused, delete with field in ptree.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*)

 val empty_envp = ([],[],[],[]):envp; 

 datatype ppobj = 

     PrfObj of {cell  : lrd option, (*where in form tac has been applied*)

 	       (*^^^FIXME.WN0607 rename this field*)

 	       form  : term,    

 	       tac   : tac,         (* also in istate*)

 	       loc   : istate option * istate option, (*for form, result 

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

 	       branch: branch,

 	       result: term * term list,    

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

   | PblObj of {cell  : lrd option,(*unused: meaningful only for some _Prf_Obj*)

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

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

                                   for efficiently adding items in probl, meth*)

 		       spec *     (*updated by Refine_Tacitly*)

 		       term,      (*headline of calc-head, as calculated 

 							      initially(!)*)

 		       (*# the origin of a root-pbl is created from fmz

                            (thus providing help for input to the user),

 			 # the origin of a sub-pbl is created from the argument

 			   -list of a script-tac 'SubProblem (spec) [arg-list]'

 			   by 'match_ags'*)

 	       spec  : spec,      (*explicitly input*)

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

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

 				   TODO: input like to 'probl'*)

 	       env   : istate option,(*for problem with initac in script*)

 	       loc   : istate option * istate option, (*for pbl+met * result*)

 	       branch: branch,

 	       result: term * term list,

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

 (*.this tree contains isac's calculations; TODO.WN03 rename to ctree;

    the 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 ptree = 

     EmptyPtree

   | Nd of ppobj * (ptree list);

 val e_ptree = EmptyPtree;

 fun rep_prfobj (PrfObj {cell,form,tac,loc,branch,result,ostate}) =

   {cell=cell,form=form,tac=tac,loc=loc,branch=branch,result=result,ostate=ostate};

 fun rep_pblobj (PblObj {cell,origin,fmz,spec,probl,meth,env,

 			loc,branch,result,ostate}) =

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

    env=env,loc=loc,branch=branch,result=result,ostate=ostate};

 fun is_prfobj (PrfObj _) = true

   | is_prfobj _ =false;

 (*val is_prfobj' = get_obj is_prfobj; *)

 fun is_pblobj (PblObj _) = true

   | is_pblobj _ = false;

 (*val is_pblobj' = get_obj is_pblobj; 'Error: unbound constructor get_obj'*)

 exception PTREE of string;

 fun nth _ []      = raise PTREE "nth _ []"

   | nth 1 (x::xs) = x

   | nth n (x::xs) = nth (n-1) xs;

 (*> nth 2 [11,22,33]; -->> val it = 22 : int*)

 fun lev_up ([]:pos) = raise PTREE "lev_up []"

   | lev_up p = (drop_last p):pos;

 fun lev_on ([]:pos) = raise PTREE "lev_on []"

   | lev_on pos = 

     let val len = length pos

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

 fun lev_onFrm ((p,_):pos') = (lev_on p,Frm):pos'

   | lev_onFrm p = raise PTREE ("*** lev_onFrm: pos'="^(pos'2str p));

 (*040216: for inform --> embed_deriv: remains on same level*)

 fun lev_back (([],_):pos') = raise PTREE "lev_on_back: called by ([],_)"

   | lev_back (p,_) =

     if last_elem p <= 1 then (p, Frm):pos' 

     else ((drop_last p) @ [(nth (length p) p) - 1], Res);

 (*.increase pos by n within a level.*)

 fun pos_plus 0 pos = pos

   | pos_plus n ((p,Frm):pos') = pos_plus (n-1) (p, Res)

   | pos_plus n ((p,  _):pos') = pos_plus (n-1) (lev_on p, Res);

 fun lev_pred ([]:pos) = raise PTREE "lev_pred []"

   | lev_pred (pos:pos) = 

     let val len = length pos

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

 (*lev_pred [1,2,3];

 val it = [1,2,2] : pos

 > lev_pred [1];

 val it = [0] : pos          *)

 fun lev_dn p = p @ [0];

 (*> (lev_dn o lev_on) [1,2,3];

 val it = [1,2,4,0] : pos    *)

 (*fun lev_dn' ((p,p_):pos') = (lev_dn p, Frm):pos'; WN.3.12.03: never used*)

 fun lev_dnRes ((p,_):pos') = (lev_dn p, Res):pos';

 (*4.4.00*)

 fun lev_up_ ((p,Res):pos') = (lev_up p,Res):pos'

   | lev_up_ p' = raise error ("lev_up_: called for "^(pos'2str p'));

 fun lev_dn_ ((p,_):pos') = (lev_dn p,Res):pos'

 fun ind ((p,_):pos') = length p; (*WN050108 deprecated in favour of lev_of*)

 fun lev_of ((p,_):pos') = length p;

 (** convert ptree 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:pos) (PblObj {origin = (ori,_,_),...}) = 

   ((pr_pos p) ^ " ----- pblobj -----\n")

 (*   ((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^

     (((Syntax.string_of_term (thy2ctxt' "Isac")) o hd(*!?!*) o #5 o hd) ori))^

    "\n") *)

   | pr_short p (PrfObj {form = form,...}) =

   ((pr_pos p) ^ (term2str form) ^ "\n");

 (*

 fun pr_cell (p:pos) (PblObj {cell = c, origin = (ori,_,_),...}) = 

   ((ints2str c) ^"   "^ 

    ((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^

     (((Syntax.string_of_term (thy2ctxt' "Isac")) o hd(*!?!*) o #5 o hd) ori))^

    "\n")

   | pr_cell p (PrfObj {cell = c, form = form,...}) =

   ((ints2str c) ^"   "^ (term2str form) ^ "\n");

 *)

 (* convert ptree *)

 fun pr_ptree f pt =

   let

     fun pr_pt pfn _  EmptyPtree = ""

       | pr_pt pfn ps (Nd (b, [])) = pfn ps b

       | pr_pt pfn ps (Nd (b, ts)) = (pfn ps b)^

       (prts pfn (ps:pos) 1 ts)

     and prts pfn ps p [] = ""

       | prts pfn ps p (t::ts) = (pr_pt pfn (ps @ [p]) t)^

       (prts pfn ps (p+1) ts)

   in pr_pt f [] pt end;

 (*

 > fun prfn ps b = (pr_pos ps)^"   "^b(*TODO*)^"\n";

 > val pt = ref EmptyPtree;

 > pt:=Nd("root",

        [Nd("xx1",[]),

 	Nd("xx2",

 	   [Nd("xx2.1.",[]),

 	    Nd("xx2.2.",[])]),

 	Nd("xx3",[])]);

 > writeln (pr_ptree prfn (!pt));

 *)

 (** access the branches of ptree **)

 fun ins_nth 1 e l  = e::l

   | ins_nth n e [] = raise PTREE "ins_nth n e []"

   | ins_nth n e (l::ls) = l::(ins_nth (n-1) e ls);

 fun repl []      _ _ = raise PTREE "repl [] _ _"

   | repl (l::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;

 (*  

 > repl [1,2,3] 2 22222;

 val it = [1,22222,3] : int list

 > repl_app [1,2,3,4] 5 5555;

 val it = [1,2,3,4,5555] : int list

 > repl_app [1,2,3] 2 22222;

 val it = [1,22222,3] : int list

 > repl_app [1] 2 22222 ;

 val it = [1,22222] : int list

 *)

 (*.get from obj at pos by f : ppobj -> 'a.*)

 fun get_obj f EmptyPtree  (_:pos)  = raise PTREE "get_obj f EmptyPtree"

   | get_obj f (Nd (b,  _)) []      = f b

   | get_obj f (Nd (b, bs)) (p::ps) =

 (* val (f, Nd (b, bs), (p::ps)) = (I, pt, p);

    *)

   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:pos)) 

       (*before WN050419: 'wrong type..' raised also if pos doesn't exist*)

     handle _ => raise PTREE (*"get_obj: at pos = "^

 			     (ints2str' (p::ps))^" wrong type of ppobj"*)

 			  ("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:pos)) = (get_nd (nth p nds) ps)

     handle _ => raise PTREE ("get_nd: not existent pos = "^(ints2str' pos));

 (* for use by get_obj *)

 fun g_cell   (PblObj {cell = c,...}) = NONE

   | g_cell   (PrfObj {cell = c,...}) = c;(*WN0607 hack for quick introduction of lrd + rewrite-at (thms, calcs)*)

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

   | 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_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 = (d,p,m),...}) = 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;

 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;

 fun gpt_cell (Nd (PblObj {cell = c,...},_)) = NONE

   | gpt_cell (Nd (PrfObj {cell = c,...},_)) = c;

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

 val e_origin = ([],e_spec,e_term): (ori list) * spec * term;

 fun just_created (pt,(p,_):pos') =

     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_):pos') 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):pos') = true

   | is_interpos _ = false;

 fun last_onlev pt pos = not (existpt (lev_on pos) pt);

 (*.find the position of the next parent which is a PblObj in ptree.*)

 fun par_pblobj pt ([]:pos) = ([]:pos)

   | par_pblobj pt p =

     let fun par pt [] = []

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

 (* lev_up for hard_gen operating with pos = [...,0] *)

 (*.find the position and the children of the next parent which is a PblObj.*)

 fun par_children (Nd (PblObj _, children)) ([]:pos) = (children, []:pos)

   | par_children (pt as Nd (PblObj _, children)) p =

     let fun par [] = (children, [])

 	  | par p = let val Nd (obj, children) = get_nd pt p

 		    in if is_pblobj obj then (children, p) else par (lev_up p)

 		    end;

     in par (lev_up p) end; 

 (*.get the children of a node in ptree.*)

 fun children (Nd (PblObj _, cn)) = cn

   | children (Nd (PrfObj _, cn)) = cn;

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

   or a PrfObj with tac = Detail_Set (return false).*)

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

 fun par_pbl_det pt ([]:pos) = (true, []:pos, Erls)

   | par_pbl_det pt p =

     let fun par pt [] = (true, [], Erls)

 	  | par pt p = if is_pblobj (get_obj I pt p) then (true, p, Erls)

 		       else case get_obj g_tac pt p of

 				(*Detail_Set rls' => (false, p, assoc_rls rls')

 			      (*^^^--- before 040206 after ---vvv*)

 			      |*)Rewrite_Set rls' => (false, p, assoc_rls rls')

 			      | Rewrite_Set_Inst (_, rls') => 

 				(false, p, assoc_rls rls')

 			      | _ => par pt (lev_up p)

     in par pt (lev_up p) end; 

 (*.get from the whole ptree by f : ppobj -> 'a.*)

 fun get_all f EmptyPtree   = []

   | get_all f (Nd (b, [])) = [f b]

   | get_all f (Nd (b, bs)) = [f b] @ (get_alls f bs)

 and get_alls f [] = []

   | get_alls f pts = flat (map (get_all f) pts);

 (*.insert obj b into ptree at pos, ev.overwriting this pos.*)

 fun insert b EmptyPtree   ([]:pos)  = Nd (b, [])

   | insert b EmptyPtree    _        = raise PTREE "insert b Empty _"

   | insert b (Nd ( _,  _)) []       = raise PTREE "insert b _ []"

   | insert b (Nd (b', bs)) (p::[])  = 

      Nd (b', repl_app bs p (Nd (b,[]))) 

   | insert b (Nd (b', bs)) (p::ps)  =

      Nd (b', repl_app bs p (insert b (nth p bs) ps));

 (*

 > type ppobj = string;

 > writeln (pr_ptree prfn (!pt));

   val pt = ref Empty;

   pt:= insert ("root":ppobj) EmptyPtree [];

   pt:= insert ("xx1":ppobj) (!pt) [1];

   pt:= insert ("xx2":ppobj) (!pt) [2];

   pt:= insert ("xx3":ppobj) (!pt) [3];

   pt:= insert ("xx2.1":ppobj) (!pt) [2,1];

   pt:= insert ("xx2.2":ppobj) (!pt) [2,2];

   pt:= insert ("xx2.1.1":ppobj) (!pt) [2,1,1];

   pt:= insert ("xx2.1.2":ppobj) (!pt) [2,1,2];

   pt:= insert ("xx2.1.3":ppobj) (!pt) [2,1,3];

 *)

 (*.insert children to a node without children.*)

 (*compare: fun insert*)

 fun ins_chn _  EmptyPtree   (_:pos) = raise PTREE "ins_chn: EmptyPtree"

   | ins_chn ns (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 Nd (b', bs') = nth p bs

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

 (* print_depth 11;ins_chn;print_depth 3; ###insert#########################*);

 (** apply f to obj at pos, f: ppobj -> ppobj **)

 fun appl_to_node f (Nd (b,bs)) = Nd (f b, bs);

 fun appl_obj f EmptyPtree    []      = EmptyPtree

   | appl_obj f 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)));

 (* for use by appl_obj *) 

 fun repl_form f (PrfObj {cell=c,form= _,tac=tac,loc=loc,

 			 branch=branch,result=result,ostate=ostate}) =

     PrfObj {cell=c,form= f,tac=tac,loc=loc,

 	    branch=branch,result=result,ostate=ostate}

   | repl_form _ _ = raise PTREE "repl_form takes no PblObj";

 fun repl_pbl x    (PblObj {cell=cell,origin=origin,fmz=fmz,

 			   spec=spec,probl=_,meth=meth,env=env,loc=loc,

 			   branch=branch,result=result,ostate=ostate}) =

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

 	  meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}

   | repl_pbl _ _ = raise PTREE "repl_pbl takes no PrfObj";

 fun repl_met x    (PblObj {cell=cell,origin=origin,fmz=fmz,

 			   spec=spec,probl=probl,meth=_,env=env,loc=loc,

 			   branch=branch,result=result,ostate=ostate}) =

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

 	  meth= x,env=env,loc=loc,branch=branch,result=result,ostate=ostate}

   | repl_met _ _ = raise PTREE "repl_pbl takes no PrfObj";

 fun repl_spec  x    (PblObj {cell=cell,origin=origin,fmz=fmz,

 			   spec= _,probl=probl,meth=meth,env=env,loc=loc,

 			   branch=branch,result=result,ostate=ostate}) =

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

 	  meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}

   | repl_spec  _ _ = raise PTREE "repl_domID takes no PrfObj";

 fun repl_domID x    (PblObj {cell=cell,origin=origin,fmz=fmz,

 			   spec=(_,p,m),probl=probl,meth=meth,env=env,loc=loc,

 			   branch=branch,result=result,ostate=ostate}) =

   PblObj {cell=cell,origin=origin,fmz=fmz,spec=(x,p,m),probl=probl,

 	  meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}

   | repl_domID _ _ = raise PTREE "repl_domID takes no PrfObj";