(* Title:  "Minisubpbl/200-start-method-NEXT_STEP.sml"

   Author: Walther Neuper 1105

   (c) copyright due to lincense terms.

*)

open Ctree;

open Pos;

open TermC;

open Istate;

open Tactic;

open I_Model;

open Pre_Conds;

open Rewrite;

open Step;

open LItool;

open LI;

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

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

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

tracing "--- Minisubplb/200-start-method-NEXT_STEP.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) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Model_Problem = tac

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Theory "Test" = tac

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Problem ["sqroot-test", "univariate", "equation", "test"] = tac

(*[], Met*)val return_Step_do_next_Specify_Problem = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)

(*/------------------- step into Step.do_next_Specify_Problem ------------------------------\\*)

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

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

  (*if*) Pos.on_calc_end ip (*else*);

      val (_, probl_id, _) = Calc.references (pt, p);

val _ =

      (*case*) tacis (*of*);

        (*if*) probl_id = Problem.id_empty (*else*);

      Step.switch_specify_solve p_ (pt, ip);

"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));

      (*if*) Pos.on_specification ([], state_pos) (*then*);

      Step.specify_do_next (pt, input_pos);

"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));

    val (_, (p_', tac)) = Specify.find_next_step ptp

    val ist_ctxt =  Ctree.get_loc pt (p, p_)

val _ =

    (*case*) tac (*of*);

Step_Specify.by_tactic_input tac (pt, (p, p_'));

"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos)) =

  (tac, (pt, (p, p_')));

      val (o_model, ctxt, i_model) =

Specify_Step.complete_for id (pt, pos);

"~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));

    val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = met_imod, ctxt,

       ...} = Calc.specify_data (ctree, pos);

    val ctxt = Ctree.get_ctxt ctree pos

    val (dI, _, _) = References.select_input o_refs refs;

    val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID

    val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))

    val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)

    val (_, (i_model, _)) = 

   M_Match.match_itms_oris ctxt o_model' (I_Model.OLD_to_TEST i_prob,

                            I_Model.OLD_to_TEST i_prob) (m_patt, where_, where_rls);

"~~~~~ fun match_itms_oris , args:"; val (ctxt, pbl, (pbt, where_, where_rls), oris) =

  (ctxt, i_prob, (m_patt, where_, where_rls), o_model');

 (*0*)val mv = Pre_Conds.max_variant pbl;

      fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.descriptor itm_;

      fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of

				SOME _ => false | NONE => true;

 (*1*)val mis = (filter (notmem pbl)) pbt;

      fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';

      fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));

 (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;

      val news = (flat o (map (oris2itms oris))) mis;

 (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;

      val newitms = filter mem_vat news;

 (*4*)val itms' = pbl @ newitms;

      val (pb, where_') = Pre_Conds.check ctxt where_rls where_ 

        (pbt, I_Model.OLD_to_TEST itms');

"~~~~~ fun check , args:"; val (ctxt, where_rls, where_, (model_patt, i_model)) =

  (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST itms'));

      val (env_model, (env_subst, env_eval)) = make_environments model_patt i_model

      val pres_subst = map (TermC.subst_atomic_all env_subst) where_;

      val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);

      val full_subst = if env_eval = [] then pres_subst_other

        else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)

(*+*)val "Test" = ctxt |> Proof_Context.theory_of |> ThyC.id_of

(*+*)val Rule_Set.Repeat {id = "prls_met_test_squ_sub", ...} = where_rls

(*+*)val [(true, tTEST as Const ("Test.precond_rootmet", _) $ Free ("x", xxx))] = full_subst

(*+*)val ctxt = Config.put rewrite_trace true ctxt;

      val evals = map (

 Pre_Conds.eval ctxt where_rls) full_subst;

(* (*declare [[rewrite_trace = true]]*)

@## rls: prls_met_test_squ_sub on: precond_rootmet x 

@### try calc: "Test.precond_rootmet" 

@#### eval asms: "(precond_rootmet x) = True" 

@### calc. to: True 

@### try calc: "Test.precond_rootmet" 

@### try calc: "Test.precond_rootmet" 

*)

(*+*)val ctxt = Config.put rewrite_trace false ctxt;

"~~~~~ fun eval_precond_rootmet , args:"; val ((thmid:string), _, (t as (Const (\<^const_name>\<open>Test.precond_rootmet\<close>, _) $ arg)), ctxt) =

  ("aaa", "bbb", tTEST, ctxt);

    SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg) "",

      HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

;

    (TermC.mk_thmid thmid (UnparseC.term ctxt arg)) "";

"~~~~~ fun mk_thmid , args:"; val (thmid, n1, n2) = (thmid, (UnparseC.term ctxt arg), "");

  thmid ^ (cut_longid n1) ^ "_" ^ (cut_longid n2);

      (cut_longid n2);

"~~~~~ fun cut_longid , args:"; val (dn) = (n2);

(*\------------------- step into Step.do_next_Specify_Problem ------------------------------//*)

val (_, ([(tac, _, _)], _, (pt, p))) = return_Step_do_next_Specify_Problem; val Specify_Method ["Test", "squ-equ-test-subpbl1"] = tac;

(*[1], Frm*)val return_Step_do_next_Specify_Method = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)

(*/------------------- step into Specify_Method --------------------------------------------\\*)

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

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

  (*if*) Pos.on_calc_end ip (*else*);

      val (_, probl_id, _) = Calc.references (pt, p);

val _ =

      (*case*) tacis (*of*);

        (*if*) probl_id = Problem.id_empty (*else*);

           switch_specify_solve p_ (pt, ip);

"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));

      (*if*) Pos.on_specification ([], state_pos) (*then*);

           specify_do_next (pt, input_pos);

"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);

    val (_, (p_', tac)) = Specify.find_next_step ptp

    val ist_ctxt =  Ctree.get_loc pt (p, p_)

(*+*)val Tactic.Apply_Method mI =

    (*case*) tac (*of*);

  	    LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))

  	      ist_ctxt (pt, (p, p_'));

"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =

  ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)),

  	      ist_ctxt, (pt, (p, p_')));

      val (itms, oris, probl, o_spec, spec) = case get_obj I pt p of

         PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ...}

         => (itms, oris, probl, o_spec, spec)

      | _ => raise ERROR ""

      val (_, pI', _) = References.select_input o_spec spec

      val (_, itms) = I_Model.s_make_complete ctxt oris

        (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pI', mI)

         val (is, env, ctxt, prog) = case

           LItool.init_pstate ctxt itms mI of

             (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)

val return_init_pstate = (is, env, ctxt, prog)

(*#------------------- un-hide local of init_pstate -----------------------------------------\*)

fun msg_miss ctxt 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 \"" ^ MethodC.id_to_string metID ^ "\" by \"" ^ caller ^ "\":\n" ^

	"formal arg \"" ^ UnparseC.term ctxt f ^ "\" doesn't match any actual arg.\n" ^

	"with:\n" ^

	(string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms ctxt formals ^ "\n" ^

	(string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms ctxt actuals

fun msg_miss_type ctxt sc metID 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 \"" ^ MethodC.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^

	"formal arg \"" ^ UnparseC.term ctxt f ^ "\" of type \"" ^ UnparseC.typ ctxt (type_of f) ^

  "\" doesn't mach any actual arg.\nwith:\n" ^

	(string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms ctxt formals ^ "\n" ^

	(string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms ctxt actuals ^ "\n" ^

  "   with types: " ^ (strs2str o (map ((UnparseC.typ ctxt) o type_of))) actuals

fun msg_ambiguous ctxt 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 \"" ^ MethodC.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^

  "formal arg. \"" ^ UnparseC.term ctxt f ^ "\" type-matches with several..."  ^

  "actual args. \"" ^ UnparseC.terms ctxt aas ^ "\"\n" ^

  "selected \"" ^ UnparseC.term ctxt (hd aas) ^ "\"\n" ^

	"with\n" ^

	"formals: " ^ UnparseC.terms ctxt formals ^ "\n" ^

	"actuals: " ^ UnparseC.terms ctxt actuals

fun trace_init ctxt metID =

  if Config.get ctxt LI_trace

  then tracing("@@@ program \"" ^ strs2str metID ^ "\"")

  else ();

fun assoc_by_type ctxt f aa prog met_id formals actuals =

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

    [] => raise ERROR (msg_miss_type ctxt prog met_id f formals actuals)

  | [a] => (f, a)

  | aas as (a :: _) => (writeln (msg_ambiguous ctxt prog met_id f aas formals actuals); (f, a));

(*

  fun assoc_formals_actuals: at "PIDE turn 11" ONLY syntax revised, NOT semantics

  Env.T ->         (* [] for building return Env.T         *)

  term list ->     (* changed during building return Env.T *)

  term list ->     (* changed during building return Env.T *)

  Proof.context -> (*                                      *)

  term ->          (* program code                         *)

  MethodC.id ->    (* for error msg                        *)

  term list ->     (* original value, unchanged            *)

  term list ->     (* original value, unchanged            *)

  Env.T            (* return Env.T                         *)

*)

fun relate_args _ (f::_) [] ctxt prog met_id formals actuals =

    raise ERROR (msg_miss ctxt prog met_id "relate_args" f formals actuals)

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

  | relate_args env (f::ff) (aas as (a::aa)) ctxt prog met_id formals actuals = 

    if type_of f = type_of a 

    then relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals

    else

      let val (f, a) = assoc_by_type ctxt f aas prog met_id formals actuals

      in relate_args (env @ [(f, a)]) ff (remove op = a aas) ctxt prog met_id formals actuals end

;

(*+*)relate_args: Env.T -> term list -> term list -> Proof.context -> term -> MethodC.id ->

    term list -> term list -> Env.T;

(*#------------------- un-hide local of init_pstate -----------------------------------------/*)

(*//------------------ step into init_pstate NEW -------------------------------------------\\*)

val (_, ctxt, i_model, met_id) = (prog_rls, ctxt, itms, mI);

"~~~~~ fun init_pstate , args:"; val (ctxt, i_model, met_id) =

    (ctxt, i_model, met_id);

    val (model_patt, program, prog, prog_rls, where_, where_rls) =

      case MethodC.from_store ctxt met_id of

        {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...} =>

          (model_patt, program, prog, prog_rls, where_, where_rls)

      | _ => raise ERROR ("init_pstate with " ^ MethodC.id_to_string met_id)

    val (env_model, (env_subst, env_eval)) = make_environments model_patt i_model;

    val actuals = map snd env_model

(*+*)val "[x + 1 = 2, x, L]" = actuals |> UnparseC.terms @{context}

    val formals = Program.formal_args prog    

(*+*)val "[e_e, v_v]" = (formals |> UnparseC.terms @{context})

(*+*)val "minisubpbl e_e v_v =\n(let e_ea =\n       (Try (Rewrite_Set ''norm_equation'') #>\n        Try (Rewrite_Set ''Test_simplify''))\n        e_e;\n     L_La =\n       SubProblem\n        (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],\n         [''Test'', ''solve_linear''])\n        [BOOL e_e, REAL v_v]\n in Check_elementwise L_L {v_v. Assumptions})" =

  (prog |> UnparseC.term @{context})

    val preconds = Pre_Conds.check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval))

(*||------------------ continue init_pstate NEW --------------------------------------------\\*)

    val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));

    val ist = Istate.e_pstate

      |> Istate.set_eval prog_rls

      |> Istate.set_env_true (relate_args [] formals actuals ctxt prog met_id formals actuals);

(*+*)                        (relate_args [] formals actuals ctxt prog met_id formals actuals);

(*+*)val "[\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\"]" =

                             (relate_args [] formals actuals ctxt prog met_id formals actuals)

       |> Subst.to_string @{context}

val return_init_pstate_steps = (* = return_init_pstate*)

    (Istate.Pstate ist, ctxt, program)

(*\\------------------ step into init_pstate NEW -------------------------------------------//*)

val (is, env, ctxt, prog) = return_init_pstate;

(*|------------------- continuing Specify_Method ---------------------------------------------*)

(*\------------------- step into Specify_Method --------------------------------------------//*)

val (_, ([(tac, _, _)], _, (pt, p))) = return_Step_do_next_Specify_Method; val Apply_Method ["Test", "squ-equ-test-subpbl1"] = tac;

(*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Rewrite_Set "norm_equation" = tac

(*[1], Res*)val return_Step_do_next_Rewrite_Set = Step.do_next p ((pt, e_pos'), []);

(*/------------------- step into Apply_Method ----------------------------------------------\\*)

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

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

  (*if*) Pos.on_calc_end ip (*else*);

      val (_, probl_id, _) = Calc.references (pt, p);

val _ =

      (*case*) tacis (*of*);

        (*if*) probl_id = Problem.id_empty (*else*);

      Step.switch_specify_solve p_ (pt, ip);

"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos))

  = (p_, (pt, ip));

      (*if*) Pos.on_specification ([], state_pos) (*else*);

        LI.do_next (pt, input_pos);

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

    (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);

	      val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;

val return_LI_find_next_step = (*case*)

        LI.find_next_step sc (pt, pos) ist ctxt (*of*);

(*//------------------ step into LI.find_next_step -----------------------------------------\\*)

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

  (sc, (pt, pos), ist, ctxt);

(*.. this showed that we have ContextC.empty*)

(*\\------------------ step into LI.find_next_step -----------------------------------------//*)

val LI.Next_Step (ist, ctxt, tac) = return_LI_find_next_step;

        LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;

"~~~~~ fun by_tactic , args:"; val (tac_, ic, (pt, pos))

  = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp);

      val pos = next_in_prog' pos

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

Solve_Step.add_general tac_ ic (pt, pos);

"~~~~~ fun add_general , args:"; val (tac, ic, cs)

  = (tac_, ic, (pt, pos));

 (*if*) Tactic.for_specify' tac (*else*);

Solve_Step.add tac ic cs;

"~~~~~ fun add , args:"; val ((Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))), (is, ctxt), (pt, (p, _)))

  = (tac, ic, cs);

      val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f 

        (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete

      val pt = Ctree.update_branch pt p Ctree.TransitiveB

val return =

      ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term ctxt f'), pt)

(*\------------------- step into Apply_Method ----------------------------------------------//*)

val (_, ([(tac, _, _)], _, (pt, p))) = return_Step_do_next_Rewrite_Set

(* final test ... ----------------------------------------------------------------------------*)

(*+*)val ([2], Res) = p;

Test_Tool.show_pt_tac pt; (*[

([], Frm), solve (x + 1 = 2, x)

. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"], 

([1], Frm), x + 1 = 2

. . . . . . . . . . Rewrite_Set "norm_equation", 

([1], Res), x + 1 + - 1 * 2 = 0

. . . . . . . . . . Rewrite_Set "Test_simplify", 

([2], Res), - 1 + x = 0

. . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"]]   ..INCORRECT

*)