(* use"ME/generate.sml";

    use"generate.sml";

    *)

 (*.initialize istate for Detail_Set.*)

 fun init_istate (Rewrite_Set rls) t =

 (* val (Rewrite_Set rls) = (get_obj g_tac pt p);

    *)

     (case assoc_rls rls of

 	 Rrls {scr=sc as Rfuns {init_state=ii,...},...} => (RrlsState (ii t))

 (* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls;

    *)

        | Rls {scr=EmptyScr,...} => 

 	 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."

 		      ^"use prep_rls' for storing rule-sets !")

        | Rls {scr = Prog s,...} =>

 	 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))

        | Seq {scr=EmptyScr,...} => 

 	 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."

 		      ^"use prep_rls' for storing rule-sets !")

        | Seq {srls=srls,scr = Prog s,...} =>

 	 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)))

 (* val ((Rewrite_Set_Inst (subs, rls)), t) = ((get_obj g_tac pt p), t);

    *)

   | init_istate (Rewrite_Set_Inst (subs, rls)) t =

     let val (_, v)::_ = subs2subst (assoc_thy "Isac") subs

     (*...we suppose the substitution of only _one_ bound variable*)

     in case assoc_rls rls of

            Rls {scr=EmptyScr,...} => 

 	   error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."

 			^"use prep_rls' for storing rule-sets !")

 	 | Rls {scr = Prog s,...} =>

 	   let val (form, bdv) = two_scr_arg s

 	   in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))

 	   end

 	 | Seq {scr=EmptyScr,...} => 

 	   error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."

 			^"use prep_rls' for storing rule-sets !")

 	 | Seq {scr = Prog s,...} =>

 	   let val (form, bdv) = two_scr_arg s

 	   in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))

 	   end

     end;

 (*.a taci holds alle information required to build a node in the calc-tree;

    a taci is assumed to be used efficiently such that the calc-tree

    resulting from applying a taci need not be stored separately;

    see "type calcstate".*)

 (*TODO.WN0504 redesign ??? or redesign generate ?? see "fun generate"

   TODO.WN0512 ? redesign this _list_:

   # only used for [Apply_Method + (Take or Subproblem)], i.e. for initacs

   # the latter problem may be resolved automatically if "fun autocalc" is 

     not any more used for the specify-phase and for changing the phases*)

 type taci = 

      (tac *            (*for comparison with input tac*)      

       tac_ *           (*for ptree generation*)

       (pos' *          (*after applying tac_, for ptree generation*)

        (istate * Proof.context)));       (*after applying tac_, for ptree generation*)

 val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', (e_istate, e_ctxt))): taci;

 (* val (tac, tac_, (pos', istate))::_ = tacis';

    *)

 fun taci2str ((tac, tac_, (pos', (istate, _))):taci) =

     "( "^tac2str tac^", "^tac_2str tac_^", ( "^pos'2str pos'

     ^", "^istate2str istate^" ))";

 fun tacis2str tacis = (strs2str o (map (linefeed o taci2str))) tacis;

 datatype pblmet =       (*%^%*)

     Upblmet             (*undefined*)

   | Problem of pblID    (*%^%*)

   | Method of metID;    (*%^%*)

 fun pblmet2str (Problem pblID) = "Problem "^(strs2str pblID)(*%^%*)

   | pblmet2str (Method metID) = "Method "^(metID2str metID);(*%^%*)

       (*%^%*)   (*26.6. moved to sequent.sml: fun ~~~~~~~~~; was here below*)

 (* copy from 03.60.usecases.sml 15.11.99 *)

 datatype user_cmd = 

   Accept   | NotAccept | Example

 | YourTurn | MyTurn (* internal use only 7.6.02 java-sml*)   

 | Rules

 | DontKnow  (*| HowComes | WhatFor       7.6.02 java-sml*)

 | Undo      (*| Back          | Forward  7.6.02 java-sml*)

 | EndProof | EndSession

 | ActivePlus | ActiveMinus | SpeedPlus | SpeedMinus

                            (*Stepwidth...7.6.02 java-sml*)

 | Auto | NotAuto | Details;

 (* for test-print-outs *)

 fun user_cmd2str Accept     ="Accept"

   | user_cmd2str NotAccept  ="NotAccept"

   | user_cmd2str Example    ="Example"

   | user_cmd2str MyTurn     ="MyTurn"

   | user_cmd2str YourTurn   ="YourTurn"

   | user_cmd2str Rules	    ="Rules"

 (*| user_cmd2str HowComes   ="HowComes"*)

   | user_cmd2str DontKnow   ="DontKnow"

 (*| user_cmd2str WhatFor    ="WhatFor"

   | user_cmd2str Back       ="Back"*)

   | user_cmd2str Undo       ="Undo"

 (*| user_cmd2str Forward    ="Forward"*)

   | user_cmd2str EndProof   ="EndProof"

   | user_cmd2str EndSession ="EndSession"

   | user_cmd2str ActivePlus = "ActivePlus"

   | user_cmd2str ActiveMinus = "ActiveMinus"

   | user_cmd2str SpeedPlus = "SpeedPlus"

   | user_cmd2str SpeedMinus = "SpeedMinus"

   | user_cmd2str Auto = "Auto"

   | user_cmd2str NotAuto = "NotAuto"

   | user_cmd2str Details = "Details";

 (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)

 datatype foppFK =                  (* in DG cases div 2 *)

   EmptyFoppFK         (*DG internal*)

 | FormFK of cterm'

 | PpcFK of cterm' ppc;

 fun foppFK2str (FormFK ct') ="FormFK "^ct'

   | foppFK2str (PpcFK  ppc) ="PpcFK "^(ppc2str ppc)

   | foppFK2str EmptyFoppFK  ="EmptyFoppFK";

 datatype nest = Open | Closed | Nundef;

 fun nest2str Open = "Open"

   | nest2str Closed = "Closed"

   | nest2str Nundef = "Nundef";

 type indent = int;

 datatype edit = EdUndef | Write | Protect;

                                    (* bridge --> kernel *)

                                    (* bridge <-> kernel *)

 (* needed in dialog.sml *)         (* bridge <-- kernel *)

 fun edit2str EdUndef = "EdUndef"

   | edit2str Write = "Write"

   | edit2str Protect = "Protect";

 datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*)

   New_User | End_User                                          (*<->*)

 | New_Proof | End_Proof                                        (*<->*)

 | Command of user_cmd                                          (*-->*)

 | Request of string | Message of string                        (*<--*) 

 | Error_ of string  | System of string                         (*<--*)

 | FoPpcFK of foppFK                                            (*-->*)

 | FormKF of cellID * edit * indent * nest * cterm'             (*<--*)

 | PpcKF of cellID * edit * indent * nest * (pblmet * item ppc) (*<--*)

 | RuleFK of tac                                              (*-->*)

 | RuleKF of edit * tac                                       (*<--*)

 | RefinedKF of (pblID * ((itm list) * ((bool * term) list))) (*<--*)

 | Select of tac list                                         (*<--*)

 | RefineKF of match list                                       (*<--*)

 | Speed of int                                                 (*<--*)

 | Active of int                                                (*<--*)

 | Domain of domID;                                             (*<--*)

 fun inout2str End_Proof = "End_Proof"

   | inout2str (Command user_cmd) = "Command "^(user_cmd2str user_cmd)

   | inout2str (Request s) = "Request "^s

   | inout2str (Message s) = "Message "^s

   | inout2str (Error_  s) = "Error_ "^s

   | inout2str (System  s) = "System "^s

   | inout2str (FoPpcFK foppFK) = "FoPpcFK "^(foppFK2str foppFK)

   | inout2str (FormKF (cellID, edit, indent, nest, ct')) =  

 	       "FormKF ("^(string_of_int cellID)^","

 	       ^(edit2str edit)^","^(string_of_int indent)^","

 	       ^(nest2str nest)^",("

 	       ^ct' ^")"

   | inout2str (PpcKF (cellID, edit, indent, nest, (pm,itemppc))) =

 	       "PpcKF ("^(string_of_int cellID)^","

 	       ^(edit2str edit)^","^(string_of_int indent)^","

 	       ^(nest2str nest)^",("

 	       ^(pblmet2str pm)^","^(itemppc2str itemppc)^"))"

   | inout2str (RuleKF (edit,tac)) = "RuleKF "^

 	       pair2str(edit2str edit,tac2str tac)

   | inout2str (RuleFK tac) = "RuleFK "^(tac2str tac)  

   | inout2str (Select tacs)= 

 	       "Select "^((strs2str' o (map tac2str)) tacs)

   | inout2str (RefineKF ms)  = "RefineKF "^(matchs2str ms)

   | inout2str (Speed i) = "Speed "^(string_of_int i)

   | inout2str (Active i) = "Active "^(string_of_int i)

   | inout2str (Domain dI) = "Domain "^dI;

 fun inouts2str ios = (strs2str' o (map inout2str)) ios; 

 datatype mout =

   Form' of inout         (* packing cterm' | cterm' ppc *)

 | Problems of inout      (* passes specify (and solve)  *)

 | Error' of inout

 | EmptyMout;

 fun mout2str (Form' inout) ="Form' "^(inout2str inout)

   | mout2str (Error'  inout) ="Error' "^(inout2str inout)

   | mout2str (EmptyMout    ) ="EmptyMout";

 (*fun Form'2str (Form' )*)

 (* init pbl with ...,dsc,empty | [] *)

 fun init_pbl pbt = 

   let 

       fun pbt2itm (f, (d, t)) = 

           ((0, [], false, f, Inc ((d, []), (e_term, []))) : itm);

   in map pbt2itm pbt end;

 (*take formal parameters from pbt, for transfer from pbl/met-hierarchy*)

 fun init_pbl' pbt = 

   let 

     fun pbt2itm (f,(d,t)) = 

       ((0,[],false,f,Inc((d,[t]),(e_term,[]))):itm);

   in map pbt2itm pbt end;

 (*generate 1 ppobj in ptree*)

 (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*)

 fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p,p_)) pt = 

       (pos:pos',[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet, itms2itemppc thy [][]))),

          case p_ of

            Pbl => update_pbl pt p itmlist

 	       | Met => update_met pt p itmlist)

     (*WN110515 probably declare_constraints with input item (without dsc) --

       -- important when specifying without formalisation*)

   | generate1 thy (Add_Find' (_, itmlist)) _ (pos as (p,p_)) pt = 

       (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),

          case p_ of

            Pbl => update_pbl pt p itmlist

 	       | Met => update_met pt p itmlist)

     (*WN110515 probably declare_constraints with input item (without dsc)*)

   | generate1 thy (Add_Relation' (_, itmlist)) _ (pos as (p,p_)) pt = 

       (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),

          case p_ of

            Pbl => update_pbl pt p itmlist

 	       | Met => update_met pt p itmlist)

   | generate1 thy (Specify_Theory' domID) _ (pos as (p,_)) pt = 

     (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),

      update_domID pt p domID)

   | generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) _

 	      (pos as (p,_)) pt = 

     let val pt = update_pbl pt p itms

 	val pt = update_pblID pt p pI

     in ((p,Pbl),[],

 	Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))), 

 	pt) end

   | generate1 thy (Specify_Method' (mID, oris, itms)) _ 

 	      (pos as (p,_)) pt = 

     let val pt = update_oris pt p oris

 	val pt = update_met pt p itms

 	val pt = update_metID pt p mID

     in ((p,Met),[],

 	Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))), 

 	pt) end

   | generate1 thy (Model_Problem' (_, itms, met)) _ (pos as (p,_)) pt =

       let 

         val pt = update_pbl pt p itms

 	      val pt = update_met pt p met

      in (pos,[],Form'(PpcKF(0,EdUndef,0,Nundef, (Upblmet, itms2itemppc thy [] []))), pt)

      end

   | generate1 thy (Refine_Tacitly' (pI,pIre,domID,metID,pbl)) 

 	      _ (pos as (p,_)) pt = 

     let val pt = update_pbl pt p pbl

 	val pt = update_orispec pt p (domID,pIre,metID)

     in (pos,[],

 	Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),

 	pt) end

   | generate1 thy (Refine_Problem' (pI,_)) _ (pos as (p,_)) pt =

     let val (dI,_,mI) = get_obj g_spec pt p

 	val pt = update_spec pt p (dI, pI, mI)

     in (pos,[],

 	Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),pt)

     end

   | generate1 thy (Apply_Method' (_,topt, is, ctxt)) _ (pos as (p,p_)) pt = 

     ((*tracing("###generate1 Apply_Method': pos = "^pos'2str (p,p_));

      tracing("###generate1 Apply_Method': topt= "^termopt2str topt);

      tracing("###generate1 Apply_Method': is  = "^istate2str is);*)

      case topt of 

 	 SOME t => 

 	 let val (pt,c) = cappend_form pt p (is, ctxt) t

 	     (*val _= tracing("###generate1 Apply_Method: after cappend")*)

 	 in (pos,c, EmptyMout,pt)

 	 end

        | NONE => 

 	 (pos,[],EmptyMout,update_env pt p (SOME (is, ctxt))))

 (* val (thy, (Take' t), l, (p,p_), pt) = 

        ((assoc_thy "Isac"), tac_, is, pos, pt);

    *)

   | generate1 thy (Take' t) l (p,p_) pt = (* val (Take' t) = m; *)

   let (*val _=tracing("### generate1: Take' pos="^pos'2str (p,p_));*)

       val p = let val (ps,p') = split_last p(*no connex to prev.ppobj*)

 	    in if p'=0 then ps@[1] else p end;

     val (pt,c) = cappend_form pt p l t;

   in ((p,Frm):pos', c, 

       Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), pt) end

 (* val (l, (p,p_)) = (RrlsState is, p);

    val (thy, Begin_Trans' t, l, (p,Frm), pt) =

        (assoc_thy "Isac", tac_, is, p, pt);

    *)

   | generate1 thy (Begin_Trans' t) l (p,Frm) pt =

   let (* print_depth 99;

 	 map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;

 	 *)

       val (pt,c) = cappend_form pt p l t

       (* print_depth 99;

 	 map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;

 	 *)

       val pt = update_branch pt p TransitiveB (*040312*)

       (*replace the old PrfOjb ~~~~~*)

       val p = (lev_on o lev_dn(*starts with [...,0]*)) p; 

       val (pt,c') = cappend_form pt p l t(*FIXME.0402 same istate ???*);

   in ((p,Frm), c @ c', Form' (FormKF (~1,EdUndef,(length p), Nundef, 

 				 term2str t)), pt) end

   (* val (thy, Begin_Trans' t, l, (p,Res), pt) =

 	 (assoc_thy "Isac", tac_, is, p, pt);

       *)

   | generate1 thy (Begin_Trans' t) l (p       ,Res) pt =

     (*append after existing PrfObj    _________*)

     generate1 thy (Begin_Trans' t) l (lev_on p,Frm) pt

   | generate1 thy (End_Trans' tasm) l (p,p_) pt =

       let

         val p' = lev_up p

         val (pt,c) = append_result pt p' l tasm Complete;

       in ((p',Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), pt) end

   | generate1 thy (Rewrite_Inst' (_,_,_,_,subs', thm', f, (f', asm))) (is, ctxt) (p,p_) pt =

       let

         val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f

           (Rewrite_Inst (subst2subs subs', thm')) (f',asm) Complete;

         val pt = update_branch pt p TransitiveB

       in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end

  | generate1 thy (Rewrite' (thy', ord', rls', pa, thm', f, (f', asm))) (is, ctxt) (p, p_) pt =

       let

         val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f

           (Rewrite thm') (f',asm) Complete

         val pt = update_branch pt p TransitiveB

       in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end

   | generate1 thy (Rewrite_Asm' all) l p pt = generate1 thy (Rewrite' all) l p pt

   | generate1 thy (Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm))) (is, ctxt) (p,p_) pt =

       let

         val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f 

           (Rewrite_Set_Inst (subst2subs subs',id_rls rls')) (f',asm) Complete

         val pt = update_branch pt p TransitiveB

       in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end

   | generate1 thy (Detail_Set_Inst' (_,_,subs,rls,f,(f',asm))) (is, ctxt) (p,p_) pt =

       let

         val ctxt' = insert_assumptions asm ctxt

         val (pt,c) = cappend_form pt p (is, ctxt') f 

         val pt = update_branch pt p TransitiveB

        val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f 

         val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt')

         val pos' = ((lev_on o lev_dn) p, Frm)

       in (*implicit Take*) generate1 thy tac_ (is, ctxt') pos' pt end

   | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) (is, ctxt) (p,p_) pt =

       let

         val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f 

           (Rewrite_Set (id_rls rls')) (f',asm) Complete

         val pt = update_branch pt p TransitiveB

       in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end

   | generate1 thy (Detail_Set' (_,_,rls,f,(f',asm))) (is, ctxt) (p,p_) pt =

       let

         val ctxt' = insert_assumptions asm ctxt

         val (pt,c) = cappend_form pt p (is, ctxt') f 

         val pt = update_branch pt p TransitiveB

         val is = init_istate (Rewrite_Set (id_rls rls)) f

         val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt')

         val pos' = ((lev_on o lev_dn) p, Frm)

       in (*implicit Take*) generate1 thy tac_ (is, ctxt') pos' pt end

   | generate1 thy (Check_Postcond' (pI, (scval, asm))) l (p,p_) pt =

       let val (pt,c) = append_result pt p l (scval, asm) Complete

       in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str scval)), pt) end

   | generate1 thy (Calculate' (thy',op_,f,(f',thm'))) l (p,p_) pt =

       let val (pt,c) = cappend_atomic pt p l f (Calculate op_) (f',[]) Complete;

       in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end

   | generate1 thy (Check_elementwise' (consts,pred,(f',asm))) l (p,p_) pt =

       let

         val (pt,c) = cappend_atomic pt p l consts (Check_elementwise pred) (f',asm) Complete;

       in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end

   | generate1 thy (Or_to_List' (ors,list)) l (p,p_) pt =

       let val (pt,c) = cappend_atomic pt p l ors Or_to_List (list,[]) Complete;

       in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, term2str list)), pt) end

   | generate1 thy (Substitute' (_, _, subte, t, t')) l (p,p_) pt =

       let 

         val (pt,c) =

           cappend_atomic pt p l t (Substitute (subte2sube subte)) (t',[]) Complete;

         in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, term2str t')), pt) 

         end

   | generate1 thy (Tac_ (_,f,id,f')) l (p,p_) pt =

       let

         val (pt,c) =

           cappend_atomic pt p l (str2term f) (Tac id) (str2term f',[]) Complete;

       in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f')), pt)end

   | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt, f)) l (p,p_) pt =

       let

 	      val (pt,c) =

           cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl);

         val pt = update_ctxt pt p ctxt

 	      val f = Syntax.string_of_term (thy2ctxt thy) f;

       in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end

   | generate1 thy m' _ _ _ = 

       error ("generate1: not impl.for "^(tac_2str m'));

 fun generate_inconsistent_rew (subs_opt, thm') f' (is, ctxt) (pos as (p,_)) pt =

   let

     val f = get_curr_formula (pt, pos);

     val pos' as (p', _) = (lev_on p, Res);

     val (pt,c) = 

       case subs_opt of

         NONE => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f

           (Rewrite thm') (f', []) Inconsistent

       | SOME subs => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f

           (Rewrite_Inst (subs, thm')) (f', []) Inconsistent

     val pt = update_branch pt p' TransitiveB;

   in (pt, pos') end

 fun generate_hard thy m' (p,p_) pt =

   let  

     val p =

       case p_ of

         Frm => p | Res => lev_on p

       | _ => error ("generate_hard: call by " ^ pos'2str (p,p_));

   in generate1 thy m' (e_istate, e_ctxt) (p,p_) pt end;

 (*tacis are in reverse order from nxt_solve_/specify_: last = fst to insert*)

 fun generate ([]: taci list) ptp = ptp

   | generate tacis (pt, c, _:pos'(*!dropped!WN0504redesign generate/tacis?*))= 

       let

         val (tacis', (_, tac_, (p, is))) = split_last tacis

 	      val (p',c',_,pt') = generate1 (assoc_thy "Isac") tac_ is p pt

       in generate tacis' (pt', c@c', p') end;

 (*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls       *

  *  of for connecting a user-input formula with the current calc-state.	     *

  *# It is somewhat incompatible with the rest of the math-engine:	     *

  *  (1) it is not created by a script					     *

  *  (2) thus there cannot be another user-input within a derivation	     *

  *# It suffers particularily from the not-well-foundedness of the math-engine*

  *  (1) FIXME other branchtyptes than Transitive will change 'embed_deriv'   *

  *  (2) FIXME and eventually 'compare_step' (ie. the script interpreter)     *

  *  (3) FIXME and eventually 'lev_back'                                      *

  *# SOME improvements are evident FIXME.040215 '_deriv'ation:	             *

  *  (1) FIXME nest Rls_ in 'make_deriv'					     *

  *  (2) FIXME do the not-reversed part in 'make_deriv' by scripts -- thus    *

  *	user-input will become possible in this part of a derivation	     *

  *  (3) FIXME do (2) only if a derivation has been found -- for efficiency,  *

  *	while a non-derivable inform requires to step until End_Proof'	     *

  *  (4) FIXME find criteria on when _not_ to step until End_Proof'           *

  *  (5) FIXME 

 .*)

 (*.update pos in tacis for embedding by generate.*)

 (* val 

    *)

 fun insert_pos _ [] = []

   | insert_pos (p:pos) (((tac,tac_,(_, ist))::tacis):taci list) = 

     ((tac,tac_,((p, Res), ist)):taci)

     ::((insert_pos (lev_on p) tacis):taci list);

 fun res_from_taci (_, Rewrite'(_,_,_,_,_,_,(res, asm)), _) = (res, asm)

   | res_from_taci (_, Rewrite_Set'(_,_,_,_,(res, asm)), _) = (res, asm)

   | res_from_taci (_, tac_, _) = 

     error ("res_from_taci: called with" ^ tac_2str tac_);

 (*.embed the tacis created by a '_deriv'ation; sys.form <> input.form

   tacis are in order, thus are reverted for generate.*)

 (* val (tacis, (pt, pos as (p, Frm))) =  (tacis', ptp);

    *)

 fun embed_deriv (tacis:taci list) (pt, pos as (p, Frm):pos') =

   (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402

     and transfer the istate (from _after_ compare_deriv) from Frm to Res*)

     let val (res, asm) = (res_from_taci o last_elem) tacis

 	val (SOME (ist, ctxt),_) = get_obj g_loc pt p

 	val form = get_obj g_form pt p

       (*val p = lev_on p; ---------------only difference to (..,Res) below*)

 	val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, ctxt)))

 		    ::(insert_pos ((lev_on o lev_dn) p) tacis)

 		    @ [(End_Trans, End_Trans' (res, asm),

 			(pos_plus (length tacis) (lev_dn p, Res), 

 			 (new_val res ist, ctxt)))]

 	val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))

 	val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res))

 	val pt = update_tac pt p (Derive (id_rls nrls))

         (*FIXME.040216 struct.ctree*)

 	val pt = update_branch pt p TransitiveB

     in (c, (pt, pos:pos')) end

 (* val (tacis, (pt, (p, Res))) =  (tacis', ptp);

    *)

   | embed_deriv tacis (pt, (p, Res)) =

   (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?

     and transfer the istate (from _after_ compare_deriv) from Res to new Res*)

     let val (res, asm) = (res_from_taci o last_elem) tacis

 	val (_, SOME (ist, ctxt)) = get_obj g_loc pt p

 	val (f,a) = get_obj g_result pt p

 	val p = lev_on p(*---------------only difference to (..,Frm) above*);

 	val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, ctxt)))

 		    ::(insert_pos ((lev_on o lev_dn) p) tacis)

 		    @ [(End_Trans, End_Trans' (res, asm), 

 			(pos_plus (length tacis) (lev_dn p, Res), 

 			 (new_val res ist, ctxt)))];

 	val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))

 	val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res))

 	val pt = update_tac pt p (Derive (id_rls nrls))

         (*FIXME.040216 struct.ctree*)

 	val pt = update_branch pt p TransitiveB

     in (c, (pt, pos)) end;