neuper@37906
|
1 |
(* test for sml/ME/mathengine.sml
|
neuper@37906
|
2 |
authors: Walther Neuper 2000, 2006
|
neuper@37906
|
3 |
(c) due to copyright terms
|
neuper@37906
|
4 |
*)
|
neuper@41940
|
5 |
(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
|
neuper@37906
|
6 |
|
neuper@38065
|
7 |
"--------------------------------------------------------";
|
neuper@38065
|
8 |
"table of contents --------------------------------------";
|
neuper@38065
|
9 |
"--------------------------------------------------------";
|
neuper@41940
|
10 |
"----------- change to parse ctxt -----------------------";
|
neuper@38065
|
11 |
"----------- debugging setContext..pbl_ -----------------";
|
neuper@38065
|
12 |
"----------- tryrefine ----------------------------------";
|
neuper@38065
|
13 |
"----------- fun step -----------------------------------";
|
neuper@38065
|
14 |
"----------- fun autocalc -------------------------------";
|
neuper@38065
|
15 |
"----------- fun autoCalculate --------------------------";
|
neuper@38065
|
16 |
"--------------------------------------------------------";
|
neuper@38065
|
17 |
"--------------------------------------------------------";
|
neuper@38065
|
18 |
"--------------------------------------------------------";
|
neuper@37906
|
19 |
|
neuper@41940
|
20 |
"----------- change to parse ctxt -----------------------";
|
neuper@41940
|
21 |
"----------- change to parse ctxt -----------------------";
|
neuper@41940
|
22 |
"----------- change to parse ctxt -----------------------";
|
neuper@41940
|
23 |
-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
|
neuper@41940
|
24 |
"===== start calculation: from problem description (fmz) to origin";
|
neuper@41940
|
25 |
val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
|
neuper@41940
|
26 |
val (thyID, pblID, metID) =
|
neuper@41940
|
27 |
("Test", ["calculate", "test"], ["Test", "test_calculate"]);
|
neuper@41940
|
28 |
val (p,_,_,nxt,_,pt) = CalcTreeTEST [(fmz, (thyID, pblID, metID))];
|
neuper@41940
|
29 |
"----- ";
|
neuper@41940
|
30 |
(* call sequence: CalcTreeTEST
|
neuper@41940
|
31 |
> nxt_specify_init_calc
|
neuper@41940
|
32 |
> prep_ori
|
neuper@41940
|
33 |
*)
|
neuper@41940
|
34 |
val (thy, pbt) = (Thy_Info.get_theory thyID, (#ppc o get_pbt) pblID);
|
neuper@41940
|
35 |
"----- in prep_ori";
|
neuper@41940
|
36 |
val ctxt = ProofContext.init_global thy;
|
neuper@41940
|
37 |
|
neuper@41940
|
38 |
val ctopts = map (parse thy) fmz;
|
neuper@41940
|
39 |
val dts = map ((split_dts thy) o term_of o the) ctopts;
|
neuper@41940
|
40 |
(*split_dts:
|
neuper@41940
|
41 |
(term * term list) list
|
neuper@41940
|
42 |
formulas: e.g. ((1+2)*4/3)^^^2
|
neuper@41940
|
43 |
description: e.g. realTestGiven
|
neuper@41940
|
44 |
*)
|
neuper@41940
|
45 |
prep_ori;
|
neuper@41940
|
46 |
(* FROM
|
neuper@41940
|
47 |
val it = fn:
|
neuper@41940
|
48 |
string list -> theory -> (string * (term * 'a)) list -> ori list
|
neuper@41940
|
49 |
TO
|
neuper@41940
|
50 |
val it = fn:
|
neuper@41940
|
51 |
string list -> theory -> (string * (term * 'a)) list -> (ori list * ctxt)
|
neuper@41940
|
52 |
AND
|
neuper@41940
|
53 |
FROM val oris = prep_ori...
|
neuper@41940
|
54 |
TO val (oris, _) = prep_ori...
|
neuper@41940
|
55 |
*)
|
neuper@41940
|
56 |
"----- insert ctxt in ptree";
|
neuper@41940
|
57 |
(* datatype ppobj
|
neuper@41940
|
58 |
FROM loc : istate option * istate option,
|
neuper@41940
|
59 |
TO loc : (istate * ctxt) option * (istate * ctxt) option,
|
neuper@41940
|
60 |
e.g.
|
neuper@41940
|
61 |
FROM val pt = Nd (PblObj
|
neuper@41940
|
62 |
{.., loc = (SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)),
|
neuper@41940
|
63 |
NONE),
|
neuper@41940
|
64 |
TO val pt = Nd (PblObj
|
neuper@41940
|
65 |
{.., loc =
|
neuper@41940
|
66 |
((SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)), ctxt),
|
neuper@41940
|
67 |
NONE),
|
neuper@41940
|
68 |
*)
|
neuper@41940
|
69 |
|
neuper@41940
|
70 |
"===== interactive specification: from origin to specification (probl)";
|
neuper@41940
|
71 |
val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
72 |
(*nxt =("Add_Given", Model_Problem)*)
|
neuper@41940
|
73 |
val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
74 |
(*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
|
neuper@41940
|
75 |
"----- ";
|
neuper@41940
|
76 |
(* call sequence: me Model_Problem
|
neuper@41940
|
77 |
> me ("Add_Given", Add_Given "realTestGiven (((1 + 2) * 4 / 3) ^^^ 2)")
|
neuper@41940
|
78 |
> locatetac tac
|
neuper@41940
|
79 |
> loc_specify_
|
neuper@41940
|
80 |
> specify GET ctxt (stored in ctree)
|
neuper@41940
|
81 |
> specify_additem
|
neuper@41940
|
82 |
> appl_add
|
neuper@41940
|
83 |
|
neuper@41940
|
84 |
*)
|
neuper@41940
|
85 |
"----- in appl_add";
|
neuper@41940
|
86 |
(* FROM appl_add thy
|
neuper@41940
|
87 |
TO appl_add ctxt
|
neuper@41940
|
88 |
FROM parse thy str
|
neuper@41940
|
89 |
TO parseNEW ctxt str
|
neuper@41940
|
90 |
*)
|
neuper@41940
|
91 |
val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
92 |
(*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
|
neuper@41940
|
93 |
val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
94 |
(*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)
|
neuper@41940
|
95 |
|
neuper@41940
|
96 |
"===== end specify: from specification (probl) to guard (method)";
|
neuper@41940
|
97 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
98 |
(*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*)
|
neuper@41940
|
99 |
|
neuper@41940
|
100 |
"===== start interpretation: from guard to environment";
|
neuper@41940
|
101 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
102 |
(*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*)
|
neuper@41940
|
103 |
"----- ";
|
neuper@41940
|
104 |
(* call sequence: me ("Apply_Method",...
|
neuper@41940
|
105 |
> locatetac
|
neuper@41940
|
106 |
> loc_solve_
|
neuper@41940
|
107 |
> solve ("Apply_Method",...
|
neuper@41940
|
108 |
*)
|
neuper@41940
|
109 |
val ((_,tac), ptp) = (nxt, (pt, p));
|
neuper@41940
|
110 |
locatetac tac (pt,p);
|
neuper@41940
|
111 |
val (mI, m) = mk_tac'_ tac;
|
neuper@41940
|
112 |
val Appl m = applicable_in p pt m;
|
neuper@41940
|
113 |
member op = specsteps mI;
|
neuper@41940
|
114 |
loc_solve_ (mI,m) ptp;
|
neuper@41940
|
115 |
val (m, (pt, pos)) = ((mI,m), ptp);
|
neuper@41940
|
116 |
solve m (pt, pos);
|
neuper@41940
|
117 |
val ((_, m as Apply_Method' (mI, _, _)), (pt, (pos as (p,_)))) =
|
neuper@41940
|
118 |
(m, (pt, pos));
|
neuper@41940
|
119 |
val {srls,...} = get_met mI;
|
neuper@41940
|
120 |
val PblObj{meth=itms,...} = get_obj I pt p;
|
neuper@41940
|
121 |
val thy' = get_obj g_domID pt p;
|
neuper@41940
|
122 |
val thy = assoc_thy thy';
|
neuper@41940
|
123 |
val (is as ScrState (env,_,_,_,_,_), sc) = init_scrstate thy itms mI;
|
neuper@41940
|
124 |
|
neuper@41940
|
125 |
"----- go on in the calculation";
|
neuper@41940
|
126 |
val (p,_,f,nxt,_,pt) = me nxt pos [1] pt;
|
neuper@41940
|
127 |
(*nxt = ("Calculate",Calculate "PLUS")*)
|
neuper@41940
|
128 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
129 |
(*nxt = ("Calculate",Calculate "TIMES")*)
|
neuper@41940
|
130 |
|
neuper@41940
|
131 |
"===== input a formula to be derived from previous istate";
|
neuper@41940
|
132 |
"----- appendFormula TODO: first repair error";
|
neuper@41940
|
133 |
val cs = ((pt,p),[]);
|
neuper@41940
|
134 |
val ("ok", cs' as (_,_,(pt,p))) = step p cs;
|
neuper@41940
|
135 |
val ifo = (* encode "4^^^2" \<longrightarrow>*) "4^2"; val encode = I;
|
neuper@41940
|
136 |
(*
|
neuper@41940
|
137 |
val ("no derivation found", (_,_,(pt, p))) = inform cs' (encode ifo);
|
neuper@41940
|
138 |
here ^^^^^^^^^^^^^^^^^^^^^ should be "ok"
|
neuper@41940
|
139 |
*)
|
neuper@41940
|
140 |
|
neuper@41940
|
141 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
142 |
(*nxt = ("Calculate",Calculate "DIVIDE")*)
|
neuper@41940
|
143 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
144 |
(*nxt = ("Calculate",Calculate "POWER")*)
|
neuper@41940
|
145 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
146 |
(*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)
|
neuper@41940
|
147 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41940
|
148 |
(*nxt = ("End_Proof'",End_Proof')*)
|
neuper@41940
|
149 |
if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then ()
|
neuper@41940
|
150 |
else error "calculate.sml: script test_calculate changed behaviour";
|
neuper@41940
|
151 |
|
neuper@41940
|
152 |
"===== tactic Subproblem: from environment to origin";
|
neuper@41940
|
153 |
"----- TODO";
|
neuper@41940
|
154 |
|
neuper@41940
|
155 |
|
neuper@41940
|
156 |
|
neuper@41940
|
157 |
(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
|
neuper@41940
|
158 |
|
neuper@38065
|
159 |
(*=== inhibit exn ?=============================================================
|
neuper@37906
|
160 |
|
neuper@38065
|
161 |
"----------- debugging setContext..pbl_ -----------------";
|
neuper@38065
|
162 |
"----------- debugging setContext..pbl_ -----------------";
|
neuper@38065
|
163 |
"----------- debugging setContext..pbl_ -----------------";
|
neuper@37906
|
164 |
states:=[];
|
neuper@37906
|
165 |
CalcTree
|
neuper@37906
|
166 |
[(["equality (x+1=2)", "solveFor x","solutions L"],
|
neuper@38058
|
167 |
("Test",
|
neuper@37906
|
168 |
["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
169 |
["Test","squ-equ-test-subpbl1"]))];
|
neuper@37906
|
170 |
Iterator 1;
|
neuper@37906
|
171 |
moveActiveRoot 1; modelProblem 1;
|
neuper@37906
|
172 |
|
neuper@37906
|
173 |
val pos as (p,_) = ([],Pbl);
|
neuper@37906
|
174 |
val guh = "pbl_equ_univ";
|
neuper@37906
|
175 |
checkContext 1 pos guh;
|
neuper@37906
|
176 |
val ((pt,_),_) = get_calc 1;
|
neuper@37906
|
177 |
val pp = par_pblobj pt p;
|
neuper@37906
|
178 |
val keID = guh2kestoreID guh;
|
neuper@37906
|
179 |
case context_pbl keID pt pp of (true,["univariate", "equation"],_,_,_)=>()
|
neuper@38031
|
180 |
| _ => error "mathengine.sml: context_pbl .. pbl_equ_univ checked";
|
neuper@37906
|
181 |
|
neuper@37906
|
182 |
case get_obj g_spec pt p of (_, ["e_pblID"], _) => ()
|
neuper@38031
|
183 |
| _ => error "mathengine.sml: context_pbl .. pbl still empty";
|
neuper@37906
|
184 |
setContext 1 pos guh;
|
neuper@37906
|
185 |
val ((pt,_),_) = get_calc 1;
|
neuper@37906
|
186 |
case get_obj g_spec pt p of (_, ["univariate", "equation"], _) => ()
|
neuper@38031
|
187 |
| _ => error "mathengine.sml: context_pbl .. pbl set";
|
neuper@37906
|
188 |
|
neuper@37906
|
189 |
|
neuper@37906
|
190 |
setContext 1 pos "met_eq_lin";
|
neuper@37906
|
191 |
val ((pt,_),_) = get_calc 1;
|
neuper@37906
|
192 |
case get_obj g_spec pt p of (_, _, ["LinEq", "solve_lineq_equation"]) => ()
|
neuper@38031
|
193 |
| _ => error "mathengine.sml: context_pbl .. pbl set";
|
neuper@37906
|
194 |
|
neuper@37906
|
195 |
|
neuper@38065
|
196 |
"----------- tryrefine ----------------------------------";
|
neuper@38065
|
197 |
"----------- tryrefine ----------------------------------";
|
neuper@38065
|
198 |
"----------- tryrefine ----------------------------------";
|
neuper@37906
|
199 |
states:=[];
|
neuper@37906
|
200 |
CalcTree [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
|
neuper@37906
|
201 |
"solveFor x", "solutions L"],
|
neuper@38058
|
202 |
("RatEq",["univariate","equation"],["no_met"]))];
|
neuper@37906
|
203 |
Iterator 1;
|
neuper@37906
|
204 |
moveActiveRoot 1; autoCalculate 1 CompleteCalc;
|
neuper@37906
|
205 |
|
neuper@37906
|
206 |
refineProblem 1 ([1],Res) "pbl_equ_univ"
|
neuper@37906
|
207 |
(*gives "pbl_equ_univ_rat" correct*);
|
neuper@37906
|
208 |
|
neuper@37906
|
209 |
refineProblem 1 ([1],Res) (pblID2guh ["linear","univariate","equation"])
|
neuper@38065
|
210 |
(*gives "pbl_equ_univ_lin" incorrect*);
|
neuper@38065
|
211 |
|
neuper@38065
|
212 |
===== inhibit exn ?===========================================================*)
|
neuper@38065
|
213 |
|
neuper@38065
|
214 |
|
neuper@38065
|
215 |
"----------- fun step -----------------------------------";
|
neuper@38065
|
216 |
"----------- fun step -----------------------------------";
|
neuper@38065
|
217 |
"----------- fun step -----------------------------------";
|
neuper@38065
|
218 |
val p = e_pos'; val c = [];
|
neuper@38065
|
219 |
val (p,_,f,nxt,_,pt) =
|
neuper@38065
|
220 |
CalcTreeTEST
|
neuper@38065
|
221 |
[(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
|
neuper@38065
|
222 |
("Integrate", ["integrate","function"], ["diff","integration"]))];
|
neuper@38065
|
223 |
"----- step 1: returns tac = Model_Problem ---";
|
neuper@38065
|
224 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
225 |
"----- step 2: returns tac = ---";
|
neuper@38065
|
226 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
227 |
"----- step 3: returns tac = ---";
|
neuper@38065
|
228 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
229 |
"----- step 4: returns tac = ---";
|
neuper@38065
|
230 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
231 |
"----- step 5: returns tac = ---";
|
neuper@38065
|
232 |
|
neuper@38065
|
233 |
(*========== inhibit exn =======================================================
|
neuper@38066
|
234 |
2002 stops here as well: TODO review actual arguments:
|
neuper@38065
|
235 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
236 |
"----- step 6: returns tac = ---";
|
neuper@38065
|
237 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
238 |
"----- step 7: returns tac = ---";
|
neuper@38065
|
239 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
240 |
"----- step 8: returns tac = ---";
|
neuper@38065
|
241 |
val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
|
neuper@38065
|
242 |
============ inhibit exn =====================================================*)
|
neuper@38065
|
243 |
|
neuper@38065
|
244 |
|
neuper@38065
|
245 |
"----------- fun autocalc -------------------------------";
|
neuper@38065
|
246 |
"----------- fun autocalc -------------------------------";
|
neuper@38065
|
247 |
"----------- fun autocalc -------------------------------";
|
neuper@38065
|
248 |
val p = e_pos'; val c = [];
|
neuper@38065
|
249 |
val (p,_,f,nxt,_,pt) =
|
neuper@38065
|
250 |
CalcTreeTEST
|
neuper@38065
|
251 |
[(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
|
neuper@38065
|
252 |
("Integrate",["integrate","function"], ["diff","integration"]))];
|
neuper@38066
|
253 |
(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
|
neuper@38066
|
254 |
modeling is skipped FIXME
|
neuper@38066
|
255 |
*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
|
neuper@38065
|
256 |
tracing "----- step 1 ---";
|
neuper@38065
|
257 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@38065
|
258 |
tracing "----- step 2 ---";
|
neuper@38065
|
259 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@38065
|
260 |
tracing "----- step 3 ---";
|
neuper@38065
|
261 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@38065
|
262 |
tracing "----- step 4 ---";
|
neuper@38065
|
263 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@38065
|
264 |
tracing "----- step 5 ---";
|
neuper@38065
|
265 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@38065
|
266 |
tracing "----- step 6 ---";
|
neuper@38065
|
267 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@38065
|
268 |
tracing "----- step 7 ---";
|
neuper@38065
|
269 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@38065
|
270 |
tracing "----- step 8 ---";
|
neuper@38065
|
271 |
val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
|
neuper@41929
|
272 |
(*========== inhibit exn 110310 ================================================
|
neuper@41929
|
273 |
if str = "end-of-calculation" andalso
|
neuper@41929
|
274 |
term2str (get_obj g_res pt (fst p)) = "c + x + 1 / 3 * x ^^^ 3" then ()
|
neuper@38065
|
275 |
else error "mathengine.sml -- fun autocalc -- end";
|
neuper@41929
|
276 |
============ inhibit exn =====================================================*)
|
neuper@38065
|
277 |
|
neuper@38065
|
278 |
|
neuper@38065
|
279 |
"----------- fun autoCalculate -----------------------------------";
|
neuper@38065
|
280 |
"----------- fun autoCalculate -----------------------------------";
|
neuper@38065
|
281 |
"----------- fun autoCalculate -----------------------------------";
|
neuper@38065
|
282 |
states := [];
|
neuper@38065
|
283 |
CalcTree (*ATTENTION: encode_fmz ... unlike CalcTreeTEST*)
|
neuper@38065
|
284 |
[(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
|
neuper@38065
|
285 |
("Integrate", ["integrate", "function"], ["diff", "integration"]))];
|
neuper@38065
|
286 |
Iterator 1;
|
neuper@38065
|
287 |
moveActiveRoot 1;
|
neuper@38066
|
288 |
(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
|
neuper@38066
|
289 |
modeling is skipped FIXME
|
neuper@38066
|
290 |
see test/../interface -- solve_linear as rootpbl FE -- for OTHER expl:
|
neuper@38066
|
291 |
setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
|
neuper@38066
|
292 |
autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
|
neuper@38066
|
293 |
|
neuper@38066
|
294 |
fetchProposedTactic 1;
|
neuper@38066
|
295 |
setNextTactic 1 (Add_Given "solveFor x");
|
neuper@38066
|
296 |
autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
|
neuper@38066
|
297 |
|
neuper@38066
|
298 |
fetchProposedTactic 1;
|
neuper@38066
|
299 |
setNextTactic 1 (Add_Find "solutions L");
|
neuper@38066
|
300 |
autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
|
neuper@38066
|
301 |
|
neuper@38066
|
302 |
fetchProposedTactic 1;
|
neuper@38066
|
303 |
setNextTactic 1 (Specify_Theory "Test");
|
neuper@38066
|
304 |
autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
|
neuper@38066
|
305 |
*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
|
neuper@38065
|
306 |
autoCalculate 1 (Step 1);
|
neuper@38065
|
307 |
"----- step 1 ---";
|
neuper@38065
|
308 |
autoCalculate 1 (Step 1);
|
neuper@38065
|
309 |
"----- step 2 ---";
|
neuper@38065
|
310 |
autoCalculate 1 (Step 1);
|
neuper@38065
|
311 |
"----- step 3 ---";
|
neuper@38065
|
312 |
autoCalculate 1 (Step 1);
|
neuper@38065
|
313 |
"----- step 4 ---";
|
neuper@38065
|
314 |
autoCalculate 1 (Step 1);
|
neuper@38065
|
315 |
"----- step 5 ---";
|
neuper@38065
|
316 |
autoCalculate 1 (Step 1);
|
neuper@38065
|
317 |
"----- step 6 ---";
|
neuper@38065
|
318 |
autoCalculate 1 (Step 1);
|
neuper@38065
|
319 |
"----- step 7 ---";
|
neuper@38065
|
320 |
autoCalculate 1 (Step 1);
|
neuper@38065
|
321 |
"----- step 8 ---";
|
neuper@38065
|
322 |
autoCalculate 1 (Step 1);
|
neuper@38065
|
323 |
val (ptp as (_, p), _) = get_calc 1;
|
neuper@38065
|
324 |
val (Form t,_,_) = pt_extract ptp;
|
neuper@41929
|
325 |
(*========== inhibit exn 110310 ================================================
|
neuper@38065
|
326 |
if term2str t = "c + x + 1 / 3 * x ^^^ 3" andalso p = ([], Res) then ()
|
neuper@38065
|
327 |
else error "mathengine.sml -- fun autoCalculate -- end";
|
neuper@41929
|
328 |
============ inhibit exn =====================================================*)
|
neuper@38065
|
329 |
|
neuper@41940
|
330 |
-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
|