src/Pure/Syntax/syntax_phases.ML
author wenzelm
Wed Nov 09 17:57:42 2011 +0100 (2011-11-09)
changeset 45427 fca432074fb2
parent 45423 92f91f990165
child 45429 fd58cbf8cae3
permissions -rw-r--r--
sort assignment before simultaneous term_check, not isolated parse_term;
prefer Syntax.read_typ over Syntax.parse_typ, to include check phase for sort assignment;
simplified Syntax_Phases.decode_sort/decode_typ;
discontinued unused Proof_Context.check_tvar;
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@42242
    16
end
wenzelm@42242
    17
wenzelm@42243
    18
structure Syntax_Phases: SYNTAX_PHASES =
wenzelm@42241
    19
struct
wenzelm@42241
    20
wenzelm@42298
    21
(** markup logical entities **)
wenzelm@42298
    22
wenzelm@42298
    23
fun markup_class ctxt c =
wenzelm@42379
    24
  [Name_Space.markup (Type.class_space (Proof_Context.tsig_of ctxt)) c];
wenzelm@42298
    25
wenzelm@42298
    26
fun markup_type ctxt c =
wenzelm@42379
    27
  [Name_Space.markup (Type.type_space (Proof_Context.tsig_of ctxt)) c];
wenzelm@42298
    28
wenzelm@42298
    29
fun markup_const ctxt c =
wenzelm@42379
    30
  [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c];
wenzelm@42298
    31
wenzelm@42298
    32
