Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] Annotation of /sml/branches/primop-branch-3/compiler/Elaborator/types/unify.sml
ViewVC logotype

Annotation of /sml/branches/primop-branch-3/compiler/Elaborator/types/unify.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2561 - (view) (download)

1 : blume 902 (* Copyright 1997 Bell Laboratories *)
2 :     (* unify.sml *)
3 :    
4 :     signature UNIFY =
5 :     sig
6 :    
7 :     datatype unifyFail
8 :     = CIRC (* circularity *)
9 :     | EQ (* equality type required *)
10 :     | TYC of Types.tycon * Types.tycon (* tycon mismatch *)
11 :     | TYP of Types.ty * Types.ty (* type mismatch *)
12 :     | LIT of Types.tvKind (* literal *)
13 : dbm 2531 | OVLD of Types.ty (* overload scheme *)
14 : blume 902 | UBVE of Types.tvKind (* UBOUND, equality mismatch *)
15 :     | UBV of Types.tvKind (* UBOUND match *)
16 :     | SCH (* SCHEME, equality mismatch *)
17 :     | REC (* record labels *)
18 :    
19 :     exception Unify of unifyFail
20 :     val failMessage: unifyFail -> string
21 :    
22 :     val unifyTy : Types.ty * Types.ty -> unit
23 :    
24 :     val debugging : bool ref
25 :    
26 :     end (* signature UNIFY *)
27 :    
28 :    
29 :     structure Unify: UNIFY =
30 :     struct
31 :    
32 :     (*** type unification ***)
33 : dbm 2456 val debugging = ElabControl.unidebugging
34 : blume 902
35 :     local
36 :     structure T = Types
37 :     structure TU = TypesUtil
38 :     structure OLL = OverloadLit
39 :     structure ED = ElabDebug
40 :     open Types
41 :    
42 :     (* debugging *)
43 :     val say = Control_Print.say
44 :     fun debugmsg (msg: string) = if !debugging then (say msg; say "\n") else ()
45 :    
46 :     fun bug msg = ErrorMsg.impossible("Unify: "^msg)
47 :    
48 :     val ppType = PPType.ppType StaticEnv.empty
49 :     fun debugPPType (msg,ty) =
50 :     ED.debugPrint debugging (msg, ppType, ty)
51 :    
52 :     in
53 :    
54 :     datatype unifyFail
55 :     = CIRC (* circularity *)
56 :     | EQ (* equality type required *)
57 :     | TYC of Types.tycon * Types.tycon (* tycon mismatch *)
58 :     | TYP of Types.ty * Types.ty (* type mismatch *)
59 :     | LIT of Types.tvKind (* literal *)
60 : dbm 2531 | OVLD of Types.ty (* overload scheme *)
61 : blume 902 | UBVE of Types.tvKind (* UBOUND, equality mismatch *)
62 :     | UBV of Types.tvKind (* UBOUND match *)
63 :     | SCH (* SCHEME, equality mismatch *)
64 :     | REC (* record labels *)
65 :    
66 :     fun failMessage failure =
67 :     case failure
68 :     of CIRC => "circularity"
69 :     | EQ => "equality type required"
70 :     | TYC(tyc1,tyc2) => "tycon mismatch"
71 :     | TYP(ty1,ty2) => "type mismatch"
72 :     | LIT(info) => "literal"
73 : dbm 2531 | OVLD(info) => "overload"
74 : blume 902 | UBVE(info) => "UBOUND, equality mismatch"
75 :     | UBV(info) => "UBOUND match"
76 :     | SCH => "SCHEME, equality mismatch"
77 :     | REC => "record labels"
78 :    
79 :    
80 :     exception Unify of unifyFail
81 :    
82 :    
83 :     (*************** misc functions *****************************************)
84 :    
85 :     val eqLabel = Symbol.eq
86 :    
87 :     fun eqLitKind (lk : T.litKind) =
88 :     case lk of (INT | WORD | CHAR | STRING) => true | REAL => false
89 :    
90 :     (*
91 :     * tyconEqprop tycon:
92 :     *
93 :     * This function returns the eqprop of tycon for use in determining
94 :     * when a CONty is an equality type.
95 :     *
96 :     * Note: Calling this function on ERRORtyc produces an impossible
97 :     * because an ERRORtyc should never occur in a CONty and hence an eqprop
98 :     * of one of them should never be needed.
99 :     *
100 : gkuan 2520 * [GK 5/7/07] The above note is not true. See bug271. Since an error
101 :     * was already flagged, it seems harmless to return YES for the eqprop
102 :     * to avoid possibly spurious eqprop related warnings.
103 :     *
104 : blume 902 * Calling this function on a DEFtyc also produces an impossible because
105 :     * the current eqprop scheme is insufficiently expressive to describe
106 :     * the possibilities. (Ex: first argument must be an eq type but not
107 :     * necessarily the second) Because of this, it is currently necessary to
108 :     * expand DEFtyc's before checking for equality types.
109 :     *)
110 :     fun tyconEqprop (GENtyc { eq, ... }) =
111 :     (case !eq of ABS => NO | ep => ep)
112 :     | tyconEqprop (RECORDtyc _) = YES
113 :     | tyconEqprop (DEFtyc _) = bug "tyconEqprop: DEFtyc"
114 : gkuan 2520 | tyconEqprop (ERRORtyc) = YES
115 : blume 902 | tyconEqprop _ = bug "unexpected tycon in tyconEqprop"
116 :    
117 :     (*
118 :     * fieldwise(just1,just2,combine,fields1,fields2):
119 :     *
120 :     * This function merges two sorted lists of (label, type) pairs
121 :     * (sorted by label) into a single sorted list of (label, type) pairs.
122 :     * If (l1,t1) occurs in fields1 but l1 doesn't occur in fields2 then
123 :     * (l1, just1 t1) occurs in the output. Similarly with just2.
124 :     * If (l, t1) occurs in fields1 and (l,t2) in fields2, then
125 :     * (l, combine t1 t2) occurs in the output.
126 :     *)
127 :     fun fieldwise(_,just2,_,[],fields2) = map (fn (n,t) => (n,just2 t)) fields2
128 :     | fieldwise(just1,_,_,fields1,[]) = map (fn (n,t) => (n,just1 t)) fields1
129 :     | fieldwise(just1,just2,combine,((n1,t1)::r1),((n2,t2)::r2)) =
130 :     if eqLabel(n1,n2) then
131 :     (n1,combine(t1,t2))::(fieldwise(just1,just2,combine,r1,r2))
132 :     else if TU.gtLabel(n2,n1) then
133 :     (n1,just1 t1)::(fieldwise(just1,just2,combine,r1,((n2,t2)::r2)))
134 :     else
135 :     (n2,just2 t2)::(fieldwise(just1,just2,combine,((n1,t1)::r1),r2))
136 :    
137 :    
138 :     (*************** adjust function *****************************************)
139 :    
140 :     (* propagate depth and eq while checking for circularities in the
141 :     * type ty that is going to unify with tyvar var *)
142 : gkuan 2459
143 :     (* ASSERT: VARty var <> ty *)
144 : blume 902 fun adjustType (var,depth,eq,ty) =
145 :     let val _ = debugPPType(">>adjustType: ",ty)
146 :     fun iter _ WILDCARDty = ()
147 :     | iter eq (VARty(var' as ref(info))) =
148 :     (case info
149 : gkuan 2459 of INSTANTIATED ty =>
150 :     (debugmsg "adjustType INSTANTIATED";
151 :     iter eq ty)
152 : blume 902 | OPEN{kind=k,depth=d,eq=e} =>
153 :     (* check for circularity, propagage eq and depth *)
154 :     if TU.eqTyvar(var,var')
155 :     then raise Unify CIRC
156 :     else (case k
157 :     of FLEX fields =>
158 :     (* recurse into FLEX field types *)
159 :     app (fn (l,t) => adjustType(var,depth,e,t))
160 :     fields
161 :     | _ => ();
162 :     var' := OPEN{depth=Int.min(depth,d),
163 :     eq=eq orelse e, kind=k})
164 :     | UBOUND{depth=d,eq=e,name} =>
165 :     (* check if eq is compatible and propagate depth *)
166 :     if eq andalso not e
167 :     then raise Unify EQ
168 :     else if depth < d
169 :     then var' := UBOUND{depth=depth,eq=e,name=name}
170 :     else ()
171 :     | SCHEME eq' =>
172 :     if TU.eqTyvar(var,var')
173 :     then raise Unify CIRC
174 :     else if eq andalso not eq'
175 :     then var' := SCHEME eq
176 :     else ()
177 :     | LITERAL{kind=k,...} =>
178 :     (* check if eq is compatible *)
179 :     if eq andalso not(eqLitKind k)
180 :     then raise Unify EQ
181 :     else ()
182 : dbm 2451 | LBOUND _ => bug "unify:adjustType:LBOUND")
183 : gkuan 2459 | iter eq (ty as CONty(DEFtyc{tyfun=TYFUN{body,...},...}, args)) =
184 :     (app (iter eq) args; iter eq (TU.headReduceType ty))
185 :     (* A headReduceType here may cause instTyvar to
186 :     * infinite loop if this CONty has a nonstrict arg
187 :     * against which we are unifying/instantiating
188 : gkuan 2468 * Because we may be instantiating to nonstrict
189 :     * univariables, it is safer to do an occurrence
190 : dbm 2529 * check on all the arguments. (typing/tests/20.sml)
191 : gkuan 2459 * [GK 4/28/07] *)
192 : blume 902 | iter eq (CONty(tycon,args)) =
193 :     (case tyconEqprop tycon
194 :     of OBJ => app (iter false) args
195 :     | YES => app (iter eq) args
196 :     | _ =>
197 :     if eq then raise Unify EQ
198 :     else app (iter false) args)
199 :     (* BUG? why don't these cases blow up (in tyconEqprop) when iter is applied
200 :     to arguments that are unreduced applications of DEFtycs? *)
201 :     | iter _ (POLYty _) = bug "adjustType 1"
202 :     | iter _ (IBOUND _) = bug "adjustType 2"
203 :     | iter _ _ = bug "adjustType 3"
204 : gkuan 2459 in iter eq ty; debugmsg "<<adjustType"
205 : blume 902 end
206 :    
207 :     (*************** unify functions *****************************************)
208 :    
209 :     (* LITERAL can be instantiated to a compatible LITERAL or a monotype of
210 :     * its LITERAL class
211 :     * UBOUND cannot be instantiated, but it's depth property can be reduced
212 :     * FLEX can merge with another FLEX or instantiate a META
213 :     * META can be instantiated to anything
214 :     *)
215 :    
216 :     (* reorder two tyvars in descending order according to the ordering
217 :     * LITERAL > UBOUND > SCHEME > OPEN/FLEX > OPEN/META *)
218 :     fun sortVars(v1 as ref i1, v2 as ref i2) =
219 :     case (i1,i2)
220 :     of (LITERAL _, _) => (v1,v2)
221 :     | (_, LITERAL _) => (v2,v1)
222 :     | (UBOUND _, _) => (v1,v2)
223 :     | (_, UBOUND _)=> (v2,v1)
224 :     | (SCHEME _, _) => (v1,v2)
225 :     | (_, SCHEME _)=> (v2,v1)
226 :     | (OPEN{kind=FLEX _,...}, _) => (v1,v2)
227 :     | (_, OPEN{kind=FLEX _,...})=> (v2,v1)
228 :     | _ => (v1,v2) (* both OPEN/META *)
229 :    
230 : gkuan 2459 (* unifyTy expects that there are no POLYtys with 0-arity
231 :     CONty(DEFtyc, _) are reduced only if absolutely necessary. *)
232 : blume 902 fun unifyTy(type1,type2) =
233 :     let val type1 = TU.prune type1
234 :     val type2 = TU.prune type2
235 :     val _ = debugPPType(">>unifyTy: type1: ",type1)
236 :     val _ = debugPPType(">>unifyTy: type2: ",type2)
237 : dbm 2529 fun unifyRaw(type1, type2) =
238 :     case (type1, type2)
239 : blume 902 of (VARty var1,VARty var2) =>
240 :     unifyTyvars(var1,var2) (* used to take type1 and type2 as args *)
241 : dbm 2529 | (VARty var1, _) => (* type2 may be WILDCARDty *)
242 :     instTyvar(var1,type2)
243 :     | (_, VARty var2) => (* type1 may be WILDCARDty *)
244 :     instTyvar(var2,type1)
245 : blume 902 | (CONty(tycon1,args1),CONty(tycon2,args2)) =>
246 :     if TU.eqTycon(tycon1,tycon2) then
247 : gkuan 2459 (* Because tycons are equal, they must have the
248 :     same arity. Assume that lengths of args1 and
249 :     args2 are the same. Type abbrev. strictness
250 :     optimization. If tycons equal, then only check
251 :     strict arguments. [GK 4/28/07] *)
252 :     (case tycon1
253 :     of DEFtyc{strict, ...} =>
254 :     let fun unifyArgs([],[],[]) = ()
255 :     | unifyArgs(true::ss, ty1::tys1, ty2::tys2) =
256 :     (unifyTy(ty1,ty2); unifyArgs(ss,tys1,tys2))
257 :     | unifyArgs(false::ss, _::tys1, _::tys2) =
258 :     unifyArgs(ss,tys1,tys2)
259 : gkuan 2520 | unifyArgs _ =
260 :     bug "unifyTy: arg ty lists wrong length"
261 : gkuan 2459 in unifyArgs(strict,args1,args2)
262 :     end
263 :     | _ => ListPair.app unifyTy (args1,args2))
264 : blume 902 else raise Unify (TYC(tycon1,tycon2))
265 :     (* if one of the types is WILDCARDty, propagate it down into the
266 :     * other type to eliminate tyvars that might otherwise cause
267 :     * generalizeTy to complain. *)
268 :     | (WILDCARDty, CONty(_, args2)) =>
269 :     (app (fn x => unifyTy(x, WILDCARDty)) args2)
270 :     | (CONty(_, args1), WILDCARDty) =>
271 :     (app (fn x => unifyTy(x, WILDCARDty)) args1)
272 :     | (WILDCARDty,_) => ()
273 :     | (_,WILDCARDty) => ()
274 :     | tys => raise Unify (TYP tys)
275 : dbm 2529 in (* first try unifying without reducing CONty(DEFtycs) *)
276 :     unifyRaw(type1, type2)
277 :     handle Unify _ =>
278 :     (* try head reducing type1 *)
279 :     let val type1' = TU.headReduceType type1
280 :     in unifyRaw(type1', type2)
281 :     handle Unify _ => (* try head reducing type2 *)
282 :     unifyRaw(type1', TU.headReduceType type2)
283 :     (* if unification still fails, then type1 and type2
284 :     really cannot be made to be equal *)
285 :     end
286 : blume 902 end
287 :    
288 :     and unifyTyvars (var1, var2) =
289 :     let fun unify(var1 as ref i1, var2 as ref i2) =
290 :     (* ASSERT: var1 <> var2 *)
291 :     case i1
292 :     of LITERAL{kind,region} =>
293 :     (case i2
294 :     of LITERAL{kind=kind',...} =>
295 :     if kind = kind'
296 :     then var2 := INSTANTIATED (VARty var1)
297 :     else raise Unify (LIT i1)
298 : dbm 2529 | (OPEN{kind=META,eq=e2,...} | SCHEME e2) =>
299 : blume 902 (* check eq compatibility *)
300 :     if not e2 orelse eqLitKind kind
301 :     then var2 := INSTANTIATED (VARty var1)
302 :     else raise Unify (LIT i1)
303 :     | _ => raise Unify (LIT i1))
304 :    
305 :     | UBOUND {depth=d1,eq=e1,name} =>
306 :     (case i2
307 :     of OPEN{kind=META,eq=e2,depth=d2} =>
308 :     if e1 orelse (not e2)
309 :     then (if d2 < d1
310 :     then var1 := UBOUND{depth=d2,eq=e1,name=name}
311 :     else ();
312 :     var2 := INSTANTIATED (VARty var1))
313 :     else raise Unify (UBV i1)
314 :     | _ => raise Unify (UBV i1))
315 :    
316 :     | SCHEME e1 =>
317 :     (case i2
318 :     of SCHEME e2 =>
319 :     if e1 orelse not e2 then var2 := INSTANTIATED (VARty var1)
320 :     else var1 := INSTANTIATED(VARty var2)
321 :     | OPEN{kind=META,eq=e2,depth=d2} =>
322 :     if e1 orelse (not e2)
323 :     then var2 := INSTANTIATED (VARty var1)
324 :     else (var1 := SCHEME e2;
325 :     var2 := INSTANTIATED (VARty var1))
326 :     | _ => raise Unify SCH)
327 :    
328 :     | OPEN{kind=k1 as FLEX f1,depth=d1,eq=e1} =>
329 :     (case i2
330 :     of OPEN{kind=k2,eq=e2,depth=d2} =>
331 :     let val d = Int.min(d1,d2)
332 :     val e = e1 orelse e2
333 :     in case k2
334 :     of FLEX f2 =>
335 :     (app (fn (l,t) => adjustType(var1,d,e,t)) f2;
336 :     app (fn (l,t) => adjustType(var2,d,e,t)) f1;
337 :     var1 :=
338 :     OPEN{depth=d, eq=e,
339 :     kind=FLEX(merge_fields(true,true,f1,f2))};
340 :     var2 := INSTANTIATED(VARty var1))
341 :     | META =>
342 :     (app (fn (l,t) => adjustType(var2,d,e,t)) f1;
343 :     var1 := OPEN{kind=k1,depth=d,eq=e};
344 :     var2 := INSTANTIATED(VARty var1))
345 :     end
346 :     | _ => bug "unifyTyvars 2")
347 :    
348 :     | OPEN{kind=META,depth=d1,eq=e1} =>
349 :     (case i2
350 :     of OPEN{kind=META,depth=d2,eq=e2} =>
351 :     let val d = Int.min(d1,d2)
352 :     val e = e1 orelse e2
353 :     in var1 := OPEN{kind=META,depth=d,eq=e};
354 :     var2 := INSTANTIATED(VARty var1)
355 :     end
356 :     | _ => bug "unifyTyvars 3")
357 :    
358 :     | _ => bug "unifyTyvars 4"
359 : dbm 2529 val _ = debugmsg ">>unifyTyvars"
360 : blume 902 in if TU.eqTyvar(var1,var2) then ()
361 :     else unify(sortVars(var1,var2))
362 :     end
363 :    
364 : dbm 2529 (* instTyvar: tyvar * ty -> unit
365 :     * instTyvar(tv,ty) -- instantiate tyvar tv to type ty.
366 :     * ty is not necessarily head normal form.
367 :     * ASSERT: ty is not a VARty (otherwise unifyTyvars would have been
368 :     * used instead. *)
369 :     and instTyvar (var as ref(OPEN{kind=META,depth,eq}),ty) =
370 :     (case ty
371 : blume 902 of WILDCARDty => ()
372 : dbm 2529 | _ => adjustType(var,depth,eq,ty);
373 : gkuan 2459 debugPPType("instTyvar ", VARty var);
374 :     debugPPType("instTyvar to ", ty);
375 :     (* Also need to check for circularity with ty here *)
376 : blume 902 var := INSTANTIATED ty)
377 :    
378 : dbm 2529 | instTyvar (var as ref(OPEN{kind=FLEX fields,depth,eq}),ty) =
379 : dbm 2531 let val ty' = TU.headReduceType ty (* try to reduce to a record type *)
380 : dbm 2529 in case ty'
381 :     of CONty(RECORDtyc field_names, field_types) =>
382 :     let val record_fields = ListPair.zip (field_names,field_types)
383 :     in app (fn t => adjustType(var,depth,eq,t)) field_types;
384 :     merge_fields(false,true,fields,record_fields);
385 :     var := INSTANTIATED ty
386 :     end
387 :     | WILDCARDty => (* propagate WILDCARDty to the fields *)
388 :     (app (fn (lab,ty) => unifyTy(WILDCARDty,ty)) fields)
389 :     | _ => raise Unify (TYP(VARty(var), ty))
390 :     end
391 : blume 902
392 : dbm 2561 (* special handling of SCHEME tyvar instantiation:
393 :     * ty must reduce to either a tyvar, var', in which case we unify
394 :     * var and var' (in that order!), or
395 :     * ty must reduce to a (basic) constant type, in which case ty
396 :     * does not contain any type variables, and the occurrence check
397 :     * (i.e. adjustType) is not necessary *)
398 : dbm 2529 | instTyvar (var as ref(i as SCHEME eq),ty) =
399 : dbm 2561 (case ty
400 :     of VARty var1 => unifyTyvars(var, var1)
401 :     (* because of asymmetric handling of SCHEME tyvars in
402 :     * unifyTyvars -- here SCHEME must be first arg *)
403 :     | CONty(tyc,nil) => var := INSTANTIATED ty
404 :     | CONty(tyc,_) => (* nonnull arguments *)
405 :     (case TU.nullReduceType ty
406 :     of VARty var1 => unifyTyvars(var, var1)
407 :     | ty' as CONty(tyc,nil) => var := INSTANTIATED ty'
408 :     (* valid potential resolution type. Could check more precisely
409 :     * for membership in the allowed basic types
410 :     * (e.g. int, real, ...) *)
411 :     | WILDCARDty => ()
412 :     | _ => raise Unify(OVLD ty))
413 :     | WILDCARDty => ()
414 :     | _ => bug "instTyvar: SCHEME")
415 : blume 902
416 : dbm 2529 | instTyvar (var as ref(i as LITERAL{kind,...}),ty) =
417 : dbm 2531 (case TU.headReduceType ty
418 : blume 902 of WILDCARDty => ()
419 : dbm 2529 | ty' =>
420 :     if OLL.isLiteralTy(kind,ty')
421 : dbm 2561 then var := INSTANTIATED (TU.nullReduceType ty)
422 : blume 902 else raise Unify (LIT i)) (* could return the ty for error msg*)
423 :    
424 : dbm 2529 | instTyvar (ref(i as UBOUND _),ty) =
425 :     (case ty
426 : blume 902 of WILDCARDty => ()
427 :     | _ => raise Unify (UBV i)) (* could return the ty for error msg*)
428 :    
429 : dbm 2531 | instTyvar (ref(INSTANTIATED _),_) = bug "instTyvar: INSTANTIATED"
430 :     | instTyvar (ref(LBOUND _),_) = bug "instTyvar: LBOUND"
431 : blume 902
432 :     (*
433 :     * merge_fields(extra1,extra2,fields1,fields2):
434 :     *
435 :     * This function merges the 2 sorted field lists. Fields occuring
436 :     * in both lists have their types unified. If a field occurs in only
437 :     * one list, say fields{i} then if extra{i} is true, an Unify error
438 :     * is raised.
439 :     *)
440 :     and merge_fields(extra1,extra2,fields1,fields2) =
441 :     let fun extra allowed t =
442 :     if not allowed
443 :     then raise Unify REC
444 :     else t
445 :     in fieldwise(extra extra1, extra extra2,
446 :     (fn (t1,t2) => (unifyTy(t1,t2); t1)),
447 :     fields1, fields2)
448 :     end
449 :    
450 :     end (* local *)
451 :     end (* structure Unify *)

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0