src/Pure/type.ML
author berghofe
Mon Oct 21 17:15:40 2002 +0200 (2002-10-21 ago)
changeset 13666 a2730043029b
parent 12726 5ae4034883d5
child 14790 0d984ee030a1
permissions -rw-r--r--
Removed add_env because Vartab.map was too slow for large environments.
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@2964
     5
Type signatures, unification of types, interface to type inference.
clasohm@0
     6
*)
clasohm@0
     7
clasohm@0
     8
signature TYPE =
wenzelm@2964
     9
sig
wenzelm@7641
    10
  (*TFrees and TVars*)
wenzelm@621
    11
  val no_tvars: typ -> typ
wenzelm@621
    12
  val varifyT: typ -> typ
wenzelm@621
    13
  val unvarifyT: typ -> typ
wenzelm@12501
    14
  val varify: term * string list -> term * (string * indexname) list
wenzelm@10495
    15
  val freeze_thaw_type : typ -> typ * (typ -> typ)
paulson@3411
    16
  val freeze_thaw : term -> term * (term -> term)
wenzelm@2964
    17
wenzelm@2964
    18
  (*type signatures*)
clasohm@0
    19
  type type_sig
nipkow@200
    20
  val rep_tsig: type_sig ->
wenzelm@256
    21
    {classes: class list,
wenzelm@7069
    22
     classrel: Sorts.classrel,
wenzelm@256
    23
     default: sort,
wenzelm@7069
    24
     tycons: int Symtab.table,
wenzelm@7641
    25
     log_types: string list,
wenzelm@7641
    26
     univ_witness: (typ * sort) option,
wenzelm@7069
    27
     abbrs: (string list * typ) Symtab.table,
wenzelm@7069
    28
     arities: Sorts.arities}
wenzelm@7641
    29
  val classes: type_sig -> class list
clasohm@0
    30
  val defaultS: type_sig -> sort
wenzelm@2964
    31
  val logical_types: type_sig -> string list
wenzelm@7641
    32
  val univ_witness: type_sig -> (typ * sort) option
wenzelm@2964
    33
  val subsort: type_sig -> sort * sort -> bool
wenzelm@2964
    34
  val eq_sort: type_sig -> sort * sort -> bool
wenzelm@2964
    35
  val norm_sort: type_sig -> sort -> sort
wenzelm@8899
    36
  val cert_class: type_sig -> class -> class
wenzelm@8899
    37
  val cert_sort: type_sig -> sort -> sort
wenzelm@7641
    38
  val witness_sorts: type_sig -> sort list -> sort list -> (typ * sort) list
wenzelm@2964
    39
  val rem_sorts: typ -> typ
wenzelm@416
    40
  val tsig0: type_sig
wenzelm@621
    41
  val ext_tsig_classes: type_sig -> (class * class list) list -> type_sig
wenzelm@2964
    42
  val ext_tsig_classrel: type_sig -> (class * class) list -> type_sig
wenzelm@422
    43
  val ext_tsig_defsort: type_sig -> sort -> type_sig
wenzelm@582
    44
  val ext_tsig_types: type_sig -> (string * int) list -> type_sig
wenzelm@621
    45
  val ext_tsig_abbrs: type_sig -> (string * string list * typ) list -> type_sig
nipkow@963
    46
  val ext_tsig_arities: type_sig -> (string * sort list * sort)list -> type_sig
wenzelm@256
    47
  val merge_tsigs: type_sig * type_sig -> type_sig
wenzelm@2964
    48
  val typ_errors: type_sig -> typ * string list -> string list
wenzelm@256
    49
  val cert_typ: type_sig -> typ -> typ
wenzelm@9504
    50
  val cert_typ_no_norm: type_sig -> typ -> typ
wenzelm@256
    51
  val norm_typ: type_sig -> typ -> typ
wenzelm@7069
    52
  val norm_term: type_sig -> term -> term
wenzelm@256
    53
  val inst_term_tvars: type_sig * (indexname * typ) list -> term -> term
berghofe@8406
    54
  val inst_typ_tvars: type_sig * (indexname * typ) list -> typ -> typ
wenzelm@2964
    55
wenzelm@2964
    56
  (*type matching*)
wenzelm@2964
    57
  exception TYPE_MATCH
berghofe@8406
    58
  val typ_match: type_sig -> typ Vartab.table * (typ * typ)
berghofe@8406
    59
    -> typ Vartab.table
wenzelm@2964
    60
  val typ_instance: type_sig * typ * typ -> bool
wenzelm@3175
    61
  val of_sort: type_sig -> typ * sort -> bool
wenzelm@2964
    62
wenzelm@2964
    63
  (*type unification*)
wenzelm@2964
    64
  exception TUNIFY
wenzelm@12528
    65
  val unify: type_sig -> typ Vartab.table * int -> typ * typ -> typ Vartab.table * int
wenzelm@450
    66
  val raw_unify: typ * typ -> bool
clasohm@0
    67
wenzelm@2964
    68
  (*type inference*)
wenzelm@3790
    69
  val get_sort: type_sig -> (indexname -> sort option) -> (sort -> sort)
wenzelm@3790
    70
    -> (indexname * sort) list -> indexname -> sort
wenzelm@2964
    71
  val constrain: term -> typ -> term
wenzelm@12528
    72
  val param: int -> string * sort -> typ
wenzelm@12528
    73
  val paramify_dummies: int * typ -> int * typ
wenzelm@2979
    74
  val infer_types: (term -> Pretty.T) -> (typ -> Pretty.T)
wenzelm@2979
    75
    -> type_sig -> (string -> typ option) -> (indexname -> typ option)
wenzelm@3790
    76
    -> (indexname -> sort option) -> (string -> string) -> (typ -> typ)
wenzelm@3790
    77
    -> (sort -> sort) -> string list -> bool -> typ list -> term list
wenzelm@2964
    78
    -> term list * (indexname * typ) list
wenzelm@2964
    79
end;
wenzelm@2964
    80
wenzelm@2964
    81
structure Type: TYPE =
clasohm@0
    82
struct
clasohm@0
    83
wenzelm@2964
    84
wenzelm@7641
    85
(*** TFrees and TVars ***)
wenzelm@621
    86
wenzelm@621
    87
