src/Pure/Syntax/type_ext.ML
author wenzelm
Sun Mar 08 17:26:14 2009 +0100 (2009-03-08)
changeset 30364 577edc39b501
parent 29565 3f8b24fcfbd6
child 32784 1a5dde5079ac
permissions -rw-r--r--
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm@18
     1
(*  Title:      Pure/Syntax/type_ext.ML
clasohm@0
     2
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
clasohm@0
     3
wenzelm@8895
     4
Utilities for input and output of types.  Also the concrete syntax of
wenzelm@8895
     5
types, which is required to bootstrap Pure.
clasohm@0
     6
*)
clasohm@0
     7
clasohm@0
     8
signature TYPE_EXT0 =
wenzelm@2584
     9
sig
wenzelm@22704
    10
  val sort_of_term: (sort -> sort) -> term -> sort
wenzelm@22704
    11
  val term_sorts: (sort -> sort) -> term -> (indexname * sort) list
wenzelm@12317
    12
  val typ_of_term: (indexname -> sort) -> (sort -> sort) -> term -> typ
wenzelm@27266
    13
  val type_constraint: typ -> term -> term
wenzelm@22764
    14
  val decode_term: (((string * int) * sort) list -> string * int -> sort) ->
wenzelm@27197
    15
    (string -> bool * string) -> (string -> string option) ->
wenzelm@22704
    16
    (typ -> typ) -> (sort -> sort) -> term -> 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
paulson@1511
    28
  val type_ext: SynExt.syn_ext
wenzelm@2584
    29
end;
clasohm@0
    30
wenzelm@15750
    31
structure TypeExt: 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@22704
    38
fun sort_of_term (map_sort: sort -> sort) tm =
wenzelm@557
    39
  let
wenzelm@18
    40
    fun classes (Const (c, _)) = [c]
wenzelm@18
    41
      | classes (Free (c, _)) = [c]
wenzelm@26039
    42
      | classes (Const ("_class", _) $ Free (c, _)) = [c]
wenzelm@3778
    43
      | classes (Const ("_classes", _) $ Const (c, _) $ cs) = c :: classes cs
wenzelm@3778
    44
      | classes (Const ("_classes", _) $ Free (c, _) $ cs) = c :: classes cs
wenzelm@26039
    45
      | classes (Const ("_classes", _) $ (Const ("_class", _) $ Free (c, _)) $ cs) = c :: classes cs
wenzelm@8895
    46
      | classes tm = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
clasohm@0
    47
wenzelm@2584
    48
    fun sort (Const ("_topsort", _)) = []
wenzelm@2584
    49
      | sort (Const (c, _)) = [c]
wenzelm@2584
    50
      | sort (Free (c, _)) = [c]
wenzelm@26039
    51
      | sort (Const ("_class", _) $ Free (c, _)) = [c]
wenzelm@3778
    52
      | sort (Const ("_sort", _) $ cs) = classes cs
wenzelm@8895
    53
      | sort tm = raise TERM ("sort_of_term: bad encoding of sort", [tm]);
wenzelm@22704
    54
  in map_sort (sort tm) end;
wenzelm@8895
    55
wenzelm@2584
    56
wenzelm@22704
    57
(* term_sorts *)
wenzelm@8895
    58
wenzelm@22704
    59
fun term_sorts map_sort tm =
wenzelm@8895
    60
  let
wenzelm@22704
    61
    val sort_of = sort_of_term map_sort;
wenzelm@22704
    62
wenzelm@22704
    63
    fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) =
wenzelm@22704
    64
          insert (op =) ((x, ~1), sort_of cs)
wenzelm@22704
    65
      | add_env (Const ("_ofsort", _) $ (Const ("_tfree", _) $ Free (x, _)) $ cs) =
wenzelm@22704
    66
          insert (op =) ((x, ~1), sort_of cs)
wenzelm@22704
    67
      | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) =
wenzelm@22704
    68
          insert (op =) (xi, sort_of cs)
wenzelm@22704
    69
      | add_env (Const ("_ofsort", _) $ (Const ("_tvar", _) $ Var (xi, _)) $ cs) =
wenzelm@22704
    70
          insert (op =) (xi, sort_of cs)
wenzelm@22704
    71
      | add_env (Abs (_, _, t)) = add_env t
wenzelm@22704
    72
      | add_env (t1 $ t2) = add_env t1 #> add_env t2
wenzelm@22704
    73
      | add_env _ = I;
wenzelm@8895
    74
  in add_env tm [] end;
wenzelm@557
    75
wenzelm@557
    76
wenzelm@2584
    77
(* typ_of_term *)
clasohm@0
    78
wenzelm@12317
    79
fun typ_of_term get_sort map_sort t =
wenzelm@557
    80
  let
wenzelm@557
    81
    fun typ_of (Free (x, _)) =
wenzelm@5690
    82
          if Lexicon.is_tid x then TFree (x, get_sort (x, ~1))
wenzelm@557
    83
          else Type (x, [])
wenzelm@557
    84
      | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
schirmer@14255
    85
      | typ_of (Const ("_tfree",_) $ (t as Free x)) = typ_of t
schirmer@14255
    86
      | typ_of (Const ("_tvar",_) $ (t as Var x)) = typ_of t
wenzelm@12317
    87
      | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
wenzelm@16614
    88
      | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) =
wenzelm@16614
    89
          TFree (x, get_sort (x, ~1))
wenzelm@12317
    90
      | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
wenzelm@16614
    91
      | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) =
wenzelm@16614
    92
          TVar (xi, get_sort xi)
wenzelm@22704
    93
      | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term map_sort t)
wenzelm@557
    94
      | typ_of tm =
clasohm@0
    95
          let
wenzelm@16614
    96
            val (t, ts) = Term.strip_comb tm;
clasohm@0
    97
            val a =
wenzelm@18
    98
              (case t of
clasohm@0
    99
                Const (x, _) => x
clasohm@0
   100
              | Free (x, _) => x
wenzelm@3778
   101
              | _ => raise TERM ("typ_of_term: bad encoding of type", [tm]));
wenzelm@12317
   102
          in Type (a, map typ_of ts) end;
wenzelm@8895
   103
  in typ_of t end;
clasohm@0
   104
clasohm@0
   105
wenzelm@22764
   106
(* decode_term -- transform parse tree into raw term *)
wenzelm@22704
   107
wenzelm@27266
   108
fun type_constraint T t =
wenzelm@27266
   109
  if T = dummyT then t
wenzelm@27266
   110
  else Const ("_type_constraint_", T --> T) $ t;
wenzelm@27266
   111
wenzelm@22764
   112
fun decode_term get_sort map_const map_free map_type map_sort tm =
wenzelm@22704
   113
  let
wenzelm@22704
   114
    val sort_env = term_sorts map_sort tm;
wenzelm@22704
   115
    val decodeT = map_type o typ_of_term (get_sort sort_env) map_sort;
wenzelm@22704
   116
wenzelm@22704
   117
    fun decode (Const ("_constrain", _) $ t $ typ) =
wenzelm@27266
   118
          type_constraint (decodeT typ) (decode t)
wenzelm@22704
   119
      | decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) =
wenzelm@22704
   120
          if T = dummyT then Abs (x, decodeT typ, decode t)
wenzelm@27266
   121
          else type_constraint (decodeT typ --> dummyT) (Abs (x, map_type T, decode t))
wenzelm@22704
   122
      | decode (Abs (x, T, t)) = Abs (x, map_type T, decode t)
wenzelm@22704
   123
      | decode (t $ u) = decode t $ decode u
wenzelm@22704
   124
      | decode (Const (a, T)) =
wenzelm@22704
   125
          let val c =
wenzelm@27197
   126
            (case try (unprefix Lexicon.constN) a of SOME c => c | NONE => snd (map_const a))
wenzelm@22704
   127
          in Const (c, map_type T) end
wenzelm@22704
   128
      | decode (Free (a, T)) =
