diff src/elab_env.sml @ 156:34ccd7d2bea8

Start of datatype support
author Adam Chlipala <adamc@hcoop.net>
date Thu, 24 Jul 2008 15:02:03 -0400
parents e3041657d653
children adc4e42e3adc
line wrap: on
line diff
--- a/src/elab_env.sml	Thu Jul 24 11:32:01 2008 -0400
+++ b/src/elab_env.sml	Thu Jul 24 15:02:03 2008 -0400
@@ -292,9 +292,18 @@
 
 fun lookupStr (env : env) x = SM.find (#renameStr env, x)
 
-fun declBinds env (d, _) =
+fun declBinds env (d, loc) =
     case d of
         DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
+      | DDatatype (x, n, xncs) =>
+        let
+            val env = pushCNamedAs env x n (KType, loc) NONE
+        in
+            foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc)
+                    | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc))
+            env xncs
+        end
+      | DDatatypeImp (x, n, m, ms, x') => pushCNamedAs env x n (KType, loc) (SOME (CModProj (m, ms, x'), loc))
       | DVal (x, n, t, _) => pushENamedAs env x n t
       | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamedAs env x n t) env vis
       | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
@@ -303,10 +312,19 @@
       | DConstraint _ => env
       | DExport _ => env
 
-fun sgiBinds env (sgi, _) =
+fun sgiBinds env (sgi, loc) =
     case sgi of
         SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
       | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
+      | SgiDatatype (x, n, xncs) =>
+        let
+            val env = pushCNamedAs env x n (KType, loc) NONE
+        in
+            foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc)
+                    | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc))
+            env xncs
+        end
+      | SgiDatatypeImp (x, n, m1, ms, x') => pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc))
       | SgiVal (x, n, t) => pushENamedAs env x n t
       | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
       | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
@@ -324,6 +342,8 @@
                     case sgi of
                         SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
                       | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
+                      | SgiDatatype (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
+                      | SgiDatatypeImp (x, n, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
                       | SgiVal _ => seek (sgis, sgns, strs, cons)
                       | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons)
                       | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons)
@@ -489,6 +509,8 @@
                     end
                   | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
                   | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
+                  | SgiDatatype (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
+                  | SgiDatatypeImp (x, n, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
                   | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
                   | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
                   | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc)