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

Annotation of /sml/trunk/src/compiler/Elaborator/types/typecheck.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 1344 - (view) (download)

1 : blume 902 (* Copyright 1996 by Bell Laboratories *)
2 :     (* typecheck.sml *)
3 :    
4 :     signature TYPECHECK =
5 :     sig
6 :    
7 :     val decType : StaticEnv.staticEnv * Absyn.dec * bool
8 :     * ErrorMsg.errorFn * SourceMap.region -> Absyn.dec
9 :     val debugging : bool ref
10 :    
11 :     end (* signature TYPECHECK *)
12 :    
13 :    
14 :     (* functorized to factor out dependencies on FLINT... *)
15 :     functor TypecheckFn (val ii_ispure : II.ii -> bool
16 :     val ii2ty : II.ii -> Types.ty option) : TYPECHECK =
17 :     struct
18 :    
19 :     local open Array List Types VarCon BasicTypes TypesUtil Unify Absyn
20 :     Overload ErrorMsg PrettyPrint PPUtil PPType PPAbsyn
21 :    
22 :     structure SE = StaticEnv
23 :     (* structure II = InlInfo *)
24 :     structure DA = Access
25 :     structure EU = ElabUtil
26 :     structure ED = ElabDebug
27 :     structure OLL = OverloadLit
28 : macqueen 1344 structure PP = PrettyPrint
29 : blume 902
30 :     in
31 :    
32 :     (* debugging *)
33 :     val say = Control_Print.say
34 :     val debugging = ref false
35 :     fun debugmsg (msg: string) = if !debugging then (say msg; say "\n") else ()
36 :     val debugPrint = (fn x => ED.debugPrint debugging x)
37 :    
38 :     fun bug msg = ErrorMsg.impossible("TypeCheck: "^msg)
39 :    
40 :     val isValue = isValue { ii_ispure = ii_ispure }
41 :    
42 :     infix 9 sub
43 :     infix -->
44 :    
45 :     val printDepth = Control_Print.printDepth
46 :    
47 :     fun refNewDcon(DATACON{name,const,rep,typ,sign,lazyp}) =
48 :     DATACON{name=name,const=const,rep=rep,typ=refPatType,sign=sign,lazyp=lazyp}
49 :    
50 :     exception NotThere
51 :    
52 :     fun message(msg,mode: Unify.unifyFail) =
53 :     String.concat[msg," [",Unify.failMessage mode,"]"]
54 :    
55 :     fun mkDummy0 () = BasicTypes.unitTy
56 :    
57 :     (*
58 :     * decType : SE.staticEnv * A.dec * bool * EM.errorFn * region -> A.dec
59 :     *)
60 :     fun decType(env,dec,toplev,err,region) =
61 :     let
62 :    
63 :     val ppType = PPType.ppType env
64 :     val ppPat = PPAbsyn.ppPat env
65 :     val ppExp = PPAbsyn.ppExp(env,NONE)
66 :     val ppRule = PPAbsyn.ppRule(env,NONE)
67 :     val ppVB = PPAbsyn.ppVB(env,NONE)
68 :     val ppRVB = PPAbsyn.ppRVB(env,NONE)
69 :     val ppDec =
70 :     (fn ppstrm => fn d => PPAbsyn.ppDec (env,NONE) ppstrm (d,!printDepth))
71 :    
72 :     fun ppDecDebug (msg,dec) =
73 :     ED.withInternals(fn () => ED.debugPrint debugging (msg, ppDec, dec))
74 :    
75 :     fun ppTypeDebug (msg,ty) =
76 :     ED.withInternals(fn () => ED.debugPrint debugging (msg, ppType, ty))
77 :    
78 :     fun ppTyvarDebug tv =
79 :     ED.withInternals(fn () => debugmsg (PPType.tyvarPrintname tv))
80 :    
81 :     fun unifyErr{ty1,name1,ty2,name2,message=m,region,kind,kindname,phrase} =
82 :     (unifyTy(ty1,ty2); true) handle Unify(mode) =>
83 :     (err region COMPLAIN (message(m,mode))
84 :     (fn ppstrm =>
85 :     (PPType.resetPPType();
86 :     let val len1= size name1
87 :     val len2= size name2
88 :     val spaces = " "
89 :     val pad1= substring(spaces,0,Int.max(0,len2-len1))
90 :     val pad2= substring(spaces,0,Int.max(0,len2-len1))
91 :     val m = if m="" then name1 ^ " and " ^ name2 ^ " don't agree"
92 :     else m
93 :     in if name1="" then ()
94 : macqueen 1344 else (newline ppstrm;
95 :     PP.string ppstrm (name1 ^ ": " ^ pad1);
96 : blume 902 ppType ppstrm ty1);
97 :     if name2="" then ()
98 : macqueen 1344 else (newline ppstrm;
99 :     PP.string ppstrm (name2 ^ ": " ^ pad2);
100 : blume 902 ppType ppstrm ty2);
101 :     if kindname="" then ()
102 : macqueen 1344 else (newline ppstrm; PP.string ppstrm("in "^kindname^":");
103 :     break ppstrm {nsp=1,offset=2}; kind ppstrm (phrase,!printDepth))
104 : blume 902 end));
105 :     false)
106 :    
107 :     val _ = debugmsg (">>decType: toplev = " ^ Bool.toString toplev)
108 :     val _ = ppDecDebug(">>decType: dec = ",dec)
109 :    
110 :     fun generalizeTy(VALvar{typ,path,...}, userbound: tyvar list,
111 :     occ:occ, generalize: bool, region) : tyvar list =
112 :     let val _ = debugmsg ("generalizeTy: "^SymPath.toString path)
113 :     val _ = debugmsg ("userbound: ")
114 :     val _ = List.app ppTyvarDebug userbound
115 :    
116 :     val failure = ref false
117 :     val mkDummy = if toplevel occ
118 :     then TypesUtil.dummyTyGen()
119 :     else mkDummy0 (* shouldn't be called *)
120 :    
121 :     val index = ref 0 (* counts no of type variables bound *)
122 :     fun next() = let val i = !index in index := i+1; i end
123 :     val sign = ref([]: Types.polysign)
124 :     fun localUbound tv =
125 :     let fun mem(tv'::rest) = eqTyvar(tv,tv') orelse mem rest
126 :     | mem [] = false
127 :     in mem userbound
128 :     end
129 :     (* menv: a reference to an association list environment mapping
130 :     * generalized tyvars to the corresponding IBOUND type.
131 :     * ASSERT: there are no duplicate tyvars in domain of menv. *)
132 :     val menv = ref([]: (tyvar*ty) list)
133 :     fun lookup tv =
134 :     let fun find [] = raise NotThere
135 :     | find((tv',ty)::rest) = if eqTyvar(tv,tv') then ty
136 :     else find rest
137 :     in find(!menv)
138 :     end
139 :     fun bind(tv,ty) = menv := (tv,ty) :: !menv
140 :     fun gen(ty) =
141 :     case ty
142 :     of VARty(ref(INSTANTIATED ty)) => gen ty
143 :     | VARty(tv as ref(OPEN{depth,eq,kind})) =>
144 :     (case kind
145 :     of FLEX[(lab,_)] =>
146 :     if ((depth > lamdepth occ) andalso
147 :     (generalize orelse (toplevel occ)))
148 :     orelse ((toplevel occ) andalso (depth=0))
149 :     then
150 :     (err region COMPLAIN (String.concat
151 :     ["unresolved flex record\n\
152 :     \ (can't tell what fields there are besides #",
153 :     Symbol.name lab, ")"])
154 :     nullErrorBody;
155 :     WILDCARDty)
156 :     else ty
157 :     | FLEX _ =>
158 :     if ((depth > lamdepth occ) andalso
159 :     (generalize orelse (toplevel occ)))
160 :     orelse ((toplevel occ) andalso (depth=0))
161 :     then
162 :     (err region COMPLAIN
163 :     "unresolved flex record (need to know the \
164 :     \names of ALL the fields\n in this context)"
165 :     (fn ppstrm =>
166 :     (PPType.resetPPType();
167 : macqueen 1344 newline ppstrm;
168 :     PP.string ppstrm "type: ";
169 : blume 902 ppType ppstrm ty));
170 :     WILDCARDty)
171 :     else ty
172 :     | META =>
173 :     if depth > lamdepth occ
174 :     then if generalize then
175 :     lookup tv handle NotThere =>
176 :     let val new = IBOUND(next())
177 :     in sign := eq :: !sign;
178 :     bind(tv,new);
179 :     new
180 :     end
181 :     else (if toplevel occ
182 :     then let val new = mkDummy()
183 :     in failure := true;
184 :     tv := INSTANTIATED new;
185 :     new
186 :     end
187 :     else (if !ElabControl.valueRestrictionLocalWarn
188 :     then err region WARN
189 :     ("type variable not generalized\
190 :     \ in local decl (value restriction): "
191 :     ^ (tyvarPrintname tv))
192 :     nullErrorBody
193 :     else ();
194 :     (* reset depth to prevent later
195 :     incorrect generalization inside
196 :     a lambda expression. See typechecking
197 :     test 5.sml *)
198 :     tv := OPEN{depth = lamdepth occ,
199 :     eq = eq, kind = kind};
200 :     ty))
201 :     else if toplevel occ andalso depth = 0
202 :     (* ASSERT: failed generalization at depth 0.
203 :     see bug 1066. *)
204 :     then lookup tv handle NotThere =>
205 :     let val new = mkDummy()
206 :     in failure := true;
207 :     tv := INSTANTIATED new;
208 :     new
209 :     end
210 :     else ty) (* raise SHARE *)
211 :     | VARty(tv as ref(UBOUND{name,depth,eq})) =>
212 :     (debugmsg ("UBOUND:" ^Symbol.name name);
213 :     if localUbound tv
214 :     then (debugmsg "is local";
215 :     if depth > lamdepth occ andalso generalize
216 :     then (debugmsg "is generalized";
217 :     lookup tv handle NotThere =>
218 :     let val new = IBOUND(next())
219 :     in sign := eq :: !sign;
220 :     bind(tv,new);
221 :     new
222 :     end)
223 :     else (err region COMPLAIN
224 :     ("explicit type variable cannot be \
225 :     \generalized at its binding \
226 :     \declaration: " ^
227 :     (tyvarPrintname tv))
228 :     nullErrorBody;
229 :     tv := INSTANTIATED WILDCARDty;
230 :     WILDCARDty))
231 :     else (debugmsg "is not local"; ty))
232 :     | (VARty(ref(LITERAL _)) | VARty(ref(SCHEME _))) => ty
233 :     | CONty(tyc,args) => CONty(tyc, map gen args) (*shareMap*)
234 :     | WILDCARDty => WILDCARDty
235 :     | _ => bug "generalizeTy -- bad arg"
236 :    
237 :     val _ = ppTypeDebug (">>gen: before: ",!typ)
238 :     val ty = gen(!typ)
239 :     val _ = ppTypeDebug (">>gen: after: ",ty)
240 :    
241 :     val generalizedTyvars = map #1 (rev(!menv))
242 :    
243 :     (* a hack to eliminate all user bound type variables --zsh *)
244 :     (* ZHONG?: is this still necessary? [dbm] *)
245 :     fun elimUbound(tv as ref(UBOUND{depth,eq,...})) =
246 :     (tv := OPEN{depth=depth,eq=eq,kind=META})
247 :     | elimUbound _ = ()
248 :    
249 :     (* turn ubound tyvars into ordinary META tyvars *)
250 :     val _ = app elimUbound generalizedTyvars
251 :    
252 :     in if !failure andalso !ElabControl.valueRestrictionTopWarn
253 :     then err region WARN
254 :     "type vars not generalized because of\n\
255 :     \ value restriction are instantiated to dummy types (X1,X2,...)"
256 :     nullErrorBody
257 :     else ();
258 :     debugmsg "generalizeTy returning";
259 :     typ := POLYty{sign = rev(!sign),
260 :     tyfun = TYFUN{arity=(!index),body=ty}};
261 :     generalizedTyvars (* return the tyvars that were generalized *)
262 :     end
263 :    
264 :     | generalizeTy _ = bug "generlizeTy - bad arg"
265 :    
266 :    
267 :     fun generalizePat(pat: pat, userbound: tyvar list, occ: occ,
268 :     generalize: bool, region) =
269 :     let val tvs : tyvar list ref = ref []
270 :     fun gen(VARpat v) =
271 :     (let val x = generalizeTy(v,userbound,occ,generalize,region)
272 :     val _ = case (x, !tvs)
273 :     of (_::_, _::_) => bug "generalizePat 1234"
274 :     | _ => ()
275 :     in tvs := (x@(!tvs))
276 :     end)
277 :     | gen(RECORDpat{fields,...}) = app (gen o #2) fields
278 :     | gen(APPpat(_,_,arg)) = gen arg
279 :     | gen(CONSTRAINTpat(pat,_)) = gen pat
280 :     | gen(LAYEREDpat(varPat,pat)) = (gen varPat; gen pat)
281 :     | gen _ = ()
282 :     in gen pat; !tvs
283 :     end
284 :    
285 :     fun applyType(ratorTy: ty, randTy: ty) : ty =
286 :     let val resultType = mkMETAty()
287 :     in unifyTy(ratorTy, (randTy --> resultType)); resultType
288 :     end
289 :    
290 :     fun patType(pat: pat, depth, region) : pat * ty =
291 :     case pat
292 :     of WILDpat => (pat,mkMETAtyBounded depth)
293 :     | VARpat(VALvar{typ as ref UNDEFty,...}) =>
294 :     (typ := mkMETAtyBounded depth; (pat,!typ))
295 :     (* multiple occurrence due to or-pat *)
296 :     | VARpat(VALvar{typ, ...}) => (pat, !typ)
297 :     | INTpat (_,ty) => (OLL.push ty; (pat,ty))
298 :     | WORDpat (_,ty) => (OLL.push ty; (pat,ty))
299 :     | REALpat _ => (pat,realTy)
300 :     | STRINGpat _ => (pat,stringTy)
301 :     | CHARpat _ => (pat,charTy)
302 :     | RECORDpat{fields,flex,typ} =>
303 :     (* fields assumed already sorted by label *)
304 :     let fun g(lab,pat') =
305 :     let val (npat,nty) = patType(pat',depth,region)
306 :     in ((lab,npat), (lab,nty))
307 :     end
308 :     val (fields',labtys) = mapUnZip g fields
309 :     val npat = RECORDpat{fields=fields',flex=flex,typ=typ}
310 :     in if flex
311 :     then let val ty = VARty(mkTyvar(mkFLEX(labtys,depth)))
312 :     in typ := ty; (npat,ty)
313 :     end
314 :     else (npat,recordTy(labtys))
315 :     end
316 :     | VECTORpat(pats,_) =>
317 :     (let val (npats,ntys) =
318 :     mapUnZip (fn pat => patType(pat,depth,region)) pats
319 :     val nty =
320 :     foldr (fn (a,b) => (unifyTy(a,b); b)) (mkMETAtyBounded depth) ntys
321 :     in (VECTORpat(npats,nty), CONty(vectorTycon,[nty]))
322 :     end handle Unify(mode) => (
323 :     err region COMPLAIN
324 :     (message("vector pattern type failure",mode)) nullErrorBody;
325 :     (pat,WILDCARDty)))
326 :     | ORpat(p1, p2) =>
327 :     let val (p1, ty1) = patType(p1, depth, region)
328 :     val (p2, ty2) = patType(p2, depth, region)
329 :     in
330 :     unifyErr{ty1=ty1,ty2=ty2,name1="expected",name2="found",
331 :     message="or-patterns don't agree",region=region,
332 :     kind=ppPat,kindname="pattern",phrase=pat};
333 :     (ORpat(p1, p2), ty1)
334 :     end
335 :     | CONpat(dcon as DATACON{typ,...},_) =>
336 :     let val (ty, insts) = instantiatePoly typ
337 :     (* the following is to set the correct depth information
338 :     * to the type variables in ty. (ZHONG)
339 :     *)
340 :     val nty = mkMETAtyBounded depth
341 :     val _ = unifyTy(nty, ty)
342 :     in (CONpat(dcon,insts),ty)
343 :     end
344 :     | APPpat(dcon as DATACON{typ,rep,...},_,arg) =>
345 :     let val (argpat,argty) = patType(arg,depth,region)
346 :     val (ty1,ndcon) = case rep
347 :     of DA.REF => (refPatType,refNewDcon dcon)
348 :     | _ => (typ,dcon)
349 :     val (ty2,insts) = instantiatePoly ty1
350 :     val npat = APPpat(ndcon,insts,argpat)
351 :     in (npat,applyType(ty2,argty))
352 :     handle Unify(mode) =>
353 :     (err region COMPLAIN
354 :     (message("constructor and argument don't agree in pattern",mode))
355 :     (fn ppstrm =>
356 :     (PPType.resetPPType();
357 : macqueen 1344 newline ppstrm;
358 :     PP.string ppstrm "constructor: ";
359 :     ppType ppstrm typ; newline ppstrm;
360 :     PP.string ppstrm "argument: ";
361 :     ppType ppstrm argty; newline ppstrm;
362 :     PP.string ppstrm "in pattern:"; break ppstrm {nsp=1,offset=2};
363 : blume 902 ppPat ppstrm (pat,!printDepth)));
364 :     (pat,WILDCARDty))
365 :     end
366 :     | CONSTRAINTpat(pat',ty) =>
367 :     let val (npat,patTy) = patType(pat',depth,region)
368 :     in if unifyErr{ty1=patTy,name1="pattern",ty2=ty,name2="constraint",
369 :     message="pattern and constraint don't agree",
370 :     region=region,kind=ppPat,kindname="pattern",phrase=pat}
371 :     then (CONSTRAINTpat(npat,ty),ty)
372 :     else (pat,WILDCARDty)
373 :     end
374 :     | LAYEREDpat(vpat as VARpat(VALvar{typ,...}),pat') =>
375 :     let val (npat,patTy) = patType(pat',depth,region)
376 :     val _ = (typ := patTy)
377 :     in (LAYEREDpat(vpat,npat),patTy)
378 :     end
379 :     | LAYEREDpat(cpat as CONSTRAINTpat(VARpat(VALvar{typ,...}),ty),pat') =>
380 :     let val (npat,patTy) = patType(pat',depth,region)
381 :     in if unifyErr{ty1=patTy,name1="pattern",ty2=ty,name2="constraint",
382 :     message="pattern and constraint don't agree",
383 :     region=region,kind=ppPat,kindname="pattern",phrase=pat}
384 :     then (typ := ty; (LAYEREDpat(cpat,npat),ty))
385 :     else (pat,WILDCARDty)
386 :     end
387 :     | p => bug "patType -- unexpected pattern"
388 :    
389 :     fun expType(exp: exp, occ: occ, region) : exp * ty =
390 : mblume 1332 let fun boolUnifyErr { ty, name, message } =
391 :     unifyErr { ty1 = ty, name1 = name, ty2 = boolTy, name2 = "",
392 :     message = message, region = region, kind = ppExp,
393 :     kindname = "expression", phrase = exp }
394 :     fun boolshortcut (con, what, e1, e2) =
395 :     let val (e1', t1) = expType (e1, occ, region)
396 :     val (e2', t2) = expType (e2, occ, region)
397 :     val m = String.concat ["operand of ", what, " is not of type bool"]
398 :     in
399 :     if boolUnifyErr { ty = t1, name = "operand", message = m }
400 :     andalso boolUnifyErr { ty = t2, name = "operand", message = m }
401 :     then (con (e1', e2'), boolTy)
402 :     else (exp, WILDCARDty)
403 :     end
404 :     in
405 : blume 902 case exp
406 :     of VARexp(r as ref(VALvar{typ, info, ...}), _) =>
407 :     (case ii2ty info of
408 :     SOME st =>
409 :     let val (sty, insts) = instantiatePoly(st)
410 :     val (nty, _) = instantiatePoly(!typ)
411 :     in
412 :     unifyTy(sty, nty) handle _ => (); (* ??? *)
413 :     (VARexp(r, insts), sty)
414 :     end
415 :     | NONE =>
416 :     let val (ty, insts) = instantiatePoly(!typ)
417 :     in (VARexp(r, insts), ty)
418 :     end)
419 :     | VARexp(refvar as ref(OVLDvar _),_) =>
420 :     (exp,pushOverloaded(refvar, err region))
421 :     | VARexp(r as ref ERRORvar, _) => (exp, WILDCARDty)
422 :     | CONexp(dcon as DATACON{typ,...},_) =>
423 :     let val (ty,insts) = instantiatePoly typ
424 :     in (CONexp(dcon,insts),ty)
425 :     end
426 :     | INTexp (_,ty) => (OLL.push ty; (exp,ty))
427 :     | WORDexp (_,ty) => (OLL.push ty; (exp,ty))
428 :     | REALexp _ => (exp,realTy)
429 :     | STRINGexp _ => (exp,stringTy)
430 :     | CHARexp _ => (exp,charTy)
431 :     | RECORDexp fields =>
432 :     let fun h(l as LABEL{name,...},exp') =
433 :     let val (nexp,nty) = expType(exp',occ,region)
434 :     in ((l,nexp),(l,nty))
435 :     end
436 :     fun extract(LABEL{name,...},t) = (name,t)
437 :     val (fields',tfields) = mapUnZip h fields
438 :     val rty = map extract (sortFields tfields)
439 :     in (RECORDexp fields',recordTy(rty))
440 :     end
441 :     | SELECTexp (l, e) =>
442 :     let val (nexp, nty) = expType(e, occ, region)
443 :     val res = mkMETAty ()
444 :     val labtys = [(EU.labsym l, res)]
445 :     val pt = VARty(mkTyvar(mkFLEX(labtys,infinity)))
446 :     in (unifyTy(pt,nty); (SELECTexp(l, nexp), res))
447 :     handle Unify(mode) =>
448 :     (err region COMPLAIN
449 :     (message("selecting a non-existing field from a record",mode))
450 :     (fn ppstrm =>
451 :     (PPType.resetPPType();
452 : macqueen 1344 newline ppstrm;
453 :     PP.string ppstrm "the field name: ";
454 : blume 902 (case l of LABEL{name,...} => ppSym ppstrm name);
455 : macqueen 1344 newline ppstrm;
456 :     PP.string ppstrm "the record type: ";
457 :     ppType ppstrm nty; newline ppstrm;
458 :     PP.string ppstrm "in expression:";
459 :     break ppstrm {nsp=1,offset=2};
460 : blume 902 ppExp ppstrm (exp,!printDepth)));
461 :     (exp, WILDCARDty))
462 :     end
463 :     | VECTORexp(exps,_) =>
464 :     (let val (exps',nty) = mapUnZip (fn e => expType(e,occ,region)) exps
465 :     val vty = foldr (fn (a,b) => (unifyTy(a,b); b)) (mkMETAty()) nty
466 :     in (VECTORexp(exps',vty), CONty(vectorTycon,[vty]))
467 :     end handle Unify(mode) =>
468 :     (err region COMPLAIN
469 :     (message("vector expression type failure",mode))
470 :     nullErrorBody; (exp,WILDCARDty)))
471 :     | SEQexp exps =>
472 :     let fun scan nil = (nil,unitTy)
473 :     | scan [e] =
474 :     let val (e',ety) = expType(e,occ,region)
475 :     in ([e'],ety)
476 :     end
477 :     | scan (e::rest) =
478 :     let val (e',_) = expType(e,occ,region)
479 :     val (el',ety) = scan rest
480 :     in (e'::el',ety)
481 :     end
482 :     val (exps',expty) = scan exps
483 :     in (SEQexp exps',expty)
484 :     end
485 :     | APPexp(rator, rand) =>
486 :     let val (rator',ratorTy) = expType(rator,occ,region)
487 :     val (rand',randTy) = expType(rand,occ,region)
488 :     val exp' = APPexp(rator',rand')
489 :     in (exp',applyType(ratorTy,randTy))
490 :     handle Unify(mode) =>
491 :     let val ratorTy = prune ratorTy
492 :     val reducedRatorTy = headReduceType ratorTy
493 :     in PPType.resetPPType();
494 :     if isArrowType(reducedRatorTy)
495 :     then (err region COMPLAIN
496 :     (message("operator and operand don't agree",mode))
497 :     (fn ppstrm =>
498 : macqueen 1344 (newline ppstrm;
499 :     PP.string ppstrm "operator domain: ";
500 : blume 902 ppType ppstrm (domain reducedRatorTy);
501 : macqueen 1344 newline ppstrm;
502 :     PP.string ppstrm "operand: ";
503 :     ppType ppstrm randTy; newline ppstrm;
504 :     PP.string ppstrm "in expression:";
505 :     break ppstrm {nsp=1,offset=2};
506 : blume 902 ppExp ppstrm (exp,!printDepth)));
507 :     (exp,WILDCARDty))
508 :     else (err region COMPLAIN
509 :     (message("operator is not a function",mode))
510 :     (fn ppstrm =>
511 : macqueen 1344 (newline ppstrm;
512 :     PP.string ppstrm "operator: ";
513 :     ppType ppstrm (ratorTy); newline ppstrm;
514 :     PP.string ppstrm "in expression:";
515 :     break ppstrm {nsp=1,offset=2};
516 : blume 902 ppExp ppstrm (exp,!printDepth)));
517 :     (exp,WILDCARDty))
518 :     end
519 :     end
520 :     | CONSTRAINTexp(e,ty) =>
521 :     let val (e',ety) = expType(e,occ,region)
522 :     in if unifyErr{ty1=ety,name1="expression", ty2=ty, name2="constraint",
523 :     message="expression doesn't match constraint",
524 :     region=region,kind=ppExp,kindname="expression",
525 :     phrase=exp}
526 :     then (CONSTRAINTexp(e',ty),ty)
527 :     else (exp,WILDCARDty)
528 :     end
529 :     | HANDLEexp(e,HANDLER h) =>
530 :     let val (e',ety) = expType(e,occ,region)
531 :     and (h',hty) = expType(h,occ,region)
532 :     val exp' = HANDLEexp(e',HANDLER h')
533 :     in (unifyTy(hty, exnTy --> ety); (exp',ety))
534 :     handle Unify(mode) =>
535 :     (if unifyErr{ty1=domain(prune hty), name1="handler domain",
536 :     ty2=exnTy, name2="",
537 :     message="handler domain is not exn",
538 :     region=region,kind=ppExp,kindname="expression",
539 :     phrase=exp}
540 :     then unifyErr{ty1=ety, name1="body",
541 :     ty2=range(prune hty), name2="handler range",
542 :     message="expression and handler don't agree",
543 :     region=region,
544 :     kind=ppExp,kindname="expression",phrase=exp}
545 :     else false;
546 :     (exp,WILDCARDty))
547 :     end
548 :     | RAISEexp(e,_) =>
549 :     let val (e',ety) = expType(e,occ,region)
550 :     val newty = mkMETAty()
551 :     in unifyErr{ty1=ety, name1="raised", ty2=exnTy, name2="",
552 :     message="argument of raise is not an exception",
553 :     region=region,kind=ppExp,kindname="expression",phrase=exp};
554 :     (RAISEexp(e',newty),newty)
555 :     end
556 :     | LETexp(d,e) =>
557 :     let val d' = decType0(d,LetDef(occ),region)
558 :     val (e',ety) = expType(e,occ,region)
559 :     in (LETexp(d',e'),ety)
560 :     end
561 :     | CASEexp(e,rules,isMatch) =>
562 :     let val (e',ety) = expType(e,occ,region)
563 :     val (rules',_,rty) = matchType(rules,occ,region)
564 :     val exp' = CASEexp(e',rules', isMatch)
565 :     in (exp',applyType(rty,ety))
566 :     handle Unify(mode) =>
567 :     (if isMatch then
568 :     unifyErr{ty1=domain rty, name1="rule domain",
569 :     ty2=ety, name2="object",
570 :     message="case object and rules don't agree",
571 :     region=region,kind=ppExp,kindname="expression",phrase=exp}
572 :     else
573 :     let val decl = case rules
574 :     of (RULE(pat,_))::_ =>
575 :     VB{pat=pat,exp=exp,tyvars=ref[],boundtvs=[]}
576 :     | _ => bug "unexpected rule list 456"
577 :     in unifyErr{ty1=domain rty, name1="pattern",
578 :     ty2=ety, name2="expression",
579 :     message="pattern and expression in val dec don't agree",
580 :     region=region,kind=ppVB,kindname="declaration",
581 :     phrase=decl}
582 :     end;
583 :     (exp,WILDCARDty))
584 :     end
585 :     (* this causes case to behave differently from let, i.e.
586 :     bound variables do not have generic types *)
587 : mblume 1332 | IFexp { test, thenCase, elseCase } =>
588 :     let val (test', tty) = expType (test, occ, region)
589 :     val (thenCase', tct) = expType (thenCase, occ, region)
590 :     val (elseCase', ect) = expType (elseCase, occ, region)
591 :     in
592 :     if boolUnifyErr
593 :     { ty = tty, name = "test expression",
594 :     message="test expression in if is not of type bool" }
595 :     andalso
596 :     unifyErr { ty1 = tct, name1 = "then branch",
597 :     ty2 = ect, name2 = "else branch",
598 :     message="types of if branches do not agree",
599 :     region = region, kind = ppExp,
600 :     kindname = "expression", phrase = exp }
601 :     then
602 :     (IFexp { test = test', thenCase = thenCase',
603 :     elseCase = elseCase' },
604 :     tct)
605 :     else
606 :     (exp, WILDCARDty)
607 :     end
608 :     | ANDALSOexp (e1, e2) =>
609 :     boolshortcut (ANDALSOexp, "andalso", e1, e2)
610 :     | ORELSEexp (e1, e2) =>
611 :     boolshortcut (ORELSEexp, "orelse", e1, e2)
612 :     | WHILEexp { test, expr } =>
613 :     let val (test', tty) = expType (test, occ, region)
614 :     val (expr', _) = expType (expr, occ, region)
615 :     in
616 :     if boolUnifyErr { ty = tty, name = "test expression",
617 :     message = "test expression in while is not of type bool" }
618 :     then
619 :     (WHILEexp { test = test', expr = expr' }, unitTy)
620 :     else
621 :     (exp, WILDCARDty)
622 :     end
623 : blume 902 | FNexp(rules,_) =>
624 :     let val (rules',ty,rty) = matchType(rules,occ,region)
625 :     in (FNexp(rules',ty),rty)
626 :     end
627 :     | MARKexp(e,region) =>
628 :     let val (e',et) = expType(e,occ,region)
629 :     in (MARKexp(e',region),et)
630 :     end
631 :     | _ => bug "exptype -- bad expression"
632 : mblume 1332 end
633 : blume 902
634 :     and ruleType(RULE(pat,exp),occ,region) =
635 :     let val occ = Abstr occ
636 :     val (pat',pty) = patType(pat,lamdepth occ,region)
637 :     val (exp',ety) = expType(exp,occ,region)
638 :     in (RULE(pat',exp'),pty,pty --> ety)
639 :     end
640 :    
641 :     and matchType(l,occ,region) =
642 :     case l
643 :     of [] => bug "empty rule list in typecheck.matchType"
644 :     | [rule] =>
645 :     let val (rule0,argt,rty) = ruleType(rule,occ,region)
646 :     in ([rule0],argt,rty)
647 :     end
648 :     | rule::rest =>
649 :     let val (rule0,argt,rty) = ruleType(rule,occ,region)
650 :     fun checkrule rule' =
651 :     let val (rule1,argt',rty') = ruleType(rule',occ,region)
652 :     in unifyErr{ty1=rty,ty2=rty', name1="earlier rule(s)",
653 :     name2="this rule",
654 :     message="types of rules don't agree",
655 :     region=region,
656 :     kind=ppRule,kindname="rule",phrase=rule'};
657 :     rule1
658 :     end
659 :     in (rule0::(map checkrule rest),argt,rty)
660 :     end
661 :    
662 :     and decType0(decl,occ,region) : dec =
663 :     case decl
664 :     of VALdec vbs =>
665 :     let fun vbType(vb as VB{pat, exp, tyvars=(tv as (ref tyvars)), boundtvs}) =
666 :     let val (pat',pty) = patType(pat,infinity,region)
667 :     val (exp',ety) = expType(exp,occ,region)
668 :     val generalize = isValue exp (* orelse isVarTy ety *)
669 :     in unifyErr{ty1=pty,ty2=ety, name1="pattern", name2="expression",
670 :     message="pattern and expression in val dec don't agree",
671 :     region=region,kind=ppVB,kindname="declaration",
672 :     phrase=vb};
673 :     VB{pat=pat',exp=exp',tyvars=tv,
674 :     boundtvs=generalizePat(pat,tyvars,occ,generalize,region)}
675 :     end
676 :     val _ = debugmsg ">>decType0: VALdec"
677 :     in VALdec(map vbType vbs)
678 :     end
679 :    
680 :     | VALRECdec(rvbs) =>
681 :     let val occ = Abstr occ
682 :    
683 :     (* First go through and type-check all the patterns and
684 :     result-constraints, unifying with each other and with
685 :     the specified result type.
686 :     *)
687 :     fun setType(rvb as RVB{var=VALvar{typ,...},exp,resultty,...}) =
688 :     let val domainty = mkMETAtyBounded(lamdepth occ)
689 :     val rangety = mkMETAtyBounded(lamdepth occ)
690 :    
691 :     val funty = domainty --> rangety
692 :    
693 :     val _ =
694 :     case resultty
695 :     of NONE => true
696 :     | SOME ty =>
697 :     unifyErr{ty1=funty,ty2=ty,
698 :     name1="",name2="constraint",
699 :     message="type constraint of val rec dec\
700 :     \ is not a function type",
701 :     region=region,kind=ppRVB,
702 :     kindname="declaration", phrase=rvb}
703 :    
704 :     fun f(FNexp(rules,_), region, funty) =
705 :     let fun unify a =
706 :     (unifyErr{ty1=a,name1="this clause",
707 :     ty2=funty,name2="previous clauses",
708 :     message="parameter or result constraints\
709 :     \ of clauses don't agree",
710 :     region=region,kind=ppRVB,
711 :     kindname="declaration", phrase=rvb};
712 :     ())
713 :    
714 :     fun approxRuleTy(RULE(pat,e)) =
715 :     let val (pat',pty) =
716 :     patType(pat,lamdepth occ,region)
717 :     in case e
718 :     of CONSTRAINTexp(e,ty) =>
719 :     (pat',pty-->ty,(e,region))
720 :     | e => (pat',pty-->rangety,(e,region))
721 :     end
722 :    
723 :     val patTyExps = map approxRuleTy rules
724 :     val pats = map #1 patTyExps
725 :     val tys = map #2 patTyExps
726 :     val exps = map #3 patTyExps
727 :    
728 :     fun doExp (e,region) =
729 :     let val (exp', ety) = expType(e,occ,region)
730 :     in unifyErr{ty1=ety, name1="expression",
731 :     ty2=rangety, name2="result type",
732 :     message="right-hand-side of clause\
733 :     \ doesn't agree with function result type",
734 :     region=region,kind=ppRVB,
735 :     kindname="declaration",phrase=rvb};
736 :     exp'
737 :     end
738 :    
739 :     in app unify tys;
740 :     typ := funty;
741 :     fn()=>
742 :     FNexp(ListPair.map RULE (pats, map doExp exps),
743 :     domain(prune(funty)))
744 :     end
745 :     | f(MARKexp(e,region),_,funty) =
746 :     let val build = f(e,region,funty)
747 :     in fn()=> MARKexp(build(), region)
748 :     end
749 :     | f(CONSTRAINTexp(e,ty),region,funty) =
750 :     let val _ =
751 :     unifyErr{ty1=ty, name1="this constraint",
752 :     ty2=funty, name2="outer constraints",
753 :     message="type constraints on val rec\
754 :     \ declaraction disagree",
755 :     region=region,kind=ppRVB,
756 :     kindname="declaration", phrase=rvb}
757 :     val build = f(e,region,funty)
758 :     in fn()=> CONSTRAINTexp(build(), ty)
759 :     end
760 :     | f _ = bug "typecheck.823"
761 :     in f(exp,region,funty)
762 :     end
763 :     | setType _ = bug "setType"
764 :    
765 :     (* Second, go through and type-check the right-hand-side
766 :     expressions (function bodies) *)
767 :     fun rvbType(RVB{var=v,resultty,tyvars,boundtvs,...}, build) =
768 :     RVB{var=v,exp=build(), resultty=resultty,tyvars=tyvars,
769 :     boundtvs=boundtvs}
770 :    
771 :     val _ = debugmsg ">>decType0: VALRECdec"
772 :     val builders = map setType rvbs
773 :     val rvbs' = ListPair.map rvbType (rvbs,builders)
774 :     (* No need to generalize here, because every VALRECdec is
775 :     wrapped in a VALdec, and the generalization occurs at the
776 :     outer level. Previously: val rvbs'' = map genType rvbs' *)
777 :     in EU.recDecs rvbs'
778 :     end
779 :    
780 :     | EXCEPTIONdec(ebs) =>
781 :     let fun check(VARty(ref(UBOUND _))) =
782 :     err region COMPLAIN
783 :     "type variable in top level exception type"
784 :     nullErrorBody
785 :     | check(CONty(_,args)) =
786 :     app check args
787 :     | check _ = ()
788 :     fun ebType(EBgen{etype=SOME ty,...}) = check ty
789 :     | ebType _ = ()
790 :     val _ = debugmsg ">>decType0: EXCEPTIONdec"
791 :     in if TypesUtil.lamdepth occ < 1 then app ebType ebs else ();
792 :     decl
793 :     end
794 :     | LOCALdec(decIn,decOut) =>
795 :     let val decIn' = decType0(decIn,LetDef occ,region)
796 :     val decOut' = decType0(decOut,occ,region)
797 :     val _ = debugmsg ">>decType0: LOCALdec"
798 :     in LOCALdec(decIn',decOut')
799 :     end
800 :     | SEQdec(decls) =>
801 :     SEQdec(map (fn decl => decType0(decl,occ,region)) decls)
802 :     | ABSTYPEdec{abstycs,withtycs,body} =>
803 :     let fun makeAbstract(GENtyc { eq, ... }) = eq := ABS
804 :     | makeAbstract _ = bug "makeAbstract"
805 :     fun redefineEq(DATATYPEdec{datatycs,...}) =
806 :     let fun setDATA (GENtyc { eq, ... }) = eq := DATA
807 :     | setDATA _ = ()
808 :     in
809 :     app setDATA datatycs;
810 :     EqTypes.defineEqProps(datatycs,nil,EntityEnv.empty)
811 :     end
812 :     | redefineEq(SEQdec decs) = app redefineEq decs
813 :     | redefineEq(LOCALdec(din,dout)) =
814 :     (redefineEq din; redefineEq dout)
815 :     | redefineEq(MARKdec(dec,_)) = redefineEq dec
816 :     | redefineEq _ = ()
817 :     val body'= decType0(body,occ,region)
818 :     val _ = debugmsg ">>decType0: ABSTYPEdec"
819 :     in app makeAbstract abstycs;
820 :     redefineEq body';
821 :     ABSTYPEdec{abstycs=abstycs,withtycs=withtycs,body=body'}
822 :     end
823 :     | MARKdec(dec,region) => MARKdec(decType0(dec,occ,region),region)
824 :    
825 :     (*
826 :     * The next several declarations will never be seen ordinarily;
827 :     * they are for re-typechecking after the instrumentation phase
828 :     * of debugger or profiler.
829 :     *)
830 :     | STRdec strbs => STRdec(map (strbType(occ,region)) strbs)
831 :     | ABSdec strbs => ABSdec(map (strbType(occ,region)) strbs)
832 :     | FCTdec fctbs => FCTdec(map (fctbType(occ,region)) fctbs)
833 :     | _ => decl
834 :    
835 :     and fctbType (occ,region) (FCTB{fct,def,name}) =
836 :     let fun fctexpType(FCTfct{param, argtycs, def}) =
837 :     FCTfct{param=param, def=strexpType (occ,region) def,
838 :     argtycs=argtycs}
839 :     | fctexpType(LETfct(dec,e)) =
840 :     LETfct(decType0(dec,LetDef occ,region), fctexpType e)
841 :     | fctexpType(MARKfct(f,region)) = MARKfct(fctexpType f,region)
842 :     | fctexpType v = v
843 :     in FCTB{fct=fct,def=fctexpType def,name=name}
844 :     end
845 :    
846 :     and strexpType (occ,region) (se as (APPstr{oper,arg,argtycs})) = se
847 :     | strexpType (occ,region) (LETstr(dec,e)) =
848 :     LETstr(decType0(dec,LetDef occ,region), strexpType (occ,region) e)
849 :     | strexpType (occ,_) (MARKstr(e,region)) =
850 :     MARKstr(strexpType (occ,region) e, region)
851 :     | strexpType _ v = v
852 :    
853 :     and strbType (occ,region) (STRB{str,def,name}) =
854 :     STRB{str=str,def=strexpType (occ,region) def,name=name}
855 :    
856 :     val _ = debugmsg ">>decType: resetOverloaded"
857 :     val _ = resetOverloaded()
858 :     val _ = debugmsg ">>decType: OverloadedLit.reset"
859 :     val _ = OLL.reset ()
860 :     val _ = debugmsg ">>decType: calling decType0"
861 :     val dec' = decType0(dec, if toplev then Root else (LetDef Root), region);
862 :     val _ = debugmsg ">>decType: OverloadedLit.resolve"
863 :     val _ = OLL.resolve ()
864 :     val _ = debugmsg ">>decType: resolveOverloaded"
865 :     val _ = resolveOverloaded env
866 :     val _ = debugmsg "<<decType: returning"
867 :     in dec'
868 :     end (* function decType *)
869 :    
870 :     val decType = Stats.doPhase (Stats.makePhase "Compiler 035 typecheck") decType
871 :    
872 :     end (* local *)
873 :     end (* structure Typecheck *)
874 :    

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