(* Title:  "Minisubpbl/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; (*nxt = ("Specify_Problem",..*)

"~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";

val (p'''',_,f'''',nxt'''',_,pt'''') = me nxt p [] pt; (* (@1) nxt'''' = ("Specify_Method",..*)

(*me nxt'''' p'''' [] pt''''; "ERROR in creating the environment..", SHOULD BE("Apply_Method",.*)

"~~~~~ we continue with (@1) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";

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

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

    val (pt, p) = 

	    (*locatetac is here for testing by me; Step.do_next would suffice in me*)

	    case locatetac tac (pt,p) of

		    ("ok", (_, _, ptp)) => ptp | _ => error "CHANGED --- Minisubplb/200-start-method 1"

(* Step.do_next p ((pt, e_pos'),[])  ..ERROR  = ("helpless",*)

"~~~~~ fun Step.do_next, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =

  (p, ((pt, e_pos'),[]));

val pIopt = get_pblID (pt,ip);

ip = ([],Res) (*= false*);

tacis (* = []*);

val SOME pI = pIopt;

member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)) (*= true*);

(*nxt_specify_ (pt, ip)  ..ERROR in creating the environment..*);

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

"~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";

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

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

1.ERROR WAS: nxt = ("Empty_Tac",..

2.ERROR WAS: *** stac2tac_ TODO: no match for (Rewrite_Set ''norm_equation'') (x + 1 = 2)*)

"~~~~~ we continue with (@2) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";

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

val ("ok", (_, _, (pt''''',p'''''))) = locatetac tac (pt,p);

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

val Appl m = applicable_in p pt tac; (*m = Apply_Method'..*)

 (*if*) Tactic.for_specify' m; (*false*)

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

"~~~~~ fun Step_Solve.by_tactic , args:"; val (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 |> ContextC.insert_assumptions pres;

val (is'''' as Pstate {env = env'''',...}, _, sc'''') = init_pstate srls ctxt meth mI;

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

    val actuals = itms2args thy metID itms

	  val scr as Prog 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 msg_miss sc metID caller f formals actuals =

  "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^

	"and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"" ^ caller ^ "\":\n" ^

	"formal arg \"" ^ Rule.term2str f ^ "\" doesn't mach an actual arg.\n" ^

	"with:\n" ^

	(string_of_int o length) formals ^ " formal args: " ^ Rule.terms2str formals ^ "\n" ^

	(string_of_int o length) actuals ^ " actual args: " ^ Rule.terms2str actuals

fun msg_ambiguous sc metID f aas formals actuals =

  "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^

	"and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^

  "formal arg. \"" ^ Rule.term2str f ^ "\" type-matches with several..."  ^

  "actual args. \"" ^ Rule.terms2str aas ^ "\"\n" ^

  "selected \"" ^ Rule.term2str (hd aas) ^ "\"\n" ^

	"with\n" ^

	"formals: " ^ Rule.terms2str formals ^ "\n" ^

	"actuals: " ^ Rule.terms2str actuals

    fun assoc_by_type f aa =

      case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of

        [] => error (msg_miss sc metID "assoc_by_type" f formals actuals)

      | [a] => (f, a)

      | aas as (a :: _) => (writeln (msg_ambiguous sc metID f aas formals actuals); (f, a));

	  fun relate_args _ (f::_)  [] = error (msg_miss sc metID "relate_args" f formals actuals)

	    | relate_args env [] _ = env (*may drop Find?*)

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

	      if type_of f = type_of a 

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

        else

          let val (f, a) = assoc_by_type f aas

          in relate_args (env @ [(f, a)]) ff (remove op = a aas) end

    val env = relate_args [] formals actuals;

  (*val _ = trace_istate env;*)

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

    val pres = Stool.check_preconds (Proof_Context.theory_of ctxt) prls pre itms |> map snd;

    val ctxt = ctxt |> ContextC.insert_assumptions pres;

"~~~~~ continue Step_Solve.by_tactic";

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 ("Real.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";

"~~~~~ continue me (@3) after locatetac";

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

"~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";

"~~~~~ fun Step.do_next, args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, Pos.e_pos'),[]));

val pIopt = get_pblID (pt,ip);

ip = ([], Pos.Res) (* = false*);

case tacis of [] => ();

case pIopt of SONE => ();

member op = [Pos.Pbl, Pos.Met] p_ andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) (* = false*);

"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt,ip);

Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false*);

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

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

"~~~~~ fun find_next_tactic , args:"; val ((ptp as(pt, (p, _))), (Rule.Prog prog), (Istate.Pstate ist, ctxt))

  = ((pt, pos), sc, is);

      (*case*) scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);

"~~~~~ fun scan_to_tactic2 , args:"; val ((prog, cc), (Istate.Pstate (ist as {path, ...})))

  = ((prog, (ptp, ctxt)), (Istate.Pstate ist));

  (*if*) path = [] (*then*);

  scan_dn2 cc (trans_scan_down2 ist) (Program.body_of prog);

"~~~~~ fun scan_dn2 , args:"; val (cc, ist, (Const ("HOL.Let"(*1*), _) $ e $ (Abs (i, T, b)))) =

  (cc, (trans_scan_down2 ist), (Program.body_of prog));

    (*case*) scan_dn2 cc (ist |> path_down [L, R]) e (*of*);

"~~~~~ fun scan_dn2 , args:"; val (cc, ist, (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a))

  = (cc, (ist |> path_down [L, R]), e);

    (*case*) scan_dn2 cc (ist |> path_down_form ([L, L, R], a)) e1 (*of*);

"~~~~~ fun scan_dn2 , args:"; val (cc, (ist as {act_arg, ...}), (Const ("Tactical.Try"(*2*), _) $ e))

  = (cc, (ist |> path_down_form ([L, L, R], a)), e1);

    (*case*) scan_dn2 cc (ist |> path_down [R]) e (*of*);

"~~~~~ fun scan_dn2 , args:"; val (((pt, p), ctxt), (ist as {eval, ...}), t) =

  (cc, (ist |> path_down [R]), e);

    val (Program.Tac stac, a') = 

      (*case*) Lucin.interpret_leaf "next  " ctxt eval (get_subst ist) t (*of*);

  	      val (m, m') = Lucin.stac2tac_ pt (Proof_Context.theory_of ctxt) stac;

"~~~~~ fun stac2tac_ , args:"; val (_, _, (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _)) =

  (pt, (Proof_Context.theory_of ctxt), stac);

(*+*)case stac2tac_ pt (Proof_Context.theory_of ctxt) stac of (Rewrite_Set "norm_equation", _) => ()

(*+*)| _ => error "stac2tac_ changed"

"~~~~~ continue last scan_dn2";

val Applicable.Appl m' = Applicable.applicable_in p pt m;

"~~~~~ fun result, args:"; val (m) = (m');

"~~~~~ fun rep_tac_, args:"; val (Tactic.Rewrite_Set' (thy', put, rls, f, (f', _))) = (m);

      val fT = type_of f;

      val lhs = Const ("Prog_Tac.Rewrite'_Set", [HOLogic.stringT, fT] ---> fT) 

        $ HOLogic.mk_string (Rule.id_rls rls) $ f;

(*        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ here was Free (Rule.id_rls rls, idT) *)

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