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