From 2396dd1bd2bdaeb7608d88bbb2f890b5788852c0 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Sat, 16 May 2009 16:02:17 -0400
Subject: Mutual datatypes through Cjrize

---
 src/cjrize.sml | 43 +++++++++++++++++++++++++------------------
 1 file changed, 25 insertions(+), 18 deletions(-)

(limited to 'src/cjrize.sml')

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)
-- 
cgit v1.2.3