src/Pure/Syntax/standard_syntax.ML
author wenzelm
Tue Apr 05 23:14:41 2011 +0200 (2011-04-05)
changeset 42242 39261908e12f
parent 42241 dd8029f71e1c
permissions -rw-r--r--
moved decode/parse operations to standard_syntax.ML;
tuned;
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@42242
     7
signature STANDARD_SYNTAX =
wenzelm@42242
     8
sig
wenzelm@42242
     9
  val term_sorts: term -> (indexname * sort) list
wenzelm@42242
    10
  val typ_of_term: (indexname -> sort) -> term -> typ
wenzelm@42242
    11
  val decode_term: Proof.context ->
wenzelm@42242
    12
    Position.reports * term Exn.result -> Position.reports * term Exn.result
wenzelm@42242
    13
  val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
wenzelm@42242
    14
end
wenzelm@42242
    15
wenzelm@42242
    16
structure Standard_Syntax: STANDARD_SYNTAX =
wenzelm@42241
    17
struct
wenzelm@42241
    18
wenzelm@42242
    19
(** decode parse trees **)
wenzelm@42242
    20
wenzelm@42242
    21
(* sort_of_term *)
wenzelm@42242
    22
wenzelm@42242
    23
fun sort_of_term tm =
wenzelm@42242
    24
  let
wenzelm@42242
    25
    fun err () = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
wenzelm@42242
    26
wenzelm@42242
    27
    fun class s = Lexicon.unmark_class s handle Fail _ => err ();
wenzelm@42242
    28
wenzelm@42242
    29
    fun classes (Const (s, _)) = [class s]
wenzelm@42242
    30
      | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
wenzelm@42242
    31
      | classes _ = err ();
wenzelm@42242
    32
wenzelm@42242
    33
    fun sort (Const ("_topsort", _)) = []
wenzelm@42242
    34
      | sort (Const (s, _)) = [class s]
wenzelm@42242
    35
      | sort (Const ("_sort", _) $ cs) = classes cs
wenzelm@42242
    36
      | sort _ = err ();
wenzelm@42242
    37
  in sort tm end;
wenzelm@42242
    38
wenzelm@42242
    39
wenzelm@42242
    40
(* term_sorts *)
wenzelm@42242
    41
wenzelm@42242
    42
fun term_sorts tm =
wenzelm@42242
    43
  let
wenzelm@42242
    44
    val sort_of = sort_of_term;
wenzelm@42242
    45
wenzelm@42242
    46
    fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) =
wenzelm@42242
    47
          insert (op =) ((x, ~1), sort_of cs)
wenzelm@42242
    48
      | add_env (Const ("_ofsort", _) $ (Const ("_tfree", _) $ Free (x, _)) $ cs) =
wenzelm@42242
    49
          insert (op =) ((x, ~1), sort_of cs)
wenzelm@42242
    50
      | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) =
wenzelm@42242
    51
          insert (op =) (xi, sort_of cs)
wenzelm@42242
    52
      | add_env (Const ("_ofsort", _) $ (Const ("_tvar", _) $ Var (xi, _)) $ cs) =
wenzelm@42242
    53
          insert (op =) (xi, sort_of cs)
wenzelm@42242
    54
      | add_env (Abs (_, _, t)) = add_env t
wenzelm@42242
    55
      | add_env (t1 $ t2) = add_env t1 #> add_env t2
wenzelm@42242
    56
      | add_env _ = I;
wenzelm@42242
    57
  in add_env tm [] end;
wenzelm@42242
    58
wenzelm@42242
    59
wenzelm@42242
    60
(* typ_of_term *)
wenzelm@42242
    61
wenzelm@42242
    62
fun typ_of_term get_sort tm =
wenzelm@42242
    63
  let
wenzelm@42242
    64
    fun err () = raise TERM ("typ_of_term: bad encoding of type", [tm]);
wenzelm@42242
    65
wenzelm@42242
    66
    fun typ_of (Free (x, _)) = TFree (x, get_sort (x, ~1))
wenzelm@42242
    67
      | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
wenzelm@42242
    68
      | typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t
wenzelm@42242
    69
      | typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t
wenzelm@42242
    70
      | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
wenzelm@42242
    71
      | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) =
wenzelm@42242
    72
          TFree (x, get_sort (x, ~1))
wenzelm@42242
    73
      | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
wenzelm@42242
    74
      | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) =
wenzelm@42242
    75
          TVar (xi, get_sort xi)
wenzelm@42242
    76
      | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term t)
