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_
62 (model, I_Model.OLD_to_TEST probl);
63 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
64 (ctxt, where_rls, where_, (model, I_Model.OLD_to_TEST probl));
65 val (env_model, (env_subst, env_eval)) =
66 make_environments model_patt i_model;
67 "~~~~~ fun make_environments , args:"; val (_, []) = (model_patt, i_model);
68 (*\------------------- step into init_calc -------------------------------------------------//*)
69 val (p,_,f,nxt,_,pt) = return_init_calc; val Model_Problem = nxt
70 val (p, _, f, nxt, _, pt) = me nxt p c pt; val Add_Given "Constants [r = 7]" = nxt
71 val return_me_add_find_Constants =
72 me nxt p c pt; val Add_Find "Maximum A" = #4 return_me_add_find_Constants;
73 (*/------------------- step into me_add_find_Constants -------------------------------------\\*)
74 "~~~~~ fun me , args:"; val (tac as Add_Given "Constants [r = 7]", p, _(*NEW remove*), pt) =
76 val ctxt = Ctree.get_ctxt pt p
77 (*+*)val PblObj {probl = (1, [1, 2, 3], false, "#Given", Inc
78 ((Const ("Input_Descript.Constants", _), []), _)) :: _, ...} = get_obj I pt (fst p)
79 (*-------------------------------------------^^--*)
80 val return_step_by_tactic = (*case*)
81 Step.by_tactic tac (pt, p) (*of*);
82 (*//------------------ step into Step.by_tactic --------------------------------------------\\*)
83 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
84 val Applicable.Yes tac' =
85 (*case*) Specify_Step.check tac (pt, p) (*of*);
86 (*if*) Tactic.for_specify' tac' (*then*);
88 (** )val return_step_by_tactic =( **)
89 (**)val return_step_specify_by_tactic =(**)
90 Step_Specify.by_tactic tac' ptp;
91 (*///----------------- step into Step_Specify.by_tactic ------------------------------------\\*)
92 "~~~~~ fun by_tactic , args:"; val ((Tactic.Add_Given' (ct, _)), (pt, p)) = (tac', ptp);
94 (** )val calling_code =( **)
95 (**)val return_by_Add_ =(**)
96 Specify.by_Add_ "#Given" ct (pt, p);
97 (*////---------------- step by_Add_ --------------------------------------------------------\\*)
98 "~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, (pt, p));
99 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
102 (*if*) p_ = Pos.Met (*else*);
103 val (i_model, m_patt) =
105 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)
106 val I_Model.Add i_single =
107 (*case*) I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
109 (** )val i_model' =( **)
110 (**)val return_add_single =(**)
111 I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model;
112 (*/////--------------- step add_single -----------------------------------------------------\\*)
113 "~~~~~ fun add_single , args:"; val (thy, itm, model) =
114 ((Proof_Context.theory_of ctxt), i_single, i_model);
115 fun eq_untouched d (0, _, _, _, itm_) = (d = I_Model.descriptor itm_)
116 | eq_untouched _ _ = false
117 val model' = case I_Model.seek_ppc (#1 itm) model of
118 SOME _ => overwrite_ppc thy itm model (*itm updated in is_notyet_input WN.11.03*)
119 (*\\\\\--------------- 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), \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)]"
123 = i_model' |> I_Model.to_string ctxt
124 val tac' = I_Model.make_tactic m_field (ct, i_model')
125 val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
126 val return_by_Add_step =
127 ("ok", ([(Tactic.input_from_T ctxt tac', tac', (pos, (Istate_Def.Uistate, ctxt)))],
129 (*+++*)val {probl, ...} = Calc.specify_data (pt', pos);
130 (*+++*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , 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)]"
131 = probl |> I_Model.to_string ctxt
132 (*\\\\---------------- step into by_Add_ ---------------------------------------------------//*)
133 val return_by_tactic_step = return_by_Add_
134 (*\\\----------------- step into Step_Specify.by_tactic ------------------------------------//*)
135 (*vvv--- this means, the return value of *)
136 val return_step_by_tactic_STEP = return_step_specify_by_tactic
137 (*\\------------------ step into Step.by_tactic --------------------------------------------//*)
138 val ("ok", (_, _, ptp)) = return_step_by_tactic;
140 (*+++*)val (pt, p) = ptp
141 (*+++*)val {probl, ...} = Calc.specify_data (pt, p);
142 (*+++*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , 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)]"
143 = probl |> I_Model.to_string ctxt;
145 val (pt, p) = ptp; (*case*)
146 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
147 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
148 (p, ((pt, Pos.e_pos'), []));
150 (*if*) Pos.on_calc_end ip (*else*);
151 val (_, probl_id, _) = Calc.references (pt, p);
153 (*case*) tacis (*of*);
155 (*if*) probl_id = Problem.id_empty (*else*);
158 val ("ok", ([(Add_Find "Maximum A", _, _)], [], _)) =
159 switch_specify_solve p_ (pt, ip);
160 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
161 (*if*) Pos.on_specification ([], state_pos) (*then*);
163 val ("ok", ([(Add_Find "Maximum A", _, _)], [], _)) =
164 specify_do_next (pt, input_pos);
165 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
166 val (_, (p_', tac)) =
167 Specify.find_next_step ptp;
168 "~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
169 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
170 spec = refs, ...} = Calc.specify_data (pt, pos);
171 val ctxt = Ctree.get_ctxt pt pos;
172 (*+*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , 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)]"
173 = pbl|> I_Model.to_string ctxt
176 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
178 (*if*) p_ = Pos.Pbl (*then*);
180 (** )val ("dummy", (Pbl, Add_Find "Maximum A")) =( **)
181 (**)val return_for_problem as ("dummy", (Pbl, Add_Find "Maximum A"))=(**)
182 for_problem ctxt oris (o_refs, refs) (pbl, I_Model.OLD_to_TEST met);
183 (*//------------------ step into for_problem -----------------------------------------------\\*)
184 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
185 (ctxt, oris, (o_refs, refs), (pbl, met));
186 val cpI = if pI = Problem.id_empty then pI' else pI;
187 val cmI = if mI = MethodC.id_empty then mI' else mI;
188 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
189 val {model = mpc, ...} = MethodC.from_store ctxt cmI
191 (** )val (preok, _) =( **)
192 (**)val return_check =(**)
193 Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
194 (*///----------------- step into Pre_Conds.check -------------------------------------------\\*)
195 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
196 (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
198 (** )val (_, (env_subst, env_eval)) =( **)
199 (**)val return_make_environments =(**)
200 Pre_Conds.make_environments model_patt i_model;
201 (*////---------------- step into make_environments -----------------------------------------\\*)
202 "~~~~~ fun make_environments , args:"; val (model_patt, i_model) = (model_patt, i_model);
203 val equal_descr_pairs = map (get_equal_descr i_model) model_patt
206 val env_model = make_env_model equal_descr_pairs
207 (** )val env_model =( **)
208 (**)val return_make_env_model =(**)
209 make_env_model equal_descr_pairs;
210 (*/////--------------- step into make_env_model --------------------------------------------\\*)
211 "~~~~~ fun make_env_model , args:"; val (equal_descr_pairs) = (equal_descr_pairs);
212 val return_make_env_model_step =
213 map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
214 => (mk_env_model id feedb)) equal_descr_pairs
216 (*map:*)val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 2 equal_descr_pairs);
218 (*///// /------------- step into mk_env_model ----------------------------------------------\\*)
219 "~~~~~ fun mk_env_model , args:"; val (_, (Model_Def.Inc_TEST (_, []))) = (id, feedb);
220 (*+*)val (patt, imod) = nth 2 equal_descr_pairs
221 (*+*)val "(#Find, (Maximum, maxx))" = patt |> Model_Pattern.pat2str ctxt
222 (*+*)val "(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T))" = imod |> I_Model.single_to_string_TEST ctxt
224 val return_mk_env_model_2_step = []
225 (*\\\\\ \------------- step into mk_env_model ----------------------------------------------//*)
226 (*\\\\\--------------- step into make_env_model --------------------------------------------//*)
227 val env_model = return_make_env_model;
229 (*||||---------------- contine.. make_environments -------------------------------------------*)
230 val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
232 (** )val subst_eval_list =( **)
233 (**)val return_make_envs_preconds =(**)
234 make_envs_preconds equal_givens;
235 (*/////--------------- step into make_envs_preconds ----------------------------------------\\*)
236 "~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
237 val return_make_envs_preconds_step =
238 map (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb) equal_givens
242 val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 1 equal_givens
243 (*\\\\\--------------- step into make_envs_preconds ----------------------------------------//*)
244 val subst_eval_list = return_make_envs_preconds;
245 val (env_subst, env_eval) = split_list subst_eval_list
247 val return_make_environments_step = (env_model, (env_subst, env_eval));
248 (*+*)if return_make_environments_step = return_make_environments
249 then () else error "return_make_environments_step <> return_make_environments";
250 (*\\\\---------------- step into make_environments -----------------------------------------//*)
251 (*|||----------------- contine.. Pre_Conds.check ---------------------------------------------*)
252 val (env_model, (env_subst, env_eval)) = return_make_environments
253 val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
254 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
255 val full_subst = if env_eval = [] then pres_subst_other
256 else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
257 val evals = map (eval ctxt where_rls) full_subst
259 val return_make_environments_step = (foldl and_ (true, map fst evals), pres_subst_other)
260 (*\\\----------------- step into Pre_Conds.check -------------------------------------------//*)
261 (*||------------------ contine.. for_problem -------------------------------------------------*)
262 val (preok, _) = return_check;
265 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
267 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
269 (*case*) find_first (fn (_, _, _, _, feedb) => I_Model.is_error feedb) pbl (*of*);
271 val SOME (fd, ct' as "Maximum A") = (*case*)
272 item_to_add ctxt oris (I_Model.OLD_to_TEST pbl) (*of*);
273 "~~~~~ fun item_to_add , args:"; val (ctxt, o_model, i_model) = (ctxt, oris, (I_Model.OLD_to_TEST pbl));
274 val max_vnt = last_elem (*this decides, for which variant initially help is given*)
275 (Model_Def.max_variants o_model i_model)
276 val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model
277 val i_to_select = i_model
278 |> filter_out (fn (_, vnts, _, _, (I_Model.Cor_TEST _, _)) => member op= vnts max_vnt | _ => false)
283 val SOME (_, _, _, m_field, (feedb, _)) = (*case*)
284 I_Model.fill_from_o o_vnts i_to_select (*of*);
285 (*+*)val "Cor_TEST Maximum A , pen2str" = feedb |> I_Model.feedback_TEST_to_string ctxt;
287 "~~~~~ fun fill_from_o , args:"; val (o_model, (i, vnts, bool, m_field, (feedb, pos))) =
288 (o_vnts, i_to_select);
289 val (m_field, all_value as [Free ("A", _)]) =
290 case find_first (fn (_, _, _, descr', _) => Pre_Conds.descriptor_exists descr' feedb) o_model of
291 SOME (_, _, m_field, _, ts) => (m_field, ts)
292 val descr = Pre_Conds.get_dscr'' feedb (*i_single has been filtered appropriately*)
295 (*if*) Model_Def.is_list_descr descr (*else*);
296 val return_fill_from_o_STEP = SOME (i, vnts, bool, m_field,
297 (Inc_TEST (descr, all_value), pos))
298 (*\------------------- step into me_add_find_Constants -------------------------------------//*)
299 val (p,_,f,nxt,_,pt) = return_me_add_find_Constants;
300 val Add_Find "Maximum A" = nxt
302 (** )val (p,_,f,nxt,_,pt) =( **)
303 (**)val return_me_Add_Find_Maximum =(**)
304 me nxt p c pt; val Add_Find "AdditionalValues [u]" = #4 return_me_Add_Find_Maximum;
305 (*/------------------- step into me_Add_Find_Maximum ---------------------------------------\\*)
306 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
307 val ctxt = Ctree.get_ctxt pt p
309 case Step.by_tactic tac (pt, p) of
310 ("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, I_Model.OLD_to_TEST met);
347 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
348 (ctxt, oris, (o_refs, refs), (pbl, I_Model.OLD_to_TEST 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, I_Model.OLD_to_TEST 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 (I_Model.OLD_to_TEST pbl) (*of*);
364 "~~~~~ fun item_to_add , args:"; val (ctxt, o_model, i_model) =
365 (ctxt, oris, (I_Model.OLD_to_TEST pbl));
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_TEST _, _)) => member op= vnts max_vnt | _ => false)
372 (*ERROR*)val "[\n(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [] [__=__, __=__], Position.T))]"
373 = i_to_select |> I_Model.to_string_TEST 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, I_Model.OLD_to_TEST 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, I_Model.OLD_to_TEST pbl);
440 (*///// //------------ step into check -------------------------------------------------\\*)
441 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
442 (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST 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_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
447 = i_model |> I_Model.to_string_TEST 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 (I_Model.OLD_to_TEST pbl) (*of*);
484 "~~~~~ fun item_to_add , args:"; val (ctxt, o_model, i_model) = (ctxt, oris, (I_Model.OLD_to_TEST 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_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
489 = i_model |> I_Model.to_string_TEST 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_TEST _, _)) => 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
627 val {origin = (o_model, _, _), probl = i_prob, ctxt,
628 ...} = Calc.specify_data (ctree, pos);
629 val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
630 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
631 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
633 val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = met_imod, ctxt,
634 ...} = Calc.specify_data (ctree, pos);
635 val ctxt = Ctree.get_ctxt ctree pos
636 val (dI, _, _) = References.select_input o_refs refs;
637 val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
638 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
639 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
642 (**)val return_match_itms_oris = (**)
643 (** )val (_, (i_model, _)) = ( **)
645 M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
647 M_Match.match_itms_oris ctxt o_model' (I_Model.OLD_to_TEST i_prob, I_Model.OLD_to_TEST i_prob)
648 (m_patt, where_, where_rls);
650 (*//################## @ {context} within fun match_itms_oris -----------------------------\\*)
651 (*///----------------- step into match_itms_oris -------------------------------------------\\*)
652 "~~~~~ fun match_itms_oris, args:"; val (ctxt, o_model, (pbl_imod, met_imod), (m_patt, where_, where_rls)) =
653 (ctxt, o_model', (I_Model.OLD_to_TEST i_prob, I_Model.OLD_to_TEST i_prob), (m_patt, where_, where_rls));
655 (**)val return_fill_method =(**)
656 (** )val met_imod =( **)
657 fill_method o_model (pbl_imod, met_imod) m_patt;
658 (*////--------------- step into fill_method -----------------------------------------------\\*)
659 "~~~~~ fun fill_method , args:"; val (o_model, (pbl_imod, met_imod), met_patt) =
660 (o_model, (pbl_imod, met_imod), m_patt);
662 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
663 = pbl_imod |> I_Model.to_string_TEST ctxt
664 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
665 = met_imod |> I_Model.to_string_TEST ctxt
667 (**)val return_max_variants =(**)
668 (** )val pbl_max_vnts as [2, 1] =( **)
669 Model_Def.max_variants o_model pbl_imod;
670 (*//------------------ step into max_variants ----------------------------------------------\\*)
671 "~~~~~ fun max_variants , args:"; val (o_model, i_model) = (o_model, pbl_imod);
672 val all_variants as [1, 2, 3] =
673 map (fn (_, variants, _, _, _) => variants) i_model
676 val variants_separated = map (filter_variants' i_model) all_variants
677 (*+*)val ["[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]",
678 "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]",
679 "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T))]"]
680 = variants_separated |> map (I_Model.to_string_TEST ctxt)
682 val sums_corr as [5, 5, 4] = map (cnt_corrects) variants_separated
683 (*----------------#--#--#*)
684 (*---------------------^-------^-------^*)
685 val sum_variant_s as [(5, 1), (5, 2), (4, 3)] = arrange_args sums_corr (1, all_variants)
686 val max_first as [(5, 2), (5, 1), (4, 3)] = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
687 (*----------------##====--##====--//////---------^^^^*)
688 (*------------^--^-#-------#*)
689 val maxes as [2, 1] = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first
691 val return_max_variants = maxes
692 (*\\------------------ step into max_variants ----------------------------------------------//*)
693 val pbl_max_vnts as [2, 1] = return_max_variants;
695 (*probably pbl/met_imod = [], so take met_patt; if empty return Sup*)
696 val i_from_met = map (fn (_, (descr, _)) => (*order from met_patt*)
697 Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt (*\<longrightarrow> right order for args*)
698 (*+MET: Sup..*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
699 = i_from_met |> I_Model.to_string_TEST ctxt
701 val met_max_vnts as [2, 1] = Model_Def.max_variants o_model i_from_met;
702 val max_vnt as 2 = hd (inter op= pbl_max_vnts met_max_vnts);
703 (*add items from pbl_imod (without overwriting existing items in met_imod)*)
705 val return_add_other = map (
706 add_other max_vnt pbl_imod) i_from_met;
707 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
708 = return_add_other |> I_Model.to_string_TEST ctxt;
709 (*/////-------------- step into add_other -------------------------------------------------\\*)
710 "~~~~~ fun add_other_5 , args:"; val (max_vnt, i1_model, (i2, _, bool2, m_field2, (Sup_TEST (descr2, ts2), pos2))) =
711 (max_vnt, pbl_imod, nth 5 i_from_met);
713 (*+*)val Const ("Input_Descript.FunctionVariable", _) = descr2;
715 val (_, vnts1, _, _, (feedb1, _)) = (i2, [], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2))
716 val SOME (descr1 as (Const ("Input_Descript.FunctionVariable", _)) ) =
721 Model_Def.member_vnt vnts1 max_vnt
723 find_first (fn (_, vnts1, _, _, (feedb1, _)) => case get_dscr' feedb1 of
725 | SOME descr1 => descr1 = descr2 andalso Model_Def.member_vnt vnts1 max_vnt) i1_model
727 val return_add_other_1 = (i2, [max_vnt], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2))
728 val check as true = return_add_other_1 = nth 5 return_add_other
729 (*\\\\\-------------- step into add_other -------------------------------------------------//*)
730 val i_from_pbl = return_add_other
731 (*\\\\---------------- step into fill_method -----------------------------------------------//*)
732 val return_fill_method_step = filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) i_from_met
734 (*+MET: dropped ALL DUE TO is_empty_single_TEST*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]" =
735 return_fill_method_step |> I_Model.to_string_TEST ctxt
736 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
737 = return_fill_method |> I_Model.to_string_TEST ctxt;
738 return_fill_method_step = return_fill_method; (*latter is correct, did not investigate further*)
739 (*\\\----------------- step into match_itms_oris -------------------------------------------//*)
740 (*\\################# @ {context} within fun match_itms_oris ------------------------------//*)
741 val (_, (i_model, _)) = return_match_itms_oris;
743 (*||------------------ continue. complete_for ------------------------------------------------*)
744 val (o_model, ctxt, i_model) = return_complete_for
745 (*+isa*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
746 = i_model |> I_Model.to_string_TEST ctxt(*+isa*)
747 (*+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)]" =
748 i_model |> I_Model.to_string ctxt ( *+isa2*)
749 (*\\------------------ step into complete_for ----------------------------------------------//*)
750 val (o_model, ctxt, i_model) = return_complete_for
752 (*|------------------- continue. complete_for ------------------------------------------------*)
753 val return_complete_for_step = (o_model', ctxt', i_model)
755 val (o_model'_step, i_model_step) = (#1 return_complete_for_step, #3 return_complete_for_step)
756 val (o_model', i_model) = (#1 return_complete_for, #3 return_complete_for)
758 (*+*)if (o_model'_step, i_model_step) = (o_model', i_model)
759 (*+*)then () else error "return_complete_for_step <> return_complete_for";
760 (*\------------------- step into me Specify_Problem ----------------------------------------//*)
761 val (p,_,f,nxt,_,pt) = return_me_Specify_Problem
763 val return_me_Specify_Method
764 = me nxt p c pt; val Add_Given "FunctionVariable a" = #4 return_me_Specify_Method;
765 (*/------------------- step into me_Specify_Method -----------------------------------------\\*)
766 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
768 (*+*)val "[]" =(*+*) get_obj g_met pt (fst p) |> I_Model.to_string ctxt
770 val ctxt = Ctree.get_ctxt pt p
772 case Step.by_tactic tac (pt, p) of
773 ("ok", (_, _, ptp)) => ptp;
775 (*quick step into --> me_Specify_Method*)
776 (*+*)val Specify_Method ["Optimisation", "by_univariate_calculus"] = tac;
778 "~~~~~ fun by_tactic , args:"; val () = ();
780 "~~~~~ fun check , args:"; val () = ();
781 (*Specify_Step.check (Tactic.Specify_Method*)
782 "~~~~~ fun check , args:"; val () = ();
783 (*Specify_Step.complete_for*)
784 "~~~~~ fun complete_for , args:"; val () = ();
785 (* M_Match.match_itms_oris*)
786 "~~~~~ fun match_itms_oris , args:"; val () = ();
788 (*+isa*)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(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(0 ,[2] ,false ,i_model_empty ,Sup FunctionVariable), \n(0 ,[2] ,false ,i_model_empty ,Sup Input_Descript.Domain), \n(0 ,[2] ,false ,i_model_empty ,Sup ErrorBound), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str)]"
789 = get_obj g_met pt (fst p) |> I_Model.to_string ctxt;
792 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
793 (*//------------------ step into Step.do_next ----------------------------------------------\\*)
794 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
795 (*if*) Pos.on_calc_end ip (*else*);
796 val (_, probl_id, _) = Calc.references (pt, p);
798 (*case*) tacis (*of*);
799 (*if*) probl_id = Problem.id_empty (*else*);
801 Step.switch_specify_solve p_ (pt, ip);
802 (*///----------------- step into Step.switch_specify_solve ---------------------------------\\*)
803 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
804 (*if*) Pos.on_specification ([], state_pos) (*then*);
806 Step.specify_do_next (pt, input_pos);
807 (*////---------------- step into Step.specify_do_next --------------------------------------\\*)
808 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
810 val (_, (p_', tac)) =
811 Specify.find_next_step ptp;
812 (*/////--------------- step into find_next_step --------------------------------------------\\*)
813 "~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
814 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
815 spec = refs, ...} = Calc.specify_data (pt, pos);
816 val ctxt = Ctree.get_ctxt pt pos;
817 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
818 (*if*) p_ = Pos.Pbl (*else*);
820 (*+isa*)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(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(0 ,[2] ,false ,i_model_empty ,Sup FunctionVariable), \n(0 ,[2] ,false ,i_model_empty ,Sup Input_Descript.Domain), \n(0 ,[2] ,false ,i_model_empty ,Sup ErrorBound), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str)]"
821 = met |> I_Model.to_string ctxt;
823 (**)val ("dummy", (Met, Add_Given "FunctionVariable a")) =(**)
824 Specify.for_method ctxt oris (o_refs, refs) (pbl, met);
825 (*///// /------------- step into Step.for_method -------------------------------------------\\*)
826 "~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (_, met))
827 = (ctxt, oris, (o_refs, refs), (pbl, met));
828 val cmI = if mI = MethodC.id_empty then mI' else mI;
829 val {model, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
830 val (preok, _) = Pre_Conds.check ctxt where_rls where_ (model, I_Model.OLD_to_TEST met);
832 (*case*) find_first (I_Model.is_error o #5) met (*of*);
834 (** )SOME (fd, ct') =( **)
835 (**)val return_item_to_add =(**)
837 Specify.item_to_add ctxt oris (I_Model.OLD_to_TEST met) (*of*);
838 (*///// //------------ step into item_to_add -----------------------------------------------\\*)
839 "~~~~~ fun item_to_add , args:"; val (ctxt, o_model, i_model) = (ctxt, oris, I_Model.OLD_to_TEST met);
840 (*+*)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\"])]"
841 = oris |> O_Model.to_string ctxt
842 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
843 = i_model |> I_Model.to_string_TEST ctxt
845 val max_vnt = last_elem (*this decides, for which variant initially help is given*)
846 (Model_Def.max_variants o_model i_model)
847 val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model
848 val i_to_select = i_model
849 |> filter_out (fn (_, vnts, _, _, (I_Model.Cor_TEST _, _)) => member op= vnts max_vnt | _ => false)
851 (*+*)val "[\n(0, [2], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T))]"
852 = i_to_select |> I_Model.to_string_TEST ctxt
855 (*if*) i_to_select = [] (*else*);
857 (** )val SOME (_, _, _, m_field, (feedb, _)) =( **)
858 (**)val return_fill_from_o = (**)
859 (*case*) I_Model.fill_from_o o_vnts (hd i_to_select) (*of*);
860 (*///// ///----------- step into fill_from_o -----------------------------------------------\\*)
861 "~~~~~ fun fill_from_o , args:"; val (o_model, (i, vnts, bool, _, (feedb, pos))) =
862 (o_vnts, (hd i_to_select));
863 val (m_field, all_value) =
864 case find_first (fn (_, _, _, descr', _) => Pre_Conds.descriptor_exists descr' feedb) o_model of
865 SOME (_, _, m_field, _, ts) => (m_field, ts)
866 val descr = Pre_Conds.get_dscr'' feedb (*i_single has been filtered appropriately*)
868 (*if*) Model_Def.is_list_descr descr (*else*);
869 val return_fill_from_o_STEP = SOME (i, vnts, bool, m_field, (Cor_TEST (descr, all_value), pos))
870 (*-------------------- stopped after ERROR found ---------------------------------------------*)
871 (*\\\\\ \\\----------- step into fill_from_o -----------------------------------------------//*)
872 val SOME (_, _, _, m_field, (feedb, _)) = return_fill_from_o
874 (*||||| ||------------ step into item_to_add -----------------------------------------------//*)
875 (*\\\\\ \\\----------- step into item_to_add -----------------------------------------------//*)
876 val return_item_to_add_STEP as SOME ("#Given", "FunctionVariable a") =
877 SOME (m_field, feedb |> I_Model.feedb_args_to_string ctxt)
878 (*\\\\\ \\------------ step into item_to_add -----------------------------------------------//*)
879 val SOME (fd, ct') = return_item_to_add;
880 (*||||| |------------- contine.. Step.for_method ---------------------------------------------*)
881 val return_for_method_STEP = ("dummy", (Pos.Met, P_Model.mk_additem fd ct'))
883 (*\\\\\ \------------- step into Step.for_method -------------------------------------------//*)
884 (*\------------------- step into me_Specify_Method -----------------------------------------//*)
886 val (p,_,f,nxt,_,pt) = return_me_Specify_Method;
887 val Add_Given "FunctionVariable a" = nxt;
888 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Input_Descript.Domain {0<..<r}" = nxt
889 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "ErrorBound (\<epsilon> = 0)" = nxt;
890 (*ErRoR type_of: type mismatch in application, bool, bool list, (#) [r = 7] --> 200a-start-method
891 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method xxx = nxt