src/Pure/Syntax/type_ext.ML
author wenzelm
Wed Jun 29 15:13:44 2005 +0200 (2005-06-29)
changeset 16614 a493a50e6c0a
parent 15833 78109c7012ed
child 19305 5c16895d548b
permissions -rw-r--r--
export no_type_brackets;
accomodate advanced trfuns;
tuned;
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@8895
    11
  val sort_of_term: term -> sort
wenzelm@3778
    12
  val raw_term_sorts: term -> (indexname * sort) list
wenzelm@12317
    13
  val typ_of_term: (indexname -> sort) -> (sort -> sort) -> term -> typ
wenzelm@6901
    14
  val term_of_typ: bool -> typ -> term
wenzelm@10572
    15
  val no_brackets: unit -> bool
wenzelm@16614
    16
  val no_type_brackets: unit -> bool
wenzelm@2584
    17
end;
clasohm@0
    18
clasohm@0
    19
signature TYPE_EXT =
wenzelm@2584
    20
sig
clasohm@0
    21
  include TYPE_EXT0
wenzelm@2584
    22
  val term_of_sort: sort -> term
paulson@1511
    23
  val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
wenzelm@8895
    24
  val sortT: typ
paulson@1511
    25
  val type_ext: SynExt.syn_ext
wenzelm@2584
    26
end;
clasohm@0
    27
wenzelm@15750
    28
structure TypeExt: TYPE_EXT =
clasohm@0
    29
struct
wenzelm@2584
    30
wenzelm@2584
    31
wenzelm@2584
    32
(** input utils **)
clasohm@0
    33
wenzelm@8895
    34
(* sort_of_term *)
wenzelm@2584
    35
wenzelm@8895
    36
fun sort_of_term tm =
wenzelm@557
    37
  let
wenzelm@18
    38
    fun classes (Const (c, _)) = [c]
wenzelm@18
    39
      | classes (Free (c, _)) = [c]
wenzelm@3778
    40
      | classes (Const ("_classes", _) $ Const (c, _) $ cs) = c :: classes cs
wenzelm@3778
    41
      | classes (Const ("_classes", _) $ Free (c, _) $ cs) = c :: classes cs
wenzelm@8895
    42
      | classes tm = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
clasohm@0
    43
wenzelm@2584
    44
    fun sort (Const ("_topsort", _)) = []
wenzelm@2584
    45
      | sort (Const (c, _)) = [c]
wenzelm@2584
    46
      | sort (Free (c, _)) = [c]
schirmer@14255
    47
      | sort (Const ("_class",_) $ Free (c, _)) = [c]
wenzelm@3778
    48
      | sort (Const ("_sort", _) $ cs) = classes cs
wenzelm@8895
    49
      | sort tm = raise TERM ("sort_of_term: bad encoding of sort", [tm]);
wenzelm@8895
    50
  in sort tm end;
wenzelm@8895
    51
wenzelm@2584
    52
wenzelm@8895
    53
(* raw_term_sorts *)
wenzelm@8895
    54
wenzelm@8895
    55
fun raw_term_sorts tm =
wenzelm@8895
    56
  let
wenzelm@16614
    57
    fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) env =
wenzelm@16614
    58
          ((x, ~1), sort_of_term cs) ins env
wenzelm@16614
    59
      | add_env (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ cs) env =
wenzelm@16614
    60
          ((x, ~1), sort_of_term cs) ins env
wenzelm@16614
    61
      | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) env =
wenzelm@16614
    62
          (xi, sort_of_term cs) ins env
wenzelm@16614
    63
      | add_env (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ cs) env =
wenzelm@16614
    64
          (xi, sort_of_term cs) ins env
wenzelm@3778
    65
      | add_env (Abs (_, _, t)) env = add_env t env
wenzelm@3778
    66
      | add_env (t1 $ t2) env = add_env t1 (add_env t2 env)
wenzelm@16614
    67
      | add_env _ env = env;
wenzelm@8895
    68
  in add_env tm [] end;
wenzelm@557
    69
wenzelm@557
    70
wenzelm@2584
    71
(* typ_of_term *)
clasohm@0
    72
wenzelm@12317
    73
fun typ_of_term get_sort map_sort t =
wenzelm@557
    74
  let
wenzelm@557
    75
    fun typ_of (Free (x, _)) =
wenzelm@5690
    76
          if Lexicon.is_tid x then TFree (x, get_sort (x, ~1))
wenzelm@557
    77
          else Type (x, [])
wenzelm@557
    78
      | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
