230 |
230 |
231 "----------- Pattern.match ------------------------------"; |
231 "----------- Pattern.match ------------------------------"; |
232 "----------- Pattern.match ------------------------------"; |
232 "----------- Pattern.match ------------------------------"; |
233 "----------- Pattern.match ------------------------------"; |
233 "----------- Pattern.match ------------------------------"; |
234 val t = TermC.parse_test @{context} "3 * x\<up>2 = (1::real)"; |
234 val t = TermC.parse_test @{context} "3 * x\<up>2 = (1::real)"; |
235 val pat = (TermC.free2var o TermC.parse_test @{context}) "a * b\<up>2 = (c::real)"; |
235 val pat = (TermC.mk_Var o TermC.parse_test @{context}) "a * b\<up>2 = (c::real)"; |
236 (* ! \<up> \<up> ^^!... necessary for Pattern.match, see Logic.varify_global below*) |
236 (* ! \<up> \<up> ^^!... necessary for Pattern.match, see Logic.varify_global below*) |
237 val insts = Pattern.match @{theory "Isac_Knowledge"} (pat, t) (Vartab.empty, Vartab.empty); |
237 val insts = Pattern.match @{theory "Isac_Knowledge"} (pat, t) (Vartab.empty, Vartab.empty); |
238 (*default_print_depth 3; 999*) insts; |
238 (*default_print_depth 3; 999*) insts; |
239 (*val insts = |
239 (*val insts = |
240 ({}, |
240 ({}, |
265 |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x \<up> #2 + #8)"],*) |
265 |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x \<up> #2 + #8)"],*) |
266 val thy = @{theory "Complex_Main"}; |
266 val thy = @{theory "Complex_Main"}; |
267 |
267 |
268 "----- test 1: OK"; |
268 "----- test 1: OK"; |
269 val pa = Logic.varify_global @{term "a = (0::real)"}; (*<<<<<<<---------------*) |
269 val pa = Logic.varify_global @{term "a = (0::real)"}; (*<<<<<<<---------------*) |
270 tracing "paIsa=..."; TermC.atomty pa; tracing "...=paIsa"; |
270 tracing "paIsa=..."; TermC.atom_trace_detail @{context} pa; tracing "...=paIsa"; |
271 (*** |
271 (*** |
272 *** Const (op =, real => real => bool) |
272 *** Const (op =, real => real => bool) |
273 *** . Var ((a, 0), real) |
273 *** . Var ((a, 0), real) |
274 *** . Const (Groups.zero_class.zero, real) |
274 *** . Const (Groups.zero_class.zero, real) |
275 ***) |
275 ***) |
282 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 1" |
282 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 1" |
283 else (); |
283 else (); |
284 |
284 |
285 "----- test 2: Nok"; |
285 "----- test 2: Nok"; |
286 val pa = Logic.varify_global (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*) |
286 val pa = Logic.varify_global (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*) |
287 tracing "paLo2=..."; TermC.atomty pa; tracing "...=paLo2"; |
287 tracing "paLo2=..."; TermC.atom_trace_detail @{context} pa; tracing "...=paLo2"; |
288 (*** |
288 (*** |
289 *** Const (op =, real => real => bool) |
289 *** Const (op =, real => real => bool) |
290 *** . Var ((a, 0), real) |
290 *** . Var ((a, 0), real) |
291 *** . Var ((0, 0), real) |
291 *** . Var ((0, 0), real) |
292 ***) |
292 ***) |
301 (* i.e. !!!!!!!!!!!!!!!!! THIS KIND OF PATTERN IS NOT RELIABLE !!!!!!!!!!!!!!!!! |
301 (* i.e. !!!!!!!!!!!!!!!!! THIS KIND OF PATTERN IS NOT RELIABLE !!!!!!!!!!!!!!!!! |
302 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 2" |
302 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 2" |
303 else ();*) |
303 else ();*) |
304 |
304 |
305 "----- test 3: OK"; |
305 "----- test 3: OK"; |
306 val pa = TermC.free2var (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*) |
306 val pa = TermC.mk_Var (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*) |
307 tracing "paF2=..."; TermC.atomty pa; tracing "...=paF2"; |
307 tracing "paF2=..."; TermC.atom_trace_detail @{context} pa; tracing "...=paF2"; |
308 (*** |
308 (*** |
309 *** Const (op =, real => real => bool) |
309 *** Const (op =, real => real => bool) |
310 *** . Var ((a, 0), real) |
310 *** . Var ((a, 0), real) |
311 *** . Free (0, real) |
311 *** . Free (0, real) |
312 ***) |
312 ***) |
318 val tm = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*) |
318 val tm = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*) |
319 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 3" |
319 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 3" |
320 else (); |
320 else (); |
321 |
321 |
322 "----- test 4=3 with specific data"; |
322 "----- test 4=3 with specific data"; |
323 val pa = TermC.free2var (TermC.parse_test @{context} "M_b 0"); |
323 val pa = TermC.mk_Var (TermC.parse_test @{context} "M_b 0"); |
324 "----- test 4a true"; |
324 "----- test 4a true"; |
325 val tm = TermC.parse_test @{context} "M_b 0"; |
325 val tm = TermC.parse_test @{context} "M_b 0"; |
326 if TermC.matches thy tm pa then () |
326 if TermC.matches thy tm pa then () |
327 else error "termC.sml diff.behav. in TermC.matches true 4"; |
327 else error "termC.sml diff.behav. in TermC.matches true 4"; |
328 "----- test 4b false"; |
328 "----- test 4b false"; |
333 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------"; |
333 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------"; |
334 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------"; |
334 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------"; |
335 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------"; |
335 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------"; |
336 (* added after Isabelle2015->17 |
336 (* added after Isabelle2015->17 |
337 > val (SOME ct) = TermC.parse thy "(-#5)\<up>#3"; |
337 > val (SOME ct) = TermC.parse thy "(-#5)\<up>#3"; |
338 > TermC.atomty (Thm.term_of ct); |
338 > TermC.atom_trace_detail @{context} (Thm.term_of ct); |
339 *** ------------- |
339 *** ------------- |
340 *** Const ( Nat.op ^, ['a, nat] => 'a) |
340 *** Const ( Nat.op ^, ['a, nat] => 'a) |
341 *** Const ( uminus, 'a => 'a) |
341 *** Const ( uminus, 'a => 'a) |
342 *** Free ( #5, 'a) |
342 *** Free ( #5, 'a) |
343 *** Free ( #3, nat) |
343 *** Free ( #3, nat) |
344 > val (SOME ct) = TermC.parse thy "R=R"; |
344 > val (SOME ct) = TermC.parse thy "R=R"; |
345 > TermC.atomty (Thm.term_of ct); |
345 > TermC.atom_trace_detail @{context} (Thm.term_of ct); |
346 *** ------------- |
346 *** ------------- |
347 *** Const ( op =, [real, real] => bool) |
347 *** Const ( op =, [real, real] => bool) |
348 *** Free ( R, real) |
348 *** Free ( R, real) |
349 *** Free ( R, real) |
349 *** Free ( R, real) |
350 |
350 |