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