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