10 "table of contents -----------------------------------------------"; |
10 "table of contents -----------------------------------------------"; |
11 "-----------------------------------------------------------------"; |
11 "-----------------------------------------------------------------"; |
12 "----------- WN0509 why does next_tac doesnt find Substitute -----"; |
12 "----------- WN0509 why does next_tac doesnt find Substitute -----"; |
13 "----------- WN0509 Substitute 2nd part --------------------------"; |
13 "----------- WN0509 Substitute 2nd part --------------------------"; |
14 "----------- fun sel_appl_atomic_tacs ----------------------------"; |
14 "----------- fun sel_appl_atomic_tacs ----------------------------"; |
15 "-----------------------------------------------------------------"; |
15 "----------- fun init_form, fun get_stac -------------------------"; |
16 "-----------------------------------------------------------------"; |
16 "-----------------------------------------------------------------"; |
17 "-----------------------------------------------------------------"; |
17 "-----------------------------------------------------------------"; |
18 |
18 "-----------------------------------------------------------------"; |
|
19 |
|
20 (*========== inhibit exn 110503 ================================================ |
19 |
21 |
20 "----------- WN0509 why does next_tac doesnt find Substitute -----"; |
22 "----------- WN0509 why does next_tac doesnt find Substitute -----"; |
21 "----------- WN0509 why does next_tac doesnt find Substitute -----"; |
23 "----------- WN0509 why does next_tac doesnt find Substitute -----"; |
22 "----------- WN0509 why does next_tac doesnt find Substitute -----"; |
24 "----------- WN0509 why does next_tac doesnt find Substitute -----"; |
23 |
25 |
245 |
247 |
246 "----- WN080102 these vvv do not work, because locatetac starts the search\ |
248 "----- WN080102 these vvv do not work, because locatetac starts the search\ |
247 \1 stac too low"; |
249 \1 stac too low"; |
248 applyTactic 1 p (hd appltacs); |
250 applyTactic 1 p (hd appltacs); |
249 autoCalculate 1 CompleteCalc; |
251 autoCalculate 1 CompleteCalc; |
250 |
252 ============ inhibit exn 110503 ==============================================*) |
|
253 |
|
254 "----------- fun init_form, fun get_stac -------------------------"; |
|
255 "----------- fun init_form, fun get_stac -------------------------"; |
|
256 "----------- fun init_form, fun get_stac -------------------------"; |
|
257 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"]; |
|
258 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"], |
|
259 ["Test","squ-equ-test-subpbl1"]); |
|
260 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
261 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
262 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
263 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
264 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
265 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
266 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
267 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
268 "~~~~~ fun me, args:"; val (_,tac) = nxt; |
|
269 "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p); |
|
270 val (mI,m) = mk_tac'_ tac; |
|
271 val Appl m = applicable_in p pt m; |
|
272 member op = specsteps mI; (*false*) |
|
273 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp); |
|
274 "~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos); |
|
275 val {srls, ...} = get_met mI; |
|
276 val PblObj {meth=itms, ...} = get_obj I pt p; |
|
277 val thy' = get_obj g_domID pt p; |
|
278 val thy = assoc_thy thy'; |
|
279 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI; |
|
280 val ini = init_form thy sc env; |
|
281 "----- fun init_form, args:"; val (Script sc) = sc; |
|
282 "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc); |
|
283 case get_stac thy sc of SOME (Free ("e_e", _)) => () |
|
284 | _ => error "script: Const (?, ?) in script (as term) changed";; |
|
285 |