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

   Author: Walther Neuper 1999

   (c) copyright due to lincense terms.

1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890

        10        20        30        40        50        60        70        80         90      100

*)

structure Solve =

struct

open Ctree;

fun safe (ScrState (_,_,_,_,s,_)) = s

  | safe (RrlsState _) = Safe;

type mstID = string;

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

val e_tac'_ = ("Empty_Tac", Empty_Tac):tac'_;

fun mk_tac'_   m = case m of

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

| Model_Problem             => ("Model_Problem", Model_Problem)

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

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

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

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

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

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

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

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

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

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

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

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

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

| Free_Solve                => ("Free_Solve",Free_Solve)

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

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

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

| Rewrite_Set_Inst (subs, rls')

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

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

| End_Ruleset		    => ("End_Ruleset", End_Ruleset)

| End_Detail                => ("End_Detail", End_Detail)

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

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

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

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

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

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

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

| Group (con, ints) 	    => ("Group", Group (con, ints)) 

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

(*

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

*)

| End_Subproblem            => ("End_Subproblem",End_Subproblem)

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

| Split_And                 => ("Split_And", Split_And) 

| Conclude_And		    => ("Conclude_And", Conclude_And) 

| Split_Or                  => ("Split_Or", Split_Or) 

| Conclude_Or		    => ("Conclude_Or", Conclude_Or) 

| Begin_Trans               => ("Begin_Trans", Begin_Trans) 

| End_Trans		    => ("End_Trans", End_Trans) 

| Begin_Sequ                => ("Begin_Sequ", Begin_Sequ) 

| End_Sequ                  => ("End_Sequ", Begin_Sequ) 

| Split_Intersect           => ("Split_Intersect", Split_Intersect) 

| End_Intersect		    => ("End_Intersect", End_Intersect) 

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

| Or_to_List                => ("Or_to_List", Or_to_List) 

| Collect_Trues	            => ("Collect_Results", Collect_Trues) 

| Empty_Tac               => ("Empty_Tac",Empty_Tac)

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

| End_Proof'                => ("End_Proof'",End_Proof'); 

(*Detail*)

val empty_tac'_ = (mk_tac'_ Empty_Tac):tac'_;

