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/kernel/ltykernel.sml
ViewVC logotype

Annotation of /sml/branches/primop-branch-2/src/compiler/FLINT/kernel/ltykernel.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2026 - (view) (download)

1 : macqueen 2014 (* COPYRIGHT (c) 1997 YALE FLINT PROJECT *)
2 : monnier 16 (* ltykernel.sml *)
3 :    
4 :     structure LtyKernel :> LTYKERNEL =
5 :     struct
6 :    
7 : macqueen 2014 structure PT = PrimTyc
8 :     structure DI = DebIndex
9 :     open Lty
10 :    
11 :     val debugging : bool ref = ref false
12 :     val dp : int ref = ref 20
13 : monnier 45 fun bug s = ErrorMsg.impossible ("LtyKernel:" ^ s)
14 :    
15 : macqueen 2014 structure PP = PrettyPrintNew
16 :     structure PU = PPUtilNew
17 :     structure EM = ErrorMsg
18 :     open PPLty
19 : monnier 16
20 : macqueen 2014 val with_pp = PP.with_default_pp
21 : monnier 16
22 : macqueen 2014 fun dgPrint (msg: string, printfn: PP.stream -> 'a -> unit, arg: 'a) =
23 :     if (!debugging)
24 :     then with_pp
25 :     (fn ppstrm =>
26 :     (PP.openHVBox ppstrm (PP.Rel 0);
27 :     PP.string ppstrm msg;
28 :     PP.newline ppstrm;
29 :     PP.nbSpace ppstrm 2;
30 :     PP.openHVBox ppstrm (PP.Rel 0);
31 :     printfn ppstrm arg;
32 :     PP.closeBox ppstrm;
33 :     PP.newline ppstrm;
34 :     PP.closeBox ppstrm;
35 :     PP.flushStream ppstrm))
36 :     else ()
37 : monnier 71
38 : macqueen 2014 (** utility functions for tc_env and lt_env *)
39 :     local
40 : monnier 16
41 : macqueen 2014 fun tcc_env_int(x, 0, 0, te) = x
42 :     | tcc_env_int(x, i, j, te) = tc_injX(TC_ENV(x, i, j, te))
43 : monnier 197
44 : macqueen 2014 fun ltc_env_int(x, 0, 0, te) = x
45 :     | ltc_env_int(x, i, j, te) = lt_injX(LT_ENV(x, i, j, te))
46 : monnier 16
47 : macqueen 2014 fun withEff ([], ol, nl, tenv) = false
48 :     | withEff (a::r, ol, nl, tenv) =
49 :     let val (i, j) = tvDecode a
50 :     val neweff =
51 :     if i > ol then (ol <> nl)
52 :     else (* case tcLookup(i, tenv)
53 :     of (NONE, n) => (nl - n) <> i
54 :     | (SOME ts, n) =>
55 :     (let val y = List.nth(ts, j)
56 :     in (case tc_outX y
57 :     of TC_VAR(ni, nj) =>
58 :     ((nj <> j) orelse ((ni+nl-n) <> i))
59 :     | _ => true)
60 :     end) *) true
61 :     in neweff orelse (withEff(r, ol, nl, tenv))
62 : monnier 16 end
63 :     in
64 :    
65 :     fun tcc_env(x, ol, nl, tenv) =
66 : georgekuan 2013 (let fun checkTCVAR tyc = case (tc_outX tyc) of
67 : georgekuan 2026 TC_VAR(i,j) => (case teLookup(tenv, i)
68 :     of SOME(Beta(j, tcs, _)) =>
69 :     if j >= length tcs
70 :     then (print "tcc_env TC_VAR ";
71 :     print (Int.toString j);
72 :     print "B tcs length ";
73 :     print (Int.toString (length tcs));
74 :     raise Fail "Bad TC_ENV TC_VAR")
75 :     else ()
76 :     | SOME(Lamb(j)) =>
77 :     print "TC_VAR referencing LAMB"
78 : georgekuan 2013 | _ => ())
79 : georgekuan 2026 | TC_ENV(tc, _, _, _) => (print "TC_ENV(";
80 :     checkTCVAR(tc);
81 :     print ")\n")
82 : georgekuan 2013 | _ => () (* print ("tcc_env OTHER " ^ tci_print tci ^"\n") *)
83 :     in checkTCVAR(x);
84 :     let val tvs = tc_vs x
85 : monnier 16 in case tvs
86 :     of NONE => tcc_env_int(x, ol, nl, tenv)
87 :     | SOME [] => x
88 :     | SOME nvs => if withEff(nvs, ol, nl, tenv)
89 :     then tcc_env_int(x, ol, nl, tenv)
90 :     else x
91 : georgekuan 2013 end
92 :     end)
93 : monnier 16
94 :     fun ltc_env(x, ol, nl, tenv) =
95 :     let val tvs = lt_vs x
96 :     in case tvs
97 :     of NONE => ltc_env_int(x, ol, nl, tenv)
98 :     | SOME [] => x
99 :     | SOME nvs => if withEff (nvs, ol, nl, tenv)
100 :     then ltc_env_int(x, ol, nl, tenv)
101 :     else x
102 :     end
103 :    
104 : macqueen 2014 end (* local -- utility functions for lt_env and tc_env *)
105 : monnier 16
106 :    
107 :     (***************************************************************************
108 :     * UTILITY FUNCTIONS ON REASONING ABOUT REDUCTIONS *
109 :     ***************************************************************************)
110 :    
111 :     (** a list of constructor functions *)
112 :     val tcc_var = tc_injX o TC_VAR
113 :     val tcc_fn = tc_injX o TC_FN
114 : georgekuan 2012 val tcc_app = fn (fntyc, argtycs) =>
115 :     (* Check that parameter arity matches number of arguments
116 :     supplied because type application must be saturated *)
117 :     let fun checkParamArity (tc,tcs) =
118 :     let
119 :     fun getArity(tycEnv) =
120 : macqueen 2014 (case (tc_outX tycEnv)
121 :     of TC_PRIM(ptyc) => PT.pt_arity ptyc
122 : georgekuan 2012 | TC_FN(params, _) => length params
123 :     | (TC_APP(tc, _)) =>
124 :     (case (tc_outX tc)
125 :     of (TC_FN(_, tc')) => getArity tc'
126 :     | _ => 0)
127 :     | (TC_FIX((numFamily,tc,freetycs),index)) =>
128 :     (case (tc_outX tc) of
129 :     (TC_FN (_,tc')) => (* generator function *)
130 :     (case (tc_outX tc') of
131 :     (TC_SEQ tycs) => getArity (List.nth (tycs, index))
132 :     | TC_FN (params, _) => length params
133 :     | _ => raise Fail "Malformed generator range")
134 :     | _ => raise Fail "FIX without generator!" )
135 : macqueen 2014 | _ => (with_pp (fn s =>
136 :     (PU.pps s "getArity?:";
137 :     PP.newline s;
138 :     ppTyc (!dp) s tc;
139 :     PP.newline s));
140 :     0)) (* giving up! *)
141 :     val arity = getArity tc
142 : georgekuan 2012 in
143 : macqueen 2014 if arity = (length tcs) then ()
144 :     else with_pp(fn s =>
145 :     (PU.pps s "TC_APP arity mismatch"; PP.newline s;
146 :     PU.pps s "arity: "; PU.ppi s arity; PP.newline s;
147 :     PU.pps s "no. arguments: "; PU.ppi s (length tcs);
148 :     PP.newline s;
149 :     PU.pps s "operator:"; PP.newline s;
150 :     ppTyc (!dp) s tc; PP.newline s) )
151 : georgekuan 2012 end
152 :     in
153 :     (checkParamArity(fntyc, argtycs);
154 :     (tc_injX o TC_APP) (fntyc, argtycs))
155 :     end
156 : monnier 16 val tcc_seq = tc_injX o TC_SEQ
157 :     val tcc_proj = tc_injX o TC_PROJ
158 :     val tcc_fix = tc_injX o TC_FIX
159 :     val tcc_abs = tc_injX o TC_ABS
160 : monnier 45 val tcc_tup = tc_injX o TC_TUPLE
161 :     val tcc_parw = tc_injX o TC_PARROW
162 : monnier 24 val tcc_box = tc_injX o TC_BOX
163 : monnier 45 val tcc_real = tc_injX (TC_PRIM PT.ptc_real)
164 : monnier 16 val ltc_tyc = lt_injX o LT_TYC
165 :     val ltc_str = lt_injX o LT_STR
166 :     val ltc_fct = lt_injX o LT_FCT
167 :     val ltc_poly = lt_injX o LT_POLY
168 : monnier 45 val tcc_sum = tc_injX o TC_SUM
169 :     val tcc_token = tc_injX o TC_TOKEN
170 : monnier 16
171 : monnier 102 (* The following functions decide on how to flatten the arguments
172 :     * and results of an arbitrary FLINT function. The current threshold
173 :     * is maintained by the "flatten_limit" parameter. This parameter
174 :     * is designed as architecture independent, however, some implicit
175 :     * constraints are:
176 :     * (1) flatten_limit <= numgpregs - numcalleesaves - 3
177 :     * (2) flatten_limit <= numfpregs - 2
178 :     * Right now (2) is in general not true for x86; we inserted a
179 :     * special hack at cpstrans phase to deal with this case. In the
180 :     * long term, if the spilling phase in the backend can offer more
181 :     * supports on large-number of arguments, then we can make this
182 :     * flattening more aggressive. (ZHONG)
183 : monnier 16 *)
184 : monnier 102 val flatten_limit = 9
185 : league 76
186 : macqueen 2014 (* tcUnbound2 -- raised when second index of a deBruijn index pair is
187 :     * out of bounds *)
188 :     exception tcUnbound2
189 :    
190 : monnier 16 fun isKnown tc =
191 :     (case tc_outX(tc_whnm tc)
192 :     of (TC_PRIM _ | TC_ARROW _ | TC_BOX _ | TC_ABS _ | TC_PARROW _) => true
193 :     | (TC_CONT _ | TC_FIX _ | TC_SUM _ | TC_TUPLE _) => true
194 :     | TC_APP(tc, _) => isKnown tc
195 :     | TC_PROJ(tc, _) => isKnown tc
196 : monnier 45 | TC_TOKEN(k, x) => token_isKnown(k, x)
197 : monnier 16 | _ => false)
198 :    
199 :     and tc_autoflat tc =
200 :     let val ntc = tc_whnm tc
201 :     in (case tc_outX ntc
202 : monnier 45 of TC_TUPLE (_, [_]) => (* singleton record is not flattened to ensure
203 : monnier 16 isomorphism btw plambdatype and flinttype *)
204 :     (true, [ntc], false)
205 : monnier 71 | TC_TUPLE (_, []) => (* unit is not flattened to avoid coercions *)
206 :     (true, [ntc], false)
207 : monnier 45 | TC_TUPLE (_, ts) =>
208 : monnier 102 if length ts <= flatten_limit then (true, ts, true)
209 : monnier 45 else (true, [ntc], false) (* ZHONG added the magic number 10 *)
210 : monnier 16 | _ => if isKnown ntc then (true, [ntc], false)
211 :     else (false, [ntc], false))
212 :     end
213 :    
214 :     and tc_autotuple [x] = x
215 : monnier 45 | tc_autotuple xs =
216 : monnier 102 if length xs <= flatten_limit then tcc_tup (RF_TMP, xs)
217 : monnier 45 else bug "fatal error with tc_autotuple"
218 : monnier 16
219 :     and tcs_autoflat (flag, ts) =
220 :     if flag then (flag, ts)
221 :     else (case ts
222 : monnier 45 of [tc] => (let val ntc = tc_whnm tc
223 :     val (nraw, ntcs, _) = tc_autoflat ntc
224 : monnier 16 in (nraw, ntcs)
225 :     end)
226 :     | _ => bug "unexpected cooked multiples in tcs_autoflat")
227 :    
228 :     and lt_autoflat lt =
229 :     (case lt_outX(lt_whnm lt)
230 :     of LT_TYC tc =>
231 :     let val (raw, ts, flag) = tc_autoflat tc
232 :     in (raw, map ltc_tyc ts, flag)
233 :     end
234 :     | _ => (true, [lt], false))
235 :    
236 :     (** a special version of tcc_arw that does automatic flattening *)
237 : monnier 45 and tcc_arw (x as (FF_FIXED, _, _)) = tc_injX (TC_ARROW x)
238 :     | tcc_arw (x as (FF_VAR (true, true), _, _)) = tc_injX (TC_ARROW x)
239 :     | tcc_arw (b as (FF_VAR (b1, b2)), ts1, ts2) =
240 : monnier 16 let val (nb1, nts1) = tcs_autoflat (b1, ts1)
241 :     val (nb2, nts2) = tcs_autoflat (b2, ts2)
242 : monnier 45 in tc_injX (TC_ARROW(FF_VAR(nb1, nb2), nts1, nts2))
243 : monnier 16 end
244 :    
245 :     (** utility function to read the top-level of a tyc *)
246 : macqueen 1993 and tc_lzrd(t: tyc) =
247 : monnier 16 let fun g x =
248 :     (case tc_outX x
249 :     of TC_IND (tc, _) => g tc
250 :     | TC_ENV (tc, i, j, te) =>
251 :     let val ntc = g(h(tc, i, j, te))
252 :     in tyc_upd(x, ntc); ntc
253 :     end
254 :     | _ => x)
255 :    
256 : macqueen 2017 (* [KM ???] claim: h will not return a TC_IND nor a TC_ENV *)
257 :     and h (x, 0, 0, _) = g x (* [KM ???] redundant call to g here? *)
258 :     | h (x, ol, nl, tenv) =
259 : georgekuan 2013 let fun prop z = tcc_env(z, ol, nl, tenv)
260 : macqueen 2014 handle Fail _ =>
261 :     (with_pp(fn s =>
262 :     (PU.pps s "tc_lzrd.prop:"; PP.newline s;
263 :     ppTyc (!dp) s z; PP.newline s));
264 :     raise Fail ("tc_lzrd prop"))
265 : monnier 16 in (case tc_outX x
266 : macqueen 2017 of TC_VAR (n,k) =>
267 : georgekuan 2026 if (n <= ol) then (* n is bound in tenv *)
268 :     (case teLookup(tenv, n)
269 :     of SOME(Lamb(nl', _)) =>
270 :     tcc_var(nl - nl', k) (* rule r5 *)
271 :     | SOME(Beta(nl', ts, _)) =>
272 : macqueen 2017 let val y = List.nth(ts, k)
273 : macqueen 2014 handle Subscript =>
274 :     (with_pp(fn s =>
275 : georgekuan 2026 let val {break,newline,openHVBox,openHOVBox,
276 :     closeBox, pps, ppi} = PU.en_pp s
277 : macqueen 2014 in openHVBox 0;
278 :     pps "***Debugging***"; newline();
279 : georgekuan 2026 pps "tc_lzrd arg: "; PPLty.ppTyc (!dp) s t;
280 :     newline();
281 :     pps "n = "; ppi n; pps ", k = "; ppi k;
282 :     newline();
283 :     pps "length(ts) = : "; ppi (length ts);
284 :     newline();
285 : macqueen 2014 pps "ts elements: "; break{nsp=2,offset=2};
286 :     openHOVBox 2;
287 :     ppList s {sep=",",pp=ppTyc (!dp)} ts;
288 :     closeBox ();
289 :     closeBox ();
290 :     newline(); PP.flushStream s
291 :     end);
292 :     raise tcUnbound2)
293 : georgekuan 2026 in h(y, 0, nl - nl', teEmpty) (* rule r6 *)
294 :     end
295 :     (* Could not find TV(n,_) in tenv
296 :     and ol = length tenv invariant
297 :     failed! *)
298 :     | NONE => raise tcUnbound)
299 : macqueen 2017 else tcc_var(n-ol+nl, k) (* rule r4 *)
300 : monnier 16 | TC_NVAR _ => x
301 : macqueen 2004 | TC_PRIM _ => x (* rule r7 *)
302 : monnier 16 | TC_FN (ks, tc) =>
303 : georgekuan 2026 let val tenv' = teCons(Lamb(nl, ks), tenv)
304 : georgekuan 2013 in tcc_fn(ks,
305 :     tcc_env(tc, ol+1, nl+1, tenv')
306 :     handle Fail _ => raise Fail "tc_lzrd TC_FN") (* rule r10 *)
307 : monnier 16 end
308 : macqueen 2004 | TC_APP (tc, tcs) => tcc_app(prop tc, map prop tcs) (* rule r9 *)
309 : monnier 16 | TC_SEQ tcs => tcc_seq (map prop tcs)
310 :     | TC_PROJ (tc, i) => tcc_proj(prop tc, i)
311 :     | TC_SUM tcs => tcc_sum (map prop tcs)
312 :     | TC_FIX ((n,tc,ts), i) =>
313 :     tcc_fix((n, prop tc, map prop ts), i)
314 :     | TC_ABS tc => tcc_abs (prop tc)
315 :     | TC_BOX tc => tcc_box (prop tc)
316 : monnier 45 | TC_TUPLE (rk, tcs) => tcc_tup (rk, map prop tcs)
317 : monnier 16 | TC_ARROW (r, ts1, ts2) =>
318 : macqueen 2004 tcc_arw (r, map prop ts1, map prop ts2) (* rule r8 *)
319 : monnier 16 | TC_PARROW (t1, t2) => tcc_parw (prop t1, prop t2)
320 : monnier 45 | TC_TOKEN (k, t) => tcc_token(k, prop t)
321 : monnier 16 | TC_CONT _ => bug "unexpected TC_CONT in tc_lzrd"
322 :     | TC_IND (tc, _) => h(tc, ol, nl, tenv)
323 :     | TC_ENV(tc, ol', nl', tenv') =>
324 : macqueen 2004 if ol = 0 then h(tc, ol', nl+nl', tenv') (* rule r11 *)
325 : monnier 16 else h(g x, ol, nl, tenv))
326 :     end (* function h *)
327 :     in if tcp_norm(t) then t else g t
328 :     end (* function tc_lzrd *)
329 :    
330 :     (** utility function to read the top-level of an lty *)
331 :     and lt_lzrd t =
332 :     let fun g x =
333 :     (case lt_outX x
334 :     of LT_IND (lt, _) => g lt
335 :     | LT_ENV(lt, i, j, te) =>
336 :     let val nlt = g(h(lt, i, j, te))
337 :     in lty_upd(x, nlt); nlt
338 :     end
339 :     | _ => x)
340 :    
341 :     and h (x, 0, 0, _) = g x
342 :     | h (x, ol, nl, tenv) =
343 :     let fun prop z = ltc_env(z, ol, nl, tenv)
344 :     in (case lt_outX x
345 :     of LT_TYC tc => ltc_tyc (tcc_env(tc, ol, nl, tenv))
346 :     | LT_STR ts => ltc_str (map prop ts)
347 :     | LT_FCT (ts1, ts2) => ltc_fct(map prop ts1, map prop ts2)
348 :     | LT_POLY (ks, ts) =>
349 : georgekuan 2026 let val tenv' = teCons(Lamb (nl, ks), tenv)
350 : monnier 16 in ltc_poly(ks,
351 :     map (fn t => ltc_env(t, ol+1, nl+1, tenv')) ts)
352 :     end
353 :     | LT_CONT _ => bug "unexpected LT_CONT in lt_lzrd"
354 :     | LT_IND (t, _) => h(t, ol, nl, tenv)
355 :     | LT_ENV (lt, ol', nl', tenv') =>
356 :     if ol = 0 then h(lt, ol', nl+nl', tenv')
357 :     else h(g x, ol, nl, tenv))
358 :     end (* function h *)
359 :     in if ltp_norm(t) then t else g t
360 :     end (* function lt_lzrd *)
361 :    
362 :     (** taking out the TC_IND indirection *)
363 :     and stripInd t = (case tc_outX t of TC_IND (x,_) => stripInd x | _ => t)
364 :    
365 : georgekuan 2012 (*
366 : georgekuan 2006 and printParamArgs (tc,tcs) =
367 : macqueen 2014 let fun getArity(tycEnv) =
368 : georgekuan 2007 (case (tc_outX tycEnv) of
369 :     TC_PRIM(ptyc) => PT.pt_arity ptyc
370 : georgekuan 2009 | TC_FN(params, _) => length params
371 : georgekuan 2007 | (TC_APP(tc, _)) =>
372 :     (case (tc_outX tc)
373 :     of (TC_FN(_, tc')) => getArity tc'
374 :     | _ => 0)
375 :     | (TC_FIX((numFamily,tc,freetycs),index)) =>
376 :     (case (tc_outX tc) of
377 :     (TC_FN (_,tc')) => (* generator function *)
378 :     (case (tc_outX tc') of
379 :     (TC_SEQ tycs) => getArity (List.nth (tycs, index))
380 :     | TC_FN (params, _) => length params
381 :     | _ => raise Fail "Malformed generator range")
382 :     | _ => raise Fail "FIX without generator!" )
383 : macqueen 2014 | _ => (with_pp (fn s => (PP.openHOVBox s (PP.Rel 2);
384 :     PU.pps s "getArity on:";
385 :     ppTyc (!dp) s tc; PP.newline s;
386 :     PP.closeBox s));
387 :     0))
388 :     val arity = getArity tc
389 : georgekuan 2006 in
390 : macqueen 2014 if arity = (length tcs) then ()
391 :     else with_pp(fn s =>
392 :     (PU.pps s "(TC_APP oper:"; PP.break s {nsp=1,offset=2};
393 :     ppTyc (!dp) s tc; PP.newline s;
394 :     PU.pps s "arity:"; PP.break s {nsp=1,offset=0};
395 :     PU.ppi s arity; PP.newline s;
396 :     PU.pps s "no. arguments:"; PP.break s {nsp=1,offset=0};
397 :     PU.ppi s (length tcs); PP.newline s))
398 : georgekuan 2006 end
399 : georgekuan 2012 *)
400 : monnier 16 (** normalizing an arbitrary tyc into a simple weak-head-normal-form *)
401 :     and tc_whnm t = if tcp_norm(t) then t else
402 : georgekuan 2013 let (* val _ = print ">>tc_whnm not norm\n" *)
403 : georgekuan 2006 val nt = tc_lzrd t
404 : monnier 16 in case (tc_outX nt)
405 :     of TC_APP(tc, tcs) =>
406 : georgekuan 2013 ((* print "\ntc_whnm: TC_APP\n"; *)
407 : georgekuan 2026 (let val tc' = tc_whnm tc
408 :     handle Fail _ => raise Fail "TC_APP in tc_whnm 1"
409 : monnier 16 in case (tc_outX tc')
410 :     of TC_FN(ks, b) =>
411 :     let fun base () =
412 : georgekuan 2026 (b, 1, 0, teCons(Beta(0, tcs, ks), teEmpty))
413 : monnier 16 val sp =
414 :     (case tc_outX b
415 :     of TC_ENV(b', ol', nl', te') =>
416 : georgekuan 2026 (case teDest te'
417 :     of SOME(Lamb(n, ks'), te) =>
418 :     if (n = nl'-1) andalso (ol' > 0)
419 :     then (b', ol', n,
420 :     teCons(Beta(n, tcs, ks),
421 :     te))
422 :     (* Which ks correspond to
423 :     this Beta? *)
424 :     else base()
425 : monnier 16 | _ => base())
426 : georgekuan 2013 | _ => base())
427 :     val res = tc_whnm(tcc_env sp)
428 : georgekuan 2026 handle Fail _ =>
429 :     raise Fail "TC_APP in tc_whnm 2"
430 : monnier 16 in tyc_upd(nt, res); res
431 :     end
432 :     | ((TC_SEQ _) | (TC_TUPLE _) | (TC_ARROW _) | (TC_IND _)) =>
433 :     bug "unexpected tycs in tc_whnm-TC_APP"
434 : georgekuan 2012 | _ => let val xx = tcc_app(tc', tcs)
435 : monnier 16 in stripInd xx
436 :     end
437 : georgekuan 2013 end))
438 : monnier 16 | TC_PROJ(tc, i) =>
439 : georgekuan 2013 ((* print "\ntc_whnm: TC_PROJ\n"; *)
440 :     (let val tc' = tc_whnm tc
441 : monnier 16 in (case (tc_outX tc')
442 :     of (TC_SEQ tcs) =>
443 :     let val res = List.nth(tcs, i)
444 :     handle _ => bug "TC_SEQ in tc_whnm"
445 :     val nres = tc_whnm res
446 :     in tyc_upd(nt, nres); nres
447 :     end
448 :     | ((TC_PRIM _) | (TC_NVAR _) | (TC_FIX _) | (TC_FN _) |
449 :     (TC_SUM _) | (TC_ARROW _) | (TC_ABS _) | (TC_BOX _) |
450 :     (TC_IND _) | (TC_TUPLE _)) =>
451 :     bug "unexpected tycs in tc_whnm-TC_PROJ"
452 :     | _ => let val xx = tcc_proj(tc', i)
453 :     in stripInd xx
454 :     end)
455 : georgekuan 2013 end))
456 : monnier 45 | TC_TOKEN(k, tc) =>
457 : georgekuan 2013 ((* print "\ntc_whnm: TC_TOKEN\n"; *)
458 :     (let val tc' = tc_whnm tc
459 : monnier 45 in if token_whnm k tc'
460 :     then let val xx = tcc_token(k, tc') in stripInd xx end
461 :     else let val res = token_reduce(k, tc')
462 :     val nres = tc_whnm res
463 :     in tyc_upd(nt, nres); nres
464 :     end
465 : georgekuan 2013 end))
466 :     | TC_IND (tc, _) => ((*print "\ntc_whnm: TC_IND\n"; *) tc_whnm tc)
467 : monnier 16 | TC_ENV _ => bug "unexpected TC_ENV in tc_whnm"
468 : georgekuan 2013 | _ => ((* print "\ntc_whnm: OTHER\n"; *) nt)
469 : monnier 16 end (* function tc_whnm *)
470 :    
471 :     (** normalizing an arbitrary lty into the simple weak-head-normal-form *)
472 :     and lt_whnm t = if ltp_norm(t) then t else
473 :     let val nt = lt_lzrd t
474 :     in case (lt_outX nt)
475 :     of LT_TYC tc => ltc_tyc(tc_whnm tc)
476 :     | _ => nt
477 :     end (* function lt_whnm *)
478 :    
479 :     (** normalizing an arbitrary tyc into the standard normal form *)
480 :     fun tc_norm t = if (tcp_norm t) then t else
481 :     let val nt = tc_whnm t
482 :     in if (tcp_norm nt) then nt
483 :     else
484 :     (let val res =
485 :     (case (tc_outX nt)
486 :     of TC_FN (ks, tc) => tcc_fn(ks, tc_norm tc)
487 : georgekuan 2006 | TC_APP (tc, tcs) => tcc_app(tc_norm tc, map tc_norm tcs)
488 : monnier 16 | TC_SEQ tcs => tcc_seq(map tc_norm tcs)
489 :     | TC_PROJ (tc, i) => tcc_proj(tc_norm tc, i)
490 :     | TC_SUM tcs => tcc_sum (map tc_norm tcs)
491 :     | TC_FIX ((n,tc,ts), i) =>
492 :     tcc_fix((n, tc_norm tc, map tc_norm ts), i)
493 :     | TC_ABS tc => tcc_abs(tc_norm tc)
494 :     | TC_BOX tc => tcc_box(tc_norm tc)
495 : monnier 45 | TC_TUPLE (rk, tcs) => tcc_tup(rk, map tc_norm tcs)
496 : monnier 16 | TC_ARROW (r, ts1, ts2) =>
497 :     tcc_arw(r, map tc_norm ts1, map tc_norm ts2)
498 :     | TC_PARROW (t1, t2) => tcc_parw(tc_norm t1, tc_norm t2)
499 : monnier 45 | TC_TOKEN (k, t) => tcc_token(k, tc_norm t)
500 : monnier 16 | TC_IND (tc, _) => tc_norm tc
501 :     | TC_ENV _ => bug "unexpected tycs in tc_norm"
502 :     | _ => nt)
503 :     in tyc_upd(nt, res); res
504 :     end)
505 :     end (* function tc_norm *)
506 :    
507 :     (** normalizing an arbitrary lty into the standard normal form *)
508 :     fun lt_norm t = if (ltp_norm t) then t else
509 :     let val nt = lt_lzrd t
510 :     in if (ltp_norm nt) then nt
511 :     else
512 :     (let val res =
513 :     (case lt_outX nt
514 :     of LT_TYC tc => ltc_tyc(tc_norm tc)
515 :     | LT_STR ts => ltc_str(map lt_norm ts)
516 :     | LT_FCT (ts1, ts2) =>
517 :     ltc_fct(map lt_norm ts1, map lt_norm ts2)
518 :     | LT_POLY (ks, ts) => ltc_poly (ks, map lt_norm ts)
519 :     | LT_IND (lt, _) => lt_norm lt
520 :     | _ => bug "unexpected ltys in lt_norm")
521 :     in lty_upd(nt, res); res
522 :     end)
523 :     end (* function lt_norm *)
524 :    
525 :     (***************************************************************************
526 : monnier 45 * REGISTER A NEW TOKEN TYC --- TC_WRAP *
527 :     ***************************************************************************)
528 :    
529 :     (** we add a new constructor named TC_RBOX through the token facility *)
530 :     local val name = "TC_WRAP"
531 :     val abbrev = "WR"
532 :     val is_known = fn _ => true (* why is this ? *)
533 :     fun tcc_tok k t = tcc_token(k, t)
534 :    
535 :     fun unknown tc =
536 :     (case tc_outX tc
537 :     of (TC_VAR _ | TC_NVAR _) => true
538 :     | (TC_APP(tc, _)) => unknown tc
539 :     | (TC_PROJ(tc, _)) => unknown tc
540 :     | _ => false)
541 :    
542 :     fun flex_tuple ts =
543 :     let fun hhh(x::r, ukn, wfree) =
544 :     let fun iswp tc =
545 :     (case tc_outX tc
546 :     of TC_TOKEN(k', t) => (* WARNING: need check k' *)
547 :     (case tc_outX t
548 :     of TC_PRIM pt => false
549 :     | _ => true)
550 :     | _ => true)
551 :     in hhh(r, (unknown x) orelse ukn, (iswp x) andalso wfree)
552 :     end
553 :     | hhh([], ukn, wfree) = ukn andalso wfree
554 :     in hhh(ts, false, true)
555 :     end
556 :    
557 :     fun is_whnm tc =
558 :     (case tc_outX tc
559 :     of (TC_ARROW(FF_FIXED, [t], _)) => (unknown t)
560 :     | (TC_TUPLE(rf, ts)) => flex_tuple ts
561 :     | (TC_PRIM pt) => PT.unboxed pt
562 :     | _ => false)
563 :    
564 :     (* invariants: tc itself is in whnm but is_whnm tc = false *)
565 :     fun reduce_one (k, tc) =
566 :     (case tc_outX tc
567 :     of TC_TUPLE (rk, ts) =>
568 :     let fun hhh (x::r, nts, ukn) =
569 :     let val nx = tc_whnm x
570 :     val b1 = unknown nx
571 :     val nnx =
572 :     (case tc_outX nx
573 :     of TC_TOKEN(k', t) =>
574 :     if token_eq(k, k') then
575 :     (case tc_outX t
576 :     of TC_PRIM _ => t
577 :     | _ => nx)
578 :     else nx
579 :     | _ => nx)
580 :     in hhh(r, nnx::nts, b1 orelse ukn)
581 :     end
582 :     | hhh ([], nts, ukn) =
583 :     let val nt = tcc_tup(rk, rev nts)
584 :     in if ukn then tcc_token(k, nt) else nt
585 :     end
586 :     in hhh(ts, [], false)
587 :     end
588 :     | TC_ARROW (FF_FIXED, [_,_], [_]) => tc
589 :     | TC_ARROW (FF_FIXED, [t1], ts2 as [_]) =>
590 :     let val nt1 = tc_whnm t1
591 :     fun ggg z =
592 :     let val nz = tc_whnm z
593 :     in (case tc_outX nz
594 :     of TC_PRIM pt =>
595 :     if PT.unboxed pt then tcc_token(k, nz)
596 :     else nz
597 :     | _ => nz)
598 :     end
599 :     val (wp, nts1) =
600 :     (case tc_outX nt1
601 :     of TC_TUPLE(_, [x,y]) => (false, [ggg x, ggg y])
602 :     | TC_TOKEN(k', x) =>
603 :     if token_eq(k, k') then
604 :     (case (tc_outX x)
605 :     of TC_TUPLE(_, [y, z]) =>
606 :     (false, [ggg y, ggg z])
607 : monnier 71 | _ => (false, [nt1]))
608 : monnier 45 else (false, [nt1])
609 :     | _ => (unknown nt1, [nt1]))
610 :     val nt = tcc_arw(FF_FIXED, nts1, ts2)
611 :     in if wp then tcc_token(k, nt) else nt
612 :     end
613 :     | TC_ARROW (FF_FIXED, _, _) =>
614 :     bug "unexpected reduce_one on ill-formed FF_FIX arrow types"
615 :     | TC_ARROW (FF_VAR(b1,b2), ts1, ts2) =>
616 :     bug "calling reduce_one on FF_VAR arrow types"
617 :     | TC_PRIM pt =>
618 :     if PT.unboxed pt then
619 :     bug "calling reduce_one on an already-reduced whnm"
620 :     else tc
621 :     | TC_TOKEN(k', t) =>
622 :     if token_eq(k, k') then tc
623 :     else bug "unexpected token in reduce_one"
624 :     | (TC_BOX _ | TC_ABS _ | TC_PARROW _) =>
625 :     bug "unexpected tc_box/abs/parrow in reduce_one"
626 :     | TC_ENV _ => bug "unexpected TC_ENV in reduce_one"
627 :     | TC_IND _ => bug "unexpected TC_IND in reduce_one"
628 :     | _ => tc)
629 :    
630 :     in
631 :    
632 :     val wrap_token =
633 :     register_token {name=name, abbrev=abbrev, reduce_one=reduce_one,
634 :     is_whnm=is_whnm, is_known=is_known}
635 :    
636 :     end (* end of creating the box token for "tcc_rbox" *)
637 :    
638 :     (** testing if a tyc is a unknown constructor *)
639 :     fun tc_unknown tc = not (isKnown tc)
640 :    
641 :     (***************************************************************************
642 : monnier 16 * REBINDING THE INJECTION AND PROJECTION FUNCTIONS *
643 :     ***************************************************************************)
644 :     (** converting from the standard reps to the hash-consing reps *)
645 :     val tk_inj = tk_injX
646 :     val tc_inj = tc_injX
647 :     val lt_inj = lt_injX
648 :    
649 :     (** converting from the hash-consing reps to the standard reps *)
650 :     val tk_out = tk_outX
651 :     val tc_out = tc_outX o tc_whnm
652 :     val lt_out = lt_outX o lt_whnm
653 :    
654 :     (***************************************************************************
655 :     * UTILITY FUNCTIONS ON TESTING EQUIVALENCE *
656 :     ***************************************************************************)
657 :    
658 :     (** testing the equality of values of tkind, tyc, lty *)
659 : league 60 fun eqlist p (x::xs, y::ys) = (p(x,y)) andalso (eqlist p (xs, ys))
660 :     | eqlist p ([], []) = true
661 :     | eqlist _ _ = false
662 : monnier 71
663 : monnier 16 (** testing the equivalence for arbitrary tkinds, tycs and ltys *)
664 :     val tk_eqv = tk_eq (* all tkinds are normalized *)
665 :    
666 : league 60 local (* tyc equivalence utilities *)
667 :     (* The efficiency of checking FIX equivalence could probably be
668 :     * improved somewhat, but it doesn't seem so bad for my purposes right
669 :     * now. Anyway, somebody might eventually want to do some profiling
670 :     * and improve this. --league, 24 March 1998
671 :     *)
672 :    
673 :     (* Profiling code, temporary?? *)
674 :     structure Click =
675 :     struct
676 :     local
677 :     val s_unroll = Stats.makeStat "FIX unrolls"
678 :     in
679 :     fun unroll() = Stats.addStat s_unroll 1
680 :     end
681 :     end (* Click *)
682 : monnier 16
683 : league 60 (** unrolling a fix, tyc -> tyc *)
684 :     fun tc_unroll_fix tyc =
685 :     case tc_outX tyc of
686 :     (TC_FIX((n,tc,ts),i)) => let
687 :     fun genfix i = tcc_fix ((n,tc,ts),i)
688 :     val fixes = List.tabulate(n, genfix)
689 :     val mu = tc
690 :     val mu = if null ts then mu
691 :     else tcc_app (mu,ts)
692 :     val mu = tcc_app (mu, fixes)
693 :     val mu = if n=1 then mu
694 :     else tcc_proj (mu, i)
695 :     in
696 :     Click.unroll();
697 :     mu
698 :     end
699 :     | _ => bug "unexpected non-FIX in tc_unroll_fix"
700 : monnier 16
701 : league 60 (* In order to check equality of two FIXes, we need to be able to
702 :     * unroll them once, and check equality on the unrolled version, with
703 :     * an inductive assumption that they ARE equal. The following code
704 :     * supports making and checking these inductive assumptions.
705 :     * Furthermore, we need to avoid unrolling any FIX more than once.
706 :     *)
707 : monnier 504 structure TcDict = RedBlackMapFn
708 : league 60 (struct
709 :     type ord_key = tyc
710 : monnier 422 val compare = tc_cmp
711 : league 60 end)
712 :     (* for each tyc in this dictionary, we store a dictionary containing
713 :     * tycs that are assumed equivalent to it.
714 :     *)
715 : monnier 422 type eqclass = unit TcDict.map
716 :     type hyp = eqclass TcDict.map
717 : league 60
718 :     (* the null hypothesis, no assumptions about equality *)
719 : monnier 422 val empty_eqclass : eqclass = TcDict.empty
720 :     val null_hyp : hyp = TcDict.empty
721 : league 60
722 :     (* add assumption t1=t2 to current hypothesis. returns composite
723 :     * hypothesis.
724 :     *)
725 :     fun assume_eq' (hyp, t1, t1eqOpt, t2) = let
726 :     val t1eq = case t1eqOpt of SOME e => e | NONE => empty_eqclass
727 :     val t1eq' = TcDict.insert (t1eq, t2, ())
728 :     val hyp' = TcDict.insert (hyp, t1, t1eq')
729 :     in
730 :     hyp'
731 :     end
732 :    
733 :     fun assume_eq (hyp, t1, t1eqOpt, t2, t2eqOpt) =
734 :     assume_eq' (assume_eq' (hyp, t1, t1eqOpt, t2),
735 :     t2, t2eqOpt, t1)
736 :    
737 :     (* check whether t1=t2 according to the hypothesis *)
738 :     val eq_by_hyp : eqclass option * tyc -> bool
739 :     = fn (NONE, t2) => false
740 :     | (SOME eqclass, t2) =>
741 : monnier 422 isSome (TcDict.find (eqclass, t2))
742 : league 60
743 :     (* have we made any assumptions about `t' already? *)
744 :     val visited : eqclass option -> bool
745 :     = isSome
746 :    
747 : monnier 71 (* testing if two recursive datatypes are equivalent *)
748 :     fun eq_fix (eqop1, hyp) (t1, t2) =
749 :     (case (tc_outX t1, tc_outX t2)
750 :     of (TC_FIX((n1,tc1,ts1),i1), TC_FIX((n2,tc2,ts2),i2)) =>
751 : monnier 122 if not (!Control.FLINT.checkDatatypes) then true
752 : league 60 else let
753 : monnier 422 val t1eqOpt = TcDict.find (hyp, t1)
754 : league 60 in
755 :     (* first check the induction hypothesis. we only ever
756 :     * make hypotheses about FIX nodes, so this test is okay
757 :     * here. if assume_eq appears in other cases, this
758 :     * test should be lifted outside the switch.
759 :     *)
760 :     if eq_by_hyp (t1eqOpt, t2) then true
761 :     (* next try structural eq on the components. i'm not sure why
762 :     * this part is necessary, but it does seem to be... --league,
763 :     * 23 March 1998
764 :     *)
765 :     else
766 :     (n1 = n2 andalso i1 = i2 andalso
767 :     eqop1 hyp (tc1, tc2) andalso
768 : monnier 71 eqlist (eqop1 hyp) (ts1, ts2)) orelse
769 : league 60 (* not equal by inspection; we have to unroll it.
770 :     * we prevent unrolling the same FIX twice by asking
771 :     * the `visited' function.
772 :     *)
773 :     if visited t1eqOpt then false
774 :     else let
775 : monnier 422 val t2eqOpt = TcDict.find (hyp, t2)
776 : league 60 in
777 :     if visited t2eqOpt then false
778 :     else eqop1 (assume_eq (hyp, t1, t1eqOpt,
779 :     t2, t2eqOpt))
780 :     (tc_unroll_fix t1, tc_unroll_fix t2)
781 :     end
782 :     end
783 : monnier 71 | _ => bug "unexpected types in eq_fix")
784 :    
785 :    
786 :     (* tc_eqv_generator, invariant: t1 and t2 are in the wh-normal form
787 :     * eqop1 is the default equality to be used for tycs
788 :     * eqop2 is used for body of FN, arguments in APP,
789 :     * eqop3 is used for ABS and BOX.
790 :     * eqop4 is used for arrow arguments and results
791 :     * Each of these first takes the set of hypotheses.
792 :     *)
793 :     fun tc_eqv_gen (eqop1, eqop2, hyp) (t1, t2) =
794 :     case (tc_outX t1, tc_outX t2) of
795 :     (TC_FIX _, TC_FIX _) => eqop2 (eqop1, hyp) (t1, t2)
796 : league 60 | (TC_FN(ks1, b1), TC_FN(ks2, b2)) =>
797 : monnier 71 eqlist tk_eqv (ks1, ks2) andalso eqop1 hyp (b1, b2)
798 : league 60 | (TC_APP(a1, b1), TC_APP(a2, b2)) =>
799 : monnier 71 eqop1 hyp (a1, a2) andalso eqlist (eqop1 hyp) (b1, b2)
800 : league 60 | (TC_SEQ ts1, TC_SEQ ts2) =>
801 :     eqlist (eqop1 hyp) (ts1, ts2)
802 :     | (TC_SUM ts1, TC_SUM ts2) =>
803 :     eqlist (eqop1 hyp) (ts1, ts2)
804 :     | (TC_TUPLE (_, ts1), TC_TUPLE (_, ts2)) =>
805 :     eqlist (eqop1 hyp) (ts1, ts2)
806 :     | (TC_ABS a, TC_ABS b) =>
807 :     eqop1 hyp (a, b)
808 :     | (TC_BOX a, TC_BOX b) =>
809 :     eqop1 hyp (a, b)
810 :     | (TC_TOKEN(k1,t1), TC_TOKEN(k2,t2)) =>
811 :     token_eq(k1,k2) andalso eqop1 hyp (t1,t2)
812 :     | (TC_PROJ(a1, i1), TC_PROJ(a2, i2)) =>
813 :     i1 = i2 andalso eqop1 hyp (a1, a2)
814 :     | (TC_ARROW(r1, a1, b1), TC_ARROW(r2, a2, b2)) =>
815 : monnier 71 r1 = r2 andalso eqlist (eqop1 hyp) (a1, a2)
816 :     andalso eqlist (eqop1 hyp) (b1, b2)
817 : league 60 | (TC_PARROW(a1, b1), TC_PARROW(a2, b2)) =>
818 :     eqop1 hyp (a1, a2) andalso eqop1 hyp (b1, b2)
819 :     | (TC_CONT ts1, TC_CONT ts2) =>
820 :     eqlist (eqop1 hyp) (ts1, ts2)
821 :     | _ => false
822 :    
823 :     (** general equality for tycs *)
824 : macqueen 2014 fun tc_eqv' hyp (x, y) =
825 :     let val t1 = tc_whnm x
826 : league 60 val t2 = tc_whnm y
827 :     in
828 :     if tcp_norm t1 andalso tcp_norm t2 then tc_eq (t1, t2)
829 : macqueen 2014 else tc_eqv_gen (tc_eqv', fn _ => tc_eq, hyp) (t1, t2)
830 : league 60 end (* tc_eqv' *)
831 :    
832 :     (* slightly relaxed constraints (???) *)
833 :     fun tc_eqv_x' hyp (x, y) =
834 : macqueen 2014 let val t1 = tc_whnm x
835 :     val t2 = tc_whnm y
836 :     in (if (tcp_norm t1) andalso (tcp_norm t2) then tc_eq(t1, t2)
837 :     else false) orelse
838 :     (tc_eqv_gen (tc_eqv_x', eq_fix, hyp) (t1, t2))
839 :     end (* function tc_eqv_x' *)
840 : monnier 45
841 : league 60 in (* tyc equivalence utilities *)
842 :    
843 :     val tc_eqv = tc_eqv' null_hyp
844 :     val tc_eqv_x = tc_eqv_x' null_hyp
845 : monnier 16
846 : league 60 end (* tyc equivalence utilities *)
847 :    
848 : monnier 71
849 : monnier 16 (** lt_eqv_generator, invariant: x and y are in the wh-normal form *)
850 :     fun lt_eqv_gen (eqop1, eqop2) (x : lty, y) =
851 : monnier 102 let (* seq should be called if t1 and t2 are weak-head normal form *)
852 : monnier 16 fun seq (t1, t2) =
853 :     (case (lt_outX t1, lt_outX t2)
854 :     of (LT_POLY(ks1, b1), LT_POLY(ks2, b2)) =>
855 : league 60 (eqlist tk_eqv (ks1, ks2)) andalso (eqlist eqop1 (b1, b2))
856 : monnier 16 | (LT_FCT(as1, bs1), LT_FCT(as2, bs2)) =>
857 : league 60 (eqlist eqop1 (as1, as2)) andalso (eqlist eqop1 (bs1, bs2))
858 : monnier 16 | (LT_TYC a, LT_TYC b) => eqop2(a, b)
859 : league 60 | (LT_STR s1, LT_STR s2) => eqlist eqop1 (s1, s2)
860 :     | (LT_CONT s1, LT_CONT s2) => eqlist eqop1 (s1, s2)
861 : monnier 16 | _ => false)
862 :     in seq(x, y)
863 :     end (* function lt_eqv_gen *)
864 :    
865 :     fun lt_eqv(x : lty, y) =
866 :     let val seq = lt_eqv_gen (lt_eqv, tc_eqv)
867 : monnier 102 in if ((ltp_norm x) andalso (ltp_norm y)) then lt_eq(x,y)
868 : monnier 16 else (let val t1 = lt_whnm x
869 :     val t2 = lt_whnm y
870 : monnier 102 in if (ltp_norm t1) andalso (ltp_norm t2) then lt_eq(x, y)
871 : monnier 16 else seq(t1, t2)
872 :     end)
873 :     end (* function lt_eqv *)
874 :    
875 : monnier 45 fun lt_eqv_x(x : lty, y) =
876 :     let val seq = lt_eqv_gen (lt_eqv_x, tc_eqv_x)
877 :     in if ((ltp_norm x) andalso (ltp_norm y)) then
878 :     (lt_eq(x, y)) orelse (seq(x, y))
879 :     else (let val t1 = lt_whnm x
880 :     val t2 = lt_whnm y
881 :     in if (ltp_norm t1) andalso (ltp_norm t2) then
882 :     (lt_eq(t1, t2)) orelse (seq(t1, t2))
883 :     else seq(t1, t2)
884 :     end)
885 :     end (* function lt_eqv *)
886 :    
887 :     (** testing equivalence of fflags and rflags *)
888 : mblume 1335 fun ff_eqv (FF_VAR (b1, b2), FF_VAR (b1', b2')) = b1 = b1' andalso b2 = b2'
889 :     | ff_eqv (FF_FIXED, FF_FIXED) = true
890 :     | ff_eqv ((FF_FIXED, FF_VAR _) | (FF_VAR _, FF_FIXED)) = false
891 : macqueen 2014
892 : mblume 1335 fun rf_eqv (RF_TMP, RF_TMP) = true
893 : monnier 45
894 :     (***************************************************************************
895 :     * UTILITY FUNCTIONS ON FINDING OUT THE DEPTH OF THE FREE TYC VARIABLES *
896 :     ***************************************************************************)
897 :     (** finding out the innermost binding depth for a tyc's free variables *)
898 :     fun tc_depth (x, d) =
899 : macqueen 2014 (* unfortunately we have to reduce everything to normal form
900 :     * before we can talk about its list of free type variables. *)
901 :     (case tc_vs (tc_norm x)
902 : monnier 45 of NONE => bug "unexpected case in tc_depth"
903 :     | SOME [] => DI.top
904 : macqueen 2014 | SOME (a::_) => d + 1 - (#1(tvDecode a)))
905 : monnier 45
906 :     fun tcs_depth ([], d) = DI.top
907 :     | tcs_depth (x::r, d) = Int.max(tc_depth(x, d), tcs_depth(r, d))
908 :    
909 : macqueen 2014 (* these return the list of free NAMED tyvars, after nomalization *)
910 : monnier 197 fun tc_nvars (tyc:tyc) =
911 : macqueen 2014 Lty.tc_nvars(tc_norm tyc)
912 : monnier 197
913 : macqueen 2014 fun lt_nvars (lty:lty) =
914 :     Lty.lt_nvars(lt_norm lty)
915 : monnier 197
916 : monnier 16 end (* abstraction LtyKernel *)

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