201 |
201 |
202 |
202 |
203 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t; |
203 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t; |
204 writeln "----------- rewrite_terms_ 1---------------------------"; |
204 writeln "----------- rewrite_terms_ 1---------------------------"; |
205 if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then () |
205 if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then () |
206 else raise error "rewrite.sml rewrite_terms_ [x = 0]"; |
206 else error "rewrite.sml rewrite_terms_ [x = 0]"; |
207 |
207 |
208 val equs = [str2term "M_b 0 = 0"]; |
208 val equs = [str2term "M_b 0 = 0"]; |
209 val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2"; |
209 val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2"; |
210 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t; |
210 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t; |
211 writeln "----------- rewrite_terms_ 2---------------------------"; |
211 writeln "----------- rewrite_terms_ 2---------------------------"; |
212 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then () |
212 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then () |
213 else raise error "rewrite.sml rewrite_terms_ [M_b 0 = 0]"; |
213 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]"; |
214 |
214 |
215 val equs = [str2term "x = 0", str2term"M_b 0 = 0"]; |
215 val equs = [str2term "x = 0", str2term"M_b 0 = 0"]; |
216 val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2"; |
216 val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2"; |
217 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t; |
217 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t; |
218 writeln "----------- rewrite_terms_ 3---------------------------"; |
218 writeln "----------- rewrite_terms_ 3---------------------------"; |
219 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then () |
219 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then () |
220 else raise error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]"; |
220 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]"; |
221 |
221 |
222 |
222 |
223 "----------- rewrite_inst_ bdvs -------------------------"; |
223 "----------- rewrite_inst_ bdvs -------------------------"; |
224 "----------- rewrite_inst_ bdvs -------------------------"; |
224 "----------- rewrite_inst_ bdvs -------------------------"; |
225 "----------- rewrite_inst_ bdvs -------------------------"; |
225 "----------- rewrite_inst_ bdvs -------------------------"; |
238 "#eval_occur_exactly_in_")) |
238 "#eval_occur_exactly_in_")) |
239 ]) |
239 ]) |
240 false bdvs (num_str @{separate_bdvs_add) t; |
240 false bdvs (num_str @{separate_bdvs_add) t; |
241 (writeln o term2str) t; |
241 (writeln o term2str) t; |
242 if term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)" |
242 if term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)" |
243 then () else raise error "rewrite.sml rewrite_inst_ bdvs"; |
243 then () else error "rewrite.sml rewrite_inst_ bdvs"; |
244 trace_rewrite:=true; |
244 trace_rewrite:=true; |
245 trace_rewrite:=false;--------------------------------------------*) |
245 trace_rewrite:=false;--------------------------------------------*) |
246 |
246 |
247 |
247 |
248 "----------- check diff 2002--2009-3 --------------------"; |
248 "----------- check diff 2002--2009-3 --------------------"; |