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/trunk/src/compiler/Semant/types/unify.sml
ViewVC logotype

Annotation of /sml/trunk/src/compiler/Semant/types/unify.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 249 - (view) (download)
Original Path: sml/branches/SMLNJ/src/compiler/Semant/types/unify.sml

1 : monnier 249 (* 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 :     | UBVE of Types.tvKind (* UBOUND, equality mismatch *)
14 :     | UBV of Types.tvKind (* UBOUND match *)
15 :     | SCH (* SCHEME, equality mismatch *)
16 :     | REC (* record labels *)
17 :    
18 :     exception Unify of unifyFail
19 :     val failMessage: unifyFail -> string
20 :    
21 :     val unifyTy : Types.ty * Types.ty -> unit
22 :    
23 :     val debugging : bool ref
24 :    
25 :     end (* signature UNIFY *)
26 :    
27 :    
28 :     structure Unify: UNIFY =
29 :     struct
30 :    
31 :     (*** type unification ***)
32 :     val debugging = ref false
33 :    
34 :     local
35 :     structure T = Types
36 :     structure TU = TypesUtil
37 :     structure OLL = OverloadLit
38 :     structure ED = ElabDebug
39 :     open Types
40 :    
41 :     (* debugging *)
42 :     val say = Control.Print.say
43 :     fun debugmsg (msg: string) = if !debugging then (say msg; say "\n") else ()
44 :    
45 :     fun bug msg = ErrorMsg.impossible("Unify: "^msg)
46 :    
47 :     val ppType = PPType.ppType StaticEnv.empty
48 :     fun debugPPType (msg,ty) =
49 :     ED.debugPrint debugging (msg, ppType, ty)
50 :    
51 :     in
52 :    
53 :     datatype unifyFail
54 :     = CIRC (* circularity *)
55 :     | EQ (* equality type required *)
56 :     | TYC of Types.tycon * Types.tycon (* tycon mismatch *)
57 :     | TYP of Types.ty * Types.ty (* type mismatch *)
58 :     | LIT of Types.tvKind (* literal *)
59 :     | UBVE of Types.tvKind (* UBOUND, equality mismatch *)
60 :     | UBV of Types.tvKind (* UBOUND match *)
61 :     | SCH (* SCHEME, equality mismatch *)
62 :     | REC (* record labels *)
63 :    
64 :     fun failMessage failure =
65 :     case failure
66 :     of CIRC => "circularity"
67 :     | EQ => "equality type required"
68 :     | TYC(tyc1,tyc2) => "tycon mismatch"
69 :     | TYP(ty1,ty2) => "type mismatch"
70 :     | LIT(info) => "literal"
71 :     | UBVE(info) => "UBOUND, equality mismatch"
72 :     | UBV(info) => "UBOUND match"
73 :     | SCH => "SCHEME, equality mismatch"
74 :     | REC => "record labels"
75 :    
76 :    
77 :     exception Unify of unifyFail
78 :    
79 :    
80 :     (*************** misc functions *****************************************)
81 :    
82 :     val eqLabel = Symbol.eq
83 :    
84 :     fun eqLitKind (lk : T.litKind) =
85 :     case lk of (INT | WORD | CHAR | STRING) => true | REAL => false
86 :    
87 :     (*
88 :     * tyconEqprop tycon:
89 :     *
90 :     * This function returns the eqprop of tycon for use in determining
91 :     * when a CONty is an equality type.
92 :     *
93 :     * Note: Calling this function on ERRORtyc produces an impossible
94 :     * because an ERRORtyc should never occur in a CONty and hence an eqprop
95 :     * of one of them should never be needed.
96 :     *
97 :     * Calling this function on a DEFtyc also produces an impossible because
98 :     * the current eqprop scheme is insufficiently expressive to describe
99 :     * the possibilities. (Ex: first argument must be an eq type but not
100 :     * necessarily the second) Because of this, it is currently necessary to
101 :     * expand DEFtyc's before checking for equality types.
102 :     *)
103 :     fun tyconEqprop (GENtyc{eq,...}) =
104 :     (case !eq of ABS => NO | ep => ep)
105 :     | tyconEqprop (RECORDtyc _) = YES
106 :     | tyconEqprop (DEFtyc _) = bug "tyconEqprop: DEFtyc"
107 :     | tyconEqprop (ERRORtyc) = bug "tyconEqprop: ERRORtyc"
108 :     | tyconEqprop _ = bug "unexpected tycon in tyconEqprop"
109 :    
110 :     (*
111 :     * fieldwise(just1,just2,combine,fields1,fields2):
112 :     *
113 :     * This function merges two sorted lists of (label, type) pairs
114 :     * (sorted by label) into a single sorted list of (label, type) pairs.
115 :     * If (l1,t1) occurs in fields1 but l1 doesn't occur in fields2 then
116 :     * (l1, just1 t1) occurs in the output. Similarly with just2.
117 :     * If (l, t1) occurs in fields1 and (l,t2) in fields2, then
118 :     * (l, combine t1 t2) occurs in the output.
119 :     *)
120 :     fun fieldwise(_,just2,_,[],fields2) = map (fn (n,t) => (n,just2 t)) fields2
121 :     | fieldwise(just1,_,_,fields1,[]) = map (fn (n,t) => (n,just1 t)) fields1
122 :     | fieldwise(just1,just2,combine,((n1,t1)::r1),((n2,t2)::r2)) =
123 :     if eqLabel(n1,n2) then
124 :     (n1,combine(t1,t2))::(fieldwise(just1,just2,combine,r1,r2))
125 :     else if TU.gtLabel(n2,n1) then
126 :     (n1,just1 t1)::(fieldwise(just1,just2,combine,r1,((n2,t2)::r2)))
127 :     else
128 :     (n2,just2 t2)::(fieldwise(just1,just2,combine,((n1,t1)::r1),r2))
129 :    
130 :    
131 :     (*************** adjust function *****************************************)
132 :    
133 :     (* propagate depth and eq while checking for circularities in the
134 :     * type ty that is going to unify with tyvar var *)
135 :     fun adjustType (var,depth,eq,ty) =
136 :     let val _ = debugPPType(">>adjustType: ",ty)
137 :     fun iter _ WILDCARDty = ()
138 :     | iter eq (VARty(var' as ref(info))) =
139 :     (case info
140 :     of INSTANTIATED ty => iter eq ty
141 :     | OPEN{kind=k,depth=d,eq=e} =>
142 :     (* check for circularity, propagage eq and depth *)
143 :     if TU.eqTyvar(var,var')
144 :     then raise Unify CIRC
145 :     else (case k
146 :     of FLEX fields =>
147 :     (* recurse into FLEX field types *)
148 :     app (fn (l,t) => adjustType(var,depth,e,t))
149 :     fields
150 :     | _ => ();
151 :     var' := OPEN{depth=Int.min(depth,d),
152 :     eq=eq orelse e, kind=k})
153 :     | UBOUND{depth=d,eq=e,name} =>
154 :     (* check if eq is compatible and propagate depth *)
155 :     if eq andalso not e
156 :     then raise Unify EQ
157 :     else if depth < d
158 :     then var' := UBOUND{depth=depth,eq=e,name=name}
159 :     else ()
160 :     | SCHEME eq' =>
161 :     if TU.eqTyvar(var,var')
162 :     then raise Unify CIRC
163 :     else if eq andalso not eq'
164 :     then var' := SCHEME eq
165 :     else ()
166 :     | LITERAL{kind=k,...} =>
167 :     (* check if eq is compatible *)
168 :     if eq andalso not(eqLitKind k)
169 :     then raise Unify EQ
170 :     else ())
171 :     | iter eq (ty as CONty(DEFtyc _, args)) =
172 :     iter eq (TU.headReduceType ty)
173 :     | iter eq (CONty(tycon,args)) =
174 :     (case tyconEqprop tycon
175 :     of OBJ => app (iter false) args
176 :     | YES => app (iter eq) args
177 :     | _ =>
178 :     if eq then raise Unify EQ
179 :     else app (iter false) args)
180 :     (* BUG? why don't these cases blow up (in tyconEqprop) when iter is applied
181 :     to arguments that are unreduced applications of DEFtycs? *)
182 :     | iter _ (POLYty _) = bug "adjustType 1"
183 :     | iter _ (IBOUND _) = bug "adjustType 2"
184 :     | iter _ _ = bug "adjustType 3"
185 :     in iter eq ty
186 :     end
187 :    
188 :     (*************** unify functions *****************************************)
189 :    
190 :     (* LITERAL can be instantiated to a compatible LITERAL or a monotype of
191 :     * its LITERAL class
192 :     * UBOUND cannot be instantiated, but it's depth property can be reduced
193 :     * FLEX can merge with another FLEX or instantiate a META
194 :     * META can be instantiated to anything
195 :     *)
196 :    
197 :     (* reorder two tyvars in descending order according to the ordering
198 :     * LITERAL > UBOUND > SCHEME > OPEN/FLEX > OPEN/META *)
199 :     fun sortVars(v1 as ref i1, v2 as ref i2) =
200 :     case (i1,i2)
201 :     of (LITERAL _, _) => (v1,v2)
202 :     | (_, LITERAL _) => (v2,v1)
203 :     | (UBOUND _, _) => (v1,v2)
204 :     | (_, UBOUND _)=> (v2,v1)
205 :     | (SCHEME _, _) => (v1,v2)
206 :     | (_, SCHEME _)=> (v2,v1)
207 :     | (OPEN{kind=FLEX _,...}, _) => (v1,v2)
208 :     | (_, OPEN{kind=FLEX _,...})=> (v2,v1)
209 :     | _ => (v1,v2) (* both OPEN/META *)
210 :    
211 :     fun unifyTy(type1,type2) =
212 :     let val type1 = TU.prune type1
213 :     val type2 = TU.prune type2
214 :     val _ = debugPPType(">>unifyTy: type1: ",type1)
215 :     val _ = debugPPType(">>unifyTy: type2: ",type2)
216 :     in case (TU.headReduceType type1, TU.headReduceType type2)
217 :     of (VARty var1,VARty var2) =>
218 :     unifyTyvars(var1,var2) (* used to take type1 and type2 as args *)
219 :     | (VARty var1,etype2) => (* etype2 may be WILDCARDty *)
220 :     instTyvar(var1,type2,etype2)
221 :     | (etype1,VARty var2) => (* etype1 may be WILDCARDty *)
222 :     instTyvar(var2,type1,etype1)
223 :     | (CONty(tycon1,args1),CONty(tycon2,args2)) =>
224 :     if TU.eqTycon(tycon1,tycon2) then
225 :     ListPair.app unifyTy (args1,args2)
226 :     else raise Unify (TYC(tycon1,tycon2))
227 :     (* if one of the types is WILDCARDty, propagate it down into the
228 :     * other type to eliminate tyvars that might otherwise cause
229 :     * generalizeTy to complain. *)
230 :     | (WILDCARDty, CONty(_, args2)) =>
231 :     (app (fn x => unifyTy(x, WILDCARDty)) args2)
232 :     | (CONty(_, args1), WILDCARDty) =>
233 :     (app (fn x => unifyTy(x, WILDCARDty)) args1)
234 :     | (WILDCARDty,_) => ()
235 :     | (_,WILDCARDty) => ()
236 :     | tys => raise Unify (TYP tys)
237 :     end
238 :    
239 :     and unifyTyvars (var1, var2) =
240 :     let fun unify(var1 as ref i1, var2 as ref i2) =
241 :     (* ASSERT: var1 <> var2 *)
242 :     case i1
243 :     of LITERAL{kind,region} =>
244 :     (case i2
245 :     of LITERAL{kind=kind',...} =>
246 :     if kind = kind'
247 :     then var2 := INSTANTIATED (VARty var1)
248 :     else raise Unify (LIT i1)
249 :     | (OPEN{kind=META,eq=e2,...} | SCHEME e2)=>
250 :     (* check eq compatibility *)
251 :     if not e2 orelse eqLitKind kind
252 :     then var2 := INSTANTIATED (VARty var1)
253 :     else raise Unify (LIT i1)
254 :     | _ => raise Unify (LIT i1))
255 :    
256 :     | UBOUND {depth=d1,eq=e1,name} =>
257 :     (case i2
258 :     of OPEN{kind=META,eq=e2,depth=d2} =>
259 :     if e1 orelse (not e2)
260 :     then (if d2 < d1
261 :     then var1 := UBOUND{depth=d2,eq=e1,name=name}
262 :     else ();
263 :     var2 := INSTANTIATED (VARty var1))
264 :     else raise Unify (UBV i1)
265 :     | _ => raise Unify (UBV i1))
266 :    
267 :     | SCHEME e1 =>
268 :     (case i2
269 :     of SCHEME e2 =>
270 :     if e1 orelse not e2 then var2 := INSTANTIATED (VARty var1)
271 :     else var1 := INSTANTIATED(VARty var2)
272 :     | OPEN{kind=META,eq=e2,depth=d2} =>
273 :     if e1 orelse (not e2)
274 :     then var2 := INSTANTIATED (VARty var1)
275 :     else (var1 := SCHEME e2;
276 :     var2 := INSTANTIATED (VARty var1))
277 :     | _ => raise Unify SCH)
278 :    
279 :     | OPEN{kind=k1 as FLEX f1,depth=d1,eq=e1} =>
280 :     (case i2
281 :     of OPEN{kind=k2,eq=e2,depth=d2} =>
282 :     let val d = Int.min(d1,d2)
283 :     val e = e1 orelse e2
284 :     in case k2
285 :     of FLEX f2 =>
286 :     (app (fn (l,t) => adjustType(var1,d,e,t)) f2;
287 :     app (fn (l,t) => adjustType(var2,d,e,t)) f1;
288 :     var1 :=
289 :     OPEN{depth=d, eq=e,
290 :     kind=FLEX(merge_fields(true,true,f1,f2))};
291 :     var2 := INSTANTIATED(VARty var1))
292 :     | META =>
293 :     (app (fn (l,t) => adjustType(var2,d,e,t)) f1;
294 :     var1 := OPEN{kind=k1,depth=d,eq=e};
295 :     var2 := INSTANTIATED(VARty var1))
296 :     end
297 :     | _ => bug "unifyTyvars 2")
298 :    
299 :     | OPEN{kind=META,depth=d1,eq=e1} =>
300 :     (case i2
301 :     of OPEN{kind=META,depth=d2,eq=e2} =>
302 :     let val d = Int.min(d1,d2)
303 :     val e = e1 orelse e2
304 :     in var1 := OPEN{kind=META,depth=d,eq=e};
305 :     var2 := INSTANTIATED(VARty var1)
306 :     end
307 :     | _ => bug "unifyTyvars 3")
308 :    
309 :     | _ => bug "unifyTyvars 4"
310 :     val _ = debugmsg ">>unifyTyvars"
311 :     in if TU.eqTyvar(var1,var2) then ()
312 :     else unify(sortVars(var1,var2))
313 :     end
314 :    
315 :     and instTyvar (var as ref(OPEN{kind=META,depth,eq}),ty,ety) =
316 :     (case ety
317 :     of WILDCARDty => ()
318 :     | _ => adjustType(var,depth,eq,ety);
319 :     var := INSTANTIATED ty)
320 :    
321 :     | instTyvar (var as ref(OPEN{kind=FLEX fields,depth,eq}),ty,ety) =
322 :     (case ety
323 :     of CONty(RECORDtyc field_names, field_types) =>
324 :     let val record_fields = ListPair.zip (field_names,field_types)
325 :     in app (fn t => adjustType(var,depth,eq,t)) field_types;
326 :     merge_fields(false,true,fields,record_fields);
327 :     var := INSTANTIATED ty
328 :     end
329 :     | WILDCARDty => (* propagate WILDCARDty to the fields *)
330 :     (app (fn (lab,ty) => unifyTy(WILDCARDty,ty)) fields)
331 :     | _ => raise Unify (TYP(VARty(var), ety)))
332 :    
333 :     | instTyvar (var as ref(i as SCHEME eq),ty,ety) =
334 :     (adjustType(var,infinity,eq,ety);
335 :     var := INSTANTIATED ty)
336 :    
337 :     | instTyvar (var as ref(i as LITERAL{kind,...}),ty,ety) =
338 :     (case ety
339 :     of WILDCARDty => ()
340 :     | _ =>
341 :     if OLL.isLiteralTy(kind,ety)
342 :     then var := INSTANTIATED ty
343 :     else raise Unify (LIT i)) (* could return the ty for error msg*)
344 :    
345 :     | instTyvar (ref(i as UBOUND _),_,ety) =
346 :     (case ety
347 :     of WILDCARDty => ()
348 :     | _ => raise Unify (UBV i)) (* could return the ty for error msg*)
349 :    
350 :     | instTyvar (ref(INSTANTIATED _),_,_) = bug "instTyvar: INSTANTIATED"
351 :     | instTyvar (ref(LBOUND _),_,_) = bug "instTyvar: LBOUND"
352 :    
353 :     (*
354 :     * merge_fields(extra1,extra2,fields1,fields2):
355 :     *
356 :     * This function merges the 2 sorted field lists. Fields occuring
357 :     * in both lists have their types unified. If a field occurs in only
358 :     * one list, say fields{i} then if extra{i} is true, an Unify error
359 :     * is raised.
360 :     *)
361 :     and merge_fields(extra1,extra2,fields1,fields2) =
362 :     let fun extra allowed t =
363 :     if not allowed
364 :     then raise Unify REC
365 :     else t
366 :     in fieldwise(extra extra1, extra extra2,
367 :     (fn (t1,t2) => (unifyTy(t1,t2); t1)),
368 :     fields1, fields2)
369 :     end
370 :    
371 :     end (* local *)
372 :     end (* structure Unify *)
373 :    
374 :     (*
375 :     * $Log$
376 :     *)
377 :    
378 :    
379 :    

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