221 val f_ = TermC.parse_test @{context} "f_f::bool"; |
221 val f_ = TermC.parse_test @{context} "f_f::bool"; |
222 val f = TermC.parse_test @{context} "A = s * (a - s)"; |
222 val f = TermC.parse_test @{context} "A = s * (a - s)"; |
223 val v_ = TermC.parse_test @{context} "v_v"; |
223 val v_ = TermC.parse_test @{context} "v_v"; |
224 val v = TermC.parse_test @{context} "s"; |
224 val v = TermC.parse_test @{context} "s"; |
225 val screxp0 = TermC.parse_test @{context} "Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))"; |
225 val screxp0 = TermC.parse_test @{context} "Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))"; |
226 TermC.atomty screxp0; |
226 TermC.atom_trace_detail @{context} screxp0; |
227 |
227 |
228 val screxp1 = subst_atomic [(f_, f), (v_, v)] screxp0; |
228 val screxp1 = subst_atomic [(f_, f), (v_, v)] screxp0; |
229 UnparseC.term screxp1; |
229 UnparseC.term screxp1; |
230 TermC.atomty screxp1; |
230 TermC.atom_trace_detail @{context} screxp1; |
231 |
231 |
232 val SOME (f'_,_) = rewrite_set_ ctxt false srls_diff screxp1; |
232 val SOME (f'_,_) = rewrite_set_ ctxt false srls_diff screxp1; |
233 if UnparseC.term f'_= "Take (A' = d_d s (s * (a - s)))" then () |
233 if UnparseC.term f'_= "Take (A' = d_d s (s * (a - s)))" then () |
234 else error "diff.sml: diff.behav. in 'primed'"; |
234 else error "diff.sml: diff.behav. in 'primed'"; |
235 TermC.atomty f'_; |
235 TermC.atom_trace_detail @{context} f'_; |
236 |
236 |
237 val str = "Program DiffEqScr (f_f::bool) (v_v::real) = \ |
237 val str = "Program DiffEqScr (f_f::bool) (v_v::real) = \ |
238 \ (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) \ |
238 \ (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) \ |
239 \ in (((Try (Repeat (Rewrite frac_conv))) #> \ |
239 \ in (((Try (Repeat (Rewrite frac_conv))) #> \ |
240 \ (Try (Repeat (Rewrite root_conv))) #> \ |
240 \ (Try (Repeat (Rewrite root_conv))) #> \ |