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/branches/primop-branch-3/compiler/FLINT/plambda/chkplexp.sml
ViewVC logotype

Annotation of /sml/branches/primop-branch-3/compiler/FLINT/plambda/chkplexp.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2384 - (view) (download)

1 : monnier 16 (* Copyright 1996 by AT&T Bell Laboratories *)
2 :     (* chkplexp.sml *)
3 :    
4 :     signature CHKPLEXP =
5 :     sig
6 :    
7 : blume 2222 exception ChkPlexp (* PLambda type check error *)
8 :    
9 :     val checkLtyTop : PLambda.lexp * int -> bool
10 :     val checkLty : PLambda.lexp * PLambdaType.ltyEnv * int -> bool
11 : monnier 16 val newlam_ref : PLambda.lexp ref
12 :     val fname_ref : string ref
13 :    
14 :     end (* signature CHKPLEXP *)
15 :    
16 :     structure ChkPlexp : CHKPLEXP =
17 :     struct
18 :    
19 :     local structure LT = PLambdaType
20 :     structure LV = LambdaVar
21 :     structure DA = Access
22 :     structure DI = DebIndex
23 :     open PLambda
24 :     in
25 :    
26 : blume 2222 exception ChkPlexp (* PLambda type check error *)
27 :    
28 :     val debugging = ref true
29 :    
30 : monnier 16 (*** a hack of printing diagnostic output into a separate file ***)
31 :     val newlam_ref : PLambda.lexp ref = ref (RECORD[])
32 :     val fname_ref : string ref = ref "yyy"
33 :    
34 :     fun bug s = ErrorMsg.impossible ("CheckLty: "^s)
35 :     val say = Control.Print.say
36 :    
37 : blume 2222 structure PP = PrettyPrintNew
38 :     structure PU = PPUtilNew
39 :     val with_pp = PP.with_default_pp
40 :     val pd = ref 20
41 :    
42 : monnier 16 val anyerror = ref false
43 :     val clickerror = fn () => (anyerror := true)
44 :    
45 :     (****************************************************************************
46 :     * BASIC UTILITY FUNCTIONS *
47 :     ****************************************************************************)
48 : blume 2222 fun debugmsg msg =
49 :     if false (* !debugging *)
50 :     then (say "[ChkPlexp]: "; say msg; say "\n")
51 :     else ()
52 :    
53 : monnier 16 fun app2(f, [], []) = ()
54 :     | app2(f, a::r, b::z) = (f(a, b); app2(f, r, z))
55 :     | app2(f, _, _) = bug "unexpected list arguments in function app2"
56 :    
57 :     fun simplify(le,0) = STRING "<dummy>"
58 :     | simplify(le,n) =
59 :     let fun h le = simplify(le, n-1)
60 :     in case le
61 :     of FN(v, t, e) => FN(v, t, h e)
62 :     | APP(e1, e2) => APP(h e1, h e2)
63 :     | LET(v, e1, e2) => LET(v, h e1, h e2)
64 :     | TFN(ks, e) => TFN(ks, h e)
65 :     | TAPP(e, ts) => TAPP(h e, ts)
66 :     | PACK(lt, ts, nts, e) => PACK(lt, ts, nts, h e)
67 :     | CON(l, x, e) => CON(l, x, h e)
68 :     (* | DECON(l, x, e) => DECON(l, x, h e) *)
69 :     | FIX(lv, lt, le, b) => FIX(lv, lt, map h le, h b)
70 :     | SWITCH(e, l, dc, opp) =>
71 :     (let fun g(c, x) = (c, h x)
72 :     fun f x = case x of SOME y => SOME(h y) | NONE => NONE
73 :     in SWITCH(h e, l, map g dc, f opp)
74 :     end)
75 :     | RECORD e => RECORD (map h e)
76 :     | SRECORD e => SRECORD (map h e)
77 :     | VECTOR(e, x) => VECTOR (map h e, x)
78 :     | SELECT(i, e) => SELECT(i, h e)
79 :     | HANDLE(e1, e2) => HANDLE(h e1, h e2)
80 :     | WRAP(t, b, e) => WRAP(t, b, h e)
81 :     | UNWRAP(t, b, e) => UNWRAP(t, b, h e)
82 :     | _ => le
83 :     end (* end of simplify *)
84 :    
85 :     (** utility functions for printing *)
86 : blume 2222 fun tkPrint tk =
87 :     with_pp (fn stm =>
88 :     (PPLty.ppTKind (!pd) stm tk;
89 :     PP.newline stm))
90 : monnier 16
91 : blume 2222 fun tcPrint tc =
92 :     with_pp (fn stm =>
93 :     (PPLty.ppTyc (!pd) stm tc;
94 :     PP.newline stm))
95 :    
96 :     fun ltPrint lt =
97 :     with_pp (fn stm =>
98 :     (PPLty.ppLty (!pd) stm lt;
99 :     PP.newline stm))
100 :    
101 :     fun lePrint le =
102 :     with_pp(fn ppstrm => PPLexp.ppLexp 20 ppstrm (simplify(le, 3)))
103 :    
104 : monnier 16 (*** a hack for type checking ***)
105 :     fun laterPhase i = (i > 20)
106 :    
107 :     (****************************************************************************
108 :     * MAIN FUNCTION --- val checkLty : PLambda.lexp -> bool *
109 :     ****************************************************************************)
110 : blume 2222 fun checkLty (lexp, venv : LT.ltyEnv, phase) =
111 : monnier 16 let
112 :    
113 :     val ltEquiv = LT.lt_eqv
114 :     val ltString = if laterPhase(phase) then LT.ltc_void else LT.ltc_string
115 :     val ltExn = if laterPhase(phase) then LT.ltc_void else LT.ltc_exn
116 :     fun ltEtag lt = if laterPhase(phase) then LT.ltc_void
117 :     else LT.ltc_etag lt
118 :     fun ltVector t = if laterPhase(phase) then LT.ltc_void
119 :     else LT.ltc_tyc(LT.tcc_vector t)
120 : monnier 72
121 : monnier 16 (** lazily selecting a field from a record/structure type *)
122 :     exception LtySelect
123 :     fun ltSel (lt, i) =
124 :     (LT.lt_select(lt, i)) handle _ => raise LtySelect
125 :    
126 :     (** build a function or functor type from a pair of arbitrary ltys *)
127 : monnier 71 fun ltFun (x, y) =
128 :     if (LT.ltp_tyc x) andalso (LT.ltp_tyc y) then LT.ltc_parrow(x, y)
129 :     else LT.ltc_pfct(x, y)
130 : monnier 16
131 :     fun ltTup ts = LT.ltc_tyc(LT.tcc_tuple (map LT.ltd_tyc ts))
132 :    
133 :     (** lazily finding out the arg and res of an lty *)
134 :     exception LtyArrow
135 : monnier 71 fun ltArrow lt =
136 :     (if LT.ltp_tyc lt then LT.ltd_parrow lt
137 :     else LT.ltd_pfct lt) handle _ => raise LtyArrow
138 : monnier 16
139 : monnier 71 val lt_inst_chk = LT.lt_inst_chk_gen()
140 : blume 2222 (* kind checker for ltys *)
141 :     val ltyChk = LtyKindChk.ltKindCheckGen ()
142 :     (* kind checker for tycs *)
143 :     val tycChk = LtyKindChk.tcKindCheckGen ()
144 : monnier 71
145 : blume 2222 fun ltAppChk (lt, ts, kenv) : LT.lty =
146 : league 53 (case lt_inst_chk(lt, ts, kenv)
147 : monnier 16 of [b] => b
148 : blume 2222 | _ => bug "unexpected arg in ltAppChk")
149 : monnier 16
150 :     (** utility functions for type checking *)
151 :     fun ltTyApp le s (lt, ts, kenv) =
152 :     ((ltAppChk(lt, ts, kenv))
153 :     handle zz =>
154 :     (clickerror ();
155 :     say (s ^ " **** Kind conflicting in lexp =====> \n ");
156 :     case zz of LT.LtyAppChk => say " exception LtyAppChk raised! \n"
157 : blume 2222 | LT.KindChk _ => say " exception KindChk raised! \n"
158 : monnier 16 | _ => say " other weird exception raised! \n";
159 :     say "\n \n"; lePrint le; say "\n For Types: \n";
160 :     ltPrint lt; say "\n and \n ";
161 :     app (fn x => (tcPrint x; say "\n")) ts; say "\n \n";
162 :     say "***************************************************** \n";
163 :     bug "fatal typing error in ltTyApp"))
164 :    
165 : blume 2222 fun ltMatch le msg (t1, t2) =
166 : monnier 16 (if ltEquiv(t1,t2) then ()
167 :     else (clickerror();
168 : blume 2222 with_pp(fn s =>
169 :     (PU.pps s ("ERROR(checkLty): ltEquiv fails in ltMatch: "^msg); PP.newline s;
170 :     PU.pps s "le:"; PP.newline s; PPLexp.ppLexp 6 s le;
171 :     PU.pps s "t1:"; PP.newline s; PPLty.ppLty 10 s t1; PP.newline s;
172 :     PU.pps s "t2:"; PP.newline s; PPLty.ppLty 10 s t2; PP.newline s;
173 :     PU.pps s"***************************************************";
174 : gkuan 2384 PP.newline s)); raise Fail "ltMatch"))
175 :     handle LT.TeUnbound =>
176 : monnier 16 (clickerror();
177 : blume 2222 with_pp(fn s =>
178 :     (PU.pps s ("ERROR(checkLty): exception teUnbound2 in ltMatch"^msg); PP.newline s;
179 :     PU.pps s "le:"; PP.newline s; PPLexp.ppLexp 6 s le;
180 :     PU.pps s "t1:"; PP.newline s; PPLty.ppLty 10 s t1; PP.newline s;
181 :     PU.pps s "t2:"; PP.newline s; PPLty.ppLty 10 s t2; PP.newline s;
182 :     PU.pps s"***************************************************";
183 :     PP.newline s)))
184 : monnier 16
185 :     fun ltFnApp le s (t1, t2) =
186 :     let val (a1, b1) =
187 :     ((ltArrow t1) handle zz =>
188 :     (clickerror ();
189 :     say (s ^ " **** Applying Non-Arrow Type in lexp =====> \n ");
190 :     case zz of LtyArrow => say "exception LtyArrow raised. \n"
191 : blume 2222 | LT.TeUnbound => say "exception TeUnbound raised. \n"
192 : monnier 16 | _ => say "other weird exceptions raised\n";
193 :     say "\n \n"; lePrint le; say "\n For Types \n";
194 :     ltPrint t1; say "\n and \n "; ltPrint t2; say "\n \n";
195 :     say "***************************************************** \n";
196 :     bug "fatal typing error in ltFnApp"))
197 :    
198 : gkuan 2384 in ltMatch le (s^":ltFnApp") (a1, t2); b1
199 : monnier 16 end
200 :    
201 :     fun ltFnAppR le s (t1, t2) = (*** used for DECON lexps ***)
202 :     let val (a1, b1) =
203 :     ((ltArrow t1) handle zz =>
204 :     (clickerror ();
205 :     say (s ^ " **** Rev-Apply Non-Arrow Type in lexp =====> \n ");
206 :     case zz of LtyArrow => say "exception LtyArrow raised. \n"
207 : blume 2222 | LT.TeUnbound => say "exception TeUnbound raised. \n"
208 : monnier 16 | _ => say "other weird exceptions raised\n";
209 :     say "\n \n"; lePrint le; say "\n For Types \n";
210 :     ltPrint t1; say "\n and \n "; ltPrint t2; say "\n \n";
211 :     say "***************************************************** \n";
212 :     bug "fatal typing error in ltFnApp"))
213 :    
214 :     in ltMatch le s (b1, t2); a1
215 :     end
216 :    
217 :     fun ltSelect le s (lt, i) =
218 :     ((ltSel(lt, i))
219 :     handle zz =>
220 :     (clickerror ();
221 :     say (s ^ " **** Select from a wrong-type lexp =====> \n ");
222 :     case zz of LtySelect => say "exception LtyArrow raised. \n"
223 : blume 2222 | LT.TeUnbound => say "exception TeUnbound raised. \n"
224 : monnier 16 | _ => say "other weird exceptions raised\n";
225 :     say "\n \n"; lePrint le; say "\n \n";
226 :     say "Selecting "; say (Int.toString i);
227 :     say "-th component from the type: \n "; ltPrint lt; say "\n \n ";
228 :     say "***************************************************** \n";
229 :     bug "fatal typing error in ltSelect"))
230 :    
231 :     (** ltConChk currently does not check the case for DATAcon *)
232 :     (** Of course, we could easily check for monomorphic DATAcons *)
233 :     fun ltConChk le s (DATAcon ((_,rep,lt), ts, v), root, kenv, venv, d) =
234 :     let val t1 = ltTyApp le "DECON" (lt, ts, kenv)
235 :     val t = ltFnAppR le "DECON" (t1, root)
236 :     in LT.ltInsert(venv, v, t, d)
237 :     end
238 :     | ltConChk le s (c, root, kenv, venv, d) =
239 :     let val nt = (case c of INT32con _ => LT.ltc_int32
240 :     | WORD32con _ => LT.ltc_int32
241 :     | REALcon _ => LT.ltc_real
242 :     | STRINGcon _ => ltString
243 : mblume 1347 | INTINFcon _ => bug "INTINFcon"
244 : monnier 16 | _ => LT.ltc_int)
245 : gkuan 2384 in ((ltMatch le s (nt, root)) handle Fail _ => say "ConChk ltEquiv\n"); venv
246 : monnier 16 end
247 :    
248 :     (** check : tkindEnv * ltyEnv * DI.depth -> lexp -> lty *)
249 :     fun check (kenv, venv, d) =
250 : blume 2222 let fun ltyChkMsg msg lexp kenv lty =
251 :     ltyChk kenv lty
252 :     handle LT.KindChk kndchkmsg =>
253 :     (say ("*** Kind check failure during \
254 :     \ PLambda type check: ");
255 :     say (msg);
256 :     say ("***\n Term: ");
257 :     with_pp(fn s => PPLexp.ppLexp 20 s lexp);
258 :     say ("\n Kind check error: ");
259 :     say kndchkmsg;
260 :     say ("\n");
261 :     raise ChkPlexp)
262 :     fun loop le =
263 :     let fun ltyChkMsgLexp msg kenv lty =
264 :     ltyChkMsg msg lexp kenv lty
265 :     fun ltyChkenv msg lty = ltyChkMsgLexp msg kenv lty
266 :     in
267 :     (case le
268 :     of VAR v =>
269 :     (LT.ltLookup(venv, v, d)
270 :     handle LT.ltUnbound =>
271 :     (say ("** Lvar ** " ^ (LV.lvarName(v))
272 :     ^ " is unbound *** \n");
273 :     bug "unexpected lambda code in checkLty"))
274 :     | (INT _ | WORD _) => LT.ltc_int
275 :     | (INT32 _ | WORD32 _) => LT.ltc_int32
276 :     | REAL _ => LT.ltc_real
277 :     | STRING _ => ltString
278 :     | PRIM(p, t, ts) =>
279 :     (* kind check t and ts *)
280 :     (ltyChkenv " PRIM " t;
281 :     map (tycChk kenv) ts;
282 :     debugmsg "PRIM";
283 :     ltTyApp le "PRIM" (t, ts, kenv))
284 :    
285 :     | FN(v, t, e1) =>
286 :     let val _ = ltyChkenv "FN bound var" t
287 :     (* kind check bound variable type *)
288 :     val venv' = LT.ltInsert(venv, v, t, d)
289 :     val res = check (kenv, venv', d) e1
290 :     val _ = ltyChkenv "FN rng" res
291 :     val _ = debugmsg "FN"
292 :     val fnlty = ltFun(t, res) (* handle both functions and functors *)
293 :     val _ = ltyChkenv "FNlty " fnlty
294 :     val _ = debugmsg "FN 2"
295 :     in fnlty
296 :     end
297 :    
298 :     | FIX(vs, ts, es, eb) =>
299 :     let val _ = map (ltyChkenv "FIX bound var") ts
300 :     (* kind check bound variable types *)
301 :     fun h (env, v::r, x::z) = h(LT.ltInsert(env, v, x, d), r, z)
302 :     | h (env, [], []) = env
303 :     | h _ = bug "unexpected FIX bindings in checkLty."
304 :     val venv' = h(venv, vs, ts)
305 :    
306 :     val nts = map (check (kenv, venv', d)) es
307 :     val _ = map (ltyChkenv "FIX body types") nts
308 :     val _ = app2(ltMatch le "FIX1", ts, nts)
309 :     val _ = debugmsg "FIX"
310 :     in check (kenv, venv', d) eb
311 :     end
312 :    
313 :     | APP(e1, e2) =>
314 :     let val top = loop e1
315 :     val targ = loop e2
316 :     val _ = ltyChkenv "APP operator " top
317 :     val _ = ltyChkenv "APP argument " targ
318 :     val _ = debugmsg "APP"
319 :     in
320 :     ltFnApp le "APP" (top, targ)
321 :     end
322 :    
323 :     | LET(v, e1, e2) =>
324 :     let val t1 = loop e1
325 :     val _ = ltyChkenv "LET definien" t1
326 :     val venv' = LT.ltInsert(venv, v, t1, d)
327 :     val bodyLty = check (kenv, venv', d) e2
328 :     val _ = ltyChkenv "LET body" bodyLty
329 :     val _ = debugmsg "LET"
330 :     in bodyLty
331 :     end
332 :    
333 :     | TFN(ks, e) =>
334 :     let val kenv' = LT.tkInsert(kenv, ks)
335 :     val lt = check (kenv', venv, DI.next d) e
336 :     val _ = ltyChkMsgLexp "TFN body" (ks::kenv) lt
337 :     val _ = debugmsg "TFN"
338 :     in LT.ltc_poly(ks, [lt])
339 :     end
340 :    
341 :     | TAPP(e, ts) =>
342 :     let val lt = loop e
343 :     val _ = map ((ltyChkenv "TAPP args") o LT.ltc_tyc) ts
344 :     (* kind check type args *)
345 :     val _ = ltyChkenv "TAPP type function " lt
346 :     val _ = debugmsg "TAPP"
347 :     in ltTyApp le "TAPP" (lt, ts, kenv)
348 :     end
349 :    
350 :     | GENOP(dict, p, t, ts) =>
351 :     ((* should type check dict also *)
352 :     (map ((ltyChkenv "GENOP args ") o LT.ltc_tyc) ts;
353 :     ltTyApp le "GENOP" (t, ts, kenv)))
354 :    
355 :     | PACK(lt, ts, nts, e) =>
356 :     let val argTy = ltTyApp le "PACK-A" (lt, ts, kenv)
357 :     val _ = ltyChkenv " PACK-A " argTy
358 :     val bodyTy = loop e
359 :     val _ = ltyChkenv " PACK body " bodyTy
360 :     val _ = debugmsg "PACK"
361 : gkuan 2384 in ((ltMatch le "PACK-M" (argTy, loop e)) handle Fail _ => say "PACK ltEquiv\n") ;
362 : blume 2222 ltTyApp le "PACK-R" (lt, nts, kenv)
363 :     end
364 :    
365 :     | CON((_, rep, lt), ts, e) =>
366 :     let val t1 = ltTyApp le "CON" (lt, ts, kenv)
367 :     val _ = ltyChkenv "CON 1 " t1
368 :     val t2 = loop e
369 :     val _ = ltyChkenv "CON 2 " t2
370 :     val _ = debugmsg "CON"
371 :     in ltFnApp le "CON-A" (t1, t2)
372 :     end
373 :     (*
374 :     | DECON((_, rep, lt), ts, e) =>
375 :     let val t1 = ltTyApp le "DECON" (lt, ts, kenv)
376 :     val t2 = loop e
377 :     in ltFnAppR le "DECON" (t1, t2)
378 :     end
379 :     *)
380 :     | RECORD el =>
381 :     let val elemsltys = map loop el
382 :     val _ = map (ltyChkenv "RECORD elem ") elemsltys
383 :     val _ = debugmsg "RECORD"
384 :     in ltTup elemsltys
385 :     end
386 :     | SRECORD el =>
387 :     let val elemsltys = map loop el
388 :     val _ = map (ltyChkenv "SRECORD elem ") elemsltys
389 :     in LT.ltc_str elemsltys
390 :     end
391 :     | VECTOR (el, t) =>
392 :     let val ts = map loop el
393 :     in ltyChkenv "VECTOR index " (LT.ltc_tyc t);
394 :     map (ltyChkenv "VECTOR vector ") ts;
395 :     app (fn x => ltMatch le "VECTOR" (x, LT.ltc_tyc t)) ts;
396 :     debugmsg "VECTOR ";
397 :     ltVector t
398 :     end
399 :    
400 :     | SELECT(i,e) =>
401 :     let val lty = loop e
402 :     val _ = ltyChkenv " SELECT " lty
403 :     val _ = debugmsg "SELECT"
404 :     in
405 :     ltSelect le "SEL" (lty, i)
406 :     end
407 :     | SWITCH(e, _, cl, opp) =>
408 :     let val root = loop e
409 :     val _ = ltyChkenv " SWITCH root " root
410 :     fun h (c, x) =
411 :     let val venv' = ltConChk le "SWT1" (c, root, kenv, venv, d)
412 :     in check (kenv, venv', d) x
413 :     end
414 :     val ts = map h cl
415 :     val _ = map (ltyChkenv "SWITCH branch ") ts
416 :     val _ = debugmsg "SWITCH"
417 :     in (case ts
418 :     of [] => bug "empty switch in checkLty"
419 :     | a::r =>
420 :     (app (fn x => ltMatch le "SWT2" (x, a)) r;
421 :     case opp
422 :     of NONE => a
423 :     | SOME be => (ltMatch le "SWT3" (loop be, a); a)))
424 :     end
425 :    
426 :     | ETAG(e, t) =>
427 :     let val z = loop e (* what do we check on e ? *)
428 :     val _ = ltyChkenv "ETAG 1 " z
429 :     val _ = ltMatch le "ETAG1" (z, LT.ltc_string)
430 :     val _ = ltyChkenv "ETAG " t
431 :     val _ = debugmsg "ETAG"
432 :     in ltEtag t
433 :     end
434 :    
435 :     | RAISE(e,t) =>
436 :     let val exlty = loop e
437 :     val _ = ltyChkenv "RAISE " exlty
438 :     val _ = debugmsg "RAISE"
439 :     in
440 :     (ltMatch le "RAISE" (exlty, ltExn); t)
441 :     end
442 :     | HANDLE(e1,e2) =>
443 :     let val t1 = loop e1
444 :     val _ = ltyChkenv "HANDLE exception " t1
445 :     val t2 = loop e2
446 :     val _ = ltyChkenv "HANDLE handler " t2
447 :     val arg = ltFnAppR le "HANDLE" (loop e2, t1)
448 :     val _ = ltyChkenv "HANDLE arg " arg
449 :     val _ = debugmsg "HANDLE"
450 :     in t1 (* [GK] Is this right?? *)
451 :     end
452 :    
453 :     (** these two cases should never happen before wrapping *)
454 :     | WRAP(t, b, e) =>
455 :     (ltMatch le "WRAP" (loop e, LT.ltc_tyc t);
456 :     if laterPhase(phase) then LT.ltc_void
457 :     else LT.ltc_tyc(if b then LT.tcc_box t else LT.tcc_abs t))
458 :    
459 :     | UNWRAP(t, b, e) =>
460 :     let val ntc = if laterPhase(phase) then LT.tcc_void
461 :     else (if b then LT.tcc_box t else LT.tcc_abs t)
462 :     val nt = LT.ltc_tyc ntc
463 :     val _ = ltyChkenv "UNWRAP " nt
464 :     in (ltMatch le "UNWRAP" (loop e, nt); LT.ltc_tyc t)
465 :     end)
466 :     end (* loop *)
467 :     in (* wrap loop with kind check of result *)
468 :     fn x => let val y = loop x in ltyChkMsg "RESULT " x kenv y; y end
469 : monnier 16 end (* end-of-fn-check *)
470 :    
471 :     in
472 : blume 2222 anyerror := false;
473 :     check (LT.initTkEnv, venv, DI.top) lexp;
474 :     !anyerror
475 : monnier 16 end (* end of function checkLty *)
476 :    
477 : blume 2222 fun checkLtyTop(lexp, phase) = checkLty(lexp, LT.initLtyEnv, phase)
478 :    
479 : monnier 16 end (* toplevel local *)
480 :     end (* structure CheckLty *)

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