Add datatype import constructor annotations; datatypes through explify

11 files changed, 221 insertions, 122 deletions

diff --git a/src/corify.sml b/src/corify.sml
index 4277c35e..0f98e99c 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -384,6 +384,8 @@ fun corifyDecl ((d, loc : EM.span), st) =
         in
             ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st)
         end
+      | L.DDatatype _ => raise Fail "Corify DDatatype"
+      | L.DDatatypeImp _ => raise Fail "Corify DDatatypeImp"
       | L.DVal (x, n, t, e) =>
         let
             val (st, n) = St.bindVal st x n
@@ -568,6 +570,8 @@ and corifyStr ((str, _), st) =
 fun maxName ds = foldl (fn ((d, _), n) =>
                            case d of
                                L.DCon (_, n', _, _) => Int.max (n, n')
+                             | L.DDatatype (_, n', _) => Int.max (n, n')
+                             | L.DDatatypeImp (_, n', _, _, _, _) => Int.max (n, n')
                              | L.DVal (_, n', _, _) => Int.max (n, n')
                              | L.DValRec vis => foldl (fn ((_, n', _, _), n) => Int.max (n, n)) n vis
                              | L.DSgn (_, n', _) => Int.max (n, n')
diff --git a/src/elab.sml b/src/elab.sml
index e0ccee25..b258d7e5 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -94,7 +94,7 @@ datatype sgn_item' =
          SgiConAbs of string * int * kind
        | SgiCon of string * int * kind * con
        | SgiDatatype of string * int * (string * int * con option) list
-       | SgiDatatypeImp of string * int * int * string list * string
+       | SgiDatatypeImp of string * int * int * string list * string * (string * int * con option) list
        | SgiVal of string * int * con
        | SgiStr of string * int * sgn
        | SgiSgn of string * int * sgn
@@ -114,7 +114,7 @@ and sgn = sgn' located
 datatype decl' =
          DCon of string * int * kind * con
        | DDatatype of string * int * (string * int * con option) list
-       | DDatatypeImp of string * int * int * string list * string
+       | DDatatypeImp of string * int * int * string list * string * (string * int * con option) list
        | DVal of string * int * con * exp
        | DValRec of (string * int * con * exp) list
        | DSgn of string * int * sgn
diff --git a/src/elab_env.sml b/src/elab_env.sml
index d28b713f..1fe5dd5a 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -353,7 +353,14 @@ fun sgiBinds env (sgi, loc) =
                     | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc))
             env xncs
         end
-      | SgiDatatypeImp (x, n, m1, ms, x') => pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc))
+      | SgiDatatypeImp (x, n, m1, ms, x', xncs) =>
+        let
+            val env = pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc))
+        in
+            foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc)
+                    | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc))
+            env xncs
+        end
       | SgiVal (x, n, t) => pushENamedAs env x n t
       | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
       | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
@@ -371,7 +378,7 @@ fun sgnSeek f sgis =
                         val cons =
                             case sgi of
                                 SgiDatatype (x, n, _) => IM.insert (cons, n, x)
-                              | SgiDatatypeImp (x, n, _, _, _) => IM.insert (cons, n, x)
+                              | SgiDatatypeImp (x, n, _, _, _, _) => IM.insert (cons, n, x)
                               | _ => cons
                     in
                         SOME (v, (sgns, strs, cons))
