(* Title:  "Specify/i-model.sml"

   Author: Walther Neuper

   (c) due to copyright terms

*)

"-----------------------------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"----------- survey on handling of input terms -------------------------------------------------";

"----------- investigate fun add_single in I_Model ---------------------------------------------";

"----------- build I_Model.init_POS -----------------------------------------------------------";

"----------- exercise preparing I_Model.is_complete --------------------------------------------";

"----------- build I_Model.is_complete_OLD -----------------------------------------------------";

"----------- build I_Model.s_make_complete -----------------------------------------------------";

"----------- check I_Model.s_make_complete for ([], [])-----------------------------------------";

"----------- fun item_to_add: Maximum-exammple -------------------------------------------------";

"----------- fun item_to_add: Biegelinie-example -----------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

open I_Model;

open Test_Code;

open Tactic;

open Pos; 

open Ctree; 

open Pre_Conds; 

open Specify; 

val ctxt = Proof_Context.init_global @{theory Biegelinie};

"----------- survey on handling of input terms -------------------------------------------------";

"----------- survey on handling of input terms -------------------------------------------------";

"----------- survey on handling of input terms -------------------------------------------------";

(*//------------------ survey on handling of input terms in specify-phase ------------------\\*)

(*        * ---------- handling of lists -----------------------------------------------------*)

(*         ** ---------- current situation ---------------------------------------------------*)

(** )(*---- from tests -------------------------------------------vvvvvvv *);

val o_single as (3, [1, 2, 3], "#Find", descr, [t1, t2]) = (nth 3 o_model)

val "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"])"

  = O_Model.single_to_string ctxt o_single

val "[u]" = UnparseC.term ctxt t1

val "[v]" = UnparseC.term ctxt t2

( **)

val t as (descr $ vals_term) = @{term "AdditionalValues [u, v]"}

val true = (*if*)Model_Def.is_list_descr descr(*else*);

val values = vals_term |> TermC.isalist2list |> map TermC.single_to_list

val feedb = Cor_POS (descr, values)

val "Cor_POS AdditionalValues [u, v] , pen2str" = feedb |> feedback_POS_to_string ctxt

(*get values out of feedback:*)

val [Free ("u", _), Free ("v", _)] = (values |> map TermC.isalist2list  |> flat): term list

(*         ** ---------- wanted situation ----------------------------------------------------*)

val t as (descr $ vals_term) = @{term "AdditionalValues [u, v]"}

val true = (*if*)Model_Def.is_list_descr descr(*else*);

val values = [vals_term]

val feedb = Cor_POS (descr, values)

val "Cor_POS AdditionalValues [u, v] , pen2str" = feedb |> feedback_POS_to_string ctxt (*OK*)

(*get values out of feedback:*)

val "[u, v]" = values |> map (UnparseC.term ctxt) |> hd

(*        * ---------- handling of NON-lists -------------------------------------------------*)

(*         ** ---------- current situation ---------------------------------------------------*)

(** )(*---- from tests -------------------------------------------vvvvvvv *);

val o_single as (2, [1, 2, 3], "#Find", Const ("Input_Descript.Maximum", _), [Free ("A", _)])

  = (nth 2 o_model) 

( **)

val t as (descr $ vals_term) = @{term "Maximum A"}

val false = (*if*)Model_Def.is_list_descr descr(*then*);

val values = [vals_term]

val feedb = Cor_POS (descr, values)

val "Cor_POS Maximum A , pen2str" = feedb |> feedback_POS_to_string ctxt (*OK*)

(*get values out of feedback:*)

val "A" = values |> map (UnparseC.term ctxt) |> hd

(*         ** ---------- wanted situation ----------------------------------------------------*)

val t as (descr $ vals_term) = @{term "Maximum A"}

val false = (*if*)Model_Def.is_list_descr descr(*then*);

val values = [vals_term]

val feedb = Cor_POS (descr, values)

val "Cor_POS Maximum A , pen2str" = feedb |> feedback_POS_to_string ctxt (*OK*)

(*get values out of feedback:*)

val "A" = values |> map (UnparseC.term ctxt) |> hd;

(*\\------------------ survey on handling of input terms in specify-phase ------------------//*)

"----------- investigate fun add_single in I_Model -------------------------------------------";

"----------- investigate fun add_single in I_Model -------------------------------------------";

"----------- investigate fun add_single in I_Model -------------------------------------------";

val f_model = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

	"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",

	"FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",

  "AbleitungBiegelinie dy"];

val f_spec = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);

(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(f_model, f_spec)]; (*\<rightarrow>Model_Problem*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "Traegerlaenge L"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "Streckenlast q_0"*)

(*[], Pbl*)val return_me_Add_Given =

           me nxt p [] pt; (*\<rightarrow>Add_Find "Biegelinie y"*)

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

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

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

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

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

Step_Specify.by_tactic tac' ptp;

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

