First Unnest tests working

11 files changed, 583 insertions, 5 deletions

diff --git a/src/compiler.sig b/src/compiler.sig
index e26ec13c..bc1974a1 100644
--- a/src/compiler.sig
+++ b/src/compiler.sig
@@ -58,6 +58,7 @@ signature COMPILER = sig
 
     val parse : (job, Source.file) phase
     val elaborate : (Source.file, Elab.file) phase
+    val unnest : (Elab.file, Elab.file) phase
     val termination : (Elab.file, Elab.file) phase
     val explify : (Elab.file, Expl.file) phase
     val corify : (Expl.file, Core.file) phase
@@ -80,6 +81,7 @@ signature COMPILER = sig
     val toParseJob : (string, job) transform
     val toParse : (string, Source.file) transform
     val toElaborate : (string, Elab.file) transform
+    val toUnnest : (string, Elab.file) transform
     val toTermination : (string, Elab.file) transform
     val toExplify : (string, Expl.file) transform
     val toCorify : (string, Core.file) transform
diff --git a/src/compiler.sml b/src/compiler.sml
index 4f1bce11..e92f86c3 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -383,12 +383,19 @@ val elaborate = {
 
 val toElaborate = transform elaborate "elaborate" o toParse
 
+val unnest = {
+    func = Unnest.unnest,
+    print = ElabPrint.p_file ElabEnv.empty
+}
+
+val toUnnest = transform unnest "unnest" o toElaborate
+
 val termination = {
     func = (fn file => (Termination.check file; file)),
     print = ElabPrint.p_file ElabEnv.empty
 }
 
-val toTermination = transform termination "termination" o toElaborate
+val toTermination = transform termination "termination" o toUnnest
 
 val explify = {
     func = Explify.explify,
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 727ee259..90cf8153 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -30,6 +30,10 @@ signature ELAB_ENV = sig
     exception SynUnif
     val liftConInCon : int -> Elab.con -> Elab.con
 
+    val liftExpInExp : int -> Elab.exp -> Elab.exp
+
+    val subExpInExp : (int * Elab.exp) -> Elab.exp -> Elab.exp
+
     type env
 
     val empty : env
diff --git a/src/elab_env.sml b/src/elab_env.sml
index f4f5d2cb..2732de13 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -61,6 +61,20 @@ val liftConInCon =
 
 val lift = liftConInCon 0
 
+val liftConInExp =
+    U.Exp.mapB {kind = fn k => k,
+                con = fn bound => fn c =>
+                                     case c of
+                                         CRel xn =>
+                                         if xn < bound then
+                                             c
+                                         else
+                                             CRel (xn + 1)
+                                       | _ => c,
+                exp = fn _ => fn e => e,
+                bind = fn (bound, U.Exp.RelC _) => bound + 1
+                        | (bound, _) => bound}
+
 val liftExpInExp =
     U.Exp.mapB {kind = fn k => k,
                 con = fn _ => fn c => c,
@@ -78,6 +92,21 @@ val liftExpInExp =
 
 val liftExp = liftExpInExp 0
 
+val subExpInExp =
+    U.Exp.mapB {kind = fn k => k,
+                con = fn _ => fn c => c,
+                exp = fn (xn, rep) => fn e =>
+                                  case e of
+                                      ERel xn' =>
+                                      (case Int.compare (xn', xn) of
+                                           EQUAL => #1 rep
+                                         | GREATER=> ERel (xn' - 1)
+                                         | LESS => e)
+                                    | _ => e,
+                bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
+                        | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep)
+                        | (ctx, _) => ctx}
+
 (* Back to environments *)
 
 datatype 'a var' =
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 3d7ce625..b236954e 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -198,7 +198,7 @@ fun p_patCon env pc =
               string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n)
           else
               string (#1 (E.lookupENamed env n)))
-         handle E.UnboundRel _ => string ("UNBOUND_NAMED" ^ Int.toString n))
+         handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n))
       | PConProj (m1, ms, x) =>
         let
             val m1x = #1 (E.lookupStrNamed env m1)
@@ -247,7 +247,7 @@ fun p_exp' par env (e, _) =
               string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n)
           else
               string (#1 (E.lookupENamed env n)))
-         handle E.UnboundRel _ => string ("UNBOUND_NAMED" ^ Int.toString n))
+         handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n))
       | EModProj (m1, ms, x) =>
         let
             val m1x = #1 (E.lookupStrNamed env m1)
