src/Pure/Syntax/syntax_phases.ML
author wenzelm
Wed Apr 06 13:33:46 2011 +0200 (2011-04-06)
changeset 42247 12fe41a92cd5
parent 42245 29e3967550d5
child 42248 04bffad68aa4
permissions -rw-r--r--
typed_print_translation: discontinued show_sorts argument;
wenzelm@42243
     1
(*  Title:      Pure/Syntax/syntax_phases.ML
wenzelm@42241
     2
    Author:     Makarius
wenzelm@42241
     3
wenzelm@42243
     4
Main phases of inner syntax processing, with standard implementations
wenzelm@42243
     5
of parse/unparse operations.
wenzelm@42241
     6
*)
wenzelm@42241
     7
wenzelm@42243
     8
signature SYNTAX_PHASES =
wenzelm@42242
     9
sig
wenzelm@42242
    10
  val term_sorts: term -> (indexname * sort) list
wenzelm@42242
    11
  val typ_of_term: (indexname -> sort) -> term -> typ
wenzelm@42242
    12
  val decode_term: Proof.context ->
wenzelm@42242
    13
    Position.reports * term Exn.result -> Position.reports * term Exn.result
wenzelm@42242
    14
  val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
wenzelm@42247
    15
  val term_of_typ: Proof.context -> typ -> term
wenzelm@42242
    16
end
wenzelm@42242
    17
wenzelm@42243
    18
structure Syntax_Phases: SYNTAX_PHASES =
wenzelm@42241
    19
struct
wenzelm@42241
    20
wenzelm@42242
    21
(** decode parse trees **)
wenzelm@42242
    22
wenzelm@42242
    23
(* sort_of_term *)
wenzelm@42242
    24
wenzelm@42242
    25
fun sort_of_term tm =
wenzelm@42242
    26
  let
wenzelm@42242
    27
    fun err () = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
wenzelm@42242
    28
wenzelm@42242
    29
    fun class s = Lexicon.unmark_class s handle Fail _ => err ();
wenzelm@42242
    30
wenzelm@42242
    31
    fun classes (Const (s, _)) = [class s]
wenzelm@42242
    32
      | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
wenzelm@42242
    33
      | classes _ = err ();
wenzelm@42242
    34
wenzelm@42242
    35
    fun sort (Const ("_topsort", _)) = []
wenzelm@42242
    36
      | sort (Const (s, _)) = [class s]
wenzelm@42242
    37
      | sort (Const ("_sort", _) $ cs) = classes cs
wenzelm@42242
    38
      | sort _ = err ();
wenzelm@42242
    39
  in sort tm end;
wenzelm@42242
    40
wenzelm@42242
    41
wenzelm@42242
    42
(* term_sorts *)
wenzelm@42242
    43
wenzelm@42242
    44
fun term_sorts tm =
wenzelm@42242
    45
  let
wenzelm@42242
    46
    val sort_of = sort_of_term;
wenzelm@42242
    47
wenzelm@42242
    48
    fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) =
wenzelm@42242
    49
          insert (op =) ((x, ~1), sort_of cs)
wenzelm@42242
    50
      | add_env (Const ("_ofsort", _) $ (Const ("_tfree", _) $ Free (x, _)) $ cs) =
wenzelm@42242
    51
          insert (op =) ((x, ~1), sort_of cs)
wenzelm@42242
    52
      | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) =
wenzelm@42242
    53
          insert (op =) (xi, sort_of cs)
wenzelm@42242
    54
      | add_env (Const ("_ofsort", _) $ (Const ("_tvar", _) $ Var (xi, _)) $ cs) =
wenzelm@42242
    55
          insert (op =) (xi, sort_of cs)
wenzelm@42242
    56
      | add_env (Abs (_, _, t)) = add_env t
wenzelm@42242
    57
      | add_env (t1 $ t2) = add_env t1 #> add_env t2
wenzelm@42242
    58
      | add_env _ = I;
wenzelm@42242
    59
  in add_env tm [] end;
wenzelm@42242
    60
wenzelm@42242
    61
wenzelm@42242
    62
(* typ_of_term *)
wenzelm@42242
    63
wenzelm@42242
    64
fun typ_of_term get_sort tm =
wenzelm@42242
    65
  let
wenzelm@42242
    66
    fun err () = raise TERM ("typ_of_term: bad encoding of type", [tm]);
wenzelm@42242
    67
wenzelm@42242
    68
    fun typ_of (Free (x, _)) = TFree (x, get_sort (x, ~1))
wenzelm@42242
    69
      | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
wenzelm@42242
    70
      | typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t
wenzelm@42242
    71
      | typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t
wenzelm@42242
    72
      | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
wenzelm@42242
    73
      | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) =
wenzelm@42242
    74
          TFree (x, get_sort (x, ~1))
wenzelm@42242
    75
      | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
wenzelm@42242
    76
      | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) =
wenzelm@42242
    77
          TVar (xi, get_sort xi)
wenzelm@42242
    78
      | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term t)
wenzelm@42242
    79
      | typ_of t =
wenzelm@42242
    80
          let
wenzelm@42242
    81
            val (head, args) = Term.strip_comb t;
wenzelm@42242
    82
            val a =
