Start of datatype support

10 files changed, 352 insertions, 6 deletions

diff --git a/src/elab.sml b/src/elab.sml
index 1ba3b454..e0ccee25 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -93,6 +93,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
        | SgiVal of string * int * con
        | SgiStr of string * int * sgn
        | SgiSgn of string * int * sgn
@@ -111,6 +113,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
        | 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 e16296ad..9f4916e3 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -292,9 +292,18 @@ fun lookupStrNamed (env : env) n =
 
 fun lookupStr (env : env) x = SM.find (#renameStr env, x)
 
-fun declBinds env (d, _) =
+fun declBinds env (d, loc) =
     case d of
         DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
+      | DDatatype (x, n, xncs) =>
+        let
+            val env = pushCNamedAs env x n (KType, loc) NONE
+        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
+      | DDatatypeImp (x, n, m, ms, x') => pushCNamedAs env x n (KType, loc) (SOME (CModProj (m, ms, x'), loc))
       | DVal (x, n, t, _) => pushENamedAs env x n t
       | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamedAs env x n t) env vis
       | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
@@ -303,10 +312,19 @@ fun declBinds env (d, _) =
       | DConstraint _ => env
       | DExport _ => env
 
-fun sgiBinds env (sgi, _) =
+fun sgiBinds env (sgi, loc) =
     case sgi of
         SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
       | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
+      | SgiDatatype (x, n, xncs) =>
+        let
+            val env = pushCNamedAs env x n (KType, loc) NONE
+        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
+      | SgiDatatypeImp (x, n, m1, ms, x') => pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc))
       | 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
@@ -324,6 +342,8 @@ fun sgnSeek f sgis =
                     case sgi of
                         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))
                       | 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)
@@ -489,6 +509,8 @@ fun sgnSeekConstraints (str, sgis) =
                     end
                   | 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)
                   | 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)
diff --git a/src/elab_print.sml b/src/elab_print.sml
index e59fb9f7..19653df9 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -309,6 +309,22 @@ fun p_named x n =
     else
         string x
 
