wneuper@59561
|
1 |
(* Title: "Interpret/lucas-interpreter.sml"
|
wneuper@59561
|
2 |
Author: Walther Neuper
|
wneuper@59561
|
3 |
(c) due to copyright terms
|
wneuper@59561
|
4 |
*)
|
wneuper@59561
|
5 |
|
wneuper@59561
|
6 |
"-----------------------------------------------------------------------------------------------";
|
wneuper@59561
|
7 |
"table of contents -----------------------------------------------------------------------------";
|
wneuper@59561
|
8 |
"-----------------------------------------------------------------------------------------------";
|
wneuper@59561
|
9 |
"----------- Take as 1st stac in program -------------------------------------------------------";
|
walther@59670
|
10 |
"----------- re-build: fun locate_input_tactic -------------------------------------------------";
|
walther@59997
|
11 |
"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
|
walther@59781
|
12 |
"----------- re-build: fun find_next_step, mini ------------------------------------------------";
|
walther@59783
|
13 |
"----------- re-build: fun locate_input_term ---------------------------------------------------";
|
wneuper@59561
|
14 |
"-----------------------------------------------------------------------------------------------";
|
wneuper@59561
|
15 |
"-----------------------------------------------------------------------------------------------";
|
wneuper@59561
|
16 |
"-----------------------------------------------------------------------------------------------";
|
wneuper@59561
|
17 |
|
wneuper@59561
|
18 |
"----------- Take as 1st stac in program -------------------------------------------------------";
|
wneuper@59561
|
19 |
"----------- Take as 1st stac in program -------------------------------------------------------";
|
wneuper@59561
|
20 |
"----------- Take as 1st stac in program -------------------------------------------------------";
|
walther@59834
|
21 |
"compare --- Apply_Method with initial Take by Step.do_next --- in test/../step-solve ----------";
|
wneuper@59561
|
22 |
val p = e_pos'; val c = [];
|
wneuper@59561
|
23 |
val (p,_,f,nxt,_,pt) =
|
wneuper@59561
|
24 |
CalcTreeTEST
|
walther@60242
|
25 |
[(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
|
walther@59997
|
26 |
("Integrate", ["integrate", "function"], ["diff", "integration"]))];
|
Walther@60567
|
27 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow> Add_Given "functionTerm (x \<up> 2 + 1)"*)
|
wneuper@59561
|
28 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59561
|
29 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59561
|
30 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59561
|
31 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
Walther@60567
|
32 |
|
Walther@60567
|
33 |
val (p''',_,f,nxt''',_,pt''') = me nxt p c pt; (*nxt'''= Specify_Method ["diff", "integration"]*)
|
Walther@60567
|
34 |
(*/------------------- step into me Specify_Method ["diff", "integration"] -----------------\*)
|
Walther@60567
|
35 |
"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt''', p''', c, pt''');
|
Walther@60567
|
36 |
val (pt, p) =
|
Walther@60567
|
37 |
(*Step.by_tactic is here for testing by me; do_next would suffice in me*)
|
Walther@60567
|
38 |
case Step.by_tactic tac (pt, p) of
|
Walther@60567
|
39 |
("ok", (_, _, ptp)) => ptp
|
Walther@60567
|
40 |
|
Walther@60567
|
41 |
val ("ok", ([(Apply_Method ["diff", "integration"], _, _)], _, _)) = (*case*)
|
Walther@60567
|
42 |
Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
|
Walther@60567
|
43 |
"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
|
Walther@60567
|
44 |
= (p, ((pt, Pos.e_pos'), []));
|
Walther@60567
|
45 |
(*if*) Pos.on_calc_end ip (*else*);
|
Walther@60567
|
46 |
val (_, probl_id, _) = Calc.references (pt, p);
|
Walther@60567
|
47 |
val _ =
|
Walther@60567
|
48 |
(*case*) tacis (*of*);
|
Walther@60567
|
49 |
(*if*) probl_id = Problem.id_empty (*else*);
|
Walther@60567
|
50 |
|
Walther@60567
|
51 |
val ("ok", ([(Apply_Method ["diff", "integration"], _, _)], _, _)) =
|
Walther@60567
|
52 |
Step.switch_specify_solve p_ (pt, ip);
|
Walther@60567
|
53 |
"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
|
Walther@60567
|
54 |
(*if*) Pos.on_specification ([], state_pos) (*then*);
|
Walther@60567
|
55 |
|
Walther@60567
|
56 |
Step.specify_do_next (pt, input_pos);
|
Walther@60567
|
57 |
"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
|
Walther@60567
|
58 |
val (_, (p_', tac)) = Specify.find_next_step ptp
|
Walther@60567
|
59 |
val ist_ctxt = Ctree.get_loc pt (p, p_)
|
Walther@60567
|
60 |
val Tactic.Apply_Method mI =
|
Walther@60567
|
61 |
(*case*) tac (*of*);
|
Walther@60567
|
62 |
|
Walther@60567
|
63 |
val ("ok", ([(Apply_Method ["diff", "integration"], _, _)], _, _)) =
|
Walther@60567
|
64 |
LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
|
Walther@60567
|
65 |
ist_ctxt (pt, (p, p_'));
|
Walther@60567
|
66 |
"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _)))
|
Walther@60567
|
67 |
= ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)),
|
Walther@60567
|
68 |
ist_ctxt, (pt, (p, p_')));
|
Walther@60567
|
69 |
val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)
|
Walther@60567
|
70 |
PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
|
Walther@60567
|
71 |
| _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
|
Walther@60567
|
72 |
val {ppc, ...} = MethodC.from_store ctxt mI;
|
Walther@60567
|
73 |
val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
|
Walther@60567
|
74 |
val srls = LItool.get_simplifier (pt, pos)
|
Walther@60567
|
75 |
val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
|
Walther@60567
|
76 |
(is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)
|
Walther@60567
|
77 |
| _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate"
|
Walther@60567
|
78 |
val ini = LItool.implicit_take prog env;
|
Walther@60567
|
79 |
val pos = start_new_level pos
|
Walther@60567
|
80 |
val NONE =
|
Walther@60567
|
81 |
(*case*) ini (*of*);
|
Walther@60567
|
82 |
|
Walther@60567
|
83 |
val Next_Step (iii, ccc, ttt) = (*case*)
|
Walther@60567
|
84 |
LI.find_next_step prog (pt, (lev_dn p, Res)) is ctxt (*of*);
|
Walther@60567
|
85 |
"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)
|
Walther@60567
|
86 |
= (prog, (pt, (lev_dn p, Res)), is, ctxt);
|
Walther@60567
|
87 |
|
Walther@60567
|
88 |
(*case*)
|
Walther@60567
|
89 |
scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
|
Walther@60567
|
90 |
"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
|
Walther@60567
|
91 |
= ((prog, (ptp, ctxt)), (Pstate ist));
|
Walther@60567
|
92 |
(*if*) path = [] (*then*);
|
Walther@60567
|
93 |
|
Walther@60567
|
94 |
val Accept_Tac (ttt, sss, ccc) =
|
Walther@60567
|
95 |
scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
|
Walther@60567
|
96 |
"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))
|
Walther@60567
|
97 |
= (cc, (trans_scan_dn ist), (Program.body_of prog));
|
Walther@60567
|
98 |
|
Walther@60567
|
99 |
val Accept_Tac (ttt, sss, ccc) = (*case*)
|
Walther@60567
|
100 |
scan_dn cc (ist |> path_down [L, R]) e (*of*);
|
Walther@60567
|
101 |
"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
|
Walther@60567
|
102 |
= (cc, (ist |> path_down [L, R]), e);
|
Walther@60567
|
103 |
(*if*) Tactical.contained_in t (*else*);
|
Walther@60567
|
104 |
val (Program.Tac prog_tac, form_arg) =
|
Walther@60567
|
105 |
(*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
|
Walther@60567
|
106 |
|
Walther@60567
|
107 |
val Accept_Tac (ttt, sss, ccc) =
|
Walther@60567
|
108 |
check_tac cc ist (prog_tac, form_arg);
|
Walther@60567
|
109 |
"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))
|
Walther@60567
|
110 |
= (cc, ist, (prog_tac, form_arg));
|
Walther@60567
|
111 |
val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac
|
Walther@60567
|
112 |
val _ =
|
Walther@60567
|
113 |
(*case*) m (*of*);
|
Walther@60567
|
114 |
|
Walther@60567
|
115 |
(*case*)
|
Walther@60567
|
116 |
Solve_Step.check m (pt, p) (*of*);
|
Walther@60567
|
117 |
"~~~~~ fun check , args:"; val ((Tactic.Take str), (pt, pos as (p_, p))) = (m, (pt, p));
|
Walther@60567
|
118 |
|
Walther@60567
|
119 |
(*+*)val ([0], Res) = pos; (*<<<-------------------------*)
|
Walther@60567
|
120 |
(*-------------------- stop step into me Specify_Method ["diff", "integration"] -------------*)
|
Walther@60567
|
121 |
(*\------------------- step into me Specify_Method ["diff", "integration"] -----------------/*)
|
Walther@60567
|
122 |
|
Walther@60567
|
123 |
val (p,_,f,nxt,_,pt) = me nxt''' p''' c pt''';
|
walther@59749
|
124 |
case nxt of (Apply_Method ["diff", "integration"]) => ()
|
wneuper@59561
|
125 |
| _ => error "integrate.sml -- me method [diff,integration] -- spec";
|
wneuper@59561
|
126 |
"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
|
wneuper@59561
|
127 |
|
walther@59749
|
128 |
"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
|
walther@59804
|
129 |
"~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
|
walther@59922
|
130 |
val Applicable.Yes m = Step.check tac (pt, p);
|
walther@59755
|
131 |
(*if*) Tactic.for_specify' m; (*false*)
|
walther@59749
|
132 |
"~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp);
|
walther@59686
|
133 |
|
walther@59751
|
134 |
"~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))
|
walther@59749
|
135 |
= (m, (pt, pos));
|
Walther@60559
|
136 |
val {srls, ...} = MethodC.from_store ctxt mI;
|
walther@59686
|
137 |
val itms = case get_obj I pt p of
|
walther@59686
|
138 |
PblObj {meth=itms, ...} => itms
|
walther@59686
|
139 |
| _ => error "solve Apply_Method: uncovered case get_obj"
|
walther@59686
|
140 |
val thy' = get_obj g_domID pt p;
|
walther@59881
|
141 |
val thy = ThyC.get_theory thy';
|
walther@59790
|
142 |
val srls = LItool.get_simplifier (pt, pos)
|
walther@59790
|
143 |
val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
|
walther@59686
|
144 |
(is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
|
walther@59697
|
145 |
| _ => error "solve Apply_Method: uncovered case init_pstate";
|
walther@60242
|
146 |
(*+*)pstate2str (the_pstate is) = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)";
|
walther@59848
|
147 |
val ini = LItool.implicit_take sc env;
|
walther@59686
|
148 |
val p = lev_dn p;
|
walther@59686
|
149 |
|
walther@59686
|
150 |
val NONE = (*case*) ini (*of*);
|
walther@59734
|
151 |
val Next_Step (is', ctxt', m') =
|
walther@59791
|
152 |
LI.find_next_step sc (pt, (p, Res)) is ctxt;
|
walther@60242
|
153 |
(*+*)pstate2str (the_pstate is') = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], empty, NONE, \nIntegral x \<up> 2 + 1 D x, ORundef, false, false)";
|
walther@59686
|
154 |
val Safe_Step (_, _, Take' _) = (*case*)
|
walther@59686
|
155 |
locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);
|
walther@59692
|
156 |
"~~~~~ fun locate_input_tactic , args:"; val ((Prog prog), cstate, istate, ctxt, tac)
|
walther@59686
|
157 |
= (sc, (pt, (p, Res)), is', ctxt', m');
|
walther@59686
|
158 |
|
walther@59692
|
159 |
(*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
|
walther@59692
|
160 |
"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
|
walther@59692
|
161 |
= ((prog, (cstate, ctxt, tac)), istate);
|
walther@59686
|
162 |
(*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
|
walther@59686
|
163 |
|
walther@59718
|
164 |
val Accept_Tac1 (_, _, Take' _) =
|
walther@59718
|
165 |
scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
|
wenzelm@60309
|
166 |
"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))))
|
walther@59718
|
167 |
= (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
|
walther@59686
|
168 |
|
walther@59868
|
169 |
(*+*) if UnparseC.term e = "Take (Integral f_f D v_v)" then () else error "scan_dn1 Integral changed";
|
walther@59686
|
170 |
|
walther@59686
|
171 |
(*case*)
|
walther@59691
|
172 |
scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
|
walther@59686
|
173 |
(*======= end of scanning tacticals, a leaf =======*)
|
walther@59722
|
174 |
"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, or, ...}), t)
|
walther@59686
|
175 |
= (xxx, (ist |> path_down [L, R]), e);
|
walther@59772
|
176 |
val (Program.Tac stac, a') = check_leaf "locate" ctxt eval (get_subst ist) t;
|
wneuper@59561
|
177 |
|
wneuper@59561
|
178 |
|
walther@59806
|
179 |
|
walther@59670
|
180 |
"----------- re-build: fun locate_input_tactic -------------------------------------------------";
|
walther@59670
|
181 |
"----------- re-build: fun locate_input_tactic -------------------------------------------------";
|
walther@59670
|
182 |
"----------- re-build: fun locate_input_tactic -------------------------------------------------";
|
walther@59997
|
183 |
val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
|
walther@59997
|
184 |
val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"],
|
walther@59997
|
185 |
["Test", "squ-equ-test-subpbl1"]);
|
wneuper@59562
|
186 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
wneuper@59562
|
187 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
wneuper@59562
|
188 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
wneuper@59562
|
189 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
wneuper@59562
|
190 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
wneuper@59562
|
191 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
wneuper@59562
|
192 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59670
|
193 |
(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
|
walther@59670
|
194 |
(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
|
wneuper@59562
|
195 |
|
walther@59781
|
196 |
(*//------------------ begin step into ------------------------------------------------------\\*)
|
walther@59686
|
197 |
(*[1], Res*)val (p'''''_''',_,f,nxt'''''_''',_,pt'''''_''') = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
|
wneuper@59562
|
198 |
|
walther@59749
|
199 |
"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
|
wneuper@59562
|
200 |
|
walther@59806
|
201 |
(** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*)
|
walther@59806
|
202 |
Step.by_tactic tac (pt,p) (*of*);
|
walther@59806
|
203 |
"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
|
walther@59921
|
204 |
val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
|
walther@59755
|
205 |
(*if*) Tactic.for_specify' m; (*false*)
|
walther@59670
|
206 |
|
walther@59806
|
207 |
(** )val (***)xxxxx_x(***) ( *(msg, cs') =( **)
|
walther@59806
|
208 |
Step_Solve.by_tactic m ptp;
|
walther@59806
|
209 |
"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, ptp);
|
walther@59670
|
210 |
(*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
|
walther@60154
|
211 |
(*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
|
walther@59670
|
212 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
Walther@60559
|
213 |
val (is, sc) = LItool.resume_prog (p,p_) pt;
|
walther@59670
|
214 |
|
walther@59670
|
215 |
locate_input_tactic sc (pt, po) (fst is) (snd is) m;
|
walther@59692
|
216 |
"~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac)
|
walther@59670
|
217 |
= (sc, (pt, po), (fst is), (snd is), m);
|
walther@59670
|
218 |
val srls = get_simplifier cstate;
|
walther@59670
|
219 |
|
walther@59718
|
220 |
(** )val Accept_Tac1 ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
|
walther@59692
|
221 |
(*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
|
walther@59692
|
222 |
"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
|
walther@59692
|
223 |
= ((prog, (cstate, ctxt, tac)), istate);
|
walther@59686
|
224 |
(*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
|
walther@59670
|
225 |
|
walther@59670
|
226 |
(** )val xxxxx_xx = ( **)
|
walther@59718
|
227 |
scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
|
wenzelm@60309
|
228 |
"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))))
|
walther@59718
|
229 |
= (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
|
walther@59670
|
230 |
|
walther@59691
|
231 |
(*case*) scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
|
walther@60336
|
232 |
"~~~~~ fun scan_dn1 , args:"; val ((xxx as (cstate, _, _)), ist, (Const (\<^const_name>\<open>Chain\<close>(*1*), _) $ e1 $ e2 $ a))
|
walther@59686
|
233 |
= (xxx, (ist |> path_down [L, R]), e);
|
walther@59670
|
234 |
|
walther@59691
|
235 |
(*case*) scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
|
walther@60336
|
236 |
"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ e))
|
walther@59686
|
237 |
= (xxx, (ist |> path_down_form ([L, L, R], a)), e1);
|
walther@59670
|
238 |
|
walther@59691
|
239 |
(*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*);
|
walther@59670
|
240 |
(*======= end of scanning tacticals, a leaf =======*)
|
walther@59691
|
241 |
"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
|
walther@59686
|
242 |
= (xxx, (ist |> path_down [R]), e);
|
walther@59721
|
243 |
val (Program.Tac stac, a') =
|
walther@59772
|
244 |
(*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
|
walther@59844
|
245 |
val LItool.Associated (m, v', ctxt) =
|
walther@59686
|
246 |
(*case*) associate pt ctxt (m, stac) (*of*);
|
walther@59670
|
247 |
|
walther@59718
|
248 |
Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*);
|
walther@59691
|
249 |
"~~~~~ from scan_dn1 to scan_to_tactic1 return val:"; val (xxxxx_xx)
|
walther@59718
|
250 |
= (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
|
walther@59670
|
251 |
|
walther@59718
|
252 |
"~~~~~ from scan_to_tactic1 to fun locate_input_tactic return val:"; val Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac')
|
walther@59718
|
253 |
= (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
|
walther@59686
|
254 |
(*if*) LibraryC.assoc (*then*);
|
walther@59670
|
255 |
|
walther@59686
|
256 |
Safe_Step (Istate.Pstate ist, ctxt, tac') (*return value*);
|
walther@59751
|
257 |
"~~~~~ from locate_input_tactic to fun Step_Solve.by_tactic return:"; val Safe_Step (istate, ctxt, tac)
|
walther@59686
|
258 |
= (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate ist, ctxt, tac')(**);
|
walther@59670
|
259 |
|
walther@59751
|
260 |
(*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of by_tactic *)
|
walther@59686
|
261 |
val (p'', _, _,pt') =
|
walther@59932
|
262 |
Step.add tac (istate, ctxt) (pt, (lev_on p, Pbl));
|
walther@59686
|
263 |
(*in*)
|
walther@59670
|
264 |
|
walther@59704
|
265 |
("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
|
walther@59686
|
266 |
[(*ctree NOT cut*)], (pt', p''))) (*return value*);
|
walther@59981
|
267 |
"~~~~~ from Step_Solve.by_tactic \<longrightarrow> Step.by_tactic return:"; val ((msg, cs' : Calc.state_post))
|
walther@59806
|
268 |
= ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)) )],
|
walther@59806
|
269 |
[(*ctree NOT cut*)], (pt', p'')));
|
walther@59670
|
270 |
|
walther@59804
|
271 |
"~~~~~ from Step.by_tactic to me return:"; val (("ok", (_, _, (pt, p)))) = (*** )xxxx( ***) ("ok", cs');
|
wneuper@59562
|
272 |
val (_, ts) =
|
walther@59765
|
273 |
(case Step.do_next p ((pt, Pos.e_pos'), []) of
|
wneuper@59562
|
274 |
("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
|
wneuper@59562
|
275 |
| ("helpless", _) => ("helpless: cannot propose tac", [])
|
wneuper@59562
|
276 |
| ("no-fmz-spec", _) => error "no-fmz-spec"
|
wneuper@59562
|
277 |
| ("end-of-calculation", (ts, _, _)) => ("", ts)
|
wneuper@59562
|
278 |
| _ => error "me: uncovered case")
|
wneuper@59562
|
279 |
handle ERROR msg => raise ERROR msg
|
wneuper@59562
|
280 |
val tac =
|
wneuper@59562
|
281 |
case ts of
|
wneuper@59562
|
282 |
tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
|
walther@59694
|
283 |
| _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
|
wneuper@59562
|
284 |
|
walther@59937
|
285 |
(p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
|
walther@59670
|
286 |
"~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt)
|
walther@59937
|
287 |
= (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
|
walther@59670
|
288 |
|
walther@59670
|
289 |
(*//--------------------- check results from modified me ----------------------------------\\*)
|
walther@59686
|
290 |
if p = ([2], Res) andalso
|
walther@59686
|
291 |
pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 = 2\n"
|
walther@59670
|
292 |
then
|
walther@59670
|
293 |
(case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => ()
|
walther@59670
|
294 |
| _ => error "")
|
walther@59670
|
295 |
else error "check results from modified me CHANGED";
|
walther@59670
|
296 |
(*\\--------------------- check results from modified me ----------------------------------//*)
|
walther@59670
|
297 |
|
walther@59670
|
298 |
"~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**);
|
walther@59781
|
299 |
(*\\------------------ end step into --------------------------------------------------------//*)
|
walther@59686
|
300 |
|
walther@59686
|
301 |
(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_''' p'''''_''' [] pt'''''_'''; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
|
walther@59670
|
302 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
|
walther@60324
|
303 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
|
walther@59670
|
304 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
|
walther@59670
|
305 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
|
walther@59670
|
306 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
|
walther@59670
|
307 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
|
walther@59670
|
308 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
|
walther@59670
|
309 |
(*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
|
walther@59670
|
310 |
(*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
|
walther@59670
|
311 |
(*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
|
walther@59670
|
312 |
(*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
|
wneuper@59562
|
313 |
(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
|
wneuper@59562
|
314 |
(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
|
wneuper@59562
|
315 |
(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
|
wneuper@59562
|
316 |
|
walther@59670
|
317 |
(*/--------------------- final test ----------------------------------\\*)
|
walther@59749
|
318 |
if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
|
walther@59670
|
319 |
". ----- pblobj -----\n" ^
|
walther@59670
|
320 |
"1. x + 1 = 2\n" ^
|
walther@60324
|
321 |
"2. x + 1 + - 1 * 2 = 0\n" ^
|
walther@59670
|
322 |
"3. ----- pblobj -----\n" ^
|
walther@60324
|
323 |
"3.1. - 1 + x = 0\n" ^
|
walther@60324
|
324 |
"3.2. x = 0 + - 1 * - 1\n" ^
|
walther@59670
|
325 |
"4. [x = 1]\n"
|
walther@59749
|
326 |
then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_tactic changed 1"
|
walther@59749
|
327 |
else error "re-build: fun locate_input_tactic changed 2";
|
wneuper@59562
|
328 |
|
walther@59670
|
329 |
|
walther@59997
|
330 |
"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
|
walther@59997
|
331 |
"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
|
walther@59997
|
332 |
"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
|
walther@59670
|
333 |
(*cp from -- try fun applyTactics ------- *)
|
walther@59670
|
334 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
|
walther@59670
|
335 |
"normalform N"],
|
walther@59997
|
336 |
("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
|
walther@59997
|
337 |
["simplification", "for_polynomials", "with_minus"]))];
|
walther@59670
|
338 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59670
|
339 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59670
|
340 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60330
|
341 |
(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*)
|
walther@60324
|
342 |
|
walther@60330
|
343 |
(*+*)val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f
|
walther@60330
|
344 |
|
walther@60330
|
345 |
(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
|
walther@60330
|
346 |
|
walther@59846
|
347 |
(*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
|
walther@60387
|
348 |
["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
|
walther@60387
|
349 |
"Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
|
walther@60351
|
350 |
(*this is new since ThmC.numerals_to_Free.-----\\*)
|
walther@60330
|
351 |
"Calculate PLUS"]
|
Walther@60441
|
352 |
then () else error "specific_from_prog ([1], Res) 1 CHANGED";
|
walther@60330
|
353 |
(*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
|
walther@60330
|
354 |
|
walther@60352
|
355 |
(*+*)if map Tactic.input_to_string (specific_from_prog pt p) = [
|
walther@60352
|
356 |
"Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")",
|
walther@60387
|
357 |
"Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
|
walther@60387
|
358 |
"Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
|
walther@60352
|
359 |
(*this is new since ThmC.numerals_to_Free.-----\\*)
|
walther@60352
|
360 |
"Calculate PLUS",
|
walther@60352
|
361 |
(*this is new since ThmC.numerals_to_Free.-----//*)
|
walther@60352
|
362 |
"Calculate MINUS"]
|
walther@60351
|
363 |
then () else error "specific_from_prog ([1], Res) 2 CHANGED";
|
walther@59823
|
364 |
(* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
|
walther@59670
|
365 |
|
walther@59670
|
366 |
(*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
|
walther@60351
|
367 |
(**)val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*)
|
walther@59921
|
368 |
Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
|
walther@59921
|
369 |
"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (hd (specific_from_prog pt p), (pt, p));
|
walther@59921
|
370 |
val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
|
walther@59755
|
371 |
(*if*) Tactic.for_specify' m; (*false*)
|
walther@59670
|
372 |
|
walther@60351
|
373 |
(**) val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*)
|
walther@59806
|
374 |
Step_Solve.by_tactic m (pt, p);
|
walther@59806
|
375 |
"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
|
walther@60154
|
376 |
(*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
|
walther@59670
|
377 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
Walther@60559
|
378 |
val (is, sc) = LItool.resume_prog (p,p_) pt;
|
walther@59670
|
379 |
|
walther@59686
|
380 |
(*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
|
walther@59692
|
381 |
"~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac)
|
walther@59670
|
382 |
= (sc, (pt, po), (fst is), (snd is), m);
|
walther@59790
|
383 |
val srls = LItool.get_simplifier cstate (*TODO: shift into Istate.T*);
|
walther@59670
|
384 |
|
walther@59692
|
385 |
(*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
|
walther@59692
|
386 |
"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
|
walther@59692
|
387 |
= ((prog, (cstate, ctxt, tac)), istate);
|
walther@59686
|
388 |
(*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
|
walther@59670
|
389 |
|
walther@59692
|
390 |
go_scan_up1 (prog, cctt) ist;
|
walther@59997
|
391 |
"~~~~~ fun go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
|
walther@59692
|
392 |
= ((prog, cctt), ist);
|
walther@59686
|
393 |
(*if*) 1 < length path (*then*);
|
walther@59670
|
394 |
|
walther@60023
|
395 |
scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
|
walther@60336
|
396 |
"~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ _))
|
walther@60023
|
397 |
= (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
|
walther@59670
|
398 |
|
walther@59997
|
399 |
go_scan_up1 pcct ist;
|
walther@59997
|
400 |
"~~~~~ and go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
|
walther@59997
|
401 |
= (pcct, ist);
|
walther@59686
|
402 |
(*if*) 1 < length path (*then*);
|
walther@59670
|
403 |
|
walther@60023
|
404 |
scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
|
walther@59997
|
405 |
"~~~~~ and scan_up1 , args:"; val ((pcct as (prog, cct as (cstate, _, _))), ist,
|
walther@60336
|
406 |
(Const (\<^const_name>\<open>Chain\<close>(*3*), _) $ _ ))
|
walther@60023
|
407 |
= (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
|
walther@59692
|
408 |
val e2 = check_Seq_up ist prog
|
walther@59686
|
409 |
;
|
walther@59997
|
410 |
(*case*) scan_dn1 cct (ist |> path_up_down [R] |> set_or ORundef) e2 (*of*);
|
walther@60336
|
411 |
"~~~~~ fun scan_dn1 , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Chain\<close>(*2*), _) $ e1 $ e2))
|
walther@59997
|
412 |
= (cct, (ist |> path_up_down [R] |> set_or ORundef), e2);
|
walther@59670
|
413 |
|
walther@59997
|
414 |
(*case*) scan_dn1 cct (ist |> path_down [L, R]) e1 (*of*);
|
walther@60336
|
415 |
"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ e))
|
walther@59997
|
416 |
= (cct, (ist |> path_down [L, R]), e1);
|
walther@59670
|
417 |
|
walther@59997
|
418 |
(*case*) scan_dn1 cct (ist |> path_down [R]) e (*of*);
|
walther@59686
|
419 |
(*======= end of scanning tacticals, a leaf =======*)
|
walther@59997
|
420 |
"~~~~~ fun scan_dn1 , args:"; val ((cct as (_, ctxt, _)), (ist as {eval, ...}), t)
|
walther@59997
|
421 |
= (cct, (ist |> path_down [R]), e);
|
walther@59997
|
422 |
(*if*) Tactical.contained_in t (*else*);
|
walther@59997
|
423 |
val (Program.Tac prog_tac, form_arg) = (*case*)
|
walther@59997
|
424 |
LItool.check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
|
walther@59997
|
425 |
|
walther@59997
|
426 |
check_tac1 cct ist (prog_tac, form_arg);
|
walther@59997
|
427 |
"~~~~~ fun check_tac1 , args:"; val (((pt, p), ctxt, tac), (ist as {act_arg, or, ...}), (prog_tac, form_arg)) =
|
walther@59997
|
428 |
(cct, ist, (prog_tac, form_arg));
|
walther@59997
|
429 |
val LItool.Not_Associated = (*case*)
|
walther@59997
|
430 |
LItool.associate pt ctxt (tac, prog_tac) (*of*);
|
walther@59997
|
431 |
val _(*ORundef*) = (*case*) or (*of*);
|
walther@60324
|
432 |
|
walther@60330
|
433 |
(*+*)Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p);
|
walther@60324
|
434 |
|
walther@59997
|
435 |
val Applicable.Yes m' =
|
walther@59997
|
436 |
(*case*) Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p) (*of*);
|
walther@59997
|
437 |
|
walther@59997
|
438 |
Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
|
walther@59997
|
439 |
(*return from check_tac1*);
|
walther@59997
|
440 |
"~~~~~ from fun check_tac1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun locate_input_tactic , return:"; val (Reject_Tac1 _) =
|
walther@59997
|
441 |
(Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac));
|
walther@59997
|
442 |
|
walther@60351
|
443 |
val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f;
|
walther@60351
|
444 |
val ([3], Res) = p;
|
walther@60324
|
445 |
|
walther@59680
|
446 |
|
walther@59792
|
447 |
"----------- re-build: fun find_next_step, mini ------------------------------------------------";
|
walther@59792
|
448 |
"----------- re-build: fun find_next_step, mini ------------------------------------------------";
|
walther@59792
|
449 |
"----------- re-build: fun find_next_step, mini ------------------------------------------------";
|
walther@59792
|
450 |
val fmz = ["Term (a + a ::real)", "normalform n_n"];
|
walther@59997
|
451 |
val (dI',pI',mI') = ("Poly",["polynomial", "simplification"],["simplification", "for_polynomials"]);
|
walther@59734
|
452 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59765
|
453 |
(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Model_Problem*)
|
walther@59792
|
454 |
(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Theory "Poly"*)
|
walther@59792
|
455 |
(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Problem ["polynomial", "simplification"]*)
|
walther@59792
|
456 |
(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["simplification", "for_polynomials"]*)
|
walther@59792
|
457 |
(*1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["simplification", "for_polynomials"]*)
|
walther@59792
|
458 |
(*[1], Res*)val (_, ([(tac'''''_', _, _)], _, (pt'''''_', p'''''_'))) =
|
walther@59734
|
459 |
|
walther@59792
|
460 |
Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_Poly"*)
|
walther@59792
|
461 |
(*//------------------ go into 1 ------------------------------------------------------------\\*)
|
walther@59792
|
462 |
"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
|
walther@59792
|
463 |
= (p, ((pt, e_pos'), []));
|
walther@59792
|
464 |
val pIopt = Ctree.get_pblID (pt, ip);
|
walther@59792
|
465 |
(*if*) ip = ([], Res) (*else*);
|
walther@59792
|
466 |
val _ = (*case*) tacis (*of*);
|
walther@59792
|
467 |
val SOME _ = (*case*) pIopt (*of*);
|
walther@60017
|
468 |
(*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
|
walther@59734
|
469 |
|
walther@59792
|
470 |
val ("ok", ([(Rewrite_Set "norm_Poly", _, _)], _, (_, ([1], Res)))) =
|
walther@59792
|
471 |
Step_Solve.do_next (pt, ip);
|
walther@59792
|
472 |
"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
|
walther@60154
|
473 |
(*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
|
walther@59734
|
474 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
Walther@60559
|
475 |
val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
|
walther@59734
|
476 |
|
walther@59878
|
477 |
val Next_Step (_, _, Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _)) =
|
walther@59792
|
478 |
LI.find_next_step sc (pt, pos) ist ctxt (*of*);
|
walther@59792
|
479 |
"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
|
walther@59734
|
480 |
= (sc, (pt, pos), ist, ctxt);
|
walther@59734
|
481 |
|
walther@59878
|
482 |
val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
|
walther@59792
|
483 |
(*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
|
walther@59792
|
484 |
"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
|
walther@59792
|
485 |
= ((prog, (ptp, ctxt)), (Pstate ist));
|
walther@59792
|
486 |
(*if*) path = [] (*then*);
|
walther@59734
|
487 |
|
walther@59878
|
488 |
val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
|
walther@59792
|
489 |
scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
|
walther@59792
|
490 |
"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
|
walther@59792
|
491 |
= (cc, (trans_scan_dn ist), (Program.body_of prog));
|
walther@59792
|
492 |
(*if*) Tactical.contained_in t (*else*);
|
walther@59792
|
493 |
val (Program.Tac prog_tac, form_arg) = (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
|
walther@59734
|
494 |
|
walther@59878
|
495 |
val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
|
walther@59799
|
496 |
check_tac cc ist (prog_tac, form_arg) (*return from xxx*);
|
walther@59792
|
497 |
"~~~~~ from fun scan_dn\<longrightarrow>fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Accept_Tac (tac, ist, ctxt))
|
walther@59799
|
498 |
= (check_tac cc ist (prog_tac, form_arg));
|
walther@59734
|
499 |
|
walther@59792
|
500 |
Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac) (*return from find_next_step*);
|
walther@59792
|
501 |
"~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (Next_Step (ist, ctxt, tac))
|
walther@59792
|
502 |
= (Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac));
|
walther@59734
|
503 |
|
walther@59792
|
504 |
LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp (*return from and do_next*);
|
walther@59792
|
505 |
"~~~~~ from and do_next\<longrightarrow>fun do_next\<longrightarrow>toplevel, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
|
walther@59793
|
506 |
= (LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp);
|
walther@59792
|
507 |
(*\\------------------ end of go into 1 -----------------------------------------------------//*)
|
walther@59734
|
508 |
|
walther@59792
|
509 |
(*[], Res*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) =
|
walther@59792
|
510 |
|
walther@59792
|
511 |
Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []);(* Check_Postcond ["polynomial", "simplification"]*)
|
walther@59792
|
512 |
(*//------------------ go into 2 ------------------------------------------------------------\\*)
|
walther@59792
|
513 |
"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
|
walther@59792
|
514 |
= (p''''', ((pt''''', e_pos'), []));
|
walther@59792
|
515 |
val pIopt = Ctree.get_pblID (pt, ip);
|
walther@59792
|
516 |
(*if*) ip = ([], Res) (*else*);
|
walther@59792
|
517 |
val _ = (*case*) tacis (*of*);
|
walther@59792
|
518 |
val SOME _ = (*case*) pIopt (*of*);
|
walther@60017
|
519 |
(*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
|
walther@59792
|
520 |
|
walther@59792
|
521 |
val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res)))) =
|
walther@59792
|
522 |
Step_Solve.do_next (pt, ip);
|
walther@59792
|
523 |
"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
|
walther@60154
|
524 |
(*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
|
walther@59792
|
525 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
Walther@60559
|
526 |
val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
|
walther@59792
|
527 |
|
walther@59792
|
528 |
(** )val End_Program (ist, tac) =
|
walther@59793
|
529 |
( *case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
|
walther@59792
|
530 |
"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
|
walther@59792
|
531 |
= (sc, (pt, pos), ist, ctxt);
|
walther@59792
|
532 |
|
wenzelm@60309
|
533 |
(* val Term_Val (Const (\<^const_name>\<open>times\<close>, _) $ Free ("2", _) $ Free ("a", _))*)
|
Walther@60558
|
534 |
(**)val Term_Val prog_result =
|
Walther@60558
|
535 |
(*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
|
walther@59792
|
536 |
"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
|
walther@59792
|
537 |
= ((prog, (ptp, ctxt)), (Pstate ist));
|
walther@59792
|
538 |
(*if*) path = [] (*else*);
|
walther@59792
|
539 |
|
walther@59792
|
540 |
go_scan_up (prog, cc) (trans_scan_up ist |> set_found);
|
walther@59792
|
541 |
"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
|
walther@59792
|
542 |
= ((prog, cc), (trans_scan_up ist(*|> set_found !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)));
|
walther@59792
|
543 |
(*if*) path = [R] (*then*);
|
walther@59792
|
544 |
(*if*) found_accept = true (*then*);
|
walther@59792
|
545 |
|
walther@59792
|
546 |
Term_Val act_arg (*return from go_scan_up*);
|
walther@59792
|
547 |
"~~~~~ from fun go_scan_up\<longrightarrow>fun scan_to_tactic, return:"; val (Term_Val prog_result) = (Term_Val act_arg);
|
walther@59792
|
548 |
|
walther@59792
|
549 |
Term_Val prog_result (*return from scan_to_tactic*);
|
walther@59792
|
550 |
"~~~~~ from fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Term_Val prog_result) = (Term_Val prog_result);
|
Walther@60559
|
551 |
val (true, p' as [], Rule_Set.Empty, _) = (*case*) parent_node pt pos (*of*);
|
walther@59792
|
552 |
val (_, pblID, _) = get_obj g_spec pt p';
|
walther@59792
|
553 |
|
walther@59843
|
554 |
End_Program (Pstate ist, Tactic.Check_Postcond' (pblID, prog_result))
|
walther@59792
|
555 |
(*return from find_next_step*);
|
walther@59792
|
556 |
"~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (End_Program (ist, tac))
|
walther@59843
|
557 |
= (End_Program (Pstate ist, Tactic.Check_Postcond' (pblID,prog_result)));
|
walther@59792
|
558 |
val _ = (*case*) tac (*of*);
|
walther@59792
|
559 |
|
walther@59792
|
560 |
val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res))))
|
walther@59793
|
561 |
= LI.by_tactic tac (ist, ctxt) ptp (*return from and do_next*);
|
walther@59792
|
562 |
"~~~~~ from and do_next\<longrightarrow>top level, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
|
walther@59793
|
563 |
= (LI.by_tactic tac (ist, ctxt) ptp);
|
walther@59792
|
564 |
(*\\------------------ end of go into 2 -----------------------------------------------------//*)
|
walther@59792
|
565 |
|
walther@59792
|
566 |
(*[], Und*)val (msg, ([], _, (pt, p))) = Step.do_next p''''' ((pt''''', Pos.e_pos'), []);(**)
|
walther@59792
|
567 |
|
walther@59983
|
568 |
Test_Tool.show_pt_tac pt; (*[
|
walther@59792
|
569 |
([], Frm), Simplify (a + a)
|
walther@59997
|
570 |
. . . . . . . . . . Apply_Method ["simplification", "for_polynomials"],
|
walther@59792
|
571 |
([1], Frm), a + a
|
walther@59792
|
572 |
. . . . . . . . . . Rewrite_Set "norm_Poly",
|
walther@59792
|
573 |
([1], Res), 2 * a
|
walther@59997
|
574 |
. . . . . . . . . . Check_Postcond ["polynomial", "simplification"],
|
walther@59792
|
575 |
([], Res), 2 * a]*)
|
walther@59792
|
576 |
|
walther@59792
|
577 |
(*/--- final test ---------------------------------------------------------------------------\\*)
|
walther@59734
|
578 |
val (res, asm) = (get_obj g_result pt (fst p));
|
walther@59868
|
579 |
if UnparseC.term res = "2 * a" andalso map UnparseC.term asm = []
|
walther@59792
|
580 |
andalso p = ([], Und) andalso msg = "end-of-calculation"
|
walther@59792
|
581 |
andalso pr_ctree pr_short pt = ". ----- pblobj -----\n1. a + a\n"
|
walther@59792
|
582 |
then
|
walther@59792
|
583 |
case tac''''' of Check_Postcond ["polynomial", "simplification"] => ()
|
walther@59792
|
584 |
| _ => error "re-build: fun find_next_step, mini 1"
|
walther@59792
|
585 |
else error "re-build: fun find_next_step, mini 2"
|
wneuper@59575
|
586 |
|
wneuper@59575
|
587 |
|
walther@59783
|
588 |
"----------- re-build: fun locate_input_term ---------------------------------------------------";
|
walther@59783
|
589 |
"----------- re-build: fun locate_input_term ---------------------------------------------------";
|
walther@59783
|
590 |
"----------- re-build: fun locate_input_term ---------------------------------------------------";
|
walther@59795
|
591 |
(*cp from inform.sml
|
walther@59795
|
592 |
----------- appendFormula: on Res + late deriv ------------------------------------------------*)
|
walther@59997
|
593 |
val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
|
walther@59997
|
594 |
val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"],
|
walther@59997
|
595 |
["Test", "squ-equ-test-subpbl1"]);
|
walther@59795
|
596 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59795
|
597 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59795
|
598 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59795
|
599 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59795
|
600 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59795
|
601 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59795
|
602 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59795
|
603 |
(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["Test", "squ-equ-test-subpbl1"]*);
|
walther@59783
|
604 |
|
walther@59795
|
605 |
(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "norm_equation"*)
|
walther@59795
|
606 |
(*+*)if f2str f = "x + 1 = 2" then () else error "locate_input_term at ([1], Frm) CHANGED";
|
walther@59783
|
607 |
|
walther@59795
|
608 |
(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "Test_simplify"*)
|
walther@60324
|
609 |
(*+*)if f2str f = "x + 1 + - 1 * 2 = 0" then () else error "locate_input_term at ([1], Frm) CHANGED";
|
walther@59783
|
610 |
|
walther@59983
|
611 |
Test_Tool.show_pt_tac pt; (*[
|
walther@59795
|
612 |
([], Frm), solve (x + 1 = 2, x)
|
walther@59997
|
613 |
. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
|
walther@59795
|
614 |
([1], Frm), x + 1 = 2
|
walther@59795
|
615 |
. . . . . . . . . . Rewrite_Set "norm_equation",
|
walther@60324
|
616 |
([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond..ERROR*)
|
walther@59795
|
617 |
|
walther@59797
|
618 |
(*//---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------\\*)
|
walther@59868
|
619 |
"~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: TermC.as_string) = ((**) "x = 1");
|
Walther@60549
|
620 |
val cs = (*States.get_calc cI*) ((pt, p), [(*nxt, nxt_, (pos, (ist, ctxt))*)])
|
Walther@60549
|
621 |
val pos = (*States.get_pos cI 1*) p
|
walther@59795
|
622 |
|
walther@59795
|
623 |
(*+*)val ptp''''' = (pt, p);
|
walther@59795
|
624 |
(*+*)if snd ptp''''' = ([1], Res) then () else error "old_cs changed";
|
walther@59983
|
625 |
(*+*)Test_Tool.show_pt_tac pt; (*[
|
walther@59795
|
626 |
(*+*)([], Frm), solve (x + 1 = 2, x)
|
walther@59997
|
627 |
(*+*). . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
|
walther@59795
|
628 |
(*+*)([1], Frm), x + 1 = 2
|
walther@59795
|
629 |
(*+*). . . . . . . . . . Rewrite_Set "norm_equation",
|
walther@60324
|
630 |
(*+*)([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond*)
|
walther@59795
|
631 |
|
walther@59798
|
632 |
val ("ok", cs' as (_, _, ptp')) =
|
walther@59795
|
633 |
(*case*) Step.do_next pos cs (*of*);
|
walther@59795
|
634 |
|
walther@59795
|
635 |
val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p'''''))) = (*case*)
|
walther@59798
|
636 |
Step_Solve.by_term ptp' (encode ifo) (*of*);
|
walther@59798
|
637 |
"~~~~~ fun Step_Solve.by_term , args:"; val ((pt, pos as (p, _)), istr)
|
walther@59798
|
638 |
= (ptp', (encode ifo));
|
walther@59795
|
639 |
val SOME f_in =
|
Walther@60424
|
640 |
(*case*) TermC.parseNEW (get_ctxt pt pos) istr (*of*);
|
walther@59795
|
641 |
val pos_pred = lev_back(*'*) pos
|
walther@59795
|
642 |
val f_pred = Ctree.get_curr_formula (pt, pos_pred);
|
walther@59795
|
643 |
val f_succ = Ctree.get_curr_formula (pt, pos);
|
walther@59795
|
644 |
(*if*) f_succ = f_in (*else*);
|
walther@59795
|
645 |
val NONE =
|
walther@59982
|
646 |
(*case*) CAS_Cmd.input f_in (*of*);
|
walther@59795
|
647 |
|
walther@59795
|
648 |
(*NEW*) LI.locate_input_term (pt, pos) f_in (*of*);
|
walther@59795
|
649 |
"~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
|
walther@59795
|
650 |
val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
|
walther@59795
|
651 |
|
walther@59795
|
652 |
val ("ok", (_, _, cstate as (pt', pos'))) =
|
walther@59795
|
653 |
(*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
|
walther@59795
|
654 |
|
walther@59795
|
655 |
(*old* )
|
walther@59807
|
656 |
Found_Step (cstate, get_istate_LI pt' pos', get_ctxt pt' pos') (*return from locate_input_term*);
|
walther@59795
|
657 |
( *old*)
|
walther@59795
|
658 |
(*NEW*) Found_Step cstate (*return from locate_input_term*);
|
Walther@60533
|
659 |
(*LI.Found_Step ( *)cstate(*, _(*istate*), _)( *return from locate_input_term*);
|
walther@59797
|
660 |
"~~~~~ from fun locate_input_term\<longrightarrow>fun Step_Solve.by_term, return:"; val ("ok", (_(*use in DG !!!*), c, ptp as (_, p)))
|
walther@59795
|
661 |
= (("ok" , ([], [], cstate (* already contains istate, ctxt *))));
|
walther@59795
|
662 |
|
walther@59797
|
663 |
("ok", ((*_ use in DG !!!,*) c, ptp(* as (_*), p))(*)*)(*return from Step_Solve.by_term*);
|
walther@59797
|
664 |
"~~~~~ from fun Step_Solve.by_term\<longrightarrow>(fun appendFormula)!toplevel, return:"; val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p''''')))
|
walther@59795
|
665 |
= ("ok", ([], [], ptp));
|
walther@59795
|
666 |
|
walther@59795
|
667 |
(*fun me requires nxt...*)
|
walther@59795
|
668 |
Step.do_next p''''' (ptp''''', []);
|
walther@59795
|
669 |
val ("ok", ([(nxt'''''_' as Check_Postcond ["LINEAR", "univariate", "equation", "test"], _, _)], _,
|
walther@59795
|
670 |
(pt'''''_', p'''''_'))) = Step.do_next p''''' (ptp''''', [])
|
walther@59797
|
671 |
(*\\---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------//*)
|
walther@59795
|
672 |
|
walther@59797
|
673 |
(*//----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----\\* )
|
walther@59795
|
674 |
(*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
|
walther@59795
|
675 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
|
walther@60324
|
676 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
|
walther@59795
|
677 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
|
walther@59795
|
678 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
|
walther@59795
|
679 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
|
walther@59795
|
680 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
|
walther@59795
|
681 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
|
walther@59795
|
682 |
(*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
|
walther@59795
|
683 |
(*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
|
walther@59795
|
684 |
(*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
|
walther@59795
|
685 |
(*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
|
walther@59797
|
686 |
( *\\----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----//*)
|
walther@59795
|
687 |
|
walther@59795
|
688 |
(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_' p'''''_' [] pt'''''_'; (*nxt = Check_elementwise "Assumptions"*)
|
walther@59795
|
689 |
(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
|
walther@59795
|
690 |
(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
|
walther@59795
|
691 |
|
walther@59795
|
692 |
(*/--- final test ---------------------------------------------------------------------------\\*)
|
walther@59795
|
693 |
if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
|
walther@59795
|
694 |
". ----- pblobj -----\n" ^
|
walther@59795
|
695 |
"1. x + 1 = 2\n" ^
|
walther@60324
|
696 |
"2. x + 1 + - 1 * 2 = 0\n" ^
|
walther@59795
|
697 |
"3. ----- pblobj -----\n" ^
|
walther@60324
|
698 |
"3.1. - 1 + x = 0\n" ^
|
walther@60324
|
699 |
"3.2. x = 0 + - 1 * - 1\n" ^
|
walther@60324
|
700 |
"3.2.1. x = 0 + - 1 * - 1\n" ^
|
walther@59795
|
701 |
"3.2.2. x = 0 + 1\n" (*ATTENTION: see complete Calc below*)
|
walther@59795
|
702 |
then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_term CHANGED 1"
|
walther@59795
|
703 |
else error "re-build: fun locate_input_term CHANGED 2";
|
walther@59795
|
704 |
|
walther@59983
|
705 |
Test_Tool.show_pt_tac pt; (*[
|
walther@59795
|
706 |
([], Frm), solve (x + 1 = 2, x)
|
walther@59997
|
707 |
. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
|
walther@59795
|
708 |
([1], Frm), x + 1 = 2
|
walther@59795
|
709 |
. . . . . . . . . . Rewrite_Set "norm_equation",
|
walther@60324
|
710 |
([1], Res), x + 1 + - 1 * 2 = 0
|
walther@59795
|
711 |
. . . . . . . . . . Rewrite_Set "Test_simplify",
|
walther@60324
|
712 |
([2], Res), - 1 + x = 0
|
walther@59997
|
713 |
. . . . . . . . . . Subproblem (Test, ["LINEAR", "univariate", "equation", "test"]),
|
walther@60324
|
714 |
([3], Pbl), solve (- 1 + x = 0, x)
|
walther@59997
|
715 |
. . . . . . . . . . Apply_Method ["Test", "solve_linear"],
|
walther@60324
|
716 |
([3,1], Frm), - 1 + x = 0
|
walther@59795
|
717 |
. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv"),
|
walther@60324
|
718 |
([3,1], Res), x = 0 + - 1 * - 1
|
walther@59795
|
719 |
. . . . . . . . . . Derive Test_simplify,
|
walther@60324
|
720 |
([3,2,1], Frm), x = 0 + - 1 * - 1
|
walther@60324
|
721 |
. . . . . . . . . . Rewrite ("#: - 1 * - 1 = 1", "- 1 * - 1 = 1"),
|
walther@59795
|
722 |
([3,2,1], Res), x = 0 + 1
|
walther@59795
|
723 |
. . . . . . . . . . Rewrite ("radd_0", "0 + ?k = ?k"),
|
walther@59795
|
724 |
([3,2,2], Res), x = 1
|
walther@59846
|
725 |
. . . . . . . . . . Tactic.input_to_string not impl. for ?!,
|
walther@59795
|
726 |
([3,2], Res), x = 1
|
walther@59997
|
727 |
. . . . . . . . . . Check_Postcond ["LINEAR", "univariate", "equation", "test"],
|
walther@59795
|
728 |
([3], Res), [x = 1]
|
walther@59997
|
729 |
. . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
|
walther@59795
|
730 |
([], Res), [x = 1]]*)
|