(* Title:  Interpret/lucase-interpreter.sml

   Author: Walther Neuper 2019

   (c) due to copyright terms

*)

signature LUCAS_INTERPRETER =

sig

  val next_tac : (*diss: next-tactic-function*)

    Rule.theory' * Rule.rls -> Ctree.state -> Rule.scr -> Selem.istate * 'a -> Tac.tac_ * (Selem.istate * 'a) * (term * Selem.safe)

  val inform : Chead.calcstate' -> string -> string * Chead.calcstate'

  val nxt_solve_ : Ctree.ctree * Ctree.pos' ->

    (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list *

      Ctree.pos' list * Ctree.state

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

  val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate'

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

end

structure LucinNEW(** ): LUCAS_INTERPRETER( **) = (*LucinNEW \<rightarrow> Lucin after code re-arrangement*)

struct

open Ctree

(*go at a location in a script and fetch the contents*)

fun go [] t = t

  | go (Celem.D :: p) (Abs(_, _, t0)) = go (p : Celem.loc_) t0

  | go (Celem.L :: p) (t1 $ _) = go p t1

  | go (Celem.R :: p) (_ $ t2) = go p t2

  | go l _ = error ("go: no " ^ Celem.loc_2str l);

(** find the next stactic in a program **)

(* handle a leaf at the end of recursive descent:

   a leaf is either a tactic or an 'expr' in "let v = expr"

   where "expr" does not contain a tactic.

   Handling a leaf comprises

   (1) 'subst_stacexpr' substitute LTool.env and complete curried tactic

   (2) rewrite the leaf by 'srls'

*)

fun handle_leaf call thy srls E a v t =

      (*WN050916 'upd_env_opt' is a blind copy from previous version*)

    case LTool.subst_stacexpr E a v t of

	    (a', LTool.STac stac) => (*script-tactic*)

	      let val stac' =

            Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (Lucin.upd_env_opt E (a,v)) stac)

	      in

          (if (! trace_script) 

	         then tracing ("@@@ "^call^" leaf '" ^ Rule.term2str t^"' ---> STac '" ^ Rule.term2str stac ^"'")

	         else ();

	         (a', LTool.STac stac'))

	      end

    | (a', LTool.Expr lexpr) => (*leaf-expression*)

	      let val lexpr' =

            Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (Lucin.upd_env_opt E (a,v)) lexpr)

	      in

          (if (! trace_script) 

	         then tracing("@@@ "^call^" leaf '" ^ Rule.term2str t^"' ---> Expr '" ^ Rule.term2str lexpr'^"'")

	         else ();

	         (a', LTool.Expr lexpr')) (*lexpr' is the value of the Expr*)

	      end;

(*appy, nxt_up, nstep_up scanning for next_tac.

  search is clearly separated into (1)-(2):

  (1) appy is recursive descent;

  (2) nxt_up resumes interpretation at a location somewhere in the script;

      nstep_up does only get to the parentnode of the scriptexpr.

  consequence:

  * call of (2) means _always_ that in this branch below

    there was an applicable stac (Repeat, Or e1, ...)

*)

datatype appy =    (* ExprVal in the sense of denotational semantics  *)

    Appy of        (* applicable stac found, search stalled           *)

    Tac.tac_ *     (* tac_ associated (fun assod) with stac           *)

    Selem.scrstate (* after determination of stac WN.18.8.03          *)

  | Napp of        (* stac found was not applicable; 

	                    this mode may become Skip in Repeat, Try and Or *)

    LTool.env      (* popped while nxt_up                             *)

  | Skip of        (* for restart after Appy, for leaving iterations,

	                    for passing the value of scriptexpressions,

		                  and for finishing the script successfully       *)

    term * LTool.env  (*a stack*);

datatype appy_ = (* as argument in nxt_up, nstep_up, from appy               *)

(*Appy              is only (final) returnvalue, not argument during search  *)

  Napp_          (* ev. detects 'script is not appropriate for this example' *)

| Skip_;         (* detects 'script successfully finished'

		                also used as init-value for resuming; this works,

	                  because 'nxt_up Or e1' treats as Appy                    *)

fun appy thy ptp E l (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) a v =

    (case appy thy ptp E (l @ [Celem.L, Celem.R]) e a v of

      Skip (res, E) => 

        let val E' = LTool.upd_env E (Free (i,T), res);

        in appy thy ptp E' (l @ [Celem.R, Celem.D]) b a v end

    | ay => ay)

  | appy (thy as (th,sr)) ptp E l (Const ("Script.While"(*1*),_) $ c $ e $ a) _ v =

    (if Rewrite.eval_true_ th sr (subst_atomic (LTool.upd_env E (a,v)) c)

     then appy thy ptp E (l @ [Celem.L, Celem.R]) e (SOME a) v

     else Skip (v, E))

  | appy (thy as (th,sr)) ptp E l (Const ("Script.While"(*2*),_) $ c $ e) a v =

    (if Rewrite.eval_true_ th sr (subst_atomic (Lucin.upd_env_opt E (a,v)) c)

     then appy thy ptp E (l @ [Celem.R]) e a v

     else Skip (v, E))

  | appy (thy as (th,sr)) ptp E l (Const ("If",_) $ c $ e1 $ e2) a v =

    (if Rewrite.eval_true_ th sr (subst_atomic (Lucin.upd_env_opt E (a,v)) c)

     then appy thy ptp E (l @ [Celem.L, Celem.R]) e1 a v

     else appy thy ptp E (l @ [Celem.R]) e2 a v)

  | appy thy ptp E l (Const ("Script.Repeat"(*1*),_) $ e $ a) _ v = 

    appy thy ptp E (l @ [Celem.L, Celem.R]) e (SOME a) v

  | appy thy ptp E l (Const ("Script.Repeat"(*2*),_) $ e) a v = appy thy ptp E (l @ [Celem.R]) e a v

  | appy thy ptp E l (Const ("Script.Try"(*2*),_) $ e $ a) _ v =

    (case appy thy ptp E (l @ [Celem.L, Celem.R]) e (SOME a) v of

      Napp E => (Skip (v, E))

    | ay => ay)

  | appy thy ptp E l(Const ("Script.Try"(*1*),_) $ e) a v =

    (case appy thy ptp E (l @ [Celem.R]) e a v of

      Napp E => (Skip (v, E))

    | ay => ay)

  | appy thy ptp E l (Const ("Script.Or"(*1*),_) $e1 $ e2 $ a) _ v =

    (case appy thy ptp E (l @ [Celem.L, Celem.L, Celem.R]) e1 (SOME a) v of

	    Appy lme => Appy lme

    | _ => appy thy ptp E (*LTool.env*) (l @ [Celem.L, Celem.R]) e2 (SOME a) v)

  | appy thy ptp E l (Const ("Script.Or"(*2*),_) $e1 $ e2) a v =

    (case appy thy ptp E (l @ [Celem.L, Celem.R]) e1 a v of

	    Appy lme => Appy lme

    | _ => appy thy ptp E (l @ [Celem.R]) e2 a v)

  | appy thy ptp E l (Const ("Script.Seq"(*2*),_) $ e1 $ e2 $ a) _ v =

    (case appy thy ptp E (l @ [Celem.L, Celem.L, Celem.R]) e1 (SOME a) v of

	    Skip (v,E) => appy thy ptp E (l @ [Celem.L, Celem.R]) e2 (SOME a) v

    | ay => ay)

  | appy thy ptp E l (Const ("Script.Seq"(*1*),_) $ e1 $ e2) a v =

    (case appy thy ptp E (l @ [Celem.L, Celem.R]) e1 a v of

	    Skip (v,E) => appy thy ptp E (l @ [Celem.R]) e2 a v

    | ay => ay)

  (* a leaf has been found *)   

  | appy ((th,sr)) (pt, p) E l t a v =

    case handle_leaf "next  " th sr E a v t of

	    (_, LTool.Expr s) => Skip (s, E)

    | (a', LTool.STac stac) =>

	    let val (m,m') = Lucin.stac2tac_ pt (Celem.assoc_thy th) stac

      in case m of

	      Tac.Subproblem _ => Appy (m', (E,l,a',Lucin.tac_2res m',Selem.Sundef,false))

	    | _ =>

        (case Applicable.applicable_in p pt m of

		       Chead.Appl m' => (Appy (m', (E,l,a',Lucin.tac_2res m',Selem.Sundef,false)))

		     | _ => Napp E)

	    end

fun nxt_up thy ptp (scr as (Rule.Prog sc)) E l ay (Const ("HOL.Let", _) $ _) a v = (*comes from let=...*)

    if ay = Napp_

    then nstep_up thy ptp scr E (drop_last l) Napp_ a v

    else (*Skip_*)

	    let

        val up = drop_last l

        val (i, T, body) =

          (case go up sc of

             Const ("HOL.Let",_) $ _ $ (Abs aa) => aa

           | t => error ("nxt_up..HOL.Let $ _ with " ^ Rule.term2str t))

        val i = TermC.mk_Free (i, T)

        val E = LTool.upd_env E (i, v)

      in

        case appy thy ptp E (up @ [Celem.R, Celem.D]) body a v  of

	        Appy lre => Appy lre

	      | Napp E => nstep_up thy ptp scr E up Napp_ a v

	      | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v

	    end

  | nxt_up thy ptp scr E l ay (Abs _) a v =  nstep_up thy ptp scr E l ay a v

  | nxt_up thy ptp scr E l ay (Const ("HOL.Let",_) $ _ $ (Abs _)) a v =

    nstep_up thy ptp scr E l ay a v

  (*no appy_: never causes Napp -> Helpless*)

  | nxt_up (thy as (th, sr)) ptp scr E l _ (Const ("Script.While"(*1*), _) $ c $ e $ _) a v = 

    if Rewrite.eval_true_ th sr (subst_atomic (Lucin.upd_env_opt E (a, v)) c) 

    then case appy thy ptp E (l @ [Celem.L, Celem.R]) e a v of

	     Appy lr => Appy lr

	  | Napp E => nstep_up thy ptp scr E l Skip_ a v

	  | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v

    else nstep_up thy ptp scr E l Skip_ a v

  (*no appy_: never causes Napp - Helpless*)

  | nxt_up (thy as (th, sr)) ptp scr E l _ (Const ("Script.While"(*2*), _) $ c $ e) a v = 

    if Rewrite.eval_true_ th sr (subst_atomic (Lucin.upd_env_opt E (a, v)) c) 

    then case appy thy ptp E (l @ [Celem.R]) e a v of

	    Appy lr => Appy lr

	  | Napp E => nstep_up thy ptp scr E l Skip_ a v

	  | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v

    else nstep_up thy ptp scr E l Skip_ a v

  | nxt_up thy ptp scr E l ay (Const ("If", _) $ _ $ _ $ _) a v = nstep_up thy ptp scr E l ay a v

  | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*)

      (Const ("Script.Repeat"(*1*), _) $ e $ _) a v =

    (case appy thy ptp (*upd_env*) E (*a,v)*) (l @ [Celem.L, Celem.R]) e a v  of

      Appy lr => Appy lr

    | Napp E =>  nstep_up thy ptp scr E l Skip_ a v

    | Skip (v,E) =>  nstep_up thy ptp scr E l Skip_ a v)

  | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*)

      (Const ("Script.Repeat"(*2*), _) $ e) a v =

    (case appy thy ptp (*upd_env*) E (*a,v)*) (l @ [Celem.R]) e a v  of

      Appy lr => Appy lr

    | Napp E => nstep_up thy ptp scr E l Skip_ a v

    | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v)

  | nxt_up thy ptp scr E l _ (Const ("Script.Try"(*2*),_) $ _ $ _) a v = (*makes Napp to Skip*)

    nstep_up thy ptp scr E l Skip_ a v

  | nxt_up thy ptp scr E l _ (Const ("Script.Try"(*1*), _) $ _) a v = (*makes Napp to Skip*)

    nstep_up thy ptp scr E l Skip_ a v

  | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ $ _ $ _) a v =

    nstep_up thy ptp scr E l ay a v

  | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ $ _) a v = nstep_up thy ptp scr E l ay a v

  | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ ) a v = 

    nstep_up thy ptp scr E (drop_last l) ay a v

  | nxt_up thy ptp scr E l ay (Const ("Script.Seq"(*1*),_) $ _ $ _ $ _) a v =

    (*all has been done in (*2*) below*) nstep_up thy ptp scr E l ay a v

  | nxt_up thy ptp scr E l ay (Const ("Script.Seq"(*2*),_) $ _ $ _) a v = (*comes from e2*)

    nstep_up thy ptp scr E l ay a v

  | nxt_up thy ptp (scr as Rule.Prog sc) E l ay (Const ("Script.Seq"(*3*),_) $ _) a v = (*comes from e1*)

    if ay = Napp_

    then nstep_up thy ptp scr E (drop_last l) Napp_ a v

    else (*Skip_*)

      let val up = drop_last l;

          val e2 =

            (case go up sc of

               Const ("Script.Seq"(*2*), _) $ _ $ e2 => e2

             | t => error ("nxt_up..Script.Seq $ _ with " ^ Rule.term2str t))

      in case appy thy ptp E (up @ [Celem.R]) e2 a v  of

        Appy lr => Appy lr

      | Napp E => nstep_up thy ptp scr E up Napp_ a v

      | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v end

  | nxt_up _ _ _ _ _ _ t _ _ = error ("nxt_up not impl for " ^ Rule.term2str t)