+fun p_datatype env (x, n, cons) =
+    let
+        val env = E.pushCNamedAs 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",
@@ -329,6 +345,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,
@@ -435,6 +467,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/elab_util.sml b/src/elab_util.sml
index 0ff2d733..0ee35320 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -365,7 +365,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,
@@ -377,6 +377,16 @@ 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 _ => S.return2 siAll
               | SgiVal (x, n, c) =>
                 S.map2 (con ctx c,
                      fn c' =>
@@ -408,6 +418,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))
@@ -512,6 +526,23 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                                               (case #1 d of
                                                    DCon (x, _, k, _) =>
                                                    bind (ctx, NamedC (x, k))
+                                                 | DDatatype (x, n, xncs) =>
+                                                   let
+                                                       val ctx = bind (ctx, NamedC (x, (KType, loc)))
+                                                   in
+                                                       foldl (fn ((x, _, co), ctx) =>
+                                                                 let
+                                                                     val t =
+                                                                         case co of
+                                                                             NONE => CNamed n
+                                                                           | SOME t => TFun (t, (CNamed n, loc))
+                                                                 in
+                                                                     bind (ctx, NamedE (x, (t, loc)))
+                                                                 end)
+                                                       ctx xncs
+                                                   end
+                                                 | DDatatypeImp (x, n, m, ms, x') =>
+                                                   bind (ctx, NamedC (x, (KType, loc)))
                                                  | DVal (x, _, c, _) =>
                                                    bind (ctx, NamedE (x, c))
                                                  | DValRec vis =>
@@ -558,6 +589,16 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                             S.map2 (mfc ctx c,
                                     fn c' =>
                                        (DCon (x, n, k', c'), loc)))
+              | DDatatype (x, n, 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' =>
+                           (DDatatype (x, n, xncs'), loc))
+              | DDatatypeImp _ => S.return2 dAll
               | DVal vi =>
                 S.map2 (mfvi ctx vi,
                      fn vi' =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 4d5e5136..c6b4ed1c 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1158,6 +1158,7 @@ datatype sgn_error =
        | UnmatchedSgi of L'.sgn_item
        | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error
        | SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error
+       | SgiMismatchedDatatypes of L'.sgn_item * L'.sgn_item * (L'.con * L'.con * cunify_error) option
        | SgnWrongForm of L'.sgn * L'.sgn
        | UnWhereable of L'.sgn * string
        | WhereWrongKind of L'.kind * L'.kind * kunify_error
@@ -1189,6 +1190,15 @@ fun sgnError env err =
                      ("Con 1", p_con env c1),
                      ("Con 2", p_con env c2)];
          cunifyError env cerr)
+      | SgiMismatchedDatatypes (sgi1, sgi2, cerro) =>
+        (ErrorMsg.errorAt (#2 sgi1) "Mismatched 'datatype' specifications:";
+         eprefaces' [("Have", p_sgn_item env sgi1),
+                     ("Need", p_sgn_item env sgi2)];
+         Option.app (fn (c1, c2, ue) =>
+                        (eprefaces "Unification error"
+                                   [("Con 1", p_con env c1),
+                                    ("Con 2", p_con env c2)];
+                         cunifyError env ue)) cerro)
       | SgnWrongForm (sgn1, sgn2) =>
         (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:";
          eprefaces' [("Sig 1", p_sgn env sgn1),
@@ -1223,6 +1233,7 @@ datatype str_error =
        | FunctorRebind of ErrorMsg.span
        | UnOpenable of L'.sgn
        | NotType of L'.kind * (L'.kind * L'.kind * kunify_error)
+       | DuplicateConstructor of string * ErrorMsg.span
 
 fun strError env err =
     case err of
@@ -1242,6 +1253,8 @@ fun strError env err =
                      ("Subkind 1", p_kind k1),
                      ("Subkind 2", p_kind k2)];
          kunifyError ue)
+      | DuplicateConstructor (x, loc) =>
+        ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
 
 val hnormSgn = E.hnormSgn
 
@@ -1270,6 +1283,10 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
             ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
         end
 
+      | L.SgiDatatype _ => raise Fail "Elaborate SgiDatatype"
+
+      | L.SgiDatatypeImp _ => raise Fail "Elaborate SgiDatatypeImp"
+
       | L.SgiVal (x, c) =>
         let
             val (c', ck, gs') = elabCon (env, denv) c
@@ -1342,6 +1359,28 @@ and elabSgn (env, denv) (sgn, loc) =
                                    else
                                        ();
                                    (SS.add (cons, x), vals, sgns, strs))
+                                | L'.SgiDatatype (x, _, xncs) =>
+                                  let
+                                      val vals = foldl (fn ((x, _, _), vals) =>
+                                                           (if SS.member (vals, x) then
+                                                                sgnError env (DuplicateVal (loc, x))
+                                                            else
+                                                                ();
+                                                            SS.add (vals, x)))
+                                                       vals xncs
+                                  in
+                                      if SS.member (cons, x) then
+                                          sgnError env (DuplicateCon (loc, x))
+                                      else
+                                          ();
+                                      (SS.add (cons, x), vals, sgns, strs)
+                                  end
+                                | L'.SgiDatatypeImp (x, _, _, _, _) =>
+                                  (if SS.member (cons, x) then
+                                       sgnError env (DuplicateCon (loc, x))
+                                   else
+                                       ();
+                                   (SS.add (cons, x), vals, sgns, strs))
                                 | L'.SgiVal (x, _, _) =>
                                   (if SS.member (vals, x) then
                                        sgnError env (DuplicateVal (loc, x))
@@ -1476,6 +1515,22 @@ fun dopen (env, denv) {str, strs, sgn} =
                                     | 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'))
@@ -1487,7 +1542,7 @@ fun dopen (env, denv) {str, strs, sgn} =
                                        (E.pushSgnNamedAs env' x n sgn, denv'))
                                     | L'.SgiConstraint (c1, c2) =>
                                       ((L'.DConstraint (c1, c2), loc),
-                                       (env', denv (* D.assert env denv (c1, c2) *) )))
+                                       (env', denv)))
                               (env, denv) sgis
           | _ => (strError env (UnOpenable sgn);
                   ([], (env, denv)))
@@ -1528,6 +1583,8 @@ fun dopenConstraints (loc, env, denv) {str, strs} =
 fun sgiOfDecl (d, loc) =
     case d of
         L'.DCon (x, n, k, c) => [(L'.SgiCon (x, n, k, c), loc)]
+      | L'.DDatatype x => [(L'.SgiDatatype x, loc)]
+      | L'.DDatatypeImp x => [(L'.SgiDatatypeImp x, loc)]
       | L'.DVal (x, n, t, _) => [(L'.SgiVal (x, n, t), loc)]
       | L'.DValRec vis => map (fn (x, n, t, _) => (L'.SgiVal (x, n, t), loc)) vis
       | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)]
@@ -1551,7 +1608,7 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
 
       | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
         let