fun markup_free ctxt x =
wenzelm@42298
    33
  [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
wenzelm@42493
    34
  (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x
wenzelm@42493
    35
   then [Variable.markup_fixed ctxt x]
wenzelm@42493
    36
   else []);
wenzelm@42298
    37
wenzelm@42298
    38
fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
wenzelm@42298
    39
wenzelm@45412
    40
fun markup_bound def ps (name, id) =
wenzelm@45412
    41
  let val entity = Markup.entity "bound variable" name in
wenzelm@45412
    42
    Markup.bound ::
wenzelm@45412
    43
      map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps
wenzelm@45412
    44
  end;
wenzelm@42298
    45
wenzelm@42298
    46
fun markup_entity ctxt c =
wenzelm@42360
    47
  (case Syntax.lookup_const (Proof_Context.syn_of ctxt) c of
wenzelm@42298
    48
    SOME "" => []
wenzelm@42298
    49
  | SOME b => markup_entity ctxt b
wenzelm@42298
    50
  | NONE => c |> Lexicon.unmark
wenzelm@42298
    51
     {case_class = markup_class ctxt,
wenzelm@42298
    52
      case_type = markup_type ctxt,
wenzelm@42298
    53
      case_const = markup_const ctxt,
wenzelm@42298
    54
      case_fixed = markup_free ctxt,
wenzelm@42298
    55
      case_default = K []});
wenzelm@42298
    56
wenzelm@42298
    57
wenzelm@42298
    58
wenzelm@42242
    59
(** decode parse trees **)
wenzelm@42242
    60
wenzelm@45427
    61
(* decode_sort *)
wenzelm@42242
    62
wenzelm@45427
    63
fun decode_sort tm =
wenzelm@42242
    64
  let
wenzelm@45427
    65
    fun err () = raise TERM ("decode_sort: bad encoding of classes", [tm]);
wenzelm@42242
    66
wenzelm@42242
    67
    fun class s = Lexicon.unmark_class s handle Fail _ => err ();
wenzelm@42242
    68
wenzelm@42242
    69
    fun classes (Const (s, _)) = [class s]
wenzelm@42242
    70
      | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
wenzelm@42242
    71
      | classes _ = err ();
wenzelm@42242
    72
wenzelm@42242
    73
    fun sort (Const ("_topsort", _)) = []
wenzelm@42242
    74
      | sort (Const (s, _)) = [class s]
wenzelm@42242
    75
      | sort (Const ("_sort", _) $ cs) = classes cs
wenzelm@42242
    76
      | sort _ = err ();
wenzelm@42242
    77
  in sort tm end;
wenzelm@42242
    78
wenzelm@42242
    79
wenzelm@45427
    80
(* decode_typ *)
wenzelm@42242
    81
wenzelm@45427
    82
fun decode_typ tm =
wenzelm@45427
    83
  let
wenzelm@45427
    84
    fun err () = raise TERM ("decode_typ: bad encoding of type", [tm]);
wenzelm@42242
    85
wenzelm@45427
    86
    fun typ (Free (x, _)) = TFree (x, dummyS)
wenzelm@45427
    87
      | typ (Var (xi, _)) = TVar (xi, dummyS)
wenzelm@45427
    88
      | typ (Const ("_tfree",_) $ (t as Free _)) = typ t
wenzelm@45427
    89
      | typ (Const ("_tvar",_) $ (t as Var _)) = typ t
wenzelm@45427
    90
      | typ (Const ("_ofsort", _) $ Free (x, _) $ s) = TFree (x, decode_sort s)
wenzelm@45427
    91
      | typ (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ s) =
wenzelm@45427
    92
          TFree (x, decode_sort s)
wenzelm@45427
    93
      | typ (Const ("_ofsort", _) $ Var (xi, _) $ s) = TVar (xi, decode_sort s)
wenzelm@45427
    94
      | typ (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ s) =
wenzelm@45427
    95
          TVar (xi, decode_sort s)
wenzelm@45427
    96
      | typ (Const ("_dummy_ofsort", _) $ s) = TFree ("'_dummy_", decode_sort s)
wenzelm@45427
    97
      | typ t =
wenzelm@42242
    98
          let
wenzelm@42242
    99
            val (head, args) = Term.strip_comb t;
wenzelm@42242
   100
            val a =
wenzelm@42242
   101
              (case head of
wenzelm@42242
   102
                Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
wenzelm@42242
   103
              | _ => err ());
wenzelm@45427
   104
          in Type (a, map typ args) end;
wenzelm@45427
   105
  in typ tm end;
wenzelm@42242
   106
wenzelm@42242
   107
wenzelm@42242
   108
(* parsetree_to_ast *)
wenzelm@42242
   109
wenzelm@42242
   110
fun parsetree_to_ast ctxt constrain_pos trf parsetree =
wenzelm@42242
   111
  let
wenzelm@44736
   112
    val reports = Unsynchronized.ref ([]: Position.report list);
wenzelm@44735
   113
    fun report pos = Position.store_reports reports [pos];
wenzelm@42242
   114
wenzelm@42242
   115
    fun trans a args =
wenzelm@42242
   116
      (case trf a of
wenzelm@42242
   117
        NONE => Ast.mk_appl (Ast.Constant a) args
wenzelm@42242
   118
      | SOME f => f ctxt args);
wenzelm@42242
   119
wenzelm@42282
   120
    fun asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
wenzelm@42242
   121
          let
wenzelm@42470
   122
            val pos = Lexicon.pos_of_token tok;
wenzelm@42470
   123
            val c = Proof_Context.read_class ctxt (Lexicon.str_of_token tok)
wenzelm@42470
   124
              handle ERROR msg => error (msg ^ Position.str_of pos);
wenzelm@42470
   125
            val _ = report pos (markup_class ctxt) c;
wenzelm@42282
   126
          in [Ast.Constant (Lexicon.mark_class c)] end
wenzelm@42282
   127
      | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
wenzelm@42242
   128
          let
wenzelm@42470
   129
            val pos = Lexicon.pos_of_token tok;
wenzelm@42470
   130
            val Type (c, _) =
wenzelm@42470
   131
              Proof_Context.read_type_name_proper ctxt false (Lexicon.str_of_token tok)
wenzelm@42470
   132
                handle ERROR msg => error (msg ^ Position.str_of pos);
wenzelm@42470
   133
            val _ = report pos (markup_type ctxt) c;
wenzelm@42282
   134
          in [Ast.Constant (Lexicon.mark_type c)] end
wenzelm@42410
   135
      | asts_of (Parser.Node ("_position", [pt as Parser.Tip tok])) =
wenzelm@42242
   136
          if constrain_pos then
wenzelm@42282
   137
            [Ast.Appl [Ast.Constant "_constrain", ast_of pt,
wenzelm@42282
   138
              Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]]
wenzelm@42282
   139
          else [ast_of pt]
wenzelm@42282
   140
      | asts_of (Parser.Node (a, pts)) =
wenzelm@42282
   141
          let
wenzelm@42282
   142
            val _ = pts |> List.app
wenzelm@42282
   143
              (fn Parser.Node _ => () | Parser.Tip tok =>
wenzelm@42282
   144
                if Lexicon.valued_token tok then ()
wenzelm@42298
   145
                else report (Lexicon.pos_of_token tok) (markup_entity ctxt) a);
wenzelm@42282
   146
          in [trans a (maps asts_of pts)] end
wenzelm@42282
   147
      | asts_of (Parser.Tip tok) =
wenzelm@42282
   148
          if Lexicon.valued_token tok
wenzelm@42282
   149
          then [Ast.Variable (Lexicon.str_of_token tok)]
wenzelm@42282
   150
          else []
wenzelm@42282
   151
wenzelm@42282
   152
    and ast_of pt =
wenzelm@42282
   153
      (case asts_of pt of
wenzelm@42282
   154
        [ast] => ast
wenzelm@42282
   155
      | asts => raise Ast.AST ("parsetree_to_ast: malformed parsetree", asts));
wenzelm@42242
   156
wenzelm@42242
   157
    val ast = Exn.interruptible_capture ast_of parsetree;
wenzelm@42242
   158
  in (! reports, ast) end;
wenzelm@42242
   159
wenzelm@42242
   160
wenzelm@42242
   161
(* ast_to_term *)
wenzelm@42242
   162
wenzelm@42242
   163
fun ast_to_term ctxt trf =
wenzelm@42242
   164
  let
wenzelm@42242
   165
    fun trans a args =
wenzelm@42242
   166
      (case trf a of
wenzelm@42476
   167
        NONE => Term.list_comb (Syntax.const a, args)
wenzelm@42242
   168
      | SOME f => f ctxt args);
wenzelm@42242
   169
wenzelm@42242
   170
    fun term_of (Ast.Constant a) = trans a []
wenzelm@42242
   171
      | term_of (Ast.Variable x) = Lexicon.read_var x
wenzelm@42242
   172
      | term_of (Ast.Appl (Ast.Constant a :: (asts as _ :: _))) =
wenzelm@42242
   173
          trans a (map term_of asts)
wenzelm@42242
   174
      | term_of (Ast.Appl (ast :: (asts as _ :: _))) =
wenzelm@42242
   175
          Term.list_comb (term_of ast, map term_of asts)
wenzelm@42242
   176
      | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
wenzelm@42242
   177
  in term_of end;
wenzelm@42242
   178
wenzelm@42242
   179
wenzelm@42242
   180
(* decode_term -- transform parse tree into raw term *)
wenzelm@42242
   181
wenzelm@44736
   182
fun decode_term _ (result as (_: Position.report list, Exn.Exn _)) = result
wenzelm@43761
   183
  | decode_term ctxt (reports0, Exn.Res tm) =
wenzelm@42242
   184
      let
wenzelm@42250
   185
        fun get_const a =
wenzelm@42360
   186
          ((true, #1 (Term.dest_Const (Proof_Context.read_const_proper ctxt false a)))
wenzelm@42360
   187
            handle ERROR _ => (false, Consts.intern (Proof_Context.consts_of ctxt) a));
wenzelm@42360
   188
        val get_free = Proof_Context.intern_skolem ctxt;
wenzelm@42250
   189
wenzelm@42242
   190
        val reports = Unsynchronized.ref reports0;
wenzelm@44735
   191
        fun report ps = Position.store_reports reports ps;
wenzelm@42242
   192
wenzelm@42242
   193
        fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
wenzelm@42264
   194
              (case Term_Position.decode_position typ of
wenzelm@42242
   195
                SOME p => decode (p :: ps) qs bs t
wenzelm@45427
   196
              | NONE => Type.constraint (decode_typ typ) (decode ps qs bs t))
wenzelm@42242
   197
          | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
wenzelm@42264
   198
              (case Term_Position.decode_position typ of
wenzelm@42242
   199
                SOME q => decode ps (q :: qs) bs t
wenzelm@45427
   200
              | NONE => Type.constraint (decode_typ typ --> dummyT) (decode ps qs bs t))
wenzelm@42242
   201
          | decode _ qs bs (Abs (x, T, t)) =
wenzelm@42242
   202
              let
wenzelm@45412
   203
                val id = serial ();
wenzelm@45412
   204
                val _ = report qs (markup_bound true qs) (x, id);
wenzelm@45412
   205
              in Abs (x, T, decode [] [] ((qs, (x, id)) :: bs) t) end
wenzelm@42242
   206
          | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
wenzelm@42242
   207
          | decode ps _ _ (Const (a, T)) =
wenzelm@42242
   208
              (case try Lexicon.unmark_fixed a of
wenzelm@42282
   209
                SOME x => (report ps (markup_free ctxt) x; Free (x, T))
wenzelm@42242
   210
              | NONE =>
wenzelm@42242
   211
                  let
wenzelm@42242
   212
                    val c =
wenzelm@42242
   213
                      (case try Lexicon.unmark_const a of
wenzelm@42242
   214
                        SOME c => c
wenzelm@42242
   215
                      | NONE => snd (get_const a));
wenzelm@42282
   216
                    val _ = report ps (markup_const ctxt) c;
wenzelm@42242
   217
                  in Const (c, T) end)
wenzelm@42242
   218
          | decode ps _ _ (Free (a, T)) =
wenzelm@42242
   219
              (case (get_free a, get_const a) of
wenzelm@42282
   220
                (SOME x, _) => (report ps (markup_free ctxt) x; Free (x, T))
wenzelm@42282
   221
              | (_, (true, c)) => (report ps (markup_const ctxt) c; Const (c, T))
wenzelm@42242
   222
              | (_, (false, c)) =>
wenzelm@42242
   223
                  if Long_Name.is_qualified c
wenzelm@42282
   224
                  then (report ps (markup_const ctxt) c; Const (c, T))
wenzelm@42282
   225
                  else (report ps (markup_free ctxt) c; Free (c, T)))
wenzelm@42242
   226
          | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
wenzelm@42242
   227
          | decode ps _ bs (t as Bound i) =
wenzelm@42242
   228
              (case try (nth bs) i of
wenzelm@45412
   229
                SOME (qs, (x, id)) => (report ps (markup_bound false qs) (x, id); t)
wenzelm@42242
   230
              | NONE => t);
wenzelm@42242
   231
wenzelm@42242
   232
        val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
wenzelm@42242
   233
      in (! reports, tm') end;
wenzelm@42242
   234
wenzelm@42242
   235
wenzelm@42242
   236
wenzelm@42242
   237
(** parse **)
wenzelm@42242
   238
wenzelm@42242
   239
(* results *)
wenzelm@42242
   240
wenzelm@42242
   241
fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
wenzelm@42242
   242
wenzelm@43761
   243
fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results;
wenzelm@42242
   244
fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
wenzelm@42242
   245
wenzelm@42242
   246
fun report_result ctxt pos results =
wenzelm@42242
   247
  (case (proper_results results, failed_results results) of
wenzelm@44736
   248
    ([], (reports, exn) :: _) => (Context_Position.reports ctxt reports; reraise exn)
wenzelm@44736
   249
  | ([(reports, x)], _) => (Context_Position.reports ctxt reports; x)
wenzelm@42242
   250
  | _ => error (ambiguity_msg pos));
wenzelm@42242
   251
wenzelm@42242
   252
wenzelm@42249
   253
(* parse raw asts *)
wenzelm@42242
   254
wenzelm@42242
   255
fun parse_asts ctxt raw root (syms, pos) =
wenzelm@42242
   256
  let
wenzelm@42360
   257
    val syn = Proof_Context.syn_of ctxt;
wenzelm@42253
   258
    val ast_tr = Syntax.parse_ast_translation syn;
wenzelm@42242
   259
wenzelm@42251
   260
    val toks = Syntax.tokenize syn raw syms;
wenzelm@44736
   261
    val _ = Context_Position.reports ctxt (map Lexicon.report_of_token toks);
wenzelm@42242
   262
wenzelm@42251
   263
    val pts = Syntax.parse ctxt syn root (filter Lexicon.is_proper toks)
wenzelm@42242
   264
      handle ERROR msg =>
wenzelm@42242
   265
        error (msg ^
wenzelm@42242
   266
          implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
wenzelm@42242
   267
    val len = length pts;
wenzelm@42242
   268
wenzelm@42242
   269
    val limit = Config.get ctxt Syntax.ambiguity_limit;
kleing@44069
   270
    val warnings = Config.get ctxt Syntax.ambiguity_warnings;
wenzelm@42242
   271
    val _ =
wenzelm@42242
   272
      if len <= Config.get ctxt Syntax.ambiguity_level then ()
wenzelm@42242
   273
      else if not (Config.get ctxt Syntax.ambiguity_enabled) then error (ambiguity_msg pos)
kleing@44069
   274
      else if warnings then
wenzelm@42242
   275
        (Context_Position.if_visible ctxt warning (cat_lines
wenzelm@44564
   276
          (("Ambiguous input" ^ Position.str_of (Position.reset_range pos) ^
wenzelm@42242
   277
            "\nproduces " ^ string_of_int len ^ " parse trees" ^
wenzelm@42242
   278
            (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
kleing@44069
   279
            map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))))
kleing@44069
   280
      else ();
wenzelm@42242
   281
wenzelm@42242
   282
    val constrain_pos = not raw andalso Config.get ctxt Syntax.positions;
wenzelm@42253
   283
    val parsetree_to_ast = parsetree_to_ast ctxt constrain_pos ast_tr;
wenzelm@42242
   284
  in map parsetree_to_ast pts end;
wenzelm@42242
   285
wenzelm@42249
   286
fun parse_raw ctxt root input =
wenzelm@42242
   287
  let
wenzelm@42360
   288
    val syn = Proof_Context.syn_of ctxt;
wenzelm@42253
   289
    val tr = Syntax.parse_translation syn;
wenzelm@42255
   290
    val parse_rules = Syntax.parse_rules syn;
wenzelm@42242
   291
  in
wenzelm@42242
   292
    parse_asts ctxt false root input
wenzelm@42255
   293
    |> (map o apsnd o Exn.maps_result)
wenzelm@42255
   294
        (Ast.normalize ctxt parse_rules #> Exn.interruptible_capture (ast_to_term ctxt tr))
wenzelm@42242
   295
  end;
wenzelm@42242
   296
wenzelm@42242
   297
wenzelm@42249
   298
(* parse logical entities *)
wenzelm@42242
   299
wenzelm@42241
   300
fun parse_failed ctxt pos msg kind =
wenzelm@42241
   301
  cat_error msg ("Failed to parse " ^ kind ^
wenzelm@42241
   302
    Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
wenzelm@42241
   303
wenzelm@43731
   304
fun parse_sort ctxt =
wenzelm@43731
   305
  Syntax.parse_token ctxt Term_XML.Decode.sort Markup.sort
wenzelm@43731
   306
    (fn (syms, pos) =>
wenzelm@42249
   307
      parse_raw ctxt "sort" (syms, pos)
wenzelm@42249
   308
      |> report_result ctxt pos
wenzelm@45427
   309
      |> decode_sort
wenzelm@43731
   310
      |> Type.minimize_sort (Proof_Context.tsig_of ctxt)
wenzelm@43731
   311
      handle ERROR msg => parse_failed ctxt pos msg "sort");
wenzelm@42241
   312
wenzelm@43731
   313
fun parse_typ ctxt =
wenzelm@43731
   314
  Syntax.parse_token ctxt Term_XML.Decode.typ Markup.typ
wenzelm@43731
   315
    (fn (syms, pos) =>
wenzelm@42249
   316
      parse_raw ctxt "type" (syms, pos)
wenzelm@42249
   317
      |> report_result ctxt pos
wenzelm@45427
   318
      |> decode_typ
wenzelm@43731
   319
      handle ERROR msg => parse_failed ctxt pos msg "type");
wenzelm@42241
   320
wenzelm@43731
   321
fun parse_term is_prop ctxt =
wenzelm@42241
   322
  let
wenzelm@42281
   323
    val (markup, kind, root, constrain) =
wenzelm@42281
   324
      if is_prop
wenzelm@42281
   325
      then (Markup.prop, "proposition", "prop", Type.constraint propT)
wenzelm@42288
   326
      else (Markup.term, "term", Config.get ctxt Syntax.root, I);
wenzelm@43731
   327
    val decode = constrain o Term_XML.Decode.term;
wenzelm@42249
   328
  in
wenzelm@43731
   329
    Syntax.parse_token ctxt decode markup
wenzelm@43731
   330
      (fn (syms, pos) =>
wenzelm@43731
   331
        let
wenzelm@43731
   332
          val results = parse_raw ctxt root (syms, pos) |> map (decode_term ctxt);
wenzelm@43731
   333
          val ambiguity = length (proper_results results);
wenzelm@42249
   334
wenzelm@43731
   335
          val level = Config.get ctxt Syntax.ambiguity_level;
wenzelm@43731
   336
          val limit = Config.get ctxt Syntax.ambiguity_limit;
kleing@44069
   337
          val warnings = Config.get ctxt Syntax.ambiguity_warnings;
wenzelm@42249
   338
wenzelm@43731
   339
          val ambig_msg =
wenzelm@43731
   340
            if ambiguity > 1 andalso ambiguity <= level then
wenzelm@43731
   341
              ["Got more than one parse tree.\n\
wenzelm@43731
   342
              \Retry with smaller syntax_ambiguity_level for more information."]
wenzelm@43731
   343
            else [];
wenzelm@43731
   344
wenzelm@43731
   345
          (*brute-force disambiguation via type-inference*)
wenzelm@43761
   346
          fun check t = (Syntax.check_term ctxt (constrain t); Exn.Res t)
wenzelm@43731
   347
            handle exn as ERROR _ => Exn.Exn exn;
wenzelm@42249
   348
wenzelm@43731
   349
          val results' =
wenzelm@43731
   350
            if ambiguity > 1 then
wenzelm@43731
   351
              (Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result)
wenzelm@43731
   352
                check results
wenzelm@43731
   353
            else results;
wenzelm@43731
   354
          val reports' = fst (hd results');
wenzelm@42249
   355
wenzelm@43731
   356
          val errs = map snd (failed_results results');
wenzelm@43731
   357
          val checked = map snd (proper_results results');
wenzelm@43731
   358
          val len = length checked;
wenzelm@42249
   359
wenzelm@43731
   360
          val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
wenzelm@43731
   361
        in
wenzelm@43731
   362
          if len = 0 then
wenzelm@43731
   363
            report_result ctxt pos
wenzelm@43731
   364
              [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))]
wenzelm@43731
   365
          else if len = 1 then
kleing@44069
   366
            (if ambiguity > level andalso warnings then
wenzelm@43731
   367
              Context_Position.if_visible ctxt warning
wenzelm@44564
   368
                ("Fortunately, only one parse tree is type correct" ^
wenzelm@44564
   369
                Position.str_of (Position.reset_range pos) ^
wenzelm@44564
   370
                ",\nbut you may still want to disambiguate your grammar or your input.")
wenzelm@43731
   371
            else (); report_result ctxt pos results')
wenzelm@43731
   372
          else
wenzelm@43731
   373
            report_result ctxt pos
wenzelm@43731
   374
              [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg @
wenzelm@43731
   375
                (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
wenzelm@43731
   376
                  (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
wenzelm@43731
   377
                  map show_term (take limit checked))))))]
wenzelm@43731
   378
        end handle ERROR msg => parse_failed ctxt pos msg kind)
wenzelm@42249
   379
  end;
wenzelm@42241
   380
wenzelm@42241
   381
wenzelm@42242
   382
(* parse_ast_pattern *)
wenzelm@42242
   383
wenzelm@42242
   384
fun parse_ast_pattern ctxt (root, str) =
wenzelm@42242
   385
  let
wenzelm@42360
   386
    val syn = Proof_Context.syn_of ctxt;
wenzelm@42242
   387
wenzelm@42242
   388
    fun constify (ast as Ast.Constant _) = ast
wenzelm@42242
   389
      | constify (ast as Ast.Variable x) =
wenzelm@42298
   390
          if is_some (Syntax.lookup_const syn x) orelse Long_Name.is_qualified x
wenzelm@42298
   391
          then Ast.Constant x
wenzelm@42242
   392
          else ast
wenzelm@42242
   393
      | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
wenzelm@42242
   394
wenzelm@42242
   395
    val (syms, pos) = Syntax.read_token str;
wenzelm@42242
   396
  in
wenzelm@42242
   397
    parse_asts ctxt true root (syms, pos)
wenzelm@42242
   398
    |> report_result ctxt pos
wenzelm@42242
   399
    |> constify
wenzelm@42242
   400
  end;
wenzelm@42242
   401
wenzelm@42242
   402
wenzelm@42242
   403
wenzelm@42245
   404
(** encode parse trees **)
wenzelm@42245
   405
wenzelm@42245
   406
(* term_of_sort *)
wenzelm@42245
   407
wenzelm@42245
   408
fun term_of_sort S =
wenzelm@42245
   409
  let
wenzelm@42476
   410
    val class = Syntax.const o Lexicon.mark_class;
wenzelm@42245
   411
wenzelm@42245
   412
    fun classes [c] = class c
wenzelm@42476
   413
      | classes (c :: cs) = Syntax.const "_classes" $ class c $ classes cs;
wenzelm@42245
   414
  in
wenzelm@42245
   415
    (case S of
wenzelm@42476
   416
      [] => Syntax.const "_topsort"
wenzelm@42245
   417
    | [c] => class c
wenzelm@42476
   418
    | cs => Syntax.const "_sort" $ classes cs)
wenzelm@42245
   419
  end;
wenzelm@42245
   420
wenzelm@42245
   421
wenzelm@42245
   422
(* term_of_typ *)
wenzelm@42245
   423
wenzelm@42247
   424
fun term_of_typ ctxt ty =
wenzelm@42245
   425
  let
wenzelm@42247
   426
    val show_sorts = Config.get ctxt show_sorts;
wenzelm@42247
   427
wenzelm@42245
   428
    fun of_sort t S =
wenzelm@42476
   429
      if show_sorts then Syntax.const "_ofsort" $ t $ term_of_sort S
wenzelm@42245
   430
      else t;
wenzelm@42245
   431
wenzelm@42245
   432
    fun term_of (Type (a, Ts)) =
wenzelm@42476
   433
          Term.list_comb (Syntax.const (Lexicon.mark_type a), map term_of Ts)
wenzelm@42245
   434
      | term_of (TFree (x, S)) =
wenzelm@42290
   435
          if is_some (Term_Position.decode x) then Syntax.free x
wenzelm@42476
   436
          else of_sort (Syntax.const "_tfree" $ Syntax.free x) S
wenzelm@42476
   437
      | term_of (TVar (xi, S)) = of_sort (Syntax.const "_tvar" $ Syntax.var xi) S;
wenzelm@42245
   438
  in term_of ty end;
wenzelm@42245
   439
wenzelm@42245
   440
wenzelm@42245
   441
(* simple_ast_of *)
wenzelm@42245
   442
wenzelm@42245
   443
fun simple_ast_of ctxt =
wenzelm@42245
   444
  let
wenzelm@42245
   445
    val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?";
wenzelm@42245
   446
    fun ast_of (Const (c, _)) = Ast.Constant c
wenzelm@42245
   447
      | ast_of (Free (x, _)) = Ast.Variable x
wenzelm@42245
   448
      | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi))
wenzelm@42245
   449
      | ast_of (t as _ $ _) =
wenzelm@42245
   450
          let val (f, args) = strip_comb t
wenzelm@42245
   451
          in Ast.mk_appl (ast_of f) (map ast_of args) end
wenzelm@42408
   452
      | ast_of (Bound i) = Ast.Appl [Ast.Constant "_loose", Ast.Variable ("B." ^ string_of_int i)]
wenzelm@42245
   453
      | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
wenzelm@42245
   454
  in ast_of end;
wenzelm@42245
   455
wenzelm@42245
   456
wenzelm@42245
   457
(* sort_to_ast and typ_to_ast *)
wenzelm@42245
   458
wenzelm@42245
   459
fun ast_of_termT ctxt trf tm =
wenzelm@42245
   460
  let
wenzelm@42245
   461
    val ctxt' = Config.put show_sorts false ctxt;
wenzelm@42245
   462
    fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
wenzelm@42245
   463
      | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
wenzelm@42245
   464
      | ast_of (Const (a, _)) = trans a []
wenzelm@42245
   465
      | ast_of (t as _ $ _) =
wenzelm@42245
   466
          (case strip_comb t of
wenzelm@42245
   467
            (Const (a, _), args) => trans a args
wenzelm@42245
   468
          | (f, args) => Ast.Appl (map ast_of (f :: args)))
wenzelm@42245
   469
      | ast_of t = simple_ast_of ctxt t
wenzelm@42254
   470
    and trans a args = ast_of (trf a ctxt' dummyT args)
wenzelm@42254
   471
      handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
wenzelm@42245
   472
  in ast_of tm end;
wenzelm@42245
   473
wenzelm@42245
   474
fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (term_of_sort S);
wenzelm@42247
   475
fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ ctxt T);
wenzelm@42245
   476
wenzelm@42245
   477
wenzelm@42245
   478
(* term_to_ast *)
wenzelm@42245
   479
wenzelm@42252
   480
fun term_to_ast idents is_syntax_const ctxt trf tm =
wenzelm@42245
   481
  let
wenzelm@42245
   482
    val show_types =
wenzelm@42245
   483
      Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
wenzelm@42245
   484
      Config.get ctxt show_all_types;
wenzelm@42245
   485
    val show_structs = Config.get ctxt show_structs;
wenzelm@42245
   486
    val show_free_types = Config.get ctxt show_free_types;
wenzelm@42245
   487
    val show_all_types = Config.get ctxt show_all_types;
wenzelm@42245
   488
wenzelm@42245
   489
    val {structs, fixes} = idents;
wenzelm@42245
   490
wenzelm@42249
   491
    fun mark_atoms ((t as Const (c, _)) $ u) =
wenzelm@42294
   492
          if member (op =) Syntax.token_markers c
wenzelm@42245
   493
          then t $ u else mark_atoms t $ mark_atoms u
wenzelm@42245
   494
      | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
wenzelm@42245
   495
      | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
wenzelm@42245
   496
      | mark_atoms (t as Const (c, T)) =
wenzelm@42252
   497
          if is_syntax_const c then t
wenzelm@42245
   498
          else Const (Lexicon.mark_const c, T)
wenzelm@42245
   499
      | mark_atoms (t as Free (x, T)) =
wenzelm@42245
   500
          let val i = find_index (fn s => s = x) structs + 1 in
wenzelm@42245
   501
            if i = 0 andalso member (op =) fixes x then
wenzelm@42245
   502
              Const (Lexicon.mark_fixed x, T)
wenzelm@42245
   503
            else if i = 1 andalso not show_structs then
wenzelm@42476
   504
              Syntax.const "_struct" $ Syntax.const "_indexdefault"
wenzelm@42476
   505
            else Syntax.const "_free" $ t
wenzelm@42245
   506
          end
wenzelm@42245
   507
      | mark_atoms (t as Var (xi, T)) =
wenzelm@42288
   508
          if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T)
wenzelm@42476
   509
          else Syntax.const "_var" $ t
wenzelm@42245
   510
      | mark_atoms a = a;
wenzelm@42245
   511
wenzelm@42245
   512
    fun prune_typs (t_seen as (Const _, _)) = t_seen
wenzelm@42245
   513
      | prune_typs (t as Free (x, ty), seen) =
wenzelm@42245
   514
          if ty = dummyT then (t, seen)
wenzelm@42290
   515
          else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen)
wenzelm@42245
   516
          else (t, t :: seen)
wenzelm@42245
   517
      | prune_typs (t as Var (xi, ty), seen) =
wenzelm@42245
   518
          if ty = dummyT then (t, seen)
wenzelm@42290
   519
          else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen)