wenzelm@42242
    77
      | typ_of t =
wenzelm@42242
    78
          let
wenzelm@42242
    79
            val (head, args) = Term.strip_comb t;
wenzelm@42242
    80
            val a =
wenzelm@42242
    81
              (case head of
wenzelm@42242
    82
                Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
wenzelm@42242
    83
              | _ => err ());
wenzelm@42242
    84
          in Type (a, map typ_of args) end;
wenzelm@42242
    85
  in typ_of tm end;
wenzelm@42242
    86
wenzelm@42242
    87
wenzelm@42242
    88
(* parsetree_to_ast *)
wenzelm@42242
    89
wenzelm@42242
    90
fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c);
wenzelm@42242
    91
wenzelm@42242
    92
fun parsetree_to_ast ctxt constrain_pos trf parsetree =
wenzelm@42242
    93
  let
wenzelm@42242
    94
    val {get_class, get_type, markup_class, markup_type} = ProofContext.type_context ctxt;
wenzelm@42242
    95
wenzelm@42242
    96
    val reports = Unsynchronized.ref ([]: Position.reports);
wenzelm@42242
    97
    fun report pos = Position.reports reports [pos];
wenzelm@42242
    98
wenzelm@42242
    99
    fun trans a args =
wenzelm@42242
   100
      (case trf a of
wenzelm@42242
   101
        NONE => Ast.mk_appl (Ast.Constant a) args
wenzelm@42242
   102
      | SOME f => f ctxt args);
wenzelm@42242
   103
wenzelm@42242
   104
    fun ast_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
wenzelm@42242
   105
          let
wenzelm@42242
   106
            val c = get_class (Lexicon.str_of_token tok);
wenzelm@42242
   107
            val _ = report (Lexicon.pos_of_token tok) markup_class c;
wenzelm@42242
   108
          in Ast.Constant (Lexicon.mark_class c) end
wenzelm@42242
   109
      | ast_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
wenzelm@42242
   110
          let
wenzelm@42242
   111
            val c = get_type (Lexicon.str_of_token tok);
wenzelm@42242
   112
            val _ = report (Lexicon.pos_of_token tok) markup_type c;
wenzelm@42242
   113
          in Ast.Constant (Lexicon.mark_type c) end
wenzelm@42242
   114
      | ast_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
wenzelm@42242
   115
          if constrain_pos then
wenzelm@42242
   116
            Ast.Appl [Ast.Constant "_constrain", ast_of pt,
wenzelm@42242
   117
              Ast.Variable (Lexicon.encode_position (Lexicon.pos_of_token tok))]
wenzelm@42242
   118
          else ast_of pt
wenzelm@42242
   119
      | ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
wenzelm@42242
   120
      | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
wenzelm@42242
   121
wenzelm@42242
   122
    val ast = Exn.interruptible_capture ast_of parsetree;
wenzelm@42242
   123
  in (! reports, ast) end;
wenzelm@42242
   124
wenzelm@42242
   125
wenzelm@42242
   126
(* ast_to_term *)
wenzelm@42242
   127
wenzelm@42242
   128
fun ast_to_term ctxt trf =
wenzelm@42242
   129
  let
wenzelm@42242
   130
    fun trans a args =
wenzelm@42242
   131
      (case trf a of
wenzelm@42242
   132
        NONE => Term.list_comb (Lexicon.const a, args)
wenzelm@42242
   133
      | SOME f => f ctxt args);
wenzelm@42242
   134
wenzelm@42242
   135
    fun term_of (Ast.Constant a) = trans a []
wenzelm@42242
   136
      | term_of (Ast.Variable x) = Lexicon.read_var x
wenzelm@42242
   137
      | term_of (Ast.Appl (Ast.Constant a :: (asts as _ :: _))) =
wenzelm@42242
   138
          trans a (map term_of asts)
wenzelm@42242
   139
      | term_of (Ast.Appl (ast :: (asts as _ :: _))) =
wenzelm@42242
   140
          Term.list_comb (term_of ast, map term_of asts)
wenzelm@42242
   141
      | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
wenzelm@42242
   142
  in term_of end;
wenzelm@42242
   143
wenzelm@42242
   144
wenzelm@42242
   145
(* decode_term -- transform parse tree into raw term *)
wenzelm@42242
   146
wenzelm@42242
   147
fun markup_bound def id =
wenzelm@42242
   148
  [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound];
wenzelm@42242
   149
wenzelm@42242
   150
fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result
wenzelm@42242
   151
  | decode_term ctxt (reports0, Exn.Result tm) =
wenzelm@42242
   152
      let
wenzelm@42242
   153
        val {get_const, get_free, markup_const, markup_free, markup_var} =
wenzelm@42242
   154
          ProofContext.term_context ctxt;
wenzelm@42242
   155
        val decodeT = typ_of_term (ProofContext.get_sort ctxt (term_sorts tm));
wenzelm@42242
   156
wenzelm@42242
   157
        val reports = Unsynchronized.ref reports0;
wenzelm@42242
   158
        fun report ps = Position.reports reports ps;
wenzelm@42242
   159
wenzelm@42242
   160
        fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
wenzelm@42242
   161
              (case Syntax.decode_position_term typ of
wenzelm@42242
   162
                SOME p => decode (p :: ps) qs bs t
wenzelm@42242
   163
              | NONE => Type.constraint (decodeT typ) (decode ps qs bs t))
wenzelm@42242
   164
          | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
wenzelm@42242
   165
              (case Syntax.decode_position_term typ of
wenzelm@42242
   166
                SOME q => decode ps (q :: qs) bs t
wenzelm@42242
   167
              | NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t))
wenzelm@42242
   168
          | decode _ qs bs (Abs (x, T, t)) =
wenzelm@42242
   169
              let
wenzelm@42242
   170
                val id = serial_string ();
wenzelm@42242
   171
                val _ = report qs (markup_bound true) id;
wenzelm@42242
   172
              in Abs (x, T, decode [] [] (id :: bs) t) end
wenzelm@42242
   173
          | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
wenzelm@42242
   174
          | decode ps _ _ (Const (a, T)) =
wenzelm@42242
   175
              (case try Lexicon.unmark_fixed a of
wenzelm@42242
   176
                SOME x => (report ps markup_free x; Free (x, T))
wenzelm@42242
   177
              | NONE =>
wenzelm@42242
   178
                  let
wenzelm@42242
   179
                    val c =
wenzelm@42242
   180
                      (case try Lexicon.unmark_const a of
wenzelm@42242
   181
                        SOME c => c
wenzelm@42242
   182
                      | NONE => snd (get_const a));
wenzelm@42242
   183
                    val _ = report ps markup_const c;
wenzelm@42242
   184
                  in Const (c, T) end)
wenzelm@42242
   185
          | decode ps _ _ (Free (a, T)) =
wenzelm@42242
   186
              (case (get_free a, get_const a) of
wenzelm@42242
   187
                (SOME x, _) => (report ps markup_free x; Free (x, T))
wenzelm@42242
   188
              | (_, (true, c)) => (report ps markup_const c; Const (c, T))
wenzelm@42242
   189
              | (_, (false, c)) =>
wenzelm@42242
   190
                  if Long_Name.is_qualified c
wenzelm@42242
   191
                  then (report ps markup_const c; Const (c, T))
wenzelm@42242
   192
                  else (report ps markup_free c; Free (c, T)))
wenzelm@42242
   193
          | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
wenzelm@42242
   194
          | decode ps _ bs (t as Bound i) =
wenzelm@42242
   195
              (case try (nth bs) i of
wenzelm@42242
   196
                SOME id => (report ps (markup_bound false) id; t)
wenzelm@42242
   197
              | NONE => t);
wenzelm@42242
   198
wenzelm@42242
   199
        val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
