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 2035 - (view) (download)

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

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