(* Title:  200-start-method.sml

   Author: Walther Neuper 1105

   (c) copyright due to lincense terms.

*)

"----------- Minisubplb/200-start-method.sml ---------------------";

"----------- Minisubplb/200-start-method.sml ---------------------";

"----------- Minisubplb/200-start-method.sml ---------------------";

val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];

val (dI',pI',mI') =

  ("Test", ["sqroot-test","univariate","equation","test"],

   ["Test","squ-equ-test-subpbl1"]);

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Apply_Method"*)

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

"~~~~~ fun me, args:"; val (_,tac) = nxt;

"~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);

val (mI,m) = mk_tac'_ tac;

val Appl m = applicable_in p pt m;

member op = specsteps mI; (*false*)

"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);

"~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);

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

val thy' = get_obj g_domID pt p;

val thy = assoc_thy thy';

val {srls, pre, prls, ...} = get_met mI;

val pres = check_preconds thy prls pre meth |> map snd;

val ctxt = ctxt |> insert_assumptions pres;

val (is'''' as ScrState (env'''',_,_,_,_,_), _, sc'''') = init_scrstate thy meth mI;

"~~~~~ fun init_scrstate, args:"; val (thy, itms, metID) = (thy, meth, mI)

    val actuals = itms2args thy metID itms

	  val scr as Script sc = (#scr o get_met) metID

    val formals = formal_args sc    

	  (*expects same sequence of (actual) args in itms and (formal) args in met*)

	  fun relate_args env [] [] = env

	    | relate_args env _ [] = 

	        error ("ERROR in creating the environment for '" ^

			    id_of_scr sc ^ "' from \nthe items of the guard of " ^

			    metID2str metID ^ ",\n" ^

			    "formal arg(s), from the script, miss actual arg(s), from the guards env:\n" ^

			    (string_of_int o length) formals ^

			    " formals: " ^ terms2str formals ^ "\n" ^

			    (string_of_int o length) actuals ^

			    " actuals: " ^ terms2str actuals)

	    | relate_args env [] actual_finds = env (*may drop Find!*)

	    | relate_args env (a::aa) (f::ff) = 

	        if type_of a = type_of f 

	        then relate_args (env @ [(a, f)]) aa ff

          else 

	          error ("ERROR in creating the environment for '" ^

			      id_of_scr sc ^ "' from \nthe items of the guard of " ^

			      metID2str metID ^ ",\n" ^

			      "different types of formal arg, from the script, " ^

			      "and actual arg, from the guards env:'\n" ^

			      "formal: '" ^ term2str a ^ "::" ^ (type2str o type_of) a ^ "'\n" ^

			      "actual: '" ^ term2str f ^ "::" ^ (type2str o type_of) f ^ "'\n" ^

			      "in\n" ^

			      "formals: " ^ terms2str formals ^ "\n" ^

			      "actuals: " ^ terms2str actuals)

     val env = relate_args [] formals actuals;

val ctxt = ProofContext.init_global thy |> declare_constraints' actuals

val {pre, prls, ...} = get_met metID;

val pres = check_preconds thy prls pre itms |> map snd;

val ctxt = ctxt |> insert_assumptions pres;

"~~~~~ continue solve";

val ini = init_form thy sc'''' env'''';

val p = lev_dn p;

val SOME t = ini;

val (pos,c,_,pt) = 

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

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

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

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

val ctxt = get_ctxt pt pos;

val SOME known_x = parseNEW ctxt "x+z+z"; (*x has declare_constraints to real*)

val SOME unknown = parseNEW ctxt "a+b+c";

if type_of known_x = Type ("RealDef.real",[]) then ()

else error "x+1=2 after start root-pbl wrong type-inference for known_x";

if  type_of unknown = TFree ("'a", ["Groups.plus"]) then ()

else error "x+1=2 after start root-pbl wrong type-inference for unknown";

val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = ("Rewrite_Set"*)

case nxt of ("Rewrite_Set", _) => ()

| _ => error "minisubpbl: Method not started in root-problem";