(* Title:  solve an example by interpreting a method's script

    Author: Walther Neuper 1999

    (c) copyright due to lincense terms.

 *)

 signature SOLVE =

 sig

   datatype auto = CompleteCalc | CompleteCalcHead | CompleteModel | CompleteSubpbl 

   | CompleteToSubpbl | Step of int

   val autoord : auto -> int

   type tac'_

   val mk_tac'_ : Tac.tac -> string * Tac.tac

   val specsteps : string list

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

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

       Ctree.pos' list * Ctree.state

   val all_solve : auto -> Ctree.pos' list -> Ctree.state ->

     string * Ctree.pos' list * (Ctree.ctree * (int list * Ctree.pos_))

   val complete_solve :

      auto -> Ctree.pos' list -> Ctree.state -> string * Ctree.pos' list * Ctree.state

   val nxt_solv : Tac.tac_ -> Selem.istate * Proof.context -> Ctree.state -> Chead.calcstate'

   val solve : string * Tac.tac_ -> Ctree.state -> string * Chead.calcstate'

   val detailrls : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'

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

   val get_form : tac'_ -> Ctree.pos' -> Ctree.ctree -> Generate.mout

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

   (* NONE *)

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

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

   (* NONE *)

 end

 (**)

 structure Solve(**): SOLVE(**) =

 struct

 (**)

 open Ctree;

 type mstID = string;

 type tac'_ = mstID * Tac.tac; (*DG <-> ME*)

 fun mk_tac'_   m = case m of (* scr not cleaned -- will disappear eventually *)

   Tac.Init_Proof (ppc, spec)    => ("Init_Proof", Tac.Init_Proof (ppc, spec )) 

 | Tac.Model_Problem             => ("Model_Problem", Tac.Model_Problem)

 | Tac.Refine_Tacitly pblID      => ("Refine_Tacitly", Tac.Refine_Tacitly pblID)

 | Tac.Refine_Problem pblID      => ("Refine_Problem", Tac.Refine_Problem pblID)

 | Tac.Add_Given cterm'          => ("Add_Given", Tac.Add_Given cterm') 

 | Tac.Del_Given cterm'          => ("Del_Given", Tac.Del_Given cterm') 

 | Tac.Add_Find cterm'           => ("Add_Find", Tac.Add_Find cterm') 

 | Tac.Del_Find cterm'           => ("Del_Find", Tac.Del_Find cterm') 

 | Tac.Add_Relation cterm'       => ("Add_Relation", Tac.Add_Relation cterm') 

 | Tac.Del_Relation cterm'       => ("Del_Relation", Tac.Del_Relation cterm') 

 | Tac.Specify_Theory domID	    => ("Specify_Theory", Tac.Specify_Theory domID) 

 | Tac.Specify_Problem pblID     => ("Specify_Problem", Tac.Specify_Problem pblID)

 | Tac.Specify_Method metID	    => ("Specify_Method", Tac.Specify_Method metID) 

 | Tac.Apply_Method metID	    => ("Apply_Method", Tac.Apply_Method metID) 

 | Tac.Check_Postcond pblID	    => ("Check_Postcond", Tac.Check_Postcond pblID)

 | Tac.Free_Solve                => ("Free_Solve", Tac.Free_Solve)

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

 | Tac.Rewrite thm'		    => ("Rewrite", Tac.Rewrite thm') 

 | Tac.Rewrite_Asm thm'	    => ("Rewrite_Asm", Tac.Rewrite_Asm thm') 

 | Tac.Rewrite_Set_Inst (subs, rls')

                => ("Rewrite_Set_Inst", Tac.Rewrite_Set_Inst (subs, rls')) 

 | Tac.Rewrite_Set rls'          => ("Rewrite_Set", Tac.Rewrite_Set rls') 

 | Tac.End_Ruleset		    => ("End_Ruleset", Tac.End_Ruleset)

 | Tac.End_Detail                => ("End_Detail", Tac.End_Detail)

 | Tac.Detail_Set rls'           => ("Detail_Set", Tac.Detail_Set rls')

 | Tac.Detail_Set_Inst (s, rls') => ("Detail_Set_Inst", Tac.Detail_Set_Inst (s, rls'))

 | Tac.Calculate op_             => ("Calculate", Tac.Calculate op_)

 | Tac.Substitute sube           => ("Substitute", Tac.Substitute sube) 

 | Tac.Apply_Assumption cts'	    => ("Apply_Assumption", Tac.Apply_Assumption cts')

 | Tac.Take cterm'               => ("Take", Tac.Take cterm') 

 | Tac.Take_Inst cterm'          => ("Take_Inst", Tac.Take_Inst cterm') 

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

 (*

 | Tac.Subproblem_Full(spec,cts')=> ("Subproblem_Full", Tac.Subproblem_Full(spec,cts')) 

 *)

 | Tac.End_Subproblem            => ("End_Subproblem", Tac.End_Subproblem)

 | Tac.CAScmd cterm'		    => ("CAScmd", Tac.CAScmd cterm')

 | Tac.Split_And                 => ("Split_And", Tac.Split_And) 

 | Tac.Conclude_And		    => ("Conclude_And", Tac.Conclude_And) 

 | Tac.Split_Or                  => ("Split_Or", Tac.Split_Or) 

 | Tac.Conclude_Or		    => ("Conclude_Or", Tac.Conclude_Or) 

 | Tac.Begin_Trans               => ("Begin_Trans", Tac.Begin_Trans) 

 | Tac.End_Trans		    => ("End_Trans", Tac.End_Trans) 

 | Tac.Begin_Sequ                => ("Begin_Sequ", Tac.Begin_Sequ) 

 | Tac.End_Sequ                  => ("End_Sequ", Tac.Begin_Sequ) 

 | Tac.Split_Intersect           => ("Split_Intersect", Tac.Split_Intersect) 

 | Tac.End_Intersect		    => ("End_Intersect", Tac.End_Intersect) 

 | Tac.Check_elementwise cterm'  => ("Check_elementwise", Tac.Check_elementwise cterm')

 | Tac.Or_to_List                => ("Or_to_List", Tac.Or_to_List) 

 | Tac.Collect_Trues	            => ("Collect_Results", Tac.Collect_Trues) 

 | Tac.Empty_Tac               => ("Empty_Tac", Tac.Empty_Tac)

 | Tac.Tac string              => ("Tac", Tac.Tac string)

 | Tac.End_Proof'                => ("End_Proof'", Tac.End_Proof')

 | _ => error "mk_tac'_: uncovered case"; 

 type squ = ctree; (* TODO: safe etc. *)

 val specsteps = ["Init_Proof", "Refine_Tacitly", "Refine_Problem", "Model_Problem",

   "Add_Given", "Del_Given", "Add_Find", "Del_Find", "Add_Relation", "Del_Relation",

   "Specify_Theory", "Specify_Problem", "Specify_Method"];

 fun step2taci ((tac_, _, pt, p, _) : Lucin.step) = (*FIXXME.040312: redesign step*)

     (Lucin.tac_2tac tac_, tac_, (p, Ctree.get_loc pt p)): Generate.taci;

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

 fun solve ("Apply_Method", m as Tac.Apply_Method' (mI, _, _, _)) (pt, (pos as (p, _))) =

     let val {srls, ...} = Specify.get_met mI;

       val itms = case get_obj I pt p of

         PblObj {meth=itms, ...} => itms

       | _ => error "solve Apply_Method: uncovered case get_obj"

       val thy' = get_obj g_domID pt p;

       val thy = Celem.assoc_thy thy';

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

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

       | _ => error "solve Apply_Method: uncovered case init_scrstate"

       val ini = Lucin.init_form thy sc env;

       val p = lev_dn p;

     in 

       case ini of

 	      SOME t =>

           let val (pos,c,_, pt) = 

 		        Generate.generate1 thy (Tac.Apply_Method' (mI, SOME t, is, ctxt))

 		        (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;

 	        in ("ok",([(Tac.Apply_Method mI, Tac.Apply_Method' (mI, SOME t, is, ctxt), 

 		        ((lev_on p, Frm), (is, ctxt)))], c, (pt, pos))) 

 	        end	      

 	    | NONE => (*execute the first tac in the Script, compare solve m*)

 	        let

             val (m', (is', ctxt'), _) = Lucin.next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);

 	          val d = Celem.e_rls (*FIXME: get simplifier from domID*);

 	        in 

 	          case Lucin.locate_gen (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') of 

 		          Lucin.Steps (_, ss as (_, _, pt', p', c') :: _) =>

 		            ("ok", (map step2taci ss, c', (pt', p')))

 		        | _ => (* NotLocatable *)

 		            let val (p, ps, _, pt) = Generate.generate_hard (Celem.assoc_thy "Isac") m (p, Frm) pt;

 		            in 

 		              ("not-found-in-script",([(Lucin.tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt, p))) 

 		            end

 	        end

     end

   | solve ("Free_Solve", Tac.Free_Solve')  (pt, po as (p, _)) =

     let

       val p' = lev_dn_ (p, Res);

       val pt = update_metID pt (par_pblobj pt p) Celem.e_metID;

     in

       ("ok", ([(Tac.Empty_Tac, Tac.Empty_Tac_, (po, (Selem.Uistate, Selem.e_ctxt)))], [], (pt,p')))

     end

   | solve ("Check_Postcond", 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 _ => (*collects and instantiates asms*)

 		         (snd o (get_obj g_result pt)) p

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

 	      handle _ => [] (*WN.27.5.03 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 "solve Check_Postcond: uncovered case get_loc"

       val thy' = get_obj g_domID pt pp;

       val thy = Celem.assoc_thy thy';

       val (_, _, (scval, scsaf)) = Lucin.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 (pos, ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt) (pp, Res) pt;

 	      in ("ok", ([(Tac.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, pos))) 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 "solve Check_Postcond resume script of parpbl: uncovered case get_loc"

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

           val ((p, p_), ps, _, pt) = Generate.generate1 thy (Tac.Check_Postcond' (pI, (scval, asm)))

 		        (Selem.ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt;

        in ("ok", ([(Tac.Check_Postcond pI, Tac.Check_Postcond'(pI, (scval, asm)),

   	      ((pp, Res), (Selem.ScrState (E, l, a, scval, scsaf, b), ctxt'')))], ps, (pt, (p, p_)))) end

      end

   | solve (_, Tac.End_Proof'') (pt, (p, p_)) =

     ("end-proof", ([(Tac.Empty_Tac, Tac.Empty_Tac_, (([], Res), (Selem.Uistate, Selem.e_ctxt)))], [], (pt, (p, p_))))

   | solve (_, Tac.End_Detail' t) (pt, (p, p_)) = (* could be done by generate1 ?!? *)

     let (*Rewrite_Set* done at Detail_Set*: this result is already in ctree*)

       val pr = (lev_up p, Res)

     in

       ("ok", ([(Tac.End_Detail, Tac.End_Detail' t , ((p, p_), get_loc pt (p, p_)))], [], (pt, pr)))

     end

   | solve (_, m) (pt, po as (p, p_)) =

     if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*29.8.02: could be detail, too !!*)

     then

       let

         val ctxt = get_ctxt pt po

         val ((p,p_),ps,_,pt) = Generate.generate1 (Celem.assoc_thy (get_obj g_domID pt (par_pblobj pt p))) 

 		      m (Selem.e_istate, ctxt) (p, p_) pt;

 	    in ("no-method-specified", (*Free_Solve*)

 	      ([(Tac.Empty_Tac, Tac.Empty_Tac_, ((p, p_), (Selem.Uistate, ctxt)))], ps, (pt, (p, p_))))

       end

     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 d = Celem.e_rls; (*FIXME.WN0108: canon.simplifier for domain is missing: generate from domID?*)

 	    in

         case Lucin.locate_gen (thy',srls) m  (pt,(p, p_)) (sc,d) is of 

 	        Lucin.Steps (_, ss as (_, _, pt', p', c') :: _) =>

 	          ("ok", (map step2taci ss, c', (pt', p')))

             (*27.8.02:next_tac may change to other branches in pt FIXXXXME*)

 	      | _ => (* NotLocatable *)

 	        let 

 	          val (p,ps, _, pt) = Generate.generate_hard (Celem.assoc_thy "Isac") m (p, p_) pt;

 	        in

 	          ("not-found-in-script", ([(Lucin.tac_2tac m, m, (po, is))], ps, (pt, p)))

           end

 	    end;

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

      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)) = Lucin.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, _)) = Lucin.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;

 (* says how may steps of a calculation should be done by "fun autocalc"

    FIXXXME040624: does NOT match interfaces/ITOCalc.java

    TODO.WN0512 redesign togehter with autocalc ?                     *)

 datatype auto = 

   Step of int      (*1 do #int steps (may stop in model/specify)

                        IS VERY INEFFICIENT IN MODEL/SPECIY                    *)

 | CompleteModel    (*2 complete modeling

                        if model complete, finish specifying                   *)

 | CompleteCalcHead (*3 complete model/specify in one go                       *)

 | CompleteToSubpbl (*4 stop at the next begin of a subproblem,

                        if none, complete the actual (sub)problem              *)

 | CompleteSubpbl   (*5 complete the actual (sub)problem (incl.ev.subproblems) *)

 | CompleteCalc;    (*6 complete the calculation as a whole                    *)

 fun autoord (Step _ ) = 1

   | autoord CompleteModel = 2

   | autoord CompleteCalcHead = 3

   | autoord CompleteToSubpbl = 4

   | autoord CompleteSubpbl = 5

   | autoord CompleteCalc = 6;

 fun complete_solve auto c (ptp as (_, p as (_, p_))) =

     if p = ([], Res)

     then ("end-of-calculation", [], ptp)

     else

       if member op = [Pbl,Met] p_

       then

         let

           val ptp = Chead.all_modspec ptp

 	        val (_, c', ptp) = all_solve auto c ptp

 	      in complete_solve auto (c @ c') ptp end

       else

         case nxt_solve_ ptp of

 	        ((Tac.Subproblem _, _, _) :: _, c', ptp') =>

 	          if autoord auto < 5

             then ("ok", c @ c', ptp)

 	          else

               let

                 val ptp = Chead.all_modspec ptp'

 	             val (_, c'', ptp) = all_solve auto (c @ c') ptp

 	           in complete_solve auto (c @ c'@ c'') ptp end

 	      | ((Tac.Check_Postcond _, _, _) :: _, c', ptp' as (_, p')) =>

 	        if autoord auto < 6 orelse p' = ([], Res)

           then ("ok", c @ c', ptp')

 	        else complete_solve auto (c @ c') ptp'

 	      | ((Tac.End_Detail, _, _) :: _, c', ptp') => 

 	        if autoord auto < 6

           then ("ok", c @ c', ptp')

 	        else complete_solve auto (c @ c') ptp'

 	      | (_, c', ptp') => complete_solve auto (c @ c') ptp'

 and all_solve auto c (ptp as (pt, pos as (p,_)): ctree * pos') = 

     let

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

       val ctxt = get_ctxt pt pos

       val (_, c', ptp) = nxt_solv (Tac.Apply_Method' (mI, NONE, Selem.e_istate, ctxt)) (Selem.e_istate, ctxt) ptp

     in

       complete_solve auto (c @ c') ptp

     end;

 (* aux.fun for detailrls with Rrls, reverse rewriting *)

 fun rul_terms_2nds _ nds _ [] = nds

   | rul_terms_2nds thy nds t ((rule, res as (t', _)) :: rts) =

     (append_atomic [] (Selem.e_istate, Selem.e_ctxt) t (Tac.rule2tac thy [] rule) res Complete EmptyPtree) ::

       (rul_terms_2nds thy nds t' rts);

 (* detail steps done internally by Rewrite_Set* into ctree by use of a script *)

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

   let

     val t = get_obj g_form pt p

 	  val tac = get_obj g_tac pt p

 	  val rls = (assoc_rls o Tac.rls_of) tac

     val ctxt = get_ctxt pt pos

   in

     case rls of

 	    Celem.Rrls {scr = Celem.Rfuns {init_state,...},...} => 

 	    let

         val (_, _, _, rul_terms) = init_state t

 	      val newnds = rul_terms_2nds (Proof_Context.theory_of ctxt) [] t rul_terms

 	      val pt''' = ins_chn newnds pt p 

 	    in ("detailrls", pt''', (p @ [length newnds], Res)) end

 	  | _ =>

 	    let

         val is = Generate.init_istate tac t

 	      (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]

 			    is wrong for simpl, but working ?!? *)

 	      val tac_ = Tac.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)

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

 	      val thy = Celem.assoc_thy "Isac"

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

 	      val (_,_, (pt'', _)) = complete_solve CompleteSubpbl [] (pt', pos')

 	      val newnds = children (get_nd pt'' p)

 	      val pt''' = ins_chn newnds pt p (*complete_solve cuts branches after*)

 	    in ("detailrls", pt''', (p @ [length newnds], Res):pos') end

   end;

 fun get_form (mI, m) (p,p_) pt = 

   case Applicable.applicable_in (p, p_) pt m of

     Chead.Notappl e => Generate.Error' e

   | Chead.Appl m => 

       if member op = specsteps mI

       then

         let val (_, _, f, _, _, _) = Chead.specify m (p, p_) [] pt

         in f end

       else Generate.EmptyMout;

 end