src/Pure/Syntax/standard_syntax.ML
author wenzelm
Tue Apr 05 18:06:45 2011 +0200 (2011-04-05)
changeset 42241 dd8029f71e1c
child 42242 39261908e12f
permissions -rw-r--r--
separate module for standard implementation of inner syntax operations;
wenzelm@42241
     1
(*  Title:      Pure/Syntax/standard_syntax.ML
wenzelm@42241
     2
    Author:     Makarius
wenzelm@42241
     3
wenzelm@42241
     4
Standard implementation of inner syntax operations.
wenzelm@42241
     5
*)
wenzelm@42241
     6
wenzelm@42241
     7
structure Standard_Syntax: sig end =
wenzelm@42241
     8
struct
wenzelm@42241
     9
wenzelm@42241
    10
fun parse_failed ctxt pos msg kind =
wenzelm@42241
    11
  cat_error msg ("Failed to parse " ^ kind ^
wenzelm@42241
    12
    Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
wenzelm@42241
    13
wenzelm@42241
    14
fun parse_sort ctxt text =
wenzelm@42241
    15
  let
wenzelm@42241
    16
    val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
wenzelm@42241
    17
    val S =
wenzelm@42241
    18
      Syntax.standard_parse_sort ctxt (ProofContext.type_context ctxt)
wenzelm@42241
    19
          (ProofContext.syn_of ctxt) (syms, pos)
wenzelm@42241
    20
        handle ERROR msg => parse_failed ctxt pos msg "sort";
wenzelm@42241
    21
  in Type.minimize_sort (ProofContext.tsig_of ctxt) S end;
wenzelm@42241
    22
wenzelm@42241
    23
fun parse_typ ctxt text =
wenzelm@42241
    24
  let
wenzelm@42241
    25
    val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
wenzelm@42241
    26
    val T =
wenzelm@42241
    27
      Syntax.standard_parse_typ ctxt (ProofContext.type_context ctxt)
wenzelm@42241
    28
          (ProofContext.syn_of ctxt) (ProofContext.get_sort ctxt) (syms, pos)
wenzelm@42241
    29
        handle ERROR msg => parse_failed ctxt pos msg "type";
wenzelm@42241
    30
  in T end;
wenzelm@42241
    31
wenzelm@42241
    32
fun parse_term T ctxt text =
wenzelm@42241
    33
  let
wenzelm@42241
    34
    val (T', _) = Type_Infer.paramify_dummies T 0;
wenzelm@42241
    35
    val (markup, kind) =
wenzelm@42241
    36
      if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
wenzelm@42241
    37
    val (syms, pos) = Syntax.parse_token ctxt markup text;
wenzelm@42241
    38
wenzelm@42241
    39
    val default_root = Config.get ctxt Syntax.default_root;
wenzelm@42241
    40
    val root =
wenzelm@42241
    41
      (case T' of
wenzelm@42241
    42
        Type (c, _) =>
wenzelm@42241
    43
          if c <> "prop" andalso Type.is_logtype (ProofContext.tsig_of ctxt) c
wenzelm@42241
    44
          then default_root else c
wenzelm@42241
    45
      | _ => default_root);
wenzelm@42241
    46
wenzelm@42241
    47
    fun check t = (Syntax.check_term ctxt (Type.constraint T' t); Exn.Result t)
wenzelm@42241
    48
      handle exn as ERROR _ => Exn.Exn exn;
wenzelm@42241
    49
    val t =
wenzelm@42241
    50
      Syntax.standard_parse_term check ctxt
wenzelm@42241
    51
        (ProofContext.type_context ctxt) (ProofContext.term_context ctxt)
wenzelm@42241
    52
        (ProofContext.syn_of ctxt) root (syms, pos)
wenzelm@42241
    53
      handle ERROR msg => parse_failed ctxt pos msg kind;
wenzelm@42241
    54
  in t end;
wenzelm@42241
    55
wenzelm@42241
    56
wenzelm@42241
    57
fun unparse_sort ctxt =
wenzelm@42241
    58
  Syntax.standard_unparse_sort {extern_class = Type.extern_class (ProofContext.tsig_of ctxt)}
wenzelm@42241
    59
    ctxt (ProofContext.syn_of ctxt);
wenzelm@42241
    60
wenzelm@42241
    61
fun unparse_typ ctxt =
wenzelm@42241
    62
  let
wenzelm@42241
    63
    val tsig = ProofContext.tsig_of ctxt;
wenzelm@42241
    64
    val extern = {extern_class = Type.extern_class tsig, extern_type = Type.extern_type tsig};
wenzelm@42241
    65
  in Syntax.standard_unparse_typ extern ctxt (ProofContext.syn_of ctxt) end;
wenzelm@42241
    66
wenzelm@42241
    67
fun unparse_term ctxt =
wenzelm@42241
    68
  let
wenzelm@42241
    69
    val tsig = ProofContext.tsig_of ctxt;
wenzelm@42241
    70
    val syntax = ProofContext.syntax_of ctxt;
wenzelm@42241
    71
    val consts = ProofContext.consts_of ctxt;
wenzelm@42241
    72
    val extern =
wenzelm@42241
    73
     {extern_class = Type.extern_class tsig,
wenzelm@42241
    74
      extern_type = Type.extern_type tsig,
wenzelm@42241
    75
      extern_const = Consts.extern consts};
wenzelm@42241
    76
  in
wenzelm@42241
    77
    Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
wenzelm@42241
    78
      (Local_Syntax.syn_of syntax) (not (Pure_Thy.old_appl_syntax (ProofContext.theory_of ctxt)))
wenzelm@42241
    79
  end;
wenzelm@42241
    80
wenzelm@42241
    81
wenzelm@42241
    82
val _ = Syntax.install_operations
wenzelm@42241
    83
  {parse_sort = parse_sort,
wenzelm@42241
    84
   parse_typ = parse_typ,
wenzelm@42241
    85
   parse_term = parse_term dummyT,
wenzelm@42241
    86
   parse_prop = parse_term propT,
wenzelm@42241
    87
   unparse_sort = unparse_sort,
wenzelm@42241
    88
   unparse_typ = unparse_typ,
wenzelm@42241
    89
   unparse_term = unparse_term};
wenzelm@42241
    90
wenzelm@42241
    91
end;