and nstep_up thy ptp (Rule.Prog sc) E l ay a v = 

    if 1 < length l

    then 

      let val up = drop_last l; 

      in (nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v ) end

    else (*interpreted to end*)

      if ay = Skip_ then Skip (v, E) else Napp E 

  | nstep_up _ _ _ _ l _ _ _ = error ("nstep_up: uncovered fun-def at " ^ Celem.loc_2str l)

(* decide for the next applicable stac in the script;

   returns (stactic, value) - the value in case the script is finished 

   12.8.02:         ~~~~~ and no assumptions ??? FIXME ???

   20.8.02: must return p in case of finished, because the next script

            consulted need not be the calling script:

            in case of detail ie. _inserted_ PrfObjs, the next stac

            has to searched in a script with PblObj.status<>Complete !

            (.. not true for other details ..PrfObj ??????????????????

   20.8.02: do NOT return safe (is only changed in locate !!!)

*)

fun next_tac (thy,_) _ (Rule.Rfuns {next_rule, ...}) (Selem.RrlsState(f, f', rss, _), ctxt) =

    if f = f'

    then (Tac.End_Detail' (f',[])(*8.6.03*), (Selem.Uistate, ctxt), 

    	(f', Selem.Sundef(*FIXME is no value of next_tac! vor 8.6.03*)))                (*finished*)

    else

      (case next_rule rss f of

    	  NONE => (Tac.Empty_Tac_, (Selem.Uistate, ctxt), (Rule.e_term, Selem.Sundef))       (*helpless*)

    	| SOME (Rule.Thm thm'')(*8.6.03: muss auch f' liefern ?!!*) => 

    	    (Tac.Rewrite' (thy, "e_rew_ord", Rule.e_rls, false, thm'', f, (Rule.e_term, [(*!?!8.6.03*)])),

  	         (Selem.Uistate, ctxt), (Rule.e_term, Selem.Sundef))                          (*next stac*)

      | _ => error "next_tac: uncovered case next_rule")

  | next_tac thy (ptp as (pt, (p, _))) (sc as Rule.Prog prog) 

	    (Selem.ScrState (E,l,a,v,s,_), ctxt) =

    (case if l = [] then appy thy ptp E [Celem.R] (LTool.body_of prog) NONE v

          else nstep_up thy ptp sc E l Skip_ a v of

       Skip (v, _) =>                                                                 (*finished*)

         (case par_pbl_det pt p of

	          (true, p', _) => 

	             let

	               val (_,pblID,_) = get_obj g_spec pt p';

	              in (Tac.Check_Postcond' (pblID, (v, [(*assigned in next step*)])), 

	                   (Selem.e_istate, ctxt), (v,s)) 

                end

	        | _ => (Tac.End_Detail' (Rule.e_term,[])(*8.6.03*), (Selem.e_istate, ctxt), (v,s)))

     | Napp _ => (Tac.Empty_Tac_, (Selem.e_istate, ctxt), (Rule.e_term, Selem.Sundef))     (*helpless*)

     | Appy (m', scrst as (_,_,_,v,_,_)) =>

         (m', (Selem.ScrState scrst, ctxt), (v, Selem.Sundef)))                      (*next stac*)

  | next_tac _ _ _ (is, _) = error ("next_tac: not impl for " ^ (Selem.istate2str is));

(* FIXME.WN050821 compare fun solve ... fun nxt_solv

   nxt_solv (Apply_Method'     vvv FIXME: get args in applicable_in *)

fun nxt_solv (Tac.Apply_Method' (mI, _, _, _)) _ (pt, pos as (p, _)) =

   let

     val {ppc, ...} = Specify.get_met mI;

     val (itms, oris, probl) = case get_obj I pt p of

       PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)

     | _ => error "nxt_solv Apply_Method': uncovered case get_obj"

     val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc

     val thy' = get_obj g_domID pt p;

     val thy = Celem.assoc_thy thy';

(*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*)

val itms =

  if mI = ["Biegelinien", "ausBelastung"]

  then itms @

    [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),

        [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),

      (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),

        [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),

    (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),

        [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),

      (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),

        [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]

  else itms

(*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)

     val (is, env, ctxt, scr) = case Lucin.init_scrstate thy itms mI of

       (is as Selem.ScrState (env,_,_,_,_,_), ctxt, scr) => (is, env, ctxt, scr)

     | _ => error "nxt_solv Apply_Method': uncovered case init_scrstate"

     val ini = Lucin.init_form thy scr env;

   in 

     case ini of

       SOME t =>

       let

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

	       val tac_ = Tac.Apply_Method' (mI, SOME t, is, ctxt);

	       val (pos, c, _, pt) = Generate.generate1 thy tac_ (is, ctxt) pos pt (* implicit Take *)

       in

        ([(Tac.Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos))

       end

     | NONE =>

       let

         val pt = update_env pt (fst pos) (SOME (is, ctxt))

	       val (tacis, c, ptp) = nxt_solve_ (pt, pos)

       in (tacis @ [(Tac.Apply_Method mI, Tac.Apply_Method' (mI, NONE, Selem.e_istate, ctxt), (pos, (is, ctxt)))],

	       c, ptp)

       end

    end

  | nxt_solv (Tac.Check_Postcond' (pI, _)) _ (pt, (p, p_))  =

    let

      val pp = par_pblobj pt p

      val asm = (case get_obj g_tac pt p of

		    Tac.Check_elementwise _ => (snd o (get_obj g_result pt)) p (*collects and instantiates asms*)

		  | _ => get_assumptions_ pt (p, p_))

	      handle _ => [] (*FIXME.WN030527 asms in subpbls not completely clear*)

      val metID = get_obj g_metID pt pp;

      val {srls = srls, scr = sc, ...} = Specify.get_met metID;

      val (loc, E, l, a, b, ctxt) = case get_loc pt (p, p_) of

        loc as (Selem.ScrState (E,l,a,_,_,b), ctxt) => (loc, E, l, a, b, ctxt)

      | _ => error "nxt_solv Check_Postcond': uncovered case get_loc"

      val thy' = get_obj g_domID pt pp;

      val thy = Celem.assoc_thy thy';

      val (_, _, (scval, scsaf)) = next_tac (thy', srls) (pt, (p, p_)) sc loc;

    in

      if pp = []

      then 

	      let

          val is = Selem.ScrState (E, l, a, scval, scsaf, b)

	        val tac_ = Tac.Check_Postcond'(pI,(scval, asm))

	        val ((p, p_), ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt) (pp, Res) pt;

	      in ([(Tac.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, (p, p_))) end

      else

        let (*resume script of parpbl, transfer value of subpbl-script*)

          val ppp = par_pblobj pt (lev_up p);

	        val thy' = get_obj g_domID pt ppp;

          val thy = Celem.assoc_thy thy';

          val (E, l, a, b, ctxt') = case get_loc pt (pp, Frm) of

            (Selem.ScrState (E,l,a,_,_,b), ctxt') => (E, l, a, b, ctxt')

          | _ => error "nxt_solv Check_Postcond' script of parpbl: uncovered case get_loc"

	        val ctxt'' = Stool.from_subpbl_to_caller ctxt scval ctxt'

          val tac_ = Tac.Check_Postcond' (pI, (scval, asm))

	        val is = Selem.ScrState (E,l,a,scval,scsaf,b)

          val ((p, p_), ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt'') (pp, Res) pt;

        in ([(Tac.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt'')))], ps, (pt, (p, p_))) end

    end

  | nxt_solv (Tac.End_Proof'') _ ptp = ([], [], ptp)

  | nxt_solv tac_ is (pt, pos) =

    let

      val pos = case pos of

 		   (p, Met) => ((lev_on o lev_dn) p, Frm) (* begin script        *)

 		  | (p, Res) => (lev_on p, Res)            (* somewhere in script *)

 		  | _ => pos

 	    val (pos', c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac") tac_ is pos pt;

    in

      ([(Lucin.tac_2tac tac_, tac_, (pos, is))], c, (pt, pos'))

    end

(* find the next tac from the script, nxt_solv will update the ctree *)

and nxt_solve_ (ptp as (pt, pos as (p, p_))) =

    if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p)

    then ([], [], (pt, (p, p_)))

    else 

      let 

        val thy' = get_obj g_domID pt (par_pblobj pt p);

	      val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;

	      val (tac_, is, (t, _)) = next_tac (thy', srls) (pt, pos) sc is;

	      (* TODO here  ^^^  return finished/helpless/ok !*)

	    in case tac_ of

		    Tac.End_Detail' _ => ([(Tac.End_Detail, Tac.End_Detail' (t, [(*FIXME.04*)]), (pos, is))], [], (pt, pos))

	    | _ => nxt_solv tac_ is ptp

      end;

(* compare inform with ctree.form at current pos by nrls;

   if found, embed the derivation generated during comparison

   if not, let the mat-engine compute the next ctree.form *)

(* code's structure is copied from complete_solve

   CAUTION: tacis in returned calcstate' do NOT construct resulting ptp --

            all_modspec etc. has to be inserted at Subproblem'*)

fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): Chead.calcstate') ifo =

  let

    val fo =

      case p_ of

        Ctree.Frm => Ctree.get_obj Ctree.g_form pt p

			| Ctree.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p

			| _ => Rule.e_term (*on PblObj is fo <> ifo*);

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

	  val {rew_ord, erls, rules, ...} = Rule.rep_rls nrls

	  val (found, der) = Inform.concat_deriv rew_ord erls rules fo ifo; (*<---------------*)

  in

    if found

    then

       let

         val tacis' = map (Inform.mk_tacis rew_ord erls) der;

		     val (c', ptp) = Generate.embed_deriv tacis' ptp;

	     in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end

     else 

	     if pos = ([], Ctree.Res) (*TODO: we should stop earlier with trying subproblems *)

	     then ("no derivation found", (tacis, c, ptp): Chead.calcstate') 

	     else

         let

           val cs' as (tacis, c', ptp) = nxt_solve_ ptp; (*<---------------------*)

		       val (tacis, c'', ptp) = case tacis of

			       ((Tac.Subproblem _, _, _)::_) => 

			         let

                 val ptp as (pt, (p,_)) = Chead.all_modspec ptp (*<--------------------*)

				         val mI = Ctree.get_obj Ctree.g_metID pt p

			         in

			           nxt_solv (Tac.Apply_Method' (mI, NONE, Selem.e_istate, Selem.e_ctxt)) (Selem.e_istate, Selem.e_ctxt) ptp

               end

			     | _ => cs';

		     in compare_step (tacis, c @ c' @ c'', ptp) ifo end

  end

end