Walther@60763
|
1 |
(* Title: "Minisubpbl/100a-init-rootpbl-Maximum.sml"
|
Walther@60763
|
2 |
Author: Walther Neuper 1105
|
Walther@60763
|
3 |
(c) copyright due to lincense terms.
|
Walther@60763
|
4 |
|
Walther@60763
|
5 |
COMPARE Specify/specify.sml --- specify-phase: low level functions ---
|
Walther@60763
|
6 |
|
Walther@60763
|
7 |
ATTENTION: the file creates buffer overflow if copied in one piece !
|
Walther@60763
|
8 |
|
Walther@60763
|
9 |
Note: This test --- steps into me --- more than once, to a somewhat extreme extent;
|
Walther@60763
|
10 |
in order not to get lost while working in Test_Some etc,
|
Walther@60763
|
11 |
re-introduce ML (*--- step into XXXXX ---*) and Co.
|
Walther@60763
|
12 |
and use Sidekick for orientation.
|
Walther@60763
|
13 |
Nesting is indicated by /--- //-- ///- at the left margin of the comments.
|
Walther@60763
|
14 |
*)
|
Walther@60763
|
15 |
(*/------- these overwrite definitions in section above ---\*)
|
Walther@60763
|
16 |
open Ctree;
|
Walther@60763
|
17 |
open Pos;
|
Walther@60763
|
18 |
open TermC;
|
Walther@60763
|
19 |
open Istate;
|
Walther@60763
|
20 |
open Tactic;
|
Walther@60763
|
21 |
open I_Model;
|
Walther@60763
|
22 |
open P_Model
|
Walther@60763
|
23 |
open Rewrite;
|
Walther@60763
|
24 |
open Step;
|
Walther@60763
|
25 |
open LItool;
|
Walther@60763
|
26 |
open LI;
|
Walther@60763
|
27 |
open Test_Code
|
Walther@60763
|
28 |
open Specify
|
Walther@60763
|
29 |
open ME_Misc
|
Walther@60763
|
30 |
open Pre_Conds;
|
Walther@60763
|
31 |
(*\------- these overwrite definitions in section above ---/*)
|
Walther@60763
|
32 |
|
Walther@60763
|
33 |
val (_(*example text*),
|
Walther@60763
|
34 |
(model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
|
Walther@60763
|
35 |
"Extremum (A = 2 * u * v - u \<up> 2)" ::
|
Walther@60763
|
36 |
"SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
|
Walther@60763
|
37 |
"SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
|
Walther@60763
|
38 |
"SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
|
Walther@60763
|
39 |
(*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)
|
Walther@60763
|
40 |
"FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
|
Walther@60763
|
41 |
"Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
|
Walther@60763
|
42 |
"ErrorBound (\<epsilon> = (0::real))" :: []),
|
Walther@60763
|
43 |
refs as ("Diff_App",
|
Walther@60763
|
44 |
["univariate_calculus", "Optimisation"],
|
Walther@60763
|
45 |
["Optimisation", "by_univariate_calculus"])))
|
Walther@60763
|
46 |
= Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
|
Walther@60763
|
47 |
|
Walther@60763
|
48 |
val c = [];
|
Walther@60763
|
49 |
val return_init_calc =
|
Walther@60763
|
50 |
Test_Code.init_calc @{context} [(model, refs)]; (*val Model_Problem = nxt;*)
|
Walther@60763
|
51 |
(*/------------------- step into init_calc -------------------------------------------------\\*)
|
Walther@60763
|
52 |
"~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))]) =
|
Walther@60763
|
53 |
(@{context}, [(model, refs)]);
|
Walther@60763
|
54 |
val thy = thy_id |> ThyC.get_theory ctxt
|
Walther@60763
|
55 |
val ((pt, p), tacis) = Step_Specify.initialise' thy (model, refs)
|
Walther@60763
|
56 |
val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
|
Walther@60763
|
57 |
val f =
|
Walther@60763
|
58 |
TESTg_form ctxt (pt,p);
|
Walther@60763
|
59 |
"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p));
|
Walther@60763
|
60 |
val (form, _, _) =
|
Walther@60763
|
61 |
ME_Misc.pt_extract ctxt ptp;
|
Walther@60763
|
62 |
"~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_ as Pbl(*Frm,Pbl*)))) = (ctxt, ptp);
|
Walther@60763
|
63 |
val ppobj = Ctree.get_obj I pt p
|
Walther@60763
|
64 |
val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p;
|
Walther@60763
|
65 |
|
Walther@60763
|
66 |
(*if*) Ctree.is_pblobj ppobj (*then*);
|
Walther@60763
|
67 |
pt_model ppobj p_ ;
|
Walther@60763
|
68 |
"~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}), Pbl_) =
|
Walther@60763
|
69 |
(ppobj, p_);
|
Walther@60763
|
70 |
val (_, pI, _) = Ctree.get_somespec' spec spec';
|
Walther@60763
|
71 |
(* val where_ = if pI = Problem.id_empty then []*)
|
Walther@60763
|
72 |
(*if*) pI = Problem.id_empty (*else*);
|
Walther@60763
|
73 |
val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
|
Walther@60763
|
74 |
val (_, where_) =
|
Walther@60763
|
75 |
Pre_Conds.check ctxt where_rls where_
|
Walther@60782
|
76 |
(model, I_Model.OLD_to probl);
|
Walther@60763
|
77 |
"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
|
Walther@60782
|
78 |
(ctxt, where_rls, where_, (model, I_Model.OLD_to probl));
|
Walther@60763
|
79 |
val (env_model, (env_subst, env_eval)) =
|
Walther@60763
|
80 |
make_environments model_patt i_model;
|
Walther@60763
|
81 |
"~~~~~ fun make_environments , args:"; val (_, []) = (model_patt, i_model);
|
Walther@60763
|
82 |
(*\------------------- step into init_calc -------------------------------------------------//*)
|
Walther@60763
|
83 |
val (p,_,f,nxt,_,pt) = return_init_calc;
|
Walther@60763
|
84 |
|
Walther@60763
|
85 |
(*+*)val PblObj {ctxt, probl, ...} = get_obj I pt [];
|
Walther@60763
|
86 |
(*+*)Proof_Context.theory_of ctxt (*= {Pure, .., Diff_App}*);
|
Walther@60763
|
87 |
(*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term ctxt "r"
|
Walther@60763
|
88 |
(*+*)val [] = probl
|
Walther@60763
|
89 |
|
Walther@60763
|
90 |
val return_me_Model_Problem =
|
Walther@60763
|
91 |
me nxt p c pt; val Add_Given "Constants [r = 7]" = #4 return_me_Model_Problem;
|
Walther@60763
|
92 |
(*/------------------- step into me_Model_Problem ------------------------------------------\\*)
|
Walther@60763
|
93 |
"~~~~~ fun me , args:"; val (tac as Model_Problem, (p:Pos.pos'), (_:Test_Code.NEW), (pt:Ctree.ctree)) = (nxt, p, c, pt);
|
Walther@60763
|
94 |
val ctxt = Ctree.get_ctxt pt p
|
Walther@60766
|
95 |
|
Walther@60763
|
96 |
val return_by_tactic = case
|
Walther@60763
|
97 |
Step.by_tactic tac (pt,p) of
|
Walther@60763
|
98 |
("ok", (_, _, ptp)) => ptp;
|
Walther@60763
|
99 |
(*//------------------ step into by_tactic -------------------------------------------------\\*)
|
Walther@60763
|
100 |
"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
|
Walther@60766
|
101 |
|
Walther@60763
|
102 |
val Applicable.Yes tac' = (*case*)
|
Walther@60763
|
103 |
Step.check tac (pt, p) (*of*);
|
Walther@60763
|
104 |
"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
|
Walther@60763
|
105 |
(*if*) Tactic.for_specify tac (*then*);
|
Walther@60763
|
106 |
|
Walther@60763
|
107 |
Specify_Step.check tac (ctree, pos);
|
Walther@60763
|
108 |
"~~~~~ fun check , args:"; val (Tactic.Model_Problem, (pt, pos as (p, _))) =
|
Walther@60763
|
109 |
(tac, (ctree, pos));
|
Walther@60766
|
110 |
val (ctxt, o_model, pI') = case Ctree.get_obj I pt p of
|
Walther@60766
|
111 |
Ctree.PblObj {ctxt, origin = (o_model, (_, pI', _), _), ...} => (ctxt, o_model, pI')
|
Walther@60766
|
112 |
| _ => raise ERROR "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj"
|
Walther@60763
|
113 |
val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
|
Walther@60782
|
114 |
val pbl = I_Model.init ctxt o_model model_patt
|
Walther@60763
|
115 |
|
Walther@60763
|
116 |
val return_check =
|
Walther@60763
|
117 |
Applicable.Yes (Tactic.Model_Problem' (pI', I_Model.TEST_to_OLD pbl, []));
|
Walther@60763
|
118 |
(*\\------------------ step into by_tactic -------------------------------------------------//*)
|
Walther@60763
|
119 |
val (pt, p) = return_by_tactic;
|
Walther@60763
|
120 |
|
Walther@60763
|
121 |
val return_do_next = (*case*)
|
Walther@60763
|
122 |
Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
|
Walther@60763
|
123 |
(*//------------------ step into do_next ---------------------------------------------------\\*)
|
Walther@60763
|
124 |
"~~~~~ fun do_next , args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) =
|
Walther@60763
|
125 |
(p, ((pt, e_pos'),[]));
|
Walther@60763
|
126 |
val pIopt = get_pblID (pt,ip);
|
Walther@60763
|
127 |
(*if*) ip = ([],Res); (* = false*)
|
Walther@60763
|
128 |
val _ = (*case*) tacis (*of*);
|
Walther@60763
|
129 |
val SOME _ = (*case*) pIopt (*of*);
|
Walther@60763
|
130 |
|
Walther@60763
|
131 |
val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
|
Walther@60763
|
132 |
Step.switch_specify_solve p_ (pt, ip);
|
Walther@60763
|
133 |
"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
|
Walther@60763
|
134 |
(*if*) Pos.on_specification ([], state_pos) (*then*);
|
Walther@60763
|
135 |
|
Walther@60763
|
136 |
val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
|
Walther@60763
|
137 |
Step.specify_do_next (pt, input_pos);
|
Walther@60763
|
138 |
(*///----------------- step into specify_do_next -------------------------------------------\\*)
|
Walther@60763
|
139 |
"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
|
Walther@60763
|
140 |
|
Walther@60763
|
141 |
(* val (_, (p_', tac)) =*)
|
Walther@60763
|
142 |
val return_find_next_step = (*keep for continuing specify_do_next*)
|
Walther@60763
|
143 |
Specify.find_next_step ptp;
|
Walther@60763
|
144 |
(*////---------------- step into find_next_step --------------------------------------------\\*)
|
Walther@60763
|
145 |
"~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
|
Walther@60763
|
146 |
val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
|
Walther@60763
|
147 |
spec = refs, ...} = Calc.specify_data (pt, pos);
|
Walther@60763
|
148 |
val ctxt = Ctree.get_ctxt pt pos;
|
Walther@60763
|
149 |
(*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
|
Walther@60763
|
150 |
(*if*) p_ = Pos.Pbl (*then*);
|
Walther@60763
|
151 |
|
Walther@60763
|
152 |
val return_for_problem as ("dummy", (Pbl, Add_Given "Constants [r = 7]")) =
|
Walther@60782
|
153 |
Specify.for_problem ctxt oris (o_refs, refs) (pbl, I_Model.OLD_to met);
|
Walther@60763
|
154 |
(*/////--------------- step into for_problem -----------------------------------------------\\*)
|
Walther@60763
|
155 |
"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
|
Walther@60763
|
156 |
= (ctxt, oris, (o_refs, refs), (pbl, met));
|
Walther@60763
|
157 |
val cdI = if dI = ThyC.id_empty then dI' else dI;
|
Walther@60763
|
158 |
val cpI = if pI = Problem.id_empty then pI' else pI;
|
Walther@60763
|
159 |
val cmI = if mI = MethodC.id_empty then mI' else mI;
|
Walther@60763
|
160 |
val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
|
Walther@60763
|
161 |
val {model = mpc, ...} = MethodC.from_store ctxt cmI;
|
Walther@60763
|
162 |
|
Walther@60763
|
163 |
val return_check =
|
Walther@60782
|
164 |
Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to pbl);
|
Walther@60763
|
165 |
(*//////-------------- step into check -------------------------------------------------\\*)
|
Walther@60763
|
166 |
"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
|
Walther@60782
|
167 |
(ctxt, where_rls, where_, (pbt, I_Model.OLD_to pbl));
|
Walther@60763
|
168 |
val return_make_environments =
|
Walther@60763
|
169 |
make_environments model_patt i_model;
|
Walther@60763
|
170 |
(*///// //------------ step into of_max_variant --------------------------------------------\\*)
|
Walther@60763
|
171 |
"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) =
|
Walther@60763
|
172 |
(model_patt, i_model);
|
Walther@60763
|
173 |
|
Walther@60782
|
174 |
(*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc Constants [] [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc SideConditions [] [__=__, __=__], Position.T))]"
|
Walther@60782
|
175 |
= i_model |> I_Model.to_string ctxt
|
Walther@60763
|
176 |
val all_variants =
|
Walther@60763
|
177 |
map (fn (_, variants, _, _, _) => variants) i_model
|
Walther@60763
|
178 |
|> flat
|
Walther@60763
|
179 |
|> distinct op =
|
Walther@60763
|
180 |
val variants_separated = map (filter_variants' i_model) all_variants
|
Walther@60763
|
181 |
val sums_corr = map (Model_Def.cnt_corrects) variants_separated
|
Walther@60763
|
182 |
val sum_variant_s = Model_Def.arrange_args sums_corr (1, all_variants)
|
Walther@60763
|
183 |
(*+*)val [(0, 1), (0, 2), (0, 3)] = sum_variant_s
|
Walther@60763
|
184 |
val (_, max_variant) = hd (*..crude decision, up to improvement *)
|
Walther@60763
|
185 |
(sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
|
Walther@60763
|
186 |
val i_model_max =
|
Walther@60763
|
187 |
filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
|
Walther@60763
|
188 |
val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
|
Walther@60763
|
189 |
(*for building make_env_s -------------------------------------------------------------------\*)
|
Walther@60763
|
190 |
(*!!!*) val ("#Given", (descr, term), pos) =
|
Walther@60763
|
191 |
Model_Pattern.split_descriptor ctxt ("#Given", @{term "Constants [r = (7::real)]"}, Position.none)
|
Walther@60763
|
192 |
(*!!!*) val patt = equal_descr_pairs |> hd |> #1
|
Walther@60763
|
193 |
(*!!!*)val equal_descr_pairs =
|
Walther@60763
|
194 |
(patt,
|
Walther@60782
|
195 |
(1, [1, 2, 3], true, "#Given", (Cor ((descr, (*!*)TermC.isalist2list(*!*) term)), pos)))
|
Walther@60763
|
196 |
:: tl equal_descr_pairs
|
Walther@60763
|
197 |
(*for building make_env_s -------------------------------------------------------------------/*)
|
Walther@60763
|
198 |
|
Walther@60763
|
199 |
val env_model = make_env_model equal_descr_pairs;
|
Walther@60763
|
200 |
(*///// ///----------- step into make_env_model --------------------------------------------\\*)
|
Walther@60763
|
201 |
"~~~~~ fun make_env_model , args:"; val (equal_descr_pairs) = (equal_descr_pairs);
|
Walther@60763
|
202 |
|
Walther@60763
|
203 |
val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
|
Walther@60763
|
204 |
=> (mk_env_model id feedb));
|
Walther@60763
|
205 |
val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 4 equal_descr_pairs;
|
Walther@60763
|
206 |
(*\\\\\ \\\----------- step into make_env_model --------------------------------------------//*)
|
Walther@60763
|
207 |
(*||||| ||------------ contine of_max_variant ------------------------------------------------*)
|
Walther@60763
|
208 |
|
Walther@60763
|
209 |
val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
|
Walther@60763
|
210 |
val subst_eval_list = make_envs_preconds equal_givens
|
Walther@60763
|
211 |
val return_make_envs_preconds =
|
Walther@60763
|
212 |
make_envs_preconds equal_givens;
|
Walther@60763
|
213 |
(*///// ///----------- step into make_envs_preconds ----------------------------------------\\*)
|
Walther@60763
|
214 |
"~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
|
Walther@60763
|
215 |
val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb)
|
Walther@60763
|
216 |
;
|
Walther@60782
|
217 |
xxx: (Model_Pattern.single * I_Model.single) -> ((term * term) * (term * term)) list;
|
Walther@60763
|
218 |
val return_discern_feedback =
|
Walther@60763
|
219 |
discern_feedback id feedb;
|
Walther@60763
|
220 |
(*nth 1 equal_descr_pairs* )
|
Walther@60782
|
221 |
"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor ((descr, ts), _))) = (id, feedb);
|
Walther@60763
|
222 |
( *nth 2 equal_descr_pairs*)
|
Walther@60782
|
223 |
"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Inc ((descr, ts)))) = (id, feedb);
|
Walther@60763
|
224 |
|
Walther@60763
|
225 |
(*nth 1 equal_descr_pairs* )
|
Walther@60763
|
226 |
(*+*)val [((Const ("fixes", typ1), Free ("r", typ2)),
|
Walther@60763
|
227 |
(Free ("r", typ3), value))] = return_discern_feedback
|
Walther@60763
|
228 |
(*+*)val true = typ1 = typ2
|
Walther@60763
|
229 |
(*+*)val true = typ3 = HOLogic.realT
|
Walther@60763
|
230 |
(*+*)val "7" = UnparseC.term ctxt value
|
Walther@60763
|
231 |
( *nth 2 equal_descr_pairs*)
|
Walther@60763
|
232 |
(*+*)val [] = return_discern_feedback
|
Walther@60763
|
233 |
|
Walther@60763
|
234 |
val return_discern_typ =
|
Walther@60763
|
235 |
discern_typ id (descr, ts);
|
Walther@60763
|
236 |
"~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts));
|
Walther@60763
|
237 |
(*nth 1 equal_descr_pairs* )
|
Walther@60763
|
238 |
(*+*)val [((Const ("fixes", typ1), Free ("r", typ2)),
|
Walther@60763
|
239 |
(Free ("r", typ3), value))] = return_discern_typ
|
Walther@60763
|
240 |
(*+*)val true = typ1 = typ2
|
Walther@60763
|
241 |
(*+*)val true = typ3 = HOLogic.realT
|
Walther@60763
|
242 |
(*+*)val "7" = UnparseC.term ctxt value
|
Walther@60763
|
243 |
( *nth 2 equal_descr_pairs*)
|
Walther@60763
|
244 |
(*+*)val [] = return_discern_typ;
|
Walther@60763
|
245 |
(**)
|
Walther@60763
|
246 |
switch_type id ts;
|
Walther@60763
|
247 |
"~~~~~ fun switch_type , args:"; val (Const (descr_string, _), ts) = (descr, ts);
|
Walther@60763
|
248 |
|
Walther@60763
|
249 |
(*nth 1 equal_descr_pairs* )
|
Walther@60782
|
250 |
val return_switch_type = Const (descr_string, ts |> hd |> TermC.lhs |> type_of)
|
Walther@60763
|
251 |
|
Walther@60782
|
252 |
(*+*)val Const ("Input_Descript.Constants", typ) = return_switch_type
|
Walther@60763
|
253 |
(*+*)val Type ("Real.real", []) = typ
|
Walther@60763
|
254 |
( *nth 2 equal_descr_pairs*)
|
Walther@60782
|
255 |
(*+*)val return_switch_type = descr
|
Walther@60763
|
256 |
(**)
|
Walther@60763
|
257 |
(*\\\\\ \\\----------- step into make_envs_preconds ----------------------------------------//*)
|
Walther@60763
|
258 |
(*||||| ||------------ contine of_max_variant ------------------------------------------------*)
|
Walther@60763
|
259 |
val subst_eval_list = make_envs_preconds equal_givens
|
Walther@60763
|
260 |
val (env_subst, env_eval) = split_list subst_eval_list
|
Walther@60763
|
261 |
val make_environments = (i_model_max, env_model, (env_subst, env_eval)); (*GOON*)
|
Walther@60763
|
262 |
(*\\\\\ \\------------ step into of_max_variant --------------------------------------------//*)
|
Walther@60763
|
263 |
val (i_model_max, env_model, (env_subst, env_eval)) = make_environments
|
Walther@60763
|
264 |
(*!!!/----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---\*)
|
Walther@60763
|
265 |
val (i_max_variant, env_model, (env_subst, env_eval)) = (i_model_max, [], ([], []))
|
Walther@60763
|
266 |
(*!!!\----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---/*)
|
Walther@60763
|
267 |
(*||||| |------------- contine check -----------------------------------------------------*)
|
Walther@60763
|
268 |
val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
|
Walther@60763
|
269 |
val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
|
Walther@60763
|
270 |
val full_subst = if env_eval = [] then pres_subst_other
|
Walther@60763
|
271 |
else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
|
Walther@60763
|
272 |
val evals = map (eval ctxt where_rls) full_subst
|
Walther@60763
|
273 |
val return_ = (i_model_max, env_subst, env_eval)
|
Walther@60763
|
274 |
(*\\\\\ \------------- step into check -----------------------------------------------------//*)
|
Walther@60763
|
275 |
val (preok, _) = return_check;
|
Walther@60763
|
276 |
|
Walther@60763
|
277 |
(*|||||--------------- contine.. for_problem -------------------------------------------------*)
|
Walther@60763
|
278 |
val false =
|
Walther@60763
|
279 |
(*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
|
Walther@60763
|
280 |
val false =
|
Walther@60763
|
281 |
(*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
|
Walther@60763
|
282 |
val NONE =
|
Walther@60763
|
283 |
(*case*) find_first (fn (_, _, _, _, feedb) => I_Model.is_error feedb) pbl (*of*);
|
Walther@60763
|
284 |
|
Walther@60763
|
285 |
(** )val SOME (fd, ct') as ("#Given", "Constants [r = 7]") =( **)
|
Walther@60763
|
286 |
(**)val return_item_to_add as SOME ("#Given", xxx) =(**) (*case*)
|
Walther@60782
|
287 |
Specify.item_to_add ctxt oris (I_Model.OLD_to pbl) (*of*);
|
Walther@60763
|
288 |
(*///// /------------- step into item_to_add -----------------------------------------------\\*)
|
Walther@60763
|
289 |
(*==================== see test/../i_model.sml --- fun item_to_add ---========================*)
|
Walther@60763
|
290 |
(*\\\\\ \------------- step into item_to_add -----------------------------------------------//*)
|
Walther@60763
|
291 |
val SOME (fd, ct') = return_item_to_add
|
Walther@60763
|
292 |
(*+*)val ("#Given", "Constants [r = 7]") = (fd, ct') (*from NEW item_to_add*)
|
Walther@60763
|
293 |
|
Walther@60763
|
294 |
(*|||||--------------- continue.. for_problem ------------------------------------------------*)
|
Walther@60763
|
295 |
val return_for_problem_step as ("dummy", (Pbl, Add_Given "Constants [r = 7]"))
|
Walther@60763
|
296 |
= ("dummy", (Pos.Pbl, P_Model.mk_additem fd ct'))
|
Walther@60763
|
297 |
(** )return_for_problem_step = return_for_problem( *..would require equality types*)
|
Walther@60763
|
298 |
(*\\\\\--------------- step into for_problem -----------------------------------------------//*)
|
Walther@60763
|
299 |
val return_find_next_step as ("dummy", (Pbl, Add_Given "Constants [r = 7]"))
|
Walther@60763
|
300 |
= return_for_problem
|
Walther@60763
|
301 |
(*\\\\---------------- step into find_next_step --------------------------------------------//*)
|
Walther@60763
|
302 |
(*|||----------------- continue.. specify_do_next --------------------------------------------*)
|
Walther@60763
|
303 |
val (_, (p_', tac as Add_Given "Constants [r = 7]")) = return_find_next_step
|
Walther@60763
|
304 |
|
Walther@60763
|
305 |
val ist_ctxt = Ctree.get_loc pt (p, p_)
|
Walther@60763
|
306 |
(*+*)val Add_Given "Constants [r = 7]" = tac
|
Walther@60763
|
307 |
val _ =
|
Walther@60763
|
308 |
(*case*) tac (*of*);
|
Walther@60763
|
309 |
|
Walther@60763
|
310 |
val return_by_tactic_input as ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
|
Walther@60763
|
311 |
Step_Specify.by_tactic_input tac (pt, (p, p_'));
|
Walther@60763
|
312 |
"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =
|
Walther@60763
|
313 |
(tac, (pt, (p, p_')));
|
Walther@60763
|
314 |
|
Walther@60763
|
315 |
Specify.by_Add_ "#Given" ct ptp;
|
Walther@60763
|
316 |
"~~~~~ fun by_Add_ , args:"; val (m_field, ct ,(pt, pos as (_, p_))) =
|
Walther@60763
|
317 |
("#Given", ct, ptp);
|
Walther@60763
|
318 |
val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
|
Walther@60763
|
319 |
val (i_model, m_patt) =
|
Walther@60763
|
320 |
if p_ = Pos.Met then
|
Walther@60763
|
321 |
(met,
|
Walther@60763
|
322 |
(if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
|
Walther@60763
|
323 |
else
|
Walther@60763
|
324 |
(pbl,
|
Walther@60763
|
325 |
(if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model);
|
Walther@60763
|
326 |
|
Walther@60763
|
327 |
(*case*)
|
Walther@60773
|
328 |
I_Model.check_single ctxt m_field oris (I_Model.TEST_to_OLD i_model) m_patt ct (*of*);
|
Walther@60763
|
329 |
"~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, (str(*, pos*))) =
|
Walther@60763
|
330 |
(ctxt, m_field, oris, i_model, m_patt, ct);
|
Walther@60763
|
331 |
val (t as (descriptor $ _)) = Syntax.read_term ctxt str
|
Walther@60763
|
332 |
|
Walther@60763
|
333 |
(*+*)val "Constants [r = 7]" = UnparseC.term ctxt t;
|
Walther@60763
|
334 |
|
Walther@60763
|
335 |
val SOME m_field' =
|
Walther@60763
|
336 |
(*case*) Model_Pattern.get_field descriptor m_patt (*of*);
|
Walther@60763
|
337 |
(*if*) m_field <> m_field' (*else*);
|
Walther@60763
|
338 |
|
Walther@60763
|
339 |
(*+*)val "#Given" = m_field; val "#Given" = m_field'
|
Walther@60763
|
340 |
|
Walther@60763
|
341 |
val ("", ori', all) =
|
Walther@60763
|
342 |
(*case*) O_Model.contains ctxt m_field o_model t (*of*);
|
Walther@60763
|
343 |
|
Walther@60763
|
344 |
(*+*)val (_, _, _, _, vals) = hd o_model;
|
Walther@60763
|
345 |
(*+*)val "Constants [r = 7]" = UnparseC.term ctxt (@{term Constants} $ (hd vals));
|
Walther@60763
|
346 |
(*+*)if "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), " ^
|
Walther@60763
|
347 |
(*+*) "\n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), " ^
|
Walther@60763
|
348 |
(*+*) "\n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), " ^
|
Walther@60763
|
349 |
(*+*) "\n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), " ^
|
Walther@60763
|
350 |
(*+*) "\n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), " ^
|
Walther@60763
|
351 |
(*+*) "\n(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), " ^
|
Walther@60763
|
352 |
(*+*) "\n(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), " ^
|
Walther@60763
|
353 |
(*+*) "\n(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), " ^
|
Walther@60763
|
354 |
(*+*) "\n(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), " ^
|
Walther@60763
|
355 |
(*+*) "\n(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), " ^
|
Walther@60763
|
356 |
(*+*) "\n(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
|
Walther@60763
|
357 |
(*+*)= O_Model.to_string ctxt o_model then () else error "o_model CHANGED";
|
Walther@60763
|
358 |
|
Walther@60763
|
359 |
(*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*);
|
Walther@60763
|
360 |
"~~~~~ fun is_notyet_input , args:"; val (ctxt, itms, all, (i, v, f, d, ts), pbt) =
|
Walther@60763
|
361 |
(ctxt, i_model, all, ori', m_patt);
|
Walther@60763
|
362 |
val SOME (_, (_, pid)) =
|
Walther@60773
|
363 |
(*case*) find_first (fn (_, (d', _)) => d = d') pbt
|
Walther@60773
|
364 |
val SOME (_, _, _, _, (feedb, _)) =
|
Walther@60773
|
365 |
(*case*) find_first (fn (_, _, _, f', (feedb, _)) =>
|
Walther@60782
|
366 |
f = f' andalso d = (descriptor feedb)) itms
|
Walther@60777
|
367 |
val ts' = inter op = (feedb_values feedb) ts
|
Walther@60773
|
368 |
val false =
|
Walther@60773
|
369 |
(*if*) subset op = (ts, ts')
|
Walther@60773
|
370 |
|
Walther@60773
|
371 |
val return_is_notyet_input = ("",
|
Walther@60778
|
372 |
single_from_o feedb pid all (i, v, f, d, subtract op = ts' ts));
|
Walther@60778
|
373 |
"~~~~~ fun single_from_o , args:"; val (feedb, pid, all, (id, vt, fd, d, ts)) =
|
Walther@60773
|
374 |
(feedb, pid, all, (i, v, f, d, subtract op = ts' ts));
|
Walther@60777
|
375 |
val ts' = union op = (feedb_values feedb) ts;
|
Walther@60763
|
376 |
val pval = [Input_Descript.join'''' (d, ts')]
|
Walther@60763
|
377 |
val complete = if eq_set op = (ts', all) then true else false
|
Walther@60763
|
378 |
|
Walther@60782
|
379 |
(*+*)val "Inc Constants [] [__=__, __=__]" = feedb |> I_Model.feedback_to_string ctxt
|
Walther@60763
|
380 |
(*\\\----------------- step into specify_do_next -------------------------------------------//*)
|
Walther@60763
|
381 |
(*\\------------------ step into do_next ---------------------------------------------------//*)
|
Walther@60763
|
382 |
val ("ok", (ts as (_, _, _) :: _, _, (pt, p))) = return_do_next
|
Walther@60763
|
383 |
|
Walther@60763
|
384 |
(*|------------------- continue with me_Model_Problem ----------------------------------------*)
|
Walther@60763
|
385 |
val tacis as (_::_) =
|
Walther@60763
|
386 |
(*case*) ts (*of*);
|
Walther@60763
|
387 |
val (tac, _, _) = last_elem tacis
|
Walther@60763
|
388 |
|
Walther@60763
|
389 |
val return_Model_Problem = (p, [] : NEW, TESTg_form ctxt (pt, p), tac, Celem.Sundef, pt);
|
Walther@60763
|
390 |
(*//------------------ step into TESTg_form ------------------------------------------------\\*)
|
Walther@60763
|
391 |
"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt, p));
|
Walther@60763
|
392 |
|
Walther@60763
|
393 |
val (form, _, _) =
|
Walther@60763
|
394 |
ME_Misc.pt_extract ctxt ptp;
|
Walther@60763
|
395 |
"~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_(*Frm,Pbl*)))) = (ctxt, ptp);
|
Walther@60763
|
396 |
val ppobj = Ctree.get_obj I pt p
|
Walther@60763
|
397 |
val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p;
|
Walther@60763
|
398 |
(*if*) Ctree.is_pblobj ppobj (*then*);
|
Walther@60763
|
399 |
|
Walther@60763
|
400 |
pt_model ppobj p_;
|
Walther@60763
|
401 |
"~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, o_spec, hdl), ctxt, ...}),
|
Walther@60763
|
402 |
Pbl(*Frm,Pbl*)) = (ppobj, p_);
|
Walther@60763
|
403 |
val (_, _, met_id) = References.select_input o_spec spec
|
Walther@60782
|
404 |
val (allcorr, _) = Pre_Conds.check_internal ctxt (I_Model.OLD_to probl) (Pos.Met, met_id)
|
Walther@60773
|
405 |
|
Walther@60782
|
406 |
val return_pt_model = Ctree.ModSpec (allcorr, Pos.Pbl, hdl, I_Model.OLD_to probl,
|
Walther@60773
|
407 |
(*where_*)[(*Problem.from_store in check*)], spec)
|
Walther@60763
|
408 |
|
Walther@60763
|
409 |
(*|------------------- continue with TESTg_form ----------------------------------------------*)
|
Walther@60763
|
410 |
val Ctree.ModSpec (spec as (_, p_, _, gfr, where_, _)) =
|
Walther@60763
|
411 |
(*case*) form (*of*);
|
Walther@60763
|
412 |
Test_Out.PpcKF ( (Test_Out.Problem [],
|
Walther@60763
|
413 |
P_Model.from (Proof_Context.theory_of ctxt) gfr where_));
|
Walther@60763
|
414 |
|
Walther@60763
|
415 |
P_Model.from (Proof_Context.theory_of ctxt) gfr where_;
|
Walther@60763
|
416 |
"~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);
|
Walther@60763
|
417 |
fun coll model [] = model
|
Walther@60763
|
418 |
| coll model ((_, _, _, field, itm_) :: itms) =
|
Walther@60763
|
419 |
coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
|
Walther@60763
|
420 |
|
Walther@60773
|
421 |
val gfr = coll P_Model.empty (I_Model.TEST_to_OLD itms);
|
Walther@60763
|
422 |
"~~~~~ fun coll , args:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: itms))
|
Walther@60773
|
423 |
= (P_Model.empty, I_Model.TEST_to_OLD itms);
|
Walther@60763
|
424 |
|
Walther@60763
|
425 |
(*+*)val 4 = length itms;
|
Walther@60763
|
426 |
(*+*)val itm = nth 1 itms;
|
Walther@60763
|
427 |
|
Walther@60763
|
428 |
coll P_Model.empty [itm];
|
Walther@60763
|
429 |
"~~~~~ fun coll , iterate:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: []))
|
Walther@60763
|
430 |
= (P_Model.empty, [itm]);
|
Walther@60763
|
431 |
|
Walther@60763
|
432 |
(add_sel_ppc thy field model (item_from_feedback thy itm_));
|
Walther@60763
|
433 |
"~~~~~ fun add_sel_ppc , args:"; val ((_: theory), sel, {Given = gi, Where = wh, Find = fi, With = wi, Relate = re}, x )
|
Walther@60763
|
434 |
= (thy, field, model, (item_from_feedback thy itm_));
|
Walther@60763
|
435 |
|
Walther@60763
|
436 |
P_Model.item_from_feedback thy itm_;
|
Walther@60763
|
437 |
"~~~~~ fun item_from_feedback , args:"; val (thy, (I_Model.Inc ((d, ts), _))) = (thy, itm_);
|
Walther@60763
|
438 |
P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)));
|
Walther@60763
|
439 |
(*\\------------------ step into TESTg_form ------------------------------------------------//*)
|
Walther@60763
|
440 |
(*\------------------- step into me_Model_Problem ------------------------------------------//*)
|
Walther@60763
|
441 |
val (p, _, f, nxt, _, pt) = return_me_Model_Problem
|
Walther@60763
|
442 |
|
Walther@60763
|
443 |
(*+++*)val {probl, ...} = Calc.specify_data (pt, pos);
|
Walther@60763
|
444 |
(*+++*)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)]"
|
Walther@60763
|
445 |
= probl |> I_Model.to_string ctxt
|
Walther@60763
|
446 |
(*-------------------- contine me's ----------------------------------------------------------*)
|
Walther@60763
|
447 |
val return_me_add_find_Constants = me nxt p c pt;
|
Walther@60763
|
448 |
val Add_Find "Maximum A" = #4 return_me_add_find_Constants;
|
Walther@60763
|
449 |
(*/------------------- step into me_add_find_Constants -------------------------------------\\*)
|
Walther@60763
|
450 |
(*==================== done in "Minisubpbl/150a-add-given-Maximum.sml" subsequently =======================*)
|