changeset 188:8e9f97508f0d

Datatype representation optimization
author Adam Chlipala <adamc@hcoop.net>
date Sun, 03 Aug 2008 19:49:21 -0400
parents fb6ed259f5bd
children 20bf7487c370
files src/cjr.sml src/cjr_env.sig src/cjr_env.sml src/cjr_print.sml src/cjrize.sml src/core.sml src/core_print.sml src/core_util.sig src/core_util.sml src/corify.sml src/elab.sml src/elab_env.sig src/elab_env.sml src/elab_print.sml src/elab_util.sig src/elab_util.sml src/elaborate.sml src/expl.sml src/expl_print.sml src/expl_util.sig src/expl_util.sml src/explify.sml src/mono.sml src/mono_env.sml src/mono_opt.sml src/mono_print.sml src/mono_reduce.sml src/mono_shake.sml src/mono_util.sig src/mono_util.sml src/monoize.sml
diffstat 31 files changed, 790 insertions(+), 681 deletions(-) [+]
line wrap: on
line diff
--- a/src/cjr.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/cjr.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -29,11 +29,13 @@
 
 type 'a located = 'a ErrorMsg.located
 
+datatype datatype_kind = datatype Mono.datatype_kind
+
 datatype typ' =
          TTop
        | TFun of typ * typ
        | TRecord of int
-       | TDatatype of int * (string * int * typ option) list
+       | TDatatype of datatype_kind * int * (string * int * typ option) list
        | TFfi of string * string
 
 withtype typ = typ' located
@@ -46,7 +48,7 @@
          PWild
        | PVar of string * typ
        | PPrim of Prim.t
-       | PCon of patCon * pat option
+       | PCon of datatype_kind * patCon * pat option
        | PRecord of (string * pat * typ) list
 
 withtype pat = pat' located
@@ -55,7 +57,7 @@
          EPrim of Prim.t
        | ERel of int
        | ENamed of int
-       | ECon of patCon * exp option
+       | ECon of datatype_kind * patCon * exp option
        | EFfi of string * string
        | EFfiApp of string * string * exp list
        | EApp of exp * exp
@@ -72,7 +74,7 @@
 
 datatype decl' =
          DStruct of int * (string * typ) list
-       | DDatatype of string * int * (string * int * typ option) list
+       | DDatatype of datatype_kind * string * int * (string * int * typ option) list
        | DVal of string * int * typ * exp
        | DFun of string * int * (string * typ) list * typ * exp
        | DFunRec of (string * int * (string * typ) list * typ * exp) list
--- a/src/cjr_env.sig	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/cjr_env.sig	Sun Aug 03 19:49:21 2008 -0400
@@ -53,5 +53,7 @@
     val lookupStruct : env -> int -> (string * Cjr.typ) list
 
     val declBinds : env -> Cjr.decl -> env
+
+    val classifyDatatype : (string * int * Cjr.typ option) list -> Cjr.datatype_kind
                                                  
 end
--- a/src/cjr_env.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/cjr_env.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -129,14 +129,21 @@
         NONE => raise UnboundStruct n
       | SOME x => x
 
+fun classifyDatatype xncs =
+    if List.all (fn (_, _, NONE) => true | _ => false) xncs then
+        Enum
+    else
+        Default
+
 fun declBinds env (d, loc) =
     case d of
-        DDatatype (x, n, xncs) =>
+        DDatatype (_, x, n, xncs) =>
         let
             val env = pushDatatype env x n xncs
+            val dt = (TDatatype (classifyDatatype xncs, n, xncs), loc)
         in
-            foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (TDatatype (n, xncs), loc)
-                    | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (TDatatype (n, xncs), loc)), loc))
+            foldl (fn ((x', n', NONE), env) => pushENamed env x' n' dt
+                    | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, dt), loc))
             env xncs
         end
       | DStruct (n, xts) => pushStruct env n xts
--- a/src/cjr_print.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/cjr_print.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -53,7 +53,7 @@
 
 val debug = ref false
 
-val dummyTyp = (TDatatype (0, []), ErrorMsg.dummySpan)
+val dummyTyp = (TDatatype (Enum, 0, []), ErrorMsg.dummySpan)
 
 fun p_typ' par env (t, loc) =
     case t of
@@ -69,7 +69,12 @@
                           space,
                           string "__lws_",
                           string (Int.toString i)]
-      | TDatatype (n, _) =>
+      | TDatatype (Enum, n, _) =>
+        (box [string "enum",
+              space,
+              string ("__lwe_" ^ #1 (E.lookupDatatype env n) ^ "_" ^ Int.toString n)]
+         handle CjrEnv.UnboundNamed _ => string ("__lwd_UNBOUND__" ^ Int.toString n))
+      | TDatatype (Default, n, _) =>
         (box [string "struct",
               space,
               string ("__lwd_" ^ #1 (E.lookupDatatype env n) ^ "_" ^ Int.toString n ^ "*")]
@@ -103,8 +108,8 @@
                              newline],
                         env)
       | PPrim _ => (box [], env)
-      | PCon (_, NONE) => (box [], env)
-      | PCon (_, SOME p) => p_pat_preamble env p
+      | PCon (_, _, NONE) => (box [], env)
+      | PCon (_, _, SOME p) => p_pat_preamble env p
       | PRecord xps =>
         foldl (fn ((_, p, _), (pp, env)) =>
                   let
@@ -161,7 +166,7 @@
          env)
       | PPrim _ => raise Fail "CjrPrint: Disallowed PPrim primitive"
 
-      | PCon (pc, po) =>
+      | PCon (dk, pc, po) =>
         let
             val (p, env) =
                 case po of
@@ -175,9 +180,10 @@
                                           let
                                               val (x, to, _) = E.lookupConstructor env n
                                           in
-                                              (x, to)
+                                              ("__lwc_" ^ x, to)
                                           end
-                                        | PConFfi _ => raise Fail "PConFfi"
+                                        | PConFfi {mod = m, con, arg, ...} =>
+                                          ("lw_" ^ m ^ "_" ^ con, arg)
 
                         val t = case to of
                                     NONE => raise Fail "CjrPrint: Constructor mismatch"
@@ -194,7 +200,7 @@
                               space,
                               string "disc",
                               string (Int.toString depth),
-                              string "->data.__lwc_",
+                              string "->data.",
                               string x,
                               string ";",
                               newline,
@@ -208,7 +214,9 @@
                   space,
                   string "(disc",
                   string (Int.toString depth),
-                  string "->tag",
+                  case dk of
+                      Enum => box []
+                    | Default => string "->tag",
                   space,
                   string "!=",
                   space,
@@ -285,7 +293,8 @@
         EPrim p => Prim.p_t p
       | ERel n => p_rel env n
       | ENamed n => p_enamed env n
-      | ECon (pc, eo) =>
+      | ECon (Enum, pc, _) => p_patCon env pc
+      | ECon (Default, pc, eo) =>
         let
             val (xd, xc) = patConInfo env pc
         in
@@ -497,7 +506,17 @@
                                                     string ";",
                                                     newline]) xts,
              string "};"]
