7 "--------------------------------------------------------"; |
7 "--------------------------------------------------------"; |
8 "----------- inst_bdv -----------------------------------"; |
8 "----------- inst_bdv -----------------------------------"; |
9 "----------- subst_atomic_all ---------------------------"; |
9 "----------- subst_atomic_all ---------------------------"; |
10 "----------- Pattern.match ------------------------------"; |
10 "----------- Pattern.match ------------------------------"; |
11 "----------- fun matches --------------------------------"; |
11 "----------- fun matches --------------------------------"; |
12 "------------parse---------------------------------------"; |
12 "----------- fun parse, fun parse_patt, fun T_a2real ----"; |
13 "----------- uminus_to_string ---------------------------"; |
13 "----------- uminus_to_string ---------------------------"; |
|
14 "----------- *** prep_pbt: syntax error in '#Where' of [v"; |
14 "--------------------------------------------------------"; |
15 "--------------------------------------------------------"; |
15 "--------------------------------------------------------"; |
16 "--------------------------------------------------------"; |
16 |
17 |
17 |
18 |
18 (*===== inhibit exn ============================================================ |
19 (*===== inhibit exn ============================================================ |
172 val tm = str2term "M_b x"; |
173 val tm = str2term "M_b x"; |
173 if matches thy tm pa then error "termC.sml diff.behav. in matches false 4" |
174 if matches thy tm pa then error "termC.sml diff.behav. in matches false 4" |
174 else (); |
175 else (); |
175 |
176 |
176 |
177 |
177 "------------parse---------------------------------------"; |
178 "----------- fun parse, fun parse_patt, fun T_a2real ----"; |
178 "------------parse---------------------------------------"; |
179 "----------- fun parse, fun parse_patt, fun T_a2real ----"; |
179 "------------parse---------------------------------------"; |
180 "----------- fun parse, fun parse_patt, fun T_a2real ----"; |
|
181 (*Makarius.1003 |
|
182 ML {* @{term "2::int"} *} |
|
183 |
|
184 term "(1.24444) :: real" |
|
185 |
|
186 ML {* numbers_to_string @{term "%x. (-9993::int) + x + 1"} *} |
|
187 |
180 Toplevel.debug := true; |
188 Toplevel.debug := true; |
181 (* literal types: |
189 |
|
190 literal types: |
182 PolyML.addPrettyPrinter |
191 PolyML.addPrettyPrinter |
183 (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ); |
192 (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ); |
184 *)(* pretty types: |
193 *)(* pretty types: |
185 PolyML.addPrettyPrinter |
194 PolyML.addPrettyPrinter |
186 (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy); |
195 (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy); |
195 val t = numbers_to_string (Syntax.read_term_global thy str); |
204 val t = numbers_to_string (Syntax.read_term_global thy str); |
196 val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str); |
205 val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str); |
197 cterm_of thy t; |
206 cterm_of thy t; |
198 val t = (the (parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed"; |
207 val t = (the (parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed"; |
199 |
208 |
200 (*Makarius.1003 |
209 "===== fun parse_patt caused error in fun T_a2real ==="; |
201 ML {* @{term "2::int"} *} |
210 val thy = theory "Poly"; |
202 |
211 parse_patt thy "?p is_addUnordered"; |
203 term "(1.24444) :: real" |
212 parse_patt thy "?p :: real"; |
204 |
|
205 ML {* numbers_to_string @{term "%x. (-9993::int) + x + 1"} *} |
|
206 *) |
|
207 |
|
208 |
213 |
209 "----------- uminus_to_string ---------------------------"; |
214 "----------- uminus_to_string ---------------------------"; |
210 "----------- uminus_to_string ---------------------------"; |
215 "----------- uminus_to_string ---------------------------"; |
211 "----------- uminus_to_string ---------------------------"; |
216 "----------- uminus_to_string ---------------------------"; |
212 val t1 = numbers_to_string @{term "-2::real"}; |
217 val t1 = numbers_to_string @{term "-2::real"}; |
213 val t2 = numbers_to_string @{term "- 2::real"}; |
218 val t2 = numbers_to_string @{term "- 2::real"}; |
214 if uminus_to_string t2 = t1 then () |
219 if uminus_to_string t2 = t1 then () |
215 else error "termC.sml diff.behav. in uminus_to_string"; |
220 else error "termC.sml diff.behav. in uminus_to_string"; |
216 |
221 |
217 |
222 "----------- *** prep_pbt: syntax error in '#Where' of [v"; |
218 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-. |
223 "----------- *** prep_pbt: syntax error in '#Where' of [v"; |
219 -.-.-.-.-.-.-isolate response.-.-.-.-.-.*) |
224 "----------- *** prep_pbt: syntax error in '#Where' of [v"; |
|
225 "===== deconstruct datatype typ ==="; |
|
226 val str = "?a"; |
|
227 val t = (thy, str) |>> thy2ctxt |
|
228 |-> ProofContext.read_term_pattern |
|
229 |> numbers_to_string; |
|
230 val Var (("a", 0), ty) = t; |
|
231 val TVar ((str, i), srt) = ty; |
|
232 if str = "'a" andalso i = 1 andalso srt = [] then () |
|
233 else error "termC.sml type-structure of \"?a\" changed"; |
|
234 |
|
235 "----- real type in pattern ---"; |
|
236 val str = "?a :: real"; |
|
237 val t = (thy, str) |>> thy2ctxt |
|
238 |-> ProofContext.read_term_pattern |
|
239 |> numbers_to_string; |
|
240 val Var (("a", 0), ty) = t; |
|
241 val Type (str, tys) = ty; |
|
242 if str = "RealDef.real" andalso tys = [] andalso ty = HOLogic.realT then () |
|
243 else error "termC.sml type-structure of \"?a :: real\" changed"; |
|
244 |
|
245 "===== Not (matchsub (?a + (?b + ?c)) t_t |... ==="; |
|
246 val (thy, str) = (thy, "Not (matchsub (?a + (?b + ?c)) t_t | " ^ |
|
247 " matchsub (?a + (?b - ?c)) t_t | " ^ |
|
248 " matchsub (?a - (?b + ?c)) t_t | " ^ |
|
249 " matchsub (?a + (?b - ?c)) t_t )"); |
|
250 "----- read_term_pattern ---"; |
|
251 val t = (thy, str) |>> thy2ctxt |
|
252 |-> ProofContext.read_term_pattern |
|
253 |> numbers_to_string; |
|
254 show_types := true; |
|
255 val t1 = typ_a2real t; |
|
256 if term2str t1 = "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n matchsub (?a + (?b - ?c)) t_t |\n matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)" |
|
257 then () else error "termC.sml type-structure of \"?a :: real\" changed expl"; |
|
258 show_types := false; |