SCM Repository
View of /sml/trunk/src/compiler/FLINT/kernel/ltykernel.sml
Parent Directory
|
Revision Log
Revision 76 -
(download)
(annotate)
Sun Apr 12 02:23:26 1998 UTC (24 years, 2 months ago) by league
File size: 50881 byte(s)
Sun Apr 12 02:23:26 1998 UTC (24 years, 2 months ago) by league
File size: 50881 byte(s)
changed max # elements to flatten to 5, to support x86 floating points. should be made machine dependent?
(* COPYRIGHT (c) 1997 YALE FLINT PROJECT *) (* ltykernel.sml *) structure LtyKernel :> LTYKERNEL = struct fun bug s = ErrorMsg.impossible ("LtyKernel:" ^ s) (*************************************************************************** * UTILITY FUNCTIONS FOR HASHCONSING BASICS * ***************************************************************************) (** hashconsing implementation basics *) local open SortedList val MVAL = 10000 val BVAL = MVAL * 2 (* all index i start from 0 *) in type enc_tvar = int fun tvEncode (d, i) = d * MVAL + i fun tvDecode x = ((x div MVAL), (x mod MVAL)) fun exitLevel xs = let fun h ([], x) = rev x | h (a::r, x) = if a < BVAL then h(r, x) else h(r, (a-MVAL)::x) in h(xs, []) end datatype aux_info = AX_REG of bool * enc_tvar list | AX_NO val mergeTvs = merge val fmergeTvs = foldmerge type 'a hash_cell = (int * 'a * aux_info) ref end (* local of hashconsing implementation basics *) (*************************************************************************** * DATATYPE DEFINITIONS * ***************************************************************************) (** definition of kinds for all the lambda tycs *) datatype tkindI = TK_MONO (* ground mono tycon *) | TK_BOX (* boxed/tagged tycon *) | TK_SEQ of tkind list (* sequence of tycons *) | TK_FUN of tkind list * tkind (* tycon function *) withtype tkind = tkindI hash_cell (* hash-consing-impl of tkind *) (* definitoins of named tyc variables *) type tvar = LambdaVar.lvar (* temporary definitions *) val mkTvar = LambdaVar.mkLvar (* an special extensible token key *) type token = int datatype fflag (* calling conventions *) = FF_VAR of bool * bool (* is it fixed ? *) | FF_FIXED (* used after rep. analysis *) datatype rflag = RF_TMP (* tuple kind: a template *) (** definitions of lambda type constructors *) datatype tycI = TC_VAR of DebIndex.index * int (* tyc variables *) | TC_NVAR of tvar * DebIndex.depth * int (* named tyc variables *) | TC_PRIM of PrimTyc.primtyc (* primitive tyc *) | TC_FN of tkind list * tyc (* tyc abstraction *) | TC_APP of tyc * tyc list (* tyc application *) | TC_SEQ of tyc list (* tyc sequence *) | TC_PROJ of tyc * int (* tyc projection *) | TC_SUM of tyc list (* sum tyc *) | TC_FIX of (int * tyc * tyc list) * int (* recursive tyc *) | TC_TUPLE of rflag * tyc list (* std record tyc *) | TC_ARROW of fflag * tyc list * tyc list (* std function tyc *) | TC_PARROW of tyc * tyc (* special fun tyc, not used *) | TC_BOX of tyc (* boxed tyc *) | TC_ABS of tyc (* abstract tyc, not used *) | TC_TOKEN of token * tyc (* extensible token tyc *) | TC_CONT of tyc list (* intern continuation tycon *) | TC_IND of tyc * tycI (* indirect tyc thunk *) | TC_ENV of tyc * int * int * tycEnv (* tyc closure *) withtype tyc = tycI hash_cell (* hash-consed tyc cell *) and tycEnv = tyc (* * This really is (tyc list option * int) list, * it is encoded using SEQ[(PROJ(SEQ tcs),i)] * and SEQ[(PROJ(VOID, i))]. (ZHONG) *) (** definitions of lambda types *) datatype ltyI = LT_TYC of tyc (* monomorphic type *) | LT_STR of lty list (* structure record type *) | LT_FCT of lty list * lty list (* functor arrow type *) | LT_POLY of tkind list * lty list (* polymorphic type *) | LT_PST of (int * lty) list (* partial-structure type *) | LT_CONT of lty list (* internal cont type *) | LT_IND of lty * ltyI (* a lty thunk and its sig *) | LT_ENV of lty * int * int * tycEnv (* lty closure *) withtype lty = ltyI hash_cell (* hash-consed lty cell *) (*************************************************************************** * TOKEN TYC UTILITY FUNCTIONS * ***************************************************************************) type token_info = {name : string, abbrev : string, reduce_one: token * tyc -> tyc, is_whnm : tyc -> bool, is_known : token * tyc -> bool} local val token_key = ref 0 val token_table_size = 10 val default_token_info = {name="TC_GARBAGE", abbrev="GB", reduce_one=(fn _ => bug "token not implemented"), is_whnm=(fn _ => bug "token not implemented"), is_known=(fn _ => bug "token not implemented")} val token_array : token_info Array.array = Array.array(token_table_size,default_token_info) val token_validity_table = Array.array(token_table_size,false) fun get_next_token () = let val n = !token_key in if n > token_table_size then bug "running out of tokens" else (token_key := n+1; n) end fun store_token_info (x, k) = Array.update(token_array, k, x) fun get_is_whnm k = #is_whnm (Array.sub(token_array, k)) fun get_reduce_one (z as (k, t)) = (#reduce_one (Array.sub(token_array, k))) z fun get_name k = #name (Array.sub(token_array, k)) fun get_abbrev k = #abbrev (Array.sub(token_array, k)) fun get_is_known (z as (k, t)) = (#is_known (Array.sub(token_array, k))) z fun is_valid k = Array.sub(token_validity_table, k) fun set_valid k = Array.update(token_validity_table, k, true) in val register_token: token_info -> token = (fn x => let val k = get_next_token () in store_token_info(x, k); set_valid k; k end) val token_name : token -> string = get_name val token_abbrev : token -> string = get_abbrev val token_whnm : token -> tyc -> bool = get_is_whnm val token_reduce : token * tyc -> tyc = get_reduce_one val token_isKnown : token * tyc -> bool = get_is_known val token_isvalid : token -> bool = is_valid val token_eq : token * token -> bool = fn (x,y) => (x=y) val token_int : token -> int = fn x => x val token_key : int -> token = fn x => x end (* end of all token-related hacks *) (*************************************************************************** * HASHCONSING IMPLEMENTATIONS * ***************************************************************************) (** Hash-consing implementations of tyc, tkind, lty *) local structure Weak = SMLofNJ.Weak structure PT = PrimTyc structure DI = DebIndex fun bug msg = ErrorMsg.impossible("LtyKernel: "^msg) val itow = Word.fromInt val wtoi = Word.toIntX val andb = Word.andb val N = 2048 (* 1024 *) val NN = itow (N*N) val P = 0w509 (* was 0w1019, a prime < 1024 so that N*N*P < maxint *) val tk_table : tkind Weak.weak list Array.array = Array.array(N,nil) val tc_table : tyc Weak.weak list Array.array = Array.array(N,nil) val lt_table : lty Weak.weak list Array.array = Array.array(N,nil) fun vector2list v = Vector.foldr (op ::) [] v fun revcat(a::rest,b) = revcat(rest,a::b) | revcat(nil,b) = b fun combine [x] = itow x | combine (a::rest) = andb(itow a +(combine rest)*P, NN - 0w1) | combine _ = bug "unexpected case in combine" (* * Because of the "cmp" function below, it's necessary to keep * each bucket-list in a consistent order, and not reverse * or move-to-front or whatever. *) fun look(table, h, t, eq, mk) = let val i = wtoi(andb(itow h, itow(N-1))) fun g(l, z as (w::rest)) = (case Weak.strong w of SOME (r as ref(h',t',_)) => if (h=h') andalso (eq {new=t, old=t'}) then (Array.update(table, i, revcat(l,z)); r) else g(w::l, rest) | NONE => g(l, rest)) | g(l, []) = let val r = mk(h, t) in Array.update(table, i, (Weak.weak r) :: rev l); r end in g([], Array.sub(table, i)) end fun cmp(table, a as ref(ai,_,_), b as ref (bi,_,_)) = if ai < bi then LESS else if ai > bi then GREATER else if a = b then EQUAL else let val index = wtoi (andb(itow ai,itow(N-1))) fun g [] = bug "unexpected case in cmp" | g (w::rest) = (case Weak.strong w of SOME r => if a=r then LESS else if b=r then GREATER else g rest | NONE => g rest) in g(Array.sub(table,index)) end fun getnum (ref(i,_,_)) = i fun tagnums nil = nil | tagnums ((i,t)::rest) = i::getnum t::tagnums rest fun tk_hash tk = let fun g (TK_MONO) = 0w1 | g (TK_BOX) = 0w2 | g (TK_SEQ ks) = combine (3::map getnum ks) | g (TK_FUN(ks, k)) = combine (4::getnum k::(map getnum ks)) in g tk end fun tc_hash tc = let fun g (TC_VAR(d, i)) = combine [1, (DI.di_key d)*10, i] | g (TC_NVAR(v, d, i)) = combine[15, v, (DI.dp_key d)*13, i] | g (TC_PRIM pt) = combine [2, PT.pt_toint pt] | g (TC_FN(ks, t)) = combine (3::(getnum t)::(map getnum ks)) | g (TC_APP(t, ts)) = combine (4::(getnum t)::(map getnum ts)) | g (TC_SEQ ts) = combine (5::(map getnum ts)) | g (TC_PROJ(t, i)) = combine [6, (getnum t), i] | g (TC_SUM ts) = combine (7::(map getnum ts)) | g (TC_FIX((n, t, ts), i)) = combine (8::n::i::(getnum t)::(map getnum ts)) | g (TC_ABS t) = combine [9, getnum t] | g (TC_BOX t) = combine [10, getnum t] | g (TC_TUPLE (_, ts)) = combine (11::(map getnum ts)) | g (TC_ARROW(rw, ts1, ts2)) = let fun h (FF_FIXED) = 10 | h (FF_VAR(true,b2)) = if b2 then 20 else 30 | h (FF_VAR(false,b2)) = if b2 then 40 else 50 in combine (12::(h rw)::(map getnum (ts1@ts2))) end | g (TC_PARROW (t1,t2)) = combine [13, getnum t1, getnum t2] | g (TC_TOKEN (i, tc)) = combine [14, i, getnum tc] | g (TC_CONT ts) = combine (15::(map getnum ts)) | g (TC_ENV(t,i,j,env)) = combine[16, getnum t, i, j, getnum env] | g (TC_IND _) = bug "unexpected TC_IND in tc_hash" in g tc end fun lt_hash lt = let fun g (LT_TYC t) = combine [1, getnum t] | g (LT_STR ts) = combine (2::(map getnum ts)) | g (LT_PST ts) = combine (3::(tagnums ts)) | g (LT_FCT(ts1, ts2)) = combine (4::(map getnum (ts1@ts2))) | g (LT_POLY(ks, ts)) = combine (5::((map getnum ts)@(map getnum ks))) | g (LT_CONT ts) = combine (6::(map getnum ts)) | g (LT_ENV(t,i,j,env)) = combine [7, getnum t, i, j, getnum env] | g (LT_IND _) = bug "unexpected LT_IND in tc_hash" in g lt end fun tkI_eq {new: tkindI, old} = (new = old) (* the 1st is one being mapped; the 2nd is in the hash table *) fun tcI_eq {new : tycI, old=TC_IND(_,s)} = tcI_eq {new=new, old=s} | tcI_eq {new, old} = (new=old) fun ltI_eq {new : ltyI, old=LT_IND(_,s)} = ltI_eq {new=new, old=s} | ltI_eq {new, old} = (new=old) val baseAux = AX_REG (true, []) fun getAux (ref(i : int, _, x)) = x fun mergeAux(AX_NO, _) = AX_NO | mergeAux(_, AX_NO) = AX_NO | mergeAux(AX_REG(b1,vs1), AX_REG(b2,vs2)) = AX_REG(b2 andalso b1, mergeTvs(vs1, vs2)) fun fsmerge [] = baseAux | fsmerge [x] = getAux x | fsmerge xs = let fun loop([], z) = z | loop(_, AX_NO) = AX_NO | loop(a::r, z) = loop(r, mergeAux(getAux a, z)) in loop(xs, baseAux) end fun exitAux(AX_REG(b, vs)) = AX_REG(b, exitLevel vs) | exitAux x = x fun tc_aux tc = let fun g (TC_VAR(d, i)) = AX_REG(true, [tvEncode(d, i)]) | g (TC_NVAR(v, d, i)) = baseAux (*** THIS IS WRONG ! ***) | g (TC_PRIM pt) = baseAux | g (TC_APP(ref(_, TC_FN _, AX_NO), _)) = AX_NO | g (TC_PROJ(ref(_, TC_SEQ _, AX_NO), _)) = AX_NO | g (TC_APP(ref(_, TC_FN _, AX_REG(_,vs)), ts)) = mergeAux(AX_REG(false, vs), fsmerge ts) (* ? *) | g (TC_PROJ(ref(_, TC_SEQ _, AX_REG(_,vs)), _)) = AX_REG(false, vs) (* ? *) | g (TC_FN(ks, t)) = exitAux(getAux t) | g (TC_APP(t, ts)) = fsmerge (t::ts) | g (TC_SEQ ts) = fsmerge ts | g (TC_PROJ(t, _)) = getAux t | g (TC_SUM ts) = fsmerge ts | g (TC_FIX((_,t,ts), _)) = let val ax = getAux t in case ax of AX_REG(_,[]) => mergeAux(ax, fsmerge ts) | _ => bug "unexpected TC_FIX freevars in tc_aux" end | g (TC_ABS t) = getAux t | g (TC_BOX t) = getAux t | g (TC_TUPLE (_, ts)) = fsmerge ts | g (TC_ARROW(_, ts1, ts2)) = fsmerge (ts1@ts2) | g (TC_PARROW(t1, t2)) = fsmerge [t1, t2] | g (TC_TOKEN (k, (ref(_, t, AX_NO)))) = AX_NO | g (TC_TOKEN (k, (x as ref(_, t, AX_REG(b,vs))))) = AX_REG((token_whnm k x) andalso b, vs) | g (TC_CONT ts) = fsmerge ts | g (TC_IND _) = bug "unexpected TC_IND in tc_aux" | g (TC_ENV _) = AX_NO in g tc end fun lt_aux lt = let fun g (LT_TYC t) = getAux t | g (LT_STR ts) = fsmerge ts | g (LT_PST ts) = fsmerge (map #2 ts) | g (LT_FCT(ts1, ts2)) = fsmerge (ts1@ts2) | g (LT_POLY(ks, ts)) = exitAux(fsmerge ts) | g (LT_CONT ts) = fsmerge ts | g (LT_IND _) = bug "unexpected LT_IND in lt_aux" | g (LT_ENV _) = AX_NO in g lt end fun tk_mk (i : int, k: tkindI) = ref (i, k, AX_NO) fun tc_mk (i : int, tc : tycI) = ref (i, tc, tc_aux tc) fun lt_mk (i : int, lt : ltyI) = ref (i, lt, lt_aux lt) in (** a temporary hack on getting the list of free tyvars *) fun tc_vs (r as ref(_ : int, _ : tycI, AX_NO)) = NONE | tc_vs (r as ref(_ : int, _ : tycI, AX_REG (_,x))) = SOME x fun lt_vs (r as ref(_ : int, _ : ltyI, AX_NO)) = NONE | lt_vs (r as ref(_ : int, _ : ltyI, AX_REG (_,x))) = SOME x (** converting from the hash-consing reps to the standard reps *) fun tk_outX (r as ref(_ : int, t : tkindI, _ : aux_info)) = t fun tc_outX (r as ref(_ : int, t : tycI, _ : aux_info)) = t fun lt_outX (r as ref(_ : int, t : ltyI, _ : aux_info)) = t (** converting from the standard reps to the hash-consing reps *) fun tk_injX t = look(tk_table, wtoi(tk_hash t), t, tkI_eq, tk_mk) fun tc_injX t = look(tc_table, wtoi(tc_hash t), t, tcI_eq, tc_mk) fun lt_injX t = look(lt_table, wtoi(lt_hash t), t, ltI_eq, lt_mk) (** key-comparison on tkind, tyc, lty *) fun tk_cmp (k1, k2) = cmp(tk_table, k1, k2) fun tc_cmp (t1, t2) = cmp(tc_table, t1, t2) fun lt_cmp (t1, t2) = cmp(lt_table, t1, t2) (** get the hash key of each lty, only used by reps/coerce.sml; a hack *) fun lt_key (ref (h : int, _ : ltyI, _ : aux_info)) = h (*************************************************************************** * UTILITY FUNCTIONS ON TKIND ENVIRONMENT * ***************************************************************************) (** tkind environment: maps each tyvar, i.e., its debindex, to its kind *) type tkindEnv = tkind list list (** utility functions for manipulating the tkindEnv *) exception tkUnbound val initTkEnv : tkindEnv = [] fun tkLookup (kenv, i, j) = let val ks = List.nth(kenv, i-1) handle _ => raise tkUnbound in List.nth(ks, j) handle _ => raise tkUnbound end fun tkInsert (kenv, ks) = ks::kenv (* strip any unused type variables out of a kenv, given a list of * [encoded] free type variables. the result is a "parallel list" of * the kinds of those free type variables in the environment. * This is meant to use the same representation of a kind environment * as in ltybasic. * --CALeague *) fun tkLookupFreeVars (kenv, tyc) = let fun g (kenv, d, []) = [] | g (kenv, d, ftv::ftvs) = let val (d', i') = tvDecode ftv val kenv' = List.drop (kenv, d'-d) handle _ => raise tkUnbound val k = List.nth (hd kenv', i') handle _ => raise tkUnbound val rest = g (kenv', d', ftvs) in k :: rest end fun h ftvs = g (kenv, 1, ftvs) in Option.map h (tc_vs tyc) end (*************************************************************************** * UTILITY FUNCTIONS ON TYC ENVIRONMENT * ***************************************************************************) (** utility functions for manipulating the tycEnv *) local val tc_void = tc_injX(TC_PRIM(PT.ptc_void)) fun tc_cons (t, b) = tc_injX(TC_ARROW(FF_FIXED, [t],[b])) fun tc_interp x = (case tc_outX x of TC_PROJ(y, i) => (case tc_outX y of TC_SEQ ts => (SOME ts, i) | TC_PRIM _ => (NONE, i) | _ => bug "unexpected tycEnv1 in tc_interp") | _ => bug "unexpected tycEnv2 in tc_interp") fun tc_encode(NONE, i) = tc_injX(TC_PROJ(tc_void,i)) | tc_encode(SOME ts, i) = tc_injX(TC_PROJ(tc_injX(TC_SEQ(ts)), i)) in exception tcUnbound val initTycEnv : tycEnv = tc_void fun tcLookup(i, tenv : tycEnv) = if i > 1 then (case tc_outX tenv of TC_ARROW(_,_,[x]) => tcLookup(i-1, x) | _ => bug "unexpected tycEnv in tcLookup") else if i = 1 then (case tc_outX tenv of TC_ARROW(_,[x],_) => tc_interp x | _ => raise tcUnbound) else bug "unexpected argument in tcLookup" fun tcInsert(tenv : tycEnv, et) = tc_cons(tc_encode et, tenv) fun tcSplit(tenv : tycEnv) = (case tc_outX tenv of TC_ARROW(_,[x],[y]) => SOME (tc_interp x, y) | _ => NONE) end (* utililty function for tycEnv *) (** checking if a tyc or an lty is in the normal form *) fun tcp_norm ((t as ref (i, _, AX_REG(b,_))) : tyc) = b | tcp_norm _ = false fun ltp_norm ((t as ref (i, _, AX_REG(b,_))) : lty) = b | ltp_norm _ = false (** utility functions for tc_env and lt_env *) local fun tcc_env_int(x, 0, 0, te) = x | tcc_env_int(x, i, j, te) = tc_injX(TC_ENV(x, i, j, te)) fun ltc_env_int(x, 0, 0, te) = x | ltc_env_int(x, i, j, te) = lt_injX(LT_ENV(x, i, j, te)) fun withEff ([], ol, nl, tenv) = false | withEff (a::r, ol, nl, tenv) = let val (i, j) = tvDecode a val neweff = if i > ol then (ol <> nl) else (* case tcLookup(i, tenv) of (NONE, n) => (nl - n) <> i | (SOME ts, n) => (let val y = List.nth(ts, j) in (case tc_outX y of TC_VAR(ni, nj) => ((nj <> j) orelse ((ni+nl-n) <> i)) | _ => true) end) *) true in neweff orelse (withEff(r, ol, nl, tenv)) end in fun tcc_env(x, ol, nl, tenv) = let val tvs = tc_vs x in case tvs of NONE => tcc_env_int(x, ol, nl, tenv) | SOME [] => x | SOME nvs => if withEff(nvs, ol, nl, tenv) then tcc_env_int(x, ol, nl, tenv) else x end fun ltc_env(x, ol, nl, tenv) = let val tvs = lt_vs x in case tvs of NONE => ltc_env_int(x, ol, nl, tenv) | SOME [] => x | SOME nvs => if withEff (nvs, ol, nl, tenv) then ltc_env_int(x, ol, nl, tenv) else x end end (* utility functions for lt_env and tc_env *) (** utility functions for updating tycs and ltys *) fun tyc_upd (tgt as ref(i : int, old : tycI, AX_NO), nt) = (tgt := (i, TC_IND (nt, old), AX_NO)) | tyc_upd (tgt as ref(i : int, old : tycI, x as (AX_REG(false, _))), nt) = (tgt := (i, TC_IND (nt, old), x)) | tyc_upd _ = bug "unexpected tyc_upd on already normalized tyc" fun lty_upd (tgt as ref(i : int, old : ltyI, AX_NO), nt) = (tgt := (i, LT_IND (nt, old), AX_NO)) | lty_upd (tgt as ref(i : int, old : ltyI, x as (AX_REG(false, _))), nt) = (tgt := (i, LT_IND (nt, old), x)) | lty_upd _ = bug "unexpected lty_upd on already normalized lty" (*************************************************************************** * UTILITY FUNCTIONS ON REASONING ABOUT REDUCTIONS * ***************************************************************************) (** a list of constructor functions *) val tcc_var = tc_injX o TC_VAR val tcc_fn = tc_injX o TC_FN val tcc_app = tc_injX o TC_APP val tcc_seq = tc_injX o TC_SEQ val tcc_proj = tc_injX o TC_PROJ val tcc_fix = tc_injX o TC_FIX val tcc_abs = tc_injX o TC_ABS val tcc_tup = tc_injX o TC_TUPLE val tcc_parw = tc_injX o TC_PARROW val tcc_box = tc_injX o TC_BOX val tcc_real = tc_injX (TC_PRIM PT.ptc_real) val ltc_tyc = lt_injX o LT_TYC val ltc_str = lt_injX o LT_STR val ltc_pst = lt_injX o LT_PST val ltc_fct = lt_injX o LT_FCT val ltc_poly = lt_injX o LT_POLY val tcc_sum = tc_injX o TC_SUM val tcc_token = tc_injX o TC_TOKEN (** the following function contains the procedure on how to * flatten the arguments and results of an arbitrary FLINT function *) val maxFlat = 5 (* most number of args to flatten *) fun isKnown tc = (case tc_outX(tc_whnm tc) of (TC_PRIM _ | TC_ARROW _ | TC_BOX _ | TC_ABS _ | TC_PARROW _) => true | (TC_CONT _ | TC_FIX _ | TC_SUM _ | TC_TUPLE _) => true | TC_APP(tc, _) => isKnown tc | TC_PROJ(tc, _) => isKnown tc | TC_TOKEN(k, x) => token_isKnown(k, x) | _ => false) and tc_autoflat tc = let val ntc = tc_whnm tc in (case tc_outX ntc of TC_TUPLE (_, [_]) => (* singleton record is not flattened to ensure isomorphism btw plambdatype and flinttype *) (true, [ntc], false) | TC_TUPLE (_, []) => (* unit is not flattened to avoid coercions *) (true, [ntc], false) | TC_TUPLE (_, ts) => if length ts < maxFlat then (true, ts, true) else (true, [ntc], false) (* ZHONG added the magic number 10 *) | _ => if isKnown ntc then (true, [ntc], false) else (false, [ntc], false)) end and tc_autotuple [x] = x | tc_autotuple xs = if length xs < maxFlat then tcc_tup (RF_TMP, xs) else bug "fatal error with tc_autotuple" and tcs_autoflat (flag, ts) = if flag then (flag, ts) else (case ts of [tc] => (let val ntc = tc_whnm tc val (nraw, ntcs, _) = tc_autoflat ntc in (nraw, ntcs) end) | _ => bug "unexpected cooked multiples in tcs_autoflat") and lt_autoflat lt = (case lt_outX(lt_whnm lt) of LT_TYC tc => let val (raw, ts, flag) = tc_autoflat tc in (raw, map ltc_tyc ts, flag) end | _ => (true, [lt], false)) (** a special version of tcc_arw that does automatic flattening *) and tcc_arw (x as (FF_FIXED, _, _)) = tc_injX (TC_ARROW x) | tcc_arw (x as (FF_VAR (true, true), _, _)) = tc_injX (TC_ARROW x) | tcc_arw (b as (FF_VAR (b1, b2)), ts1, ts2) = let val (nb1, nts1) = tcs_autoflat (b1, ts1) val (nb2, nts2) = tcs_autoflat (b2, ts2) in tc_injX (TC_ARROW(FF_VAR(nb1, nb2), nts1, nts2)) end (** utility function to read the top-level of a tyc *) and tc_lzrd t = let fun g x = (case tc_outX x of TC_IND (tc, _) => g tc | TC_ENV (tc, i, j, te) => let val ntc = g(h(tc, i, j, te)) in tyc_upd(x, ntc); ntc end | _ => x) and h (x, 0, 0, _) = g x | h (x, ol, nl, tenv) = let fun prop z = tcc_env(z, ol, nl, tenv) in (case tc_outX x of TC_VAR (i,j) => if (i <= ol) then (let val et = tcLookup(i, tenv) in case et of (NONE, n) => tcc_var(nl - n, j) | (SOME ts, n) => (let val y = List.nth(ts, j) handle _ => raise tcUnbound in h(y, 0, nl - n, initTycEnv) end) end) else tcc_var(i-ol+nl, j) | TC_NVAR _ => x | TC_PRIM _ => x | TC_FN (ks, tc) => let val tenv' = tcInsert(tenv, (NONE, nl)) in tcc_fn(ks, tcc_env(tc, ol+1, nl+1, tenv')) end | TC_APP (tc, tcs) => tcc_app(prop tc, map prop tcs) | TC_SEQ tcs => tcc_seq (map prop tcs) | TC_PROJ (tc, i) => tcc_proj(prop tc, i) | TC_SUM tcs => tcc_sum (map prop tcs) | TC_FIX ((n,tc,ts), i) => tcc_fix((n, prop tc, map prop ts), i) | TC_ABS tc => tcc_abs (prop tc) | TC_BOX tc => tcc_box (prop tc) | TC_TUPLE (rk, tcs) => tcc_tup (rk, map prop tcs) | TC_ARROW (r, ts1, ts2) => tcc_arw (r, map prop ts1, map prop ts2) | TC_PARROW (t1, t2) => tcc_parw (prop t1, prop t2) | TC_TOKEN (k, t) => tcc_token(k, prop t) | TC_CONT _ => bug "unexpected TC_CONT in tc_lzrd" | TC_IND (tc, _) => h(tc, ol, nl, tenv) | TC_ENV(tc, ol', nl', tenv') => if ol = 0 then h(tc, ol', nl+nl', tenv') else h(g x, ol, nl, tenv)) end (* function h *) in if tcp_norm(t) then t else g t end (* function tc_lzrd *) (** utility function to read the top-level of an lty *) and lt_lzrd t = let fun g x = (case lt_outX x of LT_IND (lt, _) => g lt | LT_ENV(lt, i, j, te) => let val nlt = g(h(lt, i, j, te)) in lty_upd(x, nlt); nlt end | _ => x) and h (x, 0, 0, _) = g x | h (x, ol, nl, tenv) = let fun prop z = ltc_env(z, ol, nl, tenv) in (case lt_outX x of LT_TYC tc => ltc_tyc (tcc_env(tc, ol, nl, tenv)) | LT_STR ts => ltc_str (map prop ts) | LT_PST its => ltc_pst (map (fn (i, t) => (i, prop t)) its) | LT_FCT (ts1, ts2) => ltc_fct(map prop ts1, map prop ts2) | LT_POLY (ks, ts) => let val tenv' = tcInsert(tenv, (NONE, nl)) in ltc_poly(ks, map (fn t => ltc_env(t, ol+1, nl+1, tenv')) ts) end | LT_CONT _ => bug "unexpected LT_CONT in lt_lzrd" | LT_IND (t, _) => h(t, ol, nl, tenv) | LT_ENV (lt, ol', nl', tenv') => if ol = 0 then h(lt, ol', nl+nl', tenv') else h(g x, ol, nl, tenv)) end (* function h *) in if ltp_norm(t) then t else g t end (* function lt_lzrd *) (** taking out the TC_IND indirection *) and stripInd t = (case tc_outX t of TC_IND (x,_) => stripInd x | _ => t) (** normalizing an arbitrary tyc into a simple weak-head-normal-form *) and tc_whnm t = if tcp_norm(t) then t else let val nt = tc_lzrd t in case (tc_outX nt) of TC_APP(tc, tcs) => (let val tc' = tc_whnm tc in case (tc_outX tc') of TC_FN(ks, b) => let fun base () = (b, 1, 0, tcInsert(initTycEnv,(SOME tcs, 0))) val sp = (case tc_outX b of TC_ENV(b', ol', nl', te') => (case tcSplit te' of SOME((NONE, n), te) => if (n = nl'-1) andalso (ol' > 0) then (b', ol', n, tcInsert(te, (SOME tcs, n))) else base() | _ => base()) | _ => base()) val res = tc_whnm(tcc_env sp) in tyc_upd(nt, res); res end | ((TC_SEQ _) | (TC_TUPLE _) | (TC_ARROW _) | (TC_IND _)) => bug "unexpected tycs in tc_whnm-TC_APP" | _ => let val xx = tcc_app(tc', tcs) in stripInd xx end end) | TC_PROJ(tc, i) => (let val tc' = tc_whnm tc in (case (tc_outX tc') of (TC_SEQ tcs) => let val res = List.nth(tcs, i) handle _ => bug "TC_SEQ in tc_whnm" val nres = tc_whnm res in tyc_upd(nt, nres); nres end | ((TC_PRIM _) | (TC_NVAR _) | (TC_FIX _) | (TC_FN _) | (TC_SUM _) | (TC_ARROW _) | (TC_ABS _) | (TC_BOX _) | (TC_IND _) | (TC_TUPLE _)) => bug "unexpected tycs in tc_whnm-TC_PROJ" | _ => let val xx = tcc_proj(tc', i) in stripInd xx end) end) | TC_TOKEN(k, tc) => (let val tc' = tc_whnm tc in if token_whnm k tc' then let val xx = tcc_token(k, tc') in stripInd xx end else let val res = token_reduce(k, tc') val nres = tc_whnm res in tyc_upd(nt, nres); nres end end) | TC_IND (tc, _) => tc_whnm tc | TC_ENV _ => bug "unexpected TC_ENV in tc_whnm" | _ => nt end (* function tc_whnm *) (** normalizing an arbitrary lty into the simple weak-head-normal-form *) and lt_whnm t = if ltp_norm(t) then t else let val nt = lt_lzrd t in case (lt_outX nt) of LT_TYC tc => ltc_tyc(tc_whnm tc) | _ => nt end (* function lt_whnm *) (** normalizing an arbitrary tyc into the standard normal form *) fun tc_norm t = if (tcp_norm t) then t else let val nt = tc_whnm t in if (tcp_norm nt) then nt else (let val res = (case (tc_outX nt) of TC_FN (ks, tc) => tcc_fn(ks, tc_norm tc) | TC_APP (tc, tcs) => tcc_app(tc_norm tc, map tc_norm tcs) | TC_SEQ tcs => tcc_seq(map tc_norm tcs) | TC_PROJ (tc, i) => tcc_proj(tc_norm tc, i) | TC_SUM tcs => tcc_sum (map tc_norm tcs) | TC_FIX ((n,tc,ts), i) => tcc_fix((n, tc_norm tc, map tc_norm ts), i) | TC_ABS tc => tcc_abs(tc_norm tc) | TC_BOX tc => tcc_box(tc_norm tc) | TC_TUPLE (rk, tcs) => tcc_tup(rk, map tc_norm tcs) | TC_ARROW (r, ts1, ts2) => tcc_arw(r, map tc_norm ts1, map tc_norm ts2) | TC_PARROW (t1, t2) => tcc_parw(tc_norm t1, tc_norm t2) | TC_TOKEN (k, t) => tcc_token(k, tc_norm t) | TC_IND (tc, _) => tc_norm tc | TC_ENV _ => bug "unexpected tycs in tc_norm" | _ => nt) in tyc_upd(nt, res); res end) end (* function tc_norm *) (** normalizing an arbitrary lty into the standard normal form *) fun lt_norm t = if (ltp_norm t) then t else let val nt = lt_lzrd t in if (ltp_norm nt) then nt else (let val res = (case lt_outX nt of LT_TYC tc => ltc_tyc(tc_norm tc) | LT_STR ts => ltc_str(map lt_norm ts) | LT_PST its => ltc_pst(map (fn (i, t) => (i, lt_norm t)) its) | LT_FCT (ts1, ts2) => ltc_fct(map lt_norm ts1, map lt_norm ts2) | LT_POLY (ks, ts) => ltc_poly (ks, map lt_norm ts) | LT_IND (lt, _) => lt_norm lt | _ => bug "unexpected ltys in lt_norm") in lty_upd(nt, res); res end) end (* function lt_norm *) (*************************************************************************** * REGISTER A NEW TOKEN TYC --- TC_WRAP * ***************************************************************************) (** we add a new constructor named TC_RBOX through the token facility *) local val name = "TC_WRAP" val abbrev = "WR" val is_known = fn _ => true (* why is this ? *) fun tcc_tok k t = tcc_token(k, t) fun unknown tc = (case tc_outX tc of (TC_VAR _ | TC_NVAR _) => true | (TC_APP(tc, _)) => unknown tc | (TC_PROJ(tc, _)) => unknown tc | _ => false) fun flex_tuple ts = let fun hhh(x::r, ukn, wfree) = let fun iswp tc = (case tc_outX tc of TC_TOKEN(k', t) => (* WARNING: need check k' *) (case tc_outX t of TC_PRIM pt => false | _ => true) | _ => true) in hhh(r, (unknown x) orelse ukn, (iswp x) andalso wfree) end | hhh([], ukn, wfree) = ukn andalso wfree in hhh(ts, false, true) end fun is_whnm tc = (case tc_outX tc of (TC_ARROW(FF_FIXED, [t], _)) => (unknown t) | (TC_TUPLE(rf, ts)) => flex_tuple ts | (TC_PRIM pt) => PT.unboxed pt | _ => false) (* invariants: tc itself is in whnm but is_whnm tc = false *) fun reduce_one (k, tc) = (case tc_outX tc of TC_TUPLE (rk, ts) => let fun hhh (x::r, nts, ukn) = let val nx = tc_whnm x val b1 = unknown nx val nnx = (case tc_outX nx of TC_TOKEN(k', t) => if token_eq(k, k') then (case tc_outX t of TC_PRIM _ => t | _ => nx) else nx | _ => nx) in hhh(r, nnx::nts, b1 orelse ukn) end | hhh ([], nts, ukn) = let val nt = tcc_tup(rk, rev nts) in if ukn then tcc_token(k, nt) else nt end in hhh(ts, [], false) end | TC_ARROW (FF_FIXED, [_,_], [_]) => tc | TC_ARROW (FF_FIXED, [t1], ts2 as [_]) => let val nt1 = tc_whnm t1 fun ggg z = let val nz = tc_whnm z in (case tc_outX nz of TC_PRIM pt => if PT.unboxed pt then tcc_token(k, nz) else nz | _ => nz) end val (wp, nts1) = (case tc_outX nt1 of TC_TUPLE(_, [x,y]) => (false, [ggg x, ggg y]) | TC_TOKEN(k', x) => if token_eq(k, k') then (case (tc_outX x) of TC_TUPLE(_, [y, z]) => (false, [ggg y, ggg z]) | _ => (false, [nt1])) else (false, [nt1]) | _ => (unknown nt1, [nt1])) val nt = tcc_arw(FF_FIXED, nts1, ts2) in if wp then tcc_token(k, nt) else nt end | TC_ARROW (FF_FIXED, _, _) => bug "unexpected reduce_one on ill-formed FF_FIX arrow types" | TC_ARROW (FF_VAR(b1,b2), ts1, ts2) => bug "calling reduce_one on FF_VAR arrow types" | TC_PRIM pt => if PT.unboxed pt then bug "calling reduce_one on an already-reduced whnm" else tc | TC_TOKEN(k', t) => if token_eq(k, k') then tc else bug "unexpected token in reduce_one" | (TC_BOX _ | TC_ABS _ | TC_PARROW _) => bug "unexpected tc_box/abs/parrow in reduce_one" | TC_ENV _ => bug "unexpected TC_ENV in reduce_one" | TC_IND _ => bug "unexpected TC_IND in reduce_one" | _ => tc) in val wrap_token = register_token {name=name, abbrev=abbrev, reduce_one=reduce_one, is_whnm=is_whnm, is_known=is_known} end (* end of creating the box token for "tcc_rbox" *) (** testing if a tyc is a unknown constructor *) fun tc_unknown tc = not (isKnown tc) (*************************************************************************** * REBINDING THE INJECTION AND PROJECTION FUNCTIONS * ***************************************************************************) (** converting from the standard reps to the hash-consing reps *) val tk_inj = tk_injX val tc_inj = tc_injX val lt_inj = lt_injX (** converting from the hash-consing reps to the standard reps *) val tk_out = tk_outX val tc_out = tc_outX o tc_whnm val lt_out = lt_outX o lt_whnm (*************************************************************************** * UTILITY FUNCTIONS ON TESTING EQUIVALENCE * ***************************************************************************) (** testing the equality of values of tkind, tyc, lty *) fun eqlist p (x::xs, y::ys) = (p(x,y)) andalso (eqlist p (xs, ys)) | eqlist p ([], []) = true | eqlist _ _ = false (** testing the "pointer" equality on normalized tkind, tyc, and lty *) fun tk_eq (x: tkind, y) = (x = y) fun tc_eq (x: tyc, y) = (x = y) fun lt_eq (x: lty, y) = (x = y) (** testing the equivalence for arbitrary tkinds, tycs and ltys *) val tk_eqv = tk_eq (* all tkinds are normalized *) local (* tyc equivalence utilities *) (* The efficiency of checking FIX equivalence could probably be * improved somewhat, but it doesn't seem so bad for my purposes right * now. Anyway, somebody might eventually want to do some profiling * and improve this. --league, 24 March 1998 *) (* Profiling code, temporary?? *) structure Click = struct local val s_unroll = Stats.makeStat "FIX unrolls" in fun unroll() = Stats.addStat s_unroll 1 end end (* Click *) (** unrolling a fix, tyc -> tyc *) fun tc_unroll_fix tyc = case tc_outX tyc of (TC_FIX((n,tc,ts),i)) => let fun genfix i = tcc_fix ((n,tc,ts),i) val fixes = List.tabulate(n, genfix) val mu = tc val mu = if null ts then mu else tcc_app (mu,ts) val mu = tcc_app (mu, fixes) val mu = if n=1 then mu else tcc_proj (mu, i) in Click.unroll(); mu end | _ => bug "unexpected non-FIX in tc_unroll_fix" (* In order to check equality of two FIXes, we need to be able to * unroll them once, and check equality on the unrolled version, with * an inductive assumption that they ARE equal. The following code * supports making and checking these inductive assumptions. * Furthermore, we need to avoid unrolling any FIX more than once. *) structure TcDict = BinaryDict (struct type ord_key = tyc val cmpKey = tc_cmp end) (* for each tyc in this dictionary, we store a dictionary containing * tycs that are assumed equivalent to it. *) type eqclass = unit TcDict.dict type hyp = eqclass TcDict.dict (* the null hypothesis, no assumptions about equality *) val empty_eqclass : eqclass = TcDict.mkDict() val null_hyp : hyp = TcDict.mkDict() (* add assumption t1=t2 to current hypothesis. returns composite * hypothesis. *) fun assume_eq' (hyp, t1, t1eqOpt, t2) = let val t1eq = case t1eqOpt of SOME e => e | NONE => empty_eqclass val t1eq' = TcDict.insert (t1eq, t2, ()) val hyp' = TcDict.insert (hyp, t1, t1eq') in hyp' end fun assume_eq (hyp, t1, t1eqOpt, t2, t2eqOpt) = assume_eq' (assume_eq' (hyp, t1, t1eqOpt, t2), t2, t2eqOpt, t1) (* check whether t1=t2 according to the hypothesis *) val eq_by_hyp : eqclass option * tyc -> bool = fn (NONE, t2) => false | (SOME eqclass, t2) => isSome (TcDict.peek (eqclass, t2)) (* have we made any assumptions about `t' already? *) val visited : eqclass option -> bool = isSome (* testing if two recursive datatypes are equivalent *) fun eq_fix (eqop1, hyp) (t1, t2) = (case (tc_outX t1, tc_outX t2) of (TC_FIX((n1,tc1,ts1),i1), TC_FIX((n2,tc2,ts2),i2)) => if not (!Control.CG.checkDatatypes) then true else let val t1eqOpt = TcDict.peek (hyp, t1) in (* first check the induction hypothesis. we only ever * make hypotheses about FIX nodes, so this test is okay * here. if assume_eq appears in other cases, this * test should be lifted outside the switch. *) if eq_by_hyp (t1eqOpt, t2) then true (* next try structural eq on the components. i'm not sure why * this part is necessary, but it does seem to be... --league, * 23 March 1998 *) else (n1 = n2 andalso i1 = i2 andalso eqop1 hyp (tc1, tc2) andalso eqlist (eqop1 hyp) (ts1, ts2)) orelse (* not equal by inspection; we have to unroll it. * we prevent unrolling the same FIX twice by asking * the `visited' function. *) if visited t1eqOpt then false else let val t2eqOpt = TcDict.peek (hyp, t2) in if visited t2eqOpt then false else eqop1 (assume_eq (hyp, t1, t1eqOpt, t2, t2eqOpt)) (tc_unroll_fix t1, tc_unroll_fix t2) end end | _ => bug "unexpected types in eq_fix") (* tc_eqv_generator, invariant: t1 and t2 are in the wh-normal form * eqop1 is the default equality to be used for tycs * eqop2 is used for body of FN, arguments in APP, * eqop3 is used for ABS and BOX. * eqop4 is used for arrow arguments and results * Each of these first takes the set of hypotheses. *) fun tc_eqv_gen (eqop1, eqop2, hyp) (t1, t2) = case (tc_outX t1, tc_outX t2) of (TC_FIX _, TC_FIX _) => eqop2 (eqop1, hyp) (t1, t2) | (TC_FN(ks1, b1), TC_FN(ks2, b2)) => eqlist tk_eqv (ks1, ks2) andalso eqop1 hyp (b1, b2) | (TC_APP(a1, b1), TC_APP(a2, b2)) => eqop1 hyp (a1, a2) andalso eqlist (eqop1 hyp) (b1, b2) | (TC_SEQ ts1, TC_SEQ ts2) => eqlist (eqop1 hyp) (ts1, ts2) | (TC_SUM ts1, TC_SUM ts2) => eqlist (eqop1 hyp) (ts1, ts2) | (TC_TUPLE (_, ts1), TC_TUPLE (_, ts2)) => eqlist (eqop1 hyp) (ts1, ts2) | (TC_ABS a, TC_ABS b) => eqop1 hyp (a, b) | (TC_BOX a, TC_BOX b) => eqop1 hyp (a, b) | (TC_TOKEN(k1,t1), TC_TOKEN(k2,t2)) => token_eq(k1,k2) andalso eqop1 hyp (t1,t2) | (TC_PROJ(a1, i1), TC_PROJ(a2, i2)) => i1 = i2 andalso eqop1 hyp (a1, a2) | (TC_ARROW(r1, a1, b1), TC_ARROW(r2, a2, b2)) => r1 = r2 andalso eqlist (eqop1 hyp) (a1, a2) andalso eqlist (eqop1 hyp) (b1, b2) | (TC_PARROW(a1, b1), TC_PARROW(a2, b2)) => eqop1 hyp (a1, a2) andalso eqop1 hyp (b1, b2) | (TC_CONT ts1, TC_CONT ts2) => eqlist (eqop1 hyp) (ts1, ts2) | _ => false (** general equality for tycs *) fun tc_eqv' hyp (x as ref (_, _, AX_REG(true, _)), y as ref (_, _, AX_REG(true, _))) = tc_eq(x,y) | tc_eqv' hyp (x, y) = let val t1 = tc_whnm x val t2 = tc_whnm y in if tcp_norm t1 andalso tcp_norm t2 then tc_eq (t1, t2) else tc_eqv_gen (tc_eqv', fn _ => tc_eq, hyp) (t1, t2) end (* tc_eqv' *) (* slightly relaxed constraints (???) *) fun tc_eqv_x' hyp (x, y) = let val t1 = tc_whnm x val t2 = tc_whnm y in (if (tcp_norm t1) andalso (tcp_norm t2) then tc_eq(t1, t2) else false) orelse (tc_eqv_gen (tc_eqv_x', eq_fix, hyp) (t1, t2)) end (* function tc_eqv_x *) in (* tyc equivalence utilities *) val tc_eqv = tc_eqv' null_hyp val tc_eqv_x = tc_eqv_x' null_hyp end (* tyc equivalence utilities *) (* * all the complexity of lt_eqv comes from the partial-structure (or * partial record) type (the LT_PST type). If we can remove LT_PST * type, then the following can be considerabily simplified. (ZHONG) *) (** lt_eqv_generator, invariant: x and y are in the wh-normal form *) fun lt_eqv_gen (eqop1, eqop2) (x : lty, y) = let fun sp (r, []) = true | sp (r, (i,t)::s) = (if (eqop1(List.nth(r,i),t)) then sp(r,s) else false) handle _ => false fun pp ([], _) = true | pp (_, []) = true | pp (a as ((i,t)::l), b as ((j,s)::r)) = if i > j then pp(a,r) else if i < j then pp(l,b) else if (eqop1(t,s)) then pp(l,r) else false (* seq should be called if t1 and t2 are weak-head normal form *) fun seq (t1, t2) = (case (lt_outX t1, lt_outX t2) of (LT_POLY(ks1, b1), LT_POLY(ks2, b2)) => (eqlist tk_eqv (ks1, ks2)) andalso (eqlist eqop1 (b1, b2)) | (LT_FCT(as1, bs1), LT_FCT(as2, bs2)) => (eqlist eqop1 (as1, as2)) andalso (eqlist eqop1 (bs1, bs2)) | (LT_TYC a, LT_TYC b) => eqop2(a, b) | (LT_STR s1, LT_STR s2) => eqlist eqop1 (s1, s2) | (LT_PST s1, LT_PST s2) => pp(s1, s2) | (LT_PST s1, LT_STR s2) => sp(s2, s1) | (LT_STR s1, LT_PST s2) => sp(s1, s2) | (LT_CONT s1, LT_CONT s2) => eqlist eqop1 (s1, s2) | _ => false) in seq(x, y) end (* function lt_eqv_gen *) fun lt_eqv(x : lty, y) = let val seq = lt_eqv_gen (lt_eqv, tc_eqv) in if ((ltp_norm x) andalso (ltp_norm y)) then (lt_eq(x, y)) orelse (seq(x, y)) else (let val t1 = lt_whnm x val t2 = lt_whnm y in if (ltp_norm t1) andalso (ltp_norm t2) then (lt_eq(t1, t2)) orelse (seq(t1, t2)) else seq(t1, t2) end) end (* function lt_eqv *) fun lt_eqv_x(x : lty, y) = let val seq = lt_eqv_gen (lt_eqv_x, tc_eqv_x) in if ((ltp_norm x) andalso (ltp_norm y)) then (lt_eq(x, y)) orelse (seq(x, y)) else (let val t1 = lt_whnm x val t2 = lt_whnm y in if (ltp_norm t1) andalso (ltp_norm t2) then (lt_eq(t1, t2)) orelse (seq(t1, t2)) else seq(t1, t2) end) end (* function lt_eqv *) (** testing equivalence of fflags and rflags *) val ff_eqv : fflag * fflag -> bool = (op =) val rf_eqv : rflag * rflag -> bool = (op =) (*************************************************************************** * UTILITY FUNCTIONS ON FINDING OUT THE DEPTH OF THE FREE TYC VARIABLES * ***************************************************************************) (** finding out the innermost binding depth for a tyc's free variables *) fun tc_depth (x, d) = let val tvs = tc_vs (tc_norm x) (* unfortunately we have to reduce everything to the normal form before we can talk about its list of free type variables. *) in case tvs of NONE => bug "unexpected case in tc_depth" | SOME [] => DI.top | SOME (a::_) => d + 1 - (#1(tvDecode a)) end fun tcs_depth ([], d) = DI.top | tcs_depth (x::r, d) = Int.max(tc_depth(x, d), tcs_depth(r, d)) end (* toplevel local *) end (* abstraction LtyKernel *)
root@smlnj-gforge.cs.uchicago.edu | ViewVC Help |
Powered by ViewVC 1.0.0 |