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

Annotation of /sml/branches/primop-branch/src/compiler/Elaborator/types/typecheck.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 1476 - (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 : macqueen 1475 (* No longer functorized to factor out dependencies on FLINT (ii2ty, ii_ispure)
15 :     * Instead, TypesUtil depends directly on InlInfo -- it calls InlInfo.pureInfo to test
16 :     * for the CAST primop in function isValue. *)
17 :    
18 :     structure Typecheck : TYPECHECK =
19 : blume 902 struct
20 :    
21 :     local open Array List Types VarCon BasicTypes TypesUtil Unify Absyn
22 :     Overload ErrorMsg PrettyPrint PPUtil PPType PPAbsyn
23 :    
24 :     structure SE = StaticEnv
25 :     (* structure II = InlInfo *)
26 :     structure DA = Access
27 :     structure EU = ElabUtil
28 :     structure ED = ElabDebug
29 :     structure OLL = OverloadLit
30 : macqueen 1344 structure PP = PrettyPrint
31 : blume 902
32 :     in
33 :    
34 :     (* debugging *)
35 :     val say = Control_Print.say
36 :     val debugging = ref false
37 :     fun debugmsg (msg: string) = if !debugging then (say msg; say "\n") else ()
38 :     val debugPrint = (fn x => ED.debugPrint debugging x)
39 :    
40 :     fun bug msg = ErrorMsg.impossible("TypeCheck: "^msg)
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 : macqueen 1475 (* the VARpat case seems designed to ensure that only one variable in a pattern
268 :     * can have generalized type variables: either x or !tvs must be nil or a bug
269 :     * message is generated. Why is this? [dbm] *)
270 : blume 902 fun generalizePat(pat: pat, userbound: tyvar list, occ: occ,
271 :     generalize: bool, region) =
272 :     let val tvs : tyvar list ref = ref []
273 :     fun gen(VARpat v) =
274 :     (let val x = generalizeTy(v,userbound,occ,generalize,region)
275 :     val _ = case (x, !tvs)
276 :     of (_::_, _::_) => bug "generalizePat 1234"
277 :     | _ => ()
278 :     in tvs := (x@(!tvs))
279 :     end)
280 :     | gen(RECORDpat{fields,...}) = app (gen o #2) fields
281 :     | gen(APPpat(_,_,arg)) = gen arg
282 :     | gen(CONSTRAINTpat(pat,_)) = gen pat
283 :     | gen(LAYEREDpat(varPat,pat)) = (gen varPat; gen pat)
284 :     | gen _ = ()
285 :     in gen pat; !tvs
286 :     end
287 :    
288 :     fun applyType(ratorTy: ty, randTy: ty) : ty =
289 :     let val resultType = mkMETAty()
290 :     in unifyTy(ratorTy, (randTy --> resultType)); resultType
291 :     end
292 :    
293 :     fun patType(pat: pat, depth, region) : pat * ty =
294 :     case pat
295 :     of WILDpat => (pat,mkMETAtyBounded depth)
296 :     | VARpat(VALvar{typ as ref UNDEFty,...}) =>
297 :     (typ := mkMETAtyBounded depth; (pat,!typ))
298 :     (* multiple occurrence due to or-pat *)
299 :     | VARpat(VALvar{typ, ...}) => (pat, !typ)
300 :     | INTpat (_,ty) => (OLL.push ty; (pat,ty))
301 :     | WORDpat (_,ty) => (OLL.push ty; (pat,ty))
302 :     | REALpat _ => (pat,realTy)
303 :     | STRINGpat _ => (pat,stringTy)
304 :     | CHARpat _ => (pat,charTy)
305 :     | RECORDpat{fields,flex,typ} =>
306 :     (* fields assumed already sorted by label *)
307 :     let fun g(lab,pat') =
308 :     let val (npat,nty) = patType(pat',depth,region)
309 :     in ((lab,npat), (lab,nty))
310 :     end
311 :     val (fields',labtys) = mapUnZip g fields
312 :     val npat = RECORDpat{fields=fields',flex=flex,typ=typ}
313 :     in if flex
314 :     then let val ty = VARty(mkTyvar(mkFLEX(labtys,depth)))
315 :     in typ := ty; (npat,ty)
316 :     end
317 :     else (npat,recordTy(labtys))
318 :     end
319 :     | VECTORpat(pats,_) =>
320 :     (let val (npats,ntys) =
321 :     mapUnZip (fn pat => patType(pat,depth,region)) pats
322 :     val nty =
323 :     foldr (fn (a,b) => (unifyTy(a,b); b)) (mkMETAtyBounded depth) ntys
324 :     in (VECTORpat(npats,nty), CONty(vectorTycon,[nty]))
325 :     end handle Unify(mode) => (
326 :     err region COMPLAIN
327 :     (message("vector pattern type failure",mode)) nullErrorBody;
328 :     (pat,WILDCARDty)))
329 :     | ORpat(p1, p2) =>
330 :     let val (p1, ty1) = patType(p1, depth, region)
331 :     val (p2, ty2) = patType(p2, depth, region)
332 :     in
333 :     unifyErr{ty1=ty1,ty2=ty2,name1="expected",name2="found",
334 :     message="or-patterns don't agree",region=region,
335 :     kind=ppPat,kindname="pattern",phrase=pat};
336 :     (ORpat(p1, p2), ty1)
337 :     end
338 :     | CONpat(dcon as DATACON{typ,...},_) =>
339 :     let val (ty, insts) = instantiatePoly typ
340 :     (* the following is to set the correct depth information
341 :     * to the type variables in ty. (ZHONG)
342 :     *)
343 :     val nty = mkMETAtyBounded depth
344 :     val _ = unifyTy(nty, ty)
345 : macqueen 1476 in (CONpat(dcon,ty),ty)
346 : blume 902 end
347 :     | APPpat(dcon as DATACON{typ,rep,...},_,arg) =>
348 :     let val (argpat,argty) = patType(arg,depth,region)
349 :     val (ty1,ndcon) = case rep
350 :     of DA.REF => (refPatType,refNewDcon dcon)
351 :     | _ => (typ,dcon)
352 :     val (ty2,insts) = instantiatePoly ty1
353 :     val npat = APPpat(ndcon,insts,argpat)
354 :     in (npat,applyType(ty2,argty))
355 :     handle Unify(mode) =>
356 :     (err region COMPLAIN
357 :     (message("constructor and argument don't agree in pattern",mode))
358 :     (fn ppstrm =>
359 :     (PPType.resetPPType();
360 : macqueen 1344 newline ppstrm;
361 :     PP.string ppstrm "constructor: ";
362 :     ppType ppstrm typ; newline ppstrm;
363 :     PP.string ppstrm "argument: ";
364 :     ppType ppstrm argty; newline ppstrm;
365 :     PP.string ppstrm "in pattern:"; break ppstrm {nsp=1,offset=2};
366 : blume 902 ppPat ppstrm (pat,!printDepth)));
367 :     (pat,WILDCARDty))
368 :     end
369 :     | CONSTRAINTpat(pat',ty) =>
370 :     let val (npat,patTy) = patType(pat',depth,region)
371 :     in if unifyErr{ty1=patTy,name1="pattern",ty2=ty,name2="constraint",
372 :     message="pattern and constraint don't agree",
373 :     region=region,kind=ppPat,kindname="pattern",phrase=pat}
374 :     then (CONSTRAINTpat(npat,ty),ty)
375 :     else (pat,WILDCARDty)
376 :     end
377 :     | LAYEREDpat(vpat as VARpat(VALvar{typ,...}),pat') =>
378 :     let val (npat,patTy) = patType(pat',depth,region)
379 :     val _ = (typ := patTy)
380 :     in (LAYEREDpat(vpat,npat),patTy)
381 :     end
382 :     | LAYEREDpat(cpat as CONSTRAINTpat(VARpat(VALvar{typ,...}),ty),pat') =>
383 :     let val (npat,patTy) = patType(pat',depth,region)
384 :     in if unifyErr{ty1=patTy,name1="pattern",ty2=ty,name2="constraint",
385 :     message="pattern and constraint don't agree",
386 :     region=region,kind=ppPat,kindname="pattern",phrase=pat}
387 :     then (typ := ty; (LAYEREDpat(cpat,npat),ty))
388 :     else (pat,WILDCARDty)
389 :     end
390 :     | p => bug "patType -- unexpected pattern"
391 :    
392 :     fun expType(exp: exp, occ: occ, region) : exp * ty =
393 : mblume 1332 let fun boolUnifyErr { ty, name, message } =
394 :     unifyErr { ty1 = ty, name1 = name, ty2 = boolTy, name2 = "",
395 :     message = message, region = region, kind = ppExp,
396 :     kindname = "expression", phrase = exp }
397 :     fun boolshortcut (con, what, e1, e2) =
398 :     let val (e1', t1) = expType (e1, occ, region)
399 :     val (e2', t2) = expType (e2, occ, region)
400 :     val m = String.concat ["operand of ", what, " is not of type bool"]
401 :     in
402 :     if boolUnifyErr { ty = t1, name = "operand", message = m }
403 :     andalso boolUnifyErr { ty = t2, name = "operand", message = m }
404 :     then (con (e1', e2'), boolTy)
405 :     else (exp, WILDCARDty)
406 :     end
407 :     in
408 : blume 902 case exp
409 : macqueen 1373 of VARexp(r as ref(VALvar{typ, ...}), _) =>
410 :     let val (ty, insts) = instantiatePoly(!typ)
411 : macqueen 1475 in (VARexp(r, ty), ty)
412 : macqueen 1373 end
413 : blume 902 | VARexp(refvar as ref(OVLDvar _),_) =>
414 :     (exp,pushOverloaded(refvar, err region))
415 :     | VARexp(r as ref ERRORvar, _) => (exp, WILDCARDty)
416 :     | CONexp(dcon as DATACON{typ,...},_) =>
417 :     let val (ty,insts) = instantiatePoly typ
418 : macqueen 1476 in (CONexp(dcon,ty), ty)
419 : blume 902 end
420 :     | INTexp (_,ty) => (OLL.push ty; (exp,ty))
421 :     | WORDexp (_,ty) => (OLL.push ty; (exp,ty))
422 :     | REALexp _ => (exp,realTy)
423 :     | STRINGexp _ => (exp,stringTy)
424 :     | CHARexp _ => (exp,charTy)
425 :     | RECORDexp fields =>
426 :     let fun h(l as LABEL{name,...},exp') =
427 :     let val (nexp,nty) = expType(exp',occ,region)
428 :     in ((l,nexp),(l,nty))
429 :     end
430 :     fun extract(LABEL{name,...},t) = (name,t)
431 :     val (fields',tfields) = mapUnZip h fields
432 :     val rty = map extract (sortFields tfields)
433 :     in (RECORDexp fields',recordTy(rty))
434 :     end
435 :     | SELECTexp (l, e) =>
436 :     let val (nexp, nty) = expType(e, occ, region)
437 :     val res = mkMETAty ()
438 :     val labtys = [(EU.labsym l, res)]
439 :     val pt = VARty(mkTyvar(mkFLEX(labtys,infinity)))
440 :     in (unifyTy(pt,nty); (SELECTexp(l, nexp), res))
441 :     handle Unify(mode) =>
442 :     (err region COMPLAIN
443 :     (message("selecting a non-existing field from a record",mode))
444 :     (fn ppstrm =>
445 :     (PPType.resetPPType();
446 : macqueen 1344 newline ppstrm;
447 :     PP.string ppstrm "the field name: ";
448 : blume 902 (case l of LABEL{name,...} => ppSym ppstrm name);
449 : macqueen 1344 newline ppstrm;
450 :     PP.string ppstrm "the record type: ";
451 :     ppType ppstrm nty; newline ppstrm;
452 :     PP.string ppstrm "in expression:";
453 :     break ppstrm {nsp=1,offset=2};
454 : blume 902 ppExp ppstrm (exp,!printDepth)));
455 :     (exp, WILDCARDty))
456 :     end
457 :     | VECTORexp(exps,_) =>
458 :     (let val (exps',nty) = mapUnZip (fn e => expType(e,occ,region)) exps
459 :     val vty = foldr (fn (a,b) => (unifyTy(a,b); b)) (mkMETAty()) nty
460 :     in (VECTORexp(exps',vty), CONty(vectorTycon,[vty]))
461 :     end handle Unify(mode) =>
462 :     (err region COMPLAIN
463 :     (message("vector expression type failure",mode))
464 :     nullErrorBody; (exp,WILDCARDty)))
465 :     | SEQexp exps =>
466 :     let fun scan nil = (nil,unitTy)
467 :     | scan [e] =
468 :     let val (e',ety) = expType(e,occ,region)
469 :     in ([e'],ety)
470 :     end
471 :     | scan (e::rest) =
472 :     let val (e',_) = expType(e,occ,region)
473 :     val (el',ety) = scan rest
474 :     in (e'::el',ety)
475 :     end
476 :     val (exps',expty) = scan exps
477 :     in (SEQexp exps',expty)
478 :     end
479 :     | APPexp(rator, rand) =>
480 :     let val (rator',ratorTy) = expType(rator,occ,region)
481 :     val (rand',randTy) = expType(rand,occ,region)
482 :     val exp' = APPexp(rator',rand')
483 :     in (exp',applyType(ratorTy,randTy))
484 :     handle Unify(mode) =>
485 :     let val ratorTy = prune ratorTy
486 :     val reducedRatorTy = headReduceType ratorTy
487 :     in PPType.resetPPType();
488 :     if isArrowType(reducedRatorTy)
489 :     then (err region COMPLAIN
490 :     (message("operator and operand don't agree",mode))
491 :     (fn ppstrm =>
492 : macqueen 1344 (newline ppstrm;
493 :     PP.string ppstrm "operator domain: ";
494 : blume 902 ppType ppstrm (domain reducedRatorTy);
495 : macqueen 1344 newline ppstrm;
496 :     PP.string ppstrm "operand: ";
497 :     ppType ppstrm randTy; newline ppstrm;
498 :     PP.string ppstrm "in expression:";
499 :     break ppstrm {nsp=1,offset=2};
500 : blume 902 ppExp ppstrm (exp,!printDepth)));
501 :     (exp,WILDCARDty))
502 :     else (err region COMPLAIN
503 :     (message("operator is not a function",mode))
504 :     (fn ppstrm =>
505 : macqueen 1344 (newline ppstrm;
506 :     PP.string ppstrm "operator: ";
507 :     ppType ppstrm (ratorTy); newline ppstrm;
508 :     PP.string ppstrm "in expression:";
509 :     break ppstrm {nsp=1,offset=2};
510 : blume 902 ppExp ppstrm (exp,!printDepth)));
511 :     (exp,WILDCARDty))
512 :     end
513 :     end
514 :     | CONSTRAINTexp(e,ty) =>
515 :     let val (e',ety) = expType(e,occ,region)
516 :     in if unifyErr{ty1=ety,name1="expression", ty2=ty, name2="constraint",
517 :     message="expression doesn't match constraint",
518 :     region=region,kind=ppExp,kindname="expression",
519 :     phrase=exp}
520 :     then (CONSTRAINTexp(e',ty),ty)
521 :     else (exp,WILDCARDty)
522 :     end
523 :     | HANDLEexp(e,HANDLER h) =>
524 :     let val (e',ety) = expType(e,occ,region)
525 :     and (h',hty) = expType(h,occ,region)
526 :     val exp' = HANDLEexp(e',HANDLER h')
527 :     in (unifyTy(hty, exnTy --> ety); (exp',ety))
528 :     handle Unify(mode) =>
529 :     (if unifyErr{ty1=domain(prune hty), name1="handler domain",
530 :     ty2=exnTy, name2="",
531 :     message="handler domain is not exn",
532 :     region=region,kind=ppExp,kindname="expression",
533 :     phrase=exp}
534 :     then unifyErr{ty1=ety, name1="body",
535 :     ty2=range(prune hty), name2="handler range",
536 :     message="expression and handler don't agree",
537 :     region=region,
538 :     kind=ppExp,kindname="expression",phrase=exp}
539 :     else false;
540 :     (exp,WILDCARDty))
541 :     end
542 :     | RAISEexp(e,_) =>
543 :     let val (e',ety) = expType(e,occ,region)
544 :     val newty = mkMETAty()
545 :     in unifyErr{ty1=ety, name1="raised", ty2=exnTy, name2="",
546 :     message="argument of raise is not an exception",
547 :     region=region,kind=ppExp,kindname="expression",phrase=exp};
548 :     (RAISEexp(e',newty),newty)
549 :     end
550 :     | LETexp(d,e) =>
551 :     let val d' = decType0(d,LetDef(occ),region)
552 :     val (e',ety) = expType(e,occ,region)
553 :     in (LETexp(d',e'),ety)
554 :     end
555 :     | CASEexp(e,rules,isMatch) =>
556 :     let val (e',ety) = expType(e,occ,region)
557 :     val (rules',_,rty) = matchType(rules,occ,region)
558 :     val exp' = CASEexp(e',rules', isMatch)
559 :     in (exp',applyType(rty,ety))
560 :     handle Unify(mode) =>
561 :     (if isMatch then
562 :     unifyErr{ty1=domain rty, name1="rule domain",
563 :     ty2=ety, name2="object",
564 :     message="case object and rules don't agree",
565 :     region=region,kind=ppExp,kindname="expression",phrase=exp}
566 :     else
567 :     let val decl = case rules
568 :     of (RULE(pat,_))::_ =>
569 :     VB{pat=pat,exp=exp,tyvars=ref[],boundtvs=[]}
570 :     | _ => bug "unexpected rule list 456"
571 :     in unifyErr{ty1=domain rty, name1="pattern",
572 :     ty2=ety, name2="expression",
573 :     message="pattern and expression in val dec don't agree",
574 :     region=region,kind=ppVB,kindname="declaration",
575 :     phrase=decl}
576 :     end;
577 :     (exp,WILDCARDty))
578 :     end
579 :     (* this causes case to behave differently from let, i.e.
580 :     bound variables do not have generic types *)
581 : mblume 1332 | IFexp { test, thenCase, elseCase } =>
582 :     let val (test', tty) = expType (test, occ, region)
583 :     val (thenCase', tct) = expType (thenCase, occ, region)
584 :     val (elseCase', ect) = expType (elseCase, occ, region)
585 :     in
586 :     if boolUnifyErr
587 :     { ty = tty, name = "test expression",
588 :     message="test expression in if is not of type bool" }
589 :     andalso
590 :     unifyErr { ty1 = tct, name1 = "then branch",
591 :     ty2 = ect, name2 = "else branch",
592 :     message="types of if branches do not agree",
593 :     region = region, kind = ppExp,
594 :     kindname = "expression", phrase = exp }
595 :     then
596 :     (IFexp { test = test', thenCase = thenCase',
597 :     elseCase = elseCase' },
598 :     tct)
599 :     else
600 :     (exp, WILDCARDty)
601 :     end
602 :     | ANDALSOexp (e1, e2) =>
603 :     boolshortcut (ANDALSOexp, "andalso", e1, e2)
604 :     | ORELSEexp (e1, e2) =>
605 :     boolshortcut (ORELSEexp, "orelse", e1, e2)
606 :     | WHILEexp { test, expr } =>
607 :     let val (test', tty) = expType (test, occ, region)
608 :     val (expr', _) = expType (expr, occ, region)
609 :     in
610 :     if boolUnifyErr { ty = tty, name = "test expression",
611 :     message = "test expression in while is not of type bool" }
612 :     then
613 :     (WHILEexp { test = test', expr = expr' }, unitTy)
614 :     else
615 :     (exp, WILDCARDty)
616 :     end
617 : blume 902 | FNexp(rules,_) =>
618 :     let val (rules',ty,rty) = matchType(rules,occ,region)
619 :     in (FNexp(rules',ty),rty)
620 :     end
621 :     | MARKexp(e,region) =>
622 :     let val (e',et) = expType(e,occ,region)
623 :     in (MARKexp(e',region),et)
624 :     end
625 :     | _ => bug "exptype -- bad expression"
626 : mblume 1332 end
627 : blume 902
628 :     and ruleType(RULE(pat,exp),occ,region) =
629 :     let val occ = Abstr occ
630 :     val (pat',pty) = patType(pat,lamdepth occ,region)
631 :     val (exp',ety) = expType(exp,occ,region)
632 :     in (RULE(pat',exp'),pty,pty --> ety)
633 :     end
634 :    
635 :     and matchType(l,occ,region) =
636 :     case l
637 :     of [] => bug "empty rule list in typecheck.matchType"
638 :     | [rule] =>
639 :     let val (rule0,argt,rty) = ruleType(rule,occ,region)
640 :     in ([rule0],argt,rty)
641 :     end
642 :     | rule::rest =>
643 :     let val (rule0,argt,rty) = ruleType(rule,occ,region)
644 :     fun checkrule rule' =
645 :     let val (rule1,argt',rty') = ruleType(rule',occ,region)
646 :     in unifyErr{ty1=rty,ty2=rty', name1="earlier rule(s)",
647 :     name2="this rule",
648 :     message="types of rules don't agree",
649 :     region=region,
650 :     kind=ppRule,kindname="rule",phrase=rule'};
651 :     rule1
652 :     end
653 :     in (rule0::(map checkrule rest),argt,rty)
654 :     end
655 :    
656 :     and decType0(decl,occ,region) : dec =
657 :     case decl
658 :     of VALdec vbs =>
659 :     let fun vbType(vb as VB{pat, exp, tyvars=(tv as (ref tyvars)), boundtvs}) =
660 :     let val (pat',pty) = patType(pat,infinity,region)
661 :     val (exp',ety) = expType(exp,occ,region)
662 :     val generalize = isValue exp (* orelse isVarTy ety *)
663 :     in unifyErr{ty1=pty,ty2=ety, name1="pattern", name2="expression",
664 :     message="pattern and expression in val dec don't agree",
665 :     region=region,kind=ppVB,kindname="declaration",
666 :     phrase=vb};
667 :     VB{pat=pat',exp=exp',tyvars=tv,
668 :     boundtvs=generalizePat(pat,tyvars,occ,generalize,region)}
669 :     end
670 :     val _ = debugmsg ">>decType0: VALdec"
671 :     in VALdec(map vbType vbs)
672 :     end
673 :    
674 :     | VALRECdec(rvbs) =>
675 :     let val occ = Abstr occ
676 :    
677 :     (* First go through and type-check all the patterns and
678 :     result-constraints, unifying with each other and with
679 :     the specified result type.
680 :     *)
681 :     fun setType(rvb as RVB{var=VALvar{typ,...},exp,resultty,...}) =
682 :     let val domainty = mkMETAtyBounded(lamdepth occ)
683 :     val rangety = mkMETAtyBounded(lamdepth occ)
684 :    
685 :     val funty = domainty --> rangety
686 :    
687 :     val _ =
688 :     case resultty
689 :     of NONE => true
690 :     | SOME ty =>
691 :     unifyErr{ty1=funty,ty2=ty,
692 :     name1="",name2="constraint",
693 :     message="type constraint of val rec dec\
694 :     \ is not a function type",
695 :     region=region,kind=ppRVB,
696 :     kindname="declaration", phrase=rvb}
697 :    
698 :     fun f(FNexp(rules,_), region, funty) =
699 :     let fun unify a =
700 :     (unifyErr{ty1=a,name1="this clause",
701 :     ty2=funty,name2="previous clauses",
702 :     message="parameter or result constraints\
703 :     \ of clauses don't agree",
704 :     region=region,kind=ppRVB,
705 :     kindname="declaration", phrase=rvb};
706 :     ())
707 :    
708 :     fun approxRuleTy(RULE(pat,e)) =
709 :     let val (pat',pty) =
710 :     patType(pat,lamdepth occ,region)
711 :     in case e
712 :     of CONSTRAINTexp(e,ty) =>
713 :     (pat',pty-->ty,(e,region))
714 :     | e => (pat',pty-->rangety,(e,region))
715 :     end
716 :    
717 :     val patTyExps = map approxRuleTy rules
718 :     val pats = map #1 patTyExps
719 :     val tys = map #2 patTyExps
720 :     val exps = map #3 patTyExps
721 :    
722 :     fun doExp (e,region) =
723 :     let val (exp', ety) = expType(e,occ,region)
724 :     in unifyErr{ty1=ety, name1="expression",
725 :     ty2=rangety, name2="result type",
726 :     message="right-hand-side of clause\
727 :     \ doesn't agree with function result type",
728 :     region=region,kind=ppRVB,
729 :     kindname="declaration",phrase=rvb};
730 :     exp'
731 :     end
732 :    
733 :     in app unify tys;
734 :     typ := funty;
735 :     fn()=>
736 :     FNexp(ListPair.map RULE (pats, map doExp exps),
737 :     domain(prune(funty)))
738 :     end
739 :     | f(MARKexp(e,region),_,funty) =
740 :     let val build = f(e,region,funty)
741 :     in fn()=> MARKexp(build(), region)
742 :     end
743 :     | f(CONSTRAINTexp(e,ty),region,funty) =
744 :     let val _ =
745 :     unifyErr{ty1=ty, name1="this constraint",
746 :     ty2=funty, name2="outer constraints",
747 :     message="type constraints on val rec\
748 :     \ declaraction disagree",
749 :     region=region,kind=ppRVB,
750 :     kindname="declaration", phrase=rvb}
751 :     val build = f(e,region,funty)
752 :     in fn()=> CONSTRAINTexp(build(), ty)
753 :     end
754 :     | f _ = bug "typecheck.823"
755 :     in f(exp,region,funty)
756 :     end
757 :     | setType _ = bug "setType"
758 :    
759 :     (* Second, go through and type-check the right-hand-side
760 :     expressions (function bodies) *)
761 :     fun rvbType(RVB{var=v,resultty,tyvars,boundtvs,...}, build) =
762 :     RVB{var=v,exp=build(), resultty=resultty,tyvars=tyvars,
763 :     boundtvs=boundtvs}
764 :    
765 :     val _ = debugmsg ">>decType0: VALRECdec"
766 :     val builders = map setType rvbs
767 :     val rvbs' = ListPair.map rvbType (rvbs,builders)
768 :     (* No need to generalize here, because every VALRECdec is
769 :     wrapped in a VALdec, and the generalization occurs at the
770 :     outer level. Previously: val rvbs'' = map genType rvbs' *)
771 :     in EU.recDecs rvbs'
772 :     end
773 :    
774 :     | EXCEPTIONdec(ebs) =>
775 :     let fun check(VARty(ref(UBOUND _))) =
776 :     err region COMPLAIN
777 :     "type variable in top level exception type"
778 :     nullErrorBody
779 :     | check(CONty(_,args)) =
780 :     app check args
781 :     | check _ = ()
782 :     fun ebType(EBgen{etype=SOME ty,...}) = check ty
783 :     | ebType _ = ()
784 :     val _ = debugmsg ">>decType0: EXCEPTIONdec"
785 :     in if TypesUtil.lamdepth occ < 1 then app ebType ebs else ();
786 :     decl
787 :     end
788 :     | LOCALdec(decIn,decOut) =>
789 :     let val decIn' = decType0(decIn,LetDef occ,region)
790 :     val decOut' = decType0(decOut,occ,region)
791 :     val _ = debugmsg ">>decType0: LOCALdec"
792 :     in LOCALdec(decIn',decOut')
793 :     end
794 :     | SEQdec(decls) =>
795 :     SEQdec(map (fn decl => decType0(decl,occ,region)) decls)
796 :     | ABSTYPEdec{abstycs,withtycs,body} =>
797 :     let fun makeAbstract(GENtyc { eq, ... }) = eq := ABS
798 :     | makeAbstract _ = bug "makeAbstract"
799 :     fun redefineEq(DATATYPEdec{datatycs,...}) =
800 :     let fun setDATA (GENtyc { eq, ... }) = eq := DATA
801 :     | setDATA _ = ()
802 :     in
803 :     app setDATA datatycs;
804 :     EqTypes.defineEqProps(datatycs,nil,EntityEnv.empty)
805 :     end
806 :     | redefineEq(SEQdec decs) = app redefineEq decs
807 :     | redefineEq(LOCALdec(din,dout)) =
808 :     (redefineEq din; redefineEq dout)
809 :     | redefineEq(MARKdec(dec,_)) = redefineEq dec
810 :     | redefineEq _ = ()
811 :     val body'= decType0(body,occ,region)
812 :     val _ = debugmsg ">>decType0: ABSTYPEdec"
813 :     in app makeAbstract abstycs;
814 :     redefineEq body';
815 :     ABSTYPEdec{abstycs=abstycs,withtycs=withtycs,body=body'}
816 :     end
817 :     | MARKdec(dec,region) => MARKdec(decType0(dec,occ,region),region)
818 :    
819 :     (*
820 :     * The next several declarations will never be seen ordinarily;
821 :     * they are for re-typechecking after the instrumentation phase
822 :     * of debugger or profiler.
823 :     *)
824 :     | STRdec strbs => STRdec(map (strbType(occ,region)) strbs)
825 :     | ABSdec strbs => ABSdec(map (strbType(occ,region)) strbs)
826 :     | FCTdec fctbs => FCTdec(map (fctbType(occ,region)) fctbs)
827 :     | _ => decl
828 :    
829 :     and fctbType (occ,region) (FCTB{fct,def,name}) =
830 :     let fun fctexpType(FCTfct{param, argtycs, def}) =
831 :     FCTfct{param=param, def=strexpType (occ,region) def,
832 :     argtycs=argtycs}
833 :     | fctexpType(LETfct(dec,e)) =
834 :     LETfct(decType0(dec,LetDef occ,region), fctexpType e)
835 :     | fctexpType(MARKfct(f,region)) = MARKfct(fctexpType f,region)
836 :     | fctexpType v = v
837 :     in FCTB{fct=fct,def=fctexpType def,name=name}
838 :     end
839 :    
840 :     and strexpType (occ,region) (se as (APPstr{oper,arg,argtycs})) = se
841 :     | strexpType (occ,region) (LETstr(dec,e)) =
842 :     LETstr(decType0(dec,LetDef occ,region), strexpType (occ,region) e)
843 :     | strexpType (occ,_) (MARKstr(e,region)) =
844 :     MARKstr(strexpType (occ,region) e, region)
845 :     | strexpType _ v = v
846 :    
847 :     and strbType (occ,region) (STRB{str,def,name}) =
848 :     STRB{str=str,def=strexpType (occ,region) def,name=name}
849 :    
850 :     val _ = debugmsg ">>decType: resetOverloaded"
851 :     val _ = resetOverloaded()
852 :     val _ = debugmsg ">>decType: OverloadedLit.reset"
853 :     val _ = OLL.reset ()
854 :     val _ = debugmsg ">>decType: calling decType0"
855 :     val dec' = decType0(dec, if toplev then Root else (LetDef Root), region);
856 :     val _ = debugmsg ">>decType: OverloadedLit.resolve"
857 :     val _ = OLL.resolve ()
858 :     val _ = debugmsg ">>decType: resolveOverloaded"
859 :     val _ = resolveOverloaded env
860 :     val _ = debugmsg "<<decType: returning"
861 :     in dec'
862 :     end (* function decType *)
863 :    
864 :     val decType = Stats.doPhase (Stats.makePhase "Compiler 035 typecheck") decType
865 :    
866 :     end (* local *)
867 :     end (* structure Typecheck *)
868 :    

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