wenzelm@42242
    83
              (case head of
wenzelm@42242
    84
                Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
wenzelm@42242
    85
              | _ => err ());
wenzelm@42242
    86
          in Type (a, map typ_of args) end;
wenzelm@42242
    87
  in typ_of tm end;
wenzelm@42242
    88
wenzelm@42242
    89
wenzelm@42242
    90
(* parsetree_to_ast *)
wenzelm@42242
    91
wenzelm@42242
    92
fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c);
wenzelm@42242
    93
wenzelm@42242
    94
fun parsetree_to_ast ctxt constrain_pos trf parsetree =
wenzelm@42242
    95
  let
wenzelm@42242
    96
    val {get_class, get_type, markup_class, markup_type} = ProofContext.type_context ctxt;
wenzelm@42242
    97
wenzelm@42242
    98
    val reports = Unsynchronized.ref ([]: Position.reports);
wenzelm@42242
    99
    fun report pos = Position.reports reports [pos];
wenzelm@42242
   100
wenzelm@42242
   101
    fun trans a args =
wenzelm@42242
   102
      (case trf a of
wenzelm@42242
   103
        NONE => Ast.mk_appl (Ast.Constant a) args
wenzelm@42242
   104
      | SOME f => f ctxt args);
wenzelm@42242
   105
wenzelm@42242
   106
    fun ast_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
wenzelm@42242
   107
          let
wenzelm@42242
   108
            val c = get_class (Lexicon.str_of_token tok);
wenzelm@42242
   109
            val _ = report (Lexicon.pos_of_token tok) markup_class c;
wenzelm@42242
   110
          in Ast.Constant (Lexicon.mark_class c) end
wenzelm@42242
   111
      | ast_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
wenzelm@42242
   112
          let
wenzelm@42242
   113
            val c = get_type (Lexicon.str_of_token tok);
wenzelm@42242
   114
            val _ = report (Lexicon.pos_of_token tok) markup_type c;
wenzelm@42242
   115
          in Ast.Constant (Lexicon.mark_type c) end
wenzelm@42242
   116
      | ast_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
wenzelm@42242
   117
          if constrain_pos then
wenzelm@42242
   118
            Ast.Appl [Ast.Constant "_constrain", ast_of pt,
wenzelm@42242
   119
              Ast.Variable (Lexicon.encode_position (Lexicon.pos_of_token tok))]
wenzelm@42242
   120
          else ast_of pt
wenzelm@42242
   121
      | ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
wenzelm@42242
   122
      | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
wenzelm@42242
   123
wenzelm@42242
   124
    val ast = Exn.interruptible_capture ast_of parsetree;
wenzelm@42242
   125
  in (! reports, ast) end;
wenzelm@42242
   126
wenzelm@42242
   127
wenzelm@42242
   128
(* ast_to_term *)
wenzelm@42242
   129
wenzelm@42242
   130
fun ast_to_term ctxt trf =
wenzelm@42242
   131
  let
wenzelm@42242
   132
    fun trans a args =
wenzelm@42242
   133
      (case trf a of
wenzelm@42242
   134
        NONE => Term.list_comb (Lexicon.const a, args)
wenzelm@42242
   135
      | SOME f => f ctxt args);
wenzelm@42242
   136
wenzelm@42242
   137
    fun term_of (Ast.Constant a) = trans a []
wenzelm@42242
   138
      | term_of (Ast.Variable x) = Lexicon.read_var x
wenzelm@42242
   139
      | term_of (Ast.Appl (Ast.Constant a :: (asts as _ :: _))) =
wenzelm@42242
   140
          trans a (map term_of asts)
wenzelm@42242
   141
      | term_of (Ast.Appl (ast :: (asts as _ :: _))) =
wenzelm@42242
   142
          Term.list_comb (term_of ast, map term_of asts)
wenzelm@42242
   143
      | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
wenzelm@42242
   144
  in term_of end;
wenzelm@42242
   145
wenzelm@42242
   146
wenzelm@42242
   147
(* decode_term -- transform parse tree into raw term *)
wenzelm@42242
   148
wenzelm@42242
   149
fun markup_bound def id =
wenzelm@42242
   150
  [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound];
wenzelm@42242
   151
wenzelm@42242
   152
fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result
wenzelm@42242
   153
  | decode_term ctxt (reports0, Exn.Result tm) =
wenzelm@42242
   154
      let
wenzelm@42242
   155
        val {get_const, get_free, markup_const, markup_free, markup_var} =
wenzelm@42242
   156
          ProofContext.term_context ctxt;
wenzelm@42242
   157
        val decodeT = typ_of_term (ProofContext.get_sort ctxt (term_sorts tm));
wenzelm@42242
   158
wenzelm@42242
   159
        val reports = Unsynchronized.ref reports0;
wenzelm@42242
   160
        fun report ps = Position.reports reports ps;
wenzelm@42242
   161
wenzelm@42242
   162
        fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
wenzelm@42242
   163
              (case Syntax.decode_position_term typ of
wenzelm@42242
   164
                SOME p => decode (p :: ps) qs bs t
wenzelm@42242
   165
              | NONE => Type.constraint (decodeT typ) (decode ps qs bs t))
wenzelm@42242
   166
          | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