wenzelm@42242
   200
      in (! reports, tm') end;
wenzelm@42242
   201
wenzelm@42242
   202
wenzelm@42242
   203
wenzelm@42242
   204
(** parse **)
wenzelm@42242
   205
wenzelm@42242
   206
(* results *)
wenzelm@42242
   207
wenzelm@42242
   208
fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
wenzelm@42242
   209
wenzelm@42242
   210
fun proper_results results = map_filter (fn (y, Exn.Result x) => SOME (y, x) | _ => NONE) results;
wenzelm@42242
   211
fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
wenzelm@42242
   212
wenzelm@42242
   213
fun report ctxt = List.app (fn (pos, m) => Context_Position.report ctxt pos m);
wenzelm@42242
   214
wenzelm@42242
   215
fun report_result ctxt pos results =
wenzelm@42242
   216
  (case (proper_results results, failed_results results) of
wenzelm@42242
   217
    ([], (reports, exn) :: _) => (report ctxt reports; reraise exn)
wenzelm@42242
   218
  | ([(reports, x)], _) => (report ctxt reports; x)
wenzelm@42242
   219
  | _ => error (ambiguity_msg pos));
wenzelm@42242
   220
wenzelm@42242
   221
wenzelm@42242
   222
(* parse_asts *)
wenzelm@42242
   223
wenzelm@42242
   224
fun parse_asts ctxt raw root (syms, pos) =
wenzelm@42242
   225
  let
wenzelm@42242
   226
    val {lexicon, gram, parse_ast_trtab, ...} = Syntax.rep_syntax (ProofContext.syn_of ctxt);
wenzelm@42242
   227
wenzelm@42242
   228
    val toks = Lexicon.tokenize lexicon raw syms;
wenzelm@42242
   229
    val _ = List.app (Lexicon.report_token ctxt) toks;
wenzelm@42242
   230
wenzelm@42242
   231
    val pts = Parser.parse ctxt gram root (filter Lexicon.is_proper toks)
wenzelm@42242
   232
      handle ERROR msg =>
wenzelm@42242
   233
        error (msg ^
wenzelm@42242
   234
          implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
wenzelm@42242
   235
    val len = length pts;
wenzelm@42242
   236
wenzelm@42242
   237
    val limit = Config.get ctxt Syntax.ambiguity_limit;
wenzelm@42242
   238
    val _ =
wenzelm@42242
   239
      if len <= Config.get ctxt Syntax.ambiguity_level then ()
wenzelm@42242
   240
      else if not (Config.get ctxt Syntax.ambiguity_enabled) then error (ambiguity_msg pos)
wenzelm@42242
   241
      else
wenzelm@42242
   242
        (Context_Position.if_visible ctxt warning (cat_lines
wenzelm@42242
   243
          (("Ambiguous input" ^ Position.str_of pos ^
wenzelm@42242
   244
            "\nproduces " ^ string_of_int len ^ " parse trees" ^
wenzelm@42242
   245
            (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
wenzelm@42242
   246
            map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))));
wenzelm@42242
   247
wenzelm@42242
   248
    val constrain_pos = not raw andalso Config.get ctxt Syntax.positions;
wenzelm@42242
   249
    val parsetree_to_ast = parsetree_to_ast ctxt constrain_pos (lookup_tr parse_ast_trtab);
wenzelm@42242
   250
  in map parsetree_to_ast pts end;
wenzelm@42242
   251
wenzelm@42242
   252
wenzelm@42242
   253
(* read_raw *)
wenzelm@42242
   254
wenzelm@42242
   255
fun read_raw ctxt root input =
wenzelm@42242
   256
  let
wenzelm@42242
   257
    val {parse_ruletab, parse_trtab, ...} = Syntax.rep_syntax (ProofContext.syn_of ctxt);
wenzelm@42242
   258
    val norm = Ast.normalize ctxt (Symtab.lookup_list parse_ruletab);
wenzelm@42242
   259
    val ast_to_term = ast_to_term ctxt (lookup_tr parse_trtab);
wenzelm@42242
   260
  in
wenzelm@42242
   261
    parse_asts ctxt false root input
wenzelm@42242
   262
    |> (map o apsnd o Exn.maps_result) (norm #> Exn.interruptible_capture ast_to_term)
wenzelm@42242
   263
  end;
wenzelm@42242
   264
wenzelm@42242
   265
wenzelm@42242
   266
(* read sorts *)
wenzelm@42242
   267
wenzelm@42242
   268
fun standard_parse_sort ctxt (syms, pos) =
wenzelm@42242
   269
  read_raw ctxt "sort" (syms, pos)
wenzelm@42242
   270
  |> report_result ctxt pos
wenzelm@42242
   271
  |> sort_of_term;
wenzelm@42242
   272
wenzelm@42242
   273
wenzelm@42242
   274
(* read types *)
wenzelm@42242
   275
wenzelm@42242
   276
fun standard_parse_typ ctxt (syms, pos) =
wenzelm@42242
   277
  read_raw ctxt "type" (syms, pos)
wenzelm@42242
   278
  |> report_result ctxt pos
wenzelm@42242
   279
  |> (fn t => typ_of_term (ProofContext.get_sort ctxt (term_sorts t)) t);
wenzelm@42242
   280
wenzelm@42242
   281
wenzelm@42242
   282
(* read terms -- brute-force disambiguation via type-inference *)
wenzelm@42242
   283
wenzelm@42242
   284
fun standard_parse_term check ctxt root (syms, pos) =
wenzelm@42242
   285
  let
wenzelm@42242
   286
    val results = read_raw ctxt root (syms, pos) |> map (decode_term ctxt);
wenzelm@42242
   287
wenzelm@42242
   288
    val level = Config.get ctxt Syntax.ambiguity_level;
wenzelm@42242
   289
    val limit = Config.get ctxt Syntax.ambiguity_limit;
wenzelm@42242
   290
wenzelm@42242
   291
    val ambiguity = length (proper_results results);
wenzelm@42242
   292
wenzelm@42242
   293
    fun ambig_msg () =
wenzelm@42242
   294
      if ambiguity > 1 andalso ambiguity <= level then
wenzelm@42242
   295
        "Got more than one parse tree.\n\
wenzelm@42242
   296
        \Retry with smaller syntax_ambiguity_level for more information."
wenzelm@42242
   297
      else "";
wenzelm@42242
   298
wenzelm@42242
   299
    val results' =
wenzelm@42242
   300
      if ambiguity > 1 then
wenzelm@42242
   301
        (Par_List.map_name "Syntax.disambig" o apsnd o Exn.maps_result) check results
wenzelm@42242
   302
      else results;
wenzelm@42242
   303
    val reports' = fst (hd results');
wenzelm@42242
   304
wenzelm@42242
   305
    val errs = map snd (failed_results results');
wenzelm@42242
   306
    val checked = map snd (proper_results results');
wenzelm@42242
   307
    val len = length checked;
wenzelm@42242
   308
wenzelm@42242
   309
    val show_term = Syntax.string_of_term (Config.put Syntax.show_brackets true ctxt);
wenzelm@42242
   310
  in
wenzelm@42242
   311
    if len = 0 then
wenzelm@42242
   312
      report_result ctxt pos
wenzelm@42242
   313
        [(reports', Exn.Exn (Exn.EXCEPTIONS (ERROR (ambig_msg ()) :: errs)))]
wenzelm@42242
   314
    else if len = 1 then
wenzelm@42242
   315
      (if ambiguity > level then
wenzelm@42242
   316
        Context_Position.if_visible ctxt warning
wenzelm@42242
   317
          "Fortunately, only one parse tree is type correct.\n\
wenzelm@42242
   318
          \You may still want to disambiguate your grammar or your input."
wenzelm@42242
   319
      else (); report_result ctxt pos results')
wenzelm@42242
   320
    else
wenzelm@42242
   321
      report_result ctxt pos
wenzelm@42242
   322
        [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg () ::
wenzelm@42242
   323
          (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
wenzelm@42242
   324
            (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
wenzelm@42242
   325
            map show_term (take limit checked))))))]
wenzelm@42242
   326
  end;
wenzelm@42242
   327
wenzelm@42242
   328
wenzelm@42242
   329
(* standard operations *)
wenzelm@42242
   330
wenzelm@42241
   331
fun parse_failed ctxt pos msg kind =
wenzelm@42241
   332
  cat_error msg ("Failed to parse " ^ kind ^
wenzelm@42241
   333
    Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
wenzelm@42241
   334
wenzelm@42241
   335
fun parse_sort ctxt text =
wenzelm@42241
   336
  let
wenzelm@42241
   337
    val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
wenzelm@42242
   338
    val S = standard_parse_sort ctxt (syms, pos)
wenzelm@42242
   339
      handle ERROR msg => parse_failed ctxt pos msg "sort";
wenzelm@42241
   340
  in Type.minimize_sort (ProofContext.tsig_of ctxt) S end;
wenzelm@42241
   341
wenzelm@42241
   342
fun parse_typ ctxt text =
wenzelm@42241
   343
  let
wenzelm@42241
   344
    val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
wenzelm@42242
   345
    val T = standard_parse_typ ctxt (syms, pos)
wenzelm@42242
   346
      handle ERROR msg => parse_failed ctxt pos msg "type";
wenzelm@42241
   347
  in T end;
wenzelm@42241
   348
wenzelm@42241
   349
fun parse_term T ctxt text =
wenzelm@42241
   350
  let
wenzelm@42241
   351
    val (T', _) = Type_Infer.paramify_dummies T 0;
wenzelm@42241
   352
    val (markup, kind) =
wenzelm@42241
   353
      if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
wenzelm@42241
   354
    val (syms, pos) = Syntax.parse_token ctxt markup text;
wenzelm@42241
   355
wenzelm@42241
   356
    val default_root = Config.get ctxt Syntax.default_root;
wenzelm@42241
   357
    val root =
wenzelm@42241
   358
      (case T' of
wenzelm@42241
   359
        Type (c, _) =>
wenzelm@42241
   360
          if c <> "prop" andalso Type.is_logtype (ProofContext.tsig_of ctxt) c
wenzelm@42241
   361
          then default_root else c
wenzelm@42241
   362
      | _ => default_root);
wenzelm@42241
   363
wenzelm@42241
   364
    fun check t = (Syntax.check_term ctxt (Type.constraint T' t); Exn.Result t)
wenzelm@42241
   365
      handle exn as ERROR _ => Exn.Exn exn;
wenzelm@42242
   366
    val t = standard_parse_term check ctxt root (syms, pos)
wenzelm@42241
   367
      handle ERROR msg => parse_failed ctxt pos msg kind;
wenzelm@42241
   368
  in t end;
wenzelm@42241
   369
wenzelm@42241
   370
wenzelm@42242
   371
(* parse_ast_pattern *)
wenzelm@42242
   372
wenzelm@42242
   373
fun parse_ast_pattern ctxt (root, str) =
wenzelm@42242
   374
  let
wenzelm@42242
   375
    val syn = ProofContext.syn_of ctxt;
wenzelm@42242
   376
wenzelm@42242
   377
    fun constify (ast as Ast.Constant _) = ast
wenzelm@42242
   378
      | constify (ast as Ast.Variable x) =
wenzelm@42242
   379
          if Syntax.is_const syn x orelse Long_Name.is_qualified x then Ast.Constant x
wenzelm@42242
   380
          else ast
wenzelm@42242
   381
      | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
wenzelm@42242
   382
wenzelm@42242
   383
    val (syms, pos) = Syntax.read_token str;
wenzelm@42242
   384
  in
wenzelm@42242
   385
    parse_asts ctxt true root (syms, pos)
wenzelm@42242
   386
    |> report_result ctxt pos
wenzelm@42242
   387
    |> constify
wenzelm@42242
   388
  end;
wenzelm@42242
   389
wenzelm@42242
   390
wenzelm@42242
   391
wenzelm@42242
   392
(** unparse **)
wenzelm@42242
   393
wenzelm@42241
   394
fun unparse_sort ctxt =
wenzelm@42241
   395
  Syntax.standard_unparse_sort {extern_class = Type.extern_class (ProofContext.tsig_of ctxt)}
wenzelm@42241
   396
    ctxt (ProofContext.syn_of ctxt);
wenzelm@42241
   397
wenzelm@42241
   398
fun unparse_typ ctxt =
wenzelm@42241
   399
  let
wenzelm@42241
   400
    val tsig = ProofContext.tsig_of ctxt;
wenzelm@42241
   401
    val extern = {extern_class = Type.extern_class tsig, extern_type = Type.extern_type tsig};
wenzelm@42241
   402
  in Syntax.standard_unparse_typ extern ctxt (ProofContext.syn_of ctxt) end;
wenzelm@42241
   403
wenzelm@42241
   404
fun unparse_term ctxt =
wenzelm@42241
   405
  let
wenzelm@42241
   406
    val tsig = ProofContext.tsig_of ctxt;
wenzelm@42241
   407
    val syntax = ProofContext.syntax_of ctxt;
wenzelm@42241
   408
    val consts = ProofContext.consts_of ctxt;
wenzelm@42241
   409
    val extern =
wenzelm@42241
   410
     {extern_class = Type.extern_class tsig,
wenzelm@42241
   411
      extern_type = Type.extern_type tsig,
wenzelm@42241
   412
      extern_const = Consts.extern consts};
wenzelm@42241
   413
  in
wenzelm@42241
   414
    Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
wenzelm@42241
   415
      (Local_Syntax.syn_of syntax) (not (Pure_Thy.old_appl_syntax (ProofContext.theory_of ctxt)))
wenzelm@42241
   416
  end;
wenzelm@42241
   417
wenzelm@42241
   418
wenzelm@42242
   419
(** install operations **)
wenzelm@42242
   420
wenzelm@42241
   421
val _ = Syntax.install_operations
wenzelm@42241
   422
  {parse_sort = parse_sort,
wenzelm@42241
   423
   parse_typ = parse_typ,
wenzelm@42241
   424
   parse_term = parse_term dummyT,
wenzelm@42241
   425
   parse_prop = parse_term propT,
wenzelm@42241
   426
   unparse_sort = unparse_sort,
wenzelm@42241
   427
   unparse_typ = unparse_typ,
wenzelm@42241
   428
   unparse_term = unparse_term};
wenzelm@42241
   429
wenzelm@42241
   430
end;