src/Pure/Syntax/type_ext.ML
author wenzelm
Mon Oct 04 15:30:49 1993 +0100 (1993-10-04)
changeset 18 c9ec452ff08f
parent 0 a5a9c433f639
child 239 08b6e842ec16
permissions -rw-r--r--
lots of internal cleaning and tuning;
removed {parse,print}_{pre,post}_proc;
new lexer: now human readable due to scanner combinators;
new parser installed, but still inactive (due to grammar ambiguities);
added Syntax.test_read;
typ_of_term: sorts now made distinct and sorted;
mixfix: added forced line breaks (//);
PROP now printed before subterm of type prop with non-const head;
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
wenzelm@18
     9
  move "_K" (?)
clasohm@0
    10
*)
clasohm@0
    11
clasohm@0
    12
signature TYPE_EXT0 =
clasohm@0
    13
sig
clasohm@0
    14
  val typ_of_term: (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
clasohm@0
    20
  structure Extension: EXTENSION
clasohm@0
    21
  local open Extension Extension.XGram.Ast in
clasohm@0
    22
    val term_of_typ: bool -> typ -> term
clasohm@0
    23
    val tappl_ast_tr': ast * ast list -> ast
clasohm@0
    24
    val type_ext: ext
clasohm@0
    25
  end
clasohm@0
    26
end;
clasohm@0
    27
clasohm@0
    28
functor TypeExtFun(structure Extension: EXTENSION and Lexicon: LEXICON): TYPE_EXT =
clasohm@0
    29
struct
clasohm@0
    30
clasohm@0
    31
structure Extension = Extension;
wenzelm@18
    32
open Extension Extension.XGram Extension.XGram.Ast Lexicon;
clasohm@0
    33
clasohm@0
    34
wenzelm@18
    35
(** typ_of_term **)
clasohm@0
    36
clasohm@0
    37
fun typ_of_term def_sort t =
clasohm@0
    38
  let
clasohm@0
    39
    fun sort_err (xi as (x, i)) =
wenzelm@18
    40
      error ("Inconsistent sort constraints for type variable " ^
wenzelm@18
    41
        quote (if i < 0 then x else string_of_vname xi));
clasohm@0
    42
clasohm@0
    43
    fun put_sort scs xi s =
clasohm@0
    44
      (case assoc (scs, xi) of
clasohm@0
    45
        None => (xi, s) :: scs
clasohm@0
    46
      | Some s' =>  if s = s' then scs else sort_err xi);
clasohm@0
    47
wenzelm@18
    48
    fun insert x [] = [x: string]
wenzelm@18
    49
      | insert x (lst as y :: ys) =
wenzelm@18
    50
          if x > y then y :: insert x ys
wenzelm@18
    51
          else if x = y then lst
wenzelm@18
    52
          else x :: lst;
wenzelm@18
    53
wenzelm@18
    54
    fun classes (Const (c, _)) = [c]
wenzelm@18
    55
      | classes (Free (c, _)) = [c]
wenzelm@18
    56
      | classes (Const ("_classes", _) $ Const (c, _) $ cls) =
wenzelm@18
    57
          insert c (classes cls)
wenzelm@18
    58
      | classes (Const ("_classes", _) $ Free (c, _) $ cls) =
wenzelm@18
    59
          insert c (classes cls)
wenzelm@18
    60
      | classes tm = raise_term "typ_of_term: bad encoding of classes" [tm];
clasohm@0
    61
clasohm@0
    62
    fun sort (Const ("_emptysort", _)) = []
clasohm@0
    63
      | sort (Const (s, _)) = [s]
clasohm@0
    64
      | sort (Free (s, _)) = [s]
wenzelm@18
    65
      | sort (Const ("_sort", _) $ cls) = classes cls
wenzelm@18
    66
      | sort tm = raise_term "typ_of_term: bad encoding of sort" [tm];
clasohm@0
    67
clasohm@0
    68
    fun typ (Free (x, _), scs) =
clasohm@0
    69
          (if is_tfree x then TFree (x, []) else Type (x, []), scs)
clasohm@0
    70
      | typ (Var (xi, _), scs) = (TVar (xi, []), scs)
clasohm@0
    71
      | typ (Const ("_ofsort", _) $ Free (x, _) $ st, scs) =
clasohm@0
    72
          (TFree (x, []), put_sort scs (x, ~1) (sort st))
clasohm@0
    73
      | typ (Const ("_ofsort", _) $ Var (xi, _) $ st, scs) =
clasohm@0
    74
          (TVar (xi, []), put_sort scs xi (sort st))
clasohm@0
    75
      | typ (Const (a, _), scs) = (Type (a, []), scs)
wenzelm@18
    76
      | typ (tm as _ $ _, scs) =
clasohm@0
    77
          let
clasohm@0
    78
            val (t, ts) = strip_comb tm;
clasohm@0
    79
            val a =
wenzelm@18
    80
              (case t of
clasohm@0
    81
                Const (x, _) => x
clasohm@0
    82
              | Free (x, _) => x
wenzelm@18
    83
              | _ => raise_term "typ_of_term: bad type application" [tm]);
clasohm@0
    84
            val (tys, scs') = typs (ts, scs);
clasohm@0
    85
          in
clasohm@0
    86
            (Type (a, tys), scs')
clasohm@0
    87
          end
wenzelm@18
    88
      | typ (tm, _) = raise_term "typ_of_term: bad encoding of typ" [tm]
clasohm@0
    89
    and typs (t :: ts, scs) =
clasohm@0
    90
          let
clasohm@0
    91
            val (ty, scs') = typ (t, scs);
clasohm@0
    92
            val (tys, scs'') = typs (ts, scs');
clasohm@0
    93
          in (ty :: tys, scs'') end
clasohm@0
    94
      | typs ([], scs) = ([], scs);
clasohm@0
    95
clasohm@0
    96
clasohm@0
    97
    val (ty, scs) = typ (t, []);
clasohm@0
    98
clasohm@0
    99
    fun get_sort xi =
clasohm@0
   100
      (case assoc (scs, xi) of
clasohm@0
   101
        None => def_sort xi
clasohm@0
   102
      | Some s => s);
clasohm@0
   103
clasohm@0
   104
    fun add_sorts (Type (a, tys)) = Type (a, map add_sorts tys)
clasohm@0
   105
      | add_sorts (TVar (xi, _)) = TVar (xi, get_sort xi)
clasohm@0
   106
      | add_sorts (TFree (x, _)) = TFree (x, get_sort (x, ~1));
clasohm@0
   107
  in
clasohm@0
   108
    add_sorts ty
clasohm@0
   109
  end;
clasohm@0
   110
clasohm@0
   111
clasohm@0
   112
clasohm@0
   113
(** term_of_typ **)
clasohm@0
   114
clasohm@0
   115
fun term_of_typ show_sorts ty =
clasohm@0
   116
  let
clasohm@0
   117
    fun const x = Const (x, dummyT);
wenzelm@18
   118
    fun free x = Free (x, dummyT);
wenzelm@18
   119
    fun var xi = Var (xi, dummyT);
clasohm@0
   120
clasohm@0
   121
    fun classes [] = raise Match
wenzelm@18
   122
      | classes [c] = free c
wenzelm@18
   123
      | classes (c :: cs) = const "_classes" $ free c $ classes cs;
clasohm@0
   124
clasohm@0
   125
    fun sort [] = const "_emptysort"
wenzelm@18
   126
      | sort [s] = free s
wenzelm@18
   127
      | sort ss = const "_sort" $ classes ss;
clasohm@0
   128
clasohm@0
   129
    fun of_sort t ss =
clasohm@0
   130
      if show_sorts then const "_ofsort" $ t $ sort ss else t;
clasohm@0
   131
wenzelm@18
   132
    fun term_of (Type (a, tys)) = list_comb (const a, map term_of tys)
wenzelm@18
   133
      | term_of (TFree (x, ss)) = of_sort (free x) ss
wenzelm@18
   134
      | term_of (TVar (xi, ss)) = of_sort (var xi) ss;
clasohm@0
   135
  in
wenzelm@18
   136
    term_of ty
clasohm@0
   137
  end;
clasohm@0
   138
clasohm@0
   139
clasohm@0
   140
clasohm@0
   141
(** the type syntax **)
clasohm@0
   142
wenzelm@18
   143
(* parse ast translations *)
clasohm@0
   144
wenzelm@18
   145
fun tappl_ast_tr (*"_tapp(l)"*) [types, f] =
wenzelm@18
   146
      Appl (f :: unfold_ast "_types" types)
wenzelm@18
   147
  | tappl_ast_tr (*"_tapp(l)"*) asts = raise_ast "tappl_ast_tr" asts;
clasohm@0
   148
clasohm@0
   149
fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
clasohm@0
   150
      fold_ast_p "fun" (unfold_ast "_types" dom, cod)
clasohm@0
   151
  | bracket_ast_tr (*"_bracket"*) asts = raise_ast "bracket_ast_tr" asts;
clasohm@0
   152
clasohm@0
   153
wenzelm@18
   154
(* print ast translations *)
clasohm@0
   155
clasohm@0
   156
fun tappl_ast_tr' (f, []) = raise_ast "tappl_ast_tr'" [f]
clasohm@0
   157
  | tappl_ast_tr' (f, [ty]) = Appl [Constant "_tapp", ty, f]
clasohm@0
   158
  | tappl_ast_tr' (f, tys) = Appl [Constant "_tappl", fold_ast "_types" tys, f];
clasohm@0
   159
clasohm@0
   160
fun fun_ast_tr' (*"fun"*) asts =
clasohm@0
   161
  (case unfold_ast_p "fun" (Appl (Constant "fun" :: asts)) of
wenzelm@18
   162
    (dom as _ :: _ :: _, cod)
clasohm@0
   163
      => Appl [Constant "_bracket", fold_ast "_types" dom, cod]
clasohm@0
   164
  | _ => raise Match);
clasohm@0
   165
clasohm@0
   166
clasohm@0
   167
(* type_ext *)
clasohm@0
   168
clasohm@0
   169
val sortT = Type ("sort", []);
clasohm@0
   170
val classesT = Type ("classes", []);
clasohm@0
   171
val typesT = Type ("types", []);
clasohm@0
   172
clasohm@0
   173
val type_ext =
clasohm@0
   174
  Ext {
clasohm@0
   175
    roots = [logic, "type"],
clasohm@0
   176
    mfix = [
clasohm@0
   177
      Mfix ("_",           tfreeT --> typeT,              "", [], max_pri),
clasohm@0
   178
      Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
clasohm@0
   179
      Mfix ("_",           idT --> typeT,                 "", [], max_pri),
clasohm@0
   180
      Mfix ("_::_",        [tfreeT, sortT] ---> typeT,    "_ofsort", [max_pri, 0], max_pri),
clasohm@0
   181
      Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
wenzelm@18
   182
      Mfix ("_",           idT --> sortT,                 "", [], max_pri),
wenzelm@18
   183
      Mfix ("{}",          sortT,                         "_emptysort", [], max_pri),
wenzelm@18
   184
      Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
wenzelm@18
   185
      Mfix ("_",           idT --> classesT,              "", [], max_pri),
wenzelm@18
   186
      Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
wenzelm@18
   187
      Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),  (* FIXME ambiguous *)
wenzelm@18
   188
      Mfix ("((1'(_'))_)", [typesT, idT] ---> typeT,      "_tappl", [], max_pri),           (* FIXME ambiguous *)
clasohm@0
   189
      Mfix ("_",           typeT --> typesT,              "", [], max_pri),
clasohm@0
   190
      Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
clasohm@0
   191
      Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
clasohm@0
   192
      Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0)],
wenzelm@18
   193
    extra_consts = ["_K"],
clasohm@0
   194
    parse_ast_translation = [("_tapp", tappl_ast_tr), ("_tappl", tappl_ast_tr),
clasohm@0
   195
      ("_bracket", bracket_ast_tr)],
clasohm@0
   196
    parse_translation = [],
clasohm@0
   197
    print_translation = [],
clasohm@0
   198
    print_ast_translation = [("fun", fun_ast_tr')]};
clasohm@0
   199
clasohm@0
   200
clasohm@0
   201
end;
clasohm@0
   202