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