wenzelm@22704
   129
          (case (map_free a, map_const a) of
wenzelm@22704
   130
            (SOME x, _) => Free (x, map_type T)
wenzelm@27197
   131
          | (_, (true, c)) => Const (c, map_type T)
wenzelm@30364
   132
          | (_, (false, c)) => (if Long_Name.is_qualified c then Const else Free) (c, map_type T))
wenzelm@22704
   133
      | decode (Var (xi, T)) = Var (xi, map_type T)
wenzelm@22704
   134
      | decode (t as Bound _) = t;
wenzelm@22704
   135
  in decode tm end;
wenzelm@22704
   136
wenzelm@22704
   137
clasohm@0
   138
wenzelm@2584
   139
(** output utils **)
wenzelm@2584
   140
wenzelm@2699
   141
(* term_of_sort *)
wenzelm@2584
   142
wenzelm@2584
   143
fun term_of_sort S =
wenzelm@2584
   144
  let
wenzelm@5690
   145
    fun class c = Lexicon.const "_class" $ Lexicon.free c;
wenzelm@2584
   146
wenzelm@2584
   147
    fun classes [] = sys_error "term_of_sort"
wenzelm@2584
   148
      | classes [c] = class c
wenzelm@5690
   149
      | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
wenzelm@2584
   150
  in
wenzelm@2584
   151
    (case S of
wenzelm@5690
   152
      [] => Lexicon.const "_topsort"
wenzelm@2584
   153
    | [c] => class c
wenzelm@5690
   154
    | cs => Lexicon.const "_sort" $ classes cs)
wenzelm@2584
   155
  end;
wenzelm@2584
   156
wenzelm@2584
   157
wenzelm@2584
   158
(* term_of_typ *)
clasohm@0
   159
clasohm@0
   160
fun term_of_typ show_sorts ty =
clasohm@0
   161
  let
wenzelm@2584
   162
    fun of_sort t S =
wenzelm@5690
   163
      if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
wenzelm@2584
   164
      else t;
clasohm@0
   165
wenzelm@16614
   166
    fun term_of (Type (a, Ts)) = Term.list_comb (Lexicon.const a, map term_of Ts)
wenzelm@5690
   167
      | term_of (TFree (x, S)) = of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
wenzelm@5690
   168
      | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
wenzelm@8895
   169
  in term_of ty end;
clasohm@0
   170
clasohm@0
   171
clasohm@0
   172
clasohm@0
   173
(** the type syntax **)
clasohm@0
   174
wenzelm@10572
   175
(* print mode *)
wenzelm@10572
   176
wenzelm@10572
   177
val bracketsN = "brackets";
wenzelm@10572
   178
val no_bracketsN = "no_brackets";
wenzelm@10572
   179
wenzelm@10572
   180
fun no_brackets () =
wenzelm@24613
   181
  find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN)
wenzelm@24613
   182
    (print_mode_value ()) = SOME no_bracketsN;
nipkow@11312
   183
nipkow@11312
   184
val type_bracketsN = "type_brackets";
nipkow@11312
   185
val no_type_bracketsN = "no_type_brackets";
nipkow@11312
   186
nipkow@11312
   187
fun no_type_brackets () =
wenzelm@24613
   188
  find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN)
wenzelm@24613
   189
    (print_mode_value ()) <> SOME type_bracketsN;
wenzelm@10572
   190
wenzelm@10572
   191
wenzelm@18
   192
(* parse ast translations *)
clasohm@0
   193
wenzelm@5690
   194
fun tapp_ast_tr (*"_tapp"*) [ty, f] = Ast.Appl [f, ty]
wenzelm@5690
   195
  | tapp_ast_tr (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
wenzelm@347
   196
wenzelm@347
   197
fun tappl_ast_tr (*"_tappl"*) [ty, tys, f] =
wenzelm@5690
   198
      Ast.Appl (f :: ty :: Ast.unfold_ast "_types" tys)
wenzelm@5690
   199
  | tappl_ast_tr (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts);
clasohm@0
   200
clasohm@0
   201
fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
wenzelm@5690
   202
      Ast.fold_ast_p "fun" (Ast.unfold_ast "_types" dom, cod)
wenzelm@5690
   203
  | bracket_ast_tr (*"_bracket"*) asts = raise Ast.AST ("bracket_ast_tr", asts);
clasohm@0
   204
clasohm@0
   205
wenzelm@18
   206
(* print ast translations *)
clasohm@0
   207
wenzelm@5690
   208
fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f])
wenzelm@5690
   209
  | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f]
