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_POS probl);
63 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
64 (ctxt, where_rls, where_, (model, I_Model.OLD_to_POS 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;
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 = descriptor_POS 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 -----------------------------------------------------//*)
121 (*|||||--------------- step by_Add_ ----------------------------------------------------------*)
122 val i_model' = return_add_single
123 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_POS Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_POS AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_POS Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_POS SideConditions [] [__=__, __=__], Position.T))]"
124 = i_model' |> I_Model.to_string_POS ctxt
126 val tac' = I_Model.make_tactic m_field (ct, i_model')
127 val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
128 val return_by_Add_step =
129 ("ok", ([(Tactic.input_from_T ctxt tac', tac', (pos, (Istate_Def.Uistate, ctxt)))],
131 (*+++*)val {probl, ...} = Calc.specify_data (pt', pos);
132 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_POS Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_POS AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_POS Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_POS SideConditions [] [__=__, __=__], Position.T))]"
133 = probl |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt
134 (*\\\\---------------- step into by_Add_ ---------------------------------------------------//*)
135 val return_by_tactic_step = return_by_Add_
136 (*\\\----------------- step into Step_Specify.by_tactic ------------------------------------//*)
137 (*vvv--- this means, the return value of *)
138 val return_step_by_tactic_STEP = return_step_specify_by_tactic
139 (*\\------------------ step into Step.by_tactic --------------------------------------------//*)
140 val ("ok", (_, _, ptp)) = return_step_by_tactic;
142 (*+++*)val (pt, p) = ptp
143 (*+++*)val {probl, ...} = Calc.specify_data (pt, p);
144 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_POS Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_POS AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_POS Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_POS SideConditions [] [__=__, __=__], Position.T))]"
145 = probl |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt;
147 val (pt, p) = ptp; (*case*)
148 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
149 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
150 (p, ((pt, Pos.e_pos'), []));
152 (*if*) Pos.on_calc_end ip (*else*);
153 val (_, probl_id, _) = Calc.references (pt, p);
155 (*case*) tacis (*of*);
157 (*if*) probl_id = Problem.id_empty (*else*);
160 val ("ok", ([(Add_Find "Maximum A", _, _)], [], _)) =
161 switch_specify_solve p_ (pt, ip);
162 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
163 (*if*) Pos.on_specification ([], state_pos) (*then*);
165 val ("ok", ([(Add_Find "Maximum A", _, _)], [], _)) =
166 specify_do_next (pt, input_pos);
167 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
168 val (_, (p_', tac)) =
169 Specify.find_next_step ptp;
170 "~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
171 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
172 spec = refs, ...} = Calc.specify_data (pt, pos);
173 val ctxt = Ctree.get_ctxt pt pos;
174 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_POS Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_POS AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_POS Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_POS SideConditions [] [__=__, __=__], Position.T))]"
175 = pbl |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt(*+*)
178 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
180 (*if*) p_ = Pos.Pbl (*then*);
182 (** )val ("dummy", (Pbl, Add_Find "Maximum A")) =( **)
183 (**)val return_for_problem as ("dummy", (Pbl, Add_Find "Maximum A"))=(**)
184 for_problem ctxt oris (o_refs, refs) (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met);
185 (*//------------------ step into for_problem -----------------------------------------------\\*)
186 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
187 (ctxt, oris, (o_refs, refs), (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met));
188 val cpI = if pI = Problem.id_empty then pI' else pI;
189 val cmI = if mI = MethodC.id_empty then mI' else mI;
190 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
191 val {model = mpc, ...} = MethodC.from_store ctxt cmI
193 (** )val (preok, _) =( **)
194 (**)val return_check =(**)
195 Pre_Conds.check ctxt where_rls where_ (pbt, pbl);
196 (*///----------------- step into Pre_Conds.check -------------------------------------------\\*)
197 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
198 (ctxt, where_rls, where_, (pbt, pbl));
200 (** )val (_, (env_subst, env_eval)) =( **)
201 (**)val return_make_environments =(**)
202 Pre_Conds.make_environments model_patt i_model;
203 (*////---------------- step into make_environments -----------------------------------------\\*)
204 "~~~~~ fun make_environments , args:"; val (model_patt, i_model) = (model_patt, i_model);
205 val equal_descr_pairs = map (get_equal_descr i_model) model_patt
208 val env_model = make_env_model equal_descr_pairs
209 (** )val env_model =( **)
210 (**)val return_make_env_model =(**)
211 make_env_model equal_descr_pairs;
212 (*/////--------------- step into make_env_model --------------------------------------------\\*)
213 "~~~~~ fun make_env_model , args:"; val (equal_descr_pairs) = (equal_descr_pairs);
214 val return_make_env_model_step =
215 map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
216 => (mk_env_model id feedb)) equal_descr_pairs
218 (*map:*)val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 2 equal_descr_pairs);
220 (*///// /------------- step into mk_env_model ----------------------------------------------\\*)
221 "~~~~~ fun mk_env_model , args:"; val (_, (Model_Def.Inc_POS (_, []))) = (id, feedb);
222 (*+*)val (patt, imod) = nth 2 equal_descr_pairs
223 (*+*)val "(#Find, (Maximum, maxx))" = patt |> Model_Pattern.single_to_string ctxt
224 (*+*)val "(2, [1, 2, 3], false ,#Find, (Inc_POS Maximum __, Position.T))" = imod |> I_Model.single_to_string_POS ctxt
226 val return_mk_env_model_2_step = []
227 (*\\\\\ \------------- step into mk_env_model ----------------------------------------------//*)
228 (*\\\\\--------------- step into make_env_model --------------------------------------------//*)
229 val env_model = return_make_env_model;
231 (*||||---------------- contine.. make_environments -------------------------------------------*)
232 val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
234 (** )val subst_eval_list =( **)
235 (**)val return_make_envs_preconds =(**)
236 make_envs_preconds equal_givens;
237 (*/////--------------- step into make_envs_preconds ----------------------------------------\\*)
238 "~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
239 val return_make_envs_preconds_step =
240 map (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb) equal_givens
244 val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 1 equal_givens
245 (*\\\\\--------------- step into make_envs_preconds ----------------------------------------//*)
246 val subst_eval_list = return_make_envs_preconds;
247 val (env_subst, env_eval) = split_list subst_eval_list
249 val return_make_environments_step = (env_model, (env_subst, env_eval));
250 (*+*)if return_make_environments_step = return_make_environments
251 then () else error "return_make_environments_step <> return_make_environments";
252 (*\\\\---------------- step into make_environments -----------------------------------------//*)
253 (*|||----------------- contine.. Pre_Conds.check ---------------------------------------------*)
254 val (env_model, (env_subst, env_eval)) = return_make_environments
255 val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
256 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
257 val full_subst = if env_eval = [] then pres_subst_other
258 else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
259 val evals = map (eval ctxt where_rls) full_subst
261 val return_make_environments_step = (foldl and_ (true, map fst evals), pres_subst_other)
262 (*\\\----------------- step into Pre_Conds.check -------------------------------------------//*)
263 (*||------------------ contine.. for_problem -------------------------------------------------*)
264 val (preok, _) = return_check;
267 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
269 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
271 (*case*) find_first (fn (_, _, _, _, (feedb, _)) => I_Model.is_error feedb) pbl (*of*);
273 val SOME (fd, ct' as "Maximum A") = (*case*)
274 item_to_add ctxt oris pbl (*of*);
275 "~~~~~ fun item_to_add , args:"; val (ctxt, o_model, i_model) = (ctxt, oris, pbl);
276 val max_vnt = last_elem (*this decides, for which variant initially help is given*)
277 (Model_Def.max_variants o_model i_model)
278 val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model
279 val i_to_select = i_model
280 |> filter_out (fn (_, vnts, _, _, (I_Model.Cor_POS _, _)) => member op= vnts max_vnt | _ => false)
285 val SOME (_, _, _, m_field, (feedb, _)) = (*case*)
286 I_Model.fill_from_o o_vnts i_to_select (*of*);
287 (*+*)val "Cor_POS Maximum A , pen2str" = feedb |> I_Model.feedback_POS_to_string ctxt;
289 "~~~~~ fun fill_from_o , args:"; val (o_model, (i, vnts, bool, m_field, (feedb, pos))) =
290 (o_vnts, i_to_select);
291 val (m_field, all_value as [Free ("A", _)]) =
292 case find_first (fn (_, _, _, descr', _) => Model_Def.descriptor_exists descr' feedb) o_model of
293 SOME (_, _, m_field, _, ts) => (m_field, ts)
294 val descr = Model_Def.get_descr feedb (*i_single has been filtered appropriately*)
297 (*if*) Model_Def.is_list_descr descr (*else*);
298 val return_fill_from_o_STEP = SOME (i, vnts, bool, m_field,
299 (Inc_POS (descr, all_value), pos))
300 (*\------------------- step into me_add_find_Constants -------------------------------------//*)
301 val (p,_,f,nxt,_,pt) = return_me_add_find_Constants;
302 val Add_Find "Maximum A" = nxt
304 (** )val (p,_,f,nxt,_,pt) =( **)
305 (**)val return_me_Add_Find_Maximum =(**)
306 me nxt p c pt; val Add_Find "AdditionalValues [u]" = #4 return_me_Add_Find_Maximum;
307 (*/------------------- step into me_Add_Find_Maximum ---------------------------------------\\*)
308 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
309 val ctxt = Ctree.get_ctxt pt p
311 case Step.by_tactic tac (pt, p) of
312 ("ok", (_, _, ptp)) => ptp;
314 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
315 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
316 (p, ((pt, Pos.e_pos'), []));
318 (*if*) Pos.on_calc_end ip (*else*);
319 val (_, probl_id, _) = Calc.references (pt, p);
322 (*case*) tacis (*of*);
324 (*if*) probl_id = Problem.id_empty (*else*);
326 switch_specify_solve p_ (pt, ip);
327 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
329 (*if*) Pos.on_specification ([], state_pos) (*then*);
331 specify_do_next (pt, input_pos);
332 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
334 (**)val (_, (p_', tac as Add_Find "AdditionalValues [u]")) =(**)
335 Specify.find_next_step ptp;
336 "~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
337 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
338 spec = refs, ...} = Calc.specify_data (pt, pos);
339 val ctxt = Ctree.get_ctxt pt pos
342 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
344 (*if*) p_ = Pos.Pbl (*then*);
346 (**)val return_find_next_step_STEP as ("dummy", (Pbl, Add_Find "AdditionalValues [u]")) =(**)
347 for_problem ctxt oris (o_refs, refs) (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met);
348 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
349 (ctxt, oris, (o_refs, refs), ( I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met));
350 val cpI = if pI = Problem.id_empty then pI' else pI;
351 val cmI = if mI = MethodC.id_empty then mI' else mI;
352 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
353 val {model = mpc, ...} = MethodC.from_store ctxt cmI
354 val (preok, _) = Pre_Conds.check ctxt where_rls where_ (pbt, pbl);
357 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
359 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
361 (*case*) find_first (fn (_, _, _, _, (feedb, _)) => I_Model.is_error feedb) pbl (*of*);
363 (**)val SOME (fd, ct' as "AdditionalValues [u]") = (*case*)(**)
364 item_to_add ctxt oris pbl (*of*);
365 "~~~~~ fun item_to_add , args:"; val (ctxt, o_model, i_model) =
367 val max_vnt = last_elem (*this decides, for which variant initially help is given*)
368 (Model_Def.max_variants o_model i_model)
369 val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model
370 val i_to_select = i_model
371 |> filter_out (fn (_, vnts, _, _, (I_Model.Cor_POS _, _)) => member op= vnts max_vnt | _ => false)
373 (*ERROR*)val "[\n(3, [1, 2, 3], false ,#Find, (Inc_POS AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_POS Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_POS SideConditions [] [__=__, __=__], Position.T))]"
374 = i_to_select |> I_Model.to_string_POS ctxt(*ERROR*)
377 (*if*) i_to_select = []
379 val SOME (_, _, _, m_field, (feedb, _)) = (*case*)
380 I_Model.fill_from_o o_vnts (hd i_to_select) (*of*);
381 "~~~~~ fun fill_from_o , args:";
382 (*==================== see test/../i-model.sml --- fun item_to_add ===========================*)
383 (*\------------------- step into me_Add_Find_Maximum ---------------------------------------//*)
384 val (p,_,f,nxt,_,pt) = return_me_Add_Find_Maximum;
385 val Add_Find "AdditionalValues [u]" = nxt
386 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*)
387 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)" = nxt;
388 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;
390 val return_me_Add_Relation_SideConditions as (_, _, _, Specify_Theory "Diff_App", _, _)
392 (*/------------------- step into me Add_Relation_SideConditions ----------------------------\\*)
393 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
394 val ctxt = Ctree.get_ctxt pt p;
395 (**) val (pt, p) = (**)
396 (**)case(**) Step.by_tactic tac (pt, p) (**)of(**)
397 (**) ("ok", (_, _, ptp)) => ptp (**) ;
400 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
401 (*//------------------ step into do_next ---------------------------------------------------\\*)
402 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
403 = (p, ((pt, Pos.e_pos'), [])) (*of*);
404 (*if*) Pos.on_calc_end ip (*else*);
405 val (_, probl_id, _) = Calc.references (pt, p);
406 (*case*) tacis (*of*);
407 (*if*) probl_id = Problem.id_empty (*else*);
409 Step.switch_specify_solve p_ (pt, ip);
410 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
411 (*if*) Pos.on_specification ([], state_pos) (*then*);
413 Step.specify_do_next (pt, input_pos);
414 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
415 val (_, (p_', tac as Specify_Theory "Diff_App")) =
416 Specify.find_next_step ptp;
417 "~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
418 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
419 spec = refs, ...} = Calc.specify_data (pt, pos);
420 val ctxt = Ctree.get_ctxt pt pos;
421 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
422 (*if*) p_ = Pos.Pbl (*then*);
424 (** )val ("dummy", (Pbl, tac as Specify_Theory "Diff_App")) =( **)
425 (**)val return_for_problem =(**)
426 for_problem ctxt oris (o_refs, refs) (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met);
427 (*///// /------------- step into for_problem -----------------------------------------------\\*)
428 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
429 (ctxt, oris, (o_refs, refs), (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met));
430 val cpI = if pI = Problem.id_empty then pI' else pI;
431 val cmI = if mI = MethodC.id_empty then mI' else mI;
432 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
433 val {model = mpc, ...} = MethodC.from_store ctxt cmI
435 (*+*)val [Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
436 Free ("fixes", _)] = where_;
438 (** )val (preok, _) =( **)
439 (**)return_check =(**)
440 Pre_Conds.check ctxt where_rls where_ (pbt, pbl);
441 (*///// //------------ step into check -------------------------------------------------\\*)
442 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
443 (ctxt, where_rls, where_, (pbt, pbl));
444 (*+*)val "[0 < fixes]" = pres |> UnparseC.terms ctxt
445 (*+*)val "[\"(#Given, (Constants, fixes))\", \"(#Find, (Maximum, maxx))\", \"(#Find, (AdditionalValues, vals))\", \"(#Relate, (Extremum, extr))\", \"(#Relate, (SideConditions, sideconds))\"]"
446 (*+*) = model_patt |> Model_Pattern.to_string ctxt
447 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
448 = i_model |> I_Model.to_string_POS ctxt
450 val return_make_environments as (_, (env_subst, env_eval)) =
451 Pre_Conds.make_environments model_patt i_model
453 (*+*)val [(Free ("fixes", T1), Free ("r", T2))] = env_subst (*?!? Const*)
454 (*+*)val Type ("Real.real", []) = T1
455 (*+*)val Type ("Real.real", []) = T2
457 (*+*)val [(Free ("r", T2), Const ("Num.numeral_class.numeral", _) $ _)] = env_eval
458 (*+*)val Type ("Real.real", []) = T2
460 val (_, (env_subst, env_eval)) = return_make_environments;
461 (*|||----------------- contine check -----------------------------------------------------*)
462 val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
463 (*+*)val [(true, Const ("Orderings.ord_class.less", _) $
464 Const ("Groups.zero_class.zero", _) $ Free ("r", _))] = pres_subst
466 val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
468 Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
469 (Const ("Num.numeral_class.numeral", _) $ _))] = full_subst
471 val evals = map (eval ctxt where_rls) full_subst
472 val return_check_STEP = (foldl and_ (true, map fst evals), pres_subst)
473 (*\\\\\ \\------------ step into check -------------------------------------------------\\*)
474 val (preok as true, _) = return_check
476 (*||||| |------------- contine.. for_problem -------------------------------------------------*)
478 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
480 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
482 (*case*) find_first (fn (_, _, _, _, (feedb, _)) => I_Model.is_error feedb) pbl (*of*);
484 (*case*) item_to_add ctxt oris pbl (*of*);
485 "~~~~~ fun item_to_add , args:"; val (ctxt, o_model, i_model) = (ctxt, oris, pbl);
487 (*+*)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\"])]"
488 = o_model |> O_Model.to_string ctxt
489 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
490 = i_model |> I_Model.to_string_POS ctxt
492 val max_vnt as 1= last_elem (*this decides, for which variant initially help is given*)
493 (Model_Def.max_variants o_model i_model)
494 val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model
495 (*+*)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\"])]"
496 = o_vnts |> O_Model.to_string ctxt
498 val i_to_select = i_model
499 |> filter_out (fn (_, vnts, _, _, (I_Model.Cor_POS _, _)) => member op= vnts max_vnt | _ => false)
502 (*if*) i_to_select = [] (*then*);
504 val return_for_problem_STEP = NONE
505 (*\\\\\ \------------- step into for_problem -----------------------------------------------//*)
506 val calling_code = return_for_problem;
507 (*-------------------- stopped after ERROR found ---------------------------------------------*)
509 (*\\------------------ step into do_next ---------------------------------------------------\\*)
510 (*\------------------- step into me_Add_Relation_SideConditions ----------------------------//*)
511 val (p, _, f, nxt, _, pt) = return_me_Add_Relation_SideConditions
512 val Specify_Theory "Diff_App" = nxt;
514 val return_me_Specify_Theory
515 = me nxt p c pt; val Specify_Problem ["univariate_calculus", "Optimisation"] = #4 return_me_Specify_Theory;
516 (*/------------------- step into me_Specify_Theory -----------------------------------------\\*)
517 "~~~~~ fun me , args:"; val (tac as Specify_Theory "Diff_App", p, _, pt) = (nxt, p, c, pt);
518 val ctxt = Ctree.get_ctxt pt p;
520 (*case*) Step.by_tactic tac (pt, p) (*of*);
521 (* ("ok", (_, _, ptp)) => ptp *)
522 val return_Step_by_tactic =
523 Step.by_tactic tac (pt, p);
524 (*//------------------ step into Step_by_tactic --------------------------------------------\\*)
525 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
526 (*case*) Specify_Step.check tac (pt, p) (*of*);
528 (*||------------------ contine Step_by_tactic ------------------------------------------------*)
529 (*\\------------------ step into Step_by_tactic --------------------------------------------//*)
531 val ("ok", (_, _, ptp)) = return_Step_by_tactic;
532 (*|------------------- continue me Specify_Theory --------------------------------------------*)
534 val ("ok", (ts as (_, _, _) :: _, _, _)) =
536 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
537 (*//------------------ step into do_next ---------------------------------------------------\\*)
538 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
539 = (p, ((pt, Pos.e_pos'), [])) (*of*);
540 (*if*) Pos.on_calc_end ip (*else*);
541 val (_, probl_id, _) = Calc.references (pt, p);
543 (*case*) tacis (*of*);
544 (*if*) probl_id = Problem.id_empty (*else*);
546 Step.switch_specify_solve p_ (pt, ip);
547 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
548 (*if*) Pos.on_specification ([], state_pos) (*then*);
550 Step.specify_do_next (pt, input_pos);
551 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
552 val (_, (p_', tac)) = Specify.find_next_step ptp
553 val ist_ctxt = Ctree.get_loc pt (p, p_);
556 Step_Specify.by_tactic_input tac (pt, (p, p_'));
557 (*+*)val Specify_Theory "Diff_App" = tac;
558 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Theory dI), (pt, pos as (_, Pbl)))
559 = (tac, (pt, (p, p_')));
560 val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
561 PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
562 (oris, dI, dI', pI', probl, ctxt)
563 val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');
564 val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
565 (*\\------------------ step into do_next ---------------------------------------------------//*)
566 (*\------------------- step into me_Specify_Theory -----------------------------------------//*)
567 val (p,_,f,nxt,_,pt) = return_me_Specify_Theory;
569 val return_me_Specify_Problem (* keep for continuing me *)
570 = me nxt p c pt; val Specify_Method ["Optimisation", "by_univariate_calculus"] = #4 return_me_Specify_Problem;
571 (*/------------------- step into me_Specify_Problem ----------------------------------------\\*)
572 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
573 val ctxt = Ctree.get_ctxt pt p
575 (** ) val ("ok", (_, _, ptp as (pt, p))) =( **)
576 (**) val return_by_tactic =(**) (*case*)
577 Step.by_tactic tac (pt, p) (*of*);
578 (*//------------------ step into by_tactic -------------------------------------------------\\*)
579 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
582 Step.check tac (pt, p) (*of*);
583 "~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
584 (*if*) Tactic.for_specify tac (*then*);
586 Specify_Step.check tac (ctree, pos);
587 "~~~~~ fun check , args:"; val ((Tactic.Specify_Problem pID), (pt, pos as (p, _)))
588 = (tac, (ctree, pos));
589 val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of
590 Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
591 => (oris, dI, pI, dI', pI', itms)
592 val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');
593 (*\\------------------ step into by_tactic -------------------------------------------------//*)
594 val ("ok", (_, _, ptp as (pt, p))) = return_by_tactic (* kept for continuing me *);
597 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
598 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
599 (*if*) Pos.on_calc_end ip (*else*);
600 val (_, probl_id, _) = Calc.references (pt, p);
602 (*case*) tacis (*of*);
603 (*if*) probl_id = Problem.id_empty (*else*);
605 Step.switch_specify_solve p_ (pt, ip);
606 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
607 (*if*) Pos.on_specification ([], state_pos) (*then*);
609 Step.specify_do_next (pt, input_pos);
610 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
611 val (_, (p_', tac)) = Specify.find_next_step ptp
612 val ist_ctxt = Ctree.get_loc pt (p, p_)
616 Step_Specify.by_tactic_input tac (pt, (p, p_'));
617 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos))
618 = (tac, (pt, (p, p_')));
620 (**)val return_complete_for =(**)
621 (** ) val (o_model, ctxt, i_model) =( **)
622 Specify_Step.complete_for id (pt, pos);
623 (*//------------------ step into complete_for ----------------------------------------------\\*)
624 "~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));
626 (*+*)val ["Optimisation", "by_univariate_calculus"] = mID
627 val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = met_imod, ctxt,
628 ...} = Calc.specify_data (ctree, pos);
629 val ctxt = Ctree.get_ctxt ctree pos
630 val (dI, _, _) = References.select_input o_refs refs;
631 val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
632 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
633 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
635 (**)val return_match_itms_oris = (**)
636 (** )val (_, (i_model, _)) = ( **)
637 M_Match.by_i_models ctxt o_model' (I_Model.OLD_to_POS i_prob, I_Model.OLD_to_POS i_prob)
638 (m_patt, where_, where_rls);
639 (*///----------------- step into by_i_models -------------------------------------------\\*)
640 "~~~~~ fun by_i_models, args:"; val (ctxt, o_model, (pbl_imod, met_imod), (m_patt, where_, where_rls)) =
641 (ctxt, o_model', (I_Model.OLD_to_POS i_prob, I_Model.OLD_to_POS i_prob), (m_patt, where_, where_rls));
643 (**)val return_fill_method =(**)
644 (** )val met_imod =( **)
645 fill_method o_model (pbl_imod, met_imod) m_patt;
646 (*////--------------- step into fill_method -----------------------------------------------\\*)
647 "~~~~~ fun fill_method , args:"; val (o_model, (pbl_imod, met_imod), met_patt) =
648 (o_model, (pbl_imod, met_imod), m_patt);
650 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
651 = pbl_imod |> I_Model.to_string_POS ctxt
652 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
653 = met_imod |> I_Model.to_string_POS ctxt
655 (**)val return_max_variants =(**)
656 (** )val pbl_max_vnts as [2, 1] =( **)
657 Model_Def.max_variants o_model pbl_imod;
658 (*//------------------ step into max_variants ----------------------------------------------\\*)
659 "~~~~~ fun max_variants , args:"; val (o_model, i_model) = (o_model, pbl_imod);
660 val all_variants as [1, 2, 3] =
661 map (fn (_, variants, _, _, _) => variants) i_model
664 val variants_separated = map (filter_variants' i_model) all_variants
665 (*+*)val ["[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]",
666 "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]",
667 "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T))]"]
668 = variants_separated |> map (I_Model.to_string_POS ctxt)
670 val sums_corr as [5, 5, 4] = map (cnt_corrects) variants_separated
671 (*----------------#--#--#*)
672 (*---------------------^-------^-------^*)
673 val sum_variant_s as [(5, 1), (5, 2), (4, 3)] = arrange_args sums_corr (1, all_variants)
674 val max_first as [(5, 2), (5, 1), (4, 3)] = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
675 (*----------------##====--##====--//////---------^^^^*)
676 (*------------^--^-#-------#*)
677 val maxes as [2, 1] = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first
679 val return_max_variants = maxes
680 (*\\------------------ step into max_variants ----------------------------------------------//*)
681 val pbl_max_vnts as [2, 1] = return_max_variants;
683 (*probably pbl/met_imod = [], so take met_patt; if empty return Sup*)
684 val i_from_met = map (fn (_, (descr, _)) => (*order from met_patt*)
685 Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt (*\<longrightarrow> right order for args*)
686 (*+MET: Sup..*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n(0, [], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n(0, [], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"
687 = i_from_met |> I_Model.to_string_POS ctxt
689 val met_max_vnts as [2, 1] = Model_Def.max_variants o_model i_from_met;
690 val max_vnt as 2 = hd (inter op= pbl_max_vnts met_max_vnts);
691 (*add items from pbl_imod (without overwriting existing items in met_imod)*)
693 val return_add_other = map (
694 add_other max_vnt pbl_imod) i_from_met;
695 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"
696 = return_add_other |> I_Model.to_string_POS ctxt;
697 (*/////-------------- step into add_other -------------------------------------------------\\*)
698 "~~~~~ fun add_other_5 , args:"; val (max_vnt, i1_model, (i2, _, bool2, m_field2, (Sup_POS (descr2, ts2), pos2))) =
699 (max_vnt, pbl_imod, nth 5 i_from_met);
701 (*+*)val Const ("Input_Descript.FunctionVariable", _) = descr2;
703 val (_, vnts1, _, _, (feedb1, _)) = (i2, [], bool2, m_field2, (Sup_POS (descr2, ts2), pos2))
704 val SOME (descr1 as (Const ("Input_Descript.FunctionVariable", _)) ) =
709 Model_Def.member_vnt vnts1 max_vnt
711 find_first (fn (_, vnts1, _, _, (feedb1, _)) => case get_dscr_opt feedb1 of
713 | SOME descr1 => descr1 = descr2 andalso Model_Def.member_vnt vnts1 max_vnt) i1_model
715 val return_add_other_1 = (i2, [max_vnt], bool2, m_field2, (Sup_POS (descr2, ts2), pos2))
716 val check as true = return_add_other_1 = nth 5 return_add_other
717 (*\\\\\-------------- step into add_other -------------------------------------------------//*)
718 val i_from_pbl = return_add_other
719 (*\\\\---------------- step into fill_method -----------------------------------------------//*)
720 val return_fill_method_step = filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) i_from_met
722 (*+MET: dropped ALL DUE TO is_empty_single_POS*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]" =
723 return_fill_method_step |> I_Model.to_string_POS ctxt
724 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"
725 = return_fill_method |> I_Model.to_string_POS ctxt;
726 return_fill_method_step = return_fill_method; (*latter is correct, did not investigate further*)
727 (*\\\----------------- step into by_i_models -------------------------------------------//*)
728 val (_, (i_model, _)) = return_match_itms_oris;
730 (*||------------------ continue. complete_for ------------------------------------------------*)
731 val (o_model, ctxt, i_model) = return_complete_for
732 (*+isa*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"
733 = i_model |> I_Model.to_string_POS ctxt(*+isa*)
734 (*+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)]" =
735 i_model |> I_Model.to_string ctxt ( *+isa2*)
736 (*\\------------------ step into complete_for ----------------------------------------------//*)
737 val (o_model, ctxt, i_model) = return_complete_for
739 (*|------------------- continue. complete_for ------------------------------------------------*)
740 val return_complete_for_step = (o_model', ctxt', i_model)
742 val (o_model'_step, i_model_step) = (#1 return_complete_for_step, #3 return_complete_for_step)
743 val (o_model', i_model) = (#1 return_complete_for, #3 return_complete_for)
745 (*+*)if (o_model'_step, i_model_step) = (o_model', i_model)
746 (*+*)then () else error "return_complete_for_step <> return_complete_for";
747 (*\------------------- step into me Specify_Problem ----------------------------------------//*)
748 val (p,_,f,nxt,_,pt) = return_me_Specify_Problem
750 val return_me_Specify_Method
751 = me nxt p c pt; val Add_Given "FunctionVariable a" = #4 return_me_Specify_Method;
752 (*/------------------- step into me_Specify_Method -----------------------------------------\\*)
753 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
755 (*+*)val "[]" =(*+*) get_obj g_met pt (fst p) |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt
757 val ctxt = Ctree.get_ctxt pt p
759 case Step.by_tactic tac (pt, p) of
760 ("ok", (_, _, ptp)) => ptp;
762 (*quick step into --> me_Specify_Method*)
763 (*+*)val Specify_Method ["Optimisation", "by_univariate_calculus"] = tac;
765 "~~~~~ fun by_tactic , args:"; val () = ();
767 "~~~~~ fun check , args:"; val () = ();
768 (*Specify_Step.check (Tactic.Specify_Method*)
769 "~~~~~ fun check , args:"; val () = ();
770 (*Specify_Step.complete_for*)
771 "~~~~~ fun complete_for , args:"; val () = ();
772 (* M_Match.by_i_models*)
773 "~~~~~ fun by_i_models , args:"; val () = ();
775 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"
776 = get_obj g_met pt (fst p) |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt;
779 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
780 (*//------------------ step into Step.do_next ----------------------------------------------\\*)
781 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
782 (*if*) Pos.on_calc_end ip (*else*);
783 val (_, probl_id, _) = Calc.references (pt, p);
785 (*case*) tacis (*of*);
786 (*if*) probl_id = Problem.id_empty (*else*);
788 Step.switch_specify_solve p_ (pt, ip);
789 (*///----------------- step into Step.switch_specify_solve ---------------------------------\\*)
790 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
791 (*if*) Pos.on_specification ([], state_pos) (*then*);
793 Step.specify_do_next (pt, input_pos);
794 (*////---------------- step into Step.specify_do_next --------------------------------------\\*)
795 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
797 val (_, (p_', tac)) =
798 Specify.find_next_step ptp;
799 (*/////--------------- step into find_next_step --------------------------------------------\\*)
800 "~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
801 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
802 spec = refs, ...} = Calc.specify_data (pt, pos);
803 val ctxt = Ctree.get_ctxt pt pos;
804 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
805 (*if*) p_ = Pos.Pbl (*else*);
807 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"
808 = met |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt
810 (**)val ("dummy", (Met, Add_Given "FunctionVariable a")) =(**)
811 Specify.for_method ctxt oris (o_refs, refs) (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met);
812 (*///// /------------- step into Step.for_method -------------------------------------------\\*)
813 "~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (_, met))
814 = (ctxt, oris, (o_refs, refs), (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met));
815 val cmI = if mI = MethodC.id_empty then mI' else mI;
816 val {model, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
817 val (preok, _) = Pre_Conds.check ctxt where_rls where_ (model, met);
819 (*case*) find_first (I_Model.is_error o #1 o #5) met (*of*);
821 (** )SOME (fd, ct') =( **)
822 (**)val return_item_to_add =(**)
824 Specify.item_to_add ctxt oris met (*of*);
825 (*///// //------------ step into item_to_add -----------------------------------------------\\*)
826 "~~~~~ fun item_to_add , args:"; val (ctxt, o_model, i_model) = (ctxt, oris, met);
827 (*+*)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\"])]"
828 = oris |> O_Model.to_string ctxt
829 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"
830 = i_model |> I_Model.to_string_POS ctxt
832 val max_vnt = last_elem (*this decides, for which variant initially help is given*)
833 (Model_Def.max_variants o_model i_model)
834 val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model
835 val i_to_select = i_model
836 |> filter_out (fn (_, vnts, _, _, (I_Model.Cor_POS _, _)) => member op= vnts max_vnt | _ => false)
838 (*+*)val "[\n(0, [2], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS ErrorBound, Position.T))]"
839 = i_to_select |> I_Model.to_string_POS ctxt
842 (*if*) i_to_select = [] (*else*);
844 (** )val SOME (_, _, _, m_field, (feedb, _)) =( **)
845 (**)val return_fill_from_o = (**)
846 (*case*) I_Model.fill_from_o o_vnts (hd i_to_select) (*of*);
847 (*///// ///----------- step into fill_from_o -----------------------------------------------\\*)
848 "~~~~~ fun fill_from_o , args:"; val (o_model, (i, vnts, bool, _, (feedb, pos))) =
849 (o_vnts, (hd i_to_select));
850 val (m_field, all_value) =
851 case find_first (fn (_, _, _, descr', _) => Model_Def.descriptor_exists descr' feedb) o_model of
852 SOME (_, _, m_field, _, ts) => (m_field, ts)
853 val descr = Model_Def.get_descr feedb (*i_single has been filtered appropriately*)
855 (*if*) Model_Def.is_list_descr descr (*else*);
856 val return_fill_from_o_STEP = SOME (i, vnts, bool, m_field, (Cor_POS (descr, all_value), pos))
857 (*-------------------- stopped after ERROR found ---------------------------------------------*)
858 (*\\\\\ \\\----------- step into fill_from_o -----------------------------------------------//*)
859 val SOME (_, _, _, m_field, (feedb, _)) = return_fill_from_o
861 (*||||| ||------------ step into item_to_add -----------------------------------------------//*)
862 (*\\\\\ \\\----------- step into item_to_add -----------------------------------------------//*)
863 val return_item_to_add_STEP as SOME ("#Given", "FunctionVariable a") =
864 SOME (m_field, feedb |> I_Model.feedb_args_to_string ctxt)
865 (*\\\\\ \\------------ step into item_to_add -----------------------------------------------//*)
866 val SOME (fd, ct') = return_item_to_add;
867 (*||||| |------------- contine.. Step.for_method ---------------------------------------------*)
868 val return_for_method_STEP = ("dummy", (Pos.Met, P_Model.mk_additem fd ct'))
870 (*\\\\\ \------------- step into Step.for_method -------------------------------------------//*)
871 (*\------------------- step into me_Specify_Method -----------------------------------------//*)
873 val (p,_,f,nxt,_,pt) = return_me_Specify_Method;
874 val Add_Given "FunctionVariable a" = nxt;
875 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Input_Descript.Domain {0<..<r}" = nxt
876 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "ErrorBound (\<epsilon> = 0)" = nxt;
877 (*ErRoR type_of: type mismatch in application, bool, bool list, (#) [r = 7] --> 200a-start-method
878 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method xxx = nxt