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

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