wenzelm@347
   210
  | tappl_ast_tr' (f, ty :: tys) =
wenzelm@5690
   211
      Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
clasohm@0
   212
clasohm@0
   213
fun fun_ast_tr' (*"fun"*) asts =
wenzelm@16614
   214
  if no_brackets () orelse no_type_brackets () then raise Match
wenzelm@10572
   215
  else
wenzelm@10572
   216
    (case Ast.unfold_ast_p "fun" (Ast.Appl (Ast.Constant "fun" :: asts)) of
wenzelm@10572
   217
      (dom as _ :: _ :: _, cod)
wenzelm@10572
   218
        => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
wenzelm@10572
   219
    | _ => raise Match);
clasohm@0
   220
clasohm@0
   221
clasohm@0
   222
(* type_ext *)
clasohm@0
   223
clasohm@0
   224
val sortT = Type ("sort", []);
clasohm@0
   225
val classesT = Type ("classes", []);
clasohm@0
   226
val typesT = Type ("types", []);
clasohm@0
   227
wenzelm@5690
   228
local open Lexicon SynExt in
wenzelm@5690
   229
wenzelm@14903
   230
val type_ext = syn_ext' false (K false)
wenzelm@347
   231
  [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
wenzelm@239
   232
   Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
wenzelm@239
   233
   Mfix ("_",           idT --> typeT,                 "", [], max_pri),
wenzelm@3829
   234
   Mfix ("_",           longidT --> typeT,             "", [], max_pri),
clasohm@330
   235
   Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
wenzelm@239
   236
   Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
wenzelm@14838
   237
   Mfix ("'_()::_",     sortT --> typeT,               "_dummy_ofsort", [0], max_pri),
wenzelm@239
   238
   Mfix ("_",           idT --> sortT,                 "", [], max_pri),
wenzelm@3829
   239
   Mfix ("_",           longidT --> sortT,             "", [], max_pri),
wenzelm@2584
   240
   Mfix ("{}",          sortT,                         "_topsort", [], max_pri),
wenzelm@239
   241
   Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
wenzelm@239
   242
   Mfix ("_",           idT --> classesT,              "", [], max_pri),
wenzelm@3829
   243
   Mfix ("_",           longidT --> classesT,          "", [], max_pri),
wenzelm@239
   244
   Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
wenzelm@3829
   245
   Mfix ("_,_",         [longidT, classesT] ---> classesT, "_classes", [], max_pri),
clasohm@330
   246
   Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
wenzelm@3829
   247
   Mfix ("_ _",         [typeT, longidT] ---> typeT,   "_tapp", [max_pri, 0], max_pri),
wenzelm@9067
   248
   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
wenzelm@9067
   249
   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
wenzelm@239
   250
   Mfix ("_",           typeT --> typesT,              "", [], max_pri),
wenzelm@239
   251
   Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
wenzelm@239
   252
   Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
clasohm@624
   253
   Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
wenzelm@2678
   254
   Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
wenzelm@2678
   255
   Mfix ("'_",          typeT,                         "dummy", [], max_pri)]
wenzelm@258
   256
  []
wenzelm@15750
   257
  (map SynExt.mk_trfun
wenzelm@16614
   258
   [("_tapp", K tapp_ast_tr), ("_tappl", K tappl_ast_tr), ("_bracket", K bracket_ast_tr)],
wenzelm@239
   259
   [],
wenzelm@239
   260
   [],
wenzelm@16614
   261
   map SynExt.mk_trfun [("fun", K fun_ast_tr')])
wenzelm@26708
   262
  []
wenzelm@239
   263
  ([], []);
clasohm@0
   264
clasohm@0
   265
end;
wenzelm@5690
   266
wenzelm@5690
   267
end;