137 end; |
137 end; |
138 (* |
138 (* |
139 > val t = (term_of o the o (parse thy)) "#3 + #4"; |
139 > val t = (term_of o the o (parse thy)) "#3 + #4"; |
140 > val eval_fn = the (assoc (!eval_list, "op +")); |
140 > val eval_fn = the (assoc (!eval_list, "op +")); |
141 > val (SOME (id,t')) = get_pair thy "op +" eval_fn t; |
141 > val (SOME (id,t')) = get_pair thy "op +" eval_fn t; |
142 > Sign.string_of_term (sign_of thy) t'; |
142 > Syntax.string_of_term (thy2ctxt thy) t'; |
143 > atomty t'; |
143 > atomty t'; |
144 > |
144 > |
145 > val t = (term_of o the o (parse thy)) "(a + #3) + #4"; |
145 > val t = (term_of o the o (parse thy)) "(a + #3) + #4"; |
146 > val (SOME (id,t')) = get_pair thy "op +" eval_fn t; |
146 > val (SOME (id,t')) = get_pair thy "op +" eval_fn t; |
147 > Sign.string_of_term (sign_of thy) t'; |
147 > Syntax.string_of_term (thy2ctxt thy) t'; |
148 > |
148 > |
149 > val t = (term_of o the o (parse thy)) "#3 + (#4 + (a::real))"; |
149 > val t = (term_of o the o (parse thy)) "#3 + (#4 + (a::real))"; |
150 > val (SOME (id,t')) = get_pair thy "op +" eval_fn t; |
150 > val (SOME (id,t')) = get_pair thy "op +" eval_fn t; |
151 > Sign.string_of_term (sign_of thy) t'; |
151 > Syntax.string_of_term (thy2ctxt thy) t'; |
152 > |
152 > |
153 > val t = (term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))"; |
153 > val t = (term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))"; |
154 > atomty t; |
154 > atomty t; |
155 > val (SOME (id,t')) = get_pair thy "op +" eval_fn t; |
155 > val (SOME (id,t')) = get_pair thy "op +" eval_fn t; |
156 > Sign.string_of_term (sign_of thy) t'; |
156 > Syntax.string_of_term (thy2ctxt thy) t'; |
157 > val it = "#3 + (#4 + a) = #7 + a" : string |
157 > val it = "#3 + (#4 + a) = #7 + a" : string |
158 > |
158 > |
159 > |
159 > |
160 > val t = (term_of o the o (parse thy)) "#-4//#-2"; |
160 > val t = (term_of o the o (parse thy)) "#-4//#-2"; |
161 > val eval_fn = the (assoc (!eval_list, "cancel")); |
161 > val eval_fn = the (assoc (!eval_list, "cancel")); |
162 > val (SOME (id,t')) = get_pair thy "cancel" eval_fn t; |
162 > val (SOME (id,t')) = get_pair thy "cancel" eval_fn t; |
163 > Sign.string_of_term (sign_of thy) t'; |
163 > Syntax.string_of_term (thy2ctxt thy) t'; |
164 > |
164 > |
165 > val t = (term_of o the o (parse thy)) "#2^^^#3"; |
165 > val t = (term_of o the o (parse thy)) "#2^^^#3"; |
166 > eval_binop "xxx" "pow" t thy; |
166 > eval_binop "xxx" "pow" t thy; |
167 > val eval_fn = (eval_binop "xxx") |
167 > val eval_fn = (eval_binop "xxx") |
168 > : string -> term -> theory -> (string * term) option; |
168 > : string -> term -> theory -> (string * term) option; |
169 > val SOME (id,t') = get_pair thy "pow" eval_fn t; |
169 > val SOME (id,t') = get_pair thy "pow" eval_fn t; |
170 > Sign.string_of_term (sign_of thy) t'; |
170 > Syntax.string_of_term (thy2ctxt thy) t'; |
171 > val eval_fn = the (assoc (!eval_list, "pow")); |
171 > val eval_fn = the (assoc (!eval_list, "pow")); |
172 > val (SOME (id,t')) = get_pair thy "pow" eval_fn t; |
172 > val (SOME (id,t')) = get_pair thy "pow" eval_fn t; |
173 > Sign.string_of_term (sign_of thy) t'; |
173 > Syntax.string_of_term (thy2ctxt thy) t'; |
174 > |
174 > |
175 > val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4"; |
175 > val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4"; |
176 > val eval_fn = the (assoc (!eval_list, "op *")); |
176 > val eval_fn = the (assoc (!eval_list, "op *")); |
177 > val (SOME (id,t')) = get_pair thy "op *" eval_fn t; |
177 > val (SOME (id,t')) = get_pair thy "op *" eval_fn t; |
178 > Sign.string_of_term (sign_of thy) t'; |
178 > Syntax.string_of_term (thy2ctxt thy) t'; |
179 > |
179 > |
180 > val t = (term_of o the o (parse thy)) "#0 < #4"; |
180 > val t = (term_of o the o (parse thy)) "#0 < #4"; |
181 > val eval_fn = the (assoc (!eval_list, "op <")); |
181 > val eval_fn = the (assoc (!eval_list, "op <")); |
182 > val (SOME (id,t')) = get_pair thy "op <" eval_fn t; |
182 > val (SOME (id,t')) = get_pair thy "op <" eval_fn t; |
183 > Sign.string_of_term (sign_of thy) t'; |
183 > Syntax.string_of_term (thy2ctxt thy) t'; |
184 > val t = (term_of o the o (parse thy)) "#0 < #-4"; |
184 > val t = (term_of o the o (parse thy)) "#0 < #-4"; |
185 > val (SOME (id,t')) = get_pair thy "op <" eval_fn t; |
185 > val (SOME (id,t')) = get_pair thy "op <" eval_fn t; |
186 > Sign.string_of_term (sign_of thy) t'; |
186 > Syntax.string_of_term (thy2ctxt thy) t'; |
187 > |
187 > |
188 > val t = (term_of o the o (parse thy)) "#3 is_const"; |
188 > val t = (term_of o the o (parse thy)) "#3 is_const"; |
189 > val eval_fn = the (assoc (!eval_list, "is'_const")); |
189 > val eval_fn = the (assoc (!eval_list, "is'_const")); |
190 > val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t; |
190 > val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t; |
191 > Sign.string_of_term (sign_of thy) t'; |
191 > Syntax.string_of_term (thy2ctxt thy) t'; |
192 > val t = (term_of o the o (parse thy)) "a is_const"; |
192 > val t = (term_of o the o (parse thy)) "a is_const"; |
193 > val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t; |
193 > val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t; |
194 > Sign.string_of_term (sign_of thy) t'; |
194 > Syntax.string_of_term (thy2ctxt thy) t'; |
195 > |
195 > |
196 > val t = (term_of o the o (parse thy)) "#6//(#8::real)"; |
196 > val t = (term_of o the o (parse thy)) "#6//(#8::real)"; |
197 > val eval_fn = the (assoc (!eval_list, "cancel")); |
197 > val eval_fn = the (assoc (!eval_list, "cancel")); |
198 > val (SOME (id,t')) = get_pair thy "cancel" eval_fn t; |
198 > val (SOME (id,t')) = get_pair thy "cancel" eval_fn t; |
199 > Sign.string_of_term (sign_of thy) t'; |
199 > Syntax.string_of_term (thy2ctxt thy) t'; |
200 > |
200 > |
201 > val t = (term_of o the o (parse thy)) "sqrt #12"; |
201 > val t = (term_of o the o (parse thy)) "sqrt #12"; |
202 > val eval_fn = the (assoc (!eval_list, "SqRoot.sqrt")); |
202 > val eval_fn = the (assoc (!eval_list, "SqRoot.sqrt")); |
203 > val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t; |
203 > val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t; |
204 > Sign.string_of_term (sign_of thy) t'; |
204 > Syntax.string_of_term (thy2ctxt thy) t'; |
205 > val it = "sqrt #12 = #2 * sqrt #3 " : string |
205 > val it = "sqrt #12 = #2 * sqrt #3 " : string |
206 > |
206 > |
207 > val t = (term_of o the o (parse thy)) "sqrt #9"; |
207 > val t = (term_of o the o (parse thy)) "sqrt #9"; |
208 > val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t; |
208 > val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t; |
209 > Sign.string_of_term (sign_of thy) t'; |
209 > Syntax.string_of_term (thy2ctxt thy) t'; |
210 > |
210 > |
211 > val t = (term_of o the o (parse thy)) "Nth #2 [#11,#22,#33]"; |
211 > val t = (term_of o the o (parse thy)) "Nth #2 [#11,#22,#33]"; |
212 > val eval_fn = the (assoc (!eval_list, "Tools.Nth")); |
212 > val eval_fn = the (assoc (!eval_list, "Tools.Nth")); |
213 > val (SOME (id,t')) = get_pair thy "Tools.Nth" eval_fn t; |
213 > val (SOME (id,t')) = get_pair thy "Tools.Nth" eval_fn t; |
214 > Sign.string_of_term (sign_of thy) t'; |
214 > Syntax.string_of_term (thy2ctxt thy) t'; |
215 *) |
215 *) |
216 |
216 |
217 (* val ((op_, eval_fn),ct)=(cc,pre); |
217 (* val ((op_, eval_fn),ct)=(cc,pre); |
218 (get_calculation_ Isac.thy (op_, eval_fn) ct) handle e => print_exn e; |
218 (get_calculation_ Isac.thy (op_, eval_fn) ct) handle e => print_exn e; |
219 parse thy "" |
219 parse thy "" |