739 |
739 |
740 fun parse_sort ctxt text = |
740 fun parse_sort ctxt text = |
741 let |
741 let |
742 val (syms, pos) = Syntax.parse_token ctxt Markup.sort text; |
742 val (syms, pos) = Syntax.parse_token ctxt Markup.sort text; |
743 val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos) |
743 val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos) |
744 handle ERROR msg => cat_error msg ("Failed to parse sort" ^ Position.str_of pos) |
744 handle ERROR msg => cat_error msg "Failed to parse sort"; |
745 in Type.minimize_sort (tsig_of ctxt) S end; |
745 in Type.minimize_sort (tsig_of ctxt) S end; |
746 |
746 |
747 fun parse_typ ctxt text = |
747 fun parse_typ ctxt text = |
748 let |
748 let |
749 val (syms, pos) = Syntax.parse_token ctxt Markup.typ text; |
749 val (syms, pos) = Syntax.parse_token ctxt Markup.typ text; |
750 val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos) |
750 val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos) |
751 handle ERROR msg => cat_error msg ("Failed to parse type" ^ Position.str_of pos); |
751 handle ERROR msg => cat_error msg "Failed to parse type"; |
752 in T end; |
752 in T end; |
753 |
753 |
754 fun parse_term T ctxt text = |
754 fun parse_term T ctxt text = |
755 let |
755 let |
756 val {get_sort, map_const, map_free} = term_context ctxt; |
756 val {get_sort, map_const, map_free} = term_context ctxt; |
757 |
757 |
758 val (T', _) = Type_Infer.paramify_dummies T 0; |
758 val (T', _) = Type_Infer.paramify_dummies T 0; |
759 val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term"); |
759 val (markup, kind) = |
|
760 if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term"); |
760 val (syms, pos) = Syntax.parse_token ctxt markup text; |
761 val (syms, pos) = Syntax.parse_token ctxt markup text; |
761 |
762 |
762 fun check t = (Syntax.check_term ctxt (Type_Infer.constrain T' t); NONE) |
763 fun check t = (Syntax.check_term ctxt (Type_Infer.constrain T' t); NONE) |
763 handle ERROR msg => SOME msg; |
764 handle ERROR msg => SOME msg; |
764 val t = |
765 val t = |
765 Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free |
766 Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free |
766 ctxt (Type.is_logtype (tsig_of ctxt)) (syn_of ctxt) T' (syms, pos) |
767 ctxt (Type.is_logtype (tsig_of ctxt)) (syn_of ctxt) T' (syms, pos) |
767 handle ERROR msg => cat_error msg ("Failed to parse " ^ kind ^ Position.str_of pos); |
768 handle ERROR msg => cat_error msg ("Failed to parse " ^ kind); |
768 in t end; |
769 in t end; |
769 |
770 |
770 |
771 |
771 fun unparse_sort ctxt = |
772 fun unparse_sort ctxt = |
772 Syntax.standard_unparse_sort {extern_class = Type.extern_class (tsig_of ctxt)} |
773 Syntax.standard_unparse_sort {extern_class = Type.extern_class (tsig_of ctxt)} |