wenzelm@42245
   520
          else (t, t :: seen)
wenzelm@42245
   521
      | prune_typs (t_seen as (Bound _, _)) = t_seen
wenzelm@42245
   522
      | prune_typs (Abs (x, ty, t), seen) =
wenzelm@42245
   523
          let val (t', seen') = prune_typs (t, seen);
wenzelm@42245
   524
          in (Abs (x, ty, t'), seen') end
wenzelm@42245
   525
      | prune_typs (t1 $ t2, seen) =
wenzelm@42245
   526
          let
wenzelm@42245
   527
            val (t1', seen') = prune_typs (t1, seen);
wenzelm@42245
   528
            val (t2', seen'') = prune_typs (t2, seen');
wenzelm@42245
   529
          in (t1' $ t2', seen'') end;
wenzelm@42245
   530
wenzelm@42245
   531
    fun ast_of tm =
wenzelm@42245
   532
      (case strip_comb tm of
wenzelm@42284
   533
        (t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts)
wenzelm@42245
   534
      | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
wenzelm@42290
   535
          Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
wenzelm@42245
   536
      | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
wenzelm@42290
   537
          Ast.mk_appl (constrain (c $ Syntax.var xi) T) (map ast_of ts)
wenzelm@42245
   538
      | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
wenzelm@42290
   539
          Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
wenzelm@42245
   540
      | (Const ("_idtdummy", T), ts) =>
wenzelm@42476
   541
          Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
wenzelm@42245
   542
      | (const as Const (c, T), ts) =>
wenzelm@42245
   543
          if show_all_types
wenzelm@42245
   544
          then Ast.mk_appl (constrain const T) (map ast_of ts)
wenzelm@42245
   545
          else trans c T ts
wenzelm@42245
   546
      | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
wenzelm@42245
   547
wenzelm@42254
   548
    and trans a T args = ast_of (trf a ctxt T args)
wenzelm@42254
   549
      handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
wenzelm@42245
   550
wenzelm@42245
   551
    and constrain t T =
wenzelm@42245
   552
      if show_types andalso T <> dummyT then
wenzelm@42248
   553
        Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t,
wenzelm@42247
   554
          ast_of_termT ctxt trf (term_of_typ ctxt T)]
wenzelm@42245
   555
      else simple_ast_of ctxt t;
wenzelm@42245
   556
  in
wenzelm@42245
   557
    tm
wenzelm@42284
   558
    |> Syntax_Trans.prop_tr'
wenzelm@42245
   559
    |> show_types ? (#1 o prune_typs o rpair [])
wenzelm@42245
   560
    |> mark_atoms
wenzelm@42245
   561
    |> ast_of
wenzelm@42245
   562
  end;
wenzelm@42245
   563
wenzelm@42245
   564
wenzelm@42245
   565
wenzelm@42242
   566
(** unparse **)
wenzelm@42242
   567
wenzelm@42245
   568
local
wenzelm@42245
   569
wenzelm@42267
   570
fun free_or_skolem ctxt x =
wenzelm@42267
   571
  let
wenzelm@42267
   572
    val m =
wenzelm@42267
   573
      if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
wenzelm@42267
   574
      then Markup.fixed x
wenzelm@42267
   575
      else Markup.hilite;
wenzelm@42267
   576
  in
wenzelm@42267
   577
    if can Name.dest_skolem x
wenzelm@42488
   578
    then ([m, Markup.skolem], Variable.revert_fixed ctxt x)
wenzelm@42267
   579
    else ([m, Markup.free], x)
wenzelm@42267
   580
  end;
wenzelm@42267
   581
wenzelm@42267
   582
fun var_or_skolem s =
wenzelm@42267
   583
  (case Lexicon.read_variable s of
wenzelm@42267
   584
    SOME (x, i) =>
wenzelm@42267
   585
      (case try Name.dest_skolem x of
wenzelm@42267
   586
        NONE => (Markup.var, s)
wenzelm@42267
   587
      | SOME x' => (Markup.skolem, Term.string_of_vname (x', i)))
wenzelm@42267
   588
  | NONE => (Markup.var, s));
