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