src/Pure/Syntax/syntax_phases.ML
author wenzelm
Wed Dec 12 23:36:07 2012 +0100 (2012-12-12 ago)
changeset 50499 f496b2b7bafb
parent 50201 c26369c9eda6
child 52143 36ffe23b25f8
permissions -rw-r--r--
rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
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@45427
    10
  val decode_sort: term -> sort
wenzelm@45427
    11
  val decode_typ: term -> typ
wenzelm@42242
    12
  val decode_term: Proof.context ->
wenzelm@44736
    13
    Position.report list * term Exn.result -> Position.report list * 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@45429
    16
  val print_checks: Proof.context -> unit
wenzelm@45429
    17
  val typ_check: int -> string -> (Proof.context -> typ list -> typ list) ->
wenzelm@45429
    18
    Context.generic -> Context.generic
wenzelm@45429
    19
  val term_check: int -> string -> (Proof.context -> term list -> term list) ->
wenzelm@45429
    20
    Context.generic -> Context.generic
wenzelm@45429
    21
  val typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) ->
wenzelm@45429
    22
    Context.generic -> Context.generic
wenzelm@45429
    23
  val term_uncheck: int -> string -> (Proof.context -> term list -> term list) ->
wenzelm@45429
    24
    Context.generic -> Context.generic
wenzelm@45444
    25
  val typ_check': int -> string ->
wenzelm@45444
    26
    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
wenzelm@45444
    27
    Context.generic -> Context.generic
wenzelm@45444
    28
  val term_check': int -> string ->
wenzelm@45444
    29
    (term list -> Proof.context -> (term list * Proof.context) option) ->
wenzelm@45444
    30
    Context.generic -> Context.generic
wenzelm@45444
    31
  val typ_uncheck': int -> string ->
wenzelm@45444
    32
    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
wenzelm@45444
    33
    Context.generic -> Context.generic
wenzelm@45444
    34
  val term_uncheck': int -> string ->
wenzelm@45444
    35
    (term list -> Proof.context -> (term list * Proof.context) option) ->
wenzelm@45444
    36
    Context.generic -> Context.generic
wenzelm@42242
    37
end
wenzelm@42242
    38
wenzelm@42243
    39
structure Syntax_Phases: SYNTAX_PHASES =
wenzelm@42241
    40
struct
wenzelm@42241
    41
wenzelm@42298
    42
(** markup logical entities **)
wenzelm@42298
    43
wenzelm@42298
    44
fun markup_class ctxt c =
wenzelm@42379
    45
  [Name_Space.markup (Type.class_space (Proof_Context.tsig_of ctxt)) c];
wenzelm@42298
    46
wenzelm@42298
    47
fun markup_type ctxt c =
wenzelm@42379
    48
  [Name_Space.markup (Type.type_space (Proof_Context.tsig_of ctxt)) c];
wenzelm@42298
    49
wenzelm@42298
    50
fun markup_const ctxt c =
wenzelm@42379
    51
  [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c];
wenzelm@42298
    52
wenzelm@42298
    53
fun markup_free ctxt x =
wenzelm@50201
    54
  [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
wenzelm@42493
    55
  (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x
wenzelm@42493
    56
   then [Variable.markup_fixed ctxt x]
wenzelm@42493
    57
   else []);
wenzelm@42298
    58
wenzelm@50201
    59
fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
wenzelm@42298
    60
wenzelm@45412
    61
fun markup_bound def ps (name, id) =
wenzelm@50201
    62
  let val entity = Markup.entity Markup.boundN name in
wenzelm@50201
    63
    Markup.bound ::
wenzelm@45412
    64
      map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps
wenzelm@45412
    65
  end;
wenzelm@42298
    66
wenzelm@42298
    67
fun markup_entity ctxt c =
wenzelm@42360
    68
  (case Syntax.lookup_const (Proof_Context.syn_of ctxt) c of
wenzelm@42298
    69
    SOME "" => []
wenzelm@42298
    70
  | SOME b => markup_entity ctxt b
wenzelm@42298
    71
  | NONE => c |> Lexicon.unmark
wenzelm@42298
    72
     {case_class = markup_class ctxt,
wenzelm@42298
    73
      case_type = markup_type ctxt,
wenzelm@42298
    74
      case_const = markup_const ctxt,
wenzelm@42298
    75
      case_fixed = markup_free ctxt,
wenzelm@42298
    76
      case_default = K []});
wenzelm@42298
    77
wenzelm@42298
    78
wenzelm@42298
    79
wenzelm@42242
    80
(** decode parse trees **)
wenzelm@42242
    81
wenzelm@45427
    82
(* decode_sort *)
wenzelm@42242
    83
wenzelm@45427
    84
fun decode_sort tm =
wenzelm@42242
    85
  let
wenzelm@45427
    86
    fun err () = raise TERM ("decode_sort: bad encoding of classes", [tm]);
wenzelm@42242
    87
wenzelm@42242
    88
    fun class s = Lexicon.unmark_class s handle Fail _ => err ();
wenzelm@42242
    89
wenzelm@42242
    90
    fun classes (Const (s, _)) = [class s]
wenzelm@42242
    91
      | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
wenzelm@42242
    92
      | classes _ = err ();
wenzelm@42242
    93
wenzelm@42242
    94
    fun sort (Const ("_topsort", _)) = []
wenzelm@49674
    95
      | sort (Const ("_sort", _) $ cs) = classes cs
wenzelm@42242
    96
      | sort (Const (s, _)) = [class s]
wenzelm@42242
    97
      | sort _ = err ();
wenzelm@42242
    98
  in sort tm end;
wenzelm@42242
    99
wenzelm@42242
   100
wenzelm@45427
   101
(* decode_typ *)
wenzelm@42242
   102
wenzelm@49685
   103
fun decode_pos (Free (s, _)) =
wenzelm@49685
   104
      if is_some (Term_Position.decode s) then SOME s else NONE
wenzelm@49685
   105
  | decode_pos _ = NONE;
wenzelm@49685
   106
wenzelm@45427
   107
fun decode_typ tm =
wenzelm@45427
   108
  let
wenzelm@45427
   109
    fun err () = raise TERM ("decode_typ: bad encoding of type", [tm]);
wenzelm@42242
   110
wenzelm@49685
   111
    fun typ ps sort tm =
wenzelm@49685
   112
      (case tm of
wenzelm@49685
   113
        Const ("_tfree", _) $ t => typ ps sort t
wenzelm@49685
   114
      | Const ("_tvar", _) $ t => typ ps sort t
wenzelm@49685
   115
      | Const ("_ofsort", _) $ t $ s =>
wenzelm@49685
   116
          (case decode_pos s of
wenzelm@49685
   117
            SOME p => typ (p :: ps) sort t
wenzelm@49685
   118
          | NONE =>
wenzelm@49685
   119
              if is_none sort then typ ps (SOME (decode_sort s)) t
wenzelm@49685
   120
              else err ())
wenzelm@49685
   121
      | Const ("_dummy_ofsort", _) $ s => TFree ("'_dummy_", decode_sort s)
wenzelm@49685
   122
      | Free (x, _) => TFree (x, ps @ the_default dummyS sort)
wenzelm@49685
   123
      | Var (xi, _) => TVar (xi, ps @ the_default dummyS sort)
wenzelm@49685
   124
      | _ =>
wenzelm@49685
   125
          if null ps andalso is_none sort then
wenzelm@49685
   126
            let
wenzelm@49685
   127
              val (head, args) = Term.strip_comb tm;
wenzelm@49685
   128
              val a =
wenzelm@49685
   129
                (case head of
wenzelm@49685
   130
                  Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
wenzelm@49685
   131
                | _ => err ());
wenzelm@49685
   132
            in Type (a, map (typ [] NONE) args) end
wenzelm@49685
   133
          else err ());
wenzelm@49685
   134
  in typ [] NONE tm end;
wenzelm@42242
   135
wenzelm@42242
   136
wenzelm@42242
   137
(* parsetree_to_ast *)
wenzelm@42242
   138
wenzelm@46126
   139
fun parsetree_to_ast ctxt raw trf parsetree =
wenzelm@42242
   140
  let
wenzelm@44736
   141
    val reports = Unsynchronized.ref ([]: Position.report list);
wenzelm@44735
   142
    fun report pos = Position.store_reports reports [pos];
wenzelm@42242
   143
wenzelm@42242
   144
    fun trans a args =
wenzelm@42242
   145
      (case trf a of
wenzelm@42242
   146
        NONE => Ast.mk_appl (Ast.Constant a) args
wenzelm@42242
   147
      | SOME f => f ctxt args);
wenzelm@42242
   148
wenzelm@49674
   149
    fun asts_of_token tok =
wenzelm@49674
   150
      if Lexicon.valued_token tok
wenzelm@49674
   151
      then [Ast.Variable (Lexicon.str_of_token tok)]
wenzelm@49674
   152
      else [];
wenzelm@49674
   153
wenzelm@49674
   154
    fun asts_of_position c tok =
wenzelm@49674
   155
      if raw then asts_of_token tok
wenzelm@49674
   156
      else
wenzelm@49674
   157
        [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok),
wenzelm@49674
   158
          Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]]
