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

SCM Repository

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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 4500 - (view) (download)

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

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