Closure conversion

31 files changed, 1609 insertions, 55 deletions

diff --git a/src/cloconv.sig b/src/cloconv.sig
new file mode 100644
index 00000000..d71d3201
--- /dev/null
+++ b/src/cloconv.sig
@@ -0,0 +1,32 @@
+(* 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.
+ *)
+
+signature CLOCONV = sig
+
+    val cloconv : Mono.file -> Flat.file
+
+end
diff --git a/src/cloconv.sml b/src/cloconv.sml
new file mode 100644
index 00000000..fdf05363
--- /dev/null
+++ b/src/cloconv.sml
@@ -0,0 +1,195 @@
+(* 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.
+ *)
+
+structure Cloconv :> CLOCONV = struct
+
+structure L = Mono
+structure L' = Flat
+
+structure IS = IntBinarySet
+
+structure U = FlatUtil
+structure E = FlatEnv
+
+open Print.PD
+open Print
+
+val liftExpInExp =
+    U.Exp.mapB {typ = fn t => t,
+                exp = fn bound => fn e =>
+                                     case e of
+                                         L'.ERel xn =>
+                                         if xn < bound then
+                                             e
+                                         else
+                                             L'.ERel (xn + 1)
+                                       | _ => e,
+                bind = fn (bound, U.Exp.RelE _) => bound + 1
+                        | (bound, _) => bound}
+val subExpInExp =
+    U.Exp.mapB {typ = fn t => t,
+                exp = fn (xn, rep) => fn e =>
+                                  case e of
+                                      L'.ERel xn' =>
+                                      if xn = xn' then
+                                          #1 rep
+                                      else
+                                          e
+                                    | _ => e,
+                bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
+                        | (ctx, _) => ctx}
+
+
+fun ccTyp (t, loc) =
+    case t of
+        L.TFun (t1, t2) => (L'.TFun (ccTyp t1, ccTyp t2), loc)
+      | L.TRecord xts => (L'.TRecord (map (fn (x, t) => (x, ccTyp t)) xts), loc)
+      | L.TNamed n => (L'.TNamed n, loc)
+
+structure Ds :> sig
+    type t
+
+    val empty : t
+
+    val exp : t -> string * int * L'.typ * L'.exp -> t
+    val func : t -> string * L'.typ * L'.typ * L'.exp -> t * int
+    val decls : t -> L'.decl list
+
+    val enter : t -> t
+    val used : t * int -> t
+    val leave : t -> t
+    val listUsed : t -> int list
+end = struct
+
+type t = int * L'.decl list * IS.set
+
+val empty = (0, [], IS.empty)
+
+fun exp (fc, ds, vm) (v as (_, _, _, (_, loc))) = (fc, (L'.DVal v, loc) :: ds, vm)
+
+fun func (fc, ds, vm) (x, dom, ran, e as (_, loc)) =
+    ((fc+1, (L'.DFun (fc, x, dom, ran, e), loc) :: ds, vm), fc)
+
+fun decls (_, ds, _) = rev ds
+
+fun enter (fc, ds, vm) = (fc, ds, IS.map (fn n => n + 1) vm)
+fun used ((fc, ds, vm), n) = (fc, ds, IS.add (vm, n))
+fun leave (fc, ds, vm) = (fc, ds, IS.map (fn n => n - 1) (IS.delete (vm, 0) handle NotFound => vm))
+
+fun listUsed (_, _, vm) = IS.listItems vm
+
+end
+
+
+fun ccExp env ((e, loc), D) =
+    case e of
+        L.EPrim p => ((L'.EPrim p, loc), D)
+      | L.ERel n => ((L'.ERel n, loc), Ds.used (D, n))
+      | L.ENamed n => ((L'.ENamed n, loc), D)
+      | L.EApp (e1, e2) =>
+        let
+            val (e1, D) = ccExp env (e1, D)
+            val (e2, D) = ccExp env (e2, D)
+        in
+            ((L'.ELet ([("closure", e1),
+                        ("arg", liftExpInExp 0 e2),
+                        ("code", (L'.EField ((L'.ERel 1, loc), "func"), loc)),
+                        ("env", (L'.EField ((L'.ERel 2, loc), "env"), loc))],
+                       (L'.EApp ((L'.ERel 1, loc),
+                                 (L'.ERecord [("env", (L'.ERel 0, loc)),
+                                              ("arg", (L'.ERel 2, loc))], loc)), loc)), loc), D)
+        end
+      | L.EAbs (x, dom, ran, e) =>
+        let
+            val dom = ccTyp dom
+            val ran = ccTyp ran
+            val (e, D) = ccExp (E.pushERel env x dom) (e, Ds.enter D)
+            val ns = Ds.listUsed D
+            val ns = List.filter (fn n => n <> 0) ns
+            val D = Ds.leave D
+
+            (*val () = Print.preface ("Before", FlatPrint.p_exp FlatEnv.basis e)
+            val () = List.app (fn (x, t) => preface ("Bound", box [string x,
+                                                                   space,
+                                                                   string ":",
+                                                                   space,
+                                                                   FlatPrint.p_typ env t]))
+                     (E.listERels env)
+            val () = List.app (fn n => preface ("Free", FlatPrint.p_exp (E.pushERel env x dom)
+                                                        (L'.ERel n, loc))) ns*)
+            val body = foldl (fn (n, e) =>
+                                 subExpInExp (n, (L'.EField ((L'.ERel 1, loc), "fv" ^ Int.toString n), loc)) e)
+                             e ns
+            (*val () = Print.preface (" After", FlatPrint.p_exp FlatEnv.basis body)*)
+            val body = (L'.ELet ([("env", (L'.EField ((L'.ERel 0, loc), "env"), loc)),
+                                  ("arg", (L'.EField ((L'.ERel 1, loc), "arg"), loc))],
+                                 body), loc)
+                              
+            val envT = (L'.TRecord (map (fn n => ("fv" ^ Int.toString n, #2 (E.lookupERel env (n-1)))) ns), loc)
+            val (D, fi) = Ds.func D (x, (L'.TRecord [("env", envT), ("arg", dom)], loc), ran, body)
+        in
+            ((L'.ERecord [("code", (L'.ECode fi, loc)),
+                          ("env", (L'.ERecord (map (fn n => ("fv" ^ Int.toString n,
+                                                             (L'.ERel (n-1), loc))) ns), loc))], loc), D)
+        end
+
+      | L.ERecord xes =>
+        let
+            val (xes, D) = ListUtil.foldlMap (fn ((x, e), D) =>
+                                                 let
+                                                     val (e, D) = ccExp env (e, D)
+                                                 in
+                                                     ((x, e), D)
+                                                 end) D xes
+        in
+            ((L'.ERecord xes, loc), D)
+        end
+      | L.EField (e1, x) =>
+        let
+            val (e1, D) = ccExp env (e1, D)
+        in
+            ((L'.EField (e1, x), loc), D)
+        end
+
+fun ccDecl ((d, loc), D) =
+    case d of
+        L.DVal (x, n, t, e) =>
+        let
+            val t = ccTyp t
+            val (e, D) = ccExp E.basis (e, D)
+        in
+            Ds.exp D (x, n, t, e)
+        end
+
+fun cloconv ds =
+    let
+        val D = foldl ccDecl Ds.empty ds
+    in
+        Ds.decls D
+    end
+
+end
diff --git a/src/compiler.sig b/src/compiler.sig
index 3e6ed1a3..7faa85de 100644
--- a/src/compiler.sig
+++ b/src/compiler.sig
@@ -35,6 +35,7 @@ signature COMPILER = sig
     val reduce : ElabEnv.env -> CoreEnv.env -> string -> Core.file option
     val shake : ElabEnv.env -> CoreEnv.env -> string -> Core.file option
     val monoize : ElabEnv.env -> CoreEnv.env -> string -> Mono.file option
+    val cloconv : ElabEnv.env -> CoreEnv.env -> string -> Flat.file option
 
     val testParse : string -> unit
     val testElaborate : string -> unit
@@ -42,5 +43,6 @@ signature COMPILER = sig
     val testReduce : string -> unit
     val testShake : string -> unit
     val testMonoize : string -> unit
+    val testCloconv : string -> unit
 
 end
diff --git a/src/compiler.sml b/src/compiler.sml
index 20eb3ef5..26ff6e2b 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -103,6 +103,15 @@ fun monoize eenv cenv filename =
         else
             SOME (Monoize.monoize cenv file)
 
+fun cloconv eenv cenv filename =
+    case monoize eenv cenv filename of
+        NONE => NONE
+      | SOME file =>
+        if ErrorMsg.anyErrors () then
+            NONE
+        else
+            SOME (Cloconv.cloconv file)
+
 fun testParse filename =
     case parse filename of
         NONE => print "Failed\n"
@@ -155,4 +164,13 @@ fun testMonoize filename =
     handle MonoEnv.UnboundNamed n =>
            print ("Unbound named " ^ Int.toString n ^ "\n")
 
+fun testCloconv filename =
+    (case cloconv ElabEnv.basis CoreEnv.basis filename of
+         NONE => print "Failed\n"
+       | SOME file =>
+         (Print.print (FlatPrint.p_file FlatEnv.basis file);
+          print "\n"))
+    handle FlatEnv.UnboundNamed n =>
+           print ("Unbound named " ^ Int.toString n ^ "\n")
+
 end
diff --git a/src/core.sml b/src/core.sml
index 20b1bba8..ca64959e 100644
--- a/src/core.sml
+++ b/src/core.sml
@@ -59,7 +59,7 @@ datatype exp' =
        | ERel of int
        | ENamed of int
        | EApp of exp * exp
-       | EAbs of string * con * exp
+       | EAbs of string * con * con * exp
        | ECApp of exp * con
        | ECAbs of string * kind * exp
 
diff --git a/src/core_print.sml b/src/core_print.sml
index 02aeba69..5b020d84 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -155,17 +155,17 @@ fun p_exp' par env (e, _) =
       | EApp (e1, e2) => parenIf par (box [p_exp env e1,
                                            space,
                                            p_exp' true env e2])
-      | EAbs (x, t, e) => parenIf par (box [string "fn",
-                                            space,
-                                            string x,
-                                            space,
-                                            string ":",
-                                            space,
-                                            p_con env t,
-                                            space,
-                                            string "=>",
-                                            space,
-                                            p_exp (E.pushERel env x t) e])
+      | EAbs (x, t, _, e) => parenIf par (box [string "fn",
+                                               space,
+                                               string x,
+                                               space,
+                                               string ":",
+                                               space,
+                                               p_con env t,
+                                               space,
+                                               string "=>",
+                                               space,
+                                               p_exp (E.pushERel env x t) e])
       | ECApp (e, c) => parenIf par (box [p_exp env e,
                                           space,
                                           string "[",
diff --git a/src/core_util.sml b/src/core_util.sml
index 549f7d1f..a9d022b6 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -222,12 +222,14 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
                          S.map2 (mfe ctx e2,
                               fn e2' =>
                                  (EApp (e1', e2'), loc)))
-              | EAbs (x, t, e) =>
-                S.bind2 (mfc ctx t,
-                      fn t' =>
-                         S.map2 (mfe (bind (ctx, RelE (x, t))) e,
-                              fn e' =>
-                                 (EAbs (x, t', e'), loc)))
+              | EAbs (x, dom, ran, e) =>
+                S.bind2 (mfc ctx dom,
+                      fn dom' =>
+                         S.bind2 (mfc ctx ran,
+                               fn ran' =>
+                                  S.map2 (mfe (bind (ctx, RelE (x, dom'))) e,
+                                       fn e' =>
+                                          (EAbs (x, dom', ran', e'), loc))))
 
               | ECApp (e, c) =>
                 S.bind2 (mfe ctx e,
diff --git a/src/corify.sml b/src/corify.sml
index 12972163..42fcfe81 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -68,7 +68,7 @@ fun corifyExp (e, loc) =
       | L.ERel n => (L'.ERel n, loc)
       | L.ENamed n => (L'.ENamed n, loc)
       | L.EApp (e1, e2) => (L'.EApp (corifyExp e1, corifyExp e2), loc)
-      | L.EAbs (x, t, e1) => (L'.EAbs (x, corifyCon t, corifyExp e1), 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)
 
diff --git a/src/elab.sml b/src/elab.sml
index fc6ca366..aac5eddb 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -69,7 +69,7 @@ datatype exp' =
        | ERel of int
        | ENamed of int
        | EApp of exp * exp
-       | EAbs of string * con * exp
+       | EAbs of string * con * con * exp
        | ECApp of exp * con
        | ECAbs of explicitness * string * kind * exp
 
diff --git a/src/elab_print.sml b/src/elab_print.sml
index c8e37e48..0611730c 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -170,17 +170,17 @@ fun p_exp' par env (e, _) =
       | EApp (e1, e2) => parenIf par (box [p_exp env e1,
                                            space,
                                            p_exp' true env e2])
-      | EAbs (x, t, e) => parenIf par (box [string "fn",
-                                            space,
-                                            string x,
-                                            space,
-                                            string ":",
-                                            space,
-                                            p_con env t,
-                                            space,
-                                            string "=>",
-                                            space,
-                                            p_exp (E.pushERel env x t) e])
+      | EAbs (x, t, _, e) => parenIf par (box [string "fn",
+                                               space,
+                                               string x,
+                                               space,
+                                               string ":",
+                                               space,
+                                               p_con env t,
+                                               space,
+                                               string "=>",
+                                               space,
+                                               p_exp (E.pushERel env x t) e])
       | ECApp (e, c) => parenIf par (box [p_exp env e,
                                           space,
                                           string "[",
diff --git a/src/elab_util.sml b/src/elab_util.sml
index db444f82..1f204dce 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -214,13 +214,15 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
                          S.map2 (mfe ctx e2,
                               fn e2' =>
                                  (EApp (e1', e2'), loc)))
-              | EAbs (x, t, e) =>
-                S.bind2 (mfc ctx t,
-                      fn t' =>
-                         S.map2 (mfe (bind (ctx, RelE (x, t))) e,
-                              fn e' =>
-                                 (EAbs (x, t', e'), loc)))
-
+              | EAbs (x, dom, ran, e) =>
+                S.bind2 (mfc ctx dom,
+                      fn dom' =>
+                         S.bind2 (mfc ctx ran,
+                                  fn ran' =>
+                                     S.map2 (mfe (bind (ctx, RelE (x, dom'))) e,
+                                          fn e' =>
+                                             (EAbs (x, dom', ran', e'), loc))))
+                         
               | ECApp (e, c) =>
                 S.bind2 (mfe ctx e,
                       fn e' =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 9e63ecea..c89bc8e0 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -697,7 +697,7 @@ fun typeof env (e, loc) =
         (case #1 (typeof env e1) of
              L'.TFun (_, c) => c
            | _ => raise Fail "typeof: Bad EApp")
-      | L'.EAbs (x, t, e1) => (L'.TFun (t, typeof (E.pushERel env x t) e1), loc)
+      | L'.EAbs (_, _, ran, _) => ran
       | L'.ECApp (e1, c) =>
         (case #1 (typeof env e1) of
              L'.TCFun (_, _, _, c1) => subConInCon (0, c) c1
@@ -771,7 +771,7 @@ fun elabExp env (e, loc) =
                          end
             val (e', et) = elabExp (E.pushERel env x t') e
         in
-            ((L'.EAbs (x, t', e'), loc),
+            ((L'.EAbs (x, t', et, e'), loc),
              (L'.TFun (t', et), loc))
         end
       | L.ECApp (e, c) =>
diff --git a/src/flat.sml b/src/flat.sml
new file mode 100644
index 00000000..543cd42f
--- /dev/null
+++ b/src/flat.sml
@@ -0,0 +1,62 @@
+(* 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.
+ *)
+
+structure Flat = struct
+
+type 'a located = 'a ErrorMsg.located
+
+datatype typ' =
+         TFun of typ * typ
+       | TCode of typ * typ
+       | TRecord of (string * typ) list
+       | TNamed of int
+
+withtype typ = typ' located
+
+datatype exp' =
+         EPrim of Prim.t
+       | ERel of int
+       | ENamed of int
+       | ECode of int
+       | EApp of exp * exp
+
+       | ERecord of (string * exp) list
+       | EField of exp * string
+
+       | ELet of (string * exp) list * exp
+
+withtype exp = exp' located
+
+datatype decl' =
+         DVal of string * int * typ * exp
+       | DFun of int * string * typ * typ * exp
+
+withtype decl = decl' located
+
+type file = decl list
+
+end
diff --git a/src/flat_env.sig b/src/flat_env.sig
new file mode 100644
index 00000000..30349c5b
--- /dev/null
+++ b/src/flat_env.sig
@@ -0,0 +1,54 @@
+(* 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.
+ *)
+
+signature FLAT_ENV = sig
+
+    type env
+
+    val empty : env
+    val basis : env
+
+    exception UnboundRel of int
+    exception UnboundNamed of int
+    exception UnboundF of int
+
+    val pushTNamed : env -> string -> int -> Flat.typ option -> env
+    val lookupTNamed : env -> int -> string * Flat.typ option
+
+    val pushERel : env -> string -> Flat.typ -> env
+    val lookupERel : env -> int -> string * Flat.typ
+    val listERels : env -> (string * Flat.typ) list
+
+    val pushENamed : env -> string -> int -> Flat.typ -> env
+    val lookupENamed : env -> int -> string * Flat.typ
+
+    val pushF : env -> int -> string -> Flat.typ -> Flat.typ -> env
+    val lookupF : env -> int -> string * Flat.typ * Flat.typ
+
+    val declBinds : env -> Flat.decl -> env
+                                                 
+end
diff --git a/src/flat_env.sml b/src/flat_env.sml
new file mode 100644
index 00000000..d09f0623
--- /dev/null
+++ b/src/flat_env.sml
@@ -0,0 +1,126 @@
+(* 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.
+ *)
+
+structure FlatEnv :> FLAT_ENV = struct
+
+open Flat
+
+structure IM = IntBinaryMap
+
+
+exception UnboundRel of int
+exception UnboundNamed of int
+exception UnboundF of int
+
+type env = {
+     namedT : (string * typ option) IM.map,
+
+     relE : (string * typ) list,
+     namedE : (string * typ) IM.map,
+
+     F : (string * typ * typ) IM.map
+}
+
+val empty = {
+    namedT = IM.empty,
+
+    relE = [],
+    namedE = IM.empty,
+
+    F = IM.empty
+}
+
+fun pushTNamed (env : env) x n co =
+    {namedT = IM.insert (#namedT env, n, (x, co)),
+
+     relE = #relE env,
+     namedE = #namedE env,
+
+     F = #F env}
+
+fun lookupTNamed (env : env) n =
+    case IM.find (#namedT env, n) of
+        NONE => raise UnboundNamed n
+      | SOME x => x
+
+fun pushERel (env : env) x t =
+    {namedT = #namedT env,
+
+     relE = (x, t) :: #relE env,
+     namedE = #namedE env,
+
+     F = #F env}
+
+fun lookupERel (env : env) n =
+    (List.nth (#relE env, n))
+    handle Subscript => raise UnboundRel n
+
+fun listERels (env : env) = #relE env
+
+fun pushENamed (env : env) x n t =
+    {namedT = #namedT env,
+
+     relE = #relE env,
+     namedE = IM.insert (#namedE env, n, (x, t)),
+
+     F = #F env}
+
+fun lookupENamed (env : env) n =
+    case IM.find (#namedE env, n) of
+        NONE => raise UnboundNamed n
+      | SOME x => x
+
+fun pushF (env : env) n x dom ran =
+    {namedT = #namedT env,
+
+     relE = #relE env,
+     namedE = #namedE env,
+
+     F = IM.insert (#F env, n, (x, dom, ran))}
+
+fun lookupF (env : env) n =
+    case IM.find (#F env, n) of
+        NONE => raise UnboundF n
+      | SOME x => x
+
+fun declBinds env (d, _) =
+    case d of
+        DVal (x, n, t, _) => pushENamed env x n t
+      | DFun (n, x, dom, ran, _) => pushF env n x dom ran
+
+fun bbind env x =
+    case ElabEnv.lookupC ElabEnv.basis x of
+        ElabEnv.NotBound => raise Fail "FlatEnv.bbind: Not bound"
+      | ElabEnv.Rel _ => raise Fail "FlatEnv.bbind: Rel"
+      | ElabEnv.Named (n, _) => pushTNamed env x n NONE
+
+val basis = empty
+val basis = bbind basis "int"
+val basis = bbind basis "float"
+val basis = bbind basis "string"
+
+end
diff --git a/src/flat_print.sig b/src/flat_print.sig
new file mode 100644
index 00000000..1271e811
--- /dev/null
+++ b/src/flat_print.sig
@@ -0,0 +1,38 @@
+(* 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.
+ *)
+
+(* Pretty-printing Laconic/Web flat-code language *)
+
+signature FLAT_PRINT = sig
+    val p_typ : FlatEnv.env -> Flat.typ Print.printer
+    val p_exp : FlatEnv.env -> Flat.exp Print.printer
+    val p_decl : FlatEnv.env -> Flat.decl Print.printer
+    val p_file : FlatEnv.env -> Flat.file Print.printer
+
+    val debug : bool ref
+end
+
diff --git a/src/flat_print.sml b/src/flat_print.sml
new file mode 100644
index 00000000..c3aedde5
--- /dev/null
+++ b/src/flat_print.sml
@@ -0,0 +1,197 @@
+(* 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.
+ *)
+
+(* Pretty-printing flat-code Laconic/Web *)
+
+structure FlatPrint :> FLAT_PRINT = struct
+
+open Print.PD
+open Print
+
+open Flat
+
+structure E = FlatEnv
+
+val debug = ref false
+
+val dummyTyp = (TNamed 0, ErrorMsg.dummySpan)
+
+fun p_typ' par env (t, _) =
+    case t of
+        TFun (t1, t2) => parenIf par (box [p_typ' true env t1,
+                                           space,
+                                           string "->",
+                                           space,
+                                           p_typ env t2])
+      | TCode (t1, t2) => parenIf par (box [p_typ' true env t1,
+                                            space,
+                                            string "-->",
+                                            space,
+                                            p_typ env t2])
+      | TRecord xcs => box [string "{",
+                            p_list (fn (x, t) =>
+                                       box [string x,
+                                            space,
+                                            string ":",
+                                            space,
+                                            p_typ env t]) xcs,
+                            string "}"]
+      | TNamed n =>
+        if !debug then
+            string (#1 (E.lookupTNamed env n) ^ "__" ^ Int.toString n)
+        else
+            string (#1 (E.lookupTNamed env n))
+
+and p_typ env = p_typ' false env
+
+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)))
+         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))
+      | ECode n => string ("code$" ^ Int.toString n)
+      | EApp (e1, e2) => parenIf par (box [p_exp env e1,
+                                           space,
+                                           p_exp' true env e2])
+
+      | ERecord xes => box [string "{",
+                            p_list (fn (x, e) =>
+                                       box [string x,
+                                            space,
+                                            string "=",
+                                            space,
+                                            p_exp env e]) xes,
+                            string "}"]
+      | EField (e, x) =>
+        box [p_exp' true env e,
+             string ".",
+             string x]
+
+      | ELet (xes, e) =>
+        let
+            val (env, pps) = foldl (fn ((x, e), (env, pps)) =>
+                                       (E.pushERel env x dummyTyp,
+                                        List.revAppend ([space,
+                                                        string "val",
+                                                        space,
+                                                        string x,
+                                                        space,
+                                                        string "=",
+                                                        space,
+                                                        p_exp env e],
+                                                        pps)))
+                                   (env, []) xes
+        in
+            box [string "let",
+                 space,
+                 box (rev pps),
+                 space,
+                 string "in",
+                 space,
+                 p_exp env e,
+                 space,
+                 string "end"]
+        end
+
+and p_exp env = p_exp' false env
+
+fun p_decl env ((d, _) : decl) =
+    case d of
+        DVal (x, n, t, e) =>
+        let
+            val xp = if !debug then
+                         box [string x,
+                              string "__",
+                              string (Int.toString n)]
+                     else
+                         string x        
+        in
+            box [string "val",
+                 space,
+                 xp,
+                 space,
+                 string ":",
+                 space,
+                 p_typ env t,
+                 space,
+                 string "=",
+                 space,
+                 p_exp env e]
+
+        end
+      | DFun (n, x, dom, ran, e) =>
+        let
+            val xp = if !debug then
+                         box [string x,
+                              string "__",
+                              string (Int.toString n)]
+                     else
+                         string x        
+        in
+            box [string "fun",
+                 space,
+                 string "code$",
+                 string (Int.toString n),
+                 space,
+                 string "(",
+                 xp,
+                 space,
+                 string ":",
+                 space,
+                 p_typ env dom,
+                 string ")",
+                 space,
+                 string ":",
+                 space,
+                 p_typ env ran,
+                 space,
+                 string "=",
+                 space,
+                 p_exp (E.pushERel env x dom) e]
+
+        end
+
+fun p_file env file =
+    let
+        val (_, pds) = ListUtil.mapfoldl (fn (d, env) =>
+                                             (E.declBinds env d,
+                                              p_decl env d))
+                             env file
+    in
+        p_list_sep newline (fn x => x) pds
+    end
+
+end
diff --git a/src/flat_util.sig b/src/flat_util.sig
new file mode 100644
index 00000000..4e77f3c7
--- /dev/null
+++ b/src/flat_util.sig
@@ -0,0 +1,122 @@
+(* 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.
+ *)
+
+signature FLAT_UTIL = sig
+
+structure Typ : sig
+    val mapfold : (Flat.typ', 'state, 'abort) Search.mapfolder
+                  -> (Flat.typ, 'state, 'abort) Search.mapfolder
+
+    val map : (Flat.typ' -> Flat.typ')
+              -> Flat.typ -> Flat.typ
+
+    val fold : (Flat.typ' * 'state -> 'state)
+              -> 'state -> Flat.typ -> 'state
+
+    val exists : (Flat.typ' -> bool) -> Flat.typ -> bool
+end
+
+structure Exp : sig
+    datatype binder =
+             NamedT of string * int * Flat.typ option
+           | RelE of string * Flat.typ
+           | NamedE of string * int * Flat.typ * Flat.exp option
+
+    val mapfoldB : {typ : (Flat.typ', 'state, 'abort) Search.mapfolder,
+                    exp : ('typtext, Flat.exp', 'state, 'abort) Search.mapfolderB,
+                    bind : 'typtext * binder -> 'typtext}
+                   -> ('typtext, Flat.exp, 'state, 'abort) Search.mapfolderB
+    val mapfold : {typ : (Flat.typ', 'state, 'abort) Search.mapfolder,
+                   exp : (Flat.exp', 'state, 'abort) Search.mapfolder}
+                  -> (Flat.exp, 'state, 'abort) Search.mapfolder
+
+    val map : {typ : Flat.typ' -> Flat.typ',
+               exp : Flat.exp' -> Flat.exp'}
+              -> Flat.exp -> Flat.exp
+    val mapB : {typ : Flat.typ' -> Flat.typ',
+                exp : 'typtext -> Flat.exp' -> Flat.exp',
+                bind : 'typtext * binder -> 'typtext}
+               -> 'typtext -> (Flat.exp -> Flat.exp)
+
+    val fold : {typ : Flat.typ' * 'state -> 'state,
+                exp : Flat.exp' * 'state -> 'state}
+               -> 'state -> Flat.exp -> 'state
+                                        
+    val exists : {typ : Flat.typ' -> bool,
+                  exp : Flat.exp' -> bool} -> Flat.exp -> bool
+end
+
+structure Decl : sig
+    datatype binder = datatype Exp.binder
+
+    val mapfoldB : {typ : (Flat.typ', 'state, 'abort) Search.mapfolder,
+                    exp : ('typtext, Flat.exp', 'state, 'abort) Search.mapfolderB,
+                    decl : ('typtext, Flat.decl', 'state, 'abort) Search.mapfolderB,
+                    bind : 'typtext * binder -> 'typtext}
+                   -> ('typtext, Flat.decl, 'state, 'abort) Search.mapfolderB
+    val mapfold : {typ : (Flat.typ', 'state, 'abort) Search.mapfolder,
+                   exp : (Flat.exp', 'state, 'abort) Search.mapfolder,
+                   decl : (Flat.decl', 'state, 'abort) Search.mapfolder}
+                  -> (Flat.decl, 'state, 'abort) Search.mapfolder
+
+    val fold : {typ : Flat.typ' * 'state -> 'state,
+                exp : Flat.exp' * 'state -> 'state,
+                decl : Flat.decl' * 'state -> 'state}
+               -> 'state -> Flat.decl -> 'state
+end
+
+structure File : sig
+    datatype binder =
+             NamedT of string * int * Flat.typ option
+           | RelE of string * Flat.typ
+           | NamedE of string * int * Flat.typ * Flat.exp option
+           | F of int * string * Flat.typ * Flat.typ * Flat.exp
+
+    val mapfoldB : {typ : (Flat.typ', 'state, 'abort) Search.mapfolder,
+                    exp : ('typtext, Flat.exp', 'state, 'abort) Search.mapfolderB,
+                    decl : ('typtext, Flat.decl', 'state, 'abort) Search.mapfolderB,
+                    bind : 'typtext * binder -> 'typtext}
+                   -> ('typtext, Flat.file, 'state, 'abort) Search.mapfolderB
+
+    val mapfold : {typ : (Flat.typ', 'state, 'abort) Search.mapfolder,
+                   exp : (Flat.exp', 'state, 'abort) Search.mapfolder,
+                   decl : (Flat.decl', 'state, 'abort) Search.mapfolder}
+                  -> (Flat.file, 'state, 'abort) Search.mapfolder
+
+    val mapB : {typ : Flat.typ' -> Flat.typ',
+                exp : 'typtext -> Flat.exp' -> Flat.exp',
+                decl : 'typtext -> Flat.decl' -> Flat.decl',
+                bind : 'typtext * binder -> 'typtext}
+               -> 'typtext -> Flat.file -> Flat.file
+
+    val fold : {typ : Flat.typ' * 'state -> 'state,
+                exp : Flat.exp' * 'state -> 'state,
+                decl : Flat.decl' * 'state -> 'state}
+               -> 'state -> Flat.file -> 'state
+end
+
+end
diff --git a/src/flat_util.sml b/src/flat_util.sml
new file mode 100644
index 00000000..89e6f143
--- /dev/null
+++ b/src/flat_util.sml
@@ -0,0 +1,286 @@
+(* 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.
+ *)
+
+structure FlatUtil :> FLAT_UTIL = struct
+
+open Flat
+
+structure S = Search
+
+structure Typ = struct
+
+fun mapfold fc =
+    let
+        fun mft c acc =
+            S.bindP (mft' c acc, fc)
+
+        and mft' (cAll as (c, loc)) =
+            case c of
+                TFun (t1, t2) =>
+                S.bind2 (mft t1,
+                      fn t1' =>
+                         S.map2 (mft t2,
+                              fn t2' =>
+                                 (TFun (t1', t2'), loc)))
+              | TCode (t1, t2) =>
+                S.bind2 (mft t1,
+                      fn t1' =>
+                         S.map2 (mft t2,
+                              fn t2' =>
+                                 (TCode (t1', t2'), loc)))
+              | TRecord xts =>
+                S.map2 (ListUtil.mapfold (fn (x, t) =>
+                                             S.map2 (mft t,
+                                                  fn t' =>
+                                                     (x, t')))
+                                         xts,
+                     fn xts' => (TRecord xts', loc))
+              | TNamed _ => S.return2 cAll
+    in
+        mft
+    end
+
+fun map typ c =
+    case mapfold (fn c => fn () => S.Continue (typ c, ())) c () of
+        S.Return () => raise Fail "Flat_util.Typ.map"
+      | S.Continue (c, ()) => c
+
+fun fold typ s c =
+    case mapfold (fn c => fn s => S.Continue (c, typ (c, s))) c s of
+        S.Continue (_, s) => s
+      | S.Return _ => raise Fail "FlatUtil.Typ.fold: Impossible"
+
+fun exists typ k =
+    case mapfold (fn c => fn () =>
+                             if typ c then
+                                 S.Return ()
+                             else
+                                 S.Continue (c, ())) k () of
+        S.Return _ => true
+      | S.Continue _ => false
+
+end
+
+structure Exp = struct
+
+datatype binder =
+         NamedT of string * int * typ option
+       | RelE of string * typ
+       | NamedE of string * int * typ * exp option
+
+fun mapfoldB {typ = fc, exp = fe, bind} =
+    let
+        val mft = Typ.mapfold fc
+
+        fun mfe ctx e acc =
+            S.bindP (mfe' ctx e acc, fe ctx)
+
+        and mfe' ctx (eAll as (e, loc)) =
+            case e of
+                EPrim _ => S.return2 eAll
+              | ERel _ => S.return2 eAll
+              | ENamed _ => S.return2 eAll
+              | ECode _ => S.return2 eAll
+              | EApp (e1, e2) =>
+                S.bind2 (mfe ctx e1,
+                     fn e1' =>
+                        S.map2 (mfe ctx e2,
+                             fn e2' =>
+                                (EApp (e1', e2'), loc)))
+
+              | ERecord xes =>
+                S.map2 (ListUtil.mapfold (fn (x, e) =>
+                                             S.map2 (mfe ctx e,
+                                                  fn e' =>
+                                                     (x, e')))
+                                         xes,
+                     fn xes' =>
+                        (ERecord xes', loc))
+              | EField (e, x) =>
+                S.map2 (mfe ctx e,
+                      fn e' =>
+                         (EField (e', x), loc))
+
+              | ELet (xes, e) =>
+                S.bind2 (ListUtil.mapfold (fn (x, e) =>
+                                              S.map2 (mfe ctx e,
+                                                   fn e' =>
+                                                      (x, e')))
+                                          xes,
+                      fn xes' =>
+                         S.map2 (mfe ctx e,
+                                 fn e' =>
+                                    (ELet (xes', e'), loc)))
+    in
+        mfe
+    end
+
+fun mapfold {typ = fc, exp = fe} =
+    mapfoldB {typ = fc,
+              exp = fn () => fe,
+              bind = fn ((), _) => ()} ()
+
+fun mapB {typ, exp, bind} ctx e =
+    case mapfoldB {typ = fn c => fn () => S.Continue (typ c, ()),
+                   exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
+                   bind = bind} ctx e () of
+        S.Continue (e, ()) => e
+      | S.Return _ => raise Fail "FlatUtil.Exp.mapB: Impossible"
+
+fun map {typ, exp} e =
+    case mapfold {typ = fn c => fn () => S.Continue (typ c, ()),
+                  exp = fn e => fn () => S.Continue (exp e, ())} e () of
+        S.Return () => raise Fail "Flat_util.Exp.map"
+      | S.Continue (e, ()) => e
+
+fun fold {typ, exp} s e =
+    case mapfold {typ = fn c => fn s => S.Continue (c, typ (c, s)),
+                  exp = fn e => fn s => S.Continue (e, exp (e, s))} e s of
+        S.Continue (_, s) => s
+      | S.Return _ => raise Fail "FlatUtil.Exp.fold: Impossible"
+
+fun exists {typ, exp} k =
+    case mapfold {typ = fn c => fn () =>
+                                    if typ c then
+                                        S.Return ()
+                                    else
+                                        S.Continue (c, ()),
+                  exp = fn e => fn () =>
+                                    if exp e then
+                                        S.Return ()
+                                    else
+                                        S.Continue (e, ())} k () of
+        S.Return _ => true
+      | S.Continue _ => false
+
+end
+
+structure Decl = struct
+
+datatype binder = datatype Exp.binder
+
+fun mapfoldB {typ = fc, exp = fe, decl = fd, bind} =
+    let
+        val mft = Typ.mapfold fc
+
+        val mfe = Exp.mapfoldB {typ = fc, exp = fe, bind = bind}
+
+        fun mfd ctx d acc =
+            S.bindP (mfd' ctx d acc, fd ctx)
+
+        and mfd' ctx (dAll as (d, loc)) =
+            case d of
+                DVal (x, n, t, e) =>
+                S.bind2 (mft t,
+                      fn t' =>
+                         S.map2 (mfe ctx e,
+                              fn e' =>
+                                 (DVal (x, n, t', e'), loc)))
+              | DFun (n, x, dom, ran, e) =>
+                S.bind2 (mft dom,
+                      fn dom' =>
+                         S.bind2 (mft ran,
+                               fn ran' =>
+                                  S.map2 (mfe ctx e,
+                                       fn e' =>
+                                          (DFun (n, x, dom', ran', e'), loc))))
+    in
+        mfd
+    end    
+
+fun mapfold {typ = fc, exp = fe, decl = fd} =
+    mapfoldB {typ = fc,
+              exp = fn () => fe,
+              decl = fn () => fd,
+              bind = fn ((), _) => ()} ()
+
+fun fold {typ, exp, decl} s d =
+    case mapfold {typ = fn c => fn s => S.Continue (c, typ (c, s)),
+                  exp = fn e => fn s => S.Continue (e, exp (e, s)),
+                  decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of
+        S.Continue (_, s) => s
+      | S.Return _ => raise Fail "FlatUtil.Decl.fold: Impossible"
+
+end
+
+structure File = struct
+
+datatype binder =
+         NamedT of string * int * typ option
+       | RelE of string * typ
+       | NamedE of string * int * typ * exp option
+       | F of int * string * Flat.typ * Flat.typ * Flat.exp
+
+fun mapfoldB (all as {bind, ...}) =
+    let
+        val mfd = Decl.mapfoldB all
+
+        fun mff ctx ds =
+            case ds of
+                nil => S.return2 nil
+              | d :: ds' =>
+                S.bind2 (mfd ctx d,
+                         fn d' =>
+                            let
+                                val b =
+                                    case #1 d' of
+                                        DVal (x, n, t, e) => NamedE (x, n, t, SOME e)
+                                      | DFun v => F v
+                                val ctx' = bind (ctx, b)
+                            in
+                                S.map2 (mff ctx' ds',
+                                     fn ds' =>
+                                        d' :: ds')
+                            end)
+    in
+        mff
+    end
+
+fun mapfold {typ = fc, exp = fe, decl = fd} =
+    mapfoldB {typ = fc,
+              exp = fn () => fe,
+              decl = fn () => fd,
+              bind = fn ((), _) => ()} ()
+
+fun mapB {typ, exp, decl, bind} ctx ds =
+    case mapfoldB {typ = fn c => fn () => S.Continue (typ c, ()),
+                   exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
+                   decl = fn ctx => fn d => fn () => S.Continue (decl ctx d, ()),
+                   bind = bind} ctx ds () of
+        S.Continue (ds, ()) => ds
+      | S.Return _ => raise Fail "FlatUtil.File.mapB: Impossible"
+
+fun fold {typ, exp, decl} s d =
+    case mapfold {typ = fn c => fn s => S.Continue (c, typ (c, s)),
+                  exp = fn e => fn s => S.Continue (e, exp (e, s)),
+                  decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of
+        S.Continue (_, s) => s
+      | S.Return _ => raise Fail "FlatUtil.File.fold: Impossible"
+
+end
+
+end
diff --git a/src/list_util.sig b/src/list_util.sig
index 18d348ef..8185a28b 100644
--- a/src/list_util.sig
+++ b/src/list_util.sig
@@ -33,6 +33,8 @@ signature LIST_UTIL = sig
     val mapfold : ('data, 'state, 'abort) Search.mapfolder
                   -> ('data list, 'state, 'abort) Search.mapfolder
 
+    val foldlMap : ('data1 * 'state -> 'data2 * 'state) -> 'state -> 'data1 list -> 'data2 list * 'state
+
     val search : ('a -> 'b option) -> 'a list -> 'b option
 
 end
diff --git a/src/list_util.sml b/src/list_util.sml
index 626d0ec0..aed2cdf0 100644
--- a/src/list_util.sml
+++ b/src/list_util.sml
@@ -60,6 +60,21 @@ fun mapfold f =
         mf
     end
 
+fun foldlMap 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 (h' :: ls', s') t
+                end
+    in
+        fm ([], s)
+    end
+
 fun search f =
     let
         fun s ls =
diff --git a/src/mono.sml b/src/mono.sml
index 7a4b54ee..a23ec958 100644
--- a/src/mono.sml
+++ b/src/mono.sml
@@ -41,7 +41,7 @@ datatype exp' =
        | ERel of int
        | ENamed of int
        | EApp of exp * exp
-       | EAbs of string * typ * exp
+       | EAbs of string * typ * typ * exp
 
        | ERecord of (string * exp) list
        | EField of exp * string
diff --git a/src/mono_print.sml b/src/mono_print.sml
index a23296f9..b8b73e17 100644
--- a/src/mono_print.sml
+++ b/src/mono_print.sml
@@ -77,17 +77,17 @@ fun p_exp' par env (e, _) =
       | EApp (e1, e2) => parenIf par (box [p_exp env e1,
                                            space,
                                            p_exp' true env e2])
-      | EAbs (x, t, e) => parenIf par (box [string "fn",
-                                            space,
-                                            string x,
-                                            space,
-                                            string ":",
-                                            space,
-                                            p_typ env t,
-                                            space,
-                                            string "=>",
-                                            space,
-                                            p_exp (E.pushERel env x t) e])
+      | EAbs (x, t, _, e) => parenIf par (box [string "fn",
+                                               space,
+                                               string x,
+                                               space,
+                                               string ":",
+                                               space,
+                                               p_typ env t,
+                                               space,
+                                               string "=>",
+                                               space,
+                                               p_exp (E.pushERel env x t) e])
 
       | ERecord xes => box [string "{",
                             p_list (fn (x, e) =>
diff --git a/src/mono_util.sig b/src/mono_util.sig
new file mode 100644
index 00000000..750a4d3c
--- /dev/null
+++ b/src/mono_util.sig
@@ -0,0 +1,118 @@
+(* 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.
+ *)
+
+signature MONO_UTIL = sig
+
+structure Typ : sig
+    val mapfold : (Mono.typ', 'state, 'abort) Search.mapfolder
+                  -> (Mono.typ, 'state, 'abort) Search.mapfolder
+
+    val map : (Mono.typ' -> Mono.typ')
+              -> Mono.typ -> Mono.typ
+
+    val fold : (Mono.typ' * 'state -> 'state)
+              -> 'state -> Mono.typ -> 'state
+
+    val exists : (Mono.typ' -> bool) -> Mono.typ -> bool
+end
+
+structure Exp : sig
+    datatype binder =
+             NamedT of string * int * Mono.typ option
+           | RelE of string * Mono.typ
+           | NamedE of string * int * Mono.typ * Mono.exp option
+
+    val mapfoldB : {typ : (Mono.typ', 'state, 'abort) Search.mapfolder,
+                    exp : ('typtext, Mono.exp', 'state, 'abort) Search.mapfolderB,
+                    bind : 'typtext * binder -> 'typtext}
+                   -> ('typtext, Mono.exp, 'state, 'abort) Search.mapfolderB
+    val mapfold : {typ : (Mono.typ', 'state, 'abort) Search.mapfolder,
+                   exp : (Mono.exp', 'state, 'abort) Search.mapfolder}
+                  -> (Mono.exp, 'state, 'abort) Search.mapfolder
+
+    val map : {typ : Mono.typ' -> Mono.typ',
+               exp : Mono.exp' -> Mono.exp'}
+              -> Mono.exp -> Mono.exp
+    val mapB : {typ : Mono.typ' -> Mono.typ',
+                exp : 'typtext -> Mono.exp' -> Mono.exp',
+                bind : 'typtext * binder -> 'typtext}
+               -> 'typtext -> (Mono.exp -> Mono.exp)
+
+    val fold : {typ : Mono.typ' * 'state -> 'state,
+                exp : Mono.exp' * 'state -> 'state}
+               -> 'state -> Mono.exp -> 'state
+                                        
+    val exists : {typ : Mono.typ' -> bool,
+                  exp : Mono.exp' -> bool} -> Mono.exp -> bool
+end
+
+structure Decl : sig
+    datatype binder = datatype Exp.binder
+
+    val mapfoldB : {typ : (Mono.typ', 'state, 'abort) Search.mapfolder,
+                    exp : ('typtext, Mono.exp', 'state, 'abort) Search.mapfolderB,
+                    decl : ('typtext, Mono.decl', 'state, 'abort) Search.mapfolderB,
+                    bind : 'typtext * binder -> 'typtext}
+                   -> ('typtext, Mono.decl, 'state, 'abort) Search.mapfolderB
+    val mapfold : {typ : (Mono.typ', 'state, 'abort) Search.mapfolder,
+                   exp : (Mono.exp', 'state, 'abort) Search.mapfolder,
+                   decl : (Mono.decl', 'state, 'abort) Search.mapfolder}
+                  -> (Mono.decl, 'state, 'abort) Search.mapfolder
+
+    val fold : {typ : Mono.typ' * 'state -> 'state,
+                exp : Mono.exp' * 'state -> 'state,
+                decl : Mono.decl' * 'state -> 'state}
+               -> 'state -> Mono.decl -> 'state
+end
+
+structure File : sig
+    datatype binder = datatype Exp.binder
+
+    val mapfoldB : {typ : (Mono.typ', 'state, 'abort) Search.mapfolder,
+                    exp : ('typtext, Mono.exp', 'state, 'abort) Search.mapfolderB,
+                    decl : ('typtext, Mono.decl', 'state, 'abort) Search.mapfolderB,
+                    bind : 'typtext * binder -> 'typtext}
+                   -> ('typtext, Mono.file, 'state, 'abort) Search.mapfolderB
+
+    val mapfold : {typ : (Mono.typ', 'state, 'abort) Search.mapfolder,
+                   exp : (Mono.exp', 'state, 'abort) Search.mapfolder,
+                   decl : (Mono.decl', 'state, 'abort) Search.mapfolder}
+                  -> (Mono.file, 'state, 'abort) Search.mapfolder
+
+    val mapB : {typ : Mono.typ' -> Mono.typ',
+                exp : 'typtext -> Mono.exp' -> Mono.exp',
+                decl : 'typtext -> Mono.decl' -> Mono.decl',
+                bind : 'typtext * binder -> 'typtext}
+               -> 'typtext -> Mono.file -> Mono.file
+
+    val fold : {typ : Mono.typ' * 'state -> 'state,
+                exp : Mono.exp' * 'state -> 'state,
+                decl : Mono.decl' * 'state -> 'state}
+               -> 'state -> Mono.file -> 'state
+end
+
+end
diff --git a/src/mono_util.sml b/src/mono_util.sml
new file mode 100644
index 00000000..8decf033
--- /dev/null
+++ b/src/mono_util.sml
@@ -0,0 +1,263 @@
+(* 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.
+ *)
+
+structure MonoUtil :> MONO_UTIL = struct
+
+open Mono
+
+structure S = Search
+
+structure Typ = struct
+
+fun mapfold fc =
+    let
+        fun mft c acc =
+            S.bindP (mft' c acc, fc)
+
+        and mft' (cAll as (c, loc)) =
+            case c of
+                TFun (t1, t2) =>
+                S.bind2 (mft t1,
+                      fn t1' =>
+                         S.map2 (mft t2,
+                              fn t2' =>
+                                 (TFun (t1', t2'), loc)))
+              | TRecord xts =>
+                S.map2 (ListUtil.mapfold (fn (x, t) =>
+                                             S.map2 (mft t,
+                                                  fn t' =>
+                                                     (x, t')))
+                                         xts,
+                     fn xts' => (TRecord xts', loc))
+              | TNamed _ => S.return2 cAll
+    in
+        mft
+    end
+
+fun map typ c =
+    case mapfold (fn c => fn () => S.Continue (typ c, ())) c () of
+        S.Return () => raise Fail "Mono_util.Typ.map"
+      | S.Continue (c, ()) => c
+
+fun fold typ s c =
+    case mapfold (fn c => fn s => S.Continue (c, typ (c, s))) c s of
+        S.Continue (_, s) => s
+      | S.Return _ => raise Fail "MonoUtil.Typ.fold: Impossible"
+
+fun exists typ k =
+    case mapfold (fn c => fn () =>
+                             if typ c then
+                                 S.Return ()
+                             else
+                                 S.Continue (c, ())) k () of
+        S.Return _ => true
+      | S.Continue _ => false
+
+end
+
+structure Exp = struct
+
+datatype binder =
+         NamedT of string * int * typ option
+       | RelE of string * typ
+       | NamedE of string * int * typ * exp option
+
+fun mapfoldB {typ = fc, exp = fe, bind} =
+    let
+        val mft = Typ.mapfold fc
+
+        fun mfe ctx e acc =
+            S.bindP (mfe' ctx e acc, fe ctx)
+
+        and mfe' ctx (eAll as (e, loc)) =
+            case e of
+                EPrim _ => S.return2 eAll
+              | ERel _ => S.return2 eAll
+              | ENamed _ => S.return2 eAll
+              | EApp (e1, e2) =>
+                S.bind2 (mfe ctx e1,
+                      fn e1' =>
+                         S.map2 (mfe ctx e2,
+                              fn e2' =>
+                                 (EApp (e1', e2'), loc)))
+              | EAbs (x, dom, ran, e) =>
+                S.bind2 (mft dom,
+                      fn dom' =>
+                         S.bind2 (mft ran,
+                               fn ran' =>
+                                  S.map2 (mfe (bind (ctx, RelE (x, dom'))) e,
+                                       fn e' =>
+                                          (EAbs (x, dom', ran', e'), loc))))
+
+              | ERecord xes =>
+                S.map2 (ListUtil.mapfold (fn (x, e) =>
+                                             S.map2 (mfe ctx e,
+                                                  fn e' =>
+                                                     (x, e')))
+                                         xes,
+                     fn xes' =>
+                        (ERecord xes', loc))
+              | EField (e, x) =>
+                S.map2 (mfe ctx e,
+                      fn e' =>
+                         (EField (e', x), loc))
+    in
+        mfe
+    end
+
+fun mapfold {typ = fc, exp = fe} =
+    mapfoldB {typ = fc,
+              exp = fn () => fe,
+              bind = fn ((), _) => ()} ()
+
+fun mapB {typ, exp, bind} ctx e =
+    case mapfoldB {typ = fn c => fn () => S.Continue (typ c, ()),
+                   exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
+                   bind = bind} ctx e () of
+        S.Continue (e, ()) => e
+      | S.Return _ => raise Fail "MonoUtil.Exp.mapB: Impossible"
+
+fun map {typ, exp} e =
+    case mapfold {typ = fn c => fn () => S.Continue (typ c, ()),
+                  exp = fn e => fn () => S.Continue (exp e, ())} e () of
+        S.Return () => raise Fail "Mono_util.Exp.map"
+      | S.Continue (e, ()) => e
+
+fun fold {typ, exp} s e =
+    case mapfold {typ = fn c => fn s => S.Continue (c, typ (c, s)),
+                  exp = fn e => fn s => S.Continue (e, exp (e, s))} e s of
+        S.Continue (_, s) => s
+      | S.Return _ => raise Fail "MonoUtil.Exp.fold: Impossible"
+
+fun exists {typ, exp} k =
+    case mapfold {typ = fn c => fn () =>
+                                    if typ c then
+                                        S.Return ()
+                                    else
+                                        S.Continue (c, ()),
+                  exp = fn e => fn () =>
+                                    if exp e then
+                                        S.Return ()
+                                    else
+                                        S.Continue (e, ())} k () of
+        S.Return _ => true
+      | S.Continue _ => false
+
+end
+
+structure Decl = struct
+
+datatype binder = datatype Exp.binder
+
+fun mapfoldB {typ = fc, exp = fe, decl = fd, bind} =
+    let
+        val mft = Typ.mapfold fc
+
+        val mfe = Exp.mapfoldB {typ = fc, exp = fe, bind = bind}
+
+        fun mfd ctx d acc =
+            S.bindP (mfd' ctx d acc, fd ctx)
+
+        and mfd' ctx (dAll as (d, loc)) =
+            case d of
+                DVal (x, n, t, e) =>
+                S.bind2 (mft t,
+                      fn t' =>
+                         S.map2 (mfe ctx e,
+                              fn e' =>
+                                 (DVal (x, n, t', e'), loc)))
+    in
+        mfd
+    end    
+
+fun mapfold {typ = fc, exp = fe, decl = fd} =
+    mapfoldB {typ = fc,
+              exp = fn () => fe,
+              decl = fn () => fd,
+              bind = fn ((), _) => ()} ()
+
+fun fold {typ, exp, decl} s d =
+    case mapfold {typ = fn c => fn s => S.Continue (c, typ (c, s)),
+                  exp = fn e => fn s => S.Continue (e, exp (e, s)),
+                  decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of
+        S.Continue (_, s) => s
+      | S.Return _ => raise Fail "MonoUtil.Decl.fold: Impossible"
+
+end
+
+structure File = struct
+
+datatype binder = datatype Exp.binder
+
+fun mapfoldB (all as {bind, ...}) =
+    let
+        val mfd = Decl.mapfoldB all
+
+        fun mff ctx ds =
+            case ds of
+                nil => S.return2 nil
+              | d :: ds' =>
+                S.bind2 (mfd ctx d,
+                         fn d' =>
+                            let
+                                val b =
+                                    case #1 d' of
+                                        DVal (x, n, t, e) => NamedE (x, n, t, SOME e)
+                                val ctx' = bind (ctx, b)
+                            in
+                                S.map2 (mff ctx' ds',
+                                     fn ds' =>
+                                        d' :: ds')
+                            end)
+    in
+        mff
+    end
+
+fun mapfold {typ = fc, exp = fe, decl = fd} =
+    mapfoldB {typ = fc,
+              exp = fn () => fe,
+              decl = fn () => fd,
+              bind = fn ((), _) => ()} ()
+
+fun mapB {typ, exp, decl, bind} ctx ds =
+    case mapfoldB {typ = fn c => fn () => S.Continue (typ c, ()),
+                   exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
+                   decl = fn ctx => fn d => fn () => S.Continue (decl ctx d, ()),
+                   bind = bind} ctx ds () of
+        S.Continue (ds, ()) => ds
+      | S.Return _ => raise Fail "MonoUtil.File.mapB: Impossible"
+
+fun fold {typ, exp, decl} s d =
+    case mapfold {typ = fn c => fn s => S.Continue (c, typ (c, s)),
+                  exp = fn e => fn s => S.Continue (e, exp (e, s)),
+                  decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of
+        S.Continue (_, s) => s
+      | S.Return _ => raise Fail "MonoUtil.File.fold: Impossible"
+
+end
+
+end
diff --git a/src/monoize.sml b/src/monoize.sml
index e72d7b1b..b38bd5c0 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -86,8 +86,8 @@ fun monoExp env (all as (e, loc)) =
           | L.ERel n => (L'.ERel n, loc)
           | L.ENamed n => (L'.ENamed n, loc)
           | L.EApp (e1, e2) => (L'.EApp (monoExp env e1, monoExp env e2), loc)
-          | L.EAbs (x, t, e) =>
-            (L'.EAbs (x, monoType env t, monoExp (Env.pushERel env x t) e), loc)
+          | L.EAbs (x, dom, ran, e) =>
+            (L'.EAbs (x, monoType env dom, monoType env ran, monoExp (Env.pushERel env x dom) e), loc)
           | L.ECApp _ => poly ()
           | L.ECAbs _ => poly ()
 
diff --git a/src/reduce.sml b/src/reduce.sml
index fd2d5b1a..d5449bac 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -139,7 +139,7 @@ fun exp env e =
              (_, _, SOME e') => #1 e'
            | _ => e)
 
-      | EApp ((EAbs (_, _, e1), loc), e2) =>
+      | EApp ((EAbs (_, _, _, e1), loc), e2) =>
         #1 (reduceExp env (subExpInExp (0, e2) e1))
       | ECApp ((ECAbs (_, _, e1), loc), c) =>
         #1 (reduceExp env (subConInExp (0, c) e1))
diff --git a/src/sources b/src/sources
index adcda7e9..83a6316c 100644
--- a/src/sources
+++ b/src/sources
@@ -60,11 +60,28 @@ mono.sml
 monoize.sig
 monoize.sml
 
+mono_util.sig
+mono_util.sml
+
 mono_env.sig
 mono_env.sml
 
 mono_print.sig
 mono_print.sml
 
+flat.sml
+
+flat_util.sig
+flat_util.sml
+
+flat_env.sig
+flat_env.sml
+
+flat_print.sig
+flat_print.sml
+
+cloconv.sig
+cloconv.sml
+
 compiler.sig
 compiler.sml
diff --git a/tests/cloconv.lac b/tests/cloconv.lac
new file mode 100644
index 00000000..3dd9ad86
--- /dev/null
+++ b/tests/cloconv.lac
@@ -0,0 +1 @@
+val main = fn x : int => x
diff --git a/tests/curry.lac b/tests/curry.lac
new file mode 100644
index 00000000..46577284
--- /dev/null
+++ b/tests/curry.lac
@@ -0,0 +1 @@
+val main = fn x : int => fn y : int => x
diff --git a/tests/curry3.lac b/tests/curry3.lac
new file mode 100644
index 00000000..fa2804cf
--- /dev/null
+++ b/tests/curry3.lac
@@ -0,0 +1 @@
+val main = fn x : int => fn y : int => fn z : int => x