# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1216932684 14400
# Node ID a5ae7b3e37a4d1f309cb13d2ff69d6216950ed05
# Parent  870e8abbe3b99cdfa2bec678f15a398321357602
Normalize datatype choice during SgiDatatypeImp elaboration

diff -r 870e8abbe3b9 -r a5ae7b3e37a4 src/elaborate.sml
--- a/src/elaborate.sml	Thu Jul 24 16:48:47 2008 -0400
+++ b/src/elaborate.sml	Thu Jul 24 16:51:24 2008 -0400
@@ -1337,28 +1337,32 @@
                                        | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
                                   ((L'.StrVar n, loc), sgn) ms
              in
-                 case E.projectDatatype env {sgn = sgn, str = str, field = s} of
-                     NONE => (conError env (UnboundDatatype (loc, s));
-                              ([], (env, denv, gs)))
-                   | SOME xncs =>
-                     let
-                         val k = (L'.KType, loc)
-                         val t = (L'.CModProj (n, ms, s), loc)
-                         val (env, n') = E.pushCNamed env x k (SOME t)
-                         val env = E.pushDatatype env n' xncs
+                 case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of
+                     ((L'.CModProj (n, ms, s), _), gs) =>
+                     (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
+                          NONE => (conError env (UnboundDatatype (loc, s));
+                                   ([], (env, denv, gs)))
+                        | SOME xncs =>
+                          let
+                              val k = (L'.KType, loc)
+                              val t = (L'.CModProj (n, ms, s), loc)
+                              val (env, n') = E.pushCNamed env x k (SOME t)
+                              val env = E.pushDatatype env n' xncs
 
-                         val t = (L'.CNamed n', loc)
-                         val env = foldl (fn ((x, n, to), env) =>
-                                             let
-                                                 val t = case to of
-                                                             NONE => t
-                                                           | SOME t' => (L'.TFun (t', t), loc)
-                                             in
-                                                 E.pushENamedAs env x n t
-                                             end) env xncs
-                     in
-                         ([(L'.SgiDatatypeImp (x, n', n, ms, s), loc)], (env, denv, []))
-                     end
+                              val t = (L'.CNamed n', loc)
+                              val env = foldl (fn ((x, n, to), env) =>
+                                                  let
+                                                      val t = case to of
+                                                                  NONE => t
+                                                                | SOME t' => (L'.TFun (t', t), loc)
+                                                  in
+                                                      E.pushENamedAs env x n t
+                                                  end) env xncs
+                          in
+                              ([(L'.SgiDatatypeImp (x, n', n, ms, s), loc)], (env, denv, gs))
+                          end)
+                   | _ => (strError env (NotDatatype loc);
+                           ([], (env, denv, [])))
              end)
 
       | L.SgiVal (x, c) =>