-      | DDatatype (x, n, xncs) =>
+      | DDatatype (Enum, x, n, xncs) =>
+        box [string "enum",
+             space,
+             string ("__lwe_" ^ x ^ "_" ^ Int.toString n),
+             space,
+             string "{",
+             space,
+             p_list_sep (box [string ",", space]) (fn (x, n, _) => string ("__lwc_" ^ x ^ "_" ^ Int.toString n)) xncs,
+             space,
+             string "};"]
+      | DDatatype (Default, x, n, xncs) =>
         let
             val xncsArgs = List.mapPartial (fn (x, n, NONE) => NONE
                                              | (x, n, SOME t) => SOME (x, n, t)) xncs
@@ -541,7 +560,7 @@
                                 string "data;",
                                 newline]),
                  string "};"]
-        end                 
+        end
 
       | DVal (x, n, t, e) =>
         box [p_typ env t,
@@ -753,7 +772,34 @@
                          string "})"]
                 end
 
-              | TDatatype (i, _) =>
+              | TDatatype (Enum, i, _) =>
+                let
+                    val (x, xncs) = E.lookupDatatype env i
+
+                    fun doEm xncs =
+                        case xncs of
+                            [] => string ("(lw_error(ctx, FATAL, \"Error unurlifying datatype " ^ x ^ "\"), (enum __lwe_"
+                                          ^ x ^ "_" ^ Int.toString i ^ ")0)")
+                          | (x', n, to) :: rest =>
+                            box [string "((!strncmp(request, \"",
+                                 string x',
+                                 string "\", ",
+                                 string (Int.toString (size x')),
+                                 string ") && (request[",
+                                 string (Int.toString (size x')),
+                                 string "] == 0 || request[",
+                                 string (Int.toString (size x')),
+                                 string ("] == '/')) ? __lwc_" ^ x' ^ "_" ^ Int.toString n),
+                                 space,
+                                 string ":",
+                                 space,
+                                 doEm rest,
+                                 string ")"]
+                in
+                    doEm xncs
+                end
+
+              | TDatatype (Default, i, _) =>
                 let
                     val (x, xncs) = E.lookupDatatype env i
 
--- a/src/cjrize.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/cjrize.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -84,7 +84,7 @@
         in
             ((L'.TRecord si, loc), sm)
         end
-      | L.TDatatype (n, xncs) =>
+      | L.TDatatype (dk, n, xncs) =>
         let
             val (xncs, sm) = ListUtil.foldlMap (fn ((x, n, to), sm) =>
                                                    case to of
@@ -97,7 +97,7 @@
                                                        end)
                              sm xncs
         in
-            ((L'.TDatatype (n, xncs), loc), sm)
+            ((L'.TDatatype (dk, n, xncs), loc), sm)
         end
       | L.TFfi mx => ((L'.TFfi mx, loc), sm)
 
@@ -131,18 +131,18 @@
             ((L'.PVar (x, t), loc), sm)
         end
       | L.PPrim p => ((L'.PPrim p, loc), sm)
-      | L.PCon (pc, NONE) =>
+      | L.PCon (dk, pc, NONE) =>
         let
             val (pc, sm) = cifyPatCon (pc, sm)
         in
-            ((L'.PCon (pc, NONE), loc), sm)
+            ((L'.PCon (dk, pc, NONE), loc), sm)
         end
-      | L.PCon (pc, SOME p) =>
+      | L.PCon (dk, pc, SOME p) =>
         let
             val (pc, sm) = cifyPatCon (pc, sm)
             val (p, sm) = cifyPat (p, sm)
         in
-            ((L'.PCon (pc, SOME p), loc), sm)
+            ((L'.PCon (dk, pc, SOME p), loc), sm)
         end
       | L.PRecord xps =>
         let
@@ -162,7 +162,7 @@
         L.EPrim p => ((L'.EPrim p, loc), sm)
       | L.ERel n => ((L'.ERel n, loc), sm)
       | L.ENamed n => ((L'.ENamed n, loc), sm)
-      | L.ECon (pc, eo) =>
+      | L.ECon (dk, pc, eo) =>
         let
             val (eo, sm) =
                 case eo of
@@ -175,7 +175,7 @@
                     end
             val (pc, sm) = cifyPatCon (pc, sm)
         in
-            ((L'.ECon (pc, eo), loc), sm)
+            ((L'.ECon (dk, pc, eo), loc), sm)
         end
       | L.EFfi mx => ((L'.EFfi mx, loc), sm)
       | L.EFfiApp (m, x, es) =>
@@ -268,6 +268,7 @@
     case d of
         L.DDatatype (x, n, xncs) =>
         let
+            val dk = MonoUtil.classifyDatatype xncs
             val (xncs, sm) = ListUtil.foldlMap (fn ((x, n, to), sm) =>
                                                    case to of
                                                        NONE => ((x, n, NONE), sm)
@@ -278,7 +279,7 @@
                                                            ((x, n, SOME t), sm)
                                                        end) sm xncs
         in
-            (SOME (L'.DDatatype (x, n, xncs), loc), NONE, sm)
+            (SOME (L'.DDatatype (dk, x, n, xncs), loc), NONE, sm)
         end
 
       | L.DVal (x, n, t, e, _) =>
--- a/src/core.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/core.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -59,15 +59,17 @@
 
 withtype con = con' located
 
+datatype datatype_kind = datatype Elab.datatype_kind
+
 datatype patCon =
          PConVar of int
-       | PConFfi of {mod : string, datatyp : string, con : string, arg : con option}
+       | PConFfi of {mod : string, datatyp : string, con : string, arg : con option, kind : datatype_kind}
 
 datatype pat' =
          PWild
        | PVar of string * con
        | PPrim of Prim.t
-       | PCon of patCon * pat option
+       | PCon of datatype_kind * patCon * pat option
        | PRecord of (string * pat * con) list
 
 withtype pat = pat' located
@@ -76,7 +78,7 @@
          EPrim of Prim.t
        | ERel of int
        | ENamed of int
-       | ECon of patCon * exp option
+       | ECon of datatype_kind * patCon * exp option
        | EFfi of string * string
        | EFfiApp of string * string * exp list
        | EApp of exp * exp
--- a/src/core_print.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/core_print.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -173,10 +173,10 @@
         PWild => string "_"
       | PVar (s, _) => string s
       | PPrim p => Prim.p_t p
-      | PCon (n, NONE) => p_patCon env n
-      | PCon (n, SOME p) => parenIf par (box [p_patCon env n,
-                                              space,
-                                              p_pat' true env p])
+      | PCon (_, n, NONE) => p_patCon env n
+      | PCon (_,n, SOME p) => parenIf par (box [p_patCon env n,
+                                                space,
+                                                p_pat' true env p])
       | PRecord xps =>
         box [string "{",
              p_list_sep (box [string ",", space]) (fn (x, p, _) =>
@@ -199,10 +199,10 @@
               string (#1 (E.lookupERel env n)))
          handle E.UnboundRel _ => string ("UNBOUND_" ^ Int.toString n))
       | ENamed n => p_enamed env n
-      | ECon (pc, NONE) => p_patCon env pc
-      | ECon (pc, SOME e) => parenIf par (box [p_patCon env pc,
-                                              space,
-                                              p_exp' true env e])
+      | ECon (_, pc, NONE) => p_patCon env pc
+      | ECon (_, pc, SOME e) => parenIf par (box [p_patCon env pc,
+                                                  space,
+                                                  p_exp' true env e])
       | EFfi (m, x) => box [string "FFI(", string m, string ".", string x, string ")"]
       | EFfiApp (m, x, es) => box [string "FFI(",
                                    string m,
--- a/src/core_util.sig	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/core_util.sig	Sun Aug 03 19:49:21 2008 -0400
@@ -27,6 +27,8 @@
 
 signature CORE_UTIL = sig
 
+val classifyDatatype : (string * int * Core.con option) list -> Core.datatype_kind
+
 structure Kind : sig
     val mapfold : (Core.kind', 'state, 'abort) Search.mapfolder
                   -> (Core.kind, 'state, 'abort) Search.mapfolder
--- a/src/core_util.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/core_util.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -29,6 +29,12 @@
 
 open Core
 
+fun classifyDatatype xncs =
+    if List.all (fn (_, _, NONE) => true | _ => false) xncs then
+        Enum
+    else
+        Default
+
 structure S = Search
 
 structure Kind = struct
@@ -227,11 +233,11 @@
                 EPrim _ => S.return2 eAll
               | ERel _ => S.return2 eAll
               | ENamed _ => S.return2 eAll
-              | ECon (_, NONE) => S.return2 eAll
-              | ECon (n, SOME e) =>
+              | ECon (_, _, NONE) => S.return2 eAll
+              | ECon (dk, n, SOME e) =>
                 S.map2 (mfe ctx e,
                         fn e' =>
-                           (ECon (n, SOME e'), loc))
+                           (ECon (dk, n, SOME e'), loc))
               | EFfi _ => S.return2 eAll
               | EFfiApp (m, x, es) =>
                 S.map2 (ListUtil.mapfold (fn e => mfe ctx e) es,
--- a/src/corify.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/corify.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -62,7 +62,7 @@
 
     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 @@
     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 * 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
-}
+ 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}
 
-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 = []
-}
+ 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
+ }
 
-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"
+ 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 = []
+ }
 
-datatype core_con =
-         CNormal of int
-       | CFfi of string
+ 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_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'),
+ 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 = 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},
-         n')
-    end
+          nested = nested}
+     end
 
-fun lookupConById ({cons, ...} : t) n = IM.find (cons, n)
+ fun lookupConstructorById ({constructors, ...} : t) n =
+     case IM.find (constructors, n) of
+         NONE => raise Fail "Corify.St.lookupConstructorById"
+       | SOME x => x
 
-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 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 => SOME n
 
-fun bindVal {cons, constructors, vals, strs, funs, current, nested} s n =
-    let
-        val n' = alloc ()
+ 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
 
-        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 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 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 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 lookupValById ({vals, ...} : t) n = IM.find (vals, n)
+ fun ffi m vals constructors = dummy (FFfi {mod = m, vals = vals, constructors = constructors})
 
-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 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 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 lookupStrById ({strs, ...} : t) n =
+     case IM.find (strs, n) of
+         NONE => raise Fail "Corify.St.lookupStrById"
+       | SOME f => dummy f
 
-fun lookupConstructorById ({constructors, ...} : t) n =
-    case IM.find (constructors, n) of
-        NONE => raise Fail "Corify.St.lookupConstructorById"
-      | SOME x => x
+ 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 lookupConstructorByNameOpt ({current, ...} : t) x =
-    case current of
-        FFfi {mod = m, 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 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 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 lookupFunctorById ({funs, ...} : t) n =
+     case IM.find (funs, n) of
+         NONE => raise Fail "Corify.St.lookupFunctorById"
+       | SOME v => v
 
-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 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 dummy f = {cons = IM.empty,
-               constructors = IM.empty,
-               vals = IM.empty,
-               strs = IM.empty,
-               funs = IM.empty,
-               current = f,
-               nested = []}
+ end
 
-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 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 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 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 lookupStrById ({strs, ...} : t) n =
-    case IM.find (strs, n) of
-        NONE => raise Fail "Corify.St.lookupStrById"
-      | SOME f => dummy f
+       | 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
 
-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"
+       | 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)
 
-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"
+       | L.CName s => (L'.CName s, loc)
 
-fun lookupFunctorById ({funs, ...} : t) n =
-    case IM.find (funs, n) of
-        NONE => raise Fail "Corify.St.lookupFunctorById"
-      | SOME v => v
+       | 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 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 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
 
-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)
 
-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)
+                             val (result, args) = getArgs (t, [])
 
-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)
+                             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.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.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.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.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.CName s => (L'.CName s, loc)
+       | L.EWrite e => (L'.EWrite (corifyExp st e), 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 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
 
-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
+             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)
 
-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)
+             val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms
+             val (_, {inner, ...}) = corifyStr (m, st)
 
-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 (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 (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 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
 
-      | 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)
+             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.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.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) =>
+         ([], St.bindFunctor st x n xa na str)
 
-      | L.EWrite e => (L'.EWrite (corifyExp st e), loc)
+       | 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
 
-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
+       | 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
 
-            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)
+                                  | 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 m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms
-            val (_, {inner, ...}) = corifyStr (m, st)
+                                                        val to = Option.map (corifyCon st) to
 
-            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 pc = L'.PConFfi {mod = m,
+                                                                             datatyp = x,
+                                                                             con = x',
+                                                                             arg = to,
+                                                                             kind = dk}
 
-            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.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,
+                                                        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 @@
                                                        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))
--- a/src/elab.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/elab.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -71,6 +71,10 @@
 
 withtype con = con' located
 
+datatype datatype_kind =
+         Enum
+       | Default
+
 datatype patCon =
          PConVar of int
        | PConProj of int * string list * string
@@ -79,7 +83,7 @@
          PWild
        | PVar of string * con
        | PPrim of Prim.t
-       | PCon of patCon * pat option
+       | PCon of datatype_kind * patCon * pat option
        | PRecord of (string * pat * con) list
 
 withtype pat = pat' located
--- a/src/elab_env.sig	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/elab_env.sig	Sun Aug 03 19:49:21 2008 -0400
@@ -57,7 +57,7 @@
     val lookupDatatypeConstructor : datatyp -> int -> string * Elab.con option
     val constructors : datatyp -> (string * int * Elab.con option) list
 
-    val lookupConstructor : env -> string -> (int * Elab.con option * int) option
+    val lookupConstructor : env -> string -> (Elab.datatype_kind * int * Elab.con option * int) option
 
     val pushERel : env -> string -> Elab.con -> env
     val lookupERel : env -> int -> string * Elab.con
@@ -89,7 +89,7 @@
     val projectDatatype : env -> { sgn : Elab.sgn, str : Elab.str, field : string }
                           -> (string * int * Elab.con option) list option
     val projectConstructor : env -> { sgn : Elab.sgn, str : Elab.str, field : string }
-                             -> (int * Elab.con option * Elab.con) option
+                             -> (Elab.datatype_kind * int * Elab.con option * Elab.con) option
     val projectVal : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.con option
     val projectSgn : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option
     val projectStr : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option
--- a/src/elab_env.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/elab_env.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -81,7 +81,7 @@
      namedC : (string * kind * con option) IM.map,
 
      datatypes : datatyp IM.map,
-     constructors : (int * con option * int) SM.map,
+     constructors : (datatype_kind * int * con option * int) SM.map,
 
      renameE : con var' SM.map,
      relE : (string * con) list,
@@ -189,26 +189,30 @@
       | SOME (Named' x) => Named x
 
 fun pushDatatype (env : env) n xncs =
-    {renameC = #renameC env,
-     relC = #relC env,
-     namedC = #namedC env,
+    let
+        val dk = U.classifyDatatype xncs
+    in
+        {renameC = #renameC env,
+         relC = #relC env,
+         namedC = #namedC env,
 
-     datatypes = IM.insert (#datatypes env, n,
-                            foldl (fn ((x, n, to), cons) =>
-                                      IM.insert (cons, n, (x, to))) IM.empty xncs),
-     constructors = foldl (fn ((x, n', to), cmap) =>
-                              SM.insert (cmap, x, (n', to, n)))
-                          (#constructors env) xncs,
+         datatypes = IM.insert (#datatypes env, n,
+                                foldl (fn ((x, n, to), cons) =>
+                                          IM.insert (cons, n, (x, to))) IM.empty xncs),
+         constructors = foldl (fn ((x, n', to), cmap) =>
+                                  SM.insert (cmap, x, (dk, n', to, n)))
+                              (#constructors env) xncs,
 
-     renameE = #renameE env,
-     relE = #relE env,
-     namedE = #namedE env,
+         renameE = #renameE env,
+         relE = #relE env,
+         namedE = #namedE env,
 
-     renameSgn = #renameSgn env,
-     sgn = #sgn env,
+         renameSgn = #renameSgn env,
+         sgn = #sgn env,
 
-     renameStr = #renameStr env,
-     str = #str env}
+         renameStr = #renameStr env,
+         str = #str env}
+    end
 
 fun lookupDatatype (env : env) n =
     case IM.find (#datatypes env, n) of
@@ -579,13 +583,14 @@
                                     if x <> field then
                                         NONE
                                     else
-                                        SOME (n', to, (CNamed n, #2 str))) xncs
+                                        SOME (U.classifyDatatype xncs, n', to, (CNamed n, #2 str))) xncs
         in
             case sgnSeek (fn SgiDatatype (_, n, xncs) => consider (n, xncs)
                            | SgiDatatypeImp (_, n, _, _, _, xncs) => consider (n, xncs)
                            | _ => NONE) sgis of
                 NONE => NONE
-              | SOME ((n, to, t), subs) => SOME (n, Option.map (sgnSubCon (str, subs)) to, sgnSubCon (str, subs) t)
+              | SOME ((dk, n, to, t), subs) => SOME (dk, n, Option.map (sgnSubCon (str, subs)) to,
+                                                     sgnSubCon (str, subs) t)
         end
       | _ => NONE
 
--- a/src/elab_print.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/elab_print.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -216,10 +216,10 @@
         PWild => string "_"
       | PVar (s, _) => string s
       | PPrim p => Prim.p_t p
-      | PCon (pc, NONE) => p_patCon env pc
-      | PCon (pc, SOME p) => parenIf par (box [p_patCon env pc,
-                                               space,
-                                               p_pat' true env p])
+      | PCon (_, pc, NONE) => p_patCon env pc
+      | PCon (_, pc, SOME p) => parenIf par (box [p_patCon env pc,
+                                                  space,
+                                                  p_pat' true env p])
       | PRecord xps =>
         box [string "{",
              p_list_sep (box [string ",", space]) (fn (x, p, _) =>
--- a/src/elab_util.sig	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/elab_util.sig	Sun Aug 03 19:49:21 2008 -0400
@@ -27,6 +27,8 @@
 
 signature ELAB_UTIL = sig
 
+val classifyDatatype : (string * int * Elab.con option) list -> Elab.datatype_kind
+
 structure Kind : sig
     val mapfold : (Elab.kind', 'state, 'abort) Search.mapfolder
                   -> (Elab.kind, 'state, 'abort) Search.mapfolder
--- a/src/elab_util.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/elab_util.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -29,6 +29,12 @@
 
 open Elab
 
+fun classifyDatatype xncs =
+    if List.all (fn (_, _, NONE) => true | _ => false) xncs then
+        Enum
+    else
+        Default
+
 structure S = Search
 
 structure Kind = struct
--- a/src/elaborate.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/elaborate.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -933,22 +933,21 @@
         val pterror = (perror, terror)
         val rerror = (pterror, (env, bound))
 
-        fun pcon (pc, po, to, dn) =
-
-                case (po, to) of
-                    (NONE, SOME _) => (expError env (PatHasNoArg loc);
-                                       rerror)
-                  | (SOME _, NONE) => (expError env (PatHasArg loc);
-                                       rerror)
-                  | (NONE, NONE) => (((L'.PCon (pc, NONE), loc), dn),
-                                     (env, bound))
-                  | (SOME p, SOME t) =>
-                    let
-                        val ((p', pt), (env, bound)) = elabPat (p, (env, denv, bound))
-                    in
-                        (((L'.PCon (pc, SOME p'), loc), dn),
-                         (env, bound))
-                    end
+        fun pcon (pc, po, to, dn, dk) =
+            case (po, to) of
+                (NONE, SOME _) => (expError env (PatHasNoArg loc);
+                                   rerror)
+              | (SOME _, NONE) => (expError env (PatHasArg loc);
+                                   rerror)
+              | (NONE, NONE) => (((L'.PCon (dk, pc, NONE), loc), dn),
+                                 (env, bound))
+              | (SOME p, SOME t) =>
+                let
+                    val ((p', pt), (env, bound)) = elabPat (p, (env, denv, bound))
+                in
+                    (((L'.PCon (dk, pc, SOME p'), loc), dn),
+                     (env, bound))
+                end
     in
         case p of
             L.PWild => (((L'.PWild, loc), cunif (loc, (L'.KType, loc))),
@@ -970,7 +969,7 @@
             (case E.lookupConstructor env x of
                  NONE => (expError env (UnboundConstructor (loc, [], x));
                           rerror)
-               | SOME (n, to, dn) => pcon (L'.PConVar n, po, to, (L'.CNamed dn, loc)))
+               | SOME (dk, n, to, dn) => pcon (L'.PConVar n, po, to, (L'.CNamed dn, loc), dk))
           | L.PCon (m1 :: ms, x, po) =>
             (case E.lookupStr env m1 of
                  NONE => (expError env (UnboundStrInExp (loc, m1));
@@ -986,7 +985,7 @@
                      case E.projectConstructor env {str = str, sgn = sgn, field = x} of
                          NONE => (expError env (UnboundConstructor (loc, m1 :: ms, x));
                                   rerror)
-                       | SOME (_, to, dn) => pcon (L'.PConProj (n, ms, x), po, to, dn)
+                       | SOME (dk, _, to, dn) => pcon (L'.PConProj (n, ms, x), po, to, dn, dk)
                  end)
 
           | L.PRecord (xps, flex) =>
@@ -1036,7 +1035,7 @@
                 in
                     case E.projectConstructor env {str = str, sgn = sgn, field = x} of
                         NONE => raise Fail "exhaustive: Can't project constructor"
-                      | SOME (n, _, _) => n
+                      | SOME (_, n, _, _) => n
                 end
 
         fun coverage (p, _) =
@@ -1044,8 +1043,8 @@
                 L'.PWild => Wild
               | L'.PVar _ => Wild
               | L'.PPrim _ => None
-              | L'.PCon (pc, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild))
-              | L'.PCon (pc, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p))
+              | L'.PCon (_, pc, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild))
+              | L'.PCon (_, pc, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p))
               | L'.PRecord xps => Record [foldl (fn ((x, p, _), fmap) =>
                                                     SM.insert (fmap, x, coverage p)) SM.empty xps]
 
--- a/src/expl.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/expl.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -59,6 +59,8 @@
 
 withtype con = con' located
 
+datatype datatype_kind = datatype Elab.datatype_kind
+
 datatype patCon =
          PConVar of int
        | PConProj of int * string list * string
@@ -67,7 +69,7 @@
          PWild
        | PVar of string * con
        | PPrim of Prim.t
-       | PCon of patCon * pat option
+       | PCon of datatype_kind * patCon * pat option
        | PRecord of (string * pat * con) list
 
 withtype pat = pat' located
--- a/src/expl_print.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/expl_print.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -181,10 +181,10 @@
         PWild => string "_"
       | PVar (s, _) => string s
       | PPrim p => Prim.p_t p
-      | PCon (pc, NONE) => p_patCon env pc
-      | PCon (pc, SOME p) => parenIf par (box [p_patCon env pc,
-                                               space,
-                                               p_pat' true env p])
+      | PCon (_, pc, NONE) => p_patCon env pc
+      | PCon (_, pc, SOME p) => parenIf par (box [p_patCon env pc,
+                                                  space,
+                                                  p_pat' true env p])
       | PRecord xps =>
         box [string "{",
              p_list_sep (box [string ",", space]) (fn (x, p, _) =>
--- a/src/expl_util.sig	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/expl_util.sig	Sun Aug 03 19:49:21 2008 -0400
@@ -27,6 +27,8 @@
 
 signature EXPL_UTIL = sig
 
+val classifyDatatype : (string * int * Expl.con option) list -> Expl.datatype_kind
+
 structure Kind : sig
     val mapfold : (Expl.kind', 'state, 'abort) Search.mapfolder
                   -> (Expl.kind, 'state, 'abort) Search.mapfolder
--- a/src/expl_util.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/expl_util.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -29,6 +29,12 @@
 
 open Expl
 
+fun classifyDatatype xncs =
+    if List.all (fn (_, _, NONE) => true | _ => false) xncs then
+        Enum
+    else
+        Default
+
 structure S = Search
 
 structure Kind = struct
--- a/src/explify.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/explify.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -81,7 +81,7 @@
         L.PWild => (L'.PWild, loc)
       | L.PVar (x, t) => (L'.PVar (x, explifyCon t), loc)
       | L.PPrim p => (L'.PPrim p, loc)
-      | L.PCon (pc, po) => (L'.PCon (explifyPatCon pc, Option.map explifyPat po), loc)
+      | L.PCon (dk, pc, po) => (L'.PCon (dk, explifyPatCon pc, Option.map explifyPat po), loc)
       | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, explifyPat p, explifyCon t)) xps), loc)
 
 fun explifyExp (e, loc) =
--- a/src/mono.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/mono.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -29,10 +29,12 @@
 
 type 'a located = 'a ErrorMsg.located
 
+datatype datatype_kind = datatype Core.datatype_kind
+
 datatype typ' =
          TFun of typ * typ
        | TRecord of (string * typ) list
-       | TDatatype of int * (string * int * typ option) list
+       | TDatatype of datatype_kind * int * (string * int * typ option) list
        | TFfi of string * string
 
 withtype typ = typ' located
@@ -45,7 +47,7 @@
          PWild
        | PVar of string * typ
        | PPrim of Prim.t
-       | PCon of patCon * pat option
+       | PCon of datatype_kind * patCon * pat option
        | PRecord of (string * pat * typ) list
 
 withtype pat = pat' located
@@ -54,7 +56,7 @@
          EPrim of Prim.t
        | ERel of int
        | ENamed of int
-       | ECon of patCon * exp option
+       | ECon of datatype_kind * patCon * exp option
        | EFfi of string * string
        | EFfiApp of string * string * exp list
        | EApp of exp * exp
--- a/src/mono_env.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/mono_env.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -98,9 +98,10 @@
         DDatatype (x, n, xncs) =>
         let
             val env = pushDatatype env x n xncs
+            val dt = (TDatatype (MonoUtil.classifyDatatype xncs, n, xncs), loc)
         in
-            foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (TDatatype (n, xncs), loc) NONE ""
-                    | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (TDatatype (n, xncs), loc)), loc) NONE "")
+            foldl (fn ((x', n', NONE), env) => pushENamed env x' n' dt NONE ""
+                    | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, dt), loc) NONE "")
             env xncs
         end
       | DVal (x, n, t, e, s) => pushENamed env x n t (SOME e) s
@@ -112,8 +113,8 @@
         PWild => env
       | PVar (x, t) => pushERel env x t NONE
       | PPrim _ => env
-      | PCon (_, NONE) => env
-      | PCon (_, SOME p) => patBinds env p
+      | PCon (_, _, NONE) => env
+      | PCon (_, _, SOME p) => patBinds env p
       | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps
 
 end
--- a/src/mono_opt.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/mono_opt.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -185,13 +185,13 @@
       | EWrite (EFfiApp ("Basis", "urlifyString", [e]), _) =>
         EFfiApp ("Basis", "urlifyString_w", [e])
 
-      | EFfiApp ("Basis", "urlifyBool", [(ECon (PConFfi {con = "True", ...}, NONE), _)]) =>
+      | EFfiApp ("Basis", "urlifyBool", [(ECon (Enum, PConFfi {con = "True", ...}, NONE), _)]) =>
         EPrim (Prim.String "1")
-      | EFfiApp ("Basis", "urlifyBool", [(ECon (PConFfi {con = "False", ...}, NONE), _)]) =>
+      | EFfiApp ("Basis", "urlifyBool", [(ECon (Enum, PConFfi {con = "False", ...}, NONE), _)]) =>
         EPrim (Prim.String "0")
-      | EWrite (EFfiApp ("Basis", "urlifyBool", [(ECon (PConFfi {con = "True", ...}, NONE), _)]), loc) =>
+      | EWrite (EFfiApp ("Basis", "urlifyBool", [(ECon (Enum, PConFfi {con = "True", ...}, NONE), _)]), loc) =>
         EWrite (EPrim (Prim.String "1"), loc)
-      | EWrite (EFfiApp ("Basis", "urlifyBool", [(ECon (PConFfi {con = "False", ...}, NONE), _)]), loc) =>
+      | EWrite (EFfiApp ("Basis", "urlifyBool", [(ECon (Enum, PConFfi {con = "False", ...}, NONE), _)]), loc) =>
         EWrite (EPrim (Prim.String "0"), loc)
       | EWrite (EFfiApp ("Basis", "urlifyBool", [e]), _) =>
         EFfiApp ("Basis", "urlifyBool_w", [e])
--- a/src/mono_print.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/mono_print.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -53,7 +53,7 @@
                                             space,
                                             p_typ env t]) xcs,
                             string "}"]
-      | TDatatype (n, _) =>
+      | TDatatype (_, n, _) =>
         ((if !debug then
               string (#1 (E.lookupDatatype env n) ^ "__" ^ Int.toString n)
           else
@@ -91,8 +91,8 @@
         PWild => string "_"
       | PVar (s, _) => string s
       | PPrim p => Prim.p_t p
-      | PCon (n, NONE) => p_patCon env n
-      | PCon (n, SOME p) => parenIf par (box [p_patCon env n,
+      | PCon (_, n, NONE) => p_patCon env n
+      | PCon (_, n, SOME p) => parenIf par (box [p_patCon env n,
                                               space,
                                               p_pat' true env p])
       | PRecord xps =>
@@ -117,10 +117,10 @@
               string (#1 (E.lookupERel env n)))
          handle E.UnboundRel _ => string ("UNBOUND_" ^ Int.toString n))
       | ENamed n => p_enamed env n
-      | ECon (pc, NONE) => p_patCon env pc
-      | ECon (pc, SOME e) => parenIf par (box [p_patCon env pc,
-                                               space,
-                                               p_exp' true env e])
+      | ECon (_, pc, NONE) => p_patCon env pc
+      | ECon (_, pc, SOME e) => parenIf par (box [p_patCon env pc,
+                                                  space,
+                                                  p_exp' true env e])
 
       | EFfi (m, x) => box [string "FFI(", string m, string ".", string x, string ")"]
       | EFfiApp (m, x, es) => box [string "FFI(",
--- a/src/mono_reduce.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/mono_reduce.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -79,25 +79,25 @@
         else
             NONE
 
-      | (PCon (PConVar n1, NONE), ECon (PConVar n2, NONE)) =>
+      | (PCon (_, PConVar n1, NONE), ECon (_, PConVar n2, NONE)) =>
         if n1 = n2 then
             SOME env
         else
             NONE
 
-      | (PCon (PConVar n1, SOME p), ECon (PConVar n2, SOME e)) =>
+      | (PCon (_, PConVar n1, SOME p), ECon (_, PConVar n2, SOME e)) =>
         if n1 = n2 then
             match (env, p, e)
         else
             NONE
 
-      | (PCon (PConFfi {mod = m1, con = con1, ...}, NONE), ECon (PConFfi {mod = m2, con = con2, ...}, NONE)) =>
+      | (PCon (_, PConFfi {mod = m1, con = con1, ...}, NONE), ECon (_, PConFfi {mod = m2, con = con2, ...}, NONE)) =>
         if m1 = m2 andalso con1 = con2 then
             SOME env
         else
             NONE
 
-      | (PCon (PConFfi {mod = m1, con = con1, ...}, SOME ep), ECon (PConFfi {mod = m2, con = con2, ...}, SOME e)) =>
+      | (PCon (_, PConFfi {mod = m1, con = con1, ...}, SOME ep), ECon (_, PConFfi {mod = m2, con = con2, ...}, SOME e)) =>
         if m1 = m2 andalso con1 = con2 then
             match (env, p, e)
         else
--- a/src/mono_shake.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/mono_shake.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -58,7 +58,7 @@
 
         fun typ (c, s) =
             case c of
-                TDatatype (n, _) =>
+                TDatatype (_, n, _) =>
                 if IS.member (#con s, n) then
                     s
                 else
--- a/src/mono_util.sig	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/mono_util.sig	Sun Aug 03 19:49:21 2008 -0400
@@ -27,6 +27,8 @@
 
 signature MONO_UTIL = sig
 
+val classifyDatatype : (string * int * Mono.typ option) list -> Mono.datatype_kind
+
 structure Typ : sig
     val compare : Mono.typ * Mono.typ -> order
     val sortFields : (string * Mono.typ) list -> (string * Mono.typ) list
--- a/src/mono_util.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/mono_util.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -29,6 +29,12 @@
 
 open Mono
 
+fun classifyDatatype xncs =
+    if List.all (fn (_, _, NONE) => true | _ => false) xncs then
+        Enum
+    else
+        Default
+
 structure S = Search
 
 structure Typ = struct
@@ -57,7 +63,7 @@
         in
             joinL compareFields (xts1, xts2)
         end
-      | (TDatatype (n1, _), TDatatype (n2, _)) => Int.compare (n1, n2)
+      | (TDatatype (_, n1, _), TDatatype (_, n2, _)) => Int.compare (n1, n2)
       | (TFfi (m1, x1), TFfi (m2, x2)) => join (String.compare (m1, m2), fn () => String.compare (x1, x2))
 
       | (TFun _, _) => LESS
@@ -141,11 +147,11 @@
                 EPrim _ => S.return2 eAll
               | ERel _ => S.return2 eAll
               | ENamed _ => S.return2 eAll
-              | ECon (_, NONE) => S.return2 eAll
-              | ECon (n, SOME e) =>
+              | ECon (_, _, NONE) => S.return2 eAll
+              | ECon (dk, n, SOME e) =>
                 S.map2 (mfe ctx e,
                         fn e' =>
-                           (ECon (n, SOME e'), loc))
+                           (ECon (dk, n, SOME e'), loc))
               | EFfi _ => S.return2 eAll
               | EFfiApp (m, x, es) =>
                 S.map2 (ListUtil.mapfold (fn e => mfe ctx e) es,
@@ -191,8 +197,8 @@
                                                                       PWild => ctx
                                                                     | PVar (x, t) => bind (ctx, RelE (x, t))
                                                                     | PPrim _ => ctx
-                                                                    | PCon (_, NONE) => ctx
-                                                                    | PCon (_, SOME p) => pb (p, ctx)
+                                                                    | PCon (_, _, NONE) => ctx
+                                                                    | PCon (_, _, SOME p) => pb (p, ctx)
                                                                     | PRecord xps => foldl (fn ((_, p, _), ctx) =>
                                                                                                pb (p, ctx)) ctx xps
                                                           in
@@ -355,7 +361,7 @@
                                         DDatatype (x, n, xncs) =>
                                         let
                                             val ctx = bind (ctx, Datatype (x, n, xncs))
-                                            val t = (TDatatype (n, xncs), #2 d')
+                                            val t = (TDatatype (classifyDatatype xncs, n, xncs), #2 d')
                                         in
                                             foldl (fn ((x, n, to), ctx) =>
                                                       let
--- a/src/monoize.sml	Sun Aug 03 19:01:16 2008 -0400
+++ b/src/monoize.sml	Sun Aug 03 19:49:21 2008 -0400
@@ -33,7 +33,7 @@
 structure L = Core
 structure L' = Mono
 
-val dummyTyp = (L'.TDatatype (0, []), E.dummySpan)
+val dummyTyp = (L'.TDatatype (L'.Enum, 0, []), E.dummySpan)
 
 fun monoName env (all as (c, loc)) =
     let
@@ -73,7 +73,7 @@
 
                 val xncs = map (fn (x, n, to) => (x, n, Option.map (monoType env) to)) xncs
             in
-                (L'.TDatatype (n, xncs), loc)
+                (L'.TDatatype (MonoUtil.classifyDatatype xncs, n, xncs), loc)
             end
           | L.CFfi mx => (L'.TFfi mx, loc)
           | L.CApp _ => poly ()
@@ -202,7 +202,7 @@
                     L'.TFfi (m, x) => ((L'.EFfiApp (m, fk2s fk ^ "ify" ^ capitalize x, [e]), loc), fm)
                   | L'.TRecord [] => ((L'.EPrim (Prim.String ""), loc), fm)
 
-                  | L'.TDatatype (i, _) =>
+                  | L'.TDatatype (dk, i, _) =>
                     let
                         fun makeDecl n fm =
                             let
@@ -213,7 +213,7 @@
                                         (fn ((x, n, to), fm) =>
                                             case to of
                                                 NONE =>
-                                                (((L'.PCon (L'.PConVar n, NONE), loc),
+                                                (((L'.PCon (dk, L'.PConVar n, NONE), loc),
                                                   (L'.EPrim (Prim.String x), loc)),
                                                  fm)
                                               | SOME t =>
@@ -221,7 +221,7 @@
                                                     val t = monoType env t
                                                     val (arg, fm) = fooify fm ((L'.ERel 0, loc), t)
                                                 in
-                                                    (((L'.PCon (L'.PConVar n, SOME (L'.PVar ("a", t), loc)), loc),
+                                                    (((L'.PCon (dk, L'.PConVar n, SOME (L'.PVar ("a", t), loc)), loc),
                                                       (L'.EStrcat ((L'.EPrim (Prim.String (x ^ "/")), loc),
                                                                    arg), loc)),
                                                      fm)
@@ -289,15 +289,15 @@
 fun monoPatCon env pc =
     case pc of
         L.PConVar n => L'.PConVar n
-      | L.PConFfi {mod = m, datatyp, con, arg} => L'.PConFfi {mod = m, datatyp = datatyp, con = con,
-                                                              arg = Option.map (monoType env) arg}
+      | L.PConFfi {mod = m, datatyp, con, arg, ...} => L'.PConFfi {mod = m, datatyp = datatyp, con = con,
+                                                                   arg = Option.map (monoType env) arg}
 
 fun monoPat env (p, loc) =
     case p of
         L.PWild => (L'.PWild, loc)
       | L.PVar (x, t) => (L'.PVar (x, monoType env t), loc)
       | L.PPrim p => (L'.PPrim p, loc)
-      | L.PCon (pc, po) => (L'.PCon (monoPatCon env pc, Option.map (monoPat env) po), loc)
+      | L.PCon (dk, pc, po) => (L'.PCon (dk, monoPatCon env pc, Option.map (monoPat env) po), loc)
       | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, monoPat env p, monoType env t)) xps), loc)
 
 fun monoExp (env, st, fm) (all as (e, loc)) =
@@ -311,7 +311,7 @@
             L.EPrim p => ((L'.EPrim p, loc), fm)
           | L.ERel n => ((L'.ERel n, loc), fm)
           | L.ENamed n => ((L'.ENamed n, loc), fm)
-          | L.ECon (pc, eo) =>
+          | L.ECon (dk, pc, eo) =>
             let
                 val (eo, fm) =
                     case eo of
@@ -323,7 +323,7 @@
                             (SOME e, fm)
                         end
             in
-                ((L'.ECon (monoPatCon env pc, eo), loc), fm)
+                ((L'.ECon (dk, monoPatCon env pc, eo), loc), fm)
             end
           | L.EFfi mx => ((L'.EFfi mx, loc), fm)
           | L.EFfiApp (m, x, es) =>