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