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