13 "----------- parsing ---------------------------------------------"; |
13 "----------- parsing ---------------------------------------------"; |
14 "----------- integrate by rewriting ------------------------------"; |
14 "----------- integrate by rewriting ------------------------------"; |
15 "----------- test new_c ------------------------------------------"; |
15 "----------- test new_c ------------------------------------------"; |
16 "----------- integrate by ruleset --------------------------------"; |
16 "----------- integrate by ruleset --------------------------------"; |
17 "----------- check probem type -----------------------------------"; |
17 "----------- check probem type -----------------------------------"; |
18 "----------- check method [Diff,integration] ---------------------"; |
18 "----------- check Scripts ---------------------------------------"; |
19 "----------- me method [Diff,integration] ---------------------"; |
19 "----------- me method [Diff,integration] ------------------------"; |
20 "----------- check method [Diff,integration,named] ---------------"; |
|
21 "-----------------------------------------------------------------"; |
20 "-----------------------------------------------------------------"; |
22 "-----------------------------------------------------------------"; |
21 "-----------------------------------------------------------------"; |
23 "-----------------------------------------------------------------"; |
22 "-----------------------------------------------------------------"; |
24 |
23 |
25 "----------- parsing ---------------------------------------------"; |
24 "----------- parsing ---------------------------------------------"; |
153 show_ptyps(); |
152 show_ptyps(); |
154 val pbl = get_pbt ["integrate","function"]; |
153 val pbl = get_pbt ["integrate","function"]; |
155 case #cas pbl of Some (Const ("Integrate.Integrate",_) $ _) => () |
154 case #cas pbl of Some (Const ("Integrate.Integrate",_) $ _) => () |
156 | _ => raise error "integrate.sml: Integrate.Integrate ???"; |
155 | _ => raise error "integrate.sml: Integrate.Integrate ???"; |
157 |
156 |
158 "----------- check method [Diff,integration] ---------------------"; |
157 |
159 "----------- check method [Diff,integration] ---------------------"; |
158 "----------- check Scripts ---------------------------------------"; |
160 "----------- check method [Diff,integration] ---------------------"; |
159 "----------- check Scripts ---------------------------------------"; |
161 show_mets(); |
160 "----------- check Scripts ---------------------------------------"; |
162 (* |
|
163 val str = |
161 val str = |
164 "Script IntegrationScript (f_::real) (v_::real) = \ |
162 "Script IntegrationScript (f_::real) (v_::real) = \ |
165 \ (let t_ = (Integral f_ D v_)::real \ |
163 \ (let t_ = Integral f_ D v_ \ |
166 \ in (Rewrite_Set_Inst [(bdv,v_)] integration False t_::real))"; |
164 \ in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))"; |
167 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
165 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
166 atomty thy sc; |
168 |
167 |
169 val str = |
168 val str = |
170 "Script IntegrationScript (f_::real) (v_::real) = \ |
169 "Script NamedIntegrationScript (f_::real) (v_::real) (F_::real) = \ |
171 \ (let t_ = (Integral f_ D v_)::real \ |
170 \ (let t_ = (F_ = Integral f_ D v_) \ |
172 \ in t_)"; |
171 \ in (Rewrite_Set_Inst [(bdv,v_)] integration False) t_)"; |
173 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
172 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
174 val str = |
173 atomty thy sc; |
175 "Rewrite_Set_Inst [(bdv,v_)] integration False (t_::real)"; |
174 show_mets(); |
176 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
177 |
175 |
178 |
|
179 atomty thy sc; |
|
180 ###############################################################*) |
|
181 |
176 |
182 "----------- me method [Diff,integration] ---------------------"; |
177 "----------- me method [Diff,integration] ---------------------"; |
183 "----------- me method [Diff,integration] ---------------------"; |
178 "----------- me method [Diff,integration] ---------------------"; |
184 "----------- me method [Diff,integration] ---------------------"; |
179 "----------- me method [Diff,integration] ---------------------"; |
185 val fmz = ["functionTerm (x^^^2 + 1)", |
180 val fmz = ["functionTerm (x^^^2 + 1)", |
193 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
188 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
194 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
189 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
195 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
190 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
196 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
191 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
197 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
192 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
193 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
198 val (p,_,f,nxt,_,pt) = me nxt p c pt;(*---> Empty_Tac*) |
194 val (p,_,f,nxt,_,pt) = me nxt p c pt;(*---> Empty_Tac*) |
199 |
195 |
200 |
196 |
201 |
197 |
202 |
|
203 |
|
204 "----------- check method [Diff,integration,named] ---------------"; |
|
205 "----------- check method [Diff,integration,named] ---------------"; |
|
206 "----------- check method [Diff,integration,named] ---------------"; |
|
207 val str = |
|
208 "Script NamedIntegrationScript (f_::real) (v_::real) (F_::real) = \ |
|
209 \ (F_ = Integral f_ D v_)"; |
|
210 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
211 atomty thy sc; |
|
212 |
|