66 |
66 |
67 \<close> ML \<open> |
67 \<close> ML \<open> |
68 \<close> |
68 \<close> |
69 |
69 |
70 section \<open>===================================================================================\<close> |
70 section \<open>===================================================================================\<close> |
|
71 section \<open>===== new code match_itms_oris ====================================================\<close> |
|
72 ML \<open> |
|
73 \<close> ML \<open> |
|
74 open Ctree; |
|
75 open Pos; |
|
76 open TermC; |
|
77 open Istate; |
|
78 open Tactic; |
|
79 open I_Model; |
|
80 open P_Model |
|
81 open Rewrite; |
|
82 open Step; |
|
83 open LItool; |
|
84 open LI; |
|
85 open Test_Code |
|
86 open Specify |
|
87 open ME_Misc |
|
88 open Pre_Conds; |
|
89 \<close> ML \<open> (*//----------- build fun match_itms_oris -------------------------------------------\\*) |
|
90 (*//------------------ build fun match_itms_oris -------------------------------------------\\*) |
|
91 \<close> ML \<open> |
|
92 \<close> text \<open> (*\<longrightarrow> model-def.sml*) |
|
93 fun member_vnt [] _ = true |
|
94 | member_vnt vnts vnt = member op= vnts vnt |
|
95 ; |
|
96 member_vnt: variants -> variant -> bool |
|
97 \<close> ML \<open> |
|
98 \<close> text \<open> (*\<longrightarrow> i-model.sml <> Pre_Conds.get_descr_vnt*) |
|
99 (* |
|
100 in case there is an item in i2_model = met with Sup_TEST, |
|
101 find_first an appropriate (variant, descriptor) item in i1_model = pbl and add it instead Sup_TEST, |
|
102 otherwise keep the items of i2_model. |
|
103 *) |
|
104 fun add_other max_vnt i1_model (i2, _, bool2, m_field2, (Sup_TEST (descr2, ts2), pos2)) = |
|
105 (case find_first (fn (_, vnts1, _, _, (feedb1, _)) => case Pre_Conds.get_dscr' feedb1 of |
|
106 NONE => false |
|
107 | SOME descr1 => descr1 = descr2 andalso Model_Def.member_vnt vnts1 max_vnt) i1_model of |
|
108 NONE => |
|
109 (i2, [max_vnt], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2)) (*the present in i2_model*) |
|
110 | SOME i1_single => i1_single) (*shift the item from i1_model to i2_model*) |
|
111 | add_other _ _ i2_single = i2_single (*keep all the other items in i2_model*) |
|
112 ; |
|
113 add_other: variant -> I_Model.T_TEST -> I_Model.single_TEST -> I_Model.single_TEST |
|
114 \<close> ML \<open> |
|
115 \<close> text \<open> (*\<longrightarrow> i-model.sml*) |
|
116 (* |
|
117 Establish the order of items (wrt. descriptor) in the method's i_model as given by meth_patt, |
|
118 i.e as required by the formal arguments of the program. |
|
119 Missing items are inserted as Sup(erfluous). |
|
120 /-TODO-----------------------^^-Inc [] ------- output with input-template automatically------\ |
|
121 \-TODO---------------------------------------------------------------------------------------/ |
|
122 In order to maintain what the user sees as Model, copy the items from the problem's i_model |
|
123 to the method's i_model. |
|
124 *) |
|
125 (*compare fun s_make_complete*) |
|
126 fun fill_method o_model (pbl_imod, met_imod) met_patt = |
|
127 let |
|
128 val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod |
|
129 (*probably pbl/met_imod = [], so take met_patt; if empty return Sup*) |
|
130 val i_from_met = map (fn (_, (descr, _)) => (*order from met_patt*) |
|
131 Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt (*\<longrightarrow> right order for args*) |
|
132 |
|
133 val met_max_vnts = Model_Def.max_variants o_model i_from_met; |
|
134 val max_vnt = hd (inter op= pbl_max_vnts met_max_vnts); |
|
135 (*add items from pbl_imod (without overwriting existing items in met_imod)*) |
|
136 in |
|
137 map (add_other max_vnt pbl_imod) i_from_met |
|
138 end |
|
139 ; |
|
140 fill_method: O_Model.T -> I_Model.T_TEST * I_Model.T_TEST-> Model_Pattern.T -> |
|
141 I_Model.T_TEST |
|
142 \<close> ML \<open> |
|
143 \<close> ML \<open> (*\<longrightarrow> m-match.sml*) |
|
144 (*the OLD version built upon a wrong idea with find missing items from o_model*) |
|
145 \<close> ML \<open> |
|
146 (*OLD*) |
|
147 (*---*) |
|
148 fun match_itms_oris ctxt o_model (pbl_imod, met_imod) (met_patt, where_, where_rls) = |
|
149 let |
|
150 val met_imod = I_Model.fill_method o_model (pbl_imod, met_imod) met_patt |
|
151 val (check, preconds) = Pre_Conds.check ctxt where_rls where_ (met_patt, met_imod) |
|
152 in |
|
153 (check, (met_imod, preconds)) |
|
154 end |
|
155 (*NEW*) |
|
156 ; |
|
157 match_itms_oris: Proof.context -> O_Model.T -> I_Model.T_TEST * I_Model.T_TEST -> |
|
158 Model_Pattern.T * Pre_Conds.unchecked * Rule_Def.rule_set -> |
|
159 bool * (I_Model.T_TEST * Pre_Conds.T) |
|
160 \<close> ML \<open> |
|
161 (*\\------------------ build fun match_itms_oris -------------------------------------------//*) |
|
162 \<close> ML \<open> (*\\----------- build fun match_itms_oris -------------------------------------------//*) |
|
163 \<close> ML \<open> |
|
164 \<close> |
|
165 |
|
166 (*ML_file "Minisubpbl/100-init-rootpbl-NEXT_STEP.sml" (*get from isa-a-.. -----------------*) |
|
167 section \<open>===================================================================================\<close> |
71 section \<open>===== ============================================================================\<close> |
168 section \<open>===== ============================================================================\<close> |
|
169 ML \<open> |
|
170 \<close> ML \<open> |
|
171 |
|
172 \<close> ML \<open> |
|
173 \<close> |
|
174 ---------------------------------------------------------------------- testing unnecessary *) |
|
175 |
|
176 (*ML_file "Minisubpbl/150a-add-given-Maximum.sml"*) |
|
177 section \<open>===================================================================================\<close> |
|
178 section \<open>===== "Minisubpbl/150a-add-given-Maximum.sml" ====================================\<close> |
72 ML \<open> |
179 ML \<open> |
73 \<close> ML \<open> |
180 \<close> ML \<open> |
|
181 (* Title: "Minisubpbl/150a-add-given-Maximum.sml" |
|
182 Author: Walther Neuper 1105 |
|
183 (c) copyright due to lincense terms. |
|
184 |
|
185 COMPARE Specify/specify.sml --- specify-phase: low level functions --- |
|
186 |
|
187 ATTENTION: the file creates buffer overflow if copied in one piece ! |
|
188 |
|
189 Note: This test --- steps into me --- more than once, to a somewhat extreme extent; |
|
190 in order not to get lost while working in Test_Some etc, |
|
191 re-introduce ML (*--- step into XXXXX ---*) and Co. |
|
192 and use Sidekick for orientation. |
|
193 Nesting is indicated by /--- //-- ///- at the left margin of the comments. |
|
194 *) |
|
195 |
|
196 open Ctree; |
|
197 open Pos; |
|
198 open TermC; |
|
199 open Istate; |
|
200 open Tactic; |
|
201 open I_Model; |
|
202 open P_Model |
|
203 open Rewrite; |
|
204 open Step; |
|
205 open LItool; |
|
206 open LI; |
|
207 open Test_Code |
|
208 open Specify |
|
209 open ME_Misc |
|
210 open Pre_Conds; |
|
211 |
|
212 val (_(*example text*), |
|
213 (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" :: |
|
214 "Extremum (A = 2 * u * v - u \<up> 2)" :: |
|
215 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" :: |
|
216 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" :: |
|
217 "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" :: |
|
218 (*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*) |
|
219 "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" :: |
|
220 "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" :: |
|
221 "ErrorBound (\<epsilon> = (0::real))" :: []), |
|
222 refs as ("Diff_App", |
|
223 ["univariate_calculus", "Optimisation"], |
|
224 ["Optimisation", "by_univariate_calculus"]))) |
|
225 = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"]; |
|
226 |
|
227 val c = []; |
|
228 val return_init_calc = |
|
229 Test_Code.init_calc @{context} [(model, refs)]; (*val Model_Problem = nxt;*) |
|
230 (*/------------------- step into init_calc -------------------------------------------------\\*) |
|
231 "~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))]) = |
|
232 (@{context}, [(model, refs)]); |
|
233 val thy = thy_id |> ThyC.get_theory ctxt |
|
234 val ((pt, p), tacis) = Step_Specify.initialise' thy (model, refs) |
|
235 val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis |
|
236 val f = |
|
237 TESTg_form ctxt (pt,p); |
|
238 "~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p)); |
|
239 val (form, _, _) = |
|
240 ME_Misc.pt_extract ctxt ptp; |
|
241 "~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_ as Pbl(*Frm,Pbl*)))) = (ctxt, ptp); |
|
242 val ppobj = Ctree.get_obj I pt p |
|
243 val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p; |
|
244 (*if*) Ctree.is_pblobj ppobj (*then*); |
|
245 pt_model ppobj p_ ; |
|
246 "~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}), Pbl_) = |
|
247 (ppobj, p_); |
|
248 val (_, pI, _) = Ctree.get_somespec' spec spec'; |
|
249 (* val where_ = if pI = Problem.id_empty then []*) |
|
250 (*if*) pI = Problem.id_empty (*else*); |
|
251 val {where_rls, where_, model, ...} = Problem.from_store ctxt pI |
|
252 val (_, where_) = |
|
253 Pre_Conds.check ctxt where_rls where_ |
|
254 (model, I_Model.OLD_to_TEST probl); |
|
255 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) = |
|
256 (ctxt, where_rls, where_, (model, I_Model.OLD_to_TEST probl)); |
|
257 val (env_model, (env_subst, env_eval)) = |
|
258 make_environments model_patt i_model; |
|
259 "~~~~~ fun make_environments , args:"; val (_, []) = (model_patt, i_model); |
|
260 (*\------------------- step into init_calc -------------------------------------------------//*) |
|
261 val (p,_,f,nxt,_,pt) = return_init_calc; |
|
262 |
|
263 (*+*)val PblObj {ctxt, probl, ...} = get_obj I pt []; |
|
264 (*+*)Proof_Context.theory_of ctxt (*= {Pure, .., Diff_App}*); |
|
265 (*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term ctxt "r" |
|
266 (*+*)val [] = probl |
|
267 |
|
268 val return_me_Model_Problem = |
|
269 me nxt p c pt; val Add_Given "Constants [r = 7]" = #4 return_me_Model_Problem; |
|
270 (*/------------------- step into me Model_Problem ------------------------------------------\\*) |
|
271 "~~~~~ fun me , args:"; val (tac, (p:Pos.pos'), (_:Test_Code.NEW), (pt:Ctree.ctree)) = (nxt, p, c, pt); |
|
272 val ctxt = Ctree.get_ctxt pt p |
|
273 val return_by_tactic = case |
|
274 Step.by_tactic tac (pt,p) of |
|
275 ("ok", (_, _, ptp)) => ptp; |
|
276 |
|
277 (*//------------------ step into by_tactic -------------------------------------------------\\*) |
|
278 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p)); |
|
279 val Applicable.Yes tac' = (*case*) |
|
280 Step.check tac (pt, p) (*of*); |
|
281 (*+*)val Model_Problem' _ = tac'; |
|
282 "~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p)); |
|
283 (*if*) Tactic.for_specify tac (*then*); |
|
284 |
|
285 Specify_Step.check tac (ctree, pos); |
|
286 "~~~~~ fun check , args:"; val (Tactic.Model_Problem, (pt, pos as (p, _))) = |
|
287 (tac, (ctree, pos)); |
|
288 val (o_model, pI', ctxt) = case Ctree.get_obj I pt p of |
|
289 Ctree.PblObj {origin = (o_model, (_, pI', _), _), ctxt, ...} => (o_model, pI', ctxt) |
|
290 val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI' |
|
291 val pbl = I_Model.init_TEST o_model model_patt; |
|
292 |
|
293 val return_check = |
|
294 Applicable.Yes (Tactic.Model_Problem' (pI', I_Model.TEST_to_OLD pbl, [])); |
|
295 (*\\------------------ step into by_tactic -------------------------------------------------//*) |
|
296 val (pt, p) = return_by_tactic; |
|
297 |
|
298 val return_do_next = (*case*) |
|
299 Step.do_next p ((pt, Pos.e_pos'), []) (*of*); |
|
300 (*//------------------ step into do_next ---------------------------------------------------\\*) |
|
301 "~~~~~ fun do_next , args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) = |
|
302 (p, ((pt, e_pos'),[])); |
|
303 val pIopt = get_pblID (pt,ip); |
|
304 (*if*) ip = ([],Res); (* = false*) |
|
305 val _ = (*case*) tacis (*of*); |
|
306 val SOME _ = (*case*) pIopt (*of*); |
|
307 |
|
308 val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) = |
|
309 Step.switch_specify_solve p_ (pt, ip); |
|
310 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip)); |
|
311 (*if*) Pos.on_specification ([], state_pos) (*then*); |
|
312 |
|
313 val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) = |
|
314 Step.specify_do_next (pt, input_pos); |
|
315 (*///----------------- step into specify_do_next -------------------------------------------\\*) |
|
316 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos); |
|
317 |
|
318 (* val (_, (p_', tac)) =*) |
|
319 val return_find_next_step = (*keep for continuing specify_do_next*) |
|
320 Specify.find_next_step ptp; |
|
321 (*////---------------- step into find_next_step --------------------------------------------\\*) |
|
322 "~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp); |
|
323 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl, |
|
324 spec = refs, ...} = Calc.specify_data (pt, pos); |
|
325 val ctxt = Ctree.get_ctxt pt pos; |
|
326 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*); |
|
327 (*if*) p_ = Pos.Pbl (*then*); |
|
328 |
|
329 Specify.for_problem ctxt oris (o_refs, refs) (pbl, met); |
|
330 (*/////--------------- step into for_problem -----------------------------------------------\\*) |
|
331 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) |
|
332 = (ctxt, oris, (o_refs, refs), (pbl, met)); |
|
333 val cdI = if dI = ThyC.id_empty then dI' else dI; |
|
334 val cpI = if pI = Problem.id_empty then pI' else pI; |
|
335 val cmI = if mI = MethodC.id_empty then mI' else mI; |
|
336 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI; |
|
337 val {model = mpc, ...} = MethodC.from_store ctxt cmI; |
|
338 |
|
339 val return_check_OLD = |
|
340 check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl); |
|
341 (*//////-------------- step into check -------------------------------------------------\\*) |
|
342 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) = |
|
343 (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl)); |
|
344 val return_make_environments = |
|
345 make_environments model_patt i_model; |
|
346 (*///// //------------ step into of_max_variant --------------------------------------------\\*) |
|
347 "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = |
|
348 (model_patt, i_model); |
|
349 |
|
350 (*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [] [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \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))]" |
|
351 = i_model |> I_Model.to_string_TEST @{context} |
|
352 val all_variants = |
|
353 map (fn (_, variants, _, _, _) => variants) i_model |
|
354 |> flat |
|
355 |> distinct op = |
|
356 val variants_separated = map (filter_variants' i_model) all_variants |
|
357 val sums_corr = map (Model_Def.cnt_corrects) variants_separated |
|
358 val sum_variant_s = Model_Def.arrange_args sums_corr (1, all_variants) |
|
359 (*+*)val [(0, 1), (0, 2), (0, 3)] = sum_variant_s |
|
360 val (_, max_variant) = hd (*..crude decision, up to improvement *) |
|
361 (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s) |
|
362 val i_model_max = |
|
363 filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model |
|
364 val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat |
|
365 (*for building make_env_s -------------------------------------------------------------------\*) |
|
366 (*!!!*) val ("#Given", (descr, term), pos) = |
|
367 Model_Pattern.split_descriptor ctxt ("#Given", @{term "Constants [r = (7::real)]"}, Position.none) |
|
368 (*!!!*) val patt = equal_descr_pairs |> hd |> #1 |
|
369 (*!!!*)val equal_descr_pairs = |
|
370 (patt, |
|
371 (1, [1, 2, 3], true, "#Given", (Cor_TEST ((descr, (*!*)TermC.isalist2list(*!*) term)), pos))) |
|
372 :: tl equal_descr_pairs |
|
373 (*for building make_env_s -------------------------------------------------------------------/*) |
|
374 |
|
375 val env_model = make_env_model equal_descr_pairs; |
|
376 (*///// ///----------- step into make_env_model --------------------------------------------\\*) |
|
377 "~~~~~ fun make_env_model , args:"; val (equal_descr_pairs) = (equal_descr_pairs); |
|
378 |
|
379 val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) |
|
380 => (mk_env_model id feedb)); |
|
381 val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 4 equal_descr_pairs; |
|
382 (*\\\\\ \\\----------- step into make_env_model --------------------------------------------//*) |
|
383 (*||||| ||------------ contine of_max_variant ------------------------------------------------*) |
|
384 |
|
385 val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs |
|
386 val subst_eval_list = make_envs_preconds equal_givens |
|
387 val return_make_envs_preconds = |
|
388 make_envs_preconds equal_givens; |
|
389 (*///// ///----------- step into make_envs_preconds ----------------------------------------\\*) |
|
390 "~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens); |
|
391 val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb) |
|
392 ; |
|
393 xxx: (Model_Pattern.single * I_Model.single_TEST) -> ((term * term) * (term * term)) list; |
|
394 val return_discern_feedback = |
|
395 discern_feedback id feedb; |
|
396 (*nth 1 equal_descr_pairs* ) |
|
397 "~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) = (id, feedb); |
|
398 ( *nth 2 equal_descr_pairs*) |
|
399 "~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Inc_TEST ((descr, ts)))) = (id, feedb); |
|
400 |
|
401 (*nth 1 equal_descr_pairs* ) |
|
402 (*+*)val [((Const ("fixes", typ1), Free ("r", typ2)), |
|
403 (Free ("r", typ3), value))] = return_discern_feedback |
|
404 (*+*)val true = typ1 = typ2 |
|
405 (*+*)val true = typ3 = HOLogic.realT |
|
406 (*+*)val "7" = UnparseC.term @{context} value |
|
407 ( *nth 2 equal_descr_pairs*) |
|
408 (*+*)val [] = return_discern_feedback |
|
409 |
|
410 val return_discern_typ = |
|
411 discern_typ id (descr, ts); |
|
412 "~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts)); |
|
413 (*nth 1 equal_descr_pairs* ) |
|
414 (*+*)val [((Const ("fixes", typ1), Free ("r", typ2)), |
|
415 (Free ("r", typ3), value))] = return_discern_typ |
|
416 (*+*)val true = typ1 = typ2 |
|
417 (*+*)val true = typ3 = HOLogic.realT |
|
418 (*+*)val "7" = UnparseC.term @{context} value |
|
419 ( *nth 2 equal_descr_pairs*) |
|
420 (*+*)val [] = return_discern_typ; |
|
421 (**) |
|
422 switch_type id ts; |
|
423 "~~~~~ fun switch_type , args:"; val (Const (descr_string, _), ts) = (descr, ts); |
|
424 |
|
425 (*nth 1 equal_descr_pairs* ) |
|
426 val return_switch_type_TEST = Const (descr_string, ts |> hd |> TermC.lhs |> type_of) |
|
427 |
|
428 (*+*)val Const ("Input_Descript.Constants", typ) = return_switch_type_TEST |
|
429 (*+*)val Type ("Real.real", []) = typ |
|
430 ( *nth 2 equal_descr_pairs*) |
|
431 (*+*)val return_switch_type_TEST = descr |
|
432 (**) |
|
433 (*\\\\\ \\\----------- step into make_envs_preconds ----------------------------------------//*) |
|
434 (*||||| ||------------ contine of_max_variant ------------------------------------------------*) |
|
435 val subst_eval_list = make_envs_preconds equal_givens |
|
436 val (env_subst, env_eval) = split_list subst_eval_list |
|
437 val make_environments = (i_model_max, env_model, (env_subst, env_eval)); (*GOON*) |
|
438 (*\\\\\ \\------------ step into of_max_variant --------------------------------------------//*) |
|
439 val (i_model_max, env_model, (env_subst, env_eval)) = make_environments |
|
440 (*!!!/----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---\*) |
|
441 val (i_max_variant, env_model, (env_subst, env_eval)) = (i_model_max, [], ([], [])) |
|
442 (*!!!\----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---/*) |
|
443 (*||||||-------------- contine check -----------------------------------------------------*) |
|
444 val pres_subst = map (TermC.subst_atomic_all env_subst) pres; |
|
445 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst); |
|
446 val full_subst = if env_eval = [] then pres_subst_other |
|
447 else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other) |
|
448 val evals = map (eval ctxt where_rls) full_subst |
|
449 val return_ = (i_model_max, env_subst, env_eval) |
|
450 (*\\\\\\\------------- step into check -------------------------------------------------//*) |
|
451 val (preok, _) = return_check_OLD; |
|
452 |
|
453 (*|||||--------------- contine for_problem ---------------------------------------------------*) |
|
454 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*); |
|
455 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*); |
|
456 val NONE = |
|
457 (*case*) find_first (I_Model.is_error o #5) pbl (*of*); |
|
458 |
|
459 (*case*) |
|
460 Specify.item_to_add (ThyC.get_theory ctxt |
|
461 (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*); |
|
462 "~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms) |
|
463 = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, pbt, pbl); |
|
464 fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false |
|
465 | false_and_not_Sup (_, _, false, _, _) = true |
|
466 | false_and_not_Sup _ = false |
|
467 |
|
468 val v = if itms = [] then 1 else Pre_Conds.max_variant itms |
|
469 val vors = if v = 0 then oris |
|
470 else filter ((fn variant => |
|
471 fn (_, variants, m_field, _, _) => member op= variants variant andalso m_field <> "#undef") |
|
472 v) oris |
|
473 |
|
474 (*+*)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]\"])]" |
|
475 (*+*) = vors |> O_Model.to_string @{context} |
|
476 |
|
477 val vits = if v = 0 then itms (* because of dsc without dat *) |
|
478 else filter ((fn variant => |
|
479 fn (_, variants, _, _, _) => member op= variants variant) |
|
480 v) itms; (* itms..vat *) |
|
481 |
|
482 val icl = filter false_and_not_Sup vits; (* incomplete *) |
|
483 |
|
484 (*if*) icl = [] (*else*); |
|
485 (*+*)val "[\n(1 ,[1, 2, 3] ,false ,#Given ,Inc Constants [] , pen2str), \n(2 ,[1, 2, 3] ,false ,#Find ,Inc Maximum , pen2str), \n(3 ,[1, 2, 3] ,false ,#Find ,Inc AdditionalValues [] , pen2str), \n(4 ,[1, 2, 3] ,false ,#Relate ,Inc Extremum , pen2str), \n(5 ,[1, 2] ,false ,#Relate ,Inc SideConditions [] , pen2str)]" |
|
486 = icl |> I_Model.to_string @{context} |
|
487 (*+*)val "(1 ,[1, 2, 3] ,false ,#Given ,Inc Constants [] , pen2str)" |
|
488 = hd icl |> I_Model.single_to_string @{context} |
|
489 |
|
490 (*++*)val feedback = (fn (_, _, _, _, feedback) => feedback) (hd icl) |
|
491 (*++*)val Const ("Input_Descript.Constants", _) = I_Model.descriptor feedback |
|
492 (*++*)val [] = I_Model.o_model_values feedback |
|
493 |
|
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]\"])]" |
|
495 (*+*) = vors |> O_Model.to_string @{context} |
|
496 |
|
497 val SOME ori = |
|
498 (*case*) find_first ((fn (_, _, _, _, feedback) => fn (_, _, _, d, ts) => |
|
499 d = I_Model.descriptor feedback andalso subset op = (I_Model.o_model_values feedback, ts)) |
|
500 (hd icl)) vors (*of*); |
|
501 |
|
502 (*+*)val "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"])" = |
|
503 (*+*) ori |> O_Model.single_to_string @{context} |
|
504 (*\\\\\--------------- step into for_problem -----------------------------------------------//*) |
|
505 (*\\\\---------------- step into find_next_step --------------------------------------------//*) |
|
506 (*|||----------------- continuing specify_do_next --------------------------------------------*) |
|
507 val (_, (p_', tac)) = return_find_next_step (*kept for continuing specify_do_next*) |
|
508 |
|
509 val ist_ctxt = Ctree.get_loc pt (p, p_) |
|
510 (*+*)val Add_Given "Constants [r = 7]" = tac |
|
511 val _ = |
|
512 (*case*) tac (*of*); |
|
513 |
|
514 Step_Specify.by_tactic_input tac (pt, (p, p_')); |
|
515 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) = |
|
516 (tac, (pt, (p, p_'))); |
|
517 |
|
518 Specify.by_Add_ "#Given" ct ptp; |
|
519 "~~~~~ fun by_Add_ , args:"; val (m_field, ct ,(pt, pos as (_, p_))) = |
|
520 ("#Given", ct, ptp); |
|
521 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos) |
|
522 val (i_model, m_patt) = |
|
523 if p_ = Pos.Met then |
|
524 (met, |
|
525 (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model) |
|
526 else |
|
527 (pbl, |
|
528 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model); |
|
529 |
|
530 (*case*) |
|
531 I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*); |
|
532 "~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, (str(*, pos*))) = |
|
533 (ctxt, m_field, oris, i_model, m_patt, ct); |
|
534 val (t as (descriptor $ _)) = Syntax.read_term ctxt str |
|
535 |
|
536 (*+*)val "Constants [r = 7]" = UnparseC.term @{context} t; |
|
537 |
|
538 val SOME m_field' = |
|
539 (*case*) Model_Pattern.get_field descriptor m_patt (*of*); |
|
540 (*if*) m_field <> m_field' (*else*); |
|
541 |
|
542 (*+*)val "#Given" = m_field; val "#Given" = m_field' |
|
543 |
|
544 val ("", ori', all) = |
|
545 (*case*) O_Model.contains ctxt m_field o_model t (*of*); |
|
546 |
|
547 (*+*)val (_, _, _, _, vals) = hd o_model; |
|
548 (*+*)val "Constants [r = 7]" = UnparseC.term @{context} (@{term Constants} $ (hd vals)); |
|
549 (*+*)if "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), " ^ |
|
550 (*+*) "\n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), " ^ |
|
551 (*+*) "\n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), " ^ |
|
552 (*+*) "\n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), " ^ |
|
553 (*+*) "\n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), " ^ |
|
554 (*+*) "\n(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), " ^ |
|
555 (*+*) "\n(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), " ^ |
|
556 (*+*) "\n(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), " ^ |
|
557 (*+*) "\n(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), " ^ |
|
558 (*+*) "\n(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), " ^ |
|
559 (*+*) "\n(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]" |
|
560 (*+*)= O_Model.to_string @{context} o_model then () else error "o_model CHANGED"; |
|
561 |
|
562 (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*); |
|
563 "~~~~~ fun is_notyet_input , args:"; val (ctxt, itms, all, (i, v, f, d, ts), pbt) = |
|
564 (ctxt, i_model, all, ori', m_patt); |
|
565 val SOME (_, (_, pid)) = |
|
566 (*case*) find_first (eq1 d) pbt (*of*); |
|
567 (*local*)fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (I_Model.descriptor itm_);(*local*) |
|
568 val SOME (_, _, _, _, itm_) = |
|
569 (*case*) find_first (eq3 f d) itms (*of*); |
|
570 val ts' = inter op = (o_model_values itm_) ts; |
|
571 (*if*) subset op = (ts, ts') (*else*); |
|
572 val return_is_notyet_input = ("", |
|
573 ori_2itm itm_ pid all (i, v, f, d, subtract op = ts' ts)); |
|
574 "~~~~~ fun ori_2itm , args:"; val (itm_, pid, all, (id, vt, fd, d, ts)) = |
|
575 (itm_, pid, all, (i, v, f, d, subtract op = ts' ts)); |
|
576 val ts' = union op = (o_model_values itm_) ts; |
|
577 val pval = [Input_Descript.join'''' (d, ts')] |
|
578 val complete = if eq_set op = (ts', all) then true else false |
|
579 |
|
580 (*+*)val "Inc Constants [] , pen2str" = itm_ |> I_Model.feedback_to_string @{context} |
|
581 (*\\\----------------- step into specify_do_next -------------------------------------------//*) |
|
582 (*\\------------------ step into do_next ---------------------------------------------------//*) |
|
583 val ("ok", (ts as (_, _, _) :: _, _, (pt, p))) = return_do_next |
|
584 |
|
585 (*|------------------- continue with me_Model_Problem ----------------------------------------*) |
|
586 |
|
587 val tacis as (_::_) = |
|
588 (*case*) ts (*of*); |
|
589 val (tac, _, _) = last_elem tacis |
|
590 |
|
591 val return_Model_Problem = (p, [] : NEW, TESTg_form ctxt (pt, p), tac, Celem.Sundef, pt); |
|
592 (*//------------------ step into TESTg_form ------------------------------------------------\\*) |
|
593 "~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt, p)); |
|
594 |
|
595 val (form, _, _) = |
|
596 ME_Misc.pt_extract ctxt ptp; |
|
597 "~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_(*Frm,Pbl*)))) = (ctxt, ptp); |
|
598 val ppobj = Ctree.get_obj I pt p |
|
599 val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p; |
|
600 (*if*) Ctree.is_pblobj ppobj (*then*); |
|
601 |
|
602 pt_model ppobj p_; |
|
603 "~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, o_spec, hdl), ctxt, ...}), |
|
604 Pbl(*Frm,Pbl*)) = (ppobj, p_); |
|
605 val (_, _, met_id) = References.select_input o_spec spec |
|
606 val (allcorr, _) = Pre_Conds.check_internal ctxt (I_Model.OLD_to_TEST probl) (Pos.Met, met_id) |
|
607 val return_pt_model = Ctree.ModSpec (allcorr, Pos.Pbl, hdl, probl, (*where_*)[(*Problem.from_store in check*)], spec) |
|
608 |
|
609 (*|------------------- continue with TESTg_form ----------------------------------------------*) |
|
610 val Ctree.ModSpec (spec as (_, p_, _, gfr, where_, _)) = |
|
611 (*case*) form (*of*); |
|
612 Test_Out.PpcKF ( (Test_Out.Problem [], |
|
613 P_Model.from (Proof_Context.theory_of ctxt) gfr where_)); |
|
614 |
|
615 \<close> ML \<open> |
|
616 P_Model.from (Proof_Context.theory_of ctxt) gfr where_; |
|
617 "~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_); |
|
618 fun coll model [] = model |
|
619 | coll model ((_, _, _, field, itm_) :: itms) = |
|
620 coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms; |
|
621 |
|
622 val gfr = coll P_Model.empty itms; |
|
623 "~~~~~ fun coll , args:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: itms)) |
|
624 = (P_Model.empty, itms); |
|
625 |
|
626 (*+*)val 4 = length itms; |
|
627 (*+*)val itm = nth 1 itms; |
|
628 |
|
629 coll P_Model.empty [itm]; |
|
630 "~~~~~ fun coll , iterate:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: [])) |
|
631 = (P_Model.empty, [itm]); |
|
632 |
|
633 (add_sel_ppc thy field model (item_from_feedback thy itm_)); |
|
634 "~~~~~ fun add_sel_ppc , args:"; val ((_: theory), sel, {Given = gi, Where = wh, Find = fi, With = wi, Relate = re}, x ) |
|
635 = (thy, field, model, (item_from_feedback thy itm_)); |
|
636 |
|
637 P_Model.item_from_feedback thy itm_; |
|
638 "~~~~~ fun item_from_feedback , args:"; val (thy, (I_Model.Inc ((d, ts), _))) = (thy, itm_); |
|
639 P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts))); |
|
640 (*\\------------------ step into TESTg_form ------------------------------------------------//*) |
|
641 (*\------------------- step into me Model_Problem ------------------------------------------//*) |
|
642 val (p, _, f, nxt, _, pt) = return_me_Model_Problem |
|
643 |
|
644 (*-------------------- contine me's ----------------------------------------------------------*) |
|
645 val return_me_add_find_Constants = me nxt p c pt; |
|
646 val Add_Find "Maximum A" = #4 return_me_add_find_Constants; |
|
647 (*/------------------- step into me_add_find_Constants -------------------------------------\\*) |
|
648 "~~~~~ fun me , args:"; val (tac as Add_Given "Constants [r = 7]", p, _(*NEW remove*), pt) = |
|
649 (nxt, p, c, pt); |
|
650 val ctxt = Ctree.get_ctxt pt p |
|
651 (*+*)val PblObj {probl = (1, [1, 2, 3], false, "#Given", Inc |
|
652 ((Const ("Input_Descript.Constants", _), []), _)) :: _, ...} = get_obj I pt (fst p) |
|
653 (*-------------------------------------------^^--*) |
|
654 val return_step_by_tactic = (*case*) |
|
655 Step.by_tactic tac (pt, p) (*of*); |
|
656 (*//------------------ step into Step.by_tactic --------------------------------------------\\*) |
|
657 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p)); |
|
658 val Applicable.Yes tac' = |
|
659 (*case*) Specify_Step.check tac (pt, p) (*of*); |
|
660 (*if*) Tactic.for_specify' tac' (*then*); |
|
661 Step_Specify.by_tactic tac' ptp; |
|
662 "~~~~~ fun by_tactic , args:"; val ((Tactic.Add_Given' (ct, _)), (pt, p)) = (tac', ptp); |
|
663 |
|
664 Specify.by_Add_ "#Given" ct (pt, p); |
|
665 "~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, (pt, p)); |
|
666 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos); |
|
667 (* val (i_model, m_patt) =*) |
|
668 (*if*) p_ = Pos.Met (*else*); |
|
669 val return_by_Add_ = |
|
670 (pbl, |
|
671 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model) |
|
672 val I_Model.Add i_single = |
|
673 (*case*) I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*); |
|
674 |
|
675 val i_model' = |
|
676 I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model; |
|
677 "~~~~~ fun add_single , args:"; val (thy, itm, model) = |
|
678 ((Proof_Context.theory_of ctxt), i_single, i_model); |
|
679 fun eq_untouched d (0, _, _, _, itm_) = (d = I_Model.descriptor itm_) |
|
680 | eq_untouched _ _ = false |
|
681 val model' = case I_Model.seek_ppc (#1 itm) model of |
|
682 SOME _ => overwrite_ppc thy itm model (*itm updated in is_notyet_input WN.11.03*) |
|
683 |
|
684 (*||------------------ contine Step.by_tactic ------------------------------------------------*) |
|
685 (*\\------------------ step into Step.by_tactic --------------------------------------------//*) |
|
686 val ("ok", (_, _, ptp)) = return_step_by_tactic; |
|
687 |
|
688 val (pt, p) = ptp; |
|
689 (*case*) |
|
690 Step.do_next p ((pt, Pos.e_pos'), []) (*of*); |
|
691 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = |
|
692 (p, ((pt, Pos.e_pos'), [])); |
|
693 (*if*) Pos.on_calc_end ip (*else*); |
|
694 val (_, probl_id, _) = Calc.references (pt, p); |
|
695 val _ = |
|
696 (*case*) tacis (*of*); |
|
697 (*if*) probl_id = Problem.id_empty (*else*); |
|
698 |
|
699 switch_specify_solve p_ (pt, ip); |
|
700 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip)); |
|
701 (*if*) Pos.on_specification ([], state_pos) (*then*); |
|
702 |
|
703 specify_do_next (pt, input_pos); |
|
704 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos); |
|
705 val (_, (p_', tac)) = |
|
706 Specify.find_next_step ptp; |
|
707 "~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp); |
|
708 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl, |
|
709 spec = refs, ...} = Calc.specify_data (pt, pos); |
|
710 val ctxt = Ctree.get_ctxt pt pos; |
|
711 |
|
712 (*+*)val (1, [1, 2, 3], true, "#Given", Cor ((Const ("Input_Descript.Constants", _), ts ), _)) :: _ |
|
713 = pbl |
|
714 (*+*)val "[[r = 7]]" = UnparseC.terms @{context} ts; |
|
715 (*-----ML-^------^-HOL*) |
|
716 |
|
717 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*); |
|
718 (*if*) p_ = Pos.Pbl (*then*); |
|
719 |
|
720 for_problem ctxt oris (o_refs, refs) (pbl, met); |
|
721 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) = |
|
722 (ctxt, oris, (o_refs, refs), (pbl, met)); |
|
723 val cpI = if pI = Problem.id_empty then pI' else pI; |
|
724 val cmI = if mI = MethodC.id_empty then mI' else mI; |
|
725 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI; |
|
726 val {model = mpc, ...} = MethodC.from_store ctxt cmI |
|
727 |
|
728 val (preok, _) = |
|
729 Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl); |
|
730 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) = |
|
731 (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl)); |
|
732 |
|
733 val (_, (env_subst, env_eval)) = Pre_Conds.make_environments model_patt i_model; |
|
734 "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model); |
|
735 val all_variants = |
|
736 map (fn (_, variants, _, _, _) => variants) i_model |
|
737 |> flat |
|
738 |> distinct op = |
|
739 val variants_separated = map (filter_variants' i_model) all_variants |
|
740 val sums_corr = map (Model_Def.cnt_corrects) variants_separated |
|
741 val sum_variant_s = Model_Def.arrange_args sums_corr (1, all_variants) |
|
742 val (_, max_variant) = hd (*..crude decision, up to improvement *) |
|
743 (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s) |
|
744 val i_model_max = |
|
745 filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model |
|
746 val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat |
|
747 val env_model = make_env_model equal_descr_pairs |
|
748 val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs |
|
749 |
|
750 val subst_eval_list = |
|
751 make_envs_preconds equal_givens; |
|
752 "~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens); |
|
753 val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => |
|
754 discern_feedback id feedb) |
|
755 val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 1 equal_givens; |
|
756 "~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts)))) = (id, feedb); |
|
757 |
|
758 discern_typ id (descr, ts); |
|
759 "~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts)); |
|
760 (*|------------------- contine me_add_find_Constants -----------------------------------------*) |
|
761 (*\------------------- step into me_add_find_Constants -------------------------------------//*) |
|
762 val (p,_,f,nxt,_,pt) = return_me_add_find_Constants; |
|
763 (*/########################## before destroying elementwise input of lists ##################\* ) |
|
764 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u]" = nxt; |
|
765 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [v]" = nxt; |
|
766 ( *\########################## before destroying elementwise input of lists ##################/*) |
|
767 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u, v]" = nxt; |
|
768 |
|
769 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)" = nxt; |
|
770 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; |
|
771 val return_me_Add_Relation_SideConditions |
|
772 = me nxt p c pt; |
|
773 (*+*)val (_, _, _, Specify_Theory "Diff_App", _, _) = return_me_Add_Relation_SideConditions; (*###############*) |
|
774 (*/------------------- step into me Add_Relation_SideConditions ----------------------------\\*) |
|
775 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt); |
|
776 val ctxt = Ctree.get_ctxt pt p; |
|
777 (**) val (pt, p) = (**) |
|
778 (**)case(**) Step.by_tactic tac (pt, p) (**)of(**) |
|
779 (**) ("ok", (_, _, ptp)) => ptp (**) ; |
|
780 |
|
781 (*case*) |
|
782 Step.do_next p ((pt, Pos.e_pos'), []) (*of*); |
|
783 (*//------------------ step into do_next ---------------------------------------------------\\*) |
|
784 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) |
|
785 = (p, ((pt, Pos.e_pos'), [])) (*of*); |
|
786 (*if*) Pos.on_calc_end ip (*else*); |
|
787 val (_, probl_id, _) = Calc.references (pt, p); |
|
788 (*case*) tacis (*of*); |
|
789 (*if*) probl_id = Problem.id_empty (*else*); |
|
790 |
|
791 Step.switch_specify_solve p_ (pt, ip); |
|
792 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip)); |
|
793 (*if*) Pos.on_specification ([], state_pos) (*then*); |
|
794 Step.specify_do_next (pt, input_pos); |
|
795 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos); |
|
796 (*isa------ERROR: Refine_Problem INSTEAD |
|
797 isa2: Specify_Theory "Diff_App"*) |
|
798 val (_, (p_', tac as Specify_Theory "Diff_App")) = |
|
799 (*ERROR------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) |
|
800 Specify.find_next_step ptp; |
|
801 "~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp); |
|
802 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl, |
|
803 spec = refs, ...} = Calc.specify_data (pt, pos); |
|
804 val ctxt = Ctree.get_ctxt pt pos; |
|
805 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*); |
|
806 (*if*) p_ = Pos.Pbl (*then*); |
|
807 |
|
808 val ("dummy", (Pbl, tac as Specify_Theory "Diff_App")) = |
|
809 (*ERROR------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) |
|
810 for_problem ctxt oris (o_refs, refs) (pbl, met); |
|
811 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) = |
|
812 (ctxt, oris, (o_refs, refs), (pbl, met)); |
|
813 val cpI = if pI = Problem.id_empty then pI' else pI; |
|
814 val cmI = if mI = MethodC.id_empty then mI' else mI; |
|
815 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI; |
|
816 val {model = mpc, ...} = MethodC.from_store ctxt cmI |
|
817 |
|
818 (*+*)val [Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $ |
|
819 Free ("fixes", _)] = where_ |
|
820 |
|
821 val (preok, _) = |
|
822 Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl); |
|
823 (*///----------------- step into check -------------------------------------------------\\*) |
|
824 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) = |
|
825 (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl)); |
|
826 (*+*)val "[0 < fixes]" = pres |> UnparseC.terms @{context} |
|
827 (*+*)val "[\"(#Given, (Constants, fixes))\", \"(#Find, (Maximum, maxx))\", \"(#Find, (AdditionalValues, vals))\", \"(#Relate, (Extremum, extr))\", \"(#Relate, (SideConditions, sideconds))\"]" |
|
828 (*+*) = model_patt |> Model_Pattern.to_string @{context} |
|
829 (*+*)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))]" |
|
830 = i_model |> I_Model.to_string_TEST @{context} |
|
831 |
|
832 val return_make_environments as (_, (env_subst, env_eval)) = |
|
833 Pre_Conds.make_environments model_patt i_model |
|
834 |
|
835 (*+*)val [(Free ("fixes", T1), Free ("r", T2))] = env_subst (*?!? Const*) |
|
836 (*+*)val Type ("Real.real", []) = T1 |
|
837 (*+*)val Type ("Real.real", []) = T2 |
|
838 |
|
839 (*+*)val [(Free ("r", T2), Const ("Num.numeral_class.numeral", _) $ _)] = env_eval |
|
840 (*+*)val Type ("Real.real", []) = T2 |
|
841 |
|
842 val (_, (env_subst, env_eval)) = return_make_environments; |
|
843 (*|||----------------- contine check -----------------------------------------------------*) |
|
844 val pres_subst = map (TermC.subst_atomic_all env_subst) pres; |
|
845 |
|
846 (*|||----------------- contine check -----------------------------------------------------*) |
|
847 (*+*)val [(true, Const ("Orderings.ord_class.less", _) $ |
|
848 Const ("Groups.zero_class.zero", _) $ Free ("r", _))] = pres_subst |
|
849 |
|
850 val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst |
|
851 (*+*)val [(true, |
|
852 Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $ |
|
853 (Const ("Num.numeral_class.numeral", _) $ _))] = full_subst |
|
854 |
|
855 val evals = map (eval ctxt where_rls) full_subst |
|
856 val return_check_OLD = (foldl and_ (true, map fst evals), pres_subst) |
|
857 (*\\\----------------- step into check -------------------------------------------------\\*) |
|
858 |
|
859 val (preok as true, _) = return_check_OLD |
|
860 (*+---------------^^^^*) |
|
861 (*\\------------------ step into do_next ---------------------------------------------------\\*) |
|
862 (*\------------------- step into me_Add_Relation_SideConditions ----------------------------//*) |
|
863 val (p, _, f, nxt, _, pt) = return_me_Add_Relation_SideConditions |
|
864 val Specify_Theory "Diff_App" = nxt; |
|
865 |
|
866 val return_me_Specify_Theory |
|
867 = me nxt p c pt; val Specify_Problem ["univariate_calculus", "Optimisation"] = #4 return_me_Specify_Theory; |
|
868 (*/------------------- step into me Specify_Theory -----------------------------------------\\*) |
|
869 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt); |
|
870 val ctxt = Ctree.get_ctxt pt p; |
|
871 (* val (pt, p) = *) |
|
872 (*case*) Step.by_tactic tac (pt, p) (*of*); |
|
873 (* ("ok", (_, _, ptp)) => ptp *) |
|
874 val return_Step_by_tactic = |
|
875 Step.by_tactic tac (pt, p); |
|
876 (*//------------------ step into Step_by_tactic --------------------------------------------\\*) |
|
877 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p)); |
|
878 (*case*) Specify_Step.check tac (pt, p) (*of*); |
|
879 |
|
880 (*||------------------ contine Step_by_tactic ------------------------------------------------*) |
|
881 (*\\------------------ step into Step_by_tactic --------------------------------------------//*) |
|
882 |
|
883 val ("ok", (_, _, ptp)) = return_Step_by_tactic; |
|
884 (*|------------------- continue me Specify_Theory --------------------------------------------*) |
|
885 |
|
886 val ("ok", (ts as (_, _, _) :: _, _, _)) = |
|
887 (*case*) |
|
888 Step.do_next p ((pt, Pos.e_pos'), []) (*of*); |
|
889 (*//------------------ step into do_next ---------------------------------------------------\\*) |
|
890 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) |
|
891 = (p, ((pt, Pos.e_pos'), [])) (*of*); |
|
892 (*if*) Pos.on_calc_end ip (*else*); |
|
893 val (_, probl_id, _) = Calc.references (pt, p); |
|
894 val _ = |
|
895 (*case*) tacis (*of*); |
|
896 (*if*) probl_id = Problem.id_empty (*else*); |
|
897 |
|
898 Step.switch_specify_solve p_ (pt, ip); |
|
899 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip)); |
|
900 (*if*) Pos.on_specification ([], state_pos) (*then*); |
|
901 |
|
902 Step.specify_do_next (pt, input_pos); |
|
903 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos); |
|
904 val (_, (p_', tac)) = Specify.find_next_step ptp |
|
905 val ist_ctxt = Ctree.get_loc pt (p, p_); |
|
906 (*case*) tac (*of*); |
|
907 |
|
908 Step_Specify.by_tactic_input tac (pt, (p, p_')); |
|
909 (*+*)val Specify_Theory "Diff_App" = tac; |
|
910 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Theory dI), (pt, pos as (_, Pbl))) |
|
911 = (tac, (pt, (p, p_'))); |
|
912 val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of |
|
913 PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} => |
|
914 (oris, dI, dI', pI', probl, ctxt) |
|
915 val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI'); |
|
916 val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI |
|
917 (*\\------------------ step into do_next ---------------------------------------------------//*) |
|
918 (*\------------------- step into me Specify_Theory -----------------------------------------//*) |
|
919 val (p,_,f,nxt,_,pt) = return_me_Specify_Theory; |
|
920 |
|
921 val return_me_Specify_Problem (* keep for continuing me *) |
|
922 = me nxt p c pt; val Specify_Method ["Optimisation", "by_univariate_calculus"] = #4 return_me_Specify_Problem; |
|
923 \<close> ML \<open>(*/------------- step into me_Specify_Problem ----------------------------------------\\*) |
|
924 (*/------------------- step into me_Specify_Problem ----------------------------------------\\*) |
|
925 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt); |
|
926 val ctxt = Ctree.get_ctxt pt p |
|
927 |
|
928 (** ) val ("ok", (_, _, ptp as (pt, p))) =( **) |
|
929 (**) val return_by_tactic =(**) (*case*) |
|
930 Step.by_tactic tac (pt, p) (*of*); |
|
931 (*//------------------ step into by_tactic -------------------------------------------------\\*) |
|
932 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p)); |
|
933 |
|
934 (*case*) |
|
935 Step.check tac (pt, p) (*of*); |
|
936 "~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p)); |
|
937 (*if*) Tactic.for_specify tac (*then*); |
|
938 |
|
939 Specify_Step.check tac (ctree, pos); |
|
940 "~~~~~ fun check , args:"; val ((Tactic.Specify_Problem pID), (pt, pos as (p, _))) |
|
941 = (tac, (ctree, pos)); |
|
942 val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of |
|
943 Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...} |
|
944 => (oris, dI, pI, dI', pI', itms) |
|
945 val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI'); |
|
946 (*\\------------------ step into by_tactic -------------------------------------------------//*) |
|
947 val ("ok", (_, _, ptp as (pt, p))) = return_by_tactic (* kept for continuing me *); |
|
948 |
|
949 (*case*) |
|
950 Step.do_next p ((pt, Pos.e_pos'), []) (*of*); |
|
951 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), [])); |
|
952 (*if*) Pos.on_calc_end ip (*else*); |
|
953 val (_, probl_id, _) = Calc.references (pt, p); |
|
954 val _ = |
|
955 (*case*) tacis (*of*); |
|
956 (*if*) probl_id = Problem.id_empty (*else*); |
|
957 |
|
958 Step.switch_specify_solve p_ (pt, ip); |
|
959 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip)); |
|
960 (*if*) Pos.on_specification ([], state_pos) (*then*); |
|
961 |
|
962 Step.specify_do_next (pt, input_pos); |
|
963 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos)); |
|
964 val (_, (p_', tac)) = Specify.find_next_step ptp |
|
965 val ist_ctxt = Ctree.get_loc pt (p, p_) |
|
966 val _ = |
|
967 (*case*) tac (*of*); |
|
968 |
|
969 Step_Specify.by_tactic_input tac (pt, (p, p_')); |
|
970 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos)) |
|
971 = (tac, (pt, (p, p_'))); |
|
972 |
|
973 \<close> ML \<open> |
|
974 (**)val return_complete_for =(**) |
|
975 (** ) val (o_model, ctxt, i_model) =( **) |
|
976 Specify_Step.complete_for id (pt, pos); |
|
977 \<close> ML \<open> (*//----------- step into complete_for ----------------------------------------------\\*) |
|
978 (*//------------------ step into complete_for ----------------------------------------------\\*) |
|
979 "~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos)); |
|
980 |
|
981 (*+*)val ["Optimisation", "by_univariate_calculus"] = mID |
|
982 (*OLD* ) |
|
983 val {origin = (o_model, _, _), probl = i_prob, ctxt, |
|
984 ...} = Calc.specify_data (ctree, pos); |
|
985 val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID |
|
986 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und)) |
|
987 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt) |
|
988 ( *---*) |
|
989 val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = met_imod, ctxt, |
|
990 ...} = Calc.specify_data (ctree, pos); |
|
991 val ctxt = Ctree.get_ctxt ctree pos |
|
992 val (dI, _, _) = References.select_input o_refs refs; |
|
993 val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID |
|
994 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und)) |
|
995 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt) |
|
996 (*NEW*) |
|
997 \<close> ML \<open> |
|
998 (**)val return_match_itms_oris = (**) |
|
999 (** )val (_, (i_model, _)) = ( **) |
|
1000 (*OLD* ) |
|
1001 M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model'; |
|
1002 ( *---*) |
|
1003 match_itms_oris ctxt o_model' (I_Model.OLD_to_TEST i_prob, I_Model.OLD_to_TEST i_prob) |
|
1004 (m_patt, where_, where_rls); |
|
1005 (*NEW*) |
|
1006 \<close> ML \<open> (*///---------- step into match_itms_oris -------------------------------------------\\*) |
|
1007 (*///----------------- step into match_itms_oris -------------------------------------------\\*) |
|
1008 \<close> ML \<open> (*\<longrightarrow> m-match.sml*) |
|
1009 "~~~~~ fun match_itms_oris, args:"; val (ctxt, o_model, (pbl_imod, met_imod), (m_patt, where_, where_rls)) = |
|
1010 (ctxt, o_model', (I_Model.OLD_to_TEST i_prob, I_Model.OLD_to_TEST i_prob), (m_patt, where_, where_rls)); |
|
1011 \<close> ML \<open> |
|
1012 (**)val return_fill_method =(**) |
|
1013 (** )val met_imod =( **) |
|
1014 fill_method o_model (pbl_imod, met_imod) m_patt; |
|
1015 \<close> ML \<open> (*////-------- step into fill_method -----------------------------------------------\\*) |
|
1016 (*////--------------- step into fill_method -----------------------------------------------\\*) |
|
1017 "~~~~~ fun fill_method , args:"; val (o_model, (pbl_imod, met_imod), met_patt) = |
|
1018 (o_model, (pbl_imod, met_imod), m_patt); |
|
1019 |
|
1020 val pbl_max_vnts as [2, 1] = Model_Def.max_variants o_model pbl_imod |
|
1021 (*probably pbl/met_imod = [], so take met_patt; if empty return Sup*) |
|
1022 val i_from_met = map (fn (_, (descr, _)) => (*order from met_patt*) |
|
1023 Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt (*\<longrightarrow> right order for args*) |
|
1024 (*+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))]" |
|
1025 = i_from_met |> I_Model.to_string_TEST @{context} |
|
1026 |
|
1027 val met_max_vnts as [2, 1] = Model_Def.max_variants o_model i_from_met; |
|
1028 val max_vnt as 2 = hd (inter op= pbl_max_vnts met_max_vnts); |
|
1029 (*add items from pbl_imod (without overwriting existing items in met_imod)*) |
|
1030 |
|
1031 val return_add_other = map ( |
|
1032 add_other max_vnt pbl_imod) i_from_met; |
|
1033 \<close> ML \<open> (*/////------- step into add_other -------------------------------------------------\\*) |
|
1034 (*/////-------------- step into add_other -------------------------------------------------\\*) |
|
1035 "~~~~~ fun add_other_5 , args:"; val (max_vnt, i1_model, (i2, _, bool2, m_field2, (Sup_TEST (descr2, ts2), pos2))) = |
|
1036 (max_vnt, pbl_imod, nth 5 i_from_met); |
|
1037 \<close> ML \<open> |
|
1038 (*+*)val Const ("Input_Descript.FunctionVariable", _) = descr2; |
|
1039 \<close> ML \<open> |
|
1040 val (_, vnts1, _, _, (feedb1, _)) = (i2, [], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2)) |
|
1041 \<close> ML \<open> |
|
1042 val SOME (descr1 as (Const ("Input_Descript.FunctionVariable", _)) ) = |
|
1043 get_dscr' feedb1 |
|
1044 val true = |
|
1045 descr1 = descr2 |
|
1046 val true = |
|
1047 Model_Def.member_vnt vnts1 max_vnt |
|
1048 val NONE = |
|
1049 find_first (fn (_, vnts1, _, _, (feedb1, _)) => case get_dscr' feedb1 of |
|
1050 NONE => false |
|
1051 | SOME descr1 => descr1 = descr2 andalso Model_Def.member_vnt vnts1 max_vnt) i1_model |
|
1052 \<close> ML \<open> |
|
1053 val return_add_other_1 = (i2, [max_vnt], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2)) |
|
1054 val check as true = return_add_other_1 = nth 5 return_add_other |
|
1055 \<close> ML \<open> (*\\\\\------- step into add_other -------------------------------------------------//*) |
|
1056 (*\\\\\-------------- step into add_other -------------------------------------------------//*) |
|
1057 val i_from_pbl = return_add_other |
|
1058 \<close> ML \<open> |
|
1059 \<close> ML \<open> (*\\\\--------- step into fill_method -----------------------------------------------//*) |
|
1060 (*\\\\---------------- step into fill_method -----------------------------------------------//*) |
|
1061 val return_fill_method_step = filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) i_from_met |
|
1062 \<close> ML \<open> |
|
1063 (*+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))]" = |
|
1064 return_fill_method_step |> I_Model.to_string_TEST @{context} |
|
1065 \<close> ML \<open> |
|
1066 (*+*)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))]" |
|
1067 = return_fill_method |> I_Model.to_string_TEST @{context}; |
|
1068 \<close> ML \<open> |
|
1069 return_fill_method_step = return_fill_method (*latter is correct, did not investigate further*) |
|
1070 (*\\\----------------- step into match_itms_oris -------------------------------------------//*) |
|
1071 \<close> ML \<open> (*\\\---------- step into match_itms_oris -------------------------------------------//*) |
|
1072 val (_, (i_model, _)) = return_match_itms_oris; |
|
1073 \<close> ML \<open> |
|
1074 \<close> ML \<open>(*||------------ continue. complete_for ------------------------------------------------*) |
|
1075 (*||------------------ continue. complete_for ------------------------------------------------*) |
|
1076 val (o_model, ctxt, i_model) = return_complete_for |
|
1077 \<close> ML \<open> |
|
1078 (*+*)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))]" |
|
1079 = i_model |> I_Model.to_string_TEST @{context} |
|
1080 \<close> ML \<open> |
|
1081 (* |
|
1082 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)]" |
|
1083 = i_model |> I_Model.to_string @{context} |
|
1084 *) |
|
1085 (*+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)]" = |
|
1086 i_model |> I_Model.to_string @{context} ( *+isa2*) |
|
1087 \<close> ML \<open> (*\\----------- step into complete_for ----------------------------------------------//*) |
|
1088 (*\\------------------ step into complete_for ----------------------------------------------//*) |
|
1089 val (o_model, ctxt, i_model) = return_complete_for |
|
1090 \<close> ML \<open> |
|
1091 \<close> ML \<open> (*|------------ continue. complete_for ------------------------------------------------*) |
|
1092 (*|------------------- continue. complete_for ------------------------------------------------*) |
|
1093 val return_complete_for_step = (o_model', ctxt', i_model) |
|
1094 \<close> ML \<open> |
|
1095 val (o_model'_step, i_model_step) = (#1 return_complete_for_step, #3 return_complete_for_step) |
|
1096 val (o_model', i_model) = (#1 return_complete_for, #3 return_complete_for) |
|
1097 \<close> ML \<open> |
|
1098 if (o_model'_step, i_model_step) = (o_model', i_model) |
|
1099 then () else error "return_complete_for_step <> return_complete_for"; |
|
1100 \<close> ML \<open>(*\------------- step into me Specify_Problem ----------------------------------------//*) |
|
1101 (*\------------------- step into me Specify_Problem ----------------------------------------//*) |
|
1102 val (p,_,f,nxt,_,pt) = return_me_Specify_Problem |
|
1103 |
|
1104 \<close> ML \<open> |
|
1105 val return_me_Specify_Method |
|
1106 = me nxt p c pt; val Add_Given "FunctionVariable b" = #4 return_me_Specify_Method; |
|
1107 (*/------------------- step into me_Specify_Method -----------------------------------------\\*) |
|
1108 \<close> ML \<open>(*/------------- step into me_Specify_Method -----------------------------------------\\*) |
|
1109 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt); |
|
1110 |
|
1111 (*+isa==isa2*)val "[]" =(*+*) get_obj g_met pt (fst p) |> I_Model.to_string @{context} |
|
1112 |
|
1113 val ctxt = Ctree.get_ctxt pt p |
|
1114 val (pt, p) = |
|
1115 case Step.by_tactic tac (pt, p) of |
|
1116 ("ok", (_, _, ptp)) => ptp; |
|
1117 |
|
1118 \<close> ML \<open> |
|
1119 (*quick step into --> me_Specify_Method*) |
|
1120 (*+*)val Specify_Method ["Optimisation", "by_univariate_calculus"] = tac; |
|
1121 (* Step.by_tactic*) |
|
1122 "~~~~~ fun by_tactic , args:"; val () = (); |
|
1123 (* Step.check*) |
|
1124 "~~~~~ fun check , args:"; val () = (); |
|
1125 (*Specify_Step.check (Tactic.Specify_Method*) |
|
1126 "~~~~~ fun check , args:"; val () = (); |
|
1127 (*Specify_Step.complete_for*) |
|
1128 "~~~~~ fun complete_for , args:"; val () = (); |
|
1129 (* M_Match.match_itms_oris*) |
|
1130 "~~~~~ fun match_itms_oris , args:"; val () = (); |
|
1131 \<close> ML \<open> |
|
1132 (*+*)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)]" |
|
1133 = get_obj g_met pt (fst p) |> I_Model.to_string @{context}; |
|
1134 \<close> text \<open> |
|
1135 (*+isa: METHOD.drop* )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)]" =( *+isaALLcorrect*) |
|
1136 (*+isa2:METHOD.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)]" =(*isa2*) |
|
1137 get_obj g_met pt (fst p) |> I_Model.to_string @ {context}; |
|
1138 \<close> ML \<open> |
|
1139 |
|
1140 \<close> ML \<open> |
|
1141 (*case*) |
|
1142 Step.do_next p ((pt, Pos.e_pos'), []) (*of*); |
|
1143 (*//------------------ step into Step.do_next ----------------------------------------------\\*) |
|
1144 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), [])); |
|
1145 (*if*) Pos.on_calc_end ip (*else*); |
|
1146 val (_, probl_id, _) = Calc.references (pt, p); |
|
1147 val _ = |
|
1148 (*case*) tacis (*of*); |
|
1149 (*if*) probl_id = Problem.id_empty (*else*); |
|
1150 |
|
1151 Step.switch_specify_solve p_ (pt, ip); |
|
1152 (*///----------------- step into Step.switch_specify_solve ---------------------------------\\*) |
|
1153 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip)); |
|
1154 (*if*) Pos.on_specification ([], state_pos) (*then*); |
|
1155 |
|
1156 Step.specify_do_next (pt, input_pos); |
|
1157 (*////---------------- step into Step.specify_do_next --------------------------------------\\*) |
|
1158 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos); |
|
1159 |
|
1160 val (_, (p_', tac)) = |
|
1161 Specify.find_next_step ptp; |
|
1162 "~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp); |
|
1163 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl, |
|
1164 spec = refs, ...} = Calc.specify_data (pt, pos); |
|
1165 val ctxt = Ctree.get_ctxt pt pos; |
|
1166 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*); |
|
1167 (*if*) p_ = Pos.Pbl (*else*); |
|
1168 |
|
1169 \<close> ML \<open> |
|
1170 (*+*)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)]" |
|
1171 = met |> I_Model.to_string @{context}; |
|
1172 (*isa2* )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)]" |
|
1173 =( *isa2*) met |> I_Model.to_string @{context}; |
|
1174 |
|
1175 \<close> ML \<open> |
|
1176 (*isa2*)val ("dummy", (Met, Add_Given "FunctionVariable b")) =(*isa2*) |
|
1177 Specify.for_method ctxt oris (o_refs, refs) (pbl, met); |
|
1178 (*///// /------------- step into Step.for_method -------------------------------------------\\*) |
|
1179 "~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (_, met)) |
|
1180 = (ctxt, oris, (o_refs, refs), (pbl, met)); |
|
1181 val cmI = if mI = MethodC.id_empty then mI' else mI; |
|
1182 val {model, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*) |
|
1183 val (preok, _) = Pre_Conds.check ctxt where_rls where_ (model, I_Model.OLD_to_TEST met); |
|
1184 val NONE = |
|
1185 (*case*) find_first (I_Model.is_error o #5) met (*of*); |
|
1186 |
|
1187 (*isa2*)val SOME ("#Given", "FunctionVariable b") =(*isa2*) |
|
1188 (*case*) |
|
1189 Specify.item_to_add (ThyC.get_theory ctxt |
|
1190 (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*); |
|
1191 "~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms) |
|
1192 = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met); |
|
1193 (*\------------------- step into me_Specify_Method -----------------------------------------//*) |
|
1194 \<close> ML \<open>(*\------------- step into me_Specify_Method -----------------------------------------//*) |
|
1195 |
|
1196 val (p,_,f,nxt,_,pt) = return_me_Specify_Method |
|
1197 |
|
1198 \<close> ML \<open> |
|
1199 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Input_Descript.Domain {0<..<r}" = nxt; |
|
1200 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "ErrorBound (\<epsilon> = 0)" = nxt; |
|
1201 |
74 |
1202 |
75 \<close> ML \<open> |
1203 \<close> ML \<open> |
76 \<close> |
1204 \<close> |
77 |
1205 |
|
1206 (*ML_file "Minisubpbl/biegel ? ? ?.sml"*) |
78 section \<open>===================================================================================\<close> |
1207 section \<open>===================================================================================\<close> |
79 section \<open>===== ===========================================================================\<close> |
1208 section \<open>===== ===========================================================================\<close> |
80 ML \<open> |
1209 ML \<open> |
81 \<close> ML \<open> |
1210 \<close> ML \<open> |
82 |
1211 |
83 \<close> ML \<open> |
1212 \<close> ML \<open> |
84 \<close> |
1213 \<close> |
85 |
1214 |
|
1215 section \<open>===================================================================================\<close> |
|
1216 section \<open>===== ===========================================================================\<close> |
|
1217 ML \<open> |
|
1218 \<close> ML \<open> |
|
1219 |
|
1220 \<close> ML \<open> |
|
1221 \<close> |
|
1222 |
86 end |
1223 end |