Corify removes modules

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)