(* use"../ME/solve.sml";

   use"ME/solve.sml";

   use"solve.sml";

   W.N.10.12.99

   cd ~/Isabelle/Zerlege-Isa98-1/src/HOL/

   /src/HOL> sml @SMLload=HOL-plus

   cd"~/MathEngine99/src/";

   use"ROOT.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 pblID       => ("Model_Problem", Model_Problem pblID)

| 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_Domain domID	    => ("Specify_Domain", Specify_Domain 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 subs           => ("Substitute", Substitute subs) 

| 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","op +"),("minus","op -"),("times","op *"),

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

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_Domain","Specify_Problem","Specify_Method"];

"-----------------------------------------------------------------------";

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

   *)

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

  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,_,_,_,_,_), scr) = init_scrstate thy itms mI;

    val ini = init_form thy scr env;

    val (p,p_) = (lev_dn p,Res);

  in 

    case ini of

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

	         *)

    let (*val (p,p_) = (lev_on p,Frm); implicit Take -> generate1*)

	val f = Sign.string_of_term (sign_of (assoc_thy thy')) t;

	(*val (pt,ps) = cappend_form pt p is t*)

	(*writes to pt without asking user !!!?*)

	val ((p,p_),_,_,pt) = (*implicit Take*)

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

		      is(*Uistate.19.8.03*) (lev_on p,Frm) pt

	val {srls,...} = get_met mI

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

    in ((p,p_), ((lev_onFrm o lev_dnRes) pos, is, nx), 

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

	tac_2tac nx, Safe, pt) end

  | None =>

    let val m = fst3 (next_tac (thy',srls) (pt,(lev_on p,Frm)) scr is);

	val f = case m of 

		    Subproblem' ((domID, pblID,_),_,_) => 

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

			   (Sign.string_of_term (sign_of (assoc_thy thy')) 

						(subpbl domID pblID))))

		  | _ => EmptyMout;

    (*nothing written to pt !!!*)

    in ((p,p_), (lev_dnRes pos, is, m), f, tac_2tac m, Safe, pt) end

  end

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

  let val _=writeln"###solve Free_Solve";

    val p' = lev_dn_ (p,Res);

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

  in (p', (p',Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Unsafe, pt) end

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

   *)

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

    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 ((p,p_),ps,f,pt) = 

		   generate1 thy (Check_Postcond'(pI,(scval,

						      map term2str asm)))

			     is (pp,Res) pt;

	   in ((p,p_), (([],Res),is,End_Proof''), f, End_Proof', scsaf, pt) 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 ((p,p_), ((pp,Res),is',nx), f, tac_2tac nx, scsaf, pt) end

    end

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

   *)

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

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

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

   *)

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

    let (*val rls = the (assoc(!ruleset',rls'))

	    handle _ => raise error ("solve: '"^rls'^"' not known");*)

	val thy = assoc_thy thy';

        val (srls, sc, is) = 

	    case rls of

		Rrls {scr=sc as Rfuns {init_state=ii,...},...} => 

		(e_rls, sc, RrlsState (ii t))

	      | Rls {srls=srls,scr=sc as Script s,...} => 

		(srls, sc, ScrState ([(one_scr_arg s,t)], [], 

			       None, e_term, Sundef, true));

	val pt = update_tac pt (fst p) (Detail_Set (id_rls rls));

	val (p,cid,_,pt) = generate1 thy (Begin_Trans' t) is p pt;

	val nx = (tac_2tac o fst3) (next_tac (thy',srls) (pt,p) sc is);

	val aopt = applicable_in p pt nx;

    in case aopt of

	   Notappl s => raise error ("solve Detail_Set: "^s)

	 (* val Appl m = aopt;

	    *)

	 | Appl m => solve ("discardFIXME",m) p pt end

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

    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

(* val (mI,(p,p_)) = ("xxx",p);

   *)

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

    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 ((p,p_),((p,p_),Uistate,Empty_Tac_),f, Empty_Tac, Unsafe, pt) 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', (m',f',pt',p',c')::ss) =>

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

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

		*)

	       let val nxt_ = 

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

			   (_,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 (p',(p',is',nxt_), f', tac_2tac nxt_, safe is', pt'(*'*)) end

	     | NotLocatable =>  

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

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

	       in (p,(p,Uistate,Empty_Tac_),f, Empty_Tac, Unsafe, pt) end

	end;

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

   val (mI,m) = nxt; val pos' as (p,p_) = p;

   *)

fun meOLD ((mI,m):tac'_) (pos' as (p,p_):pos') (c:cid) (pt:ptree) =

  case applicable_in (p,p_) pt m of

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

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

	       *)

    (case m of

	( Refine_Problem' ms) => 

	 (pos',[], Problems (RefinedKF ms), 

	  ("Specify_Problem", Specify_Problem (refined ms)), Safe, pt)

       | _ => (if mI mem specsteps

	       then let val (p',c,f,m,s,pt) = specify m (p,p_) [] pt;

		   in (p',[],f,mk_tac'_ m,s,pt)

		    end

	       else let val ((p,p_),c,f,m,s,pt) = solve (mI,m) (p,p_) pt;

		   in ((p,p_),[],f,mk_tac'_ m,s,pt) end))

  | Notappl e => ((p,p_),[], Error' (Error_ e),

		  mk_tac'_ Empty_Tac (*nxtstep ??*), Unsafe,pt);

val me = meOLD;

(* 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 mI mem specsteps

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

	     in f end

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

	   in f end;