schirmer@14255
    79
      | typ_of (Const ("_tfree",_) $ (t as Free x)) = typ_of t
schirmer@14255
    80
      | typ_of (Const ("_tvar",_) $ (t as Var x)) = typ_of t
wenzelm@12317
    81
      | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
wenzelm@16614
    82
      | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) =
wenzelm@16614
    83
          TFree (x, get_sort (x, ~1))
wenzelm@12317
    84
      | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
wenzelm@16614
    85
      | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) =
wenzelm@16614
    86
          TVar (xi, get_sort xi)
wenzelm@12317
    87
      | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", map_sort (sort_of_term t))
wenzelm@557
    88
      | typ_of tm =
clasohm@0
    89
          let
wenzelm@16614
    90
            val (t, ts) = Term.strip_comb tm;
clasohm@0
    91
            val a =
wenzelm@18
    92
              (case t of
clasohm@0
    93
                Const (x, _) => x
clasohm@0
    94
              | Free (x, _) => x
wenzelm@3778
    95
              | _ => raise TERM ("typ_of_term: bad encoding of type", [tm]));
wenzelm@12317
    96
          in Type (a, map typ_of ts) end;
wenzelm@8895
    97
  in typ_of t end;
clasohm@0
    98
clasohm@0
    99
clasohm@0
   100
wenzelm@2584
   101
(** output utils **)
wenzelm@2584
   102
wenzelm@2699
   103
(* term_of_sort *)
wenzelm@2584
   104
wenzelm@2584
   105
fun term_of_sort S =
wenzelm@2584
   106
  let
wenzelm@5690
   107
    fun class c = Lexicon.const "_class" $ Lexicon.free c;
wenzelm@2584
   108
wenzelm@2584
   109
    fun classes [] = sys_error "term_of_sort"
wenzelm@2584
   110
      | classes [c] = class c
wenzelm@5690
   111
      | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
wenzelm@2584
   112
  in
wenzelm@2584
   113
    (case S of
wenzelm@5690
   114
      [] => Lexicon.const "_topsort"
wenzelm@2584
   115
    | [c] => class c
wenzelm@5690
   116
    | cs => Lexicon.const "_sort" $ classes cs)
wenzelm@2584
   117
  end;
wenzelm@2584
   118
wenzelm@2584
   119
wenzelm@2584
   120
(* term_of_typ *)
clasohm@0
   121
clasohm@0
   122
fun term_of_typ show_sorts ty =
clasohm@0
   123
  let
wenzelm@2584
   124
    fun of_sort t S =
wenzelm@5690
   125
      if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
wenzelm@2584
   126
      else t;
clasohm@0
   127
wenzelm@16614
   128
    fun term_of (Type (a, Ts)) = Term.list_comb (Lexicon.const a, map term_of Ts)
wenzelm@5690
   129
      | term_of (TFree (x, S)) = of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
wenzelm@5690
   130
      | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
wenzelm@8895
   131
  in term_of ty end;
clasohm@0
   132
clasohm@0
   133
clasohm@0
   134
clasohm@0
   135
(** the type syntax **)
clasohm@0
   136
wenzelm@10572
   137
(* print mode *)
wenzelm@10572
   138
wenzelm@10572
   139
val bracketsN = "brackets";
wenzelm@10572
   140
val no_bracketsN = "no_brackets";
wenzelm@10572
   141
wenzelm@10572
   142
fun no_brackets () =
wenzelm@16614
   143
  find_first (equal bracketsN orf equal no_bracketsN) (! print_mode)
wenzelm@16614
   144
    = SOME no_bracketsN;
nipkow@11312
   145
nipkow@11312
   146
val type_bracketsN = "type_brackets";
nipkow@11312
   147
val no_type_bracketsN = "no_type_brackets";
nipkow@11312
   148
nipkow@11312
   149
fun no_type_brackets () =
wenzelm@16614
   150
  Library.find_first (equal type_bracketsN orf equal no_type_bracketsN) (! print_mode)
wenzelm@16614
   151
    <> SOME type_bracketsN;
wenzelm@10572
   152
wenzelm@10572
   153
wenzelm@18
   154
(* parse ast translations *)
clasohm@0
   155
wenzelm@5690
   156