wenzelm@49674
   159
wenzelm@49674
   160
    and asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
wenzelm@42242
   161
          let
wenzelm@42470
   162
            val pos = Lexicon.pos_of_token tok;
wenzelm@42470
   163
            val c = Proof_Context.read_class ctxt (Lexicon.str_of_token tok)
wenzelm@48992
   164
              handle ERROR msg => error (msg ^ Position.here pos);
wenzelm@42470
   165
            val _ = report pos (markup_class ctxt) c;
wenzelm@42282
   166
          in [Ast.Constant (Lexicon.mark_class c)] end
wenzelm@42282
   167
      | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
wenzelm@42242
   168
          let
wenzelm@42470
   169
            val pos = Lexicon.pos_of_token tok;
wenzelm@42470
   170
            val Type (c, _) =
wenzelm@42470
   171
              Proof_Context.read_type_name_proper ctxt false (Lexicon.str_of_token tok)
wenzelm@48992
   172
                handle ERROR msg => error (msg ^ Position.here pos);
wenzelm@42470
   173
            val _ = report pos (markup_type ctxt) c;
wenzelm@42282
   174
          in [Ast.Constant (Lexicon.mark_type c)] end
wenzelm@49674
   175
      | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
wenzelm@49674
   176
      | asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok
wenzelm@42282
   177
      | asts_of (Parser.Node (a, pts)) =
wenzelm@42282
   178
          let
wenzelm@42282
   179
            val _ = pts |> List.app
wenzelm@42282
   180
              (fn Parser.Node _ => () | Parser.Tip tok =>
wenzelm@42282
   181
                if Lexicon.valued_token tok then ()
wenzelm@42298
   182
                else report (Lexicon.pos_of_token tok) (markup_entity ctxt) a);
wenzelm@42282
   183
          in [trans a (maps asts_of pts)] end
wenzelm@49674
   184
      | asts_of (Parser.Tip tok) = asts_of_token tok
wenzelm@42282
   185
wenzelm@42282
   186
    and ast_of pt =
wenzelm@42282
   187
      (case asts_of pt of
wenzelm@42282
   188
        [ast] => ast
wenzelm@42282
   189
      | asts => raise Ast.AST ("parsetree_to_ast: malformed parsetree", asts));
wenzelm@42242
   190
wenzelm@42242
   191
    val ast = Exn.interruptible_capture ast_of parsetree;
wenzelm@42242
   192
  in (! reports, ast) end;
wenzelm@42242
   193
wenzelm@42242
   194
wenzelm@42242
   195
(* ast_to_term *)
wenzelm@42242
   196
wenzelm@42242
   197
fun ast_to_term ctxt trf =
wenzelm@42242
   198
  let
wenzelm@42242
   199
    fun trans a args =
wenzelm@42242
   200
      (case trf a of
wenzelm@42476
   201
        NONE => Term.list_comb (Syntax.const a, args)
wenzelm@42242
   202
      | SOME f => f ctxt args);
wenzelm@42242
   203
wenzelm@42242
   204
    fun term_of (Ast.Constant a) = trans a []
wenzelm@42242
   205
      | term_of (Ast.Variable x) = Lexicon.read_var x
wenzelm@42242
   206
      | term_of (Ast.Appl (Ast.Constant a :: (asts as _ :: _))) =
wenzelm@42242
   207
          trans a (map term_of asts)
wenzelm@42242
   208
      | term_of (Ast.Appl (ast :: (asts as _ :: _))) =
wenzelm@42242
   209
          Term.list_comb (term_of ast, map term_of asts)
wenzelm@42242
   210
      | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
wenzelm@42242
   211
  in term_of end;
wenzelm@42242
   212
wenzelm@42242
   213
wenzelm@42242
   214
(* decode_term -- transform parse tree into raw term *)
wenzelm@42242
   215
wenzelm@44736
   216
fun decode_term _ (result as (_: Position.report list, Exn.Exn _)) = result
wenzelm@43761
   217
  | decode_term ctxt (reports0, Exn.Res tm) =
wenzelm@42242
   218
      let
wenzelm@42250
   219
        fun get_const a =
