(* Title:  "Minisubpbl/150a-add-given-Maximum.sml"

   Author: Walther Neuper 1105

   (c) copyright due to lincense terms.

COMPARE Specify/specify.sml --- specify-phase: low level functions ---

ATTENTION: the file creates buffer overflow if copied in one piece !

Note: This test --- steps into me --- more than once, to a somewhat extreme extent;

  in order not to get lost while working in Test_Some etc, 

  re-introduce  ML (*--- step into XXXXX ---*) and Co.

  and use Sidekick for orientation.

  Nesting is indicated by  /---   //--   ///-  at the left margin of the comments.

*)

open Model_Def

open ME_Misc

open Pre_Conds;

val (_(*example text*),

  (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" :: 

     "Extremum (A = 2 * u * v - u \<up> 2)" :: 

     "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" :: 

     "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" :: 

     "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::

(*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)

     "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" :: 

     "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::

     "ErrorBound (\<epsilon> = (0::real))" :: []), 

   refs as ("Diff_App", 

     ["univariate_calculus", "Optimisation"],

     ["Optimisation", "by_univariate_calculus"])))

  = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];

val c = [];

val return_init_calc = 

 Test_Code.init_calc @{context} [(model, refs)]; (*val Model_Problem = nxt;*)

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

"~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))]) =

  (@{context}, [(model, refs)]);

    val thy = thy_id |> ThyC.get_theory ctxt

    val ((pt, p), tacis) = Step_Specify.initialise' thy (model, refs)

	  val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis

	  val f = 

           TESTg_form ctxt (pt,p);

"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p));

    val (form, _, _) =

   ME_Misc.pt_extract ctxt ptp;

"~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_ as Pbl(*Frm,Pbl*)))) = (ctxt, ptp);

        val ppobj = Ctree.get_obj I pt p

        val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p;

            (*if*) Ctree.is_pblobj ppobj (*then*);

           pt_model ppobj p_ ;

"~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}), Pbl_) =

  (ppobj, p_);

      val (_, pI, _) = Ctree.get_somespec' spec spec';

(*    val where_ = if pI = Problem.id_empty then []*)

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

	          val {where_rls, where_, model, ...} = Problem.from_store ctxt pI

	          val (_, where_) = 

 Pre_Conds.check ctxt where_rls where_

              (model, I_Model.OLD_to_POS probl);

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

  (ctxt, where_rls, where_, (model, I_Model.OLD_to_POS probl));

      val (env_model, (env_subst, env_eval)) = 

           make_environments model_patt i_model;

"~~~~~ fun make_environments , args:"; val (_, []) = (model_patt, i_model);

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

val (p,_,f,nxt,_,pt) = return_init_calc;   val Model_Problem = nxt

val (p, _, f, nxt, _, pt) = me nxt p c pt; val Add_Given "Constants [r = 7]" = nxt

val return_me_add_find_Constants =

           me nxt p c pt; val Add_Find "Maximum A" = #4 return_me_add_find_Constants;

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

"~~~~~ fun me , args:"; val (tac as Add_Given "Constants [r = 7]", p, _(*NEW remove*), pt) =

  (nxt, p, c, pt);

      val ctxt = Ctree.get_ctxt pt p

(*+*)val PblObj {probl = (1, [1, 2, 3], false, "#Given", Inc 

    ((Const ("Input_Descript.Constants", _), []), _)) :: _, ...}  = get_obj I pt (fst p)

(*-------------------------------------------^^--*)

val return_step_by_tactic = (*case*) 

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

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

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

val Applicable.Yes tac' =

    (*case*) Specify_Step.check tac (pt, p) (*of*);

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

(** )val return_step_by_tactic =( **)

(**)val return_step_specify_by_tactic =(**)

Step_Specify.by_tactic tac' ptp;

