(* use"ME/ctree.sml";

    use"ctree.sml";

    W.N.26.10.99

 writeln (pr_ptree pr_short pt);

 *)

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

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

 type cellID = int;     

 type cid = cellID list;

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

 type pos = posel list;

 datatype pos_ = 

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

   | Met    (*PblObj-position: method*)

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

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

 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;

 datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)

 	 L     (*go left at $*) 

        | R     (*go right at $*)

        | D;     (*go down at Abs*)

 type loc_ = lrd list;

 fun ldr2str L = "L"

   | ldr2str R = "R"

   | ldr2str D = "D";

 fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k;

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

 fun subst2str' thy' (s:subst) =

   (strs2str o 

    (map (pair2str o

 	 (apsnd (Sign.string_of_term (sign_of (assoc_thy thy')))) o 

 	 (apfst (Sign.string_of_term (sign_of (assoc_thy thy'))))))) s;

 type scrstate =       (*state for script interpreter*)

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

 	 * loc_       (*location of tac in script*)

 	 * term option(*argument of curried functions*)

 	 * term       (*value obtained by tac executed*)

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

        | ScrState of scrstate    (*for script interpreter*)

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

 type iist = istate option * istate option;

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

 (*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 (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)^")";

 type spec = domID * 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;

 datatype con = land | lor;

 fun subst2subs s = map (pair2str o 

 			(apfst (Sign.string_of_term (sign_of thy))) o

 			(apsnd (Sign.string_of_term (sign_of thy)))) s;

 fun subst2subs' s = map ((apfst (Sign.string_of_term (sign_of thy))) o

 			 (apsnd (Sign.string_of_term (sign_of thy)))) s;

 fun isapair2pair (Const ("Pair",_) $ a $ b) = (a,b);

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

 (*FE <-> KE: strings*)

 datatype tac = 

   Init_Proof of ((cterm' list) * spec) 

 (*Init_Proo_Hid of (dgmode * (cterm' list) * spec) 

 | Init_Proof                                       7.6.02java-sml*)

 | Model_Problem of pblID

 | Refine_Problem of pblID              | Refine_Tacitly of pblID

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

 | Apply_Method of metID                | 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      (*user_cmd for detailing some _EXISTING_ data*)

 | End_Detail  (*switches back to parent script*)                   

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

 	      (*EITHER: an input of me, details rewrites in a Set _after_

                 Rewrite_Set* has created PblObj (+ istate);

                 OR:: set by "solve Detail_Set" as tac in Transitive --

 		for recognition of "insert pt" detail (versus "cappend pt"*)

 | Calculate of string                  | End_Ruleset

             (* plus | minus | times | cancel | pow | sqrt *)

 | Substitute of subs                   | Apply_Assumption of cterm' list

 | Take of cterm'                       | Take_Inst of cterm'  

 | Group of (con * int list ) 

 (*| Subproblem_Full of (spec * (cterm' list))   *)

 | Subproblem of (domID * pblID)

 | CAScmd of cterm'  (*6.6.02 URD: Function formula *)                   

 | End_Subproblem

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

 | User (*internal, for ets*)           | 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 pblID     => "Model_Problem "^(strs2str pblID)

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

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

 (*| Match_Problem pblID     => "Match_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                  => "Detail"

   | End_Detail              => "End_Detail"

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

   | Detail_Set_Inst (subs, rls) => 

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

   | Calculate op_           => "Calculate "^op_ 

   | 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 (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 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                  => "Detail"

   | End_Detail              => "End_Detail"

   | Detail_Set rls          => "Detail_Set"

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

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

 type fmz_ = cterm' list;

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

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

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

 		       option (*only for the init_form*)

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

                     (*... form * (result* asumpts  ), saves time*)

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

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

 (*Detail' in me detailed into ...*)

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

 | Detail_Set' of theory' * rls * term(*term is needed for next_tac before 2nd

 				     applicable_in*)

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

 | End_Ruleset' of term

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

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

 | Substitute' of subst * term (*10.8.00+..*)* term              

 | 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

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

 (*TODO?: done partially for tests*)

 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')^","

     ^(Sign.string_of_term (sign_of thy) f)^",("^(Sign.string_of_term (sign_of thy) f')

     ^","^((strs2str o (map (Sign.string_of_term (sign_of thy)))) asm)^"))"

   | End_Detail' _             => "End_Detail' xxx"

   | Detail_Set' _             => "Detail_Set' xxx"

   | Detail_Set_Inst' _        => "Detail_Set_Inst' xxx"

   | 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^")"

   | _                       => "";

 (*'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= "^(Sign.string_of_term (sign_of thy) iar)^

   ",\n  res= "^(Sign.string_of_term (sign_of thy) 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 FIXSXXME*)

    (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  : cid,    (* 4.00 superfluous: use cid in DG only!!*)

 	       form  : term,    

 	       tac : tac,  (*8.01: superfluous -> ets !!!*)

 	       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,    

 	                          (*FIXX@ME result:term * term list

 				   => applicable_in =..rewrite_set_

 			           => rls = {erls: rls (NOT rls'),...}*)

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

   | PblObj of {cell  : cid,       (*unused*)

 	       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,      (*headform of calc-head*)

 	       spec  : spec,      (*explicitly input + displayed*)

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

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

 	       env   : envp,      (*FIXXXMEby loc 20.8.01 superfluous--delete*)

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

 20.8.01: loc will hold ets (diss p.94: (tac_,denval(=form|res),loc,env)*)

 	       branch: branch,

 	       result: term * term list,

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

 datatype ptree = 

     EmptyPtree

   | Nd of ppobj * (ptree list);

 val e_ptree = EmptyPtree;

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

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

 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;

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

 (*   ((((Sign.string_of_term (sign_of thy)) o #4 o hd) ori)^" "^

     (((Sign.string_of_term (sign_of thy)) 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) ^"   "^ 

    ((((Sign.string_of_term (sign_of thy)) o #4 o hd) ori)^" "^

     (((Sign.string_of_term (sign_of thy)) 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    _      = raise PTREE "get_obj f EmptyPtree"

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

   | get_obj f (Nd (b, 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:pos)) 

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

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

       (*FIXME: 'wrong type..' raised also if pos doesn't 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,...}) = c

   | g_cell   (PrfObj {cell = c,...}) = c;

 fun g_form   (PrfObj {form = 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_args    (PblObj {env = (a,_,_,_),...}) = a

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

 fun g_tacs    (PblObj {env = (_,a,_,_),...}) = a

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

 fun g_ets    (PblObj {env = (_,_,a,_),...}) = a

   | g_ets _    = raise PTREE "g_tacs not for PrfObj";

 fun g_asm    (PblObj {env = (_,_,_,a),...}) = a

   | g_asm _    = raise PTREE "g_asm 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_ostate (PblObj {ostate = r,...}) = r

   | g_ostate (PrfObj {ostate = r,...}) = r;

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

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

 fun existpt pos pt = can (get_obj I pt) pos;

 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;

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

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

 fun insert b EmptyPtree    []       = 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:pos)));

 (*

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

 *)

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

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

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

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

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

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

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

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

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

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

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

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

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

 fun repl_result l f' s (PrfObj {cell=cell,form=form,tac=tac,loc=_,

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

     PrfObj {cell=cell,form=form,tac=tac,loc= l,

 	    branch=branch,result = f',ostate = s}

   | repl_result l f' s (PblObj {cell=cell,origin=origin,fmz=fmz,

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

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

     PblObj {cell=cell,origin=origin,fmz=fmz,

 	    spec=spec,probl=probl,meth=meth,env=env,loc= l,

 	    branch=branch,result= f',ostate= s};

 fun repl_tac x (PrfObj {cell=cell,form=form,tac= _,loc=loc,

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

     PrfObj {cell=cell,form=form,tac= x,loc=loc,

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

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

 fun repl_branch b (PblObj {cell=cell,origin=origin,fmz=fmz,

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

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

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

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

   | repl_branch b (PrfObj {cell=cell,form=form,tac=tac,loc=loc,

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

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

 	    branch= b,result=result,ostate=ostate};

 fun repl_args args

   (PblObj {cell=cell,origin=origin,fmz=fmz,

 	   spec=spec,probl=probl,meth=meth,env=(_,tac,ets,asm),loc=loc,

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

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

 	  meth=meth,env=(args,tac,ets,asm),loc=loc,branch=branch,

 	  result=result,ostate=ostate}

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

 fun repl_tacs erul

   (PblObj {cell=cell,origin=origin,fmz=fmz,

 	   spec=spec,probl=probl,meth=meth,env=(arg,_,ets,asm),loc=loc,

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

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

 	  meth=meth,env=(arg,erul,ets,asm),loc=loc,branch=branch,

 	  result=result,ostate=ostate}

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

 fun repl_ets ets

   (PblObj {cell=cell,origin=origin,fmz=fmz,

 	   spec=spec,probl=probl,meth=meth,env=(arg,tac,_,asm),loc=loc,

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

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

 	  meth=meth,env=(arg,tac,ets,asm),loc=loc,branch=branch,

 	  result=result,ostate=ostate}

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

 fun repl_oris oris

   (PblObj {cell=cell,origin=(_,spe,hdf),fmz=fmz,

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

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

   PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,

 	  meth=meth,env=env,loc=loc,branch=branch,

 	  result=result,ostate=ostate}

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

 fun repl_orispec spe

   (PblObj {cell=cell,origin=(oris,_,hdf),fmz=fmz,

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

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

   PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,

 	  meth=meth,env=env,loc=loc,branch=branch,

 	  result=result,ostate=ostate}

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

 fun repl_loc l (PblObj {cell=cell,origin=origin,fmz=fmz,

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

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

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

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

   | repl_loc l (PrfObj {cell=cell,form=form,tac=tac,loc=_,

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

   PrfObj {cell=cell,form=form,tac=tac,loc= l,

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

 fun uni__asm asm' 

   (PblObj {cell=cell,origin=origin,fmz=fmz,

 	   spec=spec,probl=probl,meth=meth,env=(arg,tac,ets,asm),loc=loc,

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

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

 	  meth=meth,env=(arg,tac,ets,asm union asm'),loc=loc,branch=branch,

 	  result=result,ostate=ostate}

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

 fun uni__cid cell' 

   (PblObj {cell=cell,origin=origin,fmz=fmz,

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

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

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

 	  meth=meth,env=env,loc=loc,branch=branch,

 	  result=result,ostate=ostate}

   | uni__cid cell'

   (PrfObj {cell=cell,form=form,tac=tac,loc=loc,

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

   PrfObj {cell=cell union cell',form=form,tac=tac,loc=loc,

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

 (** applies (snd f) to 1 level of branches if ((fst f) b),

     f : (ppobj -> bool) * (int -> ptree list -> ptree list) **)

 fun appl_branch f EmptyPtree [] = (EmptyPtree, false)

   | appl_branch f EmptyPtree _  = raise PTREE "appl_branch f Empty _"

   | appl_branch f (Nd ( _, _)) [] = raise PTREE "appl_branch f _ []"

   | appl_branch f (Nd (b, bs)) (p::[]) = 

     if (fst f) b then (Nd (b, (snd f) (p:posel) bs), true)

     else (Nd (b, bs), false)

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

 	let val (b',bool) = appl_branch f (nth p bs) ps

 	in (Nd (b, repl_app bs p b'), bool) end;

 (* expl for f as used with appl_branch *)

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

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

   | test_trans _ = false;

 (*

 val cut_branch = (test_trans, curry take):

     (ppobj -> bool) * (int -> ptree list -> ptree list);

 .. formlery used for ...

 fun cut_tree _ [] = EmptyPtree

   | cut_tree pt pos = 

   let val (pt',cut) = appl_branch cut_branch pt pos

   in if cut andalso length pos > 1 then cut_tree pt' (lev_up pos)

      else pt' end;

 *)

 (* specialized appl_branch for cut + return cuts *)

 fun appl_cut EmptyPtree _  = raise PTREE "appl_cut Empty _"

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

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

   if test_trans b 

     then (Nd (b, take (p:posel, bs)), true,

 	  (flat o (map (get_all g_cell))) (takerest (p,bs)))

   else (Nd (b, bs), false, [])

   | appl_cut (Nd (b, bs)) (p::ps) =

     let val (b',bool,cuts) = appl_cut (nth p bs) ps

     in (Nd (b, repl_app bs p b'), bool, cuts) end;

 (* cut objs below and after a position as long as Transitive 

    FIXME?: whole ptree copied for each branch-level cut  

    FIXME!: should return pos list instead cellID list*)

 fun cut_tree _ ([]:pos) = raise PTREE "cut_tree _ []"

   | cut_tree pt pos =

   let

     fun cutfn pt cuts pos = 

       let val (pt', cut, cuts') = appl_cut pt pos;

 (*	val _ = writeln (foldr (op^) (cuts',""))     *)

       in if cut andalso length pos > 1 

 	   then cutfn pt' (cuts @ cuts') (lev_up pos)

 	 else (pt',cuts @ cuts') end

   in (apsnd flat (cutfn pt [] pos)):ptree * cid end;

 (* pt of max_on_surface

 > writeln (pr_ptree pr_cell pt);

 > val (pt',cutl) = cut_tree pt [4,1,1,1,1];

 val cutl = ["[4,1,1,1,2]:","[4,1,1,1,3]:"] : cid list

 > writeln (pr_ptree pr_cell pt');

 > val (pt'',cutl) = cut_tree pt [4,1];

 val cutl = [] : cid list

 > writeln (pr_ptree pr_cell pt'');

 > val (pt''',cutl) = cut_tree pt [1,1];

 val cutl =

   ["[1,2]:","[2]:","[3]:","[3,1]:","[3,2]:","[4]:","[4,1]:","[4,1,1]:",...]

   : cid list

 > writeln (pr_ptree pr_cell pt''');

 *)

 fun append_atomic p l f r f' s pt = 

   let 

       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) 

 		     else ((Some l, None), 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 = 

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

 (* called by Take *)

 fun append_form p l f pt = 

   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;

 fun cappend_form pt p loc f =

   apfst (append_form p loc f) (cut_tree pt p);

 fun append_result pt p l f s =

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

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

 fun append_parent p l f r b pt = 

   let 

     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 =

   apfst (append_parent p loc f r b) (cut_tree pt p);

 (*13.8.02 deleted again --- istate option

 fun init_ptree (strs,spec) =

   (Nd (PblObj 

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

 		origin= (strs,spec),

 		fmz = empty_ppc_ct',

 		spec  = empty_spec,

 		probl = []:itm list,

 		meth  = []:itm list,

 		env   = empty_envp,

 		loc   = (None, None),

 		branch= NoBranch,

 		result= empty_cterm',

 		ostate= Incomplete},[]));----------------*)

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

   (Nd (PblObj 

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

 		origin= (strs,spec,hdf),

 		fmz   = fmz,

 		spec  = empty_spec,

 		probl = []:itm list,

 		meth  = []:itm list,

 		env   = empty_envp,

 		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 =

   insert (PblObj 

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

 	   origin= (strs,spec,hdf),

 	   fmz   = fmz,

 	   spec  = empty_spec,

 	   probl = []:itm list,

 	   meth  = []:itm list,

 	   env   = empty_envp,

 	   loc   = (Some l, None),

 	   branch= TransitiveB,

 	   result= (e_term,[]),

 	   ostate= Incomplete}) pt p;

 fun cappend_problem _ [] loc fmz ori =

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

   | cappend_problem pt p loc fmz ori = 

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

 (* use"ME/sequent.sml";

    use"sequent.sml";

    *)

 (*

 fun update_fmz  pt pos x = appl_obj (repl_fmz  x) pt pos;

                                        1.00 not used anymore*)

 fun update_args   pt pos x = appl_obj (repl_args   x) pt pos;

 fun update_tacs   pt pos x = appl_obj (repl_tacs   x) pt pos;

 fun update_ets    pt pos x = appl_obj (repl_ets    x) pt pos;

 fun update_domID  pt pos x = appl_obj (repl_domID  x) pt pos;

 fun update_pblID  pt pos x = appl_obj (repl_pblID  x) pt pos;

 fun update_metID  pt pos x = appl_obj (repl_metID  x) pt pos;

 fun update_spec   pt pos x = appl_obj (repl_spec   x) pt pos;

 fun update_pbl    pt pos x = appl_obj (repl_pbl    x) pt pos;

 fun update_pblppc pt pos x = appl_obj (repl_pbl    x) pt pos;

 fun update_met    pt pos x = appl_obj (repl_met    x) pt pos;

 (*1.09.01 ----

 fun update_metppc pt pos x = 

   let val {rew_ord'=od,rls'=rs,asm_thm=at,asm_rls=ar,...} =

     get_obj g_met pt pos

   in appl_obj (repl_met 

      {rew_ord'=od,rls'=rs,asm_thm=at,asm_rls=ar,ppc=x}) 

     pt pos end;*)

 fun update_metppc pt pos x = appl_obj (repl_met    x) pt pos;

 fun union_asm     pt pos x = appl_obj (uni__asm    x) pt pos; 

 fun union_cid     pt pos x = appl_obj (uni__cid    x) pt pos;

 fun update_branch pt pos x = appl_obj (repl_branch x) pt pos;

 fun update_tac  pt pos x = appl_obj (repl_tac  x) pt pos;

 fun update_oris   pt pos x = appl_obj (repl_oris   x) pt pos;

 fun update_orispec   pt pos x = appl_obj (repl_orispec   x) pt pos;

  (*done by append_* !! 3.5.02*)

 fun update_loc pt (p,_) (ScrState ([],[],None,

 				   Const ("empty",_),Sundef,false)) = 

     appl_obj (repl_loc (None,None)) pt p

   | update_loc pt (p,Res) x =  

     let val (lform,_) = get_obj g_loc pt p

     in appl_obj (repl_loc (lform,Some x)) pt p end

   | update_loc pt (p,_) x = 

     let val (_,lres) = get_obj g_loc pt p

     in appl_obj (repl_loc (Some x,lres)) pt p end;

 (*13.8.02---------------------------

 fun get_loc EmptyPtree _ = None

   | get_loc pt (p,Res) =

   let val (lfrm,lres) = get_obj g_loc pt p

   in if lres = e_istate then lfrm else lres end

   | get_loc pt (p,_) =

   let val (lfrm,lres) = get_obj g_loc pt p

   in if lfrm = e_istate then lres else lfrm end;  5.10.00: too liberal ?*)

 (*13.8.02: options, because istate is no equalitype any more*)

 fun get_loc EmptyPtree _ = e_istate

   | get_loc pt (p,Res) =

     (case get_obj g_loc pt p of

 	 (Some i, None) => i

        | (None  , None) => e_istate

        | (_     , 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) => e_istate

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

 val get_istate = get_loc; (*3.5.02*)

 (*.collect the assumptions within a problem up to a certain position.*)

 fun get_asm (b:pos, p:pos) (Nd (PblObj {result=(_,asm),...},_)) = 

     ((*writeln ("### get_asm PblObj:(b,p)= "^

 		(pair2str(ints2str b, ints2str p)));*)

      (map (rpair b) asm))

   | get_asm (b, p) (Nd (PrfObj {result=(_,asm),...}, [])) = 

     ((*writeln ("### get_asm PrfObj []:(b,p)= "^

 	      (pair2str(ints2str b, ints2str p)));*)

      (map (rpair b) asm))

   | get_asm (b, p:pos) (Nd (PrfObj _, nds)) = 

     let (*val _= writeln ("### get_asm PrfObj nds:(b,p)= "^

 	      (pair2str(ints2str b, ints2str p)));*)

 	val levdn = 

 	    if p <> [] then (b @ [hd p]:pos, tl p:pos) 

 	    else (b @ [1], [99999]) (*_deeper_ nesting is always _before_ p*)

     in gets_asm levdn 1 nds end

 and gets_asm _ _ [] = []

   | gets_asm (b, p' as p::ps) i (nd::nds) = 

     if p < i then [] 

     else ((*writeln ("### gets_asm: (b,p')= "^(pair2str(ints2str b,

 						      ints2str p')));*)

 	  (get_asm (b @ [i], ps) nd) @ (gets_asm (b, p') (i + 1) nds));

 fun get_assumptions_ (Nd (PblObj {result=(r,asm),...}, cn)) (([], _):pos') = 

     if r = e_term then gets_asm ([], [99999]) 1 cn 

     else map (rpair []) asm

   | get_assumptions_ pt (p,p_) =

     let val (cn, base) = par_children pt p

 	val offset = drop (length base, p)

 	val base' = replicate (length base) 1

 	val offset' = case p_ of 

 			 Frm => let val (qs,q) = split_last offset

 				in qs @ [q - 1] end

 		       | _ => offset

         (*val _= writeln ("... get_assumptions: (b,o)= "^

 			(pair2str(ints2str base',ints2str offset)))*)

     in gets_asm (base', offset) 1 cn end;

 (*---------

 end

 open Ptree;

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

 (*pos of the formula on FE relative to the current pos,

   which is the next writepos*)

 fun pre_pos ([]:pos) = []:pos

   | pre_pos pp =

   let val (ps,p) = split_last pp

   in case p of 1 => ps | n => ps @ [n-1] end;

 (*WN.20.5.03 ... but not used*)

 fun posless [] (_::_) = true

   | posless (_::_) [] = false

   | posless (p::ps) (q::qs) = if p = q then posless ps qs else p < q;

 (* posless [2,3,4] [3,4,5];

 true

 >  posless [2,3,4] [1,2,3];

 false

 >  posless [2,3] [2,3,4];

 true

 >  posless [2,3,4] [2,3];

 false                    

 >  posless [6] [6,5,2];

 true

 +++ see Isabelle/../library.ML*)

 (*development for extracting an 'interval' from ptree stopped 8.03*)

 local

 fun hdp [] = 1     | hdp [0] = 1     | hdp x = hd x;

 fun hdq	[] = 99999 | hdq [0] = 99999 | hdq x = hd x;

 fun tlp [] = [0]     | tlp [_] = [0]     | tlp x = tl x;

 fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;

 fun drop_init ([]::xs) = drop_init xs

   | drop_init xs = xs;

 fun get_tr i (b,p) q (Nd (po, nds)) =

     [if  i <= 0 then b else []] 

     @ (writeln("get_tr: i="^(string_of_int i)^", b="^(ints2str' b)^", p="^

 	       (ints2str' p)^", q="^(ints2str' q));

        gets_tr (i-1) (b@[hdp p], tlp p) (tlq q) (take_be (hdp p) (hdq q) nds))

 and gets_tr i (b,p) q [] = ((*writeln"gets_tr: -------------------------[]";*)

 			    [])

   | gets_tr i (b,p) q (nd::nds) = 

     (writeln("gets_tr: i="^(string_of_int i)^", b="^(ints2str' b)^", p="^

 		   (ints2str' p)^", q="^(ints2str' q));

     (get_tr i (b,p) q nd) @ (gets_tr ~99999 (lev_on b, p) q nds)

     );

 fun get_trace pt p q =

     (drop_init o

      (gets_tr ((length p) -1) ([hdp p], tlp p) (tlq q))) 

 	    (take_be (hdp p) (hdq q) (children pt));

 in

 (*.get an 'interval' from ptree down to a certain level.*)

 fun get_tr f l i (b:pos, p:pos) (q:pos) (Nd (po, nds)) =

     if 0 < l then 

 	[if i<=0 then [(b, f po)] else [(*during initial recursive descent*)]]

 	@ (gets_tr f (l-1) (i-1) (b@[hdp p]:pos, tlp p:pos) (tlq q:pos) 

 		   (take_be (hdp p) (hdq q) nds))

     else []

 and gets_tr f l i (b,p) q [] = []

   | gets_tr f l i (b,p) q (nd::nds) = 

     (get_tr f l i (b,p) q nd) @ (gets_tr f l ~99999 (lev_on b, p) q nds);

 (*val get_tr = 

     fn : (ppobj -> 'a)      extracts info

          int ->             print_depth

 	 int ->             level count*~1 for initial recursive descent

 	 pos * 	            current position

 	 pos ->             preview to levels lower than current pos

 	 pos ->             end pos (static)

 	 ptree -> 

   * done by recursive descent over the whole ptree.

   * only the relevant nodes are taken at each level.

   * heads of pos dropped at each step to lower level.

   * pos going deeper than initial p q are handled by special hd tl.

   *)    

 fun get_trace pt (p:pos) (q:pos) f l =

     (flat o drop_init o

      (gets_tr f l ((length p) -1) ([hdp p], tlp p) (tlq q))) 

 	(take_be (hdp p) (hdq q) (children pt));

 end (*local*)

 (* mit rlang.sml 55b ... End_Proof

 > fun f _ = "";

 > get_trace pt [4,3] [5] f 99999;

 [[4,3],[4,4],[4,5],[4,5,1],[4,5,2],[4,5,3],[4,5,4],[4,5,5],[5]]

 > get_trace pt [4,3] [5] f 2;

 [([4,3],""),([4,4],""),([4,5],""),([5],"")]

 > get_trace pt [4,3] [4,5,1] f 99999;

 [[4,3],[4,4],[4,5],[4,5,1]]

 > get_trace pt [] [4,5,1] f 99999;

 [[1],[2],[3],[4],[4,1],[4,2],[4,3],[4,4],[4,5],[4,5,1]]

 > get_trace pt [] [] f 99999;

 [[1],[2],[3],[4],[4,1],[4,2],[4,3],[4,4],[4,5],[4,5,1],[4,5,2],[4,5,3],

  [4,5,4],[4,5,5],[5]]

 > get_trace pt [] [] f 2;

 [[1],[2],[3],[4],[4,1],[4,2],[4,3],[4,4],[4,5],[5]]

 > get_trace pt [4,5,5] [] f 99999;

 [([4,5,5],""),([5],"")]

 > get_trace pt [4,5,3] [4,5,3] f 99999;

 [([4,5,3],"")]

 *)

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

     let val domID = if dI = e_domID

 		    then if dI' = e_domID 

 			 then raise error"pt_extract: no domID in probl,origin"

 			 else dI'

 		    else dI

 	val pblID = if pI = e_pblID

 		    then if pI' = e_pblID 

 			 then raise error"pt_extract: no pblID in probl,origin"

 			 else pI'

 		    else pI

 	val metID = if mI = e_metID

 		    then if pI' = e_metID 

 			 then raise error"pt_extract: no metID in probl,origin"

 			 else mI'

 		    else mI

     in (domID, pblID, metID):spec end;

 (*extract a formula or model from ptree for itms2itemppc or model2xml*)

 type ocalhd = 

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

 	 term *                (*header: Problem... or Cas*)       

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

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

 	 spec;                 (*specification*)

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

 fun preconds2str bts = 

     (strs2str o (map (linefeed o pair2str o

 		      (apsnd term2str) o 

 		      (apfst bool2str)))) bts;

 fun ocalhd2str ((p, hdf, itms, prec, spec):ocalhd) =

     "("^pos_2str p^", "^term2str hdf^", "^itms2str (assoc_thy "Isac.thy") itms^

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

 datatype ptform =

 	 Form of term

        | ModSpec of ocalhd;

 val e_ptform = Form e_term;

 val e_ptform' = ModSpec e_ocalhd;

 fun pt_model (PblObj {meth,spec,origin=(_,spec',_),...}) Met =

     let val (_,_,metID) = get_somespec spec spec'

 	val {prls,pre=where_,...} = get_met metID

 	val (head, pre) = head_precond spec' None prls where_ meth 0

     in ModSpec (Met, head, meth, pre, spec) end

   | pt_model (PblObj {probl,spec,origin=(_,spec',_),...}) _(*Frm,Pbl*) =

     let val (_,pblID,_) = get_somespec spec spec'

 	val {prls,where_,cas,...} = get_pbt pblID

 	val (head, pre) = head_precond spec' cas prls where_ probl 0

     in ModSpec (Pbl, head, probl, pre, spec) end;

 fun pt_form (PrfObj {form,...}) = Form form

   | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =

     let val (dI, pI, _) = get_somespec spec spec'

 	val {cas,...} = get_pbt pI

     in case cas of

 	   None => Form (pblterm dI pI)

 	 | Some t => Form (subst_atomic (mk_env probl) t)

     end;

 fun pt_result (PrfObj {result=(t,_),...}) = Form t

   | pt_result (PblObj {result=(t,_),...}) = Form t;

 type asms = (term * pos) list;

 (*fun pt_extract (pt,(p,Frm):pos') = 

     let val f = get_obj pt_form pt p

     in (f, Tac"", []:asms, Sundef) end

   | pt_extract (pt,(p,Res)) =

     let val f = get_obj pt_result pt p

     in (f, Tac"", []:asms, Sundef) end

   | pt_extract (pt,(p,p_)) =

     let val ppobj = get_obj I pt p

 	val f = if is_pblobj ppobj then pt_model ppobj p_

 		else raise PTREE ("pt_extrac: tries to fetch modspec from "^

 				  pos'2str (p,p_))

     in (f, Tac"", []:asms, Sundef) end;*)

 (* val (pt,(p,p_)) = (pt, ip);

    *)

 fun pt_extract (pt,(p,Res)) =

     let val f = get_obj pt_result pt p

     in (f, Tac"", []:asms, Sundef) end

   | pt_extract (pt,(p,p_)) =

     let val ppobj = get_obj I pt p

 	val f = if is_pblobj ppobj then pt_model ppobj p_

 		else get_obj pt_form pt p

     in (f, Tac"", []:asms, Sundef) end;

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

 (**.functions for the 'ptree iterator' as seen from the FE-Kernel interface.**)

 (*.move one step down into existing nodes of ptree; regard TransitiveB.*)

 fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*)

 (* val (Nd (c, ns), ([],p_)) = (pt, get_pos cI uI);

    *)

     if is_pblobj c 

     then case p_ of Frm => ([], Pbl) 

 		  | Res => raise PTREE "end of calculation"

 		  | _ => if null ns (*go down from Pbl + Met*)

 			 then raise PTREE "solve problem not started"

 			 else ([1], Frm)

     else raise PTREE "pos not existent 1"

   (*iterate towards end of pos*)

   | move_dn P  (Nd (_, ns)) (p::(ps as (_::_)),p_) =

     if p > length ns then raise PTREE "pos not existent 2"

     else move_dn ((P@[p]): pos) (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 "pos not existent 3"

     else if is_pblnd (nth p ns)  then

 	(writeln("### move_dn: is_pblnd (nth p ns), P= "^ints2str' P^", \n"^

 		 "length ns= "^((string_of_int o length) ns)^

 		 ", p= "^string_of_int p^", p_= "^pos_2str p_);

 	 case p_ of Frm => ((P@[p], Pbl) : pos')

 		 | Res => if p = length ns 

 			  then 

 			      if g_ostate c = Complete then (P, Res)

 			      else raise PTREE "parent not complete"

 			  (*FIXME here handle not-sequential branches*)

 			  else 

 			      if g_branch c = TransitiveB 

 				 andalso (not o is_pblnd o (nth (p+1))) ns

 			      then (P@[p+1], Res) else (P@[p+1], Frm)

 		 | _ => if (null o children o (nth p)) ns (*go down from Pbl*)

 			then raise PTREE "solve subproblem not started"

 			else (P @ [p, 1], Frm)

 			     )

     else case p_ of Frm => if (null o children o (nth p)) ns then (P@[p],Res) 

 			   else (P @ [p, 1], Frm) (*go down*)

 		  | Res => if p = length ns 

 			   then 

 			      if g_ostate c = Complete then (P, Res)

 			      else raise PTREE "parent not complete"

 			   else 

 			       if g_branch c = TransitiveB 

 				  andalso (not o is_pblnd o (nth (p+1))) ns

 			       then (P@[p+1], Res) else (P@[p+1], Frm);

 (*.go one level down into ptree; goes to Frm.*)

 fun movelevel_dn [] (Nd (c, ns)) ([],p_) = (*root problem*)

     if is_pblobj c 

     then if null ns 

 	 then raise PTREE "solve problem not started"

 	 else ([1], Frm)

     else raise PTREE "pos not existent 1"

   (*iterate towards end of pos*)

   | movelevel_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =

     if p > length ns then raise PTREE "pos not existent 2"

     else movelevel_dn (P@[p]) (nth p ns) (ps, p_)

   | movelevel_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)

     if p > length ns then raise PTREE "pos not existent 3"

     else case p_ of Frm => if (null o children o (nth p)) ns 

 			   then raise PTREE "no children"

 			   else (P @ [p, 1], Frm) (*go down*)

 		  | Res => if p = length ns 

 			   then raise PTREE "no children"

 			   else 

 			       if g_branch c = TransitiveB

 			       then if (null o children o (nth (p+1))) ns

 				    then raise PTREE "no children"

 				    else (P@[p+1, 1], Frm)

 			       else if (null o children o (nth p)) ns

 				    then raise PTREE "no children"

 				    else (P@[p, 1], Frm);

 (*.go to the previous position in ptree; regard TransitiveB.*)

 fun move_up _ (Nd (c, ns)) (([],p_):pos') = (*root problem*)

     if is_pblobj c 

     then case p_ of Frm => raise PTREE "begin of calculation"

 		  | Pbl => ([], Frm) | Met => ([], Pbl)

 		  | Res => if null ns then ([], Pbl) (*Res -> Pbl (not Met)!*)

 			   else ([length ns], Res)

     else raise PTREE "pos not existent"

   | move_up P  (Nd (_, ns)) (p::(ps as (_::_)),p_) = (*iterate to end of pos*)

     if p > length ns then raise PTREE "pos not existent"

     else move_up (P@[p]) (nth p ns) (ps,p_)

   | move_up P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)

     if p > length ns then raise PTREE "pos not existent"

     else if is_pblnd (nth p ns)  then

 	case p_ of Frm => if p = 1 then (P, Pbl) else (P@[p-1], Res)

 		  | Pbl => (P@[p], Frm) | Met => (P@[p], Pbl)

 		  | Res => 

 		    let val nc = (length o children o (nth p)) ns

 		    in if nc = 0 then (P@[p], Pbl) (*Res -> Pbl (not Met)!*)

 		       else (P @ [p, nc], Res) end (*go down*)

     else case p_ of Frm => if p <> 1 then (P, Frm) 

 			  else if is_pblobj c then (P, Pbl) else (P, Frm)

 		  | Res => 

 		    let val nc = (length o children o (nth p)) ns

 		    in if nc = 0 (*cannot go down*)

 		       then if g_branch c = TransitiveB andalso p <> 1

 			    then (P@[p-1], Res) else (P@[p], Frm)

 		       else (P @ [p, nc], Res) end; (*go down*)

 (*.go one level up in ptree; sets the position on Frm.*)

 fun movelevel_up _ (Nd (c, ns)) (([],p_):pos') = (*root problem*)

     raise PTREE "pos not existent"

   (*iterate towards end of pos*)

   | movelevel_up P  (Nd (_, ns)) (p::(ps as (_::_)),p_) = 

     if p > length ns then raise PTREE "pos not existent"

     else movelevel_up (P@[p]) (nth p ns) (ps,p_)

   | movelevel_up P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)

     if p > length ns then raise PTREE "pos not existent"

     else if is_pblobj c then (P, Pbl) else (P, Frm);

 (*.go to the next calc-head up in the calc-tree.*)

 fun movecalchd_up pt ((p, Res):pos') =

     (par_pblobj pt p, Pbl):pos'

   | movecalchd_up pt (p, _) =

     if is_pblobj (get_obj I pt p) 

     then (p, Pbl) else (par_pblobj pt p, Pbl);