(* Title: generate specific entries into Ctree

   Author: Walther Neuper

   (c) due to copyright terms

*)

signature GENERATE_CALC_TREE =

sig

  (* vvv request into signature is incremental with *.sml *)

  (* for calchead.sml ---------------------------------------------------------------  vvv *)

  type taci

  val e_taci : taci

  datatype pblmet = Method of Celem.metID | Problem of Celem.pblID | Upblmet

  datatype mout =

    EmptyMout

  | Error' of string

  | FormKF of Rule.cterm'

  | PpcKF of pblmet * Model.item Model.ppc

  | RefinedKF of Celem.pblID * (Model.itm list * (bool * term) list)

  val generate1 : theory -> Tactic.T -> Istate.T * Proof.context ->

    Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree (* for calchead.sml------------- ^^^ *)

  val init_istate : Tactic.input -> term -> Istate.T

  val init_pbl : (string * (term * 'a)) list -> Model.itm list

  val init_pbl' : (string * (term * term)) list -> Model.itm list

  val embed_deriv : taci list -> Ctree.state -> Ctree.pos' list * (Ctree.state) (* for inform.sml *)

  val generate_hard : (* for solve.sml *)

    theory -> Tactic.T -> Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree

  val generate : (Tactic.input * Tactic.T * (Ctree.pos' * (Istate.T * Proof.context))) list ->

    Ctree.ctree * Ctree.pos' list * Ctree.pos' -> Ctree.ctree * Ctree.pos' list * Ctree.pos' (* for mathengine.sml *)

  val generate_inconsistent_rew : Selem.subs option * Celem.thm'' -> term -> Istate.T * Proof.context ->

    Ctree.pos' -> Ctree.ctree -> Ctree.state (* for interface.sml *)

(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

  val tacis2str : taci list -> string

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

  (*  NONE *)

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

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

  (* NONE *)

end

structure Generate(**): GENERATE_CALC_TREE(**) =

struct

open Ctree

(* initialize istate for Detail_Set *)

fun init_istate (Tactic.Rewrite_Set rls) t =

    (case assoc_rls rls of

      Rule.Rrls {scr = Rule.Rfuns {init_state = ii, ...}, ...} => Istate.RrlsState (ii t)

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

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

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

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

      (Istate.Pstate ([(hd (LTool.formal_args s), t)], [], NONE, Rule.e_term, Istate.Sundef, true))

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

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

		    " Use prep_rls' for storing rule-sets !")

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

(writeln ("### init_istate: rls = \"" ^ "rls" ^ "\", Prog = \"" ^ Rule.term2str s ^ "\"");

      (Istate.Pstate ([(hd (LTool.formal_args s), t)], [], NONE, Rule.e_term, Istate.Sundef, true))

)

    | _ => error "init_istate Rewrite_Set: uncovered case assoc_rls")

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

    let

      val v = case Selem.subs2subst (Celem.assoc_thy "Isac") subs of

        (_, v) :: _ => v

      | _ => error "init_istate: uncovered case "

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

    in case assoc_rls rls of

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

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

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

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

	    let val env = (LTool.formal_args s) ~~ [t, v]

	    in (Istate.Pstate (env, [], NONE, Rule.e_term, Istate.Sundef,true))

	    end

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

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

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

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

	    let val env = (LTool.formal_args s) ~~ [t, v]

	    in (Istate.Pstate (env,[], NONE, Rule.e_term, Istate.Sundef,true))

	    end

    | _ => error "init_istate Rewrite_Set_Inst: uncovered case assoc_rls"

    end

  | init_istate tac _ = error ("init_istate: uncovered definition for " ^ Tactic.tac2str tac)

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

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

   Tactic.T *                         (* for ctree generation                      *)

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

    (Istate.T * Proof.context)))  (* after applying tac_, for ctree generation *)

val e_taci = (Tactic.Empty_Tac, Tactic.Empty_Tac_, (e_pos', (Istate.e_istate, ContextC.e_ctxt))): taci

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

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

  Istate.istate2str istate ^ " ))"

fun tacis2str tacis = (strs2str o (map (Celem.linefeed o taci2str))) tacis

datatype pblmet =           (*%^%*)

  Upblmet                   (*undefined*)

| Problem of Celem.pblID    (*%^%*)

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

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

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

  | pblmet2str x = error ("pblmet2str: uncovered definition " ^ pblmet2str x)

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

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

  EmptyFoppFK         (*DG internal*)

| FormFK of Rule.cterm'

| PpcFK of Rule.cterm' Model.ppc

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

  | foppFK2str (PpcFK  ppc) ="PpcFK " ^ Model.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*)

  Error_ of string                                                         (*<--*)

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

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

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

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

(*

  datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout

*)

datatype mout =

  FormKF of Rule.cterm'

| PpcKF of (pblmet * Model.item Model.ppc) 

| RefinedKF of Celem.pblID * (Model.itm list * (bool * term) list)

| Error' of string

| EmptyMout

fun mout2str (FormKF cterm') = "FormKF " ^ cterm'

  | mout2str (PpcKF  (pm, itemppc)) = "PpcKF (" ^ pblmet2str pm ^ "," ^ Model.itemppc2str itemppc ^ ")"

  | mout2str (RefinedKF  (_, _)) = "mout2str: RefinedKF not impl."

  | mout2str (Error'  str) = "Error' " ^ str

  | mout2str (EmptyMout    ) = "EmptyMout"

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

fun init_pbl pbt = 

  let

    fun pbt2itm (f, (d, _)) = (0, [], false, f, Model.Inc ((d, []), (Rule.e_term, [])))

  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, Model.Inc((d, [t]), (Rule.e_term, [])))

  in map pbt2itm pbt end

(*generate 1 ppobj in ctree*)

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

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

    (pos: pos', [], PpcKF (Upblmet, Specify.itms2itemppc thy [][]),

       case p_ of

         Pbl => update_pbl pt p itmlist

	     | Met => update_met pt p itmlist

       | _ => error ("uncovered case " ^ pos_2str p_))

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

      -- important when specifying without formalisation *)

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

    (pos, [], (PpcKF (Upblmet, Specify.itms2itemppc thy [] [])),

       case p_ of

         Pbl => update_pbl pt p itmlist

	     | Met => update_met pt p itmlist

       | _ => error ("uncovered case " ^ pos_2str p_))

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

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

    (pos, [],  PpcKF (Upblmet, Specify.itms2itemppc thy [] []),

       case p_ of

         Pbl => update_pbl pt p itmlist

	     | Met => update_met pt p itmlist

       | _ => error ("uncovered case " ^ pos_2str p_))

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

    (pos, [] , PpcKF  (Upblmet, Specify.itms2itemppc thy [] []),

      update_domID pt p domID)

  | generate1 thy (Tactic.Specify_Problem' (pI, (_, (itms, _)))) _ (p, _) pt = 

    let

      val pt = update_pbl pt p itms

      val pt = update_pblID pt p pI

    in

      ((p, Pbl), [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt)

    end

  | generate1 thy (Tactic.Specify_Method' (mID, oris, itms)) _ (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), [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt)

    end

  | generate1 thy (Tactic.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, [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt)

    end

  | generate1 thy (Tactic.Refine_Tacitly' (_, 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, [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt)

    end

  | generate1 thy (Tactic.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, [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt)

    end

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

    (case topt of 

      SOME t => 

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

        in (pos, c, EmptyMout, pt) end

    | NONE => (pos, [], EmptyMout, update_env pt p (SOME (is, ctxt))))

  | generate1 _ (Tactic.Take' t) l (p, _) pt = (* val (Take' t) = m; *)

    let

      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, FormKF (Rule.term2str t), pt)

    end

  | generate1 _ (Tactic.Begin_Trans' t) l (p, Frm) pt =

    let

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

      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', FormKF (Rule.term2str t), pt)

    end

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

    (*append after existing PrfObj    vvvvvvvvvvvvv*)

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

  | generate1 _ (Tactic.End_Trans' tasm) l (p, _) pt =

    let

      val p' = lev_up p

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

    in

      ((p', Res), c, FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)

    end

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

    let

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

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

      val pt = update_branch pt p TransitiveB

    in

      ((p, Res), c, FormKF (Rule.term2str f'), pt)

    end

 | generate1 _ (Tactic.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (p, _) pt =

   let

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

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

     val pt = update_branch pt p TransitiveB

   in

    ((p, Res), c, FormKF (Rule.term2str f'), pt)

   end

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

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

    let

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

        (Tactic.Rewrite_Set_Inst (Selem.subst2subs subs', Rule.id_rls rls')) (f', asm) Complete

      val pt = update_branch pt p TransitiveB

    in

      ((p, Res), c, FormKF (Rule.term2str f'), pt)

    end

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

    let

      val ctxt' = ContextC.insert_assumptions asm ctxt

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

      val pt = update_branch pt p TransitiveB

      val is = init_istate (Tactic.Rewrite_Set_Inst (Selem.subst2subs subs, Rule.id_rls rls)) f 

      val tac_ = Tactic.Apply_Method' (Celem.e_metID, SOME Rule.e_term (*t ..has not been declared*), is, ctxt')

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

    in

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

    end

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

    let

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

        (Tactic.Rewrite_Set (Rule.id_rls rls')) (f',asm) Complete

      val pt = update_branch pt p TransitiveB

    in

      ((p, Res), c, FormKF (Rule.term2str f'), pt)

    end

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

    let

      val ctxt' = ContextC.insert_assumptions asm ctxt

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

      val pt = update_branch pt p TransitiveB

      val is = init_istate (Tactic.Rewrite_Set (Rule.id_rls rls)) f

      val tac_ = Tactic.Apply_Method' (Celem.e_metID, SOME Rule.e_term (*t ..has not been declared*), is, ctxt')

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

    in

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

    end

  | generate1 _ (Tactic.Check_Postcond' (_, (scval, asm))) l (p, _) pt =

      let

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

      in

        ((p, Res), c, FormKF (Rule.term2str scval), pt)

      end

  | generate1 _ (Tactic.Calculate' (_, op_, f, (f', _))) l (p, _) pt =

      let

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

      in

        ((p, Res), c, FormKF (Rule.term2str f'), pt)

      end

  | generate1 _ (Tactic.Check_elementwise' (consts, pred, (f', asm))) l (p, _) pt =

      let

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

      in

        ((p, Res), c, FormKF (Rule.term2str f'), pt)

      end

  | generate1 _ (Tactic.Or_to_List' (ors, list)) l (p, _) pt =

      let

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

      in

        ((p, Res), c, FormKF (Rule.term2str list), pt)

      end

  | generate1 _ (Tactic.Substitute' (_, _, subte, t, t')) l (p, _) pt =

      let

        val (pt,c) =

          cappend_atomic pt p l t (Tactic.Substitute (Selem.subte2sube subte)) (t',[]) Complete

        in ((p, Res), c, FormKF (Rule.term2str t'), pt) 

        end

  | generate1 _ (Tactic.Tac_ (_, f, id, f')) l (p, _) pt =

      let

        val (pt, c) = cappend_atomic pt p l (TermC.str2term f) (Tactic.Tac id) (TermC.str2term f', []) Complete

      in

        ((p,Res), c, FormKF f', pt)

      end

  | generate1 thy (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, _, f))

      (l as (_, ctxt)) (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 (Rule.thy2ctxt thy) f

    in

      ((p, Pbl), c, FormKF f, pt)

    end

  | generate1 _ m' _ _ _ = error ("generate1: not impl.for " ^ Tactic.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, _) = case subs_opt of

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

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

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

        (Tactic.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' (Istate.e_istate, ContextC.e_ctxt) (p,p_) pt end

(* tacis are in reverse order from do_solve_step/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 (Celem.assoc_thy "Isac") tac_ is p pt

    in

      generate tacis' (pt', c@c', p')

    end

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

fun insert_pos (_: pos) [] = []

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

    ((tac, tac_, ((p, Res), ist)): taci) :: (insert_pos (lev_on p) tacis)

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

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

  | res_from_taci (_, tac_, _) = error ("res_from_taci: called with" ^ Tactic.tac_2str tac_)

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

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

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 (ist, ctxt) = case get_obj g_loc pt p of

    	  (SOME (ist, ctxt), _) => (ist, ctxt)

      | (NONE, _) => error "embed_deriv Frm: uncovered case get_obj"

    	val form = get_obj g_form pt p

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

    	val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate.Uistate, ctxt))) ::

    		(insert_pos ((lev_on o lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),

    			(pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))]

    	val {nrls, ...} = Specify.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 (Tactic.Derive (Rule.id_rls nrls))

    	val pt = update_branch pt p TransitiveB

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

  | 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 (ist, ctxt) = case get_obj g_loc pt p of

    	  (_, SOME (ist, ctxt)) => (ist, ctxt)

      | (_, NONE) => error "embed_deriv Frm: uncovered case get_obj"

    	val (f, _) = get_obj g_result pt p

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

    	val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Frm), (Istate.Uistate, ctxt))) ::

    		(insert_pos ((lev_on o lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm), 

    			(pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))];

    	val {nrls, ...} = Specify.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 (Tactic.Derive (Rule.id_rls nrls))

    	val pt = update_branch pt p TransitiveB

    in (c, (pt, pos)) end

  | embed_deriv _ _ = error "embed_deriv: uncovered definition"

end