prepare 4: shift new code (previous CS was: intermediate I_Model.complete_method)
1 (* use this theory for tests before Build_Isac.thy has succeeded *)
2 theory Test_Theory imports "$ISABELLE_ISAC/Build_Isac"
3 "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine" (* setup for refine.sml *)
5 ML_file "$ISABELLE_ISAC/BaseDefinitions/libraryC.sml"
7 section \<open>code for copy & paste ===============================================================\<close>
10 declare [[show_sorts]]
11 find_theorems "?a <= ?a"
17 ML_command \<open>Pretty.writeln prt\<close>
18 declare [[ML_print_depth = 999]]
19 declare [[ML_exception_trace]]
23 "~~~~~ fun xxx , args:"; val () = ();
24 "~~~~~ and xxx , args:"; val () = ();
25 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
26 "~~~~~ continue fun xxx"; val () = ();
27 (*if*) (*then*); (*else*); (*andalso*) (*case*) (*of*); (*return value*); (*in*) (*end*);
29 ^ "xxx" (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)
30 \<close> ML \<open> (*//----------- build fun XXXXX -----------------------------------------------------\\*)
31 (*//------------------ build fun XXXXX -----------------------------------------------------\\*)
32 (*\\------------------ build fun XXXXX -----------------------------------------------------//*)
33 \<close> ML \<open> (*\\----------- build fun XXXXX -----------------------------------------------------//*)
35 val return_XXXXX = "XXXXX"
36 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
37 (*//------------------ step into XXXXX -----------------------------------------------------\\*)
38 \<close> ML \<open> (*||----------- contine XXXXX ---------------------------------------------------------*)
39 (*||------------------ contine XXXXX ---------------------------------------------------------*)
40 (*\\------------------ step into XXXXX -----------------------------------------------------//*)
41 \<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)
42 val "XXXXX" = return_XXXXX;
44 (* final test ... ----------------------------------------------------------------------------*)
46 \<close> ML \<open> (*//----------- inserted hidden code ------------------------------------------------\\*)
47 (*//------------------ inserted hidden code ------------------------------------------------\\*)
48 (*\\------------------ inserted hidden code ------------------------------------------------//*)
49 \<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)
54 section \<open>===================================================================================\<close>
55 section \<open>===== ============================================================================\<close>
62 section \<open>===================================================================================\<close>
63 section \<open>===== --> src/../lucas-interpreter.sml etc ========================================\<close>
73 \<close> ML \<open> (*\<longrightarrow> pre_conditions.sml | ? model-def.sml ?*)
74 fun max_variants i_model =
77 map (fn (_, variants, _, _, _) => variants) i_model
80 val variants_separated = map (filter_variants' i_model) all_variants
81 val sums_corr = map (cnt_corrects) variants_separated
82 val sum_variant_s = arrange_args sums_corr (1, all_variants)
84 val max_first = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
85 val maxes = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first
87 val option_sequence = map
88 (fn (_, vnt) => if (member (op =) maxes vnt) then SOME vnt else NONE) sum_variant_s
89 (*das ist UNSINN .., siehe (*+*)if (pbl_max_imos*)
90 val max_i_models = map (fn (pos_in_sum_variant_s, i_model) =>
91 if is_some pos_in_sum_variant_s then i_model else [])
92 (option_sequence ~~ variants_separated)
93 |> filter_out (fn place_holder => place_holder = []);
94 (*/-- fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------\ * )
96 val option_sequence = map
97 (fn (_, vnt) => if (member (op =) maxes vnt) then SOME vnt else NONE) sum_variant_s
98 val max_i_models = map (fn (pos_in_sum_variant_s, i_model) =>
99 if is_some pos_in_sum_variant_s then i_model else [])
100 (option_sequence ~~ variants_separated)
101 |> filter_out (fn place_holder => place_holder = []);
103 [(1, [1, 2, 3]), (2, [1, 2, 3]), (3, [1, 2, 3]), (4, [1, 2, 3]), (5, [1, 2])],
104 [(1, [1, 2, 3]), (2, [1, 2, 3]), (3, [1, 2, 3]), (4, [1, 2, 3]), (5, [1, 2])]]
105 ------ ----------------------------------------------------------------------------------------
106 val equal_descr_pairs = map (get_equal_descr (hd max_i_models)) model_patt
107 |> flat (*a hack for continuing ------------^^-- "turn to PIDE", works for test example*)
108 val env_model = make_env_model equal_descr_pairs
109 val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
110 val subst_eval_list = make_envs_preconds equal_givens
111 val (env_subst, env_eval) = split_list subst_eval_list
112 ( *\-- fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------/ *)
114 ((maxes, max_i_models)(*, env_model, (env_subst, env_eval)*))
115 (* (maxes, max_i_models)*)
116 (*/-- fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------\ * )
117 (env_model, (env_subst, env_eval)
118 ( *\--fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------/ *)
121 max_variants: Model_Def.i_model_TEST ->
122 (variant list * Model_Def.i_model_TEST list)(* * Env.T * (env_subst * env_eval)*)
124 \<close> ML \<open> (*\<longrightarrow> pre-conditions.sml*)
126 fun get_dscr' (Cor_TEST ((descr, _), _)) = SOME descr
127 | get_dscr' (Inc_TEST ((descr, _), _)) = SOME descr
128 | get_dscr' (Sup_TEST (descr, _)) = SOME descr
130 (*other feedback cannot contribute to I_Model.mk_env_TEST and Pre_Conds.mk_env_TEST*)
131 (* get_descr: I_Model.single_TEST -> descriptor option*)
133 get_dscr': feedback_TEST -> descriptor option
135 fun get_descr (_, _, _, _, (feedb, _)) =
136 case get_dscr' feedb of NONE => NONE | some_descr => some_descr
137 (* get_equal_descr: I_Model.T_TEST -> Model_Pattern.single ->
138 (Model_Pattern.single * I_Model.single_TEST) list*)
140 get_descr: single_TEST -> descriptor option;
143 (*get an appropriate (description, variant) item from pbl_imod, otherwise return empty item*)
144 fun get_descr_vnt descr vnts i_model =
146 val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr' feedb of NONE => false
147 | SOME descr' => if descr = descr' then true else false) i_model
149 case find_first (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
151 | NONE => (0, [], false, "i_model_empty", (Sup_TEST (descr, []), Position.none))
154 get_descr_vnt: descriptor -> variants -> T_TEST -> single_TEST
156 \<close> ML \<open> (*\<longrightarrow> i-model.sml*)
159 get an appropriate (description, variant) item from o_model;
160 called in case of item in met_imod is_empty_single_TEST
161 (i.e. was not transferred pbl_mod by \<open>fun get_descr_vnt\<close>).
163 fun get_descr_vnt' feedb vnts o_model =
164 find_first (fn (_, vnts', _, descr', _) =>
165 case get_dscr' feedb of
166 SOME descr => if descr' = descr andalso inter op= vnts' vnts <> [] then true else false
167 | NONE => false) o_model
169 get_descr_vnt': feedback_TEST -> variants -> O_Model.T -> O_Model.single option
171 fun msg vnts feedb = "get_descr_vnt' returns NONE: i.e. it does not find an item of o_model with\n" ^
172 "variants " ^ ints2str' vnts ^ " and descriptor " ^
173 (feedb |> get_dscr' |> the |> UnparseC.term (ContextC.for_ERROR ()))
175 msg: variants -> feedback_TEST -> string
177 fun fill_method o_model pbl_imod met_patt =
179 val (pbl_max_vnts, _) = max_variants pbl_imod;
180 val from_pbl = map (fn (_, (descr, _)) => get_descr_vnt descr pbl_max_vnts pbl_imod) met_patt
181 val from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
182 if is_empty_single_TEST i_single
184 case get_descr_vnt' feedb pbl_max_vnts o_model of
185 NONE => raise ERROR (msg pbl_max_vnts feedb)
186 | SOME (i, vnts, m_field, descr, ts) =>
187 (i, vnts, true, m_field, (Cor_TEST ((descr, ts), (TermC.empty, [])), Position.none))
188 else i_single (*fetched before from pbl_imod*))) from_pbl
193 fill_method: O_Model.T -> I_Model.T_TEST -> Model_Pattern.T -> I_Model.T_TEST
195 \<close> ML \<open> (*\<longrightarrow> lucas-interpreter.sml*)
196 fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) =
200 ("ok", Calc.state_empty_post)
203 by_tactic: Tactic.T -> Istate.T * Proof.context -> Calc.T -> string * Calc.state_post
207 (** )ML_file "Minisubpbl/150a-add-given-Maximum.sml" ( ** )check file with test under repair below( **)
208 section \<open>===================================================================================\<close>
209 section \<open>===== Minisubpbl/150a-add-given-Maximum.sml ======================================\<close>
212 (* Title: "Minisubpbl/150a-add-given-Maximum.sml"
213 Author: Walther Neuper 1105
214 (c) copyright due to lincense terms.
216 COMPARE Specify/specify.sml --- specify-phase: low level functions ---
218 ATTENTION: the file creates buffer overflow if copied in one piece !
220 Note: This test --- steps into me --- more than once, to a somewhat extreme extent;
221 in order not to get lost while working in Test_Some etc,
222 re-introduce ML (*--- step into XXXXX ---*) and Co.
223 and use Sidekick for orientation.
224 Nesting is indicated by /--- //-- ///- at the left margin of the comments.
243 val (_(*example text*),
244 (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
245 "Extremum (A = 2 * u * v - u \<up> 2)" ::
246 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
247 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
248 "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" :: (*INCORRECT 2 / v*)
249 (*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)
250 "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
251 "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
252 "ErrorBound (\<epsilon> = (0::real))" :: []),
254 ["univariate_calculus", "Optimisation"],
255 ["Optimisation", "by_univariate_calculus"])))
256 = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
259 val return_init_calc =
260 Test_Code.init_calc @{context} [(model, refs)]; (*val Model_Problem = nxt;*)
261 (*/------------------- step into init_calc -------------------------------------------------\\*)
262 "~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))]) =
263 (@{context}, [(model, refs)]);
264 val thy = thy_id |> ThyC.get_theory ctxt
265 val ((pt, p), tacis) = Step_Specify.initialise' thy (model, refs)
266 val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
268 TESTg_form ctxt (pt,p);
269 "~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p));
271 ME_Misc.pt_extract ctxt ptp;
272 "~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_ as Pbl(*Frm,Pbl*)))) = (ctxt, ptp);
273 val ppobj = Ctree.get_obj I pt p
274 val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p;
275 (*if*) Ctree.is_pblobj ppobj (*then*);
277 "~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}), Pbl_) =
279 val (_, pI, _) = Ctree.get_somespec' spec spec';
280 (* val where_ = if pI = Problem.id_empty then []*)
281 (*if*) pI = Problem.id_empty (*else*);
282 val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
284 Pre_Conds.check ctxt where_rls where_
285 (model, I_Model.OLD_to_TEST probl);
286 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
287 (ctxt, where_rls, where_, (model, I_Model.OLD_to_TEST probl));
288 val (_, _, (env_subst, env_eval)) =
289 of_max_variant model_patt i_model;
290 "~~~~~ fun of_max_variant , args:"; val (_, []) = (model_patt, i_model);
291 (*\------------------- step into init_calc -------------------------------------------------//*)
292 val (p,_,f,nxt,_,pt) = return_init_calc;
294 (*+*)val PblObj {ctxt, probl, ...} = get_obj I pt [];
295 (*+*)Proof_Context.theory_of ctxt (*= {Pure, .., Diff_App}*);
296 (*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term ctxt "r"
299 val return_me_Model_Problem =
300 me nxt p c pt; val Add_Given "Constants [r = 7]" = #4 return_me_Model_Problem;
301 (*/------------------- step into me Model_Problem ------------------------------------------\\*)
302 "~~~~~ fun me , args:"; val (tac, (p:Pos.pos'), (_:Test_Code.NEW), (pt:Ctree.ctree)) = (nxt, p, c, pt);
303 val ctxt = Ctree.get_ctxt pt p
304 val return_by_tactic = case
305 Step.by_tactic tac (pt,p) of
306 ("ok", (_, _, ptp)) => ptp;
308 (*//------------------ step into by_tactic -------------------------------------------------\\*)
309 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
310 val Applicable.Yes tac' = (*case*)
311 Step.check tac (pt, p) (*of*);
312 (*+*)val Model_Problem' _ = tac';
313 "~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
314 (*if*) Tactic.for_specify tac (*then*);
316 Specify_Step.check tac (ctree, pos);
317 "~~~~~ fun check , args:"; val (Tactic.Model_Problem, (pt, pos as (p, _))) =
319 val (o_model, pI', ctxt) = case Ctree.get_obj I pt p of
320 Ctree.PblObj {origin = (o_model, (_, pI', _), _), ctxt, ...} => (o_model, pI', ctxt)
321 val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
322 val pbl = I_Model.init_TEST o_model model_patt;
325 Applicable.Yes (Tactic.Model_Problem' (pI', I_Model.TEST_to_OLD pbl, []));
326 (*\\------------------ step into by_tactic -------------------------------------------------//*)
327 val (pt, p) = return_by_tactic;
329 val return_do_next = (*case*)
330 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
331 (*//------------------ step into do_next ---------------------------------------------------\\*)
332 "~~~~~ fun do_next , args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) =
333 (p, ((pt, e_pos'),[]));
334 val pIopt = get_pblID (pt,ip);
335 (*if*) ip = ([],Res); (* = false*)
336 val _ = (*case*) tacis (*of*);
337 val SOME _ = (*case*) pIopt (*of*);
339 val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
340 Step.switch_specify_solve p_ (pt, ip);
341 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
342 (*if*) Pos.on_specification ([], state_pos) (*then*);
344 val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
345 Step.specify_do_next (pt, input_pos);
346 (*///----------------- step into specify_do_next -------------------------------------------\\*)
347 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
349 (* val (_, (p_', tac)) =*)
350 val return_find_next_step = (*keep for continuing specify_do_next*)
351 Specify.find_next_step ptp;
352 (*////---------------- step into find_next_step --------------------------------------------\\*)
353 "~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
354 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
355 spec = refs, ...} = Calc.specify_data (pt, pos);
356 val ctxt = Ctree.get_ctxt pt pos;
357 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
358 (*if*) p_ = Pos.Pbl (*then*);
360 Specify.for_problem ctxt oris (o_refs, refs) (pbl, met);
361 (*/////--------------- step into for_problem -----------------------------------------------\\*)
362 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
363 = (ctxt, oris, (o_refs, refs), (pbl, met));
364 val cdI = if dI = ThyC.id_empty then dI' else dI;
365 val cpI = if pI = Problem.id_empty then pI' else pI;
366 val cmI = if mI = MethodC.id_empty then mI' else mI;
367 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
368 val {model = mpc, ...} = MethodC.from_store ctxt cmI;
370 val return_check_OLD =
371 check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
372 (*//////-------------- step into check -------------------------------------------------\\*)
373 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
374 (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
375 val return_of_max_variant =
376 of_max_variant model_patt i_model;
377 (*///// //------------ step into of_max_variant --------------------------------------------\\*)
378 "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) =
379 (model_patt, i_model);
381 (*+*)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))]"
382 = i_model |> I_Model.to_string_TEST @{context}
384 map (fn (_, variants, _, _, _) => variants) i_model
387 val variants_separated = map (filter_variants' i_model) all_variants
388 val sums_corr = map (cnt_corrects) variants_separated
389 val sum_variant_s = arrange_args sums_corr (1, all_variants)
390 (*+*)val [(0, 1), (0, 2), (0, 3)] = sum_variant_s
391 val (_, max_variant) = hd (*..crude decision, up to improvement *)
392 (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
394 filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
395 val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
396 (*for building make_env_s -------------------------------------------------------------------\*)
397 (*!!!*) val ("#Given", (descr, term), pos) =
398 Model_Pattern.split_descriptor ctxt ("#Given", @{term "Constants [r = (7::real)]"}, Position.none)
399 (*!!!*) val patt = equal_descr_pairs |> hd |> #1
400 (*!!!*)val equal_descr_pairs =
402 (1, [1, 2, 3], true, "#Given", (Cor_TEST ((descr, (*!*)TermC.isalist2list(*!*) term),
403 (TermC.empty, [])), pos)))
404 :: tl equal_descr_pairs
405 (*for building make_env_s -------------------------------------------------------------------/*)
407 val env_model = make_env_model equal_descr_pairs;
408 (*///// ///----------- step into make_env_model --------------------------------------------\\*)
409 "~~~~~ fun make_env_model , args:"; val (equal_descr_pairs) = (equal_descr_pairs);
411 val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
412 => (mk_env_model id feedb));
413 val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 4 equal_descr_pairs;
414 (*\\\\\ \\\----------- step into make_env_model --------------------------------------------//*)
415 (*||||| ||------------ contine of_max_variant ------------------------------------------------*)
417 val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
418 val subst_eval_list = make_envs_preconds equal_givens
419 val return_make_envs_preconds =
420 make_envs_preconds equal_givens;
421 (*///// ///----------- step into make_envs_preconds ----------------------------------------\\*)
422 "~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
423 val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb)
425 xxx: (Model_Pattern.single * I_Model.single_TEST) -> ((term * term) * (term * term)) list;
426 val return_discern_feedback =
427 discern_feedback id feedb;
428 (*nth 1 equal_descr_pairs* )
429 "~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) = (id, feedb);
430 ( *nth 2 equal_descr_pairs*)
431 "~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Inc_TEST ((descr, ts), _))) = (id, feedb);
433 (*nth 1 equal_descr_pairs* )
434 (*+*)val [((Const ("fixes", typ1), Free ("r", typ2)),
435 (Free ("r", typ3), value))] = return_discern_feedback
436 (*+*)val true = typ1 = typ2
437 (*+*)val true = typ3 = HOLogic.realT
438 (*+*)val "7" = UnparseC.term @{context} value
439 ( *nth 2 equal_descr_pairs*)
440 (*+*)val [] = return_discern_feedback
442 val return_discern_typ =
443 discern_typ id (descr, ts);
444 "~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts));
445 (*nth 1 equal_descr_pairs* )
446 (*+*)val [((Const ("fixes", typ1), Free ("r", typ2)),
447 (Free ("r", typ3), value))] = return_discern_typ
448 (*+*)val true = typ1 = typ2
449 (*+*)val true = typ3 = HOLogic.realT
450 (*+*)val "7" = UnparseC.term @{context} value
451 ( *nth 2 equal_descr_pairs*)
452 (*+*)val [] = return_discern_typ;
455 "~~~~~ fun switch_type , args:"; val (Const (descr_string, _), ts) = (descr, ts);
457 (*nth 1 equal_descr_pairs* )
458 val return_switch_type_TEST = Const (descr_string, ts |> hd |> TermC.lhs |> type_of)
460 (*+*)val Const ("Input_Descript.Constants", typ) = return_switch_type_TEST
461 (*+*)val Type ("Real.real", []) = typ
462 ( *nth 2 equal_descr_pairs*)
463 (*+*)val return_switch_type_TEST = descr
465 (*\\\\\ \\\----------- step into make_envs_preconds ----------------------------------------//*)
467 (*||||| ||------------ contine of_max_variant ------------------------------------------------*)
468 val subst_eval_list = make_envs_preconds equal_givens
469 val (env_subst, env_eval) = split_list subst_eval_list
471 val return_of_max_variant = ((length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model_max)
472 = length model_patt, max_variant, i_model_max),
473 env_model, (env_subst, env_eval));
474 return_of_max_variant: (bool * variant * T_TEST) * Env.T * (env_subst * env_eval);
475 (*\\\\\ \\------------ step into of_max_variant --------------------------------------------//*)
476 val (i_model_max, env_model, (env_subst, env_eval)) = return_of_max_variant
477 (*!!!/----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---\*)
478 val (i_max_variant, env_model, (env_subst, env_eval)) = (i_model_max, [], ([], []))
479 (*!!!\----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---/*)
480 (*||||||-------------- contine check -----------------------------------------------------*)
481 val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
482 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
483 val full_subst = if env_eval = [] then pres_subst_other
484 else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
485 val evals = map (eval ctxt where_rls) full_subst
486 val return_ = (i_model_max, env_subst, env_eval)
487 (*\\\\\\\------------- step into check -------------------------------------------------//*)
488 val (preok, _) = return_check_OLD;
490 (*|||||--------------- contine for_problem ---------------------------------------------------*)
491 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
492 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
494 (*case*) find_first (I_Model.is_error o #5) pbl (*of*);
497 Specify.item_to_add (ThyC.get_theory ctxt
498 (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
499 "~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
500 = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, pbt, pbl);
501 fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
502 | false_and_not_Sup (_, _, false, _, _) = true
503 | false_and_not_Sup _ = false
505 val v = if itms = [] then 1 else Pre_Conds.max_variant itms
506 val vors = if v = 0 then oris
507 else filter ((fn variant =>
508 fn (_, variants, m_field, _, _) => member op= variants variant andalso m_field <> "#undef")
511 (*+*)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]\"])]"
512 (*+*) = vors |> O_Model.to_string @{context}
514 val vits = if v = 0 then itms (* because of dsc without dat *)
515 else filter ((fn variant =>
516 fn (_, variants, _, _, _) => member op= variants variant)
517 v) itms; (* itms..vat *)
519 val icl = filter false_and_not_Sup vits; (* incomplete *)
521 (*if*) icl = [] (*else*);
522 (*+*)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)]"
523 = icl |> I_Model.to_string @{context}
524 (*+*)val "(1 ,[1, 2, 3] ,false ,#Given ,Inc Constants [] , pen2str)"
525 = hd icl |> I_Model.single_to_string @{context}
527 (*++*)val feedback = (fn (_, _, _, _, feedback) => feedback) (hd icl)
528 (*++*)val Const ("Input_Descript.Constants", _) = I_Model.descriptor feedback
529 (*++*)val [] = I_Model.o_model_values feedback
531 (*+*)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]\"])]"
532 (*+*) = vors |> O_Model.to_string @{context}
535 (*case*) find_first ((fn (_, _, _, _, feedback) => fn (_, _, _, d, ts) =>
536 d = I_Model.descriptor feedback andalso subset op = (I_Model.o_model_values feedback, ts))
537 (hd icl)) vors (*of*);
539 (*+*)val "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"])" =
540 (*+*) ori |> O_Model.single_to_string @{context}
541 (*\\\\\--------------- step into for_problem -----------------------------------------------//*)
542 (*\\\\---------------- step into find_next_step --------------------------------------------//*)
543 (*|||----------------- continuing specify_do_next --------------------------------------------*)
544 val (_, (p_', tac)) = return_find_next_step (*kept for continuing specify_do_next*)
546 val ist_ctxt = Ctree.get_loc pt (p, p_)
547 (*+*)val Add_Given "Constants [r = 7]" = tac
551 Step_Specify.by_tactic_input tac (pt, (p, p_'));
552 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =
553 (tac, (pt, (p, p_')));
555 Specify.by_Add_ "#Given" ct ptp;
556 "~~~~~ fun by_Add_ , args:"; val (m_field, ct ,(pt, pos as (_, p_))) =
558 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
559 val (i_model, m_patt) =
562 (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
565 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model);
568 I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
569 "~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, (str(*, pos*))) =
570 (ctxt, m_field, oris, i_model, m_patt, ct);
571 val (t as (descriptor $ _)) = Syntax.read_term ctxt str
573 (*+*)val "Constants [r = 7]" = UnparseC.term @{context} t;
576 (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
577 (*if*) m_field <> m_field' (*else*);
579 (*+*)val "#Given" = m_field; val "#Given" = m_field'
581 val ("", ori', all) =
582 (*case*) O_Model.contains ctxt m_field o_model t (*of*);
584 (*+*)val (_, _, _, _, vals) = hd o_model;
585 (*+*)val "Constants [r = 7]" = UnparseC.term @{context} (@{term Constants} $ (hd vals));
586 (*+*)if "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), " ^
587 (*+*) "\n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), " ^
588 (*+*) "\n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), " ^
589 (*+*) "\n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), " ^
590 (*+*) "\n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), " ^
591 (*+*) "\n(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), " ^
592 (*+*) "\n(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), " ^
593 (*+*) "\n(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), " ^
594 (*+*) "\n(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), " ^
595 (*+*) "\n(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), " ^
596 (*+*) "\n(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
597 (*+*)= O_Model.to_string @{context} o_model then () else error "o_model CHANGED";
599 (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*);
600 "~~~~~ fun is_notyet_input , args:"; val (ctxt, itms, all, (i, v, f, d, ts), pbt) =
601 (ctxt, i_model, all, ori', m_patt);
602 val SOME (_, (_, pid)) =
603 (*case*) find_first (eq1 d) pbt (*of*);
604 (*local*)fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (I_Model.descriptor itm_);(*local*)
605 val SOME (_, _, _, _, itm_) =
606 (*case*) find_first (eq3 f d) itms (*of*);
607 val ts' = inter op = (o_model_values itm_) ts;
608 (*if*) subset op = (ts, ts') (*else*);
609 val return_is_notyet_input = ("",
610 ori_2itm itm_ pid all (i, v, f, d, subtract op = ts' ts));
611 "~~~~~ fun ori_2itm , args:"; val (itm_, pid, all, (id, vt, fd, d, ts)) =
612 (itm_, pid, all, (i, v, f, d, subtract op = ts' ts));
613 val ts' = union op = (o_model_values itm_) ts;
614 val pval = [Input_Descript.join'''' (d, ts')]
615 val complete = if eq_set op = (ts', all) then true else false
617 (*+*)val "Inc Constants [] , pen2str" = itm_ |> I_Model.feedback_to_string @{context}
618 (*\\\----------------- step into specify_do_next -------------------------------------------//*)
619 (*\\------------------ step into do_next ---------------------------------------------------//*)
620 val ("ok", (ts as (_, _, _) :: _, _, (pt, p))) = return_do_next
622 (*|------------------- continue with me_Model_Problem ----------------------------------------*)
624 val tacis as (_::_) =
626 val (tac, _, _) = last_elem tacis
628 val return_Model_Problem = (p, [] : NEW, TESTg_form ctxt (pt, p), tac, Celem.Sundef, pt);
629 (*//------------------ step into TESTg_form ------------------------------------------------\\*)
630 "~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt, p));
633 ME_Misc.pt_extract ctxt ptp;
634 "~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_(*Frm,Pbl*)))) = (ctxt, ptp);
635 val ppobj = Ctree.get_obj I pt p
636 val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p;
637 (*if*) Ctree.is_pblobj ppobj (*then*);
640 "~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}),
641 Pbl(*Frm,Pbl*)) = (ppobj, p_);
642 val (_, pI, _) = Ctree.get_somespec' spec spec';
643 (*if*) pI = Problem.id_empty (*else*);
644 (* val where_ = if pI = Problem.id_empty then []*)
647 val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
648 val (_, where_) = (*Pre_Conds.*)check ctxt where_rls where_ (model, I_Model.OLD_to_TEST probl)
650 val allcorrect = I_Model.is_complete probl andalso foldl and_ (true, (map #1 where_))
651 val return_pt_model = Ctree.ModSpec (allcorrect, Pos.Pbl, hdl, probl, where_, spec)
653 (*|------------------- continue with TESTg_form ----------------------------------------------*)
654 val Ctree.ModSpec (spec as (_, p_, _, gfr, where_, _)) =
655 (*case*) form (*of*);
656 Test_Out.PpcKF ( (Test_Out.Problem [],
657 P_Model.from (Proof_Context.theory_of ctxt) gfr where_));
659 P_Model.from (Proof_Context.theory_of ctxt) gfr where_;
660 "~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);
661 fun coll model [] = model
662 | coll model ((_, _, _, field, itm_) :: itms) =
663 coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
665 val gfr = coll P_Model.empty itms;
666 "~~~~~ fun coll , args:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: itms))
667 = (P_Model.empty, itms);
669 (*+*)val 4 = length itms;
670 (*+*)val itm = nth 1 itms;
672 coll P_Model.empty [itm];
673 "~~~~~ fun coll , iterate:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: []))
674 = (P_Model.empty, [itm]);
676 (add_sel_ppc thy field model (item_from_feedback thy itm_));
677 "~~~~~ fun add_sel_ppc , args:"; val ((_: theory), sel, {Given = gi, Where = wh, Find = fi, With = wi, Relate = re}, x )
678 = (thy, field, model, (item_from_feedback thy itm_));
680 P_Model.item_from_feedback thy itm_;
681 "~~~~~ fun item_from_feedback , args:"; val (thy, (I_Model.Inc ((d, ts), _))) = (thy, itm_);
682 P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)));
683 (*\\------------------ step into TESTg_form ------------------------------------------------//*)
684 (*\------------------- step into me Model_Problem ------------------------------------------//*)
685 val (p, _, f, nxt, _, pt) = return_me_Model_Problem
687 (*-------------------- contine me's ----------------------------------------------------------*)
688 val return_me_add_find_Constants = me nxt p c pt;
689 val Add_Find "Maximum A" = #4 return_me_add_find_Constants;
690 (*/------------------- step into me_add_find_Constants -------------------------------------\\*)
691 "~~~~~ fun me , args:"; val (tac as Add_Given "Constants [r = 7]", p, _(*NEW remove*), pt) =
693 val ctxt = Ctree.get_ctxt pt p
694 (*+*)val PblObj {probl = (1, [1, 2, 3], false, "#Given", Inc
695 ((Const ("Input_Descript.Constants", _), []), _)) :: _, ...} = get_obj I pt (fst p)
696 (*-------------------------------------------^^--*)
697 val return_step_by_tactic = (*case*)
698 Step.by_tactic tac (pt, p) (*of*);
699 (*//------------------ step into Step.by_tactic --------------------------------------------\\*)
700 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
701 val Applicable.Yes tac' =
702 (*case*) Specify_Step.check tac (pt, p) (*of*);
703 (*if*) Tactic.for_specify' tac' (*then*);
704 Step_Specify.by_tactic tac' ptp;
705 "~~~~~ fun by_tactic , args:"; val ((Tactic.Add_Given' (ct, _)), (pt, p)) = (tac', ptp);
707 Specify.by_Add_ "#Given" ct (pt, p);
708 "~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, (pt, p));
709 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
710 (* val (i_model, m_patt) =*)
711 (*if*) p_ = Pos.Met (*else*);
714 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)
715 val I_Model.Add i_single =
716 (*case*) I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
719 I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model;
720 "~~~~~ fun add_single , args:"; val (thy, itm, model) =
721 ((Proof_Context.theory_of ctxt), i_single, i_model);
722 fun eq_untouched d (0, _, _, _, itm_) = (d = I_Model.descriptor itm_)
723 | eq_untouched _ _ = false
724 val model' = case I_Model.seek_ppc (#1 itm) model of
725 SOME _ => overwrite_ppc thy itm model (*itm updated in is_notyet_input WN.11.03*)
727 (*||------------------ contine Step.by_tactic ------------------------------------------------*)
728 (*\\------------------ step into Step.by_tactic --------------------------------------------//*)
729 val ("ok", (_, _, ptp)) = return_step_by_tactic;
733 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
734 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
735 (p, ((pt, Pos.e_pos'), []));
736 (*if*) Pos.on_calc_end ip (*else*);
737 val (_, probl_id, _) = Calc.references (pt, p);
739 (*case*) tacis (*of*);
740 (*if*) probl_id = Problem.id_empty (*else*);
742 switch_specify_solve p_ (pt, ip);
743 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
744 (*if*) Pos.on_specification ([], state_pos) (*then*);
746 specify_do_next (pt, input_pos);
747 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
748 val (_, (p_', tac)) =
749 Specify.find_next_step ptp;
750 "~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
751 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
752 spec = refs, ...} = Calc.specify_data (pt, pos);
753 val ctxt = Ctree.get_ctxt pt pos;
755 (*+*)val (1, [1, 2, 3], true, "#Given", Cor ((Const ("Input_Descript.Constants", _), ts ), _)) :: _
757 (*+*)val "[[r = 7]]" = UnparseC.terms @{context} ts;
758 (*-----ML-^------^-HOL*)
760 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
761 (*if*) p_ = Pos.Pbl (*then*);
763 for_problem ctxt oris (o_refs, refs) (pbl, met);
764 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
765 (ctxt, oris, (o_refs, refs), (pbl, met));
766 val cpI = if pI = Problem.id_empty then pI' else pI;
767 val cmI = if mI = MethodC.id_empty then mI' else mI;
768 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
769 val {model = mpc, ...} = MethodC.from_store ctxt cmI
772 Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
773 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
774 (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
776 val (_, _, (env_subst, env_eval)) = of_max_variant model_patt i_model;
777 "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
779 map (fn (_, variants, _, _, _) => variants) i_model
782 val variants_separated = map (filter_variants' i_model) all_variants
783 val sums_corr = map (cnt_corrects) variants_separated
784 val sum_variant_s = arrange_args sums_corr (1, all_variants)
785 val (_, max_variant) = hd (*..crude decision, up to improvement *)
786 (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
788 filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
789 val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
790 val env_model = make_env_model equal_descr_pairs
791 val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
793 val subst_eval_list =
794 make_envs_preconds equal_givens;
795 "~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
796 val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) =>
797 discern_feedback id feedb)
798 val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 1 equal_givens;
799 "~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) = (id, feedb);
801 discern_typ id (descr, ts);
802 "~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts));
803 (*|------------------- contine me_add_find_Constants -----------------------------------------*)
804 (*\------------------- step into me_add_find_Constants -------------------------------------//*)
805 val (p,_,f,nxt,_,pt) = return_me_add_find_Constants;
806 (*/########################## before destroying elementwise input of lists ##################\* )
807 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u]" = nxt;
808 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [v]" = nxt;
809 ( *\########################## before destroying elementwise input of lists ##################/*)
810 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u, v]" = nxt;
812 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)" = nxt;
813 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;
814 val return_me_Add_Relation_SideConditions
816 (*+*)val (_, _, _, Specify_Theory "Diff_App", _, _) = return_me_Add_Relation_SideConditions; (*###############*)
817 (*/------------------- step into me Add_Relation_SideConditions ----------------------------\\*)
818 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
819 val ctxt = Ctree.get_ctxt pt p;
820 (**) val (pt, p) = (**)
821 (**)case(**) Step.by_tactic tac (pt, p) (**)of(**)
822 (**) ("ok", (_, _, ptp)) => ptp (**) ;
825 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
826 (*//------------------ step into do_next ---------------------------------------------------\\*)
827 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
828 = (p, ((pt, Pos.e_pos'), [])) (*of*);
829 (*if*) Pos.on_calc_end ip (*else*);
830 val (_, probl_id, _) = Calc.references (pt, p);
831 (*case*) tacis (*of*);
832 (*if*) probl_id = Problem.id_empty (*else*);
834 Step.switch_specify_solve p_ (pt, ip);
835 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
836 (*if*) Pos.on_specification ([], state_pos) (*then*);
837 Step.specify_do_next (pt, input_pos);
838 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
839 (*isa------ERROR: Refine_Problem INSTEAD
840 isa2: Specify_Theory "Diff_App"*)
841 val (_, (p_', tac as Specify_Theory "Diff_App")) =
842 (*ERROR------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
843 Specify.find_next_step ptp;
844 "~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
845 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
846 spec = refs, ...} = Calc.specify_data (pt, pos);
847 val ctxt = Ctree.get_ctxt pt pos;
848 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
849 (*if*) p_ = Pos.Pbl (*then*);
851 val ("dummy", (Pbl, tac as Specify_Theory "Diff_App")) =
852 (*ERROR------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
853 for_problem ctxt oris (o_refs, refs) (pbl, met);
854 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
855 (ctxt, oris, (o_refs, refs), (pbl, met));
856 val cpI = if pI = Problem.id_empty then pI' else pI;
857 val cmI = if mI = MethodC.id_empty then mI' else mI;
858 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
859 val {model = mpc, ...} = MethodC.from_store ctxt cmI
861 (*+*)val [Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
862 Free ("fixes", _)] = where_
865 Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
866 (*///----------------- step into check -------------------------------------------------\\*)
867 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
868 (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
869 (*+*)val "[0 < fixes]" = pres |> UnparseC.terms @{context}
870 (*+*)val "[\"(#Given, (Constants, fixes))\", \"(#Find, (Maximum, maxx))\", \"(#Find, (AdditionalValues, vals))\", \"(#Relate, (Extremum, extr))\", \"(#Relate, (SideConditions, sideconds))\"]"
871 (*+*) = model_patt |> Model_Pattern.to_string @{context}
872 (*+*)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))]"
873 = i_model |> I_Model.to_string_TEST @{context}
875 val return_of_max_variant as (_, _, (env_subst, env_eval)) =
876 of_max_variant model_patt i_model
878 (*+*)val [(Free ("fixes", T1), Free ("r", T2))] = env_subst (*?!? Const*)
879 (*+*)val Type ("Real.real", []) = T1
880 (*+*)val Type ("Real.real", []) = T2
882 (*+*)val [(Free ("r", T2), Const ("Num.numeral_class.numeral", _) $ _)] = env_eval
883 (*+*)val Type ("Real.real", []) = T2
885 val (_, _, (env_subst, env_eval)) = return_of_max_variant;
886 (*|||----------------- contine check -----------------------------------------------------*)
887 val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
889 (*|||----------------- contine check -----------------------------------------------------*)
890 (*+*)val [(true, Const ("Orderings.ord_class.less", _) $
891 Const ("Groups.zero_class.zero", _) $ Free ("r", _))] = pres_subst
893 val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
895 Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
896 (Const ("Num.numeral_class.numeral", _) $ _))] = full_subst
898 val evals = map (eval ctxt where_rls) full_subst
899 val return_check_OLD = (foldl and_ (true, map fst evals), pres_subst)
900 (*\\\----------------- step into check -------------------------------------------------\\*)
902 val (preok as true, _) = return_check_OLD
903 (*+---------------^^^^*)
904 (*\\------------------ step into do_next ---------------------------------------------------\\*)
905 (*\------------------- step into me_Add_Relation_SideConditions ----------------------------//*)
906 val (p, _, f, nxt, _, pt) = return_me_Add_Relation_SideConditions
907 val Specify_Theory "Diff_App" = nxt;
909 val return_me_Specify_Theory
910 = me nxt p c pt; val Specify_Problem ["univariate_calculus", "Optimisation"] = #4 return_me_Specify_Theory;
911 (*/------------------- step into me Specify_Theory -----------------------------------------\\*)
912 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
913 val ctxt = Ctree.get_ctxt pt p;
915 (*case*) Step.by_tactic tac (pt, p) (*of*);
916 (* ("ok", (_, _, ptp)) => ptp *)
917 val return_Step_by_tactic =
918 Step.by_tactic tac (pt, p);
919 (*//------------------ step into Step_by_tactic --------------------------------------------\\*)
920 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
921 (*case*) Specify_Step.check tac (pt, p) (*of*);
923 (*||------------------ contine Step_by_tactic ------------------------------------------------*)
924 (*\\------------------ step into Step_by_tactic --------------------------------------------//*)
926 val ("ok", (_, _, ptp)) = return_Step_by_tactic;
927 (*|------------------- continue me Specify_Theory --------------------------------------------*)
929 val ("ok", (ts as (_, _, _) :: _, _, _)) =
931 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
932 (*//------------------ step into do_next ---------------------------------------------------\\*)
933 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
934 = (p, ((pt, Pos.e_pos'), [])) (*of*);
935 (*if*) Pos.on_calc_end ip (*else*);
936 val (_, probl_id, _) = Calc.references (pt, p);
938 (*case*) tacis (*of*);
939 (*if*) probl_id = Problem.id_empty (*else*);
941 Step.switch_specify_solve p_ (pt, ip);
942 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
943 (*if*) Pos.on_specification ([], state_pos) (*then*);
945 Step.specify_do_next (pt, input_pos);
946 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
947 val (_, (p_', tac)) = Specify.find_next_step ptp
948 val ist_ctxt = Ctree.get_loc pt (p, p_);
951 Step_Specify.by_tactic_input tac (pt, (p, p_'));
952 (*+*)val Specify_Theory "Diff_App" = tac;
953 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Theory dI), (pt, pos as (_, Pbl)))
954 = (tac, (pt, (p, p_')));
955 val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
956 PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
957 (oris, dI, dI', pI', probl, ctxt)
958 val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');
959 val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
960 (*\\------------------ step into do_next ---------------------------------------------------//*)
961 (*\------------------- step into me Specify_Theory -----------------------------------------//*)
962 val (p,_,f,nxt,_,pt) = return_me_Specify_Theory;
964 val return_me_Specify_Problem (* keep for continuing me *)
965 = me nxt p c pt; val Specify_Method ["Optimisation", "by_univariate_calculus"] = #4 return_me_Specify_Problem;
966 (*/------------------- step into me Specify_Problem ----------------------------------------\\*)
967 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
968 val ctxt = Ctree.get_ctxt pt p
970 (** ) val ("ok", (_, _, ptp as (pt, p))) =( **)
971 (**) val return_by_tactic =(**) (*case*)
972 Step.by_tactic tac (pt, p) (*of*);
973 (*//------------------ step into by_tactic -------------------------------------------------\\*)
974 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
977 Step.check tac (pt, p) (*of*);
978 "~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
979 (*if*) Tactic.for_specify tac (*then*);
981 Specify_Step.check tac (ctree, pos);
982 "~~~~~ fun check , args:"; val ((Tactic.Specify_Problem pID), (pt, pos as (p, _)))
983 = (tac, (ctree, pos));
984 val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of
985 Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
986 => (oris, dI, pI, dI', pI', itms)
987 val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');
988 (*\\------------------ step into by_tactic -------------------------------------------------//*)
989 val ("ok", (_, _, ptp as (pt, p))) = return_by_tactic (* kept for continuing me *);
992 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
993 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
994 (*if*) Pos.on_calc_end ip (*else*);
995 val (_, probl_id, _) = Calc.references (pt, p);
997 (*case*) tacis (*of*);
998 (*if*) probl_id = Problem.id_empty (*else*);
1000 Step.switch_specify_solve p_ (pt, ip);
1001 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
1002 (*if*) Pos.on_specification ([], state_pos) (*then*);
1004 Step.specify_do_next (pt, input_pos);
1005 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
1006 val (_, (p_', tac)) = Specify.find_next_step ptp
1007 val ist_ctxt = Ctree.get_loc pt (p, p_)
1009 (*case*) tac (*of*);
1011 Step_Specify.by_tactic_input tac (pt, (p, p_'));
1012 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos))
1013 = (tac, (pt, (p, p_')));
1015 val (o_model, ctxt, i_model) =
1016 Specify_Step.complete_for id (pt, pos);
1017 "~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));
1018 val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
1019 ...} = Calc.specify_data (ctree, pos);
1020 val ctxt = Ctree.get_ctxt ctree pos
1021 val (dI, _, _) = References.select_input o_refs refs;
1022 val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
1023 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
1024 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
1025 val thy = ThyC.get_theory ctxt dI
1026 val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
1027 (*\------------------- step into me Specify_Problem ----------------------------------------//*)
1028 val (p,_,f,nxt,_,pt) = return_me_Specify_Problem
1030 val return_me_Add_Given_FunctionVariable
1031 = me nxt p c pt; val Add_Given "FunctionVariable a" = #4 return_me_Add_Given_FunctionVariable;
1032 (*/------------------- step into me Specify_Method -----------------------------------------\\*)
1033 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
1034 val ctxt = Ctree.get_ctxt pt p
1036 (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
1037 case Step.by_tactic tac (pt, p) of
1038 ("ok", (_, _, ptp)) => ptp;
1041 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
1042 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
1043 (*if*) Pos.on_calc_end ip (*else*);
1044 val (_, probl_id, _) = Calc.references (pt, p);
1046 (*case*) tacis (*of*);
1047 (*if*) probl_id = Problem.id_empty (*else*);
1049 Step.switch_specify_solve p_ (pt, ip);
1050 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
1051 (*if*) Pos.on_specification ([], state_pos) (*then*);
1053 Step.specify_do_next (pt, input_pos);
1054 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
1056 val (_, (p_', tac)) =
1057 Specify.find_next_step ptp;
1058 "~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
1059 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
1060 spec = refs, ...} = Calc.specify_data (pt, pos);
1061 val ctxt = Ctree.get_ctxt pt pos;
1062 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
1063 (*if*) p_ = Pos.Pbl (*else*);
1065 Specify.for_method ctxt oris (o_refs, refs) (pbl, met);
1066 "~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (_, met))
1067 = (ctxt, oris, (o_refs, refs), (pbl, met));
1068 val cmI = if mI = MethodC.id_empty then mI' else mI;
1069 val {model, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
1070 val (preok, _) = Pre_Conds.check ctxt where_rls where_ (model, I_Model.OLD_to_TEST met);
1072 (*case*) find_first (I_Model.is_error o #5) met (*of*);
1075 Specify.item_to_add (ThyC.get_theory ctxt
1076 (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
1077 "~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
1078 = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
1079 (*\------------------- step into me Specify_Method -----------------------------------------//*)
1080 val (p,_,f,nxt,_,pt) = return_me_Add_Given_FunctionVariable
1082 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Input_Descript.Domain {0<..<r}" = nxt;
1083 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "ErrorBound (\<epsilon> = 0)" = nxt;
1085 (* ------------------- step into UNTIL A PROGRAM IS REQUIRED (not yet impl. ---------------- )*)
1086 \<close> ML \<open>(*/------------- step into me_Add_Given_ErrorBound------------------------------------\\*)
1087 (*/------------------- step into me_Add_Given_ErrorBound------------------------------------\\*)
1088 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
1089 val ctxt = Ctree.get_ctxt pt p
1091 (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
1092 case Step.by_tactic tac (pt, p) of
1093 ("ok", (_, _, ptp)) => ptp;
1094 (*ERROR due to missing program in creating the environment from formal args* )
1096 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
1098 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis) ) =
1099 (p, ((pt, Pos.e_pos'), []));
1100 (*if*) Pos.on_calc_end ip (*else*);
1101 val (_, probl_id, _) = Calc.references (pt, p);
1103 (*case*) tacis (*of*);
1104 (*if*) probl_id = Problem.id_empty (*else*);
1106 (*ERROR due to missing program in creating the environment from formal args* )
1107 switch_specify_solve p_ (pt, ip);
1109 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
1110 (*if*) Pos.on_specification ([], state_pos) (*then*);
1112 (*ERROR due to missing program in creating the environment from formal args* )
1113 specify_do_next (pt, input_pos)
1115 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
1116 val (_, (p_', tac as Apply_Method ["Optimisation", "by_univariate_calculus"])) =
1117 (*-------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ not yet impl.*)
1118 Specify.find_next_step ptp
1119 val ist_ctxt = Ctree.get_loc pt (p, p_)
1121 val Tactic.Apply_Method (mI as ["Optimisation", "by_univariate_calculus"]) =
1122 (*case*) tac (*of*);
1123 (*ERROR due to missing program in creating the environment from formal args* )
1124 LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
1125 ist_ctxt (pt, (p, p_'))
1127 \<close> ML \<open> (*//----------- step into by_tactic -------------------------------------------------\\*)
1128 (*//------------------ step into by_tactic -------------------------------------------------\\*)
1129 "~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
1130 ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));
1131 (*new*)val (itms, oris, pI, probl) = case get_obj I pt p of
1132 (*new*) PblObj {meth = itms, origin = (oris, (_, pI, _), _), probl, ...} => (itms, oris, pI, probl)
1133 | _ => raise ERROR ""
1135 (*new*)val {model = pbl_patt, ...} = Problem.from_store ctxt pI;
1136 (*new*)val {model = met_patt, ...} = MethodC.from_store ctxt mI;
1137 (*if*) itms <> [] (*then*);
1138 \<close> text \<open>(*old*)
1140 I_Model.complete oris probl [] met_patt;
1141 \<close> ML \<open>(*new*)
1143 (*I_Model.*)fill_method oris (I_Model.OLD_to_TEST probl) met_patt;
1145 val return_fill_method = fill_method oris (I_Model.OLD_to_TEST probl) met_patt;
1146 \<close> ML \<open> (*///---------- step into fill_method -----------------------------------------------\\*)
1147 (*///----------------- step into fill_method -----------------------------------------------\\*)
1148 "~~~~~ fun fill_method , args:"; val (o_model, pbl_imod, met_patt) =
1149 (oris, I_Model.OLD_to_TEST probl, met_patt);
1151 (*+*)if (o_model |> O_Model.to_string @{context}) = "[\n" ^
1152 "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n" ^
1153 "(2, [\"1\", \"2\", \"3\"], #Given, Maximum, [\"A\"]), \n" ^
1154 "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n" ^
1155 "(4, [\"1\", \"2\", \"3\"], #Given, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n" ^
1156 "(5, [\"1\", \"2\"], #Given, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n" ^
1157 (*ERROR----------------------------------------------------------^^^^^*)
1158 "(6, [\"3\"], #Given, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n" ^
1159 "(7, [\"1\"], #Given, FunctionVariable, [\"a\"]), \n" ^
1160 "(8, [\"2\"], #Given, FunctionVariable, [\"b\"]), \n" ^
1161 "(9, [\"3\"], #Given, FunctionVariable, [\"\<alpha>\"]), \n" ^
1162 "(10, [\"1\", \"2\"], #Given, Input_Descript.Domain, [\"{0<..<r}\"]), \n" ^
1163 "(11, [\"3\"], #Given, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n" ^
1164 "(12, [\"1\", \"2\", \"3\"], #Given, ErrorBound, [\"\<epsilon> = 0\"])]"
1165 then () else error "complete_TEST: init. o_model CHANGED"
1167 (*+*)if (pbl_imod |> I_Model.to_string_TEST @{context}) = "[\n" ^
1168 "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
1169 "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
1170 "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
1171 "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
1172 "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
1173 (*ERROR----------------------------------------------------------------^^^^^*)
1174 then () else error "complete_TEST: init. pbl_imod CHANGED";
1176 (*+*)if (met_patt |> Model_Pattern.to_string @{context}) = "[\"" ^
1177 "(#Given, (Constants, fixes))\", \"" ^
1178 "(#Given, (Maximum, maxx))\", \"" ^
1179 "(#Given, (Extremum, extr))\", \"" ^
1180 "(#Given, (SideConditions, sideconds))\", \"" ^
1181 "(#Given, (FunctionVariable, funvar))\", \"" ^
1182 "(#Given, (Input_Descript.Domain, doma))\", \"" ^
1183 "(#Given, (ErrorBound, err))\", \"" ^
1184 "(#Find, (AdditionalValues, vals))\"]"
1185 then () else error "complete_TEST: init. met_patt CHANGED";
1187 (*old*)val ((_, pbl_max_vnt as 3, pbl_i_max), _, _) = I_Model.of_max_variant pbl_patt pbl_imod
1188 (*new below step into*)
1190 val return_max_variants =
1191 (*I_Model.*)max_variants pbl_imod;
1192 \<close> ML \<open> (*////--------- step into max_variants ----------------------------------------------\\*)
1193 (*////---------------- step into max_variants ----------------------------------------------\\*)
1194 "~~~~~ fun max_variants , args:"; val (model_patt, i_model) = (pbl_patt, pbl_imod);
1197 map (fn (_, variants, _, _, _) => variants) i_model
1201 (*+*)val [1, 2, 3] = all_variants
1203 val variants_separated = map (filter_variants' i_model) all_variants
1205 (*+*)if map (I_Model.to_string_TEST @{context}) variants_separated =
1206 ["[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
1207 "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
1208 "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
1209 "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
1210 "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]",
1211 "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
1212 "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
1213 "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
1214 "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
1215 "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]",
1216 "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
1217 "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
1218 "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
1219 "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T))]"]
1220 then () else error "of_max_variant: variants_separated CHANGED"
1222 val sums_corr = map (cnt_corrects) variants_separated
1223 (*+*)val [5, 5, 4] = sums_corr
1225 val sum_variant_s = arrange_args sums_corr (1, all_variants)
1226 (*+*)val [(5(*--- items with Cor_TEST in variant ---*), 1), (5, 2), (4, 3)] = sum_variant_s
1228 val max_first = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
1229 (*+*)val [(5, 2), (5, 1), (4, 3)] = max_first
1231 val maxes = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first
1233 (*+*)val [2, 1] = maxes
1235 val option_sequence = map
1236 (fn (_, vnt) => if (member (op =) maxes vnt) then SOME vnt else NONE) sum_variant_s
1237 (*+*)val [SOME 1, SOME 2, NONE] = option_sequence
1239 val max_i_models = map (fn (pos_in_sum_variant_s, i_model) =>
1240 if is_some pos_in_sum_variant_s then i_model else [])
1241 (option_sequence ~~ variants_separated)
1242 |> filter_out (fn place_holder => place_holder = []);
1243 (*+*)if map (I_Model.to_string_TEST @{context}) max_i_models = [
1244 "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
1245 "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
1246 "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
1247 "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
1248 "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]",
1249 "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
1250 "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
1251 "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
1252 "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
1253 "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"]
1254 then () else error "of_max_variant: resulting max_i_models CHANGED"
1256 (*+*)if length max_i_models = length maxes
1257 (*+*)then () else error "of_max_variant: resulting max_i_models AND maxes OF UNEQUAL LENGTH"
1259 val return_max_variants_step = (maxes, max_i_models)
1261 (*+*)if return_max_variants_step = return_max_variants
1262 (*+*)then () else error "max_variants CHANGED"
1263 \<close> ML \<open> (*\\\\--------- step into max_variants ----------------------------------------------//*)
1264 (*\\\\---------------- step into max_variants ----------------------------------------------//*)
1265 val (pbl_max_vnts, pbl_max_imos) = return_max_variants
1267 \<close> ML \<open> (*|||---------- continue fill_method --------------------------------------------------*)
1268 (*|||----------------- continue fill_method --------------------------------------------------*)
1270 val (pbl_max_vnts, pbl_max_imos) = (*I_Model.*)max_variants pbl_imod
1272 (*+*)val [2, 1] = pbl_max_vnts;
1273 (*-------pbl_max_imos is NONSENSE (*+*)if (pbl_max_imos ..*)
1274 (*+*)if (pbl_max_imos |> map (map (fn (no, vnts, _, _, _) => (no, vnts)))) = [
1275 [(1, [1, 2, 3]), (2, [1, 2, 3]), (3, [1, 2, 3]), (4, [1, 2, 3]), (5, [1, 2])],
1276 [(1, [1, 2, 3]), (2, [1, 2, 3]), (3, [1, 2, 3]), (4, [1, 2, 3]), (5, [1, 2])]]
1277 (*+*)then () else error "of_max_variant: RESULT pbl_max_imos CHANGED";
1279 (*we maintain the sequence of items in model_patt for sequence of formals*)
1280 val from_pbl = map (fn (_, (descr, _)) => get_descr_vnt descr maxes pbl_imod) met_patt
1282 (*+*)if (from_pbl |> to_string_TEST @{context}) = "[\n" ^
1283 "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
1284 "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
1285 "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
1286 "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
1287 "(0, [], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n" ^
1288 "(0, [], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n" ^
1289 "(0, [], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n" ^
1290 (*RESULT OF program ---------------------AdditionalValues [u, v]-------------------------*)
1291 "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
1292 (*+*)then () else error "get_descr_vntL result CHANGED";
1295 \<close> ML \<open> (*////--------- step into get_descr_vnt' --------------------------------------------\\*)
1296 (*////---------------- step into get_descr_vnt' --------------------------------------------\\*)
1298 "~~~~~ fun get_descr_vnt' , args:"; val (feedb, vnts, o_model) =
1299 (Sup_TEST (@{term FunctionVariable}, [@{term "a::real"}]), maxes, o_model);
1301 (*+*)val "(7, [\"1\"], #Given, FunctionVariable, [\"a\"])"
1302 (*+*) = (get_descr_vnt' feedb vnts o_model |> the |> O_Model.single_to_string @{context});
1304 val (_, vnts', _, descr', ts) = nth 7 o_model
1305 val (_, _, _, _, (feedb, _)) = nth 5 from_pbl
1307 (*+*)val SOME (Const ("Input_Descript.FunctionVariable", _)) = get_dscr' feedb
1309 (*+*)val xxx = (fn (_, vnts', _, descr', _) =>
1310 case get_dscr' feedb of
1311 SOME descr => if descr' = descr andalso inter op= vnts' vnts <> [] then true else false)
1313 (*+*)xxx: O_Model.single -> bool
1315 (*+*)val SOME (7, [1], "#Given", Const ("Input_Descript.FunctionVariable", _), [Free ("a", _)])
1316 = find_first (fn (_, vnts', _, descr', _) =>
1317 case get_dscr' feedb of
1318 SOME descr => if descr' = descr andalso inter op= vnts' vnts <> [] then true else false
1319 | NONE => false) o_model
1321 (*\\\\---------------- step into get_descr_vnt' --------------------------------------------//*)
1322 \<close> ML \<open> (*\\\\--------- step into get_descr_vnt' --------------------------------------------//*)
1324 \<close> ML \<open> (*|||---------- continue fill_method --------------------------------------------------*)
1325 (*|||----------------- continue fill_method --------------------------------------------------*)
1327 val from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
1328 if is_empty_single_TEST i_single
1330 case get_descr_vnt' feedb vnts o_model of
1331 NONE => raise ERROR (msg vnts feedb)
1332 | SOME (i, vnts, m_field, descr, ts) =>
1333 (i, vnts, true, m_field, (Cor_TEST ((descr, ts), (TermC.empty, [])), Position.none))
1334 else i_single (*fetched before from pbl_imod*))) from_pbl
1337 (*+*)val 8 = length from_o_model;
1338 (*+*)if (from_o_model |> I_Model.to_string_TEST @{context}) = "[\n" ^
1339 "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
1340 "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
1341 "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
1342 "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
1343 "(7, [1], true ,#Given, (Cor_TEST FunctionVariable a , pen2str, Position.T)), \n" ^
1344 "(10, [1, 2], true ,#Given, (Cor_TEST Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
1345 "(12, [1, 2, 3], true ,#Given, (Cor_TEST ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
1346 "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
1347 then () else error "RESULT of fill_method CHANGED"
1349 (*+*)if (o_model |> O_Model.to_string @{context}) = "[\n" ^
1350 (*from_pbl*)"(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n" ^
1351 (*from_pbl*)"(2, [\"1\", \"2\", \"3\"], #Given, Maximum, [\"A\"]), \n" ^
1352 (*from_pbl*)"(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n" ^
1353 (*from_pbl*)"(4, [\"1\", \"2\", \"3\"], #Given, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n" ^
1354 (*from_pbl*)"(5, [\"1\", \"2\"], #Given, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n" ^
1355 "(6, [\"3\"], #Given, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n" ^
1357 (*from_omo*)"(7, [\"1\"], #Given, FunctionVariable, [\"a\"]), \n" ^ (*..both in intersection *)
1358 (*from_omo*)"(8, [\"2\"], #Given, FunctionVariable, [\"b\"]), \n" ^ (*..both in intersection *)
1359 "(9, [\"3\"], #Given, FunctionVariable, [\"\<alpha>\"]), \n" ^
1360 (*from_omo*)"(10, [\"1\", \"2\"], #Given, Input_Descript.Domain, [\"{0<..<r}\"]), \n" ^
1361 "(11, [\"3\"], #Given, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n" ^
1362 (*from_omo*)"(12, [\"1\", \"2\", \"3\"], #Given, ErrorBound, [\"\<epsilon> = 0\"])]"
1363 (*^^^^^^^^ these should go to met_imod: COME "from_pbl" OR "from o_model-------------------------*)
1364 then () else error "CHANGED o_model with items to add marked"
1366 \<close> ML \<open>(*new*)
1368 (*I_Model.*)fill_method oris (I_Model.OLD_to_TEST probl) met_patt;
1372 \<close> ML \<open> (*\\\---------- step into fill_method -----------------------------------------------//*)
1373 (*\\\----------------- step into fill_method -----------------------------------------------//*)
1375 \<close> ML \<open>(*||------------ continue by_tactic ----------------------------------------------------*)
1376 (*||------------------ continue by_tactic ----------------------------------------------------*)
1377 \<close> ML \<open>(*new*)
1378 (*new*)val itms = return_fill_method
1380 \<close> ML \<open> (*\\----------- step into by_tactic -------------------------------------------------//*)
1381 (*\\------------------ step into by_tactic -------------------------------------------------//*)
1384 * of_max_variant returns hd maxes (works by chance for the example)
1385 * do the same ^^^ with MethodC
1386 * take the MethodC.model from the intersection of respective maxes
1387 * if intersection = [] then message calling for interactive resolution
1391 \<close> text \<open> (*beim verschieben*)
1392 val ((pbl_max_vnt, pbl_i_max), _, _) = return_of_max_variant;
1395 \<close> text \<open> (*itermediate test result, before starting*)
1396 (*+*) (pbl_i_max |> I_Model.to_string_TEST @ {context}) = "[\n" ^
1397 "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
1398 "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
1399 "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
1400 "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T))]"
1403 \<close> text \<open>
1404 (*+*)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] ,true ,#Given ,Cor FunctionVariable a , pen2str), \n(10 ,[1, 2] ,true ,#Given ,Cor Input_Descript.Domain {0<..<r} , pen2str), \n(12 ,[1, 2, 3] ,true ,#Given ,Cor ErrorBound (\<epsilon> = 0) , pen2str)]"
1405 = itms |> I_Model.to_string @ {context}
1406 (*+*)val 8 = length itms
1407 (*+*)val 8 = length model
1408 \<close> ML \<open>(*\------------- step into me_Add_Given_ErrorBound------------------------------------//*)
1409 (*\------------------- step into me_Add_Given_ErrorBound------------------------------------//*)
1415 section \<open>===================================================================================\<close>
1416 section \<open>===== ===========================================================================\<close>