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@59670
|
11 |
"----------- fun locate_input_tactic Helpless, but applicable ----------------------------------";
|
walther@59743
|
12 |
"----------- re-build: fun find_next_tactic ----------------------------------------------------";
|
wneuper@59564
|
13 |
"----------- re-build: fun locate_input_formula ------------------------------------------------";
|
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 -------------------------------------------------------";
|
wneuper@59561
|
21 |
val p = e_pos'; val c = [];
|
wneuper@59561
|
22 |
val (p,_,f,nxt,_,pt) =
|
wneuper@59561
|
23 |
CalcTreeTEST
|
wneuper@59561
|
24 |
[(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
|
wneuper@59561
|
25 |
("Integrate", ["integrate","function"], ["diff","integration"]))];
|
wneuper@59561
|
26 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
|
wneuper@59561
|
27 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
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;
|
wneuper@59561
|
32 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@59749
|
33 |
case nxt of (Apply_Method ["diff", "integration"]) => ()
|
wneuper@59561
|
34 |
| _ => error "integrate.sml -- me method [diff,integration] -- spec";
|
wneuper@59561
|
35 |
"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
|
wneuper@59561
|
36 |
|
walther@59749
|
37 |
"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
|
wneuper@59561
|
38 |
"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
|
wneuper@59561
|
39 |
val (mI,m) = mk_tac'_ tac;
|
wneuper@59561
|
40 |
val Appl m = applicable_in p pt m;
|
wneuper@59561
|
41 |
member op = specsteps mI (*false*);
|
walther@59749
|
42 |
"~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp);
|
walther@59686
|
43 |
|
walther@59751
|
44 |
"~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))
|
walther@59749
|
45 |
= (m, (pt, pos));
|
walther@59686
|
46 |
val {srls, ...} = get_met mI;
|
walther@59686
|
47 |
val itms = case get_obj I pt p of
|
walther@59686
|
48 |
PblObj {meth=itms, ...} => itms
|
walther@59686
|
49 |
| _ => error "solve Apply_Method: uncovered case get_obj"
|
walther@59686
|
50 |
val thy' = get_obj g_domID pt p;
|
walther@59686
|
51 |
val thy = Celem.assoc_thy thy';
|
walther@59686
|
52 |
val srls = Lucin.get_simplifier (pt, pos)
|
walther@59686
|
53 |
val (is, env, ctxt, sc) = case Lucin.init_pstate srls ctxt itms mI of
|
walther@59686
|
54 |
(is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
|
walther@59697
|
55 |
| _ => error "solve Apply_Method: uncovered case init_pstate";
|
walther@59718
|
56 |
(*+*)scrstate2str (the_pstate is) = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, ORundef, AppUndef_, true)";
|
walther@59686
|
57 |
val ini = Lucin.init_form thy sc env;
|
walther@59686
|
58 |
val p = lev_dn p;
|
walther@59686
|
59 |
|
walther@59686
|
60 |
val NONE = (*case*) ini (*of*);
|
walther@59734
|
61 |
val Next_Step (is', ctxt', m') =
|
walther@59743
|
62 |
LucinNEW.find_next_tactic sc (pt, (p, Res)) is ctxt;
|
walther@59718
|
63 |
(*+*)scrstate2str (the_pstate is') = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], e_rls, NONE, \nIntegral x ^^^ 2 + 1 D x, ORundef, AppUndef_, false)";
|
walther@59686
|
64 |
val Safe_Step (_, _, Take' _) = (*case*)
|
walther@59686
|
65 |
locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);
|
walther@59692
|
66 |
"~~~~~ fun locate_input_tactic , args:"; val ((Prog prog), cstate, istate, ctxt, tac)
|
walther@59686
|
67 |
= (sc, (pt, (p, Res)), is', ctxt', m');
|
walther@59686
|
68 |
|
walther@59692
|
69 |
(*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
|
walther@59692
|
70 |
"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
|
walther@59692
|
71 |
= ((prog, (cstate, ctxt, tac)), istate);
|
walther@59686
|
72 |
(*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
|
walther@59686
|
73 |
|
walther@59718
|
74 |
val Accept_Tac1 (_, _, Take' _) =
|
walther@59718
|
75 |
scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
|
walther@59691
|
76 |
"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
|
walther@59718
|
77 |
= (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
|
walther@59686
|
78 |
|
walther@59691
|
79 |
(*+*) if term2str e = "Take (Integral f_f D v_v)" then () else error "scan_dn1 Integral changed";
|
walther@59686
|
80 |
|
walther@59686
|
81 |
(*case*)
|
walther@59691
|
82 |
scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
|
walther@59686
|
83 |
(*======= end of scanning tacticals, a leaf =======*)
|
walther@59722
|
84 |
"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, or, ...}), t)
|
walther@59686
|
85 |
= (xxx, (ist |> path_down [L, R]), e);
|
walther@59722
|
86 |
val (Program.Tac stac, a') = interpret_leaf "locate" ctxt eval (get_subst ist) t;
|
wneuper@59561
|
87 |
|
wneuper@59561
|
88 |
|
walther@59670
|
89 |
"----------- re-build: fun locate_input_tactic -------------------------------------------------";
|
walther@59670
|
90 |
"----------- re-build: fun locate_input_tactic -------------------------------------------------";
|
walther@59670
|
91 |
"----------- re-build: fun locate_input_tactic -------------------------------------------------";
|
wneuper@59562
|
92 |
val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
|
walther@59670
|
93 |
val (dI',pI',mI') = ("Test", ["sqroot-test","univariate","equation","test"],
|
wneuper@59562
|
94 |
["Test","squ-equ-test-subpbl1"]);
|
wneuper@59562
|
95 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
wneuper@59562
|
96 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
wneuper@59562
|
97 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
wneuper@59562
|
98 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
wneuper@59562
|
99 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
wneuper@59562
|
100 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
wneuper@59562
|
101 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59670
|
102 |
(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
|
walther@59670
|
103 |
(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
|
wneuper@59562
|
104 |
|
walther@59670
|
105 |
(*// relevant call --------------------------------------------------------------------------\\*)
|
walther@59686
|
106 |
(*[1], Res*)val (p'''''_''',_,f,nxt'''''_''',_,pt'''''_''') = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
|
wneuper@59562
|
107 |
|
walther@59749
|
108 |
"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
|
wneuper@59562
|
109 |
|
walther@59670
|
110 |
(** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*) locatetac tac (pt,p) (*of*);
|
walther@59670
|
111 |
"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
|
walther@59670
|
112 |
val (mI, m) = Solve.mk_tac'_ tac;
|
walther@59737
|
113 |
val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
|
walther@59670
|
114 |
(*if*) member op = Solve.specsteps mI; (*else*)
|
walther@59670
|
115 |
|
walther@59749
|
116 |
(** )val (***)xxxxx(***) ( *Updated (cs' as (_, _, (_, p'))) =( **) loc_solve_ m ptp;
|
walther@59749
|
117 |
"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = (m, ptp);
|
walther@59670
|
118 |
|
walther@59751
|
119 |
(** )val (***)xxxxx_x(***) ( *(msg, cs') =( **) Step_Solve.by_tactic m (pt, pos);
|
walther@59751
|
120 |
"~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, pos));
|
walther@59670
|
121 |
(*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
|
walther@59670
|
122 |
(*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*)
|
walther@59670
|
123 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
walther@59670
|
124 |
val (_, is, sc) = Lucin.from_pblobj' thy' (p,p_) pt;
|
walther@59670
|
125 |
|
walther@59670
|
126 |
locate_input_tactic sc (pt, po) (fst is) (snd is) m;
|
walther@59692
|
127 |
"~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac)
|
walther@59670
|
128 |
= (sc, (pt, po), (fst is), (snd is), m);
|
walther@59670
|
129 |
val srls = get_simplifier cstate;
|
walther@59670
|
130 |
|
walther@59718
|
131 |
(** )val Accept_Tac1 ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
|
walther@59692
|
132 |
(*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
|
walther@59692
|
133 |
"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
|
walther@59692
|
134 |
= ((prog, (cstate, ctxt, tac)), istate);
|
walther@59686
|
135 |
(*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
|
walther@59670
|
136 |
|
walther@59670
|
137 |
(** )val xxxxx_xx = ( **)
|
walther@59718
|
138 |
scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
|
walther@59691
|
139 |
"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
|
walther@59718
|
140 |
= (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
|
walther@59670
|
141 |
|
walther@59691
|
142 |
(*case*) scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
|
walther@59691
|
143 |
"~~~~~ fun scan_dn1 , args:"; val ((xxx as (cstate, _, _)), ist, (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a))
|
walther@59686
|
144 |
= (xxx, (ist |> path_down [L, R]), e);
|
walther@59670
|
145 |
|
walther@59691
|
146 |
(*case*) scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
|
walther@59691
|
147 |
"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("Tactical.Try"(*2*), _) $ e))
|
walther@59686
|
148 |
= (xxx, (ist |> path_down_form ([L, L, R], a)), e1);
|
walther@59670
|
149 |
|
walther@59691
|
150 |
(*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*);
|
walther@59670
|
151 |
(*======= end of scanning tacticals, a leaf =======*)
|
walther@59691
|
152 |
"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
|
walther@59686
|
153 |
= (xxx, (ist |> path_down [R]), e);
|
walther@59721
|
154 |
val (Program.Tac stac, a') =
|
walther@59722
|
155 |
(*case*) interpret_leaf "locate" ctxt eval (get_subst ist) t (*of*);
|
walther@59686
|
156 |
val Lucin.Ass (m, v', ctxt) =
|
walther@59686
|
157 |
(*case*) associate pt ctxt (m, stac) (*of*);
|
walther@59670
|
158 |
|
walther@59718
|
159 |
Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*);
|
walther@59691
|
160 |
"~~~~~ from scan_dn1 to scan_to_tactic1 return val:"; val (xxxxx_xx)
|
walther@59718
|
161 |
= (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
|
walther@59670
|
162 |
|
walther@59718
|
163 |
"~~~~~ from scan_to_tactic1 to fun locate_input_tactic return val:"; val Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac')
|
walther@59718
|
164 |
= (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
|
walther@59686
|
165 |
(*if*) LibraryC.assoc (*then*);
|
walther@59670
|
166 |
|
walther@59686
|
167 |
Safe_Step (Istate.Pstate ist, ctxt, tac') (*return value*);
|
walther@59751
|
168 |
"~~~~~ from locate_input_tactic to fun Step_Solve.by_tactic return:"; val Safe_Step (istate, ctxt, tac)
|
walther@59686
|
169 |
= (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate ist, ctxt, tac')(**);
|
walther@59670
|
170 |
|
walther@59751
|
171 |
(*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of by_tactic *)
|
walther@59686
|
172 |
val (p'', _, _,pt') =
|
walther@59686
|
173 |
Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
|
walther@59686
|
174 |
(* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
|
walther@59686
|
175 |
(istate, ctxt) (lev_on p, Pbl) pt;
|
walther@59686
|
176 |
(*in*)
|
walther@59670
|
177 |
|
walther@59704
|
178 |
("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
|
walther@59686
|
179 |
[(*ctree NOT cut*)], (pt', p''))) (*return value*);
|
walther@59751
|
180 |
"~~~~~ from Step_Solve.by_tactic to loc_solve_ return:"; val ((msg, cs' : calcstate'))
|
walther@59704
|
181 |
= ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)) )], [(*ctree NOT cut*)], (pt', p'')));
|
walther@59670
|
182 |
|
walther@59670
|
183 |
"~~~~~ from loc_solve_ to locatetac return:"; val (Updated (cs' as (_, _, (_, p'))))
|
walther@59670
|
184 |
= (*** )xxxxx( ***) (Updated (cs'));
|
walther@59694
|
185 |
(*if*) p' = ([], Pos.Res); (*else*)
|
walther@59670
|
186 |
("ok", cs');
|
walther@59670
|
187 |
"~~~~~ from locatetac to me return:"; val (("ok", (_, _, (pt, p)))) = (*** )xxxx( ***) ("ok", cs');
|
wneuper@59562
|
188 |
val (_, ts) =
|
walther@59694
|
189 |
(case step p ((pt, Pos.e_pos'), []) of
|
wneuper@59562
|
190 |
("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
|
wneuper@59562
|
191 |
| ("helpless", _) => ("helpless: cannot propose tac", [])
|
wneuper@59562
|
192 |
| ("no-fmz-spec", _) => error "no-fmz-spec"
|
wneuper@59562
|
193 |
| ("end-of-calculation", (ts, _, _)) => ("", ts)
|
wneuper@59562
|
194 |
| _ => error "me: uncovered case")
|
wneuper@59562
|
195 |
handle ERROR msg => raise ERROR msg
|
wneuper@59562
|
196 |
val tac =
|
wneuper@59562
|
197 |
case ts of
|
wneuper@59562
|
198 |
tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
|
walther@59694
|
199 |
| _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
|
wneuper@59562
|
200 |
|
walther@59675
|
201 |
(p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Telem.Sundef, pt);
|
walther@59670
|
202 |
"~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt)
|
walther@59675
|
203 |
= (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Telem.Sundef, pt);
|
walther@59670
|
204 |
|
walther@59670
|
205 |
(*//--------------------- check results from modified me ----------------------------------\\*)
|
walther@59686
|
206 |
if p = ([2], Res) andalso
|
walther@59686
|
207 |
pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 = 2\n"
|
walther@59670
|
208 |
then
|
walther@59670
|
209 |
(case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => ()
|
walther@59670
|
210 |
| _ => error "")
|
walther@59670
|
211 |
else error "check results from modified me CHANGED";
|
walther@59670
|
212 |
(*\\--------------------- check results from modified me ----------------------------------//*)
|
walther@59670
|
213 |
|
walther@59670
|
214 |
"~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**);
|
walther@59670
|
215 |
(*\\------------------ end of modified "fun me" ---------------------------------------------//*)
|
walther@59686
|
216 |
|
walther@59686
|
217 |
(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_''' p'''''_''' [] pt'''''_'''; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
|
walther@59670
|
218 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
|
walther@59670
|
219 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + x = 0)"*)
|
walther@59670
|
220 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
|
walther@59670
|
221 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
|
walther@59670
|
222 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
|
walther@59670
|
223 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
|
walther@59670
|
224 |
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
|
walther@59670
|
225 |
(*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
|
walther@59670
|
226 |
(*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
|
walther@59670
|
227 |
(*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
|
walther@59670
|
228 |
(*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
|
wneuper@59562
|
229 |
(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
|
wneuper@59562
|
230 |
(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
|
wneuper@59562
|
231 |
(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
|
wneuper@59562
|
232 |
|
walther@59670
|
233 |
(*/--------------------- final test ----------------------------------\\*)
|
walther@59749
|
234 |
if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
|
walther@59670
|
235 |
". ----- pblobj -----\n" ^
|
walther@59670
|
236 |
"1. x + 1 = 2\n" ^
|
walther@59670
|
237 |
"2. x + 1 + -1 * 2 = 0\n" ^
|
walther@59670
|
238 |
"3. ----- pblobj -----\n" ^
|
walther@59670
|
239 |
"3.1. -1 + x = 0\n" ^
|
walther@59670
|
240 |
"3.2. x = 0 + -1 * -1\n" ^
|
walther@59670
|
241 |
"4. [x = 1]\n"
|
walther@59749
|
242 |
then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_tactic changed 1"
|
walther@59749
|
243 |
else error "re-build: fun locate_input_tactic changed 2";
|
wneuper@59562
|
244 |
|
walther@59670
|
245 |
|
walther@59670
|
246 |
"----------- fun locate_input_tactic Helpless, but applicable ----------------------------------";
|
walther@59670
|
247 |
"----------- fun locate_input_tactic Helpless, but applicable ----------------------------------";
|
walther@59670
|
248 |
"----------- fun locate_input_tactic Helpless, but applicable ----------------------------------";
|
walther@59670
|
249 |
(*cp from -- try fun applyTactics ------- *)
|
walther@59670
|
250 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
|
walther@59670
|
251 |
"normalform N"],
|
walther@59670
|
252 |
("PolyMinus",["plus_minus","polynom","vereinfachen"],
|
walther@59670
|
253 |
["simplification","for_polynomials","with_minus"]))];
|
walther@59670
|
254 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59670
|
255 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59670
|
256 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59670
|
257 |
(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*)
|
walther@59670
|
258 |
(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
|
walther@59670
|
259 |
|
walther@59686
|
260 |
(*+*)if map tac2str (sel_appl_atomic_tacs pt p) =
|
walther@59670
|
261 |
["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
|
walther@59686
|
262 |
"Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")"]
|
walther@59686
|
263 |
then () else error "sel_appl_atomic_tacs ([1], Res) CHANGED";
|
walther@59670
|
264 |
(*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);
|
walther@59670
|
265 |
|
walther@59686
|
266 |
(*+*)if map tac2str (sel_appl_atomic_tacs pt p) =
|
walther@59670
|
267 |
["Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")", "Rewrite (\"tausche_plus_minus\", \"?b kleiner ?c \<Longrightarrow> ?a + ?c - ?b = ?a - ?b + ?c\")",
|
walther@59670
|
268 |
"Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
|
walther@59686
|
269 |
"Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", "Calculate MINUS"]
|
walther@59686
|
270 |
then () else error "sel_appl_atomic_tacs ([1], Res) CHANGED";
|
walther@59670
|
271 |
(* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);
|
walther@59670
|
272 |
|
walther@59670
|
273 |
(*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
|
walther@59670
|
274 |
(** )val ("ok", (_, _, ptp as (pt, p))) =( **) locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);
|
walther@59670
|
275 |
"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (hd (sel_appl_atomic_tacs pt p), (pt, p));
|
walther@59670
|
276 |
val (mI, m) = Solve.mk_tac'_ tac;
|
walther@59737
|
277 |
val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
|
walther@59670
|
278 |
(*if*) member op = Solve.specsteps mI (*else*);
|
walther@59670
|
279 |
|
walther@59749
|
280 |
loc_solve_ m ptp;
|
walther@59749
|
281 |
"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = (m, ptp);
|
walther@59751
|
282 |
Step_Solve.by_tactic m (pt, pos);
|
walther@59670
|
283 |
(* ======== general case ======== *)
|
walther@59751
|
284 |
"~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, pos));
|
walther@59670
|
285 |
(*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
|
walther@59670
|
286 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
walther@59670
|
287 |
val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
|
walther@59670
|
288 |
|
walther@59686
|
289 |
(*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
|
walther@59692
|
290 |
"~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac)
|
walther@59670
|
291 |
= (sc, (pt, po), (fst is), (snd is), m);
|
walther@59670
|
292 |
val srls = Lucin.get_simplifier cstate (*TODO: shift into Istate.T*);
|
walther@59670
|
293 |
|
walther@59692
|
294 |
(*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
|
walther@59692
|
295 |
"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
|
walther@59692
|
296 |
= ((prog, (cstate, ctxt, tac)), istate);
|
walther@59686
|
297 |
(*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
|
walther@59670
|
298 |
|
walther@59692
|
299 |
go_scan_up1 (prog, cctt) ist;
|
walther@59692
|
300 |
"~~~~~ and go_scan_up1 , args:"; val ((yyy as (prog, _)), (ist as {path, ...}))
|
walther@59692
|
301 |
= ((prog, cctt), ist);
|
walther@59686
|
302 |
(*if*) 1 < length path (*then*);
|
walther@59670
|
303 |
|
walther@59692
|
304 |
scan_up1 yyy (ist |> path_up) (go (path_up' path) prog);
|
walther@59691
|
305 |
"~~~~~ fun scan_up1 , args:"; val (yyy, ist, (Const ("Tactical.Try"(*2*), _) $ _))
|
walther@59692
|
306 |
= (yyy, (ist |> path_up), (go (path_up' path) prog));
|
walther@59670
|
307 |
|
walther@59691
|
308 |
go_scan_up1 yyy ist;
|
walther@59692
|
309 |
"~~~~~ and go_scan_up1 , args:"; val ((yyy as (prog, _)), (ist as {path, ...}))
|
walther@59686
|
310 |
= (yyy, ist);
|
walther@59686
|
311 |
(*if*) 1 < length path (*then*);
|
walther@59670
|
312 |
|
walther@59692
|
313 |
scan_up1 yyy (ist |> path_up) (go (path_up' path) prog);
|
walther@59692
|
314 |
"~~~~~ fun scan_up1 , args:"; val ((yyy as (prog, xxx as (cstate, _, _))), ist,
|
walther@59688
|
315 |
(Const ("Tactical.Chain"(*3*), _) $ _ ))
|
walther@59692
|
316 |
= (yyy, (ist |> path_up), (go (path_up' path) prog));
|
walther@59692
|
317 |
val e2 = check_Seq_up ist prog
|
walther@59686
|
318 |
;
|
walther@59718
|
319 |
(*case*) scan_dn1 xxx (ist |> path_up_down [R] |> set_or ORundef) e (*of*);
|
walther@59691
|
320 |
"~~~~~ fun scan_dn1 , args:"; val (yyy, ist, (Const ("Tactical.Chain"(*2*), _) $ _ $ _))
|
walther@59718
|
321 |
= (xxx, (ist |> path_up_down [R] |> set_or ORundef), e2);
|
walther@59670
|
322 |
|
walther@59691
|
323 |
(*case*) scan_dn1 xxx (ist |> path_down [L, R]) e1 (*of*);
|
walther@59691
|
324 |
"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("Tactical.Try"(*2*), _) $ e))
|
walther@59686
|
325 |
= (xxx, (ist |> path_down [L, R]), e1);
|
walther@59670
|
326 |
|
walther@59691
|
327 |
(*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*);
|
walther@59686
|
328 |
(*======= end of scanning tacticals, a leaf =======*)
|
walther@59709
|
329 |
"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, act_arg, or, ...}), t)
|
walther@59686
|
330 |
= (xxx, (ist |> path_down [R]), e);
|
walther@59722
|
331 |
val (Program.Tac stac, a') = (*case*) interpret_leaf "locate" ctxt eval (get_subst ist) t (*of*);
|
walther@59686
|
332 |
val NotAss = (*case*) associate pt ctxt (tac, stac) (*of*);
|
walther@59718
|
333 |
val ORundef = (*case*) or (*of*);
|
walther@59686
|
334 |
val Notappl "norm_equation not applicable" =
|
walther@59686
|
335 |
(*case*) Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) (*of*);
|
walther@59670
|
336 |
|
walther@59712
|
337 |
(Term_Val1 act_arg) (* return value *);
|
walther@59670
|
338 |
|
walther@59670
|
339 |
val Rewrite' ("PolyMinus", "tless_true", _, _, ("tausche_minus",_ (*"?b ist_monom \<Longrightarrow> ?a kleiner ?b \<Longrightarrow> ?b - ?a = - ?a + ?b"*)),
|
walther@59670
|
340 |
t, (res, asm)) = m;
|
walther@59686
|
341 |
|
walther@59686
|
342 |
if scrstate2str ist =
|
walther@59686
|
343 |
"([\"\n(t_t, 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12)\"], [R,L,R,R,L,R,R], e_rls, SOMEt_t, \n" ^
|
walther@59718
|
344 |
"- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, ORundef, AppUndef_, false)"
|
walther@59670
|
345 |
andalso
|
walther@59670
|
346 |
term2str t = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g"
|
walther@59670
|
347 |
andalso
|
walther@59670
|
348 |
term2str res = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f) + 10 * g"
|
walther@59670
|
349 |
andalso
|
walther@59670
|
350 |
terms2str asm = "[\"4 kleiner 6\",\"6 ist_monom\"]"
|
walther@59670
|
351 |
then () else error "locate_input_tactic Helpless, but applicable CHANGED";
|
wneuper@59562
|
352 |
|
walther@59680
|
353 |
|
walther@59743
|
354 |
"----------- re-build: fun find_next_tactic -----------------------------------------------";
|
walther@59743
|
355 |
"----------- re-build: fun find_next_tactic -----------------------------------------------";
|
walther@59743
|
356 |
"----------- re-build: fun find_next_tactic -----------------------------------------------";
|
walther@59734
|
357 |
(*//--------- exception Size raised (line 171 of "./basis/LibrarySupport.sml") ---------------\\
|
walther@59734
|
358 |
THIS CODE WORKS IN Test.Some.thy
|
walther@59734
|
359 |
------------------------------------
|
walther@59734
|
360 |
val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
|
walther@59734
|
361 |
val (dI',pI',mI') =
|
walther@59734
|
362 |
("Test", ["sqroot-test","univariate","equation","test"],
|
walther@59734
|
363 |
["Test","squ-equ-test-subpbl1"]);
|
walther@59734
|
364 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59734
|
365 |
(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Pos.e_pos'), []);(*Model_Problem*)
|
walther@59734
|
366 |
(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Pos.e_pos'), []);(*Specify_Theory*)
|
walther@59734
|
367 |
(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Pos.e_pos'), []);(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)
|
walther@59734
|
368 |
(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
|
walther@59734
|
369 |
(*1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
|
walther@59734
|
370 |
(*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*)
|
walther@59734
|
371 |
|
walther@59734
|
372 |
(*// relevant call --------------------------------------------------------------------------\\*)
|
walther@59734
|
373 |
(*[2], Res*)val (aaa, ([(tac'''', bbb, ccc)], ddd, (pt'''', p''''))) =(**) step p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)
|
walther@59734
|
374 |
(*-- relevant call ----------------------------------------------------------------------------*)
|
walther@59734
|
375 |
|
walther@59734
|
376 |
"~~~~~ fun step , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []));
|
walther@59734
|
377 |
val pIopt = get_pblID (pt,ip);
|
walther@59734
|
378 |
(*if*) ip = ([], Pos.Res) (*else*);
|
walther@59734
|
379 |
val _ = (*case*) tacis (*of*);
|
walther@59734
|
380 |
val SOME _ = (*case*) pIopt (*of*);
|
walther@59734
|
381 |
(*if*) member op = [Pos.Pbl, Pos.Met] p_
|
walther@59734
|
382 |
andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) (*else*);
|
walther@59734
|
383 |
|
walther@59734
|
384 |
(** )val cs''''' = ( *..interpret "if member op ="..*)
|
walther@59734
|
385 |
(*case*) do_solve_step (pt, ip) (*of*);
|
walther@59734
|
386 |
"~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
|
walther@59734
|
387 |
(*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
|
walther@59734
|
388 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
walther@59734
|
389 |
val (_, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
|
walther@59734
|
390 |
|
walther@59734
|
391 |
(*NEW*) val Next_Step (_, _, Rewrite_Set' (_, _, Rls {id = "Test_simplify", ...}, _, _)) = (*case*)
|
walther@59743
|
392 |
(*NEW*) find_next_tactic sc (pt, pos) ist ctxt (*of*);
|
walther@59743
|
393 |
"~~~~~ fun find_next_tactic , args:"; val (Rule.Prog prog, ptp as (pt, (p, _)), Istate.Pstate ist, ctxt)
|
walther@59734
|
394 |
= (sc, (pt, pos), ist, ctxt);
|
walther@59734
|
395 |
(*OLD* ) val Accept_Tac2 (m', ist as {act_arg, ...}, ctxt) =
|
walther@59734
|
396 |
(*OLD*) (*case*) scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
|
walther@59734
|
397 |
( *OLD*)
|
walther@59734
|
398 |
(*NEW*) val Accept_Tac2 (tac, ist, ctxt) =
|
walther@59734
|
399 |
(*NEW*)(*case*) scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
|
walther@59734
|
400 |
(*NEW* )| Term_Val2 prog_result => End_Program (ist, Check_Postcond' ...prog_result...)
|
walther@59734
|
401 |
(*NEW*) (* ist indicates ^^\<Or>?, ctxt already updated, ^^^*)
|
walther@59734
|
402 |
(*NEW*)| Reject_Tac2 => Helpless
|
walther@59734
|
403 |
( *NEW*)
|
walther@59734
|
404 |
|
walther@59734
|
405 |
(*OLD* )(m', (Pstate ist, ctxt), (act_arg, Telem.Safe)) (*return value*);
|
walther@59734
|
406 |
( *OLD*)
|
walther@59734
|
407 |
(*NEW*) Next_Step (Istate.Pstate ist, Tactic.insert_assumptions tac ctxt, tac) (*return value*);
|
walther@59734
|
408 |
(*NEW*)
|
walther@59743
|
409 |
"~~~~~ from fun find_next_tactic\<longrightarrow>and do_solve_step , return:"; val (Next_Step (ist, ctxt, tac))
|
walther@59734
|
410 |
= (Next_Step (Istate.Pstate ist, Tactic.insert_assumptions tac ctxt, tac));
|
walther@59743
|
411 |
(*NEW* ) case find_next_tactic sc (pt, pos) ist ctxt of
|
walther@59734
|
412 |
(*NEW*) Next_Step (ist, ctxt, tac) =>
|
walther@59734
|
413 |
( *NEW*)
|
walther@59751
|
414 |
LucinNEW.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
|
walther@59751
|
415 |
(*NEW* ) | End_Program (ist, tac) => LucinNEW.by_tactic tac (ist, ctxt) ptp
|
walther@59734
|
416 |
(*NEW*) | Helpless => Chead.e_calcstate'
|
walther@59734
|
417 |
( *NEW*)
|
walther@59734
|
418 |
|
walther@59734
|
419 |
(*+*)val Rewrite_Set' ("Test", false, Rls {id = "Test_simplify", ...}, _, _) = tac;
|
walther@59734
|
420 |
|
walther@59734
|
421 |
"~~~~~ fun begin_end_prog , args:"; val (tac_, is, (pt, pos))
|
walther@59734
|
422 |
(*skip* )= (tac_'''''_', is, ptp);( *skip*)
|
walther@59734
|
423 |
(*use*) = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp) (*use*)
|
walther@59734
|
424 |
val pos = case pos of
|
walther@59734
|
425 |
(p, Met) => ((lev_on o lev_dn) p, Frm) (* begin script *)
|
walther@59734
|
426 |
| (p, Res) => (lev_on p, Res) (* somewhere in script *)
|
walther@59734
|
427 |
| _ => pos
|
walther@59734
|
428 |
val (pos', c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac_ is pos pt;
|
walther@59734
|
429 |
|
walther@59734
|
430 |
([(Tactic.input_from_T tac_, tac_, (pos, is))], c, (pt, pos')) (*return from do_solve_step*);
|
walther@59734
|
431 |
"~~~~~ from and do_solve_step\<longrightarrow>fun step , return:";
|
walther@59734
|
432 |
(*use*)val cs =
|
walther@59734
|
433 |
(*use*)([(Tactic.input_from_T tac_, tac_, (pos, is))], c, (pt, pos'));
|
walther@59734
|
434 |
(*use*)
|
walther@59734
|
435 |
"~~~~~ from fun step\<longrightarrow>TOPLEVEL return:";
|
walther@59734
|
436 |
(*OLD skip* )val (_, ([(tac'''', _, _)], _, (pt'''', p''''))) = ("ok", cs''''')( **);
|
walther@59734
|
437 |
(*OLD skip*)
|
walther@59734
|
438 |
(*use*)val ([(tac, _, (_, _))], _, (pt'''', p'''')) = cs
|
walther@59734
|
439 |
(*use*)
|
walther@59734
|
440 |
(*\\------------------ end of modified "fun step" -------------------------------------------//*)
|
walther@59734
|
441 |
|
walther@59734
|
442 |
(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p'''' ((pt'''', e_pos'), []);(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
|
walther@59734
|
443 |
(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Model_Problem*)
|
walther@59734
|
444 |
(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Theory "Test"*)
|
walther@59734
|
445 |
(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
|
walther@59734
|
446 |
(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Method ["Test", "solve_linear"]*)
|
walther@59734
|
447 |
(*[3, 1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Apply_Method ["Test", "solve_linear"]*)
|
walther@59734
|
448 |
(*[3, 1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
|
walther@59734
|
449 |
(*[3, 2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)
|
walther@59734
|
450 |
(*[3], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
|
walther@59734
|
451 |
(*[4], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Check_elementwise "Assumptions"*)
|
walther@59734
|
452 |
(*[], Res*)val ("ok", ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
|
walther@59734
|
453 |
(*[], Res*)val ("end-of-calculation", ([], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
|
walther@59734
|
454 |
|
walther@59734
|
455 |
(*/--------------------- final test ----------------------------------\\*)
|
walther@59734
|
456 |
val (res, asm) = (get_obj g_result pt (fst p));
|
walther@59734
|
457 |
|
walther@59734
|
458 |
if term2str res = "[x = 1]" andalso terms2str asm = "[\"precond_rootmet 1\"]"
|
walther@59743
|
459 |
then () else error "re-build: fun find_next_tactic CHANGED 1";
|
walther@59734
|
460 |
|
walther@59734
|
461 |
if p = ([], Und) (*.. should be ([], Res) *)
|
walther@59734
|
462 |
then
|
walther@59734
|
463 |
case get_obj g_tac pt (fst p) of
|
walther@59734
|
464 |
Apply_Method ["Test", "squ-equ-test-subpbl1"] => ((*ok, further tactics are level down*))
|
walther@59743
|
465 |
| _ => error "re-build: fun find_next_tactic CHANGED 3"
|
walther@59743
|
466 |
else error "re-build: fun find_next_tactic CHANGED 2";
|
walther@59734
|
467 |
\\--------- exception Size raised (line 171 of "./basis/LibrarySupport.sml") ---------------//*)
|
wneuper@59575
|
468 |
|
wneuper@59575
|
469 |
|
walther@59724
|
470 |
"----------- re-build: fun locate_input_formula ------------------------------------------------";
|
walther@59724
|
471 |
"----------- re-build: fun locate_input_formula ------------------------------------------------";
|
walther@59724
|
472 |
"----------- re-build: fun locate_input_formula ------------------------------------------------";
|