0
|
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;
|