fun mk_tac ((_,m):tac'_) = m; 

fun mk_mstID ((mI,_):tac'_) = mI;

fun tac'_2str ((ID,ms):tac'_) = ID ^ (tac2str ms);

(* TODO: tac2str, tac'_2str NOT tested *)

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

(*13.9.02--------------

type ctr = (loc * pos) list;

val ops = [("PLUS","Groups.plus_class.plus"),("MINUS","Groups.minus_class.minus"),("TIMES","Groups.times_class.times"),

	   ("cancel","cancel"),("pow","pow"),("sqrt","sqrt")];

ML {* 

@{term "PLUS"};   (*Free ("PLUS", "'a") : term*)

@{term "plus"};   (*Const ("Groups.plus_class.plus", "'a => 'a => 'a")*)

@{term "MINUS"};  (*Free ("MINUS", "'a")*)

@{term "minus"};  (*Const ("Groups.minus_class.minus", "'a => 'a => 'a")*)

@{term "TIMES"};  (*Free ("TIMES", "'a")*)

@{term "times"};  (*Const ("Groups.times_class.times", "'a => 'a => 'a")*)

@{term "CANCEL"}; (*Free ("CANCEL", "'a")*)

@{term "cancel"}; (*Free ("cancel", "'a")*)

@{term "POWER"};  (*Free ("POWER", "'a")*)

@{term "pow"};    (*Free ("pow", "'a")*)

@{term "SQRT"};   (*Free ("SQRT", "'a")*)

@{term "sqrt"};   (*Const ("NthRoot.sqrt", "RealDef.real => RealDef.real")*)

*}

fun op_intern op_ =

  case assoc (ops, op_) of

    SOME op' => op' | NONE => error ("op_intern: no op= "^op_);

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

(* use"ME/solve.sml";

   use"solve.sml";

val ttt = (Thm.term_of o the o (parse thy))"Substitute [(bdv,x)] g";

val ttt = (Thm.term_of o the o (parse thy))"Rewrite thmid True g";

  Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thm',_) $ Const (pa,_) $ f'

   *)

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

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

(* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m);

   val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos);

   *)

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

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

        val PblObj {meth=itms, ...} = get_obj I pt p;

        val thy' = get_obj g_domID pt p;

        val thy = assoc_thy thy';

        val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = Lucin.init_scrstate thy itms mI;

        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 (Apply_Method' (mI, SOME t, is, ctxt))

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

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

		          ((lev_on p, Frm), (is, ctxt)))], c, (pt, pos)) : Chead.calcstate') 

	          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 = 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 (is'', ss as (m'',f',pt',p',c')::_) =>

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

		          | NotLocatable =>  

		              let val (p,ps,f,pt) = Generate.generate_hard (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", Free_Solve')  (pt,po as (p,_)) =

      let (*val _=tracing"###solve Free_Solve";*)

        val p' = lev_dn_ (p,Res);

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

      in ("ok", ([(Empty_Tac, Empty_Tac_, (po, (Uistate, e_ctxt)))], [], (pt,p')))

      end

  | solve ("Check_Postcond", Check_Postcond' (pI,_)) (pt,(pos as (p,p_))) =

      let

        val pp = par_pblobj pt p

        val asm = 

          (case get_obj g_tac pt p of

		         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 as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_); 

        val thy' = get_obj g_domID pt pp;

        val thy = assoc_thy thy';

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

      in 

        if pp = [] 

        then

	        let 

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

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

	          val (pos,ps,f,pt) = Generate.generate1 thy tac_ (is, ctxt) (pp,Res) pt;

	        in ("ok", ([(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 = assoc_thy thy';

	          val metID = get_obj g_metID pt ppp;

            val sc = (#scr o Specify.get_met) metID;

            val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm); 

	          val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'

            val ((p,p_),ps,f,pt) = 

	            Generate.generate1 thy (Check_Postcond' (pI, (scval, asm)))

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

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

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

	     end

     end

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

      ("end-proof",

       ([(Empty_Tac,Empty_Tac_,(([],Res),(Uistate, e_ctxt)))],[],(pt,(p,p_))))

(*-----------vvvvvvvvvvv could be done by generate1 ?!?*)

  | solve (_,End_Detail' t) (pt, (p,p_)) =

      let

        val pr as (p',_) = (lev_up p, Res)

	      val pp = par_pblobj pt p

	      val r = (fst o (get_obj g_result pt)) p' 

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

	      val thy' = get_obj g_domID pt pp

	      val (srls, is, sc) = Lucin.from_pblobj' thy' pr pt

	      val (tac_,is',_) = Lucin.next_tac (thy',srls) (pt,pr) sc is

      in ("ok", ([(End_Detail, End_Detail' t , 

	      ((p,p_), get_loc pt (p,p_)))], [], (pt,pr)))

      end

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

      if 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,f,pt) = 

		        Generate.generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) 

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

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

	        ([(Empty_Tac,Empty_Tac_, ((p,p_),(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 = 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 (is', ss as (m',f',pt',p',c')::_) =>

	            let 

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

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

	        | NotLocatable =>  

	            let val (p,ps,f,pt) = 

		            Generate.generate_hard (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 (Apply_Method' (mI,_,_,_)) _ (pt:ctree, pos as (p,_)) =

      let

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

        val PblObj{meth=itms,origin=(oris,_,_),probl, ...} = get_obj I pt p;

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

        val thy' = get_obj g_domID pt p;

        val thy = assoc_thy thy';

        val (is as ScrState (env,_,_,_,_,_), ctxt, scr) = Lucin.init_scrstate thy itms mI;

        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_ = Apply_Method' (mI, SOME t, is, ctxt);

	            val (pos,c,_,pt) = (*implicit Take*)

	              Generate.generate1 thy tac_ (is, ctxt) pos pt

            in ([(Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)) : Chead.calcstate' end

        | NONE =>

            let

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

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

            in (tacis @ 

	              [(Apply_Method mI, Apply_Method' (mI, NONE, e_istate, ctxt), (pos, (is, ctxt)))],

	             c, ptp)

            end

      end

    (*TODO.WN050913 remove unnecessary code below*)

  | nxt_solv (Check_Postcond' (pI,_)) _ (pt, pos as (p,p_))  =

      let

        val pp = par_pblobj pt p

        val asm =

          (case get_obj g_tac pt p of

		         Check_elementwise _ => (*collects and instantiates asms*)

		           (snd o (get_obj g_result pt)) p

		       | _ => 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 as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_); 

        val thy' = get_obj g_domID pt pp;

        val thy = assoc_thy thy';

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

      in

        if pp = []

        then 

	        let

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

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

	          val ((p,p_),ps,f,pt) = 

		          Generate.generate1 thy tac_ (is, ctxt) (pp,Res) pt;

	        in ([(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 = assoc_thy thy';

	          val metID = get_obj g_metID pt ppp;

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

            val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)

	          val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'

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

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

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

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

      end

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

  | nxt_solv tac_ is (pt, pos as (p,p_)) =

      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 (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 e_metID = get_obj g_metID pt (par_pblobj pt p)

      then ([], [], (pt, (p, p_))) : Chead.calcstate'

      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

		         End_Detail' _ => ([(End_Detail, End_Detail' (t,[(*FIXME.040215*)]), 

				       (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_)): ctree * pos') =

  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

	      ((Subproblem _, tac_, (_, is))::_, 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

	    | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) =>

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

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

	        else complete_solve auto (c @ c') ptp'

	    | ((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 (Apply_Method' (mI, NONE, e_istate, ctxt)) (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 t [] = nds

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

    (append_atomic [] (e_istate, e_ctxt) t (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,p_):pos') = 

  let

    val t = get_obj g_form pt p

	  val tac = get_obj g_tac pt p

	  val rls = (assoc_rls o rls_of) tac

    val ctxt = get_ctxt pt pos

  in

    case rls of

	    Rrls {scr = 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):pos') 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_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)

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

	        val thy = assoc_thy "Isac"

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

	        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;

(* val(mI,m)=m;val ppp=p;(*!!!*)val(p,p_)=pos;val(_,pt,_)=ppp(*!!!*);

   get_form ((mI,m):tac'_) ((p,p_):pos') ppp;

   *)

fun get_form ((mI,m):tac'_) ((p,p_):pos') pt = 

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

    Chead.Notappl e => Generate.Error' e

  | Chead.Appl m => 

      (* val Appl m=applicable_in (p,p_) pt m;

         *)

      if member op = specsteps mI

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

	     in f end

      else let val (*_,_,f,_,_,_*)_ = solve (mI,m) (pt,(p,p_))

	   in (*f*) Generate.EmptyMout end;

end