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

    (c) Walther Neuper 1999

 use"ME/solve.sml";

 use"solve.sml";

 *)

 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)

 | User                      => ("User",User)

 | 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 = ptree; (* TODO: safe etc. *)

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

 type ctr = (loc * pos) list;

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

 	   ("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 => raise error ("op_intern: no op= "^op_);

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

 (* use"ME/solve.sml";

    use"solve.sml";

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

 val ttt = (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, _):step) = (*FIXXME.040312: redesign step*)

     (tac_2tac tac_, tac_, (p, get_istate pt p)):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:ptree, (pos as (p,_))) =

   let val {srls,...} = 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,_,_,_,_,_), sc) = init_scrstate thy itms mI;

     val ini = init_form thy sc env;

     val p = lev_dn p;

   in 

       case ini of

 	  SOME t => (* val SOME t = ini; 

 	             *)

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

 		  generate1 thy (Apply_Method' (mI, SOME t, is))

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

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

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

 	  end	      

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

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

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

 	  in 

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

 		  Steps (is'', ss as (m'',f',pt',p',c')::_) =>

 (* val Steps (is'', ss as (m'',f',pt',p',c')::_) =

        locate_gen (thy',srls) m'  (pt,(p,Res)) (sc,d) is';

  *)

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

 		| NotLocatable =>  

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

 			  generate_hard (assoc_thy "Isac.thy") m (p,Frm) pt;

 		  in ("not-found-in-script",

 		      ([(tac_2tac m, m, (pos, is))], ps, (pt,p))) end

     (*just-before------------------------------------------------------

 	      ("ok",([(Apply_Method mI,Apply_Method'(mI,NONE,e_istate),

 		       (pos, is))],

 		     [], (update_env pt (fst pos) (SOME is),pos)))

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

 	  end

   end

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

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

     val p' = lev_dn_ (p,Res);

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

   in ("ok", ((*(p',Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Unsafe,*)

       [(Empty_Tac, Empty_Tac_, (po, Uistate))], [], (pt,p'))) end

 (* val (("Check_Postcond",Check_Postcond' (pI,_)), (pt,(pos as (p,p_)))) =

        (  m,                                       (pt, pos));

    *)

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

     let (*val _=writeln"###solve Check_Postcond";*)

       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

 		  | _ => ((map fst) o (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,...} = get_met metID;

       val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_); 

      (*val _= writeln("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));

       val _= writeln("### solve Check_postc, is= "^(istate2str is));*)

       val thy' = get_obj g_domID pt pp;

       val thy = assoc_thy thy';

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

       (*val _= writeln("### solve Check_postc, scval= "^(term2str scval));*)

     in if pp = [] then

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

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

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

 	   in ("ok", ((*(([],Res),is,End_Proof''), f, End_Proof', scsaf,*)

 	       [(Check_Postcond pI, tac_, ((pp,Res),is))], 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 get_met) metID;

         val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm); 

      (*val _=writeln("### solve Check_postc, parpbl pos= "^(pos'2str(pp,Frm)));

   	val _=writeln("### solve Check_postc, is(pt)= "^(istate2str is));

   	val _=writeln("### solve Check_postc, is'= "^

 		      (istate2str (E,l,a,scval,scsaf,b)));*)

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

 	    generate1 thy (Check_Postcond' (pI, (scval, map term2str asm)))

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

 	(*val _=writeln("### solve Check_postc, is(pt')= "^

 		      (istate2str (get_istate pt ([3],Res))));

 	val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) sc 

 				(ScrState (E,l,a,scval,scsaf,b));*)

        in ("ok",(*((pp,Res),is',nx), f, tac_2tac nx, scsaf,*)

 	   ([(Check_Postcond pI, Check_Postcond'(pI,(scval, map term2str asm)),

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

 	end

     end

 (* val (msg, cs') = 

     ("ok",([(Check_Postcond pI,Check_Postcond'(pI, (scval, map term2str asm))),

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

     val (_,(pt',p')) = cs';

    (writeln o istate2str) (get_istate pt' p');

    (term2str o fst) (get_obj g_result pt' (fst p'));

    *)

 (* writeln(istate2str(get_istate pt (p,p_)));

    *)

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

       ("end-proof",

        ((*(([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe,*)

        [(Empty_Tac,Empty_Tac_,(([],Res),Uistate))],[],(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 ptree*)

 	val thy' = get_obj g_domID pt pp

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

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

     in ("ok", ((*((pp,Frm(*???*)),is,tac_), 

 	Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)),

 	tac_2tac tac_, Sundef,*)

 	[(End_Detail, End_Detail' t , 

 	  ((p,p_), get_istate pt (p,p_)))], [], (pt,pr))) end

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

 (* val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));

    *)

     if e_metID = get_obj g_metID pt (par_pblobj pt p)(*29.8.02:

 						      could be detail, too !!*)

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

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

 			   m e_istate (p,p_) pt;

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

 	     ((*((p,p_),Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*)

 	     [(Empty_Tac,Empty_Tac_, ((p,p_),Uistate))], ps, (pt,(p,p_)))) end

     else

 	let 

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

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

 (*val _= writeln("### solve, before locate_gen p="^(pos'2str(p,p_)));*)

 		val d = e_rls; (*FIXME: canon.simplifier for domain is missing

 				8.01: generate from domID?*)

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

 	       Steps (is', ss as (m',f',pt',p',c')::_) =>

 (* val Steps (is', ss as (m',f',pt',p',c')::_) =

        locate_gen (thy',srls) m  (pt,(p,p_)) (sc,d) is;

  *)

 	       let (*val _= writeln("### solve, after locate_gen: is= ")

 		       val _= writeln(istate2str is')*)

 		   (*val nxt_ = 

 		       case p' of (*change from solve to model subpbl*)

 			   (_,Pbl) => nxt_model_pbl m' (pt',p')

 			 | _ => fst3 (next_tac (thy',srls) (pt',p') sc is');*) 

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

 	       in ("ok", ((*(p',is',nxt_), f', tac_2tac nxt_, safe is',*)

 		   map step2taci ss, c', (pt',p'))) end

 	     | NotLocatable =>  

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

 		       generate_hard (assoc_thy "Isac.thy") m (p,p_) pt;

 	       in ("not-found-in-script",

 		   ((*(p,Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*) 

 		   [(tac_2tac m, m, (po,is))], ps, (pt,p))) end

 	end;

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

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

 fun nxt_solv (Apply_Method' (mI,_,_)) _ (pt:ptree, pos as (p,_)) =

 (* val ((Apply_Method' (mI,_,_)),             _,    (pt:ptree, pos as (p,_))) =

        ((Apply_Method' (mI, NONE, e_istate)), e_istate, ptp);

    *)

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

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

     val itms = if itms <> [] then itms

 	       else complete_metitms oris probl [] ppc

     val thy' = get_obj g_domID pt p;

     val thy = assoc_thy thy';

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

     val ini = init_form thy scr env;

   in 

     case ini of

     SOME t => (* val SOME t = ini; 

 	         *)

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

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

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

 	    generate1 thy tac_ is pos pt

       (*val _= ("### nxt_solv Apply_Method, pos= "^pos'2str (lev_on p,Frm));*)

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

   | NONE =>

     let val pt = update_env pt (fst pos) (SOME is)

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

     in (tacis @ 

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

 	c, ptp) end

   end

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

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

        (tac_,                  is,  ptp);

    *)

   (*TODO.WN050913 remove unnecessary code below*)

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

     let (*val _=writeln"###solve Check_Postcond";*)

       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

 		  | _ => ((map fst) o (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,...} = get_met metID;

       val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_); 

      (*val _= writeln("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));

       val _= writeln("### solve Check_postc, is= "^(istate2str is));*)

       val thy' = get_obj g_domID pt pp;

       val thy = assoc_thy thy';

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

       (*val _= writeln("### solve Check_postc, scval= "^(term2str scval));*)

     in if pp = [] then 

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

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

            (*val _= writeln"### nxt_solv2 Apply_Method: stored is =";

                val _= writeln(istate2str is);*)

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

 		   generate1 thy tac_ is (pp,Res) pt;

 	   in ([(Check_Postcond pI, tac_, ((pp,Res), is))],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,...} = get_met metID;

         val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm)

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

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

     (*val _= writeln"### nxt_solv3 Apply_Method: stored is =";

         val _= writeln(istate2str is);*)

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

 	(*val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) scr is;WN050913*)

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

     end

 (* writeln(istate2str(get_istate pt (p,p_)));

    *)

 (*.start interpreter and do one rewrite.*)

 (* val (_,Detail_Set'(thy',rls,t)) = (mI,m); val p = (p,p_);

    solve ("",Detail_Set'(thy', rls, t)) p pt;

   | nxt_solv (Detail_Set'(thy', rls, t)) _ (pt, p) = **********

 ---> Frontend/sml.sml

   | nxt_solv (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 ptree*)

 	val thy' = get_obj g_domID pt pp

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

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

     in (pr, ((pp,Frm(*???*)),is,tac_), 

 	Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)),

 	tac_2tac tac_, Sundef, pt) end

 *)

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

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

 (* val (pt, pos as (p,p_)) = ptp;

    *)

     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  (*somewhere in script*)

     (*val _= writeln"### nxt_solv4 Apply_Method: stored is =";

         val _= writeln(istate2str is);*)

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

     in ([(tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end

   (*(p,p_), (([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe, pt*)

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

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

    val (ptp as (pt, pos as (p,p_))) = ptp'';

    val (ptp as (pt, pos as (p,p_))) = ptp;

    val (ptp as (pt, pos as (p,p_))) = (pt,ip);

    val (ptp as (pt, pos as (p,p_))) = (pt, pos);

    *)

 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_))):calcstate'

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

 	     val (srls, is, sc) = 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 !*)

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

 	    *)

 	 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".*)

 (*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 + start solving*)

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

 | 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;

 (* val (auto, c, (ptp as (_, p))) = (auto, (c@c'), ptp);

    *)

 fun complete_solve auto c (ptp as (_, p): ptree * pos') =

     if p = ([], Res) then ("end-of-calculation", [], ptp) else

     case nxt_solve_ ptp of

 	((Subproblem _, tac_, (_, is))::_, c', ptp') =>

 (* val ptp' = ptp''';

    *)

 	if autoord auto < 5 then ("ok", c@c', ptp)

 	else let val ptp = 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'

 (* val (tacis, c', ptp') = nxt_solve_ ptp;

    val (tacis, c', ptp'') = nxt_solve_ ptp';

    val (tacis, c', ptp''') = nxt_solve_ ptp'';

    val (tacis, c', ptp'''') = nxt_solve_ ptp''';

    val (tacis, c', ptp''''') = nxt_solve_ ptp'''';

    *)

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

 (* val (ptp as (pt, (p,_))) = ptp;

    val (ptp as (pt, (p,_))) = ptp';

    val (ptp as (pt, (p,_))) = (pt, pos);

    *)

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

         val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate))

 				e_istate ptp;

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

 (*@@@ vvv @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)

 fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') =

     if p = ([], Res) then ("end-of-calculation", [], ptp) else

     if member op = [Pbl,Met] p_

     then let val ptp = 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 = 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, (p,_)): ptree * pos') = 

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

         val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate))

 				    e_istate ptp

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

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

 (* val (nds, t, ((rule, (t', asm)) :: rts)) = ([], t, rul_terms);

    *)

 fun rul_terms_2nds nds t [] = nds

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

     (append_atomic [] e_istate t (rule2tac [] rule) res Complete EmptyPtree) ::

     (rul_terms_2nds nds t' rts);

 (*. detail steps done internally by Rewrite_Set* 

     into ctree by use of a script .*)

 (* val (pt, (p,p_)) = (pt, pos);

    *)

 fun detailrls pt ((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

     in case rls of

 (* val Rrls {scr = Rfuns {init_state,...},...} = rls;

    *)

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

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

 	       val newnds = rul_terms_2nds [] t rul_terms

 	       val pt''' = ins_chn newnds pt p 

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

 	 | _ =>

 	   let val is = 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)

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

 	       val thy = assoc_thy "Isac.thy"

 	       val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ is 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'''(*, get_formress [] ((lev_on o lev_dn) p)cn*),

 	       (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_in (p,p_) pt m of

     Notappl e => Error' (Error_ e)

   | Appl m => 

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

          *)

       if member op = specsteps mI

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

 	     in f end

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

 	   in (*f*) EmptyMout end;