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'' |> ContextC.is_empty; (*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 |> ContextC.is_empty; (**OKfalse*)
39 val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*nxt = Rewrite_Set "Test_simplify"*);
40 get_ctxt pt p |> ContextC.is_empty; (*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 |> ContextC.is_empty; (*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 Step.by_tactic tac (pt,p) of
49 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml Step.by_tactic";
50 Test_Tool.show_pt pt; (*...(([3], Res), [x = 1])]... back in root, OK *)
51 "~~~~~ fun do_next, 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_; (*= false*)
55 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
56 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
57 val thy' = get_obj g_domID pt (par_pblobj pt p);
58 val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt;
60 val Next_Step (_, _, Check_elementwise' _) =
61 (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
62 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, (p, _))), Istate.Pstate ist, ctxt)
63 = (sc, (pt, pos), ist, ctxt);
66 scan_to_tactic (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
67 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cct), (Istate.Pstate (ist as {path, ...})))
68 = ((prog, (ptp, ctxt)), (Istate.Pstate ist));
69 (*if*) 0 = length path (*else*);
71 go_scan_up (prog, cct) (trans_scan_up ist |> set_found);
72 "~~~~~ and go_scan_up , args:"; val ((yyy as (prog, _)), (ist as {env, path, found_accept, ...}))
73 = ((prog, cct), (trans_scan_up ist |> set_found));
74 (*if*) 1 < length path (*then*);
76 scan_up yyy (ist |> path_up) (go_up path prog);
77 "~~~~~ fun scan_up , args:"; val ((yyy as (prog, xxx)), (ist as {found_accept, ...}), (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _))
78 = (yyy, (ist |> path_up), (go_up path prog));
79 (*if* ) found_accept = Napp_ ( *else*);
80 val (i, body) = check_Let_up ist prog;
83 scan_dn xxx (ist |> path_up_down [R, D] |> upd_env i) body (*of*);
84 (*========== a leaf has been found ==========*)
85 "~~~~~ fun scan_dn , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t)
86 = (xxx, (ist |> path_up_down [R, D] |> upd_env i), body);
87 val (Program.Tac stac, a') = (*case*)
88 check_leaf "next " ctxt eval (get_subst ist) t;
90 val Check_elementwise "Assumptions" =
91 LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) stac;
92 "~~~~~ fun tac_from_prog , args:"; val (pt, thy, (Const (\<^const_name>\<open>Check_elementwise\<close>, _) $ _ $
93 (set as Const (\<^const_name>\<open>Collect\<close>,_) $ Abs (_,_,pred))))
94 = (pt, (Proof_Context.theory_of ctxt), stac);
96 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*WAS nxt = ("Empty_Tac", Empty_Tac)*)
97 case nxt of (Check_elementwise "Assumptions") => ()
98 | _ => error "Check_elementwise changed; after switch sub-->root-method";
100 Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)