diff src/expl_util.sml @ 64:d609820c5834

Proper hiding of shadowed bindings in principal signatures
author Adam Chlipala <adamc@hcoop.net>
date Thu, 26 Jun 2008 08:54:49 -0400
parents 3c1ce1b4eb3d
children c1e21ab42896
line wrap: on
line diff
--- a/src/expl_util.sml	Sun Jun 22 20:11:59 2008 -0400
+++ b/src/expl_util.sml	Thu Jun 26 08:54:49 2008 -0400
@@ -294,6 +294,7 @@
          RelC of string * Expl.kind
        | NamedC of string * Expl.kind
        | Str of string * Expl.sgn
+       | Sgn of string * Expl.sgn
 
 fun mapfoldB {kind, con, sgn_item, sgn, bind} =
     let
@@ -332,6 +333,10 @@
                 S.map2 (sg ctx s,
                      fn s' =>
                         (SgiStr (x, n, s'), loc))
+              | SgiSgn (x, n, s) =>
+                S.map2 (sg ctx s,
+                     fn s' =>
+                        (SgiSgn (x, n, s'), loc))
 
         and sg ctx s acc =
             S.bindP (sg' ctx s acc, sgn ctx)
@@ -347,7 +352,9 @@
                                                    bind (ctx, NamedC (x, k))
                                                  | SgiVal _ => ctx
                                                  | SgiStr (x, _, sgn) =>
-                                                   bind (ctx, Str (x, sgn)),
+                                                   bind (ctx, Str (x, sgn))
+                                                 | SgiSgn (x, _, sgn) =>
+                                                   bind (ctx, Sgn (x, sgn)),
                                                sgi ctx si)) ctx sgis,
                      fn sgis' =>
                         (SgnConst sgis', loc))
@@ -366,6 +373,7 @@
                          S.map2 (con ctx c,
                               fn c' =>
                                  (SgnWhere (sgn', x, c'), loc)))
+              | SgnProj _ => S.return2 sAll
     in
         sg
     end