Mutual datatypes through Corify

6 files changed, 93 insertions, 60 deletions

diff --git a/src/corify.sml b/src/corify.sml
index 65f32fc2..9ac5c84e 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -621,7 +621,8 @@ fun corifyDecl mods (all as (d, loc : EM.span), st) =
         in
             ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st)
         end
-      | L.DDatatype (x, n, xs, xncs) =>
+      | L.DDatatype _ => raise Fail "Corify DDatatype"
+      (*| L.DDatatype (x, n, xs, xncs) =>
         let
             val (st, n) = St.bindCon st x n
             val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
@@ -658,7 +659,7 @@ fun corifyDecl mods (all as (d, loc : EM.span), st) =
                                 end) xncs
         in
             ((L'.DDatatype (x, n, xs, xncs), loc) :: dcons, st)
-        end
+        end*)
       | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
         let
             val (st, n) = St.bindCon st x n
@@ -795,7 +796,8 @@ fun corifyDecl mods (all as (d, loc : EM.span), st) =
                                         trans)
                                    end
 
-                                 | L.SgiDatatype (x, n, xs, xnts) =>
+                                 | L.SgiDatatype _ => raise Fail "Corify SgiDatatype"
+                                 (*| L.SgiDatatype (x, n, xs, xnts) =>
                                    let
                                        val k = (L'.KType, loc)
                                        val dk = ElabUtil.classifyDatatype xnts
@@ -856,7 +858,7 @@ fun corifyDecl mods (all as (d, loc : EM.span), st) =
                                         conmap,
                                         st,
                                         trans)
-                                   end
+                                   end*)
 
                                  | L.SgiVal (x, _, c) =>
                                    let