(*///----------------- step into Step_Specify.by_tactic ------------------------------------\\*)

"~~~~~ fun by_tactic , args:"; val ((Tactic.Add_Given' (ct, _)), (pt, p)) = (tac', ptp);

(** )val calling_code =( **)

(**)val return_by_Add_ =(**)

   Specify.by_Add_ "#Given" ct (pt, p);

(*////---------------- step by_Add_ --------------------------------------------------------\\*)

"~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, (pt, p));

    val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);

val false =

       (*if*) p_ = Pos.Met (*else*);

val (i_model, m_patt) =

         (pbl,

           (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)

val I_Model.Add i_single =

      (*case*) I_Model.check_single ctxt m_field oris i_model m_patt ct;

(** )val i_model' =( **)

(**)val return_add_single =(**)

   I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model;

(*/////--------------- step add_single -----------------------------------------------------\\*)

"~~~~~ fun add_single , args:"; val (thy, itm, model) =

  ((Proof_Context.theory_of ctxt), i_single, i_model);

    fun eq_untouched d (0, _, _, _, (itm_, _)) = (d = descriptor_POS itm_)

      | eq_untouched _ _ = false

    val model' = case I_Model.seek_ppc (#1 itm) model of

      SOME _ => overwrite_ppc thy itm model (*itm updated in is_notyet_input WN.11.03*)

(*\\\\\--------------- step add_single -----------------------------------------------------//*)

(*|||||--------------- step by_Add_ ----------------------------------------------------------*)

            val i_model' = return_add_single

(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_POS Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_POS AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_POS Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_POS SideConditions [] [__=__, __=__], Position.T))]"

 = i_model' |> I_Model.to_string_POS ctxt

            val tac' = I_Model.make_tactic m_field (ct, i_model')

	          val  (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)

val return_by_Add_step =

            ("ok", ([(Tactic.input_from_T ctxt tac', tac', (pos, (Istate_Def.Uistate, ctxt)))],

              [], (pt', pos)))

(*+++*)val {probl, ...} = Calc.specify_data (pt', pos);

(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_POS Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_POS AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_POS Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_POS SideConditions [] [__=__, __=__], Position.T))]"

 = probl |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt

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

val return_by_tactic_step = return_by_Add_

(*\\\----------------- step into Step_Specify.by_tactic ------------------------------------//*)

(*vvv--- this means, the return value of *)

val return_step_by_tactic_STEP = return_step_specify_by_tactic

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

val ("ok", (_, _, ptp)) = return_step_by_tactic;

(*+++*)val (pt, p) = ptp

(*+++*)val {probl, ...} = Calc.specify_data (pt, p);

(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_POS Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_POS AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_POS Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_POS SideConditions [] [__=__, __=__], Position.T))]"

 = probl |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt;

      val (pt, p) = ptp; (*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'), []));

val false =

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

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

val _ =

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

val false =

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

val ("ok", ([(Add_Find "Maximum A", _, _)], [], _)) =

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

val ("ok", ([(Add_Find "Maximum A", _, _)], [], _)) =

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

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

      spec = refs, ...} = Calc.specify_data (pt, pos);

    val ctxt = Ctree.get_ctxt pt pos;

(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_POS Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_POS AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_POS Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_POS SideConditions [] [__=__, __=__], Position.T))]"

 = pbl |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt(*+*)

val false =

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

val true =

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

(** )val ("dummy", (Pbl, Add_Find "Maximum A")) =( **)

(**)val return_for_problem as ("dummy", (Pbl, Add_Find "Maximum A"))=(**)

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

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

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

  (ctxt, oris, (o_refs, refs), (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS 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, _) =( **)

(**)val return_check =(**)

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

(*///----------------- step into Pre_Conds.check -------------------------------------------\\*)

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

  (ctxt, where_rls, where_, (pbt, pbl));

(** )val (_, (env_subst, env_eval)) =( **)

(**)val return_make_environments =(**)

Pre_Conds.make_environments model_patt i_model;

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

"~~~~~ fun make_environments , args:"; val (model_patt, i_model) = (model_patt, 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 env_model =( **)

(**)val return_make_env_model =(**)

  make_env_model equal_descr_pairs;

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

"~~~~~ fun make_env_model , args:"; val (equal_descr_pairs) = (equal_descr_pairs);

val return_make_env_model_step =

  map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))

        => (mk_env_model id feedb)) equal_descr_pairs

  |> flat

(*map:*)val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 2 equal_descr_pairs);

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