wenzelm@42267
   589
wenzelm@42267
   590
fun unparse_t t_to_ast prt_t markup ctxt t =
wenzelm@42245
   591
  let
wenzelm@42360
   592
    val syn = Proof_Context.syn_of ctxt;
wenzelm@42267
   593
wenzelm@42267
   594
    fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x))
wenzelm@42267
   595
      | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
wenzelm@42267
   596
      | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
wenzelm@42267
   597
      | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x))
wenzelm@42408
   598
      | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.malformed, x))
wenzelm@42267
   599
      | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
wenzelm@42267
   600
      | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x))
wenzelm@42267
   601
      | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x))
wenzelm@42267
   602
      | token_trans _ _ = NONE;
wenzelm@42267
   603
wenzelm@42301
   604
    fun markup_extern c =
wenzelm@42301
   605
      (case Syntax.lookup_const syn c of
wenzelm@42301
   606
        SOME "" => ([], c)
wenzelm@42301
   607
      | SOME b => markup_extern b
wenzelm@42301
   608
      | NONE => c |> Lexicon.unmark
wenzelm@43548
   609
         {case_class = fn x => (markup_class ctxt x, Proof_Context.extern_class ctxt x),
wenzelm@43552
   610
          case_type = fn x => (markup_type ctxt x, Proof_Context.extern_type ctxt x),
wenzelm@43552
   611
          case_const = fn x => (markup_const ctxt x, Proof_Context.extern_const ctxt x),
wenzelm@42301
   612
          case_fixed = fn x => free_or_skolem ctxt x,
wenzelm@42301
   613
          case_default = fn x => ([], x)});
