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