wenzelm@42242
   167
              (case Syntax.decode_position_term typ of
wenzelm@42242
   168
                SOME q => decode ps (q :: qs) bs t
wenzelm@42242
   169
              | NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t))
wenzelm@42242
   170
          | decode _ qs bs (Abs (x, T, t)) =
wenzelm@42242
   171
              let
wenzelm@42242
   172
                val id = serial_string ();
wenzelm@42242
   173
                val _ = report qs (markup_bound true) id;
wenzelm@42242
   174
              in Abs (x, T, decode [] [] (id :: bs) t) end
wenzelm@42242
   175
          | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
wenzelm@42242
   176
          | decode ps _ _ (Const (a, T)) =
wenzelm@42242
   177
              (case try Lexicon.unmark_fixed a of
wenzelm@42242
   178
                SOME x => (report ps markup_free x; Free (x, T))
wenzelm@42242
   179
              | NONE =>
wenzelm@42242
   180
                  let
wenzelm@42242
   181
                    val c =
wenzelm@42242
   182
                      (case try Lexicon.unmark_const a of
wenzelm@42242
   183
                        SOME c => c
wenzelm@42242
   184
                      | NONE => snd (get_const a));
wenzelm@42242
   185
                    val _ = report ps markup_const c;
wenzelm@42242
   186
                  in Const (c, T) end)
wenzelm@42242
   187
          | decode ps _ _ (Free (a, T)) =
wenzelm@42242
   188
              (case (get_free a, get_const a) of
wenzelm@42242
   189
                (SOME x, _) => (report ps markup_free x; Free (x, T))
wenzelm@42242
   190
              | (_, (true, c)) => (report ps markup_const c; Const (c, T))
wenzelm@42242
   191
              | (_, (false, c)) =>
wenzelm@42242
   192
                  if Long_Name.is_qualified c
wenzelm@42242
   193
                  then (report ps markup_const c; Const (c, T))
wenzelm@42242
   194
                  else (report ps markup_free c; Free (c, T)))
wenzelm@42242
   195
          | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
wenzelm@42242
   196
          | decode ps _ bs (t as Bound i) =
wenzelm@42242
   197
              (case try (nth bs) i of
wenzelm@42242
   198
                SOME id => (report ps (markup_bound false) id; t)
wenzelm@42242
   199
              | NONE => t);
wenzelm@42242
   200
wenzelm@42242
   201
        val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
