src/Pure/Syntax/type_ext.ML
author wenzelm
Fri Aug 19 15:38:18 1994 +0200 (1994-08-19)
changeset 557 9d386e6c02b7
parent 347 cd41a57221d0
child 624 33b9b5da3e6f
permissions -rw-r--r--
added raw_term_sorts and changed typ_of_term accordingly (part of fix
of the typevar-sort-constraint BUG);
various minor internal changes;
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@18
     5
The concrete syntax of types (used to bootstrap Pure).
wenzelm@18
     6
wenzelm@18
     7
TODO:
wenzelm@18
     8
  term_of_typ: prune sorts
clasohm@0
     9
*)
clasohm@0
    10
clasohm@0
    11
signature TYPE_EXT0 =
clasohm@0
    12
sig
wenzelm@557
    13
  val raw_term_sorts: term -> (indexname * sort) list
wenzelm@557
    14
  val typ_of_term: (indexname * sort) list -> (indexname -> sort) -> term -> typ
clasohm@0
    15
end;
clasohm@0
    16
clasohm@0
    17
signature TYPE_EXT =
clasohm@0
    18
sig
clasohm@0
    19
  include TYPE_EXT0
wenzelm@239
    20
  structure SynExt: SYN_EXT
wenzelm@239
    21
  local open SynExt SynExt.Ast in
clasohm@0
    22
    val term_of_typ: bool -> typ -> term
clasohm@0
    23
    val tappl_ast_tr': ast * ast list -> ast
wenzelm@239
    24
    val type_ext: syn_ext
clasohm@0
    25
  end
clasohm@0
    26
end;
clasohm@0
    27
wenzelm@239
    28
functor TypeExtFun(structure Lexicon: LEXICON and SynExt: SYN_EXT): TYPE_EXT =
clasohm@0
    29
struct
clasohm@0
    30
wenzelm@239
    31
structure SynExt = SynExt;
wenzelm@239
    32
open Lexicon SynExt SynExt.Ast;
clasohm@0
    33
clasohm@0
    34
wenzelm@557
    35
(** raw_term_sorts **)
clasohm@0
    36
wenzelm@557
    37
fun raw_term_sorts tm =
wenzelm@557
    38
  let
wenzelm@557
    39
    fun show_var (xi as (x, i)) = if i < 0 then x else string_of_vname xi;
wenzelm@18
    40
wenzelm@18
    41
    fun classes (Const (c, _)) = [c]
wenzelm@18
    42
      | classes (Free (c, _)) = [c]
wenzelm@557
    43
      | classes (Const ("_classes", _) $ Const (c, _) $ cls) = c :: classes cls
wenzelm@557
    44
      | classes (Const ("_classes", _) $ Free (c, _) $ cls) = c :: classes cls
wenzelm@557
    45
      | classes tm = raise_term "raw_term_sorts: bad encoding of classes" [tm];
clasohm@0
    46
clasohm@0
    47
    fun sort (Const ("_emptysort", _)) = []
clasohm@0
    48
      | sort (Const (s, _)) = [s]
clasohm@0
    49
      | sort (Free (s, _)) = [s]
wenzelm@18
    50
      | sort (Const ("_sort", _) $ cls) = classes cls
wenzelm@557
    51
      | sort tm = raise_term "raw_term_sorts: bad encoding of sort" [tm];
wenzelm@557
    52
wenzelm@557
    53
    fun env_of (Const ("_ofsort", _) $ Free (x, _) $ srt) = [((x, ~1), sort srt)]
wenzelm@557
    54
      | env_of (Const ("_ofsort", _) $ Var (xi, _) $ srt) = [(xi, sort srt)]
wenzelm@557
    55
      | env_of (Abs (_, _, t)) = env_of t
wenzelm@557
    56
      | env_of (t1 $ t2) = env_of t1 @ env_of t2
wenzelm@557
    57
      | env_of t = [];
wenzelm@557
    58
wenzelm@557
    59
    val env = distinct (env_of tm);
wenzelm@557
    60
  in
