changeset 808:d8f58d488cfb

Mutual datatypes through Pathcheck
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 May 2009 15:55:15 -0400
parents 61a1f5c5ae2c
children 81fce435e255
files src/cjrize.sml src/jscomp.sml src/mono.sml src/mono_env.sml src/mono_print.sml src/mono_shake.sml src/mono_util.sml src/monoize.sml
diffstat 8 files changed, 81 insertions(+), 70 deletions(-) [+]
line wrap: on
line diff
--- a/src/cjrize.sml	Sat May 16 15:45:12 2009 -0400
+++ b/src/cjrize.sml	Sat May 16 15:55:15 2009 -0400
@@ -483,7 +483,8 @@
 
 fun cifyDecl ((d, loc), sm) =
     case d of
-        L.DDatatype (x, n, xncs) =>
+        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) =>
@@ -497,7 +498,7 @@
                                                        end) sm xncs
         in
             (SOME (L'.DDatatype (dk, x, n, xncs), loc), NONE, sm)
-        end
+        end*)
 
       | L.DVal (x, n, t, e, _) =>
         let
--- a/src/jscomp.sml	Sat May 16 15:45:12 2009 -0400
+++ b/src/jscomp.sml	Sat May 16 15:55:15 2009 -0400
@@ -176,13 +176,14 @@
                     | ((DValRec vis, _), (someTs, nameds)) =>
                       (someTs, foldl (fn ((_, n, _, e, _), nameds) => IM.insert (nameds, n, e))
                                      nameds vis)
-                    | ((DDatatype (_, _, cs), _), state as (someTs, nameds)) =>
-                      if ElabUtil.classifyDatatype cs = Option then
-                          (foldl (fn ((_, n, SOME t), someTs) => IM.insert (someTs, n, t)
-                                   | (_, someTs) => someTs) someTs cs,
-                           nameds)
-                      else
-                          state
+                    | ((DDatatype dts, _), state as (someTs, nameds)) =>
+                      (foldl (fn ((_, _, cs), someTs) =>
+                                 if ElabUtil.classifyDatatype cs = Option then
+                                     foldl (fn ((_, n, SOME t), someTs) => IM.insert (someTs, n, t)
+                                             | (_, someTs) => someTs) someTs cs
+                                 else
+                                     someTs) someTs dts,
+                       nameds)
                     | (_, state) => state)
                   (IM.empty, IM.empty) file
 
--- a/src/mono.sml	Sat May 16 15:45:12 2009 -0400
+++ b/src/mono.sml	Sat May 16 15:55:15 2009 -0400
@@ -121,7 +121,7 @@
 withtype exp = exp' located
 
 datatype decl' =
-         DDatatype of string * int * (string * int * typ option) list
+         DDatatype of (string * int * (string * int * typ option) list) list
        | DVal of string * int * typ * exp * string
        | DValRec of (string * int * typ * exp * string) list
        | DExport of export_kind * string * int * typ list * typ
--- a/src/mono_env.sml	Sat May 16 15:45:12 2009 -0400
+++ b/src/mono_env.sml	Sat May 16 15:55:15 2009 -0400
@@ -109,15 +109,16 @@
 
 fun declBinds env (d, loc) =
     case d of
-        DDatatype (x, n, xncs) =>
-        let
-            val env = pushDatatype env x n xncs
-            val dt = (TDatatype (n, ref (ElabUtil.classifyDatatype xncs, xncs)), loc)
-        in
-            foldl (fn ((x', n', NONE), env) => pushENamed env x' n' dt NONE ""
-                    | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, dt), loc) NONE "")
-            env xncs
-        end
+        DDatatype dts =>
+        foldl (fn ((x, n, xncs), env) =>
+                  let
+                      val env = pushDatatype env x n xncs
+                      val dt = (TDatatype (n, ref (ElabUtil.classifyDatatype xncs, xncs)), loc)
+                  in
+                      foldl (fn ((x', n', NONE), env) => pushENamed env x' n' dt NONE ""
+                              | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, dt), loc) NONE "")
+                            env xncs
+                  end) env dts
       | DVal (x, n, t, e, s) => pushENamed env x n t (SOME e) s
       | DValRec vis => foldl (fn ((x, n, t, e, s), env) => pushENamed env x n t NONE s) env vis
       | DExport _ => env