wenzelm@42360
   220
          ((true, #1 (Term.dest_Const (Proof_Context.read_const_proper ctxt false a)))
wenzelm@42360
   221
            handle ERROR _ => (false, Consts.intern (Proof_Context.consts_of ctxt) a));
wenzelm@42360
   222
        val get_free = Proof_Context.intern_skolem ctxt;
wenzelm@42250
   223
wenzelm@42242
   224
        val reports = Unsynchronized.ref reports0;
wenzelm@44735
   225
        fun report ps = Position.store_reports reports ps;
wenzelm@42242
   226
wenzelm@42242
   227
        fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
wenzelm@42264
   228
              (case Term_Position.decode_position typ of
wenzelm@45445
   229
                SOME (p, T) => Type.constraint T (decode (p :: ps) qs bs t)
wenzelm@45427
   230
              | NONE => Type.constraint (decode_typ typ) (decode ps qs bs t))
wenzelm@42242
   231
          | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
wenzelm@42264
   232
              (case Term_Position.decode_position typ of
wenzelm@45445
   233
                SOME (q, T) => Type.constraint (T --> dummyT) (decode ps (q :: qs) bs t)
wenzelm@45427
   234
              | NONE => Type.constraint (decode_typ typ --> dummyT) (decode ps qs bs t))
wenzelm@42242
   235
          | decode _ qs bs (Abs (x, T, t)) =
wenzelm@42242
   236
              let
wenzelm@45412
   237
                val id = serial ();
wenzelm@45412
   238
                val _ = report qs (markup_bound true qs) (x, id);
wenzelm@45412
   239
              in Abs (x, T, decode [] [] ((qs, (x, id)) :: bs) t) end
wenzelm@42242
   240
          | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
wenzelm@42242
   241
          | decode ps _ _ (Const (a, T)) =
wenzelm@42242
   242
              (case try Lexicon.unmark_fixed a of
wenzelm@42282
   243
                SOME x => (report ps (markup_free ctxt) x; Free (x, T))
wenzelm@42242
   244
              | NONE =>
wenzelm@42242
   245
                  let
wenzelm@42242
   246
                    val c =
wenzelm@42242
   247
                      (case try Lexicon.unmark_const a of
wenzelm@42242
   248
                        SOME c => c
wenzelm@42242
   249
                      | NONE => snd (get_const a));
wenzelm@42282
   250
                    val _ = report ps (markup_const ctxt) c;
wenzelm@42242
   251
                  in Const (c, T) end)
wenzelm@42242
   252
          | decode ps _ _ (Free (a, T)) =
wenzelm@42242
   253
              (case (get_free a, get_const a) of
wenzelm@42282
   254
                (SOME x, _) => (report ps (markup_free ctxt) x; Free (x, T))
wenzelm@42282
   255
              | (_, (true, c)) => (report ps (markup_const ctxt) c; Const (c, T))
wenzelm@42242
   256
              | (_, (false, c)) =>
wenzelm@42242
   257
                  if Long_Name.is_qualified c
wenzelm@42282
   258
                  then (report ps (markup_const ctxt) c; Const (c, T))
wenzelm@42282
   259
                  else (report ps (markup_free ctxt) c; Free (c, T)))
wenzelm@42242
   260
          | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
wenzelm@42242
   261
          | decode ps _ bs (t as Bound i) =
wenzelm@42242
   262
              (case try (nth bs) i of
wenzelm@45412
   263
                SOME (qs, (x, id)) => (report ps (markup_bound false qs) (x, id); t)
wenzelm@42242
   264
              | NONE => t);
wenzelm@42242
   265
wenzelm@42242
   266
        val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
wenzelm@42242
   267
      in (! reports, tm') end;
wenzelm@42242
   268
wenzelm@42242
   269
wenzelm@42242
   270
wenzelm@42242
   271
(** parse **)
wenzelm@42242
   272
wenzelm@42242
   273
(* results *)
wenzelm@42242
   274
wenzelm@43761
   275
fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results;
wenzelm@42242
   276
fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
wenzelm@42242
   277
wenzelm@46512
   278
fun report_result ctxt pos ambig_msgs results =
wenzelm@42242
   279
  (case (proper_results results, failed_results results) of
wenzelm@44736
   280
    ([], (reports, exn) :: _) => (Context_Position.reports ctxt reports; reraise exn)
wenzelm@44736
   281
  | ([(reports, x)], _) => (Context_Position.reports ctxt reports; x)
wenzelm@46512
   282
  | _ =>
wenzelm@46512
   283
      if null ambig_msgs then
wenzelm@48992
   284
        error ("Parse error: ambiguous syntax" ^ Position.here pos)
wenzelm@46512
   285
      else error (cat_lines ambig_msgs));
wenzelm@42242
   286
wenzelm@42242
   287
wenzelm@42249
   288
(* parse raw asts *)
wenzelm@42242
   289
wenzelm@42242
   290
fun parse_asts ctxt raw root (syms, pos) =
wenzelm@42242
   291
  let
wenzelm@42360
   292
    val syn = Proof_Context.syn_of ctxt;
wenzelm@42253
   293
    val ast_tr = Syntax.parse_ast_translation syn;
wenzelm@42242
   294
wenzelm@42251
   295
    val toks = Syntax.tokenize syn raw syms;
wenzelm@44736
   296
    val _ = Context_Position.reports ctxt (map Lexicon.report_of_token toks);
wenzelm@42242
   297
wenzelm@45641
   298
    val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
wenzelm@42242
   299
      handle ERROR msg =>
wenzelm@42242
   300
        error (msg ^
wenzelm@50201
   301
          implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
wenzelm@42242
   302
    val len = length pts;
wenzelm@42242
   303
wenzelm@42242
   304
    val limit = Config.get ctxt Syntax.ambiguity_limit;
wenzelm@46512
   305
    val ambig_msgs =
wenzelm@46512
   306
      if len <= 1 then []
wenzelm@46506
   307
      else
wenzelm@46512
   308
        [cat_lines
wenzelm@48992
   309
          (("Ambiguous input" ^ Position.here (Position.reset_range pos) ^
wenzelm@46512
   310
            "\nproduces " ^ string_of_int len ^ " parse trees" ^
wenzelm@46512
   311
            (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
wenzelm@46512
   312
            map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))];
wenzelm@46512
   313
wenzelm@46512
   314
  in (ambig_msgs, map (parsetree_to_ast ctxt raw ast_tr) pts) end;
wenzelm@42242
   315
wenzelm@46506
   316
fun parse_tree ctxt root input =
wenzelm@42242
   317
  let
wenzelm@42360
   318
    val syn = Proof_Context.syn_of ctxt;
wenzelm@42253
   319
    val tr = Syntax.parse_translation syn;
wenzelm@42255
   320
    val parse_rules = Syntax.parse_rules syn;
wenzelm@46512
   321
    val (ambig_msgs, asts) = parse_asts ctxt false root input;
wenzelm@46512
   322
    val results =
wenzelm@46512
   323
      (map o apsnd o Exn.maps_result)
wenzelm@46512
   324
        (Ast.normalize ctxt parse_rules #> Exn.interruptible_capture (ast_to_term ctxt tr)) asts;
wenzelm@46512
   325
  in (ambig_msgs, results) end;
wenzelm@42242
   326
wenzelm@42242
   327
wenzelm@42249
   328
(* parse logical entities *)
wenzelm@42242
   329
wenzelm@42241
   330
fun parse_failed ctxt pos msg kind =
wenzelm@42241
   331
  cat_error msg ("Failed to parse " ^ kind ^
wenzelm@50201
   332
    Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
wenzelm@42241
   333
wenzelm@43731
   334
fun parse_sort ctxt =
wenzelm@50201
   335
  Syntax.parse_token ctxt Term_XML.Decode.sort Markup.sort
wenzelm@43731
   336
    (fn (syms, pos) =>
wenzelm@46506
   337
      parse_tree ctxt "sort" (syms, pos)
wenzelm@46512
   338
      |> uncurry (report_result ctxt pos)
wenzelm@45427
   339
      |> decode_sort
wenzelm@43731
   340
      |> Type.minimize_sort (Proof_Context.tsig_of ctxt)
wenzelm@43731
   341
      handle ERROR msg => parse_failed ctxt pos msg "sort");
wenzelm@42241
   342
wenzelm@43731
   343
fun parse_typ ctxt =
wenzelm@50201
   344
  Syntax.parse_token ctxt Term_XML.Decode.typ Markup.typ
wenzelm@43731
   345
    (fn (syms, pos) =>
wenzelm@46506
   346
      parse_tree ctxt "type" (syms, pos)
wenzelm@46512
   347
      |> uncurry (report_result ctxt pos)
wenzelm@45427
   348
      |> decode_typ
wenzelm@43731
   349
      handle ERROR msg => parse_failed ctxt pos msg "type");
wenzelm@42241
   350
wenzelm@43731
   351
fun parse_term is_prop ctxt =
wenzelm@42241
   352
  let
wenzelm@42281
   353
    val (markup, kind, root, constrain) =
wenzelm@42281
   354
      if is_prop
wenzelm@50201
   355
      then (Markup.prop, "proposition", "prop", Type.constraint propT)
wenzelm@50201
   356
      else (Markup.term, "term", Config.get ctxt Syntax.root, I);
wenzelm@43731
   357
    val decode = constrain o Term_XML.Decode.term;
wenzelm@42249
   358
  in
wenzelm@43731
   359
    Syntax.parse_token ctxt decode markup
wenzelm@43731
   360
      (fn (syms, pos) =>
wenzelm@43731
   361
        let
wenzelm@46512
   362
          val (ambig_msgs, results) = parse_tree ctxt root (syms, pos) ||> map (decode_term ctxt);
wenzelm@46506
   363
          val parsed_len = length (proper_results results);
wenzelm@42249
   364
wenzelm@46512
   365
          val ambiguity_warning = Config.get ctxt Syntax.ambiguity_warning;
wenzelm@43731
   366
          val limit = Config.get ctxt Syntax.ambiguity_limit;
wenzelm@42249
   367
wenzelm@43731
   368
          (*brute-force disambiguation via type-inference*)
wenzelm@43761
   369
          fun check t = (Syntax.check_term ctxt (constrain t); Exn.Res t)
wenzelm@43731
   370
            handle exn as ERROR _ => Exn.Exn exn;
wenzelm@42249
   371
wenzelm@43731
   372
          val results' =
wenzelm@46506
   373
            if parsed_len > 1 then
wenzelm@46989
   374
              (grouped 10 (Par_List.map_name "Syntax_Phases.parse_term") o apsnd o Exn.maps_result)
wenzelm@43731
   375
                check results
wenzelm@43731
   376
            else results;
wenzelm@43731
   377
          val reports' = fst (hd results');
wenzelm@42249
   378
wenzelm@43731
   379
          val errs = map snd (failed_results results');
wenzelm@43731
   380
          val checked = map snd (proper_results results');
wenzelm@46506
   381
          val checked_len = length checked;
wenzelm@42249
   382
wenzelm@43731
   383
          val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
wenzelm@43731
   384
        in
wenzelm@46506
   385
          if checked_len = 0 then
wenzelm@46512
   386
            report_result ctxt pos []
wenzelm@46512
   387
              [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msgs @ errs)))]
wenzelm@46506
   388
          else if checked_len = 1 then
wenzelm@46512
   389
            (if parsed_len > 1 andalso ambiguity_warning then
wenzelm@43731
   390
              Context_Position.if_visible ctxt warning
wenzelm@46512
   391
                (cat_lines (ambig_msgs @
wenzelm@46512
   392
                  ["Fortunately, only one parse tree is type correct" ^
wenzelm@48992
   393
                  Position.here (Position.reset_range pos) ^
wenzelm@46512
   394
                  ",\nbut you may still want to disambiguate your grammar or your input."]))
wenzelm@46512
   395
             else (); report_result ctxt pos [] results')
wenzelm@43731
   396
          else
wenzelm@46512
   397
            report_result ctxt pos []
wenzelm@46512
   398
              [(reports', Exn.Exn (ERROR (cat_lines (ambig_msgs @
wenzelm@46512
   399
                (("Ambiguous input\n" ^ string_of_int checked_len ^ " terms are type correct" ^
wenzelm@46506
   400
                  (if checked_len <= limit then ""
wenzelm@46506
   401
                   else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
wenzelm@43731
   402
                  map show_term (take limit checked))))))]
wenzelm@43731
   403
        end handle ERROR msg => parse_failed ctxt pos msg kind)
wenzelm@42249
   404
  end;
wenzelm@42241
   405
wenzelm@42241
   406
wenzelm@42242
   407
(* parse_ast_pattern *)
wenzelm@42242
   408
wenzelm@42242
   409
fun parse_ast_pattern ctxt (root, str) =
wenzelm@42242
   410
  let
wenzelm@42360
   411
    val syn = Proof_Context.syn_of ctxt;
wenzelm@42242
   412
wenzelm@42242
   413
    fun constify (ast as Ast.Constant _) = ast
wenzelm@42242
   414
      | constify (ast as Ast.Variable x) =
wenzelm@42298
   415
          if is_some (Syntax.lookup_const syn x) orelse Long_Name.is_qualified x
wenzelm@42298
   416
          then Ast.Constant x
wenzelm@42242
   417
          else ast
wenzelm@42242
   418
      | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
wenzelm@42242
   419
wenzelm@42242
   420
    val (syms, pos) = Syntax.read_token str;
wenzelm@42242
   421
  in
wenzelm@42242
   422
    parse_asts ctxt true root (syms, pos)
wenzelm@46512
   423
    |> uncurry (report_result ctxt pos)
wenzelm@42242
   424
    |> constify
wenzelm@42242
   425
  end;
wenzelm@42242
   426
wenzelm@42242
   427
wenzelm@42242
   428
wenzelm@42245
   429
(** encode parse trees **)
wenzelm@42245
   430
wenzelm@42245
   431
(* term_of_sort *)
wenzelm@42245
   432
wenzelm@42245
   433
fun term_of_sort S =
wenzelm@42245
   434
  let
wenzelm@42476
   435
    val class = Syntax.const o Lexicon.mark_class;
wenzelm@42245
   436
wenzelm@42245
   437
    fun classes [c] = class c
wenzelm@42476
   438
      | classes (c :: cs) = Syntax.const "_classes" $ class c $ classes cs;
wenzelm@42245
   439
  in
wenzelm@42245
   440
    (case S of
wenzelm@42476
   441
      [] => Syntax.const "_topsort"
wenzelm@42245
   442
    | [c] => class c
wenzelm@42476
   443
    | cs => Syntax.const "_sort" $ classes cs)
wenzelm@42245
   444
  end;
wenzelm@42245
   445
wenzelm@42245
   446
wenzelm@42245
   447
(* term_of_typ *)
wenzelm@42245
   448
wenzelm@42247
   449
fun term_of_typ ctxt ty =
wenzelm@42245
   450
  let
wenzelm@49690
   451
    val show_sort_constraint = Printer.show_sort_constraint ctxt;
wenzelm@42247
   452
wenzelm@49686
   453
    fun ofsort t raw_S =
wenzelm@49690
   454
      if show_sort_constraint then
wenzelm@49686
   455
        let val S = #2 (Term_Position.decode_positionS raw_S)
wenzelm@49686
   456
        in if S = dummyS then t else Syntax.const "_ofsort" $ t $ term_of_sort S end
wenzelm@42245
   457
      else t;
wenzelm@42245
   458
wenzelm@42245
   459
    fun term_of (Type (a, Ts)) =
wenzelm@42476
   460
          Term.list_comb (Syntax.const (Lexicon.mark_type a), map term_of Ts)
wenzelm@42245
   461
      | term_of (TFree (x, S)) =
wenzelm@42290
   462
          if is_some (Term_Position.decode x) then Syntax.free x
wenzelm@49686
   463
          else ofsort (Syntax.const "_tfree" $ Syntax.free x) S
wenzelm@49686
   464
      | term_of (TVar (xi, S)) = ofsort (Syntax.const "_tvar" $ Syntax.var xi) S;
wenzelm@42245
   465
  in term_of ty end;
wenzelm@42245
   466
wenzelm@42245
   467
wenzelm@42245
   468
(* simple_ast_of *)
wenzelm@42245
   469
wenzelm@42245
   470
fun simple_ast_of ctxt =
wenzelm@42245
   471
  let
wenzelm@42245
   472
    val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?";
wenzelm@42245
   473
    fun ast_of (Const (c, _)) = Ast.Constant c
wenzelm@42245
   474
      | ast_of (Free (x, _)) = Ast.Variable x
wenzelm@42245
   475
      | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi))
wenzelm@42245
   476
      | ast_of (t as _ $ _) =
wenzelm@42245
   477
          let val (f, args) = strip_comb t
wenzelm@42245
   478
          in Ast.mk_appl (ast_of f) (map ast_of args) end
wenzelm@42408
   479
      | ast_of (Bound i) = Ast.Appl [Ast.Constant "_loose", Ast.Variable ("B." ^ string_of_int i)]
wenzelm@42245
   480
      | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
wenzelm@42245
   481
  in ast_of end;
wenzelm@42245
   482
wenzelm@42245
   483
wenzelm@42245
   484
(* sort_to_ast and typ_to_ast *)
wenzelm@42245
   485
wenzelm@42245
   486
fun ast_of_termT ctxt trf tm =
wenzelm@42245
   487
  let
wenzelm@42245
   488
    val ctxt' = Config.put show_sorts false ctxt;
wenzelm@42245
   489
    fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
wenzelm@42245
   490
      | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
wenzelm@42245
   491
      | ast_of (Const (a, _)) = trans a []
wenzelm@42245
   492
      | ast_of (t as _ $ _) =
wenzelm@42245
   493
          (case strip_comb t of
wenzelm@42245
   494
            (Const (a, _), args) => trans a args
wenzelm@42245
   495
          | (f, args) => Ast.Appl (map ast_of (f :: args)))
wenzelm@42245
   496
      | ast_of t = simple_ast_of ctxt t
wenzelm@42254
   497
    and trans a args = ast_of (trf a ctxt' dummyT args)
wenzelm@42254
   498
      handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
wenzelm@42245
   499
  in ast_of tm end;
wenzelm@42245
   500
wenzelm@42245
   501
fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (term_of_sort S);
wenzelm@42247
   502
fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ ctxt T);
wenzelm@42245
   503
wenzelm@42245
   504
wenzelm@42245
   505
(* term_to_ast *)
wenzelm@42245
   506
wenzelm@42252
   507
fun term_to_ast idents is_syntax_const ctxt trf tm =
wenzelm@42245
   508
  let
wenzelm@42245
   509
    val show_types =
wenzelm@42245
   510
      Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
wenzelm@42245
   511
      Config.get ctxt show_all_types;
wenzelm@42245
   512
    val show_structs = Config.get ctxt show_structs;
wenzelm@42245
   513
    val show_free_types = Config.get ctxt show_free_types;
wenzelm@42245
   514
    val show_all_types = Config.get ctxt show_all_types;
wenzelm@49657
   515
    val show_markup = Config.get ctxt show_markup;
wenzelm@42245
   516
wenzelm@42245
   517
    val {structs, fixes} = idents;
wenzelm@42245
   518
wenzelm@42249
   519
    fun mark_atoms ((t as Const (c, _)) $ u) =
wenzelm@42294
   520
          if member (op =) Syntax.token_markers c
wenzelm@42245
   521
          then t $ u else mark_atoms t $ mark_atoms u
wenzelm@42245
   522
      | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
wenzelm@42245
   523
      | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
wenzelm@42245
   524
      | mark_atoms (t as Const (c, T)) =
wenzelm@42252
   525
          if is_syntax_const c then t
wenzelm@42245
   526
          else Const (Lexicon.mark_const c, T)
wenzelm@42245
   527
      | mark_atoms (t as Free (x, T)) =
wenzelm@42245
   528
          let val i = find_index (fn s => s = x) structs + 1 in
wenzelm@42245
   529
            if i = 0 andalso member (op =) fixes x then
wenzelm@42245
   530
              Const (Lexicon.mark_fixed x, T)
wenzelm@42245
   531
            else if i = 1 andalso not show_structs then
wenzelm@42476
   532
              Syntax.const "_struct" $ Syntax.const "_indexdefault"
wenzelm@42476
   533
            else Syntax.const "_free" $ t
wenzelm@42245
   534
          end
wenzelm@42245
   535
      | mark_atoms (t as Var (xi, T)) =
wenzelm@42288
   536
          if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T)
wenzelm@42476
   537
          else Syntax.const "_var" $ t
wenzelm@42245
   538
      | mark_atoms a = a;
wenzelm@42245
   539
wenzelm@42245
   540
    fun prune_typs (t_seen as (Const _, _)) = t_seen
wenzelm@42245
   541
      | prune_typs (t as Free (x, ty), seen) =
wenzelm@42245
   542
          if ty = dummyT then (t, seen)
wenzelm@42290
   543
          else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen)
