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/compiler/Elaborator/types/eqtypes.sml
ViewVC logotype

Annotation of /sml/trunk/compiler/Elaborator/types/eqtypes.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2162 - (view) (download)

1 : blume 902 (* Copyright 1996 by AT&T Bell Laboratories *)
2 :     (* eqtypes.sml *)
3 :    
4 :     (*
5 :     * This file probably should not belong here ! It relies on the module
6 :     * semantics; and probably it should be moved to modules/ directory. (ZHONG)
7 :     *)
8 :    
9 :     signature EQTYPES =
10 :     sig
11 :    
12 :     val eqAnalyze : Modules.Structure * (Stamps.stamp -> bool)
13 :     * ErrorMsg.complainer -> unit
14 :    
15 :     val defineEqProps : Types.tycon list * ExpandTycon.sigContext
16 :     * EntityEnv.entityEnv -> unit
17 :     val checkEqTySig : Types.ty * Types.polysign -> bool
18 :     (* check whether type ty is an equality type, given a polysign
19 :     * indicating which IBOUND elements are equality types.
20 :     * This isn't accurate on (relatized) types containing PATHtycs,
21 :     * which are effectively treated as OBJ *)
22 :     val isEqTycon : Types.tycon -> bool
23 :     val isEqType : Types.ty -> bool
24 :     val debugging : bool ref
25 :    
26 :     end (* signature EQTYPES *)
27 :    
28 :    
29 :     structure EqTypes : EQTYPES =
30 :     struct
31 :    
32 :     (* functions to determine and check equality types *)
33 :     local structure EM = ErrorMsg
34 :     structure IP = InvPath
35 :     structure TU = TypesUtil
36 :     structure M = Modules
37 :     structure MU = ModuleUtil
38 :     open Types Stamps TypesUtil
39 :    
40 :     in
41 :    
42 :     (* debugging *)
43 :     fun bug msg = EM.impossible("EqTypes: "^msg)
44 :     val say = Control_Print.say
45 :     val debugging = ref false
46 :     fun debugmsg (msg: string) =
47 :     if !debugging then (say msg; say "\n") else ()
48 :    
49 :     fun all (f: 'a -> bool) [] = true
50 :     | all f (x::r) = f x andalso all f r
51 :    
52 :     (* join of eqprops *)
53 :     exception INCONSISTENT
54 :    
55 :     fun join(UNDEF,YES) = YES
56 :     | join(YES,UNDEF) = YES
57 :     | join(UNDEF,NO) = NO
58 :     | join(NO,UNDEF) = NO
59 :     | join(UNDEF,IND) = IND
60 :     | join(IND,UNDEF) = IND
61 :     | join(UNDEF,DATA) = DATA
62 :     | join(DATA,UNDEF) = DATA
63 :     | join(UNDEF,UNDEF) = UNDEF
64 :     | join(DATA,YES) = YES
65 :     | join(YES,DATA) = YES
66 :     | join(DATA,NO) = NO
67 :     | join(NO,DATA) = NO
68 :     | join(DATA,IND) = IND
69 :     | join(IND,DATA) = IND
70 :     | join(DATA,DATA) = DATA
71 :     | join(IND,YES) = YES (* ? *)
72 :     | join(YES,IND) = YES (* ? *)
73 :     | join(IND,NO) = NO
74 :     | join(NO,IND) = NO
75 :     | join(IND,IND) = IND
76 :     | join(YES,YES) = YES
77 :     | join(NO,NO) = NO
78 :     | join(OBJ,OBJ) = OBJ
79 :     | join(ABS,e) = join(NO,e)
80 :     | join(e,ABS) = join(e,NO)
81 :     | join(e1,e2) =
82 :     (say(String.concat[TU.eqpropToString e1,",",TU.eqpropToString e2,"\n"]);
83 :     raise INCONSISTENT)
84 :    
85 :     fun objectTyc (GENtyc { eq = ref OBJ, ... }) = true
86 :     | objectTyc _ = false
87 :    
88 :     (* calculating eqtypes in toplevel signatures *)
89 :    
90 :     exception NOT_EQ
91 :     exception UnboundStamp
92 :    
93 :     (*
94 :     * eqAnalyze is called in just one place, in Instantiate, to compute the
95 :     * actual eqprops of types in an instantiated signature. It has to propagate
96 :     * equality properties to respect type equivalences induced by sharing
97 :     * constraints.
98 :     *)
99 :    
100 :     fun eqAnalyze(str,localStamp : Stamps.stamp -> bool,err : EM.complainer) =
101 :     let val tycons = ref StampMap.empty
102 :     val depend = ref StampMap.empty
103 :     val dependr = ref StampMap.empty
104 :     val eqprop = ref StampMap.empty
105 :     val dependsInd = ref false
106 :     val tycStampsRef : stamp list ref = ref nil
107 :    
108 :     fun dflApply dfl (mr, k) =
109 :     case StampMap.find (!mr, k) of
110 :     NONE => dfl
111 :     | SOME x => x
112 :    
113 :     fun applyMap' x = dflApply [] x
114 :     fun applyMap'' x = dflApply UNDEF x
115 :    
116 :     fun updateMap mr (k, v) = mr := StampMap.insert (!mr, k, v)
117 :    
118 :     val err = fn s => err EM.COMPLAIN s EM.nullErrorBody
119 :    
120 :     fun checkdcons(datatycStamp: stamp,
121 :     evalty: ty -> ty,
122 :     dcons: dconDesc list,
123 :     stamps, members, freetycs) : (eqprop * stamp list) =
124 :     let val depend = ref([]: stamp list)
125 :     val dependsInd = ref false
126 :     fun member(stamp,[]) = false
127 :     | member(st,st'::rest) = Stamps.eq(st,st') orelse member(st,rest)
128 :     fun eqtyc(tyc as GENtyc { stamp, eq, ... }) =
129 :     (case !eq
130 :     of YES => ()
131 :     | OBJ => ()
132 :     | (NO | ABS) => raise NOT_EQ
133 :     | IND => dependsInd := true
134 :     | (DATA | UNDEF) =>
135 :     if member(stamp,!depend)
136 :     orelse Stamps.eq(stamp,datatycStamp) then ()
137 :     else depend := stamp :: !depend)
138 :     | eqtyc(RECORDtyc _) = ()
139 :     | eqtyc _ = bug "eqAnalyze.eqtyc"
140 :     and eqty(VARty(ref(INSTANTIATED ty)))
141 :     = eqty ty (* shouldn't happen *)
142 :     | eqty(ty as CONty(tyc,args)) =
143 :     let val ntyc =
144 :     (case tyc
145 :     of FREEtyc i =>
146 :     (List.nth(freetycs, i) handle _ =>
147 :     bug "unexpected freetycs in eqty")
148 :     | _ => tyc)
149 :     in (case ntyc
150 :     of GENtyc _ =>
151 :     (if objectTyc ntyc then ()
152 :     else (eqtyc ntyc; app eqty args))
153 :     | DEFtyc{tyfun,...} => eqty(headReduceType ty)
154 :     | RECtyc i =>
155 :     let val stamp = Vector.sub(stamps,i)
156 :     val {tycname,dcons,...}: dtmember =
157 :     Vector.sub(members,i)
158 :     in if member(stamp,!depend)
159 :     orelse Stamps.eq(stamp,datatycStamp)
160 :     then ()
161 :     else depend := stamp :: !depend
162 :     end
163 :     | _ => app eqty args)
164 :     end
165 :     | eqty _ = ()
166 :     fun eqdcon{domain=SOME ty',name,rep} = eqty ty'
167 :     | eqdcon _ = ()
168 :     in app eqdcon dcons;
169 :     case (!depend,!dependsInd)
170 :     of ([],false) => (YES,[])
171 :     | (d,false) => (DATA,d)
172 :     | (_,true) => (IND,[])
173 :     end
174 :     handle NOT_EQ => (NO,[])
175 :    
176 :     fun addstr(str as M.STR { sign, rlzn = {entities,...}, ... }) =
177 :     let fun addtyc (tyc as (GENtyc { stamp, eq, kind, path, ... })) =
178 :     if localStamp stamp (* local spec *)
179 :     then ((updateMap tycons
180 :     (stamp,tyc::applyMap'(tycons,stamp));
181 :     tycStampsRef := stamp :: !tycStampsRef;
182 :     case kind
183 :     of DATATYPE{index,stamps,family={members,...},
184 :     root,freetycs} =>
185 :     let val dcons = #dcons(Vector.sub(members,index))
186 :     val eqOrig = !eq
187 :     val (eqpCalc,deps) =
188 :     case eqOrig
189 :     of DATA =>
190 :     checkdcons(stamp,
191 :     MU.transType entities,
192 :     dcons,stamps,members,
193 :     freetycs)
194 :     | e => (e,[])
195 :     (* ASSERT: e = YES or NO *)
196 :     val eq' =
197 :     join(join(eqOrig,
198 :     applyMap''(eqprop,stamp)),
199 :     eqpCalc)
200 :     in
201 :     eq := eq';
202 :     updateMap eqprop (stamp,eq');
203 :     app (fn s => updateMap dependr
204 :     (s, stamp :: applyMap'(dependr,s))) deps;
205 :     updateMap depend
206 :     (stamp, deps @ applyMap'(depend,stamp))
207 :     end
208 :     | (FLEXTYC _ | ABSTRACT _ | PRIMITIVE _) =>
209 :     let val eq' = join(applyMap''(eqprop,stamp), !eq)
210 :     in
211 :     eq := eq';
212 :     updateMap eqprop (stamp,eq')
213 :     end
214 :     | _ => bug "eqAnalyze.scan.tscan")
215 :     handle INCONSISTENT =>
216 :     err "inconsistent equality properties")
217 :     else () (* external -- assume eqprop already defined *)
218 :     | addtyc _ = ()
219 :     in
220 :     if localStamp(MU.getStrStamp str) then
221 :     (List.app (fn s => addstr s) (MU.getStrs str);
222 :     List.app (fn t => addtyc t) (MU.getTycs str))
223 :     (* BUG? - why can we get away with ignoring functor elements??? *)
224 :     else ()
225 :     end
226 :     | addstr _ = () (* must be external or error structure *)
227 :    
228 :     fun propagate (eqp,depset,earlier) =
229 :     let fun prop stamp' =
230 :     app (fn s =>
231 :     let val eqpold = applyMap''(eqprop,s)
232 :     val eqpnew = join(eqp,eqpold)
233 :     in if eqpold <> eqpnew
234 :     then (updateMap eqprop (s,eqp);
235 :     if earlier s then prop s else ())
236 :     else ()
237 :     end handle INCONSISTENT =>
238 :     err "inconsistent equality properties B")
239 :     (depset(stamp'))
240 :     in prop
241 :     end
242 :    
243 :     (* propagate the NO eqprop forward and the YES eqprop backward *)
244 :     fun propagate_YES_NO(stamp) =
245 :     let fun earlier s = Stamps.compare(s,stamp) = LESS
246 :     in case applyMap''(eqprop,stamp)
247 :     of YES =>
248 :     propagate (YES,(fn s => applyMap'(depend,s)),earlier) stamp
249 :     | NO => propagate (NO,(fn s => applyMap'(dependr,s)),earlier) stamp
250 :     | _ => ()
251 :     end
252 :    
253 :     (* propagate the IND eqprop *)
254 :     fun propagate_IND(stamp) =
255 :     let fun depset s = applyMap'(dependr,s)
256 :     fun earlier s = Stamps.compare(s,stamp) = LESS
257 :     in case applyMap''(eqprop,stamp)
258 :     of UNDEF => (updateMap eqprop (stamp,IND);
259 :     propagate (IND,depset,earlier) stamp)
260 :     | IND => propagate (IND,depset,earlier) stamp
261 :     | _ => ()
262 :     end
263 :    
264 :     (* phase 0: scan signature strenv, joining eqprops of shared tycons *)
265 :     val _ = addstr str
266 :     val tycStamps =
267 :     ListMergeSort.sort (fn xy => Stamps.compare xy = GREATER) (!tycStampsRef)
268 :     in
269 :     (* phase 1: propagate YES backwards and NO forward *)
270 :     app propagate_YES_NO tycStamps;
271 :    
272 :     (* phase 2: convert UNDEF to IND and propagate INDs *)
273 :     app propagate_IND tycStamps; (* convert UNDEFs to INDs and propagate *)
274 :    
275 :     (* phase 3: convert DATA to YES; reset stored eqprops from eqprop map *)
276 :     app (fn s =>
277 :     let val eqp = case applyMap''(eqprop,s)
278 :     of DATA => YES
279 :     | e => e
280 :     fun set (GENtyc { eq, ... }) = eq := eqp
281 :     | set _ = ()
282 :     in app set (applyMap'(tycons,s))
283 :     end)
284 :     tycStamps
285 :     end
286 :    
287 :     exception CHECKEQ
288 :    
289 :    
290 :     (* WARNING - defineEqTycon uses eq field ref as a tycon identifier.
291 :     Since defineEqTycon is called only within elabDATATYPEdec, this
292 :     should be ok.*)
293 :    
294 :     val unitTy = BasicTypes.unitTy
295 :    
296 :     fun member(_,[]) = false
297 :     | member(i:int, j::rest) = i=j orelse member(i,rest)
298 :    
299 :     fun namesToString ([]: Symbol.symbol list) = "[]"
300 :     | namesToString (x::xs) =
301 :     String.concat("[" :: (Symbol.name x) ::
302 :     foldl (fn (y,l) => ","::(Symbol.name y)::l) ["]"] xs)
303 :    
304 :     fun defineEqProps (datatycs,sigContext,sigEntEnv) =
305 :     let val names = map TU.tycName datatycs
306 :     val _ = debugmsg (">>defineEqProps: "^ namesToString names)
307 :     val n = List.length datatycs
308 :     val {family={members,...}, freetycs,...} =
309 :     case List.hd datatycs of
310 :     GENtyc { kind = DATATYPE x, ...} => x
311 :     | _ => bug "defineEqProps (List.hd datatycs)"
312 :     val eqs =
313 :     let fun get (GENtyc { eq, ... }) = eq
314 :     | get _ = bug "eqs:get"
315 :     in map get datatycs
316 :     end
317 :     fun getEq i =
318 :     !(List.nth(eqs,i))
319 :     handle Subscript =>
320 :     (say "$getEq "; say(Int.toString i); say " from ";
321 :     say(Int.toString(length eqs)); say "\n";
322 :     raise Subscript)
323 :     fun setEq(i,eqp) =
324 :     (debugmsg (String.concat["setEq: ",Int.toString i," ",
325 :     TU.eqpropToString eqp]);
326 :     (List.nth(eqs,i) := eqp)
327 :     handle Subscript =>
328 :     (say (String.concat["$setEq ",(Int.toString i)," from ",
329 :     (Int.toString(length eqs)),"\n"]);
330 :     raise Subscript))
331 :     val visited = ref([]: int list)
332 :    
333 :     fun checkTyc (tyc0 as GENtyc { eq, kind, path, ... }) =
334 :     (case (!eq, kind) of
335 :     (DATA, DATATYPE { index, ... }) =>
336 :     let val _ = debugmsg (">>checkTyc: "^
337 :     Symbol.name(IP.last path)^" "^
338 :     Int.toString index)
339 :     fun eqtyc (GENtyc { eq = e', kind = k', path, ... }) =
340 :     (case (!e', k')
341 :     of (DATA,DATATYPE{index,...}) =>
342 :     (debugmsg ("eqtyc[GENtyc(DATA)]: " ^
343 :     Symbol.name(IP.last path) ^
344 :     " " ^ Int.toString index);
345 :     (* ASSERT: argument tycon is a member of datatycs *)
346 :     checkDomains index)
347 :     | (UNDEF,_) =>
348 :     (debugmsg ("eqtyc[GENtyc(UNDEF)]: " ^
349 :     Symbol.name(IP.last path));
350 :     IND)
351 :     | (eqp,_) =>
352 :     (debugmsg ("eqtyc[GENtyc(_)]: " ^
353 :     Symbol.name(IP.last path) ^
354 :     " " ^ TU.eqpropToString eqp);
355 :     eqp))
356 :     | eqtyc(RECtyc i) =
357 :     (debugmsg ("eqtyc[RECtyc]: " ^ Int.toString i);
358 :     checkDomains i)
359 :     | eqtyc(RECORDtyc _) = YES
360 :     | eqtyc(ERRORtyc) = IND
361 :     | eqtyc(FREEtyc i) = bug "eqtyc - FREEtyc"
362 :     | eqtyc(PATHtyc _) = bug "eqtyc - PATHtyc"
363 :     | eqtyc(DEFtyc _) = bug "eqtyc - DEFtyc"
364 :    
365 :     and checkDomains i =
366 :     if member(i,!visited) then getEq i
367 :     else let
368 :     val _ = visited := i :: !visited
369 :     val {tycname,dcons,...} : dtmember
370 :     = Vector.sub(members,i)
371 :     handle Subscript =>
372 :     (say (String.concat
373 :     ["$getting member ",
374 :     Int.toString i,
375 :     " from ",
376 :     Int.toString(Vector.length members),"\n"]);
377 :     raise Subscript)
378 :     val _ = debugmsg("checkDomains: visiting "
379 :     ^ Symbol.name tycname ^ " "
380 :     ^ Int.toString i)
381 :     val domains =
382 :     map (fn {domain=SOME ty,name,rep} => ty
383 :     | {domain=NONE,name,rep} => unitTy)
384 :     dcons
385 :     val eqp = eqtylist(domains)
386 :     in
387 :     setEq(i,eqp);
388 :     debugmsg ("checkDomains: setting "^
389 :     Int.toString i^
390 :     " to "^TU.eqpropToString eqp);
391 :     eqp
392 :     end
393 :    
394 :     and eqty(VARty(ref(INSTANTIATED ty))) =
395 :     (* shouldn't happen *)
396 :     eqty ty
397 :     | eqty(CONty(tyc,args)) =
398 :     (case ExpandTycon.expandTycon(tyc,sigContext,sigEntEnv)
399 :     of FREEtyc i =>
400 :     let val _ =
401 :     debugmsg ("eqtyc[FREEtyc]: " ^ Int.toString i)
402 :     val tc = (List.nth(freetycs,i)
403 :     handle _ =>
404 :     bug "unexpected freetycs 343")
405 :     in
406 :     eqty(CONty(tc, args))
407 :     end
408 :     | DEFtyc{tyfun,...} =>
409 :     (* shouldn't happen - type abbrevs in domains
410 :     * should have been expanded *)
411 :     eqty(applyTyfun(tyfun,args))
412 :     | tyc =>
413 :     (case eqtyc tyc
414 :     of (NO | ABS) => NO
415 :     | OBJ => YES
416 :     | YES => eqtylist(args)
417 :     | DATA =>
418 :     (case eqtylist(args) of YES => DATA | e => e)
419 :     | IND => IND
420 :     | UNDEF =>
421 :     bug ("defineEqTycon.eqty: UNDEF - " ^
422 :     Symbol.name(TU.tycName tyc))))
423 :     | eqty _ = YES
424 :    
425 :     and eqtylist(tys) =
426 :     let fun loop([],eqp) = eqp
427 :     | loop(ty::rest,eqp) =
428 :     case eqty ty
429 :     of (NO | ABS) => NO (* return NO immediately;
430 :     no further checking *)
431 :     | YES => loop(rest,eqp)
432 :     | IND => loop(rest,IND)
433 :     | DATA =>
434 :     (case eqp
435 :     of IND => loop(rest,IND)
436 :     | _ => loop(rest,DATA))
437 :     | _ => bug "defineEqTycon.eqtylist"
438 :     in loop(tys,YES)
439 :     end
440 :    
441 :     in
442 :     case eqtyc tyc0
443 :     of YES => app (fn i =>
444 :     case getEq i
445 :     of DATA => setEq(i,YES)
446 :     | _ => ()) (!visited)
447 :     | DATA => app (fn i =>
448 :     case getEq i
449 :     of DATA => setEq(i,YES)
450 :     | _ => ()) (!visited)
451 :     | NO => app (fn i =>
452 :     if i > index
453 :     then case getEq i
454 :     of IND => setEq(i,DATA)
455 :     | _ => ()
456 :     else ()) (!visited)
457 :     (* have to be reanalyzed, throwing away information ??? *)
458 :     | IND => ()
459 :     | _ => bug "defineEqTycon";
460 :     (* ASSERT: eqprop of tyc0 is YES, NO, or IND *)
461 :     case !eq
462 :     of (YES | NO | IND) => ()
463 :     | DATA =>
464 :     bug ("checkTyc[=>DATA]: "^Symbol.name(IP.last path))
465 :     | _ =>
466 :     bug ("checkTyc[=>other]: "^Symbol.name(IP.last path))
467 :     end
468 :     | _ => ())
469 :     | checkTyc _ = ()
470 :     in
471 :     List.app checkTyc datatycs
472 :     end
473 :    
474 :     fun isEqType ty =
475 :     let fun eqty(VARty(ref(INSTANTIATED ty))) = eqty ty
476 :     | eqty(VARty(ref(OPEN {eq,...}))) =
477 :     if eq then ()
478 :     else raise CHECKEQ
479 :     | eqty(CONty(DEFtyc{tyfun,...}, args)) = eqty(applyTyfun(tyfun,args))
480 :     | eqty(CONty(GENtyc { eq, ... }, args)) =
481 :     (case !eq
482 :     of OBJ => ()
483 :     | YES => app eqty args
484 :     | (NO | ABS | IND) => raise CHECKEQ
485 :     | _ => bug "isEqType")
486 :     | eqty(CONty(RECORDtyc _, args)) = app eqty args
487 :     | eqty _ = ()
488 :     in eqty ty; true
489 :     end
490 :     handle CHECKEQ => false
491 :    
492 :     fun checkEqTySig(ty, sign: polysign) =
493 :     let fun eqty(VARty(ref(INSTANTIATED ty))) = eqty ty
494 :     | eqty(CONty(DEFtyc{tyfun,...}, args)) =
495 :     eqty(applyTyfun(tyfun,args))
496 :     | eqty(CONty(GENtyc { eq, ... }, args)) =
497 :     (case !eq
498 :     of OBJ => ()
499 :     | YES => app eqty args
500 :     | (NO | ABS | IND) => raise CHECKEQ
501 :     | _ => bug "checkEqTySig")
502 :     | eqty(IBOUND n) =
503 :     let val eq = List.nth(sign,n)
504 :     in if eq then () else raise CHECKEQ
505 :     end
506 :     | eqty _ = ()
507 :     in eqty ty;
508 :     true
509 :     end
510 :     handle CHECKEQ => false
511 :    
512 :     fun replicate(0,x) = nil | replicate(i,x) = x::replicate(i-1,x)
513 :    
514 :     fun isEqTycon(GENtyc { eq, ... }) =
515 :     (case !eq
516 :     of YES => true
517 :     | OBJ => true
518 :     | _ => false)
519 :     | isEqTycon(DEFtyc{tyfun as TYFUN{arity,...},...}) =
520 :     isEqType(applyTyfun(tyfun,replicate(arity,BasicTypes.intTy)))
521 :     | isEqTycon _ = bug "isEqTycon"
522 :    
523 :     end (* local *)
524 :     end (* structure EqTypes *)
525 :    
526 :    

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