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