src/Pure/Syntax/type_ext.ML
author wenzelm
Sun Apr 03 21:59:33 2011 +0200 (2011-04-03)
changeset 42204 b3277168c1e7
parent 42170 a37a47aa985b
child 42223 098c86e53153
permissions -rw-r--r--
added Position.reports convenience;
modernized Syntax.trrule constructors;
modernized Sign.add_trrules/del_trrules: internal arguments;
modernized Isar_Cmd.translations/no_translations: external arguments;
explicit syntax categories class_name/type_name, with reports via type_context;
eliminated former class_name/type_name ast translations;
tuned signatures;
wenzelm@18
     1
(*  Title:      Pure/Syntax/type_ext.ML
clasohm@0
     2
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
clasohm@0
     3
wenzelm@35429
     4
Utilities for input and output of types.  The concrete syntax of types.
clasohm@0
     5
*)
clasohm@0
     6
clasohm@0
     7
signature TYPE_EXT0 =
wenzelm@2584
     8
sig
wenzelm@35429
     9
  val sort_of_term: term -> sort
wenzelm@35429
    10
  val term_sorts: term -> (indexname * sort) list
wenzelm@35429
    11
  val typ_of_term: (indexname -> sort) -> term -> typ
wenzelm@42053
    12
  val is_position: term -> bool
wenzelm@42050
    13
  val strip_positions: term -> term
wenzelm@42052
    14
  val strip_positions_ast: Ast.ast -> Ast.ast
wenzelm@42134
    15
  type term_context
wenzelm@42204
    16
  val decode_term: term_context -> Position.reports * term -> Position.reports * term
wenzelm@6901
    17
  val term_of_typ: bool -> typ -> term
wenzelm@10572
    18
  val no_brackets: unit -> bool
wenzelm@16614
    19
  val no_type_brackets: unit -> bool
wenzelm@2584
    20
end;
clasohm@0
    21
clasohm@0
    22
signature TYPE_EXT =
wenzelm@2584
    23
sig
clasohm@0
    24
  include TYPE_EXT0
wenzelm@2584
    25
  val term_of_sort: sort -> term
paulson@1511
    26
  val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
wenzelm@8895
    27
  val sortT: typ
wenzelm@37216
    28
  val type_ext: Syn_Ext.syn_ext
wenzelm@2584
    29
end;
clasohm@0
    30
wenzelm@37216
    31
structure Type_Ext: TYPE_EXT =
clasohm@0
    32
struct
wenzelm@2584
    33
wenzelm@2584
    34
(** input utils **)
clasohm@0
    35
wenzelm@8895
    36
(* sort_of_term *)
wenzelm@2584
    37
wenzelm@35429
    38
fun sort_of_term tm =
wenzelm@557
    39
  let
wenzelm@35429
    40
    fun err () = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
wenzelm@35429
    41
wenzelm@35429
    42
    fun class s = Lexicon.unmark_class s handle Fail _ => err ();
wenzelm@35429
    43
wenzelm@35429
    44
    fun classes (Const (s, _)) = [class s]
wenzelm@35429
    45
      | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
wenzelm@35429
    46
      | classes _ = err ();
clasohm@0
    47
wenzelm@2584
    48
    fun sort (Const ("_topsort", _)) = []
wenzelm@35429
    49
      | sort (Const (s, _)) = [class s]
wenzelm@3778
    50
      | sort (Const ("_sort", _) $ cs) = classes cs
wenzelm@35429
    51
      | sort _ = err ();
wenzelm@35429
    52
  in sort tm end;
wenzelm@8895
    53
wenzelm@2584
    54
wenzelm@22704
    55
(* term_sorts *)
wenzelm@8895
    56
wenzelm@35429
    57
fun term_sorts tm =
wenzelm@8895
    58
  let
wenzelm@35429
    59
    val sort_of = sort_of_term;
wenzelm@22704
    60
wenzelm@22704
    61
    fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) =