"~~~~~ fun mk_env_model , args:"; val (_, (Model_Def.Inc_POS (_, []))) = (id, feedb);

(*+*)val (patt, imod) = nth 2 equal_descr_pairs

(*+*)val "(#Find, (Maximum, maxx))" = patt |> Model_Pattern.single_to_string ctxt

(*+*)val "(2, [1, 2, 3], false ,#Find, (Inc_POS Maximum __, Position.T))" = imod |> I_Model.single_to_string_POS ctxt

val return_mk_env_model_2_step = []

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

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

val env_model = return_make_env_model;

(*||||---------------- contine.. make_environments -------------------------------------------*)

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

(** )val subst_eval_list =( **)

(**)val return_make_envs_preconds =(**)

  make_envs_preconds equal_givens;

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

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

val return_make_envs_preconds_step = 

  map (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb) equal_givens

  |> flat

val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 1 equal_givens

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

    val subst_eval_list = return_make_envs_preconds;

    val (env_subst, env_eval) = split_list subst_eval_list

val return_make_environments_step = (env_model, (env_subst, env_eval));

(*+*)if return_make_environments_step = return_make_environments

  then () else error "return_make_environments_step <> return_make_environments";

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

(*|||----------------- contine.. Pre_Conds.check ---------------------------------------------*)

      val (env_model, (env_subst, env_eval)) = return_make_environments

      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 evals = map (eval ctxt where_rls) full_subst

    (*in*)

val return_make_environments_step = (foldl and_ (true, map fst evals), pres_subst_other)

