src/Pure/Syntax/type_ext.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 18 c9ec452ff08f
permissions -rw-r--r--
Initial revision
clasohm@0
     1
(*  Title:      Pure/Syntax/type_ext
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
clasohm@0
     4
clasohm@0
     5
The concrete syntax of types (used to bootstrap Pure)
clasohm@0
     6
*)
clasohm@0
     7
clasohm@0
     8
signature TYPE_EXT0 =
clasohm@0
     9
sig
clasohm@0
    10
  val typ_of_term: (indexname -> sort) -> term -> typ
clasohm@0
    11
end;
clasohm@0
    12
clasohm@0
    13
signature TYPE_EXT =
clasohm@0
    14
sig
clasohm@0
    15
  include TYPE_EXT0
clasohm@0
    16
  structure Extension: EXTENSION
clasohm@0
    17
  local open Extension Extension.XGram.Ast in
clasohm@0
    18
    val term_of_typ: bool -> typ -> term
clasohm@0
    19
    val tappl_ast_tr': ast * ast list -> ast
clasohm@0
    20
    val type_ext: ext
clasohm@0
    21
  end
clasohm@0
    22
end;
clasohm@0
    23
clasohm@0
    24
functor TypeExtFun(structure Extension: EXTENSION and Lexicon: LEXICON): TYPE_EXT =
clasohm@0
    25
struct
clasohm@0
    26
clasohm@0
    27
structure Extension = Extension;
clasohm@0
    28
open Extension Extension.XGram.Ast;
clasohm@0
    29
clasohm@0
    30
clasohm@0
    31
(** typ_of_term **)   (* FIXME check *)
clasohm@0
    32
clasohm@0
    33
fun typ_of_term def_sort t =
clasohm@0
    34
  let
clasohm@0
    35
    fun sort_err (xi as (x, i)) =
clasohm@0
    36
      error ("typ_of_term: inconsistent sort constraints for type variable " ^
clasohm@0
    37
        (if i < 0 then x else Lexicon.string_of_vname xi));
clasohm@0
    38
clasohm@0
    39
    fun is_tfree name =
clasohm@0
    40
      (case explode name of
clasohm@0
    41
        "'" :: _ :: _ => true
clasohm@0
    42
      | _ :: _ => false
clasohm@0
    43
      | _ => error ("typ_of_term: bad var name " ^ quote name));
clasohm@0
    44
clasohm@0
    45
    fun put_sort scs xi s =
clasohm@0
    46
      (case assoc (scs, xi) of
clasohm@0
    47
        None => (xi, s) :: scs
clasohm@0
    48
      | Some s' =>  if s = s' then scs else sort_err xi);
clasohm@0
    49
clasohm@0
    50
    fun classes (Const (s, _)) = [s]
clasohm@0
    51
      | classes (Free (s, _)) = [s]
clasohm@0
    52
      | classes (Const ("_sortcons", _) $ Const (s, _) $ cls) = s :: classes cls
clasohm@0
    53
      | classes (Const ("_sortcons", _) $ Free (s, _) $ cls) = s :: classes cls
clasohm@0
    54
      | classes tm = raise (TERM ("typ_of_term: bad encoding of classes", [tm]));
clasohm@0
    55
clasohm@0
    56
    fun sort (Const ("_emptysort", _)) = []
clasohm@0
    57
      | sort (Const (s, _)) = [s]
clasohm@0
    58
      | sort (Free (s, _)) = [s]
clasohm@0
    59
      | sort (Const ("_classes", _) $ cls) = classes cls
clasohm@0
    60
      | sort tm = raise (TERM ("typ_of_term: bad encoding of sort", [tm]));
clasohm@0
    61
clasohm@0
    62
    fun typ (Free (x, _), scs) =
clasohm@0
    63
          (if is_tfree x then TFree (x, []) else Type (x, []), scs)
clasohm@0
    64
      | typ (Var (xi, _), scs) = (TVar (xi, []), scs)
clasohm@0
    65
      | typ (Const ("_ofsort", _) $ Free (x, _) $ st, scs) =
clasohm@0
    66
          (TFree (x, []), put_sort scs (x, ~1) (sort st))
