170 |
170 |
171 "----------- simplify by ruleset reducing make_ratpoly_in"; |
171 "----------- simplify by ruleset reducing make_ratpoly_in"; |
172 "----------- simplify by ruleset reducing make_ratpoly_in"; |
172 "----------- simplify by ruleset reducing make_ratpoly_in"; |
173 "----------- simplify by ruleset reducing make_ratpoly_in"; |
173 "----------- simplify by ruleset reducing make_ratpoly_in"; |
174 val thy = @{theory "Isac_Knowledge"}; |
174 val thy = @{theory "Isac_Knowledge"}; |
|
175 val subst = [(TermC.str2term "bdv ::real", TermC.str2term "x ::real")]; (*DOESN'T HELP*) |
175 "===== test 1"; |
176 "===== test 1"; |
176 val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)"; |
177 val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)"; |
177 |
178 |
178 "----- stepwise from the rulesets in simplify_Integral and below-----"; |
179 "----- stepwise from the rulesets in simplify_Integral and below-----"; |
179 val rls = norm_Rational_noadd_fractions; |
180 val rls = norm_Rational_noadd_fractions; |
181 SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2" |
182 SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2" |
182 | NONE => (); |
183 | NONE => (); |
183 |
184 |
184 "===== test 2"; |
185 "===== test 2"; |
185 val rls = order_add_mult_in; |
186 val rls = order_add_mult_in; |
186 (*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO\\ |
187 val SOME (t, []) = rewrite_set_inst_ thy true subst rls t; |
187 assume flawed test setup hidden by "handle _ => ..." |
|
188 ERROR ord_make_polynomial_in called with subst = [] |
|
189 val SOME (t,[]) = rewrite_set_ thy true rls t; |
|
190 if UnparseC.term t = "1 / EI * (L * (q_0 * x) / 2 + - 1 * (q_0 * x \<up> 2) / 2)" then() |
188 if UnparseC.term t = "1 / EI * (L * (q_0 * x) / 2 + - 1 * (q_0 * x \<up> 2) / 2)" then() |
191 else error "integrate.sml simplify by ruleset order_add_mult_in #2"; |
189 else error "integrate.sml simplify by ruleset order_add_mult_in #2"; |
192 \\--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----//*) |
|
193 |
190 |
194 "===== test 3"; |
191 "===== test 3"; |
195 val rls = discard_parentheses; |
192 val rls = discard_parentheses; |
196 (*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO\\ |
193 val SOME (t, []) = rewrite_set_ thy true rls t; |
197 assume flawed test setup hidden by "handle _ => ..." |
|
198 ERROR ord_make_polynomial_in called with subst = [] |
|
199 val SOME (t,[]) = rewrite_set_ thy true rls t; |
|
200 if UnparseC.term t = "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)" then () |
194 if UnparseC.term t = "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)" then () |
201 else error "integrate.sml simplify by ruleset discard_parenth.. #3"; |
195 else error "integrate.sml simplify by ruleset discard_parenth.. #3"; |
202 \\--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO//*) |
|
203 |
196 |
204 "===== test 4"; |
197 "===== test 4"; |
205 val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")]; |
198 val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")]; |
206 val rls = |
199 val rls = |
207 (Rule_Set.append_rules "separate_bdv" collect_bdv |
200 (Rule_Set.append_rules "separate_bdv" collect_bdv |