summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-06-19 12:39:22 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-06-19 12:39:22 -0400
commit8e98be7de2dd3db541994aae47aeb45756f60098 (patch)
treebbc63e96871ef6513d974d96311deab9afd4e7a3 /src
parent371b414262cfb5888759c786e21c66f883ad13c0 (diff)
Corify removes modules
Diffstat (limited to 'src')
-rw-r--r--src/compiler.sig2
-rw-r--r--src/compiler.sml22
-rw-r--r--src/core_print.sml36
-rw-r--r--src/corify.sig2
-rw-r--r--src/corify.sml263
-rw-r--r--src/elab_env.sig2
-rw-r--r--src/list_util.sig2
-rw-r--r--src/list_util.sml33
-rw-r--r--src/shake.sml5
9 files changed, 309 insertions, 58 deletions
diff --git a/src/compiler.sig b/src/compiler.sig
index 9b5f36cd..eac2c538 100644
--- a/src/compiler.sig
+++ b/src/compiler.sig
@@ -35,6 +35,7 @@ signature COMPILER = sig
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 @@ signature COMPILER = sig
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
diff --git a/src/compiler.sml b/src/compiler.sml
index 332e2298..8e011d8e 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -77,14 +77,23 @@ fun explify eenv filename =
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 @@ fun testCorify filename =
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"
diff --git a/src/core_print.sml b/src/core_print.sml
index 42cbbc7a..3bcb982e 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -79,15 +79,17 @@ fun p_con' par env (c, _) =
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 @@ fun p_exp' par env (e, _) =
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])
diff --git a/src/corify.sig b/src/corify.sig
index 8cd197ce..0e1bb80d 100644
--- a/src/corify.sig
+++ b/src/corify.sig
@@ -27,6 +27,6 @@
signature CORIFY = sig
- val corify : Elab.file -> Core.file
+ val corify : Expl.file -> Core.file
end
diff --git a/src/corify.sml b/src/corify.sml
index 61634a5d..607d173a 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -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 @@ fun corifyKind (k, loc) =
| 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.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)
+ | 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)
-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) =
+fun corifyDecl ((d, loc : EM.span), st) =
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.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)
+
+ | 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
+
+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
+
+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
- | L.DSgn _ => raise Fail "Not ready to corify signature"
- | L.DStr _ => raise Fail "Not ready to corify structure"
+and maxNameStr (str, _) =
+ case str of
+ L.StrConst ds => maxName ds
+ | L.StrVar n => n
+ | L.StrProj (str, _) => maxNameStr str
-val corify = map corifyDecl
+fun corify ds =
+ let
+ val () = reset (maxName ds + 1)
+ val (ds, _) = ListUtil.foldlMapConcat corifyDecl St.empty ds
+ in
+ ds
+ end
end
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 89d5fb60..98f59c38 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -80,4 +80,6 @@ signature ELAB_ENV = sig
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
diff --git a/src/list_util.sig b/src/list_util.sig
index 76d08d23..b4ea338c 100644
--- a/src/list_util.sig
+++ b/src/list_util.sig
@@ -33,6 +33,8 @@ signature LIST_UTIL = sig
-> ('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
diff --git a/src/list_util.sml b/src/list_util.sml
index e3d8515e..7f87b87e 100644
--- a/src/list_util.sml
+++ b/src/list_util.sml
@@ -80,6 +80,39 @@ fun foldlMap f s =
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 =
diff --git a/src/shake.sml b/src/shake.sml
index ec2e43e5..e51d7013 100644
--- a/src/shake.sml
+++ b/src/shake.sml
@@ -42,10 +42,10 @@ type free = {
}
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 @@ fun shake file =
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)