wenzelm@42245
   614
  in
wenzelm@42255
   615
    t_to_ast ctxt (Syntax.print_translation syn) t
wenzelm@42255
   616
    |> Ast.normalize ctxt (Syntax.print_rules syn)
wenzelm@42267
   617
    |> prt_t ctxt (Syntax.prtabs syn) (Syntax.print_ast_translation syn) token_trans markup_extern
wenzelm@42253
   618
    |> Pretty.markup markup
wenzelm@42245
   619
  end;
wenzelm@42245
   620
wenzelm@42245
   621
in
wenzelm@42245
   622
wenzelm@42267
   623
val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.sort;
wenzelm@42267
   624
val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.typ;
wenzelm@42241
   625
wenzelm@42241
   626
fun unparse_term ctxt =
wenzelm@42241
   627
  let
wenzelm@42360
   628
    val thy = Proof_Context.theory_of ctxt;
wenzelm@42360
   629
    val syn = Proof_Context.syn_of ctxt;
wenzelm@42360
   630
    val idents = Local_Syntax.idents_of (Proof_Context.syntax_of ctxt);
wenzelm@42241
   631
  in
wenzelm@42298
   632
    unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn))
wenzelm@42267
   633
      (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
wenzelm@42267
   634
      Markup.term ctxt
wenzelm@42241
   635
  end;
wenzelm@42241
   636
wenzelm@42249
   637
end;
wenzelm@42249
   638
wenzelm@42241
   639
wenzelm@42245
   640
wenzelm@42245
   641
(** translations **)
wenzelm@42245
   642
wenzelm@42245
   643
(* type propositions *)
wenzelm@42245
   644
wenzelm@42247
   645
fun type_prop_tr' ctxt T [Const ("\\<^const>Pure.sort_constraint", _)] =
wenzelm@42476
   646
      Syntax.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T
wenzelm@42247
   647
  | type_prop_tr' ctxt T [t] =
wenzelm@42476
   648
      Syntax.const "_ofclass" $ term_of_typ ctxt T $ t
wenzelm@42245
   649
  | type_prop_tr' _ T ts = raise TYPE ("type_prop_tr'", [T], ts);
wenzelm@42245
   650
wenzelm@42245
   651
wenzelm@42245
   652
(* type reflection *)
wenzelm@42245
   653
wenzelm@42247
   654
fun type_tr' ctxt (Type ("itself", [T])) ts =
wenzelm@42476
   655
      Term.list_comb (Syntax.const "_TYPE" $ term_of_typ ctxt T, ts)
wenzelm@42245
   656
  | type_tr' _ _ _ = raise Match;
wenzelm@42245
   657
wenzelm@42245
   658
wenzelm@42245
   659
(* type constraints *)
wenzelm@42245
   660
wenzelm@42247
   661
fun type_constraint_tr' ctxt (Type ("fun", [T, _])) (t :: ts) =
wenzelm@42476
   662
      Term.list_comb (Syntax.const "_constrain" $ t $ term_of_typ ctxt T, ts)
wenzelm@42245
   663
  | type_constraint_tr' _ _ _ = raise Match;
wenzelm@42245
   664
wenzelm@42245
   665
wenzelm@42295
   666
(* authentic syntax *)
wenzelm@42295
   667
wenzelm@42295
   668
fun const_ast_tr intern ctxt [Ast.Variable c] =
wenzelm@42295
   669
      let
wenzelm@42360
   670
        val Const (c', _) = Proof_Context.read_const_proper ctxt false c;
wenzelm@42295
   671
        val d = if intern then Lexicon.mark_const c' else c;
wenzelm@42295
   672
      in Ast.Constant d end
wenzelm@42470
   673
  | const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T as Ast.Variable pos]] =