@@ -381,7 +388,7 @@ fun sgnSeek f sgis =
                         SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
                       | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
                       | SgiDatatype (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
-                      | SgiDatatypeImp (x, n, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
+                      | SgiDatatypeImp (x, n, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
                       | SgiVal _ => seek (sgis, sgns, strs, cons)
                       | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons)
                       | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons)
@@ -529,7 +536,7 @@ fun projectCon env {sgn, str, field} =
         (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE
                         | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE
                         | SgiDatatype (x, _, _) => if x = field then SOME ((KType, #2 sgn), NONE) else NONE
-                        | SgiDatatypeImp (x, _, m1, ms, x') =>
+                        | SgiDatatypeImp (x, _, m1, ms, x', _) =>
                           if x = field then
                               SOME ((KType, #2 sgn), SOME (CModProj (m1, ms, x'), #2 sgn))
                           else
@@ -544,15 +551,7 @@ fun projectDatatype env {sgn, str, field} =
     case #1 (hnormSgn env sgn) of
         SgnConst sgis =>
         (case sgnSeek (fn SgiDatatype (x, _, xncs) => if x = field then SOME xncs else NONE
-                        | SgiDatatypeImp (x, _, m1, ms, x') =>
-                          if x = field then
-                              let
-                                  val (str, sgn) = chaseMpath env (m1, ms)
-                              in
-                                  projectDatatype env {sgn = sgn, str = str, field = x'}
-                              end
-                          else
-                              NONE
+                        | SgiDatatypeImp (x, _, _, _, _, xncs) => if x = field then SOME xncs else NONE
                         | _ => NONE) sgis of
              NONE => NONE
            | SOME (xncs, subs) => SOME (map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs))
@@ -561,33 +560,23 @@ fun projectDatatype env {sgn, str, field} =
 fun projectVal env {sgn, str, field} =
     case #1 (hnormSgn env sgn) of
         SgnConst sgis =>
-        (case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE
-                        | SgiDatatype (_, n, xncs) =>
-                          ListUtil.search (fn (x, _, to) =>
-                                              if x = field then
-                                                  SOME (case to of
-                                                            NONE => (CNamed n, #2 sgn)
-                                                          | SOME t => (TFun (t, (CNamed n, #2 sgn)), #2 sgn))
-                                              else
-                                                  NONE) xncs
-                        | SgiDatatypeImp (_, n, m1, ms, x') =>
-                          let
-                              val (str, sgn) = chaseMpath env (m1, ms)
-                          in
-                              case projectDatatype env {sgn = sgn, str = str, field = x'} of
-                                  NONE => NONE
-                                | SOME xncs =>
-                                  ListUtil.search (fn (x, _, to) =>
-                                                      if x = field then
-                                                          SOME (case to of
-                                                                    NONE => (CNamed n, #2 sgn)
-                                                                  | SOME t => (TFun (t, (CNamed n, #2 sgn)), #2 sgn))
-                                                      else
-                                                          NONE) xncs
-                          end
-                        | _ => NONE) sgis of
-             NONE => NONE
-           | SOME (c, subs) => SOME (sgnSubCon (str, subs) c))
+        let
+            fun seek (n, xncs) =
+                ListUtil.search (fn (x, _, to) =>
+                                    if x = field then
+                                        SOME (case to of
+                                                  NONE => (CNamed n, #2 sgn)
+                                                | SOME t => (TFun (t, (CNamed n, #2 sgn)), #2 sgn))
+                                    else
+                                        NONE) xncs
+        in
+            case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE
+                           | SgiDatatype (_, n, xncs) => seek (n, xncs)
+                           | SgiDatatypeImp (_, n, _, _, _, xncs) => seek (n, xncs)
+                           | _ => NONE) sgis of
+                NONE => NONE
+              | SOME (c, subs) => SOME (sgnSubCon (str, subs) c)
+        end
       | SgnError => SOME (CError, ErrorMsg.dummySpan)
       | _ => NONE
 
@@ -607,7 +596,7 @@ fun sgnSeekConstraints (str, sgis) =
                   | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
                   | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
                   | SgiDatatype (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
-                  | SgiDatatypeImp (x, n, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
+                  | SgiDatatypeImp (x, n, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
                   | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
                   | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
                   | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc)
@@ -632,19 +621,10 @@ fun declBinds env (d, loc) =
                     | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc))
             env xncs
         end
-      | DDatatypeImp (x, n, m, ms, x') =>
+      | DDatatypeImp (x, n, m, ms, x', xncs) =>
         let
             val t = (CModProj (m, ms, x'), loc)
             val env = pushCNamedAs env x n (KType, loc) (SOME t)
-            val (_, sgn) = lookupStrNamed env m
-            val (str, sgn) = foldl (fn (m, (str, sgn)) =>
-                                       case projectStr env {sgn = sgn, str = str, field = m} of
-                                           NONE => raise Fail "ElabEnv.declBinds: Couldn't projectStr"
-                                         | SOME sgn => ((StrProj (str, m), loc), sgn))
-                                   ((StrVar m, loc), sgn) ms
-            val xncs = case projectDatatype env {sgn = sgn, str = str, field = x'} of
-                           NONE => raise Fail "ElabEnv.declBinds: Couldn't projectDatatype"
-                         | SOME xncs => xncs
 
             val t = (CNamed n, loc)
         in
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 19653df9..693bc443 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -346,7 +346,7 @@ fun p_sgn_item env (sgi, _) =
                                     space,
                                     p_con env c]
       | SgiDatatype x => p_datatype env x
-      | SgiDatatypeImp (x, _, m1, ms, x') =>
+      | SgiDatatypeImp (x, _, m1, ms, x', _) =>
         let
             val m1x = #1 (E.lookupStrNamed env m1)
                 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
@@ -468,7 +468,7 @@ fun p_decl env (dAll as (d, _) : decl) =
                                   space,
                                   p_con env c]
       | DDatatype x => p_datatype env x
-      | DDatatypeImp (x, _, m1, ms, x') =>
+      | DDatatypeImp (x, _, m1, ms, x', _) =>
         let
             val m1x = #1 (E.lookupStrNamed env m1)
                 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 0ee35320..05f80ad1 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -386,7 +386,15 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                                                       fn c' => (x, n, SOME c'))) xncs,
                         fn xncs' =>
                            (SgiDatatype (x, n, xncs'), loc))
-              | SgiDatatypeImp _ => S.return2 siAll
+              | SgiDatatypeImp (x, n, m1, ms, s, xncs) =>
+                S.map2 (ListUtil.mapfold (fn (x, n, c) =>
+                                             case c of
+                                                 NONE => S.return2 (x, n, c)
+                                               | SOME c =>
+                                                 S.map2 (con ctx c,
+                                                      fn c' => (x, n, SOME c'))) xncs,
+                        fn xncs' =>
+                           (SgiDatatypeImp (x, n, m1, ms, s, xncs'), loc))
               | SgiVal (x, n, c) =>
                 S.map2 (con ctx c,
                      fn c' =>
@@ -420,7 +428,7 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                                                    bind (ctx, NamedC (x, k))
                                                  | SgiDatatype (x, n, xncs) =>
                                                    bind (ctx, NamedC (x, (KType, loc)))
-                                                 | SgiDatatypeImp (x, _, _, _, _) =>
+                                                 | SgiDatatypeImp (x, _, _, _, _, _) =>
                                                    bind (ctx, NamedC (x, (KType, loc)))
                                                  | SgiVal _ => ctx
                                                  | SgiStr (x, _, sgn) =>
@@ -541,7 +549,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                                                                  end)
                                                        ctx xncs
                                                    end
-                                                 | DDatatypeImp (x, n, m, ms, x') =>
+                                                 | DDatatypeImp (x, n, m, ms, x', _) =>
                                                    bind (ctx, NamedC (x, (KType, loc)))
                                                  | DVal (x, _, c, _) =>
                                                    bind (ctx, NamedE (x, c))
@@ -598,7 +606,15 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                                                       fn c' => (x, n, SOME c'))) xncs,
                         fn xncs' =>
                            (DDatatype (x, n, xncs'), loc))
-              | DDatatypeImp _ => S.return2 dAll
+              | DDatatypeImp (x, n, m1, ms, s, xncs) =>
+                S.map2 (ListUtil.mapfold (fn (x, n, c) =>
+                                             case c of
+                                                 NONE => S.return2 (x, n, c)
+                                               | SOME c =>
+                                                 S.map2 (mfc ctx c,
+                                                      fn c' => (x, n, SOME c'))) xncs,
+                        fn xncs' =>
+                           (DDatatypeImp (x, n, m1, ms, s, xncs'), loc))
               | DVal vi =>
                 S.map2 (mfvi ctx vi,
                      fn vi' =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 802cef7b..cd2c25d7 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1359,7 +1359,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
                                                       E.pushENamedAs env x n t
                                                   end) env xncs
                           in
-                              ([(L'.SgiDatatypeImp (x, n', n, ms, s), loc)], (env, denv, gs))
+                              ([(L'.SgiDatatypeImp (x, n', n, ms, s, xncs), loc)], (env, denv, gs))
                           end)
                    | _ => (strError env (NotDatatype loc);
                            ([], (env, denv, [])))
@@ -1453,7 +1453,7 @@ and elabSgn (env, denv) (sgn, loc) =
                                           ();
                                       (SS.add (cons, x), vals, sgns, strs)
                                   end
-                                | L'.SgiDatatypeImp (x, _, _, _, _) =>
+                                | L'.SgiDatatypeImp (x, _, _, _, _, _) =>
                                   (if SS.member (cons, x) then
                                        sgnError env (DuplicateCon (loc, x))
                                    else
@@ -1546,7 +1546,7 @@ fun selfify env {str, strs, sgn} =
         (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) =>
                               (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
                             | (L'.SgiDatatype (x, n, xncs), loc) =>
-                              (L'.SgiDatatypeImp (x, n, str, strs, x), loc)
+                              (L'.SgiDatatypeImp (x, n, str, strs, x, xncs), loc)
                             | (L'.SgiStr (x, n, sgn), loc) =>
                               (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
                             | x => x) sgis), #2 sgn)
@@ -1584,45 +1584,32 @@ fun dopen (env, denv) {str, strs, sgn} =
         case #1 (hnormSgn env sgn) of
             L'.SgnConst sgis =>
             ListUtil.foldlMap (fn ((sgi, loc), (env', denv')) =>
-                                  case sgi of
-                                      L'.SgiConAbs (x, n, k) =>
-                                      let
-                                          val c = (L'.CModProj (str, strs, x), loc)
-                                      in
-                                          ((L'.DCon (x, n, k, c), loc),
-                                           (E.pushCNamedAs env' x n k (SOME c), denv'))
-                                      end
-                                    | L'.SgiCon (x, n, k, c) =>
-                                      ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc),
-                                       (E.pushCNamedAs env' x n k (SOME c), denv'))
-                                    | L'.SgiDatatype (x, n, xncs) =>
-                                      let
-                                          val k = (L'.KType, loc)
-                                          val c = (L'.CModProj (str, strs, x), loc)
-                                      in
-                                          ((L'.DDatatypeImp (x, n, str, strs, x), loc),
-                                           (E.pushCNamedAs env' x n k (SOME c), denv'))
-                                      end
-                                    | L'.SgiDatatypeImp (x, n, m1, ms, x') =>
-                                      let
-                                          val k = (L'.KType, loc)
-                                          val c = (L'.CModProj (m1, ms, x'), loc)
-                                      in
-                                          ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc),
-                                           (E.pushCNamedAs env' x n k (SOME c), denv'))
-                                      end
-                                    | L'.SgiVal (x, n, t) =>
-                                      ((L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc),
-                                       (E.pushENamedAs env' x n t, denv'))
-                                    | L'.SgiStr (x, n, sgn) =>
-                                      ((L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc),
-                                       (E.pushStrNamedAs env' x n sgn, denv'))
-                                    | L'.SgiSgn (x, n, sgn) =>
-                                      ((L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc),
-                                       (E.pushSgnNamedAs env' x n sgn, denv'))
-                                    | L'.SgiConstraint (c1, c2) =>
-                                      ((L'.DConstraint (c1, c2), loc),
-                                       (env', denv)))
+                                  let
+                                      val d =
+                                          case sgi of
+                                              L'.SgiConAbs (x, n, k) =>
+                                              let
+                                                  val c = (L'.CModProj (str, strs, x), loc)
+                                              in
+                                                  (L'.DCon (x, n, k, c), loc)
+                                              end
+                                            | L'.SgiCon (x, n, k, c) =>
+                                              (L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
+                                            | L'.SgiDatatype (x, n, xncs) =>
+                                              (L'.DDatatypeImp (x, n, str, strs, x, xncs), loc)
+                                            | L'.SgiDatatypeImp (x, n, m1, ms, x', xncs) =>
+                                              (L'.DDatatypeImp (x, n, m1, ms, x', xncs), loc)
+                                            | L'.SgiVal (x, n, t) =>
+                                              (L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc)
+                                            | L'.SgiStr (x, n, sgn) =>
+                                              (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)
+                                            | L'.SgiSgn (x, n, sgn) =>
+                                              (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)
+                                            | L'.SgiConstraint (c1, c2) =>
+                                              (L'.DConstraint (c1, c2), loc)
+                                  in
+                                      (d, (E.declBinds env' d, denv'))
+                                  end)
                               (env, denv) sgis
           | _ => (strError env (UnOpenable sgn);
                   ([], (env, denv)))
@@ -1729,7 +1716,7 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                          L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE)
                                        | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, SOME c1)
                                        | L'.SgiDatatype (x', n1, _) => found (x', n1, (L'.KType, loc), NONE)
-                                       | L'.SgiDatatypeImp (x', n1, m1, ms, s) =>
+                                       | L'.SgiDatatypeImp (x', n1, m1, ms, s, _) =>
                                          found (x', n1, (L'.KType, loc), SOME (L'.CModProj (m1, ms, s), loc))
                                        | _ => NONE
                                  end)
@@ -1796,21 +1783,18 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                              found (n1, xncs1)
                                          else
                                              NONE
-                                       | L'.SgiDatatypeImp (x', n1, m1, ms, s) =>
-                                         let
-                                             val (str, sgn) = E.chaseMpath env (m1, ms)
-                                         in
-                                             case E.projectDatatype env {str = str, sgn = sgn, field = s} of
-                                                 NONE => NONE
-                                               | SOME xncs1 => found (n1, xncs1)
-                                         end
+                                       | L'.SgiDatatypeImp (x', n1, _, _, _, xncs1) =>
+                                         if x' = x then
+                                             found (n1, xncs1)
+                                         else
+                                             NONE
                                        | _ => NONE
                                  end)
 
-                      | L'.SgiDatatypeImp (x, n2, m11, ms1, s1) =>
+                      | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, _) =>
                         seek (fn sgi1All as (sgi1, _) =>
                                  case sgi1 of
-                                     L'.SgiDatatypeImp (x', n1, m12, ms2, s2) =>
+                                     L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _) =>
                                      if x = x' then
                                          let
                                              val k = (L'.KType, loc)
@@ -2016,7 +2000,7 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
                                                       E.pushENamedAs env x n t
                                                   end) env xncs
                           in
-                              ([(L'.DDatatypeImp (x, n', n, ms, s), loc)], (env, denv, gs))
+                              ([(L'.DDatatypeImp (x, n', n, ms, s, xncs), loc)], (env, denv, gs))
                           end)
                    | _ => (strError env (NotDatatype loc);
                            ([], (env, denv, [])))
@@ -2294,7 +2278,7 @@ and elabStr (env, denv) (str, loc) =
                               in
                                   ((L'.SgiDatatype (x, n, xncs), loc) :: sgis, cons, vals, sgns, strs)
                               end
-                            | L'.SgiDatatypeImp (x, n, m1, ms, x') =>
+                            | L'.SgiDatatypeImp (x, n, m1, ms, x', xncs) =>
                               let
                                   val (cons, x) =
                                       if SS.member (cons, x) then
@@ -2302,7 +2286,7 @@ and elabStr (env, denv) (str, loc) =
                                       else
                                           (SS.add (cons, x), x)
                               in
-                                  ((L'.SgiDatatypeImp (x, n, m1, ms, x'), loc) :: sgis, cons, vals, sgns, strs)
+                                  ((L'.SgiDatatypeImp (x, n, m1, ms, x', xncs), loc) :: sgis, cons, vals, sgns, strs)
                               end
                             | L'.SgiVal (x, n, c) =>
                               let
diff --git a/src/expl.sml b/src/expl.sml
index b1a0e389..183dbc31 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -81,6 +81,8 @@ withtype exp = exp' located
 datatype sgn_item' =
          SgiConAbs of string * int * kind
        | SgiCon of string * int * kind * con
+       | SgiDatatype of string * int * (string * int * con option) list
+       | SgiDatatypeImp of string * int * int * string list * string * (string * int * con option) list
        | SgiVal of string * int * con
        | SgiSgn of string * int * sgn
        | SgiStr of string * int * sgn
@@ -97,6 +99,8 @@ and sgn = sgn' located
 
 datatype decl' =
          DCon of string * int * kind * con
+       | DDatatype of string * int * (string * int * con option) list
+       | DDatatypeImp of string * int * int * string list * string * (string * int * con option) list
        | DVal of string * int * con * exp
        | DValRec of (string * int * con * exp) list
        | DSgn of string * int * sgn
diff --git a/src/expl_env.sml b/src/expl_env.sml
index 1871e560..359c92a3 100644
--- a/src/expl_env.sml
+++ b/src/expl_env.sml
@@ -236,9 +236,28 @@ fun lookupStrNamed (env : env) n =
         NONE => raise UnboundNamed n
       | SOME x => x
 
-fun declBinds env (d, _) =
+fun declBinds env (d, loc) =
     case d of
         DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
+      | DDatatype (x, n, xncs) =>
+        let
+            val env = pushCNamed env x n (KType, loc) NONE
+        in
+            foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc)
+                    | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc))
+            env xncs
+        end
+      | DDatatypeImp (x, n, m, ms, x', xncs) =>
+        let
+            val t = (CModProj (m, ms, x'), loc)
+            val env = pushCNamed env x n (KType, loc) (SOME t)
+
+            val t = (CNamed n, loc)
+        in
+            foldl (fn ((x', n', NONE), env) => pushENamed env x' n' t
+                    | ((x', n', SOME t'), env) => pushENamed env x' n' (TFun (t', t), loc))
+            env xncs
+        end
       | DVal (x, n, t, _) => pushENamed env x n t
       | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamed env x n t) env vis
       | DSgn (x, n, sgn) => pushSgnNamed env x n sgn
@@ -246,10 +265,26 @@ fun declBinds env (d, _) =
       | DFfiStr (x, n, sgn) => pushStrNamed env x n sgn
       | DExport _ => env
 
-fun sgiBinds env (sgi, _) =
+fun sgiBinds env (sgi, loc) =
     case sgi of
         SgiConAbs (x, n, k) => pushCNamed env x n k NONE
       | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c)
+      | SgiDatatype (x, n, xncs) =>
+        let
+            val env = pushCNamed env x n (KType, loc) NONE
+        in
+            foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc)
+                    | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc))
+            env xncs
+        end
+      | SgiDatatypeImp (x, n, m1, ms, x', xncs) =>
+        let
+            val env = pushCNamed env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc))
+        in
+            foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc)
+                    | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc))
+            env xncs
+        end
       | SgiVal (x, n, t) => pushENamed env x n t
       | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn
       | SgiStr (x, n, sgn) => pushStrNamed env x n sgn
diff --git a/src/expl_print.sml b/src/expl_print.sml
index 58508097..472d83ae 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -274,6 +274,22 @@ fun p_named x n =
     else
         string x
 
+fun p_datatype env (x, n, cons) =
+    let
+        val env = E.pushCNamed env x n (KType, ErrorMsg.dummySpan) NONE
+    in
+        box [string "datatype",
+             space,
+             string x,
+             space,
+             string "=",
+             space,
+             p_list_sep (box [space, string "|", space])
+                        (fn (x, _, NONE) => string x
+                          | (x, _, SOME t) => box [string x, space, string "of", space, p_con env t])
+                        cons]
+    end
+
 fun p_sgn_item env (sgi, _) =
     case sgi of
         SgiConAbs (x, n, k) => box [string "con",
@@ -294,6 +310,22 @@ fun p_sgn_item env (sgi, _) =
                                     string "=",
                                     space,
                                     p_con env c]
+      | SgiDatatype x => p_datatype env x
+      | SgiDatatypeImp (x, _, m1, ms, x', _) =>
+        let
+            val m1x = #1 (E.lookupStrNamed env m1)
+                handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
+        in
+            box [string "datatype",
+                 space,
+                 string x,
+                 space,
+                 string "=",
+                 space,
+                 string "datatype",
+                 space,
+                 p_list_sep (string ".") string (m1x :: ms @ [x'])]
+        end
       | SgiVal (x, n, c) => box [string "val",
                                  space,
                                  p_named x n,
@@ -392,6 +424,22 @@ fun p_decl env (dAll as (d, _) : decl) =
                                   string "=",
                                   space,
                                   p_con env c]
+      | DDatatype x => p_datatype env x
+      | DDatatypeImp (x, _, m1, ms, x', _) =>
+        let
+            val m1x = #1 (E.lookupStrNamed env m1)
+                handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
+        in
+            box [string "datatype",
+                 space,
+                 string x,
+                 space,
+                 string "=",
+                 space,
+                 string "datatype",
+                 space,
+                 p_list_sep (string ".") string (m1x :: ms @ [x'])]
+        end
       | DVal vi => box [string "val",
                         space,
                         p_vali env vi]
diff --git a/src/expl_util.sml b/src/expl_util.sml
index 976df246..e1a5d30f 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -342,7 +342,7 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
         fun sgi ctx si acc =
             S.bindP (sgi' ctx si acc, sgn_item ctx)
 
-        and sgi' ctx (si, loc) =
+        and sgi' ctx (siAll as (si, loc)) =
             case si of
                 SgiConAbs (x, n, k) =>
                 S.map2 (kind k,
@@ -354,6 +354,24 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                         S.map2 (con ctx c,
                              fn c' =>
                                 (SgiCon (x, n, k', c'), loc)))
+              | SgiDatatype (x, n, xncs) =>
+                S.map2 (ListUtil.mapfold (fn (x, n, c) =>
+                                             case c of
+                                                 NONE => S.return2 (x, n, c)
+                                               | SOME c =>
+                                                 S.map2 (con ctx c,
+                                                      fn c' => (x, n, SOME c'))) xncs,
+                        fn xncs' =>
+                           (SgiDatatype (x, n, xncs'), loc))
+              | SgiDatatypeImp (x, n, m1, ms, s, xncs) =>
+                S.map2 (ListUtil.mapfold (fn (x, n, c) =>
+                                             case c of
+                                                 NONE => S.return2 (x, n, c)
+                                               | SOME c =>
+                                                 S.map2 (con ctx c,
+                                                      fn c' => (x, n, SOME c'))) xncs,
+                        fn xncs' =>
+                           (SgiDatatypeImp (x, n, m1, ms, s, xncs'), loc))
               | SgiVal (x, n, c) =>
                 S.map2 (con ctx c,
                      fn c' =>
@@ -379,6 +397,10 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                                                    bind (ctx, NamedC (x, k))
                                                  | SgiCon (x, _, k, _) =>
                                                    bind (ctx, NamedC (x, k))
+                                                 | SgiDatatype (x, n, xncs) =>
+                                                   bind (ctx, NamedC (x, (KType, loc)))
+                                                 | SgiDatatypeImp (x, _, _, _, _, _) =>
+                                                   bind (ctx, NamedC (x, (KType, loc)))
                                                  | SgiVal _ => ctx
                                                  | SgiStr (x, _, sgn) =>
                                                    bind (ctx, Str (x, sgn))
diff --git a/src/explify.sml b/src/explify.sml
index f179ce36..c193a631 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -95,8 +95,11 @@ fun explifySgi (sgi, loc) =
     case sgi of
         L.SgiConAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, explifyKind k), loc)
       | L.SgiCon (x, n, k, c) => SOME (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc)
-      | L.SgiDatatype _ => raise Fail "Explify SgiDatatype"
-      | L.SgiDatatypeImp _ => raise Fail "Explify SgiDatatypeImp"
+      | L.SgiDatatype (x, n, xncs) => SOME (L'.SgiDatatype (x, n, map (fn (x, n, co) =>
+                                                                          (x, n, Option.map explifyCon co)) xncs), loc)
+      | L.SgiDatatypeImp (x, n, m1, ms, s, xncs) =>
+        SOME (L'.SgiDatatypeImp (x, n, m1, ms, s, map (fn (x, n, co) =>
+                                                          (x, n, Option.map explifyCon co)) xncs), loc)
       | L.SgiVal (x, n, c) => SOME (L'.SgiVal (x, n, explifyCon c), loc)
       | L.SgiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, explifySgn sgn), loc)
       | L.SgiSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, explifySgn sgn), loc)
@@ -114,8 +117,11 @@ and explifySgn (sgn, loc) =
 fun explifyDecl (d, loc : EM.span) =
     case d of
         L.DCon (x, n, k, c) => SOME (L'.DCon (x, n, explifyKind k, explifyCon c), loc)
-      | L.DDatatype _ => raise Fail "Explify DDatatype"
-      | L.DDatatypeImp _ => raise Fail "Explify DDatatypeImp"
+      | L.DDatatype (x, n, xncs) => SOME (L'.DDatatype (x, n, map (fn (x, n, co) =>
+                                                                      (x, n, Option.map explifyCon co)) xncs), loc)
+      | L.DDatatypeImp (x, n, m1, ms, s, xncs) =>
+        SOME (L'.DDatatypeImp (x, n, m1, ms, s, map (fn (x, n, co) =>
+                                                        (x, n, Option.map explifyCon co)) xncs), loc)
       | L.DVal (x, n, t, e) => SOME (L'.DVal (x, n, explifyCon t, explifyExp e), loc)
       | L.DValRec vis => SOME (L'.DValRec (map (fn (x, n, t, e) => (x, n, explifyCon t, explifyExp e)) vis), loc)