wenzelm@42245
   544
          else (t, t :: seen)
wenzelm@42245
   545
      | prune_typs (t as Var (xi, ty), seen) =
wenzelm@42245
   546
          if ty = dummyT then (t, seen)
wenzelm@42290
   547
          else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen)
wenzelm@42245
   548
          else (t, t :: seen)
wenzelm@42245
   549
      | prune_typs (t_seen as (Bound _, _)) = t_seen
wenzelm@42245
   550
      | prune_typs (Abs (x, ty, t), seen) =
wenzelm@42245
   551
          let val (t', seen') = prune_typs (t, seen);
wenzelm@42245
   552
          in (Abs (x, ty, t'), seen') end
wenzelm@42245
   553
      | prune_typs (t1 $ t2, seen) =
wenzelm@42245
   554
          let
wenzelm@42245
   555
            val (t1', seen') = prune_typs (t1, seen);
wenzelm@42245
   556
            val (t2', seen'') = prune_typs (t2, seen');
wenzelm@42245
   557
          in (t1' $ t2', seen'') end;
wenzelm@42245
   558
wenzelm@42245
   559
    fun ast_of tm =
wenzelm@42245
   560
      (case strip_comb tm of
wenzelm@42284
   561
        (t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts)
wenzelm@42245
   562
      | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
wenzelm@42290
   563
          Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
wenzelm@42245
   564
      | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
wenzelm@42290
   565
          Ast.mk_appl (constrain (c $ Syntax.var xi) T) (map ast_of ts)
wenzelm@49660
   566
      | ((c as Const ("_bound", B)), Free (x, T) :: ts) =>
wenzelm@49660
   567
          let
wenzelm@49660
   568
            val X =
wenzelm@49660
   569
              if show_markup andalso not show_types orelse B <> dummyT then T
wenzelm@49660
   570
              else dummyT;
wenzelm@49660
   571
          in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end
wenzelm@42245
   572
      | (Const ("_idtdummy", T), ts) =>
wenzelm@42476
   573
          Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
wenzelm@42245
   574
      | (const as Const (c, T), ts) =>
wenzelm@42245
   575
          if show_all_types
wenzelm@42245
   576
          then Ast.mk_appl (constrain const T) (map ast_of ts)
wenzelm@42245
   577
          else trans c T ts
wenzelm@42245
   578
      | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
wenzelm@42245
   579
wenzelm@42254
   580
    and trans a T args = ast_of (trf a ctxt T args)
wenzelm@42254
   581
      handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
wenzelm@42245
   582
wenzelm@42245
   583
    and constrain t T =
wenzelm@49657
   584
      if (show_types orelse show_markup) andalso T <> dummyT then
wenzelm@42248
   585
        Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t,
wenzelm@42247
   586
          ast_of_termT ctxt trf (term_of_typ ctxt T)]
wenzelm@42245
   587
      else simple_ast_of ctxt t;
wenzelm@42245
   588
  in
wenzelm@42245
   589
    tm
wenzelm@42284
   590
    |> Syntax_Trans.prop_tr'
wenzelm@49659
   591
    |> show_types ? (#1 o prune_typs o rpair [])
wenzelm@42245
   592
    |> mark_atoms
wenzelm@42245
   593
    |> ast_of
wenzelm@42245
   594
  end;
wenzelm@42245
   595
wenzelm@42245
   596
wenzelm@42245
   597
wenzelm@42242
   598
(** unparse **)
wenzelm@42242
   599
wenzelm@42245
   600
local
wenzelm@42245
   601
wenzelm@42267
   602
fun free_or_skolem ctxt x =
wenzelm@42267
   603
  let
wenzelm@42267
   604
    val m =
wenzelm@42267
   605
      if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
wenzelm@50201
   606
      then Markup.fixed x else Markup.intensify;
wenzelm@42267
   607
  in
wenzelm@42267
   608
    if can Name.dest_skolem x
wenzelm@50201
   609
    then ([m, Markup.skolem], Variable.revert_fixed ctxt x)
wenzelm@50201
   610
    else ([m, Markup.free], x)
wenzelm@42267
   611
  end;
wenzelm@42267
   612
wenzelm@42267
   613
fun var_or_skolem s =
wenzelm@42267
   614
  (case Lexicon.read_variable s of
wenzelm@42267
   615
    SOME (x, i) =>
wenzelm@42267
   616
      (case try Name.dest_skolem x of
wenzelm@50201
   617
        NONE => (Markup.var, s)
wenzelm@50201
   618
      | SOME x' => (Markup.skolem, Term.string_of_vname (x', i)))
wenzelm@50201
   619
  | NONE => (Markup.var, s));
