changeset 249:b6b75e6e0898

Corify transaction wrappers
author Adam Chlipala <adamc@hcoop.net>
date Sun, 31 Aug 2008 09:45:23 -0400
parents d5b12daa9b47
children 98f551ddd54b
files src/corify.sml src/elaborate.sml tests/query.ur
diffstat 3 files changed, 691 insertions(+), 628 deletions(-) [+]
line wrap: on
line diff
--- a/src/corify.sml	Sun Aug 31 09:05:33 2008 -0400
+++ b/src/corify.sml	Sun Aug 31 09:45:23 2008 -0400
@@ -64,6 +64,9 @@
     val leave : t -> {outer : t, inner : t}
     val ffi : string -> L'.con SM.map -> (string * string list * L'.con option * L'.datatype_kind) SM.map -> t
 
+    val basisIs : t * int -> t
+    val lookupBasis : t -> int option
+
     datatype core_con =
              CNormal of int
            | CFfi of string
@@ -75,650 +78,673 @@
     val lookupConstructorByNameOpt : t -> string -> L'.patCon option
     val lookupConstructorByName : t -> string -> L'.patCon
     val lookupConstructorById : t -> int -> L'.patCon
+                                            
+    datatype core_val =
+             ENormal of int
+           | EFfi of string * L'.con
+    val bindVal : t -> string -> int -> t * int
+    val bindConstructorVal : t -> string -> int -> t
+    val lookupValById : t -> int -> int option
+    val lookupValByName : t -> string -> core_val
 
-     datatype core_val =
-              ENormal of int
-            | EFfi of string * L'.con
-     val bindVal : t -> string -> int -> t * int
-     val bindConstructorVal : t -> string -> int -> t
-     val lookupValById : t -> int -> int option
-     val lookupValByName : t -> string -> core_val
+    val bindStr : t -> string -> int -> t -> t
+    val lookupStrById : t -> int -> t
+    val lookupStrByName : string * t -> t
 
-     val bindStr : t -> string -> int -> t -> t
-     val lookupStrById : t -> int -> t
-     val lookupStrByName : string * t -> t
+    val bindFunctor : t -> string -> int -> string -> int -> L.str -> t
+    val lookupFunctorById : t -> int -> string * int * L.str
+    val lookupFunctorByName : string * t -> string * int * L.str
+end = struct
 
-     val bindFunctor : t -> string -> int -> string -> int -> L.str -> t
-     val lookupFunctorById : t -> int -> string * int * L.str
-     val lookupFunctorByName : string * t -> string * int * L.str
- end = struct
+datatype flattening =
+         FNormal of {cons : int SM.map,
+                     constructors : L'.patCon SM.map,
+                     vals : int SM.map,
+                     strs : flattening SM.map,
+                     funs : (string * int * L.str) SM.map}
+       | FFfi of {mod : string,
+                  vals : L'.con SM.map,
+                  constructors : (string * string list * L'.con option * L'.datatype_kind) SM.map}
 
- datatype flattening =
-          FNormal of {cons : int SM.map,
-                      constructors : L'.patCon SM.map,
-                      vals : int SM.map,
-                      strs : flattening SM.map,
-                      funs : (string * int * L.str) SM.map}
-        | FFfi of {mod : string,
-                   vals : L'.con SM.map,
-                   constructors : (string * string list * L'.con option * L'.datatype_kind) SM.map}
+type t = {
+     basis : int option,
+     cons : int IM.map,
+     constructors : L'.patCon IM.map,
+     vals : int IM.map,
+     strs : flattening IM.map,
+     funs : (string * int * L.str) IM.map,
+     current : flattening,
+     nested : flattening list
+}
 
- type t = {
-      cons : int IM.map,
-      constructors : L'.patCon IM.map,
-      vals : int IM.map,
-      strs : flattening IM.map,
-      funs : (string * int * L.str) IM.map,
-      current : flattening,
-      nested : flattening list
- }
+val empty = {
+    basis = NONE,
+    cons = IM.empty,
+    constructors = IM.empty,
+    vals = IM.empty,
+    strs = IM.empty,
+    funs = IM.empty,
+    current = FNormal { cons = SM.empty, constructors = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty },
+    nested = []
+}
 
- val empty = {
-     cons = IM.empty,
-     constructors = IM.empty,
-     vals = IM.empty,
-     strs = IM.empty,
-     funs = IM.empty,
-     current = FNormal { cons = SM.empty, constructors = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty },
-     nested = []
- }
+fun debug ({current = FNormal {cons, constructors, vals, strs, funs}, ...} : t) =
+    print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; "
+           ^ "constructors: " ^ Int.toString (SM.numItems constructors) ^ "; "
+           ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; "
+           ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; "
+           ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n")
+  | debug _ = print "Not normal!\n"
 
- fun debug ({current = FNormal {cons, constructors, vals, strs, funs}, ...} : t) =
-     print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; "
-            ^ "constructors: " ^ Int.toString (SM.numItems constructors) ^ "; "
-            ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; "
-            ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; "
-            ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n")
-   | debug _ = print "Not normal!\n"
+fun basisIs ({cons, constructors, vals, strs, funs, current, nested, ...} : t, basis) =
+    {basis = SOME basis,
+     cons = cons,
+     constructors = constructors,
+     vals = vals,
+     strs = strs,
+     funs = funs,
+     current = current,
+     nested = nested}
 
- datatype core_con =
-          CNormal of int
-        | CFfi of string
+fun lookupBasis ({basis, ...} : t) = basis
 
- datatype core_val =
-          ENormal of int
-        | EFfi of string * L'.con
+datatype core_con =
+         CNormal of int
+       | CFfi of string
 
- fun bindCon {cons, constructors, vals, strs, funs, current, nested} s n =
-     let
-         val n' = alloc ()
+datatype core_val =
+         ENormal of int
+       | EFfi of string * L'.con
 
