src/Pure/Syntax/type_ext.ML
author wenzelm
Wed Jun 09 18:54:26 2004 +0200 (2004-06-09)
changeset 14903 d264b8ad3eec
parent 14838 b12855d44c97
child 14981 e73f8140af78
permissions -rw-r--r--
removed separate logtypes field of syntax;
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
wenzelm@12785
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
clasohm@0
     5
wenzelm@8895
     6
Utilities for input and output of types.  Also the concrete syntax of
wenzelm@8895
     7
types, which is required to bootstrap Pure.
clasohm@0
     8
*)
clasohm@0
     9
clasohm@0
    10
signature TYPE_EXT0 =
wenzelm@2584
    11
sig
wenzelm@8895
    12
  val sort_of_term: term -> sort
wenzelm@3778
    13
  val raw_term_sorts: term -> (indexname * sort) list
wenzelm@12317
    14
  val typ_of_term: (indexname -> sort) -> (sort -> sort) -> term -> typ
wenzelm@6901
    15
  val term_of_typ: bool -> typ -> term
wenzelm@10572
    16
  val no_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
paulson@1511
    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@8895
    57
    fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) env = ((x, ~1), sort_of_term cs) ins env
schirmer@14255
    58
      | add_env (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ cs) env 
schirmer@14255
    59
                = ((x, ~1), sort_of_term cs) ins env
wenzelm@8895
    60
      | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) env = (xi, sort_of_term cs) ins env
schirmer@14255
    61
      | add_env (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ cs) env 
schirmer@14255
    62
                = (xi, sort_of_term cs) ins env
wenzelm@3778
    63
      | add_env (Abs (_, _, t)) env = add_env t env
wenzelm@3778
    64
      | add_env (t1 $ t2) env = add_env t1 (add_env t2 env)
wenzelm@3778
    65
      | add_env t env = env;
wenzelm@8895
    66
  in add_env tm [] end;
wenzelm@557
    67
wenzelm@557
    68
wenzelm@2584
    69
(* typ_of_term *)
clasohm@0
    70
wenzelm@12317
    71
fun typ_of_term get_sort map_sort t =
wenzelm@557
    72
  let
wenzelm@557
    73
    fun typ_of (Free (x, _)) =
wenzelm@5690
    74
          if Lexicon.is_tid x then TFree (x, get_sort (x, ~1))
wenzelm@557
    75
          else Type (x, [])
wenzelm@557
    76
      | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
schirmer@14255
    77
      | typ_of (Const ("_tfree",_) $ (t as Free x)) = typ_of t
schirmer@14255
    78
      | typ_of (Const ("_tvar",_) $ (t as Var x)) = typ_of t
wenzelm@12317
    79
      | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
schirmer@14255
    80
      | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) 
schirmer@14255
    81
               = TFree (x, get_sort (x, ~1))
wenzelm@12317
    82
      | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
schirmer@14255
    83
      | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) 
schirmer@14255
    84
               = TVar (xi, get_sort xi)
wenzelm@12317
    85
      | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", map_sort (sort_of_term t))
schirmer@14255
    86
     
wenzelm@557
    87
      | typ_of tm =
clasohm@0
    88
          let
clasohm@0
    89
            val (t, ts) = strip_comb tm;
clasohm@0
    90
            val a =
wenzelm@18
    91
              (case t of
clasohm@0
    92
                Const (x, _) => x
clasohm@0
    93
              | Free (x, _) => x
wenzelm@3778
    94
              | _ => raise TERM ("typ_of_term: bad encoding of type", [tm]));
wenzelm@12317
    95
          in Type (a, map typ_of ts) end;
wenzelm@8895
    96
  in typ_of t end;
clasohm@0
    97
clasohm@0
    98
clasohm@0
    99
wenzelm@2584
   100
(** output utils **)
wenzelm@2584
   101
wenzelm@2699
   102
(* term_of_sort *)
wenzelm@2584
   103
wenzelm@2584
   104
fun term_of_sort S =
wenzelm@2584
   105
  let
wenzelm@5690
   106
    fun class c = Lexicon.const "_class" $ Lexicon.free c;
wenzelm@2584
   107
wenzelm@2584
   108
    fun classes [] = sys_error "term_of_sort"
wenzelm@2584
   109
      | classes [c] = class c
wenzelm@5690
   110
      | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
wenzelm@2584
   111
  in
wenzelm@2584
   112
    (case S of
wenzelm@5690
   113
      [] => Lexicon.const "_topsort"
wenzelm@2584
   114
    | [c] => class c
wenzelm@5690
   115
    | cs => Lexicon.const "_sort" $ classes cs)
wenzelm@2584
   116
  end;
wenzelm@2584
   117
wenzelm@2584
   118
wenzelm@2584
   119
(* term_of_typ *)
clasohm@0
   120
clasohm@0
   121
fun term_of_typ show_sorts ty =
clasohm@0
   122
  let
wenzelm@2584
   123
    fun of_sort t S =
wenzelm@5690
   124
      if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
wenzelm@2584
   125
      else t;
clasohm@0
   126
wenzelm@5690
   127
    fun term_of (Type (a, Ts)) = list_comb (Lexicon.const a, map term_of Ts)
wenzelm@5690
   128
      | term_of (TFree (x, S)) = of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
wenzelm@5690
   129
      | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
wenzelm@8895
   130
  in term_of ty end;
clasohm@0
   131
clasohm@0
   132
clasohm@0
   133
clasohm@0
   134
(** the type syntax **)
clasohm@0
   135
wenzelm@10572
   136
(* print mode *)
wenzelm@10572
   137
wenzelm@10572
   138
val bracketsN = "brackets";
wenzelm@10572
   139
val no_bracketsN = "no_brackets";
wenzelm@10572
   140
wenzelm@10572
   141
fun no_brackets () =
nipkow@11312
   142
  Library.find_first (equal bracketsN orf equal no_bracketsN) (! print_mode)
nipkow@11312
   143
  = Some no_bracketsN;
nipkow@11312
   144
nipkow@11312
   145
val type_bracketsN = "type_brackets";
nipkow@11312
   146
val no_type_bracketsN = "no_type_brackets";
nipkow@11312
   147
nipkow@11312
   148
fun no_type_brackets () =
nipkow@11312
   149
  Library.find_first (equal type_bracketsN orf equal no_type_bracketsN)
nipkow@11312
   150
                     (! print_mode)
nipkow@14086
   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 =
nipkow@11312
   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@347
   219
  ([("_tapp", tapp_ast_tr), ("_tappl", tappl_ast_tr), ("_bracket", bracket_ast_tr)],
wenzelm@239
   220
   [],
wenzelm@239
   221
   [],
wenzelm@239
   222
   [("fun", fun_ast_tr')])
wenzelm@2699
   223
  TokenTrans.token_translation
wenzelm@239
   224
  ([], []);
clasohm@0
   225
clasohm@0
   226
end;
wenzelm@5690
   227
wenzelm@5690
   228
end;