--- a/src/mono_print.sml	Sat May 16 15:45:12 2009 -0400
+++ b/src/mono_print.sml	Sat May 16 15:55:15 2009 -0400
@@ -377,9 +377,7 @@
     let
         val env = E.pushDatatype env x n cons
     in
-        box [string "datatype",
-             space,
-             string x,
+        box [string x,
              space,
              string "=",
              space,
@@ -393,7 +391,9 @@
 
 fun p_decl env (dAll as (d, _) : decl) =
     case d of
-        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]
       | DVal vi => box [string "val",
                         space,
                         p_vali env vi]
--- a/src/mono_shake.sml	Sat May 16 15:45:12 2009 -0400
+++ b/src/mono_shake.sml	Sat May 16 15:55:15 2009 -0400
@@ -48,8 +48,8 @@
                             | ((DDatabase {expunge = n1, initialize = n2, ...}, _), page_es) => n1 :: n2 :: page_es
                             | (_, page_es) => page_es) [] file
 
-        val (cdef, edef) = foldl (fn ((DDatatype (_, n, xncs), _), (cdef, edef)) =>
-                                     (IM.insert (cdef, n, xncs), edef)
+        val (cdef, edef) = foldl (fn ((DDatatype dts, _), (cdef, edef)) =>
+                                     (foldl (fn ((_, n, xncs), cdef) => IM.insert (cdef, n, xncs)) cdef dts, edef)
                                    | ((DVal (_, n, t, e, _), _), (cdef, edef)) =>
                                      (cdef, IM.insert (edef, n, (t, e)))
                                    | ((DValRec vis, _), (cdef, edef)) =>
@@ -111,7 +111,7 @@
                               NONE => raise Fail "Shake: Couldn't find 'val'"
                             | SOME (t, e) => shakeExp s e) s page_es
     in
-        List.filter (fn (DDatatype (_, n, _), _) => IS.member (#con s, n)
+        List.filter (fn (DDatatype dts, _) => List.exists (fn (_, n, _) => IS.member (#con s, n)) dts
                       | (DVal (_, n, _, _, _), _) => IS.member (#exp s, n)
                       | (DValRec vis, _) => List.exists (fn (_, n, _, _, _) => IS.member (#exp s, n)) vis
                       | (DExport _, _) => true
--- a/src/mono_util.sml	Sat May 16 15:45:12 2009 -0400
+++ b/src/mono_util.sml	Sat May 16 15:55:15 2009 -0400
@@ -466,15 +466,17 @@
 
         and mfd' ctx (dAll as (d, loc)) =
             case d of
-                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 (mft c,
-                                                      fn c' => (x, n, SOME c'))) xncs,
-                        fn xncs' =>
-                           (DDatatype (x, n, xncs'), loc))
+                DDatatype dts =>
+                S.map2 (ListUtil.mapfold (fn (x, n, xncs) =>
+                                             S.map2 (ListUtil.mapfold (fn (x, n, c) =>
+                                                                          case c of
+                                                                              NONE => S.return2 (x, n, c)
+                                                                            | SOME c =>
+                                                                              S.map2 (mft c,
+                                                                                   fn c' => (x, n, SOME c'))) xncs,
+                                                  fn xncs' => (x, n, xncs'))) dts,
+                        fn dts' =>
+                           (DDatatype dts', loc))
               | DVal vi =>
                 S.map2 (mfvi ctx vi,
                      fn vi' =>
@@ -566,21 +568,23 @@
                             let
                                 val ctx' =
                                     case #1 d' of
-                                        DDatatype (x, n, xncs) =>
-                                        let
-                                            val ctx = bind (ctx, Datatype (x, n, xncs))
-                                            val t = (TDatatype (n, ref (ElabUtil.classifyDatatype xncs, xncs)), #2 d')
-                                        in
-                                            foldl (fn ((x, n, to), ctx) =>
-                                                      let
-                                                          val t = case to of
-                                                                      NONE => t
-                                                                    | SOME t' => (TFun (t', t), #2 d')
-                                                      in
-                                                          bind (ctx, NamedE (x, n, t, NONE, ""))
-                                                      end)
-                                            ctx xncs
-                                        end
+                                        DDatatype dts =>
+                                        foldl (fn ((x, n, xncs), ctx) =>
+                                                  let
+                                                      val ctx = bind (ctx, Datatype (x, n, xncs))
+                                                      val t = (TDatatype (n, ref (ElabUtil.classifyDatatype xncs, xncs)),
+                                                               #2 d')
+                                                  in
+                                                      foldl (fn ((x, n, to), ctx) =>
+                                                                let
+                                                                    val t = case to of
+                                                                                NONE => t
+                                                                              | SOME t' => (TFun (t', t), #2 d')
+                                                                in
+                                                                    bind (ctx, NamedE (x, n, t, NONE, ""))
+                                                                end)
+                                                            ctx xncs
+                                                  end) ctx dts
                                       | DVal (x, n, t, e, s) => bind (ctx, NamedE (x, n, t, SOME e, s))
                                       | DValRec vis => foldl (fn ((x, n, t, e, s), ctx) =>
                                                                  bind (ctx, NamedE (x, n, t, NONE, s))) ctx vis
@@ -631,9 +635,10 @@
 
 val maxName = foldl (fn ((d, _) : decl, count) =>
                         case d of
-                            DDatatype (_, n, ns) =>
-                            foldl (fn ((_, n', _), m) => Int.max (n', m))
-                                  (Int.max (n, count)) ns
+                            DDatatype dts =>
+                            foldl (fn ((_, n, ns), count) =>
+                                      foldl (fn ((_, n', _), m) => Int.max (n', m))
+                                            (Int.max (n, count)) ns) count dts
                           | DVal (_, n, _, _, _) => Int.max (n, count)
                           | DValRec vis => foldl (fn ((_, n, _, _, _), count) => Int.max (n, count)) count vis
                           | DExport _ => count
--- a/src/monoize.sml	Sat May 16 15:45:12 2009 -0400
+++ b/src/monoize.sml	Sat May 16 15:55:15 2009 -0400
@@ -3045,27 +3045,30 @@
     in
         case d of
             L.DCon _ => NONE
-          | L.DDatatype _ => raise Fail "Monoize DDatatype"
-          (*| L.DDatatype (x, n, [], xncs) =>
-            let
-                val env' = Env.declBinds env all
-                val d = (L'.DDatatype (x, n, map (fn (x, n, to) => (x, n, Option.map (monoType env') to)) xncs), loc)
-            in
-                SOME (env', fm, [d])
-            end
-          | L.DDatatype ("list", n, [_], [("Nil", _, NONE),
-                                          ("Cons", _, SOME (L.TRecord (L.CRecord (_,
-                                                                                  [((L.CName "1", _),
-                                                                                    (L.CRel 0, _)),
-                                                                                   ((L.CName "2", _),
-                                                                                    (L.CApp ((L.CNamed n', _),
-                                                                                             (L.CRel 0, _)),
-                                                                                     _))]), _), _))]) =>
+          | L.DDatatype [("list", n, [_], [("Nil", _, NONE),
+                                           ("Cons", _, SOME (L.TRecord (L.CRecord (_,
+                                                                                   [((L.CName "1", _),
+                                                                                     (L.CRel 0, _)),
+                                                                                    ((L.CName "2", _),
+                                                                                     (L.CApp ((L.CNamed n', _),
+                                                                                              (L.CRel 0, _)),
+                                                                                      _))]), _), _))])] =>
             if n = n' then
                 NONE
             else
                 poly ()
-          | L.DDatatype _ => poly ()*)
+          | L.DDatatype dts =>
+            let
+                val env' = Env.declBinds env all
+                val dts = map (fn (x, n, [], xncs) =>
+                                  (x, n, map (fn (x, n, to) => (x, n, Option.map (monoType env') to)) xncs)
+                                | _ => (E.errorAt loc "Polymorphic datatype needed too late";
+                                        Print.eprefaces' [("Declaration", CorePrint.p_decl env all)];
+                                        ("", 0, []))) dts
+                val d = (L'.DDatatype dts, loc)
+            in
+                SOME (env', fm, [d])
+            end
           | L.DVal (x, n, t, e, s) =>
             let
                 val (e, fm) = monoExp (env, St.empty, fm) e