test/Tools/isac/Minisubpbl/100a-init-rootpbl-Maximum.sml
author wneuper <Walther.Neuper@jku.at>
Mon, 01 Jan 2024 11:31:16 +0100
changeset 60789 8fa678b678e8
parent 60782 e797d1bdfe37
permissions -rw-r--r--
Doc/Specify_Phase 4: start use antiquotations from isar-ref
     1 (* Title:  "Minisubpbl/100a-init-rootpbl-Maximum.sml"
     2    Author: Walther Neuper 1105
     3    (c) copyright due to lincense terms.
     4 
     5 COMPARE Specify/specify.sml --- specify-phase: low level functions ---
     6 
     7 ATTENTION: the file creates buffer overflow if copied in one piece !
     8 
     9 Note: This test --- steps into me --- more than once, to a somewhat extreme extent;
    10   in order not to get lost while working in Test_Some etc, 
    11   re-introduce  ML (*--- step into XXXXX ---*) and Co.
    12   and use Sidekick for orientation.
    13   Nesting is indicated by  /---   //--   ///-  at the left margin of the comments.
    14 *)
    15 (*/------- these overwrite definitions in section above ---\*)
    16 open Ctree;
    17 open Pos;
    18 open TermC;
    19 open Istate;
    20 open Tactic;
    21 open I_Model;
    22 open P_Model
    23 open Rewrite;
    24 open Step;
    25 open LItool;
    26 open LI;
    27 open Test_Code
    28 open Specify
    29 open ME_Misc
    30 open Pre_Conds;
    31 (*\------- these overwrite definitions in section above ---/*)
    32 
    33 val (_(*example text*),
    34   (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" :: 
    35      "Extremum (A = 2 * u * v - u \<up> 2)" :: 
    36      "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" :: 
    37      "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" :: 
    38      "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
    39 (*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)
    40      "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" :: 
    41      "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
    42      "ErrorBound (\<epsilon> = (0::real))" :: []), 
    43    refs as ("Diff_App", 
    44      ["univariate_calculus", "Optimisation"],
    45      ["Optimisation", "by_univariate_calculus"])))
    46   = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
    47 
    48 val c = [];
    49 val return_init_calc = 
    50  Test_Code.init_calc @{context} [(model, refs)]; (*val Model_Problem = nxt;*)
    51 (*/------------------- step into init_calc -------------------------------------------------\\*)
    52 "~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))]) =
    53   (@{context}, [(model, refs)]);
    54     val thy = thy_id |> ThyC.get_theory ctxt
    55     val ((pt, p), tacis) = Step_Specify.initialise' thy (model, refs)
    56 	  val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
    57 	  val f = 
    58            TESTg_form ctxt (pt,p);
    59 "~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p));
    60     val (form, _, _) =
    61    ME_Misc.pt_extract ctxt ptp;
    62 "~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_ as Pbl(*Frm,Pbl*)))) = (ctxt, ptp);
    63         val ppobj = Ctree.get_obj I pt p
    64         val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p;
    65 
    66             (*if*) Ctree.is_pblobj ppobj (*then*);
    67            pt_model ppobj p_ ;
    68 "~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}), Pbl_) =
    69   (ppobj, p_);
    70       val (_, pI, _) = Ctree.get_somespec' spec spec';
    71 (*    val where_ = if pI = Problem.id_empty then []*)
    72                (*if*) pI = Problem.id_empty (*else*);
    73 	          val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
    74 	          val (_, where_) = 
    75  Pre_Conds.check ctxt where_rls where_
    76               (model, I_Model.OLD_to probl);
    77 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
    78   (ctxt, where_rls, where_, (model, I_Model.OLD_to probl));
    79       val (env_model, (env_subst, env_eval)) = 
    80            make_environments model_patt i_model;
    81 "~~~~~ fun make_environments , args:"; val (_, []) = (model_patt, i_model);
    82 (*\------------------- step into init_calc -------------------------------------------------//*)
    83 val (p,_,f,nxt,_,pt) = return_init_calc;
    84 
    85 (*+*)val PblObj {ctxt, probl, ...} = get_obj I pt [];
    86 (*+*)Proof_Context.theory_of ctxt (*= {Pure, .., Diff_App}*);
    87 (*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term ctxt "r"
    88 (*+*)val [] = probl
    89 
    90 val return_me_Model_Problem = 
    91            me nxt p c pt; val Add_Given "Constants [r = 7]" = #4 return_me_Model_Problem;
    92 (*/------------------- step into me_Model_Problem ------------------------------------------\\*)
    93 "~~~~~ fun me , args:"; val (tac as Model_Problem, (p:Pos.pos'), (_:Test_Code.NEW), (pt:Ctree.ctree)) = (nxt, p, c, pt);
    94       val ctxt = Ctree.get_ctxt pt p
    95 
    96 val return_by_tactic = case
    97       Step.by_tactic tac (pt,p) of
    98 		    ("ok", (_, _, ptp)) => ptp;
    99 (*//------------------ step into by_tactic -------------------------------------------------\\*)
   100 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
   101 
   102 val Applicable.Yes tac' = (*case*)
   103       Step.check tac (pt, p) (*of*);
   104 "~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
   105   (*if*) Tactic.for_specify tac (*then*);
   106 
   107 Specify_Step.check tac (ctree, pos);
   108 "~~~~~ fun check , args:"; val (Tactic.Model_Problem, (pt, pos as (p, _))) =
   109   (tac, (ctree, pos));
   110         val (ctxt, o_model, pI') = case Ctree.get_obj I pt p of
   111           Ctree.PblObj {ctxt, origin = (o_model, (_, pI', _), _), ...} => (ctxt, o_model, pI')
   112         | _ => raise ERROR "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj"
   113 	      val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
   114 	      val pbl = I_Model.init ctxt o_model model_patt
   115 
   116 val return_check =
   117     Applicable.Yes (Tactic.Model_Problem' (pI', I_Model.TEST_to_OLD pbl, []));
   118 (*\\------------------ step into by_tactic -------------------------------------------------//*)
   119 val (pt, p) = return_by_tactic;
   120 
   121 val return_do_next = (*case*)
   122       Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
   123 (*//------------------ step into do_next ---------------------------------------------------\\*)
   124 "~~~~~ fun do_next , args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) =
   125   (p, ((pt, e_pos'),[]));
   126     val pIopt = get_pblID (pt,ip);
   127     (*if*) ip = ([],Res); (* = false*)
   128       val _ = (*case*) tacis (*of*);
   129       val SOME _ = (*case*) pIopt (*of*);
   130 
   131     val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
   132       Step.switch_specify_solve p_ (pt, ip);
   133 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
   134       (*if*) Pos.on_specification ([], state_pos) (*then*);
   135 
   136     val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
   137       Step.specify_do_next (pt, input_pos);
   138 (*///----------------- step into specify_do_next -------------------------------------------\\*)
   139 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
   140 
   141 (*  val (_, (p_', tac)) =*)
   142 val return_find_next_step = (*keep for continuing specify_do_next*)
   143    Specify.find_next_step ptp;
   144 (*////---------------- step into find_next_step --------------------------------------------\\*)
   145 "~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
   146     val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
   147       spec = refs, ...} = Calc.specify_data (pt, pos);
   148     val ctxt = Ctree.get_ctxt pt pos;
   149       (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
   150         (*if*) p_ = Pos.Pbl (*then*);
   151 
   152 val return_for_problem as ("dummy", (Pbl, Add_Given "Constants [r = 7]")) =
   153    Specify.for_problem ctxt oris (o_refs, refs) (pbl, I_Model.OLD_to met);
   154 (*/////--------------- step into for_problem -----------------------------------------------\\*)
   155 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
   156   = (ctxt, oris, (o_refs, refs), (pbl, met));
   157     val cdI = if dI = ThyC.id_empty then dI' else dI;
   158     val cpI = if pI = Problem.id_empty then pI' else pI;
   159     val cmI = if mI = MethodC.id_empty then mI' else mI;
   160     val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
   161     val {model = mpc, ...} = MethodC.from_store ctxt cmI;
   162 
   163     val return_check =
   164  Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to pbl);
   165 (*//////-------------- step into check -------------------------------------------------\\*)
   166 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
   167   (ctxt, where_rls, where_, (pbt, I_Model.OLD_to pbl));
   168       val return_make_environments =
   169            make_environments model_patt i_model;
   170 (*///// //------------ step into of_max_variant --------------------------------------------\\*)
   171 "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) =
   172   (model_patt, i_model);
   173 
   174 (*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc Constants [] [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc SideConditions [] [__=__, __=__], Position.T))]"
   175  = i_model |> I_Model.to_string ctxt
   176     val all_variants =
   177         map (fn (_, variants, _, _, _) => variants) i_model
   178         |> flat
   179         |> distinct op =
   180     val variants_separated = map (filter_variants' i_model) all_variants
   181     val sums_corr = map (Model_Def.cnt_corrects) variants_separated
   182     val sum_variant_s = Model_Def.arrange_args sums_corr (1, all_variants)
   183 (*+*)val [(0, 1), (0, 2), (0, 3)] = sum_variant_s
   184     val (_, max_variant) = hd (*..crude decision, up to improvement *)
   185       (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
   186     val i_model_max =
   187       filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
   188     val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
   189 (*for building make_env_s -------------------------------------------------------------------\*)
   190 (*!!!*) val ("#Given", (descr, term), pos) =
   191   Model_Pattern.split_descriptor ctxt ("#Given", @{term "Constants [r = (7::real)]"}, Position.none)
   192 (*!!!*) val patt = equal_descr_pairs |> hd |> #1
   193 (*!!!*)val equal_descr_pairs =
   194   (patt,
   195   (1, [1, 2, 3], true, "#Given", (Cor ((descr, (*!*)TermC.isalist2list(*!*) term)), pos)))
   196   :: tl equal_descr_pairs
   197 (*for building make_env_s -------------------------------------------------------------------/*)
   198 
   199     val env_model = make_env_model equal_descr_pairs;
   200 (*///// ///----------- step into make_env_model --------------------------------------------\\*)
   201 "~~~~~ fun make_env_model , args:"; val (equal_descr_pairs) = (equal_descr_pairs);
   202 
   203 val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
   204        => (mk_env_model id feedb));
   205 val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 4 equal_descr_pairs;
   206 (*\\\\\ \\\----------- step into make_env_model --------------------------------------------//*)
   207 (*||||| ||------------ contine of_max_variant ------------------------------------------------*)
   208 
   209     val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
   210     val subst_eval_list = make_envs_preconds equal_givens
   211 val return_make_envs_preconds =
   212            make_envs_preconds equal_givens;
   213 (*///// ///----------- step into make_envs_preconds ----------------------------------------\\*)
   214 "~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
   215 val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb)
   216 ;
   217 xxx: (Model_Pattern.single * I_Model.single) -> ((term * term) * (term * term)) list;
   218 val return_discern_feedback =
   219            discern_feedback id feedb;
   220 (*nth 1 equal_descr_pairs* )
   221 "~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor ((descr, ts), _))) = (id, feedb);
   222 ( *nth 2 equal_descr_pairs*)
   223 "~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Inc ((descr, ts)))) = (id, feedb);
   224 
   225 (*nth 1 equal_descr_pairs* )
   226 (*+*)val [((Const ("fixes", typ1), Free ("r", typ2)),
   227            (Free ("r", typ3), value))] = return_discern_feedback
   228 (*+*)val true = typ1 = typ2
   229 (*+*)val true = typ3 = HOLogic.realT
   230 (*+*)val "7" = UnparseC.term ctxt value
   231 ( *nth 2 equal_descr_pairs*)
   232 (*+*)val [] = return_discern_feedback
   233 
   234 val return_discern_typ =
   235            discern_typ id (descr, ts);
   236 "~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts));
   237 (*nth 1 equal_descr_pairs* )
   238 (*+*)val [((Const ("fixes", typ1), Free ("r", typ2)),
   239            (Free ("r", typ3), value))] = return_discern_typ
   240 (*+*)val true = typ1 = typ2
   241 (*+*)val true = typ3 = HOLogic.realT
   242 (*+*)val "7" = UnparseC.term ctxt value
   243 ( *nth 2 equal_descr_pairs*)
   244 (*+*)val [] = return_discern_typ;
   245 (**)
   246            switch_type id ts;
   247 "~~~~~ fun switch_type , args:"; val (Const (descr_string, _), ts) = (descr, ts);
   248 
   249 (*nth 1 equal_descr_pairs* )
   250 val return_switch_type = Const (descr_string, ts |> hd |> TermC.lhs |> type_of)
   251 
   252 (*+*)val Const ("Input_Descript.Constants", typ) = return_switch_type
   253 (*+*)val Type ("Real.real", []) = typ
   254 ( *nth 2 equal_descr_pairs*)
   255 (*+*)val return_switch_type = descr
   256 (**)
   257 (*\\\\\ \\\----------- step into make_envs_preconds ----------------------------------------//*)
   258 (*||||| ||------------ contine of_max_variant ------------------------------------------------*)
   259     val subst_eval_list = make_envs_preconds equal_givens
   260     val (env_subst, env_eval) = split_list subst_eval_list
   261 val make_environments = (i_model_max, env_model, (env_subst, env_eval)); (*GOON*)
   262 (*\\\\\ \\------------ step into of_max_variant --------------------------------------------//*)
   263       val (i_model_max, env_model, (env_subst, env_eval)) = make_environments
   264 (*!!!/----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---\*)
   265       val (i_max_variant, env_model, (env_subst, env_eval)) = (i_model_max, [], ([], []))
   266 (*!!!\----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---/*) 
   267 (*||||| |------------- contine check -----------------------------------------------------*)
   268       val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
   269       val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
   270       val full_subst = if env_eval = [] then pres_subst_other
   271         else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
   272       val evals = map (eval ctxt where_rls) full_subst
   273 val return_ = (i_model_max, env_subst, env_eval)
   274 (*\\\\\ \------------- step into check -----------------------------------------------------//*)
   275 val (preok, _) = return_check;
   276 
   277 (*|||||--------------- contine.. for_problem -------------------------------------------------*)
   278 val false =
   279     (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
   280 val false =
   281       (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
   282 val NONE =
   283      (*case*) find_first (fn (_, _, _, _, feedb) => I_Model.is_error feedb) pbl (*of*);
   284 
   285 (** )val SOME (fd, ct') as ("#Given", "Constants [r = 7]") =( **)
   286 (**)val return_item_to_add as SOME ("#Given", xxx) =(**) (*case*) 
   287    Specify.item_to_add ctxt oris (I_Model.OLD_to pbl) (*of*);
   288 (*///// /------------- step into item_to_add -----------------------------------------------\\*)
   289 (*==================== see test/../i_model.sml --- fun item_to_add ---========================*)
   290 (*\\\\\ \------------- step into item_to_add -----------------------------------------------//*)
   291 val SOME (fd, ct') = return_item_to_add
   292 (*+*)val ("#Given", "Constants [r = 7]")  = (fd, ct') (*from NEW item_to_add*)
   293 
   294 (*|||||--------------- continue.. for_problem ------------------------------------------------*)
   295 val return_for_problem_step as ("dummy", (Pbl, Add_Given "Constants [r = 7]"))
   296   = ("dummy", (Pos.Pbl, P_Model.mk_additem fd ct'))
   297 (** )return_for_problem_step = return_for_problem( *..would require equality types*)
   298 (*\\\\\--------------- step into for_problem -----------------------------------------------//*)
   299 val return_find_next_step as ("dummy", (Pbl, Add_Given "Constants [r = 7]"))
   300   = return_for_problem
   301 (*\\\\---------------- step into find_next_step --------------------------------------------//*)
   302 (*|||----------------- continue.. specify_do_next --------------------------------------------*)
   303 val (_, (p_', tac as Add_Given "Constants [r = 7]")) = return_find_next_step
   304 
   305     val ist_ctxt =  Ctree.get_loc pt (p, p_)
   306 (*+*)val Add_Given "Constants [r = 7]" = tac
   307 val _ =
   308     (*case*) tac (*of*);
   309 
   310 val return_by_tactic_input as ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
   311 Step_Specify.by_tactic_input tac (pt, (p, p_'));
   312 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =
   313   (tac, (pt, (p, p_')));
   314 
   315    Specify.by_Add_ "#Given" ct ptp;
   316 "~~~~~ fun by_Add_ , args:"; val (m_field, ct ,(pt, pos as (_, p_))) =
   317   ("#Given", ct, ptp);
   318     val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
   319     val (i_model, m_patt) =
   320        if p_ = Pos.Met then
   321          (met,
   322            (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
   323        else
   324          (pbl,
   325            (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model);
   326 
   327       (*case*)
   328    I_Model.check_single ctxt m_field oris (I_Model.TEST_to_OLD i_model) m_patt ct (*of*);
   329 "~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, (str(*, pos*))) =
   330   (ctxt, m_field, oris, i_model, m_patt, ct);
   331         val (t as (descriptor $ _)) = Syntax.read_term ctxt str
   332 
   333 (*+*)val "Constants [r = 7]" = UnparseC.term ctxt t;
   334 
   335         val SOME m_field' =
   336           (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
   337            (*if*) m_field <> m_field' (*else*);
   338 
   339 (*+*)val "#Given" = m_field; val "#Given" = m_field'
   340 
   341 val ("", ori', all) =
   342           (*case*) O_Model.contains ctxt m_field o_model t (*of*);
   343 
   344 (*+*)val (_, _, _, _, vals) = hd o_model;
   345 (*+*)val "Constants [r = 7]" = UnparseC.term ctxt (@{term Constants} $ (hd vals));
   346 (*+*)if "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), " ^ 
   347 (*+*)    "\n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), " ^ 
   348 (*+*)    "\n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), " ^ 
   349 (*+*)    "\n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), " ^ 
   350 (*+*)    "\n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), " ^ 
   351 (*+*)    "\n(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), " ^ 
   352 (*+*)    "\n(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), " ^ 
   353 (*+*)    "\n(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), " ^ 
   354 (*+*)    "\n(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), " ^ 
   355 (*+*)    "\n(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), " ^ 
   356 (*+*)    "\n(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
   357 (*+*)= O_Model.to_string ctxt o_model then () else error "o_model CHANGED";
   358 
   359   (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*);
   360 "~~~~~ fun is_notyet_input , args:"; val (ctxt, itms, all, (i, v, f, d, ts), pbt) =
   361   (ctxt, i_model, all, ori', m_patt);
   362 val SOME (_, (_, pid)) =
   363   (*case*) find_first (fn (_, (d', _)) => d = d') pbt
   364 val SOME (_, _, _, _, (feedb, _)) =
   365     (*case*) find_first (fn (_, _, _, f', (feedb, _)) =>
   366           f = f' andalso d = (descriptor feedb)) itms
   367             val ts' = inter op = (feedb_values feedb) ts
   368 val false =
   369             (*if*) subset op = (ts, ts') 
   370 
   371 val return_is_notyet_input = ("",
   372            single_from_o feedb pid all (i, v, f, d, subtract op = ts' ts));
   373 "~~~~~ fun single_from_o , args:"; val (feedb, pid, all, (id, vt, fd, d, ts)) =
   374   (feedb, pid, all, (i, v, f, d, subtract op = ts' ts));
   375     val ts' = union op = (feedb_values feedb) ts;
   376     val pval = [Input_Descript.join'''' (d, ts')]
   377     val complete = if eq_set op = (ts', all) then true else false
   378 
   379 (*+*)val "Inc Constants [] [__=__, __=__]" = feedb |> I_Model.feedback_to_string ctxt
   380 (*\\\----------------- step into specify_do_next -------------------------------------------//*)
   381 (*\\------------------ step into do_next ---------------------------------------------------//*)
   382 val ("ok", (ts as (_, _, _) :: _, _, (pt, p))) = return_do_next
   383 
   384 (*|------------------- continue with me_Model_Problem ----------------------------------------*)
   385 val tacis as (_::_) =
   386         (*case*) ts (*of*);
   387           val (tac, _, _) = last_elem tacis
   388 
   389 val return_Model_Problem = (p, [] : NEW, TESTg_form ctxt (pt, p), tac, Celem.Sundef, pt);
   390 (*//------------------ step into TESTg_form ------------------------------------------------\\*)
   391 "~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt, p));
   392 
   393     val (form, _, _) =
   394    ME_Misc.pt_extract ctxt ptp;
   395 "~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_(*Frm,Pbl*)))) = (ctxt, ptp);
   396         val ppobj = Ctree.get_obj I pt p
   397         val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p;
   398           (*if*) Ctree.is_pblobj ppobj (*then*);
   399 
   400            pt_model ppobj p_;
   401 "~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, o_spec, hdl), ctxt, ...}), 
   402   Pbl(*Frm,Pbl*)) = (ppobj, p_);
   403       val (_, _, met_id) = References.select_input o_spec spec
   404       val (allcorr, _) = Pre_Conds.check_internal ctxt (I_Model.OLD_to probl) (Pos.Met, met_id)
   405 
   406 val return_pt_model = Ctree.ModSpec (allcorr, Pos.Pbl, hdl, I_Model.OLD_to probl,
   407   (*where_*)[(*Problem.from_store in check*)], spec)
   408 
   409 (*|------------------- continue with TESTg_form ----------------------------------------------*)
   410 val Ctree.ModSpec (spec as (_, p_, _, gfr, where_, _)) =
   411     (*case*) form (*of*);
   412     Test_Out.PpcKF (  (Test_Out.Problem [],
   413  			P_Model.from (Proof_Context.theory_of ctxt) gfr where_));
   414 
   415    P_Model.from (Proof_Context.theory_of ctxt) gfr where_;
   416 "~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);
   417     fun coll model [] = model
   418       | coll model ((_, _, _, field, itm_) :: itms) =
   419         coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
   420 
   421  val gfr = coll P_Model.empty (I_Model.TEST_to_OLD itms);
   422 "~~~~~ fun coll , args:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: itms))
   423   = (P_Model.empty, I_Model.TEST_to_OLD  itms);
   424 
   425 (*+*)val 4 = length itms;
   426 (*+*)val itm = nth 1 itms;
   427 
   428            coll P_Model.empty [itm];
   429 "~~~~~ fun coll , iterate:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: []))
   430   = (P_Model.empty, [itm]);
   431 
   432           (add_sel_ppc thy field model (item_from_feedback thy itm_));
   433 "~~~~~ fun add_sel_ppc , args:"; val ((_: theory), sel, {Given = gi, Where = wh, Find = fi, With = wi, Relate = re}, x )
   434   = (thy, field, model, (item_from_feedback thy itm_));
   435 
   436    P_Model.item_from_feedback thy itm_;
   437 "~~~~~ fun item_from_feedback , args:"; val (thy, (I_Model.Inc ((d, ts), _))) = (thy, itm_);
   438    P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)));
   439 (*\\------------------ step into TESTg_form ------------------------------------------------//*)
   440 (*\------------------- step into me_Model_Problem ------------------------------------------//*)
   441 val (p, _, f, nxt, _, pt) = return_me_Model_Problem
   442 
   443 (*+++*)val {probl, ...} = Calc.specify_data (pt, pos);
   444 (*+++*)val "[\n(1 ,[1, 2, 3] ,false ,#Given ,Inc Constants [] , pen2str), \n(2 ,[1, 2, 3] ,false ,#Find ,Inc Maximum , pen2str), \n(3 ,[1, 2, 3] ,false ,#Find ,Inc AdditionalValues [] , pen2str), \n(4 ,[1, 2, 3] ,false ,#Relate ,Inc Extremum , pen2str), \n(5 ,[1, 2] ,false ,#Relate ,Inc SideConditions [] , pen2str)]"
   445  = probl |> I_Model.to_string ctxt
   446 (*-------------------- contine me's ----------------------------------------------------------*)
   447 val return_me_add_find_Constants = me nxt p c pt;
   448                                       val Add_Find "Maximum A" = #4 return_me_add_find_Constants;
   449 (*/------------------- step into me_add_find_Constants -------------------------------------\\*)
   450 (*==================== done in "Minisubpbl/150a-add-given-Maximum.sml" subsequently =======================*)