1 (* Title: "Minisubpbl/150a-add-given-Maximum.sml"
2 Author: Walther Neuper 1105
3 (c) copyright due to lincense terms.
5 COMPARE Specify/specify.sml --- specify-phase: low level functions ---
7 ATTENTION: the file creates buffer overflow if copied in one piece !
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.
20 val (_(*example text*),
21 (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
22 "Extremum (A = 2 * u * v - u \<up> 2)" ::
23 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
24 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
25 "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
26 (*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)
27 "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
28 "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
29 "ErrorBound (\<epsilon> = (0::real))" :: []),
31 ["univariate_calculus", "Optimisation"],
32 ["Optimisation", "by_univariate_calculus"])))
33 = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
36 val return_init_calc =
37 Test_Code.init_calc @{context} [(model, refs)]; (*val Model_Problem = nxt;*)
38 (*/------------------- step into init_calc -------------------------------------------------\\*)
39 "~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))]) =
40 (@{context}, [(model, refs)]);
41 val thy = thy_id |> ThyC.get_theory ctxt
42 val ((pt, p), tacis) = Step_Specify.initialise' thy (model, refs)
43 val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
45 TESTg_form ctxt (pt,p);
46 "~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p));
48 ME_Misc.pt_extract ctxt ptp;
49 "~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_ as Pbl(*Frm,Pbl*)))) = (ctxt, ptp);
50 val ppobj = Ctree.get_obj I pt p
51 val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p;
52 (*if*) Ctree.is_pblobj ppobj (*then*);
54 "~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}), Pbl_) =
56 val (_, pI, _) = Ctree.get_somespec' spec spec';
57 (* val where_ = if pI = Problem.id_empty then []*)
58 (*if*) pI = Problem.id_empty (*else*);
59 val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
61 Pre_Conds.check ctxt where_rls where_ (model, probl);
62 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
63 (ctxt, where_rls, where_, (model, probl));
64 val (env_model, (env_subst, env_eval)) =
65 make_environments model_patt i_model;
66 "~~~~~ fun make_environments , args:"; val (_, []) = (model_patt, i_model);
67 (*\------------------- step into init_calc -------------------------------------------------//*)
68 val (p,_,f,nxt,_,pt) = return_init_calc; val Model_Problem = nxt
69 val (p, _, f, nxt, _, pt) = me nxt p c pt; val Add_Given "Constants [r = 7]" = nxt
70 val return_me_add_find_Constants =
71 me nxt p c pt; val Add_Find "Maximum A" = #4 return_me_add_find_Constants;
72 (*/------------------- step into me_add_find_Constants -------------------------------------\\*)
73 "~~~~~ fun me , args:"; val (tac as Add_Given "Constants [r = 7]", p, _(*NEW remove*), pt) =
75 val ctxt = Ctree.get_ctxt pt p
76 (*+*)val PblObj {probl = (1, [1, 2, 3], false, "#Given",
77 (Inc (Const ("Input_Descript.Constants", _), []), _)) :: _, ...} = get_obj I pt (fst p)
78 (*-------------------------------------------^^--*)
79 val return_step_by_tactic = (*case*)
80 Step.by_tactic tac (pt, p) (*of*);
81 (*//------------------ step into Step.by_tactic --------------------------------------------\\*)
82 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
83 val Applicable.Yes tac' =
84 (*case*) Specify_Step.check tac (pt, p) (*of*);
85 (*if*) Tactic.for_specify' tac' (*then*);
87 (** )val return_step_by_tactic =( **)
88 (**)val return_step_specify_by_tactic =(**)
89 Step_Specify.by_tactic tac' ptp;
90 (*///----------------- step into Step_Specify.by_tactic ------------------------------------\\*)
91 "~~~~~ fun by_tactic , args:"; val ((Tactic.Add_Given' (ct, _)), (pt, p)) = (tac', ptp);
93 (** )val calling_code =( **)
94 (**)val return_by_Add_ =(**)
95 Specify.by_Add_ "#Given" ct (pt, p);
96 (*////---------------- step by_Add_ --------------------------------------------------------\\*)
97 "~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, (pt, p));
98 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
101 (*if*) p_ = Pos.Met (*else*);
102 val (i_model, m_patt) =
104 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)
105 val I_Model.Add i_single =
106 (*case*) I_Model.check_single ctxt m_field oris i_model m_patt ct;
108 (** )val i_model' =( **)
109 (**)val return_add_single =(**)
110 I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model;
111 (*/////--------------- step add_single -----------------------------------------------------\\*)
112 "~~~~~ fun add_single , args:"; val (thy, itm, model) =
113 ((Proof_Context.theory_of ctxt), i_single, i_model);
114 fun eq_untouched d (0, _, _, _, (itm_, _)) = (d = descriptor itm_)
115 | eq_untouched _ _ = false
116 val model' = case I_Model.seek_ppc (#1 itm) model of
117 SOME _ => overwrite_ppc thy itm model (*itm updated in is_notyet_input WN.11.03*)
118 (*\\\\\--------------- step add_single -----------------------------------------------------//*)
120 (*|||||--------------- step by_Add_ ----------------------------------------------------------*)
121 val i_model' = return_add_single
122 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor Constants [r = 7] , pen2str, 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))]"
123 = i_model' |> I_Model.to_string ctxt
125 val tac' = I_Model.make_tactic m_field (ct, i_model')
126 val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
127 val return_by_Add_step =
128 ("ok", ([(Tactic.input_from_T ctxt tac', tac', (pos, (Istate_Def.Uistate, ctxt)))],
130 (*+++*)val {probl, ...} = Calc.specify_data (pt', pos);
131 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor Constants [r = 7] , pen2str, 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))]"
132 = probl |> I_Model.to_string ctxt
133 (*\\\\---------------- step into by_Add_ ---------------------------------------------------//*)
134 val return_by_tactic_step = return_by_Add_
135 (*\\\----------------- step into Step_Specify.by_tactic ------------------------------------//*)
136 (*vvv--- this means, the return value of *)
137 val return_step_by_tactic_STEP = return_step_specify_by_tactic
138 (*\\------------------ step into Step.by_tactic --------------------------------------------//*)
139 val ("ok", (_, _, ptp)) = return_step_by_tactic;
141 (*+++*)val (pt, p) = ptp
142 (*+++*)val {probl, ...} = Calc.specify_data (pt, p);
143 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor Constants [r = 7] , pen2str, 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))]"
144 = probl |> I_Model.to_string ctxt;
146 val (pt, p) = ptp; (*case*)
147 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
148 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
149 (p, ((pt, Pos.e_pos'), []));
151 (*if*) Pos.on_calc_end ip (*else*);
152 val (_, probl_id, _) = Calc.references (pt, p);
154 (*case*) tacis (*of*);
156 (*if*) probl_id = Problem.id_empty (*else*);
159 val ("ok", ([(Add_Find "Maximum A", _, _)], [], _)) =
160 switch_specify_solve p_ (pt, ip);
161 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
162 (*if*) Pos.on_specification ([], state_pos) (*then*);
164 val ("ok", ([(Add_Find "Maximum A", _, _)], [], _)) =
165 specify_do_next (pt, input_pos);
166 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
167 val (_, (p_', tac)) =
168 Specify.find_next_step ptp;
169 "~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
170 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
171 spec = refs, ...} = Calc.specify_data (pt, pos);
172 val ctxt = Ctree.get_ctxt pt pos;
173 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor Constants [r = 7] , pen2str, 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))]"
174 = pbl |> I_Model.to_string ctxt(*+*)
177 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
179 (*if*) p_ = Pos.Pbl (*then*);
181 (** )val ("dummy", (Pbl, Add_Find "Maximum A")) =( **)
182 (**)val return_for_problem as ("dummy", (Pbl, Add_Find "Maximum A"))=(**)
183 for_problem ctxt oris (o_refs, refs) (pbl, met);
184 (*//------------------ step into for_problem -----------------------------------------------\\*)
185 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
186 (ctxt, oris, (o_refs, refs), (pbl, met));
187 val cpI = if pI = Problem.id_empty then pI' else pI;
188 val cmI = if mI = MethodC.id_empty then mI' else mI;
189 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
190 val {model = mpc, ...} = MethodC.from_store ctxt cmI
192 (** )val (preok, _) =( **)
193 (**)val return_check =(**)
194 Pre_Conds.check ctxt where_rls where_ (pbt, pbl);
195 (*///----------------- step into Pre_Conds.check -------------------------------------------\\*)
196 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
197 (ctxt, where_rls, where_, (pbt, pbl));
199 (** )val (_, (env_subst, env_eval)) =( **)
200 (**)val return_make_environments =(**)
201 Pre_Conds.make_environments model_patt i_model;
202 (*////---------------- step into make_environments -----------------------------------------\\*)
203 "~~~~~ fun make_environments , args:"; val (model_patt, i_model) = (model_patt, i_model);
204 val equal_descr_pairs = map (get_equal_descr i_model) model_patt
207 val env_model = make_env_model equal_descr_pairs
208 (** )val env_model =( **)
209 (**)val return_make_env_model =(**)
210 make_env_model equal_descr_pairs;
211 (*/////--------------- step into make_env_model --------------------------------------------\\*)
212 "~~~~~ fun make_env_model , args:"; val (equal_descr_pairs) = (equal_descr_pairs);
213 val return_make_env_model_step =
214 map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
215 => (mk_env_model id feedb)) equal_descr_pairs
217 (*map:*)val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 2 equal_descr_pairs);
219 (*///// /------------- step into mk_env_model ----------------------------------------------\\*)
220 "~~~~~ fun mk_env_model , args:"; val (_, (Model_Def.Inc (_, []))) = (id, feedb);
221 (*+*)val (patt, imod) = nth 2 equal_descr_pairs
222 (*+*)val "(#Find, (Maximum, maxx))" = patt |> Model_Pattern.single_to_string ctxt
223 (*+*)val "(2, [1, 2, 3], false ,#Find, (Inc Maximum __, Position.T))" = imod |> I_Model.single_to_string ctxt
225 val return_mk_env_model_2_step = []
226 (*\\\\\ \------------- step into mk_env_model ----------------------------------------------//*)
227 (*\\\\\--------------- step into make_env_model --------------------------------------------//*)
228 val env_model = return_make_env_model;
230 (*||||---------------- contine.. make_environments -------------------------------------------*)
231 val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
233 (** )val subst_eval_list =( **)
234 (**)val return_make_envs_preconds =(**)
235 make_envs_preconds equal_givens;
236 (*/////--------------- step into make_envs_preconds ----------------------------------------\\*)
237 "~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
238 val return_make_envs_preconds_step =
239 map (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb) equal_givens
243 val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 1 equal_givens
244 (*\\\\\--------------- step into make_envs_preconds ----------------------------------------//*)
245 val subst_eval_list = return_make_envs_preconds;
246 val (env_subst, env_eval) = split_list subst_eval_list
248 val return_make_environments_step = (env_model, (env_subst, env_eval));
249 (*+*)if return_make_environments_step = return_make_environments
250 then () else error "return_make_environments_step <> return_make_environments";
251 (*\\\\---------------- step into make_environments -----------------------------------------//*)
252 (*|||----------------- contine.. Pre_Conds.check ---------------------------------------------*)
253 val (env_model, (env_subst, env_eval)) = return_make_environments
254 val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
255 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
256 val full_subst = if env_eval = [] then pres_subst_other
257 else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
258 val evals = map (eval ctxt where_rls) full_subst
260 val return_make_environments_step = (foldl and_ (true, map fst evals), pres_subst_other)
261 (*\\\----------------- step into Pre_Conds.check -------------------------------------------//*)
262 (*||------------------ contine.. for_problem -------------------------------------------------*)
263 val (preok, _) = return_check;
266 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
268 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
270 (*case*) find_first (fn (_, _, _, _, (feedb, _)) => I_Model.is_error feedb) pbl (*of*);
272 val SOME (fd, ct' as "Maximum A") = (*case*)
273 item_to_add ctxt oris pbl (*of*);
274 "~~~~~ fun item_to_add , args:"; val (ctxt, o_model, i_model) = (ctxt, oris, pbl);
275 val max_vnt = last_elem (*this decides, for which variant initially help is given*)
276 (Model_Def.max_variants o_model i_model)
277 val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model
278 val i_to_select = i_model
279 |> filter_out (fn (_, vnts, _, _, (I_Model.Cor _, _)) => member op= vnts max_vnt | _ => false)
284 val SOME (_, _, _, m_field, (feedb, _)) = (*case*)
285 I_Model.fill_from_o o_vnts i_to_select (*of*);
286 (*+*)val "Cor Maximum A , pen2str" = feedb |> I_Model.feedback_to_string ctxt;
288 "~~~~~ fun fill_from_o , args:"; val (o_model, (i, vnts, bool, m_field, (feedb, pos))) =
289 (o_vnts, i_to_select);
290 val (m_field, all_value as [Free ("A", _)]) =
291 case find_first (fn (_, _, _, descr', _) => Model_Def.descriptor_exists descr' feedb) o_model of
292 SOME (_, _, m_field, _, ts) => (m_field, ts)
293 val descr = Model_Def.get_descr feedb (*i_single has been filtered appropriately*)
296 (*if*) Model_Def.is_list_descr descr (*else*);
297 val return_fill_from_o_STEP = SOME (i, vnts, bool, m_field,
298 (Inc (descr, all_value), pos))
299 (*\------------------- step into me_add_find_Constants -------------------------------------//*)
300 val (p,_,f,nxt,_,pt) = return_me_add_find_Constants;
301 val Add_Find "Maximum A" = nxt
303 (** )val (p,_,f,nxt,_,pt) =( **)
304 (**)val return_me_Add_Find_Maximum =(**)
305 me nxt p c pt; val Add_Find "AdditionalValues [u]" = #4 return_me_Add_Find_Maximum;
306 (*/------------------- step into me_Add_Find_Maximum ---------------------------------------\\*)
307 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
308 val ctxt = Ctree.get_ctxt pt p
310 case Step.by_tactic tac (pt, p) of
311 ("ok", (_, _, ptp)) => ptp;
313 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
314 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
315 (p, ((pt, Pos.e_pos'), []));
317 (*if*) Pos.on_calc_end ip (*else*);
318 val (_, probl_id, _) = Calc.references (pt, p);
321 (*case*) tacis (*of*);
323 (*if*) probl_id = Problem.id_empty (*else*);
325 switch_specify_solve p_ (pt, ip);
326 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
328 (*if*) Pos.on_specification ([], state_pos) (*then*);
330 specify_do_next (pt, input_pos);
331 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
333 (**)val (_, (p_', tac as Add_Find "AdditionalValues [u]")) =(**)
334 Specify.find_next_step ptp;
335 "~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
336 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
337 spec = refs, ...} = Calc.specify_data (pt, pos);
338 val ctxt = Ctree.get_ctxt pt pos
341 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
343 (*if*) p_ = Pos.Pbl (*then*);
345 (**)val return_find_next_step_STEP as ("dummy", (Pbl, Add_Find "AdditionalValues [u]")) =(**)
346 for_problem ctxt oris (o_refs, refs) (pbl, met);
347 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
348 (ctxt, oris, (o_refs, refs), (pbl, met));
349 val cpI = if pI = Problem.id_empty then pI' else pI;
350 val cmI = if mI = MethodC.id_empty then mI' else mI;
351 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
352 val {model = mpc, ...} = MethodC.from_store ctxt cmI
353 val (preok, _) = Pre_Conds.check ctxt where_rls where_ (pbt, pbl);
356 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
358 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
360 (*case*) find_first (fn (_, _, _, _, (feedb, _)) => I_Model.is_error feedb) pbl (*of*);
362 (**)val SOME (fd, ct' as "AdditionalValues [u]") = (*case*)(**)
363 item_to_add ctxt oris pbl (*of*);
364 "~~~~~ fun item_to_add , args:"; val (ctxt, o_model, i_model) =
366 val max_vnt = last_elem (*this decides, for which variant initially help is given*)
367 (Model_Def.max_variants o_model i_model)
368 val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model
369 val i_to_select = i_model
370 |> filter_out (fn (_, vnts, _, _, (I_Model.Cor _, _)) => member op= vnts max_vnt | _ => false)
372 (*ERROR*)val "[\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))]"
373 = i_to_select |> I_Model.to_string ctxt(*ERROR*)
376 (*if*) i_to_select = []
378 val SOME (_, _, _, m_field, (feedb, _)) = (*case*)
379 I_Model.fill_from_o o_vnts (hd i_to_select) (*of*);
380 "~~~~~ fun fill_from_o , args:";
381 (*==================== see test/../i-model.sml --- fun item_to_add ===========================*)
382 (*\------------------- step into me_Add_Find_Maximum ---------------------------------------//*)
383 val (p,_,f,nxt,_,pt) = return_me_Add_Find_Maximum;
384 val Add_Find "AdditionalValues [u]" = nxt
385 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u, v]" = nxt;(*ERROR after repairing item_to_add, investigate in testcode above*)
386 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)" = nxt;
387 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;
389 val return_me_Add_Relation_SideConditions as (_, _, _, Specify_Theory "Diff_App", _, _)
391 (*/------------------- step into me Add_Relation_SideConditions ----------------------------\\*)
392 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
393 val ctxt = Ctree.get_ctxt pt p;
394 (**) val (pt, p) = (**)
395 (**)case(**) Step.by_tactic tac (pt, p) (**)of(**)
396 (**) ("ok", (_, _, ptp)) => ptp (**) ;
399 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
400 (*//------------------ step into do_next ---------------------------------------------------\\*)
401 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
402 = (p, ((pt, Pos.e_pos'), [])) (*of*);
403 (*if*) Pos.on_calc_end ip (*else*);
404 val (_, probl_id, _) = Calc.references (pt, p);
405 (*case*) tacis (*of*);
406 (*if*) probl_id = Problem.id_empty (*else*);
408 Step.switch_specify_solve p_ (pt, ip);
409 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
410 (*if*) Pos.on_specification ([], state_pos) (*then*);
412 Step.specify_do_next (pt, input_pos);
413 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
414 val (_, (p_', tac as Specify_Theory "Diff_App")) =
415 Specify.find_next_step ptp;
416 "~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
417 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
418 spec = refs, ...} = Calc.specify_data (pt, pos);
419 val ctxt = Ctree.get_ctxt pt pos;
420 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
421 (*if*) p_ = Pos.Pbl (*then*);
423 (** )val ("dummy", (Pbl, tac as Specify_Theory "Diff_App")) =( **)
424 (**)val return_for_problem =(**)
425 for_problem ctxt oris (o_refs, refs) (pbl, met);
426 (*///// /------------- step into for_problem -----------------------------------------------\\*)
427 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
428 (ctxt, oris, (o_refs, refs), (pbl, met));
429 val cpI = if pI = Problem.id_empty then pI' else pI;
430 val cmI = if mI = MethodC.id_empty then mI' else mI;
431 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
432 val {model = mpc, ...} = MethodC.from_store ctxt cmI
434 (*+*)val [Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
435 Free ("fixes", _)] = where_;
437 (** )val (preok, _) =( **)
438 (**)return_check =(**)
439 Pre_Conds.check ctxt where_rls where_ (pbt, pbl);
440 (*///// //------------ step into check -------------------------------------------------\\*)
441 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
442 (ctxt, where_rls, where_, (pbt, pbl));
443 (*+*)val "[0 < fixes]" = pres |> UnparseC.terms ctxt
444 (*+*)val "[\"(#Given, (Constants, fixes))\", \"(#Find, (Maximum, maxx))\", \"(#Find, (AdditionalValues, vals))\", \"(#Relate, (Extremum, extr))\", \"(#Relate, (SideConditions, sideconds))\"]"
445 (*+*) = model_patt |> Model_Pattern.to_string ctxt
446 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
447 = i_model |> I_Model.to_string ctxt
449 val return_make_environments as (_, (env_subst, env_eval)) =
450 Pre_Conds.make_environments model_patt i_model
452 (*+*)val [(Free ("fixes", T1), Free ("r", T2))] = env_subst (*?!? Const*)
453 (*+*)val Type ("Real.real", []) = T1
454 (*+*)val Type ("Real.real", []) = T2
456 (*+*)val [(Free ("r", T2), Const ("Num.numeral_class.numeral", _) $ _)] = env_eval
457 (*+*)val Type ("Real.real", []) = T2
459 val (_, (env_subst, env_eval)) = return_make_environments;
460 (*|||----------------- contine check -----------------------------------------------------*)
461 val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
462 (*+*)val [(true, Const ("Orderings.ord_class.less", _) $
463 Const ("Groups.zero_class.zero", _) $ Free ("r", _))] = pres_subst
465 val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
467 Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
468 (Const ("Num.numeral_class.numeral", _) $ _))] = full_subst
470 val evals = map (eval ctxt where_rls) full_subst
471 val return_check_STEP = (foldl and_ (true, map fst evals), pres_subst)
472 (*\\\\\ \\------------ step into check -------------------------------------------------\\*)
473 val (preok as true, _) = return_check
475 (*||||| |------------- contine.. for_problem -------------------------------------------------*)
477 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
479 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
481 (*case*) find_first (fn (_, _, _, _, (feedb, _)) => I_Model.is_error feedb) pbl (*of*);
483 (*case*) item_to_add ctxt oris pbl (*of*);
484 "~~~~~ fun item_to_add , args:"; val (ctxt, o_model, i_model) = (ctxt, oris, pbl);
486 (*+*)val "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), \n(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), \n(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), \n(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
487 = o_model |> O_Model.to_string ctxt
488 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
489 = i_model |> I_Model.to_string ctxt
491 val max_vnt as 1= last_elem (*this decides, for which variant initially help is given*)
492 (Model_Def.max_variants o_model i_model)
493 val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model
494 (*+*)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\"])]"
495 = o_vnts |> O_Model.to_string ctxt
497 val i_to_select = i_model
498 |> filter_out (fn (_, vnts, _, _, (I_Model.Cor _, _)) => member op= vnts max_vnt | _ => false)
501 (*if*) i_to_select = [] (*then*);
503 val return_for_problem_STEP = NONE
504 (*\\\\\ \------------- step into for_problem -----------------------------------------------//*)
505 val calling_code = return_for_problem;
506 (*-------------------- stopped after ERROR found ---------------------------------------------*)
508 (*\\------------------ step into do_next ---------------------------------------------------\\*)
509 (*\------------------- step into me_Add_Relation_SideConditions ----------------------------//*)
510 val (p, _, f, nxt, _, pt) = return_me_Add_Relation_SideConditions
511 val Specify_Theory "Diff_App" = nxt;
513 val return_me_Specify_Theory
514 = me nxt p c pt; val Specify_Problem ["univariate_calculus", "Optimisation"] = #4 return_me_Specify_Theory;
515 (*/------------------- step into me_Specify_Theory -----------------------------------------\\*)
516 "~~~~~ fun me , args:"; val (tac as Specify_Theory "Diff_App", p, _, pt) = (nxt, p, c, pt);
517 val ctxt = Ctree.get_ctxt pt p;
519 (*case*) Step.by_tactic tac (pt, p) (*of*);
520 (* ("ok", (_, _, ptp)) => ptp *)
521 val return_Step_by_tactic =
522 Step.by_tactic tac (pt, p);
523 (*//------------------ step into Step_by_tactic --------------------------------------------\\*)
524 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
525 (*case*) Specify_Step.check tac (pt, p) (*of*);
527 (*||------------------ contine Step_by_tactic ------------------------------------------------*)
528 (*\\------------------ step into Step_by_tactic --------------------------------------------//*)
530 val ("ok", (_, _, ptp)) = return_Step_by_tactic;
531 (*|------------------- continue me Specify_Theory --------------------------------------------*)
533 val ("ok", (ts as (_, _, _) :: _, _, _)) =
535 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
536 (*//------------------ step into do_next ---------------------------------------------------\\*)
537 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
538 = (p, ((pt, Pos.e_pos'), [])) (*of*);
539 (*if*) Pos.on_calc_end ip (*else*);
540 val (_, probl_id, _) = Calc.references (pt, p);
542 (*case*) tacis (*of*);
543 (*if*) probl_id = Problem.id_empty (*else*);
545 Step.switch_specify_solve p_ (pt, ip);
546 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
547 (*if*) Pos.on_specification ([], state_pos) (*then*);
549 Step.specify_do_next (pt, input_pos);
550 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
551 val (_, (p_', tac)) = Specify.find_next_step ptp
552 val ist_ctxt = Ctree.get_loc pt (p, p_);
555 Step_Specify.by_tactic_input tac (pt, (p, p_'));
556 (*+*)val Specify_Theory "Diff_App" = tac;
557 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Theory dI), (pt, pos as (_, Pbl)))
558 = (tac, (pt, (p, p_')));
559 val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
560 PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
561 (oris, dI, dI', pI', probl, ctxt)
562 val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');
563 val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
564 (*\\------------------ step into do_next ---------------------------------------------------//*)
565 (*\------------------- step into me_Specify_Theory -----------------------------------------//*)
566 val (p,_,f,nxt,_,pt) = return_me_Specify_Theory;
568 val return_me_Specify_Problem (* keep for continuing me *)
569 = me nxt p c pt; val Specify_Method ["Optimisation", "by_univariate_calculus"] = #4 return_me_Specify_Problem;
570 (*/------------------- step into me_Specify_Problem ----------------------------------------\\*)
571 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
572 val ctxt = Ctree.get_ctxt pt p
574 (** ) val ("ok", (_, _, ptp as (pt, p))) =( **)
575 (**) val return_by_tactic =(**) (*case*)
576 Step.by_tactic tac (pt, p) (*of*);
577 (*//------------------ step into by_tactic -------------------------------------------------\\*)
578 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
581 Step.check tac (pt, p) (*of*);
582 "~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
583 (*if*) Tactic.for_specify tac (*then*);
585 Specify_Step.check tac (ctree, pos);
586 "~~~~~ fun check , args:"; val ((Tactic.Specify_Problem pID), (pt, pos as (p, _)))
587 = (tac, (ctree, pos));
588 val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of
589 Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
590 => (oris, dI, pI, dI', pI', itms)
591 val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');
592 (*\\------------------ step into by_tactic -------------------------------------------------//*)
593 val ("ok", (_, _, ptp as (pt, p))) = return_by_tactic (* kept for continuing me *);
596 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
597 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
598 (*if*) Pos.on_calc_end ip (*else*);
599 val (_, probl_id, _) = Calc.references (pt, p);
601 (*case*) tacis (*of*);
602 (*if*) probl_id = Problem.id_empty (*else*);
604 Step.switch_specify_solve p_ (pt, ip);
605 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
606 (*if*) Pos.on_specification ([], state_pos) (*then*);
608 Step.specify_do_next (pt, input_pos);
609 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
610 val (_, (p_', tac)) = Specify.find_next_step ptp
611 val ist_ctxt = Ctree.get_loc pt (p, p_)
615 Step_Specify.by_tactic_input tac (pt, (p, p_'));
616 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos))
617 = (tac, (pt, (p, p_')));
619 (**)val return_complete_for =(**)
620 (** ) val (o_model, ctxt, i_model) =( **)
621 Specify_Step.complete_for id (pt, pos);
622 (*//------------------ step into complete_for ----------------------------------------------\\*)
623 "~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));
625 (*+*)val ["Optimisation", "by_univariate_calculus"] = mID
626 val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = met_imod, ctxt,
627 ...} = Calc.specify_data (ctree, pos);
628 val ctxt = Ctree.get_ctxt ctree pos
629 val (dI, _, _) = References.select_input o_refs refs;
630 val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
631 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
632 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
634 (**)val return_match_itms_oris = (**)
635 (** )val (_, (i_model, _)) = ( **)
636 M_Match.by_i_models ctxt o_model' (i_prob, i_prob)
637 (m_patt, where_, where_rls);
638 (*///----------------- step into by_i_models -------------------------------------------\\*)
639 "~~~~~ fun by_i_models, args:"; val (ctxt, o_model, (pbl_imod, met_imod), (m_patt, where_, where_rls)) =
640 (ctxt, o_model', (i_prob, i_prob), (m_patt, where_, where_rls));
642 (**)val return_fill_method =(**)
643 (** )val met_imod =( **)
644 fill_method o_model (pbl_imod, met_imod) m_patt;
645 (*////--------------- step into fill_method -----------------------------------------------\\*)
646 "~~~~~ fun fill_method , args:"; val (o_model, (pbl_imod, met_imod), met_patt) =
647 (o_model, (pbl_imod, met_imod), m_patt);
649 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
650 = pbl_imod |> I_Model.to_string ctxt
651 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
652 = met_imod |> I_Model.to_string ctxt
654 (**)val return_max_variants =(**)
655 (** )val pbl_max_vnts as [2, 1] =( **)
656 Model_Def.max_variants o_model pbl_imod;
657 (*//------------------ step into max_variants ----------------------------------------------\\*)
658 "~~~~~ fun max_variants , args:"; val (o_model, i_model) = (o_model, pbl_imod);
659 val all_variants as [1, 2, 3] =
660 map (fn (_, variants, _, _, _) => variants) i_model
663 val variants_separated = map (filter_variants' i_model) all_variants
664 (*+*)val ["[\n(1, [1, 2, 3], true ,#Given, (Cor Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]",
665 "[\n(1, [1, 2, 3], true ,#Given, (Cor Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]",
666 "[\n(1, [1, 2, 3], true ,#Given, (Cor Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T))]"]
667 = variants_separated |> map (I_Model.to_string ctxt)
669 val sums_corr as [5, 5, 4] = map (cnt_corrects) variants_separated
670 (*----------------#--#--#*)
671 (*---------------------^-------^-------^*)
672 val sum_variant_s as [(5, 1), (5, 2), (4, 3)] = arrange_args sums_corr (1, all_variants)
673 val max_first as [(5, 2), (5, 1), (4, 3)] = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
674 (*----------------##====--##====--//////---------^^^^*)
675 (*------------^--^-#-------#*)
676 val maxes as [2, 1] = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first
678 val return_max_variants = maxes
679 (*\\------------------ step into max_variants ----------------------------------------------//*)
680 val pbl_max_vnts as [2, 1] = return_max_variants;
682 (*probably pbl/met_imod = [], so take met_patt; if empty return Sup*)
683 val i_from_met = map (fn (_, (descr, _)) => (*order from met_patt*)
684 Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt (*\<longrightarrow> right order for args*)
685 (*+MET: Sup..*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [], false ,i_model_empty, (Sup FunctionVariable, Position.T)), \n(0, [], false ,i_model_empty, (Sup Input_Descript.Domain, Position.T)), \n(0, [], false ,i_model_empty, (Sup ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor AdditionalValues [u, v] , pen2str, Position.T))]"
686 = i_from_met |> I_Model.to_string ctxt
688 val met_max_vnts as [2, 1] = Model_Def.max_variants o_model i_from_met;
689 val max_vnt as 2 = hd (inter op= pbl_max_vnts met_max_vnts);
690 (*add items from pbl_imod (without overwriting existing items in met_imod)*)
692 val return_add_other = map (
693 add_other max_vnt pbl_imod) i_from_met;
694 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor AdditionalValues [u, v] , pen2str, Position.T))]"
695 = return_add_other |> I_Model.to_string ctxt;
696 (*/////-------------- step into add_other -------------------------------------------------\\*)
697 "~~~~~ fun add_other_5 , args:"; val (max_vnt, i1_model, (i2, _, bool2, m_field2, (Sup (descr2, ts2), pos2))) =
698 (max_vnt, pbl_imod, nth 5 i_from_met);
700 (*+*)val Const ("Input_Descript.FunctionVariable", _) = descr2;
702 val (_, vnts1, _, _, (feedb1, _)) = (i2, [], bool2, m_field2, (Sup (descr2, ts2), pos2))
703 val SOME (descr1 as (Const ("Input_Descript.FunctionVariable", _)) ) =
708 Model_Def.member_vnt vnts1 max_vnt
710 find_first (fn (_, vnts1, _, _, (feedb1, _)) => case get_dscr_opt feedb1 of
712 | SOME descr1 => descr1 = descr2 andalso Model_Def.member_vnt vnts1 max_vnt) i1_model
714 val return_add_other_1 = (i2, [max_vnt], bool2, m_field2, (Sup (descr2, ts2), pos2))
715 val check as true = return_add_other_1 = nth 5 return_add_other
716 (*\\\\\-------------- step into add_other -------------------------------------------------//*)
717 val i_from_pbl = return_add_other
718 (*\\\\---------------- step into fill_method -----------------------------------------------//*)
719 val return_fill_method_step = filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) i_from_met
721 (*+MET: dropped ALL DUE TO is_empty_single*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor AdditionalValues [u, v] , pen2str, Position.T))]" =
722 return_fill_method_step |> I_Model.to_string ctxt
723 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor AdditionalValues [u, v] , pen2str, Position.T))]"
724 = return_fill_method |> I_Model.to_string ctxt;
725 return_fill_method_step = return_fill_method; (*latter is correct, did not investigate further*)
726 (*\\\----------------- step into by_i_models -------------------------------------------//*)
727 val (_, (i_model, _)) = return_match_itms_oris;
729 (*||------------------ continue. complete_for ------------------------------------------------*)
730 val (o_model, ctxt, i_model) = return_complete_for
731 (*+isa*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor AdditionalValues [u, v] , pen2str, Position.T))]"
732 = i_model |> I_Model.to_string ctxt(*+isa*)
733 (*+isa2:MET.Mis* ) val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(7 ,[1] ,false ,#Given ,Mis FunctionVariable funvar), \n(10 ,[1, 2] ,false ,#Given ,Mis Input_Descript.Domain doma), \n(12 ,[1, 2, 3] ,false ,#Given ,Mis ErrorBound err)]" =
734 i_model |> I_Model.to_string ctxt ( *+isa2*)
735 (*\\------------------ step into complete_for ----------------------------------------------//*)
736 val (o_model, ctxt, i_model) = return_complete_for
738 (*|------------------- continue. complete_for ------------------------------------------------*)
739 val return_complete_for_step = (o_model', ctxt', i_model)
741 val (o_model'_step, i_model_step) = (#1 return_complete_for_step, #3 return_complete_for_step)
742 val (o_model', i_model) = (#1 return_complete_for, #3 return_complete_for)
744 (*+*)if (o_model'_step, i_model_step) = (o_model', i_model)
745 (*+*)then () else error "return_complete_for_step <> return_complete_for";
746 (*\------------------- step into me Specify_Problem ----------------------------------------//*)
747 val (p,_,f,nxt,_,pt) = return_me_Specify_Problem
749 val return_me_Specify_Method
750 = me nxt p c pt; val Add_Given "FunctionVariable a" = #4 return_me_Specify_Method;
751 (*/------------------- step into me_Specify_Method -----------------------------------------\\*)
752 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
754 (*+*)val "[]" =(*+*) get_obj g_met pt (fst p) |> I_Model.to_string ctxt
756 val ctxt = Ctree.get_ctxt pt p
758 case Step.by_tactic tac (pt, p) of
759 ("ok", (_, _, ptp)) => ptp;
761 (*quick step into --> me_Specify_Method*)
762 (*+*)val Specify_Method ["Optimisation", "by_univariate_calculus"] = tac;
764 "~~~~~ fun by_tactic , args:"; val () = ();
766 "~~~~~ fun check , args:"; val () = ();
767 (*Specify_Step.check (Tactic.Specify_Method*)
768 "~~~~~ fun check , args:"; val () = ();
769 (*Specify_Step.complete_for*)
770 "~~~~~ fun complete_for , args:"; val () = ();
771 (* M_Match.by_i_models*)
772 "~~~~~ fun by_i_models , args:"; val () = ();
774 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor AdditionalValues [u, v] , pen2str, Position.T))]"
775 = get_obj g_met pt (fst p) |> I_Model.to_string ctxt;
778 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
779 (*//------------------ step into Step.do_next ----------------------------------------------\\*)
780 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
781 (*if*) Pos.on_calc_end ip (*else*);
782 val (_, probl_id, _) = Calc.references (pt, p);
784 (*case*) tacis (*of*);
785 (*if*) probl_id = Problem.id_empty (*else*);
787 Step.switch_specify_solve p_ (pt, ip);
788 (*///----------------- step into Step.switch_specify_solve ---------------------------------\\*)
789 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
790 (*if*) Pos.on_specification ([], state_pos) (*then*);
792 Step.specify_do_next (pt, input_pos);
793 (*////---------------- step into Step.specify_do_next --------------------------------------\\*)
794 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
796 val (_, (p_', tac)) =
797 Specify.find_next_step ptp;
798 (*/////--------------- step into find_next_step --------------------------------------------\\*)
799 "~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
800 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
801 spec = refs, ...} = Calc.specify_data (pt, pos);
802 val ctxt = Ctree.get_ctxt pt pos;
803 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
804 (*if*) p_ = Pos.Pbl (*else*);
806 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor AdditionalValues [u, v] , pen2str, Position.T))]"
807 = met |> I_Model.to_string ctxt
809 (**)val ("dummy", (Met, Add_Given "FunctionVariable a")) =(**)
810 Specify.for_method ctxt oris (o_refs, refs) (pbl, met);
811 (*///// /------------- step into Step.for_method -------------------------------------------\\*)
812 "~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (_, met))
813 = (ctxt, oris, (o_refs, refs), (pbl, met));
814 val cmI = if mI = MethodC.id_empty then mI' else mI;
815 val {model, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
816 val (preok, _) = Pre_Conds.check ctxt where_rls where_ (model, met);
818 (*case*) find_first (I_Model.is_error o #1 o #5) met (*of*);
820 (** )SOME (fd, ct') =( **)
821 (**)val return_item_to_add =(**)
823 Specify.item_to_add ctxt oris met (*of*);
824 (*///// //------------ step into item_to_add -----------------------------------------------\\*)
825 "~~~~~ fun item_to_add , args:"; val (ctxt, o_model, i_model) = (ctxt, oris, met);
826 (*+*)val "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n(2, [\"1\", \"2\", \"3\"], #Given, Maximum, [\"A\"]), \n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n(4, [\"1\", \"2\", \"3\"], #Given, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n(5, [\"1\", \"2\"], #Given, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n(6, [\"3\"], #Given, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n(7, [\"1\"], #Given, FunctionVariable, [\"a\"]), \n(8, [\"2\"], #Given, FunctionVariable, [\"b\"]), \n(9, [\"3\"], #Given, FunctionVariable, [\"\<alpha>\"]), \n(10, [\"1\", \"2\"], #Given, Input_Descript.Domain, [\"{0<..<r}\"]), \n(11, [\"3\"], #Given, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n(12, [\"1\", \"2\", \"3\"], #Given, ErrorBound, [\"\<epsilon> = 0\"])]"
827 = oris |> O_Model.to_string ctxt
828 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor AdditionalValues [u, v] , pen2str, Position.T))]"
829 = i_model |> I_Model.to_string ctxt
831 val max_vnt = last_elem (*this decides, for which variant initially help is given*)
832 (Model_Def.max_variants o_model i_model)
833 val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model
834 val i_to_select = i_model
835 |> filter_out (fn (_, vnts, _, _, (I_Model.Cor _, _)) => member op= vnts max_vnt | _ => false)
837 (*+*)val "[\n(0, [2], false ,i_model_empty, (Sup FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup ErrorBound, Position.T))]"
838 = i_to_select |> I_Model.to_string ctxt
841 (*if*) i_to_select = [] (*else*);
843 (** )val SOME (_, _, _, m_field, (feedb, _)) =( **)
844 (**)val return_fill_from_o = (**)
845 (*case*) I_Model.fill_from_o o_vnts (hd i_to_select) (*of*);
846 (*///// ///----------- step into fill_from_o -----------------------------------------------\\*)
847 "~~~~~ fun fill_from_o , args:"; val (o_model, (i, vnts, bool, _, (feedb, pos))) =
848 (o_vnts, (hd i_to_select));
849 val (m_field, all_value) =
850 case find_first (fn (_, _, _, descr', _) => Model_Def.descriptor_exists descr' feedb) o_model of
851 SOME (_, _, m_field, _, ts) => (m_field, ts)
852 val descr = Model_Def.get_descr feedb (*i_single has been filtered appropriately*)
854 (*if*) Model_Def.is_list_descr descr (*else*);
855 val return_fill_from_o_STEP = SOME (i, vnts, bool, m_field, (Cor (descr, all_value), pos))
856 (*-------------------- stopped after ERROR found ---------------------------------------------*)
857 (*\\\\\ \\\----------- step into fill_from_o -----------------------------------------------//*)
858 val SOME (_, _, _, m_field, (feedb, _)) = return_fill_from_o
860 (*||||| ||------------ step into item_to_add -----------------------------------------------//*)
861 (*\\\\\ \\\----------- step into item_to_add -----------------------------------------------//*)
862 val return_item_to_add_STEP as SOME ("#Given", "FunctionVariable a") =
863 SOME (m_field, feedb |> I_Model.feedb_args_to_string ctxt)
864 (*\\\\\ \\------------ step into item_to_add -----------------------------------------------//*)
865 val SOME (fd, ct') = return_item_to_add;
866 (*||||| |------------- contine.. Step.for_method ---------------------------------------------*)
867 val return_for_method_STEP = ("dummy", (Pos.Met, P_Model.mk_additem fd ct'))
869 (*\\\\\ \------------- step into Step.for_method -------------------------------------------//*)
870 (*\------------------- step into me_Specify_Method -----------------------------------------//*)
872 val (p,_,f,nxt,_,pt) = return_me_Specify_Method;
873 val Add_Given "FunctionVariable a" = nxt;
874 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Input_Descript.Domain {0<..<r}" = nxt
875 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "ErrorBound (\<epsilon> = 0)" = nxt;
876 (*ErRoR type_of: type mismatch in application, bool, bool list, (#) [r = 7] --> 200a-start-method
877 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method xxx = nxt