Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] Annotation of /sml/trunk/src/compiler/Semant/types/typecheck.sml
ViewVC logotype

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

Parent Directory Parent Directory | Revision Log Revision Log


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

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

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