clasohm@0
    67
      | typ (Const ("_ofsort", _) $ Var (xi, _) $ st, scs) =
clasohm@0
    68
          (TVar (xi, []), put_sort scs xi (sort st))
clasohm@0
    69
      | typ (Const (a, _), scs) = (Type (a, []), scs)
clasohm@0
    70
      | typ (tm as (_ $ _), scs) =
clasohm@0
    71
          let
clasohm@0
    72
            val (t, ts) = strip_comb tm;
clasohm@0
    73
            val a =
clasohm@0
    74
              case t of
clasohm@0
    75
                Const (x, _) => x
clasohm@0
    76
              | Free (x, _) => x
clasohm@0
    77
              | _ => raise (TERM ("typ_of_term: bad type application", [tm]));
clasohm@0
    78
            val (tys, scs') = typs (ts, scs);
clasohm@0
    79
          in
clasohm@0
    80
            (Type (a, tys), scs')
clasohm@0
    81
          end
clasohm@0
    82
      | typ (tm, _) = raise (TERM ("typ_of_term: bad encoding of typ", [tm]))
clasohm@0
    83
    and typs (t :: ts, scs) =
clasohm@0
    84
          let
clasohm@0
    85
            val (ty, scs') = typ (t, scs);
clasohm@0
    86
            val (tys, scs'') = typs (ts, scs');
clasohm@0
    87
          in (ty :: tys, scs'') end
clasohm@0
    88
      | typs ([], scs) = ([], scs);
clasohm@0
    89
clasohm@0
    90
clasohm@0
    91
    val (ty, scs) = typ (t, []);
clasohm@0
    92
clasohm@0
    93
    fun get_sort xi =
clasohm@0
    94
      (case assoc (scs, xi) of
clasohm@0
    95
        None => def_sort xi
clasohm@0
    96
      | Some s => s);
clasohm@0
    97
clasohm@0
    98
    fun add_sorts (Type (a, tys)) = Type (a, map add_sorts tys)
clasohm@0
    99
      | add_sorts (TVar (xi, _)) = TVar (xi, get_sort xi)
clasohm@0
   100
      | add_sorts (TFree (x, _)) = TFree (x, get_sort (x, ~1));
clasohm@0
   101
  in
clasohm@0
   102
    add_sorts ty
clasohm@0
   103
  end;
clasohm@0
   104
clasohm@0
   105
clasohm@0
   106
clasohm@0
   107
(** term_of_typ **)
clasohm@0
   108
clasohm@0
   109
fun term_of_typ show_sorts ty =
clasohm@0
   110
  let
clasohm@0
   111
    fun const x = Const (x, dummyT);
clasohm@0
   112
clasohm@0
   113
    fun classes [] = raise Match
clasohm@0
   114
      | classes [s] = const s
clasohm@0
   115
      | classes (s :: ss) = const "_sortcons" $ const s $ classes ss;
clasohm@0
   116
clasohm@0
   117
    fun sort [] = const "_emptysort"
clasohm@0
   118
      | sort [s] = const s
clasohm@0
   119
      | sort ss = const "_classes" $ classes ss;
clasohm@0
   120
clasohm@0
   121
    fun of_sort t ss =
clasohm@0
   122
      if show_sorts then const "_ofsort" $ t $ sort ss else t;
clasohm@0
   123
clasohm@0
   124
    fun typ (Type (a, tys)) = list_comb (const a, map typ tys)
clasohm@0
   125
      | typ (TFree (x, ss)) = of_sort (Free (x, dummyT)) ss
clasohm@0
   126
      | typ (TVar (xi, ss)) = of_sort (Var (xi, dummyT)) ss;
clasohm@0
   127
  in
clasohm@0
   128
    typ ty
clasohm@0
   129
  end;
clasohm@0
   130
clasohm@0
   131
clasohm@0
   132
clasohm@0
   133
(** the type syntax **)
clasohm@0
   134
clasohm@0
   135
(* parse translations *)
clasohm@0
   136
clasohm@0
   137
fun tappl_ast_tr (*"_tappl"*) [types, f] = Appl (f :: unfold_ast "_types" types)
clasohm@0
   138
  | tappl_ast_tr (*"_tappl"*) asts = raise_ast "tappl_ast_tr" asts;
clasohm@0
   139
clasohm@0
   140
fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
clasohm@0
   141
      fold_ast_p "fun" (unfold_ast "_types" dom, cod)
clasohm@0
   142
  | bracket_ast_tr (*"_bracket"*) asts = raise_ast "bracket_ast_tr" asts;
clasohm@0
   143
clasohm@0
   144
clasohm@0
   145
(* print translations *)
clasohm@0
   146
clasohm@0
   147
fun tappl_ast_tr' (f, []) = raise_ast "tappl_ast_tr'" [f]
clasohm@0
   148
  | tappl_ast_tr' (f, [ty]) = Appl [Constant "_tapp", ty, f]
clasohm@0
   149
  | tappl_ast_tr' (f, tys) = Appl [Constant "_tappl", fold_ast "_types" tys, f];
clasohm@0
   150
clasohm@0
   151
fun fun_ast_tr' (*"fun"*) asts =
clasohm@0
   152
  (case unfold_ast_p "fun" (Appl (Constant "fun" :: asts)) of
clasohm@0
   153
    (dom as (_ :: _ :: _), cod)
clasohm@0
   154
      => Appl [Constant "_bracket", fold_ast "_types" dom, cod]
clasohm@0
   155
  | _ => raise Match);
clasohm@0
   156
clasohm@0
   157
clasohm@0
   158
(* type_ext *)
clasohm@0
   159
clasohm@0
   160
val sortT = Type ("sort", []);
clasohm@0
   161
val classesT = Type ("classes", []);
clasohm@0
   162
val typesT = Type ("types", []);
clasohm@0
   163
clasohm@0
   164
val type_ext =
clasohm@0
   165
  Ext {
clasohm@0
   166
    roots = [logic, "type"],
clasohm@0
   167
    mfix = [
clasohm@0
   168
      Mfix ("_",           idT --> sortT,                 "", [], max_pri),
clasohm@0
   169
      Mfix ("{}",          sortT,                         "_emptysort", [], max_pri),
clasohm@0
   170
      Mfix ("{_}",         classesT --> sortT,            "_classes", [], max_pri),
clasohm@0
   171
      Mfix ("_",           idT --> classesT,              "", [], max_pri),
clasohm@0
   172
      Mfix ("_,_",         [idT, classesT] ---> classesT, "_sortcons", [], max_pri),
clasohm@0
   173
      Mfix ("_",           tfreeT --> typeT,              "", [], max_pri),
clasohm@0
   174
      Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
clasohm@0
   175
      Mfix ("_",           idT --> typeT,                 "", [], max_pri),
clasohm@0
   176
      Mfix ("_::_",        [tfreeT, sortT] ---> typeT,    "_ofsort", [max_pri, 0], max_pri),
clasohm@0
   177
      Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
clasohm@0
   178
      Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
clasohm@0
   179
      Mfix ("((1'(_'))_)", [typesT, idT] ---> typeT,      "_tappl", [], max_pri),
clasohm@0
   180
      Mfix ("_",           typeT --> typesT,              "", [], max_pri),
clasohm@0
   181
      Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
clasohm@0
   182
      Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
clasohm@0
   183
      Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0)],
clasohm@0
   184
    extra_consts = ["fun"],
clasohm@0
   185
    parse_ast_translation = [("_tapp", tappl_ast_tr), ("_tappl", tappl_ast_tr),
clasohm@0
   186
      ("_bracket", bracket_ast_tr)],
clasohm@0
   187
    parse_preproc = None,
clasohm@0
   188
    parse_postproc = None,
clasohm@0
   189
    parse_translation = [],
clasohm@0
   190
    print_translation = [],
clasohm@0
   191
    print_preproc = None,
clasohm@0
   192
    print_postproc = None,
clasohm@0
   193
    print_ast_translation = [("fun", fun_ast_tr')]};
clasohm@0
   194
clasohm@0
   195
clasohm@0
   196
end;
clasohm@0
   197