Mutual datatypes through Cjrize

4 files changed, 100 insertions, 83 deletions

diff --git a/src/cjr.sml b/src/cjr.sml
index 6728e5c8..2b81de1a 100644
--- a/src/cjr.sml
+++ b/src/cjr.sml
@@ -100,7 +100,7 @@ withtype exp = exp' located
 
 datatype decl' =
          DStruct of int * (string * typ) list
-       | DDatatype of datatype_kind * string * int * (string * int * typ option) list
+       | DDatatype of (datatype_kind * string * int * (string * int * typ option) list) list
        | DDatatypeForward of datatype_kind * string * int
        | DVal of string * int * typ * exp
        | DFun of string * int * (string * typ) list * typ * exp
diff --git a/src/cjr_env.sml b/src/cjr_env.sml
index 54dbea17..217efb3a 100644
--- a/src/cjr_env.sml
+++ b/src/cjr_env.sml
@@ -137,15 +137,16 @@ fun classifyDatatype xncs =
 
 fun declBinds env (d, loc) =
     case d of
-        DDatatype (_, x, n, xncs) =>
-        let
-            val env = pushDatatype env x n xncs
-            val dt = (TDatatype (classifyDatatype xncs, n, ref xncs), loc)
-        in
-            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
+        DDatatype dts =>
+        foldl (fn ((_, x, n, xncs), env) =>
+                  let
+                      val env = pushDatatype env x n xncs
+                      val dt = (TDatatype (classifyDatatype xncs, n, ref xncs), loc)
+                  in
+                      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) env dts
       | DDatatypeForward (_, x, n) => pushDatatype env x n []
       | DStruct (n, xts) => pushStruct env n xts
       | DVal (x, n, t, _) => pushENamed env x n t
diff --git a/src/cjr_print.sml b/src/cjr_print.sml
index 85e1c3f7..7f5dccde 100644
--- a/src/cjr_print.sml
+++ b/src/cjr_print.sml
@@ -2037,63 +2037,72 @@ fun p_decl env (dAll as (d, _) : decl) =
                                                         newline]) xts,
                  string "};"]
         end
-      | DDatatype (Enum, x, n, xncs) =>
-        box [string "enum",
-             space,
-             string ("__uwe_" ^ ident x ^ "_" ^ Int.toString n),
-             space,
-             string "{",
-             space,
-             p_list_sep (box [string ",", space]) (fn (x, n, _) =>
-                                                      string ("__uwc_" ^ ident x ^ "_" ^ Int.toString n)) xncs,
-             space,
-             string "};"]
-      | DDatatype (Option, _, _, _) => box []
-      | DDatatype (Default, x, n, xncs) =>
+      | DDatatype dts =>
         let
-            val xncsArgs = List.mapPartial (fn (x, n, NONE) => NONE
-                                             | (x, n, SOME t) => SOME (x, n, t)) xncs
+            val dts = ListMergeSort.sort (fn ((dk1, _, _, _), (dk2, _, _, _)) =>
+                                             dk1 = Enum andalso dk2 <> Enum) dts
+
+            fun p_one (Enum, x, n, xncs) =
+                box [string "enum",
+                     space,
+                     string ("__uwe_" ^ ident x ^ "_" ^ Int.toString n),
+                     space,
+                     string "{",
+                     space,
+                     p_list_sep (box [string ",", space]) (fn (x, n, _) =>
+                                                              string ("__uwc_" ^ ident x ^ "_" ^ Int.toString n)) xncs,
+                     space,
+                     string "};"]
+              | p_one (Option, _, _, _) = box []
+              | p_one (Default, x, n, xncs) =
+                let
+                    val xncsArgs = List.mapPartial (fn (x, n, NONE) => NONE
+                                                     | (x, n, SOME t) => SOME (x, n, t)) xncs
+                in
+                    box [string "enum",
+                         space,
+                         string ("__uwe_" ^ ident x ^ "_" ^ Int.toString n),
+                         space,
+                         string "{",
+                         space,
+                         p_list_sep (box [string ",", space]) (fn (x, n, _) =>
+                                                                  string ("__uwc_" ^ ident x ^ "_" ^ Int.toString n))
+                                    xncs,
+                         space,
+                         string "};",
+                         newline,
+                         newline,
+                         string "struct",
+                         space,
+                         string ("__uwd_" ^ ident x ^ "_" ^ Int.toString n),
+                         space,
+                         string "{",
+                         newline,
+                         string "enum",
+                         space,
+                         string ("__uwe_" ^ ident x ^ "_" ^ Int.toString n),
+                         space,
+                         string "tag;",
+                         newline,
+                         box (case xncsArgs of
+                                  [] => []
+                                | _ => [string "union",
+                                        space,
+                                        string "{",
+                                        newline,
+                                        p_list_sep newline (fn (x, n, t) => box [p_typ env t,
+                                                                                 space,
+                                                                                 string ("uw_" ^ ident x),
+                                                                                 string ";"]) xncsArgs,
+                                        newline,
+                                        string "}",
+                                        space,
+                                        string "data;",
+                                        newline]),
+                         string "};"]
+                end
         in
