diff src/cjr_env.sml @ 165:e52dfb1e6b19

Datatypes through cjrize, modulo decoding
author Adam Chlipala <adamc@hcoop.net>
date Tue, 29 Jul 2008 13:50:53 -0400
parents 78d59cf0a0cc
children a991431b77eb
line wrap: on
line diff
--- a/src/cjr_env.sml	Tue Jul 29 13:32:07 2008 -0400
+++ b/src/cjr_env.sml	Tue Jul 29 13:50:53 2008 -0400
@@ -118,7 +118,16 @@
 
 fun declBinds env (d, loc) =
     case d of
-        DVal (x, n, t, _) => pushENamed env x n t
+        DDatatype (x, n, xncs) =>
+        let
+            val env = pushTNamed env x n NONE
+        in
+            foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (TNamed n, loc)
+                    | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (TNamed n, loc)), loc))
+            env xncs
+        end
+      | DStruct (n, xts) => pushStruct env n xts
+      | DVal (x, n, t, _) => pushENamed env x n t
       | DFun (fx, n, args, ran, _) =>
         let
             val t = foldl (fn ((_, arg), t) => (TFun (arg, t), loc)) ran args
@@ -132,6 +141,6 @@
                   in
                       pushENamed env fx n t
                   end) env vis
-      | DStruct (n, xts) => pushStruct env n xts
+
 
 end