src/Pure/type.ML
author wenzelm
Tue Sep 06 13:09:58 1994 +0200 (1994-09-06 ago)
changeset 582 8f1f1fab70ad
parent 565 653b752e2ddb
child 585 409c9ee7a9f3
permissions -rw-r--r--
added ext_tsig_types;
various minor changes;
wenzelm@256
     1
(*  Title:      Pure/type.ML
clasohm@0
     2
    ID:         $Id$
wenzelm@416
     3
    Author:     Tobias Nipkow & Lawrence C Paulson
clasohm@0
     4
wenzelm@416
     5
Type classes and sorts. Type signatures. Type unification and inference.
wenzelm@256
     6
wenzelm@256
     7
TODO:
wenzelm@416
     8
  move type unification and inference to type_unify.ML (TypeUnify) (?)
wenzelm@416
     9
  rename args -> tycons, coreg -> arities (?)
wenzelm@416
    10
  clean err msgs
clasohm@0
    11
*)
clasohm@0
    12
clasohm@0
    13
signature TYPE =
clasohm@0
    14
sig
wenzelm@256
    15
  structure Symtab: SYMTAB
wenzelm@416
    16
  val str_of_sort: sort -> string
wenzelm@416
    17
  val str_of_arity: string * sort list * sort -> string
clasohm@0
    18
  type type_sig
nipkow@200
    19
  val rep_tsig: type_sig ->
wenzelm@256
    20
    {classes: class list,
wenzelm@256
    21
     subclass: (class * class list) list,
wenzelm@256
    22
     default: sort,
wenzelm@256
    23
     args: (string * int) list,
wenzelm@256
    24
     abbrs: (string * (indexname list * typ)) list,
wenzelm@256
    25
     coreg: (string * (class * sort list) list) list}
clasohm@0
    26
  val defaultS: type_sig -> sort
wenzelm@416
    27
  val tsig0: type_sig
wenzelm@256
    28
  val logical_types: type_sig -> string list
wenzelm@256
    29
  val extend_tsig: type_sig ->
wenzelm@256
    30
    (class * class list) list * sort * (string list * int) list *
wenzelm@256
    31
    (string list * (sort list * class)) list -> type_sig
wenzelm@422
    32
  val ext_tsig_subclass: type_sig -> (class * class) list -> type_sig
wenzelm@422
    33
  val ext_tsig_defsort: type_sig -> sort -> type_sig
wenzelm@582
    34
  val ext_tsig_types: type_sig -> (string * int) list -> type_sig
wenzelm@256
    35
  val ext_tsig_abbrs: type_sig -> (string * (indexname list * typ)) list
wenzelm@256
    36
    -> type_sig
wenzelm@256
    37
  val merge_tsigs: type_sig * type_sig -> type_sig
wenzelm@416
    38
  val subsort: type_sig -> sort * sort -> bool
wenzelm@416
    39
  val norm_sort: type_sig -> sort -> sort
wenzelm@416
    40
  val rem_sorts: typ -> typ
wenzelm@256
    41
  val cert_typ: type_sig -> typ -> typ
wenzelm@256
    42
  val norm_typ: type_sig -> typ -> typ
clasohm@0
    43
  val freeze: (indexname -> bool) -> term -> term
clasohm@0
    44
  val freeze_vars: typ -> typ
wenzelm@565
    45
  val infer_types: type_sig * (string -> typ option) * (indexname -> typ option) *
wenzelm@256
    46
    (indexname -> sort option) * typ * term -> term * (indexname * typ) list
wenzelm@256
    47
  val inst_term_tvars: type_sig * (indexname * typ) list -> term -> term
clasohm@0
    48
  val thaw_vars: typ -> typ
wenzelm@256
    49
  val typ_errors: type_sig -> typ * string list -> string list
clasohm@0
    50
  val typ_instance: type_sig * typ * typ -> bool
wenzelm@256
    51
  val typ_match: type_sig -> (indexname * typ) list * (typ * typ)
wenzelm@256
    52
    -> (indexname * typ) list
wenzelm@256
    53
  val unify: type_sig -> (typ * typ) * (indexname * typ) list
wenzelm@256
    54
    -> (indexname * typ) list
wenzelm@450
    55
  val raw_unify: typ * typ -> bool
clasohm@0
    56
  val varifyT: typ -> typ
clasohm@0
    57
  val varify: term * string list -> term
clasohm@0
    58
  exception TUNIFY
wenzelm@256
    59
  exception TYPE_MATCH
clasohm@0
    60
end;
clasohm@0
    61
wenzelm@416
    62
functor TypeFun(structure Symtab: SYMTAB and Syntax: SYNTAX): TYPE =
clasohm@0
    63
struct
clasohm@0
    64
wenzelm@256
    65
structure Symtab = Symtab;
clasohm@0
    66
clasohm@0
    67
wenzelm@416
    68
(*** type classes and sorts ***)
wenzelm@416
    69
wenzelm@416
    70
(*
wenzelm@416
    71
  Classes denote (possibly empty) collections of types (e.g. sets of types)
wenzelm@416
    72
  and are partially ordered by 'inclusion'. They are represented by strings.
wenzelm@416
    73
wenzelm@416
    74
  Sorts are intersections of finitely many classes. They are represented by
wenzelm@416
    75
  lists of classes.
wenzelm@416
    76
*)
clasohm@0
    77
clasohm@0
    78
type domain = sort list;
wenzelm@416
    79
wenzelm@416
    80
wenzelm@416
    81
(* print sorts and arities *)
clasohm@0
    82
wenzelm@416
    83
fun str_of_sort [c] = c
wenzelm@565
    84
  | str_of_sort cs = enclose "{" "}" (commas cs);
wenzelm@416
    85
wenzelm@565
    86
fun str_of_dom dom = enclose "(" ")" (commas (map str_of_sort dom));
wenzelm@416
    87
wenzelm@416
    88
fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S
wenzelm@416
    89
  | str_of_arity (t, SS, S) =
wenzelm@416
    90
      t ^ " :: " ^ str_of_dom SS ^ " " ^ str_of_sort S;
wenzelm@256
    91
wenzelm@256
    92
wenzelm@256
    93
wenzelm@416
    94
(*** type signatures ***)
wenzelm@256
    95
wenzelm@256
    96
(*
wenzelm@256
    97
  classes:
wenzelm@256
    98
    a list of all declared classes;
clasohm@0
    99
wenzelm@256
   100
  subclass:
wenzelm@416
   101
    an association list representing the subclass relation; (c, cs) is
wenzelm@256
   102
    interpreted as "c is a proper subclass of all elemenst of cs"; note that
wenzelm@256
   103
    c itself is not a memeber of cs;
wenzelm@256
   104
wenzelm@256
   105
  default:
wenzelm@256
   106
    the default sort attached to all unconstrained type vars;
wenzelm@256
   107
wenzelm@256
   108
  args:
wenzelm@256
   109
    an association list of all declared types with the number of their
wenzelm@256
   110
    arguments;
wenzelm@256
   111
wenzelm@256
   112
  abbrs:
wenzelm@256
   113
    an association list of type abbreviations;
wenzelm@256
   114
wenzelm@256
   115
  coreg:
wenzelm@256
   116
    a two-fold association list of all type arities; (t, al) means that type
wenzelm@256
   117
    constructor t has the arities in al; an element (c, ss) of al represents
wenzelm@256
   118
    the arity (ss)c;
clasohm@0
   119
*)
clasohm@0
   120
wenzelm@256
   121
datatype type_sig =
wenzelm@256
   122
  TySg of {
wenzelm@256
   123
    classes: class list,
wenzelm@256
   124
    subclass: (class * class list) list,
wenzelm@256
   125
    default: sort,
wenzelm@256
   126
    args: (string * int) list,
wenzelm@256
   127
    abbrs: (string * (indexname list * typ)) list,
wenzelm@256
   128
    coreg: (string * (class * domain) list) list};
wenzelm@256
   129
nipkow@189
   130
fun rep_tsig (TySg comps) = comps;
clasohm@0
   131
wenzelm@256
   132
fun defaultS (TySg {default, ...}) = default;
wenzelm@256
   133
wenzelm@256
   134
wenzelm@582
   135
(* error messages *)
wenzelm@256
   136
wenzelm@416
   137
fun undcl_class c = "Undeclared class " ^ quote c;
wenzelm@256
   138
val err_undcl_class = error o undcl_class;
clasohm@0
   139
wenzelm@422
   140
