Proper hiding of shadowed bindings in principal signatures

7 files changed, 86 insertions, 33 deletions

diff --git a/src/elaborate.sml b/src/elaborate.sml
index 64613703..d2d468db 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1580,37 +1580,60 @@ and elabStr env (str, loc) =
             val sgis = map sgiOfDecl ds'
 
             val (sgis, _, _, _, _) =
-                foldr (fn (sgall as (sgi, loc), (sgis, cons, vals, sgns, strs)) =>
+                foldr (fn ((sgi, loc), (sgis, cons, vals, sgns, strs)) =>
                           case sgi of
-                              L'.SgiConAbs (x, _, _) =>
-                              (if SS.member (cons, x) then
-                                   sgnError env (DuplicateCon (loc, x))
-                               else
-                                   ();
-                               (sgall :: sgis, SS.add (cons, x), vals, sgns, strs))
-                            | L'.SgiCon (x, _, _, _) =>
-                              (if SS.member (cons, x) then
-                                   sgnError env (DuplicateCon (loc, x))
-                               else
-                                   ();
-                               (sgall :: sgis, SS.add (cons, x), vals, sgns, strs))
-                            | L'.SgiVal (x, _, _) =>
-                              if SS.member (vals, x) then
-                                  (sgis, cons, vals, sgns, strs)
-                              else
-                                  (sgall :: sgis, cons, SS.add (vals, x), sgns, strs)
-                            | L'.SgiSgn (x, _, _) =>
-                              (if SS.member (sgns, x) then
-                                   sgnError env (DuplicateSgn (loc, x))
-                               else
-                                   ();
-                               (sgall :: sgis, cons, vals, SS.add (sgns, x), strs))
-                            | L'.SgiStr (x, _, _) =>
-                              (if SS.member (strs, x) then
-                                   sgnError env (DuplicateStr (loc, x))
-                               else
-                                   ();
-                               (sgall :: sgis, cons, vals, sgns, SS.add (strs, x))))
+                              L'.SgiConAbs (x, n, k) =>
+                              let
+                                  val (cons, x) =
+                                      if SS.member (cons, x) then
+                                          (cons, "?" ^ x)
+                                      else
+                                          (SS.add (cons, x), x)
+                              in
+                                  ((L'.SgiConAbs (x, n, k), loc) :: sgis, cons, vals, sgns, strs)
+                              end
+                            | L'.SgiCon (x, n, k, c) =>
+                              let
+                                  val (cons, x) =
+                                      if SS.member (cons, x) then
+                                          (cons, "?" ^ x)
+                                      else
+                                          (SS.add (cons, x), x)
+                              in
+                                  ((L'.SgiCon (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs)
+                              end
+                            | L'.SgiVal (x, n, c) =>
+                              let
+                                  val (vals, x) =
+                                      if SS.member (vals, x) then
+                                          (vals, "?" ^ x)
+                                      else
+                                          (SS.add (vals, x), x)
+                              in
+                                  ((L'.SgiVal (x, n, c), loc) :: sgis, cons, vals, sgns, strs)
+                              end
+                            | L'.SgiSgn (x, n, sgn) =>
+                              let
+                                  val (sgns, x) =
+                                      if SS.member (sgns, x) then
+                                          (sgns, "?" ^ x)
+                                      else
+                                          (SS.add (sgns, x), x)
+                              in
+                                  ((L'.SgiSgn (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
+                              end
+ 
+                            | L'.SgiStr (x, n, sgn) =>
+                              let
+                                  val (strs, x) =
+                                      if SS.member (strs, x) then
+                                          (strs, "?" ^ x)
+                                      else
+                                          (SS.add (strs, x), x)
+                              in
+                                  ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
+                              end)
+
                 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
         in
             ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc))
diff --git a/src/expl.sml b/src/expl.sml
index 49633d27..8e9bdfed 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -74,6 +74,7 @@ datatype sgn_item' =
          SgiConAbs of string * int * kind
        | SgiCon of string * int * kind * con
        | SgiVal of string * int * con
+       | SgiSgn of string * int * sgn
        | SgiStr of string * int * sgn
 
 and sgn' =
@@ -81,6 +82,7 @@ and sgn' =
   | SgnVar of int
   | SgnFun of string * int * sgn * sgn
   | SgnWhere of sgn * string * con
+  | SgnProj of int * string list * string
 
 withtype sgn_item = sgn_item' located
 and sgn = sgn' located
diff --git a/src/expl_env.sml b/src/expl_env.sml
index b1bea90b..ad4ec00b 100644
--- a/src/expl_env.sml
+++ b/src/expl_env.sml
@@ -249,6 +249,7 @@ fun sgiBinds env (sgi, _) =
         SgiConAbs (x, n, k) => pushCNamed env x n k NONE
       | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c)
       | SgiVal (x, n, t) => pushENamed env x n t
+      | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn
       | SgiStr (x, n, sgn) => pushStrNamed env x n sgn
 
 end
diff --git a/src/expl_print.sml b/src/expl_print.sml
index 900a4063..aca89834 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -277,6 +277,13 @@ fun p_sgn_item env (sgi, _) =
                                    string ":",
                                    space,
                                    p_sgn env sgn]
+      | SgiSgn (x, n, sgn) => box [string "signature",
+                                   space,
+                                   p_named x n,
+                                   space,
+                                   string "=",
+                                   space,
+                                   p_sgn env sgn]
 
 and p_sgn env (sgn, _) =
     case sgn of
@@ -317,6 +324,17 @@ and p_sgn env (sgn, _) =
                                      string "=",
                                      space,
                                      p_con env c]
+      | SgnProj (m1, ms, x) =>
+        let
+            val (m1x, sgn) = E.lookupStrNamed env m1
+                             
+            val m1s = if !debug then
+                          m1x ^ "__" ^ Int.toString m1
+                      else
+                          m1x
+        in
+            p_list_sep (string ".") string (m1x :: ms @ [x])
+        end
 
 fun p_decl env ((d, _) : decl) =
     case d of
diff --git a/src/expl_util.sig b/src/expl_util.sig
index 40ede9a4..2a6c7abe 100644
--- a/src/expl_util.sig
+++ b/src/expl_util.sig
@@ -82,6 +82,7 @@ structure Sgn : sig
     datatype binder =
              RelC of string * Expl.kind
            | NamedC of string * Expl.kind
+           | Sgn of string * Expl.sgn
            | Str of string * Expl.sgn
 
     val mapfoldB : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder,
diff --git a/src/expl_util.sml b/src/expl_util.sml
index ebdd22d2..23329f3e 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -294,6 +294,7 @@ datatype binder =
          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 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                 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 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                                                    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 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                          S.map2 (con ctx c,
                               fn c' =>
                                  (SgnWhere (sgn', x, c'), loc)))
+              | SgnProj _ => S.return2 sAll
     in
         sg
     end
diff --git a/src/explify.sml b/src/explify.sml
index 03744dba..0c3f5f1f 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -87,7 +87,7 @@ fun explifySgi (sgi, loc) =
       | L.SgiCon (x, n, k, c) => (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc)
       | L.SgiVal (x, n, c) => (L'.SgiVal (x, n, explifyCon c), loc)
       | L.SgiStr (x, n, sgn) => (L'.SgiStr (x, n, explifySgn sgn), loc)
-      | L.SgiSgn _ => raise Fail "Explify SgiSgn"
+      | L.SgiSgn (x, n, sgn) => (L'.SgiSgn (x, n, explifySgn sgn), loc)
 
 and explifySgn (sgn, loc) =
     case sgn of
@@ -95,7 +95,7 @@ and explifySgn (sgn, loc) =
       | L.SgnVar n => (L'.SgnVar n, loc)
       | L.SgnFun (m, n, dom, ran) => (L'.SgnFun (m, n, explifySgn dom, explifySgn ran), loc)
       | L.SgnWhere (sgn, x, c) => (L'.SgnWhere (explifySgn sgn, x, explifyCon c), loc)
-      | L.SgnProj _ => raise Fail "Explify SgnProj"
+      | L.SgnProj x => (L'.SgnProj x, loc)
       | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc)
 
 fun explifyDecl (d, loc : EM.span) =