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-2/src/compiler/FLINT/plambda/chkplexp.sml
ViewVC logotype

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2046 - (view) (download)

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

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