fun err_dup_classes cs =
wenzelm@422
   141
  error ("Duplicate declaration of class(es) " ^ commas_quote cs);
wenzelm@416
   142
wenzelm@416
   143
fun undcl_type c = "Undeclared type constructor " ^ quote c;
wenzelm@256
   144
val err_undcl_type = error o undcl_type;
wenzelm@256
   145
wenzelm@582
   146
fun err_neg_args c =
wenzelm@582
   147
  error ("Negative number of arguments of type constructor " ^ quote c);
wenzelm@582
   148
wenzelm@416
   149
fun err_dup_tycon c =
wenzelm@416
   150
  error ("Duplicate declaration of type constructor " ^ quote c);
wenzelm@416
   151
wenzelm@416
   152
fun err_dup_tyabbr c =
wenzelm@416
   153
  error ("Duplicate declaration of type abbreviation " ^ quote c);
wenzelm@416
   154
wenzelm@416
   155
fun ty_confl c = "Conflicting type constructor and abbreviation " ^ quote c;
wenzelm@416
   156
val err_ty_confl = error o ty_confl;
clasohm@0
   157
clasohm@0
   158
clasohm@0
   159
(* 'leq' checks the partial order on classes according to the
clasohm@0
   160
   statements in the association list 'a' (i.e.'subclass')
clasohm@0
   161
*)
clasohm@0
   162
wenzelm@256
   163
fun less a (C, D) = case assoc (a, C) of
clasohm@0
   164
     Some(ss) => D mem ss
wenzelm@256
   165
   | None => err_undcl_class (C) ;
clasohm@0
   166
wenzelm@256
   167
fun leq a (C, D)  =  C = D orelse less a (C, D);
clasohm@0
   168
clasohm@0
   169
wenzelm@416
   170
(* logical_types *)
clasohm@0
   171
wenzelm@416
   172
(*return all logical types of tsig, i.e. all types t with some arity t::(ss)c
wenzelm@416
   173
  and c <= logic*)
clasohm@0
   174
wenzelm@416
   175
fun logical_types tsig =
wenzelm@416
   176
  let
wenzelm@416
   177
    val TySg {subclass, coreg, args, ...} = tsig;
wenzelm@416
   178
wenzelm@416
   179
    fun log_class c = leq subclass (c, logicC);