wenzelm@42242
   202
      in (! reports, tm') end;
wenzelm@42242
   203
wenzelm@42242
   204
wenzelm@42242
   205
wenzelm@42242
   206
(** parse **)
wenzelm@42242
   207
wenzelm@42242
   208
(* results *)
wenzelm@42242
   209
wenzelm@42242
   210
fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
wenzelm@42242
   211
wenzelm@42242
   212
fun proper_results results = map_filter (fn (y, Exn.Result x) => SOME (y, x) | _ => NONE) results;
wenzelm@42242
   213
fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
wenzelm@42242
   214
wenzelm@42242
   215
fun report ctxt = List.app (fn (pos, m) => Context_Position.report ctxt pos m);
wenzelm@42242
   216
wenzelm@42242
   217
fun report_result ctxt pos results =
wenzelm@42242
   218
  (case (proper_results results, failed_results results) of
wenzelm@42242
   219
    ([], (reports, exn) :: _) => (report ctxt reports; reraise exn)
wenzelm@42242
   220
  | ([(reports, x)], _) => (report ctxt reports; x)
wenzelm@42242
   221
  | _ => error (ambiguity_msg pos));
wenzelm@42242
   222
wenzelm@42242
   223
wenzelm@42242
   224
(* parse_asts *)
wenzelm@42242
   225
wenzelm@42242
   226
fun parse_asts ctxt raw root (syms, pos) =
wenzelm@42242
   227
  let
wenzelm@42242
   228
    val {lexicon, gram, parse_ast_trtab, ...} = Syntax.rep_syntax (ProofContext.syn_of ctxt);
wenzelm@42242
   229
wenzelm@42242
   230
    val toks = Lexicon.tokenize lexicon raw syms;
wenzelm@42242
   231
    val _ = List.app (Lexicon.report_token ctxt) toks;
wenzelm@42242
   232
wenzelm@42242
   233
    val pts = Parser.parse ctxt gram root (filter Lexicon.is_proper toks)
wenzelm@42242
   234
      handle ERROR msg =>
wenzelm@42242
   235
        error (msg ^
wenzelm@42242
   236
          implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
wenzelm@42242
   237
    val len = length pts;
wenzelm@42242
   238
wenzelm@42242
   239
    val limit = Config.get ctxt Syntax.ambiguity_limit;
wenzelm@42242
   240
    val _ =
wenzelm@42242
   241
      if len <= Config.get ctxt Syntax.ambiguity_level then ()
wenzelm@42242
   242
      else if not (Config.get ctxt Syntax.ambiguity_enabled) then error (ambiguity_msg pos)
wenzelm@42242
   243
      else
wenzelm@42242
   244
        (Context_Position.if_visible ctxt warning (cat_lines
wenzelm@42242
   245
          (("Ambiguous input" ^ Position.str_of pos ^
wenzelm@42242
   246
            "\nproduces " ^ string_of_int len ^ " parse trees" ^
wenzelm@42242
   247
            (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
wenzelm@42242
   248
            map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))));
wenzelm@42242
   249
wenzelm@42242
   250
    val constrain_pos = not raw andalso Config.get ctxt Syntax.positions;
wenzelm@42242
   251
    val parsetree_to_ast = parsetree_to_ast ctxt constrain_pos (lookup_tr parse_ast_trtab);
wenzelm@42242
   252
  in map parsetree_to_ast pts end;
wenzelm@42242
   253
wenzelm@42242
   254
wenzelm@42242
   255
(* read_raw *)
wenzelm@42242
   256
wenzelm@42242
   257
fun read_raw ctxt root input =
wenzelm@42242
   258
  let
wenzelm@42242
   259
    val {parse_ruletab, parse_trtab, ...} = Syntax.rep_syntax (ProofContext.syn_of ctxt);
wenzelm@42242
   260
    val norm = Ast.normalize ctxt (Symtab.lookup_list parse_ruletab);
wenzelm@42242
   261
    val ast_to_term = ast_to_term ctxt (lookup_tr parse_trtab);
wenzelm@42242
   262
  in
wenzelm@42242
   263
    parse_asts ctxt false root input
wenzelm@42242
   264
    |> (map o apsnd o Exn.maps_result) (norm #> Exn.interruptible_capture ast_to_term)
wenzelm@42242
   265
  end;
wenzelm@42242
   266
wenzelm@42242
   267
wenzelm@42242
   268
(* read sorts *)
wenzelm@42242
   269
wenzelm@42242
   270
fun standard_parse_sort ctxt (syms, pos) =
wenzelm@42242
   271
  read_raw ctxt "sort" (syms, pos)
wenzelm@42242
   272
  |> report_result ctxt pos
wenzelm@42242
   273
  |> sort_of_term;
wenzelm@42242
   274
wenzelm@42242
   275
wenzelm@42242
   276
(* read types *)
wenzelm@42242
   277
wenzelm@42242
   278
fun standard_parse_typ ctxt (syms, pos) =
wenzelm@42242
   279
  read_raw ctxt "type" (syms, pos)
wenzelm@42242
   280
  |> report_result ctxt pos
wenzelm@42242
   281
  |> (fn t => typ_of_term (ProofContext.get_sort ctxt (term_sorts t)) t);
wenzelm@42242
   282
wenzelm@42242
   283
wenzelm@42242
   284
(* read terms -- brute-force disambiguation via type-inference *)
wenzelm@42242
   285
wenzelm@42242
   286
fun standard_parse_term check ctxt root (syms, pos) =
wenzelm@42242
   287
  let
wenzelm@42242
   288
    val results = read_raw ctxt root (syms, pos) |> map (decode_term ctxt);
wenzelm@42242
   289
wenzelm@42242
   290
    val level = Config.get ctxt Syntax.ambiguity_level;
wenzelm@42242
   291
    val limit = Config.get ctxt Syntax.ambiguity_limit;
wenzelm@42242
   292
wenzelm@42242
   293
    val ambiguity = length (proper_results results);
wenzelm@42242
   294
wenzelm@42242
   295
    fun ambig_msg () =
wenzelm@42242
   296
      if ambiguity > 1 andalso ambiguity <= level then
wenzelm@42242
   297
        "Got more than one parse tree.\n\
wenzelm@42242
   298
        \Retry with smaller syntax_ambiguity_level for more information."
wenzelm@42242
   299
      else "";
wenzelm@42242
   300
wenzelm@42242
   301
    val results' =
wenzelm@42242
   302
      if ambiguity > 1 then
wenzelm@42242
   303
        (Par_List.map_name "Syntax.disambig" o apsnd o Exn.maps_result) check results
wenzelm@42242
   304
      else results;
wenzelm@42242
   305
    val reports' = fst (hd results');
wenzelm@42242
   306
wenzelm@42242
   307
    val errs = map snd (failed_results results');
wenzelm@42242
   308
    val checked = map snd (proper_results results');
wenzelm@42242
   309
    val len = length checked;
wenzelm@42242
   310
wenzelm@42242
   311
    val show_term = Syntax.string_of_term (Config.put Syntax.show_brackets true ctxt);
wenzelm@42242
   312
  in
wenzelm@42242
   313
    if len = 0 then
wenzelm@42242
   314
      report_result ctxt pos
wenzelm@42242
   315
        [(reports', Exn.Exn (Exn.EXCEPTIONS (ERROR (ambig_msg ()) :: errs)))]
wenzelm@42242
   316
    else if len = 1 then
wenzelm@42242
   317
      (if ambiguity > level then
wenzelm@42242
   318
        Context_Position.if_visible ctxt warning
wenzelm@42242
   319
          "Fortunately, only one parse tree is type correct.\n\
wenzelm@42242
   320
          \You may still want to disambiguate your grammar or your input."
wenzelm@42242
   321
      else (); report_result ctxt pos results')
wenzelm@42242
   322
    else
wenzelm@42242
   323
      report_result ctxt pos
wenzelm@42242
   324
        [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg () ::
wenzelm@42242
   325
          (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
wenzelm@42242
   326
            (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
wenzelm@42242
   327
            map show_term (take limit checked))))))]
wenzelm@42242
   328
  end;
wenzelm@42242
   329
wenzelm@42242
   330
wenzelm@42242
   331
(* standard operations *)
wenzelm@42242
   332
wenzelm@42241
   333
fun parse_failed ctxt pos msg kind =
wenzelm@42241
   334
  cat_error msg ("Failed to parse " ^ kind ^
wenzelm@42241
   335
    Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
wenzelm@42241
   336
wenzelm@42241
   337
fun parse_sort ctxt text =
wenzelm@42241
   338
  let
wenzelm@42241
   339
    val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
wenzelm@42242
   340
    val S = standard_parse_sort ctxt (syms, pos)
wenzelm@42242
   341
      handle ERROR msg => parse_failed ctxt pos msg "sort";
wenzelm@42241
   342
  in Type.minimize_sort (ProofContext.tsig_of ctxt) S end;
wenzelm@42241
   343
wenzelm@42241
   344
fun parse_typ ctxt text =
wenzelm@42241
   345
  let
wenzelm@42241
   346
    val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
wenzelm@42242
   347
    val T = standard_parse_typ ctxt (syms, pos)
wenzelm@42242
   348
      handle ERROR msg => parse_failed ctxt pos msg "type";
wenzelm@42241
   349
  in T end;
wenzelm@42241
   350
wenzelm@42241
   351
fun parse_term T ctxt text =
wenzelm@42241
   352
  let
wenzelm@42241
   353
    val (T', _) = Type_Infer.paramify_dummies T 0;
wenzelm@42241
   354
    val (markup, kind) =
wenzelm@42241
   355
      if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
wenzelm@42241
   356
    val (syms, pos) = Syntax.parse_token ctxt markup text;
wenzelm@42241
   357
wenzelm@42241
   358
    val default_root = Config.get ctxt Syntax.default_root;
wenzelm@42241
   359
    val root =
wenzelm@42241
   360
      (case T' of
wenzelm@42241
   361
        Type (c, _) =>
wenzelm@42241
   362
          if c <> "prop" andalso Type.is_logtype (ProofContext.tsig_of ctxt) c
wenzelm@42241
   363
          then default_root else c
wenzelm@42241
   364
      | _ => default_root);
wenzelm@42241
   365
wenzelm@42241
   366
    fun check t = (Syntax.check_term ctxt (Type.constraint T' t); Exn.Result t)
wenzelm@42241
   367
      handle exn as ERROR _ => Exn.Exn exn;
wenzelm@42242
   368
    val t = standard_parse_term check ctxt root (syms, pos)
wenzelm@42241
   369
      handle ERROR msg => parse_failed ctxt pos msg kind;
wenzelm@42241
   370
  in t end;
wenzelm@42241
   371
wenzelm@42241
   372
wenzelm@42242
   373
(* parse_ast_pattern *)
wenzelm@42242
   374
wenzelm@42242
   375
fun parse_ast_pattern ctxt (root, str) =
wenzelm@42242
   376
  let
wenzelm@42242
   377
    val syn = ProofContext.syn_of ctxt;
wenzelm@42242
   378
wenzelm@42242
   379
    fun constify (ast as Ast.Constant _) = ast
wenzelm@42242
   380
      | constify (ast as Ast.Variable x) =
wenzelm@42242
   381
          if Syntax.is_const syn x orelse Long_Name.is_qualified x then Ast.Constant x
wenzelm@42242
   382
          else ast
wenzelm@42242
   383
      | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
wenzelm@42242
   384
wenzelm@42242
   385
    val (syms, pos) = Syntax.read_token str;
wenzelm@42242
   386
  in
wenzelm@42242
   387
    parse_asts ctxt true root (syms, pos)
wenzelm@42242
   388
    |> report_result ctxt pos
wenzelm@42242
   389
    |> constify
wenzelm@42242
   390
  end;
wenzelm@42242
   391
wenzelm@42242
   392
wenzelm@42242
   393
wenzelm@42245
   394
(** encode parse trees **)
wenzelm@42245
   395
wenzelm@42245
   396
(* term_of_sort *)
wenzelm@42245
   397
wenzelm@42245
   398
fun term_of_sort S =
wenzelm@42245
   399
  let
wenzelm@42245
   400
    val class = Lexicon.const o Lexicon.mark_class;
wenzelm@42245
   401
wenzelm@42245
   402
    fun classes [c] = class c
wenzelm@42245
   403
      | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
wenzelm@42245
   404
  in
wenzelm@42245
   405
    (case S of
wenzelm@42245
   406
      [] => Lexicon.const "_topsort"
wenzelm@42245
   407
    | [c] => class c
wenzelm@42245
   408
    | cs => Lexicon.const "_sort" $ classes cs)
wenzelm@42245
   409
  end;
wenzelm@42245
   410
wenzelm@42245
   411
wenzelm@42245
   412
(* term_of_typ *)
wenzelm@42245
   413
wenzelm@42247
   414
fun term_of_typ ctxt ty =
wenzelm@42245
   415
  let
wenzelm@42247
   416
    val show_sorts = Config.get ctxt show_sorts;
wenzelm@42247
   417
wenzelm@42245
   418
    fun of_sort t S =
wenzelm@42245
   419
      if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
wenzelm@42245
   420
      else t;
wenzelm@42245
   421
wenzelm@42245
   422
    fun term_of (Type (a, Ts)) =
wenzelm@42245
   423
          Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
wenzelm@42245
   424
      | term_of (TFree (x, S)) =
wenzelm@42245
   425
          if is_some (Lexicon.decode_position x) then Lexicon.free x
wenzelm@42245
   426
          else of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
wenzelm@42245
   427
      | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
wenzelm@42245
   428
  in term_of ty end;
wenzelm@42245
   429
wenzelm@42245
   430
wenzelm@42245
   431
(* simple_ast_of *)
wenzelm@42245
   432
wenzelm@42245
   433
fun simple_ast_of ctxt =
wenzelm@42245
   434
  let
wenzelm@42245
   435
    val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?";
wenzelm@42245
   436
    fun ast_of (Const (c, _)) = Ast.Constant c
wenzelm@42245
   437
      | ast_of (Free (x, _)) = Ast.Variable x
wenzelm@42245
   438
      | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi))
wenzelm@42245
   439
      | ast_of (t as _ $ _) =
wenzelm@42245
   440
          let val (f, args) = strip_comb t
wenzelm@42245
   441
          in Ast.mk_appl (ast_of f) (map ast_of args) end
wenzelm@42245
   442
      | ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
wenzelm@42245
   443
      | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
wenzelm@42245
   444
  in ast_of end;
wenzelm@42245
   445
wenzelm@42245
   446
wenzelm@42245
   447
(* sort_to_ast and typ_to_ast *)
wenzelm@42245
   448
wenzelm@42247
   449
fun apply_typed x fs = map (fn f => fn ctxt => f ctxt x) fs;
wenzelm@42245
   450
wenzelm@42245
   451
fun ast_of_termT ctxt trf tm =
wenzelm@42245
   452
  let
wenzelm@42245
   453
    val ctxt' = Config.put show_sorts false ctxt;
wenzelm@42245
   454
    fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
wenzelm@42245
   455
      | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
wenzelm@42245
   456
      | ast_of (Const (a, _)) = trans a []
wenzelm@42245
   457
      | ast_of (t as _ $ _) =
wenzelm@42245
   458
          (case strip_comb t of
wenzelm@42245
   459
            (Const (a, _), args) => trans a args
wenzelm@42245
   460
          | (f, args) => Ast.Appl (map ast_of (f :: args)))
wenzelm@42245
   461
      | ast_of t = simple_ast_of ctxt t
wenzelm@42245
   462
    and trans a args =
wenzelm@42245
   463
      ast_of (Syntax.apply_trans ctxt' (apply_typed dummyT (trf a)) args)
wenzelm@42245
   464
        handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
wenzelm@42245
   465
  in ast_of tm end;
wenzelm@42245
   466
wenzelm@42245
   467
fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (term_of_sort S);
wenzelm@42247
   468
fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ ctxt T);
wenzelm@42245
   469
wenzelm@42245
   470
wenzelm@42245
   471
(* term_to_ast *)
wenzelm@42245
   472
wenzelm@42245
   473
fun term_to_ast idents consts ctxt trf tm =
wenzelm@42245
   474
  let
wenzelm@42245
   475
    val show_types =
wenzelm@42245
   476
      Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
wenzelm@42245
   477
      Config.get ctxt show_all_types;
wenzelm@42245
   478
    val show_sorts = Config.get ctxt show_sorts;
wenzelm@42245
   479
    val show_structs = Config.get ctxt show_structs;
wenzelm@42245
   480
    val show_free_types = Config.get ctxt show_free_types;
wenzelm@42245
   481
    val show_all_types = Config.get ctxt show_all_types;
wenzelm@42245
   482
wenzelm@42245
   483
    val {structs, fixes} = idents;
wenzelm@42245
   484
wenzelm@42245
   485
    fun mark_atoms ((t as Const (c, T)) $ u) =
wenzelm@42245
   486
          if member (op =) Syntax.standard_token_markers c
wenzelm@42245
   487
          then t $ u else mark_atoms t $ mark_atoms u
wenzelm@42245
   488
      | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
wenzelm@42245
   489
      | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
wenzelm@42245
   490
      | mark_atoms (t as Const (c, T)) =
wenzelm@42245
   491
          if member (op =) consts c then t
wenzelm@42245
   492
          else Const (Lexicon.mark_const c, T)
wenzelm@42245
   493
      | mark_atoms (t as Free (x, T)) =
wenzelm@42245
   494
          let val i = find_index (fn s => s = x) structs + 1 in
wenzelm@42245
   495
            if i = 0 andalso member (op =) fixes x then
wenzelm@42245
   496
              Const (Lexicon.mark_fixed x, T)
wenzelm@42245
   497
            else if i = 1 andalso not show_structs then
wenzelm@42245
   498
              Lexicon.const "_struct" $ Lexicon.const "_indexdefault"
wenzelm@42245
   499
            else Lexicon.const "_free" $ t
wenzelm@42245
   500
          end
wenzelm@42245
   501
      | mark_atoms (t as Var (xi, T)) =
wenzelm@42245
   502
          if xi = Syntax.dddot_indexname then Const ("_DDDOT", T)
wenzelm@42245
   503
          else Lexicon.const "_var" $ t
wenzelm@42245
   504
      | mark_atoms a = a;
wenzelm@42245
   505
wenzelm@42245
   506
    fun prune_typs (t_seen as (Const _, _)) = t_seen
wenzelm@42245
   507
      | prune_typs (t as Free (x, ty), seen) =
wenzelm@42245
   508
          if ty = dummyT then (t, seen)
wenzelm@42245
   509
          else if not show_free_types orelse member (op aconv) seen t then (Lexicon.free x, seen)
wenzelm@42245
   510
          else (t, t :: seen)
wenzelm@42245
   511
      | prune_typs (t as Var (xi, ty), seen) =
wenzelm@42245
   512
          if ty = dummyT then (t, seen)
wenzelm@42245
   513
          else if not show_free_types orelse member (op aconv) seen t then (Lexicon.var xi, seen)
wenzelm@42245
   514
          else (t, t :: seen)
wenzelm@42245
   515
      | prune_typs (t_seen as (Bound _, _)) = t_seen
wenzelm@42245
   516
      | prune_typs (Abs (x, ty, t), seen) =
wenzelm@42245
   517
          let val (t', seen') = prune_typs (t, seen);
wenzelm@42245
   518
          in (Abs (x, ty, t'), seen') end
wenzelm@42245
   519
      | prune_typs (t1 $ t2, seen) =
wenzelm@42245
   520
          let
wenzelm@42245
   521
            val (t1', seen') = prune_typs (t1, seen);
wenzelm@42245
   522
            val (t2', seen'') = prune_typs (t2, seen');
wenzelm@42245
   523
          in (t1' $ t2', seen'') end;
wenzelm@42245
   524
wenzelm@42245
   525
    fun ast_of tm =
wenzelm@42245
   526
      (case strip_comb tm of
wenzelm@42245
   527
        (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' ctxt t)) (map ast_of ts)
wenzelm@42245
   528
      | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
wenzelm@42245
   529
          Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
wenzelm@42245
   530
      | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
wenzelm@42245
   531
          Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts)
wenzelm@42245
   532
      | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
wenzelm@42245
   533
          Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
wenzelm@42245
   534
      | (Const ("_idtdummy", T), ts) =>
wenzelm@42245
   535
          Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
wenzelm@42245
   536
      | (const as Const (c, T), ts) =>
wenzelm@42245
   537
          if show_all_types
wenzelm@42245
   538
          then Ast.mk_appl (constrain const T) (map ast_of ts)
wenzelm@42245
   539
          else trans c T ts
wenzelm@42245
   540
      | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
wenzelm@42245
   541
wenzelm@42245
   542
    and trans a T args =
wenzelm@42245
   543
      ast_of (Syntax.apply_trans ctxt (apply_typed T (trf a)) args)
wenzelm@42245
   544
        handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
wenzelm@42245
   545
wenzelm@42245
   546
    and constrain t T =
wenzelm@42245
   547
      if show_types andalso T <> dummyT then
wenzelm@42245
   548
        Ast.Appl [Ast.Constant Syntax.constrainC, simple_ast_of ctxt t,
wenzelm@42247
   549
          ast_of_termT ctxt trf (term_of_typ ctxt T)]
wenzelm@42245
   550
      else simple_ast_of ctxt t;
wenzelm@42245
   551
  in
wenzelm@42245
   552
    tm
wenzelm@42245
   553
    |> Syn_Trans.prop_tr'
wenzelm@42245
   554
    |> show_types ? (#1 o prune_typs o rpair [])
wenzelm@42245
   555
    |> mark_atoms
wenzelm@42245
   556
    |> ast_of
wenzelm@42245
   557
  end;
wenzelm@42245
   558
wenzelm@42245
   559
wenzelm@42245
   560
wenzelm@42242
   561
(** unparse **)
wenzelm@42242
   562
wenzelm@42245
   563
(** unparse terms, typs, sorts **)
wenzelm@42245
   564
wenzelm@42245
   565
local
wenzelm@42245
   566
wenzelm@42245
   567
fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
wenzelm@42245
   568
wenzelm@42245
   569
fun unparse_t t_to_ast prt_t markup ctxt curried t =
wenzelm@42245
   570
  let
wenzelm@42245
   571
    val {consts, print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} =
wenzelm@42245
   572
      Syntax.rep_syntax (ProofContext.syn_of ctxt);
wenzelm@42245
   573
    val ast = t_to_ast consts ctxt (lookup_tr' print_trtab) t;
wenzelm@42245
   574
  in
wenzelm@42245
   575
    Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
wenzelm@42245
   576
      (Syntax.lookup_tokentr tokentrtab (print_mode_value ()))
wenzelm@42245
   577
      (Ast.normalize ctxt (Symtab.lookup_list print_ruletab) ast))
wenzelm@42245
   578
  end;
wenzelm@42245
   579
wenzelm@42245
   580
in
wenzelm@42245
   581
wenzelm@42245
   582
fun standard_unparse_sort {extern_class} ctxt =
wenzelm@42245
   583
  unparse_t (K sort_to_ast)
wenzelm@42245
   584
    (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I})
wenzelm@42245
   585
    Markup.sort ctxt false;
wenzelm@42245
   586
wenzelm@42245
   587
fun standard_unparse_typ extern ctxt =
wenzelm@42245
   588
  unparse_t (K typ_to_ast) (Printer.pretty_typ_ast extern) Markup.typ ctxt false;
wenzelm@42245
   589
wenzelm@42245
   590
fun standard_unparse_term idents extern =
wenzelm@42245
   591
  unparse_t (term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
wenzelm@42245
   592
wenzelm@42245
   593
end;
wenzelm@42245
   594
wenzelm@42245
   595
wenzelm@42241
   596
fun unparse_sort ctxt =
wenzelm@42245
   597
  standard_unparse_sort {extern_class = Type.extern_class (ProofContext.tsig_of ctxt)} ctxt;
wenzelm@42241
   598
wenzelm@42241
   599
fun unparse_typ ctxt =
wenzelm@42241
   600
  let
wenzelm@42241
   601
    val tsig = ProofContext.tsig_of ctxt;
wenzelm@42241
   602
    val extern = {extern_class = Type.extern_class tsig, extern_type = Type.extern_type tsig};
wenzelm@42245
   603
  in standard_unparse_typ extern ctxt end;
wenzelm@42241
   604
wenzelm@42241
   605
fun unparse_term ctxt =
wenzelm@42241
   606
  let
wenzelm@42241
   607
    val tsig = ProofContext.tsig_of ctxt;
wenzelm@42241
   608
    val syntax = ProofContext.syntax_of ctxt;
wenzelm@42241
   609
    val consts = ProofContext.consts_of ctxt;
wenzelm@42241
   610
    val extern =
wenzelm@42241
   611
     {extern_class = Type.extern_class tsig,
wenzelm@42241
   612
      extern_type = Type.extern_type tsig,
wenzelm@42241
   613
      extern_const = Consts.extern consts};
wenzelm@42241
   614
  in
wenzelm@42245
   615
    standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
wenzelm@42245
   616
      (not (Pure_Thy.old_appl_syntax (ProofContext.theory_of ctxt)))
wenzelm@42241
   617
  end;
wenzelm@42241
   618
wenzelm@42241
   619
wenzelm@42245
   620
wenzelm@42245
   621
(** translations **)
wenzelm@42245
   622
wenzelm@42245
   623
(* type propositions *)
wenzelm@42245
   624
wenzelm@42247
   625
fun type_prop_tr' ctxt T [Const ("\\<^const>Pure.sort_constraint", _)] =
wenzelm@42247
   626
      Lexicon.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T
wenzelm@42247
   627
  | type_prop_tr' ctxt T [t] =
wenzelm@42247
   628
      Lexicon.const "_ofclass" $ term_of_typ ctxt T $ t
wenzelm@42245
   629
  | type_prop_tr' _ T ts = raise TYPE ("type_prop_tr'", [T], ts);
wenzelm@42245
   630
wenzelm@42245
   631
wenzelm@42245
   632
(* type reflection *)
wenzelm@42245
   633
wenzelm@42247
   634
fun type_tr' ctxt (Type ("itself", [T])) ts =
wenzelm@42247
   635
      Term.list_comb (Lexicon.const "_TYPE" $ term_of_typ ctxt T, ts)
wenzelm@42245
   636
  | type_tr' _ _ _ = raise Match;
wenzelm@42245
   637
wenzelm@42245
   638
wenzelm@42245
   639
(* type constraints *)
wenzelm@42245
   640
wenzelm@42247
   641
fun type_constraint_tr' ctxt (Type ("fun", [T, _])) (t :: ts) =
wenzelm@42247
   642
      Term.list_comb (Lexicon.const Syntax.constrainC $ t $ term_of_typ ctxt T, ts)
wenzelm@42245
   643
  | type_constraint_tr' _ _ _ = raise Match;
wenzelm@42245
   644
wenzelm@42245
   645
wenzelm@42245
   646
(* setup translations *)
wenzelm@42245
   647
wenzelm@42245
   648
val _ = Context.>> (Context.map_theory
wenzelm@42247
   649
  (Sign.add_advanced_trfunsT
wenzelm@42245
   650
   [("_type_prop", type_prop_tr'),
wenzelm@42245
   651
    ("\\<^const>TYPE", type_tr'),
wenzelm@42245
   652
    ("_type_constraint_", type_constraint_tr')]));
wenzelm@42245
   653
wenzelm@42245
   654
wenzelm@42245
   655
wenzelm@42242
   656
(** install operations **)
wenzelm@42242
   657
wenzelm@42241
   658
val _ = Syntax.install_operations
wenzelm@42241
   659
  {parse_sort = parse_sort,
wenzelm@42241
   660
   parse_typ = parse_typ,
wenzelm@42241
   661
   parse_term = parse_term dummyT,
wenzelm@42241
   662
   parse_prop = parse_term propT,
wenzelm@42241
   663
   unparse_sort = unparse_sort,
wenzelm@42241
   664
   unparse_typ = unparse_typ,
wenzelm@42241
   665
   unparse_term = unparse_term};
wenzelm@42241
   666
wenzelm@42241
   667
end;