|
1 (* Title: Types and Sorts |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow & Lawrence C Paulson |
|
4 |
|
5 Maybe type classes should go in a separate module? |
|
6 *) |
|
7 |
|
8 |
|
9 signature TYPE = |
|
10 sig |
|
11 structure Symtab:SYMTAB |
|
12 type type_sig |
|
13 val defaultS: type_sig -> sort |
|
14 val extend: type_sig * (class * class list)list * sort * |
|
15 (string list * int)list * |
|
16 (string list * (sort list * class))list -> type_sig |
|
17 val freeze: (indexname -> bool) -> term -> term |
|
18 val freeze_vars: typ -> typ |
|
19 val infer_types: type_sig * typ Symtab.table * (indexname -> typ option) * |
|
20 (indexname -> sort option) * (typ -> string) * typ * term |
|
21 -> term * (indexname*typ)list |
|
22 val inst_term_tvars: type_sig * (indexname * typ)list -> term -> term |
|
23 val logical_type: type_sig -> string -> bool |
|
24 val merge: type_sig * type_sig -> type_sig |
|
25 val thaw_vars: typ -> typ |
|
26 val tsig0: type_sig |
|
27 val type_errors: type_sig * (typ->string) -> typ * string list -> string list |
|
28 val typ_instance: type_sig * typ * typ -> bool |
|
29 val typ_match: type_sig -> (indexname*typ)list * (typ*typ) -> |
|
30 (indexname*typ)list |
|
31 val unify: type_sig -> (typ*typ) * (indexname*typ)list -> (indexname*typ)list |
|
32 val varifyT: typ -> typ |
|
33 val varify: term * string list -> term |
|
34 exception TUNIFY |
|
35 exception TYPE_MATCH; |
|
36 end; |
|
37 |
|
38 functor TypeFun(structure Symtab:SYMTAB and Syntax:SYNTAX) : TYPE = |
|
39 struct |
|
40 structure Symtab = Symtab |
|
41 |
|
42 (* Miscellany *) |
|
43 |
|
44 val commas = space_implode ","; |
|
45 fun str_of_sort S = "{" ^ commas S ^ "}"; |
|
46 fun str_of_dom dom = "(" ^ commas (map str_of_sort dom) ^ ")"; |
|
47 fun str_of_decl(t,w,C) = t ^ ": " ^ str_of_dom w ^ C; |
|
48 |
|
49 |
|
50 (* Association list Manipulation *) |
|
51 |
|
52 |
|
53 (* two-fold Association list lookup *) |
|
54 |
|
55 fun assoc2 (aal,(key1,key2)) = case assoc (aal,key1) of |
|
56 Some (al) => assoc (al,key2) |
|
57 | None => None; |
|
58 |
|
59 |
|
60 |
|
61 (**** TYPE CLASSES ****) |
|
62 |
|
63 type domain = sort list; |
|
64 type arity = domain * class; |
|
65 |
|
66 datatype type_sig = |
|
67 TySg of {classes: class list, |
|
68 default: sort, |
|
69 subclass: (class * class list) list, |
|
70 args: (string * int) list, |
|
71 coreg: (string * (class * domain) list) list }; |
|
72 |
|
73 (* classes: a list of all declared classes; |
|
74 default: the default sort attached to all unconstrained TVars |
|
75 occurring in a term to be type-inferred; |
|
76 subclass: association list representation of subclass relationship; |
|
77 (c,cs) is interpreted as "c is a proper subclass of all |
|
78 elemenst of cs". Note that c itself is not a memeber of cs. |
|
79 args: an association list of all declared types with the number of their |
|
80 arguments |
|
81 coreg: a two-fold association list of all type arities; (t,al) means that |
|
82 type constructor t has the arities in al; an element (c,ss) of al |
|
83 represents the arity (ss)c |
|
84 *) |
|
85 |
|
86 |
|
87 val tsig0 = TySg{classes = [], |
|
88 default = [], |
|
89 subclass = [], |
|
90 args = [], |
|
91 coreg = []}; |
|
92 |
|
93 fun undcl_class (s) = error("Class " ^ s ^ " has not been declared"); |
|
94 |
|
95 fun undcl_type(c) = "Undeclared type: " ^ c; |
|
96 fun undcl_type_err(c) = error(undcl_type(c)); |
|
97 |
|
98 |
|
99 (* 'leq' checks the partial order on classes according to the |
|
100 statements in the association list 'a' (i.e.'subclass') |
|
101 *) |
|
102 |
|
103 fun less a (C,D) = case assoc (a,C) of |
|
104 Some(ss) => D mem ss |
|
105 | None => undcl_class (C) ; |
|
106 |
|
107 fun leq a (C,D) = C = D orelse less a (C,D); |
|
108 |
|
109 |
|
110 fun defaultS(TySg{default,...}) = default; |
|
111 |
|
112 (* 'logical_type' checks if some type declaration t has as range |
|
113 a class which is a subclass of "logic" *) |
|
114 |
|
115 fun logical_type(tsig as TySg{subclass,coreg,...}) t = |
|
116 let fun is_log C = leq subclass (C,"logic") |
|
117 in case assoc (coreg,t) of |
|
118 Some(ars) => exists (is_log o #1) ars |
|
119 | None => undcl_type_err(t) |
|
120 end; |
|
121 |
|
122 |
|
123 (* 'sortorder' checks the ordering on sets of classes,i.e. on sorts: |
|
124 S1 <= S2 ,iff for every class C2 in S2 there exists a class C1 in S1 |
|
125 with C1 <= C2 (according to an association list 'a') |
|
126 *) |
|
127 |
|
128 fun sortorder a (S1,S2) = |
|
129 forall (fn C2 => exists (fn C1 => leq a (C1,C2)) S1) S2; |
|
130 |
|
131 |
|
132 (* 'inj' inserts a new class C into a given class set S (i.e.sort) only if |
|
133 there exists no class in S which is <= C; |
|
134 the resulting set is minimal if S was minimal |
|
135 *) |
|
136 |
|
137 fun inj a (C,S) = |
|
138 let fun inj1 [] = [C] |
|
139 | inj1 (D::T) = if leq a (D,C) then D::T |
|
140 else if leq a (C,D) then inj1 T |
|
141 else D::(inj1 T) |
|
142 in inj1 S end; |
|
143 |
|
144 |
|
145 (* 'union_sort' forms the minimal union set of two sorts S1 and S2 |
|
146 under the assumption that S2 is minimal *) |
|
147 |
|
148 fun union_sort a = foldr (inj a); |
|
149 |
|
150 |
|
151 (* 'elementwise_union' forms elementwise the minimal union set of two |
|
152 sort lists under the assumption that the two lists have the same length |
|
153 *) |
|
154 |
|
155 fun elementwise_union a (Ss1,Ss2) = map (union_sort a) (Ss1~~Ss2); |
|
156 |
|
157 |
|
158 (* 'lew' checks for two sort lists the ordering for all corresponding list |
|
159 elements (i.e. sorts) *) |
|
160 |
|
161 fun lew a (w1,w2) = forall (sortorder a) (w1~~w2); |
|
162 |
|
163 |
|
164 (* 'is_min' checks if a class C is minimal in a given sort S under the |
|
165 assumption that S contains C *) |
|
166 |
|
167 fun is_min a S C = not (exists (fn (D) => less a (D,C)) S); |
|
168 |
|
169 |
|
170 (* 'min_sort' reduces a sort to its minimal classes *) |
|
171 |
|
172 fun min_sort a S = distinct(filter (is_min a S) S); |
|
173 |
|
174 |
|
175 (* 'min_domain' minimizes the domain sorts of type declarationsl; |
|
176 the function will be applied on the type declarations in extensions *) |
|
177 |
|
178 fun min_domain subclass = |
|
179 let fun one_min (f,(doms,ran)) = (f, (map (min_sort subclass) doms, ran)) |
|
180 in map one_min end; |
|
181 |
|
182 |
|
183 (* 'min_filter' filters a list 'ars' consisting of arities (domain * class) |
|
184 and gives back a list of those range classes whose domains meet the |
|
185 predicate 'pred' *) |
|
186 |
|
187 fun min_filter a pred ars = |
|
188 let fun filt ([],l) = l |
|
189 | filt ((c,x)::xs,l) = if pred(x) then filt (xs,inj a (c,l)) |
|
190 else filt (xs,l) |
|
191 in filt (ars,[]) end; |
|
192 |
|
193 |
|
194 (* 'cod_above' filters all arities whose domains are elementwise >= than |
|
195 a given domain 'w' and gives back a list of the corresponding range |
|
196 classes *) |
|
197 |
|
198 fun cod_above (a,w,ars) = min_filter a (fn w' => lew a (w,w')) ars; |
|
199 |
|
200 |
|
201 (* 'least_sort' returns for a given type its maximum sort: |
|
202 - type variables, free types: the sort brought with |
|
203 - type constructors: recursive determination of the maximum sort of the |
|
204 arguments if the type is declared in 'coreg' of the |
|
205 given type signature *) |
|
206 |
|
207 fun least_sort (tsig as TySg{subclass,coreg,...}) = |
|
208 let fun ls(T as Type(a,Ts)) = |
|
209 let val ars = case assoc (coreg,a) of Some(ars) => ars |
|
210 | None => raise TYPE(undcl_type a,[T],[]); |
|
211 in cod_above(subclass,map ls Ts,ars) end |
|
212 | ls(TFree(a,S)) = S |
|
213 | ls(TVar(a,S)) = S |
|
214 in ls end; |
|
215 |
|
216 |
|
217 fun check_has_sort(tsig as TySg{subclass,coreg,...},T,S) = |
|
218 if sortorder subclass ((least_sort tsig T),S) then () |
|
219 else raise TYPE("Type not of sort " ^ (str_of_sort S),[T],[]) |
|
220 |
|
221 |
|
222 (*Instantiation of type variables in types *) |
|
223 fun inst_typ_tvars(tsig,tye) = |
|
224 let fun inst(Type(a,Ts)) = Type(a, map inst Ts) |
|
225 | inst(T as TFree _) = T |
|
226 | inst(T as TVar(v,S)) = (case assoc(tye,v) of |
|
227 None => T | Some(U) => (check_has_sort(tsig,U,S); U)) |
|
228 in inst end; |
|
229 |
|
230 (*Instantiation of type variables in terms *) |
|
231 fun inst_term_tvars(tsig,tye) = map_term_types (inst_typ_tvars(tsig,tye)); |
|
232 |
|
233 exception TYPE_MATCH; |
|
234 |
|
235 (* Typ matching |
|
236 typ_match(ts,s,(U,T)) = s' <=> s'(U)=T and s' is an extension of s *) |
|
237 fun typ_match tsig = |
|
238 let fun tm(subs, (TVar(v,S), T)) = (case assoc(subs,v) of |
|
239 None => ( (v, (check_has_sort(tsig,T,S); T))::subs |
|
240 handle TYPE _ => raise TYPE_MATCH ) |
|
241 | Some(U) => if U=T then subs else raise TYPE_MATCH) |
|
242 | tm(subs, (Type(a,Ts), Type(b,Us))) = |
|
243 if a<>b then raise TYPE_MATCH |
|
244 else foldl tm (subs, Ts~~Us) |
|
245 | tm(subs, (TFree(x), TFree(y))) = |
|
246 if x=y then subs else raise TYPE_MATCH |
|
247 | tm _ = raise TYPE_MATCH |
|
248 in tm end; |
|
249 |
|
250 fun typ_instance(tsig,T,U) = let val x = typ_match tsig ([],(U,T)) in true end |
|
251 handle TYPE_MATCH => false; |
|
252 |
|
253 |
|
254 (* EXTENDING AND MERGIN TYPE SIGNATURES *) |
|
255 |
|
256 fun not_ident(s) = error("Must be an identifier: " ^ s); |
|
257 |
|
258 fun twice(a) = error("Type constructor " ^a^ " has already been declared."); |
|
259 |
|
260 (*Is the type valid? Accumulates error messages in "errs".*) |
|
261 fun type_errors (tsig as TySg{classes,subclass,args,...}, |
|
262 string_of_typ) (T,errs) = |
|
263 let fun class_err([],errs) = errs |
|
264 | class_err(S::Ss,errs) = |
|
265 if S mem classes then class_err (Ss,errs) |
|
266 else class_err (Ss,("Class " ^ S ^ " has not been declared") :: errs) |
|
267 fun errors(Type(c,Us), errs) = |
|
268 let val errs' = foldr errors (Us,errs) |
|
269 in case assoc(args,c) of |
|
270 None => (undcl_type c) :: errs |
|
271 | Some(n) => if n=length(Us) then errs' |
|
272 else ("Wrong number of arguments: " ^ c) :: errs |
|
273 end |
|
274 | errors(TFree(_,S), errs) = class_err(S,errs) |
|
275 | errors(TVar(_,S), errs) = class_err(S,errs); |
|
276 in case errors(T,[]) of |
|
277 [] => ((least_sort tsig T; errs) |
|
278 handle TYPE(_,[U],_) => ("Ill-formed type: " ^ string_of_typ U) |
|
279 :: errs) |
|
280 | errs' => errs'@errs |
|
281 end; |
|
282 |
|
283 |
|
284 (* 'add_class' adds a new class to the list of all existing classes *) |
|
285 |
|
286 fun add_class (classes,(s,_)) = |
|
287 if s mem classes then error("Class " ^ s ^ " declared twice.") |
|
288 else s::classes; |
|
289 |
|
290 (* 'add_subclass' adds a tuple consisiting of a new class (the new class |
|
291 has already been inserted into the 'classes' list) and its |
|
292 superclasses (they must be declared in 'classes' too) to the 'subclass' |
|
293 list of the given type signature; |
|
294 furthermore all inherited superclasses according to the superclasses |
|
295 brought with are inserted and there is a check that there are no |
|
296 cycles (i.e. C <= D <= C, with C <> D); *) |
|
297 |
|
298 fun add_subclass classes (subclass,(s,ges)) = |
|
299 let fun upd (subclass,s') = if s' mem classes then |
|
300 let val Some(ges') = assoc (subclass,s) |
|
301 in case assoc (subclass,s') of |
|
302 Some(sups) => if s mem sups |
|
303 then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s ) |
|
304 else overwrite (subclass,(s,sups union ges')) |
|
305 | None => subclass |
|
306 end |
|
307 else undcl_class(s') |
|
308 in foldl upd (subclass@[(s,ges)],ges) end; |
|
309 |
|
310 |
|
311 (* 'extend_classes' inserts all new classes into the corresponding |
|
312 lists ('classes','subclass') if possible *) |
|
313 |
|
314 fun extend_classes (classes,subclass,newclasses) = |
|
315 if newclasses = [] then (classes,subclass) else |
|
316 let val classes' = foldl add_class (classes,newclasses); |
|
317 val subclass' = foldl (add_subclass classes') (subclass,newclasses); |
|
318 in (classes',subclass') end; |
|
319 |
|
320 (* Corregularity *) |
|
321 |
|
322 (* 'is_unique_decl' checks if there exists just one declaration t:(Ss)C *) |
|
323 |
|
324 fun is_unique_decl coreg (t,(s,w)) = case assoc2 (coreg,(t,s)) of |
|
325 Some(w1) => if w = w1 then () else |
|
326 error("There are two declarations\n" ^ |
|
327 str_of_decl(t,w,s) ^ " and\n" ^ |
|
328 str_of_decl(t,w1,s) ^ "\n" ^ |
|
329 "with the same result class.") |
|
330 | None => (); |
|
331 |
|
332 (* 'restr2' checks if there are two declarations t:(Ss1)C1 and t:(Ss2)C2 |
|
333 such that C1 >= C2 then Ss1 >= Ss2 (elementwise) *) |
|
334 |
|
335 fun subs (classes,subclass) C = |
|
336 let fun sub (rl,l) = if leq subclass (l,C) then l::rl else rl |
|
337 in foldl sub ([],classes) end; |
|
338 |
|
339 fun coreg_err(t,(w1,C),(w2,D)) = |
|
340 error("Declarations " ^ str_of_decl(t,w1,C) ^ " and " |
|
341 ^ str_of_decl(t,w2,D) ^ " are in conflict"); |
|
342 |
|
343 fun restr2 classes (subclass,coreg) (t,(s,w)) = |
|
344 let fun restr ([],test) = () |
|
345 | restr (s1::Ss,test) = (case assoc2 (coreg,(t,s1)) of |
|
346 Some (dom) => if lew subclass (test (w,dom)) then restr (Ss,test) |
|
347 else coreg_err (t,(w,s),(dom,s1)) |
|
348 | None => restr (Ss,test)) |
|
349 fun forward (t,(s,w)) = |
|
350 let val s_sups = case assoc (subclass,s) of |
|
351 Some(s_sups) => s_sups | None => undcl_class(s); |
|
352 in restr (s_sups,I) end |
|
353 fun backward (t,(s,w)) = |
|
354 let val s_subs = subs (classes,subclass) s |
|
355 in restr (s_subs,fn (x,y) => (y,x)) end |
|
356 in (backward (t,(s,w)); forward (t,(s,w))) end; |
|
357 |
|
358 |
|
359 fun varying_decls(t) = |
|
360 error("Type constructor "^t^" has varying number of arguments."); |
|
361 |
|
362 |
|
363 |
|
364 (* 'coregular' checks |
|
365 - the two restriction conditions 'is_unique_decl' and 'restr2' |
|
366 - if the classes in the new type declarations are known in the |
|
367 given type signature |
|
368 - if one type constructor has always the same number of arguments; |
|
369 if one type declaration has passed all checks it is inserted into |
|
370 the 'coreg' association list of the given type signatrure *) |
|
371 |
|
372 fun coregular (classes,subclass,args) = |
|
373 let fun ex C = if C mem classes then () else undcl_class(C); |
|
374 |
|
375 fun addar(w,C) (coreg,t) = case assoc(args,t) of |
|
376 Some(n) => if n <> length w then varying_decls(t) else |
|
377 (is_unique_decl coreg (t,(C,w)); |
|
378 (seq o seq) ex w; |
|
379 restr2 classes (subclass,coreg) (t,(C,w)); |
|
380 let val Some(ars) = assoc(coreg,t) |
|
381 in overwrite(coreg,(t,(C,w) ins ars)) end) |
|
382 | None => undcl_type_err(t); |
|
383 |
|
384 fun addts(coreg,(ts,ar)) = foldl (addar ar) (coreg,ts) |
|
385 |
|
386 in addts end; |
|
387 |
|
388 |
|
389 (* 'close' extends the 'coreg' association list after all new type |
|
390 declarations have been inserted successfully: |
|
391 for every declaration t:(Ss)C , for all classses D with C <= D: |
|
392 if there is no declaration t:(Ss')C' with C < C' and C' <= D |
|
393 then insert the declaration t:(Ss)D into 'coreg' |
|
394 this means, if there exists a declaration t:(Ss)C and there is |
|
395 no declaration t:(Ss')D with C <=D then the declaration holds |
|
396 for all range classes more general than C *) |
|
397 |
|
398 fun close (coreg,subclass) = |
|
399 let fun check sl (l,(s,dom)) = case assoc (subclass,s) of |
|
400 Some(sups) => |
|
401 let fun close_sup (l,sup) = |
|
402 if exists (fn s'' => less subclass (s,s'') andalso |
|
403 leq subclass (s'',sup)) sl |
|
404 then l |
|
405 else (sup,dom)::l |
|
406 in foldl close_sup (l,sups) end |
|
407 | None => l; |
|
408 fun ext (s,l) = (s, foldl (check (map #1 l)) (l,l)); |
|
409 in map ext coreg end; |
|
410 |
|
411 fun add_types(ac,(ts,n)) = |
|
412 let fun add_type((args,coreg),t) = case assoc(args,t) of |
|
413 Some _ => twice(t) | None => ((t,n)::args,(t,[])::coreg) |
|
414 in if n<0 |
|
415 then error("Type constructor cannot have negative number of arguments") |
|
416 else foldl add_type (ac,ts) |
|
417 end; |
|
418 |
|
419 (* 'extend' takes the above described check- and extend-functions to |
|
420 extend a given type signature with new classes and new type declarations *) |
|
421 |
|
422 fun extend (TySg{classes,default,subclass,args,coreg}, |
|
423 newclasses,newdefault,types,arities) = |
|
424 let val (classes',subclass') = extend_classes(classes,subclass,newclasses); |
|
425 val (args',coreg') = foldl add_types ((args,coreg),types); |
|
426 val old_coreg = map #1 coreg; |
|
427 fun is_old(c) = if c mem old_coreg then () else undcl_type_err(c); |
|
428 fun is_new(c) = if c mem old_coreg then twice(c) else (); |
|
429 val coreg'' = foldl (coregular (classes',subclass',args')) |
|
430 (coreg',min_domain subclass' arities); |
|
431 val coreg''' = close (coreg'',subclass'); |
|
432 val default' = if null newdefault then default else newdefault; |
|
433 in TySg{classes=classes', default=default',subclass=subclass', args=args', |
|
434 coreg=coreg'''} end; |
|
435 |
|
436 |
|
437 (* 'assoc_union' merges two association lists if the contents associated |
|
438 the keys are lists *) |
|
439 |
|
440 fun assoc_union (as1,[]) = as1 |
|
441 | assoc_union (as1,(key,l2)::as2) = case assoc (as1,key) of |
|
442 Some(l1) => assoc_union (overwrite(as1,(key,l1 union l2)),as2) |
|
443 | None => assoc_union ((key,l2)::as1,as2); |
|
444 |
|
445 |
|
446 fun trcl r = |
|
447 let val r' = transitive_closure r |
|
448 in if exists (op mem) r' then error("Cyclic class structure!") else r' end; |
|
449 |
|
450 |
|
451 (* 'merge_coreg' builds the union of two 'coreg' lists; |
|
452 it only checks the two restriction conditions and inserts afterwards |
|
453 all elements of the second list into the first one *) |
|
454 |
|
455 fun merge_coreg classes subclass1 = |
|
456 let fun test_ar classes (t,ars1) (coreg1,(s,w)) = |
|
457 (is_unique_decl coreg1 (t,(s,w)); |
|
458 restr2 classes (subclass1,coreg1) (t,(s,w)); |
|
459 overwrite (coreg1,(t,(s,w) ins ars1))); |
|
460 |
|
461 fun merge_c (coreg1,(c as (t,ars2))) = case assoc (coreg1,t) of |
|
462 Some(ars1) => foldl (test_ar classes (t,ars1)) (coreg1,ars2) |
|
463 | None => c::coreg1 |
|
464 in foldl merge_c end; |
|
465 |
|
466 fun merge_args(args,(t,n)) = case assoc(args,t) of |
|
467 Some(m) => if m=n then args else varying_decls(t) |
|
468 | None => (t,n)::args; |
|
469 |
|
470 (* 'merge' takes the above declared functions to merge two type signatures *) |
|
471 |
|
472 fun merge(TySg{classes=classes1,default=default1,subclass=subclass1,args=args1, |
|
473 coreg=coreg1}, |
|
474 TySg{classes=classes2,default=default2,subclass=subclass2,args=args2, |
|
475 coreg=coreg2}) = |
|
476 let val classes' = classes1 union classes2; |
|
477 val subclass' = trcl (assoc_union (subclass1,subclass2)); |
|
478 val args' = foldl merge_args (args1,args2) |
|
479 val coreg' = merge_coreg classes' subclass' (coreg1,coreg2); |
|
480 val default' = min_sort subclass' (default1 @ default2) |
|
481 in TySg{classes=classes' , default=default',subclass=subclass', args=args', |
|
482 coreg=coreg'} |
|
483 end; |
|
484 |
|
485 (**** TYPE INFERENCE ****) |
|
486 |
|
487 (* |
|
488 |
|
489 Input: |
|
490 - a 'raw' term which contains only dummy types and some explicit type |
|
491 constraints encoded as terms. |
|
492 - the expected type of the term. |
|
493 |
|
494 Output: |
|
495 - the correctly typed term |
|
496 - the substitution needed to unify the actual type of the term with its |
|
497 expected type; only the TVars in the expected type are included. |
|
498 |
|
499 During type inference all TVars in the term have negative index. This keeps |
|
500 them apart from normal TVars, which is essential, because at the end the type |
|
501 of the term is unified with the expected type, which contains normal TVars. |
|
502 |
|
503 1. Add initial type information to the term (add_types). |
|
504 This freezes (freeze_vars) TVars in explicitly provided types (eg |
|
505 constraints or defaults) by turning them into TFrees. |
|
506 2. Carry out type inference, possibly introducing new negative TVars. |
|
507 3. Unify actual and expected type. |
|
508 4. Turn all (negative) TVars into unique new TFrees (freeze). |
|
509 5. Thaw all TVars frozen in step 1 (thaw_vars). |
|
510 |
|
511 *) |
|
512 |
|
513 (*Raised if types are not unifiable*) |
|
514 exception TUNIFY; |
|
515 |
|
516 val tyvar_count = ref(~1); |
|
517 |
|
518 fun tyinit() = (tyvar_count := ~1); |
|
519 |
|
520 fun new_tvar_inx() = (tyvar_count := !tyvar_count-1; !tyvar_count) |
|
521 |
|
522 (* |
|
523 Generate new TVar. Index is < ~1 to distinguish it from TVars generated from |
|
524 variable names (see id_type). Name is arbitrary because index is new. |
|
525 *) |
|
526 |
|
527 fun gen_tyvar(S) = TVar(("'a", new_tvar_inx()),S); |
|
528 fun new_id_type(a) = TVar(("'"^a, new_tvar_inx()),[]); |
|
529 |
|
530 (*Occurs check: type variable occurs in type?*) |
|
531 fun occ v tye = |
|
532 let fun occ(Type(_,Ts)) = exists occ Ts |
|
533 | occ(TFree _) = false |
|
534 | occ(TVar(w,_)) = v=w orelse |
|
535 (case assoc(tye,w) of |
|
536 None => false |
|
537 | Some U => occ U); |
|
538 in occ end; |
|
539 |
|
540 (*Chase variable assignments in tye. |
|
541 If devar (T,tye) returns a type var then it must be unassigned.*) |
|
542 fun devar (T as TVar(v,_), tye) = (case assoc(tye,v) of |
|
543 Some U => devar (U,tye) |
|
544 | None => T) |
|
545 | devar (T,tye) = T; |
|
546 |
|
547 |
|
548 (* 'dom' returns for a type constructor t the list of those domains |
|
549 which deliver a given range class C *) |
|
550 |
|
551 fun dom coreg t C = case assoc2 (coreg, (t,C)) of |
|
552 Some(Ss) => Ss |
|
553 | None => raise TUNIFY; |
|
554 |
|
555 |
|
556 (* 'Dom' returns the union of all domain lists of 'dom' for a given sort S |
|
557 (i.e. a set of range classes ); the union is carried out elementwise |
|
558 for the seperate sorts in the domains *) |
|
559 |
|
560 fun Dom (subclass,coreg) (t,S) = |
|
561 let val domlist = map (dom coreg t) S; |
|
562 in if null domlist then [] |
|
563 else foldl (elementwise_union subclass) (hd domlist,tl domlist) |
|
564 end; |
|
565 |
|
566 |
|
567 fun W ((T,S),tsig as TySg{subclass,coreg,...},tye) = |
|
568 let fun Wd ((T,S),tye) = W ((devar (T,tye),S),tsig,tye) |
|
569 fun Wk(T as TVar(v,S')) = |
|
570 if sortorder subclass (S',S) then tye |
|
571 else (v,gen_tyvar(union_sort subclass (S',S)))::tye |
|
572 | Wk(T as TFree(v,S')) = if sortorder subclass (S',S) then tye |
|
573 else raise TUNIFY |
|
574 | Wk(T as Type(f,Ts)) = |
|
575 if null S then tye |
|
576 else foldr Wd (Ts~~(Dom (subclass,coreg) (f,S)) ,tye) |
|
577 in Wk(T) end; |
|
578 |
|
579 |
|
580 (* Order-sorted Unification of Types (U) *) |
|
581 |
|
582 |
|
583 (* Precondition: both types are well-formed w.r.t. type constructor arities *) |
|
584 fun unify (tsig as TySg{subclass,coreg,...}) = |
|
585 let fun unif ((T,U),tye) = |
|
586 case (devar(T,tye), devar(U,tye)) of |
|
587 (T as TVar(v,S1), U as TVar(w,S2)) => |
|
588 if v=w then tye else |
|
589 if sortorder subclass (S1,S2) then (w,T)::tye else |
|
590 if sortorder subclass (S2,S1) then (v,U)::tye |
|
591 else let val nu = gen_tyvar (union_sort subclass (S1,S2)) |
|
592 in (v,nu)::(w,nu)::tye end |
|
593 | (T as TVar(v,S), U) => |
|
594 if occ v tye U then raise TUNIFY else W ((U,S),tsig,(v,U)::tye) |
|
595 | (U, T as TVar (v,S)) => |
|
596 if occ v tye U then raise TUNIFY else W ((U,S),tsig,(v,U)::tye) |
|
597 | (Type(a,Ts),Type(b,Us)) => |
|
598 if a<>b then raise TUNIFY else foldr unif (Ts~~Us,tye) |
|
599 | (T,U) => if T=U then tye else raise TUNIFY |
|
600 in unif end; |
|
601 |
|
602 (*Instantiation of type variables in types*) |
|
603 (*Pre: instantiations obey restrictions! *) |
|
604 fun inst_typ tye = |
|
605 let fun inst(Type(a,Ts)) = Type(a, map inst Ts) |
|
606 | inst(T as TFree _) = T |
|
607 | inst(T as TVar(v,_)) = |
|
608 (case assoc(tye,v) of Some U => inst U | None => T) |
|
609 in inst end; |
|
610 |
|
611 (*Type inference for polymorphic term*) |
|
612 fun infer tsig = |
|
613 let fun inf(Ts, Const (_,T), tye) = (T,tye) |
|
614 | inf(Ts, Free (_,T), tye) = (T,tye) |
|
615 | inf(Ts, Bound i, tye) = ((nth_elem(i,Ts) , tye) |
|
616 handle LIST _=> raise TYPE ("loose bound variable", [], [Bound i])) |
|
617 | inf(Ts, Var (_,T), tye) = (T,tye) |
|
618 | inf(Ts, Abs (_,T,body), tye) = |
|
619 let val (U,tye') = inf(T::Ts, body, tye) in (T-->U, tye') end |
|
620 | inf(Ts, f$u, tye) = |
|
621 let val (U,tyeU) = inf(Ts, u, tye); |
|
622 val (T,tyeT) = inf(Ts, f, tyeU); |
|
623 fun err s = |
|
624 raise TYPE(s, [inst_typ tyeT T, inst_typ tyeT U], [f$u]) |
|
625 in case T of |
|
626 Type("fun",[T1,T2]) => |
|
627 ( (T2, unify tsig ((T1,U), tyeT)) |
|
628 handle TUNIFY => err"type mismatch in application" ) |
|
629 | TVar _ => |
|
630 let val T2 = gen_tyvar([]) |
|
631 in (T2, unify tsig ((T, U-->T2), tyeT)) |
|
632 handle TUNIFY => err"type mismatch in application" |
|
633 end |
|
634 | _ => err"rator must have function type" |
|
635 end |
|
636 in inf end; |
|
637 |
|
638 fun freeze_vars(Type(a,Ts)) = Type(a,map freeze_vars Ts) |
|
639 | freeze_vars(T as TFree _) = T |
|
640 | freeze_vars(TVar(v,S)) = TFree(Syntax.string_of_vname v, S); |
|
641 |
|
642 (* Attach a type to a constant *) |
|
643 fun type_const (a,T) = Const(a, incr_tvar (new_tvar_inx()) T); |
|
644 |
|
645 (*Find type of ident. If not in table then use ident's name for tyvar |
|
646 to get consistent typing.*) |
|
647 fun type_of_ixn(types,ixn as (a,_)) = |
|
648 case types ixn of Some T => freeze_vars T | None => TVar(("'"^a,~1),[]); |
|
649 |
|
650 fun constrain(term,T) = Const(Syntax.constrainC,T-->T) $ term; |
|
651 fun constrainAbs(Abs(a,_,body),T) = Abs(a,T,body); |
|
652 |
|
653 (* |
|
654 |
|
655 Attach types to a term. Input is a "parse tree" containing dummy types. |
|
656 Type constraints are translated and checked for validity wrt tsig. |
|
657 TVars in constraints are frozen. |
|
658 |
|
659 The atoms in the resulting term satisfy the following spec: |
|
660 |
|
661 Const(a,T): |
|
662 T is a renamed copy of the generic type of a; renaming decreases index of |
|
663 all TVars by new_tvar_inx(), which is less than ~1. The index of all TVars |
|
664 in the generic type must be 0 for this to work! |
|
665 |
|
666 Free(a,T), Var(ixn,T): |
|
667 T is either the frozen default type of a or TVar(("'"^a,~1),[]) |
|
668 |
|
669 Abs(a,T,_): |
|
670 T is either a type constraint or TVar(("'"^a,i),[]), where i is generated |
|
671 by new_tvar_inx(). Thus different abstractions can have the bound variables |
|
672 of the same name but different types. |
|
673 |
|
674 *) |
|
675 |
|
676 fun add_types (tsig, const_tab, types, sorts, string_of_typ) = |
|
677 let val S0 = defaultS tsig; |
|
678 fun defS0 ixn = case sorts ixn of Some S => S | None => S0; |
|
679 fun prepareT(typ) = |
|
680 let val T = Syntax.typ_of_term defS0 typ; |
|
681 val T' = freeze_vars T |
|
682 in case type_errors (tsig,string_of_typ) (T,[]) of |
|
683 [] => T' |
|
684 | errs => raise TYPE(cat_lines errs,[T],[]) |
|
685 end |
|
686 fun add (Const(a,_)) = |
|
687 (case Symtab.lookup(const_tab, a) of |
|
688 Some T => type_const(a,T) |
|
689 | None => raise TYPE ("No such constant: "^a, [], [])) |
|
690 | add (Bound i) = Bound i |
|
691 | add (Free(a,_)) = |
|
692 (case Symtab.lookup(const_tab, a) of |
|
693 Some T => type_const(a,T) |
|
694 | None => Free(a, type_of_ixn(types,(a,~1)))) |
|
695 | add (Var(ixn,_)) = Var(ixn, type_of_ixn(types,ixn)) |
|
696 | add (Abs(a,_,body)) = Abs(a, new_id_type a, add body) |
|
697 | add ((f as Const(a,_)$t1)$t2) = |
|
698 if a=Syntax.constrainC then constrain(add t1,prepareT t2) else |
|
699 if a=Syntax.constrainAbsC then constrainAbs(add t1,prepareT t2) |
|
700 else add f $ add t2 |
|
701 | add (f$t) = add f $ add t |
|
702 in add end; |
|
703 |
|
704 |
|
705 (* Post-Processing *) |
|
706 |
|
707 |
|
708 (*Instantiation of type variables in terms*) |
|
709 fun inst_types tye = map_term_types (inst_typ tye); |
|
710 |
|
711 (*Delete explicit constraints -- occurrences of "_constrain" *) |
|
712 fun unconstrain (Abs(a,T,t)) = Abs(a, T, unconstrain t) |
|
713 | unconstrain ((f as Const(a,_)) $ t) = |
|
714 if a=Syntax.constrainC then unconstrain t |
|
715 else unconstrain f $ unconstrain t |
|
716 | unconstrain (f$t) = unconstrain f $ unconstrain t |
|
717 | unconstrain (t) = t; |
|
718 |
|
719 |
|
720 (* Turn all TVars which satisfy p into new TFrees *) |
|
721 fun freeze p t = |
|
722 let val fs = add_term_tfree_names(t,[]); |
|
723 val inxs = filter p (add_term_tvar_ixns(t,[])); |
|
724 val vmap = inxs ~~ variantlist(map #1 inxs, fs); |
|
725 fun free(Type(a,Ts)) = Type(a, map free Ts) |
|
726 | free(T as TVar(v,S)) = |
|
727 (case assoc(vmap,v) of None => T | Some(a) => TFree(a,S)) |
|
728 | free(T as TFree _) = T |
|
729 in map_term_types free t end; |
|
730 |
|
731 (* Thaw all TVars that were frozen in freeze_vars *) |
|
732 fun thaw_vars(Type(a,Ts)) = Type(a, map thaw_vars Ts) |
|
733 | thaw_vars(T as TFree(a,S)) = (case explode a of |
|
734 "?"::"'"::vn => let val ((b,i),_) = Syntax.scan_varname vn |
|
735 in TVar(("'"^b,i),S) end |
|
736 | _ => T) |
|
737 | thaw_vars(T) = T; |
|
738 |
|
739 |
|
740 fun restrict tye = |
|
741 let fun clean(tye1, ((a,i),T)) = |
|
742 if i < 0 then tye1 else ((a,i),inst_typ tye T) :: tye1 |
|
743 in foldl clean ([],tye) end |
|
744 |
|
745 |
|
746 (*Infer types for term t using tables. Check that t's type and T unify *) |
|
747 |
|
748 fun infer_term (tsig, const_tab, types, sorts, string_of_typ, T, t) = |
|
749 let val u = add_types (tsig, const_tab, types, sorts, string_of_typ) t; |
|
750 val (U,tye) = infer tsig ([], u, []); |
|
751 val uu = unconstrain u; |
|
752 val tye' = unify tsig ((T,U),tye) handle TUNIFY => raise TYPE |
|
753 ("Term does not have expected type", [T, U], [inst_types tye uu]) |
|
754 val Ttye = restrict tye' (* restriction to TVars in T *) |
|
755 val all = Const("", Type("", map snd Ttye)) $ (inst_types tye' uu) |
|
756 (* all is a dummy term which contains all exported TVars *) |
|
757 val Const(_,Type(_,Ts)) $ u'' = |
|
758 map_term_types thaw_vars (freeze (fn (_,i) => i<0) all) |
|
759 (* turn all internally generated TVars into TFrees |
|
760 and thaw all initially frozen TVars *) |
|
761 in (u'', (map fst Ttye) ~~ Ts) end; |
|
762 |
|
763 fun infer_types args = (tyinit(); infer_term args); |
|
764 |
|
765 |
|
766 (* Turn TFrees into TVars to allow types & axioms to be written without "?" *) |
|
767 fun varifyT(Type(a,Ts)) = Type(a,map varifyT Ts) |
|
768 | varifyT(TFree(a,S)) = TVar((a,0),S) |
|
769 | varifyT(T) = T; |
|
770 |
|
771 (* Turn TFrees except those in fixed into new TVars *) |
|
772 fun varify(t,fixed) = |
|
773 let val fs = add_term_tfree_names(t,[]) \\ fixed; |
|
774 val ixns = add_term_tvar_ixns(t,[]); |
|
775 val fmap = fs ~~ variantlist(fs, map #1 ixns) |
|
776 fun thaw(Type(a,Ts)) = Type(a, map thaw Ts) |
|
777 | thaw(T as TVar _) = T |
|
778 | thaw(T as TFree(a,S)) = |
|
779 (case assoc(fmap,a) of None => T | Some b => TVar((b,0),S)) |
|
780 in map_term_types thaw t end; |
|
781 |
|
782 |
|
783 end; |