wenzelm@42267
   620
wenzelm@50201
   621
val typing_elem = YXML.output_markup_elem Markup.typing;
wenzelm@50201
   622
val sorting_elem = YXML.output_markup_elem Markup.sorting;
wenzelm@49657
   623
wenzelm@42267
   624
fun unparse_t t_to_ast prt_t markup ctxt t =
wenzelm@42245
   625
  let
wenzelm@49686
   626
    val show_markup = Config.get ctxt show_markup;
wenzelm@49686
   627
    val show_sorts = Config.get ctxt show_sorts;
wenzelm@49659
   628
    val show_types =
wenzelm@49686
   629
      Config.get ctxt show_types orelse show_sorts orelse
wenzelm@49659
   630
      Config.get ctxt show_all_types;
wenzelm@49657
   631
wenzelm@42360
   632
    val syn = Proof_Context.syn_of ctxt;
wenzelm@49657
   633
    val prtabs = Syntax.prtabs syn;
wenzelm@49657
   634
    val trf = Syntax.print_ast_translation syn;
wenzelm@49657
   635
wenzelm@49657
   636
    fun markup_extern c =
wenzelm@49657
   637
      (case Syntax.lookup_const syn c of
wenzelm@49657
   638
        SOME "" => ([], c)
wenzelm@49657
   639
      | SOME b => markup_extern b
wenzelm@49657
   640
      | NONE => c |> Lexicon.unmark
wenzelm@49657
   641
         {case_class = fn x => (markup_class ctxt x, Proof_Context.extern_class ctxt x),
wenzelm@49657
   642
          case_type = fn x => (markup_type ctxt x, Proof_Context.extern_type ctxt x),
wenzelm@49657
   643
          case_const = fn x => (markup_const ctxt x, Proof_Context.extern_const ctxt x),
wenzelm@49657
   644
          case_fixed = fn x => free_or_skolem ctxt x,
wenzelm@49657
   645
          case_default = fn x => ([], x)});