-            fun folder (sgi2All as (sgi, _), (env, denv)) =
+            fun folder (sgi2All as (sgi, loc), (env, denv)) =
                 let
                     fun seek p =
                         let
@@ -1613,6 +1670,49 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                          NONE
                                    | _ => NONE)
 
+                      | L'.SgiDatatype (x, n2, xncs2) =>
+                        seek (fn sgi1All as (sgi1, _) =>
+                                 case sgi1 of
+                                     L'.SgiDatatype (x', n1, xncs1) =>
+                                     let
+                                         fun mismatched ue =
+                                             (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue));
+                                              SOME (env, denv))
+
+                                         fun good () =
+                                             let
+                                                 val env = E.sgiBinds env sgi2All
+                                                 val env = if n1 = n2 then
+                                                               env
+                                                           else
+                                                               E.pushCNamedAs env x n1 (L'.KType, loc)
+                                                                              (SOME (L'.CNamed n1, loc))
+                                             in
+                                                 SOME (env, denv)
+                                             end
+
+                                         fun xncBad ((x1, _, t1), (x2, _, t2)) =
+                                             String.compare (x1, x2) <> EQUAL
+                                             orelse case (t1, t2) of
+                                                        (NONE, NONE) => false
+                                                      | (SOME t1, SOME t2) =>
+                                                        not (List.null (unifyCons (env, denv) t1 t2))
+                                                      | _ => true
+                                     in
+                                         (if x = x' then
+                                             if length xncs1 <> length xncs2
+                                                orelse ListPair.exists xncBad (xncs1, xncs2) then
+                                                 mismatched NONE
+                                             else
+                                                 good ()
+                                          else
+                                              NONE)
+                                         handle CUnify ue => mismatched (SOME ue)
+                                     end
+                                   | _ => NONE)
+
+                      | L'.SgiDatatypeImp _ => raise Fail "SgiDatatypeImp in subsgn"
+
                       | L'.SgiVal (x, n2, c2) =>
                         seek (fn sgi1All as (sgi1, _) =>
                                  case sgi1 of
@@ -1722,6 +1822,40 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
 
             ([(L'.DCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
         end
+      | L.DDatatype (x, xcs) =>
+        let
+            val k = (L'.KType, loc)
+            val (env, n) = E.pushCNamed env x k NONE
+            val t = (L'.CNamed n, loc)
+
+            val (xcs, (used, env, gs)) =
+                ListUtil.foldlMap
+                (fn ((x, to), (used, env, gs)) =>
+                    let
+                        val (to, t, gs') = case to of
+                                           NONE => (NONE, t, gs)
+                                         | SOME t' =>
+                                           let
+                                               val (t', tk, gs') = elabCon (env, denv) t'
+                                           in
+                                               checkKind env t' tk k;
+                                               (SOME t', (L'.TFun (t', t), loc), gs' @ gs)
+                                           end
+
+                        val (env, n') = E.pushENamed env x t
+                    in
+                        if SS.member (used, x) then
+                            strError env (DuplicateConstructor (x, loc))
+                        else
+                            ();
+                        ((x, n', to), (SS.add (used, x), env, gs'))
+                    end)
+                (SS.empty, env, []) xcs
+        in
+            ([(L'.DDatatype (x, n, xcs), loc)], (env, denv, gs))
+        end
+
+      | L.DDatatypeImp _ => raise Fail "Elaborate DDatatypeImp"
       | L.DVal (x, co, e) =>
         let
             val (c', _, gs1) = case co of
@@ -1975,6 +2109,35 @@ and elabStr (env, denv) (str, loc) =
                               in
                                   ((L'.SgiCon (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs)
                               end
+                            | L'.SgiDatatype (x, n, xncs) =>
+                              let
+                                  val (cons, x) =
+                                      if SS.member (cons, x) then
+                                          (cons, "?" ^ x)
+                                      else
+                                          (SS.add (cons, x), x)
+
+                                  val (xncs, vals) =
+                                      ListUtil.foldlMap
+                                          (fn ((x, n, t), vals) =>
+                                              if SS.member (vals, x) then
+                                                  (("?" ^ x, n, t), vals)
+                                              else
+                                                  ((x, n, t), SS.add (vals, x)))
+                                      vals xncs
+                              in
+                                  ((L'.SgiDatatype (x, n, xncs), loc) :: sgis, cons, vals, sgns, strs)
+                              end
+                            | L'.SgiDatatypeImp (x, n, m1, ms, x') =>
+                              let
+                                  val (cons, x) =
+                                      if SS.member (cons, x) then
+                                          (cons, "?" ^ x)
+                                      else
+                                          (SS.add (cons, x), x)
+                              in
+                                  ((L'.SgiDatatypeImp (x, n, m1, ms, x'), loc) :: sgis, cons, vals, sgns, strs)
+                              end
                             | L'.SgiVal (x, n, c) =>
                               let
                                   val (vals, x) =
diff --git a/src/explify.sml b/src/explify.sml
index 2013f20a..f179ce36 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -95,6 +95,8 @@ 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.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)
@@ -112,6 +114,8 @@ 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.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)
 
diff --git a/src/lacweb.grm b/src/lacweb.grm
index efe26719..08e36356 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -42,9 +42,10 @@ fun uppercaseFirst "" = ""
  | STRING of string | INT of Int64.int | FLOAT of Real64.real
  | SYMBOL of string | CSYMBOL of string
  | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
- | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER
+ | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER | BAR
  | DIVIDE | GT
  | CON | LTYPE | VAL | REC | AND | FOLD | UNIT | KUNIT
+ | DATATYPE | OF
  | TYPE | NAME
  | ARROW | LARROW | DARROW
  | FN | PLUSPLUS | MINUSMINUS | DOLLAR | TWIDDLE
@@ -62,6 +63,10 @@ fun uppercaseFirst "" = ""
  | vali of string * con option * exp
  | valis of (string * con option * exp) list
 
+ | barOpt of unit
+ | dcons of (string * con option) list
+ | dcon of string * con option
+
  | sgn of sgn
  | sgntm of sgn
  | sgi of sgn_item
@@ -73,6 +78,7 @@ fun uppercaseFirst "" = ""
  | kcolon of explicitness
 
  | path of string list * string
+ | cpath of string list * string
  | spath of str
  | mpath of string list
 
@@ -129,6 +135,8 @@ decl   : CON SYMBOL EQ cexp             (DCon (SYMBOL, NONE, cexp), s (CONleft,
        | CON SYMBOL DCOLON kind EQ cexp (DCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright))
        | LTYPE SYMBOL EQ cexp           (DCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp),
                                          s (LTYPEleft, cexpright))
+       | DATATYPE SYMBOL EQ barOpt dcons(DDatatype (SYMBOL, dcons), s (DATATYPEleft, dconsright))
+       | DATATYPE SYMBOL EQ DATATYPE path(DDatatypeImp (SYMBOL, #1 path, #2 path), s (DATATYPEleft, pathright))
        | VAL vali                       (DVal vali, s (VALleft, valiright))
        | VAL REC valis                  (DValRec valis, s (VALleft, valisright))
 
@@ -153,6 +161,15 @@ decl   : CON SYMBOL EQ cexp             (DCon (SYMBOL, NONE, cexp), s (CONleft,
        | CONSTRAINT cterm TWIDDLE cterm (DConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))
        | EXPORT spath                   (DExport spath, s (EXPORTleft, spathright))
 
+barOpt :                                ()
+       | BAR                            ()
+
+dcons  : dcon                           ([dcon])
+       | dcon BAR dcons                 (dcon :: dcons)
+
+dcon   : CSYMBOL                        (CSYMBOL, NONE)
+       | CSYMBOL OF cexp                (CSYMBOL, SOME cexp)
+
 vali   : SYMBOL EQ eexp                 (SYMBOL, NONE, eexp)
        | SYMBOL COLON cexp EQ eexp      (SYMBOL, SOME cexp, eexp)
 
@@ -182,6 +199,8 @@ sgi    : CON SYMBOL DCOLON kind         (SgiConAbs (SYMBOL, kind), s (CONleft, k
        | CON SYMBOL DCOLON kind EQ cexp (SgiCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright))
        | LTYPE SYMBOL EQ cexp           (SgiCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp),
                                          s (LTYPEleft, cexpright))
+       | DATATYPE SYMBOL EQ barOpt dcons(SgiDatatype (SYMBOL, dcons), s (DATATYPEleft, dconsright))
+       | DATATYPE SYMBOL EQ DATATYPE path(SgiDatatypeImp (SYMBOL, #1 path, #2 path), s (DATATYPEleft, pathright))
        | VAL SYMBOL COLON cexp          (SgiVal (SYMBOL, cexp), s (VALleft, cexpright))
 
        | STRUCTURE CSYMBOL COLON sgn    (SgiStr (CSYMBOL, sgn), s (STRUCTUREleft, sgnright))
@@ -239,6 +258,9 @@ kcolon : DCOLON                         (Explicit)
 path   : SYMBOL                         ([], SYMBOL)
        | CSYMBOL DOT path               (let val (ms, x) = path in (CSYMBOL :: ms, x) end)
 
+cpath  : CSYMBOL                        ([], CSYMBOL)
+       | CSYMBOL DOT cpath              (let val (ms, x) = cpath in (CSYMBOL :: ms, x) end)
+
 mpath  : CSYMBOL                        ([CSYMBOL])
        | CSYMBOL DOT mpath              (CSYMBOL :: mpath)
 
@@ -290,6 +312,7 @@ eexp   : eapps                          (eapps)
 eterm  : LPAREN eexp RPAREN             (#1 eexp, s (LPARENleft, RPARENright))
 
        | path                           (EVar path, s (pathleft, pathright))
+       | cpath                          (EVar cpath, s (cpathleft, cpathright))
        | LBRACE rexp RBRACE             (ERecord rexp, s (LBRACEleft, RBRACEright))
        | UNIT                           (ERecord [], s (UNITleft, UNITright))
 
diff --git a/src/lacweb.lex b/src/lacweb.lex
index 4412d9e4..506537e5 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -248,9 +248,12 @@ notags = [^<{\n]+;
 <INITIAL> "__"        => (Tokens.UNDERUNDER (pos yypos, pos yypos + size yytext));
 <INITIAL> "_"         => (Tokens.UNDER (pos yypos, pos yypos + size yytext));
 <INITIAL> "~"         => (Tokens.TWIDDLE (pos yypos, pos yypos + size yytext));
+<INITIAL> "|"         => (Tokens.BAR (pos yypos, pos yypos + size yytext));
 
 <INITIAL> "con"       => (Tokens.CON (pos yypos, pos yypos + size yytext));
 <INITIAL> "type"      => (Tokens.LTYPE (pos yypos, pos yypos + size yytext));
+<INITIAL> "datatype"  => (Tokens.DATATYPE (pos yypos, pos yypos + size yytext));
+<INITIAL> "of"        => (Tokens.OF (pos yypos, pos yypos + size yytext));
 <INITIAL> "val"       => (Tokens.VAL (pos yypos, pos yypos + size yytext));
 <INITIAL> "rec"       => (Tokens.REC (pos yypos, pos yypos + size yytext));
 <INITIAL> "and"       => (Tokens.AND (pos yypos, pos yypos + size yytext));
diff --git a/src/source.sml b/src/source.sml
index 9427d6d6..6439aaa4 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -71,6 +71,8 @@ withtype con = con' located
 datatype sgn_item' =
          SgiConAbs of string * kind
        | SgiCon of string * kind option * con
+       | SgiDatatype of string * (string * con option) list
+       | SgiDatatypeImp of string * string list * string
        | SgiVal of string * con
        | SgiStr of string * sgn
        | SgiSgn of string * sgn
@@ -107,6 +109,8 @@ withtype exp = exp' located
 
 datatype decl' =
          DCon of string * kind option * con
+       | DDatatype of string * (string * con option) list
+       | DDatatypeImp of string * string list * string
        | DVal of string * con option * exp
        | DValRec of (string * con option * exp) list
        | DSgn of string * sgn
diff --git a/src/source_print.sml b/src/source_print.sml
index ba9219be..b69b0b58 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -241,6 +241,18 @@ fun p_exp' par (e, _) =
 
 and p_exp e = p_exp' false e
 
+fun p_datatype (x, cons) =
+    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 t])
+         cons]
+
 fun p_sgn_item (sgi, _) =
     case sgi of
         SgiConAbs (x, k) => box [string "con",
@@ -268,6 +280,17 @@ fun p_sgn_item (sgi, _) =
                                       string "=",
                                       space,
                                       p_con c]
+      | SgiDatatype x => p_datatype x
+      | SgiDatatypeImp (x, ms, x') =>
+        box [string "datatype",
+             space,
+             string x,
+             space,
+             string "=",
+             space,
+             string "datatype",
+             space,
+             p_list_sep (string ".") string (ms @ [x'])]
       | SgiVal (x, c) => box [string "val",
                               space,
                               string x,
@@ -371,6 +394,17 @@ fun p_decl ((d, _) : decl) =
                                     string "=",
                                     space,
                                     p_con c]
+      | DDatatype x => p_datatype x
+      | DDatatypeImp (x, ms, x') =>
+        box [string "datatype",
+             space,
+             string x,
+             space,
+             string "=",
+             space,
+             string "datatype",
+             space,
+             p_list_sep (string ".") string (ms @ [x'])]
       | DVal vi => box [string "val",
                         space,
                         p_vali vi]