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/FLINT/flint/chkflint.sml
ViewVC logotype

Annotation of /sml/trunk/src/compiler/FLINT/flint/chkflint.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 74 - (view) (download)

1 : monnier 45 (* COPYRIGHT (c) 1997, 1998 YALE FLINT PROJECT *)
2 : monnier 16 (* chkflint.sml *)
3 :    
4 :     (* FLINT Type Checker *)
5 :    
6 :     signature CHKFLINT = sig
7 :    
8 :     (** which set of the typing rules to use while doing the typecheck *)
9 : monnier 71 type typsys (* currently very crude *)
10 : monnier 16
11 :     val checkTop : FLINT.fundec * typsys -> bool
12 :     val checkExp : FLINT.lexp * typsys -> bool
13 :    
14 :     end (* signature CHKFLINT *)
15 :    
16 :     structure ChkFlint : CHKFLINT =
17 :     struct
18 :    
19 : monnier 45 (** which set of the typing rules to use while doing the typecheck *)
20 : monnier 71 type typsys = bool (* currently very crude *)
21 : monnier 45
22 : monnier 16 local structure LT = LtyExtern
23 :     structure LV = LambdaVar
24 :     structure DA = Access
25 :     structure DI = DebIndex
26 :     structure PP = PPFlint
27 : monnier 71 structure PO = PrimOp
28 : monnier 16 open FLINT
29 :    
30 :     fun bug s = ErrorMsg.impossible ("ChkFlint: "^s)
31 :     val say = Control.Print.say
32 :     val anyerror = ref false
33 :    
34 :     (****************************************************************************
35 :     * BASIC UTILITY FUNCTIONS *
36 :     ****************************************************************************)
37 :    
38 : monnier 45 fun foldl2 (f,a,xs,ys,g) = let
39 :     val rec loop =
40 :     fn (a, nil, nil) => a
41 :     | (a, x::xs, y::ys) => loop (f (x,y,a), xs, ys)
42 :     | (a, xs', _) => g (a, xs', length xs, length ys)
43 :     in loop (a,xs,ys) end
44 :    
45 :     fun simplify (le,0) = RET [STRING "<...>"]
46 :     | simplify (le,n) =
47 :     let fun h le = simplify (le, n-1)
48 :     fun h1 (fk,v,args,le) = (fk, v, args, h le)
49 :     fun h2 (v,tvs,le) = (v, tvs, h le)
50 : monnier 16 in case le
51 : monnier 45 of LET (vs,e1,e2) => LET (vs, h e1, h e2)
52 :     | FIX (fdecs,b) => FIX (map h1 fdecs, h b)
53 :     | TFN (tdec,e) => TFN (h2 tdec, h e)
54 :     | SWITCH (v,l,dc,opp) =>
55 :     let fun g (c,x) = (c, h x)
56 :     val f = fn SOME y => SOME (h y) | NONE => NONE
57 :     in SWITCH (v, l, map g dc, f opp)
58 :     end
59 :     | CON (dc,tcs,vs,lv,le) => CON (dc, tcs, vs, lv, h le)
60 :     | RECORD (rk,vs,lv,le) => RECORD (rk, vs, lv, h le)
61 :     | SELECT (v,n,lv,le) => SELECT (v, n, lv, h le)
62 :     | HANDLE (e,v) => HANDLE (h e, v)
63 :     | PRIMOP (po,vs,lv,le) => PRIMOP (po, vs, lv, h le)
64 : monnier 16 | _ => le
65 :     end (* end of simplify *)
66 :    
67 :     (** utility functions for printing *)
68 :     val tkPrint = say o LT.tk_print
69 :     val tcPrint = say o LT.tc_print
70 :     val ltPrint = say o LT.lt_print
71 : monnier 45 fun lePrint le = PP.printLexp (simplify (le, 3))
72 :     val svPrint = PP.printSval
73 : monnier 16
74 : monnier 45 fun error (le,g) = (
75 :     anyerror := true;
76 :     say "\n************************************************************\
77 :     \\n**** FLINT type checking failed: ";
78 :     g () before (say "\n** term:\n"; lePrint le))
79 : monnier 16
80 : monnier 45 fun errMsg (le,s,r) = error (le, fn () => (say s; r))
81 : monnier 16
82 : monnier 45 fun catchExn f (le,g) =
83 :     f () handle ex => error
84 :     (le, fn () => g () before say ("\n** exception " ^ exnName ex ^ " raised"))
85 : monnier 16
86 : monnier 45 (*** a hack for type checkng ***)
87 : monnier 71 fun laterPhase postReify = postReify
88 : monnier 16
89 : monnier 45 fun check phase envs lexp = let
90 :     val ltEquiv = LT.lt_eqv_x (* should be LT.lt_eqv *)
91 : monnier 71 val ltTAppChk =
92 :     if !Control.CG.checkKinds then LT.lt_inst_chk_gen()
93 :     else fn (lt,ts,_) => LT.lt_inst(lt,ts)
94 : monnier 16
95 : monnier 45 fun constVoid _ = LT.ltc_void
96 : monnier 71 val (ltString,ltExn,ltEtag,ltVector,ltWrap,ltBool) =
97 : monnier 45 if laterPhase phase then
98 : monnier 71 (LT.ltc_string, LT.ltc_void, constVoid, constVoid, constVoid,
99 :     LT.ltc_void)
100 : monnier 45 else
101 :     (LT.ltc_string, LT.ltc_exn, LT.ltc_etag, LT.ltc_tyc o LT.tcc_vector,
102 : monnier 71 LT.ltc_tyc o LT.tcc_box, LT.ltc_bool)
103 : monnier 16
104 : monnier 45 fun prMsgLt (s,lt) = (say s; ltPrint lt)
105 : monnier 16
106 : monnier 45 fun prList f s t = let
107 :     val rec loop =
108 :     fn [] => say "<empty list>\n"
109 :     | [x] => (f x; say "\n")
110 :     | x::xs => (f x; say "\n* and\n"; loop xs)
111 :     in say s; loop t end
112 : monnier 16
113 : monnier 45 fun print2Lts (s,s',lt,lt') = (prList ltPrint s lt; prList ltPrint s' lt')
114 : monnier 16
115 : monnier 45 fun ltMatch (le,s) (t,t') =
116 :     if ltEquiv (t,t') then ()
117 :     else error
118 :     (le, fn () =>
119 :     (prMsgLt (s ^ ": Lty conflict\n** types:\n", t);
120 :     prMsgLt ("\n** and\n", t')))
121 : monnier 16
122 : monnier 45 fun ltsMatch (le,s) (ts,ts') =
123 :     foldl2 (fn (t,t',_) => ltMatch (le,s) (t,t'),
124 :     (), ts, ts',
125 :     fn (_,_,n,n') => error
126 :     (le,
127 :     fn () => print2Lts
128 :     (concat [s, ": type list mismatch (", Int.toString n, " vs ",
129 :     Int.toString n', ")\n** expected types:\n"],
130 :     "** actual types:\n",
131 :     ts, ts')))
132 : monnier 16
133 : monnier 45 local
134 :     fun ltFnAppGen opr (le,s,msg) (t,ts) =
135 :     catchExn
136 : monnier 71 (fn () => let val (xs,ys) = opr (LT.ltd_fkfun t)
137 :     in ltsMatch (le,s) (xs,ts); ys
138 :     end)
139 : monnier 45 (le, fn () => (prMsgLt (s ^ msg ^ "\n** type:\n", t); []))
140 :     in
141 :     fun ltFnApp (le,s) =
142 :     ltFnAppGen (fn x => x) (le,s,": Applying term of non-arrow type")
143 :     fun ltFnAppR (le,s) =
144 :     ltFnAppGen (fn (x,y) => (y,x)) (le,s,": Rev-app term of non-arrow type")
145 :     end
146 : monnier 16
147 : monnier 45 fun ltTyApp (le,s) (lt,ts,kenv) =
148 :     catchExn
149 :     (fn () => ltTAppChk (lt,ts,kenv))
150 :     (le,
151 :     fn () =>
152 :     (prMsgLt (s ^ ": Kind conflict\n** function Lty:\n", lt);
153 :     prList tcPrint "\n** argument Tycs:\n" ts;
154 :     []))
155 : monnier 16
156 : monnier 45 fun ltArrow (le,s) (isfct,alts,rlts) =
157 :     (case isfct
158 :     of NONE => LT.ltc_fct (alts,rlts)
159 :     | SOME raw =>
160 :     (catchExn
161 :     (fn () => LT.ltc_arrow (raw,alts,rlts))
162 :     (le,
163 :     fn () =>
164 :     (print2Lts
165 :     (s ^ ": deeply polymorphic non-functor\n** parameter types:\n",
166 :     "** result types:\n",
167 :     alts, rlts);
168 :     LT.ltc_void))))
169 : monnier 16
170 : monnier 45 (* typeInEnv : LT.tkindEnv * LT.ltyEnv * DI.depth -> lexp -> lty list *)
171 :     fun typeInEnv (kenv,venv,d) = let
172 :     fun extEnv (lv,lt,ve) = LT.ltInsert (ve,lv,lt,d)
173 :     fun bogusBind (lv,ve) = extEnv (lv,LT.ltc_void,ve)
174 :     fun typeIn venv' = typeInEnv (kenv,venv',d)
175 :     fun typeWith (v,t) = typeIn (LT.ltInsert (venv,v,t,d))
176 :     fun mismatch (le,s) (a,r,n,n') = errMsg
177 :     (le,
178 :     concat [s, ": binding/result list mismatch\n** expected ",
179 :     Int.toString n, " elements, got ", Int.toString n'],
180 :     foldl bogusBind a r)
181 : monnier 16
182 : monnier 45 fun typeof le = let
183 :     fun typeofVar lv = LT.ltLookup (venv,lv,d)
184 :     handle ltUnbound =>
185 :     errMsg (le, "Unbound Lvar " ^ LV.lvarName lv, LT.ltc_void)
186 :     val typeofVal =
187 :     fn VAR lv => typeofVar lv
188 :     | (INT _ | WORD _) => LT.ltc_int
189 :     | (INT32 _ | WORD32 _) => LT.ltc_int32
190 :     | REAL _ => LT.ltc_real
191 :     | STRING _ => LT.ltc_string
192 :     fun typeofFn ve (_,_,vts,eb) = let
193 :     fun split ((lv,t), (ve,ts)) = (LT.ltInsert (ve,lv,t,d), t::ts)
194 :     val (ve',ts) = foldr split (ve,[]) vts
195 :     in (ts, typeIn ve' eb)
196 :     end
197 : monnier 16
198 : league 74 (* There are lvars hidden in Access.conrep, used by dcon.
199 :     * These functions just make sure that they are defined in the
200 :     * current environemnent; we don't bother to typecheck them properly
201 :     * because supposedly conrep will go away...
202 :     *)
203 :     fun checkAccess (DA.LVAR v) = ignore (typeofVar v)
204 :     | checkAccess (DA.PATH (a,_)) = checkAccess a
205 :     | checkAccess _ = ()
206 :    
207 :     fun checkConrep (DA.EXN a) =
208 :     checkAccess a
209 :     | checkConrep (DA.SUSP (SOME (a1,a2))) =
210 :     (checkAccess a1;
211 :     checkAccess a2)
212 :     | checkConrep _ =
213 :     ()
214 :    
215 : monnier 45 fun chkSnglInst (fp as (le,s)) (lt,ts) =
216 :     if null ts then lt
217 :     else case ltTyApp fp (lt,ts,kenv)
218 :     of [] => LT.ltc_unit
219 :     | [lt] => lt
220 :     | lts => errMsg
221 :     (le,
222 :     concat [s, ": inst yields ", Int.toString (length lts),
223 :     " results instead of 1"],
224 :     LT.ltc_void)
225 :     fun typeWithBindingToSingleRsltOfInstAndApp (s,lt,ts,vs,lv) e = let
226 :     val fp = (le,s)
227 :     val lt = case ltFnApp fp (chkSnglInst fp (lt,ts), map typeofVal vs)
228 :     of [lt] => lt
229 :     | _ => errMsg
230 :     (le,
231 :     concat [s, ": primop/dcon must return single result type "],
232 :     LT.ltc_void)
233 :     (*
234 :     | [] => LT.ltc_unit
235 :     | lts => LT.ltc_tuple lts
236 :     (*** until PRIMOPs start returning multiple results... ***)
237 :     *)
238 :     in typeWith (lv,lt) e
239 :     end
240 : monnier 16
241 : monnier 45 fun matchAndTypeWith (s,v,lt,lt',lv,e) =
242 :     (ltMatch (le,s) (typeofVal v, lt); typeWith (lv, lt') e)
243 :     in case le
244 :     of RET vs => map typeofVal vs
245 :     | LET (lvs,e,e') =>
246 :     typeIn (foldl2 (extEnv, venv, lvs, typeof e, mismatch (le,"LET"))) e'
247 :     | FIX ([],e) =>
248 :     (say "\n**** Warning: empty declaration list in FIX\n"; typeof e)
249 :     | FIX ((fd as ((FK_FUN{isrec=NONE,...} | FK_FCT),
250 :     _, _, _)) :: fds', e) => let
251 :     val (fk, lv, _, _) = fd
252 :     val isfct = case fk of FK_FCT => NONE
253 :     | FK_FUN{fixed, ...} => SOME fixed
254 :     val (alts,rlts) = typeofFn venv fd
255 :     val lt = ltArrow (le,"non-rec FIX") (isfct,alts,rlts)
256 :     val ve = extEnv (lv,lt,venv)
257 :     val venv' =
258 :     if null fds' then ve
259 :     else errMsg
260 :     (le,
261 :     "multiple bindings in FIX, not all recursive",
262 :     foldl (fn ((_,lv,_,_), ve) => bogusBind (lv,ve)) ve fds')
263 :     in typeIn venv' e
264 :     end
265 :     | FIX (fds,e) => let
266 :     val isfct = false
267 :     fun extEnv ((FK_FCT, _, _, _), _) =
268 :     bug "unexpected case in extEnv"
269 :     | extEnv ((FK_FUN {isrec,fixed,...}, lv, vts, _) : fundec, ve) =
270 :     case (isrec, isfct)
271 :     of (SOME lts, false) => let
272 :     val lt = ltArrow (le,"FIX") (SOME fixed,
273 :     map #2 vts, lts)
274 :     in LT.ltInsert (ve,lv,lt,d)
275 :     end
276 :     | _ => let
277 :     val msg =
278 :     if isfct then "recursive functor "
279 :     else "a non-recursive function "
280 :     in errMsg (le, "in FIX: " ^ msg ^ LV.lvarName lv, ve)
281 :     end
282 :     val venv' = foldl extEnv venv fds
283 :     fun chkDcl ((FK_FUN {isrec = NONE, ...}, _, _, _) : fundec) = ()
284 :     | chkDcl (fd as (FK_FUN {isrec = SOME lts, ...}, _, _, _)) = let
285 :     in ltsMatch (le,"FIX") (lts, #2 (typeofFn venv' fd))
286 :     end
287 :     | chkDcl _ = ()
288 :     in
289 :     app chkDcl fds;
290 :     typeIn venv' e
291 :     end
292 :     | APP (v,vs) => ltFnApp (le,"APP") (typeofVal v, map typeofVal vs)
293 :     | TFN ((lv,tks,e), e') => let
294 :     val ks = map #2 tks
295 :     val lts = typeInEnv (LT.tkInsert (kenv,ks), venv, DI.next d) e
296 :     in typeWith (lv, LT.ltc_poly (ks,lts)) e'
297 :     end
298 :     | TAPP (v,ts) => ltTyApp (le,"TAPP") (typeofVal v, ts, kenv)
299 :     | SWITCH (_,_,[],_) => errMsg (le,"empty SWITCH",[])
300 :     | SWITCH (v, _, ce::ces, lo) => let
301 :     val selLty = typeofVal v
302 :     fun g lt = (ltMatch (le,"SWITCH branch 1") (lt,selLty); venv)
303 :     fun brLts (c,e) = let
304 :     val venv' = case c
305 : league 74 of DATAcon ((_,conrep,lt), ts, v) => let
306 :     val _ = checkConrep conrep
307 : monnier 45 val fp = (le,"SWITCH DECON")
308 :     val ct = chkSnglInst fp (lt,ts)
309 :     val nts = ltFnAppR fp (ct, [selLty])
310 :     in foldl2 (extEnv, venv, [v], nts, mismatch fp)
311 :     end
312 :     | (INTcon _ | WORDcon _) => g LT.ltc_int
313 :     | (INT32con _ | WORD32con _) => g LT.ltc_int32
314 :     | REALcon _ => g LT.ltc_real
315 :     | STRINGcon _ => g ltString
316 :     | VLENcon _ => g LT.ltc_int (* ? *)
317 :     in typeIn venv' e
318 :     end
319 :     val ts = brLts ce
320 :     fun chkBranch (ce,n) =
321 :     (ltsMatch (le, "SWITCH branch " ^ Int.toString n) (ts, brLts ce);
322 :     n+1)
323 :     in
324 :     foldl chkBranch 2 ces;
325 :     case lo
326 :     of SOME e => ltsMatch (le,"SWITCH else") (ts, typeof e)
327 :     | NONE => ();
328 :     ts
329 :     end
330 : league 74 | CON ((_,conrep,lt), ts, u, lv, e) =>
331 :     (checkConrep conrep;
332 :     typeWithBindingToSingleRsltOfInstAndApp ("CON",lt,ts,[u],lv) e)
333 : monnier 45 | RECORD (rk,vs,lv,e) => let
334 :     val lt = case rk
335 :     of RK_VECTOR t => let
336 :     val lt = LT.ltc_tyc t
337 :     val match = ltMatch (le,"VECTOR")
338 :     in
339 :     app (fn v => match (lt, typeofVal v)) vs;
340 :     ltVector t
341 :     end
342 :     | RK_TUPLE _ =>
343 :     if null vs then LT.ltc_unit
344 :     else let
345 :     fun chkMono v = let val t = typeofVal v
346 :     in
347 :     if LT.ltp_fct t orelse LT.ltp_poly t then
348 :     error (le, fn () =>
349 :     prMsgLt
350 :     ("RECORD: poly type in mono record:\n",t))
351 :     else ();
352 :     t
353 :     end
354 :     in LT.ltc_tuple (map chkMono vs)
355 :     end
356 :     | RK_STRUCT => LT.ltc_str (map typeofVal vs)
357 :     in typeWith (lv,lt) e
358 :     end
359 :     | SELECT (v,n,lv,e) => let
360 :     val lt = catchExn
361 :     (fn () => LT.lt_select (typeofVal v, n))
362 :     (le,
363 :     fn () =>
364 :     (say "SELECT from wrong type or out of range"; LT.ltc_void))
365 :     in typeWith (lv,lt) e
366 :     end
367 :     | RAISE (v,lts) => (ltMatch (le,"RAISE") (typeofVal v, ltExn); lts)
368 :     | HANDLE (e,v) => let val lts = typeof e
369 :     in ltFnAppR (le,"HANDLE") (typeofVal v, lts); lts
370 :     end
371 :     | BRANCH ((_,_,lt,ts), vs, e1, e2) =>
372 :     let val fp = (le, "BRANCH")
373 :     val lt =
374 :     case ltFnApp fp (chkSnglInst fp (lt,ts), map typeofVal vs)
375 :     of [lt] => lt
376 :     | _ => errMsg
377 :     (le,
378 :     "BRANCK : primop must return single result ",
379 :     LT.ltc_void)
380 : monnier 71 val _ = ltMatch fp (lt, ltBool)
381 : monnier 45 val lts1 = typeof e1
382 :     val lts2 = typeof e2
383 :     in ltsMatch fp (lts1, lts2);
384 :     lts1
385 :     end
386 : monnier 71 | PRIMOP ((_,PO.WCAST,lt,[]), [u], lv, e) =>
387 :     (*** a hack: checked only after reifY is done ***)
388 :     if laterPhase phase then
389 :     (case LT.ltd_fct lt
390 :     of ([argt], [rt]) =>
391 :     (ltMatch (le, "WCAST") (typeofVal u, argt);
392 :     typeWith (lv, rt) e)
393 :     | _ => bug "unexpected WCAST in typecheck")
394 :     else bug "unexpected WCAST in typecheck"
395 : league 74 | PRIMOP ((dc,_,lt,ts), vs, lv, e) => let
396 :     (* There are lvars hidden inside dicts, which we didn't check
397 :     * before. This is a first-order check that they at least
398 :     * are bound to something; for now we don't care about their
399 :     * types. (I'm not sure what the rules should look like)
400 :     * --league, 10 april 1998.
401 :     *)
402 :     fun checkDict (SOME {default, table}) =
403 :     (typeofVar default;
404 :     app (ignore o typeofVar o #2) table)
405 :     | checkDict (NONE : dict option) = ()
406 :     in
407 :     checkDict dc;
408 :     typeWithBindingToSingleRsltOfInstAndApp ("PRIMOP",lt,ts,vs,lv) e
409 :     end
410 : monnier 45 (*
411 :     | GENOP (dict, (_,lt,ts), vs, lv, e) =>
412 :     (* verify dict ? *)
413 :     typeWithBindingToSingleRsltOfInstAndApp ("GENOP",lt,ts,vs,lv) e
414 :     | ETAG (t,v,lv,e) =>
415 :     matchAndTypeWith ("ETAG", v, ltString, ltEtag (LT.ltc_tyc t), lv, e)
416 :     | WRAP (t,v,lv,e) =>
417 :     matchAndTypeWith ("WRAP", v, LT.ltc_tyc t, ltWrap t, lv, e)
418 :     | UNWRAP (t,v,lv,e) =>
419 :     matchAndTypeWith ("UNWRAP", v, ltWrap t, LT.ltc_tyc t, lv, e)
420 :     *)
421 :     end
422 :     in typeof end
423 : monnier 16
424 : monnier 45 in
425 :     anyerror := false;
426 :     ignore (typeInEnv envs lexp);
427 :     !anyerror
428 :     end
429 : monnier 16
430 : monnier 45 in (* loplevel local *)
431 : monnier 16
432 : monnier 45 (****************************************************************************
433 :     * MAIN FUNCTION --- val checkTop : FLINT.fundec * typsys -> bool *
434 :     ****************************************************************************)
435 :     fun checkTop ((fkind, v, args, lexp) : fundec, phase) = let
436 :     val ve =
437 :     foldl (fn ((v,t), ve) => LT.ltInsert (ve,v,t,DI.top)) LT.initLtyEnv args
438 :     val err = check phase (LT.initTkEnv, ve, DI.top) lexp
439 :     val err = case fkind
440 :     of FK_FCT => err
441 :     | _ => (say "**** Not a functor at top level\n"; true)
442 :     in err end
443 : monnier 16
444 : monnier 45 val checkTop =
445 :     Stats.doPhase (Stats.makePhase "Compiler 051 FLINTCheck") checkTop
446 : monnier 16
447 : monnier 45 (****************************************************************************
448 :     * MAIN FUNCTION --- val checkExp : FLINT.lexp * typsys -> bool *
449 :     * (currently unused?) *
450 :     ****************************************************************************)
451 :     fun checkExp (le,phase) = check phase (LT.initTkEnv, LT.initLtyEnv, DI.top) le
452 : monnier 16
453 :     end (* toplevel local *)
454 :     end (* structure ChkFlint *)

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