(*\\\----------------- step into Pre_Conds.check -------------------------------------------//*)

(*||------------------ contine.. for_problem -------------------------------------------------*)

    val (preok, _) = return_check;

  (*in*)

val false =

    (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);

val false =

      (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);

val NONE =

      (*case*) find_first (fn (_, _, _, _, (feedb, _)) => I_Model.is_error feedb) pbl (*of*);

val SOME (fd, ct' as "Maximum A") = (*case*)

           item_to_add ctxt oris pbl (*of*);

"~~~~~ fun item_to_add , args:"; val (ctxt, o_model, i_model) = (ctxt, oris, pbl);

    val max_vnt = last_elem (*this decides, for which variant initially help is given*)

      (Model_Def.max_variants o_model i_model)

    val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model

    val i_to_select = i_model

      |> filter_out (fn (_, vnts, _, _, (I_Model.Cor_POS _, _)) => member op= vnts max_vnt | _ => false)

      |> select_inc_lists

      |> hd

  (*in*)

val SOME (_, _, _, m_field, (feedb, _)) = (*case*)

   I_Model.fill_from_o o_vnts i_to_select (*of*);

(*+*)val "Cor_POS Maximum A , pen2str" = feedb |> I_Model.feedback_POS_to_string ctxt;

"~~~~~ fun fill_from_o , args:"; val (o_model, (i, vnts, bool, m_field, (feedb, pos))) =

  (o_vnts, i_to_select);

    val (m_field, all_value as [Free ("A", _)]) =

      case find_first (fn (_, _, _, descr', _) => Model_Def.descriptor_exists descr' feedb) o_model of

        SOME (_, _, m_field, _, ts) =>  (m_field, ts)

    val descr = Model_Def.get_descr feedb (*i_single has been filtered appropriately*)

  (*in*)

val false =

    (*if*) Model_Def.is_list_descr descr (*else*);

val return_fill_from_o_STEP = SOME (i, vnts, bool, m_field,

      (Inc_POS (descr, all_value), pos))

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

val (p,_,f,nxt,_,pt) = return_me_add_find_Constants;

                                      val Add_Find "Maximum A" = nxt

(** )val (p,_,f,nxt,_,pt) =( **)

(**)val return_me_Add_Find_Maximum =(**)

       me nxt p c pt;  val Add_Find "AdditionalValues [u]" = #4 return_me_Add_Find_Maximum;

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

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

      val ctxt = Ctree.get_ctxt pt p

      val (pt, p) = 

  	    case Step.by_tactic tac (pt, p) of

  		    ("ok", (_, _, ptp)) => ptp;

      (*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'), []));

val false =

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

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

    (*in*)

val [] =

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

val false =

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

val true =

      (*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 as Add_Find "AdditionalValues [u]")) =(**)

   Specify.find_next_step ptp;

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

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

      spec = refs, ...} = Calc.specify_data (pt, pos);

    val ctxt = Ctree.get_ctxt pt pos

  (*in*)

val false =

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

val true =

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

(**)val return_find_next_step_STEP as ("dummy", (Pbl, Add_Find "AdditionalValues [u]")) =(**)

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

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

  (ctxt, oris, (o_refs, refs), ( I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS 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, _) = Pre_Conds.check ctxt where_rls where_ (pbt, pbl);

  (*in*)

val false =

    (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);

val false =

      (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);

val NONE =

      (*case*) find_first (fn (_, _, _, _, (feedb, _)) => I_Model.is_error feedb) pbl (*of*);

(**)val SOME (fd, ct' as "AdditionalValues [u]") = (*case*)(**)

           item_to_add ctxt oris pbl (*of*);

"~~~~~ fun item_to_add , args:"; val (ctxt, o_model, i_model) =

  (ctxt, oris, pbl);

    val max_vnt = last_elem (*this decides, for which variant initially help is given*)

      (Model_Def.max_variants o_model i_model)

    val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model

    val i_to_select = i_model

      |> filter_out (fn (_, vnts, _, _, (I_Model.Cor_POS _, _)) => member op= vnts max_vnt | _ => false)

      |> select_inc_lists

(*ERROR*)val "[\n(3, [1, 2, 3], false ,#Find, (Inc_POS AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_POS Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_POS SideConditions [] [__=__, __=__], Position.T))]"

 = i_to_select |> I_Model.to_string_POS ctxt(*ERROR*)

  (*in*)

val false =

    (*if*) i_to_select = []

val SOME (_, _, _, m_field, (feedb, _)) = (*case*)

   I_Model.fill_from_o o_vnts (hd i_to_select) (*of*);

"~~~~~ fun fill_from_o , args:";

(*==================== see test/../i-model.sml --- fun item_to_add ===========================*)

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

val (p,_,f,nxt,_,pt) = return_me_Add_Find_Maximum; 

                                      val Add_Find "AdditionalValues [u]" = nxt

val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u, v]" = nxt;(*ERROR after repairing item_to_add, investigate in testcode above*)

val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)" = nxt;

val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" = nxt;

val return_me_Add_Relation_SideConditions as (_, _, _, Specify_Theory "Diff_App", _, _)

                     = me nxt p c pt;

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

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

      val ctxt = Ctree.get_ctxt pt p;

(**)  val (pt, p) = (**) 

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

(**) 		    ("ok", (_, _, ptp)) => ptp (**) ;

   (*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'), [])) (*of*);

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

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

      (*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 as Specify_Theory "Diff_App")) =

   Specify.find_next_step ptp;

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

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

      spec = refs, ...} = Calc.specify_data (pt, pos);

    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 ("dummy", (Pbl, tac as Specify_Theory "Diff_App")) =( **)

(**)val return_for_problem =(**)

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

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

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

  (ctxt, oris, (o_refs, refs), (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS 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 [Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $

  Free ("fixes", _)] = where_;

(** )val (preok, _) =( **)

(**)return_check =(**)

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

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

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

  (ctxt, where_rls, where_, (pbt, pbl));

(*+*)val "[0 < fixes]" = pres |> UnparseC.terms ctxt

(*+*)val "[\"(#Given, (Constants, fixes))\", \"(#Find, (Maximum, maxx))\", \"(#Find, (AdditionalValues, vals))\", \"(#Relate, (Extremum, extr))\", \"(#Relate, (SideConditions, sideconds))\"]"

(*+*)  = model_patt |> Model_Pattern.to_string ctxt

(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"

 = i_model |> I_Model.to_string_POS ctxt

val return_make_environments as (_, (env_subst, env_eval)) =

           Pre_Conds.make_environments model_patt i_model

(*+*)val [(Free ("fixes", T1), Free ("r", T2))] = env_subst (*?!? Const*)

(*+*)val Type ("Real.real", []) = T1

(*+*)val Type ("Real.real", []) = T2

(*+*)val [(Free ("r", T2), Const ("Num.numeral_class.numeral", _) $ _)] = env_eval

(*+*)val Type ("Real.real", []) = T2

val (_, (env_subst, env_eval)) = return_make_environments;

(*|||----------------- contine check -----------------------------------------------------*)

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

(*+*)val [(true, Const ("Orderings.ord_class.less", _) $

  Const ("Groups.zero_class.zero", _) $ Free ("r", _))] = pres_subst

      val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst

(*+*)val [(true,

     Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $

       (Const ("Num.numeral_class.numeral", _) $ _))] = full_subst

      val evals = map (eval ctxt where_rls) full_subst

val return_check_STEP = (foldl and_ (true, map fst evals), pres_subst)

(*\\\\\ \\------------ step into check -------------------------------------------------\\*)

    val (preok as true, _) = return_check

(*||||| |------------- contine.. for_problem -------------------------------------------------*)

val false =

    (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);

val false =

      (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);

val NONE =

      (*case*) find_first (fn (_, _, _, _, (feedb, _)) => I_Model.is_error feedb) pbl (*of*);

  (*case*) item_to_add ctxt oris pbl (*of*);

"~~~~~ fun item_to_add , args:"; val (ctxt, o_model, i_model) = (ctxt, oris, pbl);

(*+*)val "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), \n(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), \n(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), \n(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"

 = o_model |> O_Model.to_string ctxt

(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"

 = i_model |> I_Model.to_string_POS ctxt

    val max_vnt as 1= last_elem (*this decides, for which variant initially help is given*)

      (Model_Def.max_variants o_model i_model)

    val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model

(*+*)val "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), \n(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), \n(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"

 = o_vnts |> O_Model.to_string ctxt

    val i_to_select = i_model

      |> filter_out (fn (_, vnts, _, _, (I_Model.Cor_POS _, _)) => member op= vnts max_vnt | _ => false)

      |> select_inc_lists

val true =

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

val return_for_problem_STEP = NONE

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

val calling_code = return_for_problem;

(*-------------------- stopped after ERROR found ---------------------------------------------*)

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

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

val (p, _, f, nxt, _, pt) = return_me_Add_Relation_SideConditions

                                      val Specify_Theory "Diff_App" = nxt;

val return_me_Specify_Theory

                     = me nxt p c pt; val Specify_Problem ["univariate_calculus", "Optimisation"] = #4 return_me_Specify_Theory;

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

"~~~~~ fun me , args:"; val (tac as Specify_Theory "Diff_App", p, _, pt) = (nxt, p, c, pt);

      val ctxt = Ctree.get_ctxt pt p;

(*      val (pt, p) = *)

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

(*		    ("ok", (_, _, ptp)) => ptp *)

val return_Step_by_tactic =

      Step.by_tactic tac (pt, p);

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

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

    (*case*) Specify_Step.check tac (pt, p) (*of*);

(*||------------------ contine Step_by_tactic ------------------------------------------------*)

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

val ("ok", (_, _, ptp)) = return_Step_by_tactic;

(*|------------------- continue me Specify_Theory --------------------------------------------*)

val ("ok", (ts as (_, _, _) :: _, _, _)) =

    (*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'), [])) (*of*);

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

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

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

(*+*)val Specify_Theory "Diff_App" = tac;

"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Theory dI), (pt, pos as (_, Pbl)))

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

      val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of

        PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>

          (oris, dI, dI', pI', probl, ctxt)

	    val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');

      val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI

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

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

val (p,_,f,nxt,_,pt) = return_me_Specify_Theory;

val return_me_Specify_Problem (* keep for continuing me *)

                     = me nxt p c pt; val Specify_Method ["Optimisation", "by_univariate_calculus"] = #4 return_me_Specify_Problem;

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

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

      val ctxt = Ctree.get_ctxt pt p

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

(**)    val return_by_tactic =(**) (*case*)

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

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

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

    (*case*)

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

"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));

  (*if*) Tactic.for_specify tac (*then*);

Specify_Step.check tac (ctree, pos);

"~~~~~ fun check , args:"; val ((Tactic.Specify_Problem pID), (pt, pos as (p, _)))

  = (tac, (ctree, pos));

		    val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of

		      Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}

		        => (oris, dI, pI, dI', pI', itms)

	      val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');

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

val ("ok", (_, _, ptp as (pt, p))) = return_by_tactic (* kept for continuing me *);

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

      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 return_complete_for =(**)

(** )  val (o_model, ctxt, i_model) =( **)

Specify_Step.complete_for id (pt, pos);

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

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

(*+*)val ["Optimisation", "by_univariate_calculus"] = mID

    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 return_match_itms_oris = (**)

(** )val (_, (i_model, _)) = ( **)

     M_Match.by_i_models ctxt o_model' (I_Model.OLD_to_POS i_prob, I_Model.OLD_to_POS i_prob)

              (m_patt, where_, where_rls);

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

"~~~~~ fun by_i_models, args:"; val (ctxt, o_model, (pbl_imod, met_imod), (m_patt, where_, where_rls)) =

  (ctxt, o_model', (I_Model.OLD_to_POS i_prob, I_Model.OLD_to_POS i_prob), (m_patt, where_, where_rls));

(**)val return_fill_method =(**)

(** )val met_imod =( **)

           fill_method o_model (pbl_imod, met_imod) m_patt;

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

"~~~~~ fun fill_method , args:"; val (o_model, (pbl_imod, met_imod), met_patt) =

  (o_model, (pbl_imod, met_imod), m_patt);

(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"

 = pbl_imod |> I_Model.to_string_POS ctxt

(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"

 = met_imod |> I_Model.to_string_POS ctxt

(**)val return_max_variants =(**)

(** )val pbl_max_vnts as [2, 1] =( **)

 Model_Def.max_variants o_model pbl_imod;

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

"~~~~~ fun max_variants , args:"; val (o_model, i_model) = (o_model, pbl_imod);

      val all_variants as [1, 2, 3] =

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

          |> flat

          |> distinct op =

      val variants_separated = map (filter_variants' i_model) all_variants

(*+*)val ["[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]",

          "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]",

          "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T))]"]

 = variants_separated |> map (I_Model.to_string_POS ctxt)

      val sums_corr as [5, 5, 4] = map (cnt_corrects) variants_separated

      (*----------------#--#--#*)

      (*---------------------^-------^-------^*)

      val sum_variant_s as [(5, 1), (5, 2), (4, 3)] = arrange_args sums_corr (1, all_variants)

      val max_first as [(5, 2), (5, 1), (4, 3)] = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)

      (*----------------##====--##====--//////---------^^^^*)

      (*------------^--^-#-------#*)

      val maxes as [2, 1] = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first

        |> map snd

val return_max_variants = maxes

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

val pbl_max_vnts as [2, 1] = return_max_variants;

    (*probably pbl/met_imod = [], so take met_patt; if empty return Sup*)

    val i_from_met = map (fn (_, (descr, _)) => (*order from met_patt*)

      Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt (*\<longrightarrow> right order for args*)

(*+MET: Sup..*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n(0, [], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n(0, [], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"

  = i_from_met |> I_Model.to_string_POS ctxt

    val met_max_vnts as [2, 1] = Model_Def.max_variants o_model i_from_met;

    val max_vnt as 2 = hd (inter op= pbl_max_vnts met_max_vnts);

    (*add items from pbl_imod (without overwriting existing items in met_imod)*)

val return_add_other = map (

           add_other max_vnt pbl_imod) i_from_met;

(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"

  = return_add_other |> I_Model.to_string_POS ctxt;

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

"~~~~~ fun add_other_5 , args:"; val (max_vnt, i1_model, (i2, _, bool2, m_field2, (Sup_POS (descr2, ts2), pos2))) =

  (max_vnt, pbl_imod, nth 5 i_from_met);

(*+*)val Const ("Input_Descript.FunctionVariable", _) = descr2;

val (_, vnts1, _, _, (feedb1, _)) = (i2, [], bool2, m_field2, (Sup_POS (descr2, ts2), pos2))

val SOME (descr1 as (Const ("Input_Descript.FunctionVariable", _)) ) =

      get_dscr_opt feedb1

val true =

        descr1 = descr2

val true =

          Model_Def.member_vnt vnts1 max_vnt

val NONE =

    find_first (fn (_, vnts1, _, _, (feedb1, _)) => case get_dscr_opt feedb1 of

          NONE => false

        | SOME descr1 => descr1 = descr2 andalso Model_Def.member_vnt vnts1 max_vnt) i1_model

val return_add_other_1 = (i2, [max_vnt], bool2, m_field2, (Sup_POS (descr2, ts2), pos2))

val check as true = return_add_other_1 = nth 5 return_add_other

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

    val i_from_pbl = return_add_other

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

val return_fill_method_step = filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) i_from_met

(*+MET: dropped ALL DUE TO is_empty_single_POS*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]" =

  return_fill_method_step |> I_Model.to_string_POS ctxt

(*+*)val                                             "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"

 = return_fill_method |> I_Model.to_string_POS ctxt;

return_fill_method_step = return_fill_method; (*latter is correct, did not investigate further*)

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

val (_, (i_model, _)) = return_match_itms_oris;

(*||------------------ continue. complete_for ------------------------------------------------*)

      val (o_model, ctxt, i_model) = return_complete_for

(*+isa*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"

 = i_model |> I_Model.to_string_POS ctxt(*+isa*)

(*+isa2:MET.Mis* ) val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(7 ,[1] ,false ,#Given ,Mis FunctionVariable funvar), \n(10 ,[1, 2] ,false ,#Given ,Mis Input_Descript.Domain doma), \n(12 ,[1, 2, 3] ,false ,#Given ,Mis ErrorBound err)]" =

  i_model |> I_Model.to_string ctxt ( *+isa2*)

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

      val (o_model, ctxt, i_model) = return_complete_for

(*|------------------- continue. complete_for ------------------------------------------------*)

val return_complete_for_step = (o_model', ctxt', i_model)

val (o_model'_step, i_model_step) = (#1 return_complete_for_step, #3 return_complete_for_step)

val (o_model', i_model) = (#1 return_complete_for, #3 return_complete_for)

;

(*+*)if (o_model'_step, i_model_step) = (o_model', i_model)

(*+*)then () else error "return_complete_for_step <> return_complete_for";

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

val (p,_,f,nxt,_,pt) = return_me_Specify_Problem

val return_me_Specify_Method

                     = me nxt p c pt; val Add_Given "FunctionVariable a" = #4 return_me_Specify_Method;

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

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

(*+*)val "[]" =(*+*) get_obj g_met pt (fst p) |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt

      val ctxt = Ctree.get_ctxt pt p

      val (pt, p) = 

  	    case Step.by_tactic tac (pt, p) of

  		    ("ok", (_, _, ptp)) => ptp;

(*quick step into --> me_Specify_Method*)

(*+*)val Specify_Method ["Optimisation", "by_univariate_calculus"] = tac;

(*    Step.by_tactic*)

"~~~~~ fun by_tactic , args:"; val () = ();

(*    Step.check*)

"~~~~~ fun check , args:"; val () = ();

(*Specify_Step.check (Tactic.Specify_Method*)

"~~~~~ fun check , args:"; val () = ();

(*Specify_Step.complete_for*)

"~~~~~ fun complete_for , args:"; val () = ();

(* M_Match.by_i_models*)

"~~~~~ fun by_i_models , args:"; val () = ();

(*+*)val  "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"

 = get_obj g_met pt (fst p) |> I_Model.OLD_to_POS |> I_Model.to_string_POS  ctxt;

         (*case*)

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

(*//------------------ step into Step.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*);

      Step.switch_specify_solve p_ (pt, ip);

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

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

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

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

    val (_, (p_', tac)) =

   Specify.find_next_step ptp;

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

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

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

      spec = refs, ...} = Calc.specify_data (pt, pos);

    val ctxt = Ctree.get_ctxt pt pos;

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

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

(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"

 = met |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt

(**)val ("dummy", (Met, Add_Given "FunctionVariable a")) =(**)

   Specify.for_method ctxt oris (o_refs, refs) (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met);

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

"~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (_, met))

  = (ctxt, oris, (o_refs, refs), (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met));

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

    val {model, where_rls, where_, ...} = MethodC.from_store ctxt cmI;    (*..MethodC ?*)

    val (preok, _) = Pre_Conds.check ctxt where_rls where_ (model, met);

val NONE =

    (*case*) find_first (I_Model.is_error o #1 o #5) met (*of*);

(** )SOME (fd, ct') =( **)

(**)val return_item_to_add =(**)

      (*case*)

   Specify.item_to_add  ctxt oris met (*of*);

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

"~~~~~ fun item_to_add , args:"; val (ctxt, o_model, i_model) = (ctxt, oris, met);

(*+*)val "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n(2, [\"1\", \"2\", \"3\"], #Given, Maximum, [\"A\"]), \n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n(4, [\"1\", \"2\", \"3\"], #Given, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n(5, [\"1\", \"2\"], #Given, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n(6, [\"3\"], #Given, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n(7, [\"1\"], #Given, FunctionVariable, [\"a\"]), \n(8, [\"2\"], #Given, FunctionVariable, [\"b\"]), \n(9, [\"3\"], #Given, FunctionVariable, [\"\<alpha>\"]), \n(10, [\"1\", \"2\"], #Given, Input_Descript.Domain, [\"{0<..<r}\"]), \n(11, [\"3\"], #Given, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n(12, [\"1\", \"2\", \"3\"], #Given, ErrorBound, [\"\<epsilon> = 0\"])]"

 = oris |> O_Model.to_string ctxt

(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"

 = i_model |> I_Model.to_string_POS ctxt

    val max_vnt = last_elem (*this decides, for which variant initially help is given*)

      (Model_Def.max_variants o_model i_model)

    val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model

    val i_to_select = i_model

      |> filter_out (fn (_, vnts, _, _, (I_Model.Cor_POS _, _)) => member op= vnts max_vnt | _ => false)

      |> select_inc_lists

(*+*)val "[\n(0, [2], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS ErrorBound, Position.T))]"

 = i_to_select |> I_Model.to_string_POS ctxt

val false =

    (*if*) i_to_select = [] (*else*);

(** )val SOME (_, _, _, m_field, (feedb, _)) =( **)

(**)val return_fill_from_o = (**)

      (*case*) I_Model.fill_from_o o_vnts (hd i_to_select) (*of*);

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

"~~~~~ fun fill_from_o , args:"; val (o_model, (i, vnts, bool, _, (feedb, pos))) =

  (o_vnts, (hd i_to_select));

    val (m_field, all_value) =

      case find_first (fn (_, _, _, descr', _) => Model_Def.descriptor_exists descr' feedb) o_model of

        SOME (_, _, m_field, _, ts) =>  (m_field, ts)

    val descr = Model_Def.get_descr feedb (*i_single has been filtered appropriately*)

val false =

    (*if*) Model_Def.is_list_descr descr (*else*);

val return_fill_from_o_STEP = SOME (i, vnts, bool, m_field, (Cor_POS (descr, all_value), pos))

(*-------------------- stopped after ERROR found ---------------------------------------------*)

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

val SOME (_, _, _, m_field, (feedb, _)) = return_fill_from_o

(*||||| ||------------ step into item_to_add -----------------------------------------------//*)

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

val return_item_to_add_STEP as SOME ("#Given", "FunctionVariable a") =

  SOME (m_field, feedb |> I_Model.feedb_args_to_string ctxt)

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

val SOME (fd, ct') = return_item_to_add;

(*||||| |------------- contine.. Step.for_method ---------------------------------------------*)

val return_for_method_STEP = ("dummy", (Pos.Met, P_Model.mk_additem fd ct'))

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

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

val (p,_,f,nxt,_,pt) = return_me_Specify_Method;

                                      val Add_Given "FunctionVariable a" = nxt;

val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Input_Descript.Domain {0<..<r}" = nxt

val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "ErrorBound (\<epsilon> = 0)" = nxt;

(*ErRoR type_of: type mismatch in application, bool, bool list, (#) [r = 7] --> 200a-start-method

val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method xxx = nxt

*)