-            box [string "enum",
-                 space,
-                 string ("__uwe_" ^ ident x ^ "_" ^ Int.toString n),
-                 space,
-                 string "{",
-                 space,
-                 p_list_sep (box [string ",", space]) (fn (x, n, _) =>
-                                                          string ("__uwc_" ^ ident x ^ "_" ^ Int.toString n)) xncs,
-                 space,
-                 string "};",
-                 newline,
-                 newline,
-                 string "struct",
-                 space,
-                 string ("__uwd_" ^ ident x ^ "_" ^ Int.toString n),
-                 space,
-                 string "{",
-                 newline,
-                 string "enum",
-                 space,
-                 string ("__uwe_" ^ ident x ^ "_" ^ Int.toString n),
-                 space,
-                 string "tag;",
-                 newline,
-                 box (case xncsArgs of
-                          [] => []
-                        | _ => [string "union",
-                                space,
-                                string "{",
-                                newline,
-                                p_list_sep newline (fn (x, n, t) => box [p_typ env t,
-                                                                         space,
-                                                                         string ("uw_" ^ ident x),
-                                                                         string ";"]) xncsArgs,
-                                newline,
-                                string "}",
-                                space,
-                                string "data;",
-                                newline]),
-                 string "};"]
+            p_list_sep (box []) p_one dts
         end
 
       | DDatatypeForward _ => box []
diff --git a/src/cjrize.sml b/src/cjrize.sml
index 9c2128bc..c4d916eb 100644
--- a/src/cjrize.sml
+++ b/src/cjrize.sml
@@ -483,22 +483,28 @@ fun cifyExp (eAll as (e, loc), sm) =
 
 fun cifyDecl ((d, loc), sm) =
     case d of
-        L.DDatatype _ => raise Fail "Cjrize DDatatype"
-        (*L.DDatatype (x, n, xncs) =>
-        let
-            val dk = ElabUtil.classifyDatatype xncs
-            val (xncs, sm) = ListUtil.foldlMap (fn ((x, n, to), sm) =>
-                                                   case to of
-                                                       NONE => ((x, n, NONE), sm)
-                                                     | SOME t =>
-                                                       let
-                                                           val (t, sm) = cifyTyp (t, sm)
-                                                       in
-                                                           ((x, n, SOME t), sm)
-                                                       end) sm xncs
-        in
-            (SOME (L'.DDatatype (dk, x, n, xncs), loc), NONE, sm)
-        end*)
+        L.DDatatype dts =>
+        let
+            val (dts, sm) = ListUtil.foldlMap
+                                (fn ((x, n, xncs), sm) =>
+                                    let
+                                        val dk = ElabUtil.classifyDatatype xncs
+                                        val (xncs, sm) = ListUtil.foldlMap (fn ((x, n, to), sm) =>
+                                                                               case to of
+                                                                                   NONE => ((x, n, NONE), sm)
+                                                                                 | SOME t =>
+                                                                                   let
+                                                                                       val (t, sm) = cifyTyp (t, sm)
+                                                                                   in
+                                                                                       ((x, n, SOME t), sm)
+                                                                                   end) sm xncs
+                                    in
+                                        ((dk, x, n, xncs), sm)
+                                    end)
+                                sm dts
+        in
+            (SOME (L'.DDatatype dts, loc), NONE, sm)
+        end
 
       | L.DVal (x, n, t, e, _) =>
         let
@@ -643,8 +649,9 @@ fun cjrize ds =
                                               val (dop, pop, sm) = cifyDecl (d, sm)
 
                                               val dsF = case dop of
-                                                            SOME (L'.DDatatype (dk, x, n, _), loc) =>
-                                                            (L'.DDatatypeForward (dk, x, n), loc) :: dsF
+                                                            SOME (L'.DDatatype dts, loc) =>
+                                                            map (fn (dk, x, n, _) =>
+                                                                    (L'.DDatatypeForward (dk, x, n), loc)) dts @ dsF
                                                           | _ => dsF
 
                                               val dsF = map (fn v => (L'.DStruct v, ErrorMsg.dummySpan)) (Sm.declares sm)