fun tapp_ast_tr (*"_tapp"*) [ty, f] = Ast.Appl [f, ty]
wenzelm@5690
   157
  | tapp_ast_tr (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
wenzelm@347
   158
wenzelm@347
   159
fun tappl_ast_tr (*"_tappl"*) [ty, tys, f] =
wenzelm@5690
   160
      Ast.Appl (f :: ty :: Ast.unfold_ast "_types" tys)
wenzelm@5690
   161
  | tappl_ast_tr (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts);
clasohm@0
   162
clasohm@0
   163
fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
wenzelm@5690
   164
      Ast.fold_ast_p "fun" (Ast.unfold_ast "_types" dom, cod)
wenzelm@5690
   165
  | bracket_ast_tr (*"_bracket"*) asts = raise Ast.AST ("bracket_ast_tr", asts);
clasohm@0
   166
clasohm@0
   167
wenzelm@18
   168
(* print ast translations *)
clasohm@0
   169
wenzelm@5690
   170
fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f])
wenzelm@5690
   171
  | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f]
wenzelm@347
   172
  | tappl_ast_tr' (f, ty :: tys) =
wenzelm@5690
   173
      Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
clasohm@0
   174
clasohm@0
   175
fun fun_ast_tr' (*"fun"*) asts =
wenzelm@16614
   176
  if no_brackets () orelse no_type_brackets () then raise Match
wenzelm@10572
   177
  else
wenzelm@10572
   178
    (case Ast.unfold_ast_p "fun" (Ast.Appl (Ast.Constant "fun" :: asts)) of
wenzelm@10572
   179
      (dom as _ :: _ :: _, cod)
wenzelm@10572
   180
        => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
wenzelm@10572
   181
    | _ => raise Match);
clasohm@0
   182
clasohm@0
   183
clasohm@0
   184
(* type_ext *)
clasohm@0
   185
clasohm@0
   186
val sortT = Type ("sort", []);
clasohm@0
   187
val classesT = Type ("classes", []);
clasohm@0
   188
val typesT = Type ("types", []);
clasohm@0
   189
wenzelm@5690
   190
local open Lexicon SynExt in
wenzelm@5690
   191
wenzelm@14903
   192
val type_ext = syn_ext' false (K false)
wenzelm@347
   193
  [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
wenzelm@239
   194
   Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
wenzelm@239
   195
   Mfix ("_",           idT --> typeT,                 "", [], max_pri),
wenzelm@3829
   196
   Mfix ("_",           longidT --> typeT,             "", [], max_pri),
clasohm@330
   197
   Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
wenzelm@239
   198
   Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
wenzelm@14838
   199
   Mfix ("'_()::_",     sortT --> typeT,               "_dummy_ofsort", [0], max_pri),
wenzelm@239
   200
   Mfix ("_",           idT --> sortT,                 "", [], max_pri),
wenzelm@3829
   201
   Mfix ("_",           longidT --> sortT,             "", [], max_pri),
wenzelm@2584
   202
   Mfix ("{}",          sortT,                         "_topsort", [], max_pri),
wenzelm@239
   203
   Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
wenzelm@239
   204
   Mfix ("_",           idT --> classesT,              "", [], max_pri),
wenzelm@3829
   205
   Mfix ("_",           longidT --> classesT,          "", [], max_pri),
wenzelm@239
   206
   Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
wenzelm@3829
   207
   Mfix ("_,_",         [longidT, classesT] ---> classesT, "_classes", [], max_pri),
clasohm@330
   208
   Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
wenzelm@3829
   209
   Mfix ("_ _",         [typeT, longidT] ---> typeT,   "_tapp", [max_pri, 0], max_pri),
wenzelm@9067
   210
   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
wenzelm@9067
   211
   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
wenzelm@239
   212
   Mfix ("_",           typeT --> typesT,              "", [], max_pri),
wenzelm@239
   213
   Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
wenzelm@239
   214
   Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
clasohm@624
   215
   Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
wenzelm@2678
   216
   Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
wenzelm@2678
   217
   Mfix ("'_",          typeT,                         "dummy", [], max_pri)]
wenzelm@258
   218
  []
wenzelm@15750
   219
  (map SynExt.mk_trfun
wenzelm@16614
   220
   [("_tapp", K tapp_ast_tr), ("_tappl", K tappl_ast_tr), ("_bracket", K bracket_ast_tr)],
wenzelm@239
   221
   [],
wenzelm@239
   222
   [],
wenzelm@16614
   223
   map SynExt.mk_trfun [("fun", K fun_ast_tr')])
wenzelm@15833
   224
  (map (fn s => ("", s, Output.output_width)) SynExt.standard_token_classes)
wenzelm@239
   225
  ([], []);
clasohm@0
   226
clasohm@0
   227
end;
wenzelm@5690
   228
wenzelm@5690
   229
end;