diff src/expl_env.sml @ 806:0e554bfd6d6a

Mutual datatypes through Corify
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 May 2009 15:22:05 -0400
parents 8688e01ae469
children b2311dfb3158
line wrap: on
line diff
--- a/src/expl_env.sml	Sat May 16 15:14:17 2009 -0400
+++ b/src/expl_env.sml	Sat May 16 15:22:05 2009 -0400
@@ -255,22 +255,33 @@
 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 @@
     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