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

Parent Directory | 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