neuper@41985
|
1 |
(* Title: 400-start-meth-subpbl.sml
|
neuper@41985
|
2 |
Author: Walther Neuper 1105
|
neuper@41985
|
3 |
(c) copyright due to lincense terms.
|
neuper@41985
|
4 |
*)
|
neuper@41985
|
5 |
|
neuper@41985
|
6 |
val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
|
neuper@41985
|
7 |
val (dI',pI',mI') =
|
neuper@41990
|
8 |
("Test", ["sqroot-test","univariate","equation","test"],
|
neuper@41990
|
9 |
["Test","squ-equ-test-subpbl1"]);
|
neuper@41985
|
10 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@41985
|
11 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41990
|
12 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41990
|
13 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41990
|
14 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41990
|
15 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41990
|
16 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41999
|
17 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
|
neuper@41990
|
18 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41990
|
19 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41999
|
20 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)
|
neuper@41990
|
21 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41990
|
22 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41990
|
23 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41990
|
24 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41990
|
25 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41990
|
26 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41990
|
27 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41999
|
28 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
|
neuper@41999
|
29 |
get_ctxt pt p |> is_e_ctxt; (*false... OK: from specify, PblObj{ctxt,...}*)
|
neuper@41999
|
30 |
val ctxt = get_ctxt pt p;
|
neuper@41999
|
31 |
val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
|
neuper@41999
|
32 |
get_loc pt p |> snd |> is_e_ctxt; (*true ... OK: interpreter not yet started*)
|
neuper@41999
|
33 |
val (pt'',p'') = (pt, p);
|
neuper@41999
|
34 |
"~~~~~ fun me, args:"; val (_,tac) = nxt;
|
neuper@41999
|
35 |
"~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
|
neuper@41999
|
36 |
val (mI,m) = mk_tac'_ tac;
|
neuper@41999
|
37 |
val Appl m = applicable_in p pt m;
|
neuper@41999
|
38 |
member op = specsteps mI; (*false*)
|
neuper@41999
|
39 |
"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
|
neuper@41999
|
40 |
"~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
|
neuper@41999
|
41 |
val {srls, ...} = get_met mI;
|
neuper@42019
|
42 |
val PblObj {meth=itms, ...} = get_obj I pt p;
|
neuper@41999
|
43 |
val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
|
neuper@41999
|
44 |
val thy' = get_obj g_domID pt p;
|
neuper@41999
|
45 |
val thy = assoc_thy thy';
|
neuper@42019
|
46 |
val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
|
neuper@41999
|
47 |
(*dont take ctxt ^^^ from ^^^^^^^^^^^^^*)
|
neuper@41999
|
48 |
(*= the first part vvvvvvvvv works now =======================================*)
|
neuper@41999
|
49 |
val (pt, p) = case locatetac tac (pt'',p'') of
|
neuper@41999
|
50 |
("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
|
neuper@41999
|
51 |
val ctxt = get_ctxt pt p;
|
neuper@41999
|
52 |
val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
|
neuper@41999
|
53 |
(*= the first part ^^^^^^^^^^ works now =======================================*)
|
neuper@41999
|
54 |
val (pt'',p'') = (pt, p);
|
neuper@41999
|
55 |
"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
|
neuper@41999
|
56 |
val pIopt = get_pblID (pt,ip);
|
neuper@41999
|
57 |
tacis; (*= []*)
|
neuper@41999
|
58 |
member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
|
neuper@41999
|
59 |
"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
|
neuper@41999
|
60 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
neuper@41999
|
61 |
val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
|
neuper@41999
|
62 |
"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
|
neuper@41999
|
63 |
(ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
|
neuper@41999
|
64 |
val ctxt = get_ctxt pt pos;
|
neuper@41999
|
65 |
val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
|
neuper@41999
|
66 |
(*= the first part ^^^^^^^^^^ works now =======================================*)
|
neuper@41999
|
67 |
l = [];
|
neuper@41999
|
68 |
appy thy ptp E [R] body NONE v;
|
neuper@41999
|
69 |
val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*nxt = Rewrite_Set_Inst isolate_bdv*);
|
neuper@41990
|
70 |
|