diff --git a/src/elab_util.sig b/src/elab_util.sig
index f4edd972..f9988981 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -57,6 +57,11 @@ structure Con : sig
               -> Elab.con -> Elab.con
     val exists : {kind : Elab.kind' -> bool,
                   con : Elab.con' -> bool} -> Elab.con -> bool
+
+    val foldB : {kind : Elab.kind' * 'state -> 'state,
+                 con : 'context * Elab.con' * 'state -> 'state,
+                 bind : 'context * binder -> 'context}
+                -> 'context -> 'state -> Elab.con -> 'state
 end
 
 structure Exp : sig
@@ -83,6 +88,12 @@ structure Exp : sig
     val exists : {kind : Elab.kind' -> bool,
                   con : Elab.con' -> bool,
                   exp : Elab.exp' -> bool} -> Elab.exp -> bool
+
+    val foldB : {kind : Elab.kind' * 'state -> 'state,
+                 con : 'context * Elab.con' * 'state -> 'state,
+                 exp : 'context * Elab.exp' * 'state -> 'state,
+                 bind : 'context * binder -> 'context}
+                -> 'context -> 'state -> Elab.exp -> 'state
 end
 
 structure Sgn : sig
@@ -156,6 +167,20 @@ structure Decl : sig
                   str : Elab.str' -> 'a option,
                   decl : Elab.decl' -> 'a option}
                  -> Elab.decl -> 'a option
+
+    val foldMapB : {kind : Elab.kind' * 'state -> Elab.kind' * 'state,
+                    con : 'context * Elab.con' * 'state -> Elab.con' * 'state,
+                    exp : 'context * Elab.exp' * 'state -> Elab.exp' * 'state,
+                    sgn_item : 'context * Elab.sgn_item' * 'state -> Elab.sgn_item' * 'state,
+                    sgn : 'context * Elab.sgn' * 'state -> Elab.sgn' * 'state,
+                    str : 'context * Elab.str' * 'state -> Elab.str' * 'state,
+                    decl : 'context * Elab.decl' * 'state -> Elab.decl' * 'state,
+                    bind : 'context * binder -> 'context}
+                   -> 'context -> 'state -> Elab.decl -> Elab.decl * 'state
+end
+
+structure File : sig
+    val maxName : Elab.file -> int
 end
 
 end
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 28fe8f22..2e190d1e 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -226,6 +226,13 @@ fun exists {kind, con} k =
         S.Return _ => true
       | S.Continue _ => false
 
+fun foldB {kind, con, bind} ctx st c =
+    case mapfoldB {kind = fn k => fn st => S.Continue (k, kind (k, st)),
+                   con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)),
+                   bind = bind} ctx c st of
+        S.Continue (_, st) => st
+      | S.Return _ => raise Fail "ElabUtil.Con.foldB: Impossible"
+
 end
 
 structure Exp = struct
@@ -340,8 +347,20 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
                 S.bind2 (mfe ctx e,
                          fn e' =>
                             S.bind2 (ListUtil.mapfold (fn (p, e) =>
-                                                         S.map2 (mfe ctx e,
-                                                              fn e' => (p, e'))) pes,
+                                                          let
+                                                              fun pb ((p, _), ctx) =
+                                                                  case p of
+                                                                      PWild => ctx
+                                                                    | PVar (x, t) => bind (ctx, RelE (x, t))
+                                                                    | PPrim _ => ctx
+                                                                    | PCon (_, _, _, NONE) => ctx
+                                                                    | PCon (_, _, _, SOME p) => pb (p, ctx)
+                                                                    | PRecord xps => foldl (fn ((_, p, _), ctx) =>
+                                                                                               pb (p, ctx)) ctx xps
+                                                          in
+                                                              S.map2 (mfe (pb (p, ctx)) e,
+                                                                   fn e' => (p, e'))
+                                                          end) pes,
                                     fn pes' =>
                                        S.bind2 (mfc ctx disc,
                                              fn disc' =>
@@ -431,6 +450,14 @@ fun mapB {kind, con, exp, bind} ctx e =
         S.Continue (e, ()) => e
       | S.Return _ => raise Fail "ElabUtil.Exp.mapB: Impossible"
 
+fun foldB {kind, con, exp, bind} ctx st e =
+    case mapfoldB {kind = fn k => fn st => S.Continue (k, kind (k, st)),
+                   con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)),
+                   exp = fn ctx => fn e => fn st => S.Continue (e, exp (ctx, e, st)),
+                   bind = bind} ctx e st of
+        S.Continue (_, st) => st
+      | S.Return _ => raise Fail "ElabUtil.Exp.foldB: Impossible"
+
 end
 
 structure Sgn = struct
