diff src/elaborate.sml @ 46:44a1bc863f0f

Corifying functors
author Adam Chlipala <adamc@hcoop.net>
date Thu, 19 Jun 2008 17:55:36 -0400
parents a9f3ce2d1b9b
children 0a5c312de09a
line wrap: on
line diff
--- a/src/elaborate.sml	Thu Jun 19 17:11:24 2008 -0400
+++ b/src/elaborate.sml	Thu Jun 19 17:55:36 2008 -0400
@@ -1015,6 +1015,7 @@
 datatype str_error =
          UnboundStr of ErrorMsg.span * string
        | NotFunctor of L'.sgn
+       | FunctorRebind of ErrorMsg.span
 
 fun strError env err =
     case err of
@@ -1023,6 +1024,8 @@
       | NotFunctor sgn =>
         (ErrorMsg.errorAt (#2 sgn) "Application of non-functor";
          eprefaces' [("Signature", p_sgn env sgn)])
+      | FunctorRebind loc =>
+        ErrorMsg.errorAt loc "Attempt to rebind functor"
 
 val hnormSgn = E.hnormSgn
 
@@ -1391,6 +1394,13 @@
 
                 val (env', n) = E.pushStrNamed env x sgn'
             in
+                case #1 (hnormSgn env sgn') of
+                    L'.SgnFun _ =>
+                    (case #1 str' of
+                         L'.StrFun _ => ()
+                       | _ => strError env (FunctorRebind loc))
+                  | _ => ();
+
                 ((L'.DStr (x, n, sgn', str'), loc), env')
             end
     end