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/SMLNJ/src/compiler/FLINT/flint/chkflint.sml
ViewVC logotype

Annotation of /sml/branches/SMLNJ/src/compiler/FLINT/flint/chkflint.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 24 - (view) (download)

1 : monnier 24 (* COPYRIGHT (c) 1997 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 :     val fname_ref : string ref (* a filename hack *)
14 :    
15 :     end (* signature CHKFLINT *)
16 :    
17 :     structure ChkFlint : CHKFLINT =
18 :     struct
19 :    
20 :     local structure LT = LtyExtern
21 :     structure LV = LambdaVar
22 :     structure DA = Access
23 :     structure DI = DebIndex
24 :     structure PP = PPFlint
25 :     open FLINT
26 : monnier 24 in
27 : monnier 16
28 : monnier 24 (** which set of the typing rules to use while doing the typecheck *)
29 :     type typsys = int (* currently very crude, use int for phases *)
30 :    
31 :     (*** a hack of printing diagnostic output into a separate file ***)
32 :     val fname_ref : string ref = ref "yyy"
33 :    
34 : monnier 16 fun bug s = ErrorMsg.impossible ("ChkFlint: "^s)
35 :     val say = Control.Print.say
36 :     val anyerror = ref false
37 : monnier 24 val clickerror = fn () => (anyerror := true)
38 : monnier 16
39 :     (****************************************************************************
40 :     * BASIC UTILITY FUNCTIONS *
41 :     ****************************************************************************)
42 : monnier 24 fun app2(f, [], []) = ()
43 :     | app2(f, a::r, b::z) = (f(a, b); app2(f, r, z))
44 :     | app2(f, _, _) = bug "unexpected list arguments in function app2"
45 : monnier 16
46 : monnier 24 fun simplify(le,0) = RET [STRING "<-dummy->"]
47 :     | simplify(le,n) =
48 :     let fun h le = simplify(le, n-1)
49 :     fun h1 (fk,v,args,le) = (fk,v,args,h le)
50 :     fun h2 (v,tvs,le) = (v,tvs,h le)
51 : monnier 16 in case le
52 : monnier 24 of LET(vs, e1, e2) => LET(vs, h e1, h e2)
53 :     | FIX(fdecs, b) => FIX(map h1 fdecs, h b)
54 :     | TFN(tdec, e) => TFN(h2 tdec, h e)
55 :     | SWITCH(v, l, dc, opp) =>
56 :     (let fun g(c, x) = (c, h x)
57 :     fun f x = case x of SOME y => SOME(h y) | NONE => NONE
58 :     in SWITCH(v, l, map g dc, f opp)
59 :     end)
60 :     | HANDLE(e, v) => HANDLE(h e, v)
61 : monnier 16 | _ => le
62 :     end (* end of simplify *)
63 :    
64 :     (** utility functions for printing *)
65 :     val tkPrint = say o LT.tk_print
66 :     val tcPrint = say o LT.tc_print
67 :     val ltPrint = say o LT.lt_print
68 : monnier 24 fun lePrint le = PP.printLexp (simplify(le, 3))
69 :     fun svPrint sv = PP.printSval (sv)
70 : monnier 16
71 : monnier 24 (*** a hack for type checking ***)
72 :     fun laterPhase i = (i > 20)
73 : monnier 16
74 : monnier 24 (****************************************************************************
75 :     * MAIN FUNCTION --- val checkTop : Lambda.fundec * typsys -> bool *
76 :     ****************************************************************************)
77 :     fun checkTop ((fk,v,args,lexp), phase) = bug "not implemented"
78 :     (*
79 :     let
80 :     val ltEquiv = LT.lt_eqv_bx
81 :     val ltAppChk = LT.lt_inst_chk
82 :     val ltString = if laterPhase(phase) then LT.ltc_void else LT.ltc_string
83 :     val ltExn = if laterPhase(phase) then LT.ltc_void else LT.ltc_exn
84 :     fun ltEtag lt = if laterPhase(phase) then LT.ltc_void
85 :     else LT.ltc_etag lt
86 :     fun ltVector t = if laterPhase(phase) then LT.ltc_void
87 :     else LT.ltc_tyc(LT.tcc_app(LT.tcc_vector,[t]))
88 :     exception tcUnbound = LT.tcUnbound
89 :     exception LtyArrow
90 :     exception LtySelect
91 :     fun ltArrow lt =
92 :     (LT.lt_arrow lt) handle _ => raise LtyArrow
93 :     fun ltSel (lt, i) =
94 :     (LT.lt_select(lt, i)) handle _ => raise LtySelect
95 :     fun ltFun (t1, t2) = LT.ltc_fun(t1, t2)
96 : monnier 16
97 : monnier 24 (** utility values and functions on ltyEnv *)
98 :     type ltyEnv = LT.ltyEnv
99 :     val initLtyEnv : ltyEnv = LT.initLtyEnv
100 :     val ltLookup = LT.ltLookup
101 :     val ltInsert = LT.ltInsert
102 : monnier 16
103 : monnier 24 (** utility functions for type checking *)
104 :     fun ltTyApp le s (lt, ts, kenv) =
105 :     ((ltAppChk(lt, ts, kenv))
106 :     handle zz =>
107 :     (clickerror ();
108 :     say (s ^ " **** Kind conflicting in lexp =====> \n ");
109 :     case zz of LT.LtyAppChk => say " exception LtyAppChk raised! \n"
110 :     | LT.TkTycChk => say " exception TkTycChk raised! \n"
111 :     | _ => say " other weird exception raised! \n";
112 :     say "\n \n"; lePrint le; say "\n For Types: \n";
113 :     ltPrint lt; say "\n and \n ";
114 :     app (fn x => (tcPrint x; say "\n")) ts; say "\n \n";
115 :     say "***************************************************** \n";
116 :     bug "fatal typing error in ltTyApp"))
117 : monnier 16
118 : monnier 24 fun ltMatch le s (t1, t2) =
119 :     (if ltEquiv(t1,t2) then ()
120 :     else (clickerror();
121 :     say (s ^ " **** Lty conflicting in lexp =====> \n ");
122 :     ltPrint t1; say "\n and \n "; ltPrint t2;
123 :     say "\n \n"; MCprint.printLexp le;
124 :     say "***************************************************** \n"))
125 :     handle zz =>
126 :     (clickerror();
127 :     say (s ^ " **** Lty conflicting in lexp =====> \n ");
128 :     say "uncaught exception found ";
129 :     say "\n \n"; MCprint.printLexp le; say "\n";
130 :     ltPrint t1; say "\n and \n "; ltPrint t2; say "\n";
131 :     say "***************************************************** \n")
132 : monnier 16
133 : monnier 24 fun ltsMatch le s (ts1, ts2) = app2 (ltMatch le s) (ts1, ts2)
134 : monnier 16
135 : monnier 24 fun ltFnApp le s (t1, t2) =
136 :     let val (a1, b1) =
137 :     ((ltArrow t1) handle zz =>
138 :     (clickerror ();
139 :     say (s ^ " **** Applying Non-Arrow Type in lexp =====> \n ");
140 :     case zz of LtyArrow => say "exception LtyArrow raised. \n"
141 :     | tcUnbound => say "exception tcUnbound raised. \n"
142 :     | _ => say "other weird exceptions raised\n";
143 :     say "\n \n"; lePrint le; say "\n For Types \n";
144 :     ltPrint t1; say "\n and \n "; ltPrint t2; say "\n \n";
145 :     say "***************************************************** \n";
146 :     bug "fatal typing error in ltFnApp"))
147 : monnier 16
148 : monnier 24 in ltMatch le s (a1, t2); b1
149 :     end
150 : monnier 16
151 : monnier 24 fun ltFnAppR le s (t1, t2) = (*** used for DECON lexps ***)
152 :     let val (a1, b1) =
153 :     ((ltArrow t1) handle zz =>
154 :     (clickerror ();
155 :     say (s ^ " **** Rev-Apply Non-Arrow Type in lexp =====> \n ");
156 :     case zz of LtyArrow => say "exception LtyArrow raised. \n"
157 :     | tcUnbound => say "exception tcUnbound raised. \n"
158 :     | _ => say "other weird exceptions raised\n";
159 :     say "\n \n"; lePrint le; say "\n For Types \n";
160 :     ltPrint t1; say "\n and \n "; ltPrint t2; say "\n \n";
161 :     say "***************************************************** \n";
162 :     bug "fatal typing error in ltFnApp"))
163 : monnier 16
164 : monnier 24 in ltMatch le s (b1, t2); a1
165 :     end
166 : monnier 16
167 : monnier 24 fun ltSelect le s (lt, i) =
168 :     ((ltSel(lt, i))
169 :     handle zz =>
170 :     (clickerror ();
171 :     say (s ^ " **** Select from a wrong-type lexp =====> \n ");
172 :     case zz of LtySelect => say "exception LtyArrow raised. \n"
173 :     | tcUnbound => say "exception tcUnbound raised. \n"
174 :     | _ => say "other weird exceptions raised\n";
175 :     say "\n \n"; lePrint le; say "\n \n";
176 :     say "Selecting "; say (Int.toString i);
177 :     say "-th component from the type: \n "; ltPrint lt; say "\n \n ";
178 :     say "***************************************************** \n";
179 :     bug "fatal typing error in ltSelect"))
180 : monnier 16
181 : monnier 24 (*
182 :     * Right now, ltConChk does not check the case for DATAcon but this
183 :     * will be fixed soon. (ZHONG)
184 :     *)
185 :     fun ltConChk le s (DATAcon ((_, rep, lt), ts, vs), root, venv, kenv, d) =
186 :     let val nt = ltTyApp le "DECON" (lt, ts, kenv)
187 :     val nts = ltFnAppR le "DECON" (nt, [root])
188 :     fun h(env, v::r, x::s) =
189 :     h(ltInsert(env, v, x, d), r, s)
190 :     | h(env, [], []) = env
191 :     | h _ = (say ("** SWI BINDINGS mismatch ** vs=" ^
192 :     (Int.toString (length vs)) ^ " e1s=" ^
193 :     (Int.toString (length nts)) ^ " \n");
194 :     bug "unexpected lambda code in ltConChk")
195 :     in h(venv, vs, nts)
196 :     end
197 :     | ltConChk le s (c, lt, venv, kenv, d) =
198 :     let val nt = (case c of INT32con _ => LT.ltc_int32
199 :     | WORD32con _ => LT.ltc_int32
200 :     | REALcon _ => LT.ltc_real
201 :     | STRINGcon _ => ltString
202 :     | _ => LT.ltc_int)
203 :     in ltMatch le s (nt, lt); venv
204 :     end
205 : monnier 16
206 : monnier 24 (** check : tkindEnv * ltyEnv * DI.depth -> lexp -> lty list *)
207 :     fun check (kenv, venv, d) =
208 :     let fun lpsv (INT _) = LT.ltc_int
209 :     | lpsv (WORD _) = LT.ltc_int
210 :     | lpsv (INT32 _) = LT.ltc_int32
211 :     | lpsv (WORD32 _) = LT.ltc_int32
212 :     | lpsv (REAL _) = LT.ltc_real
213 :     | lpsv (STRING _) = ltString
214 :     | lpsv (VAR v) =
215 :     (ltLookup(venv, v, d)
216 :     handle LT.ltUnbound =>
217 :     (say ("** Lvar ** " ^ (LV.lvarName(v)) ^ " is unbound *** \n");
218 :     bug "unexpected lambda code in checkTop"))
219 : monnier 16
220 : monnier 24 fun loop le =
221 :     (case le
222 :     of RET vs => map lpsv sv
223 :     | APP(v, vs) => ltFnApp le "APP" (lpsv v, map lpsv vs)
224 :     | TAPP(sv, ts) => ltTyApp le "TAPP" (lpsv sv, ts, kenv)
225 :     | LET(vs, e1, e2) =>
226 :     let val ts = loop e1
227 :     fun h(env, v::r, t::s) =
228 :     h(ltInsert(env,v,t,d), r, s)
229 :     | h(env, [], []) = env
230 :     | h _ = (say ("** LET BINDINGS mismatch ** vs=" ^
231 :     (Int.toString (length vs)) ^ " e1s=" ^
232 :     (Int.toString (length ts)) ^ " \n");
233 :     bug "unexpected lambda code in checkTop")
234 :     val venv1 = h(venv, vs, ts)
235 :     in check (kenv, venv1, d) e2
236 :     end
237 :     | FIX (fs, eb) =>
238 :     let fun h (env, (_,v,t,_,_)::r) = h(ltInsert(env,v,t,d), r)
239 :     | h (env, []) = env
240 :     val venv1 = h(venv, fs)
241 : monnier 16
242 : monnier 24 fun g (_,_,_,args,e) =
243 :     let fun m (env, (v,t)::r) = m(ltInsert(env,v,t,d), r)
244 :     | m (env, []) = env
245 :     val venv2 = m(venv1, args)
246 :     val argts = map #1 args
247 :     val rests = check (kenv, venv2, d) e
248 :     in LT.ltc_fun(argts, rests)
249 :     end
250 :     val nts = map g fs
251 :     val _ = ltsMatch le "FIX1" (map #3 fs, nts)
252 :     in check (kenv, venv1, d) eb
253 :     end
254 :     | TFN((v,t,tvs,e), eb) =>
255 :     let val kenv1 = LT.tkInsert(kenv, map #2 tvs)
256 :     (*** temporarily using the old format of type variables ***)
257 :     val lts = check (kenv1, venv, DI.next d) e
258 :     val nt = LT.ltc_poly(ks, lts)
259 :     val _ = ltMatch le "TFN" (t, nt)
260 :     val venv1 = ltInsert(venv,v,t,d)
261 :     in check (kenv, venv1, d) eb
262 :     end
263 :     | SWITCH(v, _, cl, opp) =>
264 :     let val root = lpsv v
265 :     fun h (c, x) =
266 :     let val venv1 = ltConChk le "SWT1" (c, root, venv, kenv, d)
267 :     in check (kenv, venv1, d) x
268 :     end
269 :     val ts = map h cl
270 :     in (case ts
271 :     of [] => bug "empty switch in checkTop"
272 :     | a::r =>
273 :     (app (fn x => ltsMatch le "SWT2" (x, a)) r;
274 :     case opp
275 :     of NONE => a
276 :     | SOME be => (ltsMatch le "SWT3" (loop be, a); a)))
277 :     end
278 :     | CON((_, rep, lt), ts, vs, v, eb) =>
279 :     let val ts1 = ltTyApp le "CON" (lt, ts, kenv)
280 :     val ts2 = map lpsv vs
281 :     in case ts1
282 :     of [t1] =>
283 :     let val nt = ltFnApp le "CON-A" (t1, ts2)
284 :     val venv1 = ltInsert(venv, v, nt, d)
285 :     in check (kenv, venv1, d) eb
286 :     end
287 :     | _ => bug "unexpected case in check CON"
288 :     end
289 :     | RECORD (RK_VECTOR t, vl) =>
290 :     let val ts = map lpsv vl
291 :     in app (fn x => ltMatch le "VECTOR" (x, LT.ltc_tyc t)) ts;
292 :     ltVector t
293 :     end
294 :     | RECORD (_, []) => LT.ltc_unit
295 :     | RECORD (RK_RECORD, vl) => LT.ltc_tuple (map lpsv vl)
296 :     | RECORD (RK_STRUCT, vl) => LT.ltc_str (map lpsv vl)
297 : monnier 16
298 : monnier 24 | SELECT(u, i, v, eb) =>
299 :     let val t = ltSelect le "SEL" (lpsv u, i)
300 :     val venv1 = ltInsert(venv, v, t, d)
301 :     in check (kenv, venv1, d) eb
302 :     end
303 : monnier 16
304 : monnier 24 | ETAG(v, t) => (* v is string but the result should be eflag[t] *)
305 :     let val z = lpsv v (* what do we check on e ? *)
306 :     val _ = ltMatch le "ETAG1" (z, LT.ltc_string)
307 :     in ltEtag t
308 :     end
309 : monnier 16
310 : monnier 24 | RAISE(v,t) =>
311 :     (ltMatch le "RAISE" (lpsv v, ltExn); t)
312 : monnier 16
313 : monnier 24 | HANDLE(e,sv) =>
314 :     let val ts = loop e
315 :     val arg = ltFnAppR le "HANDLE" (lpsv sv, ts)
316 :     in ts
317 :     end
318 : monnier 16
319 : monnier 24 | PRIM((p, t, ts), vs, v, eb) =>
320 :     let val xx = ltTyApp (SVAL sv) "PRIM" (t, ts, kenv)
321 :     in check (kenv, ltInsert(venv, v, t, d), d) eb
322 :     end
323 : monnier 16
324 : monnier 24 | GENOP(dict, (p, t, ts), vs, v, eb) =>
325 :     (* should check the consistency of dict here *)
326 :     ltTyApp (SVAL sv) "GENOP" (t, ts, kenv)
327 : monnier 16
328 : monnier 24 | PACK(lt, ts, nts, sv) =>
329 :     let val argTy = ltTyApp le "PACK-A" (lt, ts, kenv)
330 :     in ltMatch le "PACK-M" (argTy, lpsv sv);
331 :     ltTyApp le "PACK-R" (lt, nts, kenv)
332 :     end
333 : monnier 16
334 : monnier 24 (** these two cases should never happen before wrapping *)
335 :     | WRAP(t, b, sv, v, eb) =>
336 :     (ltMatch le "WRAP" (lpsv sv, LT.ltc_tyc t);
337 :     if laterPhase(phase) then LT.ltc_void
338 :     else LT.ltc_tyc(if b then LT.tcc_box t else LT.tcc_abs t))
339 : monnier 16
340 : monnier 24 | UNWRAP(t, b, sv, v, eb) =>
341 :     let val ntc = if laterPhase(phase) then LT.tcc_void
342 :     else (if b then LT.tcc_box t else LT.tcc_abs t)
343 :     val nt = LT.ltc_tyc ntc
344 :     in (ltMatch le "UNWRAP" (lpsv sv, nt); LT.ltc_tyc t)
345 :     end
346 :    
347 :     | FN(v, t, e1) =>
348 :     let val venv' = ltInsert(venv, v, t, d)
349 :     val res = check (kenv, venv', d) e1
350 :     in ltFun(t, res) (* handle both functions and functors *)
351 :     end)
352 :    
353 :    
354 :     in loop
355 :     end (* end-of-fn-check *)
356 :    
357 :     in
358 :     anyerror := false; check (LT.initTkEnv, initLtyEnv, DI.top) lexp; !anyerror;
359 :     end (* end of function checkTop *)
360 :     *)
361 :    
362 :     fun checkExp _ = bug "checkExp not implemented yet"
363 :    
364 : monnier 16 end (* toplevel local *)
365 :     end (* structure ChkFlint *)
366 : monnier 24

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