wenzelm@42267
   646
wenzelm@50201
   647
    fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x))
wenzelm@50201
   648
      | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
wenzelm@42267
   649
      | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
wenzelm@50201
   650
      | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x))
wenzelm@50201
   651
      | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.bad, x))
wenzelm@42267
   652
      | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
wenzelm@50201
   653
      | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x))
wenzelm@50201
   654
      | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x))
wenzelm@42267
   655
      | token_trans _ _ = NONE;
wenzelm@42267
   656
wenzelm@49655
   657
    fun markup_trans a [Ast.Variable x] = token_trans a x
wenzelm@49662
   658
      | markup_trans "_constrain" [t, ty] = constrain_trans t ty
wenzelm@49662
   659
      | markup_trans "_idtyp" [t, ty] = constrain_trans t ty
wenzelm@49686
   660
      | markup_trans "_ofsort" [ty, s] = ofsort_trans ty s
wenzelm@49657
   661
      | markup_trans _ _ = NONE
wenzelm@49655
   662
wenzelm@49662
   663
    and constrain_trans t ty =
wenzelm@49686
   664
      if show_markup andalso not show_types then
wenzelm@49662
   665
        let
wenzelm@49662
   666
          val ((bg1, bg2), en) = typing_elem;
wenzelm@49662
   667
          val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty ty) ^ bg2;
wenzelm@49662
   668
        in SOME (Pretty.raw_markup (bg, en) (0, [pretty_ast Markup.empty t])) end
wenzelm@49662
   669
      else NONE
wenzelm@49662
   670
wenzelm@49686
   671
    and ofsort_trans ty s =
wenzelm@49686
   672
      if show_markup andalso not show_sorts then
wenzelm@49686
   673
        let
wenzelm@49686
   674
          val ((bg1, bg2), en) = sorting_elem;
wenzelm@49686
   675
          val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty s) ^ bg2;
wenzelm@49686
   676
        in SOME (Pretty.raw_markup (bg, en) (0, [pretty_typ_ast Markup.empty ty])) end
