24 val local_naming: Name_Space.naming |
24 val local_naming: Name_Space.naming |
25 val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context |
25 val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context |
26 val naming_of: Proof.context -> Name_Space.naming |
26 val naming_of: Proof.context -> Name_Space.naming |
27 val restore_naming: Proof.context -> Proof.context -> Proof.context |
27 val restore_naming: Proof.context -> Proof.context -> Proof.context |
28 val full_name: Proof.context -> binding -> string |
28 val full_name: Proof.context -> binding -> string |
|
29 val syntax_of: Proof.context -> Local_Syntax.T |
29 val syn_of: Proof.context -> Syntax.syntax |
30 val syn_of: Proof.context -> Syntax.syntax |
30 val tsig_of: Proof.context -> Type.tsig |
31 val tsig_of: Proof.context -> Type.tsig |
31 val set_defsort: sort -> Proof.context -> Proof.context |
32 val set_defsort: sort -> Proof.context -> Proof.context |
32 val default_sort: Proof.context -> indexname -> sort |
33 val default_sort: Proof.context -> indexname -> sort |
33 val consts_of: Proof.context -> Consts.T |
34 val consts_of: Proof.context -> Consts.T |
63 val read_const_proper: Proof.context -> bool -> string -> term |
64 val read_const_proper: Proof.context -> bool -> string -> term |
64 val read_const: Proof.context -> bool -> typ -> string -> term |
65 val read_const: Proof.context -> bool -> typ -> string -> term |
65 val allow_dummies: Proof.context -> Proof.context |
66 val allow_dummies: Proof.context -> Proof.context |
66 val check_tvar: Proof.context -> indexname * sort -> indexname * sort |
67 val check_tvar: Proof.context -> indexname * sort -> indexname * sort |
67 val check_tfree: Proof.context -> string * sort -> string * sort |
68 val check_tfree: Proof.context -> string * sort -> string * sort |
|
69 val get_sort: Proof.context -> (indexname * sort) list -> indexname -> sort |
68 val type_context: Proof.context -> Syntax.type_context |
70 val type_context: Proof.context -> Syntax.type_context |
69 val term_context: Proof.context -> Syntax.term_context |
71 val term_context: Proof.context -> Syntax.term_context |
70 val decode_term: Proof.context -> |
72 val decode_term: Proof.context -> |
71 Position.reports * term Exn.result -> Position.reports * term Exn.result |
73 Position.reports * term Exn.result -> Position.reports * term Exn.result |
72 val standard_infer_types: Proof.context -> term list -> term list |
74 val standard_infer_types: Proof.context -> term list -> term list |
744 |
746 |
745 end; |
747 end; |
746 |
748 |
747 |
749 |
748 |
750 |
749 (** inner syntax operations **) |
|
750 |
|
751 local |
|
752 |
|
753 fun parse_failed ctxt pos msg kind = |
|
754 cat_error msg ("Failed to parse " ^ kind ^ |
|
755 Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad "")); |
|
756 |
|
757 fun parse_sort ctxt text = |
|
758 let |
|
759 val (syms, pos) = Syntax.parse_token ctxt Markup.sort text; |
|
760 val S = |
|
761 Syntax.standard_parse_sort ctxt (type_context ctxt) (syn_of ctxt) (syms, pos) |
|
762 handle ERROR msg => parse_failed ctxt pos msg "sort"; |
|
763 in Type.minimize_sort (tsig_of ctxt) S end; |
|
764 |
|
765 fun parse_typ ctxt text = |
|
766 let |
|
767 val (syms, pos) = Syntax.parse_token ctxt Markup.typ text; |
|
768 val T = |
|
769 Syntax.standard_parse_typ ctxt (type_context ctxt) (syn_of ctxt) (get_sort ctxt) (syms, pos) |
|
770 handle ERROR msg => parse_failed ctxt pos msg "type"; |
|
771 in T end; |
|
772 |
|
773 fun parse_term T ctxt text = |
|
774 let |
|
775 val (T', _) = Type_Infer.paramify_dummies T 0; |
|
776 val (markup, kind) = |
|
777 if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term"); |
|
778 val (syms, pos) = Syntax.parse_token ctxt markup text; |
|
779 |
|
780 val default_root = Config.get ctxt Syntax.default_root; |
|
781 val root = |
|
782 (case T' of |
|
783 Type (c, _) => |
|
784 if c <> "prop" andalso Type.is_logtype (tsig_of ctxt) c |
|
785 then default_root else c |
|
786 | _ => default_root); |
|
787 |
|
788 fun check t = (Syntax.check_term ctxt (Type.constraint T' t); Exn.Result t) |
|
789 handle exn as ERROR _ => Exn.Exn exn; |
|
790 val t = |
|
791 Syntax.standard_parse_term check ctxt (type_context ctxt) (term_context ctxt) (syn_of ctxt) |
|
792 root (syms, pos) |
|
793 handle ERROR msg => parse_failed ctxt pos msg kind; |
|
794 in t end; |
|
795 |
|
796 |
|
797 fun unparse_sort ctxt = |
|
798 Syntax.standard_unparse_sort {extern_class = Type.extern_class (tsig_of ctxt)} |
|
799 ctxt (syn_of ctxt); |
|
800 |
|
801 fun unparse_typ ctxt = |
|
802 let |
|
803 val tsig = tsig_of ctxt; |
|
804 val extern = {extern_class = Type.extern_class tsig, extern_type = Type.extern_type tsig}; |
|
805 in Syntax.standard_unparse_typ extern ctxt (syn_of ctxt) end; |
|
806 |
|
807 fun unparse_term ctxt = |
|
808 let |
|
809 val tsig = tsig_of ctxt; |
|
810 val syntax = syntax_of ctxt; |
|
811 val consts = consts_of ctxt; |
|
812 val extern = |
|
813 {extern_class = Type.extern_class tsig, |
|
814 extern_type = Type.extern_type tsig, |
|
815 extern_const = Consts.extern consts}; |
|
816 in |
|
817 Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt |
|
818 (Local_Syntax.syn_of syntax) (not (Pure_Thy.old_appl_syntax (theory_of ctxt))) |
|
819 end; |
|
820 |
|
821 in |
|
822 |
|
823 val _ = Syntax.install_operations |
|
824 {parse_sort = parse_sort, |
|
825 parse_typ = parse_typ, |
|
826 parse_term = parse_term dummyT, |
|
827 parse_prop = parse_term propT, |
|
828 unparse_sort = unparse_sort, |
|
829 unparse_typ = unparse_typ, |
|
830 unparse_term = unparse_term}; |
|
831 |
|
832 end; |
|
833 |
|
834 |
|
835 |
|
836 (** export results **) |
751 (** export results **) |
837 |
752 |
838 fun common_export is_goal inner outer = |
753 fun common_export is_goal inner outer = |
839 map (Assumption.export is_goal inner outer) #> |
754 map (Assumption.export is_goal inner outer) #> |
840 Variable.export inner outer; |
755 Variable.export inner outer; |