233 "----------- Pattern.match ------------------------------"; |
233 "----------- Pattern.match ------------------------------"; |
234 "----------- Pattern.match ------------------------------"; |
234 "----------- Pattern.match ------------------------------"; |
235 val t = (Thm.term_of o the o (parse thy)) "3 * x^^^2 = (1::real)"; |
235 val t = (Thm.term_of o the o (parse thy)) "3 * x^^^2 = (1::real)"; |
236 val pat = (free2var o Thm.term_of o the o (parse thy)) "a * b^^^2 = (c::real)"; |
236 val pat = (free2var o Thm.term_of o the o (parse thy)) "a * b^^^2 = (c::real)"; |
237 (* !^^^^^^^^!... necessary for Pattern.match, see Logic.varify_global below*) |
237 (* !^^^^^^^^!... necessary for Pattern.match, see Logic.varify_global below*) |
238 val insts = Pattern.match @{theory "Isac"} (pat, t) (Vartab.empty, Vartab.empty); |
238 val insts = Pattern.match @{theory "Isac_Knowledge"} (pat, t) (Vartab.empty, Vartab.empty); |
239 (*default_print_depth 3; 999*) insts; |
239 (*default_print_depth 3; 999*) insts; |
240 (*val insts = |
240 (*val insts = |
241 ({}, |
241 ({}, |
242 {(("a", 0), ("Real.real", Free ("3", "Real.real"))), |
242 {(("a", 0), ("Real.real", Free ("3", "Real.real"))), |
243 (("b", 0), ("Real.real", Free ("x", "Real.real"))), |
243 (("b", 0), ("Real.real", Free ("x", "Real.real"))), |
244 (("c", 0), ("Real.real", Free ("1", "Real.real")))})*) |
244 (("c", 0), ("Real.real", Free ("1", "Real.real")))})*) |
245 |
245 |
246 "----- throws exn MATCH..."; |
246 "----- throws exn MATCH..."; |
247 (* val t = str2term "x"; |
247 (* val t = str2term "x"; |
248 (Pattern.match @{theory "Isac"} (pat, t) (Vartab.empty, Vartab.empty)) |
248 (Pattern.match @{theory "Isac_Knowledge"} (pat, t) (Vartab.empty, Vartab.empty)) |
249 handle MATCH => ???; *) |
249 handle MATCH => ???; *) |
250 |
250 |
251 val thy = @{theory "Complex_Main"}; |
251 val thy = @{theory "Complex_Main"}; |
252 val PARSE = Syntax.read_term_global thy; |
252 val PARSE = Syntax.read_term_global thy; |
253 val (pa, tm) = (PARSE "a + b::real", PARSE "x + 2*z::real"); |
253 val (pa, tm) = (PARSE "a + b::real", PARSE "x + 2*z::real"); |
486 "----------- check writeln, tracing for string markup ---"; |
486 "----------- check writeln, tracing for string markup ---"; |
487 "----------- check writeln, tracing for string markup ---"; |
487 "----------- check writeln, tracing for string markup ---"; |
488 "----------- check writeln, tracing for string markup ---"; |
488 "----------- check writeln, tracing for string markup ---"; |
489 val t = @{term "x + 1"}; |
489 val t = @{term "x + 1"}; |
490 val str_markup = (Syntax.string_of_term |
490 val str_markup = (Syntax.string_of_term |
491 (Proof_Context.init_global (Thy_Info_get_theory "Isac"))) t; |
491 (Proof_Context.init_global (Thy_Info_get_theory "Isac_Knowledge"))) t; |
492 val str = term_to_string'' "Isac" t; |
492 val str = term_to_string'' "Isac_Knowledge" t; |
493 |
493 |
494 writeln "----------------writeln str_markup---"; |
494 writeln "----------------writeln str_markup---"; |
495 writeln str_markup; |
495 writeln str_markup; |
496 writeln "----------------writeln str---"; |
496 writeln "----------------writeln str---"; |
497 writeln str; |
497 writeln str; |
524 *) |
524 *) |
525 |
525 |
526 "----------- check writeln, tracing for string markup ---"; |
526 "----------- check writeln, tracing for string markup ---"; |
527 val t = @{term "x + 1"}; |
527 val t = @{term "x + 1"}; |
528 val str_markup = (Syntax.string_of_term |
528 val str_markup = (Syntax.string_of_term |
529 (Proof_Context.init_global (Thy_Info_get_theory "Isac"))) t; |
529 (Proof_Context.init_global (Thy_Info_get_theory "Isac_Knowledge"))) t; |
530 val str = term_to_string'' "Isac" t; |
530 val str = term_to_string'' "Isac_Knowledge" t; |
531 |
531 |
532 writeln "----------------writeln str_markup---"; |
532 writeln "----------------writeln str_markup---"; |
533 writeln str_markup; |
533 writeln str_markup; |
534 writeln "----------------writeln str---"; |
534 writeln "----------------writeln str---"; |
535 writeln str; |
535 writeln str; |