wenzelm@49686
   677
      else NONE
wenzelm@49686
   678
wenzelm@49657
   679
    and pretty_typ_ast m ast = ast
wenzelm@49657
   680
      |> Printer.pretty_typ_ast ctxt prtabs trf markup_trans markup_extern
wenzelm@49657
   681
      |> Pretty.markup m
wenzelm@49657
   682
wenzelm@49657
   683
    and pretty_ast m ast = ast
wenzelm@49657
   684
      |> prt_t ctxt prtabs trf markup_trans markup_extern
wenzelm@49657
   685
      |> Pretty.markup m;
wenzelm@42245
   686
  in
wenzelm@42255
   687
    t_to_ast ctxt (Syntax.print_translation syn) t
wenzelm@42255
   688
    |> Ast.normalize ctxt (Syntax.print_rules syn)
wenzelm@49657
   689
    |> pretty_ast markup
wenzelm@42245
   690
  end;
wenzelm@42245
   691
wenzelm@42245
   692
in
wenzelm@42245
   693
wenzelm@50201
   694
val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.sort;
wenzelm@50201
   695
val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.typ;
wenzelm@42241
   696
wenzelm@42241
   697
fun unparse_term ctxt =
wenzelm@42241
   698
  let
wenzelm@42360
   699
    val thy = Proof_Context.theory_of ctxt;
wenzelm@42360
   700
    val syn = Proof_Context.syn_of ctxt;
wenzelm@42360
   701
    val idents = Local_Syntax.idents_of (Proof_Context.syntax_of ctxt);
wenzelm@42241
   702
  in
wenzelm@42298
   703
    unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn))
wenzelm@42267
   704
      (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
wenzelm@50201
   705
      Markup.term ctxt
wenzelm@42241
   706
  end;
wenzelm@42241
   707
wenzelm@42249
   708
end;
wenzelm@42249
   709
wenzelm@42241
   710
wenzelm@42245
   711
wenzelm@42245
   712
(** translations **)
wenzelm@42245
   713
wenzelm@42245
   714
(* type propositions *)
wenzelm@42245
   715
wenzelm@42247
   716
fun type_prop_tr' ctxt T [Const ("\\<^const>Pure.sort_constraint", _)] =
wenzelm@42476
   717
      Syntax.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T
wenzelm@42247
   718
  | type_prop_tr' ctxt T [t] =
wenzelm@42476
   719
      Syntax.const "_ofclass" $ term_of_typ ctxt T $ t
wenzelm@42245
   720
  | type_prop_tr' _ T ts = raise TYPE ("type_prop_tr'", [T], ts);
wenzelm@42245
   721
wenzelm@42245
   722
wenzelm@42245
   723
(* type reflection *)
wenzelm@42245
   724
wenzelm@42247
   725
fun type_tr' ctxt (Type ("itself", [T])) ts =
wenzelm@42476
   726
      Term.list_comb (Syntax.const "_TYPE" $ term_of_typ ctxt T, ts)
wenzelm@42245
   727
  | type_tr' _ _ _ = raise Match;
wenzelm@42245
   728
wenzelm@42245
   729
wenzelm@42245
   730
(* type constraints *)
wenzelm@42245
   731
wenzelm@42247
   732
fun type_constraint_tr' ctxt (Type ("fun", [T, _])) (t :: ts) =
wenzelm@42476
   733
      Term.list_comb (Syntax.const "_constrain" $ t $ term_of_typ ctxt T, ts)
wenzelm@42245
   734
  | type_constraint_tr' _ _ _ = raise Match;
wenzelm@42245
   735
wenzelm@42245
   736
wenzelm@42295
   737
(* authentic syntax *)
wenzelm@42295
   738
wenzelm@42295
   739
fun const_ast_tr intern ctxt [Ast.Variable c] =
wenzelm@42295
   740
      let
wenzelm@42360
   741
        val Const (c', _) = Proof_Context.read_const_proper ctxt false c;
wenzelm@42295
   742
        val d = if intern then Lexicon.mark_const c' else c;
wenzelm@42295
   743
      in Ast.Constant d end
wenzelm@42470
   744
  | const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T as Ast.Variable pos]] =
wenzelm@42470
   745
      (Ast.Appl [Ast.Constant "_constrain", const_ast_tr intern ctxt [x], T]
wenzelm@42470
   746
        handle ERROR msg =>
wenzelm@48992
   747
          error (msg ^ Position.here (the_default Position.none (Term_Position.decode pos))))
wenzelm@42295
   748
  | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
wenzelm@42295
   749
wenzelm@42295
   750
wenzelm@42245
   751
(* setup translations *)
wenzelm@42245
   752
wenzelm@42245
   753