val ("ok", ([(Add_Given "Streckenlast q_0", _, _)], [], _)) = (*case*)

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

"~~~~~ 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 (i_model, m_patt) =

       if p_ = Pos.Met then

         (met,

           (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)

       else

         (pbl,

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

;

(*+*)if O_Model.to_string @{context} oris = "[\n" ^

  "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^

  "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

  "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^

  "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^

  "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^

  "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^

  "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"

(*+*)then () else error "INITIAL O_Model CHANGED";

(*+*)val "[\n(1, [1], true ,#Given, (Cor_POS Traegerlaenge L , pen2str, Position.T)), \n(2, [1], false ,#Given, (Inc_POS Streckenlast __, Position.T)), \n(3, [1], false ,#Find, (Inc_POS Biegelinie __, Position.T)), \n(4, [1], false ,#Relate, (Inc_POS Randbedingungen [] [__=__, __=__], Position.T))]"

 = pbl |> I_Model.to_string_POS ctxt

val return_check_single = (*case*)

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

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

"~~~~~ fun check_single , args <>[]:"; val (ctxt, m_field, o_model, i_model, m_patt, str)

  = (ctxt, m_field, oris, (I_Model.TEST_to_OLD i_model), m_patt, ct);

      val (t as (descriptor $ _)) = Syntax.read_term ctxt str

        handle ERROR msg => error (msg (*^ Position.here pp*))

val SOME m_field' =

        (*case*) Model_Pattern.get_field descriptor m_patt;

val false =

          (*if*) m_field <> m_field' (*else*);

        val ("", ori', all) =(**)

          (*case*) O_Model.contains ctxt m_field o_model t (*of*);

(*+*)O_Model.single_to_string @{context} ori';

(*+*)val [Free ("q_0", _)] = all;

(**)val ("", itm) =(**)

 (*case*) is_notyet_input ctxt (OLD_to_POS i_model) all ori' m_patt (*of*);

(*+*)val (2, [1], true, "#Given", (Cor_POS (Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]), _)) = itm

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

val I_Model.Add i_single = return_check_single

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

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

              [], (pt', pos)));

(*-------------------- stop into me Add_Given ------------------------------------------------*)

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

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

(*ErRoR Clash of types "_ \<Rightarrow> _" and "_ list", Randbedingungen :: bool list \<Rightarrow> una, y :: real \<Rightarrow> real* )

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]"*)

(* final test ... BEFORE BREAKING ELEMENTWISE INPUT TO LISTS* )

if p = ([], Pbl) then

  case nxt of Add_Relation "Randbedingungen [y 0 = 0]" => () | _

    => error "investigate fun add_single CHANGED 1"

else error "investigate fun add_single CHANGED 2"

( * final test ... AFTER BREAKING ELEMENTWISE INPUT TO LISTS*)

if p = ([], Pbl) then

  case nxt of Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" => () | _

    => error "investigate fun add_single CHANGED 1"

else error "investigate fun add_single CHANGED 2"

( *ErRoR Clash of types "_ \<Rightarrow> _" and "_ list", Randbedingungen :: bool list \<Rightarrow> una, y :: real \<Rightarrow> real*)

"----------- build I_Model.init_POS -----------------------------------------------------------";

"----------- build I_Model.init_POS -----------------------------------------------------------";

"----------- build I_Model.init_POS -----------------------------------------------------------";

(*/---------------------------------------- mimic input from PIDE -----------------------------\*)

(* Test_Example "Diff_App-No.123a" (*complete Model, empty References*) *)

val in_refs as (thy_id, probl_id, meth_id) = ("__", "__/__", "__/__")

val thy = @{theory}

val model_input = (*type Position.T is hidden, thus redefinition*)

 [("#Given", [("Constants [r = 7]", Position.none)]),

  ("#Where", [("0 < r", Position.none)]),

  ("#Find",

   [("Maximum A", Position.none), ("AdditionalValues [u, v]", Position.none)]),

  ("#Relate",

   [("Extremum (A = 2 * u * v - u \<up> 2)", Position.none),

    ("SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", Position.none)])]

: (Model_Pattern.m_field * (string * Position.T) list) list

val example_id = "Diff_App-No.123a";

(*----------------------------------------- init state -----------------------------------------*)

set_data CTbasic_POS.EmptyPtree @{theory Calculation};

(*\---------------------------------------- mimic input from PIDE -----------------------------/*)

val CTbasic_POS.EmptyPtree =

              (*case*) the_data @{theory Calculation} (*of*);

(* Calculation..*)

"~~~~~ fun init_ctree , args:"; val (thy, example_id) = (thy, example_id);

      val example_id' = References_Def.explode_id example_id

      val (_, (formalise as (model, refs as (thy_id, probl_id, meth_id)))) =

        Store.get (Know_Store.get_expls @{theory}) example_id' example_id' 

      val {model = model_patt, ...} = Problem.from_store (Proof_Context.init_global thy) probl_id

      val (o_model, ctxt) = O_Model.init thy model model_patt

;

(*+*)o_model: O_Model.T; (* |> O_Model.to_string @{context}*)

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

(*+*)  refs       

      val empty_i_model =

   I_Model.init_POS ctxt o_model model_patt;

"~~~~~ fun init_POS , args:"; val (ctxt, model_patt) = (ctxt, model_patt);

;

(*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_POS Constants [] [__=__, __=__], 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.to_string_POS @{context} empty_i_model;

"----------- exercise preparing I_Model.is_complete --------------------------------------------";

"----------- exercise preparing I_Model.is_complete --------------------------------------------";

"----------- exercise preparing I_Model.is_complete --------------------------------------------";

fun check str = if str = "true" then true else false

fun complete str = if str = "true" then true else false

val i_model_envs_v = [("i_model_envs-1", 11), ("i_model_envs-2", 12), ("i_model_envs-3", 13)]

val result_all_variants =

  map (fn (a, variant) => if check a andalso complete a then SOME [variant] else NONE) i_model_envs_v;

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

;

val [NONE, NONE, NONE] = result_all_variants: int list option list

(*+*)val true = forall is_none result_all_variants

val variants_complete =

  if forall is_none result_all_variants

  then NONE

  else SOME (map (fn x => if is_some x then [the x] else []) result_all_variants |> flat |> flat)

;

val NONE = variants_complete: int list option

(*more significant result ..*)

val result_all_variants = [SOME [11], NONE, SOME [13]]: int list option list

(*

in case the result is null, no I_Model is_complete,

in case the result contains more than 1 variant, this might determine the decision for MethodC.

*)

val variants_complete =

  if forall is_none result_all_variants

  then NONE

  else SOME (map (fn x => if is_some x then [the x] else []) result_all_variants |> flat |> flat)

;

val SOME [11, 13] = variants_complete: int list option;

(*/----- reactivate with CS "remove sep_variants_envs"-----\* )

"----------- build I_Model.is_complete_OLD -----------------------------------------------------";

"----------- build I_Model.is_complete_OLD -----------------------------------------------------";

"----------- build I_Model.is_complete_OLD -----------------------------------------------------";

(*see Outer_Syntax:    val (model, where_) = Model_Pattern.parse_pos_empty ctxt model_input*)

open I_Model

open Pre_Conds;

(*//------------------ test data setup -----------------------------------------------------\\*)

(*

*****************************************************************************************

***** WE FIRST MAINTAIN THE ERROR, THAT ITEMS WITH TYPE list ARE STORED AS isalist, *****

***** NOT AS term list (NECESSARY TO DETECT INCOMPLETE INPUT OF lists)              *****

*****************************************************************************************

  The ERROR occurred somewhere since introducing structure or since transition to PIDE.

*****************************************************************************************

  We complete the two single_POS "1" and "5" below and replace them in  empty_input;

  we add "6" as variant of "5" to the empty input.

  later we shall replace empty_input by partial input "AdditionalValues [v]" (u missing).

  The test intermediatly pairs (feedback_POS, Position.T) in I_Model.T_POS 

  and leaves the rest as is.

I_Model.is_complete_OLD: because PIDE gets instantiated Pre_Conds by Template.show,

  I_Model.is_complete_POS NO instantiation (done in Template.show):

  it serves to maintain the OLD test/*

*)

val thy = @{theory Calculation}

            val state =

              case the_data thy of

                  CTbasic_POS.EmptyPtree => Preliminary.init_ctree thy example_id

                | _(*state (*FOR TEST*)*) => (**)the_data thy(**)

                  (*let*)

                    val {origin = (o_model, o_ref, _), spec = spec_ref, probl, meth, ctxt, ...} =

                      CTbasic_POS.get_obj I state [(*Pos will become variable*)] |> CTbasic_POS.rep_specify_data

;

probl: Model_Def.i_model_POS 

(*[(1, [1, 2, 3], false, "#Given", (Inp_POS (Const ("Input_Descript.Constants", "bool list \<Rightarrow> nam"), "[__=__, __=__]"), {})),

   (2, [1, 2, 3], false, "#Find", (Inp_POS (Const ("Input_Descript.Maximum", "real \<Rightarrow> toreal"), "__"), {})),

   (3, [1, 2, 3], false, "#Find", (Inp_POS (Const ("Input_Descript.AdditionalValues", "real list \<Rightarrow> toreall"), "[__, __]"), {})),

   (4, [1, 2, 3], false, "#Relate", (Inp_POS (Const ("Input_Descript.Extremum", "bool \<Rightarrow> toreal"), "(__=__)"), {})),

   (5, [1, 2], false, "#Relate", (Inp_POS (Const ("Input_Descript.SideConditions", "bool list \<Rightarrow> una"), "[__=__, __=__]"), {}))]*)

;

val probl_POS = (*from above, #1 and #5,6 replaced by complete items for building code.test*)

  (1, [1,2,3], true, "#Given",

    (Cor_POS ((@{term "Constants"}, [@{term "[r = (7::real)]"(*should be "r = (7::real)"*)}]),

      (@{term "fixes::bool list"}, [@{term "[r = (7::real)]"}])), Position.none )) ::

  nth 2 probl :: nth 3 probl :: nth 4 probl ::

  (5, [1,2], true, "#Relate",

    (Cor_POS ((@{term "SideConditions"}, [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]),

      (@{term "sideconds::bool list"}, [TermC.empty])), Position.none )) ::

  (6, [3], true, "#Relate",

    (Cor_POS ((@{term "SideConditions"}, [@{term "[2 * u = r * sin \<alpha>, 2 * v = r * cos \<alpha>]"}]),

      (@{term "sideconds::bool list"}, [TermC.empty])), Position.none ))

  :: [];

val {model = model_patt, where_rls, where_ = where_OLD, ...} = (*from_store without Position.T-vv*)

  Problem.from_store ctxt (References.explode_id "univariate_calculus/Optimisation")

;

val [Const ("Orderings.ord_class.less", _(*"real \<Rightarrow> real \<Rightarrow> bool"*)) $

  Const ("Groups.zero_class.zero", _(*"real"*)) $ Free ("fixes", _(*"real"*))] = where_OLD

(*design-ERROR: "fixes" is used twice, as variable ------^^^^^^^^^^^^^^^^^^^^^^^^^^^ in pre-condition

  AND as "id" in Subst.T [("fixes", [0 < x])] *);

(model_patt |> Model_Pattern.to_string ctxt) =

 "[\"(#Given, (Constants, fixes))\", " ^

  "\"(#Find, (Maximum, maxx))\", " ^

  "\"(#Find, (AdditionalValues, vals))\", " ^

  "\"(#Relate, (Extremum, extr))\", " ^

  "\"(#Relate, (SideConditions, sideconds))\"]";

val "[0 < fixes]" = (where_OLD |> UnparseC.terms @{context})

(*\\------------------ test data setup -----------------------------------------------------//*)

(*/------------------- test on OLD algorithm (with I_Model.T_POS) --------------------------\*)

(*\------------------- test on OLD algorithm (with I_Model.T_POS) --------------------------/*)

( *\----- reactivate with CS "remove sep_variants_envs"-----/*)

"----------- build I_Model.s_make_complete -----------------------------------------------------";

"----------- build I_Model.s_make_complete -----------------------------------------------------";

"----------- build I_Model.s_make_complete -----------------------------------------------------";

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>]" :: (*INCORRECT 2 / v*)

(*---------------------------------------------,(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 (p,_,f,nxt,_,pt) = 

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

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

(*//------------------ setup test data for I_Model.s_make_complete -------------------------\\*)

val (o_model, (pbl_imod, met_imod), (pI, mI)) = case get_obj I pt (fst p) of

   PblObj {meth = met_imod, origin = (o_model, (_, pI, mI), _), probl = pbl_imod, ...}

      => (o_model, (pbl_imod, met_imod), (pI, mI))

       | _ => raise ERROR ""

val pbl_imod = [ (*2 items for creating code ---> variants [1, 2]*)

  (1, [1, 2, 3], true, "#undef", (Cor_POS (@{term Constants},

    [@{term "[r = (7::real)]"}]), Position.none)),

  (1, [1, 2], true, "#undef", (Cor_POS (@{term SideConditions},

    [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]), Position.none))]

val met_imod = [ (*1 item for creating code*)

(8, [2], true, "#undef", (Cor_POS (@{term FunctionVariable}, [@{term "b::real"}]), Position.none))]

;

(*+*)if (o_model |> O_Model.to_string @{context}) = "[\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\"])]"

then () else error "setup test data for I_Model.s_make_complete CHANGED";

(*\\------------------ setup test data for I_Model.s_make_complete -------------------------//*)

val return_s_make_complete =

           s_make_complete ctxt o_model (pbl_imod, met_imod) (pI, mI);

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

"~~~~~ fun s_make_complete , args:"; val (o_model, (pbl_imod, met_imod), (pI, mI)) =

  (o_model, (pbl_imod, met_imod), (pI, mI));

    val {model = pbl_patt, ...} = Problem.from_store ctxt pI;

    val {model = met_patt, ...} = MethodC.from_store ctxt mI;

    val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;

    val i_from_pbl = map (fn (_, (descr, _)) =>

      Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;

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

"~~~~~ fun get_descr_vnt , args:"; val (descr, vnts, i_model) =

  (@{term Constants}, pbl_max_vnts, pbl_imod);

    val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr_opt feedb of NONE => false

      | SOME descr' => if descr = descr' then true else false) i_model 

;

(*+*)filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr: I_Model.T_POS

;

val return_get_descr_vnt_1 =

    case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of

      [] => (0, [], false, "i_model_empty", (Sup_POS (descr, []), Position.none))

    | items => Library.the_single items (*only applied to model_patt, which has each descr once*)

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

(*|------------------- continue s_make_complete ----------------------------------------------*)

    val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>

      if is_empty_single_POS i_single

      then

        case get_descr_vnt' feedb pbl_max_vnts o_model of

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

            [] => raise ERROR (msg pbl_max_vnts feedb)

          | o_singles => map transfer_terms o_singles

      else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat

(*+*)val [2, 1] = vnts;

(*+*)if (pbl_from_o_model |> I_Model.to_string_POS @{context}) = "[\n" ^

  "(1, [1, 2, 3], true ,#undef, (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" ^

  "(1, [1, 2], true ,#undef, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"

then () else error "pbl_from_o_model CHANGED 1"

(*//------------------ step into map ((fn i_single -----------------------------------------\\*)

"~~~~~ fun map ((fn i_single , args:"; val (i_single as (_, _, _, _, (feedb, _))) = (nth 1 i_from_pbl);

      (*if*) is_empty_single_POS i_single (*else*);

             get_descr_vnt' feedb pbl_max_vnts o_model;

    val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>

      if is_empty_single_POS i_single

      then

        case get_descr_vnt' feedb pbl_max_vnts o_model of

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

            [] => raise ERROR (msg pbl_max_vnts feedb)

          | o_singles => map transfer_terms o_singles

      else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat

(*\\------------------ step into map ((fn i_single -----------------------------------------//*)

(*|------------------- continue s_make_complete ----------------------------------------------*)

    val i_from_met = map (fn (_, (descr, _)) =>

      Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt

;

(*+*)if (i_from_met |> I_Model.to_string_POS @{context}) = "[\n" ^

  "(0, [], false ,i_model_empty, (Sup_POS Constants [], Position.T)), \n" ^

  "(0, [], false ,i_model_empty, (Sup_POS Maximum, Position.T)), \n" ^

  "(0, [], false ,i_model_empty, (Sup_POS Extremum, Position.T)), \n" ^

  "(0, [], false ,i_model_empty, (Sup_POS SideConditions [], Position.T)), \n" ^

  "(8, [2], true ,#undef, (Cor_POS FunctionVariable b , pen2str, Position.T)), \n" ^

(*---there is 1 item already input -^^^^^^^^^^^^^^^^^^*)

  "(0, [], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n" ^

  "(0, [], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n" ^

  "(0, [], false ,i_model_empty, (Sup_POS AdditionalValues [], Position.T))]"

(*+*)then () else error "s_make_complete: from_met CHANGED";

;

    val met_max_vnts = Model_Def.max_variants o_model i_from_met;

(*+*)val [2] = met_max_vnts

    val met_max_vnt = hd met_max_vnts (*need only one for solve-phase*)

    val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>

      if is_empty_single_POS i_single

      then

        case get_descr_vnt' feedb [met_max_vnt] o_model of

            [] => raise ERROR (msg [met_max_vnt] feedb)

          | o_singles => map transfer_terms o_singles

      else [i_single (*fetched before from met_imod*)])) i_from_met |> flat

;

(*+*)if (met_from_pbl |> I_Model.to_string_POS @{context}) = "[\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" ^

  "(8, [2], true ,#undef, (Cor_POS FunctionVariable b , pen2str, Position.T)), \n" ^

  "(10, [1, 2], true ,#undef, (Cor_POS Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^

  "(12, [1, 2, 3], true ,#undef, (Cor_POS ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^

  "(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"

(*+*)then () else error "s_make_complete: met_from_pbl CHANGED";

;

val return_s_make_complete_step = (pbl_from_o_model, met_from_pbl)

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

;

if return_s_make_complete = return_s_make_complete_step

then () else error "s_make_complete: stewise construction <> value of fun"

"----------- check I_Model.s_make_complete for ([], [])-----------------------------------------";

"----------- check I_Model.s_make_complete for ([], [])-----------------------------------------";

"----------- check I_Model.s_make_complete for ([], [])-----------------------------------------";

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>]" :: (*INCORRECT 2 / v*)

(*---------------------------------------------,(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 (p,_,f,nxt,_,pt) = 

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

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

(*//------------------ setup test data for I_Model.s_make_complete -------------------------\\*)

val (o_model, (pI, mI)) = case get_obj I pt (fst p) of

   PblObj {origin = (o_model, (_, pI, mI), _), ...}

      => (o_model, (pI, mI))

       | _ => raise ERROR ""

val pbl_imod = []

val met_imod = []

;

(*+*)if (o_model |> O_Model.to_string @{context}) = "[\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\"])]"

then () else error "setup test data for I_Model.s_make_complete CHANGED";

(*\\------------------ setup test data for I_Model.s_make_complete -------------------------//*)

val return_s_make_complete =

           s_make_complete ctxt o_model (pbl_imod, met_imod) (pI, mI);

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

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

  (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt));

    val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;

    val i_from_pbl = map (fn (_, (descr, _)) =>

      Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;

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

"~~~~~ fun get_descr_vnt , args:"; val (descr, vnts, i_model) =

  (@{term Constants}, pbl_max_vnts, pbl_imod);

    val equal_descr(*for (*+*)filter (fn (_, vnts',..*): I_Model.T_POS =

                      filter (fn (_, _, _, _, (feedb, _)) => case get_dscr_opt feedb of NONE => false

      | SOME descr' => if descr = descr' then true else false) i_model 

;

(*+*)filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) (equal_descr: I_Model.T_POS)

(*+*): I_Model.T_POS

;

val return_get_descr_vnt_1 =

    case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of

      [] => (0, [], false, "i_model_empty", (Sup_POS (descr, []), Position.none))

    | items => Library.the_single items (*only applied to model_patt, which has each descr once*)

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

;

(*+*)if return_get_descr_vnt_1 = nth 1 i_from_pbl

(*+*)then () else error "return_get_descr_vnt_1 <> nth 1 i_from_pbl";

(*+*)if (i_from_pbl |> I_Model.to_string_POS @{context}) = "[\n" ^

  "(0, [], false ,i_model_empty, (Sup_POS Constants [], Position.T)), \n" ^

  "(0, [], false ,i_model_empty, (Sup_POS Maximum, Position.T)), \n" ^

  "(0, [], false ,i_model_empty, (Sup_POS AdditionalValues [], Position.T)), \n" ^

  "(0, [], false ,i_model_empty, (Sup_POS Extremum, Position.T)), \n" ^

  "(0, [], false ,i_model_empty, (Sup_POS SideConditions [], Position.T))]"

(*+*)then () else error "I_Model.s_make_complete > i_from_pbl CHANGED";

(*|------------------- continue s_make_complete ----------------------------------------------*)

    val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>

      if is_empty_single_POS i_single

      then

        case get_descr_vnt' feedb pbl_max_vnts o_model of

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

            [] => raise ERROR (msg pbl_max_vnts feedb)

          | o_singles => map transfer_terms o_singles

      else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat

(*+*)val [1, 2, 3] = vnts;

(*+*)if (pbl_from_o_model |> I_Model.to_string_POS @{context}) = "[\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" ^

  "(6, [3], true ,#Relate, (Cor_POS SideConditions [u / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>] , pen2str, Position.T))]"

then () else error "pbl_from_o_model CHANGED 2"

(*//------------------ step into map ((fn i_single -----------------------------------------\\*)

"~~~~~ fun map nth 1 ((fn i_single , args:"; val (i_single as (_, _, _, _, (feedb, _))) =

  (nth 1 i_from_pbl);

      (*if*) is_empty_single_POS i_single (*then*);

  (*case*) get_descr_vnt' feedb pbl_max_vnts o_model;

(*+*)val (0, [], false, "i_model_empty", (Sup_POS (Const ("Input_Descript.Constants", _), []), _))

  = i_single

(*+*)val true = is_empty_single_POS i_single

val return_get_descr_vnt'= (*case*)

           get_descr_vnt' feedb pbl_max_vnts o_model (*of*);

(*\\------------------ step into map ((fn i_single -----------------------------------------//*)

(*|------------------- continue s_make_complete ----------------------------------------------*)

    val i_from_met = map (fn (_, (descr, _)) =>

      Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt

(*+*)val [1, 2, 3] = pbl_max_vnts (*..? ? GOON*);

(*+*)if (i_from_met |> I_Model.to_string_POS @{context}) = "[\n" ^

  "(0, [], false ,i_model_empty, (Sup_POS Constants [], Position.T)), \n" ^

  "(0, [], false ,i_model_empty, (Sup_POS Maximum, Position.T)), \n" ^

  "(0, [], false ,i_model_empty, (Sup_POS Extremum, Position.T)), \n" ^

  "(0, [], false ,i_model_empty, (Sup_POS SideConditions [], 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" ^

  "(0, [], false ,i_model_empty, (Sup_POS AdditionalValues [], Position.T))]"

(*+*)then () else error "s_make_complete: i_from_met CHANGED";

    val met_max_vnts = Model_Def.max_variants o_model i_from_met;

(*+*)val [1, 2, 3]: variant list = met_max_vnts

    val max_vnt = hd met_max_vnts (*need only one for solve-phase*)

    val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>

      if is_empty_single_POS i_single

      then

        case get_descr_vnt' feedb [max_vnt] o_model of

            [] => raise ERROR (msg [max_vnt] feedb)

          | o_singles => map transfer_terms o_singles

      else [i_single (*fetched before from met_imod*)])) i_from_met |> flat

(*+*)val 1 = max_vnt;

(*+*)if (met_from_pbl |> I_Model.to_string_POS @{context}) = "[\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" ^

  "(7, [1], true ,#undef, (Cor_POS FunctionVariable a , pen2str, Position.T)), \n" ^

  "(10, [1, 2], true ,#undef, (Cor_POS Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^

  "(12, [1, 2, 3], true ,#undef, (Cor_POS ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^

  "(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"

(*+*)then () else error "s_make_complete: met_from_pbl CHANGED";

val return_s_make_complete_step as (pbl_imod_step, met_imod_step)=

    (filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) pbl_from_o_model,

      met_from_pbl);

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

if return_s_make_complete = return_s_make_complete_step

then () else error "s_make_complete: stewise construction <> value of fun"

;

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

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_step |> I_Model.to_string_POS @{context}

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(7, [1], true ,#undef, (Cor_POS FunctionVariable a , pen2str, Position.T)), \n(10, [1, 2], true ,#undef, (Cor_POS Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n(12, [1, 2, 3], true ,#undef, (Cor_POS ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"

 = met_imod_step |> I_Model.to_string_POS @{context};

(*** fun item_to_add: Maximum-example ====================================================== ***);

"----------- fun item_to_add: Maximum-example --------------------------------------------------";

"----------- fun item_to_add: Maximum-example --------------------------------------------------";

(*//------------------ setup test data for item_to_add Maximum-exammple --------------------\\*)

(*

(*+*)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_model |> O_Model.to_string ctxt

val true = o_model_test = o_model

*)

val ctxt = @{context}

val o_model_test = [

  (1, [1, 2, 3], "#Given",  @{term Constants},        [@{term "[r = (7::real)]"}]),

  (2, [1, 2, 3], "#Find",   @{term Maximum},          [@{term "A::real"}            ]),

  (3, [1, 2, 3], "#Find",   @{term AdditionalValues}, [@{term "[u::real]"}, @{term "[v::real]"}]),

  (4, [1, 2, 3], "#Relate", @{term Extremum},         [@{term "A = 2 * u * v - u \<up> 2"}]),

  (5, [1, 2],    "#Relate", @{term SideConditions},   [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]),

  (7, [1],       "#undef",  @{term FunctionVariable}, [@{term "a::real"}]),

  (10,[1, 2],    "#undef",  @{term Domain},           [@{term "{0<..<(r::real)}"}]),

  (12,[1, 2, 3], "#undef",  @{term ErrorBound},       [@{term "\<epsilon> = (0::real)"}]),

  (0, [1],       "#Find",   @{term solutions},        [@{term "L::real list"}])

];

(*\\------------------ setup test data for item_to_add Maximum-exammple --------------------//*)

(** fun item_to_add: Constants [r = (7::real)] ============================================== **);

val i_single : I_Model.single_POS =

((3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term Constants}, []) , Position.none)))

val SOME ("#Given", "Constants [r = 7]") = item_to_add ctxt o_model_test [i_single];

(** fun item_to_add: Maximum A ============================================================== **);

val i_single : I_Model.single_POS =

((3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term Maximum}, []) , Position.none)))

val SOME ("#Find", "Maximum A") = item_to_add ctxt o_model_test [i_single];

(** fun item_to_add: AdditionalValues [u] =================================================== **);

val i_single : I_Model.single_POS =

((3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term AdditionalValues}, []) , Position.none)))

val SOME ("#Find", "AdditionalValues [u]") = item_to_add ctxt o_model_test [i_single];

(** fun item_to_add: AdditionalValues [u, v] ================================================ **);

val i_single : I_Model.single_POS =

((3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term AdditionalValues}, [@{term "[u::real]"}]) , Position.none)))

(**)val SOME ("#Find", "AdditionalValues [u, v]") = item_to_add ctxt o_model_test [i_single];

(** fun item_to_add: AdditionalValues [v, u] ================================================ **);

(*/------------------- fun item_to_add: AdditionalValues [v, u] ----------------------------\\*)

val i_single : I_Model.single_POS =

(*present [v, u] (reverse order), because second element has been input first ------vvvvvvvvvv*)

((3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term AdditionalValues}, [@{term "[v::real]"}]) , Position.none)))

(**)val return_item_to_add as SOME ("#Find", "AdditionalValues [v, u]") = (**)

(** )val calling_code as SOME ("#Find", "AdditionalValues [v, u]") =( **)

           item_to_add ctxt o_model_test [i_single];

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

"~~~~~ fun item_to_add , args:"; val (ctxt, o_model, i_model) = (ctxt, o_model_test, [i_single]);

    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 i_to_select = i_model

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

      |> select_inc_lists

    (*in*)

(*+*)val "[\n(3, [1, 2, 3], false ,from o_model, (Inc_POS AdditionalValues [v] , pen2str, Position.T))]"

 = i_to_select |> I_Model.to_string_POS ctxt

(*+*)val [(_, _, _, _, (Inc_POS (_, [Const ("List.list.Cons", _) $ Free ("v", _) $ _]), _))]

 = i_to_select

val false =

    (*if*) i_to_select = []

(** )val return_item_to_add =( **)

(**)val return_fill_from_o as

      SOME (_, _, _, _, (Cor_POS (Const ("Input_Descript.AdditionalValues", _), xxx), _)) =(**)

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

      | NONE => raise ERROR "I_Model.fill_from_o does NOT find a descriptor in O_Model"

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

(*+*)val "[[u], [v]]" = all_value |> UnparseC.terms ctxt

    (*in*)

val true =

    (*if*) Model_Def.is_list_descr descr

        val already_input as [Const ("List.list.Cons", _) $ Free ("v", _) $ _] = feedb |> feedb_values

        val miss = subtract op= already_input all_value

(*+*)val "[[u]]" = miss |> UnparseC.terms ctxt

        val ts = already_input @ [hd miss]

val "[[v], [u]]" = ts |> UnparseC.terms ctxt

    (*in*)

val true =

        (*if*) length all_value = length ts

val return_fill_from_o_STEP = SOME (i, vnts, bool, m_field, (Cor_POS (descr, [values_to_present ts]), pos))

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

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

(*+*)val Cor_POS (Const ("Input_Descript.AdditionalValues", _), xxx) = feedb;

(*+*)val xxx = xxx |> UnparseC.terms ctxt;

(*||------------------ contiue.. item_to_add -------------------------------------------------*)

(** )val return_item_to_add = ( **)

  SOME (m_field, feedb |> 

   (*I_Model.*)feedb_args_to_string ctxt);

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

"~~~~~ fun feedb_args_to_string , args:"; val (ctxt, Cor_POS (descr, values)) = (ctxt, feedb);

(** )val return_feedb_args_to_string =( **)

val return_feedb_args_to_string_STEP =

    UnparseC.term ctxt (descr $ values_to_present values);

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

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

val calling_code as SOME ("#Find", "AdditionalValues [v, u]") = return_item_to_add;

(*\------------------- fun item_to_add: AdditionalValues [v, u] ----------------------------//*)

(** fun item_to_add: Constants Extremum (A = 2 * u * v - u \<up> 2) ============================= **);

val i_single : I_Model.single_POS =

((3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term Extremum}, []) , Position.none)))