wenzelm@22704
    62
          insert (op =) ((x, ~1), sort_of cs)
wenzelm@22704
    63
      | add_env (Const ("_ofsort", _) $ (Const ("_tfree", _) $ Free (x, _)) $ cs) =
wenzelm@22704
    64
          insert (op =) ((x, ~1), sort_of cs)
wenzelm@22704
    65
      | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) =
wenzelm@22704
    66
          insert (op =) (xi, sort_of cs)
wenzelm@22704
    67
      | add_env (Const ("_ofsort", _) $ (Const ("_tvar", _) $ Var (xi, _)) $ cs) =
wenzelm@22704
    68
          insert (op =) (xi, sort_of cs)
wenzelm@22704
    69
      | add_env (Abs (_, _, t)) = add_env t
wenzelm@22704
    70
      | add_env (t1 $ t2) = add_env t1 #> add_env t2
wenzelm@22704
    71
      | add_env _ = I;
wenzelm@8895
    72
  in add_env tm [] end;
wenzelm@557
    73
wenzelm@557
    74
wenzelm@2584
    75
(* typ_of_term *)
clasohm@0
    76
wenzelm@35429
    77
fun typ_of_term get_sort tm =
wenzelm@557
    78
  let
wenzelm@35429
    79
    fun err () = raise TERM ("typ_of_term: bad encoding of type", [tm]);
wenzelm@35429
    80
wenzelm@35429
    81
    fun typ_of (Free (x, _)) = TFree (x, get_sort (x, ~1))
wenzelm@557
    82
      | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
wenzelm@32784
    83
      | typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t
wenzelm@32784
    84
      | typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t
wenzelm@12317
    85
      | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
wenzelm@16614
    86
      | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) =
wenzelm@16614
    87
          TFree (x, get_sort (x, ~1))
wenzelm@12317
    88
      | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
wenzelm@16614
    89
      | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) =
wenzelm@16614
    90
          TVar (xi, get_sort xi)
wenzelm@35429
    91
      | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term t)
wenzelm@35429
    92
      | typ_of t =
clasohm@0
    93
          let
wenzelm@35429
    94
            val (head, args) = Term.strip_comb t;
clasohm@0
    95
            val a =
wenzelm@35429
    96
              (case head of
wenzelm@35429
    97
                Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
wenzelm@35429
    98
              | _ => err ());
wenzelm@35429
    99
          in Type (a, map typ_of args) end;
wenzelm@35429
   100
  in typ_of tm end;
clasohm@0
   101
clasohm@0
   102
wenzelm@42050
   103
(* positions *)
wenzelm@22704
   104
wenzelm@42131
   105
fun decode_position (Free (x, _)) = Lexicon.decode_position x
wenzelm@42131
   106
  | decode_position _ = NONE;
wenzelm@42131
   107
wenzelm@42131
   108
val is_position = is_some o decode_position;
wenzelm@42048
   109
wenzelm@42050
   110
fun strip_positions ((t as Const (c, _)) $ u $ v) =
wenzelm@42050
   111
      if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v
wenzelm@42050
   112
      then strip_positions u
wenzelm@42050
   113
      else t $ strip_positions u $ strip_positions v
wenzelm@42050
   114
  | strip_positions (t $ u) = strip_positions t $ strip_positions u
wenzelm@42050
   115
  | strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t)
wenzelm@42050
   116
  | strip_positions t = t;
wenzelm@42050
   117
wenzelm@42052
   118
fun strip_positions_ast (Ast.Appl ((t as Ast.Constant c) :: u :: (v as Ast.Variable x) :: asts)) =
wenzelm@42052
   119
      if (c = "_constrain" orelse c = "_constrainAbs") andalso is_some (Lexicon.decode_position x)
wenzelm@42052
   120
      then Ast.mk_appl (strip_positions_ast u) (map strip_positions_ast asts)
wenzelm@42052
   121
      else Ast.Appl (map strip_positions_ast (t :: u :: v :: asts))
