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