Some more nested functor bug-fixing, including generating fresh internal names at applications; still need to debug issues with datatype constructors

9 files changed, 595 insertions, 6 deletions

diff --git a/src/corify.sml b/src/corify.sml
index c1c60045..7fda1034 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -64,7 +64,10 @@ fun alloc () =
     in
         count := r + 1;
         r
-end
+    end
+
+fun getCounter () = !count
+fun setCounter n = count := n
 
 end
 
@@ -107,11 +110,13 @@ structure St : sig
 
     val bindStr : t -> string -> int -> t -> t
     val lookupStrById : t -> int -> t
+    val lookupStrByIdOpt : t -> int -> t option
     val lookupStrByName : string * t -> t
     val lookupStrByNameOpt : string * t -> t option
 
     val bindFunctor : t -> string -> int -> string -> int -> L.str -> t
     val lookupFunctorById : t -> int -> string * int * L.str
+    val lookupFunctorByIdOpt : t -> int -> (string * int * L.str) option
     val lookupFunctorByName : string * t -> string * int * L.str
 end = struct
 
@@ -399,6 +404,11 @@ fun lookupStrById ({basis, strs, ...} : t) n =
         NONE => raise Fail ("Corify.St.lookupStrById(" ^ Int.toString n ^ ")")
       | SOME f => dummy (basis, f)
 
