//reduce the number of TermC.parse*; "//"means: tests broken .
broken tests are outcommented with "reduce the number of TermC.parse*"
1 (* testexamples for RootratEq, equations mixing fractions and roots
2 WN120314 some complicated equations still are outcommented.
5 "-----------------------------------------------------------------";
6 "table of contents -----------------------------------------------";
7 "-----------------------------------------------------------------";
8 "------------ tests on predicates -------------------------------";
9 "------------ test thm rootrat_equation_left_1 -------------------";
10 "------------ test thm rootrat_equation_left_2 -------------------";
11 "------------ test thm rootrat_equation_right_1 ------------------";
12 "------------ test thm rootrat_equation_right_2 ------------------";
13 "-----------------------------------------------------------------";
14 "-----------------------------------------------------------------";
15 (* Note on ERROR "check_elementwise: no set 1 + sqrt x = 3".
16 this error popped up with this harmless changeset, which
17 (1) triggered ["RootEq", "solve_sq_root_equation"] first time, because wrong '' in
18 (Try (Repeat (Rewrite_Set ''make_rooteq ''))) was found
19 (2) correction ''make_rooteq'' led further to "check_elementwise: no set 1 + sqrt x = 3"
20 Since the changeset seems have nothing todo with these errors, this indicates that
21 (a) either method ["RootEq", "solve_sq_root_equation"] & Co are somewhat indeterministic
22 (b) of this is a case of indeterminism due to something elementary.
25 val thy = @{theory "RootRatEq"};
27 "------------ tests on predicates -------------------------------";
28 "------------ tests on predicates -------------------------------";
29 "------------ tests on predicates -------------------------------";
30 val t1 = TermC.parseNEW'' thy "(-8 - sqrt(x) + x \<up> 2) is_rootRatAddTerm_in x";
31 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
32 if (UnparseC.term t) = "False" then ()
33 else error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in";
35 val t1 = TermC.parseNEW'' thy "(1/x) is_rootRatAddTerm_in x";
36 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
37 if (UnparseC.term t) = "False" then ()
38 else error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in";
40 val t1 = TermC.parseNEW'' thy "(1/sqrt(x)) is_rootRatAddTerm_in x";
41 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
42 if (UnparseC.term t) = "False" then ()
43 else error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in";
45 val t1 = TermC.parseNEW'' thy "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
46 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
47 if (UnparseC.term t) = "True" then ()
48 else error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in";
50 val t1 = TermC.parseNEW'' thy "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
51 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
52 if (UnparseC.term t) = "True" then ()
53 else error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in";
55 val t1 = TermC.parseNEW'' thy "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
56 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
57 if (UnparseC.term t) = "True" then ()
58 else error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in";
60 val t1 = TermC.parseNEW'' thy "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x";
61 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
62 if (UnparseC.term t) = "True" then ()
63 else error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in";
65 "------------ test thm rootrat_equation_left_1 -------------------";
66 "------------ test thm rootrat_equation_left_1 -------------------";
67 "------------ test thm rootrat_equation_left_1 -------------------";
69 val fmz = ["equality ( - 2 + 1/(1 - sqrt(x))= (0::real))", "solveFor x", "solutions L"];
70 val (dI',pI',mI') = ("RootRatEq",["univariate", "equation"],["no_met"]);
71 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
72 val (p,_,f,nxt,_,pt) = me nxt p c pt;
73 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
74 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
75 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
76 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
77 val (p,_,f,nxt,_,pt) = me nxt p c pt;
78 (*============ inhibit exn WN120319 ==============================================
79 (*From final Test_Isac.thy we suddenly have
81 nxt = ("Model_Problem", Model_Problem)
83 which we did not investigate further due to the decision to drop the whole type of equation.
85 if f2str f = "1 = (0 - - 2) * (1 + - 1 * sqrt x)" then ()
86 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 a";
87 (*-> Subproblem ("RootRatEq", ["sq", "rootX", "univariate", "equation"])*)
88 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
89 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
90 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
91 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
92 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p''',_,f,nxt,_,pt''') = me nxt p c pt;
94 (*we investigate, why the next step results in Empty_Tac*)
95 f2str f = "1 = 2 * (1 + - 1 * sqrt x)";
96 nxt = ("Rewrite_Set", Rewrite_Set "make_rooteq");
97 (*... these ar the step's arguments; from these we do directly ...*)
98 val SOME t = parseNEW ctxt "1 = 2 * (1 + - 1 * sqrt x)"
99 val SOME (t, _) = rewrite_set_ thy true make_rooteq t;
100 UnparseC.term t = "1 = 2 + - 2 * sqrt x";
101 (*... which works; thus error must be in script interpretation*)
103 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
104 val (pt, p) = case Step.by_tactic tac (pt,p) of
105 ("ok", (_, _, ptp)) => ptp;
106 "~~~~~ fun Step.do_next, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
107 val pIopt = get_pblID (pt,ip);
108 ip; (*= ([3, 2], Res)*)
110 pIopt; (*= SOME ["sq", "rootX", "univariate", "equation"]*)
111 member op = [Pbl,Met] p_; (*= false*)
112 "~~~~~ fun do_next, args:"; (*stopped due to strange exn
113 "check_elementwise: no set 1 = 2 + - 2 * sqrt x"*)
115 (*---- 2nd try: we investigate the script ["RootEq", "solve_sq_root_equation"] found via pbl*)
116 val t = TermC.str2term "((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v)";
117 val t = TermC.str2term ("((lhs (1 = 2 * (1 + - 1 * sqrt x))) is_sqrtTerm_in x) |" ^
118 " ((rhs (1 = 2 * (1 + - 1 * sqrt x))) is_sqrtTerm_in x)");
119 val SOME (t, _) = rewrite_set_ thy true rooteq_srls t;
120 UnparseC.term t = "True | True"; (*...was same in 2002 (NOT "True"); so program seems to take
121 [univariate,equation] and to refine to ["sq", "rootX", "univariate", "equation"] in 2002*)
123 (*(*these are the errors during stepping into the code:*)
124 Step_Solve.do_next (pt,ip); (*check_elementwise: no set 1 = 2 + - 2 * sqrt x: fun mk_set raises
125 this exn in Check_elementwise ONLY ?!?*)
126 Step.do_next p ((pt, e_pos'),[]); (* = ("helpless",*)
129 val (p,_,f,nxt,_,pt) = me nxt p''' c pt''';
130 f2str f = "1 = 2 + - 2 * sqrt x)"; (* <<<-------------- this should be*)
131 fst nxt = "Empty_Tac"; (* <<<-------------- this we have*)
132 (*============ inhibit exn WN120314: stopped due to effort; continue with equ-solver
133 The equation is strange: it calls script ["RootEq", "solve_sq_root_equation"] twice
134 and works differently due to an "if" in that script.
136 if f2str f = "1 = 2 + - 2 * sqrt x" then ()
137 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 b";
138 (*-> Subproblem ("RootRatEq", ["sq", "rootX", "univariate", "equation"]) ?!? the SAME as above*)
139 val (p,_,f,nxt,_,pt) = me nxt p c pt;
140 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
141 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
142 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
143 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
144 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
145 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
146 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
147 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
148 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
149 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
150 if f2str f = "1 = 4 * x" then ()
151 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 c";
152 (*-> Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"])*)
153 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
154 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
155 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
156 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
157 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
158 val (p,_,f,nxt,_,pt) = me nxt p c pt;
159 if f2str f = "1 + -4 * x = 0" then ()
160 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1";
161 (*-> Subproblem ("PolyEq", ["degree_1", "polynomial", "univariate", "equation"])*)
162 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
163 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
164 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
165 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
166 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
167 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
168 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
169 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
170 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
171 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
172 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
173 | _ => error "rootrateq.sml: diff.behav. in - 2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
174 ============ inhibit exn WN120314 ==============================================*)
175 ============ inhibit exn WN120319 ==============================================*)
177 "------------ test thm rootrat_equation_left_2 -------------------";
178 "------------ test thm rootrat_equation_left_2 -------------------";
179 "------------ test thm rootrat_equation_left_2 -------------------";
180 val fmz = ["equality (3/(1+sqrt(x))= 1)", "solveFor x", "solutions L"];
181 val (dI',pI',mI') = ("RootRatEq",["univariate", "equation"],["no_met"]);
183 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
184 val (p,_,f,nxt,_,pt) = me nxt p c pt;
185 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
186 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
187 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
189 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
190 (*-> Subproblem ("RootEq", ["univariate", ...])*)
191 val (p,_,f,nxt,_,pt) = me nxt p c pt;
192 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
193 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
194 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
196 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
198 (*//------------------ ERROR check_elementwise: no set 1 + sqrt x = 3 -----------------------\\* )
199 val (p,_,f,nxt,_,pt) = me nxt p c pt;
200 (*-> Subproblem ("RootEq", ["univariate", ...])*)
201 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
202 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
203 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
205 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
206 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
207 val (p,_,f,nxt,_,pt) = me nxt p c pt;
208 (*-> Subproblem ("RootEq", ["univariate", ...])*)
209 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
210 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
212 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
213 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
214 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
215 val (p,_,f,nxt,_,pt) = me nxt p c pt;
216 ( *\\------------------ ERROR check_elementwise: no set 1 + sqrt x = 3 -----------------------//*)
218 (*============ inhibit exn WN120314 ==============================================
219 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "4 + - 1 * x = 0")) then ()
220 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_2";
221 (*-> Subproblem ("PolyEq", ["polynomial", ...])*)
222 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
223 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
224 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
225 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
226 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
227 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
228 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
229 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
230 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
231 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
232 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
233 | _ => error "rootrateq.sml: diff.behav. in 3/(1+sqrt(x))= 1 -> [x = 4]";
234 ============ inhibit exn WN120314 ==============================================*)
236 "------------ test thm rootrat_equation_right_1 ------------------";
237 "------------ test thm rootrat_equation_right_1 ------------------";
238 "------------ test thm rootrat_equation_right_1 ------------------";
239 val fmz = ["equality ( 0= - 2 + 1/(1 - sqrt(x)))", "solveFor x", "solutions L"];
240 val (dI',pI',mI') = ("RootRatEq",["univariate", "equation"],["no_met"]);
242 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
243 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
244 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
245 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
246 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
247 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
249 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
250 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
251 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
252 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
253 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
255 (*//------------------ ERROR check_elementwise: no set 1 + sqrt x = 3 -----------------------\\* )
256 val (p,_,f,nxt,_,pt) = me nxt p c pt;
257 val (p,_,f,nxt,_,pt) = me nxt p c pt;
258 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
259 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
260 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
261 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
263 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
264 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
265 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
266 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
267 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
269 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
270 val (p,_,f,nxt,_,pt) = me nxt p c pt;
271 ( *\\------------------ ERROR check_elementwise: no set 1 + sqrt x = 3 -----------------------//*)
273 (*============ inhibit exn WN120314: similar complicated equation, dropped.
274 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "- 1 + 4 * x = 0")) then ()
275 else error "rootrateq.sml: diff.behav.ppoly in rootrat_equation_right_1";
276 val (p,_,f,nxt,_,pt) = me nxt p c pt;
277 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
278 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
279 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
280 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
281 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
282 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
283 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
284 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
285 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
286 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
287 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
288 | _ => error "rootrateq.sml: diff.behav. in - 2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
289 ============ inhibit exn WN120314 ==============================================*)
291 "------------ test thm rootrat_equation_right_2 ------------------";
292 "------------ test thm rootrat_equation_right_2 ------------------";
293 "------------ test thm rootrat_equation_right_2 ------------------";
294 val fmz = ["equality (1 = 3/(1+sqrt(x)))", "solveFor x", "solutions L"];
295 val (dI',pI',mI') = ("RootRatEq",["univariate", "equation"],["no_met"]);
297 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
298 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
299 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
300 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
301 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
302 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
304 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
305 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
306 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
307 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
309 (*//------------------ ERROR rls "make_rooteq " missing in Know_Store.
310 after repair (Try (Repeat (Rewrite_Set ''make_rooteq '')))
311 ------------------ ERROR check_elementwise: no set 1 + sqrt x = 3 -----------------------\\* )
312 (*val (p,_,f,nxt,_,pt) =*) me nxt p c pt;
313 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
315 (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
316 case Step.by_tactic tac (pt, p) of
317 ("ok", (_, _, ptp)) => ptp
318 | ("unsafe-ok", (_, _, ptp)) => ptp
319 | ("not-applicable",_) => (pt, p)
320 | ("end-of-calculation", (_, _, ptp)) => ptp
321 | ("failure", _) => error "sys-error"
322 | _ => error "me: uncovered case Step.by_tactic"
325 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
326 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
327 = (p, ((pt, Pos.e_pos'), []));
328 val pIopt = Ctree.get_pblID (pt, ip);
329 (*if*) ip = ([], Pos.Res) (*else*);
330 val _ = (*case*) tacis (*of*);
331 val SOME _ = (*case*) pIopt (*of*);
333 switch_specify_solve p_ (pt, ip);
334 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
335 (*if*) member op = [Pos.Pbl, Pos.Met] state_pos (*else*);
337 LI.do_next (pt, input_pos);
338 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
339 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
340 val thy' = get_obj g_domID pt (par_pblobj pt p);
342 val (_, (ist, ctxt), sc) =
343 LItool.resume_prog thy' (p,p_) pt;
344 "~~~~~ fun resume_prog , args:"; val (thy, (p, p_), pt) = (thy', (p,p_), pt);
345 (*if*) Pos.on_specification (p, p_) (*else*);
346 val (pbl, p', rls') = parent_node pt p
348 val metID = get_obj g_metID pt p'
349 (*["RootEq", "solve_sq_root_equation"] found for correction, which caused ERROR 2*)
351 (*\\------------------ end ERROR check ------------------------------------------------------//*)
353 val (p,_,f,nxt,_,pt) = me nxt p c pt;
355 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
356 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
357 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
358 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
359 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
361 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
362 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
363 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
364 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
365 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
367 val (p,_,f,nxt,_,pt) = me nxt p c pt;
368 ( *\\------------------ ERROR WN200211 1, 2 -------------------------------------------------//*)
370 (*============ inhibit exn WN120314 ==============================================
371 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "-4 + x = 0")) then ()
372 else error "rootrateq.sml: diff.behav. in rootrat_equation_right_2";
373 val (p,_,f,nxt,_,pt) = me nxt p c pt;
374 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
375 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
376 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
377 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
378 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
379 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
380 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
381 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
382 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
383 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
384 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
385 | _ => error "rootrateq.sml: diff.behav. in 3/(1+sqrt(x))= 1 -> [x = 4]";
386 ============ inhibit exn WN120314 ==============================================*)