val SOME ("#Relate", "Extremum (A = 2 * u * v - u \<up> 2)")

  = item_to_add ctxt o_model_test [i_single];

(** fun item_to_add: Constants SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] ============ **);

val i_single : I_Model.single_POS =

((3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term SideConditions}, []) , Position.none)))

val SOME ("#Relate", "SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]")

  = item_to_add ctxt o_model_test [i_single];

(** fun item_to_add: Solutions L ============================================================ **);

val i_single : I_Model.single_POS =

(3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term solutions}, []) , Position.none))

val SOME ("#Find", "solutions L") = item_to_add ctxt o_model_test [i_single];

(*** fun item_to_add Biegelinie-exammple =================================================== ***);

"----------- fun item_to_add: Biegelinie-exammple ----------------------------------------------";

"----------- fun item_to_add: Biegelinie-exammple ----------------------------------------------";

(** fun item_to_add: solveForVars [c] ======================================================= **);

val (descr $ t) = @{term "solveForVars [c, c_2, c_3, c_4]"}

val [Const ("List.list.Cons", _) $ Free ("c",   _) $ Const ("List.list.Nil", _),

     Const ("List.list.Cons", _) $ Free ("c_2", _) $ Const ("List.list.Nil", _),

     Const ("List.list.Cons", _) $ Free ("c_3", _) $ Const ("List.list.Nil", _),

     Const ("List.list.Cons", _) $ Free ("c_4", _) $ Const ("List.list.Nil", _)]

  = make_values (descr, t)

val o_model_test : O_Model.T = [(0, [1], "#Given", descr, make_values (descr, t))]

val i_model_test : I_Model.T_POS = [

  (0, [1], false, "get-from-o_model", (Inc_POS (descr, []) , Position.none))]

val SOME ("#Given", "solveForVars [c]") = item_to_add ctxt o_model_test i_model_test;

(** fun item_to_add: solveForVars [c, c_2] ================================================== **);

val i_model_test : I_Model.T_POS = [

  (0, [1], false, "get-from-o_model", (Inc_POS (descr,

    [nth 1 (make_values (descr, t))]) , Position.none))]

val SOME ("#Given", "solveForVars [c, c_2]") = item_to_add ctxt o_model_test i_model_test;

(** fun item_to_add: solveForVars [c, c_2, c_3] ============================================= **);

val i_model_test : I_Model.T_POS = [

  (0, [1], false, "get-from-o_model", (Inc_POS (descr,

    (nth 1 (make_values (descr, t))) :: (nth 2 (make_values (descr, t))) :: []) , Position.none))]

val SOME ("#Given", "solveForVars [c, c_2, c_3]") = item_to_add ctxt o_model_test i_model_test;