wenzelm@416
   180
    fun log_type t = exists (log_class o #1) (assocs coreg t);
wenzelm@416
   181
  in
wenzelm@416
   182
    filter log_type (map #1 args)
clasohm@0
   183
  end;
clasohm@0
   184
nipkow@162
   185
wenzelm@256
   186
(* 'sortorder' checks the ordering on sets of classes, i.e. on sorts:
wenzelm@256
   187
   S1 <= S2 , iff for every class C2 in S2 there exists a class C1 in S1
clasohm@0
   188
   with C1 <= C2 (according to an association list 'a')
clasohm@0
   189
*)
clasohm@0
   190
wenzelm@256
   191
fun sortorder a (S1, S2) =
wenzelm@256
   192
  forall  (fn C2 => exists  (fn C1 => leq a (C1, C2))  S1)  S2;
clasohm@0
   193
clasohm@0
   194
clasohm@0
   195
(* 'inj' inserts a new class C into a given class set S (i.e.sort) only if
clasohm@0
   196
  there exists no class in S which is <= C;
clasohm@0
   197
  the resulting set is minimal if S was minimal
clasohm@0
   198
*)
clasohm@0
   199
wenzelm@256
   200
fun inj a (C, S) =
clasohm@0
   201
  let fun inj1 [] = [C]
wenzelm@256
   202
        | inj1 (D::T) = if leq a (D, C) then D::T
wenzelm@256
   203
                        else if leq a (C, D) then inj1 T
clasohm@0
   204
                             else D::(inj1 T)
clasohm@0
   205
  in inj1 S end;
clasohm@0
   206
clasohm@0
   207
clasohm@0
   208
(* 'union_sort' forms the minimal union set of two sorts S1 and S2
clasohm@0
   209
   under the assumption that S2 is minimal *)
wenzelm@256
   210
(* FIXME rename to inter_sort (?) *)
clasohm@0
   211
clasohm@0
   212
fun union_sort a = foldr (inj a);
clasohm@0
   213
clasohm@0
   214
clasohm@0
   215
(* 'elementwise_union' forms elementwise the minimal union set of two
clasohm@0
   216
   sort lists under the assumption that the two lists have the same length
wenzelm@256
   217
*)
clasohm@0
   218
wenzelm@256
   219
fun elementwise_union a (Ss1, Ss2) = map (union_sort a) (Ss1~~Ss2);
wenzelm@256
   220
clasohm@0
   221
clasohm@0
   222
(* 'lew' checks for two sort lists the ordering for all corresponding list
clasohm@0
   223
   elements (i.e. sorts) *)
clasohm@0
   224
wenzelm@256
   225
fun lew a (w1, w2) = forall (sortorder a)  (w1~~w2);
wenzelm@256
   226
clasohm@0
   227
wenzelm@256
   228
(* 'is_min' checks if a class C is minimal in a given sort S under the
wenzelm@256
   229
   assumption that S contains C *)
clasohm@0
   230
wenzelm@256
   231
fun is_min a S C = not (exists (fn (D) => less a (D, C)) S);
clasohm@0
   232
clasohm@0
   233
clasohm@0
   234
(* 'min_sort' reduces a sort to its minimal classes *)
clasohm@0
   235
clasohm@0
   236
fun min_sort a S = distinct(filter (is_min a S) S);
clasohm@0
   237
clasohm@0
   238
clasohm@0
   239
(* 'min_domain' minimizes the domain sorts of type declarationsl;
wenzelm@256
   240
   the function will be applied on the type declarations in extensions *)
clasohm@0
   241
clasohm@0
   242
fun min_domain subclass =
wenzelm@256
   243
  let fun one_min (f, (doms, ran)) = (f, (map (min_sort subclass) doms, ran))
clasohm@0
   244
  in map one_min end;
clasohm@0
   245
clasohm@0
   246
clasohm@0
   247
(* 'min_filter' filters a list 'ars' consisting of arities (domain * class)
wenzelm@256
   248
   and gives back a list of those range classes whose domains meet the
clasohm@0
   249
   predicate 'pred' *)
wenzelm@256
   250
clasohm@0
   251
fun min_filter a pred ars =
wenzelm@256
   252
  let fun filt ([], l) = l
wenzelm@256
   253
        | filt ((c, x)::xs, l) = if pred(x) then filt (xs, inj a (c, l))
wenzelm@256
   254
                               else filt (xs, l)
wenzelm@256
   255
  in filt (ars, []) end;
clasohm@0
   256
clasohm@0
   257
clasohm@0
   258
(* 'cod_above' filters all arities whose domains are elementwise >= than
wenzelm@256
   259
   a given domain 'w' and gives back a list of the corresponding range
clasohm@0
   260
   classes *)
clasohm@0
   261
wenzelm@256
   262
fun cod_above (a, w, ars) = min_filter a (fn w' => lew a (w, w')) ars;
wenzelm@256
   263
wenzelm@256
   264
clasohm@0
   265
nipkow@200
   266
(*Instantiation of type variables in types*)
nipkow@200
   267
(*Pre: instantiations obey restrictions! *)
nipkow@200
   268
fun inst_typ tye =
wenzelm@256
   269
  let fun inst(Type(a, Ts)) = Type(a, map inst Ts)
nipkow@200
   270
        | inst(T as TFree _) = T
wenzelm@256
   271
        | inst(T as TVar(v, _)) =
wenzelm@256
   272
            (case assoc(tye, v) of Some U => inst U | None => T)
nipkow@200
   273
  in inst end;
clasohm@0
   274
clasohm@0
   275
(* 'least_sort' returns for a given type its maximum sort:
clasohm@0
   276
   - type variables, free types: the sort brought with
clasohm@0
   277
   - type constructors: recursive determination of the maximum sort of the
wenzelm@256
   278
                    arguments if the type is declared in 'coreg' of the
wenzelm@256
   279
                    given type signature  *)
clasohm@0
   280
wenzelm@256
   281
fun least_sort (tsig as TySg{subclass, coreg, ...}) =
wenzelm@256
   282
  let fun ls(T as Type(a, Ts)) =
wenzelm@256
   283
                 (case assoc (coreg, a) of
wenzelm@256
   284
                          Some(ars) => cod_above(subclass, map ls Ts, ars)
wenzelm@256
   285
                        | None => raise TYPE(undcl_type a, [T], []))
wenzelm@256
   286
        | ls(TFree(a, S)) = S
wenzelm@256
   287
        | ls(TVar(a, S)) = S
clasohm@0
   288
  in ls end;
clasohm@0
   289
clasohm@0
   290
wenzelm@256
   291
fun check_has_sort(tsig as TySg{subclass, coreg, ...}, T, S) =
wenzelm@256
   292
  if sortorder subclass ((least_sort tsig T), S) then ()
wenzelm@256
   293
  else raise TYPE("Type not of sort " ^ (str_of_sort S), [T], [])
clasohm@0
   294
clasohm@0
   295
clasohm@0
   296
(*Instantiation of type variables in types *)
wenzelm@256
   297
fun inst_typ_tvars(tsig, tye) =
wenzelm@256
   298
  let fun inst(Type(a, Ts)) = Type(a, map inst Ts)
wenzelm@256
   299
        | inst(T as TFree _) = T
wenzelm@256
   300
        | inst(T as TVar(v, S)) = (case assoc(tye, v) of
wenzelm@256
   301
                None => T | Some(U) => (check_has_sort(tsig, U, S); U))
clasohm@0
   302
  in inst end;
clasohm@0
   303
clasohm@0
   304
(*Instantiation of type variables in terms *)
wenzelm@256
   305
fun inst_term_tvars(tsig, tye) = map_term_types (inst_typ_tvars(tsig, tye));
nipkow@200
   306
nipkow@200
   307
nipkow@200
   308
(* expand_typ *)
nipkow@200
   309
wenzelm@256
   310
fun expand_typ (TySg {abbrs, ...}) ty =
wenzelm@256
   311
  let
wenzelm@256
   312
    fun exptyp (Type (a, Ts)) =
wenzelm@256
   313
          (case assoc (abbrs, a) of
wenzelm@256
   314
            Some (vs, U) => exptyp (inst_typ (vs ~~ Ts) U)
wenzelm@256
   315
          | None => Type (a, map exptyp Ts))
wenzelm@256
   316
      | exptyp T = T
wenzelm@256
   317
  in
wenzelm@256
   318
    exptyp ty
wenzelm@256
   319
  end;
wenzelm@256
   320
wenzelm@256
   321
wenzelm@256
   322
(* norm_typ *)      (* FIXME norm sorts *)
wenzelm@256
   323
wenzelm@256
   324
val norm_typ = expand_typ;
wenzelm@256
   325
wenzelm@256
   326
wenzelm@256
   327
wenzelm@256
   328
(** type matching **)
nipkow@200
   329
clasohm@0
   330
exception TYPE_MATCH;
clasohm@0
   331
wenzelm@256
   332
(*typ_match (s, (U, T)) = s' <==> s'(U) = T and s' is an extension of s*)
wenzelm@256
   333
fun typ_match tsig =
wenzelm@256
   334
  let
wenzelm@256
   335
    fun match (subs, (TVar (v, S), T)) =
wenzelm@256
   336
          (case assoc (subs, v) of
wenzelm@256
   337
            None => ((v, (check_has_sort (tsig, T, S); T)) :: subs
wenzelm@256
   338
              handle TYPE _ => raise TYPE_MATCH)
wenzelm@422
   339
          | Some U => if U = T then subs else raise TYPE_MATCH)
wenzelm@256
   340
      | match (subs, (Type (a, Ts), Type (b, Us))) =
wenzelm@256
   341
          if a <> b then raise TYPE_MATCH
wenzelm@256
   342
          else foldl match (subs, Ts ~~ Us)
wenzelm@422
   343
      | match (subs, (TFree x, TFree y)) =
wenzelm@256
   344
          if x = y then subs else raise TYPE_MATCH
wenzelm@256
   345
      | match _ = raise TYPE_MATCH;
wenzelm@256
   346
  in match end;
clasohm@0
   347
clasohm@0
   348
wenzelm@256
   349
fun typ_instance (tsig, T, U) =
wenzelm@256
   350
  (typ_match tsig ([], (U, T)); true) handle TYPE_MATCH => false;
wenzelm@256
   351
wenzelm@256
   352
wenzelm@256
   353
wenzelm@256
   354
(** build type signatures **)
wenzelm@256
   355
wenzelm@416
   356
fun make_tsig (classes, subclass, default, args, abbrs, coreg) =
wenzelm@416
   357
  TySg {classes = classes, subclass = subclass, default = default,
wenzelm@416
   358
    args = args, abbrs = abbrs, coreg = coreg};
wenzelm@416
   359
wenzelm@416
   360
val tsig0 = make_tsig ([], [], [], [], [], []);
wenzelm@256
   361
clasohm@0
   362
wenzelm@401
   363
(* sorts *)
wenzelm@401
   364
wenzelm@416
   365
fun subsort (TySg {subclass, ...}) (S1, S2) =
wenzelm@416
   366
  sortorder subclass (S1, S2);
wenzelm@416
   367
wenzelm@401
   368
fun norm_sort (TySg {subclass, ...}) S =
wenzelm@401
   369
  sort_strings (min_sort subclass S);
wenzelm@401
   370
wenzelm@416
   371
fun rem_sorts (Type (a, tys)) = Type (a, map rem_sorts tys)
wenzelm@416
   372
  | rem_sorts (TFree (x, _)) = TFree (x, [])
wenzelm@416
   373
  | rem_sorts (TVar (xi, _)) = TVar (xi, []);
wenzelm@401
   374
wenzelm@401
   375
clasohm@0
   376
clasohm@0
   377
fun twice(a) = error("Type constructor " ^a^ " has already been declared.");
clasohm@0
   378
wenzelm@256
   379
fun tyab_conflict(a) = error("Can't declare type "^(quote a)^"!\nAn abbreviation with this name exists already.");
clasohm@0
   380
clasohm@0
   381
wenzelm@416
   382
(* typ_errors *)
wenzelm@256
   383
wenzelm@416
   384
(*check validity of (not necessarily normal) type; accumulate error messages*)
wenzelm@256
   385
wenzelm@416
   386
fun typ_errors tsig (typ, errors) =
wenzelm@256
   387
  let
wenzelm@416
   388
    val TySg {classes, args, abbrs, ...} = tsig;
wenzelm@416
   389
wenzelm@416
   390
    fun class_err (errs, c) =
wenzelm@416
   391
      if c mem classes then errs
wenzelm@416
   392
      else undcl_class c ins errs;
wenzelm@256
   393
wenzelm@256
   394
    val sort_err = foldl class_err;
clasohm@0
   395
wenzelm@256
   396
    fun typ_errs (Type (c, Us), errs) =
wenzelm@256
   397
          let
wenzelm@256
   398
            val errs' = foldr typ_errs (Us, errs);
wenzelm@256
   399
            fun nargs n =
wenzelm@256
   400
              if n = length Us then errs'
wenzelm@416
   401
              else ("Wrong number of arguments: " ^ quote c) ins errs';
wenzelm@256
   402
          in
wenzelm@256
   403
            (case assoc (args, c) of
wenzelm@256
   404
              Some n => nargs n
wenzelm@256
   405
            | None =>
wenzelm@256
   406
                (case assoc (abbrs, c) of
wenzelm@256
   407
                  Some (vs, _) => nargs (length vs)
wenzelm@416
   408
                | None => undcl_type c ins errs))
wenzelm@256
   409
          end
wenzelm@256
   410
    | typ_errs (TFree (_, S), errs) = sort_err (errs, S)
wenzelm@416
   411
    | typ_errs (TVar ((x, i), S), errs) =
wenzelm@416
   412
        if i < 0 then
wenzelm@416
   413
          ("Negative index for TVar " ^ quote x) ins sort_err (errs, S)
wenzelm@416
   414
        else sort_err (errs, S);
wenzelm@256
   415
  in
wenzelm@416
   416
    typ_errs (typ, errors)
wenzelm@256
   417
  end;
wenzelm@256
   418
wenzelm@256
   419
wenzelm@256
   420
(* cert_typ *)
wenzelm@256
   421
wenzelm@256
   422
(*check and normalize typ wrt. tsig; errors are indicated by exception TYPE*)
wenzelm@256
   423
wenzelm@256
   424
fun cert_typ tsig ty =
wenzelm@256
   425
  (case typ_errors tsig (ty, []) of
wenzelm@256
   426
    [] => norm_typ tsig ty
wenzelm@256
   427
  | errs => raise_type (cat_lines errs) [ty] []);
wenzelm@256
   428
wenzelm@256
   429
wenzelm@256
   430
wenzelm@422
   431
(** merge type signatures **)
wenzelm@256
   432
wenzelm@422
   433
(*'assoc_union' merges two association lists if the contents associated
wenzelm@422
   434
  the keys are lists*)
clasohm@0
   435
wenzelm@422
   436
fun assoc_union (as1, []) = as1
wenzelm@422
   437
  | assoc_union (as1, (key, l2) :: as2) =
wenzelm@422
   438
      (case assoc (as1, key) of
wenzelm@422
   439
        Some l1 => assoc_union (overwrite (as1, (key, l1 union l2)), as2)
wenzelm@422
   440
      | None => assoc_union ((key, l2) :: as1, as2));
clasohm@0
   441
clasohm@0
   442
wenzelm@422
   443
(* merge subclass *)
clasohm@0
   444
wenzelm@422
   445
fun merge_subclass (subclass1, subclass2) =
wenzelm@422
   446
  let val subclass = transitive_closure (assoc_union (subclass1, subclass2)) in
wenzelm@422
   447
    if exists (op mem) subclass then
wenzelm@422
   448
      error ("Cyclic class structure!")   (* FIXME improve msg, raise TERM *)
wenzelm@422
   449
    else subclass
wenzelm@416
   450
  end;
wenzelm@416
   451
wenzelm@416
   452
wenzelm@422
   453
(* coregularity *)
clasohm@0
   454
clasohm@0
   455
(* 'is_unique_decl' checks if there exists just one declaration t:(Ss)C *)
clasohm@0
   456
wenzelm@256
   457
fun is_unique_decl coreg (t, (s, w)) = case assoc2 (coreg, (t, s)) of
clasohm@0
   458
      Some(w1) => if w = w1 then () else
wenzelm@256
   459
        error("There are two declarations\n" ^
wenzelm@416
   460
              str_of_arity(t, w, [s]) ^ " and\n" ^
wenzelm@416
   461
              str_of_arity(t, w1, [s]) ^ "\n" ^
clasohm@0
   462
              "with the same result class.")
clasohm@0
   463
    | None => ();
clasohm@0
   464
clasohm@0
   465
(* 'restr2' checks if there are two declarations t:(Ss1)C1 and t:(Ss2)C2
clasohm@0
   466
   such that C1 >= C2 then Ss1 >= Ss2 (elementwise) *)
clasohm@0
   467
wenzelm@256
   468
fun subs (classes, subclass) C =
wenzelm@256
   469
  let fun sub (rl, l) = if leq subclass (l, C) then l::rl else rl
wenzelm@256
   470
  in foldl sub ([], classes) end;
clasohm@0
   471
wenzelm@256
   472
fun coreg_err(t, (w1, C), (w2, D)) =
wenzelm@416
   473
    error("Declarations " ^ str_of_arity(t, w1, [C]) ^ " and "
wenzelm@416
   474
                          ^ str_of_arity(t, w2, [D]) ^ " are in conflict");
clasohm@0
   475
wenzelm@256
   476
fun restr2 classes (subclass, coreg) (t, (s, w)) =
wenzelm@256
   477
  let fun restr ([], test) = ()
wenzelm@416
   478
        | restr (s1::Ss, test) =
wenzelm@416
   479
            (case assoc2 (coreg, (t, s1)) of
wenzelm@416
   480
              Some dom =>
wenzelm@416
   481
                if lew subclass (test (w, dom))
wenzelm@416
   482
                then restr (Ss, test)
wenzelm@416
   483
                else coreg_err (t, (w, s), (dom, s1))
wenzelm@256
   484
            | None => restr (Ss, test))
wenzelm@256
   485
      fun forward (t, (s, w)) =
wenzelm@256
   486
        let val s_sups = case assoc (subclass, s) of
wenzelm@256
   487
                   Some(s_sups) => s_sups | None => err_undcl_class(s);
wenzelm@256
   488
        in restr (s_sups, I) end
wenzelm@256
   489
      fun backward (t, (s, w)) =
wenzelm@256
   490
        let val s_subs = subs (classes, subclass) s
wenzelm@256
   491
        in restr (s_subs, fn (x, y) => (y, x)) end
wenzelm@256
   492
  in (backward (t, (s, w)); forward (t, (s, w))) end;
clasohm@0
   493
clasohm@0
   494
wenzelm@256
   495
fun varying_decls t =
wenzelm@256
   496
  error ("Type constructor " ^ quote t ^ " has varying number of arguments");
clasohm@0
   497
clasohm@0
   498
wenzelm@422
   499
(* 'merge_coreg' builds the union of two 'coreg' lists;
wenzelm@422
   500
   it only checks the two restriction conditions and inserts afterwards
wenzelm@422
   501
   all elements of the second list into the first one *)
wenzelm@422
   502
wenzelm@422
   503
fun merge_coreg classes subclass1 =
wenzelm@422
   504
  let fun test_ar classes (t, ars1) (coreg1, (s, w)) =
wenzelm@422
   505
        (is_unique_decl coreg1 (t, (s, w));
wenzelm@422
   506
         restr2 classes (subclass1, coreg1) (t, (s, w));
wenzelm@422
   507
         overwrite (coreg1, (t, (s, w) ins ars1)));
wenzelm@422
   508
wenzelm@422
   509
      fun merge_c (coreg1, (c as (t, ars2))) = case assoc (coreg1, t) of
wenzelm@422
   510
          Some(ars1) => foldl (test_ar classes (t, ars1)) (coreg1, ars2)
wenzelm@422
   511
        | None => c::coreg1
wenzelm@422
   512
  in foldl merge_c end;
wenzelm@422
   513
wenzelm@422
   514
fun merge_args (args, (t, n)) =
wenzelm@422
   515
  (case assoc (args, t) of
wenzelm@422
   516
    Some m => if m = n then args else varying_decls t
wenzelm@422
   517
  | None => (t, n) :: args);
wenzelm@422
   518
wenzelm@422
   519
(* FIXME raise TERM *)
wenzelm@422
   520
fun merge_abbrs (abbrs1, abbrs2) =
wenzelm@422
   521
  let
wenzelm@422
   522
    val abbrs = abbrs1 union abbrs2;
wenzelm@422
   523
    val names = map fst abbrs;
wenzelm@422
   524
  in
wenzelm@422
   525
    (case duplicates names of
wenzelm@422
   526
      [] => abbrs
wenzelm@422
   527
    | dups => error ("Duplicate declaration of type abbreviations: " ^
wenzelm@422
   528
        commas_quote dups))
wenzelm@422
   529
  end;
wenzelm@422
   530
wenzelm@422
   531
wenzelm@422
   532
(* 'merge_tsigs' takes the above declared functions to merge two type
wenzelm@422
   533
  signatures *)
wenzelm@422
   534
wenzelm@422
   535
fun merge_tsigs(TySg{classes=classes1, default=default1, subclass=subclass1, args=args1,
wenzelm@422
   536
           coreg=coreg1, abbrs=abbrs1},
wenzelm@422
   537
          TySg{classes=classes2, default=default2, subclass=subclass2, args=args2,
wenzelm@422
   538
           coreg=coreg2, abbrs=abbrs2}) =
wenzelm@422
   539
  let val classes' = classes1 union classes2;
wenzelm@422
   540
      val subclass' = merge_subclass (subclass1, subclass2);
wenzelm@422
   541
      val args' = foldl merge_args (args1, args2)
wenzelm@422
   542
      val coreg' = merge_coreg classes' subclass' (coreg1, coreg2);
wenzelm@422
   543
      val default' = min_sort subclass' (default1 @ default2);
wenzelm@422
   544
      val abbrs' = merge_abbrs(abbrs1, abbrs2);
wenzelm@422
   545
  in TySg{classes=classes' , default=default', subclass=subclass', args=args',
wenzelm@422
   546
          coreg=coreg' , abbrs = abbrs' }
wenzelm@422
   547
  end;
wenzelm@422
   548
wenzelm@422
   549
wenzelm@422
   550
wenzelm@422
   551
(*** extend type signatures ***)
wenzelm@422
   552
wenzelm@422
   553
(** add classes **)
wenzelm@422
   554
wenzelm@422
   555
(* FIXME use? *)
wenzelm@422
   556
fun add_classes classes cs =
wenzelm@422
   557
  (case cs inter classes of
wenzelm@422
   558
    [] => cs @ classes
wenzelm@422
   559
  | dups => err_dup_classes cs);
wenzelm@422
   560
wenzelm@422
   561
wenzelm@422
   562
(* 'add_class' adds a new class to the list of all existing classes *)
wenzelm@422
   563
wenzelm@422
   564
fun add_class (classes, (s, _)) =
wenzelm@422
   565
  if s mem classes then error("Class " ^ s ^ " declared twice.")
wenzelm@422
   566
  else s :: classes;
wenzelm@422
   567
wenzelm@422
   568
wenzelm@422
   569
(*'add_subclass' adds a tuple consisting of a new class (the new class has
wenzelm@422
   570
  already been inserted into the 'classes' list) and its superclasses (they
wenzelm@422
   571
  must be declared in 'classes' too) to the 'subclass' list of the given type
wenzelm@422
   572
  signature; furthermore all inherited superclasses according to the
wenzelm@422
   573
  superclasses brought with are inserted and there is a check that there are
wenzelm@422
   574
  no cycles (i.e. C <= D <= C, with C <> D);*)
wenzelm@422
   575
wenzelm@422
   576
fun add_subclass classes (subclass, (s, ges)) =
wenzelm@422
   577
let fun upd (subclass, s') = if s' mem classes then
wenzelm@422
   578
        let val ges' = the (assoc (subclass, s))
wenzelm@422
   579
        in case assoc (subclass, s') of
wenzelm@422
   580
             Some sups => if s mem sups
wenzelm@422
   581
                           then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s )
wenzelm@422
   582
                           else overwrite (subclass, (s, sups union ges'))
wenzelm@422
   583
           | None => subclass
wenzelm@422
   584
         end
wenzelm@422
   585
         else err_undcl_class(s')
wenzelm@422
   586
in foldl upd (subclass@[(s, ges)], ges) end;
wenzelm@422
   587
wenzelm@422
   588
wenzelm@422
   589
(* 'extend_classes' inserts all new classes into the corresponding
wenzelm@422
   590
   lists ('classes', 'subclass') if possible *)
wenzelm@422
   591
wenzelm@422
   592
fun extend_classes (classes, subclass, newclasses) =
wenzelm@422
   593
  if newclasses = [] then (classes, subclass) else
wenzelm@422
   594
  let val classes' = foldl add_class (classes, newclasses);
wenzelm@422
   595
      val subclass' = foldl (add_subclass classes') (subclass, newclasses);
wenzelm@422
   596
  in (classes', subclass') end;
wenzelm@422
   597
wenzelm@422
   598
wenzelm@422
   599
(* ext_tsig_subclass *)
wenzelm@422
   600
wenzelm@422
   601
fun ext_tsig_subclass tsig pairs =
wenzelm@422
   602
  let
wenzelm@422
   603
    val TySg {classes, subclass, default, args, abbrs, coreg} = tsig;
wenzelm@422
   604
wenzelm@422
   605
    (* FIXME clean! *)
wenzelm@422
   606
    val subclass' =
wenzelm@422
   607
      merge_subclass (subclass, map (fn (c1, c2) => (c1, [c2])) pairs);
wenzelm@422
   608
  in
wenzelm@422
   609
    make_tsig (classes, subclass', default, args, abbrs, coreg)
wenzelm@422
   610
  end;
wenzelm@422
   611
wenzelm@422
   612
wenzelm@422
   613
(* ext_tsig_defsort *)
wenzelm@422
   614
wenzelm@422
   615
fun ext_tsig_defsort (TySg {classes, subclass, args, abbrs, coreg, ...}) default =
wenzelm@422
   616
  make_tsig (classes, subclass, default, args, abbrs, coreg);
wenzelm@422
   617
wenzelm@422
   618
wenzelm@422
   619
wenzelm@582
   620
(** add types **)   (* FIXME check *)
wenzelm@582
   621
wenzelm@582
   622
fun ext_tsig_types (TySg {classes, subclass, default, args, abbrs, coreg}) ts =
wenzelm@582
   623
  let
wenzelm@582
   624
    fun check_type (c, n) =
wenzelm@582
   625
      if n < 0 then err_neg_args c
wenzelm@582
   626
      else if is_some (assoc (args, c)) then err_dup_tycon c
wenzelm@582
   627
      else if is_some (assoc (abbrs, c)) then err_ty_confl c
wenzelm@582
   628
      else ();
wenzelm@582
   629
  in
wenzelm@582
   630
    seq check_type ts;
wenzelm@582
   631
    make_tsig (classes, subclass, default, ts @ args, abbrs,
wenzelm@582
   632
      map (rpair [] o #1) ts @ coreg)    (* FIXME (t, []) needed? *)
wenzelm@582
   633
  end;
wenzelm@582
   634
wenzelm@582
   635
wenzelm@582
   636
wenzelm@582
   637
(** add type abbreviations **)
wenzelm@582
   638
wenzelm@582
   639
fun abbr_errors tsig (a, (lhs_vs, rhs)) =
wenzelm@582
   640
  let
wenzelm@582
   641
    val TySg {args, abbrs, ...} = tsig;
wenzelm@582
   642
    val rhs_vs = map #1 (typ_tvars rhs);
wenzelm@582
   643
    val show_idxs = commas_quote o map fst;
wenzelm@582
   644
wenzelm@582
   645
    val dup_lhs_vars =
wenzelm@582
   646
      (case duplicates lhs_vs of
wenzelm@582
   647
        [] => []
wenzelm@582
   648
      | vs => ["Duplicate variables on lhs: " ^ show_idxs vs]);
wenzelm@582
   649
wenzelm@582
   650
    val extra_rhs_vars =
wenzelm@582
   651
      (case gen_rems (op =) (rhs_vs, lhs_vs) of
wenzelm@582
   652
        [] => []
wenzelm@582
   653
      | vs => ["Extra variables on rhs: " ^ show_idxs vs]);
wenzelm@582
   654
wenzelm@582
   655
    val tycon_confl =
wenzelm@582
   656
      if is_none (assoc (args, a)) then []
wenzelm@582
   657
      else [ty_confl a];
wenzelm@582
   658
wenzelm@582
   659
    val dup_abbr =
wenzelm@582
   660
      if is_none (assoc (abbrs, a)) then []
wenzelm@582
   661
      else ["Duplicate declaration of abbreviation"];
wenzelm@582
   662
  in
wenzelm@582
   663
    dup_lhs_vars @ extra_rhs_vars @ tycon_confl @ dup_abbr @
wenzelm@582
   664
      typ_errors tsig (rhs, [])
wenzelm@582
   665
  end;
wenzelm@582
   666
wenzelm@582
   667
fun add_abbr (tsig, abbr as (a, _)) =
wenzelm@582
   668
  let val TySg {classes, subclass, default, args, coreg, abbrs} = tsig in
wenzelm@582
   669
    (case abbr_errors tsig abbr of
wenzelm@582
   670
      [] => make_tsig (classes, subclass, default, args, abbr :: abbrs, coreg)
wenzelm@582
   671
    | errs => (seq writeln errs;
wenzelm@582
   672
        error ("The error(s) above occurred in type abbreviation " ^ quote a)))
wenzelm@582
   673
  end;
wenzelm@582
   674
wenzelm@582
   675
fun ext_tsig_abbrs tsig abbrs = foldl add_abbr (tsig, abbrs);
wenzelm@582
   676
wenzelm@582
   677
wenzelm@582
   678
wenzelm@422
   679
(** add arities **)
wenzelm@422
   680
clasohm@0
   681
(* 'coregular' checks
clasohm@0
   682
   - the two restriction conditions 'is_unique_decl' and 'restr2'
wenzelm@256
   683
   - if the classes in the new type declarations are known in the
clasohm@0
   684
     given type signature
clasohm@0
   685
   - if one type constructor has always the same number of arguments;
wenzelm@256
   686
   if one type declaration has passed all checks it is inserted into
clasohm@0
   687
   the 'coreg' association list of the given type signatrure  *)
clasohm@0
   688
wenzelm@256
   689
fun coregular (classes, subclass, args) =
wenzelm@256
   690
  let fun ex C = if C mem classes then () else err_undcl_class(C);
clasohm@0
   691
wenzelm@256
   692
      fun addar(w, C) (coreg, t) = case assoc(args, t) of
clasohm@0
   693
            Some(n) => if n <> length w then varying_decls(t) else
wenzelm@256
   694
                     (is_unique_decl coreg (t, (C, w));
wenzelm@256
   695
                      (seq o seq) ex w;
wenzelm@256
   696
                      restr2 classes (subclass, coreg) (t, (C, w));
wenzelm@416
   697
                      let val ars = the (assoc(coreg, t))
wenzelm@256
   698
                      in overwrite(coreg, (t, (C, w) ins ars)) end)
wenzelm@256
   699
          | None => err_undcl_type(t);
clasohm@0
   700
wenzelm@256
   701
      fun addts(coreg, (ts, ar)) = foldl (addar ar) (coreg, ts)
clasohm@0
   702
clasohm@0
   703
  in addts end;
clasohm@0
   704
clasohm@0
   705
clasohm@0
   706
(* 'close' extends the 'coreg' association list after all new type
clasohm@0
   707
   declarations have been inserted successfully:
clasohm@0
   708
   for every declaration t:(Ss)C , for all classses D with C <= D:
clasohm@0
   709
      if there is no declaration t:(Ss')C' with C < C' and C' <= D
clasohm@0
   710
      then insert the declaration t:(Ss)D into 'coreg'
clasohm@0
   711
   this means, if there exists a declaration t:(Ss)C and there is
clasohm@0
   712
   no declaration t:(Ss')D with C <=D then the declaration holds
wenzelm@256
   713
   for all range classes more general than C *)
wenzelm@256
   714
wenzelm@256
   715
fun close (coreg, subclass) =
wenzelm@256
   716
  let fun check sl (l, (s, dom)) = case assoc (subclass, s) of
clasohm@0
   717
          Some(sups) =>
wenzelm@256
   718
            let fun close_sup (l, sup) =
wenzelm@256
   719
                  if exists (fn s'' => less subclass (s, s'') andalso
wenzelm@256
   720
                                       leq subclass (s'', sup)) sl
clasohm@0
   721
                  then l
wenzelm@256
   722
                  else (sup, dom)::l
wenzelm@256
   723
            in foldl close_sup (l, sups) end
clasohm@0
   724
        | None => l;
wenzelm@256
   725
      fun ext (s, l) = (s, foldl (check (map #1 l)) (l, l));
clasohm@0
   726
  in map ext coreg end;
clasohm@0
   727
wenzelm@422
   728
wenzelm@422
   729
(** add types **)
wenzelm@422
   730
wenzelm@582
   731
(* FIXME old *)
wenzelm@416
   732
fun add_types (aca, (ts, n)) =
wenzelm@416
   733
  let
wenzelm@416
   734
    fun add_type ((args, coreg, abbrs), t) =
wenzelm@416
   735
      case assoc(args, t) of              (* FIXME from new *)
wenzelm@416
   736
        Some _ => twice(t)
wenzelm@416
   737
      | None =>
wenzelm@416
   738
          (case assoc(abbrs, t) of
wenzelm@416
   739
            Some _ => tyab_conflict(t)
wenzelm@416
   740
          | None => ((t, n)::args, (t, [])::coreg, abbrs))
wenzelm@416
   741
  in
wenzelm@416
   742
    if n < 0 then     (* FIXME err_neg_args *)
wenzelm@416
   743
      error ("Type constructor cannot have negative number of arguments")
wenzelm@416
   744
    else foldl add_type (aca, ts)
clasohm@0
   745
  end;
clasohm@0
   746
wenzelm@256
   747
wenzelm@422
   748
wenzelm@256
   749
(* 'extend_tsig' takes the above described check- and extend-functions to
clasohm@0
   750
   extend a given type signature with new classes and new type declarations *)
clasohm@0
   751
wenzelm@256
   752
fun extend_tsig (TySg{classes, default, subclass, args, coreg, abbrs})
wenzelm@582
   753
            (newclasses, [], types, arities) =
wenzelm@416
   754
  let
wenzelm@416
   755
    val (classes', subclass') = extend_classes(classes, subclass, newclasses);
wenzelm@256
   756
    val (args', coreg', _) = foldl add_types ((args, coreg, abbrs), types);
wenzelm@422
   757
wenzelm@416
   758
    val coreg'' =
wenzelm@416
   759
      foldl (coregular (classes', subclass', args'))
wenzelm@416
   760
        (coreg', min_domain subclass' arities);
wenzelm@256
   761
    val coreg''' = close (coreg'', subclass');
wenzelm@416
   762
  in
wenzelm@582
   763
    TySg {classes = classes', subclass = subclass', default = default,
wenzelm@416
   764
      args = args', coreg = coreg''', abbrs = abbrs}
wenzelm@416
   765
  end;
clasohm@0
   766
clasohm@0
   767
wenzelm@416
   768
wenzelm@416
   769
wenzelm@416
   770
(*** type unification and inference ***)
clasohm@0
   771
clasohm@0
   772
(*
clasohm@0
   773
clasohm@0
   774
Input:
clasohm@0
   775
- a 'raw' term which contains only dummy types and some explicit type
clasohm@0
   776
  constraints encoded as terms.
clasohm@0
   777
- the expected type of the term.
clasohm@0
   778
clasohm@0
   779
Output:
clasohm@0
   780
- the correctly typed term
clasohm@0
   781
- the substitution needed to unify the actual type of the term with its
clasohm@0
   782
  expected type; only the TVars in the expected type are included.
clasohm@0
   783
clasohm@0
   784
During type inference all TVars in the term have negative index. This keeps
clasohm@0
   785
them apart from normal TVars, which is essential, because at the end the type
clasohm@0
   786
of the term is unified with the expected type, which contains normal TVars.
clasohm@0
   787
wenzelm@565
   788
1. Add initial type information to the term (attach_types).
clasohm@0
   789
   This freezes (freeze_vars) TVars in explicitly provided types (eg
clasohm@0
   790
   constraints or defaults) by turning them into TFrees.
clasohm@0
   791
2. Carry out type inference, possibly introducing new negative TVars.
clasohm@0
   792
3. Unify actual and expected type.
clasohm@0
   793
4. Turn all (negative) TVars into unique new TFrees (freeze).
clasohm@0
   794
5. Thaw all TVars frozen in step 1 (thaw_vars).
clasohm@0
   795
clasohm@0
   796
*)
clasohm@0
   797
clasohm@0
   798
(*Raised if types are not unifiable*)
clasohm@0
   799
exception TUNIFY;
clasohm@0
   800
clasohm@0
   801
val tyvar_count = ref(~1);
clasohm@0
   802
clasohm@0
   803
fun tyinit() = (tyvar_count := ~1);
clasohm@0
   804
clasohm@0
   805
fun new_tvar_inx() = (tyvar_count := !tyvar_count-1; !tyvar_count)
clasohm@0
   806
clasohm@0
   807
(*
clasohm@0
   808
Generate new TVar.  Index is < ~1 to distinguish it from TVars generated from
clasohm@0
   809
variable names (see id_type).  Name is arbitrary because index is new.
clasohm@0
   810
*)
clasohm@0
   811
wenzelm@256
   812
fun gen_tyvar(S) = TVar(("'a", new_tvar_inx()), S);
clasohm@0
   813
clasohm@0
   814
(*Occurs check: type variable occurs in type?*)
clasohm@0
   815
fun occ v tye =
wenzelm@256
   816
  let fun occ(Type(_, Ts)) = exists occ Ts
clasohm@0
   817
        | occ(TFree _) = false
wenzelm@256
   818
        | occ(TVar(w, _)) = v=w orelse
wenzelm@256
   819
                           (case assoc(tye, w) of
clasohm@0
   820
                              None   => false
clasohm@0
   821
                            | Some U => occ U);
clasohm@0
   822
  in occ end;
clasohm@0
   823
wenzelm@256
   824
(*Chase variable assignments in tye.
wenzelm@256
   825
  If devar (T, tye) returns a type var then it must be unassigned.*)
wenzelm@256
   826
fun devar (T as TVar(v, _), tye) = (case  assoc(tye, v)  of
wenzelm@256
   827
          Some U =>  devar (U, tye)
clasohm@0
   828
        | None   =>  T)
wenzelm@256
   829
  | devar (T, tye) = T;
clasohm@0
   830
clasohm@0
   831
clasohm@0
   832
(* 'dom' returns for a type constructor t the list of those domains
clasohm@0
   833
   which deliver a given range class C *)
clasohm@0
   834
wenzelm@256
   835
fun dom coreg t C = case assoc2 (coreg, (t, C)) of
clasohm@0
   836
    Some(Ss) => Ss
clasohm@0
   837
  | None => raise TUNIFY;
clasohm@0
   838
clasohm@0
   839
clasohm@0
   840
(* 'Dom' returns the union of all domain lists of 'dom' for a given sort S
clasohm@0
   841
   (i.e. a set of range classes ); the union is carried out elementwise
clasohm@0
   842
   for the seperate sorts in the domains *)
clasohm@0
   843
wenzelm@256
   844
fun Dom (subclass, coreg) (t, S) =
clasohm@0
   845
  let val domlist = map (dom coreg t) S;
clasohm@0
   846
  in if null domlist then []
wenzelm@256
   847
     else foldl (elementwise_union subclass) (hd domlist, tl domlist)
clasohm@0
   848
  end;
clasohm@0
   849
clasohm@0
   850
wenzelm@256
   851
fun W ((T, S), tsig as TySg{subclass, coreg, ...}, tye) =
wenzelm@256
   852
  let fun Wd ((T, S), tye) = W ((devar (T, tye), S), tsig, tye)
wenzelm@256
   853
      fun Wk(T as TVar(v, S')) =
wenzelm@256
   854
              if sortorder subclass (S', S) then tye
wenzelm@256
   855
              else (v, gen_tyvar(union_sort subclass (S', S)))::tye
wenzelm@256
   856
        | Wk(T as TFree(v, S')) = if sortorder subclass (S', S) then tye
wenzelm@256
   857
                                 else raise TUNIFY
wenzelm@256
   858
        | Wk(T as Type(f, Ts)) =
wenzelm@256
   859
           if null S then tye
wenzelm@256
   860
           else foldr Wd (Ts~~(Dom (subclass, coreg) (f, S)) , tye)
clasohm@0
   861
  in Wk(T) end;
clasohm@0
   862
clasohm@0
   863
clasohm@0
   864
(* Order-sorted Unification of Types (U)  *)
clasohm@0
   865
clasohm@0
   866
(* Precondition: both types are well-formed w.r.t. type constructor arities *)
wenzelm@256
   867
fun unify (tsig as TySg{subclass, coreg, ...}) =
wenzelm@256
   868
  let fun unif ((T, U), tye) =
wenzelm@256
   869
        case (devar(T, tye), devar(U, tye)) of
wenzelm@256
   870
          (T as TVar(v, S1), U as TVar(w, S2)) =>
clasohm@0
   871
             if v=w then tye else
wenzelm@256
   872
             if sortorder subclass (S1, S2) then (w, T)::tye else
wenzelm@256
   873
             if sortorder subclass (S2, S1) then (v, U)::tye
wenzelm@256
   874
             else let val nu = gen_tyvar (union_sort subclass (S1, S2))
wenzelm@256
   875
                  in (v, nu)::(w, nu)::tye end
wenzelm@256
   876
        | (T as TVar(v, S), U) =>
wenzelm@256
   877
             if occ v tye U then raise TUNIFY else W ((U, S), tsig, (v, U)::tye)
wenzelm@256
   878
        | (U, T as TVar (v, S)) =>
wenzelm@256
   879
             if occ v tye U then raise TUNIFY else W ((U, S), tsig, (v, U)::tye)
wenzelm@256
   880
        | (Type(a, Ts), Type(b, Us)) =>
wenzelm@256
   881
             if a<>b then raise TUNIFY else foldr unif (Ts~~Us, tye)
wenzelm@256
   882
        | (T, U) => if T=U then tye else raise TUNIFY
clasohm@0
   883
  in unif end;
clasohm@0
   884
clasohm@0
   885
wenzelm@450
   886
(* raw_unify (ignores sorts) *)
wenzelm@450
   887
wenzelm@450
   888
fun raw_unify (ty1, ty2) =
wenzelm@450
   889
  (unify tsig0 ((rem_sorts ty1, rem_sorts ty2), []); true)
wenzelm@450
   890
    handle TUNIFY => false;
wenzelm@450
   891
wenzelm@450
   892
clasohm@0
   893
(*Type inference for polymorphic term*)
clasohm@0
   894
fun infer tsig =
wenzelm@256
   895
  let fun inf(Ts, Const (_, T), tye) = (T, tye)
wenzelm@256
   896
        | inf(Ts, Free  (_, T), tye) = (T, tye)
wenzelm@256
   897
        | inf(Ts, Bound i, tye) = ((nth_elem(i, Ts) , tye)
clasohm@0
   898
          handle LIST _=> raise TYPE ("loose bound variable", [], [Bound i]))
wenzelm@256
   899
        | inf(Ts, Var (_, T), tye) = (T, tye)
wenzelm@256
   900
        | inf(Ts, Abs (_, T, body), tye) =
wenzelm@256
   901
            let val (U, tye') = inf(T::Ts, body, tye) in  (T-->U, tye')  end
clasohm@0
   902
        | inf(Ts, f$u, tye) =
wenzelm@256
   903
            let val (U, tyeU) = inf(Ts, u, tye);
wenzelm@256
   904
                val (T, tyeT) = inf(Ts, f, tyeU);
clasohm@0
   905
                fun err s =
clasohm@0
   906
                  raise TYPE(s, [inst_typ tyeT T, inst_typ tyeT U], [f$u])
wenzelm@256
   907
            in case T of
wenzelm@256
   908
                 Type("fun", [T1, T2]) =>
wenzelm@256
   909
                   ( (T2, unify tsig ((T1, U), tyeT))
clasohm@0
   910
                     handle TUNIFY => err"type mismatch in application" )
wenzelm@256
   911
               | TVar _ =>
clasohm@0
   912
                   let val T2 = gen_tyvar([])
clasohm@0
   913
                   in (T2, unify tsig ((T, U-->T2), tyeT))
clasohm@0
   914
                      handle TUNIFY => err"type mismatch in application"
clasohm@0
   915
                   end
clasohm@0
   916
               | _ => err"rator must have function type"
clasohm@0
   917
           end
clasohm@0
   918
  in inf end;
clasohm@0
   919
wenzelm@256
   920
fun freeze_vars(Type(a, Ts)) = Type(a, map freeze_vars Ts)
clasohm@0
   921
  | freeze_vars(T as TFree _) = T
wenzelm@256
   922
  | freeze_vars(TVar(v, S)) = TFree(Syntax.string_of_vname v, S);
clasohm@0
   923
clasohm@0
   924
(* Attach a type to a constant *)
wenzelm@256
   925
fun type_const (a, T) = Const(a, incr_tvar (new_tvar_inx()) T);
clasohm@0
   926
clasohm@0
   927
(*Find type of ident.  If not in table then use ident's name for tyvar
clasohm@0
   928
  to get consistent typing.*)
wenzelm@256
   929
fun new_id_type a = TVar(("'"^a, new_tvar_inx()), []);
wenzelm@256
   930
fun type_of_ixn(types, ixn as (a, _)) =
wenzelm@565
   931
  case types ixn of Some T => freeze_vars T | None => TVar(("'"^a, ~1), []);
wenzelm@565
   932
wenzelm@565
   933
fun constrain (term, T) = Const (Syntax.constrainC, T --> T) $ term;
clasohm@0
   934
wenzelm@565
   935
fun constrainAbs (Abs (a, _, body), T) = Abs (a, T, body)
wenzelm@565
   936
  | constrainAbs _ = sys_error "constrainAbs";
wenzelm@256
   937
clasohm@0
   938
wenzelm@565
   939
(* attach_types *)
wenzelm@565
   940
clasohm@0
   941
(*
wenzelm@256
   942
  Attach types to a term. Input is a "parse tree" containing dummy types.
wenzelm@256
   943
  Type constraints are translated and checked for validity wrt tsig. TVars in
wenzelm@256
   944
  constraints are frozen.
clasohm@0
   945
wenzelm@256
   946
  The atoms in the resulting term satisfy the following spec:
clasohm@0
   947
wenzelm@256
   948
  Const (a, T):
wenzelm@256
   949
    T is a renamed copy of the generic type of a; renaming decreases index of
wenzelm@256
   950
    all TVars by new_tvar_inx(), which is less than ~1. The index of all
wenzelm@256
   951
    TVars in the generic type must be 0 for this to work!
clasohm@0
   952
wenzelm@256
   953
  Free (a, T), Var (ixn, T):
wenzelm@256
   954
    T is either the frozen default type of a or TVar (("'"^a, ~1), [])
clasohm@0
   955
wenzelm@256
   956
  Abs (a, T, _):
wenzelm@256
   957
    T is either a type constraint or TVar (("'" ^ a, i), []), where i is
wenzelm@256
   958
    generated by new_tvar_inx(). Thus different abstractions can have the
wenzelm@256
   959
    bound variables of the same name but different types.
clasohm@0
   960
*)
clasohm@0
   961
wenzelm@565
   962
(* FIXME consitency of sort_env / sorts (!?) *)
wenzelm@256
   963
wenzelm@565
   964
(* FIXME check *)
wenzelm@565
   965
wenzelm@565
   966
fun attach_types (tsig, const_type, types, sorts) tm =
wenzelm@256
   967
  let
wenzelm@565
   968
    val sort_env = Syntax.raw_term_sorts tm;
wenzelm@565
   969
    fun def_sort xi = if_none (sorts xi) (defaultS tsig);
wenzelm@256
   970
wenzelm@565
   971
    fun prepareT t =
wenzelm@565
   972
      freeze_vars (cert_typ tsig (Syntax.typ_of_term sort_env def_sort t));
wenzelm@256
   973
wenzelm@256
   974
    fun add (Const (a, _)) =
wenzelm@565
   975
          (case const_type a of
wenzelm@256
   976
            Some T => type_const (a, T)
wenzelm@256
   977
          | None => raise_type ("No such constant: " ^ quote a) [] [])
wenzelm@256
   978
      | add (Free (a, _)) =
wenzelm@565
   979
          (case const_type a of
wenzelm@256
   980
            Some T => type_const (a, T)
wenzelm@256
   981
          | None => Free (a, type_of_ixn (types, (a, ~1))))
wenzelm@256
   982
      | add (Var (ixn, _)) = Var (ixn, type_of_ixn (types, ixn))
wenzelm@565
   983
      | add (Bound i) = Bound i
wenzelm@256
   984
      | add (Abs (a, _, body)) = Abs (a, new_id_type a, add body)
wenzelm@256
   985
      | add ((f as Const (a, _) $ t1) $ t2) =
wenzelm@256
   986
          if a = Syntax.constrainC then
wenzelm@256
   987
            constrain (add t1, prepareT t2)
wenzelm@256
   988
          else if a = Syntax.constrainAbsC then
wenzelm@256
   989
            constrainAbs (add t1, prepareT t2)
wenzelm@256
   990
          else add f $ add t2
wenzelm@256
   991
      | add (f $ t) = add f $ add t;
wenzelm@565
   992
  in add tm end;
clasohm@0
   993
clasohm@0
   994
clasohm@0
   995
(* Post-Processing *)
clasohm@0
   996
clasohm@0
   997
(*Instantiation of type variables in terms*)
clasohm@0
   998
fun inst_types tye = map_term_types (inst_typ tye);
clasohm@0
   999
clasohm@0
  1000
(*Delete explicit constraints -- occurrences of "_constrain" *)
wenzelm@256
  1001
fun unconstrain (Abs(a, T, t)) = Abs(a, T, unconstrain t)
wenzelm@256
  1002
  | unconstrain ((f as Const(a, _)) $ t) =
clasohm@0
  1003
      if a=Syntax.constrainC then unconstrain t
clasohm@0
  1004
      else unconstrain f $ unconstrain t
clasohm@0
  1005
  | unconstrain (f$t) = unconstrain f $ unconstrain t
clasohm@0
  1006
  | unconstrain (t) = t;
clasohm@0
  1007
clasohm@0
  1008
clasohm@0
  1009
(* Turn all TVars which satisfy p into new TFrees *)
clasohm@0
  1010
fun freeze p t =
wenzelm@256
  1011
  let val fs = add_term_tfree_names(t, []);
wenzelm@256
  1012
      val inxs = filter p (add_term_tvar_ixns(t, []));
clasohm@0
  1013
      val vmap = inxs ~~ variantlist(map #1 inxs, fs);
wenzelm@256
  1014
      fun free(Type(a, Ts)) = Type(a, map free Ts)
wenzelm@256
  1015
        | free(T as TVar(v, S)) =
wenzelm@256
  1016
            (case assoc(vmap, v) of None => T | Some(a) => TFree(a, S))
clasohm@0
  1017
        | free(T as TFree _) = T
clasohm@0
  1018
  in map_term_types free t end;
clasohm@0
  1019
clasohm@0
  1020
(* Thaw all TVars that were frozen in freeze_vars *)
wenzelm@256
  1021
fun thaw_vars(Type(a, Ts)) = Type(a, map thaw_vars Ts)
wenzelm@256
  1022
  | thaw_vars(T as TFree(a, S)) = (case explode a of
wenzelm@256
  1023
          "?"::"'"::vn => let val ((b, i), _) = Syntax.scan_varname vn
wenzelm@256
  1024
                          in TVar(("'"^b, i), S) end
wenzelm@256
  1025
        | _ => T)
clasohm@0
  1026
  | thaw_vars(T) = T;
clasohm@0
  1027
clasohm@0
  1028
clasohm@0
  1029
fun restrict tye =
wenzelm@256
  1030
  let fun clean(tye1, ((a, i), T)) =
wenzelm@256
  1031
        if i < 0 then tye1 else ((a, i), inst_typ tye T) :: tye1
wenzelm@256
  1032
  in foldl clean ([], tye) end
clasohm@0
  1033
clasohm@0
  1034
clasohm@0
  1035
(*Infer types for term t using tables. Check that t's type and T unify *)
clasohm@0
  1036
wenzelm@565
  1037
fun infer_term (tsig, const_type, types, sorts, T, t) =
wenzelm@565
  1038
  let
wenzelm@565
  1039
    val u = attach_types (tsig, const_type, types, sorts) t;
wenzelm@565
  1040
    val (U, tye) = infer tsig ([], u, []);
wenzelm@565
  1041
    val uu = unconstrain u;
wenzelm@565
  1042
    val tye' = unify tsig ((T, U), tye) handle TUNIFY => raise TYPE
wenzelm@565
  1043
      ("Term does not have expected type", [T, U], [inst_types tye uu])
wenzelm@565
  1044
    val Ttye = restrict tye' (*restriction to TVars in T*)
wenzelm@565
  1045
    val all = Const("", Type("", map snd Ttye)) $ (inst_types tye' uu)
wenzelm@565
  1046
      (*all is a dummy term which contains all exported TVars*)
wenzelm@565
  1047
    val Const(_, Type(_, Ts)) $ u'' =
wenzelm@565
  1048
      map_term_types thaw_vars (freeze (fn (_, i) => i < 0) all)
wenzelm@565
  1049
      (*turn all internally generated TVars into TFrees
wenzelm@565
  1050
        and thaw all initially frozen TVars*)
wenzelm@565
  1051
  in
wenzelm@565
  1052
    (u'', (map fst Ttye) ~~ Ts)
wenzelm@565
  1053
  end;
clasohm@0
  1054
clasohm@0
  1055
fun infer_types args = (tyinit(); infer_term args);
clasohm@0
  1056
clasohm@0
  1057
clasohm@0
  1058
(* Turn TFrees into TVars to allow types & axioms to be written without "?" *)
wenzelm@256
  1059
fun varifyT (Type (a, Ts)) = Type (a, map varifyT Ts)
wenzelm@256
  1060
  | varifyT (TFree (a, S)) = TVar ((a, 0), S)
wenzelm@256
  1061
  | varifyT T = T;
clasohm@0
  1062
clasohm@0
  1063
(* Turn TFrees except those in fixed into new TVars *)
wenzelm@256
  1064
fun varify (t, fixed) =
wenzelm@256
  1065
  let val fs = add_term_tfree_names(t, []) \\ fixed;
wenzelm@256
  1066
      val ixns = add_term_tvar_ixns(t, []);
clasohm@0
  1067
      val fmap = fs ~~ variantlist(fs, map #1 ixns)
wenzelm@256
  1068
      fun thaw(Type(a, Ts)) = Type(a, map thaw Ts)
clasohm@0
  1069
        | thaw(T as TVar _) = T
wenzelm@256
  1070
        | thaw(T as TFree(a, S)) =
wenzelm@256
  1071
            (case assoc(fmap, a) of None => T | Some b => TVar((b, 0), S))
clasohm@0
  1072
  in map_term_types thaw t end;
clasohm@0
  1073
clasohm@0
  1074
clasohm@0
  1075
end;
wenzelm@256
  1076