156 "----------- rewrite_terms_ -------------------------------------"; |
156 "----------- rewrite_terms_ -------------------------------------"; |
157 "----------- rewrite_terms_ -------------------------------------"; |
157 "----------- rewrite_terms_ -------------------------------------"; |
158 "----------- rewrite_terms_ -------------------------------------"; |
158 "----------- rewrite_terms_ -------------------------------------"; |
159 val subte = [str2term"x = 0"]; |
159 val subte = [str2term"x = 0"]; |
160 val t = str2term"M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2"; |
160 val t = str2term"M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2"; |
161 val Some (t',_) = rewrite_terms_ thy dummy_ord Erls subte t; |
161 val SOME (t',_) = rewrite_terms_ thy dummy_ord Erls subte t; |
162 if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then () |
162 if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then () |
163 else raise error "rewrite.sml rewrite_terms_ [x = 0]"; |
163 else raise error "rewrite.sml rewrite_terms_ [x = 0]"; |
164 |
164 |
165 val subte = [str2term"M_b 0 = 0"]; |
165 val subte = [str2term"M_b 0 = 0"]; |
166 val t = str2term"M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2"; |
166 val t = str2term"M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2"; |
167 val Some (t',_) = rewrite_terms_ thy dummy_ord Erls subte t; |
167 val SOME (t',_) = rewrite_terms_ thy dummy_ord Erls subte t; |
168 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then () |
168 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then () |
169 else raise error "rewrite.sml rewrite_terms_ [M_b 0 = 0]"; |
169 else raise error "rewrite.sml rewrite_terms_ [M_b 0 = 0]"; |
170 |
170 |
171 val subte = [str2term"x = 0", str2term"M_b 0 = 0"]; |
171 val subte = [str2term"x = 0", str2term"M_b 0 = 0"]; |
172 val t = str2term"M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2"; |
172 val t = str2term"M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2"; |
173 val Some (t',_) = rewrite_terms_ thy dummy_ord Erls subte t; |
173 val SOME (t',_) = rewrite_terms_ thy dummy_ord Erls subte t; |
174 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then () |
174 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then () |
175 else raise error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]"; |
175 else raise error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]"; |
176 |
176 |
177 |
177 |
178 "----------- rewrite_inst_ bdvs ----------------------------------"; |
178 "----------- rewrite_inst_ bdvs ----------------------------------"; |
183 val bdvs = [(str2term"bdv_1",str2term"c"), |
183 val bdvs = [(str2term"bdv_1",str2term"c"), |
184 (str2term"bdv_2",str2term"c_2"), |
184 (str2term"bdv_2",str2term"c_2"), |
185 (str2term"bdv_3",str2term"c_3"), |
185 (str2term"bdv_3",str2term"c_3"), |
186 (str2term"bdv_4",str2term"c_4")]; |
186 (str2term"bdv_4",str2term"c_4")]; |
187 (*------------ outcommented WN071210, after inclusion into ROOT.ML |
187 (*------------ outcommented WN071210, after inclusion into ROOT.ML |
188 val Some (t,_) = |
188 val SOME (t,_) = |
189 rewrite_inst_ thy e_rew_ord |
189 rewrite_inst_ thy e_rew_ord |
190 (append_rls "erls_isolate_bdvs" e_rls |
190 (append_rls "erls_isolate_bdvs" e_rls |
191 [(Calc ("EqSystem.occur'_exactly'_in", |
191 [(Calc ("EqSystem.occur'_exactly'_in", |
192 eval_occur_exactly_in |
192 eval_occur_exactly_in |
193 "#eval_occur_exactly_in_")) |
193 "#eval_occur_exactly_in_")) |