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 1373 - (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 : macqueen 1373 (* PRIMOP: val ii2ty : II.ii -> Types.ty option *)) : TYPECHECK =
17 : blume 902 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 : macqueen 1373 of VARexp(r as ref(VALvar{typ, ...}), _) =>
407 :     let val (ty, insts) = instantiatePoly(!typ)
408 :     in (VARexp(r, insts), ty)
409 :     end
410 :     (* PRIMOP:
411 : blume 902 (case ii2ty info of
412 :     SOME st =>
413 :     let val (sty, insts) = instantiatePoly(st)
414 :     val (nty, _) = instantiatePoly(!typ)
415 :     in
416 :     unifyTy(sty, nty) handle _ => (); (* ??? *)
417 :     (VARexp(r, insts), sty)
418 :     end
419 :     | NONE =>
420 :     let val (ty, insts) = instantiatePoly(!typ)
421 :     in (VARexp(r, insts), ty)
422 :     end)
423 : macqueen 1373 *)
424 : blume 902 | VARexp(refvar as ref(OVLDvar _),_) =>
425 :     (exp,pushOverloaded(refvar, err region))
426 :     | VARexp(r as ref ERRORvar, _) => (exp, WILDCARDty)
427 :     | CONexp(dcon as DATACON{typ,...},_) =>
428 :     let val (ty,insts) = instantiatePoly typ
429 :     in (CONexp(dcon,insts),ty)
430 :     end
431 :     | INTexp (_,ty) => (OLL.push ty; (exp,ty))
432 :     | WORDexp (_,ty) => (OLL.push ty; (exp,ty))
433 :     | REALexp _ => (exp,realTy)
434 :     | STRINGexp _ => (exp,stringTy)
435 :     | CHARexp _ => (exp,charTy)
436 :     | RECORDexp fields =>
437 :     let fun h(l as LABEL{name,...},exp') =
438 :     let val (nexp,nty) = expType(exp',occ,region)
439 :     in ((l,nexp),(l,nty))
440 :     end
441 :     fun extract(LABEL{name,...},t) = (name,t)
442 :     val (fields',tfields) = mapUnZip h fields
443 :     val rty = map extract (sortFields tfields)
444 :     in (RECORDexp fields',recordTy(rty))
445 :     end
446 :     | SELECTexp (l, e) =>
447 :     let val (nexp, nty) = expType(e, occ, region)
448 :     val res = mkMETAty ()
449 :     val labtys = [(EU.labsym l, res)]
450 :     val pt = VARty(mkTyvar(mkFLEX(labtys,infinity)))
451 :     in (unifyTy(pt,nty); (SELECTexp(l, nexp), res))
452 :     handle Unify(mode) =>
453 :     (err region COMPLAIN
454 :     (message("selecting a non-existing field from a record",mode))
455 :     (fn ppstrm =>
456 :     (PPType.resetPPType();
457 : macqueen 1344 newline ppstrm;
458 :     PP.string ppstrm "the field name: ";
459 : blume 902 (case l of LABEL{name,...} => ppSym ppstrm name);
460 : macqueen 1344 newline ppstrm;
461 :     PP.string ppstrm "the record type: ";
462 :     ppType ppstrm nty; newline ppstrm;
463 :     PP.string ppstrm "in expression:";
464 :     break ppstrm {nsp=1,offset=2};
465 : blume 902 ppExp ppstrm (exp,!printDepth)));
466 :     (exp, WILDCARDty))
467 :     end
468 :     | VECTORexp(exps,_) =>
469 :     (let val (exps',nty) = mapUnZip (fn e => expType(e,occ,region)) exps
470 :     val vty = foldr (fn (a,b) => (unifyTy(a,b); b)) (mkMETAty()) nty
471 :     in (VECTORexp(exps',vty), CONty(vectorTycon,[vty]))
472 :     end handle Unify(mode) =>
473 :     (err region COMPLAIN
474 :     (message("vector expression type failure",mode))
475 :     nullErrorBody; (exp,WILDCARDty)))
476 :     | SEQexp exps =>
477 :     let fun scan nil = (nil,unitTy)
478 :     | scan [e] =
479 :     let val (e',ety) = expType(e,occ,region)
480 :     in ([e'],ety)
481 :     end
482 :     | scan (e::rest) =
483 :     let val (e',_) = expType(e,occ,region)
484 :     val (el',ety) = scan rest
485 :     in (e'::el',ety)
486 :     end
487 :     val (exps',expty) = scan exps
488 :     in (SEQexp exps',expty)
489 :     end
490 :     | APPexp(rator, rand) =>
491 :     let val (rator',ratorTy) = expType(rator,occ,region)
492 :     val (rand',randTy) = expType(rand,occ,region)
493 :     val exp' = APPexp(rator',rand')
494 :     in (exp',applyType(ratorTy,randTy))
495 :     handle Unify(mode) =>
496 :     let val ratorTy = prune ratorTy
497 :     val reducedRatorTy = headReduceType ratorTy
498 :     in PPType.resetPPType();
499 :     if isArrowType(reducedRatorTy)
500 :     then (err region COMPLAIN
501 :     (message("operator and operand don't agree",mode))
502 :     (fn ppstrm =>
503 : macqueen 1344 (newline ppstrm;
504 :     PP.string ppstrm "operator domain: ";
505 : blume 902 ppType ppstrm (domain reducedRatorTy);
506 : macqueen 1344 newline ppstrm;
507 :     PP.string ppstrm "operand: ";
508 :     ppType ppstrm randTy; newline ppstrm;
509 :     PP.string ppstrm "in expression:";
510 :     break ppstrm {nsp=1,offset=2};
511 : blume 902 ppExp ppstrm (exp,!printDepth)));
512 :     (exp,WILDCARDty))
513 :     else (err region COMPLAIN
514 :     (message("operator is not a function",mode))
515 :     (fn ppstrm =>
516 : macqueen 1344 (newline ppstrm;
517 :     PP.string ppstrm "operator: ";
518 :     ppType ppstrm (ratorTy); newline ppstrm;
519 :     PP.string ppstrm "in expression:";
520 :     break ppstrm {nsp=1,offset=2};
521 : blume 902 ppExp ppstrm (exp,!printDepth)));
522 :     (exp,WILDCARDty))
523 :     end
524 :     end
525 :     | CONSTRAINTexp(e,ty) =>
526 :     let val (e',ety) = expType(e,occ,region)
527 :     in if unifyErr{ty1=ety,name1="expression", ty2=ty, name2="constraint",
528 :     message="expression doesn't match constraint",
529 :     region=region,kind=ppExp,kindname="expression",
530 :     phrase=exp}
531 :     then (CONSTRAINTexp(e',ty),ty)
532 :     else (exp,WILDCARDty)
533 :     end
534 :     | HANDLEexp(e,HANDLER h) =>
535 :     let val (e',ety) = expType(e,occ,region)
536 :     and (h',hty) = expType(h,occ,region)
537 :     val exp' = HANDLEexp(e',HANDLER h')
538 :     in (unifyTy(hty, exnTy --> ety); (exp',ety))
539 :     handle Unify(mode) =>
540 :     (if unifyErr{ty1=domain(prune hty), name1="handler domain",
541 :     ty2=exnTy, name2="",
542 :     message="handler domain is not exn",
543 :     region=region,kind=ppExp,kindname="expression",
544 :     phrase=exp}
545 :     then unifyErr{ty1=ety, name1="body",
546 :     ty2=range(prune hty), name2="handler range",
547 :     message="expression and handler don't agree",
548 :     region=region,
549 :     kind=ppExp,kindname="expression",phrase=exp}
550 :     else false;
551 :     (exp,WILDCARDty))
552 :     end
553 :     | RAISEexp(e,_) =>
554 :     let val (e',ety) = expType(e,occ,region)
555 :     val newty = mkMETAty()
556 :     in unifyErr{ty1=ety, name1="raised", ty2=exnTy, name2="",
557 :     message="argument of raise is not an exception",
558 :     region=region,kind=ppExp,kindname="expression",phrase=exp};
559 :     (RAISEexp(e',newty),newty)
560 :     end
561 :     | LETexp(d,e) =>
562 :     let val d' = decType0(d,LetDef(occ),region)
563 :     val (e',ety) = expType(e,occ,region)
564 :     in (LETexp(d',e'),ety)
565 :     end
566 :     | CASEexp(e,rules,isMatch) =>
567 :     let val (e',ety) = expType(e,occ,region)
568 :     val (rules',_,rty) = matchType(rules,occ,region)
569 :     val exp' = CASEexp(e',rules', isMatch)
570 :     in (exp',applyType(rty,ety))
571 :     handle Unify(mode) =>
572 :     (if isMatch then
573 :     unifyErr{ty1=domain rty, name1="rule domain",
574 :     ty2=ety, name2="object",
575 :     message="case object and rules don't agree",
576 :     region=region,kind=ppExp,kindname="expression",phrase=exp}
577 :     else
578 :     let val decl = case rules
579 :     of (RULE(pat,_))::_ =>
580 :     VB{pat=pat,exp=exp,tyvars=ref[],boundtvs=[]}
581 :     | _ => bug "unexpected rule list 456"
582 :     in unifyErr{ty1=domain rty, name1="pattern",
583 :     ty2=ety, name2="expression",
584 :     message="pattern and expression in val dec don't agree",
585 :     region=region,kind=ppVB,kindname="declaration",
586 :     phrase=decl}
587 :     end;
588 :     (exp,WILDCARDty))
589 :     end
590 :     (* this causes case to behave differently from let, i.e.
591 :     bound variables do not have generic types *)
592 : mblume 1332 | IFexp { test, thenCase, elseCase } =>
593 :     let val (test', tty) = expType (test, occ, region)
594 :     val (thenCase', tct) = expType (thenCase, occ, region)
595 :     val (elseCase', ect) = expType (elseCase, occ, region)
596 :     in
597 :     if boolUnifyErr
598 :     { ty = tty, name = "test expression",
599 :     message="test expression in if is not of type bool" }
600 :     andalso
601 :     unifyErr { ty1 = tct, name1 = "then branch",
602 :     ty2 = ect, name2 = "else branch",
603 :     message="types of if branches do not agree",
604 :     region = region, kind = ppExp,
605 :     kindname = "expression", phrase = exp }
606 :     then
607 :     (IFexp { test = test', thenCase = thenCase',
608 :     elseCase = elseCase' },
609 :     tct)
610 :     else
611 :     (exp, WILDCARDty)
612 :     end
613 :     | ANDALSOexp (e1, e2) =>
614 :     boolshortcut (ANDALSOexp, "andalso", e1, e2)
615 :     | ORELSEexp (e1, e2) =>
616 :     boolshortcut (ORELSEexp, "orelse", e1, e2)
617 :     | WHILEexp { test, expr } =>
618 :     let val (test', tty) = expType (test, occ, region)
619 :     val (expr', _) = expType (expr, occ, region)
620 :     in
621 :     if boolUnifyErr { ty = tty, name = "test expression",
622 :     message = "test expression in while is not of type bool" }
623 :     then
624 :     (WHILEexp { test = test', expr = expr' }, unitTy)
625 :     else
626 :     (exp, WILDCARDty)
627 :     end
628 : blume 902 | FNexp(rules,_) =>
629 :     let val (rules',ty,rty) = matchType(rules,occ,region)
630 :     in (FNexp(rules',ty),rty)
631 :     end
632 :     | MARKexp(e,region) =>
633 :     let val (e',et) = expType(e,occ,region)
634 :     in (MARKexp(e',region),et)
635 :     end
636 :     | _ => bug "exptype -- bad expression"
637 : mblume 1332 end
638 : blume 902
639 :     and ruleType(RULE(pat,exp),occ,region) =
640 :     let val occ = Abstr occ
641 :     val (pat',pty) = patType(pat,lamdepth occ,region)
642 :     val (exp',ety) = expType(exp,occ,region)
643 :     in (RULE(pat',exp'),pty,pty --> ety)
644 :     end
645 :    
646 :     and matchType(l,occ,region) =
647 :     case l
648 :     of [] => bug "empty rule list in typecheck.matchType"
649 :     | [rule] =>
650 :     let val (rule0,argt,rty) = ruleType(rule,occ,region)
651 :     in ([rule0],argt,rty)
652 :     end
653 :     | rule::rest =>
654 :     let val (rule0,argt,rty) = ruleType(rule,occ,region)
655 :     fun checkrule rule' =
656 :     let val (rule1,argt',rty') = ruleType(rule',occ,region)
657 :     in unifyErr{ty1=rty,ty2=rty', name1="earlier rule(s)",
658 :     name2="this rule",
659 :     message="types of rules don't agree",
660 :     region=region,
661 :     kind=ppRule,kindname="rule",phrase=rule'};
662 :     rule1
663 :     end
664 :     in (rule0::(map checkrule rest),argt,rty)
665 :     end
666 :    
667 :     and decType0(decl,occ,region) : dec =
668 :     case decl
669 :     of VALdec vbs =>
670 :     let fun vbType(vb as VB{pat, exp, tyvars=(tv as (ref tyvars)), boundtvs}) =
671 :     let val (pat',pty) = patType(pat,infinity,region)
672 :     val (exp',ety) = expType(exp,occ,region)
673 :     val generalize = isValue exp (* orelse isVarTy ety *)
674 :     in unifyErr{ty1=pty,ty2=ety, name1="pattern", name2="expression",
675 :     message="pattern and expression in val dec don't agree",
676 :     region=region,kind=ppVB,kindname="declaration",
677 :     phrase=vb};
678 :     VB{pat=pat',exp=exp',tyvars=tv,
679 :     boundtvs=generalizePat(pat,tyvars,occ,generalize,region)}
680 :     end
681 :     val _ = debugmsg ">>decType0: VALdec"
682 :     in VALdec(map vbType vbs)
683 :     end
684 :    
685 :     | VALRECdec(rvbs) =>
686 :     let val occ = Abstr occ
687 :    
688 :     (* First go through and type-check all the patterns and
689 :     result-constraints, unifying with each other and with
690 :     the specified result type.
691 :     *)
692 :     fun setType(rvb as RVB{var=VALvar{typ,...},exp,resultty,...}) =
693 :     let val domainty = mkMETAtyBounded(lamdepth occ)
694 :     val rangety = mkMETAtyBounded(lamdepth occ)
695 :    
696 :     val funty = domainty --> rangety
697 :    
698 :     val _ =
699 :     case resultty
700 :     of NONE => true
701 :     | SOME ty =>
702 :     unifyErr{ty1=funty,ty2=ty,
703 :     name1="",name2="constraint",
704 :     message="type constraint of val rec dec\
705 :     \ is not a function type",
706 :     region=region,kind=ppRVB,
707 :     kindname="declaration", phrase=rvb}
708 :    
709 :     fun f(FNexp(rules,_), region, funty) =
710 :     let fun unify a =
711 :     (unifyErr{ty1=a,name1="this clause",
712 :     ty2=funty,name2="previous clauses",
713 :     message="parameter or result constraints\
714 :     \ of clauses don't agree",
715 :     region=region,kind=ppRVB,
716 :     kindname="declaration", phrase=rvb};
717 :     ())
718 :    
719 :     fun approxRuleTy(RULE(pat,e)) =
720 :     let val (pat',pty) =
721 :     patType(pat,lamdepth occ,region)
722 :     in case e
723 :     of CONSTRAINTexp(e,ty) =>
724 :     (pat',pty-->ty,(e,region))
725 :     | e => (pat',pty-->rangety,(e,region))
726 :     end
727 :    
728 :     val patTyExps = map approxRuleTy rules
729 :     val pats = map #1 patTyExps
730 :     val tys = map #2 patTyExps
731 :     val exps = map #3 patTyExps
732 :    
733 :     fun doExp (e,region) =
734 :     let val (exp', ety) = expType(e,occ,region)
735 :     in unifyErr{ty1=ety, name1="expression",
736 :     ty2=rangety, name2="result type",
737 :     message="right-hand-side of clause\
738 :     \ doesn't agree with function result type",
739 :     region=region,kind=ppRVB,
740 :     kindname="declaration",phrase=rvb};
741 :     exp'
742 :     end
743 :    
744 :     in app unify tys;
745 :     typ := funty;
746 :     fn()=>
747 :     FNexp(ListPair.map RULE (pats, map doExp exps),
748 :     domain(prune(funty)))
749 :     end
750 :     | f(MARKexp(e,region),_,funty) =
751 :     let val build = f(e,region,funty)
752 :     in fn()=> MARKexp(build(), region)
753 :     end
754 :     | f(CONSTRAINTexp(e,ty),region,funty) =
755 :     let val _ =
756 :     unifyErr{ty1=ty, name1="this constraint",
757 :     ty2=funty, name2="outer constraints",
758 :     message="type constraints on val rec\
759 :     \ declaraction disagree",
760 :     region=region,kind=ppRVB,
761 :     kindname="declaration", phrase=rvb}
762 :     val build = f(e,region,funty)
763 :     in fn()=> CONSTRAINTexp(build(), ty)
764 :     end
765 :     | f _ = bug "typecheck.823"
766 :     in f(exp,region,funty)
767 :     end
768 :     | setType _ = bug "setType"
769 :    
770 :     (* Second, go through and type-check the right-hand-side
771 :     expressions (function bodies) *)
772 :     fun rvbType(RVB{var=v,resultty,tyvars,boundtvs,...}, build) =
773 :     RVB{var=v,exp=build(), resultty=resultty,tyvars=tyvars,
774 :     boundtvs=boundtvs}
775 :    
776 :     val _ = debugmsg ">>decType0: VALRECdec"
777 :     val builders = map setType rvbs
778 :     val rvbs' = ListPair.map rvbType (rvbs,builders)
779 :     (* No need to generalize here, because every VALRECdec is
780 :     wrapped in a VALdec, and the generalization occurs at the
781 :     outer level. Previously: val rvbs'' = map genType rvbs' *)
782 :     in EU.recDecs rvbs'
783 :     end
784 :    
785 :     | EXCEPTIONdec(ebs) =>
786 :     let fun check(VARty(ref(UBOUND _))) =
787 :     err region COMPLAIN
788 :     "type variable in top level exception type"
789 :     nullErrorBody
790 :     | check(CONty(_,args)) =
791 :     app check args
792 :     | check _ = ()
793 :     fun ebType(EBgen{etype=SOME ty,...}) = check ty
794 :     | ebType _ = ()
795 :     val _ = debugmsg ">>decType0: EXCEPTIONdec"
796 :     in if TypesUtil.lamdepth occ < 1 then app ebType ebs else ();
797 :     decl
798 :     end
799 :     | LOCALdec(decIn,decOut) =>
800 :     let val decIn' = decType0(decIn,LetDef occ,region)
801 :     val decOut' = decType0(decOut,occ,region)
802 :     val _ = debugmsg ">>decType0: LOCALdec"
803 :     in LOCALdec(decIn',decOut')
804 :     end
805 :     | SEQdec(decls) =>
806 :     SEQdec(map (fn decl => decType0(decl,occ,region)) decls)
807 :     | ABSTYPEdec{abstycs,withtycs,body} =>
808 :     let fun makeAbstract(GENtyc { eq, ... }) = eq := ABS
809 :     | makeAbstract _ = bug "makeAbstract"
810 :     fun redefineEq(DATATYPEdec{datatycs,...}) =
811 :     let fun setDATA (GENtyc { eq, ... }) = eq := DATA
812 :     | setDATA _ = ()
813 :     in
814 :     app setDATA datatycs;
815 :     EqTypes.defineEqProps(datatycs,nil,EntityEnv.empty)
816 :     end
817 :     | redefineEq(SEQdec decs) = app redefineEq decs
818 :     | redefineEq(LOCALdec(din,dout)) =
819 :     (redefineEq din; redefineEq dout)
820 :     | redefineEq(MARKdec(dec,_)) = redefineEq dec
821 :     | redefineEq _ = ()
822 :     val body'= decType0(body,occ,region)
823 :     val _ = debugmsg ">>decType0: ABSTYPEdec"
824 :     in app makeAbstract abstycs;
825 :     redefineEq body';
826 :     ABSTYPEdec{abstycs=abstycs,withtycs=withtycs,body=body'}
827 :     end
828 :     | MARKdec(dec,region) => MARKdec(decType0(dec,occ,region),region)
829 :    
830 :     (*
831 :     * The next several declarations will never be seen ordinarily;
832 :     * they are for re-typechecking after the instrumentation phase
833 :     * of debugger or profiler.
834 :     *)
835 :     | STRdec strbs => STRdec(map (strbType(occ,region)) strbs)
836 :     | ABSdec strbs => ABSdec(map (strbType(occ,region)) strbs)
837 :     | FCTdec fctbs => FCTdec(map (fctbType(occ,region)) fctbs)
838 :     | _ => decl
839 :    
840 :     and fctbType (occ,region) (FCTB{fct,def,name}) =
841 :     let fun fctexpType(FCTfct{param, argtycs, def}) =
842 :     FCTfct{param=param, def=strexpType (occ,region) def,
843 :     argtycs=argtycs}
844 :     | fctexpType(LETfct(dec,e)) =
845 :     LETfct(decType0(dec,LetDef occ,region), fctexpType e)
846 :     | fctexpType(MARKfct(f,region)) = MARKfct(fctexpType f,region)
847 :     | fctexpType v = v
848 :     in FCTB{fct=fct,def=fctexpType def,name=name}
849 :     end
850 :    
851 :     and strexpType (occ,region) (se as (APPstr{oper,arg,argtycs})) = se
852 :     | strexpType (occ,region) (LETstr(dec,e)) =
853 :     LETstr(decType0(dec,LetDef occ,region), strexpType (occ,region) e)
854 :     | strexpType (occ,_) (MARKstr(e,region)) =
855 :     MARKstr(strexpType (occ,region) e, region)
856 :     | strexpType _ v = v
857 :    
858 :     and strbType (occ,region) (STRB{str,def,name}) =
859 :     STRB{str=str,def=strexpType (occ,region) def,name=name}
860 :    
861 :     val _ = debugmsg ">>decType: resetOverloaded"
862 :     val _ = resetOverloaded()
863 :     val _ = debugmsg ">>decType: OverloadedLit.reset"
864 :     val _ = OLL.reset ()
865 :     val _ = debugmsg ">>decType: calling decType0"
866 :     val dec' = decType0(dec, if toplev then Root else (LetDef Root), region);
867 :     val _ = debugmsg ">>decType: OverloadedLit.resolve"
868 :     val _ = OLL.resolve ()
869 :     val _ = debugmsg ">>decType: resolveOverloaded"
870 :     val _ = resolveOverloaded env
871 :     val _ = debugmsg "<<decType: returning"
872 :     in dec'
873 :     end (* function decType *)
874 :    
875 :     val decType = Stats.doPhase (Stats.makePhase "Compiler 035 typecheck") decType
876 :    
877 :     end (* local *)
878 :     end (* structure Typecheck *)
879 :    

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