66 val mk_num_op_num: typ -> typ -> string * typ -> int -> int -> term |
66 val mk_num_op_num: typ -> typ -> string * typ -> int -> int -> term |
67 val mk_num_op_var: term -> string -> typ -> typ -> int -> term |
67 val mk_num_op_var: term -> string -> typ -> typ -> int -> term |
68 val mk_var_op_num: term -> string -> typ -> typ -> int -> term |
68 val mk_var_op_num: term -> string -> typ -> typ -> int -> term |
69 |
69 |
70 val matches: theory -> term -> term -> bool |
70 val matches: theory -> term -> term -> bool |
71 val parse: theory -> string -> cterm option |
|
72 val parseN: theory -> string -> cterm option |
|
73 val parseNEW: Proof.context -> string -> term option |
71 val parseNEW: Proof.context -> string -> term option |
74 val parseNEW': Proof.context -> string -> term |
72 val parseNEW': Proof.context -> string -> term |
75 val parseNEW'': theory -> string -> term |
73 val parseNEW'': theory -> string -> term |
76 val parseold: theory -> string -> cterm option |
|
77 val parse_strict: theory -> string -> term |
74 val parse_strict: theory -> string -> term |
78 val parse_patt: theory -> string -> term |
75 val parse_patt: theory -> string -> term |
79 val perm: term -> term -> bool |
76 val perm: term -> term -> bool |
80 |
77 |
81 val str_of_free_opt: term -> string option |
78 val str_of_free_opt: term -> string option |
531 | typ_a2real (Var( n, T)) = (Var( n, T_a2real T)) |
528 | typ_a2real (Var( n, T)) = (Var( n, T_a2real T)) |
532 | typ_a2real (Bound i) = (Bound i) |
529 | typ_a2real (Bound i) = (Bound i) |
533 | typ_a2real (Abs(s,T,t)) = Abs(s, T, typ_a2real t) |
530 | typ_a2real (Abs(s,T,t)) = Abs(s, T, typ_a2real t) |
534 | typ_a2real (t1 $ t2) = (typ_a2real t1) $ (typ_a2real t2); |
531 | typ_a2real (t1 $ t2) = (typ_a2real t1) $ (typ_a2real t2); |
535 |
532 |
536 (* TODO clarify parse with Test_Isac *) |
533 (* TODO clarify parse with Test_Isac * ) |
537 fun parseold thy str = (* before 2002 *) |
534 fun parseold thy str = (* before 2002 *) |
538 \<^try>\<open> |
535 \<^try>\<open> |
539 let val t = Syntax.read_term_global thy str |
536 let val t = Syntax.read_term_global thy str |
540 in Thm.global_cterm_of thy t end\<close>; |
537 in Thm.global_cterm_of thy t end\<close>; |
541 fun parseN thy str = (* introduced 2002 *) |
538 fun parseN thy str = (* introduced 2002 *) |
542 \<^try>\<open> |
539 \<^try>\<open> |
543 let val t = (*(typ_a2real o numbers_to_string)*) (Syntax.read_term_global thy str) |
540 let val t = Syntax.read_term_global thy str |
544 in Thm.global_cterm_of thy t end\<close>; |
541 in Thm.global_cterm_of thy t end\<close>; |
545 |
542 |
546 fun parse_strict thy str = typ_a2real (Syntax.read_term_global thy str); |
|
547 fun parse thy str = (* introduced 2010 *) |
543 fun parse thy str = (* introduced 2010 *) |
548 \<^try>\<open> |
544 \<^try>\<open> |
549 let val t = parse_strict thy str |
545 let val t = parse_strict thy str |
550 in Thm.global_cterm_of thy t end\<close>; |
546 in Thm.global_cterm_of thy t end\<close>; |
|
547 *) |
551 |
548 |
552 (*WN110317 parseNEW will replace parse after introduction of ctxt completed*) |
549 (*WN110317 parseNEW will replace parse after introduction of ctxt completed*) |
553 fun parseNEW ctxt str = \<^try>\<open>Syntax.read_term ctxt str\<close>; |
550 fun parseNEW ctxt str = \<^try>\<open>Syntax.read_term ctxt str\<close>; |
554 fun parseNEW' ctxt str = |
551 fun parseNEW' ctxt str = |
555 case parseNEW ctxt str of |
552 case parseNEW ctxt str of |
557 | NONE => raise TERM ("NO parseNEW' for " ^ str, []) |
554 | NONE => raise TERM ("NO parseNEW' for " ^ str, []) |
558 fun parseNEW'' thy str = |
555 fun parseNEW'' thy str = |
559 case parseNEW (ThyC.to_ctxt thy) str of |
556 case parseNEW (ThyC.to_ctxt thy) str of |
560 SOME t => t |
557 SOME t => t |
561 | NONE => raise TERM ("NO parseNEW'' for " ^ str, []) |
558 | NONE => raise TERM ("NO parseNEW'' for " ^ str, []) |
|
559 fun parse_strict thy str = (*typ_a2real*) (parseNEW'' thy str); |
562 |
560 |
563 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation |
561 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation |
564 WN130613 probably compare to |
562 WN130613 probably compare to |
565 http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04249.html*) |
563 http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04249.html*) |
566 fun parse_patt thy str = (thy, str) |
564 fun parse_patt thy str = (thy, str) |