wenzelm@42470
   674
      (Ast.Appl [Ast.Constant "_constrain", const_ast_tr intern ctxt [x], T]
wenzelm@42470
   675
        handle ERROR msg =>
wenzelm@42470
   676
          error (msg ^ Position.str_of (the_default Position.none (Term_Position.decode pos))))
wenzelm@42295
   677
  | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
wenzelm@42295
   678
wenzelm@42295
   679
wenzelm@42245
   680
(* setup translations *)
wenzelm@42245
   681
wenzelm@42245
   682
val _ = Context.>> (Context.map_theory
wenzelm@42295
   683
 (Sign.add_advanced_trfuns
wenzelm@42295
   684
  ([("_context_const", const_ast_tr true),
wenzelm@42295
   685
    ("_context_xconst", const_ast_tr false)], [], [], []) #>
wenzelm@42295
   686
  Sign.add_advanced_trfunsT
wenzelm@42245
   687
   [("_type_prop", type_prop_tr'),
wenzelm@42245
   688
    ("\\<^const>TYPE", type_tr'),
wenzelm@42245
   689
    ("_type_constraint_", type_constraint_tr')]));
wenzelm@42245
   690
wenzelm@42245
   691
wenzelm@42245
   692
wenzelm@42382
   693
(** check/uncheck **)
wenzelm@42382
   694
wenzelm@45427
   695
fun prepare_types ctxt tys =
wenzelm@45427
   696
  let
wenzelm@45427
   697
    fun constraint (xi: indexname, S) = S <> dummyS ? insert (op =) (xi, S);
wenzelm@45427
   698
    val env =
wenzelm@45427
   699
      (fold o fold_atyps)
wenzelm@45427
   700
        (fn TFree (x, S) => constraint ((x, ~1), S)
wenzelm@45427
   701
          | TVar v => constraint v
wenzelm@45427
   702
          | _ => I) tys [];
wenzelm@45427
   703
    val get_sort = Proof_Context.get_sort ctxt env;
wenzelm@45427
   704
  in
wenzelm@45427
   705
    (map o map_atyps)
wenzelm@45427
   706
      (fn TFree (x, _) => TFree (x, get_sort (x, ~1))
wenzelm@45427
   707
        | TVar (xi, _) => TVar (xi, get_sort xi)
wenzelm@45427
   708
        | T => T) tys
wenzelm@45427
   709
  end;
wenzelm@45427
   710
wenzelm@45423
   711
fun check_typs ctxt =
wenzelm@45427
   712
  prepare_types ctxt #>
wenzelm@45427
   713
  Syntax.apply_typ_check ctxt #>
wenzelm@45427
   714
  Term_Sharing.typs (Proof_Context.theory_of ctxt);
wenzelm@45423
   715
wenzelm@45423
   716
fun check_terms ctxt =
wenzelm@45427
   717
  Term.burrow_types (prepare_types ctxt) #>
wenzelm@45427
   718
  Syntax.apply_term_check ctxt #>
wenzelm@45427
   719
  Term_Sharing.terms (Proof_Context.theory_of ctxt);
wenzelm@45423
   720
wenzelm@42382
   721
fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
wenzelm@42382
   722
wenzelm@45423
   723
val uncheck_typs = Syntax.apply_typ_uncheck;
wenzelm@45423
   724
val uncheck_terms = Syntax.apply_term_uncheck;
wenzelm@42382
   725
wenzelm@42382
   726
wenzelm@42382
   727
wenzelm@42242
   728
(** install operations **)
wenzelm@42242
   729
wenzelm@42241
   730
val _ = Syntax.install_operations
wenzelm@42241
   731
  {parse_sort = parse_sort,
wenzelm@42241
   732
   parse_typ = parse_typ,
wenzelm@42281
   733
   parse_term = parse_term false,
wenzelm@42281
   734
   parse_prop = parse_term true,
wenzelm@42241
   735
   unparse_sort = unparse_sort,
wenzelm@42241
   736
   unparse_typ = unparse_typ,
wenzelm@42382
   737
   unparse_term = unparse_term,
wenzelm@42382
   738
   check_typs = check_typs,
wenzelm@42382
   739
   check_terms = check_terms,
wenzelm@42382
   740
   check_props = check_props,
wenzelm@42382
   741
   uncheck_typs = uncheck_typs,
wenzelm@42382
   742
   uncheck_terms = uncheck_terms};
wenzelm@42241
   743
wenzelm@42241
   744
end;