wenzelm@42052
   122
  | strip_positions_ast (Ast.Appl asts) = Ast.Appl (map strip_positions_ast asts)
wenzelm@42052
   123
  | strip_positions_ast ast = ast;
wenzelm@42052
   124
wenzelm@42050
   125
wenzelm@42050
   126
(* decode_term -- transform parse tree into raw term *)
wenzelm@42050
   127
wenzelm@42133
   128
fun markup_bound def id =
wenzelm@42170
   129
  [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound];
wenzelm@42131
   130
wenzelm@42134
   131
type term_context =
wenzelm@42134
   132
 {get_sort: (indexname * sort) list -> indexname -> sort,
wenzelm@42134
   133
  get_const: string -> bool * string,
wenzelm@42135
   134
  get_free: string -> string option,
wenzelm@42170
   135
  markup_const: string -> Markup.T list,
wenzelm@42170
   136
  markup_free: string -> Markup.T list,
wenzelm@42170
   137
  markup_var: indexname -> Markup.T list};
wenzelm@42134
   138
wenzelm@42204
   139
fun decode_term (term_context: term_context) (reports0: Position.reports, tm) =
wenzelm@22704
   140
  let
wenzelm@42135
   141
    val {get_sort, get_const, get_free, markup_const, markup_free, markup_var} = term_context;
wenzelm@36448
   142
    val decodeT = typ_of_term (get_sort (term_sorts tm));
wenzelm@22704
   143
wenzelm@42204
   144
    val reports = Unsynchronized.ref reports0;
wenzelm@42204
   145
    fun report ps = Position.reports reports ps;
wenzelm@42131
   146
wenzelm@42133
   147
    fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
wenzelm@42131
   148
          (case decode_position typ of
wenzelm@42133
   149
            SOME p => decode (p :: ps) qs bs t
wenzelm@42133
   150
          | NONE => Type.constraint (decodeT typ) (decode ps qs bs t))
wenzelm@42133
   151
      | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
wenzelm@42131
   152
          (case decode_position typ of
wenzelm@42133
   153
            SOME q => decode ps (q :: qs) bs t
wenzelm@42133
   154
          | NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t))
wenzelm@42133
   155
      | decode _ qs bs (Abs (x, T, t)) =
wenzelm@42131
   156
          let
wenzelm@42131
   157
            val id = serial_string ();
wenzelm@42133
   158
            val _ = report qs (markup_bound true) id;
wenzelm@42133
   159
          in Abs (x, T, decode [] [] (id :: bs) t) end
wenzelm@42133
   160
      | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
wenzelm@42133
   161
      | decode ps _ _ (Const (a, T)) =
wenzelm@36502
   162
          (case try Lexicon.unmark_fixed a of
wenzelm@42131
   163
            SOME x => (report ps markup_free x; Free (x, T))
wenzelm@36502
   164
          | NONE =>
wenzelm@42131
   165
              let
wenzelm@42131
   166
                val c =
wenzelm@42131
   167
                  (case try Lexicon.unmark_const a of
wenzelm@42131
   168
                    SOME c => c
wenzelm@42134
   169
                  | NONE => snd (get_const a));
wenzelm@42131
   170
                val _ = report ps markup_const c;
wenzelm@36502
   171
              in Const (c, T) end)
wenzelm@42133
   172
      | decode ps _ _ (Free (a, T)) =
wenzelm@42134
   173
          (case (get_free a, get_const a) of
wenzelm@42131
   174
            (SOME x, _) => (report ps markup_free x; Free (x, T))
wenzelm@42131
   175
          | (_, (true, c)) => (report ps markup_const c; Const (c, T))
wenzelm@42131
   176
          | (_, (false, c)) =>
wenzelm@42131
   177
              if Long_Name.is_qualified c
wenzelm@42131
   178
              then (report ps markup_const c; Const (c, T))
wenzelm@42131
   179
              else (report ps markup_free c; Free (c, T)))
wenzelm@42133
   180
      | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