@@ -888,6 +915,82 @@ fun search {kind, con, exp, sgn_item, sgn, str, decl} k =
         S.Return x => SOME x
       | S.Continue _ => NONE
 
+fun foldMapB {kind, con, exp, sgn_item, sgn, str, decl, bind} ctx st d =
+    case mapfoldB {kind = fn x => fn st => S.Continue (kind (x, st)),
+                   con = fn ctx => fn x => fn st => S.Continue (con (ctx, x, st)),
+                   exp = fn ctx => fn x => fn st => S.Continue (exp (ctx, x, st)),
+                   sgn_item = fn ctx => fn x => fn st => S.Continue (sgn_item (ctx, x, st)),
+                   sgn = fn ctx => fn x => fn st => S.Continue (sgn (ctx, x, st)),
+                   str = fn ctx => fn x => fn st => S.Continue (str (ctx, x, st)),
+                   decl = fn ctx => fn x => fn st => S.Continue (decl (ctx, x, st)),
+                   bind = bind} ctx d st of
+        S.Continue x => x
+      | S.Return _ => raise Fail "ElabUtil.Decl.foldMapB: Impossible"
+
+end
+
+structure File = struct
+
+fun maxName ds = foldl (fn (d, count) => Int.max (maxNameDecl d, count)) 0 ds
+
+and maxNameDecl (d, _) =
+    case d of
+        DCon (_, n, _, _) => n
+      | DDatatype (_, n, _, ns) =>
+                  foldl (fn ((_, n', _), m) => Int.max (n', m))
+                        n ns
+      | DDatatypeImp (_, n1, n2, _, _, _, ns) =>
+        foldl (fn ((_, n', _), m) => Int.max (n', m))
+              (Int.max (n1, n2)) ns
+      | DVal (_, n, _, _) => n
+      | DValRec vis => foldl (fn ((_, n, _, _), count) => Int.max (n, count)) 0 vis
+      | DStr (_, n, sgn, str) => Int.max (n, Int.max (maxNameSgn sgn, maxNameStr str))
+      | DSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
+      | DFfiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
+      | DConstraint _ => 0
+      | DClass (_, n, _) => n
+      | DExport _ => 0
+      | DTable (n, _, _, _) => n
+      | DSequence (n, _, _) => n
+      | DDatabase _ => 0
+
+and maxNameStr (str, _) =
+    case str of
+        StrConst ds => maxName ds
+      | StrVar n => n
+      | StrProj (str, _) => maxNameStr str
+      | StrFun (_, n, dom, ran, str) => foldl Int.max n [maxNameSgn dom, maxNameSgn ran, maxNameStr str]
+      | StrApp (str1, str2) => Int.max (maxNameStr str1, maxNameStr str2)
+      | StrError => 0
+
+and maxNameSgn (sgn, _) =
+    case sgn of
+        SgnConst sgis => foldl (fn (sgi, count) => Int.max (maxNameSgi sgi, count)) 0 sgis
+      | SgnVar n => n
+      | SgnFun (_, n, dom, ran) => Int.max (n, Int.max (maxNameSgn dom, maxNameSgn ran))
+      | SgnWhere (sgn, _, _) => maxNameSgn sgn
+      | SgnProj (n, _, _) => n
+      | SgnError => 0
+
+and maxNameSgi (sgi, _) =
+    case sgi of
+        SgiConAbs (_, n, _) => n
+      | SgiCon (_, n, _, _) => n
+      | SgiDatatype (_, n, _, ns) =>
+        foldl (fn ((_, n', _), m) => Int.max (n', m))
+              n ns
+      | SgiDatatypeImp (_, n1, n2, _, _, _, ns) =>
+        foldl (fn ((_, n', _), m) => Int.max (n', m))
+              (Int.max (n1, n2)) ns
+      | SgiVal (_, n, _) => n
+      | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
+      | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
+      | SgiConstraint _ => 0
+      | SgiTable (n, _, _, _) => n
+      | SgiSequence (n, _, _) => n
+      | SgiClassAbs (_, n) => n
+      | SgiClass (_, n, _) => n
+              
 end
 
 end
diff --git a/src/sources b/src/sources
index ebf71d9e..984b5e23 100644
--- a/src/sources
+++ b/src/sources
@@ -50,6 +50,9 @@ elab_err.sml
 elaborate.sig
 elaborate.sml
 
+unnest.sig
+unnest.sml
+
 termination.sig
 termination.sml
 
diff --git a/src/termination.sml b/src/termination.sml
index b0716eca..6ed4d92f 100644
--- a/src/termination.sml
+++ b/src/termination.sml
@@ -292,6 +292,8 @@ fun declOk' env (d, loc) =
                       | EError => (Rabble, calls)
                       | EUnif (ref (SOME e)) => exp parent (penv, calls) e
                       | EUnif (ref NONE) => (Rabble, calls)
+
+                      | ELet (_, e) => exp parent (penv, calls) e
                 end
 
             fun doVali (i, (_, f, _, e), calls) =
diff --git a/src/unnest.sig b/src/unnest.sig
new file mode 100644
index 00000000..6508a781
--- /dev/null
+++ b/src/unnest.sig
@@ -0,0 +1,34 @@
+(* Copyright (c) 2008, 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.
+ *)
+
+(* Remove nested function definitions *)
+
+signature UNNEST = sig
+
+    val unnest : Elab.file -> Elab.file
+    
+end
diff --git a/src/unnest.sml b/src/unnest.sml
new file mode 100644
index 00000000..e5eddc42
--- /dev/null
+++ b/src/unnest.sml
@@ -0,0 +1,369 @@
+(* Copyright (c) 2008, 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.
+ *)
+
+(* Remove nested function definitions *)
+
+structure Unnest :> UNNEST = struct
+
+open Elab
+
+structure E = ElabEnv
+structure U = ElabUtil
+
+structure IS = IntBinarySet
+
+val fvsCon = U.Con.foldB {kind = fn (_, st) => st,
+                          con = fn (cb, c, cvs) =>
+                                   case c of
+                                       CRel n =>
+                                       if n >= cb then
+                                           IS.add (cvs, n - cb)
+                                       else
+                                           cvs
+                                     | _ => cvs,
+                          bind = fn (cb, b) =>
+                                    case b of
+                                        U.Con.Rel _ => cb + 1
+                                      | _ => cb}
+                         0 IS.empty
+
+fun fvsExp nr = U.Exp.foldB {kind = fn (_, st) => st,
+                             con = fn ((cb, eb), c, st as (cvs, evs)) =>
+                                      case c of
+                                          CRel n =>
+                                          if n >= cb then
+                                              (IS.add (cvs, n - cb), evs)
+                                          else
+                                              st
+                                        | _ => st,
+                             exp = fn ((cb, eb), e, st as (cvs, evs)) =>
+                                      case e of
+                                          ERel n =>
+                                          if n >= eb then
+                                              (cvs, IS.add (evs, n - eb))
+                                          else
+                                              st
+                                        | _ => st,
+                             bind = fn (ctx as (cb, eb), b) =>
+                                       case b of
+                                           U.Exp.RelC _ => (cb + 1, eb)
+                                         | U.Exp.RelE _ => (cb, eb + 1)
+                                         | _ => ctx}
+                            (0, nr) (IS.empty, IS.empty)
+
+fun positionOf (x : int) ls =
+    let
+        fun po n ls =
+            case ls of
+                [] => raise Fail "Unnest.positionOf"
+              | x' :: ls' =>
+                if x' = x then
+                    n
+                else
+                    po (n + 1) ls'
+    in
+        po 0 ls
+        handle Fail _ => raise Fail ("Unnset.positionOf("
+                                     ^ Int.toString x
+                                     ^ ", "
+                                     ^ String.concatWith ";" (map Int.toString ls)
+                                     ^ ")")
+    end
+
+fun squishCon cfv =
+    U.Con.mapB {kind = fn k => k,
+                con = fn cb => fn c =>
+                                  case c of
+                                      CRel n =>
+                                      if n >= cb then
+                                          CRel (positionOf (n - cb) cfv + cb)
+                                      else
+                                          c
+                                    | _ => c,
+                bind = fn (cb, b) =>
+                          case b of
+                              U.Con.Rel _ => cb + 1
+                            | _ => cb}
+               0
+
+fun squishExp (nr, cfv, efv) =
+    U.Exp.mapB {kind = fn k => k,
+                con = fn (cb, eb) => fn c =>
+                                        case c of
+                                            CRel n =>
+                                            if n >= cb then
+                                                CRel (positionOf (n - cb) cfv + cb)
+                                            else
+                                                c
+                                          | _ => c,
+                exp = fn (cb, eb) => fn e =>
+                                        case e of
+                                            ERel n =>
+                                            if n >= eb then
+                                                 ERel (positionOf (n - eb) efv + eb)
+                                            else
+                                                e
+                                          | _ => e,
+                bind = fn (ctx as (cb, eb), b) =>
+                          case b of
+                              U.Exp.RelC _ => (cb + 1, eb)
+                            | U.Exp.RelE _ => (cb, eb + 1)
+                            | _ => ctx}
+               (0, nr)
+
+type state = {
+     maxName : int,
+     decls : decl list
+}
+
+fun kind (k, st) = (k, st)
+
+fun exp ((ks, ts), e, st : state) =
+    case e of
+        ELet (eds, e) =>
+        let
+            val doSubst = foldl (fn (p, e) => E.subExpInExp p e)
+
+            val (eds, (maxName, ds, subs)) =
+                ListUtil.foldlMapConcat
+                (fn (ed, (maxName, ds, subs)) =>
+                    case #1 ed of
+                        EDVal _ => ([ed], (maxName, ds, map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs))
+                      | EDValRec vis =>
+                        let
+                            val loc = #2 ed
+
+                            val nr = length vis
+                            val (cfv, efv) = foldl (fn ((_, t, e), (cfv, efv)) =>
+                                                       let
+                                                           val (cfv', efv') = fvsExp nr e
+                                                           (*val () = Print.prefaces "fvsExp"
+                                                                    [("e", ElabPrint.p_exp E.empty e),
+                                                                     ("cfv", Print.PD.string
+                                                                                 (Int.toString (IS.numItems cfv'))),
+                                                                     ("efv", Print.PD.string
+                                                                                 (Int.toString (IS.numItems efv')))]*)
+                                                           val cfv'' = fvsCon t
+                                                       in
+                                                           (IS.union (cfv, IS.union (cfv', cfv'')),
+                                                            IS.union (efv, efv'))
+                                                       end)
+                                                   (IS.empty, IS.empty) vis
+
+                            (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n")*)
+                            val cfv = IS.foldl (fn (x, cfv) =>
+                                                   let
+                                                       (*val () = print (Int.toString x ^ "\n")*)
+                                                       val (_, t) = List.nth (ts, x)
+                                                   in
+                                                       IS.union (cfv, fvsCon t)
+                                                   end)
+                                               cfv efv
+                            (*val () = print "B\n"*)
+
+                            val (vis, maxName) =
+                                ListUtil.foldlMap (fn ((x, t, e), maxName) =>
+                                                      ((x, maxName, t, e),
+                                                       maxName + 1))
+                                maxName vis
+
+                            fun apply e =
+                                let
+                                    val e = IS.foldl (fn (x, e) =>
+                                                         (ECApp (e, (CRel x, loc)), loc))
+                                            e cfv
+                                in
+                                    IS.foldl (fn (x, e) =>
+                                                 (EApp (e, (ERel x, loc)), loc))
+                                             e efv
+                                end
+
+                            val subs = map (fn (n, e) => (n + nr, E.liftExpInExp nr e)) subs
+
+                            val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) =>
+                                                          let
+                                                              val e = apply (ENamed n, loc)
+                                                          in
+                                                              (0, E.liftExpInExp (nr - i - 1) e)
+                                                          end)
+                                            vis
+                            val subs' = rev subs'
+
+                            val cfv = IS.listItems cfv
+                            val efv = IS.listItems efv
+                            val efn = length efv
+
+                            (*val subsInner = subs
+                                            @ map (fn (i, e) =>
+                                                      (i + efn,
+                                                       E.liftExpInExp efn e)) subs'*)
+
+                            val subs = subs @ subs'
+
+                            val vis = map (fn (x, n, t, e) =>
+                                              let
+                                                  (*val () = Print.prefaces "preSubst"
+                                                                          [("e", ElabPrint.p_exp E.empty e)]*)
+                                                  val e = doSubst e subs(*Inner*)
+
+                                                  (*val () = Print.prefaces "squishCon"
+                                                                          [("t", ElabPrint.p_con E.empty t)]*)
+                                                  val t = squishCon cfv t
+                                                  (*val () = Print.prefaces "squishExp"
+                                                                          [("e", ElabPrint.p_exp E.empty e)]*)
+                                                  val e = squishExp (nr, cfv, efv) e
+
+                                                  val (e, t) = foldr (fn (ex, (e, t)) =>
+                                                                         let
+                                                                             val (name, t') = List.nth (ts, ex)
+                                                                         in
+                                                                             ((EAbs (name,
+                                                                                     t',
+                                                                                     t,
+                                                                                     e), loc),
+                                                                              (TFun (t',
+                                                                                     t), loc))
+                                                                         end)
+                                                                     (e, t) efv
+
+                                                  val (e, t) = foldr (fn (cx, (e, t)) =>
+                                                                         let
+                                                                             val (name, k) = List.nth (ks, cx)
+                                                                         in
+                                                                             ((ECAbs (Explicit,
+                                                                                      name,
+                                                                                      k,
+                                                                                      e), loc),
+                                                                              (TCFun (Explicit,
+                                                                                      name,
+                                                                                      k,
+                                                                                      t), loc))
+                                                                         end)
+                                                                     (e, t) cfv
+                                              in
+                                                  (x, n, t, e)
+                                              end)
+                                          vis
+
+                            val d = (DValRec vis, #2 ed)
+                        in
+                            ([], (maxName, d :: ds, subs))
+                        end)
+                (#maxName st, #decls st, []) eds
+        in
+            (ELet (eds, doSubst e subs),
+             {maxName = maxName,
+              decls = ds})
+        end
+
+      | _ => (e, st)
+
+fun default (ctx, d, st) = (d, st)
+
+fun bind ((ks, ts), b) =
+    case b of
+        U.Decl.RelC p => (p :: ks, map (fn (name, t) => (name, E.liftConInCon 0 t)) ts)
+      | U.Decl.RelE p => (ks, p :: ts)
+      | _ => (ks, ts)                        
+
+val unnestDecl = U.Decl.foldMapB {kind = kind,
+                                  con = default,
+                                  exp = exp,
+                                  sgn_item = default,
+                                  sgn = default,
+                                  str = default,
+                                  decl = default,
+                                  bind = bind}
+                                 ([], [])
+
+fun unnest file =
+    let
+        fun doDecl (all as (d, loc), st : state) =
+            let
+                fun default () = ([all], st)
+                fun explore () =
+                    let
+                        val (d, st) = unnestDecl st all
+                    in
+                        (rev (d :: #decls st),
+                         {maxName = #maxName st,
+                          decls = []})
+                    end
+            in
+                case d of
+                    DCon _ => default ()
+                  | DDatatype _ => default ()
+                  | DDatatypeImp _ => default ()
+                  | DVal _ => explore ()
+                  | DValRec _ => explore ()
+                  | DSgn _ => default ()
+                  | DStr (x, n, sgn, str) =>
+                    let
+                        val (str, st) = doStr (str, st)
+                    in
+                        ([(DStr (x, n, sgn, str), loc)], st)
+                    end
+                  | DFfiStr _ => default ()
+                  | DConstraint _ => default ()
+                  | DExport _ => default ()
+                  | DTable _ => default ()
+                  | DSequence _ => default ()
+                  | DClass _ => default ()
+                  | DDatabase _ => default ()
+            end
+
+        and doStr (all as (str, loc), st) =
+            let
+                fun default () = (all, st)
+            in
+                case str of
+                    StrConst ds =>
+                    let
+                        val (ds, st) = ListUtil.foldlMapConcat doDecl st ds
+                    in
+                        ((StrConst ds, loc), st)
+                    end
+                  | StrVar _ => default ()
+                  | StrProj _ => default ()
+                  | StrFun (x, n, dom, ran, str) =>
+                    let
+                        val (str, st) = doStr (str, st)
+                    in
+                        ((StrFun (x, n, dom, ran, str), loc), st)
+                    end
+                  | StrApp _ => default ()
+                  | StrError => raise Fail "Unnest: StrError"
+            end
+
+        val (ds, _) = ListUtil.foldlMapConcat doDecl
+                      {maxName = U.File.maxName file + 1,
+                       decls = []} file
+    in
+        ds
+    end
+
+end