val _ = Context.>> (Context.map_theory
wenzelm@42295
   754
 (Sign.add_advanced_trfuns
wenzelm@42295
   755
  ([("_context_const", const_ast_tr true),
wenzelm@42295
   756
    ("_context_xconst", const_ast_tr false)], [], [], []) #>
wenzelm@42295
   757
  Sign.add_advanced_trfunsT
wenzelm@42245
   758
   [("_type_prop", type_prop_tr'),
wenzelm@42245
   759
    ("\\<^const>TYPE", type_tr'),
wenzelm@42245
   760
    ("_type_constraint_", type_constraint_tr')]));
wenzelm@42245
   761
wenzelm@42245
   762
wenzelm@42245
   763
wenzelm@42382
   764
(** check/uncheck **)
wenzelm@42382
   765
wenzelm@45429
   766
(* context-sensitive (un)checking *)
wenzelm@45429
   767
wenzelm@45429
   768
type key = int * bool;
wenzelm@45429
   769
wenzelm@45429
   770
structure Checks = Generic_Data
wenzelm@45429
   771
(
wenzelm@45429
   772
  type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
wenzelm@45429
   773
  type T =
wenzelm@45429
   774
    ((key * ((string * typ check) * stamp) list) list *
wenzelm@45429
   775
     (key * ((string * term check) * stamp) list) list);
wenzelm@45429
   776
  val empty = ([], []);
wenzelm@45429
   777
  val extend = I;
wenzelm@45429
   778
  fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
wenzelm@45429
   779
    (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2),
wenzelm@45429
   780
     AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
wenzelm@45429
   781
);
wenzelm@45429
   782
wenzelm@45429
   783
fun print_checks ctxt =
wenzelm@45429
   784
  let
wenzelm@45429
   785
    fun split_checks checks =
wenzelm@45429
   786
      List.partition (fn ((_, un), _) => not un) checks
wenzelm@45429
   787
      |> pairself (map (fn ((i, _), fs) => (i, map (fst o fst) fs))
wenzelm@45429
   788
          #> sort (int_ord o pairself fst));
wenzelm@45429
   789
    fun pretty_checks kind checks =
wenzelm@45429
   790
      checks |> map (fn (i, names) => Pretty.block
wenzelm@45429
   791
        [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"),
wenzelm@45429
   792
          Pretty.brk 1, Pretty.strs names]);
wenzelm@45429
   793
wenzelm@45429
   794
    val (typs, terms) = Checks.get (Context.Proof ctxt);
wenzelm@45429
   795
    val (typ_checks, typ_unchecks) = split_checks typs;
wenzelm@45429
   796
    val (term_checks, term_unchecks) = split_checks terms;
wenzelm@45429
   797
  in
wenzelm@45429
   798
    pretty_checks "typ_checks" typ_checks @
wenzelm@45429
   799
    pretty_checks "term_checks" term_checks @
wenzelm@45429
   800
    pretty_checks "typ_unchecks" typ_unchecks @
wenzelm@45429
   801
    pretty_checks "term_unchecks" term_unchecks
wenzelm@45429
   802
  end |> Pretty.chunks |> Pretty.writeln;
wenzelm@45429
   803
wenzelm@45429
   804
wenzelm@45429
   805
local
wenzelm@45429
   806
wenzelm@45429
   807
fun context_check which (key: key) name f =
wenzelm@45429
   808
  Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
wenzelm@45429
   809
wenzelm@45429
   810
fun simple_check eq f xs ctxt =
wenzelm@45429
   811
  let val xs' = f ctxt xs
wenzelm@45429
   812
  in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end;
wenzelm@45429
   813
wenzelm@45429
   814
in
wenzelm@45429
   815
wenzelm@45444
   816
fun typ_check' stage = context_check apfst (stage, false);
wenzelm@45444
   817
fun term_check' stage = context_check apsnd (stage, false);
wenzelm@45444
   818
fun typ_uncheck' stage = context_check apfst (stage, true);
wenzelm@45444
   819
fun term_uncheck' stage = context_check apsnd (stage, true);
wenzelm@45429
   820
wenzelm@45444
   821
fun typ_check key name f = typ_check' key name (simple_check (op =) f);
wenzelm@45444
   822
fun term_check key name f = term_check' key name (simple_check (op aconv) f);
wenzelm@45444
   823
fun typ_uncheck key name f = typ_uncheck' key name (simple_check (op =) f);
wenzelm@45444
   824
fun term_uncheck key name f = term_uncheck' key name (simple_check (op aconv) f);
wenzelm@45429
   825
wenzelm@45429
   826
end;
wenzelm@45429
   827
wenzelm@45429
   828
wenzelm@45429
   829
local
wenzelm@45429
   830
wenzelm@45429
   831
fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
wenzelm@45429
   832
fun check_all fs = perhaps_apply (map check_stage fs);
wenzelm@45429
   833
wenzelm@45429
   834
fun check which uncheck ctxt0 xs0 =
wenzelm@45429
   835
  let
wenzelm@45429
   836
    val funs = which (Checks.get (Context.Proof ctxt0))
wenzelm@45429
   837
      |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
wenzelm@45429
   838
      |> Library.sort (int_ord o pairself fst) |> map snd
wenzelm@45429
   839
      |> not uncheck ? map rev;
wenzelm@45429
   840
  in #1 (perhaps (check_all funs) (xs0, ctxt0)) end;
wenzelm@45429
   841
wenzelm@45429
   842
val apply_typ_check = check fst false;
wenzelm@45429
   843
val apply_term_check = check snd false;
wenzelm@45429
   844
val apply_typ_uncheck = check fst true;
wenzelm@45429
   845
val apply_term_uncheck = check snd true;
wenzelm@45429
   846
wenzelm@45429
   847
in
wenzelm@45429
   848
wenzelm@49674
   849
fun check_typs ctxt raw_tys =
wenzelm@49674
   850
  let
wenzelm@49674
   851
    val (sorting_report, tys) = Proof_Context.prepare_sortsT ctxt raw_tys;
wenzelm@49674
   852
    val _ = Context_Position.if_visible ctxt Output.report sorting_report;
wenzelm@49674
   853
  in
wenzelm@49674
   854
    tys
wenzelm@49674
   855
    |> apply_typ_check ctxt
wenzelm@49674
   856
    |> Term_Sharing.typs (Proof_Context.theory_of ctxt)
wenzelm@49674
   857
  end;
wenzelm@45423
   858
wenzelm@45445
   859
fun check_terms ctxt raw_ts =
wenzelm@45445
   860
  let
wenzelm@49674
   861
    val (sorting_report, raw_ts') = Proof_Context.prepare_sorts ctxt raw_ts;
wenzelm@49674
   862
    val (ts, ps) = Type_Infer_Context.prepare_positions ctxt raw_ts';
wenzelm@49674
   863
wenzelm@45445
   864
    val tys = map (Logic.mk_type o snd) ps;
wenzelm@45448
   865
    val (ts', tys') = ts @ tys
wenzelm@45445
   866
      |> apply_term_check ctxt
wenzelm@45445
   867
      |> chop (length ts);
wenzelm@49674
   868
    val typing_report =
wenzelm@49674
   869
      fold2 (fn (pos, _) => fn ty =>
wenzelm@45445
   870
        if Position.is_reported pos then
wenzelm@50201
   871
          cons (Position.reported_text pos Markup.typing
wenzelm@49674
   872
            (Syntax.string_of_typ ctxt (Logic.dest_type ty)))
wenzelm@49674
   873
        else I) ps tys' []
wenzelm@49674
   874
      |> implode;
wenzelm@49674
   875
wenzelm@49674
   876
    val _ = Context_Position.if_visible ctxt Output.report (sorting_report ^ typing_report);
wenzelm@45445
   877
  in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end;
wenzelm@45423
   878
wenzelm@42382
   879
fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
wenzelm@42382
   880
wenzelm@45429
   881
val uncheck_typs = apply_typ_uncheck;
wenzelm@45429
   882
val uncheck_terms = apply_term_uncheck;
wenzelm@45429
   883
wenzelm@45429
   884
end;
wenzelm@45429
   885
wenzelm@45429
   886
wenzelm@45429
   887
(* standard phases *)
wenzelm@45429
   888
wenzelm@45429
   889
val _ = Context.>>
wenzelm@45429
   890
 (typ_check 0 "standard" Proof_Context.standard_typ_check #>
wenzelm@45429
   891
  term_check 0 "standard"
wenzelm@45429
   892
    (fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #>
wenzelm@45429
   893
  term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #>
wenzelm@45429
   894
  term_uncheck 0 "standard" Proof_Context.standard_term_uncheck);
wenzelm@42382
   895
wenzelm@42382
   896
wenzelm@42382
   897
wenzelm@42242
   898
(** install operations **)
wenzelm@42242
   899
wenzelm@42241
   900
val _ = Syntax.install_operations
wenzelm@42241
   901
  {parse_sort = parse_sort,
wenzelm@42241
   902
   parse_typ = parse_typ,
wenzelm@42281
   903
   parse_term = parse_term false,
wenzelm@42281
   904
   parse_prop = parse_term true,
wenzelm@42241
   905
   unparse_sort = unparse_sort,
wenzelm@42241
   906
   unparse_typ = unparse_typ,
wenzelm@42382
   907
   unparse_term = unparse_term,
wenzelm@42382
   908
   check_typs = check_typs,
wenzelm@42382
   909
   check_terms = check_terms,
wenzelm@42382
   910
   check_props = check_props,
wenzelm@42382
   911
   uncheck_typs = uncheck_typs,
wenzelm@42382
   912
   uncheck_terms = uncheck_terms};
wenzelm@42241
   913
wenzelm@42241
   914
end;