Datatype representation optimization

1 files changed, 594 insertions, 590 deletions

diff --git a/src/corify.sml b/src/corify.sml
index 146868e6..7e2f2493 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -62,7 +62,7 @@ structure St : sig
 
     val enter : t -> t
     val leave : t -> {outer : t, inner : t}
-    val ffi : string -> L'.con SM.map -> (string * L'.con option) SM.map -> t
+    val ffi : string -> L'.con SM.map -> (string * L'.con option * L'.datatype_kind) SM.map -> t
 
     datatype core_con =
              CNormal of int
@@ -76,605 +76,609 @@ structure St : sig
     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
-
-    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
-
-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 * L'.con option) SM.map}
-                           
-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 = {
-    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"
-
-datatype core_con =
-         CNormal of int
-       | CFfi of string
-
-datatype core_val =
-         ENormal of int
-       | EFfi of string * L'.con
-
-fun bindCon {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 = SM.insert (cons, s, n'),
-                         constructors = constructors,
-                         vals = vals,
-                         strs = strs,
-                         funs = funs}
-    in
-        ({cons = IM.insert (cons, n, n'),
+     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 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 * L'.con option * L'.datatype_kind) SM.map}
+
+ 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 = {
+     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"
+
+ datatype core_con =
+          CNormal of int
+        | CFfi of string
+
+ datatype core_val =
+          ENormal of int
+        | EFfi of string * L'.con
+
+ fun bindCon {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 = 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 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,
           constructors = constructors,
-          vals = vals,
+          vals = IM.insert (vals, n, n),
           strs = strs,
           funs = funs,
           current = current,
-          nested = nested},
-         n')
-    end
-
-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'),
+          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},
-         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,
-         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
-
-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
+          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, to, dk) => SOME (L'.PConFfi {mod = m, datatyp = n, con = x, arg = to, kind = dk}))
+       | FNormal {constructors, ...} =>
+         case SM.find (constructors, x) of
              NONE => NONE
-           | SOME (n, to) => SOME (L'.PConFfi {mod = m, datatyp = n, con = x, arg = to}))
-      | 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, to) => L'.PConFfi {mod = m, datatyp = n, con = x, arg = to})
-      | 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 dummy f = {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 ffi m vals constructors = dummy (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 lookupStrById ({strs, ...} : t) n =
-    case IM.find (strs, n) of
-        NONE => raise Fail "Corify.St.lookupStrById"
-      | SOME f => dummy 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 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 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"
-
-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)
-
-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.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc)
-      | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc)
-
-      | L.CName s => (L'.CName s, loc)
-
-      | L.CRecord (k, xcs) =>
-        (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon 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)
-
-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 (pc, po) => (L'.PCon (corifyPatCon st pc, 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, arg, ...}) =>
-                (case arg of
-                     NONE => (L'.ECon (pc, NONE), loc)
-                   | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc),
-                                           (L'.ECon (pc, SOME (L'.ERel 0, loc)), loc)), loc))
-              | _ =>
-                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 (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.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)
-
-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, 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 t = (L'.CNamed n, loc)
-            val dcons = map (fn (x, n, to) =>
-                                let
-                                    val (e, t) =
-                                        case to of
-                                            NONE => ((L'.ECon (L'.PConVar n, NONE), loc), t)
-                                          | SOME t' => ((L'.EAbs ("x", t', t,
-                                                                  (L'.ECon (L'.PConVar n, SOME (L'.ERel 0, loc)), loc)),
-                                                         loc),
-                                                        (L'.TFun (t', t), loc))
-                                in
-                                    (L'.DVal (x, n, t, e, ""), loc)
-                                end) xncs
-        in
-            ((L'.DDatatype (x, n, xncs), loc) :: dcons, st)
-        end
-      | L.DDatatypeImp (x, n, m1, ms, s, 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 (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 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)
-                              in
-                                  (L'.DVal (x, n, t, e, x), loc)
-                              end) xncs
-        in
-            ((L'.DCon (x, n, (L'.KType, loc), 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) =>
+           | 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, to, dk) => L'.PConFfi {mod = m, datatyp = n, 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 dummy f = {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 ffi m vals constructors = dummy (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 lookupStrById ({strs, ...} : t) n =
+     case IM.find (strs, n) of
+         NONE => raise Fail "Corify.St.lookupStrById"
+       | SOME f => dummy 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 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 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"
+
+ 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)
+
+ 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.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc)
+       | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc)
+
+       | L.CName s => (L'.CName s, loc)
+
+       | L.CRecord (k, xcs) =>
+         (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon 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)
+
+ 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, po) => (L'.PCon (dk, corifyPatCon st pc, 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, arg, kind, ...}) =>
+                 (case arg of
+                      NONE => (L'.ECon (kind, pc, NONE), loc)
+                    | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc),
+                                            (L'.ECon (kind, pc, SOME (L'.ERel 0, loc)), loc)), loc))
+               | _ =>
+                 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 (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.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)
+
+ 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, 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 = CoreUtil.classifyDatatype xncs
+             val t = (L'.CNamed n, loc)
+             val dcons = map (fn (x, n, to) =>
+                                 let
+                                     val (e, t) =
+                                         case to of
+                                             NONE => ((L'.ECon (dk, L'.PConVar n, NONE), loc), t)
+                                           | SOME t' => ((L'.EAbs ("x", t', t,
+                                                                   (L'.ECon (dk, L'.PConVar n, SOME (L'.ERel 0, loc)),
+                                                                    loc)),
+                                                          loc),
+                                                         (L'.TFun (t', t), loc))
+                                 in
+                                     (L'.DVal (x, n, t, e, ""), loc)
+                                 end) xncs
+         in
+             ((L'.DDatatype (x, n, xncs), loc) :: dcons, st)
+         end
+       | L.DDatatypeImp (x, n, m1, ms, s, 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 (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 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)
+                               in
+                                   (L'.DVal (x, n, t, e, x), loc)
+                               end) xncs
+         in
+             ((L'.DCon (x, n, (L'.KType, loc), 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)
+
+       | 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.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.bindVal st x n
+                                        val (st, n') = St.bindCon 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)
-
-      | 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.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'.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, xnts) =>
-                                   let
-                                       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 to = Option.map (corifyCon st) to
-
-                                                       val pc = L'.PConFfi {mod = m,
-                                                                            datatyp = x,
-                                                                            con = x',
-                                                                            arg = to}
-
-                                                       val (cmap, d) =
-                                                           case to of
-                                                               NONE => (SM.insert (cmap, x', dt),
-                                                                        (L'.DVal (x', n, dt,
-                                                                                  (L'.ECon (pc, NONE), loc),
-                                                                                  ""), loc))
-                                                             | SOME t =>
-                                                               let
-                                                                   val tf = (L'.TFun (t, dt), loc)
-                                                                   val d = (L'.DVal (x', n, tf,
-                                                                                     (L'.EAbs ("x", t, tf,
-                                                                                               (L'.ECon (pc,
-                                                                                                         SOME (L'.ERel 0,
+                                  | L.SgiDatatype (x, n, xnts) =>
+                                    let
+                                        val dk = ExplUtil.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 to = Option.map (corifyCon st) to
+
+                                                        val pc = L'.PConFfi {mod = m,
+                                                                             datatyp = x,
+                                                                             con = x',
+                                                                             arg = to,
+                                                                             kind = dk}
+
+                                                        val (cmap, d) =
+                                                            case to of
+                                                                NONE => (SM.insert (cmap, x', dt),
+                                                                         (L'.DVal (x', n, dt,
+                                                                                   (L'.ECon (dk, pc, NONE), loc),
+                                                                                   ""), loc))
+                                                              | SOME t =>
+                                                                let
+                                                                    val tf = (L'.TFun (t, dt), loc)
+                                                                    val d = (L'.DVal (x', n, tf,
+                                                                                      (L'.EAbs ("x", t, tf,
+                                                                                                (L'.ECon (dk, pc,
+                                                                                                          SOME (L'.ERel 0,
                                                                                                                loc)),
                                                                                                 loc)), loc), ""), loc)
                                                                in
@@ -684,7 +688,7 @@ fun corifyDecl ((d, loc : EM.span), st) =
                                                        val st = St.bindConstructor st x' n pc
                                                        (*val st = St.bindConstructorVal st x' n*)
 
-                                                       val conmap = SM.insert (conmap, x', (x, to))
+                                                       val conmap = SM.insert (conmap, x', (x, to, dk))
                                                    in
                                                        ((x', n, to),
                                                         (d :: ds', st, cmap, conmap))