wenzelm@42241: (*  Title:      Pure/Syntax/standard_syntax.ML
wenzelm@42241:     Author:     Makarius
wenzelm@42241: 
wenzelm@42241: Standard implementation of inner syntax operations.
wenzelm@42241: *)
wenzelm@42241: 
wenzelm@42241: structure Standard_Syntax: sig end =
wenzelm@42241: struct
wenzelm@42241: 
wenzelm@42241: fun parse_failed ctxt pos msg kind =
wenzelm@42241:   cat_error msg ("Failed to parse " ^ kind ^
wenzelm@42241:     Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
wenzelm@42241: 
wenzelm@42241: fun parse_sort ctxt text =
wenzelm@42241:   let
wenzelm@42241:     val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
wenzelm@42241:     val S =
wenzelm@42241:       Syntax.standard_parse_sort ctxt (ProofContext.type_context ctxt)
wenzelm@42241:           (ProofContext.syn_of ctxt) (syms, pos)
wenzelm@42241:         handle ERROR msg => parse_failed ctxt pos msg "sort";
wenzelm@42241:   in Type.minimize_sort (ProofContext.tsig_of ctxt) S end;
wenzelm@42241: 
wenzelm@42241: fun parse_typ ctxt text =
wenzelm@42241:   let
wenzelm@42241:     val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
wenzelm@42241:     val T =
wenzelm@42241:       Syntax.standard_parse_typ ctxt (ProofContext.type_context ctxt)
wenzelm@42241:           (ProofContext.syn_of ctxt) (ProofContext.get_sort ctxt) (syms, pos)
wenzelm@42241:         handle ERROR msg => parse_failed ctxt pos msg "type";
wenzelm@42241:   in T end;
wenzelm@42241: 
wenzelm@42241: fun parse_term T ctxt text =
wenzelm@42241:   let
wenzelm@42241:     val (T', _) = Type_Infer.paramify_dummies T 0;
wenzelm@42241:     val (markup, kind) =
wenzelm@42241:       if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
wenzelm@42241:     val (syms, pos) = Syntax.parse_token ctxt markup text;
wenzelm@42241: 
wenzelm@42241:     val default_root = Config.get ctxt Syntax.default_root;
wenzelm@42241:     val root =
wenzelm@42241:       (case T' of
wenzelm@42241:         Type (c, _) =>
wenzelm@42241:           if c <> "prop" andalso Type.is_logtype (ProofContext.tsig_of ctxt) c
wenzelm@42241:           then default_root else c
wenzelm@42241:       | _ => default_root);
wenzelm@42241: 
wenzelm@42241:     fun check t = (Syntax.check_term ctxt (Type.constraint T' t); Exn.Result t)
wenzelm@42241:       handle exn as ERROR _ => Exn.Exn exn;
wenzelm@42241:     val t =
wenzelm@42241:       Syntax.standard_parse_term check ctxt
wenzelm@42241:         (ProofContext.type_context ctxt) (ProofContext.term_context ctxt)
wenzelm@42241:         (ProofContext.syn_of ctxt) root (syms, pos)
wenzelm@42241:       handle ERROR msg => parse_failed ctxt pos msg kind;
wenzelm@42241:   in t end;
wenzelm@42241: 
wenzelm@42241: 
wenzelm@42241: fun unparse_sort ctxt =
wenzelm@42241:   Syntax.standard_unparse_sort {extern_class = Type.extern_class (ProofContext.tsig_of ctxt)}
wenzelm@42241:     ctxt (ProofContext.syn_of ctxt);
wenzelm@42241: 
wenzelm@42241: fun unparse_typ ctxt =
wenzelm@42241:   let
wenzelm@42241:     val tsig = ProofContext.tsig_of ctxt;
wenzelm@42241:     val extern = {extern_class = Type.extern_class tsig, extern_type = Type.extern_type tsig};
wenzelm@42241:   in Syntax.standard_unparse_typ extern ctxt (ProofContext.syn_of ctxt) end;
wenzelm@42241: 
wenzelm@42241: fun unparse_term ctxt =
wenzelm@42241:   let
wenzelm@42241:     val tsig = ProofContext.tsig_of ctxt;
wenzelm@42241:     val syntax = ProofContext.syntax_of ctxt;
wenzelm@42241:     val consts = ProofContext.consts_of ctxt;
wenzelm@42241:     val extern =
wenzelm@42241:      {extern_class = Type.extern_class tsig,
wenzelm@42241:       extern_type = Type.extern_type tsig,
wenzelm@42241:       extern_const = Consts.extern consts};
wenzelm@42241:   in
wenzelm@42241:     Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
wenzelm@42241:       (Local_Syntax.syn_of syntax) (not (Pure_Thy.old_appl_syntax (ProofContext.theory_of ctxt)))
wenzelm@42241:   end;
wenzelm@42241: 
wenzelm@42241: 
wenzelm@42241: val _ = Syntax.install_operations
wenzelm@42241:   {parse_sort = parse_sort,
wenzelm@42241:    parse_typ = parse_typ,
wenzelm@42241:    parse_term = parse_term dummyT,
wenzelm@42241:    parse_prop = parse_term propT,
wenzelm@42241:    unparse_sort = unparse_sort,
wenzelm@42241:    unparse_typ = unparse_typ,
wenzelm@42241:    unparse_term = unparse_term};
wenzelm@42241: 
wenzelm@42241: end;