akargl@42176
|
1 |
(* Title: tests on solve.sml
|
akargl@42176
|
2 |
Author: Walther Neuper 060508,
|
neuper@37906
|
3 |
(c) due to copyright terms
|
neuper@37906
|
4 |
|
neuper@37906
|
5 |
is NOT ONLY dependent on Test, but on other thys:
|
neuper@37906
|
6 |
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
neuper@37906
|
7 |
uses from Rational.ML: Rrls cancel_p, Rrls cancel
|
neuper@37906
|
8 |
which in turn
|
neuper@37906
|
9 |
uses from Poly.ML: Rls make_polynomial, Rls expand_binom
|
neuper@37906
|
10 |
|
neuper@37906
|
11 |
*)
|
neuper@37906
|
12 |
|
neuper@37906
|
13 |
"-----------------------------------------------------------------";
|
neuper@37906
|
14 |
"table of contents -----------------------------------------------";
|
neuper@37906
|
15 |
"-----------------------------------------------------------------";
|
neuper@37906
|
16 |
"--------- interSteps on norm_Rational ---------------------------";
|
neuper@37906
|
17 |
(*---vvv NOT working after meNEW.04mmdd*)
|
neuper@37906
|
18 |
"###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
|
neuper@37906
|
19 |
"--------- prepare pbl, met --------------------------------------";
|
neuper@37906
|
20 |
"-------- cancel, without detail ------------------------------";
|
neuper@37906
|
21 |
"-------- cancel, detail rev-rew (cancel) afterwards ----------";
|
neuper@37906
|
22 |
"-------------- cancel_p, without detail ------------------------------";
|
neuper@37906
|
23 |
"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
|
neuper@37906
|
24 |
(*---^^^ NOT working*)
|
neuper@37906
|
25 |
"on 'miniscript with mini-subpbl':";
|
neuper@37906
|
26 |
"------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
|
neuper@37906
|
27 |
"------ interSteps'detailrls' after CompleteCalc -----------------";
|
neuper@37906
|
28 |
"------ interSteps after appendFormula ---------------------------";
|
neuper@37906
|
29 |
(*---vvv not brought to work 0403*)
|
neuper@37906
|
30 |
"------ Detail_Set -----------------------------------------------";
|
neuper@37906
|
31 |
"###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";
|
neuper@37906
|
32 |
"-----------------------------------------------------------------";
|
neuper@37906
|
33 |
"-----------------------------------------------------------------";
|
neuper@37906
|
34 |
"-----------------------------------------------------------------";
|
neuper@37906
|
35 |
|
neuper@37906
|
36 |
|
neuper@37906
|
37 |
"--------- interSteps on norm_Rational ---------------------------";
|
neuper@37906
|
38 |
"--------- interSteps on norm_Rational ---------------------------";
|
neuper@37906
|
39 |
"--------- interSteps on norm_Rational ---------------------------";
|
akargl@42176
|
40 |
states:=[];(*exp_IsacCore_Simp_Rat_Double_No-7.xml*)
|
akargl@42176
|
41 |
CalcTree [(["Term ((2/(x+3) + 2/(x - 3)) / (8*x/(x^2 - 9)))","normalform N"],
|
akargl@42176
|
42 |
("Rational",
|
akargl@42176
|
43 |
["rational","simplification"],
|
akargl@42176
|
44 |
["simplification","of_rationals"]))];
|
akargl@42176
|
45 |
moveActiveRoot 1;
|
akargl@42176
|
46 |
autoCalculate 1 CompleteCalc;
|
akargl@42176
|
47 |
val ((pt,_),_) = get_calc 1; show_pt pt;
|
neuper@37906
|
48 |
|
neuper@37906
|
49 |
(*with "Script SimplifyScript (t_::real) = -----------------
|
neuper@37906
|
50 |
\ ((Rewrite_Set norm_Rational False) t_)"
|
neuper@37906
|
51 |
case pt of Nd (PblObj _, [Nd _]) => ((*met only applies norm_Rational*))
|
neuper@38031
|
52 |
| _ => error "solve.sml: interSteps on norm_Rational 1";
|
neuper@37906
|
53 |
interSteps 1 ([1], Res);
|
neuper@37906
|
54 |
getFormulaeFromTo 1 ([1], Frm) ([1,12], Res) 99999 false;
|
neuper@37906
|
55 |
interSteps 1 ([1,3], Res);
|
neuper@37906
|
56 |
|
neuper@37906
|
57 |
getTactic 1 ([1,4], Res) (*here get the tactic, and ...*);
|
neuper@37906
|
58 |
interSteps 1 ([1,5], Res) (*... here get the intermediate steps above*);
|
neuper@37906
|
59 |
|
neuper@37906
|
60 |
getTactic 1 ([1,5,1], Frm);
|
neuper@37906
|
61 |
val ((pt,_),_) = get_calc 1; show_pt pt;
|
neuper@37906
|
62 |
|
neuper@37906
|
63 |
getTactic 1 ([1,8], Res) (*Rewrite_Set "common_nominator_p" *);
|
neuper@37906
|
64 |
interSteps 1 ([1,9], Res)(*TODO.WN060606 reverse rew*);
|
neuper@37906
|
65 |
--------------------------------------------------------------------*)
|
neuper@37906
|
66 |
|
neuper@37906
|
67 |
case pt of Nd (PblObj _, [Nd _, Nd _, Nd _, Nd _, Nd _, Nd _]) => ()
|
neuper@38031
|
68 |
| _ => error "solve.sml: interSteps on norm_Rational 1";
|
neuper@37906
|
69 |
(*these have been done now by the script ^^^ immediately...
|
neuper@37906
|
70 |
interSteps 1 ([1], Res);
|
neuper@37906
|
71 |
getFormulaeFromTo 1 ([1], Frm) ([1,12], Res) 99999 false;
|
neuper@37906
|
72 |
*)
|
neuper@37906
|
73 |
interSteps 1 ([6], Res);
|
neuper@37906
|
74 |
|
neuper@37906
|
75 |
getTactic 1 ([6,1], Frm) (*here get the tactic, and ...*);
|
neuper@37906
|
76 |
interSteps 1 ([6,1], Res) (*... here get the intermediate steps above*);
|
neuper@37906
|
77 |
|
neuper@37906
|
78 |
getTactic 1 ([3,4,1], Frm);
|
neuper@37906
|
79 |
val ((pt,_),_) = get_calc 1; show_pt pt;
|
neuper@37926
|
80 |
val (Form form, SOME tac, asm) = pt_extract (pt, ([6], Res));
|
neuper@37906
|
81 |
case (term2str form, tac, terms2strs asm) of
|
neuper@37906
|
82 |
("1 / 2", Check_Postcond ["rational", "simplification"],
|
neuper@37906
|
83 |
["-36 * x + 4 * x ^^^ 3 ~= 0"]) => ()
|
neuper@38031
|
84 |
| _ => error "solve.sml: interSteps on norm_Rational 2";
|
neuper@37906
|
85 |
|
neuper@37906
|
86 |
|
neuper@37906
|
87 |
|
neuper@37906
|
88 |
"###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
|
neuper@37906
|
89 |
"###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
|
neuper@37906
|
90 |
"###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
|
neuper@37906
|
91 |
val intermediate_ptyps = !ptyps;
|
neuper@37906
|
92 |
val intermediate_mets = !mets;
|
neuper@37906
|
93 |
|
neuper@37906
|
94 |
"--------- prepare pbl, met --------------------------------------";
|
neuper@37906
|
95 |
"--------- prepare pbl, met --------------------------------------";
|
neuper@37906
|
96 |
"--------- prepare pbl, met --------------------------------------";
|
neuper@37906
|
97 |
store_pbt
|
akargl@42176
|
98 |
(prep_pbt @{theory Test} "pbl_ttestt" [] e_pblID
|
neuper@37906
|
99 |
(["test"],
|
neuper@37906
|
100 |
[],
|
neuper@37926
|
101 |
e_rls, NONE, []));
|
neuper@37906
|
102 |
store_pbt
|
akargl@42176
|
103 |
(prep_pbt @{theory Test} "pbl_ttestt_detail" [] e_pblID
|
neuper@37906
|
104 |
(["detail","test"],
|
akargl@42176
|
105 |
[("#Given" ,["realTestGiven t_t"]),
|
akargl@42176
|
106 |
("#Find" ,["realTestFind s_s"])
|
neuper@37906
|
107 |
],
|
neuper@37926
|
108 |
e_rls, NONE, [["Test","test_detail"]]));
|
neuper@37906
|
109 |
|
neuper@37906
|
110 |
store_met
|
akargl@42176
|
111 |
(prep_met @{theory Test} "met_detbin" [] e_metID
|
neuper@37906
|
112 |
(["Test","test_detail_binom"]:metID,
|
akargl@42176
|
113 |
[("#Given" ,["realTestGiven t_t"]),
|
akargl@42176
|
114 |
("#Find" ,["realTestFind s_s"])
|
neuper@37906
|
115 |
],
|
akargl@42176
|
116 |
{rew_ord' = "sqrt_right", rls' = tval_rls, calc = [], srls = e_rls, prls = e_rls,
|
akargl@42176
|
117 |
crls = tval_rls, nrls = e_rls(*,
|
neuper@37906
|
118 |
asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]*)},
|
akargl@42176
|
119 |
"Script Testterm (g_g::real) = \
|
neuper@37906
|
120 |
\(((Rewrite_Set expand_binoms False) @@\
|
akargl@42176
|
121 |
\ (Rewrite_Set cancel False)) g_g)"
|
neuper@37906
|
122 |
));
|
neuper@37906
|
123 |
store_met
|
akargl@42176
|
124 |
(prep_met @{theory Test} "met_detpoly" [] e_metID
|
neuper@37906
|
125 |
(["Test","test_detail_poly"]:metID,
|
akargl@42176
|
126 |
[("#Given" ,["realTestGiven t_t"]),
|
akargl@42176
|
127 |
("#Find" ,["realTestFind s_s"])
|
neuper@37906
|
128 |
],
|
akargl@42176
|
129 |
{rew_ord' = "sqrt_right", rls' = tval_rls, calc = [], srls = e_rls, prls = e_rls,
|
akargl@42176
|
130 |
crls = tval_rls, nrls = e_rls(*,
|
neuper@37906
|
131 |
asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]*)},
|
akargl@42176
|
132 |
"Script Testterm (g_g::real) = \
|
neuper@37906
|
133 |
\(((Rewrite_Set make_polynomial False) @@\
|
akargl@42176
|
134 |
\ (Rewrite_Set cancel_p False)) g_g)"
|
neuper@37906
|
135 |
));
|
neuper@37906
|
136 |
|
neuper@37906
|
137 |
(*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*)
|
neuper@37906
|
138 |
|
neuper@37906
|
139 |
"-------- cancel, without detail ------------------------------";
|
neuper@37906
|
140 |
"-------- cancel, without detail ------------------------------";
|
neuper@37906
|
141 |
"-------- cancel, without detail ------------------------------";
|
neuper@37906
|
142 |
val fmz = ["realTestGiven (((3 + x) * (3 - x)) / ((3 + x) * (3 + x)))",
|
neuper@37906
|
143 |
"realTestFind s"];
|
neuper@37906
|
144 |
val (dI',pI',mI') =
|
neuper@38058
|
145 |
("Test",["detail","test"],["Test","test_detail_binom"]);
|
neuper@37906
|
146 |
|
neuper@37906
|
147 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
148 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
149 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
150 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
151 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
152 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
153 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@38058
|
154 |
(*nxt = ("Apply_Method",Apply_Method ("Test","test_detail"))*)
|
neuper@37906
|
155 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
156 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
157 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
158 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
159 |
(*"(3 + -1 * x) / (3 + x)"*)
|
neuper@37906
|
160 |
if nxt = ("End_Proof'",End_Proof') then ()
|
neuper@38031
|
161 |
else error "details.sml, changed behaviour in: without detail";
|
neuper@37906
|
162 |
|
neuper@37906
|
163 |
val str = pr_ptree pr_short pt;
|
neuper@37906
|
164 |
writeln str;
|
neuper@37906
|
165 |
|
neuper@37906
|
166 |
|
neuper@37906
|
167 |
"-------- cancel, detail rev-rew (cancel) afterwards ----------";
|
neuper@37906
|
168 |
"-------- cancel, detail rev-rew (cancel) afterwards ----------";
|
neuper@37906
|
169 |
"-------- cancel, detail rev-rew (cancel) afterwards ----------";
|
neuper@37906
|
170 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
171 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
172 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
173 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
174 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
175 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
176 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@38058
|
177 |
(*nxt = ("Apply_Method",Apply_Method ("Test","test_detail"))*)
|
neuper@37906
|
178 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
179 |
(*val nxt = ("Rewrite_Set",Rewrite_Set "expand_binoms")*)
|
neuper@37906
|
180 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
|
neuper@37906
|
181 |
(* val nxt = ("Detail",Detail);"----------------------";*)
|
neuper@37906
|
182 |
|
neuper@37906
|
183 |
|
neuper@37906
|
184 |
(*WN.11.9.03: after meNEW not yet implemented -------------------------*)
|
neuper@37906
|
185 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
186 |
(*FIXXXXXME.040216 #####################################################
|
neuper@37906
|
187 |
# val nxt = ("Detail", Detail) : string * tac
|
neuper@37906
|
188 |
val it = "----------------------" : string
|
neuper@37906
|
189 |
> val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
190 |
val f = Form' (FormKF (~1, EdUndef, ...)) : mout
|
neuper@37906
|
191 |
val nxt = ("Empty_Tac", Empty_Tac) : string * tac
|
neuper@37906
|
192 |
val p = ([2, 1], Res) : pos'
|
neuper@37906
|
193 |
#########################################################################
|
neuper@37906
|
194 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
195 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
196 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
197 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
198 |
(*val nxt = ("End_Detail",End_Detail)*)
|
neuper@37906
|
199 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
200 |
(*val nxt = ("Rewrite_Set",Rewrite_Set "cancel")*)
|
neuper@37906
|
201 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
|
neuper@37906
|
202 |
val nxt = ("Detail",Detail);"----------------------";
|
neuper@38043
|
203 |
val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e;
|
neuper@37906
|
204 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
akargl@42176
|
205 |
|
neuper@37906
|
206 |
(*15.10.02*)
|
neuper@37906
|
207 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
208 |
(*
|
neuper@38058
|
209 |
rewrite "Rationals" "tless_true""e_rls"true("sym_real_plus_minus_binom","")
|
neuper@37906
|
210 |
"3 ^^^ 2 - x ^^^ 2";
|
neuper@37906
|
211 |
*)
|
neuper@37906
|
212 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
213 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
214 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@38043
|
215 |
val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e;
|
neuper@37906
|
216 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
217 |
if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 - x) / (3 + x)"))
|
neuper@37906
|
218 |
andalso nxt = ("End_Proof'",End_Proof') then ()
|
neuper@38031
|
219 |
else error "new behaviour in details.sml, \
|
neuper@37906
|
220 |
\cancel, rev-rew (cancel) afterwards";
|
neuper@37906
|
221 |
FIXXXXXME.040216 #####################################################*)
|
neuper@37906
|
222 |
|
neuper@37906
|
223 |
(*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*)
|
neuper@37906
|
224 |
|
neuper@37906
|
225 |
"-------------- cancel_p, without detail ------------------------------";
|
neuper@37906
|
226 |
"-------------- cancel_p, without detail ------------------------------";
|
neuper@37906
|
227 |
"-------------- cancel_p, without detail ------------------------------";
|
neuper@37906
|
228 |
val fmz = ["realTestGiven (((3 + x)*(3+(-1)*x)) / ((3+x) * (3+x)))",
|
neuper@37906
|
229 |
"realTestFind s"];
|
neuper@37906
|
230 |
val (dI',pI',mI') =
|
neuper@38058
|
231 |
("Test",["detail","test"],["Test","test_detail_poly"]);
|
neuper@37906
|
232 |
|
neuper@37906
|
233 |
(*val p = e_pos'; val c = [];
|
neuper@37906
|
234 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
235 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
236 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
237 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
238 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
239 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
240 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
241 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
242 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@38058
|
243 |
(*nxt = ("Apply_Method",Apply_Method ("Test","test_detail"))*)
|
neuper@37906
|
244 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
245 |
"(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))";
|
neuper@37906
|
246 |
|
neuper@37906
|
247 |
(*14.3.03*)
|
neuper@37906
|
248 |
(*---------------WN060614?!?---
|
neuper@37906
|
249 |
val t = str2term "(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))";
|
neuper@37926
|
250 |
val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
251 |
"(9 + - (x ^^^ 2)) / (9 + 6 * x + x ^^^ 2)";
|
neuper@37926
|
252 |
val SOME (t,_) = rewrite_set_ thy false cancel_p t; term2str t;
|
neuper@37906
|
253 |
cancel_p_ thy t;
|
neuper@37906
|
254 |
(---------------WN060614?!?---*)
|
neuper@37906
|
255 |
|
neuper@37906
|
256 |
val t = str2term "(3 + x) * (3 + -1 * x)";
|
akargl@42209
|
257 |
(*============ inhibit exn AK110725 ==============================================
|
akargl@42209
|
258 |
(* ERROR: error is only visible in Test_Isac.sml -
|
akargl@42209
|
259 |
can't unify theory to domID * rls *)
|
neuper@37926
|
260 |
val SOME (t,_) = rewrite_set_ thy false expand_poly t; term2str t;
|
neuper@37906
|
261 |
"3 * 3 + 3 * (-1 * x) + (x * 3 + x * (-1 * x))";
|
neuper@37926
|
262 |
val SOME (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;
|
neuper@37906
|
263 |
"3 * 3 + (3 * x + (-1 * (3 * x) + -1 * (x * x)))";
|
neuper@37926
|
264 |
val SOME (t,_) = rewrite_set_ thy false simplify_power t; term2str t;
|
neuper@37906
|
265 |
"3 ^^^ 2 + (3 * x + (-1 * (3 * x) + -1 * x ^^^ 2))";
|
neuper@37926
|
266 |
val SOME (t,_) = rewrite_set_ thy false collect_numerals t; term2str t;
|
neuper@37906
|
267 |
"9 + (0 * x + -1 * x ^^^ 2)";
|
neuper@37926
|
268 |
val SOME (t,_) = rewrite_set_ thy false reduce_012 t; term2str t;
|
neuper@37906
|
269 |
"9 + - (x ^^^ 2)";
|
akargl@42209
|
270 |
============ inhibit exn AK110725 ==============================================*)
|
akargl@42209
|
271 |
|
neuper@37906
|
272 |
(*14.3.03*)
|
neuper@37906
|
273 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
274 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
275 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
276 |
(*"(3 + -1 * x) / (3 + x)"*)
|
neuper@37906
|
277 |
if nxt = ("End_Proof'",End_Proof') then ()
|
neuper@38031
|
278 |
else error "details.sml, changed behaviour in: cancel_p, without detail";
|
neuper@37906
|
279 |
|
neuper@37906
|
280 |
"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
|
neuper@37906
|
281 |
"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
|
neuper@37906
|
282 |
"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
|
neuper@37906
|
283 |
(* val p = e_pos'; val c = [];
|
neuper@37906
|
284 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
285 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
286 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
287 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
288 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
289 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
290 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
291 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
292 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@38058
|
293 |
(*nxt = ("Apply_Method",Apply_Method ("Test","test_detail_poly"))*)
|
neuper@37906
|
294 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
295 |
(*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*)
|
neuper@37906
|
296 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
|
neuper@37906
|
297 |
|
neuper@37906
|
298 |
(*14.3.03.FIXXXXXME since Isa02/reverse-rew.sml:
|
neuper@37906
|
299 |
fun make_deriv ... Rls_ not yet impl. (| Thm | Calc)
|
neuper@37906
|
300 |
Rls_ needed for make_polynomial ----------------------
|
neuper@37906
|
301 |
val nxt = ("Detail",Detail);"----------------------";
|
neuper@37906
|
302 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
303 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
304 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
305 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
306 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
307 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
308 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
309 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
310 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
311 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
312 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
313 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
314 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
315 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
316 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
317 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
318 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
319 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
320 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
321 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
322 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
323 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
324 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
325 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
326 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
327 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
328 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
329 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
330 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
331 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
332 |
if nxt = ("End_Detail",End_Detail) then ()
|
neuper@38031
|
333 |
else error "details.sml: new behav. in Detail make_polynomial";
|
neuper@37906
|
334 |
----------------------------------------------------------------------*)
|
neuper@37906
|
335 |
|
neuper@37906
|
336 |
(*---------------
|
neuper@37906
|
337 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
338 |
(*val nxt = ("Rewrite_Set",Rewrite_Set "cancel_p")*)
|
neuper@37906
|
339 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
|
neuper@37906
|
340 |
val nxt = ("Detail",Detail);"----------------------";
|
neuper@38043
|
341 |
val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e;
|
neuper@37906
|
342 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
343 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
344 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
345 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
346 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@38043
|
347 |
val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e;
|
neuper@37906
|
348 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
349 |
if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 + x) / (3 - x)"))
|
neuper@37906
|
350 |
andalso nxt = ("End_Proof'",End_Proof') then ()
|
neuper@38031
|
351 |
else error "new behaviour in details.sml, cancel_p afterwards";
|
neuper@37906
|
352 |
|
neuper@37906
|
353 |
----------------*)
|
neuper@37906
|
354 |
|
neuper@37906
|
355 |
|
neuper@37906
|
356 |
|
neuper@37906
|
357 |
|
neuper@37906
|
358 |
val fmz = ["realTestGiven ((x+3)+(-1)*(2+6*x))",
|
neuper@37906
|
359 |
"realTestFind s"];
|
neuper@37906
|
360 |
val (dI',pI',mI') =
|
neuper@38058
|
361 |
("Test",["detail","test"],["Test","test_detail_poly"]);
|
neuper@37906
|
362 |
|
neuper@37906
|
363 |
(* val p = e_pos'; val c = [];
|
neuper@37906
|
364 |
val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
365 |
val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
|
neuper@37906
|
366 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
367 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
368 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
369 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
370 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
371 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
372 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@38058
|
373 |
(*nxt = ("Apply_Method",Apply_Method ("Test","test_detail_poly"))*)
|
neuper@37906
|
374 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
375 |
(*16.10.02 --- kommt auf POLY_EXCEPTION ?!??? ----------------------------
|
neuper@37906
|
376 |
(*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*)
|
neuper@37906
|
377 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
|
neuper@37906
|
378 |
val nxt = ("Detail",Detail);"----------------------";
|
neuper@37906
|
379 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
380 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
381 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
382 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
383 |
-------------------------------------------------------------------------*)
|
neuper@37906
|
384 |
|
neuper@37906
|
385 |
|
neuper@37906
|
386 |
"------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
|
neuper@37906
|
387 |
"------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
|
neuper@37906
|
388 |
"------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
|
neuper@37906
|
389 |
states:=[];
|
neuper@41970
|
390 |
CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
|
neuper@41970
|
391 |
("Test", ["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
392 |
["Test","squ-equ-test-subpbl1"]))];
|
neuper@37906
|
393 |
Iterator 1;
|
neuper@37906
|
394 |
moveActiveRoot 1;
|
neuper@37906
|
395 |
autoCalculate 1 CompleteCalc;
|
neuper@37906
|
396 |
moveActiveRoot 1;
|
neuper@37906
|
397 |
|
neuper@37906
|
398 |
interSteps 1 ([],Res);
|
neuper@37906
|
399 |
val [(_,(((pt,_),_),[(_,ip)]))] = !states;
|
neuper@37906
|
400 |
val ("donesteps",_(*,ss*), lastpos) = detailstep pt ip;
|
neuper@37906
|
401 |
(*case ss of [(_,_,t1),(_,_,t2),(_,_,t3),(_,_,t4),(_,_,t5),(_,_,t6)] =>
|
neuper@37906
|
402 |
(writeln o terms2str) [t1,t2,t3,t4,t5,t6]
|
neuper@38031
|
403 |
| _ => error "details.sml: diff.behav. in detail miniscript";*) if lastpos = ([4], Res) then ()
|
neuper@38031
|
404 |
else error "details.sml: diff.behav. in interSteps'donesteps' 1";
|
neuper@37906
|
405 |
|
neuper@37906
|
406 |
moveActiveDown 1;
|
neuper@37906
|
407 |
moveActiveDown 1;
|
neuper@37906
|
408 |
moveActiveDown 1;
|
neuper@37906
|
409 |
moveActiveDown 1;
|
neuper@37906
|
410 |
|
neuper@37906
|
411 |
interSteps 1 ([3],Pbl) (*subproblem*);
|
neuper@37906
|
412 |
val [(_,(((pt,_),_),[(_,ip)]))] = !states;
|
neuper@37906
|
413 |
val ("donesteps",_(*,ss*), lastpos) = detailstep pt ip;
|
neuper@37906
|
414 |
(*case ss of [(_,_,t1),(_,_,t2),(_,_,t3)] =>
|
neuper@37906
|
415 |
(writeln o terms2str) [t1,t2,t3]
|
neuper@38031
|
416 |
| _ => error "details.sml: diff.behav. in detail miniscript";*) if lastpos = ([3, 2], Res) then ()
|
neuper@38031
|
417 |
else error "details.sml: diff.behav. in interSteps'donesteps' 1";
|
neuper@37906
|
418 |
|
neuper@37906
|
419 |
|
neuper@37906
|
420 |
(* val [(_,(((pt,_),_),[(_,ip)]))] = !states;
|
neuper@37906
|
421 |
writeln (pr_ptree pr_short pt);
|
neuper@37906
|
422 |
get_obj g_tac pt [4];
|
neuper@37906
|
423 |
*)
|
neuper@37906
|
424 |
|
neuper@37906
|
425 |
"------ interSteps'detailrls' after CompleteCalc -----------------";
|
neuper@37906
|
426 |
"------ interSteps'detailrls' after CompleteCalc -----------------";
|
neuper@37906
|
427 |
"------ interSteps'detailrls' after CompleteCalc -----------------";
|
neuper@37906
|
428 |
states:=[];
|
neuper@41970
|
429 |
CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
|
neuper@41970
|
430 |
("Test", ["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
431 |
["Test","squ-equ-test-subpbl1"]))];
|
neuper@37906
|
432 |
Iterator 1;
|
neuper@37906
|
433 |
moveActiveRoot 1;
|
neuper@37906
|
434 |
autoCalculate 1 CompleteCalc;
|
neuper@37906
|
435 |
interSteps 1 ([],Res);
|
neuper@37906
|
436 |
moveActiveRoot 1;
|
neuper@37906
|
437 |
moveActiveDown 1;
|
neuper@37906
|
438 |
moveActiveDown 1;
|
neuper@37906
|
439 |
moveActiveDown 1;
|
neuper@37906
|
440 |
refFormula 1 (get_pos 1 1); (* 2 Res, <ISA> -1 + x = 0 </ISA> *)
|
neuper@37906
|
441 |
|
neuper@37906
|
442 |
interSteps 1 ([2],Res);
|
neuper@37906
|
443 |
val [(_,(((pt,_),_),[(_,(p,_))]))] = !states;
|
neuper@37906
|
444 |
if length (children (get_nd pt p)) = 6 then ()
|
neuper@38031
|
445 |
else error "details.sml: diff.behav. in interSteps'detailrls' 1";
|
neuper@37906
|
446 |
|
neuper@37906
|
447 |
moveActiveDown 1;
|
neuper@37906
|
448 |
moveActiveDown 1; refFormula 1 (get_pos 1 1); (* 3,1 Frm, <ISA> -1 + x = 0 </ISA> *);
|
neuper@37906
|
449 |
|
neuper@37906
|
450 |
interSteps 1 ([3,1],Frm) (*<ERROR> first formula on level has NO detail </E*);
|
neuper@37906
|
451 |
val [(_,(((pt,_),_),[(_,(p,_))]))] = !states;
|
neuper@37906
|
452 |
if length (children (get_nd pt p)) = 0 then () (*NO detail at ([xxx,1],Frm)*)
|
neuper@38031
|
453 |
else error "details.sml: diff.behav. in interSteps'detailrls' 2";
|
neuper@37906
|
454 |
|
neuper@37906
|
455 |
moveActiveDown 1;
|
neuper@37906
|
456 |
refFormula 1 (get_pos 1 1); (* 3,1 Res, <ISA> x = 0 + -1 * -1 </ISA> *)
|
neuper@37906
|
457 |
|
neuper@37906
|
458 |
interSteps 1 ([3,1],Res);
|
neuper@37906
|
459 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
neuper@37906
|
460 |
term2str (get_obj g_res pt [3,1,1]);(*"x = 0 + -1 * -1" ok*)
|
neuper@37906
|
461 |
term2str (get_obj g_form pt [3,2]); (*"x = 0 + -1 * -1" ok*)
|
neuper@37906
|
462 |
get_obj g_tac pt [3,1,1]; (*Rewrite_Inst.."risolate_bdv_add ok*)
|
neuper@37906
|
463 |
|
neuper@37906
|
464 |
moveActiveDown 1;
|
neuper@37906
|
465 |
refFormula 1 (get_pos 1 1); (* 3,2 Res, <ISA> x = 1 </ISA> *)
|
neuper@37906
|
466 |
|
neuper@37906
|
467 |
interSteps 1 ([3,2],Res);
|
neuper@37906
|
468 |
val [(_,(((pt,_),_),[(_,(p,_))]))] = !states;
|
neuper@37906
|
469 |
if length (children (get_nd pt p)) = 2 then ()
|
neuper@38031
|
470 |
else error "details.sml: diff.behav. in interSteps'detailrls' 3";
|
neuper@37906
|
471 |
|
neuper@37906
|
472 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
neuper@37906
|
473 |
|
neuper@37906
|
474 |
|
neuper@37906
|
475 |
"------ interSteps after appendFormula ---------------------------";
|
neuper@37906
|
476 |
"------ interSteps after appendFormula ---------------------------";
|
neuper@37906
|
477 |
"------ interSteps after appendFormula ---------------------------";
|
neuper@37906
|
478 |
states:=[];
|
neuper@41970
|
479 |
CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
|
neuper@41970
|
480 |
("Test", ["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
481 |
["Test","squ-equ-test-subpbl1"]))];
|
neuper@37906
|
482 |
Iterator 1;
|
neuper@37906
|
483 |
moveActiveRoot 1;
|
neuper@37906
|
484 |
autoCalculate 1 CompleteCalcHead;
|
neuper@37906
|
485 |
autoCalculate 1 (Step 1);
|
neuper@37906
|
486 |
autoCalculate 1 (Step 1);
|
neuper@37906
|
487 |
appendFormula 1 "x - 1 = 0"(*generates intermediate steps*);
|
neuper@37906
|
488 |
(*these are not shown, because the resulting formula is on the same
|
neuper@37906
|
489 |
level as the previous formula*)
|
neuper@37906
|
490 |
interSteps 1 ([2],Res) (*error: last unchanged was ([2, 9], Res)*);
|
neuper@37906
|
491 |
(*...and these are the internals*)
|
neuper@37906
|
492 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
neuper@37906
|
493 |
val (_,_,lastpos) =detailstep pt p;
|
neuper@37906
|
494 |
if p = ([2], Res) andalso lastpos = ([2, 9], Res) then ()
|
neuper@38031
|
495 |
else error "solve.sml: diff.beh. after appendFormula x - 1 = 0";
|
neuper@37906
|
496 |
|
neuper@37906
|
497 |
|
neuper@37906
|
498 |
"------ Detail_Set -----------------------------------------------";
|
neuper@37906
|
499 |
"------ Detail_Set -----------------------------------------------";
|
neuper@37906
|
500 |
"------ Detail_Set -----------------------------------------------";
|
neuper@41970
|
501 |
states:=[]; (*start of calculation, return No.1*)
|
neuper@41970
|
502 |
CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
|
neuper@41970
|
503 |
("Test", ["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
504 |
["Test","squ-equ-test-subpbl1"]))];
|
neuper@37906
|
505 |
Iterator 1; moveActiveRoot 1;
|
neuper@37906
|
506 |
autoCalculate 1 CompleteCalcHead;
|
neuper@37906
|
507 |
autoCalculate 1 (Step 1);
|
neuper@37906
|
508 |
autoCalculate 1 (Step 1);
|
neuper@37906
|
509 |
|
neuper@37906
|
510 |
fetchProposedTactic 1 (*DG decides to do this tactic in detail*);
|
neuper@37906
|
511 |
(*TODO ...*)
|
neuper@37906
|
512 |
setNextTactic 1 (Detail_Set "Test_simplify");
|
neuper@37906
|
513 |
|
neuper@37906
|
514 |
|
neuper@37906
|
515 |
val ((pt,p),tacis) = get_calc 1;
|
neuper@37906
|
516 |
val str = pr_ptree pr_short pt;
|
neuper@37906
|
517 |
writeln str;
|
neuper@37906
|
518 |
|
neuper@37906
|
519 |
print_depth 3;
|
neuper@37906
|
520 |
term2str (fst (get_obj g_result pt [1]));
|
neuper@37906
|
521 |
|
neuper@37906
|
522 |
|
neuper@37906
|
523 |
|
neuper@37906
|
524 |
|
neuper@37906
|
525 |
"###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";
|
neuper@37906
|
526 |
"###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";
|
neuper@37906
|
527 |
"###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";
|
neuper@37906
|
528 |
ptyps:= intermediate_ptyps;
|
neuper@37906
|
529 |
mets:= intermediate_mets;
|