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

   Author: Walther Neuper 1105

   (c) copyright due to lincense terms.

Note: This test --- steps into me --- more than once;

  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.

*)

open Test_Code

open Pos

open Ctree

open Tactic

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>]" :: 

     "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 (KEStore_Elems.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];

val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(model, refs)]; val Model_Problem = nxt;

val c = [];

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

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

"~~~~~ fun me , args:"; val (tac, (p:Pos.pos'), (_:Test_Code.NEW), (pt:Ctree.ctree)) = (nxt, p, c, pt);

    val (pt, p) = 

      (*ERROR Specify.item_to_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt ... see 100-init-rootpbl.sml*)

	    case Step.by_tactic tac (pt,p) of

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

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

    (*case*)

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

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

val (ts'''', (pt'''', p'''')) = (ts, (pt, p)); (* keep for continuing me Model_Problem *)

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

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

    val pIopt = get_pblID (pt,ip);

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

      val _ = (*case*) tacis (*of*);

      val SOME _ = (*case*) pIopt (*of*);

    val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =

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

    val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =

      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;

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

   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 cdI = if dI = ThyC.id_empty then dI' else dI;

    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 {ppc = mpc, ...} = MethodC.from_store ctxt cmI

    val (preok, _) = Pre_Conds.check where_rls where_ pbl 0;

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

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

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

        (*case*)

   Specify.item_to_add (ThyC.get_theory_PIDE ctxt

            (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);

"~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)

  = ((ThyC.get_theory_PIDE ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, pbt, pbl);

      fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"

      fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v

      fun test_id ids r = member op= ids (#1 (r : O_Model.single))

      fun test_subset itm (_, _, _, d, ts) = 

        (I_Model.descriptor (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.o_model_values (#5 itm), ts)

      fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false

        | false_and_not_Sup (_, _, false, _, _) = true

        | false_and_not_Sup _ = false

      val v = if itms = [] then 1 else I_Model.max_variant itms

      val vors = if v = 0 then oris else filter (testr_vt v) oris

      val vits =

        if v = 0

        then itms                                 (* because of dsc without dat *)

  	    else filter (testi_vt v) itms;                             (* itms..vat *)

      val icl = filter false_and_not_Sup vits;                    (* incomplete *)

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

val SOME ori =

        (*case*) find_first (test_subset (hd icl)) vors (*of*);

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

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

(*-------------------- continue with me Model_Problem ----------------------------------------*)

"~~~~~ continue fun me Model_Problem";  val (ts, (p, pt)) = (ts'''', (p'''', pt''''));

val tacis as (_::_) =

        (*case*) ts (*of*);

          val (tac, _, _) = last_elem tacis

val return = (p, [] : NEW,

           TESTg_form ctxt (pt, p), tac, Celem.Sundef, pt);

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

    val (form, _, _) = ME_Misc.pt_extract ctxt ptp

val Ctree.ModSpec (_, p_, _, gfr, pre, _) =

    (*case*) form (*of*);

(*+*)val Pos.Pbl = p_;

    Test_Out.PpcKF (  (Test_Out.Problem [],

 			P_Model.from (Proof_Context.theory_of ctxt) gfr pre));

   P_Model.from (Proof_Context.theory_of ctxt) gfr pre;

"~~~~~ fun from , args:"; val (thy, itms, pre) = ((Proof_Context.theory_of ctxt), gfr, pre);

    fun coll ppc [] = ppc

      | coll ppc ((_, _, _, field, itm_) :: itms) =

        coll (add_sel_ppc thy field ppc (item_from_feedback thy itm_)) itms;

 val gfr = coll P_Model.empty itms;

"~~~~~ fun coll , args:"; val (ppc, ((aaa, bbb_,ccc_, field, itm_) :: itms))

  = (P_Model.empty, itms);

(*+*)val 4 = length itms;

(*+*)val itm = nth 1 itms;

           coll P_Model.empty [itm];

"~~~~~ fun coll , iterate:"; val (ppc, ((aaa, bbb_,ccc_, field, itm_) :: []))

  = (P_Model.empty, [itm]);

          (add_sel_ppc thy field ppc (item_from_feedback thy itm_));

"~~~~~ fun add_sel_ppc , args:"; val ((_: theory), sel, {Given = gi, Where = wh, Find = fi, With = wi, Relate = re}, x )

  = (thy, field, ppc, (item_from_feedback thy itm_));

   P_Model.item_from_feedback thy itm_;

"~~~~~ fun item_from_feedback , args:"; val (thy, (I_Model.Inc ((d, ts), _))) = (thy, itm_);

  P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)));

(*-------------------- stop step into me Model_Problem ---------------------------------------*)

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

val (p,_,f,nxt,_,pt) = me nxt''' p''' c pt'''; val Add_Find "Maximum A" = nxt;

val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u]" = nxt;

val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [v]" = nxt;

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 (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Diff_App" = nxt;

val (p''',_,f,nxt''',_,pt''') = me nxt p [1] pt; val Specify_Problem ["univariate_calculus", "Optimisation"] = nxt''';

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

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

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

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

  = (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_PIDE ctxt (if dI' = ThyC.id_empty then dI else dI');

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

(*-------------------- stop step into me Specify_Theory --------------------------------------*)

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

val (p'''',_,f'''',nxt'''',_,pt'''') = me nxt''' p''' c pt'''; val Specify_Method ["Optimisation", "by_univariate_calculus"] = nxt'''';

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

  	    (*case*)

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

"~~~~~ 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_PIDE ctxt (if dI' = ThyC.id_empty then dI else dI');

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

(*-------------------- stop step into me Specify_Problem -------------------------------------*)

val (p, pt, nxt) = (p''''', pt''''', nxt'''); (* 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 (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, ctxt,

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

    val ctxt = Ctree.get_ctxt ctree pos

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

    val {ppc = m_patt, pre, prls, ...} = 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 thy = ThyC.get_theory_PIDE ctxt dI

    val (_, (i_model, _)) = M_Match.match_itms_oris thy i_prob (m_patt, pre, prls) o_model';

(*-------------------- stop step into me Specify_Problem -------------------------------------*)

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

val (p''',_,f,nxt''',_,pt''') = me nxt'''' p'''' c pt''''; val Add_Given "FunctionVariable a" = nxt''';

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

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

      val ctxt = Ctree.get_ctxt pt p

      val (pt, p) = 

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

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

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

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

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

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

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

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

    val {ppc = mpc, prls, pre, ...} = MethodC.from_store ctxt cmI;    (*..MethodC ?*)

    val (preok, _) = Pre_Conds.check prls pre pbl 0;

val NONE =

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

      (*case*)

   Specify.item_to_add (ThyC.get_theory_PIDE ctxt 

     (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);

"~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)

  = ((ThyC.get_theory_PIDE ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);

(*-------------------- stop step into me Specify_Method --------------------------------------*)

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

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;

(*

  nxt would be Tactic.Apply_Method, which tries to determine a next step in the ***Program***,

  but the Program is not yet perfectly implemented.

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

*)