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