Walther@60640
|
1 |
(* Title: "Minisubpbl/530-error-Check_Elementwise.sml"
|
Walther@60640
|
2 |
Author: Walther Neuper 1105
|
Walther@60640
|
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 ---*)
|
walther@59997
|
10 |
val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
|
neuper@42021
|
11 |
val (dI',pI',mI') =
|
walther@59997
|
12 |
("Test", ["sqroot-test", "univariate", "equation", "test"],
|
walther@59997
|
13 |
["Test", "squ-equ-test-subpbl1"]);
|
Walther@60571
|
14 |
val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(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*);
|
walther@59846
|
34 |
get_ctxt pt'' p'' |> ContextC.is_empty; (*OKfalse*)
|
neuper@42451
|
35 |
val ctxt = get_ctxt pt'' p'';
|
Walther@60663
|
36 |
val SOME t = ParseC.term_opt ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
|
walther@59846
|
37 |
get_loc pt'' p'' |> snd |> ContextC.is_empty; (**OKfalse*)
|
neuper@42387
|
38 |
|
neuper@42451
|
39 |
val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*nxt = Rewrite_Set "Test_simplify"*);
|
walther@59846
|
40 |
get_ctxt pt p |> ContextC.is_empty; (*false*)
|
neuper@42021
|
41 |
val ctxt = get_ctxt pt p;
|
Walther@60663
|
42 |
val SOME t = ParseC.term_opt ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
|
walther@59846
|
43 |
get_loc pt p |> snd |> ContextC.is_empty; (*false*)
|
walther@59997
|
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);
|
walther@59749
|
47 |
"~~~~~ fun me, args:"; val tac = nxt;
|
walther@59804
|
48 |
val (pt, p) = case Step.by_tactic tac (pt,p) of
|
walther@59804
|
49 |
("ok", (_, _, ptp)) => ptp | _ => error "script.sml Step.by_tactic";
|
walther@59983
|
50 |
Test_Tool.show_pt pt; (*...(([3], Res), [x = 1])]... back in root, OK *)
|
walther@59761
|
51 |
"~~~~~ fun do_next, 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; (*= []*)
|
walther@60017
|
54 |
member op = [Pbl,Met] p_; (*= false*)
|
walther@59760
|
55 |
"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
|
walther@60154
|
56 |
(*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
|
walther@59686
|
57 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
Walther@60559
|
58 |
val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
|
walther@59686
|
59 |
|
walther@59734
|
60 |
val Next_Step (_, _, Check_elementwise' _) =
|
walther@59791
|
61 |
(*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
|
walther@59772
|
62 |
"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, (p, _))), Istate.Pstate ist, ctxt)
|
walther@59723
|
63 |
= (sc, (pt, pos), ist, ctxt);
|
walther@59686
|
64 |
|
walther@59686
|
65 |
(*case*)
|
walther@59769
|
66 |
scan_to_tactic (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
|
walther@59769
|
67 |
"~~~~~ fun scan_to_tactic , args:"; val ((prog, cct), (Istate.Pstate (ist as {path, ...})))
|
walther@59722
|
68 |
= ((prog, (ptp, ctxt)), (Istate.Pstate ist));
|
walther@59686
|
69 |
(*if*) 0 = length path (*else*);
|
walther@59686
|
70 |
|
walther@59785
|
71 |
go_scan_up (prog, cct) (trans_scan_up ist |> set_found);
|
walther@59784
|
72 |
"~~~~~ and go_scan_up , args:"; val ((yyy as (prog, _)), (ist as {env, path, found_accept, ...}))
|
walther@59785
|
73 |
= ((prog, cct), (trans_scan_up ist |> set_found));
|
walther@59686
|
74 |
(*if*) 1 < length path (*then*);
|
walther@59686
|
75 |
|
Walther@60679
|
76 |
scan_up yyy (ist |> path_up) (go_up ctxt path prog);
|
wenzelm@60309
|
77 |
"~~~~~ fun scan_up , args:"; val ((yyy as (prog, xxx)), (ist as {found_accept, ...}), (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _))
|
Walther@60679
|
78 |
= (yyy, (ist |> path_up), (go_up ctxt path prog));
|
walther@59784
|
79 |
(*if* ) found_accept = Napp_ ( *else*);
|
Walther@60611
|
80 |
val (i, body) = check_Let_up ctxt ist prog;
|
walther@59686
|
81 |
|
walther@59686
|
82 |
(*case*)
|
walther@59769
|
83 |
scan_dn xxx (ist |> path_up_down [R, D] |> upd_env i) body (*of*);
|
walther@59686
|
84 |
(*========== a leaf has been found ==========*)
|
walther@59769
|
85 |
"~~~~~ fun scan_dn , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t)
|
walther@59698
|
86 |
= (xxx, (ist |> path_up_down [R, D] |> upd_env i), body);
|
walther@59721
|
87 |
val (Program.Tac stac, a') = (*case*)
|
walther@59772
|
88 |
check_leaf "next " ctxt eval (get_subst ist) t;
|
walther@59686
|
89 |
|
walther@59825
|
90 |
val Check_elementwise "Assumptions" =
|
Walther@60640
|
91 |
LItool.tac_from_prog (pt, p) stac;
|
walther@60336
|
92 |
"~~~~~ fun tac_from_prog , args:"; val (pt, thy, (Const (\<^const_name>\<open>Check_elementwise\<close>, _) $ _ $
|
wenzelm@60309
|
93 |
(set as Const (\<^const_name>\<open>Collect\<close>,_) $ Abs (_,_,pred))))
|
walther@59722
|
94 |
= (pt, (Proof_Context.theory_of ctxt), stac);
|
neuper@42394
|
95 |
|
neuper@42021
|
96 |
val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*WAS nxt = ("Empty_Tac", Empty_Tac)*)
|
walther@59749
|
97 |
case nxt of (Check_elementwise "Assumptions") => ()
|
wneuper@59253
|
98 |
| _ => error "Check_elementwise changed; after switch sub-->root-method";
|
Walther@60529
|
99 |
|
Walther@60533
|
100 |
Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
|