wenzelm@557
    61
    (case gen_duplicates eq_fst env of
wenzelm@557
    62
      [] => env
wenzelm@557
    63
    | dups => error ("Inconsistent sort constraints for type variable(s) " ^
wenzelm@557
    64
        commas (map (quote o show_var o #1) dups)))
wenzelm@557
    65
  end;
wenzelm@557
    66
wenzelm@557
    67
clasohm@0
    68
wenzelm@557
    69
(** typ_of_term **)
wenzelm@557
    70
wenzelm@557
    71
fun typ_of_term sort_env def_sort t =
wenzelm@557
    72
  let
wenzelm@557
    73
    fun get_sort xi =
wenzelm@557
    74
      (case assoc (sort_env, xi) of
wenzelm@557
    75
        None => def_sort xi
wenzelm@557
    76
      | Some s => s);
wenzelm@557
    77
wenzelm@557
    78
    fun typ_of (Free (x, _)) =
wenzelm@557
    79
          if is_tid x then TFree (x, get_sort (x, ~1))
wenzelm@557
    80
          else Type (x, [])
wenzelm@557
    81
      | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
wenzelm@557
    82
      | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) =
wenzelm@557
    83
          TFree (x, get_sort (x, ~1))
wenzelm@557
    84
      | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) =
wenzelm@557
    85
          TVar (xi, get_sort xi)
wenzelm@557
    86
      | typ_of tm =
clasohm@0
    87
          let
clasohm@0
    88
            val (t, ts) = strip_comb tm;
clasohm@0
    89
            val a =
wenzelm@18
    90
              (case t of
clasohm@0
    91
                Const (x, _) => x
clasohm@0
    92
              | Free (x, _) => x
wenzelm@557
    93
              | _ => raise_term "typ_of_term: bad encoding of type" [tm]);
clasohm@0
    94
          in
wenzelm@557
    95
            Type (a, map typ_of ts)
wenzelm@557
    96
          end;
clasohm@0
    97
  in
wenzelm@557
    98
    typ_of t
clasohm@0
    99
  end;
clasohm@0
   100
clasohm@0
   101
clasohm@0
   102
clasohm@0
   103
(** term_of_typ **)
clasohm@0
   104
clasohm@0
   105
fun term_of_typ show_sorts ty =
clasohm@0
   106
  let
clasohm@0
   107
    fun classes [] = raise Match
wenzelm@18
   108
      | classes [c] = free c
wenzelm@18
   109
      | classes (c :: cs) = const "_classes" $ free c $ classes cs;
clasohm@0
   110
clasohm@0
   111
    fun sort [] = const "_emptysort"
wenzelm@18
   112
      | sort [s] = free s
wenzelm@18
   113
      | sort ss = const "_sort" $ classes ss;
clasohm@0
   114
clasohm@0
   115
    fun of_sort t ss =
clasohm@0
   116
      if show_sorts then const "_ofsort" $ t $ sort ss else t;
clasohm@0
   117
wenzelm@18
   118
    fun term_of (Type (a, tys)) = list_comb (const a, map term_of tys)
wenzelm@18
   119
      | term_of (TFree (x, ss)) = of_sort (free x) ss
wenzelm@18
   120
      | term_of (TVar (xi, ss)) = of_sort (var xi) ss;
clasohm@0
   121
  in
wenzelm@18
   122
    term_of ty
clasohm@0
   123
  end;
clasohm@0
   124
clasohm@0
   125
clasohm@0
   126
clasohm@0
   127
(** the type syntax **)
clasohm@0
   128
wenzelm@18
   129
(* parse ast translations *)
clasohm@0
   130
wenzelm@347
   131
fun tapp_ast_tr (*"_tapp"*) [ty, f] = Appl [f, ty]
wenzelm@347
   132
  | tapp_ast_tr (*"_tapp"*) asts = raise_ast "tapp_ast_tr" asts;
wenzelm@347
   133
wenzelm@347
   134
fun tappl_ast_tr (*"_tappl"*) [ty, tys, f] =
wenzelm@347
   135
      Appl (f :: ty :: unfold_ast "_types" tys)
wenzelm@347
   136
  | tappl_ast_tr (*"_tappl"*) asts = raise_ast "tappl_ast_tr" asts;
clasohm@0
   137
clasohm@0
   138
fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
clasohm@0
   139
      fold_ast_p "fun" (unfold_ast "_types" dom, cod)
clasohm@0
   140
  | bracket_ast_tr (*"_bracket"*) asts = raise_ast "bracket_ast_tr" asts;
clasohm@0
   141
clasohm@0
   142
wenzelm@18
   143
(* print ast translations *)
clasohm@0
   144
clasohm@0
   145
fun tappl_ast_tr' (f, []) = raise_ast "tappl_ast_tr'" [f]
clasohm@0
   146
  | tappl_ast_tr' (f, [ty]) = Appl [Constant "_tapp", ty, f]
wenzelm@347
   147
  | tappl_ast_tr' (f, ty :: tys) =
wenzelm@347
   148
      Appl [Constant "_tappl", ty, fold_ast "_types" tys, f];
clasohm@0
   149
clasohm@0
   150
fun fun_ast_tr' (*"fun"*) asts =
clasohm@0
   151
  (case unfold_ast_p "fun" (Appl (Constant "fun" :: asts)) of
wenzelm@18
   152
    (dom as _ :: _ :: _, cod)
clasohm@0
   153
      => Appl [Constant "_bracket", fold_ast "_types" dom, cod]
clasohm@0
   154
  | _ => raise Match);
clasohm@0
   155
clasohm@0
   156
clasohm@0
   157
(* type_ext *)
clasohm@0
   158
clasohm@0
   159
val sortT = Type ("sort", []);
clasohm@0
   160
val classesT = Type ("classes", []);
clasohm@0
   161
val typesT = Type ("types", []);
clasohm@0
   162
wenzelm@239
   163
val type_ext = syn_ext
clasohm@330
   164
  [logic, "type"] [logic, "type"]
wenzelm@347
   165
  [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
wenzelm@239
   166
   Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
wenzelm@239
   167
   Mfix ("_",           idT --> typeT,                 "", [], max_pri),
clasohm@330
   168
   Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
wenzelm@239
   169
   Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
wenzelm@239
   170
   Mfix ("_",           idT --> sortT,                 "", [], max_pri),
wenzelm@239
   171
   Mfix ("{}",          sortT,                         "_emptysort", [], max_pri),
wenzelm@239
   172
   Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
wenzelm@239
   173
   Mfix ("_",           idT --> classesT,              "", [], max_pri),
wenzelm@239
   174
   Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
clasohm@330
   175
   Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
clasohm@330
   176
   Mfix ("((1'(_,/ _'))_)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
wenzelm@239
   177
   Mfix ("_",           typeT --> typesT,              "", [], max_pri),
wenzelm@239
   178
   Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
wenzelm@239
   179
   Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
wenzelm@239
   180
   Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0)]
wenzelm@258
   181
  []
wenzelm@347
   182
  ([("_tapp", tapp_ast_tr), ("_tappl", tappl_ast_tr), ("_bracket", bracket_ast_tr)],
wenzelm@239
   183
   [],
wenzelm@239
   184
   [],
wenzelm@239
   185
   [("fun", fun_ast_tr')])
wenzelm@239
   186
  ([], []);
clasohm@0
   187
clasohm@0
   188
clasohm@0
   189
end;
clasohm@0
   190