@@ -1061,7 +1063,7 @@ and corifyStr mods ((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.DDatatype dts => foldl (fn ((_, n', _, _), n) => Int.max (n, n')) n dts
                              | 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
diff --git a/src/expl.sml b/src/expl.sml
index cc40e8b4..4a9acd8a 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -115,7 +115,7 @@ withtype exp = exp' located
 datatype sgn_item' =
          SgiConAbs of string * int * kind
        | SgiCon of string * int * kind * con
-       | SgiDatatype of string * int * string list * (string * int * con option) list
+       | SgiDatatype of (string * int * string list * (string * int * con option) list) list
        | SgiDatatypeImp of string * int * int * string list * string * string list * (string * int * con option) list
        | SgiVal of string * int * con
        | SgiSgn of string * int * sgn
@@ -133,7 +133,7 @@ and sgn = sgn' located
 
 datatype decl' =
          DCon of string * int * kind * con
-       | DDatatype of string * int * string list * (string * int * con option) list
+       | DDatatype of (string * int * string list * (string * int * con option) list) list
        | DDatatypeImp of string * int * int * string list * string * string list * (string * int * con option) list
        | DVal of string * int * con * exp
        | DValRec of (string * int * con * exp) list
diff --git a/src/expl_env.sml b/src/expl_env.sml
index 2bb049a3..836af42c 100644
--- a/src/expl_env.sml
+++ b/src/expl_env.sml
@@ -255,22 +255,33 @@ fun lookupStrNamed (env : env) n =
 fun declBinds env (d, loc) =
     case d of
         DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
-      | DDatatype (x, n, xs, xncs) =>
+      | DDatatype dts =>
         let
-            val env = pushCNamed env x n (KType, loc) NONE
+            fun doOne ((x, n, xs, xncs), env) =
+                let
+                    val k = (KType, loc) 
+                    val nxs = length xs
+                    val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) =>
+                                                       ((CApp (tb, (CRel (nxs - i - 1), loc)), loc),
+                                                        (KArrow (k, kb), loc)))
+                                                   ((CNamed n, loc), k) xs
+                                   
+                    val env = pushCNamed env x n kb NONE
+                in
+                    foldl (fn ((x', n', to), env) =>
+                              let
+                                  val t =
+                                      case to of
+                                          NONE => tb
+                                        | SOME t => (TFun (t, tb), loc)
+                                  val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
+                              in
+                                  pushENamed env x' n' t
+                              end)
+                          env xncs
+                end
         in
-            foldl (fn ((x', n', to), env) =>
-                      let
-                          val t =
-                              case to of
-                                  NONE => (CNamed n, loc)
-                                | SOME t => (TFun (t, (CNamed n, loc)), loc)
-                          val k = (KType, loc)
-                          val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
-                      in
-                          pushENamed env x' n' t
-                      end)
-                  env xncs
+            foldl doOne env dts
         end
       | DDatatypeImp (x, n, m, ms, x', xs, xncs) =>
         let
@@ -337,22 +348,31 @@ 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, xs, xncs) =>
+      | SgiDatatype dts =>
         let
-            val env = pushCNamed env x n (KType, loc) NONE
+            fun doOne ((x, n, xs, xncs), env) =
+                let
+                    val k = (KType, loc)
+                    val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs
+
+                    val env = pushCNamed env x n k' NONE
+                in
+                    foldl (fn ((x', n', to), env) =>
+                              let
+                                  val t =
+                                      case to of
+                                          NONE => (CNamed n, loc)
+                                        | SOME t => (TFun (t, (CNamed n, loc)), loc)
+
+                                  val k = (KType, loc)
+                                  val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
+                              in
+                                  pushENamed env x' n' t
+                              end)
+                          env xncs
+                end
         in
-            foldl (fn ((x', n', to), env) =>
-                      let
-                          val t =
-                              case to of
-                                  NONE => (CNamed n, loc)
-                                | SOME t => (TFun (t, (CNamed n, loc)), loc)
-                          val k = (KType, loc)
-                          val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
-                      in
-                          pushENamed env x' n' t
-                      end)
-                  env xncs
+            foldl doOne env dts
         end
       | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
         let
diff --git a/src/expl_print.sml b/src/expl_print.sml
index 7aa36c6d..0783facc 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -460,9 +460,7 @@ fun p_datatype env (x, n, xs, cons) =
         val env = E.pushCNamed env x n k NONE
         val env = foldl (fn (x, env) => E.pushCRel env x k) env xs
     in
-        box [string "datatype",
-             space,
-             string x,
+        box [string x,
              p_list_sep (box []) (fn x => box [space, string x]) xs,
              space,
              string "=",
@@ -475,7 +473,7 @@ fun p_datatype env (x, n, xs, cons) =
                         cons]
     end
 
-fun p_sgn_item env (sgi, _) =
+fun p_sgn_item env (sgiAll as (sgi, _)) =
     case sgi of
         SgiConAbs (x, n, k) => box [string "con",
                                     space,
@@ -495,7 +493,9 @@ fun p_sgn_item env (sgi, _) =
                                     string "=",
                                     space,
                                     p_con env c]
-      | SgiDatatype x => p_datatype env x
+      | SgiDatatype x => box [string "datatype",
+                              space,
+                              p_list_sep (box [space, string "and", space]) (p_datatype (E.sgiBinds env sgiAll)) x]
       | SgiDatatypeImp (x, _, m1, ms, x', _, _) =>
         let
             val m1x = #1 (E.lookupStrNamed env m1)
@@ -609,7 +609,9 @@ fun p_decl env (dAll as (d, _) : decl) =
                                   string "=",
                                   space,
                                   p_con env c]
-      | DDatatype x => p_datatype env x
+      | DDatatype x => box [string "datatype",
+                            space,
+                            p_list_sep (box [space, string "and", space]) (p_datatype (E.declBinds env dAll)) x]
       | DDatatypeImp (x, _, m1, ms, x', _, _) =>
         let
             val m1x = #1 (E.lookupStrNamed env m1)
diff --git a/src/expl_util.sml b/src/expl_util.sml
index 9e150b87..1932d52d 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -453,15 +453,17 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                         S.map2 (con ctx c,
                              fn c' =>
                                 (SgiCon (x, n, k', c'), loc)))
-              | SgiDatatype (x, n, xs, 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, xs, xncs'), loc))
+              | SgiDatatype dts =>
+                S.map2 (ListUtil.mapfold (fn (x, n, xs, 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' => (x, n, xs, xncs'))) dts,
+                        fn dts' =>
+                           (SgiDatatype dts', loc))
               | SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
                 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
                                              case c of
@@ -496,8 +498,15 @@ 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)))
+                                                 | SgiDatatype dts =>
+                                                   foldl (fn ((x, _, ks, _), ctx) =>
+                                                             let
+                                                                 val k' = (KType, loc)
+                                                                 val k = foldl (fn (_, k) => (KArrow (k', k), loc))
+                                                                               k' ks
+                                                             in
+                                                                 bind (ctx, NamedC (x, k))
+                                                             end) ctx dts
                                                  | SgiDatatypeImp (x, _, _, _, _, _, _) =>
                                                    bind (ctx, NamedC (x, (KType, loc)))
                                                  | SgiVal _ => ctx
diff --git a/src/explify.sml b/src/explify.sml
index 145fccd2..d8bd6bff 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -137,10 +137,10 @@ 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 (x, n, xs, xncs) => SOME (L'.SgiDatatype (x, n, xs,
-                                                                map (fn (x, n, co) =>
-                                                                        (x, n, Option.map explifyCon co)) xncs), loc)*)
-      | L.SgiDatatype _ => raise Fail "Explify SgiDatatype"
+      | L.SgiDatatype dts => SOME (L'.SgiDatatype (map (fn (x, n, xs, xncs) =>
+                                                           (x, n, xs,
+                                                            map (fn (x, n, co) =>
+                                                                    (x, n, Option.map explifyCon co)) xncs)) dts), loc)
       | L.SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
         SOME (L'.SgiDatatypeImp (x, n, m1, ms, s, xs, map (fn (x, n, co) =>
                                                               (x, n, Option.map explifyCon co)) xncs), loc)
@@ -164,10 +164,10 @@ 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 (x, n, xs, xncs) => SOME (L'.DDatatype (x, n, xs,
-                                                            map (fn (x, n, co) =>
-                                                                    (x, n, Option.map explifyCon co)) xncs), loc)*)
-      | L.DDatatype _ => raise Fail "Explify DDatatype"
+      | L.DDatatype dts => SOME (L'.DDatatype (map (fn (x, n, xs, xncs) =>
+                                                       (x, n, xs,
+                                                        map (fn (x, n, co) =>
+                                                                (x, n, Option.map explifyCon co)) xncs)) dts), loc)
       | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
         SOME (L'.DDatatypeImp (x, n, m1, ms, s, xs,
                                map (fn (x, n, co) =>