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.
32 val (_(*example text*),
33 (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
34 "Extremum (A = 2 * u * v - u \<up> 2)" ::
35 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
36 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
37 "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
38 (*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)
39 "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
40 "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
41 "ErrorBound (\<epsilon> = (0::real))" :: []),
43 ["univariate_calculus", "Optimisation"],
44 ["Optimisation", "by_univariate_calculus"])))
45 = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
48 val return_init_calc =
49 Test_Code.init_calc @{context} [(model, refs)]; (*val Model_Problem = nxt;*)
50 (*/------------------- step into init_calc -------------------------------------------------\\*)
51 "~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))]) =
52 (@{context}, [(model, refs)]);
53 val thy = thy_id |> ThyC.get_theory ctxt
54 val ((pt, p), tacis) = Step_Specify.initialise' thy (model, refs)
55 val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
57 TESTg_form ctxt (pt,p);
58 "~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p));
60 ME_Misc.pt_extract ctxt ptp;
61 "~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_ as Pbl(*Frm,Pbl*)))) = (ctxt, ptp);
62 val ppobj = Ctree.get_obj I pt p
63 val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p;
64 (*if*) Ctree.is_pblobj ppobj (*then*);
66 "~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}), Pbl_) =
68 val (_, pI, _) = Ctree.get_somespec' spec spec';
69 (* val where_ = if pI = Problem.id_empty then []*)
70 (*if*) pI = Problem.id_empty (*else*);
71 val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
73 Pre_Conds.check_OLD ctxt where_rls where_
74 (model, I_Model.OLD_to_TEST probl);
75 "~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
76 (ctxt, where_rls, where_, (model, I_Model.OLD_to_TEST probl));
77 val (_, _, (env_subst, env_eval)) =
78 of_max_variant model_patt i_model;
79 "~~~~~ fun of_max_variant , args:"; val (_, []) = (model_patt, i_model);
80 (*\------------------- step into init_calc -------------------------------------------------//*)
81 val (p,_,f,nxt,_,pt) = return_init_calc;
83 (*+*)val PblObj {ctxt, probl, ...} = get_obj I pt [];
84 (*+*)Proof_Context.theory_of ctxt (*= {Pure, .., Diff_App}*);
85 (*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term ctxt "r"
88 val return_me_Model_Problem =
89 me nxt p c pt; val Add_Given "Constants [r = 7]" = #4 return_me_Model_Problem;
90 (*/------------------- step into me Model_Problem ------------------------------------------\\*)
91 "~~~~~ fun me , args:"; val (tac, (p:Pos.pos'), (_:Test_Code.NEW), (pt:Ctree.ctree)) = (nxt, p, c, pt);
92 val ctxt = Ctree.get_ctxt pt p
93 val return_by_tactic = case
94 Step.by_tactic tac (pt,p) of
95 ("ok", (_, _, ptp)) => ptp;
97 (*//------------------ step into by_tactic -------------------------------------------------\\*)
98 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
99 val Applicable.Yes tac' = (*case*)
100 Step.check tac (pt, p) (*of*);
101 (*+*)val Model_Problem' _ = tac';
102 "~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
103 (*if*) Tactic.for_specify tac (*then*);
105 Specify_Step.check tac (ctree, pos);
106 "~~~~~ fun check , args:"; val (Tactic.Model_Problem, (pt, pos as (p, _))) =
108 val (o_model, pI', ctxt) = case Ctree.get_obj I pt p of
109 Ctree.PblObj {origin = (o_model, (_, pI', _), _), ctxt, ...} => (o_model, pI', ctxt)
110 val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
111 val pbl = I_Model.init_TEST o_model model_patt;
114 Applicable.Yes (Tactic.Model_Problem' (pI', I_Model.TEST_to_OLD pbl, []));
115 (*\\------------------ step into by_tactic -------------------------------------------------//*)
116 val (pt, p) = return_by_tactic;
118 val return_do_next = (*case*)
119 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
120 (*//------------------ step into do_next ---------------------------------------------------\\*)
121 "~~~~~ fun do_next , args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) =
122 (p, ((pt, e_pos'),[]));
123 val pIopt = get_pblID (pt,ip);
124 (*if*) ip = ([],Res); (* = false*)
125 val _ = (*case*) tacis (*of*);
126 val SOME _ = (*case*) pIopt (*of*);
128 val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
129 Step.switch_specify_solve p_ (pt, ip);
130 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
131 (*if*) Pos.on_specification ([], state_pos) (*then*);
133 val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
134 Step.specify_do_next (pt, input_pos);
135 (*///----------------- step into specify_do_next -------------------------------------------\\*)
136 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
138 (* val (_, (p_', tac)) =*)
139 val return_find_next_step = (*keep for continuing specify_do_next*)
140 Specify.find_next_step ptp;
141 (*////---------------- step into find_next_step --------------------------------------------\\*)
142 "~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
143 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
144 spec = refs, ...} = Calc.specify_data (pt, pos);
145 val ctxt = Ctree.get_ctxt pt pos;
146 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
147 (*if*) p_ = Pos.Pbl (*then*);
149 Specify.for_problem ctxt oris (o_refs, refs) (pbl, met);
150 (*/////--------------- step into for_problem -----------------------------------------------\\*)
151 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
152 = (ctxt, oris, (o_refs, refs), (pbl, met));
153 val cdI = if dI = ThyC.id_empty then dI' else dI;
154 val cpI = if pI = Problem.id_empty then pI' else pI;
155 val cmI = if mI = MethodC.id_empty then mI' else mI;
156 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
157 val {model = mpc, ...} = MethodC.from_store ctxt cmI;
158 (*//------------------ adhoc inserted fun of_max_variant -----------------------------------\\*)
159 (*\\------------------ adhoc inserted fun check_OLD ----------------------------------------//*)
161 val return_check_OLD =
162 check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
163 (*//////-------------- step into check_OLD -------------------------------------------------\\*)
164 "~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
165 (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
166 val return_of_max_variant =
167 of_max_variant model_patt i_model;
168 (*///// //------------ step into of_max_variant --------------------------------------------\\*)
169 "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) =
170 (model_patt, i_model);
173 (*+*)val "[\n(0, [], false ,#Given, (Inc_TEST Constants [__=__, __=__], Position.T)), \n(0, [], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(0, [], false ,#Find, (Inc_TEST AdditionalValues [__, __], Position.T)), \n(0, [], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(0, [], false ,#Relate, (Inc_TEST SideConditions [__=__, __=__], Position.T))]"
174 = i_model |> I_Model.to_string_TEST @ {context}
176 (*+*)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))]"
177 = i_model |> I_Model.to_string_TEST @{context}
179 map (fn (_, variants, _, _, _) => variants) i_model
182 val variants_separated = map (filter_variants' i_model) all_variants
183 val sums_corr = map (cnt_corrects) variants_separated
184 val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
185 (*+*)val [(0, 1), (0, 2), (0, 3)] = sum_variant_s
186 val (_, max_variant) = hd (*..crude decision, up to improvement *)
187 (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
189 filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
190 val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
191 (*for building make_env_s -------------------------------------------------------------------\*)
192 (*!!!*) val ("#Given", (descr, term), pos) =
193 Model_Pattern.split_descriptor ctxt ("#Given", @{term "Constants [r = (7::real)]"}, Position.none)
194 (*!!!*) val patt = equal_descr_pairs |> hd |> #1
195 (*!!!*)val equal_descr_pairs =
197 (1, [1, 2, 3], true, "#Given", (Cor_TEST ((descr, (*!*)TermC.isalist2list(*!*) term),
198 (TermC.empty, [])), pos)))
199 :: tl equal_descr_pairs
200 (*for building make_env_s -------------------------------------------------------------------/*)
202 val env_model = make_env_model equal_descr_pairs;
203 (*///// ///----------- step into make_env_model --------------------------------------------\\*)
204 "~~~~~ fun make_env_model , args:"; val (equal_descr_pairs) = (equal_descr_pairs);
206 val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
207 => (mk_env_model id feedb));
208 val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 4 equal_descr_pairs;
209 (*\\\\\ \\\----------- step into make_env_model --------------------------------------------//*)
210 (*||||| ||------------ contine of_max_variant ------------------------------------------------*)
212 val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
213 val subst_eval_list = make_envs_preconds equal_givens
214 val return_make_envs_preconds =
215 make_envs_preconds equal_givens;
216 (*///// ///----------- step into make_envs_preconds ----------------------------------------\\*)
217 "~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
218 val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb)
220 xxx: (Model_Pattern.single * I_Model.single_TEST) -> ((term * term) * (term * term)) list;
221 val return_discern_feedback =
222 discern_feedback id feedb;
223 (*nth 1 equal_descr_pairs* )
224 "~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) = (id, feedb);
225 ( *nth 2 equal_descr_pairs*)
226 "~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Inc_TEST ((descr, ts), _))) = (id, feedb);
228 (*nth 1 equal_descr_pairs* )
229 (*+*)val [((Const ("fixes", typ1), Free ("r", typ2)),
230 (Free ("r", typ3), value))] = return_discern_feedback
231 (*+*)val true = typ1 = typ2
232 (*+*)val true = typ3 = HOLogic.realT
233 (*+*)val "7" = UnparseC.term @{context} value
234 ( *nth 2 equal_descr_pairs*)
235 (*+*)val [] = return_discern_feedback
237 val return_discern_typ =
238 discern_typ id (descr, ts);
239 "~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts));
240 (*nth 1 equal_descr_pairs* )
241 (*+*)val [((Const ("fixes", typ1), Free ("r", typ2)),
242 (Free ("r", typ3), value))] = return_discern_typ
243 (*+*)val true = typ1 = typ2
244 (*+*)val true = typ3 = HOLogic.realT
245 (*+*)val "7" = UnparseC.term @{context} value
246 ( *nth 2 equal_descr_pairs*)
247 (*+*)val [] = return_discern_typ;
249 switch_type_TEST id ts;
250 "~~~~~ fun switch_type_TEST , args:"; val (Const (descr_string, _), ts) = (descr, ts);
252 (*nth 1 equal_descr_pairs* )
253 val return_switch_type_TEST = Const (descr_string, ts |> hd |> TermC.lhs |> type_of)
255 (*+*)val Const ("Input_Descript.Constants", typ) = return_switch_type_TEST
256 (*+*)val Type ("Real.real", []) = typ
257 ( *nth 2 equal_descr_pairs*)
258 (*+*)val return_switch_type_TEST = descr
260 (*\\\\\ \\\----------- step into make_envs_preconds ----------------------------------------//*)
261 (*||||| ||------------ contine of_max_variant ------------------------------------------------*)
262 val subst_eval_list = make_envs_preconds equal_givens
263 val (env_subst, env_eval) = split_list subst_eval_list
264 val return_of_max_variant = (i_model_max, env_model, (env_subst, env_eval)); (*GOON*)
265 (*\\\\\ \\------------ step into of_max_variant --------------------------------------------//*)
266 val (i_model_max, env_model, (env_subst, env_eval)) = return_of_max_variant
267 (*!!!/----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---\*)
268 val (i_max_variant, env_model, (env_subst, env_eval)) = (i_model_max, [], ([], []))
269 (*!!!\----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---/*)
270 (*||||||-------------- contine check_OLD -----------------------------------------------------*)
271 val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
272 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
273 val full_subst = if env_eval = [] then pres_subst_other
274 else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
275 val evals = map (eval ctxt where_rls) full_subst
276 val return_ = (i_model_max, env_subst, env_eval)
277 (*\\\\\\\------------- step into check_OLD -------------------------------------------------//*)
278 val (preok, _) = return_check_OLD;
280 (*|||||--------------- contine for_problem ---------------------------------------------------*)
281 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
282 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
284 (*case*) find_first (I_Model.is_error o #5) pbl (*of*);
287 Specify.item_to_add (ThyC.get_theory ctxt
288 (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
289 "~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
290 = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, pbt, pbl);
291 fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
292 | false_and_not_Sup (_, _, false, _, _) = true
293 | false_and_not_Sup _ = false
295 val v = if itms = [] then 1 else Pre_Conds.max_variant itms
296 val vors = if v = 0 then oris
297 else filter ((fn variant =>
298 fn (_, variants, m_field, _, _) => member op= variants variant andalso m_field <> "#undef")
301 (*+*)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]\"])]"
302 (*+*) = vors |> O_Model.to_string @{context}
304 val vits = if v = 0 then itms (* because of dsc without dat *)
305 else filter ((fn variant =>
306 fn (_, variants, _, _, _) => member op= variants variant)
307 v) itms; (* itms..vat *)
309 val icl = filter false_and_not_Sup vits; (* incomplete *)
311 (*if*) icl = [] (*else*);
312 (*+*)val "[\n(1 ,[1, 2, 3] ,false ,#Given ,Inc Constants [] ,(Constants, [])), \n(2 ,[1, 2, 3] ,false ,#Find ,Inc Maximum ,(Maximum, [])), \n(3 ,[1, 2, 3] ,false ,#Find ,Inc AdditionalValues [] ,(AdditionalValues, [])), \n(4 ,[1, 2, 3] ,false ,#Relate ,Inc Extremum ,(Extremum, [])), \n(5 ,[1, 2] ,false ,#Relate ,Inc SideConditions [] ,(SideConditions, []))]"
313 (*+*) = icl |> I_Model.to_string @{context}
314 (*+*)val "(1 ,[1, 2, 3] ,false ,#Given ,Inc Constants [] ,(Constants, []))"
315 (*+*) = hd icl |> I_Model.single_to_string @{context}
317 (*++*)val feedback = (fn (_, _, _, _, feedback) => feedback) (hd icl)
318 (*++*)val Const ("Input_Descript.Constants", _) = I_Model.descriptor feedback
319 (*++*)val [] = I_Model.o_model_values feedback
321 (*+*)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]\"])]"
322 (*+*) = vors |> O_Model.to_string @{context}
325 (*case*) find_first ((fn (_, _, _, _, feedback) => fn (_, _, _, d, ts) =>
326 d = I_Model.descriptor feedback andalso subset op = (I_Model.o_model_values feedback, ts))
327 (hd icl)) vors (*of*);
329 (*+*)val "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"])" =
330 (*+*) ori |> O_Model.single_to_string @{context}
331 (*\\\\\--------------- step into for_problem -----------------------------------------------//*)
332 (*\\\\---------------- step into find_next_step --------------------------------------------//*)
333 (*|||----------------- continuing specify_do_next --------------------------------------------*)
334 val (_, (p_', tac)) = return_find_next_step (*kept for continuing specify_do_next*)
336 val ist_ctxt = Ctree.get_loc pt (p, p_)
337 (*+*)val Add_Given "Constants [r = 7]" = tac
341 Step_Specify.by_tactic_input tac (pt, (p, p_'));
342 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =
343 (tac, (pt, (p, p_')));
345 Specify.by_Add_ "#Given" ct ptp;
346 "~~~~~ fun by_Add_ , args:"; val (m_field, ct ,(pt, pos as (_, p_))) =
348 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
349 val (i_model, m_patt) =
352 (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
355 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model);
358 I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
359 "~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, (str(*, pos*))) =
360 (ctxt, m_field, oris, i_model, m_patt, ct);
361 val (t as (descriptor $ _)) = Syntax.read_term ctxt str
363 (*+*)val "Constants [r = 7]" = UnparseC.term @{context} t;
366 (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
367 (*if*) m_field <> m_field' (*else*);
369 (*+*)val "#Given" = m_field; val "#Given" = m_field'
371 val ("", ori', all) =
372 (*case*) O_Model.contains ctxt m_field o_model t (*of*);
374 (*+*)val (_, _, _, _, vals) = hd o_model;
375 (*+*)val "Constants [r = 7]" = UnparseC.term @{context} (@{term Constants} $ (hd vals));
376 (*+*)if "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), " ^
377 (*+*) "\n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), " ^
378 (*+*) "\n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), " ^
379 (*+*) "\n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), " ^
380 (*+*) "\n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), " ^
381 (*+*) "\n(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), " ^
382 (*+*) "\n(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), " ^
383 (*+*) "\n(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), " ^
384 (*+*) "\n(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), " ^
385 (*+*) "\n(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), " ^
386 (*+*) "\n(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
387 (*+*)= O_Model.to_string @{context} o_model then () else error "o_model CHANGED";
389 (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*);
390 "~~~~~ fun is_notyet_input , args:"; val (ctxt, itms, all, (i, v, f, d, ts), pbt) =
391 (ctxt, i_model, all, ori', m_patt);
392 val SOME (_, (_, pid)) =
393 (*case*) find_first (eq1 d) pbt (*of*);
394 (*local*)fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (I_Model.descriptor itm_);(*local*)
395 val SOME (_, _, _, _, itm_) =
396 (*case*) find_first (eq3 f d) itms (*of*);
397 val ts' = inter op = (o_model_values itm_) ts;
398 (*if*) subset op = (ts, ts') (*else*);
399 val return_is_notyet_input = ("",
400 ori_2itm itm_ pid all (i, v, f, d, subtract op = ts' ts));
401 "~~~~~ fun ori_2itm , args:"; val (itm_, pid, all, (id, vt, fd, d, ts)) =
402 (itm_, pid, all, (i, v, f, d, subtract op = ts' ts));
403 val ts' = union op = (o_model_values itm_) ts;
404 val pval = [Input_Descript.join'''' (d, ts')]
405 val complete = if eq_set op = (ts', all) then true else false
407 (*+*)val "Inc Constants [] ,(Constants, [])" = itm_ |> I_Model.feedback_to_string @{context}
408 (*\\\----------------- step into specify_do_next -------------------------------------------//*)
409 (*\\------------------ step into do_next ---------------------------------------------------//*)
410 val ("ok", (ts as (_, _, _) :: _, _, (pt, p))) = return_do_next
412 (*|------------------- continue with me_Model_Problem ----------------------------------------*)
414 val tacis as (_::_) =
416 val (tac, _, _) = last_elem tacis
418 val return_Model_Problem = (p, [] : NEW, TESTg_form ctxt (pt, p), tac, Celem.Sundef, pt);
419 (*//------------------ step into TESTg_form ------------------------------------------------\\*)
420 "~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt, p));
423 ME_Misc.pt_extract ctxt ptp;
424 "~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_(*Frm,Pbl*)))) = (ctxt, ptp);
425 val ppobj = Ctree.get_obj I pt p
426 val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p;
427 (*if*) Ctree.is_pblobj ppobj (*then*);
430 "~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}),
431 Pbl(*Frm,Pbl*)) = (ppobj, p_);
432 val (_, pI, _) = Ctree.get_somespec' spec spec';
433 (*if*) pI = Problem.id_empty (*else*);
434 (* val where_ = if pI = Problem.id_empty then []*)
437 val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
438 val (_, where_) = (*Pre_Conds.*)check_OLD ctxt where_rls where_ (model, I_Model.OLD_to_TEST probl)
440 val allcorrect = I_Model.is_complete probl andalso foldl and_ (true, (map #1 where_))
441 val return_pt_model = Ctree.ModSpec (allcorrect, Pos.Pbl, hdl, probl, where_, spec)
443 (*|------------------- continue with TESTg_form ----------------------------------------------*)
444 val Ctree.ModSpec (spec as (_, p_, _, gfr, where_, _)) =
445 (*case*) form (*of*);
446 Test_Out.PpcKF ( (Test_Out.Problem [],
447 P_Model.from (Proof_Context.theory_of ctxt) gfr where_));
449 P_Model.from (Proof_Context.theory_of ctxt) gfr where_;
450 "~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);
451 fun coll model [] = model
452 | coll model ((_, _, _, field, itm_) :: itms) =
453 coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
455 val gfr = coll P_Model.empty itms;
456 "~~~~~ fun coll , args:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: itms))
457 = (P_Model.empty, itms);
459 (*+*)val 4 = length itms;
460 (*+*)val itm = nth 1 itms;
462 coll P_Model.empty [itm];
463 "~~~~~ fun coll , iterate:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: []))
464 = (P_Model.empty, [itm]);
466 (add_sel_ppc thy field model (item_from_feedback thy itm_));
467 "~~~~~ fun add_sel_ppc , args:"; val ((_: theory), sel, {Given = gi, Where = wh, Find = fi, With = wi, Relate = re}, x )
468 = (thy, field, model, (item_from_feedback thy itm_));
470 P_Model.item_from_feedback thy itm_;
471 "~~~~~ fun item_from_feedback , args:"; val (thy, (I_Model.Inc ((d, ts), _))) = (thy, itm_);
472 P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)));
473 (*\\------------------ step into TESTg_form ------------------------------------------------//*)
474 (*\------------------- step into me Model_Problem ------------------------------------------//*)
475 val (p, _, f, nxt, _, pt) = return_me_Model_Problem
477 (*-------------------- contine me's ----------------------------------------------------------*)
478 val return_me_add_find_Constants = me nxt p c pt;
479 val Add_Find "Maximum A" = #4 return_me_add_find_Constants;
480 (*/------------------- step into me_add_find_Constants -------------------------------------\\*)
481 "~~~~~ fun me , args:"; val (tac as Add_Given "Constants [r = 7]", p, _(*NEW remove*), pt) =
483 val ctxt = Ctree.get_ctxt pt p
484 (*+*)val PblObj {probl = (1, [1, 2, 3], false, "#Given", Inc
485 ((Const ("Input_Descript.Constants", _), []), _)) :: _, ...} = get_obj I pt (fst p)
486 (*-------------------------------------------^^--*)
487 val return_step_by_tactic = (*case*)
488 Step.by_tactic tac (pt, p) (*of*);
489 (*//------------------ step into Step.by_tactic --------------------------------------------\\*)
490 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
491 val Applicable.Yes tac' =
492 (*case*) check tac (pt, p) (*of*);
493 (*if*) Tactic.for_specify' tac' (*then*);
494 Step_Specify.by_tactic tac' ptp;
495 "~~~~~ fun by_tactic , args:"; val ((Tactic.Add_Given' (ct, _)), (pt, p)) = (tac', ptp);
497 Specify.by_Add_ "#Given" ct (pt, p);
498 "~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, (pt, p));
499 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
500 (* val (i_model, m_patt) =*)
501 (*if*) p_ = Pos.Met (*else*);
504 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)
505 val I_Model.Add i_single =
506 (*case*) I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
509 I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model;
510 "~~~~~ fun add_single , args:"; val (thy, itm, model) =
511 ((Proof_Context.theory_of ctxt), i_single, i_model);
512 fun eq_untouched d (0, _, _, _, itm_) = (d = I_Model.descriptor itm_)
513 | eq_untouched _ _ = false
514 val model' = case I_Model.seek_ppc (#1 itm) model of
515 SOME _ => overwrite_ppc thy itm model (*itm updated in is_notyet_input WN.11.03*)
517 (*||------------------ contine Step.by_tactic ------------------------------------------------*)
518 (*\\------------------ step into Step.by_tactic --------------------------------------------//*)
519 val ("ok", (_, _, ptp)) = return_step_by_tactic;
523 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
524 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
525 (p, ((pt, Pos.e_pos'), []));
526 (*if*) Pos.on_calc_end ip (*else*);
527 val (_, probl_id, _) = Calc.references (pt, p);
529 (*case*) tacis (*of*);
530 (*if*) probl_id = Problem.id_empty (*else*);
532 switch_specify_solve p_ (pt, ip);
533 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
534 (*if*) Pos.on_specification ([], state_pos) (*then*);
536 specify_do_next (pt, input_pos);
537 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
538 val (_, (p_', tac)) =
539 Specify.find_next_step ptp;
540 "~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
541 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
542 spec = refs, ...} = Calc.specify_data (pt, pos);
543 val ctxt = Ctree.get_ctxt pt pos;
545 (*+*)val (1, [1, 2, 3], true, "#Given", Cor ((Const ("Input_Descript.Constants", _), ts ), _)) :: _
547 (*+*)val "[[r = 7]]" = UnparseC.terms @{context} ts;
548 (*-----ML-^------^-HOL*)
550 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
551 (*if*) p_ = Pos.Pbl (*then*);
553 for_problem ctxt oris (o_refs, refs) (pbl, met);
554 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
555 (ctxt, oris, (o_refs, refs), (pbl, met));
556 val cpI = if pI = Problem.id_empty then pI' else pI;
557 val cmI = if mI = MethodC.id_empty then mI' else mI;
558 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
559 val {model = mpc, ...} = MethodC.from_store ctxt cmI
562 Pre_Conds.check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
563 "~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
564 (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
566 val (_, _, (env_subst, env_eval)) = of_max_variant model_patt i_model;
567 "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
569 map (fn (_, variants, _, _, _) => variants) i_model
572 val variants_separated = map (filter_variants' i_model) all_variants
573 val sums_corr = map (cnt_corrects) variants_separated
574 val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
575 val (_, max_variant) = hd (*..crude decision, up to improvement *)
576 (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
578 filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
579 val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
580 val env_model = make_env_model equal_descr_pairs
581 val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
583 val subst_eval_list =
584 make_envs_preconds equal_givens;
585 "~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
586 val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) =>
587 discern_feedback id feedb)
588 val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 1 equal_givens;
589 "~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) = (id, feedb);
591 discern_typ id (descr, ts);
592 "~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts));
593 (*|------------------- contine me_add_find_Constants -----------------------------------------*)
594 (*\------------------- step into me_add_find_Constants -------------------------------------//*)
595 val (p,_,f,nxt,_,pt) = return_me_add_find_Constants;
596 (*/########################## before destroying elementwise input of lists ##################\* )
597 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u]" = nxt;
598 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [v]" = nxt;
599 ( *\########################## before destroying elementwise input of lists ##################/*)
600 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u, v]" = nxt;
602 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)" = nxt;
603 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;
604 val return_me_Add_Relation_SideConditions
606 (*+*)val (_, _, _, Specify_Theory "Diff_App", _, _) = return_me_Add_Relation_SideConditions; (*###############*)
607 (*/------------------- step into me Add_Relation_SideConditions ----------------------------\\*)
608 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
609 val ctxt = Ctree.get_ctxt pt p;
610 (**) val (pt, p) = (**)
611 (**)case(**) Step.by_tactic tac (pt, p) (**)of(**)
612 (**) ("ok", (_, _, ptp)) => ptp (**) ;
615 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
616 (*//------------------ step into do_next ---------------------------------------------------\\*)
617 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
618 = (p, ((pt, Pos.e_pos'), [])) (*of*);
619 (*if*) Pos.on_calc_end ip (*else*);
620 val (_, probl_id, _) = Calc.references (pt, p);
621 (*case*) tacis (*of*);
622 (*if*) probl_id = Problem.id_empty (*else*);
624 Step.switch_specify_solve p_ (pt, ip);
625 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
626 (*if*) Pos.on_specification ([], state_pos) (*then*);
627 Step.specify_do_next (pt, input_pos);
628 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
629 (*isa------ERROR: Refine_Problem INSTEAD
630 isa2: Specify_Theory "Diff_App"*)
631 val (_, (p_', tac as Specify_Theory "Diff_App")) =
632 (*ERROR------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
633 Specify.find_next_step ptp;
634 "~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
635 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
636 spec = refs, ...} = Calc.specify_data (pt, pos);
637 val ctxt = Ctree.get_ctxt pt pos;
638 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
639 (*if*) p_ = Pos.Pbl (*then*);
641 val ("dummy", (Pbl, tac as Specify_Theory "Diff_App")) =
642 (*ERROR------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
643 for_problem ctxt oris (o_refs, refs) (pbl, met);
644 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
645 (ctxt, oris, (o_refs, refs), (pbl, met));
646 val cpI = if pI = Problem.id_empty then pI' else pI;
647 val cmI = if mI = MethodC.id_empty then mI' else mI;
648 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
649 val {model = mpc, ...} = MethodC.from_store ctxt cmI
651 (*+*)val [Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
652 Free ("fixes", _)] = where_
655 Pre_Conds.check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
656 (*///----------------- step into check_OLD -------------------------------------------------\\*)
657 "~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
658 (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
659 (*+*)val "[0 < fixes]" = pres |> UnparseC.terms @{context}
660 (*+*)val "[\"(#Given, (Constants, fixes))\", \"(#Find, (Maximum, maxx))\", \"(#Find, (AdditionalValues, vals))\", \"(#Relate, (Extremum, extr))\", \"(#Relate, (SideConditions, sideconds))\"]"
661 (*+*) = model_patt |> Model_Pattern.to_string @{context}
662 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] ,(fixes, [[r = 7]]), Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A ,(maxx, [A]), Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] ,(vals, [[u, v]]), Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) ,(extr, [A = 2 * u * v - u \<up> 2]), Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] ,(sideconds, [[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]]), Position.T))]"
663 (*+*) = i_model |> I_Model.to_string_TEST @{context}
665 val return_of_max_variant as (_, _, (env_subst, env_eval)) =
666 of_max_variant model_patt i_model
668 (*+*)val [(Free ("fixes", T1), Free ("r", T2))] = env_subst (*?!? Const*)
669 (*+*)val Type ("Real.real", []) = T1
670 (*+*)val Type ("Real.real", []) = T2
672 (*+*)val [(Free ("r", T2), Const ("Num.numeral_class.numeral", _) $ _)] = env_eval
673 (*+*)val Type ("Real.real", []) = T2
675 val (_, _, (env_subst, env_eval)) = return_of_max_variant;
676 (*|||----------------- contine check_OLD -----------------------------------------------------*)
677 val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
679 (*|||----------------- contine check_OLD -----------------------------------------------------*)
680 (*+*)val [(true, Const ("Orderings.ord_class.less", _) $
681 Const ("Groups.zero_class.zero", _) $ Free ("r", _))] = pres_subst
683 val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
685 Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
686 (Const ("Num.numeral_class.numeral", _) $ _))] = full_subst
688 val evals = map (eval ctxt where_rls) full_subst
689 val return_check_OLD = (foldl and_ (true, map fst evals), pres_subst)
690 (*\\\----------------- step into check_OLD -------------------------------------------------\\*)
692 val (preok as true, _) = return_check_OLD
693 (*+---------------^^^^*)
694 (*\\------------------ step into do_next ---------------------------------------------------\\*)
695 (*\------------------- step into me_Add_Relation_SideConditions ----------------------------//*)
696 val (p, _, f, nxt, _, pt) = return_me_Add_Relation_SideConditions
697 val Specify_Theory "Diff_App" = nxt;
699 val return_me_Specify_Theory
700 = me nxt p c pt; val Specify_Problem ["univariate_calculus", "Optimisation"] = #4 return_me_Specify_Theory;
701 (*/------------------- step into me Specify_Theory -----------------------------------------\\*)
702 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
703 val ctxt = Ctree.get_ctxt pt p;
705 (*case*) Step.by_tactic tac (pt, p) (*of*);
706 (* ("ok", (_, _, ptp)) => ptp *)
707 val return_Step_by_tactic =
708 Step.by_tactic tac (pt, p);
709 (*//------------------ step into Step_by_tactic --------------------------------------------\\*)
710 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
711 (*case*) check tac (pt, p) (*of*);
713 (*||------------------ contine Step_by_tactic ------------------------------------------------*)
714 (*\\------------------ step into Step_by_tactic --------------------------------------------//*)
716 val ("ok", (_, _, ptp)) = return_Step_by_tactic;
717 (*|------------------- continue me Specify_Theory --------------------------------------------*)
719 val ("ok", (ts as (_, _, _) :: _, _, _)) =
721 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
722 (*//------------------ step into do_next ---------------------------------------------------\\*)
723 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
724 = (p, ((pt, Pos.e_pos'), [])) (*of*);
725 (*if*) Pos.on_calc_end ip (*else*);
726 val (_, probl_id, _) = Calc.references (pt, p);
728 (*case*) tacis (*of*);
729 (*if*) probl_id = Problem.id_empty (*else*);
731 Step.switch_specify_solve p_ (pt, ip);
732 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
733 (*if*) Pos.on_specification ([], state_pos) (*then*);
735 Step.specify_do_next (pt, input_pos);
736 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
737 val (_, (p_', tac)) = Specify.find_next_step ptp
738 val ist_ctxt = Ctree.get_loc pt (p, p_);
741 Step_Specify.by_tactic_input tac (pt, (p, p_'));
742 (*+*)val Specify_Theory "Diff_App" = tac;
743 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Theory dI), (pt, pos as (_, Pbl)))
744 = (tac, (pt, (p, p_')));
745 val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
746 PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
747 (oris, dI, dI', pI', probl, ctxt)
748 val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');
749 val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
750 (*\\------------------ step into do_next ---------------------------------------------------//*)
751 (*\------------------- step into me Specify_Theory -----------------------------------------//*)
752 val (p,_,f,nxt,_,pt) = return_me_Specify_Theory;
754 val return_me_Specify_Problem (* keep for continuing me *)
755 = me nxt p c pt; val Specify_Method ["Optimisation", "by_univariate_calculus"] = #4 return_me_Specify_Problem;
756 (*/------------------- step into me Specify_Problem ----------------------------------------\\*)
757 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
758 val ctxt = Ctree.get_ctxt pt p
760 (** ) val ("ok", (_, _, ptp as (pt, p))) =( **)
761 (**) val return_by_tactic =(**) (*case*)
762 Step.by_tactic tac (pt, p) (*of*);
763 (*//------------------ step into by_tactic -------------------------------------------------\\*)
764 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
767 Step.check tac (pt, p) (*of*);
768 "~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
769 (*if*) Tactic.for_specify tac (*then*);
771 Specify_Step.check tac (ctree, pos);
772 "~~~~~ fun check , args:"; val ((Tactic.Specify_Problem pID), (pt, pos as (p, _)))
773 = (tac, (ctree, pos));
774 val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of
775 Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
776 => (oris, dI, pI, dI', pI', itms)
777 val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');
778 (*\\------------------ step into by_tactic -------------------------------------------------//*)
779 val ("ok", (_, _, ptp as (pt, p))) = return_by_tactic (* kept for continuing me *);
782 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
783 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
784 (*if*) Pos.on_calc_end ip (*else*);
785 val (_, probl_id, _) = Calc.references (pt, p);
787 (*case*) tacis (*of*);
788 (*if*) probl_id = Problem.id_empty (*else*);
790 Step.switch_specify_solve p_ (pt, ip);
791 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
792 (*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 val (_, (p_', tac)) = Specify.find_next_step ptp
797 val ist_ctxt = Ctree.get_loc pt (p, p_)
801 Step_Specify.by_tactic_input tac (pt, (p, p_'));
802 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos))
803 = (tac, (pt, (p, p_')));
805 val (o_model, ctxt, i_model) =
806 Specify_Step.complete_for id (pt, pos);
807 "~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));
808 val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
809 ...} = Calc.specify_data (ctree, pos);
810 val ctxt = Ctree.get_ctxt ctree pos
811 val (dI, _, _) = References.select_input o_refs refs;
812 val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
813 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
814 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
815 val thy = ThyC.get_theory ctxt dI
816 val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
817 (*\------------------- step into me Specify_Problem ----------------------------------------//*)
818 val (p,_,f,nxt,_,pt) = return_me_Specify_Problem
820 val return_me_Add_Given_FunctionVariable
821 = me nxt p c pt; val Add_Given "FunctionVariable a" = #4 return_me_Add_Given_FunctionVariable;
822 (*/------------------- step into me Specify_Method -----------------------------------------\\*)
823 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
824 val ctxt = Ctree.get_ctxt pt p
826 (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
827 case Step.by_tactic tac (pt, p) of
828 ("ok", (_, _, ptp)) => ptp;
831 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
832 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
833 (*if*) Pos.on_calc_end ip (*else*);
834 val (_, probl_id, _) = Calc.references (pt, p);
836 (*case*) tacis (*of*);
837 (*if*) probl_id = Problem.id_empty (*else*);
839 Step.switch_specify_solve p_ (pt, ip);
840 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
841 (*if*) Pos.on_specification ([], state_pos) (*then*);
843 Step.specify_do_next (pt, input_pos);
844 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
846 val (_, (p_', tac)) =
847 Specify.find_next_step ptp;
848 "~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
849 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
850 spec = refs, ...} = Calc.specify_data (pt, pos);
851 val ctxt = Ctree.get_ctxt pt pos;
852 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
853 (*if*) p_ = Pos.Pbl (*else*);
855 Specify.for_method ctxt oris (o_refs, refs) (pbl, met);
856 "~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
857 = (ctxt, oris, (o_refs, refs), (pbl, met));
858 val cmI = if mI = MethodC.id_empty then mI' else mI;
859 val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
860 val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0;
862 (*case*) find_first (I_Model.is_error o #5) met (*of*);
865 Specify.item_to_add (ThyC.get_theory ctxt
866 (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
867 "~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
868 = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
869 (*\------------------- step into me Specify_Method -----------------------------------------//*)
870 val (p,_,f,nxt,_,pt) = return_me_Add_Given_FunctionVariable
872 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Input_Descript.Domain {0<..<r}" = nxt;
873 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "ErrorBound (\<epsilon> = 0)" = nxt;
875 (* ------------------- step into UNTIL A PROGRAM IS REQUIRED (not yet impl. ---------------- )*)
876 (*/------------------- step into me_Add_Given_ErrorBound------------------------------------\\*)
877 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
878 val ctxt = Ctree.get_ctxt pt p
880 (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
881 case Step.by_tactic tac (pt, p) of
882 ("ok", (_, _, ptp)) => ptp;
883 (*ERROR due to missing program in creating the environment from formal args* )
885 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
887 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis) ) =
888 (p, ((pt, Pos.e_pos'), []));
889 (*if*) Pos.on_calc_end ip (*else*);
890 val (_, probl_id, _) = Calc.references (pt, p);
892 (*case*) tacis (*of*);
893 (*if*) probl_id = Problem.id_empty (*else*);
895 (*ERROR due to missing program in creating the environment from formal args* )
896 switch_specify_solve p_ (pt, ip);
898 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
899 (*if*) Pos.on_specification ([], state_pos) (*then*);
901 (*ERROR due to missing program in creating the environment from formal args* )
902 specify_do_next (pt, input_pos)
904 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
905 val (_, (p_', tac as Apply_Method ["Optimisation", "by_univariate_calculus"])) =
906 (*-------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ not yet impl.*)
907 Specify.find_next_step ptp
908 val ist_ctxt = Ctree.get_loc pt (p, p_)
910 val Tactic.Apply_Method (mI as ["Optimisation", "by_univariate_calculus"]) =
912 (*ERROR due to missing program in creating the environment from formal args* )
913 LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
914 ist_ctxt (pt, (p, p_'))
916 "~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
917 ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));
918 val (itms, oris, probl) = case get_obj I pt p of
919 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
920 val {model, ...} = MethodC.from_store ctxt mI;
921 (*if*) itms <> [] (*then*);
922 val itms = I_Model.complete oris probl [] model
924 (*+*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] ,(fixes, [[r = 7]])), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A ,(maxx, [A])), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] ,(vals, [[u, v]])), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) ,(extr, [A = 2 * u * v - u \<up> 2])), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] ,(sideconds, [[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]])), \n(7 ,[1] ,true ,#Given ,Cor FunctionVariable a ,(funvar, [a])), \n(10 ,[1, 2] ,true ,#Given ,Cor Input_Descript.Domain {0<..<r} ,(doma, [{0<..<r}])), \n(12 ,[1, 2, 3] ,true ,#Given ,Cor ErrorBound (\<epsilon> = 0) ,(err, [\<epsilon> = 0]))]"
925 = itms |> I_Model.to_string @{context}
926 (*+*)val 8 = length itms
927 (*+*)val 8 = length model
928 (*\------------------- step into me_Add_Given_ErrorBound------------------------------------//*)