+fun lookupStrByIdOpt ({basis, strs, ...} : t) n =
+    case IM.find (strs, n) of
+        NONE => NONE
+      | SOME f => SOME (dummy (basis, f))
+
 fun lookupStrByName (m, {basis, current = FNormal {strs, ...}, ...} : t) =
     (case SM.find (strs, m) of
          NONE => raise Fail "Corify.St.lookupStrByName [1]"
@@ -435,6 +445,9 @@ fun lookupFunctorById ({funs, ...} : t) n =
         NONE => raise Fail "Corify.St.lookupFunctorById"
       | SOME v => v
 
+fun lookupFunctorByIdOpt ({funs, ...} : t) n =
+    IM.find (funs, n)
+
 fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) =
     (case SM.find (funs, m) of
          NONE => raise Fail ("Corify.St.lookupFunctorByName " ^ m ^ "[1]")
@@ -781,6 +794,11 @@ fun corifyDecl mods (all as (d, loc : EM.span), st) =
             ([], st)
         end
 
+      | L.DStr (x, n, _, (L.StrVar n', _)) =>
+        (case St.lookupFunctorByIdOpt st n' of
+             SOME (arg, dom, body) => ([], St.bindFunctor st x n arg dom body)
+           | NONE => ([], St.bindStr st x n (St.lookupStrById st n')))
+
       | L.DStr (x, n, _, str) =>
         let
             val mods' =
@@ -1130,7 +1148,7 @@ fun corifyDecl mods (all as (d, loc : EM.span), st) =
                       ([], st))
         end
 
-and corifyStr mods ((str, _), st) =
+and corifyStr mods ((str, loc), st) =
     case str of
         L.StrConst ds =>
         let
@@ -1163,6 +1181,20 @@ and corifyStr mods ((str, _), st) =
 
             val (xa, na, body) = unwind str1
 
+            (* An important step to make sure that nested functors
+             * "close under their environments": *)
+            val (next, body') = ExplRename.rename {NextId = getCounter (),
+                                                   FormalName = xa,
+                                                   FormalId = na,
+                                                   Body = body}
+
+            (*val () = Print.prefaces ("RENAME " ^ ErrorMsg.spanToString loc)
+                     [("FROM", ExplPrint.p_str ExplEnv.empty body),
+                      ("TO", ExplPrint.p_str ExplEnv.empty body')]*)
+            val body = body'
+
+            val () = setCounter next
+
             val (ds1, {inner = inner', outer}) = corifyStr mods (str2, st)
 
             val (ds2, {inner, outer}) = corifyStr mods (body, St.bindStr outer xa na inner')
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 959a6cd1..6d223585 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -4295,7 +4295,8 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
 
         (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*)
     in
-        (*prefaces "/elabDecl" [("d", SourcePrint.p_decl dAll)];*)
+        (*prefaces "/elabDecl" [("d", SourcePrint.p_decl dAll),
+                              ("d'", p_list_sep PD.newline (ElabPrint.p_decl env) (#1 r))];*)
         r
     end
 
@@ -4454,6 +4455,16 @@ and elabStr (env, denv) (str, loc) =
                         subSgn env' loc actual ran';
                         (ran', gs)
                     end
+
+            (* Later compiler phases are simplified by alpha-varying
+             * the functor formal argument here, if the same name
+             * will be defined independently in the functor body. *)
+            fun ensureUnused m =
+                case E.projectStr env' {sgn = actual, str = (L'.StrVar 0, loc), field = m} of
+                    NONE => m
+                  | SOME _ => ensureUnused ("?" ^ m)
+
+            val m = ensureUnused m
         in
             ((L'.StrFun (m, n, dom', formal, str'), loc),
              (L'.SgnFun (m, n, dom', formal), loc),
@@ -4491,13 +4502,22 @@ and elabStr (env, denv) (str, loc) =
                           * with the invariant in mind.  Luckily for us, references to
                           * an identifier later within a signature work by globally
                           * unique index, so we just need to change the string name in the
-                          * new declaration. *)
-                         val m =
+                          * new declaration.
+                          *
+                          * ~~~ A few days later.... ~~~
+                          * This is trickier than I thought!  We might need to add
+                          * arbitarily many question marks before the module name to
+                          * avoid a clash, since some other code might depend on
+                          * question-mark identifiers generated previously by this
+                          * very code fragment. *)
+                         fun mungeName m =
                              if List.exists (fn (L'.SgiStr (x, _, _), _) => x = m
                                               | _ => false) sgis then
-                                 "?" ^ m
+                                 mungeName ("?" ^ m)
                              else
                                  m
+
+                         val m = mungeName m
                      in
                          ((L'.StrApp (str1', str2'), loc),
                           (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc),
diff --git a/src/expl_print.sig b/src/expl_print.sig
index 8f1cee97..3b074014 100644
--- a/src/expl_print.sig
+++ b/src/expl_print.sig
@@ -31,6 +31,7 @@ signature EXPL_PRINT = sig
     val p_exp : ExplEnv.env -> Expl.exp Print.printer
     val p_decl : ExplEnv.env -> Expl.decl Print.printer
     val p_sgn_item : ExplEnv.env -> Expl.sgn_item Print.printer
+    val p_str : ExplEnv.env -> Expl.str Print.printer
     val p_file : ExplEnv.env -> Expl.file Print.printer
 
     val debug : bool ref
diff --git a/src/expl_rename.sig b/src/expl_rename.sig
new file mode 100644
index 00000000..1aff3151
--- /dev/null
+++ b/src/expl_rename.sig
@@ -0,0 +1,41 @@
+(* Copyright (c) 2014, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+(* To simplify Corify, it helps to apply a particular kind of renaming to functor
+ * bodies, so that nested functors refer only to fresh names.  The payoff is that
+ * we can then implement applications of those nested functors by evaluating their
+ * bodies in arbitrary later contexts, even where identifiers defined in the
+ * outer functor body may have been shadowed. *)
+
+signature EXPL_RENAME = sig
+
+    val rename : {NextId : int,
+                  FormalName : string,
+                  FormalId : int,
+                  Body : Expl.str} -> int * Expl.str
+
+end
diff --git a/src/expl_rename.sml b/src/expl_rename.sml
new file mode 100644
index 00000000..751c22e8
--- /dev/null
+++ b/src/expl_rename.sml
@@ -0,0 +1,431 @@
+(* Copyright (c) 2014, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+structure ExplRename :> EXPL_RENAME = struct
+
+open Expl
+structure E = ExplEnv
+
+structure IM = IntBinaryMap
+
+structure St :> sig
+    type t
+
+    val create : int -> t
+    val next : t -> int
+
+    val bind : t * int -> t * int
+    val lookup: t * int -> int option
+end = struct
+
+type t = {next : int,
+          renaming : int IM.map}
+
+fun create next = {next = next,
+                   renaming = IM.empty}
+
+fun next (t : t) = #next t
+
+fun bind ({next, renaming}, n) =
+    ({next = next + 1,
+      renaming = IM.insert (renaming, n, next)}, next)
+
+fun lookup ({next, renaming}, n) =
+    IM.find (renaming, n)
+
+end
+
+fun renameCon st (all as (c, loc)) =
+    case c of
+        TFun (c1, c2) => (TFun (renameCon st c1, renameCon st c2), loc)
+      | TCFun (x, k, c) => (TCFun (x, k, renameCon st c), loc)
+      | TRecord c => (TRecord (renameCon st c), loc)
+      | CRel _ => all
+      | CNamed n =>
+        (case St.lookup (st, n) of
+             NONE => all
+           | SOME n' => (CNamed n', loc))
+      | CModProj (n, ms, x) =>
+        (case St.lookup (st, n) of
+             NONE => all
+           | SOME n' => (CModProj (n', ms, x), loc))
+      | CApp (c1, c2) => (CApp (renameCon st c1, renameCon st c2), loc)
+      | CAbs (x, k, c) => (CAbs (x, k, renameCon st c), loc)
+      | CKAbs (x, c) => (CKAbs (x, renameCon st c), loc)
+      | CKApp (c, k) => (CKApp (renameCon st c, k), loc)
+      | TKFun (x, c) => (TKFun (x, renameCon st c), loc)
+      | CName _ => all
+      | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (renameCon st x, renameCon st c)) xcs), loc)
+      | CConcat (c1, c2) => (CConcat (renameCon st c1, renameCon st c2), loc)
+      | CMap _ => all
+      | CUnit => all
+      | CTuple cs => (CTuple (map (renameCon st) cs), loc)
+      | CProj (c, n) => (CProj (renameCon st c, n), loc)
+
+fun renamePatCon st pc =
+    case pc of
+        PConVar n =>
+        (case St.lookup (st, n) of
+             NONE => pc
+           | SOME n' => PConVar n')
+      | PConProj (n, ms, x) =>
+        (case St.lookup (st, n) of
+             NONE => pc
+           | SOME n' => PConProj (n', ms, x))
+
+fun renamePat st (all as (p, loc)) =
+    case p of
+        PWild => all
+      | PVar (x, c) => (PVar (x, renameCon st c), loc)
+      | PPrim _ => all
+      | PCon (dk, pc, cs, po) => (PCon (dk, renamePatCon st pc,
+                                        map (renameCon st) cs,
+                                        Option.map (renamePat st) po), loc)
+      | PRecord xpcs => (PRecord (map (fn (x, p, c) =>
+                                          (x, renamePat st p, renameCon st c)) xpcs), loc)
+
+fun renameExp st (all as (e, loc)) =
+    case e of
+        EPrim _ => all
+      | ERel _ => all
+      | ENamed n =>
+        (case St.lookup (st, n) of
+             NONE => all
+           | SOME n' => (ENamed n', loc))
+      | EModProj (n, ms, x) =>
+        (case St.lookup (st, n) of
+             NONE => all
+           | SOME n' => (EModProj (n', ms, x), loc))
+      | EApp (e1, e2) => (EApp (renameExp st e1, renameExp st e2), loc)
+      | EAbs (x, dom, ran, e) => (EAbs (x, renameCon st dom, renameCon st ran, renameExp st e), loc)
+      | ECApp (e, c) => (ECApp (renameExp st e, renameCon st c), loc)
+      | ECAbs (x, k, e) => (ECAbs (x, k, renameExp st e), loc)
+      | EKAbs (x, e) => (EKAbs (x, renameExp st e), loc)
+      | EKApp (e, k) => (EKApp (renameExp st e, k), loc)
+      | ERecord xecs => (ERecord (map (fn (x, e, c) => (renameCon st x,
+                                                        renameExp st e,
+                                                        renameCon st c)) xecs), loc)
+      | EField (e, c, {field, rest}) => (EField (renameExp st e,
+                                                 renameCon st c,
+                                                 {field = renameCon st field,
+                                                  rest = renameCon st rest}), loc)
+      | EConcat (e1, c1, e2, c2) => (EConcat (renameExp st e1,
+                                              renameCon st c1,
+                                              renameExp st e2,
+                                              renameCon st c2), loc)
+      | ECut (e, c, {field, rest}) => (ECut (renameExp st e,
+                                             renameCon st c,
+                                             {field = renameCon st field,
+                                              rest = renameCon st rest}), loc)
+      | ECutMulti (e, c, {rest}) => (ECutMulti (renameExp st e,
+                                                renameCon st c,
+                                                {rest = renameCon st rest}), loc)
+      | ECase (e, pes, {disc, result}) => (ECase (renameExp st e,
+                                                  map (fn (p, e) => (renamePat st p, renameExp st e)) pes,
+                                                  {disc = renameCon st disc,
+                                                   result = renameCon st result}), loc)
+      | EWrite e => (EWrite (renameExp st e), loc)
+      | ELet (x, c1, e1, e2) => (ELet (x, renameCon st c1,
+                                      renameExp st e1,
+                                      renameExp st e2), loc)
+
+fun renameSitem st (all as (si, loc)) =
+    case si of
+        SgiConAbs _ => all
+      | SgiCon (x, n, k, c) => (SgiCon (x, n, k, renameCon st c), loc)
+      | SgiDatatype dts => (SgiDatatype (map (fn (x, n, xs, cns) =>
+                                                 (x, n, xs,
+                                                  map (fn (x, n, co) =>
+                                                          (x, n, Option.map (renameCon st) co)) cns)) dts),
+                            loc)
+      | SgiDatatypeImp (x, n, n', xs, x', xs', cns) =>
+        (SgiDatatypeImp (x, n, n', xs, x', xs',
+                         map (fn (x, n, co) =>
+                                 (x, n, Option.map (renameCon st) co)) cns), loc)
+      | SgiVal (x, n, c) => (SgiVal (x, n, renameCon st c), loc)
+      | SgiSgn (x, n, sg) => (SgiSgn (x, n, renameSgn st sg), loc)
+      | SgiStr (x, n, sg) => (SgiStr (x, n, renameSgn st sg), loc)
+
+and renameSgn st (all as (sg, loc)) =
+    case sg of
+        SgnConst sis => (SgnConst (map (renameSitem st) sis), loc)
+      | SgnVar n =>
+        (case St.lookup (st, n) of
+             NONE => all
+           | SOME n' => (SgnVar n', loc))
+      | SgnFun (x, n, dom, ran) => (SgnFun (x, n, renameSgn st dom, renameSgn st ran), loc)
+      | SgnWhere (sg, xs, s, c) => (SgnWhere (renameSgn st sg, xs, s, renameCon st c), loc)
+      | SgnProj (n, ms, x) =>
+        (case St.lookup (st, n) of
+             NONE => all
+           | SOME n' => (SgnProj (n', ms, x), loc))
+
+fun renameDecl st (all as (d, loc)) =
+    case d of
+        DCon (x, n, k, c) => (DCon (x, n, k, renameCon st c), loc)
+      | DDatatype dts => (DDatatype (map (fn (x, n, xs, cns) =>
+                                             (x, n, xs,
+                                              map (fn (x, n, co) =>
+                                                      (x, n, Option.map (renameCon st) co)) cns)) dts),
+                          loc)
+      | DDatatypeImp (x, n, n', xs, x', xs', cns) =>
+        (DDatatypeImp (x, n, n', xs, x', xs',
+                       map (fn (x, n, co) =>
+                               (x, n, Option.map (renameCon st) co)) cns), loc)
+      | DVal (x, n, c, e) => (DVal (x, n, renameCon st c, renameExp st e), loc)
+      | DValRec vis => (DValRec (map (fn (x, n, c, e) => (x, n, renameCon st c, renameExp st e)) vis), loc)
+      | DSgn (x, n, sg) => (DSgn (x, n, renameSgn st sg), loc)
+      | DStr (x, n, sg, str) => (DStr (x, n, renameSgn st sg, renameStr st str), loc)
+      | DFfiStr (x, n, sg) => (DFfiStr (x, n, renameSgn st sg), loc)
+      | DExport (n, sg, str) =>
+        (case St.lookup (st, n) of
+             NONE => all
+           | SOME n' => (DExport (n', renameSgn st sg, renameStr st str), loc))
+      | DTable (n, x, m, c1, e1, c2, e2, c3) =>
+        (DTable (n, x, m, renameCon st c1, renameExp st e1, renameCon st c2,
+                 renameExp st e2, renameCon st c3), loc)
+      | DSequence _ => all
+      | DView (n, x, n', e, c) => (DView (n, x, n', renameExp st e, renameCon st c), loc)
+      | DDatabase _ => all
+      | DCookie (n, x, n', c) => (DCookie (n, x, n', renameCon st c), loc)
+      | DStyle _ => all
+      | DTask (e1, e2) => (DTask (renameExp st e1, renameExp st e2), loc)
+      | DPolicy e => (DPolicy (renameExp st e), loc)
+      | DOnError (n, xs, x) =>
+        (case St.lookup (st, n) of
+             NONE => all
+           | SOME n' => (DOnError (n', xs, x), loc))
+
+and renameStr st (all as (str, loc)) =
+    case str of
+        StrConst ds => (StrConst (map (renameDecl st) ds), loc)
+      | StrVar n =>
+        (case St.lookup (st, n) of
+             NONE => all
+           | SOME n' => (StrVar n', loc))
+      | StrProj (str, x) => (StrProj (renameStr st str, x), loc)
+      | StrFun (x, n, dom, ran, str) => (StrFun (x, n, renameSgn st dom,
+                                                 renameSgn st ran,
+                                                 renameStr st str), loc)
+      | StrApp (str1, str2) => (StrApp (renameStr st str1, renameStr st str2), loc)
+
+
+
+fun fromArity (n, loc) =
+    case n of
+        0 => (KType, loc)
+      | _ => (KArrow ((KType, loc), fromArity (n - 1, loc)), loc)
+
+fun dupDecl (all as (d, loc), st) =
+    case d of
+        DCon (x, n, k, c) =>
+        let
+            val (st, n') = St.bind (st, n)
+        in
+            ([(DCon (x, n, k, renameCon st c), loc),
+              (DCon (x, n', k, (CNamed n, loc)), loc)],
+             st)
+        end
+      | DDatatype dts =>
+        let
+            val (dts', st) = ListUtil.foldlMap (fn ((x, n, xs, cns), st) =>
+                                                   let
+                                                       val (st, n') = St.bind (st, n)
+
+                                                       val (cns', st) = ListUtil.foldlMap
+                                                                            (fn ((x, n, _), st) =>
+                                                                                let
+                                                                                    val (st, n') =
+                                                                                        St.bind (st, n)
+                                                                                in
+                                                                                    ((x, n, n'), st)
+                                                                                end) st cns
+                                                   in
+                                                       ((x, n, length xs, n', cns'), st)
+                                                   end) st dts
+
+            val d = (DDatatype (map (fn (x, n, xs, cns) =>
+                                        (x, n, xs,
+                                         map (fn (x, n, co) =>
+                                                 (x, n, Option.map (renameCon st) co)) cns)) dts),
+                     loc)
+
+            val env = E.declBinds E.empty d
+        in
+            (d
+             :: map (fn (x, n, arity, n', _) =>
+                        (DCon (x, n', fromArity (arity, loc), (CNamed n, loc)), loc)) dts'
+             @ ListUtil.mapConcat (fn (_, _, _, _, cns') =>
+                                      map (fn (x, n, n') =>
+                                              (DVal (x, n', #2 (E.lookupENamed env n), (ENamed n, loc)),
+                                               loc)) cns') dts',
+             st)
+        end
+      | DDatatypeImp (x, n, n', xs, x', xs', cns) =>
+        let
+            val (cns', st) = ListUtil.foldlMap
+                                 (fn ((x, n, _), st) =>
+                                     let
+                                         val (st, n') =
+                                             St.bind (st, n)
+                                     in
+                                         ((x, n, n'), st)
+                                     end) st cns
+
+            val (st, n') = St.bind (st, n)
+
+            val d = (DDatatypeImp (x, n, n', xs, x', xs',
+                                   map (fn (x, n, co) =>
+                                           (x, n, Option.map (renameCon st) co)) cns), loc)
+
+            val env = E.declBinds E.empty d
+        in
+            (d
+             :: (DCon (x, n', fromArity (length xs, loc), (CNamed n, loc)), loc)
+             :: map (fn (x, n, n') =>
+                        (DVal (x, n', #2 (E.lookupENamed env n), (ENamed n, loc)),
+                         loc)) cns',
+             st)
+        end
+      | DVal (x, n, c, e) =>
+        let
+            val (st, n') = St.bind (st, n)
+            val c' = renameCon st c
+        in
+            ([(DVal (x, n, c', renameExp st e), loc),
+              (DVal (x, n', c', (ENamed n, loc)), loc)],
+             st)
+        end
+      | DValRec vis =>
+        let
+            val d = (DValRec (map (fn (x, n, c, e) => (x, n, renameCon st c, renameExp st e)) vis), loc)
+
+            val (vis', st) = ListUtil.foldlMap (fn ((x, n, _, _), st) =>
+                                                   let
+                                                       val (st, n') = St.bind (st, n)
+                                                   in
+                                                       ((x, n, n'), st)
+                                                   end) st vis
+
+            val env = E.declBinds E.empty d
+        in
+            (d
+             :: map (fn (x, n, n') => (DVal (x, n', #2 (E.lookupENamed env n), (ENamed n, loc)), loc)) vis',
+             st)
+        end
+      | DSgn (x, n, sg) =>
+        let
+            val (st, n') = St.bind (st, n)
+        in
+            ([(DSgn (x, n, renameSgn st sg), loc),
+              (DSgn (x, n', (SgnVar n, loc)), loc)],
+             st)
+        end
+      | DStr (x, n, sg, str) =>
+        let
+            val (st, n') = St.bind (st, n)
+            val sg' = renameSgn st sg
+        in
+            ([(DStr (x, n, sg', renameStr st str), loc),
+              (DStr (x, n', sg', (StrVar n, loc)), loc)],
+             st)
+        end
+      | DFfiStr (x, n, sg) => ([(DFfiStr (x, n, renameSgn st sg), loc)], st)
+      | DExport (n, sg, str) =>
+        (case St.lookup (st, n) of
+             NONE => ([all], st)
+           | SOME n' => ([(DExport (n', renameSgn st sg, renameStr st str), loc)], st))
+      | DTable (n, x, m, c1, e1, c2, e2, c3) =>
+        let
+            val (st, m') = St.bind (st, m)
+
+            val d = (DTable (n, x, m, renameCon st c1, renameExp st e1, renameCon st c2,
+                             renameExp st e2, renameCon st c3), loc)
+
+            val env = E.declBinds E.empty d
+        in
+            ([d, (DVal (x, m', #2 (E.lookupENamed env m), (ENamed m, loc)), loc)], st)
+        end
+      | DSequence (n, x, m) =>
+        let
+            val (st, m') = St.bind (st, m)
+
+            val env = E.declBinds E.empty all
+        in
+            ([all, (DVal (x, m', #2 (E.lookupENamed env m), (ENamed m, loc)), loc)], st)
+        end
+      | DView (n, x, m, e, c) =>
+        let
+            val (st, m') = St.bind (st, m)
+
+            val d = (DView (n, x, m, renameExp st e, renameCon st c), loc)
+
+            val env = E.declBinds E.empty d
+        in
+            ([d, (DVal (x, m', #2 (E.lookupENamed env m), (ENamed m, loc)), loc)], st)
+        end
+      | DDatabase _ => ([all], st)
+      | DCookie (n, x, m, c) =>
+        let
+            val (st, m') = St.bind (st, m)
+
+            val d = (DCookie (n, x, m, renameCon st c), loc)
+
+            val env = E.declBinds E.empty d
+        in
+            ([d, (DVal (x, m', #2 (E.lookupENamed env m), (ENamed m, loc)), loc)], st)
+        end
+      | DStyle (n, x, m) =>
+        let
+            val (st, m') = St.bind (st, m)
+
+            val env = E.declBinds E.empty all
+        in
+            ([all, (DVal (x, m', #2 (E.lookupENamed env m), (ENamed m, loc)), loc)], st)
+        end
+      | DTask (e1, e2) => ([(DTask (renameExp st e1, renameExp st e2), loc)], st)
+      | DPolicy e => ([(DPolicy (renameExp st e), loc)], st)
+      | DOnError (n, xs, x) =>
+        (case St.lookup (st, n) of
+             NONE => ([all], st)
+           | SOME n' => ([(DOnError (n', xs, x), loc)], st))
+
+fun rename {NextId, FormalName, FormalId, Body = all as (str, loc)} =
+    case str of
+        StrConst ds =>
+        let
+            val st = St.create NextId
+            val (st, n) = St.bind (st, FormalId)
+                     
+            val (ds, st) = ListUtil.foldlMapConcat dupDecl st ds
+            val ds = (DStr (FormalName, n, (SgnConst [], loc), (StrVar FormalId, loc)), loc) :: ds
+        in
+            (St.next st, (StrConst ds, loc))
+        end
+      | _ => (NextId, all)
+
+end
diff --git a/src/main.mlton.sml b/src/main.mlton.sml
index 6bdc9539..71fefc48 100644
--- a/src/main.mlton.sml
+++ b/src/main.mlton.sml
@@ -124,6 +124,13 @@ fun oneRun args =
               | "-dumpSource" :: rest =>
                 (Compiler.dumpSource := true;
                  doArgs rest)
+              | "-dumpVerboseSource" :: rest =>
+                (Compiler.dumpSource := true;
+                 ElabPrint.debug := true;
+                 ExplPrint.debug := true;
+                 CorePrint.debug := true;
+                 MonoPrint.debug := true;
+                 doArgs rest)
               | "-output" :: s :: rest =>
                 (Settings.setExe (SOME s);
                  doArgs rest)
diff --git a/src/sources b/src/sources
index 7ce9a7a0..f75803a3 100644
--- a/src/sources
+++ b/src/sources
@@ -115,6 +115,9 @@ $(SRC)/core_env.sml
 $(SRC)/core_print.sig
 $(SRC)/core_print.sml
 
+$(SRC)/expl_rename.sig
+$(SRC)/expl_rename.sml
+
 $(SRC)/corify.sig
 $(SRC)/corify.sml
 
diff --git a/tests/functorMadness.ur b/tests/functorMadness.ur
new file mode 100644
index 00000000..c7ddeaca
--- /dev/null
+++ b/tests/functorMadness.ur
@@ -0,0 +1,18 @@
+functor F(M : sig end) = struct
+    fun f () = f ()
+
+    functor G(M : sig end) = struct
+        fun g () = f ()
+    end
+end
+
+structure M1 = F(struct end)
+structure M2 = F(struct end)
+
+structure N1 = M1.G(struct end)
+structure N2 = M2.G(struct end)
+
+fun main () : transaction page =
+    return (N1.g ());
+    return (N2.g ());
+    return <xml/>
diff --git a/tests/functorMania.ur b/tests/functorMania.ur
new file mode 100644
index 00000000..c11ff473
--- /dev/null
+++ b/tests/functorMania.ur
@@ -0,0 +1,36 @@
+functor F1(M : sig type t end) = struct
+    type t = M.t
+    fun g () : M.t = g ()
+    fun f () = g ()
+end
+functor F2(M : sig type t end) = F1(M)
+functor F3(M : sig type t end) = F2(M)
+
+functor F4(M : sig end) = F1(struct type t = int end)
+functor F5(M : sig end) = F2(struct type t = int end)
+functor F6(M : sig end) = F3(struct type t = int end)
+
+functor F7(M : sig end) = F1(struct type t = string end)
+functor F8(M : sig end) = F2(struct type t = string end)
+functor F9(M : sig end) = F3(struct type t = string end)
+
+structure M1 = F1(struct type t = string end)
+structure M2 = F2(struct type t = string end)
+structure M3 = F3(struct type t = string end)
+
+structure M4 = F4(struct  end)
+structure M5 = F5(struct end)
+structure M6 = F6(struct end)
+
+structure M7 = F7(struct end)
+structure M8 = F8(struct end)
+structure M9 = F9(struct end)
+
+fun loop x : unit = loop (M1.f (), M2.f (), M3.f (),
+                          M4.f (), M5.f (), M6.f (),
+                          M7.f (), M8.f (), M9.f ())
+
+fun main () : transaction page =
+    x <- error <xml/>;
+    u <- return (loop x);
+    return <xml/>