wenzelm@42133
   181
      | decode ps _ bs (t as Bound i) =
wenzelm@42131
   182
          (case try (nth bs) i of
wenzelm@42133
   183
            SOME id => (report ps (markup_bound false) id; t)
wenzelm@42131
   184
          | NONE => t);
wenzelm@42131
   185
wenzelm@42133
   186
    val tm' = decode [] [] [] tm;
wenzelm@42131
   187
  in (! reports, tm') end;
wenzelm@22704
   188
wenzelm@22704
   189
clasohm@0
   190
wenzelm@2584
   191
(** output utils **)
wenzelm@2584
   192
wenzelm@2699
   193
(* term_of_sort *)
wenzelm@2584
   194
wenzelm@2584
   195
fun term_of_sort S =
wenzelm@2584
   196
  let
wenzelm@35429
   197
    val class = Lexicon.const o Lexicon.mark_class;
wenzelm@2584
   198
wenzelm@35429
   199
    fun classes [c] = class c
wenzelm@5690
   200
      | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
wenzelm@2584
   201
  in
wenzelm@2584
   202
    (case S of
wenzelm@5690
   203
      [] => Lexicon.const "_topsort"
wenzelm@2584
   204
    | [c] => class c
wenzelm@5690
   205
    | cs => Lexicon.const "_sort" $ classes cs)
wenzelm@2584
   206
  end;
wenzelm@2584
   207
wenzelm@2584
   208
wenzelm@2584
   209
(* term_of_typ *)
clasohm@0
   210
clasohm@0
   211
fun term_of_typ show_sorts ty =
clasohm@0
   212
  let
wenzelm@2584
   213
    fun of_sort t S =
wenzelm@5690
   214
      if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
wenzelm@2584
   215
      else t;
clasohm@0
   216
wenzelm@35429
   217
    fun term_of (Type (a, Ts)) =
wenzelm@35429
   218
          Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
wenzelm@42048
   219
      | term_of (TFree (x, S)) =
wenzelm@42048
   220
          if is_some (Lexicon.decode_position x) then Lexicon.free x
wenzelm@42048
   221
          else of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
wenzelm@5690
   222
      | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
wenzelm@8895
   223
  in term_of ty end;
clasohm@0
   224
clasohm@0
   225
clasohm@0
   226
clasohm@0
   227
(** the type syntax **)
clasohm@0
   228
wenzelm@10572
   229
(* print mode *)
wenzelm@10572
   230
wenzelm@10572
   231
val bracketsN = "brackets";
wenzelm@10572
   232
val no_bracketsN = "no_brackets";
wenzelm@10572
   233
wenzelm@10572
   234
fun no_brackets () =
wenzelm@24613
   235
  find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN)
wenzelm@24613
   236
    (print_mode_value ()) = SOME no_bracketsN;
nipkow@11312
   237
nipkow@11312
   238
val type_bracketsN = "type_brackets";
nipkow@11312
   239
val no_type_bracketsN = "no_type_brackets";
nipkow@11312
   240
nipkow@11312
   241
fun no_type_brackets () =
wenzelm@24613
   242
  find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN)
wenzelm@24613
   243
    (print_mode_value ()) <> SOME type_bracketsN;
wenzelm@10572
   244
wenzelm@10572
   245
wenzelm@18
   246
(* parse ast translations *)
clasohm@0
   247
wenzelm@42204
   248
fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty]
wenzelm@42204
   249
  | tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts);
wenzelm@347
   250
wenzelm@42204
   251
fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys)
wenzelm@42204
   252
  | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts);
wenzelm@35429
   253
wenzelm@42204
   254
fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
wenzelm@42204
   255
  | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts);
clasohm@0
   256
clasohm@0
   257
wenzelm@18
   258
(* print ast translations *)
clasohm@0
   259
wenzelm@5690
   260
fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f])
wenzelm@5690
   261
  | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f]
wenzelm@347
   262
  | tappl_ast_tr' (f, ty :: tys) =