fun no_tvars T =
wenzelm@12501
    88
  (case typ_tvars T of [] => T
wenzelm@12501
    89
  | vs => raise TYPE ("Illegal schematic type variable(s): " ^
wenzelm@12501
    90
      commas (map (Syntax.string_of_vname o #1) vs), [T], []));
wenzelm@621
    91
wenzelm@7641
    92
wenzelm@2964
    93
(* varify, unvarify *)
wenzelm@621
    94
wenzelm@2964
    95
val varifyT = map_type_tfree (fn (a, S) => TVar ((a, 0), S));
wenzelm@2964
    96
wenzelm@621
    97
fun unvarifyT (Type (a, Ts)) = Type (a, map unvarifyT Ts)
wenzelm@621
    98
  | unvarifyT (TVar ((a, 0), S)) = TFree (a, S)
wenzelm@621
    99
  | unvarifyT T = T;
wenzelm@621
   100
wenzelm@621
   101
fun varify (t, fixed) =
wenzelm@621
   102
  let
wenzelm@621
   103
    val fs = add_term_tfree_names (t, []) \\ fixed;
wenzelm@621
   104
    val ixns = add_term_tvar_ixns (t, []);
wenzelm@12501
   105
    val fmap = fs ~~ map (rpair 0) (variantlist (fs, map #1 ixns))
wenzelm@2964
   106
    fun thaw (f as (a, S)) =
wenzelm@2964
   107
      (case assoc (fmap, a) of
wenzelm@2964
   108
        None => TFree f
wenzelm@12501
   109
      | Some b => TVar (b, S));
wenzelm@12501
   110
  in (map_term_types (map_type_tfree thaw) t, fmap) end;
wenzelm@2964
   111
wenzelm@2964
   112
wenzelm@7641
   113
(* freeze_thaw: freeze TVars in a term; return the "thaw" inverse *)
paulson@3411
   114
wenzelm@7641
   115
local
wenzelm@7641
   116
wenzelm@7641
   117
fun new_name (ix, (pairs,used)) =
paulson@3411
   118
      let val v = variant used (string_of_indexname ix)
paulson@3411
   119
      in  ((ix,v)::pairs, v::used)  end;
wenzelm@621
   120
wenzelm@7641
   121
fun freeze_one alist (ix,sort) =
wenzelm@3790
   122
  TFree (the (assoc (alist, ix)), sort)
wenzelm@4142
   123
    handle OPTION =>
wenzelm@3790
   124
      raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []);
wenzelm@2964
   125
wenzelm@7641
   126
fun thaw_one alist (a,sort) = TVar (the (assoc (alist,a)), sort)
wenzelm@4142
   127
      handle OPTION => TFree(a,sort);
wenzelm@416
   128
wenzelm@10495
   129
in
wenzelm@10495
   130
wenzelm@10495
   131
(*this sort of code could replace unvarifyT*)
wenzelm@7641
   132
fun freeze_thaw_type T =
wenzelm@7641
   133
  let
wenzelm@7641
   134
    val used = add_typ_tfree_names (T, [])
wenzelm@7641
   135
    and tvars = map #1 (add_typ_tvars (T, []));
wenzelm@7641
   136
    val (alist, _) = foldr new_name (tvars, ([], used));
wenzelm@7641
   137
  in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
wenzelm@7641
   138
paulson@3411
   139
fun freeze_thaw t =
wenzelm@7641
   140
  let
wenzelm@7641
   141
    val used = it_term_types add_typ_tfree_names (t, [])
wenzelm@7641
   142
    and tvars = map #1 (it_term_types add_typ_tvars (t, []));
wenzelm@7641
   143
    val (alist, _) = foldr new_name (tvars, ([], used));
wenzelm@7641
   144
  in
wenzelm@7641
   145
    (case alist of
wenzelm@7641
   146
      [] => (t, fn x => x) (*nothing to do!*)
wenzelm@7641
   147
    | _ => (map_term_types (map_type_tvar (freeze_one alist)) t,
wenzelm@7641
   148
      map_term_types (map_type_tfree (thaw_one (map swap alist)))))
wenzelm@7641
   149
  end;
wenzelm@7641
   150
wenzelm@7641
   151
end;
wenzelm@7641
   152
wenzelm@256
   153
wenzelm@256
   154
wenzelm@416
   155
(*** type signatures ***)
wenzelm@256
   156
wenzelm@2964
   157
(* type type_sig *)
wenzelm@2964
   158
wenzelm@256
   159
(*
wenzelm@7641
   160
  classes: list of all declared classes;
wenzelm@7641
   161
  classrel: (see Pure/sorts.ML)
wenzelm@7641
   162
  default: default sort attached to all unconstrained type vars;
wenzelm@7641
   163
  tycons: table of all declared types with the number of their arguments;
wenzelm@7641
   164
  log_types: list of logical type constructors sorted by number of arguments;
wenzelm@7641
   165
  univ_witness: type witnessing non-emptiness of least sort
wenzelm@7641
   166
  abbrs: table of type abbreviations;
wenzelm@7641
   167
  arities: (see Pure/sorts.ML)
clasohm@0
   168
*)
clasohm@0
   169
wenzelm@256
   170
datatype type_sig =
wenzelm@256
   171
  TySg of {
wenzelm@256
   172
    classes: class list,
wenzelm@7069
   173
    classrel: Sorts.classrel,
wenzelm@256
   174
    default: sort,
wenzelm@7069
   175
    tycons: int Symtab.table,
wenzelm@7641
   176
    log_types: string list,
wenzelm@7641
   177
    univ_witness: (typ * sort) option,
wenzelm@7069
   178
    abbrs: (string list * typ) Symtab.table,
wenzelm@7069
   179
    arities: Sorts.arities};
wenzelm@256
   180
nipkow@189
   181
fun rep_tsig (TySg comps) = comps;
clasohm@0
   182
wenzelm@7641
   183
fun classes (TySg {classes = cs, ...}) = cs;
wenzelm@256
   184
fun defaultS (TySg {default, ...}) = default;
wenzelm@7641
   185
fun logical_types (TySg {log_types, ...}) = log_types;
wenzelm@7641
   186
fun univ_witness (TySg {univ_witness, ...}) = univ_witness;
wenzelm@8899
   187
wenzelm@8899
   188
wenzelm@8899
   189
(* error messages *)
wenzelm@8899
   190
wenzelm@8899
   191
fun undeclared_class c = "Undeclared class: " ^ quote c;
wenzelm@8899
   192
fun undeclared_classes cs = "Undeclared class(es): " ^ commas_quote cs;
wenzelm@8899
   193
wenzelm@8899
   194
fun err_undeclared_class s = error (undeclared_class s);
wenzelm@8899
   195
wenzelm@8899
   196
fun err_dup_classes cs =
wenzelm@8899
   197
  error ("Duplicate declaration of class(es): " ^ commas_quote cs);
wenzelm@8899
   198
wenzelm@8899
   199
fun undeclared_type c = "Undeclared type constructor: " ^ quote c;
wenzelm@8899
   200
wenzelm@8899
   201
fun err_neg_args c =
wenzelm@8899
   202
  error ("Negative number of arguments of type constructor: " ^ quote c);
wenzelm@8899
   203
wenzelm@8899
   204
fun err_dup_tycon c =
wenzelm@8899
   205
  error ("Duplicate declaration of type constructor: " ^ quote c);
wenzelm@8899
   206
wenzelm@8899
   207
fun dup_tyabbrs ts =
wenzelm@8899
   208
  "Duplicate declaration of type abbreviation(s): " ^ commas_quote ts;
wenzelm@8899
   209
wenzelm@8899
   210
fun ty_confl c = "Conflicting type constructor and abbreviation: " ^ quote c;
wenzelm@2964
   211
wenzelm@2964
   212
wenzelm@2964
   213
(* sorts *)
wenzelm@2964
   214
wenzelm@2964
   215
fun subsort (TySg {classrel, ...}) = Sorts.sort_le classrel;
wenzelm@2964
   216
fun eq_sort (TySg {classrel, ...}) = Sorts.sort_eq classrel;
wenzelm@2964
   217
fun norm_sort (TySg {classrel, ...}) = Sorts.norm_sort classrel;
wenzelm@2964
   218
wenzelm@8899
   219
fun cert_class (TySg {classes, ...}) c =
wenzelm@8899
   220
  if c mem_string classes then c else raise TYPE (undeclared_class c, [], []);
wenzelm@8899
   221
wenzelm@8899
   222
fun cert_sort tsig S = norm_sort tsig (map (cert_class tsig) S);
wenzelm@8899
   223
wenzelm@7641
   224
fun witness_sorts (tsig as TySg {classrel, arities, log_types, ...}) =
wenzelm@7641
   225
  Sorts.witness_sorts (classrel, arities, log_types);
wenzelm@2964
   226
wenzelm@2964
   227
fun rem_sorts (Type (a, tys)) = Type (a, map rem_sorts tys)
wenzelm@2964
   228
  | rem_sorts (TFree (x, _)) = TFree (x, [])
wenzelm@2964
   229
  | rem_sorts (TVar (xi, _)) = TVar (xi, []);
wenzelm@2964
   230
wenzelm@256
   231
wenzelm@8899
   232
(* FIXME err_undeclared_class! *)
clasohm@0
   233
(* 'leq' checks the partial order on classes according to the
wenzelm@7641
   234
   statements in classrel 'a'
clasohm@0
   235
*)
clasohm@0
   236
wenzelm@7069
   237
fun less a (C, D) = case Symtab.lookup (a, C) of
paulson@2182
   238
     Some ss => D mem_string ss
wenzelm@8899
   239
   | None => err_undeclared_class C;
clasohm@0
   240
wenzelm@256
   241
fun leq a (C, D)  =  C = D orelse less a (C, D);
clasohm@0
   242
clasohm@0
   243
clasohm@0
   244
wenzelm@2964
   245
(* FIXME *)
nipkow@200
   246
(*Instantiation of type variables in types*)
nipkow@200
   247
(*Pre: instantiations obey restrictions! *)
nipkow@200
   248
fun inst_typ tye =
nipkow@949
   249
  let fun inst(var as (v, _)) = case assoc(tye, v) of
nipkow@949
   250
                                  Some U => inst_typ tye U
nipkow@949
   251
                                | None => TVar(var)
nipkow@949
   252
  in map_type_tvar inst end;
clasohm@0
   253
clasohm@0
   254
wenzelm@3175
   255
wenzelm@7641
   256
fun of_sort (TySg {classrel, arities, ...}) = Sorts.of_sort (classrel, arities);
wenzelm@3175
   257
wenzelm@3175
   258
fun check_has_sort (tsig, T, S) =
wenzelm@3175
   259
  if of_sort tsig (T, S) then ()
wenzelm@3790
   260
  else raise TYPE ("Type not of sort " ^ Sorts.str_of_sort S, [T], []);
clasohm@0
   261
clasohm@0
   262
clasohm@0
   263
(*Instantiation of type variables in types *)
wenzelm@256
   264
fun inst_typ_tvars(tsig, tye) =
nipkow@949
   265
  let fun inst(var as (v, S)) = case assoc(tye, v) of
nipkow@949
   266
              Some U => (check_has_sort(tsig, U, S); U)
nipkow@949
   267
            | None => TVar(var)
nipkow@949
   268
  in map_type_tvar inst end;
clasohm@0
   269
clasohm@0
   270
(*Instantiation of type variables in terms *)
paulson@2617
   271
fun inst_term_tvars (_,[]) t = t
paulson@2617
   272
  | inst_term_tvars arg    t = map_term_types (inst_typ_tvars arg) t;
nipkow@200
   273
nipkow@200
   274
wenzelm@7069
   275
(* norm_typ, norm_term *)
nipkow@200
   276
wenzelm@2991
   277
(*expand abbreviations and normalize sorts*)
wenzelm@2991
   278
fun norm_typ (tsig as TySg {abbrs, ...}) ty =
wenzelm@256
   279
  let
wenzelm@621
   280
    val idx = maxidx_of_typ ty + 1;
wenzelm@621
   281
wenzelm@2991
   282
    fun norm (Type (a, Ts)) =
wenzelm@7069
   283
          (case Symtab.lookup (abbrs, a) of
wenzelm@2991
   284
            Some (vs, U) => norm (inst_typ (map (rpair idx) vs ~~ Ts) (incr_tvar idx U))
wenzelm@2991
   285
          | None => Type (a, map norm Ts))
wenzelm@2991
   286
      | norm (TFree (x, S)) = TFree (x, norm_sort tsig S)
wenzelm@2991
   287
      | norm (TVar (xi, S)) = TVar (xi, norm_sort tsig S);
wenzelm@7069
   288
wenzelm@7069
   289
    val ty' = norm ty;
wenzelm@7069
   290
  in if ty = ty' then ty else ty' end;  (*dumb tuning to avoid copying*)
wenzelm@256
   291
wenzelm@7069
   292
fun norm_term tsig t =
wenzelm@7069
   293
  let val t' = map_term_types (norm_typ tsig) t
wenzelm@7069
   294
  in if t = t' then t else t' end;  (*dumb tuning to avoid copying*)
wenzelm@256
   295
wenzelm@256
   296
wenzelm@256
   297
wenzelm@256
   298
(** build type signatures **)
wenzelm@256
   299
wenzelm@7641
   300
fun make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities) =
wenzelm@7641
   301
  TySg {classes = classes, classrel = classrel, default = default, tycons = tycons,
wenzelm@7641
   302
    log_types = log_types, univ_witness = univ_witness, abbrs = abbrs, arities = arities};
wenzelm@7641
   303
wenzelm@7641
   304
fun rebuild_tsig (TySg {classes, classrel, default, tycons, log_types = _, univ_witness = _, abbrs, arities}) =
wenzelm@7641
   305
  let
wenzelm@7641
   306
    fun log_class c = Sorts.class_le classrel (c, logicC);
wenzelm@7641
   307
    fun log_type (t, _) = exists (log_class o #1) (Symtab.lookup_multi (arities, t));
wenzelm@7641
   308
    val ts = filter log_type (Symtab.dest tycons);
wenzelm@416
   309
wenzelm@7641
   310
    val log_types = map #1 (Library.sort (Library.int_ord o pairself #2) ts);
wenzelm@7641
   311
    val univ_witness =
wenzelm@7641
   312
      (case Sorts.witness_sorts (classrel, arities, log_types) [] [classes] of
wenzelm@7641
   313
        [w] => Some w | _ => None);
wenzelm@7641
   314
  in make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities) end;
wenzelm@256
   315
wenzelm@7641
   316
val tsig0 =
wenzelm@7641
   317
  make_tsig ([], Symtab.empty, [], Symtab.empty, [], None, Symtab.empty, Symtab.empty)
wenzelm@7641
   318
  |> rebuild_tsig;
wenzelm@1215
   319
wenzelm@1215
   320
wenzelm@416
   321
(* typ_errors *)
wenzelm@256
   322
wenzelm@416
   323
(*check validity of (not necessarily normal) type; accumulate error messages*)
wenzelm@256
   324
wenzelm@416
   325
fun typ_errors tsig (typ, errors) =
wenzelm@256
   326
  let
wenzelm@7069
   327
    val {classes, tycons, abbrs, ...} = rep_tsig tsig;
wenzelm@416
   328
wenzelm@416
   329
    fun class_err (errs, c) =
paulson@2182
   330
      if c mem_string classes then errs
wenzelm@8899
   331
      else undeclared_class c ins_string errs;
wenzelm@256
   332
wenzelm@256
   333
    val sort_err = foldl class_err;
clasohm@0
   334
wenzelm@7069
   335
    fun typ_errs (errs, Type (c, Us)) =
wenzelm@256
   336
          let
wenzelm@7069
   337
            val errs' = foldl typ_errs (errs, Us);
wenzelm@256
   338
            fun nargs n =
wenzelm@256
   339
              if n = length Us then errs'
paulson@2182
   340
              else ("Wrong number of arguments: " ^ quote c) ins_string errs';
wenzelm@256
   341
          in
wenzelm@7069
   342
            (case Symtab.lookup (tycons, c) of
wenzelm@256
   343
              Some n => nargs n
wenzelm@256
   344
            | None =>
wenzelm@7069
   345
                (case Symtab.lookup (abbrs, c) of
wenzelm@256
   346
                  Some (vs, _) => nargs (length vs)
wenzelm@8899
   347
                | None => undeclared_type c ins_string errs))
wenzelm@256
   348
          end
wenzelm@7069
   349
    | typ_errs (errs, TFree (_, S)) = sort_err (errs, S)
wenzelm@7069
   350
    | typ_errs (errs, TVar ((x, i), S)) =
wenzelm@416
   351
        if i < 0 then
paulson@2182
   352
          ("Negative index for TVar " ^ quote x) ins_string sort_err (errs, S)
wenzelm@416
   353
        else sort_err (errs, S);
wenzelm@7069
   354
  in typ_errs (errors, typ) end;
wenzelm@256
   355
wenzelm@256
   356
wenzelm@8899
   357
(* cert_typ *)           (*exception TYPE*)
wenzelm@256
   358
wenzelm@9504
   359
fun cert_typ_no_norm tsig T =
wenzelm@2964
   360
  (case typ_errors tsig (T, []) of
wenzelm@9504
   361
    [] => T
wenzelm@3790
   362
  | errs => raise TYPE (cat_lines errs, [T], []));
wenzelm@256
   363
wenzelm@9504
   364
fun cert_typ tsig T = norm_typ tsig (cert_typ_no_norm tsig T);
wenzelm@9504
   365
wenzelm@256
   366
wenzelm@256
   367
wenzelm@422
   368
(** merge type signatures **)
wenzelm@256
   369
wenzelm@7641
   370
(* merge classrel *)
clasohm@0
   371
wenzelm@422
   372
fun assoc_union (as1, []) = as1
wenzelm@422
   373
  | assoc_union (as1, (key, l2) :: as2) =
paulson@2182
   374
      (case assoc_string (as1, key) of
wenzelm@7641
   375
        Some l1 => assoc_union (overwrite (as1, (key, l1 union_string l2)), as2)
wenzelm@422
   376
      | None => assoc_union ((key, l2) :: as1, as2));
clasohm@0
   377
wenzelm@2964
   378
fun merge_classrel (classrel1, classrel2) =
wenzelm@7069
   379
  let
wenzelm@7069
   380
    val classrel = transitive_closure (assoc_union (Symtab.dest classrel1, Symtab.dest classrel2))
paulson@2182
   381
  in
wenzelm@2964
   382
    if exists (op mem_string) classrel then
wenzelm@422
   383
      error ("Cyclic class structure!")   (* FIXME improve msg, raise TERM *)
wenzelm@7069
   384
    else Symtab.make classrel
wenzelm@416
   385
  end;
wenzelm@416
   386
wenzelm@416
   387
wenzelm@422
   388
(* coregularity *)
clasohm@0
   389
wenzelm@7641
   390
local
wenzelm@7641
   391
clasohm@0
   392
(* 'is_unique_decl' checks if there exists just one declaration t:(Ss)C *)
clasohm@0
   393
nipkow@963
   394
fun is_unique_decl ars (t,(C,w)) = case assoc (ars, C) of
clasohm@0
   395
      Some(w1) => if w = w1 then () else
wenzelm@256
   396
        error("There are two declarations\n" ^
wenzelm@2964
   397
              Sorts.str_of_arity(t, w, [C]) ^ " and\n" ^
wenzelm@2964
   398
              Sorts.str_of_arity(t, w1, [C]) ^ "\n" ^
clasohm@0
   399
              "with the same result class.")
clasohm@0
   400
    | None => ();
clasohm@0
   401
nipkow@963
   402
(* 'coreg' checks if there are two declarations t:(Ss1)C1 and t:(Ss2)C2
clasohm@0
   403
   such that C1 >= C2 then Ss1 >= Ss2 (elementwise) *)
clasohm@0
   404
nipkow@963
   405
fun coreg_err(t, (C1,w1), (C2,w2)) =
wenzelm@2964
   406
    error("Declarations " ^ Sorts.str_of_arity(t, w1, [C1]) ^ " and "
wenzelm@2964
   407
                          ^ Sorts.str_of_arity(t, w2, [C2]) ^ " are in conflict");
clasohm@0
   408
wenzelm@2964
   409
fun coreg classrel (t, Cw1) =
wenzelm@2964
   410
  let
wenzelm@2964
   411
    fun check1(Cw1 as (C1,w1), Cw2 as (C2,w2)) =
wenzelm@2964
   412
      if leq classrel (C1,C2) then
wenzelm@2964
   413
        if Sorts.sorts_le classrel (w1,w2) then ()
wenzelm@2964
   414
        else coreg_err(t, Cw1, Cw2)
wenzelm@2964
   415
      else ()
wenzelm@2964
   416
    fun check(Cw2) = (check1(Cw1,Cw2); check1(Cw2,Cw1))
nipkow@963
   417
  in seq check end;
clasohm@0
   418
wenzelm@7641
   419
in
wenzelm@7641
   420
wenzelm@2964
   421
fun add_arity classrel ars (tCw as (_,Cw)) =
wenzelm@2964
   422
      (is_unique_decl ars tCw; coreg classrel tCw ars; Cw ins ars);
clasohm@0
   423
wenzelm@7641
   424
end;
clasohm@0
   425
clasohm@0
   426
nipkow@963
   427
(* 'merge_arities' builds the union of two 'arities' lists;
wenzelm@422
   428
   it only checks the two restriction conditions and inserts afterwards
wenzelm@422
   429
   all elements of the second list into the first one *)
wenzelm@422
   430
wenzelm@7641
   431
local
wenzelm@7641
   432
wenzelm@7069
   433
fun merge_arities_aux classrel =
wenzelm@2964
   434
  let fun test_ar t (ars1, sw) = add_arity classrel ars1 (t,sw);
wenzelm@422
   435
nipkow@963
   436
      fun merge_c (arities1, (c as (t, ars2))) = case assoc (arities1, t) of
nipkow@963
   437
          Some(ars1) =>
nipkow@963
   438
            let val ars = foldl (test_ar t) (ars1, ars2)
nipkow@963
   439
            in overwrite (arities1, (t,ars)) end
nipkow@963
   440
        | None => c::arities1
wenzelm@422
   441
  in foldl merge_c end;
wenzelm@422
   442
wenzelm@7641
   443
in
wenzelm@7641
   444
wenzelm@7069
   445
fun merge_arities classrel (a1, a2) =
wenzelm@7069
   446
  Symtab.make (merge_arities_aux classrel (Symtab.dest a1, Symtab.dest a2));
wenzelm@422
   447
wenzelm@7641
   448
end;
wenzelm@7641
   449
wenzelm@7641
   450
wenzelm@7641
   451
(* tycons *)
wenzelm@7641
   452
wenzelm@7641
   453
fun varying_decls t =
wenzelm@7641
   454
  error ("Type constructor " ^ quote t ^ " has varying number of arguments");
wenzelm@7641
   455
wenzelm@7069
   456
fun add_tycons (tycons, tn as (t,n)) =
wenzelm@7069
   457
  (case Symtab.lookup (tycons, t) of
wenzelm@7069
   458
    Some m => if m = n then tycons else varying_decls t
wenzelm@7069
   459
  | None => Symtab.update (tn, tycons));
wenzelm@7069
   460
wenzelm@7641
   461
wenzelm@7641
   462
(* merge_abbrs *)
wenzelm@7641
   463
wenzelm@7069
   464
fun merge_abbrs abbrs =
wenzelm@7069
   465
  Symtab.merge (op =) abbrs handle Symtab.DUPS dups => raise TERM (dup_tyabbrs dups, []);
wenzelm@422
   466
wenzelm@422
   467
wenzelm@7641
   468
(* merge_tsigs *)
wenzelm@422
   469
wenzelm@7641
   470
fun merge_tsigs
wenzelm@7641
   471
 (TySg {classes = classes1, default = default1, classrel = classrel1, tycons = tycons1,
wenzelm@7641
   472
    log_types = _, univ_witness = _, arities = arities1, abbrs = abbrs1},
wenzelm@7641
   473
  TySg {classes = classes2, default = default2, classrel = classrel2, tycons = tycons2,
wenzelm@7641
   474
    log_types = _, univ_witness = _, arities = arities2, abbrs = abbrs2}) =
wenzelm@7641
   475
  let
wenzelm@7641
   476
    val classes' = classes1 union_string classes2;
wenzelm@7641
   477
    val classrel' = merge_classrel (classrel1, classrel2);
wenzelm@7641
   478
    val arities' = merge_arities classrel' (arities1, arities2);
wenzelm@7641
   479
    val tycons' = foldl add_tycons (tycons1, Symtab.dest tycons2);
wenzelm@7641
   480
    val default' = Sorts.norm_sort classrel' (default1 @ default2);
wenzelm@7641
   481
    val abbrs' = merge_abbrs (abbrs1, abbrs2);
wenzelm@7641
   482
  in
wenzelm@7641
   483
    make_tsig (classes', classrel', default', tycons', [], None, abbrs', arities')
wenzelm@7641
   484
    |> rebuild_tsig
wenzelm@7641
   485
  end;
wenzelm@422
   486
wenzelm@422
   487
wenzelm@422
   488
wenzelm@422
   489
(*** extend type signatures ***)
wenzelm@422
   490
wenzelm@2964
   491
(** add classes and classrel relations **)
wenzelm@422
   492
wenzelm@422
   493
fun add_classes classes cs =
paulson@2182
   494
  (case cs inter_string classes of
wenzelm@422
   495
    [] => cs @ classes
wenzelm@422
   496
  | dups => err_dup_classes cs);
wenzelm@422
   497
wenzelm@422
   498
wenzelm@2964
   499
(*'add_classrel' adds a tuple consisting of a new class (the new class has
wenzelm@422
   500
  already been inserted into the 'classes' list) and its superclasses (they
wenzelm@2964
   501
  must be declared in 'classes' too) to the 'classrel' list of the given type
wenzelm@422
   502
  signature; furthermore all inherited superclasses according to the
wenzelm@422
   503
  superclasses brought with are inserted and there is a check that there are
wenzelm@422
   504
  no cycles (i.e. C <= D <= C, with C <> D);*)
wenzelm@422
   505
wenzelm@2964
   506
fun add_classrel classes (classrel, (s, ges)) =
wenzelm@621
   507
  let
wenzelm@2964
   508
    fun upd (classrel, s') =
paulson@2182
   509
      if s' mem_string classes then
wenzelm@7069
   510
        let val ges' = the (Symtab.lookup (classrel, s))
wenzelm@7069
   511
        in case Symtab.lookup (classrel, s') of
paulson@2182
   512
             Some sups => if s mem_string sups
wenzelm@422
   513
                           then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s )
wenzelm@7069
   514
                           else Symtab.update ((s, sups union_string ges'), classrel)
wenzelm@2964
   515
           | None => classrel
wenzelm@621
   516
        end
wenzelm@8899
   517
      else err_undeclared_class s'
wenzelm@7069
   518
  in foldl upd (Symtab.update ((s, ges), classrel), ges) end;
wenzelm@422
   519
wenzelm@422
   520
wenzelm@422
   521
(* 'extend_classes' inserts all new classes into the corresponding
wenzelm@2964
   522
   lists ('classes', 'classrel') if possible *)
wenzelm@422
   523
wenzelm@2964
   524
fun extend_classes (classes, classrel, new_classes) =
wenzelm@621
   525
  let
wenzelm@621
   526
    val classes' = add_classes classes (map fst new_classes);
wenzelm@2964
   527
    val classrel' = foldl (add_classrel classes') (classrel, new_classes);
wenzelm@2964
   528
  in (classes', classrel') end;
wenzelm@422
   529
wenzelm@422
   530
wenzelm@621
   531
(* ext_tsig_classes *)
wenzelm@621
   532
wenzelm@621
   533
fun ext_tsig_classes tsig new_classes =
wenzelm@621
   534
  let
wenzelm@7641
   535
    val TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities} = tsig;
wenzelm@11022
   536
    val (classes', classrel') = extend_classes (classes,classrel, new_classes);
wenzelm@12222
   537
  in
wenzelm@12222
   538
    make_tsig (classes', classrel', default, tycons, log_types, univ_witness, abbrs, arities)
wenzelm@12222
   539
    |> rebuild_tsig
wenzelm@12222
   540
  end;
wenzelm@621
   541
wenzelm@621
   542
wenzelm@2964
   543
(* ext_tsig_classrel *)
wenzelm@422
   544
wenzelm@2964
   545
fun ext_tsig_classrel tsig pairs =
wenzelm@422
   546
  let
wenzelm@7641
   547
    val TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities} = tsig;
wenzelm@11022
   548
    val cert = cert_class tsig;
wenzelm@422
   549
wenzelm@422
   550
    (* FIXME clean! *)
wenzelm@2964
   551
    val classrel' =
wenzelm@11022
   552
      merge_classrel (classrel, Symtab.make (map (fn (c1, c2) => (cert c1, [cert c2])) pairs));
wenzelm@422
   553
  in
wenzelm@7641
   554
    make_tsig (classes, classrel', default, tycons, log_types, univ_witness, abbrs, arities)
wenzelm@7641
   555
    |> rebuild_tsig
wenzelm@422
   556
  end;
wenzelm@422
   557
wenzelm@422
   558
wenzelm@422
   559
(* ext_tsig_defsort *)
wenzelm@422
   560
wenzelm@7641
   561
fun ext_tsig_defsort
wenzelm@7641
   562
    (TySg {classes, classrel, default = _, tycons, log_types, univ_witness, abbrs, arities, ...}) default =
wenzelm@7641
   563
  make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities);
wenzelm@422
   564
wenzelm@422
   565
wenzelm@422
   566
wenzelm@621
   567
(** add types **)
wenzelm@582
   568
wenzelm@7641
   569
fun ext_tsig_types (TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities}) ts =
wenzelm@582
   570
  let
wenzelm@582
   571
    fun check_type (c, n) =
wenzelm@582
   572
      if n < 0 then err_neg_args c
wenzelm@7069
   573
      else if is_some (Symtab.lookup (tycons, c)) then err_dup_tycon c
wenzelm@7069
   574
      else if is_some (Symtab.lookup (abbrs, c)) then error (ty_confl c)
wenzelm@582
   575
      else ();
wenzelm@7641
   576
    val _ = seq check_type ts;
wenzelm@7641
   577
    val tycons' = Symtab.extend (tycons, ts);
wenzelm@7641
   578
    val arities' = Symtab.extend (arities, map (rpair [] o #1) ts);
wenzelm@7641
   579
  in make_tsig (classes, classrel, default, tycons', log_types, univ_witness, abbrs, arities') end;
wenzelm@582
   580
wenzelm@582
   581
wenzelm@582
   582
wenzelm@582
   583
(** add type abbreviations **)
wenzelm@582
   584
wenzelm@582
   585
fun abbr_errors tsig (a, (lhs_vs, rhs)) =
wenzelm@582
   586
  let
nipkow@963
   587
    val TySg {tycons, abbrs, ...} = tsig;
wenzelm@621
   588
    val rhs_vs = map (#1 o #1) (typ_tvars rhs);
wenzelm@582
   589
wenzelm@582
   590
    val dup_lhs_vars =
wenzelm@582
   591
      (case duplicates lhs_vs of
wenzelm@582
   592
        [] => []
wenzelm@621
   593
      | vs => ["Duplicate variables on lhs: " ^ commas_quote vs]);
wenzelm@582
   594
wenzelm@582
   595
    val extra_rhs_vars =
wenzelm@582
   596
      (case gen_rems (op =) (rhs_vs, lhs_vs) of
wenzelm@582
   597
        [] => []
wenzelm@621
   598
      | vs => ["Extra variables on rhs: " ^ commas_quote vs]);
wenzelm@582
   599
wenzelm@582
   600
    val tycon_confl =
wenzelm@7069
   601
      if is_none (Symtab.lookup (tycons, a)) then []
wenzelm@582
   602
      else [ty_confl a];
wenzelm@582
   603
wenzelm@582
   604
    val dup_abbr =
wenzelm@7069
   605
      if is_none (Symtab.lookup (abbrs, a)) then []
wenzelm@582
   606
      else ["Duplicate declaration of abbreviation"];
wenzelm@582
   607
  in
wenzelm@582
   608
    dup_lhs_vars @ extra_rhs_vars @ tycon_confl @ dup_abbr @
wenzelm@582
   609
      typ_errors tsig (rhs, [])
wenzelm@582
   610
  end;
wenzelm@582
   611
wenzelm@621
   612
fun prep_abbr tsig (a, vs, raw_rhs) =
wenzelm@621
   613
  let
wenzelm@4974
   614
    fun err msgs = (seq error_msg msgs;
wenzelm@621
   615
      error ("The error(s) above occurred in type abbreviation " ^ quote a));
wenzelm@621
   616
wenzelm@621
   617
    val rhs = rem_sorts (varifyT (no_tvars raw_rhs))
wenzelm@621
   618
      handle TYPE (msg, _, _) => err [msg];
wenzelm@621
   619
    val abbr = (a, (vs, rhs));
wenzelm@621
   620
  in
wenzelm@582
   621
    (case abbr_errors tsig abbr of
wenzelm@621
   622
      [] => abbr
wenzelm@621
   623
    | msgs => err msgs)
wenzelm@582
   624
  end;
wenzelm@582
   625
wenzelm@7641
   626
fun add_abbr
wenzelm@7641
   627
    (tsig as TySg {classes, classrel, default, tycons, log_types, univ_witness, arities, abbrs}, abbr) =
wenzelm@7641
   628
  make_tsig (classes, classrel, default, tycons, log_types, univ_witness,
wenzelm@7641
   629
    Symtab.update (prep_abbr tsig abbr, abbrs), arities);
wenzelm@621
   630
wenzelm@621
   631
fun ext_tsig_abbrs tsig raw_abbrs = foldl add_abbr (tsig, raw_abbrs);
wenzelm@582
   632
wenzelm@582
   633
wenzelm@582
   634
wenzelm@422
   635
(** add arities **)
wenzelm@422
   636
clasohm@0
   637
(* 'coregular' checks
nipkow@963
   638
   - the two restrictions 'is_unique_decl' and 'coreg'
wenzelm@256
   639
   - if the classes in the new type declarations are known in the
clasohm@0
   640
     given type signature
clasohm@0
   641
   - if one type constructor has always the same number of arguments;
wenzelm@256
   642
   if one type declaration has passed all checks it is inserted into
nipkow@963
   643
   the 'arities' association list of the given type signatrure  *)
clasohm@0
   644
wenzelm@2964
   645
fun coregular (classes, classrel, tycons) =
wenzelm@8899
   646
  let fun ex C = if C mem_string classes then () else err_undeclared_class(C);
clasohm@0
   647
wenzelm@7069
   648
      fun addar(arities, (t, (w, C))) = case Symtab.lookup (tycons, t) of
clasohm@0
   649
            Some(n) => if n <> length w then varying_decls(t) else
nipkow@963
   650
                     ((seq o seq) ex w; ex C;
wenzelm@7069
   651
                      let val ars = the (Symtab.lookup (arities, t))
wenzelm@2964
   652
                          val ars' = add_arity classrel ars (t,(C,w))
wenzelm@7069
   653
                      in Symtab.update ((t,ars'), arities) end)
wenzelm@8899
   654
          | None => error (undeclared_type t);
clasohm@0
   655
nipkow@963
   656
  in addar end;
clasohm@0
   657
clasohm@0
   658
nipkow@963
   659
(* 'close' extends the 'arities' association list after all new type
clasohm@0
   660
   declarations have been inserted successfully:
clasohm@0
   661
   for every declaration t:(Ss)C , for all classses D with C <= D:
clasohm@0
   662
      if there is no declaration t:(Ss')C' with C < C' and C' <= D
nipkow@963
   663
      then insert the declaration t:(Ss)D into 'arities'
clasohm@0
   664
   this means, if there exists a declaration t:(Ss)C and there is
clasohm@0
   665
   no declaration t:(Ss')D with C <=D then the declaration holds
wenzelm@256
   666
   for all range classes more general than C *)
wenzelm@256
   667
wenzelm@2964
   668
fun close classrel arities =
wenzelm@7069
   669
  let fun check sl (l, (s, dom)) = case Symtab.lookup (classrel, s) of
wenzelm@621
   670
          Some sups =>
wenzelm@256
   671
            let fun close_sup (l, sup) =
wenzelm@2964
   672
                  if exists (fn s'' => less classrel (s, s'') andalso
wenzelm@2964
   673
                                       leq classrel (s'', sup)) sl
clasohm@0
   674
                  then l
wenzelm@256
   675
                  else (sup, dom)::l
wenzelm@256
   676
            in foldl close_sup (l, sups) end
clasohm@0
   677
        | None => l;
wenzelm@256
   678
      fun ext (s, l) = (s, foldl (check (map #1 l)) (l, l));
nipkow@963
   679
  in map ext arities end;
clasohm@0
   680
wenzelm@422
   681
wenzelm@621
   682
(* ext_tsig_arities *)
wenzelm@256
   683
wenzelm@2964
   684
fun norm_domain classrel =
wenzelm@2964
   685
  let fun one_min (f, (doms, ran)) = (f, (map (Sorts.norm_sort classrel) doms, ran))
wenzelm@2964
   686
  in map one_min end;
wenzelm@2964
   687
wenzelm@621
   688
fun ext_tsig_arities tsig sarities =
wenzelm@416
   689
  let
wenzelm@7641
   690
    val TySg {classes, classrel, default, tycons, log_types, univ_witness, arities, abbrs} = tsig;
nipkow@963
   691
    val arities1 =
wenzelm@7641
   692
      flat (map (fn (t, ss, cs) => map (fn c => (t, (ss, c))) cs) sarities);
wenzelm@7641
   693
    val arities2 =
wenzelm@7641
   694
      foldl (coregular (classes, classrel, tycons)) (arities, norm_domain classrel arities1)
wenzelm@7069
   695
      |> Symtab.dest |> close classrel |> Symtab.make;
wenzelm@416
   696
  in
wenzelm@7641
   697
    make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities2)
wenzelm@7641
   698
    |> rebuild_tsig
wenzelm@416
   699
  end;
clasohm@0
   700
clasohm@0
   701
wenzelm@416
   702
wenzelm@2964
   703
(*** type unification and friends ***)
clasohm@0
   704
wenzelm@2964
   705
(** matching **)
clasohm@0
   706
wenzelm@2964
   707
exception TYPE_MATCH;
clasohm@0
   708
wenzelm@2964
   709
fun typ_match tsig =
wenzelm@2964
   710
  let
wenzelm@2964
   711
    fun match (subs, (TVar (v, S), T)) =
berghofe@8406
   712
          (case Vartab.lookup (subs, v) of
berghofe@8406
   713
            None => (Vartab.update_new ((v, (check_has_sort (tsig, T, S); T)), subs)
wenzelm@2964
   714
              handle TYPE _ => raise TYPE_MATCH)
wenzelm@2964
   715
          | Some U => if U = T then subs else raise TYPE_MATCH)
wenzelm@2964
   716
      | match (subs, (Type (a, Ts), Type (b, Us))) =
wenzelm@2964
   717
          if a <> b then raise TYPE_MATCH
wenzelm@2964
   718
          else foldl match (subs, Ts ~~ Us)
wenzelm@2964
   719
      | match (subs, (TFree x, TFree y)) =
wenzelm@2964
   720
          if x = y then subs else raise TYPE_MATCH
wenzelm@2964
   721
      | match _ = raise TYPE_MATCH;
wenzelm@2964
   722
  in match end;
clasohm@0
   723
wenzelm@2964
   724
fun typ_instance (tsig, T, U) =
berghofe@8406
   725
  (typ_match tsig (Vartab.empty, (U, T)); true) handle TYPE_MATCH => false;
wenzelm@2964
   726
clasohm@0
   727
wenzelm@2964
   728
wenzelm@2964
   729
(** unification **)
wenzelm@2964
   730
clasohm@0
   731
exception TUNIFY;
clasohm@0
   732
clasohm@0
   733
wenzelm@2964
   734
(* occurs check *)
clasohm@0
   735
wenzelm@2964
   736
fun occurs v tye =
wenzelm@2964
   737
  let
wenzelm@2964
   738
    fun occ (Type (_, Ts)) = exists occ Ts
wenzelm@2964
   739
      | occ (TFree _) = false
wenzelm@2964
   740
      | occ (TVar (w, _)) =
wenzelm@2964
   741
          eq_ix (v, w) orelse
berghofe@8406
   742
            (case Vartab.lookup (tye, w) of
wenzelm@2964
   743
              None => false
wenzelm@2964
   744
            | Some U => occ U);
clasohm@0
   745
  in occ end;
clasohm@0
   746
wenzelm@2964
   747
wenzelm@2964
   748
(* chase variable assignments *)
wenzelm@2964
   749
wenzelm@2964
   750
(*if devar returns a type var then it must be unassigned*)
wenzelm@2964
   751
fun devar (T as TVar (v, _), tye) =
berghofe@8406
   752
      (case  Vartab.lookup (tye, v) of
wenzelm@2964
   753
        Some U => devar (U, tye)
wenzelm@2964
   754
      | None => T)
wenzelm@256
   755
  | devar (T, tye) = T;
clasohm@0
   756
berghofe@1627
   757
wenzelm@2964
   758
(* unify *)
wenzelm@2964
   759
wenzelm@12528
   760
fun unify (tsig as TySg {classrel, arities, ...}) (tyenv, maxidx) TU =
wenzelm@2964
   761
  let
wenzelm@2964
   762
    val tyvar_count = ref maxidx;
wenzelm@2964
   763
    fun gen_tyvar S = TVar (("'a", inc tyvar_count), S);
wenzelm@2964
   764
wenzelm@2964
   765
    fun mg_domain a S =
wenzelm@7641
   766
      Sorts.mg_domain (classrel, arities) a S handle Sorts.DOMAIN _ => raise TUNIFY;
wenzelm@2964
   767
wenzelm@2964
   768
    fun meet ((_, []), tye) = tye
wenzelm@2964
   769
      | meet ((TVar (xi, S'), S), tye) =
wenzelm@2964
   770
          if Sorts.sort_le classrel (S', S) then tye
berghofe@13666
   771
          else Vartab.update_new ((xi,
berghofe@13666
   772
            gen_tyvar (Sorts.inter_sort classrel (S', S))), tye)
wenzelm@2964
   773
      | meet ((TFree (_, S'), S), tye) =
wenzelm@2964
   774
          if Sorts.sort_le classrel (S', S) then tye
wenzelm@2964
   775
          else raise TUNIFY
wenzelm@2964
   776
      | meet ((Type (a, Ts), S), tye) = meets ((Ts, mg_domain a S), tye)
wenzelm@2964
   777
    and meets (([], []), tye) = tye
wenzelm@2964
   778
      | meets ((T :: Ts, S :: Ss), tye) =
wenzelm@2964
   779
          meets ((Ts, Ss), meet ((devar (T, tye), S), tye))
wenzelm@2964
   780
      | meets _ = sys_error "meets";
wenzelm@2964
   781
wenzelm@2964
   782
    fun unif ((ty1, ty2), tye) =
wenzelm@2964
   783
      (case (devar (ty1, tye), devar (ty2, tye)) of
wenzelm@2964
   784
        (T as TVar (v, S1), U as TVar (w, S2)) =>
wenzelm@2964
   785
          if eq_ix (v, w) then tye
berghofe@13666
   786
          else if Sorts.sort_le classrel (S1, S2) then
berghofe@13666
   787
            Vartab.update_new ((w, T), tye)
berghofe@13666
   788
          else if Sorts.sort_le classrel (S2, S1) then
berghofe@13666
   789
            Vartab.update_new ((v, U), tye)
wenzelm@2964
   790
          else
wenzelm@2964
   791
            let val S = gen_tyvar (Sorts.inter_sort classrel (S1, S2)) in
berghofe@13666
   792
              Vartab.update_new ((v, S), Vartab.update_new ((w, S), tye))
wenzelm@2964
   793
            end
wenzelm@2964
   794
      | (TVar (v, S), T) =>
wenzelm@2964
   795
          if occurs v tye T then raise TUNIFY
berghofe@13666
   796
          else meet ((T, S), Vartab.update_new ((v, T), tye))
wenzelm@2964
   797
      | (T, TVar (v, S)) =>
wenzelm@2964
   798
          if occurs v tye T then raise TUNIFY
berghofe@13666
   799
          else meet ((T, S), Vartab.update_new ((v, T), tye))
wenzelm@2964
   800
      | (Type (a, Ts), Type (b, Us)) =>
wenzelm@2964
   801
          if a <> b then raise TUNIFY
wenzelm@2964
   802
          else foldr unif (Ts ~~ Us, tye)
wenzelm@2964
   803
      | (T, U) => if T = U then tye else raise TUNIFY);
wenzelm@12528
   804
  in (unif (TU, tyenv), ! tyvar_count) end;
clasohm@0
   805
clasohm@0
   806
wenzelm@2964
   807
(* raw_unify *)
clasohm@0
   808
wenzelm@2964
   809
(*purely structural unification -- ignores sorts*)
wenzelm@450
   810
fun raw_unify (ty1, ty2) =
wenzelm@12528
   811
  (unify tsig0 (Vartab.empty, 0) (rem_sorts ty1, rem_sorts ty2); true)
wenzelm@450
   812
    handle TUNIFY => false;
wenzelm@450
   813
wenzelm@450
   814
clasohm@0
   815
wenzelm@2964
   816
(** type inference **)
nipkow@1435
   817
wenzelm@3790
   818
(* sort constraints *)
wenzelm@3790
   819
wenzelm@3790
   820
fun get_sort tsig def_sort map_sort raw_env =
wenzelm@3790
   821
  let
wenzelm@3790
   822
    fun eq ((xi, S), (xi', S')) =
wenzelm@3790
   823
      xi = xi' andalso eq_sort tsig (S, S');
wenzelm@3790
   824
wenzelm@3790
   825
    val env = gen_distinct eq (map (apsnd map_sort) raw_env);
wenzelm@3790
   826
    val _ =
wenzelm@3790
   827
      (case gen_duplicates eq_fst env of
wenzelm@3790
   828
        [] => ()
wenzelm@3790
   829
      | dups => error ("Inconsistent sort constraints for type variable(s) " ^
wenzelm@3790
   830
          commas (map (quote o Syntax.string_of_vname' o fst) dups)));
wenzelm@2587
   831
wenzelm@3790
   832
    fun get xi =
wenzelm@3790
   833
      (case (assoc (env, xi), def_sort xi) of
wenzelm@3790
   834
        (None, None) => defaultS tsig
wenzelm@3790
   835
      | (None, Some S) => S
wenzelm@3790
   836
      | (Some S, None) => S
wenzelm@3790
   837
      | (Some S, Some S') =>
wenzelm@3804
   838
          if eq_sort tsig (S, S') then S'
wenzelm@3790
   839
          else error ("Sort constraint inconsistent with default for type variable " ^
wenzelm@3790
   840
            quote (Syntax.string_of_vname' xi)));
wenzelm@3790
   841
  in get end;
wenzelm@3790
   842
wenzelm@3790
   843
wenzelm@3790
   844
(* type constraints *)
wenzelm@2587
   845
wenzelm@2964
   846
fun constrain t T =
wenzelm@2964
   847
  if T = dummyT then t
wenzelm@2964
   848
  else Const ("_type_constraint_", T) $ t;
clasohm@0
   849
clasohm@0
   850
wenzelm@4603
   851
(* user parameters *)
wenzelm@4603
   852
wenzelm@4603
   853
fun is_param (x, _) = size x > 0 andalso ord x = ord "?";
wenzelm@12528
   854
fun param i (x, S) = TVar (("?" ^ x, i), S);
wenzelm@12528
   855
wenzelm@12726
   856
fun paramify_dummies (maxidx, TFree ("'_dummy_", S)) =
wenzelm@12726
   857
      (maxidx + 1, param (maxidx + 1) ("'dummy", S))
wenzelm@12726
   858
  | paramify_dummies (maxidx, Type (a, Ts)) =
wenzelm@12726
   859
      let val (maxidx', Ts') = foldl_map paramify_dummies (maxidx, Ts)
wenzelm@12726
   860
      in (maxidx', Type (a, Ts')) end
wenzelm@12528
   861
  | paramify_dummies arg = arg;
wenzelm@4603
   862
wenzelm@4603
   863
wenzelm@2964
   864
(* decode_types *)
clasohm@0
   865
wenzelm@3804
   866
(*transform parse tree into raw term*)
wenzelm@3790
   867
fun decode_types tsig is_const def_type def_sort map_const map_type map_sort tm =
wenzelm@2964
   868
  let
wenzelm@2964
   869
    fun get_type xi = if_none (def_type xi) dummyT;
wenzelm@5080
   870
    fun is_free x = is_some (def_type (x, ~1));
wenzelm@3790
   871
    val raw_env = Syntax.raw_term_sorts tm;
wenzelm@3790
   872
    val sort_of = get_sort tsig def_sort map_sort raw_env;
wenzelm@2964
   873
wenzelm@3804
   874
    val certT = cert_typ tsig o map_type;
wenzelm@12314
   875
    fun decodeT t = certT (Syntax.typ_of_term sort_of map_sort t);
clasohm@0
   876
wenzelm@2964
   877
    fun decode (Const ("_constrain", _) $ t $ typ) =
wenzelm@2964
   878
          constrain (decode t) (decodeT typ)
wenzelm@3804
   879
      | decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) =
wenzelm@2964
   880
          if T = dummyT then Abs (x, decodeT typ, decode t)
wenzelm@3804
   881
          else constrain (Abs (x, certT T, decode t)) (decodeT typ --> dummyT)
wenzelm@3804
   882
      | decode (Abs (x, T, t)) = Abs (x, certT T, decode t)
wenzelm@2964
   883
      | decode (t $ u) = decode t $ decode u
wenzelm@3804
   884
      | decode (Free (x, T)) =
wenzelm@3790
   885
          let val c = map_const x in
wenzelm@8721
   886
            if not (is_free x) andalso (is_const c orelse NameSpace.is_qualified c) then
wenzelm@5080
   887
              Const (c, certT T)
wenzelm@3790
   888
            else if T = dummyT then Free (x, get_type (x, ~1))
wenzelm@3804
   889
            else constrain (Free (x, certT T)) (get_type (x, ~1))
wenzelm@3790
   890
          end
wenzelm@3804
   891
      | decode (Var (xi, T)) =
wenzelm@2964
   892
          if T = dummyT then Var (xi, get_type xi)
wenzelm@3804
   893
          else constrain (Var (xi, certT T)) (get_type xi)
wenzelm@2964
   894
      | decode (t as Bound _) = t
wenzelm@3804
   895
      | decode (Const (c, T)) = Const (map_const c, certT T);
wenzelm@8610
   896
  in decode tm end;
clasohm@0
   897
clasohm@0
   898
wenzelm@2964
   899
(* infer_types *)
nipkow@949
   900
nipkow@949
   901
(*
wenzelm@2964
   902
  Given [T1,...,Tn] and [t1,...,tn], ensure that the type of ti
wenzelm@2964
   903
  unifies with Ti (for i=1,...,n).
wenzelm@2964
   904
wenzelm@2964
   905
  tsig: type signature
wenzelm@3790
   906
  const_type: name mapping and signature lookup
wenzelm@2964
   907
  def_type: partial map from indexnames to types (constrains Frees, Vars)
wenzelm@2964
   908
  def_sort: partial map from indexnames to sorts (constrains TFrees, TVars)
wenzelm@2964
   909
  used: list of already used type variables
wenzelm@2964
   910
  freeze: if true then generated parameters are turned into TFrees, else TVars
nipkow@949
   911
*)
clasohm@0
   912
wenzelm@3790
   913
fun infer_types prt prT tsig const_type def_type def_sort
wenzelm@3790
   914
    map_const map_type map_sort used freeze pat_Ts raw_ts =
wenzelm@565
   915
  let
wenzelm@2964
   916
    val TySg {classrel, arities, ...} = tsig;
wenzelm@2964
   917
    val pat_Ts' = map (cert_typ tsig) pat_Ts;
wenzelm@3790
   918
    val is_const = is_some o const_type;
wenzelm@2964
   919
    val raw_ts' =
wenzelm@3790
   920
      map (decode_types tsig is_const def_type def_sort map_const map_type map_sort) raw_ts;
wenzelm@2964
   921
    val (ts, Ts, unifier) =
wenzelm@2979
   922
      TypeInfer.infer_types prt prT const_type classrel arities used freeze
wenzelm@4603
   923
        is_param raw_ts' pat_Ts';
wenzelm@7641
   924
  in (ts, unifier) end;
clasohm@0
   925
wenzelm@3790
   926
clasohm@0
   927
end;