Mercurial > urweb
changeset 39:02f42e9a1825
Corify removes modules
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 19 Jun 2008 12:39:22 -0400 |
| parents | d16ef24de78b |
| children | e3d3c2791105 |
| files | src/compiler.sig src/compiler.sml src/core_print.sml src/corify.sig src/corify.sml src/elab_env.sig src/list_util.sig src/list_util.sml src/shake.sml tests/modnested.lac tests/modproj.lac |
| diffstat | 11 files changed, 312 insertions(+), 59 deletions(-) [+] |
line wrap: on
line diff
--- a/src/compiler.sig Thu Jun 19 10:06:59 2008 -0400 +++ b/src/compiler.sig Thu Jun 19 12:39:22 2008 -0400 @@ -35,6 +35,7 @@ val elaborate : ElabEnv.env -> string -> (Elab.file * ElabEnv.env) option val explify : ElabEnv.env -> string -> Expl.file option val corify : ElabEnv.env -> string -> Core.file option + val shake' : ElabEnv.env -> string -> Core.file option val reduce : ElabEnv.env -> string -> Core.file option val shake : ElabEnv.env -> string -> Core.file option val monoize : ElabEnv.env -> CoreEnv.env -> string -> Mono.file option @@ -45,6 +46,7 @@ val testElaborate : string -> unit val testExplify : string -> unit val testCorify : string -> unit + val testShake' : string -> unit val testReduce : string -> unit val testShake : string -> unit val testMonoize : string -> unit
--- a/src/compiler.sml Thu Jun 19 10:06:59 2008 -0400 +++ b/src/compiler.sml Thu Jun 19 12:39:22 2008 -0400 @@ -77,14 +77,23 @@ SOME (Explify.explify file) fun corify eenv filename = - case elaborate eenv filename of + case explify eenv filename of NONE => NONE - | SOME (file, _) => + | SOME file => if ErrorMsg.anyErrors () then NONE else SOME (Corify.corify file) +fun shake' eenv filename = + case corify eenv filename of + NONE => NONE + | SOME file => + if ErrorMsg.anyErrors () then + NONE + else + SOME (Shake.shake file) + fun reduce eenv filename = case corify eenv filename of NONE => NONE @@ -165,6 +174,15 @@ handle CoreEnv.UnboundNamed n => print ("Unbound named " ^ Int.toString n ^ "\n") +fun testShake' filename = + (case shake' ElabEnv.basis filename of + NONE => print "Failed\n" + | SOME file => + (Print.print (CorePrint.p_file CoreEnv.basis file); + print "\n")) + handle CoreEnv.UnboundNamed n => + print ("Unbound named " ^ Int.toString n ^ "\n") + fun testReduce filename = (case reduce ElabEnv.basis filename of NONE => print "Failed\n"
--- a/src/core_print.sml Thu Jun 19 10:06:59 2008 -0400 +++ b/src/core_print.sml Thu Jun 19 12:39:22 2008 -0400 @@ -79,15 +79,17 @@ p_con' true env c] | CRel n => - if !debug then - string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n) - else - string (#1 (E.lookupCRel env n)) + ((if !debug then + string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n) + else + string (#1 (E.lookupCRel env n))) + handle E.UnboundRel _ => string ("UNBOUND_" ^ Int.toString n)) | CNamed n => - if !debug then - string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n) - else - string (#1 (E.lookupCNamed env n)) + ((if !debug then + string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n) + else + string (#1 (E.lookupCNamed env n))) + handle E.UnboundNamed _ => string ("UNBOUNDN_" ^ Int.toString n)) | CApp (c1, c2) => parenIf par (box [p_con env c1, space, @@ -143,15 +145,17 @@ case e of EPrim p => Prim.p_t p | ERel n => - if !debug then - string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n) - else - string (#1 (E.lookupERel env n)) + ((if !debug then + string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n) + else + string (#1 (E.lookupERel env n))) + handle E.UnboundRel _ => string ("UNBOUND_" ^ Int.toString n)) | ENamed n => - if !debug then - string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n) - else - string (#1 (E.lookupENamed env n)) + ((if !debug then + string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n) + else + string (#1 (E.lookupENamed env n))) + handle E.UnboundNamed _ => string ("UNBOUNDN_" ^ Int.toString n)) | EApp (e1, e2) => parenIf par (box [p_exp env e1, space, p_exp' true env e2])
--- a/src/corify.sig Thu Jun 19 10:06:59 2008 -0400 +++ b/src/corify.sig Thu Jun 19 12:39:22 2008 -0400 @@ -27,6 +27,6 @@ signature CORIFY = sig - val corify : Elab.file -> Core.file + val corify : Expl.file -> Core.file end
--- a/src/corify.sml Thu Jun 19 10:06:59 2008 -0400 +++ b/src/corify.sml Thu Jun 19 12:39:22 2008 -0400 @@ -28,9 +28,133 @@ structure Corify :> CORIFY = struct structure EM = ErrorMsg -structure L = Elab +structure L = Expl structure L' = Core +structure IM = IntBinaryMap +structure SM = BinaryMapFn(struct + type ord_key = string + val compare = String.compare + end) + +local + val count = ref 0 +in + +fun reset v = count := v + +fun alloc () = + let + val r = !count + in + count := r + 1; + r +end + +end + +structure St : sig + type t + + val empty : t + + val enter : t -> t + val leave : t -> {outer : t, inner : t} + + val bindCore : t -> string -> int -> t * int + val lookupCoreById : t -> int -> int option + val lookupCoreByName : t -> string -> int + + val bindStr : t -> string -> int -> t -> t + val lookupStrById : t -> int -> t + val lookupStrByName : string * t -> t +end = struct + +datatype flattening = F of { + core : int SM.map, + strs : flattening SM.map +} + +type t = { + core : int IM.map, + strs : flattening IM.map, + current : flattening, + nested : flattening list +} + +val empty = { + core = IM.empty, + strs = IM.empty, + current = F { core = SM.empty, strs = SM.empty }, + nested = [] +} + +fun bindCore {core, strs, current, nested} s n = + let + val n' = alloc () + + val current = + let + val F {core, strs} = current + in + F {core = SM.insert (core, s, n'), + strs = strs} + end + in + ({core = IM.insert (core, n, n'), + strs = strs, + current = current, + nested = nested}, + n') + end + +fun lookupCoreById ({core, ...} : t) n = IM.find (core, n) + +fun lookupCoreByName ({current = F {core, ...}, ...} : t) x = + case SM.find (core, x) of + NONE => raise Fail "Corify.St.lookupCoreByName" + | SOME n => n + +fun enter {core, strs, current, nested} = + {core = core, + strs = strs, + current = F {core = SM.empty, + strs = SM.empty}, + nested = current :: nested} + +fun dummy f = {core = IM.empty, + strs = IM.empty, + current = f, + nested = []} + +fun leave {core, strs, current, nested = m1 :: rest} = + {outer = {core = core, + strs = strs, + current = m1, + nested = rest}, + inner = dummy current} + | leave _ = raise Fail "Corify.St.leave" + +fun bindStr ({core, strs, current = F {core = mcore, strs = mstrs}, nested} : t) x n ({current = f, ...} : t) = + {core = core, + strs = IM.insert (strs, n, f), + current = F {core = mcore, + strs = SM.insert (mstrs, x, f)}, + nested = nested} + +fun lookupStrById ({strs, ...} : t) n = + case IM.find (strs, n) of + NONE => raise Fail "Corify.St.lookupStr" + | SOME f => dummy f + +fun lookupStrByName (m, {current = F {strs, ...}, ...} : t) = + case SM.find (strs, m) of + NONE => raise Fail "Corify.St.lookupStrByName" + | SOME f => dummy f + +end + + fun corifyKind (k, loc) = case k of L.KType => (L'.KType, loc) @@ -38,57 +162,122 @@ | L.KName => (L'.KName, loc) | L.KRecord k => (L'.KRecord (corifyKind k), loc) - | L.KError => raise Fail ("corifyKind: KError at " ^ EM.spanToString loc) - | L.KUnif (_, ref (SOME k)) => corifyKind k - | L.KUnif _ => raise Fail ("corifyKind: KUnif at " ^ EM.spanToString loc) - -fun corifyCon (c, loc) = +fun corifyCon st (c, loc) = case c of - L.TFun (t1, t2) => (L'.TFun (corifyCon t1, corifyCon t2), loc) - | L.TCFun (_, x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon t), loc) - | L.TRecord c => (L'.TRecord (corifyCon c), loc) + L.TFun (t1, t2) => (L'.TFun (corifyCon st t1, corifyCon st t2), loc) + | L.TCFun (x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon st t), loc) + | L.TRecord c => (L'.TRecord (corifyCon st c), loc) | L.CRel n => (L'.CRel n, loc) - | L.CNamed n => (L'.CNamed n, loc) - | L.CModProj _ => raise Fail "Corify CModProj" + | L.CNamed n => + (case St.lookupCoreById st n of + NONE => (L'.CNamed n, loc) + | SOME n => (L'.CNamed n, loc)) + | L.CModProj (m, ms, x) => + let + val st = St.lookupStrById st m + val st = foldl St.lookupStrByName st ms + val n = St.lookupCoreByName st x + in + (L'.CNamed n, loc) + end - | L.CApp (c1, c2) => (L'.CApp (corifyCon c1, corifyCon c2), loc) - | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon c), loc) + | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc) + | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc) | L.CName s => (L'.CName s, loc) - | L.CRecord (k, xcs) => (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon c1, corifyCon c2)) xcs), loc) - | L.CConcat (c1, c2) => (L'.CConcat (corifyCon c1, corifyCon c2), loc) + | L.CRecord (k, xcs) => + (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc) + | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc) - | L.CError => raise Fail ("corifyCon: CError at " ^ EM.spanToString loc) - | L.CUnif (_, _, ref (SOME c)) => corifyCon c - | L.CUnif _ => raise Fail ("corifyCon: CUnif at " ^ EM.spanToString loc) - -fun corifyExp (e, loc) = +fun corifyExp st (e, loc) = case e of L.EPrim p => (L'.EPrim p, loc) | L.ERel n => (L'.ERel n, loc) - | L.ENamed n => (L'.ENamed n, loc) - | L.EModProj _ => raise Fail "Corify EModProj" - | L.EApp (e1, e2) => (L'.EApp (corifyExp e1, corifyExp e2), loc) - | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon dom, corifyCon ran, corifyExp e1), loc) - | L.ECApp (e1, c) => (L'.ECApp (corifyExp e1, corifyCon c), loc) - | L.ECAbs (_, x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp e1), loc) + | L.ENamed n => + (case St.lookupCoreById st n of + NONE => (L'.ENamed n, loc) + | SOME n => (L'.ENamed n, loc)) + | L.EModProj (m, ms, x) => + let + val st = St.lookupStrById st m + val st = foldl St.lookupStrByName st ms + val n = St.lookupCoreByName st x + in + (L'.ENamed n, loc) + end + | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), loc) + | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc) + | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc) + | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc) - | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) => (corifyCon c, corifyExp e, corifyCon t)) xes), loc) - | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp e1, corifyCon c, - {field = corifyCon field, rest = corifyCon rest}), loc) + | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) => (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc) + | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c, + {field = corifyCon st field, rest = corifyCon st rest}), loc) - | L.EError => raise Fail ("corifyExp: EError at " ^ EM.spanToString loc) +fun corifyDecl ((d, loc : EM.span), st) = + case d of + L.DCon (x, n, k, c) => + let + val (st, n) = St.bindCore st x n + in + ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st) + end + | L.DVal (x, n, t, e) => + let + val (st, n) = St.bindCore st x n + in + ([(L'.DVal (x, n, corifyCon st t, corifyExp st e), loc)], st) + end + + | L.DSgn _ => ([], st) -fun corifyDecl (d, loc : EM.span) = - case d of - L.DCon (x, n, k, c) => (L'.DCon (x, n, corifyKind k, corifyCon c), loc) - | L.DVal (x, n, t, e) => (L'.DVal (x, n, corifyCon t, corifyExp e), loc) + | L.DStr (x, n, _, str) => + let + val (ds, {inner, outer}) = corifyStr (str, st) + val st = St.bindStr outer x n inner + in + (ds, st) + end - | L.DSgn _ => raise Fail "Not ready to corify signature" - | L.DStr _ => raise Fail "Not ready to corify structure" +and corifyStr ((str, _), st) = + case str of + L.StrConst ds => + let + val st = St.enter st + val (ds, st) = ListUtil.foldlMapConcat corifyDecl st ds + in + (ds, St.leave st) + end + | L.StrVar n => ([], {inner = St.lookupStrById st n, outer = st}) + | L.StrProj (str, x) => + let + val (ds, {inner, outer}) = corifyStr (str, st) + in + (ds, {inner = St.lookupStrByName (x, inner), outer = outer}) + end -val corify = map corifyDecl +fun maxName ds = foldl (fn ((d, _), n) => + case d of + L.DCon (_, n', _, _) => Int.max (n, n') + | L.DVal (_, n', _ , _) => Int.max (n, n') + | L.DSgn (_, n', _) => Int.max (n, n') + | L.DStr (_, n', _, str) => Int.max (n, Int.max (n', maxNameStr str))) + 0 ds + +and maxNameStr (str, _) = + case str of + L.StrConst ds => maxName ds + | L.StrVar n => n + | L.StrProj (str, _) => maxNameStr str + +fun corify ds = + let + val () = reset (maxName ds + 1) + val (ds, _) = ListUtil.foldlMapConcat corifyDecl St.empty ds + in + ds + end end
--- a/src/elab_env.sig Thu Jun 19 10:06:59 2008 -0400 +++ b/src/elab_env.sig Thu Jun 19 12:39:22 2008 -0400 @@ -80,4 +80,6 @@ val projectVal : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.con option val projectStr : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option + + end
--- a/src/list_util.sig Thu Jun 19 10:06:59 2008 -0400 +++ b/src/list_util.sig Thu Jun 19 12:39:22 2008 -0400 @@ -33,6 +33,8 @@ -> ('context, 'data list, 'state, 'abort) Search.mapfolderB val foldlMap : ('data1 * 'state -> 'data2 * 'state) -> 'state -> 'data1 list -> 'data2 list * 'state + val foldlMapPartial : ('data1 * 'state -> 'data2 option * 'state) -> 'state -> 'data1 list -> 'data2 list * 'state + val foldlMapConcat : ('data1 * 'state -> 'data2 list * 'state) -> 'state -> 'data1 list -> 'data2 list * 'state val search : ('a -> 'b option) -> 'a list -> 'b option
--- a/src/list_util.sml Thu Jun 19 10:06:59 2008 -0400 +++ b/src/list_util.sml Thu Jun 19 12:39:22 2008 -0400 @@ -80,6 +80,39 @@ fm ([], s) end +fun foldlMapConcat f s = + let + fun fm (ls', s) ls = + case ls of + nil => (rev ls', s) + | h :: t => + let + val (h', s') = f (h, s) + in + fm (List.revAppend (h', ls'), s') t + end + in + fm ([], s) + end + +fun foldlMapPartial f s = + let + fun fm (ls', s) ls = + case ls of + nil => (rev ls', s) + | h :: t => + let + val (h', s') = f (h, s) + val ls' = case h' of + NONE => ls' + | SOME h' => h' :: ls' + in + fm (ls', s') t + end + in + fm ([], s) + end + fun search f = let fun s ls =
--- a/src/shake.sml Thu Jun 19 10:06:59 2008 -0400 +++ b/src/shake.sml Thu Jun 19 12:39:22 2008 -0400 @@ -42,10 +42,10 @@ } fun shake file = - case List.foldl (fn ((DVal ("main", n, _, e), _), _) => SOME (n, e) + case List.foldl (fn ((DVal ("main", n, t, e), _), _) => SOME (n, t, e) | (_, s) => s) NONE file of NONE => [] - | SOME (main, body) => + | SOME (main, mainT, body) => let val (cdef, edef) = foldl (fn ((DCon (_, n, _, c), _), (cdef, edef)) => (IM.insert (cdef, n, c), edef) | ((DVal (_, n, t, e), _), (cdef, edef)) => (cdef, IM.insert (edef, n, (t, e)))) @@ -92,6 +92,7 @@ val s = {con = IS.empty, exp = IS.singleton main} + val s = U.Con.fold {kind = kind, con = con} s mainT val s = U.Exp.fold {kind = kind, con = con, exp = exp} s body in List.filter (fn (DCon (_, n, _, _), _) => IS.member (#con s, n)