wenzelm@5690
   263
      Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
clasohm@0
   264
wenzelm@35429
   265
fun fun_ast_tr' (*"\\<^type>fun"*) asts =
wenzelm@16614
   266
  if no_brackets () orelse no_type_brackets () then raise Match
wenzelm@10572
   267
  else
wenzelm@35429
   268
    (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of
wenzelm@10572
   269
      (dom as _ :: _ :: _, cod)
wenzelm@10572
   270
        => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
wenzelm@10572
   271
    | _ => raise Match);
clasohm@0
   272
clasohm@0
   273
clasohm@0
   274
(* type_ext *)
clasohm@0
   275
wenzelm@42204
   276
fun typ c = Type (c, []);
wenzelm@42204
   277
wenzelm@42204
   278
val class_nameT = typ "class_name";
wenzelm@42204
   279
val type_nameT = typ "type_name";
wenzelm@42204
   280
wenzelm@42204
   281
val sortT = typ "sort";
wenzelm@42204
   282
val classesT = typ "classes";
wenzelm@42204
   283
val typesT = typ "types";
clasohm@0
   284
wenzelm@37216
   285
local open Lexicon Syn_Ext in
wenzelm@5690
   286
wenzelm@35668
   287
val type_ext = syn_ext' false (K false)
wenzelm@347
   288
  [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
wenzelm@239
   289
   Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
wenzelm@42204
   290
   Mfix ("_",           type_nameT --> typeT,          "", [], max_pri),
wenzelm@42204
   291
   Mfix ("_",           idT --> type_nameT,            "_type_name", [], max_pri),
wenzelm@42204
   292
   Mfix ("_",           longidT --> type_nameT,        "_type_name", [], max_pri),
clasohm@330
   293
   Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
wenzelm@239
   294
   Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
wenzelm@14838
   295
   Mfix ("'_()::_",     sortT --> typeT,               "_dummy_ofsort", [0], max_pri),
wenzelm@42204
   296
   Mfix ("_",           class_nameT --> sortT,         "", [], max_pri),
wenzelm@42204
   297
   Mfix ("_",           idT --> class_nameT,           "_class_name", [], max_pri),
wenzelm@42204
   298
   Mfix ("_",           longidT --> class_nameT,       "_class_name", [], max_pri),
wenzelm@2584
   299
   Mfix ("{}",          sortT,                         "_topsort", [], max_pri),
wenzelm@239
   300
   Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
wenzelm@42204
   301
   Mfix ("_",           class_nameT --> classesT,      "", [], max_pri),
wenzelm@42204
   302
   Mfix ("_,_",         [class_nameT, classesT] ---> classesT, "_classes", [], max_pri),
wenzelm@42204
   303
   Mfix ("_ _",         [typeT, type_nameT] ---> typeT, "_tapp", [max_pri, 0], max_pri),
wenzelm@42204
   304
   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, type_nameT] ---> typeT, "_tappl", [], max_pri),
wenzelm@239
   305
   Mfix ("_",           typeT --> typesT,              "", [], max_pri),
wenzelm@239
   306
   Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
wenzelm@35429
   307
   Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "\\<^type>fun", [1, 0], 0),
clasohm@624
   308
   Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
wenzelm@2678
   309
   Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
wenzelm@35429
   310
   Mfix ("'_",          typeT,                         "\\<^type>dummy", [], max_pri)]
wenzelm@35433
   311
  ["_type_prop"]
wenzelm@42204
   312
  (map Syn_Ext.mk_trfun
wenzelm@42204
   313
    [("_tapp", K tapp_ast_tr), ("_tappl", K tappl_ast_tr), ("_bracket", K bracket_ast_tr)],
wenzelm@42204
   314
   [], [], map Syn_Ext.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
wenzelm@26708
   315
  []
wenzelm@239
   316
  ([], []);
clasohm@0
   317
clasohm@0
   318
end;
wenzelm@5690
   319
wenzelm@5690
   320
end;