(* Title:  "Minisubplb/400-start-meth-subpbl.sml"

   Author: Walther Neuper 1105

   (c) copyright due to lincense terms.

ATTENTION: THE FILE IS TOO BIG FOR Java BUFFERS, so copy in pieces.

*)

open Test_Code

open Pos;

open Ctree;

open Istate;

open TermC;

open Step;

open LI;

open Tactic;

open Refine;

open Specify;

"----------- Minisubpbl/400-start-meth-subpbl.sml ----------------";

"----------- Minisubpbl/400-start-meth-subpbl.sml ----------------";

"----------- Minisubpbl/400-start-meth-subpbl.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'))];

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; val Apply_Method ["Test", "squ-equ-test-subpbl1"] = nxt;

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 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]) = nxt;

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 Add_Find "solutions x_i" = nxt;

val return_Add_Find = me nxt p [] pt;

(*/------------------- step into me Add_Find ------------------------------------------------\*)

"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);

      val ctxt = Ctree.get_ctxt pt p

val ("ok", (_, _, ptp as (pt, p))) =

  	    (*case*) Step.by_tactic tac (pt, p) (*of*);

    (*case*)

      Step.do_next p ((pt, Pos.e_pos'), []) (*of*);

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

  (p, ((pt, Pos.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;

"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);

(*+isa* )val Refine_Problem ["LINEAR", "univariate", "equation", "test"] = tac;( **)

(*+isa2*)val Specify_Theory "Test" = tac;(**)

    val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,

      spec = refs, ...} = Calc.specify_data (pt, pos); (*I_Model.T------------------^^^*)

    val ctxt = Ctree.get_ctxt pt pos;

      (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);

        (*if*) p_ = Pos.Pbl (*then*);

val return_for_problem as (_, (_, xxx)) =

   Specify.for_problem ctxt oris (o_refs, refs) (pbl, met);

"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =

  (ctxt, oris, (o_refs, refs), (pbl, met));

    val cpI = if pI = Problem.id_empty then pI' else pI;

    val cmI = if mI = MethodC.id_empty then mI' else mI;

    val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;

    val {model = mpc, ...} = MethodC.from_store ctxt cmI

val (preok, xxxxx) =

 Pre_Conds.check ctxt where_rls where_ (pbt, pbl);

(*+*)val [(true, xxx)] = xxxxx;

(*+*)if (xxx |> UnparseC.term @{context}) =

  "matches (x = 0) (- 1 + x = 0) \<or>\n" ^

  "matches (?b * x = 0) (- 1 + x = 0) \<or>\n" ^

  "matches (?a + x = 0) (- 1 + x = 0) \<or>\n" ^

  "matches (?a + ?b * x = 0) (- 1 + x = 0)"

  then () else error "pre-cond, to be evaluated, CHANGED";

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

  (ctxt, where_rls, where_, (pbt, pbl)); (*..delete double above --- adhoc inserted n ---*)

      val (env_model, (env_subst, env_eval)) = 

           make_environments model_patt i_model;

"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);

(*+*)(pbt |> Model_Pattern.to_string @{context}) = "[\"" ^

  "(#Given, (equality, e_e))\", \"" ^ 

  "(#Given, (solveFor, v_v))\", \"" ^ 

  "(#Find, (solutions, v_v'i'))\"]";

(*+*)(( pbl) |> I_Model.to_string @{context}) =   "[\n" ^ 

  "(1, [1], true ,#Given, (Cor equality (- 1 + x = 0) ,(e_e, [- 1 + x = 0]), Position.T)), \n" ^ 

  "(2, [1], true ,#Given, (Cor solveFor x ,(v_v, [x]), Position.T)), \n" ^ 

  "(3, [1], true ,#Find, (Cor solutions x_i ,(v_v'i', [x_i]), Position.T))]";

    val all_variants =

        map (fn (_, variants, _, _, _) => variants) i_model

        |> flat

        |> distinct op =

    val variants_separated = map (filter_variants' i_model) all_variants

    val sums_corr = map (Model_Def.cnt_corrects) variants_separated

    val sum_variant_s = Model_Def.arrange_args sums_corr (1, all_variants)

    val (_, max_variant) = hd (*..crude decision, up to improvement *)

      (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)

    val i_model_max =

      filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model

    val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat

    val env_model = make_env_model equal_descr_pairs

    val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs

    val subst_eval_list =

        make_envs_preconds equal_givens;

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

"~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);

"~~~~~ fun xxx , args:"; val (((_, (_, id)), (_, _, _, _, (feedb, _)))) = (nth 1 equal_givens);

val [] =

           discern_feedback id feedb;

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

(*-------------------- continuing of_max_variant ---------------------------------------------*)

     val (env_subst, env_eval) = split_list subst_eval_list

val return_of_max_variant = (i_model_max, env_model, (env_subst, env_eval))

(*\------------------- step into me Add_Find ------------------------------------------------/*)

val (p,_,f,nxt,_,pt) = return_Add_Find; (** )val Specify_Theory "Test" = nxt;( **)

(*isa* )val Empty_Tac = nxt;( **)

(*isa2*)val Specify_Theory "Test" = nxt;(**)

val (p,_,f,nxt,_,pt) = me nxt p [] pt; (** )val Specify_Problem ["LINEAR", "univariate", "equation", "test"] = nxt;( **)

val return_Specify_Method

                     = me nxt p [] pt;

(*/------------------- step into me Specify_Problem -----------------------------------------\*)

(*\------------------- step into me Specify_Problem -----------------------------------------/*)

val (p,_,f,nxt,_,pt) = return_Specify_Method; val Specify_Method ["Test", "solve_linear"] = nxt;

val return_Specify_Method

                     = me nxt p [] pt;

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

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

val (p_return_Specify_Method,_,f,nxt,_,pt) = return_Specify_Method; val Apply_Method ["Test", "solve_linear"] = nxt;

val return_Apply_Method

                     = me nxt p_return_Specify_Method [] pt;

(*+*)val ([3], Pbl) = p;

(*+*)if get_ctxt pt p |> ContextC.is_empty then error "ctxt not initialised by specify, PblObj{ctxt,...}" else ();

(*+*)if get_ctxt pt p_return_Specify_Method |> ContextC.is_empty then error "ctxt NOT initialised by Subproblem'}" else ();

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

"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p_return_Specify_Method, [], pt);

  val ("ok", (_, _, (_, _))) = (*case*)

      Step.by_tactic tac (pt, p) (*of*);

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

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

   val Applicable.Yes tac' = (*case*) Step.check tac (pt, p) (*of*);

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

Step_Solve.by_tactic tac' ptp;

"~~~~~ fun by_tactic , args:"; val (tac as Tactic.Apply_Method' _, ptp as (pt, p))

  = (tac', ptp);

(*+*)val PblObj {ctxt, ...} = get_obj I pt [3];

(*+isa==isa2*)ContextC.get_assumptions ctxt = [];

(*+isa==isa2*)(Ctree.get_assumptions pt p |> map (UnparseC.term @{context})) = [];

        LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp;

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

  = (tac, (get_istate_LI pt p, get_ctxt_LI pt p), (pt, p));

(*+isa==isa2*)if (ContextC.get_assumptions ctxt |> map (UnparseC.term ctxt))

(*+*)   = ["precond_rootmet x"]

(*+*)then () else error "assumptions 7 from Apply_Method'";

(*+*)val [3] = 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 "LI.by_tactic Apply_Method': uncovered case get_obj";

(*+isa==isa2*)if (ContextC.get_assumptions ctxt |> map (UnparseC.term ctxt))

(*+*)   = ["precond_rootmet x"]

(*+*)then () else error "assumptions 8";

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

      val (_, itms) = I_Model.s_make_complete ctxt oris (probl, itms) (pI', mI)

         val prog_rls = LItool.get_simplifier (pt, pos)

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

           LItool.init_pstate ctxt itms mI of

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

         | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate";

(*+*)(ContextC.get_assumptions ctxt |> map (UnparseC.term ctxt))

(*+isa==isa2*)  = ["matches (?a = ?b) (- 1 + x = 0)", "precond_rootmet x"]; 

        val ini = LItool.implicit_take ctxt prog env;

        val pos = start_new_level pos

val SOME t =

      (*case*) ini (*of*);

          val show_add = Tactic.Apply_Method' (mI, SOME t, is, ctxt);

          val (pos, c, _, pt) = Solve_Step.add show_add (is, ctxt) (pt, pos);

(*+*)if (ContextC.get_assumptions ctxt |> map (UnparseC.term ctxt))

(*+isa==isa2*) = ["matches (?a = ?b) (- 1 + x = 0)", "precond_rootmet x"]

(*+*)then () else error "assumptions 9";

val return = ("ok", ([(Tactic.Apply_Method mI, show_add, (pos, (is, ctxt)))], c, (pt, pos)));

"~~~~~ from LI.by_tactic to..to me return"; val ("ok", (_, _, ptp)) = return;

      val (pt, p) = ptp;

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

(*|------------------- continue me Applythod ------------------------------------------------|*)

    (*case*)

      Step.do_next p ((pt, Pos.e_pos'), []) (*of*);

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

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

  = (p, ((pt, Pos.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) (*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 Next_Step (ist, ctxt, tac) =

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

val continue_do_next = (ist, ctxt, tac, ptp)(*keep for continuing LI.do_next*);

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

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

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

  (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);

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

  ((prog, (ptp, ctxt)), (Pstate ist));

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

           scan_dn cc (trans_scan_dn ist) (Program.body_of prog);

"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b)))) =

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

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

"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Tactical.Repeat\<close>(*1*), _) $ e $ a)) =

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

       scan_dn cc (ist |> path_down_form ([L, R], a)) e;

"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ e1 $ e2)) =

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

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

"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t (*fall-through*)) =

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

    (*if*) Tactical.contained_in t (*else*);

val (Program.Tac prog_tac, form_arg) =

      (*case*) LItool.check_leaf "next  " ctxt eval (get_subst ist) t (*of*);

           check_tac cc ist (prog_tac, form_arg);

"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg)) =

  (cc, ist, (prog_tac, form_arg));

    val m =

    LItool.tac_from_prog (pt, p) prog_tac;

"~~~~~ fun tac_from_prog , args:"; val (_, _, (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ sub $ rls $ _)) =

  ((pt, p), (Proof_Context.theory_of ctxt), prog_tac);

      val sub' =

     Subst.program_to_input ctxt sub

(*-------------------- stop step into find_next_step -----------------------------------------*)

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

(*kept for continuing LI.do_next*)val (ist, ctxt, tac, ptp) = continue_do_next;

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

"~~~~~ fun by_tactic , args:"; val (tac_, ic, (pt, pos) (*fall through*)) =

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

           add tac ic cs;

"~~~~~ fun add , args:"; val ((Tactic.Rewrite_Set_Inst' (_, _, subs', 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_Inst (Subst.T_to_input ctxt subs', Rule_Set.id rls')) (f', asm) Ctree.Complete;

"~~~~~ fun cappend_atomic , args:"; val (pt, p, ic_res, f, r, f', s) =

  (pt, p, (is, ctxt), f, 

        (Tactic.Rewrite_Set_Inst (Subst.T_to_input ctxt subs', Rule_Set.id rls')), (f', asm), Ctree.Complete);

     Subst.T_to_input ctxt subs';

"~~~~~ from fun switch_specify_solve \<longrightarrow>fun Step.do_next \<longrightarrow>fun me , return:"; val (_, ts) 

        = (LI.do_next (pt, input_pos));

(*-------------------- stop step into do_next ------------------------------------------------*)

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

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

val (p_return_Apply_Method,_,f,nxt,_,pt) = return_Apply_Method; 

                                                           val Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv") = nxt;

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

(* final tests ... ---------------------------------------------------------------------------*)

val ([3, 1], Frm) = p_return_Apply_Method;

val "Rewrite_Set \"Test_simplify\"" =  Tactic.input_to_string ctxt nxt;

(*p_frm BEFORE Apply_Method at Subproblem*)

val p_frm = ([3], Frm);

val ["precond_rootmet x"] = Ctree.get_assumptions pt p_frm |> map (UnparseC.term @{context});

(*assumptions<>[] before Apply_Method of Subproblem*)

val ([3], Met) = p_return_Specify_Method;

val [(*--- inserted by Apply_Method ---*)] = Ctree.get_assumptions pt p_return_Specify_Method;

(*FALSE: 2 assumptions recorded Apply_Method of Subproblem*)

val ([3, 1], Frm) = p_return_Apply_Method;

val ["matches (?a = ?b) (- 1 + x = 0)", "precond_rootmet x"] =

  Ctree.get_assumptions pt p_return_Apply_Method |> map (UnparseC.term @{context});

(*p_res AFTER Apply_Method at Subproblem*)

val p_res = ([3], Res);

val ["precond_rootmet x"] = Ctree.get_assumptions pt p_res |> map (UnparseC.term @{context});