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@59670
|
12 |
"----------- re-build: fun determine_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;
|
wneuper@59561
|
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 |
|
wneuper@59561
|
37 |
"~~~~~ fun me, args:"; val (((_,tac):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@59677
|
42 |
"~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = ((mI,m), ptp);
|
walther@59686
|
43 |
|
walther@59686
|
44 |
"~~~~~ fun solve , args:"; val ((_, m as Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p,_)))) =
|
wneuper@59561
|
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@59696
|
56 |
(*+*)scrstate2str (the_pstate is) = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, Aundef, 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@59686
|
61 |
val (m', (is', ctxt'), _) =
|
walther@59686
|
62 |
LucinNEW.determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);
|
walther@59696
|
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, Aundef, 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@59712
|
74 |
val Ackn_Tac1 (_, _, Take' _) =
|
walther@59698
|
75 |
scan_dn1 cctt (ist |> set_path [R] |> set_or Aundef) (Program.body_of prog);
|
walther@59691
|
76 |
"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
|
walther@59698
|
77 |
= (cctt, (ist |> set_path [R] |> set_or Aundef), (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@59691
|
84 |
"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
|
walther@59686
|
85 |
= (xxx, (ist |> path_down [L, R]), e);
|
walther@59686
|
86 |
val (a', STac stac) = handle_leaf "locate" (Context.theory_name (Rule.Isac"")) 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@59670
|
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@59670
|
113 |
val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
|
walther@59670
|
114 |
(*if*) member op = Solve.specsteps mI; (*else*)
|
walther@59670
|
115 |
|
walther@59670
|
116 |
(** )val (***)xxxxx(***) ( *Updated (cs' as (_, _, (_, p'))) =( **) loc_solve_ (mI,m) ptp;
|
walther@59670
|
117 |
"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp);
|
walther@59670
|
118 |
|
walther@59670
|
119 |
(** )val (***)xxxxx_x(***) ( *(msg, cs') =( **) Solve.solve m (pt, pos);
|
walther@59670
|
120 |
"~~~~~ fun solve , 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@59712
|
131 |
(** )val Ackn_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@59698
|
138 |
scan_dn1 cctt (ist |> set_path [R] |> set_or Aundef) (Program.body_of prog);
|
walther@59691
|
139 |
"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
|
walther@59698
|
140 |
= (cctt, (ist |> set_path [R] |> set_or Aundef), (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@59686
|
154 |
val (a', Celem.STac stac) =
|
walther@59686
|
155 |
(*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) 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@59712
|
159 |
Ackn_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@59712
|
161 |
= (Ackn_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
|
walther@59670
|
162 |
|
walther@59712
|
163 |
"~~~~~ from scan_to_tactic1 to fun locate_input_tactic return val:"; val Ackn_Tac1 ((ist as {assoc, ...}), ctxt, tac')
|
walther@59712
|
164 |
= (Ackn_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@59686
|
168 |
"~~~~~ from locate_input_tactic to fun solve return:"; val Safe_Step (istate, ctxt, tac)
|
walther@59686
|
169 |
= (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate ist, ctxt, tac')(**);
|
walther@59670
|
170 |
|
walther@59670
|
171 |
(*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of solve *)
|
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@59670
|
180 |
"~~~~~ from solve 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@59670
|
234 |
if p = ([], Res) andalso f2str f = "[x = 1]" andalso fst nxt = "End_Proof'"
|
walther@59670
|
235 |
andalso pr_ctree pr_short pt =
|
walther@59670
|
236 |
". ----- pblobj -----\n" ^
|
walther@59670
|
237 |
"1. x + 1 = 2\n" ^
|
walther@59670
|
238 |
"2. x + 1 + -1 * 2 = 0\n" ^
|
walther@59670
|
239 |
"3. ----- pblobj -----\n" ^
|
walther@59670
|
240 |
"3.1. -1 + x = 0\n" ^
|
walther@59670
|
241 |
"3.2. x = 0 + -1 * -1\n" ^
|
walther@59670
|
242 |
"4. [x = 1]\n"
|
walther@59670
|
243 |
then () else error "re-build: fun locate_input_tactic changed";
|
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@59670
|
277 |
val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
|
walther@59670
|
278 |
(*if*) member op = Solve.specsteps mI (*else*);
|
walther@59670
|
279 |
|
walther@59670
|
280 |
loc_solve_ (mI, m) ptp;
|
walther@59670
|
281 |
"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI, m), ptp);
|
walther@59670
|
282 |
solve m (pt, pos);
|
walther@59670
|
283 |
(* ======== general case ======== *)
|
walther@59670
|
284 |
"~~~~~ fun solve , 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@59698
|
319 |
(*case*) scan_dn1 xxx (ist |> path_up_down [R] |> set_or Aundef) e (*of*);
|
walther@59691
|
320 |
"~~~~~ fun scan_dn1 , args:"; val (yyy, ist, (Const ("Tactical.Chain"(*2*), _) $ _ $ _))
|
walther@59698
|
321 |
= (xxx, (ist |> path_up_down [R] |> set_or Aundef), 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@59686
|
331 |
val (a', STac stac) = (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
|
walther@59686
|
332 |
val NotAss = (*case*) associate pt ctxt (tac, stac) (*of*);
|
walther@59686
|
333 |
val Aundef = (*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@59686
|
344 |
"- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, Aundef, 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 |
|
wneuper@59564
|
354 |
"----------- re-build: fun determine_next_tactic -----------------------------------------------";
|
wneuper@59564
|
355 |
"----------- re-build: fun determine_next_tactic -----------------------------------------------";
|
wneuper@59564
|
356 |
"----------- re-build: fun determine_next_tactic -----------------------------------------------";
|
wneuper@59575
|
357 |
|
wneuper@59575
|
358 |
|
wneuper@59575
|
359 |
"----------- re-build: fun locate_input_tactic -------------------------------------------------";
|
wneuper@59575
|
360 |
"----------- re-build: fun locate_input_tactic -------------------------------------------------";
|
wneuper@59575
|
361 |
"----------- re-build: fun locate_input_tactic -------------------------------------------------";
|