-         val current =
-             case current of
-                 FFfi _ => raise Fail "Binding inside FFfi"
-               | FNormal {cons, constructors, vals, strs, funs} =>
-                 FNormal {cons = SM.insert (cons, s, n'),
-                          constructors = constructors,
-                          vals = vals,
-                          strs = strs,
-                          funs = funs}
-     in
-         ({cons = IM.insert (cons, n, n'),
-           constructors = constructors,
-           vals = vals,
-           strs = strs,
-           funs = funs,
-           current = current,
-           nested = nested},
-          n')
-     end
+fun bindCon {basis, cons, constructors, vals, strs, funs, current, nested} s n =
+    let
+        val n' = alloc ()
 
- fun lookupConById ({cons, ...} : t) n = IM.find (cons, n)
-
- fun lookupConByName ({current, ...} : t) x =
-     case current of
-         FFfi {mod = m, ...} => CFfi m
-       | FNormal {cons, ...} =>
-         case SM.find (cons, x) of
-             NONE => raise Fail "Corify.St.lookupConByName"
-           | SOME n => CNormal n
-
- fun bindVal {cons, constructors, vals, strs, funs, current, nested} s n =
-     let
-         val n' = alloc ()
-
-         val current =
-             case current of
-                 FFfi _ => raise Fail "Binding inside FFfi"
-               | FNormal {cons, constructors, vals, strs, funs} =>
-                 FNormal {cons = cons,
-                          constructors = constructors,
-                          vals = SM.insert (vals, s, n'),
-                          strs = strs,
-                          funs = funs}
-     in
-         ({cons = cons,
-           constructors = constructors,
-           vals = IM.insert (vals, n, n'),
-           strs = strs,
-           funs = funs,
-           current = current,
-           nested = nested},
-          n')
-     end
-
- fun bindConstructorVal {cons, constructors, vals, strs, funs, current, nested} s n =
-     let
-         val current =
-             case current of
-                 FFfi _ => raise Fail "Binding inside FFfi"
-               | FNormal {cons, constructors, vals, strs, funs} =>
-                 FNormal {cons = cons,
-                          constructors = constructors,
-                          vals = SM.insert (vals, s, n),
-                          strs = strs,
-                          funs = funs}
-     in
-         {cons = cons,
+        val current =
+            case current of
+                FFfi _ => raise Fail "Binding inside FFfi"
+              | FNormal {cons, constructors, vals, strs, funs} =>
+                FNormal {cons = SM.insert (cons, s, n'),
+                         constructors = constructors,
+                         vals = vals,
+                         strs = strs,
+                         funs = funs}
+    in
+        ({basis = basis,
+          cons = IM.insert (cons, n, n'),
           constructors = constructors,
-          vals = IM.insert (vals, n, n),
-          strs = strs,
-          funs = funs,
-          current = current,
-          nested = nested}
-     end
-
-
- fun lookupValById ({vals, ...} : t) n = IM.find (vals, n)
-
- fun lookupValByName ({current, ...} : t) x =
-     case current of
-         FFfi {mod = m, vals, ...} =>
-         (case SM.find (vals, x) of
-              NONE => raise Fail "Corify.St.lookupValByName: no type for FFI val"
-            | SOME t => EFfi (m, t))
-       | FNormal {vals, ...} =>
-         case SM.find (vals, x) of
-             NONE => raise Fail "Corify.St.lookupValByName"
-           | SOME n => ENormal n
-
- fun bindConstructor {cons, constructors, vals, strs, funs, current, nested} s n n' =
-     let
-         val current =
-             case current of
-                 FFfi _ => raise Fail "Binding inside FFfi"
-               | FNormal {cons, constructors, vals, strs, funs} =>
-                 FNormal {cons = cons,
-                          constructors = SM.insert (constructors, s, n'),
-                          vals = vals,
-                          strs = strs,
-                          funs = funs}
-     in
-         {cons = cons,
-          constructors = IM.insert (constructors, n, n'),
           vals = vals,
           strs = strs,
           funs = funs,
           current = current,
-          nested = nested}
-     end
+          nested = nested},
+         n')
+    end
 
- fun lookupConstructorById ({constructors, ...} : t) n =
-     case IM.find (constructors, n) of
-         NONE => raise Fail "Corify.St.lookupConstructorById"
-       | SOME x => x
+fun lookupConById ({cons, ...} : t) n = IM.find (cons, n)
 
- fun lookupConstructorByNameOpt ({current, ...} : t) x =
-     case current of
-         FFfi {mod = m, constructors, ...} =>
-         (case SM.find (constructors, x) of
-              NONE => NONE
-            | SOME (n, xs, to, dk) => SOME (L'.PConFfi {mod = m, datatyp = n, params = xs, con = x, arg = to, kind = dk}))
-       | FNormal {constructors, ...} =>
-         case SM.find (constructors, x) of
+fun lookupConByName ({current, ...} : t) x =
+    case current of
+        FFfi {mod = m, ...} => CFfi m
+      | FNormal {cons, ...} =>
+        case SM.find (cons, x) of
+            NONE => raise Fail "Corify.St.lookupConByName"
+          | SOME n => CNormal n
+
+fun bindVal {basis, cons, constructors, vals, strs, funs, current, nested} s n =
+    let
+        val n' = alloc ()
+
+        val current =
+            case current of
+                FFfi _ => raise Fail "Binding inside FFfi"
+              | FNormal {cons, constructors, vals, strs, funs} =>
+                FNormal {cons = cons,
+                         constructors = constructors,
+                         vals = SM.insert (vals, s, n'),
+                         strs = strs,
+                         funs = funs}
+    in
+        ({basis = basis,
+          cons = cons,
+          constructors = constructors,
+          vals = IM.insert (vals, n, n'),
+          strs = strs,
+          funs = funs,
+          current = current,
+          nested = nested},
+         n')
+    end
+
+fun bindConstructorVal {basis, cons, constructors, vals, strs, funs, current, nested} s n =
+    let
+        val current =
+            case current of
+                FFfi _ => raise Fail "Binding inside FFfi"
+              | FNormal {cons, constructors, vals, strs, funs} =>
+                FNormal {cons = cons,
+                         constructors = constructors,
+                         vals = SM.insert (vals, s, n),
+                         strs = strs,
+                         funs = funs}
+    in
+        {basis = basis,
+         cons = cons,
+         constructors = constructors,
+         vals = IM.insert (vals, n, n),
+         strs = strs,
+         funs = funs,
+         current = current,
+         nested = nested}
+    end
+
+
+fun lookupValById ({vals, ...} : t) n = IM.find (vals, n)
+
+fun lookupValByName ({current, ...} : t) x =
+    case current of
+        FFfi {mod = m, vals, ...} =>
+        (case SM.find (vals, x) of
+             NONE => raise Fail "Corify.St.lookupValByName: no type for FFI val"
+           | SOME t => EFfi (m, t))
+      | FNormal {vals, ...} =>
+        case SM.find (vals, x) of
+            NONE => raise Fail "Corify.St.lookupValByName"
+          | SOME n => ENormal n
+
+fun bindConstructor {basis, cons, constructors, vals, strs, funs, current, nested} s n n' =
+    let
+        val current =
+            case current of
+                FFfi _ => raise Fail "Binding inside FFfi"
+              | FNormal {cons, constructors, vals, strs, funs} =>
+                FNormal {cons = cons,
+                         constructors = SM.insert (constructors, s, n'),
+                         vals = vals,
+                         strs = strs,
+                         funs = funs}
+    in
+        {basis = basis,
+         cons = cons,
+         constructors = IM.insert (constructors, n, n'),
+         vals = vals,
+         strs = strs,
+         funs = funs,
+         current = current,
+         nested = nested}
+    end
+
+fun lookupConstructorById ({constructors, ...} : t) n =
+    case IM.find (constructors, n) of
+        NONE => raise Fail "Corify.St.lookupConstructorById"
+      | SOME x => x
+
+fun lookupConstructorByNameOpt ({current, ...} : t) x =
+    case current of
+        FFfi {mod = m, constructors, ...} =>
+        (case SM.find (constructors, x) of
              NONE => NONE
-           | SOME n => SOME n
+           | SOME (n, xs, to, dk) => SOME (L'.PConFfi {mod = m, datatyp = n, params = xs, con = x, arg = to, kind = dk}))
+      | FNormal {constructors, ...} =>
+        case SM.find (constructors, x) of
+            NONE => NONE
+          | SOME n => SOME n
 
- fun lookupConstructorByName ({current, ...} : t) x =
-     case current of
-         FFfi {mod = m, constructors, ...} =>
-         (case SM.find (constructors, x) of
-              NONE => raise Fail "Corify.St.lookupConstructorByName [1]"
-            | SOME (n, xs, to, dk) => L'.PConFfi {mod = m, datatyp = n, params = xs, con = x, arg = to, kind = dk})
-       | FNormal {constructors, ...} =>
-         case SM.find (constructors, x) of
-             NONE => raise Fail "Corify.St.lookupConstructorByName [2]"
-           | SOME n => n
+fun lookupConstructorByName ({current, ...} : t) x =
+    case current of
+        FFfi {mod = m, constructors, ...} =>
+        (case SM.find (constructors, x) of
+             NONE => raise Fail "Corify.St.lookupConstructorByName [1]"
+           | SOME (n, xs, to, dk) => L'.PConFfi {mod = m, datatyp = n, params = xs, con = x, arg = to, kind = dk})
+      | FNormal {constructors, ...} =>
+        case SM.find (constructors, x) of
+            NONE => raise Fail "Corify.St.lookupConstructorByName [2]"
+          | SOME n => n
 
- fun enter {cons, constructors, vals, strs, funs, current, nested} =
-     {cons = cons,
-      constructors = constructors,
-      vals = vals,
-      strs = strs,
-      funs = funs,
-      current = FNormal {cons = SM.empty,
-                         constructors = SM.empty,
-                         vals = SM.empty,
-                         strs = SM.empty,
-                         funs = SM.empty},
-      nested = current :: nested}
+fun enter {basis, cons, constructors, vals, strs, funs, current, nested} =
+    {basis = basis,
+     cons = cons,
+     constructors = constructors,
+     vals = vals,
+     strs = strs,
+     funs = funs,
+     current = FNormal {cons = SM.empty,
+                        constructors = SM.empty,
+                        vals = SM.empty,
+                        strs = SM.empty,
+                        funs = SM.empty},
+     nested = current :: nested}
 
- fun dummy f = {cons = IM.empty,
-                constructors = IM.empty,
-                vals = IM.empty,
-                strs = IM.empty,
-                funs = IM.empty,
-                current = f,
-                nested = []}
+fun dummy (b, f) = {basis = b,
+                    cons = IM.empty,
+                    constructors = IM.empty,
+                    vals = IM.empty,
+                    strs = IM.empty,
+                    funs = IM.empty,
+                    current = f,
+                    nested = []}
 
- fun leave {cons, constructors, vals, strs, funs, current, nested = m1 :: rest} =
-         {outer = {cons = cons,
-                   constructors = constructors,
-                   vals = vals,
-                   strs = strs,
-                   funs = funs,
-                   current = m1,
-                   nested = rest},
-          inner = dummy current}
-   | leave _ = raise Fail "Corify.St.leave"
+fun leave {basis, cons, constructors, vals, strs, funs, current, nested = m1 :: rest} =
+    {outer = {basis = basis,
+              cons = cons,
+              constructors = constructors,
+              vals = vals,
+              strs = strs,
+              funs = funs,
+              current = m1,
+              nested = rest},
+     inner = dummy (basis, current)}
+  | leave _ = raise Fail "Corify.St.leave"
 
- fun ffi m vals constructors = dummy (FFfi {mod = m, vals = vals, constructors = constructors})
+fun ffi m vals constructors = dummy (NONE, FFfi {mod = m, vals = vals, constructors = constructors})
 
- fun bindStr ({cons, constructors, vals, strs, funs,
-               current = FNormal {cons = mcons, constructors = mconstructors,
-                                  vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
-             x n ({current = f, ...} : t) =
-     {cons = cons,
-      constructors = constructors,
-      vals = vals,
-      strs = IM.insert (strs, n, f),
-      funs = funs,
-      current = FNormal {cons = mcons,
-                         constructors = mconstructors,
-                         vals = mvals,
-                         strs = SM.insert (mstrs, x, f),
-                         funs = mfuns},
-      nested = nested}
-   | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr"
+fun bindStr ({basis, cons, constructors, vals, strs, funs,
+              current = FNormal {cons = mcons, constructors = mconstructors,
+                                 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
+            x n ({current = f, ...} : t) =
+    {basis = basis,
+     cons = cons,
+     constructors = constructors,
+     vals = vals,
+     strs = IM.insert (strs, n, f),
+     funs = funs,
+     current = FNormal {cons = mcons,
+                        constructors = mconstructors,
+                        vals = mvals,
+                        strs = SM.insert (mstrs, x, f),
+                        funs = mfuns},
+     nested = nested}
+  | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr"
 
- fun lookupStrById ({strs, ...} : t) n =
-     case IM.find (strs, n) of
-         NONE => raise Fail "Corify.St.lookupStrById"
-       | SOME f => dummy f
+fun lookupStrById ({basis, strs, ...} : t) n =
+    case IM.find (strs, n) of
+        NONE => raise Fail "Corify.St.lookupStrById"
+      | SOME f => dummy (basis, f)
 
- fun lookupStrByName (m, {current = FNormal {strs, ...}, ...} : t) =
-     (case SM.find (strs, m) of
-          NONE => raise Fail "Corify.St.lookupStrByName"
-        | SOME f => dummy f)
-   | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName"
+fun lookupStrByName (m, {basis, current = FNormal {strs, ...}, ...} : t) =
+    (case SM.find (strs, m) of
+         NONE => raise Fail "Corify.St.lookupStrByName"
+       | SOME f => dummy (basis, f))
+  | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName"
 
- fun bindFunctor ({cons, constructors, vals, strs, funs,
-                   current = FNormal {cons = mcons, constructors = mconstructors,
-                                      vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
-                 x n xa na str =
-     {cons = cons,
-      constructors = constructors,
-      vals = vals,
-      strs = strs,
-      funs = IM.insert (funs, n, (xa, na, str)),
-      current = FNormal {cons = mcons,
-                         constructors = mconstructors,
-                         vals = mvals,
-                         strs = mstrs,
-                         funs = SM.insert (mfuns, x, (xa, na, str))},
-      nested = nested}
-   | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor"
+fun bindFunctor ({basis, cons, constructors, vals, strs, funs,
+                  current = FNormal {cons = mcons, constructors = mconstructors,
+                                     vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
+                x n xa na str =
+    {basis = basis,
+     cons = cons,
+     constructors = constructors,
+     vals = vals,
+     strs = strs,
+     funs = IM.insert (funs, n, (xa, na, str)),
+     current = FNormal {cons = mcons,
+                        constructors = mconstructors,
+                        vals = mvals,
+                        strs = mstrs,
+                        funs = SM.insert (mfuns, x, (xa, na, str))},
+     nested = nested}
+  | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor"
 
- fun lookupFunctorById ({funs, ...} : t) n =
-     case IM.find (funs, n) of
-         NONE => raise Fail "Corify.St.lookupFunctorById"
-       | SOME v => v
+fun lookupFunctorById ({funs, ...} : t) n =
+    case IM.find (funs, n) of
+        NONE => raise Fail "Corify.St.lookupFunctorById"
+      | SOME v => v
 
- fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) =
-     (case SM.find (funs, m) of
-          NONE => raise Fail "Corify.St.lookupFunctorByName"
-        | SOME v => v)
-   | lookupFunctorByName _ = raise Fail "Corify.St.lookupFunctorByName"
+fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) =
+    (case SM.find (funs, m) of
+         NONE => raise Fail "Corify.St.lookupFunctorByName"
+       | SOME v => v)
+  | lookupFunctorByName _ = raise Fail "Corify.St.lookupFunctorByName"
 
- end
+end
 
 
- fun corifyKind (k, loc) =
-     case k of
-         L.KType => (L'.KType, loc)
-       | L.KArrow (k1, k2) => (L'.KArrow (corifyKind k1, corifyKind k2), loc)
-       | L.KName => (L'.KName, loc)
-       | L.KRecord k => (L'.KRecord (corifyKind k), loc)
-       | L.KUnit => (L'.KUnit, loc)
-       | L.KTuple ks => (L'.KTuple (map corifyKind ks), loc)
+fun corifyKind (k, loc) =
+    case k of
+        L.KType => (L'.KType, loc)
+      | L.KArrow (k1, k2) => (L'.KArrow (corifyKind k1, corifyKind k2), loc)
+      | L.KName => (L'.KName, loc)
+      | L.KRecord k => (L'.KRecord (corifyKind k), loc)
+      | L.KUnit => (L'.KUnit, loc)
+      | L.KTuple ks => (L'.KTuple (map corifyKind ks), loc)
 
- fun corifyCon st (c, loc) =
-     case c of
-         L.TFun (t1, t2) => (L'.TFun (corifyCon st t1, corifyCon st t2), loc)
-       | L.TCFun (x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon st t), loc)
-       | L.TRecord c => (L'.TRecord (corifyCon st c), loc)
+fun corifyCon st (c, loc) =
+    case c of
+        L.TFun (t1, t2) => (L'.TFun (corifyCon st t1, corifyCon st t2), loc)
+      | L.TCFun (x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon st t), loc)
+      | L.TRecord c => (L'.TRecord (corifyCon st c), loc)
 
-       | L.CRel n => (L'.CRel n, loc)
-       | L.CNamed n =>
-         (case St.lookupConById st n of
-              NONE => (L'.CNamed n, loc)
-            | SOME n => (L'.CNamed n, loc))
-       | L.CModProj (m, ms, x) =>
-         let
-             val st = St.lookupStrById st m
-             val st = foldl St.lookupStrByName st ms
-         in
-             case St.lookupConByName st x of
-                 St.CNormal n => (L'.CNamed n, loc)
-               | St.CFfi m => (L'.CFfi (m, x), loc)
-         end
+      | L.CRel n => (L'.CRel n, loc)
+      | L.CNamed n =>
+        (case St.lookupConById st n of
+             NONE => (L'.CNamed n, loc)
+           | SOME n => (L'.CNamed n, loc))
+      | L.CModProj (m, ms, x) =>
+        let
+            val st = St.lookupStrById st m
+            val st = foldl St.lookupStrByName st ms
+        in
+            case St.lookupConByName st x of
+                St.CNormal n => (L'.CNamed n, loc)
+              | St.CFfi m => (L'.CFfi (m, x), loc)
+        end
 
-       | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc)
-       | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc)
+      | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc)
+      | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc)
 
-       | L.CName s => (L'.CName s, loc)
+      | L.CName s => (L'.CName s, loc)
 
-       | L.CRecord (k, xcs) =>
-         (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc)
-       | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc)
-       | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc)
-       | L.CUnit => (L'.CUnit, loc)
+      | L.CRecord (k, xcs) =>
+        (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc)
+      | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc)
+      | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc)
+      | L.CUnit => (L'.CUnit, loc)
 
-       | L.CTuple cs => (L'.CTuple (map (corifyCon st) cs), loc)
-       | L.CProj (c, n) => (L'.CProj (corifyCon st c, n), loc)
+      | L.CTuple cs => (L'.CTuple (map (corifyCon st) cs), loc)
+      | L.CProj (c, n) => (L'.CProj (corifyCon st c, n), loc)
 
- fun corifyPatCon st pc =
-     case pc of
-         L.PConVar n => St.lookupConstructorById st n
-       | L.PConProj (m1, ms, x) =>
-         let
-             val st = St.lookupStrById st m1
-             val st = foldl St.lookupStrByName st ms
-         in
-             St.lookupConstructorByName st x
-         end
+fun corifyPatCon st pc =
+    case pc of
+        L.PConVar n => St.lookupConstructorById st n
+      | L.PConProj (m1, ms, x) =>
+        let
+            val st = St.lookupStrById st m1
+            val st = foldl St.lookupStrByName st ms
+        in
+            St.lookupConstructorByName st x
+        end
 
- fun corifyPat st (p, loc) =
-     case p of
-         L.PWild => (L'.PWild, loc)
-       | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc)
-       | L.PPrim p => (L'.PPrim p, loc)
-       | L.PCon (dk, pc, ts, po) => (L'.PCon (dk, corifyPatCon st pc, map (corifyCon st) ts,
-                                              Option.map (corifyPat st) po), loc)
-       | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc)
+fun corifyPat st (p, loc) =
+    case p of
+        L.PWild => (L'.PWild, loc)
+      | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc)
+      | L.PPrim p => (L'.PPrim p, loc)
+      | L.PCon (dk, pc, ts, po) => (L'.PCon (dk, corifyPatCon st pc, map (corifyCon st) ts,
+                                             Option.map (corifyPat st) po), loc)
+      | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc)
 
- fun corifyExp st (e, loc) =
-     case e of
-         L.EPrim p => (L'.EPrim p, loc)
-       | L.ERel n => (L'.ERel n, loc)
-       | L.ENamed n =>
-         (case St.lookupValById st n of
-              NONE => (L'.ENamed n, loc)
-            | SOME n => (L'.ENamed n, loc))
-       | L.EModProj (m, ms, x) =>
-         let
-             val st = St.lookupStrById st m
-             val st = foldl St.lookupStrByName st ms
-         in
-             case St.lookupConstructorByNameOpt st x of
-                 SOME (pc as L'.PConFfi {mod = m, datatyp, params, arg, kind, ...}) =>
-                 let
-                     val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) params
-                     val e = case arg of
-                                 NONE => (L'.ECon (kind, pc, args, NONE), loc)
-                               | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc),
-                                                       (L'.ECon (kind, pc, args, SOME (L'.ERel 0, loc)), loc)), loc)
+fun corifyExp st (e, loc) =
+    case e of
+        L.EPrim p => (L'.EPrim p, loc)
+      | L.ERel n => (L'.ERel n, loc)
+      | L.ENamed n =>
+        (case St.lookupValById st n of
+             NONE => (L'.ENamed n, loc)
+           | SOME n => (L'.ENamed n, loc))
+      | L.EModProj (m, ms, x) =>
+        let
+            val st = St.lookupStrById st m
+            val st = foldl St.lookupStrByName st ms
+        in
+            case St.lookupConstructorByNameOpt st x of
+                SOME (pc as L'.PConFfi {mod = m, datatyp, params, arg, kind, ...}) =>
+                let
+                    val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) params
+                    val e = case arg of
+                                NONE => (L'.ECon (kind, pc, args, NONE), loc)
+                              | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc),
+                                                      (L'.ECon (kind, pc, args, SOME (L'.ERel 0, loc)), loc)), loc)
 
-                     val k = (L'.KType, loc)
-                 in
-                     foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e params
-                 end
-               | _ =>
-                 case St.lookupValByName st x of
-                     St.ENormal n => (L'.ENamed n, loc)
-                   | St.EFfi (m, t) =>
-                     case t of
-                         (L'.TFun (dom as (L'.TRecord (L'.CRecord (_, []), _), _), ran), _) =>
-                         (L'.EAbs ("arg", dom, ran, (L'.EFfiApp (m, x, []), loc)), loc)
-                       | t as (L'.TFun _, _) =>
-                         let
-                             fun getArgs (all as (t, _), args) =
-                                 case t of
-                                     L'.TFun (dom, ran) => getArgs (ran, dom :: args)
-                                   | _ => (all, rev args)
+                    val k = (L'.KType, loc)
+                in
+                    foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e params
+                end
+              | _ =>
+                case St.lookupValByName st x of
+                    St.ENormal n => (L'.ENamed n, loc)
+                  | St.EFfi (m, t) =>
+                    case t of
+                        (L'.TFun (dom as (L'.TRecord (L'.CRecord (_, []), _), _), ran), _) =>
+                        (L'.EAbs ("arg", dom, ran, (L'.EFfiApp (m, x, []), loc)), loc)
+                      | t as (L'.TFun _, _) =>
+                        let
+                            fun getArgs (all as (t, _), args) =
+                                case t of
+                                    L'.TFun (dom, ran) => getArgs (ran, dom :: args)
+                                  | _ => (all, rev args)
 
-                             val (result, args) = getArgs (t, [])
+                            val (result, args) = getArgs (t, [])
 
-                             val (actuals, _) = foldr (fn (_, (actuals, n)) =>
-                                                          ((L'.ERel n, loc) :: actuals,
-                                                           n + 1)) ([], 0) args
-                             val app = (L'.EFfiApp (m, x, actuals), loc)
-                             val (abs, _, _) = foldr (fn (t, (abs, ran, n)) =>
-                                                         ((L'.EAbs ("arg" ^ Int.toString n,
-                                                                    t,
-                                                                    ran,
-                                                                    abs), loc),
-                                                          (L'.TFun (t, ran), loc),
-                                                          n - 1)) (app, result, length args - 1) args
-                         in
-                             abs
-                         end
-                       | _ => (L'.EFfi (m, x), loc)
-         end
-       | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), loc)
-       | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc)
-       | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc)
-       | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc)
+                            val (actuals, _) = foldr (fn (_, (actuals, n)) =>
+                                                         ((L'.ERel n, loc) :: actuals,
+                                                          n + 1)) ([], 0) args
+                            val app = (L'.EFfiApp (m, x, actuals), loc)
+                            val (abs, _, _) = foldr (fn (t, (abs, ran, n)) =>
+                                                        ((L'.EAbs ("arg" ^ Int.toString n,
+                                                                   t,
+                                                                   ran,
+                                                                   abs), loc),
+                                                         (L'.TFun (t, ran), loc),
+                                                         n - 1)) (app, result, length args - 1) args
+                        in
+                            abs
+                        end
+                      | _ => (L'.EFfi (m, x), loc)
+        end
+      | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), loc)
+      | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc)
+      | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc)
+      | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc)
 
-       | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) =>
-                                               (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc)
-       | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c,
-                                                        {field = corifyCon st field, rest = corifyCon st rest}), loc)
-       | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c,
-                                                    {field = corifyCon st field, rest = corifyCon st rest}), loc)
-       | L.EFold k => (L'.EFold (corifyKind k), loc)
+      | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) =>
+                                              (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc)
+      | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c,
+                                                       {field = corifyCon st field, rest = corifyCon st rest}), loc)
+      | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c,
+                                                   {field = corifyCon st field, rest = corifyCon st rest}), loc)
+      | L.EFold k => (L'.EFold (corifyKind k), loc)
 
-       | L.ECase (e, pes, {disc, result}) =>
-         (L'.ECase (corifyExp st e,
-                    map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes,
-                    {disc = corifyCon st disc, result = corifyCon st result}),
-          loc)
+      | L.ECase (e, pes, {disc, result}) =>
+        (L'.ECase (corifyExp st e,
+                   map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes,
+                   {disc = corifyCon st disc, result = corifyCon st result}),
+         loc)
 
-       | L.EWrite e => (L'.EWrite (corifyExp st e), loc)
+      | L.EWrite e => (L'.EWrite (corifyExp st e), loc)
 
- fun corifyDecl ((d, loc : EM.span), st) =
-     case d of
-         L.DCon (x, n, k, c) =>
-         let
-             val (st, n) = St.bindCon st x n
-         in
-             ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st)
-         end
-       | L.DDatatype (x, n, xs, xncs) =>
-         let
-             val (st, n) = St.bindCon st x n
-             val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
-                                                    let
-                                                        val st = St.bindConstructor st x n (L'.PConVar n)
-                                                        val st = St.bindConstructorVal st x n
-                                                        val co = Option.map (corifyCon st) co
-                                                    in
-                                                        ((x, n, co), st)
-                                                    end) st xncs
+fun corifyDecl ((d, loc : EM.span), st) =
+    case d of
+        L.DCon (x, n, k, c) =>
+        let
+            val (st, n) = St.bindCon st x n
+        in
+            ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st)
+        end
+      | L.DDatatype (x, n, xs, xncs) =>
+        let
+            val (st, n) = St.bindCon st x n
+            val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
+                                                   let
+                                                       val st = St.bindConstructor st x n (L'.PConVar n)
+                                                       val st = St.bindConstructorVal st x n
+                                                       val co = Option.map (corifyCon st) co
+                                                   in
+                                                       ((x, n, co), st)
+                                                   end) st xncs
 
-             val dk = ElabUtil.classifyDatatype xncs
-             val t = (L'.CNamed n, loc)
-             val nxs = length xs - 1
-             val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
-             val k = (L'.KType, loc)
-             val dcons = map (fn (x, n, to) =>
-                                 let
-                                     val args = ListUtil.mapi (fn (i, _) => (L'.CRel (nxs - i), loc)) xs
-                                     val (e, t) =
-                                         case to of
-                                             NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE), loc), t)
-                                           | SOME t' => ((L'.EAbs ("x", t', t,
-                                                                   (L'.ECon (dk, L'.PConVar n, args,
-                                                                             SOME (L'.ERel 0, loc)),
-                                                                    loc)),
-                                                          loc),
-                                                         (L'.TFun (t', t), loc))
+            val dk = ElabUtil.classifyDatatype xncs
+            val t = (L'.CNamed n, loc)
+            val nxs = length xs - 1
+            val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
+            val k = (L'.KType, loc)
+            val dcons = map (fn (x, n, to) =>
+                                let
+                                    val args = ListUtil.mapi (fn (i, _) => (L'.CRel (nxs - i), loc)) xs
+                                    val (e, t) =
+                                        case to of
+                                            NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE), loc), t)
+                                          | SOME t' => ((L'.EAbs ("x", t', t,
+                                                                  (L'.ECon (dk, L'.PConVar n, args,
+                                                                            SOME (L'.ERel 0, loc)),
+                                                                   loc)),
+                                                         loc),
+                                                        (L'.TFun (t', t), loc))
 
-                                     val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
-                                     val e = foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs
-                                 in
-                                     (L'.DVal (x, n, t, e, ""), loc)
-                                 end) xncs
-         in
-             ((L'.DDatatype (x, n, xs, xncs), loc) :: dcons, st)
-         end
-       | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
-         let
-             val (st, n) = St.bindCon st x n
-             val c = corifyCon st (L.CModProj (m1, ms, s), loc)
+                                    val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
+                                    val e = foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs
+                                in
+                                    (L'.DVal (x, n, t, e, ""), loc)
+                                end) xncs
+        in
+            ((L'.DDatatype (x, n, xs, xncs), loc) :: dcons, st)
+        end
+      | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
+        let
+            val (st, n) = St.bindCon st x n
+            val c = corifyCon st (L.CModProj (m1, ms, s), loc)
 
-             val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms
-             val (_, {inner, ...}) = corifyStr (m, st)
+            val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms
+            val (_, {inner, ...}) = corifyStr (m, st)
 
-             val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
-                                                    let
-                                                        val n' = St.lookupConstructorByName inner x
-                                                        val st = St.bindConstructor st x n n'
-                                                        val (st, n) = St.bindVal st x n
-                                                        val co = Option.map (corifyCon st) co
-                                                    in
-                                                        ((x, n, co), st)
-                                                    end) st xncs
+            val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
+                                                   let
+                                                       val n' = St.lookupConstructorByName inner x
+                                                       val st = St.bindConstructor st x n n'
+                                                       val (st, n) = St.bindVal st x n
+                                                       val co = Option.map (corifyCon st) co
+                                                   in
+                                                       ((x, n, co), st)
+                                                   end) st xncs
 
-             val nxs = length xs - 1
-             val c = ListUtil.foldli (fn (i, _, c) => (L'.CApp (c, (L'.CRel (nxs - i), loc)), loc)) c xs
-             val k = (L'.KType, loc)
-             val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
+            val nxs = length xs - 1
+            val c = ListUtil.foldli (fn (i, _, c) => (L'.CApp (c, (L'.CRel (nxs - i), loc)), loc)) c xs
+            val k = (L'.KType, loc)
+            val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
 
-             val cds = map (fn (x, n, co) =>
-                               let
-                                   val t = case co of
-                                               NONE => c
-                                             | SOME t' => (L'.TFun (t', c), loc)
-                                   val e = corifyExp st (L.EModProj (m1, ms, x), loc)
+            val cds = map (fn (x, n, co) =>
+                              let
+                                  val t = case co of
+                                              NONE => c
+                                            | SOME t' => (L'.TFun (t', c), loc)
+                                  val e = corifyExp st (L.EModProj (m1, ms, x), loc)
 
-                                   val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
-                               in
-                                   (L'.DVal (x, n, t, e, x), loc)
-                               end) xncs
-         in
-             ((L'.DCon (x, n, k', c), loc) :: cds, st)
-         end
-       | L.DVal (x, n, t, e) =>
-         let
-             val (st, n) = St.bindVal st x n
-             val s =
-                 if String.isPrefix "wrap_" x then
-                     String.extract (x, 5, NONE)
-                 else
-                     x
-         in
-             ([(L'.DVal (x, n, corifyCon st t, corifyExp st e, s), loc)], st)
-         end
-       | L.DValRec vis =>
-         let
-             val (vis, st) = ListUtil.foldlMap
-                                 (fn ((x, n, t, e), st) =>
-                                     let
-                                         val (st, n) = St.bindVal st x n
-                                     in
-                                         ((x, n, t, e), st)
-                                     end)
-                                 st vis
+                                  val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
+                              in
+                                  (L'.DVal (x, n, t, e, x), loc)
+                              end) xncs
+        in
+            ((L'.DCon (x, n, k', c), loc) :: cds, st)
+        end
+      | L.DVal (x, n, t, e) =>
+        let
+            val (st, n) = St.bindVal st x n
+            val s =
+                if String.isPrefix "wrap_" x then
+                    String.extract (x, 5, NONE)
+                else
+                    x
+        in
+            ([(L'.DVal (x, n, corifyCon st t, corifyExp st e, s), loc)], st)
+        end
+      | L.DValRec vis =>
+        let
+            val (vis, st) = ListUtil.foldlMap
+                                (fn ((x, n, t, e), st) =>
+                                    let
+                                        val (st, n) = St.bindVal st x n
+                                    in
+                                        ((x, n, t, e), st)
+                                    end)
+                                st vis
 
-             val vis = map
-                           (fn (x, n, t, e) =>
-                               let
-                                   val s =
-                                       if String.isPrefix "wrap_" x then
-                                           String.extract (x, 5, NONE)
-                                       else
-                                           x
-                               in
-                                   (x, n, corifyCon st t, corifyExp st e, s)
-                               end)
-                           vis
-         in
-             ([(L'.DValRec vis, loc)], st)
-         end
-       | L.DSgn _ => ([], st)
+            val vis = map
+                          (fn (x, n, t, e) =>
+                              let
+                                  val s =
+                                      if String.isPrefix "wrap_" x then
+                                          String.extract (x, 5, NONE)
+                                      else
+                                          x
+                              in
+                                  (x, n, corifyCon st t, corifyExp st e, s)
+                              end)
+                          vis
+        in
+            ([(L'.DValRec vis, loc)], st)
+        end
+      | L.DSgn _ => ([], st)
 
-       | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) =>
-         ([], St.bindFunctor st x n xa na str)
+      | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) =>
+        ([], St.bindFunctor st x n xa na str)
 
-       | L.DStr (x, n, _, str) =>
-         let
-             val (ds, {inner, outer}) = corifyStr (str, st)
-             val st = St.bindStr outer x n inner
-         in
-             (ds, st)
-         end
+      | L.DStr (x, n, _, str) =>
+        let
+            val (ds, {inner, outer}) = corifyStr (str, st)
+            val st = St.bindStr outer x n inner
+        in
+            (ds, st)
+        end
 
-       | L.DFfiStr (m, n, (sgn, _)) =>
-         (case sgn of
-              L.SgnConst sgis =>
-              let
-                  val (ds, cmap, conmap, st) =
-                      foldl (fn ((sgi, _), (ds, cmap, conmap, st)) =>
-                                case sgi of
-                                    L.SgiConAbs (x, n, k) =>
-                                    let
-                                        val (st, n') = St.bindCon st x n
-                                    in
-                                        ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
-                                         cmap,
-                                         conmap,
-                                         st)
-                                    end
-                                  | L.SgiCon (x, n, k, _) =>
-                                    let
-                                        val (st, n') = St.bindCon st x n
-                                    in
-                                        ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
-                                         cmap,
-                                         conmap,
-                                         st)
-                                    end
+      | L.DFfiStr (m, n, (sgn, _)) =>
+        (case sgn of
+             L.SgnConst sgis =>
+             let
+                 val (ds, cmap, conmap, st) =
+                     foldl (fn ((sgi, _), (ds, cmap, conmap, st)) =>
+                               case sgi of
+                                   L.SgiConAbs (x, n, k) =>
+                                   let
+                                       val (st, n') = St.bindCon st x n
+                                   in
+                                       ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
+                                        cmap,
+                                        conmap,
+                                        st)
+                                   end
+                                 | L.SgiCon (x, n, k, _) =>
+                                   let
+                                       val (st, n') = St.bindCon st x n
+                                   in
+                                       ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
+                                        cmap,
+                                        conmap,
+                                        st)
+                                   end
 
-                                  | L.SgiDatatype (x, n, xs, xnts) =>
-                                    let
-                                        val k = (L'.KType, loc)
-                                        val dk = ElabUtil.classifyDatatype xnts
-                                        val (st, n') = St.bindCon st x n
-                                        val (xnts, (ds', st, cmap, conmap)) =
-                                            ListUtil.foldlMap
-                                                (fn ((x', n, to), (ds', st, cmap, conmap)) =>
-                                                    let
-                                                        val dt = (L'.CNamed n', loc)
-                                                        val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) xs
+                                 | L.SgiDatatype (x, n, xs, xnts) =>
+                                   let
+                                       val k = (L'.KType, loc)
+                                       val dk = ElabUtil.classifyDatatype xnts
+                                       val (st, n') = St.bindCon st x n
+                                       val (xnts, (ds', st, cmap, conmap)) =
+                                           ListUtil.foldlMap
+                                               (fn ((x', n, to), (ds', st, cmap, conmap)) =>
+                                                   let
+                                                       val dt = (L'.CNamed n', loc)
+                                                       val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) xs
 
-                                                        val to = Option.map (corifyCon st) to
+                                                       val to = Option.map (corifyCon st) to
 
-                                                        val pc = L'.PConFfi {mod = m,
-                                                                             datatyp = x,
-                                                                             params = xs,
-                                                                             con = x',
-                                                                             arg = to,
-                                                                             kind = dk}
+                                                       val pc = L'.PConFfi {mod = m,
+                                                                            datatyp = x,
+                                                                            params = xs,
+                                                                            con = x',
+                                                                            arg = to,
+                                                                            kind = dk}
 
-                                                        fun wrapT t =
-                                                            foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
-                                                        fun wrapE e =
-                                                            foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs
+                                                       fun wrapT t =
+                                                           foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
+                                                       fun wrapE e =
+                                                           foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs
 
-                                                        val (cmap, d) =
-                                                            case to of
-                                                                NONE => (SM.insert (cmap, x', wrapT dt),
-                                                                         (L'.DVal (x', n, wrapT dt,
-                                                                                   wrapE
-                                                                                       (L'.ECon (dk, pc, args, NONE),
-                                                                                        loc),
-                                                                                   ""), loc))
-                                                              | SOME t =>
-                                                                let
-                                                                    val tf = (L'.TFun (t, dt), loc)
-                                                                    val e = wrapE (L'.EAbs ("x", t, tf,
-                                                                                            (L'.ECon (dk, pc, args,
-                                                                                                      SOME (L'.ERel 0,
-                                                                                                            loc)),
-                                                                                             loc)), loc)
-                                                                    val d = (L'.DVal (x', n, wrapT tf,
-                                                                                      e, ""), loc)
+                                                       val (cmap, d) =
+                                                           case to of
+                                                               NONE => (SM.insert (cmap, x', wrapT dt),
+                                                                        (L'.DVal (x', n, wrapT dt,
+                                                                                  wrapE
+                                                                                      (L'.ECon (dk, pc, args, NONE),
+                                                                                       loc),
+                                                                                  ""), loc))
+                                                             | SOME t =>
+                                                               let
+                                                                   val tf = (L'.TFun (t, dt), loc)
+                                                                   val e = wrapE (L'.EAbs ("x", t, tf,
+                                                                                           (L'.ECon (dk, pc, args,
+                                                                                                     SOME (L'.ERel 0,
+                                                                                                           loc)),
+                                                                                            loc)), loc)
+                                                                   val d = (L'.DVal (x', n, wrapT tf,
+                                                                                     e, ""), loc)
                                                                in
                                                                    (SM.insert (cmap, x', wrapT tf), d)
                                                                end
@@ -746,7 +772,7 @@
 
                  val st = St.bindStr st m n (St.ffi m cmap conmap)
              in
-                 (rev ds, st)
+                 (rev ds, St.basisIs (st, n))
              end
            | _ => raise Fail "Non-const signature for FFI structure")
 
@@ -766,30 +792,52 @@
                               ([], st))
                    | SOME (m, ms) =>
                      let
+                         val basis_n = case St.lookupBasis st of
+                                           NONE => raise Fail "Corify: Don't know number of Basis"
+                                         | SOME n => n
+
                          fun wrapSgi ((sgi, _), (wds, eds))  =
                              case sgi of
                                  L.SgiVal (s, _, t as (L.TFun (dom, ran), _)) =>
                                  (case (#1 dom, #1 ran) of
-                                      (L.TRecord (L.CRecord (_, []), _),
-                                       L.CApp
-                                           ((L.CApp
-                                                 ((L.CApp ((L.CModProj (_, [], "xml"), _),
-                                                           (L.CRecord (_, [((L.CName "Html", _),
-                                                                            _)]), _)), _), _), _), _)) =>
+                                      (L.TRecord _,
+                                       L.CApp ((L.CModProj (basis, [], "transaction"), _),
+                                               ran' as
+                                                    (L.CApp
+                                                         ((L.CApp
+                                                               ((L.CApp ((L.CModProj (basis', [], "xml"), _),
+                                                                         (L.CRecord (_, [((L.CName "Html", _),
+                                                                                          _)]), _)), _), _),
+                                                           _), _), _))) =>
                                       let
                                           val ran = (L.TRecord (L.CRecord ((L.KType, loc), []), loc), loc)
+                                          val ranT = (L.CApp ((L.CModProj (basis, [], "transaction"), loc),
+                                                              ran), loc)
                                           val e = (L.EModProj (m, ms, s), loc)
-                                          val e = (L.EAbs ("vs", dom, ran,
-                                                           (L.EWrite (L.EApp (e, (L.ERel 0, loc)), loc), loc)), loc)
+
+                                          val ef = (L.EModProj (basis, [], "bind"), loc)
+                                          val ef = (L.ECApp (ef, ran'), loc)
+                                          val ef = (L.EApp (ef, (L.EApp (e, (L.ERel 0, loc)), loc)), loc)
+
+                                          val eat = (L.CApp ((L.CModProj (basis, [], "transaction"), loc),
+                                                             ran), loc)
+                                          val ea = (L.EAbs ("p", ran', eat,
+                                                            (L.EWrite (L.ERel 0, loc), loc)), loc)
+
+                                          val e = (L.EApp (ef, ea), loc)
+                                          val e = (L.EAbs ("vs", dom, ran, e), loc)
                                       in
-                                          ((L.DVal ("wrap_" ^ s, 0,
-                                                    (L.TFun (dom, ran), loc),
-                                                    e), loc) :: wds,
-                                           (fn st =>
-                                               case #1 (corifyExp st (L.EModProj (en, [], "wrap_" ^ s), loc)) of
-                                                   L'.ENamed n => (L'.DExport (L'.Link, n), loc)
-                                                 | _ => raise Fail "Corify: Value to export didn't corify properly")
-                                           :: eds)
+                                          if basis = basis_n andalso basis' = basis_n then
+                                              ((L.DVal ("wrap_" ^ s, 0,
+                                                        (L.TFun (dom, ranT), loc),
+                                                        e), loc) :: wds,
+                                               (fn st =>
+                                                   case #1 (corifyExp st (L.EModProj (en, [], "wrap_" ^ s), loc)) of
+                                                       L'.ENamed n => (L'.DExport (L'.Link, n), loc)
+                                                     | _ => raise Fail "Corify: Value to export didn't corify properly")
+                                               :: eds)
+                                          else
+                                              (wds, eds)
                                       end
                                     | _ => (wds, eds))
                                | _ => (wds, eds)
@@ -798,7 +846,7 @@
                          val wrapper = (L.StrConst wds, loc)
                          val (ds, {inner, outer}) = corifyStr (wrapper, st)
                          val st = St.bindStr outer "wrapper" en inner
-                         
+                                  
                          val ds = ds @ map (fn f => f st) eds
                      in
                          (ds, st)
@@ -806,13 +854,13 @@
              end
            | _ => raise Fail "Non-const signature for 'export'")
 
-       | L.DTable (_, x, n, c) =>
-         let
-             val (st, n) = St.bindVal st x n
-             val s = x
-         in
-             ([(L'.DTable (x, n, corifyCon st c, s), loc)], st)
-         end
+      | L.DTable (_, x, n, c) =>
+        let
+            val (st, n) = St.bindVal st x n
+            val s = x
+        in
+            ([(L'.DTable (x, n, corifyCon st c, s), loc)], st)
+        end
 
 and corifyStr ((str, _), st) =
     case str of
@@ -865,7 +913,7 @@
                              | L.DFfiStr (_, n', _) => Int.max (n, n')
                              | L.DExport _ => n
                              | L.DTable (_, _, n', _) => Int.max (n, n'))
-                 0 ds
+                       0 ds
 
 and maxNameStr (str, _) =
     case str of
--- a/src/elaborate.sml	Sun Aug 31 09:05:33 2008 -0400
+++ b/src/elaborate.sml	Sun Aug 31 09:45:23 2008 -0400
@@ -3036,27 +3036,36 @@
                                       ((L'.TFun (dom, ran), _), []) =>
                                       (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of
                                            (((L'.TRecord domR, _), []),
-                                            ((L'.CApp (tf, arg3), _), [])) =>
-                                           (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of
-                                                (((L'.CApp (tf, arg2), _), []),
-                                                 (((L'.CRecord (_, []), _), []))) =>
-                                                (case (hnormCon (env, denv) tf) of
-                                                     ((L'.CApp (tf, arg1), _), []) =>
-                                                     (case (hnormCon (env, denv) tf,
-                                                            hnormCon (env, denv) domR,
-                                                            hnormCon (env, denv) arg1,
-                                                            hnormCon (env, denv) arg2) of
-                                                          ((tf, []), (domR, []), (arg1, []),
-                                                           ((L'.CRecord (_, []), _), [])) =>
-                                                          let
-                                                              val t = (L'.CApp (tf, arg1), loc)
-                                                              val t = (L'.CApp (t, arg2), loc)
-                                                              val t = (L'.CApp (t, arg3), loc)
-                                                          in
-                                                              (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, loc),
-                                                                                          t),
-                                                                                 loc)), loc)
-                                                          end
+                                            ((L'.CApp (tf, arg), _), [])) =>
+                                           (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg) of
+                                                (((L'.CModProj (basis, [], "transaction"), _), []),
+                                                 ((L'.CApp (tf, arg3), _), [])) =>
+                                                (case (basis = !basis_r,
+                                                       hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of
+                                                     (true,
+                                                      ((L'.CApp (tf, arg2), _), []),
+                                                      (((L'.CRecord (_, []), _), []))) =>
+                                                     (case (hnormCon (env, denv) tf) of
+                                                          ((L'.CApp (tf, arg1), _), []) =>
+                                                          (case (hnormCon (env, denv) tf,
+                                                                 hnormCon (env, denv) domR,
+                                                                 hnormCon (env, denv) arg1,
+                                                                 hnormCon (env, denv) arg2) of
+                                                               ((tf, []), (domR, []), (arg1, []),
+                                                                ((L'.CRecord (_, []), _), [])) =>
+                                                               let
+                                                                   val t = (L'.CApp (tf, arg1), loc)
+                                                                   val t = (L'.CApp (t, arg2), loc)
+                                                                   val t = (L'.CApp (t, arg3), loc)
+                                                                   val t = (L'.CApp (
+                                                                            (L'.CModProj (basis, [], "transaction"), loc),
+                                                                            t), loc)
+                                                               in
+                                                                   (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, loc),
+                                                                                               t),
+                                                                                      loc)), loc)
+                                                               end
+                                                             | _ => all)
                                                         | _ => all)
                                                    | _ => all)
                                               | _ => all)
--- a/tests/query.ur	Sun Aug 31 09:05:33 2008 -0400
+++ b/tests/query.ur	Sun Aug 31 09:45:23 2008 -0400
@@ -9,8 +9,14 @@
         (fn fs _ acc => return (Cons (fs.T1, acc)))
         Nil
 
-val r2 : transaction int =
+val r2 : transaction string =
         ls <- r1;
         return (case ls of
-                    Nil => 0
-                  | Cons ({A = a, ...}, _) => a)
+                    Nil => "Problem"
+                  | Cons ({B = b, ...}, _) => b)
+
+val main : unit -> transaction page = fn () =>
+        s <- r2;
+        return <html><body>
+                {cdata s}
+        </body></html>