neuper@42279
|
1 |
(* Title: tests for Interpret/mathengine.sml
|
neuper@42279
|
2 |
Author: Walther Neuper 2000, 2006
|
neuper@37906
|
3 |
(c) due to copyright terms
|
neuper@37906
|
4 |
*)
|
neuper@38065
|
5 |
"--------------------------------------------------------";
|
neuper@38065
|
6 |
"table of contents --------------------------------------";
|
neuper@38065
|
7 |
"--------------------------------------------------------";
|
neuper@41940
|
8 |
"----------- change to parse ctxt -----------------------";
|
neuper@38065
|
9 |
"----------- debugging setContext..pbl_ -----------------";
|
neuper@38065
|
10 |
"----------- tryrefine ----------------------------------";
|
neuper@41982
|
11 |
"----------- fun step: Apply_Method without init_form ---";
|
neuper@38065
|
12 |
"----------- fun step -----------------------------------";
|
neuper@38065
|
13 |
"----------- fun autocalc -------------------------------";
|
neuper@38065
|
14 |
"----------- fun autoCalculate --------------------------";
|
neuper@42067
|
15 |
"----------- fun autoCalculate..CompleteCalc ------------";
|
t@42225
|
16 |
"----------- search for Or_to_List ----------------------";
|
neuper@42279
|
17 |
"----------- check thy in CalcTreeTEST ------------------";
|
neuper@38065
|
18 |
"--------------------------------------------------------";
|
neuper@38065
|
19 |
"--------------------------------------------------------";
|
neuper@38065
|
20 |
"--------------------------------------------------------";
|
neuper@37906
|
21 |
|
neuper@41940
|
22 |
"----------- change to parse ctxt -----------------------";
|
neuper@41940
|
23 |
"----------- change to parse ctxt -----------------------";
|
neuper@41940
|
24 |
"----------- change to parse ctxt -----------------------";
|
neuper@41940
|
25 |
"===== start calculation: from problem description (fmz) to origin";
|
neuper@41940
|
26 |
val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
|
neuper@41940
|
27 |
val (thyID, pblID, metID) =
|
neuper@41940
|
28 |
("Test", ["calculate", "test"], ["Test", "test_calculate"]);
|
neuper@41940
|
29 |
val (p,_,_,nxt,_,pt) = CalcTreeTEST [(fmz, (thyID, pblID, metID))];
|
neuper@41940
|
30 |
"----- ";
|
neuper@41940
|
31 |
(* call sequence: CalcTreeTEST
|
neuper@41940
|
32 |
> nxt_specify_init_calc
|
neuper@41940
|
33 |
> prep_ori
|
neuper@41940
|
34 |
*)
|
neuper@41940
|
35 |
val (thy, pbt) = (Thy_Info.get_theory thyID, (#ppc o get_pbt) pblID);
|
neuper@41940
|
36 |
"----- in prep_ori";
|
neuper@48761
|
37 |
val ctxt = Proof_Context.init_global thy;
|
neuper@41940
|
38 |
|
bonzai@41952
|
39 |
val ctopts = map (parseNEW ctxt) fmz;
|
bonzai@41952
|
40 |
val dts = map (split_dts o the) ctopts;
|
neuper@41940
|
41 |
(*split_dts:
|
neuper@41940
|
42 |
(term * term list) list
|
neuper@41940
|
43 |
formulas: e.g. ((1+2)*4/3)^^^2
|
neuper@41940
|
44 |
description: e.g. realTestGiven
|
neuper@41940
|
45 |
*)
|
neuper@41940
|
46 |
prep_ori;
|
neuper@41940
|
47 |
(* FROM
|
neuper@41940
|
48 |
val it = fn:
|
neuper@41940
|
49 |
string list -> theory -> (string * (term * 'a)) list -> ori list
|
neuper@41940
|
50 |
TO
|
neuper@41940
|
51 |
val it = fn:
|
neuper@41940
|
52 |
string list -> theory -> (string * (term * 'a)) list -> (ori list * ctxt)
|
neuper@41940
|
53 |
AND
|
neuper@41940
|
54 |
FROM val oris = prep_ori...
|
neuper@41940
|
55 |
TO val (oris, _) = prep_ori...
|
neuper@41940
|
56 |
*)
|
neuper@41940
|
57 |
"----- insert ctxt in ptree";
|
neuper@41940
|
58 |
(* datatype ppobj
|
neuper@41940
|
59 |
FROM loc : istate option * istate option,
|
neuper@41940
|
60 |
TO loc : (istate * ctxt) option * (istate * ctxt) option,
|
neuper@41940
|
61 |
e.g.
|
neuper@41940
|
62 |
FROM val pt = Nd (PblObj
|
neuper@41940
|
63 |
{.., loc = (SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)),
|
neuper@41940
|
64 |
NONE),
|
neuper@41940
|
65 |
TO val pt = Nd (PblObj
|
neuper@41940
|
66 |
{.., loc =
|
neuper@41940
|
67 |
((SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)), ctxt),
|
neuper@41940
|
68 |
NONE),
|
neuper@41940
|
69 |
*)
|
neuper@41940
|
70 |
|
neuper@41940
|
71 |
"===== interactive specification: from origin to specification (probl)";
|
neuper@41940
|
72 |
val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
73 |
(*nxt =("Add_Given", Model_Problem)*)
|
neuper@41940
|
74 |
val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
75 |
(*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
|
neuper@41940
|
76 |
"----- ";
|
neuper@41940
|
77 |
(* call sequence: me Model_Problem
|
neuper@41940
|
78 |
> me ("Add_Given", Add_Given "realTestGiven (((1 + 2) * 4 / 3) ^^^ 2)")
|
neuper@41940
|
79 |
> locatetac tac
|
neuper@41940
|
80 |
> loc_specify_
|
neuper@41940
|
81 |
> specify GET ctxt (stored in ctree)
|
neuper@41940
|
82 |
> specify_additem
|
neuper@41940
|
83 |
> appl_add
|
neuper@41940
|
84 |
|
neuper@41940
|
85 |
*)
|
neuper@41940
|
86 |
"----- in appl_add";
|
neuper@41940
|
87 |
(* FROM appl_add thy
|
neuper@41940
|
88 |
TO appl_add ctxt
|
neuper@41940
|
89 |
FROM parse thy str
|
neuper@41940
|
90 |
TO parseNEW ctxt str
|
neuper@41940
|
91 |
*)
|
neuper@41940
|
92 |
val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
93 |
(*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
|
neuper@41940
|
94 |
val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
95 |
(*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)
|
neuper@41940
|
96 |
|
neuper@41940
|
97 |
"===== end specify: from specification (probl) to guard (method)";
|
neuper@41940
|
98 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
99 |
(*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*)
|
neuper@41940
|
100 |
|
neuper@41940
|
101 |
"===== start interpretation: from guard to environment";
|
neuper@41940
|
102 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
103 |
(*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*)
|
neuper@41940
|
104 |
"----- ";
|
neuper@41940
|
105 |
(* call sequence: me ("Apply_Method",...
|
neuper@41940
|
106 |
> locatetac
|
neuper@41940
|
107 |
> loc_solve_
|
neuper@41940
|
108 |
> solve ("Apply_Method",...
|
neuper@41940
|
109 |
*)
|
neuper@41940
|
110 |
val ((_,tac), ptp) = (nxt, (pt, p));
|
neuper@41940
|
111 |
locatetac tac (pt,p);
|
neuper@41940
|
112 |
val (mI, m) = mk_tac'_ tac;
|
neuper@41940
|
113 |
val Appl m = applicable_in p pt m;
|
neuper@41940
|
114 |
member op = specsteps mI;
|
neuper@41940
|
115 |
loc_solve_ (mI,m) ptp;
|
neuper@41940
|
116 |
val (m, (pt, pos)) = ((mI,m), ptp);
|
neuper@41940
|
117 |
solve m (pt, pos);
|
bonzai@41949
|
118 |
val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) =
|
neuper@41940
|
119 |
(m, (pt, pos));
|
neuper@41940
|
120 |
val {srls,...} = get_met mI;
|
neuper@41940
|
121 |
val PblObj{meth=itms,...} = get_obj I pt p;
|
neuper@41940
|
122 |
val thy' = get_obj g_domID pt p;
|
neuper@41940
|
123 |
val thy = assoc_thy thy';
|
bonzai@41949
|
124 |
val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
|
neuper@41940
|
125 |
|
neuper@41940
|
126 |
"----- go on in the calculation";
|
neuper@41940
|
127 |
val (p,_,f,nxt,_,pt) = me nxt pos [1] pt;
|
neuper@41940
|
128 |
(*nxt = ("Calculate",Calculate "PLUS")*)
|
neuper@41940
|
129 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
130 |
(*nxt = ("Calculate",Calculate "TIMES")*)
|
neuper@41940
|
131 |
|
neuper@41940
|
132 |
"===== input a formula to be derived from previous istate";
|
neuper@41940
|
133 |
"----- appendFormula TODO: first repair error";
|
neuper@41940
|
134 |
val cs = ((pt,p),[]);
|
neuper@41940
|
135 |
val ("ok", cs' as (_,_,(pt,p))) = step p cs;
|
neuper@41943
|
136 |
val ifo = (* encode "4^^^2" \<longrightarrow>*) "4^2";
|
neuper@41940
|
137 |
(*
|
neuper@41943
|
138 |
val ("no derivation found", (_,_,(pt, p))) = inform cs' ((*encode*) ifo);
|
neuper@41940
|
139 |
here ^^^^^^^^^^^^^^^^^^^^^ should be "ok"
|
neuper@41940
|
140 |
*)
|
neuper@41940
|
141 |
|
neuper@41940
|
142 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
143 |
(*nxt = ("Calculate",Calculate "DIVIDE")*)
|
neuper@41940
|
144 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
145 |
(*nxt = ("Calculate",Calculate "POWER")*)
|
neuper@41940
|
146 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
147 |
(*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)
|
neuper@41940
|
148 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
149 |
(*nxt = ("End_Proof'",End_Proof')*)
|
neuper@41940
|
150 |
if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then ()
|
neuper@41940
|
151 |
else error "calculate.sml: script test_calculate changed behaviour";
|
neuper@41940
|
152 |
|
neuper@41940
|
153 |
"===== tactic Subproblem: from environment to origin";
|
neuper@41940
|
154 |
"----- TODO";
|
neuper@41940
|
155 |
|
neuper@37906
|
156 |
|
neuper@38065
|
157 |
"----------- debugging setContext..pbl_ -----------------";
|
neuper@38065
|
158 |
"----------- debugging setContext..pbl_ -----------------";
|
neuper@38065
|
159 |
"----------- debugging setContext..pbl_ -----------------";
|
neuper@37906
|
160 |
states:=[];
|
neuper@41970
|
161 |
CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
|
neuper@41970
|
162 |
("Test", ["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
163 |
["Test","squ-equ-test-subpbl1"]))];
|
neuper@37906
|
164 |
Iterator 1;
|
neuper@37906
|
165 |
moveActiveRoot 1; modelProblem 1;
|
neuper@37906
|
166 |
|
neuper@37906
|
167 |
val pos as (p,_) = ([],Pbl);
|
neuper@37906
|
168 |
val guh = "pbl_equ_univ";
|
neuper@37906
|
169 |
checkContext 1 pos guh;
|
neuper@37906
|
170 |
val ((pt,_),_) = get_calc 1;
|
neuper@37906
|
171 |
val pp = par_pblobj pt p;
|
neuper@37906
|
172 |
val keID = guh2kestoreID guh;
|
neuper@37906
|
173 |
case context_pbl keID pt pp of (true,["univariate", "equation"],_,_,_)=>()
|
neuper@38031
|
174 |
| _ => error "mathengine.sml: context_pbl .. pbl_equ_univ checked";
|
neuper@37906
|
175 |
|
neuper@37906
|
176 |
case get_obj g_spec pt p of (_, ["e_pblID"], _) => ()
|
neuper@38031
|
177 |
| _ => error "mathengine.sml: context_pbl .. pbl still empty";
|
neuper@37906
|
178 |
setContext 1 pos guh;
|
neuper@37906
|
179 |
val ((pt,_),_) = get_calc 1;
|
neuper@37906
|
180 |
case get_obj g_spec pt p of (_, ["univariate", "equation"], _) => ()
|
neuper@38031
|
181 |
| _ => error "mathengine.sml: context_pbl .. pbl set";
|
neuper@37906
|
182 |
|
neuper@37906
|
183 |
|
neuper@37906
|
184 |
setContext 1 pos "met_eq_lin";
|
neuper@37906
|
185 |
val ((pt,_),_) = get_calc 1;
|
neuper@37906
|
186 |
case get_obj g_spec pt p of (_, _, ["LinEq", "solve_lineq_equation"]) => ()
|
neuper@38031
|
187 |
| _ => error "mathengine.sml: context_pbl .. pbl set";
|
neuper@37906
|
188 |
|
neuper@37906
|
189 |
|
neuper@38065
|
190 |
"----------- tryrefine ----------------------------------";
|
neuper@38065
|
191 |
"----------- tryrefine ----------------------------------";
|
neuper@38065
|
192 |
"----------- tryrefine ----------------------------------";
|
neuper@37906
|
193 |
states:=[];
|
neuper@37906
|
194 |
CalcTree [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
|
neuper@37906
|
195 |
"solveFor x", "solutions L"],
|
neuper@38058
|
196 |
("RatEq",["univariate","equation"],["no_met"]))];
|
neuper@37906
|
197 |
Iterator 1;
|
neuper@37906
|
198 |
moveActiveRoot 1; autoCalculate 1 CompleteCalc;
|
neuper@37906
|
199 |
|
neuper@37906
|
200 |
refineProblem 1 ([1],Res) "pbl_equ_univ"
|
neuper@37906
|
201 |
(*gives "pbl_equ_univ_rat" correct*);
|
neuper@37906
|
202 |
|
neuper@55279
|
203 |
refineProblem 1 ([1],Res) (pblID2guh ["LINEAR","univariate","equation"])
|
neuper@38065
|
204 |
(*gives "pbl_equ_univ_lin" incorrect*);
|
neuper@38065
|
205 |
|
neuper@38065
|
206 |
|
neuper@41982
|
207 |
"----------- fun step: Apply_Method without init_form ---";
|
neuper@41982
|
208 |
"----------- fun step: Apply_Method without init_form ---";
|
neuper@41982
|
209 |
"----------- fun step: Apply_Method without init_form ---";
|
neuper@41982
|
210 |
val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
|
neuper@41982
|
211 |
val (dI',pI',mI') =
|
neuper@41982
|
212 |
("Test", ["sqroot-test","univariate","equation","test"],
|
neuper@41982
|
213 |
["Test","squ-equ-test-subpbl1"]);
|
neuper@41982
|
214 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@41982
|
215 |
"~~~~~ fun me, args:"; val (_,tac) = nxt;
|
neuper@41982
|
216 |
val ("ok", (_, _, (pt, p))) = locatetac tac (pt,p);
|
neuper@41982
|
217 |
"~~~~~ fun step, args:"; val (ip as (_,p_), ptp as (pt,p), tacis) = (p, (pt, e_pos'), []);
|
neuper@41982
|
218 |
val pIopt = get_pblID (pt,ip);
|
neuper@41982
|
219 |
ip = ([],Res) (*false*);
|
neuper@41982
|
220 |
val SOME pI = pIopt;
|
neuper@48895
|
221 |
(*========== inhibit exn AK110718 ==============================================
|
neuper@41982
|
222 |
member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p))
|
neuper@41982
|
223 |
(*^^^^^^^^: Apply_Method without init_form*)
|
neuper@48895
|
224 |
========== inhibit exn AK110718 ==============================================*)
|
neuper@38065
|
225 |
|
neuper@38065
|
226 |
"----------- fun step -----------------------------------";
|
neuper@38065
|
227 |
"----------- fun step -----------------------------------";
|
neuper@38065
|
228 |
"----------- fun step -----------------------------------";
|
neuper@38065
|
229 |
val p = e_pos'; val c = [];
|
neuper@38065
|
230 |
val (p,_,f,nxt,_,pt) =
|
neuper@38065
|
231 |
CalcTreeTEST
|
neuper@38065
|
232 |
[(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
|
neuper@38065
|
233 |
("Integrate", ["integrate","function"], ["diff","integration"]))];
|
neuper@38065
|
234 |
"----- step 1: returns tac = Model_Problem ---";
|
neuper@38065
|
235 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
236 |
"----- step 2: returns tac = ---";
|
neuper@38065
|
237 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
238 |
"----- step 3: returns tac = ---";
|
neuper@38065
|
239 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
240 |
"----- step 4: returns tac = ---";
|
neuper@38065
|
241 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
242 |
"----- step 5: returns tac = ---";
|
neuper@38065
|
243 |
|
neuper@48895
|
244 |
(*========== inhibit exn AK110718 ==============================================
|
neuper@38066
|
245 |
2002 stops here as well: TODO review actual arguments:
|
neuper@38065
|
246 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
247 |
"----- step 6: returns tac = ---";
|
neuper@38065
|
248 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
249 |
"----- step 7: returns tac = ---";
|
neuper@38065
|
250 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
251 |
"----- step 8: returns tac = ---";
|
neuper@38065
|
252 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@48895
|
253 |
========== inhibit exn AK110718 ==============================================*)
|
neuper@38065
|
254 |
|
neuper@38065
|
255 |
|
neuper@38065
|
256 |
"----------- fun autocalc -------------------------------";
|
neuper@38065
|
257 |
"----------- fun autocalc -------------------------------";
|
neuper@38065
|
258 |
"----------- fun autocalc -------------------------------";
|
neuper@38065
|
259 |
val p = e_pos'; val c = [];
|
neuper@38065
|
260 |
val (p,_,f,nxt,_,pt) =
|
neuper@38065
|
261 |
CalcTreeTEST
|
neuper@38065
|
262 |
[(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
|
neuper@38065
|
263 |
("Integrate",["integrate","function"], ["diff","integration"]))];
|
neuper@38066
|
264 |
(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
|
neuper@38066
|
265 |
modeling is skipped FIXME
|
neuper@38066
|
266 |
*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
|
neuper@38065
|
267 |
tracing "----- step 1 ---";
|
neuper@38065
|
268 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@38065
|
269 |
tracing "----- step 2 ---";
|
neuper@38065
|
270 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@38065
|
271 |
tracing "----- step 3 ---";
|
neuper@38065
|
272 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@38065
|
273 |
tracing "----- step 4 ---";
|
neuper@38065
|
274 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@38065
|
275 |
tracing "----- step 5 ---";
|
neuper@38065
|
276 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@38065
|
277 |
tracing "----- step 6 ---";
|
neuper@38065
|
278 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@38065
|
279 |
tracing "----- step 7 ---";
|
neuper@38065
|
280 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@38065
|
281 |
tracing "----- step 8 ---";
|
neuper@38065
|
282 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@48895
|
283 |
(*========== inhibit exn AK110718 ==============================================
|
neuper@42067
|
284 |
WN110628: Integration does not work, see Knowledge/integrate.sml
|
neuper@42067
|
285 |
|
neuper@41929
|
286 |
if str = "end-of-calculation" andalso
|
neuper@41929
|
287 |
term2str (get_obj g_res pt (fst p)) = "c + x + 1 / 3 * x ^^^ 3" then ()
|
neuper@38065
|
288 |
else error "mathengine.sml -- fun autocalc -- end";
|
neuper@48895
|
289 |
========== inhibit exn AK110718 ==============================================*)
|
neuper@38065
|
290 |
|
neuper@38065
|
291 |
|
neuper@38065
|
292 |
"----------- fun autoCalculate -----------------------------------";
|
neuper@38065
|
293 |
"----------- fun autoCalculate -----------------------------------";
|
neuper@38065
|
294 |
"----------- fun autoCalculate -----------------------------------";
|
neuper@38065
|
295 |
states := [];
|
neuper@38065
|
296 |
CalcTree (*ATTENTION: encode_fmz ... unlike CalcTreeTEST*)
|
neuper@38065
|
297 |
[(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
|
neuper@38065
|
298 |
("Integrate", ["integrate", "function"], ["diff", "integration"]))];
|
neuper@38065
|
299 |
Iterator 1;
|
neuper@38065
|
300 |
moveActiveRoot 1;
|
neuper@38066
|
301 |
(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
|
neuper@38066
|
302 |
modeling is skipped FIXME
|
neuper@38066
|
303 |
see test/../interface -- solve_linear as rootpbl FE -- for OTHER expl:
|
neuper@38066
|
304 |
setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
|
neuper@38066
|
305 |
autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
|
neuper@38066
|
306 |
|
neuper@38066
|
307 |
fetchProposedTactic 1;
|
neuper@38066
|
308 |
setNextTactic 1 (Add_Given "solveFor x");
|
neuper@38066
|
309 |
autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
|
neuper@38066
|
310 |
|
neuper@38066
|
311 |
fetchProposedTactic 1;
|
neuper@38066
|
312 |
setNextTactic 1 (Add_Find "solutions L");
|
neuper@38066
|
313 |
autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
|
neuper@38066
|
314 |
|
neuper@38066
|
315 |
fetchProposedTactic 1;
|
neuper@38066
|
316 |
setNextTactic 1 (Specify_Theory "Test");
|
neuper@38066
|
317 |
autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
|
neuper@38066
|
318 |
*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
|
neuper@38065
|
319 |
autoCalculate 1 (Step 1);
|
neuper@38065
|
320 |
"----- step 1 ---";
|
neuper@38065
|
321 |
autoCalculate 1 (Step 1);
|
neuper@38065
|
322 |
"----- step 2 ---";
|
neuper@38065
|
323 |
autoCalculate 1 (Step 1);
|
neuper@38065
|
324 |
"----- step 3 ---";
|
neuper@38065
|
325 |
autoCalculate 1 (Step 1);
|
neuper@38065
|
326 |
"----- step 4 ---";
|
neuper@38065
|
327 |
autoCalculate 1 (Step 1);
|
neuper@38065
|
328 |
"----- step 5 ---";
|
neuper@38065
|
329 |
autoCalculate 1 (Step 1);
|
neuper@38065
|
330 |
"----- step 6 ---";
|
neuper@38065
|
331 |
autoCalculate 1 (Step 1);
|
neuper@38065
|
332 |
"----- step 7 ---";
|
neuper@38065
|
333 |
autoCalculate 1 (Step 1);
|
neuper@38065
|
334 |
"----- step 8 ---";
|
neuper@38065
|
335 |
autoCalculate 1 (Step 1);
|
neuper@38065
|
336 |
val (ptp as (_, p), _) = get_calc 1;
|
neuper@38065
|
337 |
val (Form t,_,_) = pt_extract ptp;
|
akargl@42108
|
338 |
|
neuper@38065
|
339 |
if term2str t = "c + x + 1 / 3 * x ^^^ 3" andalso p = ([], Res) then ()
|
neuper@38065
|
340 |
else error "mathengine.sml -- fun autoCalculate -- end";
|
neuper@38065
|
341 |
|
neuper@42067
|
342 |
"----------- fun autoCalculate..CompleteCalc ------------";
|
neuper@42067
|
343 |
"----------- fun autoCalculate..CompleteCalc ------------";
|
neuper@42067
|
344 |
"----------- fun autoCalculate..CompleteCalc ------------";
|
neuper@42067
|
345 |
states:=[];
|
neuper@42067
|
346 |
CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
|
neuper@42067
|
347 |
("Test", ["sqroot-test","univariate","equation","test"],
|
neuper@42067
|
348 |
["Test","squ-equ-test-subpbl1"]))];
|
neuper@42067
|
349 |
Iterator 1;
|
neuper@42103
|
350 |
moveActiveRoot 1;
|
neuper@42103
|
351 |
(*autoCalculate 1 CompleteCalc; (*WAS <SYSERROR>..<ERROR> error in kernel </ERROR>*)*)
|
neuper@42103
|
352 |
"~~~~~ fun autoCalculate, args:"; val (cI, auto) = (1, CompleteCalc);
|
neuper@42103
|
353 |
val pold = get_pos cI 1;
|
neuper@42103
|
354 |
(*autocalc [] pold (get_calc cI) auto; (*WAS Type unification failed
|
neuper@42103
|
355 |
Type error in application: incompatible operand type
|
neuper@42103
|
356 |
Operator: solveFor :: real \<Rightarrow> una
|
neuper@42103
|
357 |
Operand: x :: 'a *)*)
|
neuper@42103
|
358 |
"~~~~~ fun autocalc, args:"; val (c, (pos as (_,p_)), ((pt,_), _), auto)
|
neuper@42103
|
359 |
= ([] : pos' list, pold, (get_calc cI), auto);
|
neuper@42103
|
360 |
autoord auto > 3 andalso just_created (pt, pos); (*true*)
|
neuper@42103
|
361 |
val ptp = all_modspec (pt, pos);
|
neuper@42103
|
362 |
"TODO all_modspec: preconds for rootpbl";
|
neuper@42103
|
363 |
(*all_solve auto c ptp; (*WAS Type unification failed...*)*)
|
neuper@42103
|
364 |
"~~~~~ and all_solve, args:"; val (auto, c, (ptp as (pt, pos as (p,_)))) =
|
neuper@42103
|
365 |
(auto, c, ptp);
|
neuper@42103
|
366 |
val (_,_,mI) = get_obj g_spec pt p
|
neuper@42103
|
367 |
val ctxt = get_ctxt pt pos
|
neuper@42103
|
368 |
val (ttt, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp;
|
neuper@42103
|
369 |
(* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*) pos = ([], Met)*)
|
neuper@42103
|
370 |
"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
|
neuper@42103
|
371 |
(auto, (c @ c'), ptp);
|
neuper@42103
|
372 |
p = ([], Res) (*false p = ([1], Frm)*);
|
neuper@42103
|
373 |
member op = [Pbl,Met] p_ (*false*);
|
neuper@42103
|
374 |
val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "norm_equation"*)
|
neuper@42103
|
375 |
(* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
|
neuper@42103
|
376 |
"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
|
neuper@42103
|
377 |
(auto, (c @ c'), ptp');
|
neuper@42103
|
378 |
p = ([], Res) (*false p = ([1], Res)*);
|
neuper@42103
|
379 |
member op = [Pbl,Met] p_ (*false*);
|
neuper@42103
|
380 |
val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "Test_simplify"*)
|
neuper@42103
|
381 |
(* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
|
neuper@42103
|
382 |
"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
|
neuper@42103
|
383 |
(auto, (c @ c'), ptp');
|
neuper@42103
|
384 |
p = ([], Res) (*false p = ([2], Res)*);
|
neuper@42103
|
385 |
member op = [Pbl,Met] p_ (*false*);
|
neuper@42103
|
386 |
val ((Subproblem _, tac_, (_, is))::_, c', ptp') = nxt_solve_ ptp;
|
neuper@42103
|
387 |
autoord auto < 5 (*false*);
|
neuper@42103
|
388 |
(* val ptp = all_modspec ptp' (*WAS Type unification failed...*)*)
|
neuper@42103
|
389 |
"~~~~~ fun all_modspec, args:"; val (pt, pos as (p,_)) = (ptp');
|
neuper@42103
|
390 |
val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;
|
neuper@42103
|
391 |
val thy = assoc_thy dI;
|
neuper@42103
|
392 |
val {ppc, ...} = get_met mI;
|
neuper@42103
|
393 |
(* val (mors, ctxt) = prep_ori fmz_ thy ppc; WAS Type unification failed because
|
neuper@48761
|
394 |
val ctxt' = dI |> Thy_Info.get_theory |> Proof_Context.init_global;
|
neuper@42103
|
395 |
(parseNEW ctxt' "x" |> the |> type_of) = TFree ("'a",[]);
|
neuper@42103
|
396 |
^^^^^ *)
|
neuper@42103
|
397 |
(*vvv from: | assod pt _ (Subproblem'...*)
|
neuper@42103
|
398 |
val (fmz_, vals) = oris2fmz_vals pors;
|
neuper@42103
|
399 |
(**)
|
neuper@48761
|
400 |
val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global
|
neuper@42103
|
401 |
|> declare_constraints' vals
|
neuper@42103
|
402 |
(**)
|
neuper@42103
|
403 |
(*^^^ from: | assod pt _ (Subproblem'...*)
|
neuper@42103
|
404 |
val [(1, [1], "#Given", dsc_eq, [equality]),
|
neuper@42103
|
405 |
(2, [1], "#Given", dsc_solvefor, [xxx]),
|
neuper@42103
|
406 |
(3, [1], "#Find", dsc_solutions, [x_i])] = pors;
|
neuper@42103
|
407 |
if term2str xxx = "x" andalso type_of xxx = HOLogic.realT then ()
|
neuper@42103
|
408 |
else error "autoCalculate..CompleteCalc: SubProblem broken 1";
|
neuper@42103
|
409 |
val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
|
neuper@42103
|
410 |
val pt = update_metppc pt p (map (ori2Coritm ppc) pors);
|
neuper@42103
|
411 |
val pt = update_spec pt p (dI,pI,mI);
|
neuper@42103
|
412 |
val pt = update_ctxt pt p ctxt;
|
neuper@42103
|
413 |
"~~~~~ return to complete_solve, args:"; val (ptp) = (pt, (p,Met));
|
neuper@42103
|
414 |
val (msg, c, (pt, p)) = complete_solve auto (c @ c') ptp;
|
neuper@42103
|
415 |
if msg = "end-of-calculation" andalso c = [] andalso p = ([], Res) then ()
|
neuper@42103
|
416 |
else error "autoCalculate..CompleteCalc: final result";
|
neuper@42103
|
417 |
if terms2strs (get_assumptions_ pt p) =
|
neuper@42105
|
418 |
["matches (?a = ?b) (-1 + x = 0)", (*precond of submet*)
|
neuper@42104
|
419 |
"x = 1", (*result of subpbl and rootpbl*)
|
neuper@42104
|
420 |
"precond_rootmet x"] (*precond of rootmet*)
|
neuper@42103
|
421 |
then () else error "autoCalculate..CompleteCalc: ctxt at final result";
|
neuper@42067
|
422 |
|
akargl@42108
|
423 |
|
neuper@42394
|
424 |
"--------- search for Or_to_List ------------------------";
|
neuper@42394
|
425 |
"--------- search for Or_to_List ------------------------";
|
t@42225
|
426 |
"--------- search for Or_to_List ------------------------";
|
t@42225
|
427 |
val fmz = ["equality (x^^^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"];
|
t@42225
|
428 |
val (dI',pI',mI') = ("Isac", ["univariate","equation"], ["no_met"])
|
t@42225
|
429 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
t@42225
|
430 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
431 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
432 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
433 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
434 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
435 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
436 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
437 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
438 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
439 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
|
t@42225
|
440 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
441 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
442 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
443 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
444 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
445 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
446 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
447 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
448 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
449 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
t@42225
|
450 |
"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW(*remove*)), (pt:ptree)) =
|
t@42225
|
451 |
(nxt, p, [], pt);
|
t@42225
|
452 |
val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
|
t@42225
|
453 |
val (pt, p) = ptp;
|
t@42225
|
454 |
"~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
|
t@42225
|
455 |
(p, ((pt, e_pos'),[]));
|
t@42225
|
456 |
val pIopt = get_pblID (pt,ip);
|
t@42225
|
457 |
ip = ([],Res); (*false*)
|
t@42225
|
458 |
ip = p; (*false*)
|
t@42225
|
459 |
member op = [Pbl,Met] p_; (*false*)
|
t@42225
|
460 |
"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
|
t@42225
|
461 |
e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
|
t@42225
|
462 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
t@42225
|
463 |
val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
|
t@42225
|
464 |
val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is; (*WAS Empty_Tac_: tac_*)
|
t@42225
|
465 |
case tac_ of Or_to_List' _ => ()
|
t@42225
|
466 |
| _ => error "Or_to_List broken ?"
|
akargl@42108
|
467 |
|
neuper@42394
|
468 |
|
neuper@42279
|
469 |
"----------- check thy in CalcTreeTEST ------------------";
|
neuper@42279
|
470 |
"----------- check thy in CalcTreeTEST ------------------";
|
neuper@42279
|
471 |
"----------- check thy in CalcTreeTEST ------------------";
|
neuper@42279
|
472 |
"WN1109 with Inverse_Z_Transform.thy when starting tests with CalcTreeTEST \n" ^
|
neuper@42279
|
473 |
"we got the message: ME_Isa: thy 'Build_Inverse_Z_Transform' not in system \n" ^
|
neuper@42279
|
474 |
"Below there are the steps which found out the reason: \n" ^
|
neuper@42279
|
475 |
"store_pbt mistakenly stored that theory.";
|
neuper@48761
|
476 |
val ctxt = Proof_Context.init_global @{theory Isac};
|
neuper@42279
|
477 |
val SOME t = parseNEW ctxt "filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))";
|
neuper@42279
|
478 |
val SOME t = parseNEW ctxt "stepResponse (x[n::real]::bool)";
|
akargl@42108
|
479 |
|
neuper@42279
|
480 |
val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
|
neuper@42279
|
481 |
"stepResponse (x[n::real]::bool)"];
|
neuper@42405
|
482 |
val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
|
neuper@42405
|
483 |
["SignalProcessing","Z_Transform","Inverse"]);
|
neuper@42279
|
484 |
|
neuper@42279
|
485 |
val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
|
neuper@42279
|
486 |
(*WAS ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
|
neuper@42279
|
487 |
|
neuper@42279
|
488 |
"~~~~~ T fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI,pI,mI))];
|
neuper@42279
|
489 |
"~~~~~ fun nxt_specify_init_calc, args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
|
neuper@42279
|
490 |
val thy = assoc_thy dI;
|
neuper@42279
|
491 |
mI = ["no_met"]; (*false*)
|
neuper@42279
|
492 |
val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
|
neuper@42279
|
493 |
val {cas, ppc, thy=thy',...} = get_pbt pI; (*take dI from _refined_ pbl*)
|
neuper@42279
|
494 |
"tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*)
|
neuper@42279
|
495 |
val dI = theory2theory' (maxthy thy thy');
|
neuper@42279
|
496 |
"tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
|
neuper@42279
|
497 |
cas = NONE; (*true*)
|
neuper@42279
|
498 |
val hdl = pblterm dI pI;
|
neuper@42279
|
499 |
val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
|
neuper@42279
|
500 |
(pors, (dI, pI, mI), hdl)
|
neuper@42279
|
501 |
val pt = update_ctxt pt [] pctxt;
|
neuper@42279
|
502 |
|
neuper@42279
|
503 |
"~~~~~ fun nxt_specif, args:"; val ((tac as Model_Problem), (pt, pos as (p,p_))) = (Model_Problem, (pt, ([], Pbl)));
|
neuper@42279
|
504 |
val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p;
|
neuper@42279
|
505 |
"tracing bottom up"; #1(ospec) = "Build_Inverse_Z_Transform"; (*WAS true*)
|
neuper@42279
|
506 |
|
neuper@42279
|
507 |
"~~~~~ fun some_spec, args:"; val ((odI, opI, omI), (dI, pI, mI)) = (ospec, spec);
|
neuper@42279
|
508 |
dI = e_domID; (*true*)
|
neuper@42279
|
509 |
odI = "Build_Inverse_Z_Transform"; (*true*)
|
neuper@42279
|
510 |
dI = "e_domID"; (*true*)
|
neuper@42279
|
511 |
"~~~~~ after fun some_spec:";
|
neuper@42279
|
512 |
val (dI, pI, mI) = some_spec ospec spec;
|
neuper@42279
|
513 |
"tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
|
neuper@42279
|
514 |
val thy = assoc_thy dI; (*caused ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
|
neuper@42279
|
515 |
|