neuper@42021
|
1 |
(* Title: 530-error-Check_Elementwise.sml
|
neuper@42021
|
2 |
Author: Walther Neuper 1105
|
neuper@42021
|
3 |
(c) copyright due to lincense terms.
|
neuper@42021
|
4 |
*)
|
neuper@42021
|
5 |
|
neuper@42021
|
6 |
"----------- Minisubplb/530-error-Check_Elementwise.sml ----------";
|
neuper@42021
|
7 |
"----------- Minisubplb/530-error-Check_Elementwise.sml ----------";
|
neuper@42021
|
8 |
"----------- Minisubplb/530-error-Check_Elementwise.sml ----------";
|
neuper@42394
|
9 |
(*see also --- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x" by me ---*)
|
neuper@42021
|
10 |
val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
|
neuper@42021
|
11 |
val (dI',pI',mI') =
|
neuper@42021
|
12 |
("Test", ["sqroot-test","univariate","equation","test"],
|
neuper@42021
|
13 |
["Test","squ-equ-test-subpbl1"]);
|
neuper@42021
|
14 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@42021
|
15 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@42021
|
16 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@42021
|
17 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@42021
|
18 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@42021
|
19 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@42021
|
20 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@42021
|
21 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
|
neuper@42021
|
22 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@42021
|
23 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@55279
|
24 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["LINEAR", "univariate", "equation", "test"]*)
|
neuper@42021
|
25 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@42021
|
26 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@42021
|
27 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@42021
|
28 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@42021
|
29 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@42021
|
30 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@42021
|
31 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@42451
|
32 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*OKnxt = Apply_Method ["Test", "solve_linear"]*)
|
neuper@42451
|
33 |
val (p'',_,f,nxt,_,pt'') = me nxt p [] pt; (*nxt = Rewrite_Set_Inst..OK isolate_bdv*);
|
neuper@42451
|
34 |
get_ctxt pt'' p'' |> is_e_ctxt; (*OKfalse*)
|
neuper@42451
|
35 |
val ctxt = get_ctxt pt'' p'';
|
neuper@42021
|
36 |
val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
|
neuper@42451
|
37 |
get_loc pt'' p'' |> snd |> is_e_ctxt; (**OKfalse*)
|
neuper@42387
|
38 |
|
neuper@42451
|
39 |
val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*nxt = Rewrite_Set "Test_simplify"*);
|
neuper@42021
|
40 |
get_ctxt pt p |> is_e_ctxt; (*false*)
|
neuper@42021
|
41 |
val ctxt = get_ctxt pt p;
|
neuper@42021
|
42 |
val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
|
neuper@42021
|
43 |
get_loc pt p |> snd |> is_e_ctxt; (*false*)
|
neuper@55279
|
44 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR","univariate", ...]) *);
|
neuper@42021
|
45 |
|
neuper@42021
|
46 |
val (pt'''', p'''') = (pt, p);
|
neuper@42021
|
47 |
"~~~~~ fun me, args:"; val (_,tac) = nxt;
|
neuper@42021
|
48 |
val (pt, p) = case locatetac tac (pt,p) of
|
neuper@42021
|
49 |
("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
|
neuper@42021
|
50 |
show_pt pt; (*...(([3], Res), [x = 1])]... back in root, OK *)
|
neuper@42021
|
51 |
"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
|
neuper@42021
|
52 |
val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*)
|
neuper@42021
|
53 |
tacis; (*= []*)
|
neuper@42021
|
54 |
member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
|
neuper@42021
|
55 |
"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
|
neuper@42021
|
56 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
neuper@42021
|
57 |
val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
|
neuper@48790
|
58 |
"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'), (sc as Prog (h $ body)),
|
neuper@42021
|
59 |
(ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
|
neuper@42021
|
60 |
val ctxt = get_ctxt pt pos
|
neuper@42021
|
61 |
val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
|
neuper@42021
|
62 |
l; (*= [R, R, D, L, R]*)
|
neuper@48790
|
63 |
"~~~~~ fun nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
|
neuper@42021
|
64 |
(thy, ptp, sc, E, l, Skip_, a, v);
|
neuper@42021
|
65 |
1 < length l; (*true*)
|
neuper@42021
|
66 |
val up = drop_last l;
|
neuper@42021
|
67 |
go up sc; (* = Const ("HOL.Let", *)
|
neuper@48790
|
68 |
"~~~~~ fun nxt_up, args:"; val (thy, ptp, (scr as (Prog sc)), E, l, ay,
|
neuper@42021
|
69 |
(t as Const ("HOL.Let",_) $ _), a, v) =
|
neuper@48790
|
70 |
(thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v);
|
neuper@42021
|
71 |
ay = Napp_; (*false*)
|
neuper@42021
|
72 |
val up = drop_last l;
|
neuper@42021
|
73 |
val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc;
|
neuper@42021
|
74 |
val i = mk_Free (i, T);
|
neuper@42021
|
75 |
val E = upd_env E (i, v);
|
neuper@42021
|
76 |
body; (*= Const ("Script.Check'_elementwise"*)
|
neuper@42021
|
77 |
"~~~~~ fun appy, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v)=
|
neuper@42021
|
78 |
(thy, ptp, E, (up@[R,D]), body, a, v);
|
neuper@42021
|
79 |
handle_leaf "next " th sr E a v t; (*= (NONE, STac (Const ("Script.Check'_elementwise"*)
|
neuper@42021
|
80 |
val (a', STac stac) = handle_leaf "next " th sr E a v t;
|
neuper@42021
|
81 |
"~~~~~ fun stac2tac_, args:"; val (pt, thy, (Const("Script.Check'_elementwise",_) $ _ $
|
neuper@42021
|
82 |
(set as Const ("Set.Collect",_) $ Abs (_,_,pred)))) = (pt, (assoc_thy th), stac);
|
neuper@42021
|
83 |
(*2011 changed ^^^^^ *)
|
neuper@42394
|
84 |
|
neuper@42021
|
85 |
val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*WAS nxt = ("Empty_Tac", Empty_Tac)*)
|
wneuper@59253
|
86 |
case nxt of ("Check_elementwise", Check_elementwise "Assumptions") => ()
|
wneuper@59253
|
87 |
| _ => error "Check_elementwise changed; after switch sub-->root-method";
|