[ deadcode ] local private things are not in scope at top-level but i…

…mported things should be

The previous restriction of the top level scope (7f47d51) was a bit draconian and removed
not only local private definitions but all imported things from the scope. This is fixed by this
commit.

src/full/Agda/Syntax/Scope/Base.hs

@@ -12,6 +12,7 @@ module Agda.Syntax.Scope.Base where
 import Control.Arrow (first)
 import Control.Applicative
 import Control.DeepSeq
+import Control.Monad
 
 import Data.Function
 import Data.List as List
@@ -351,6 +352,13 @@ mapScope_ :: (NamesInScope   -> NamesInScope  ) ->
              Scope -> Scope
 mapScope_ fd fm = mapScope (const fd) (const fm)
 
+-- | Same as 'mapScope' but applies the function only on the given name space.
+mapScope' :: NameSpaceId -> (NamesInScope   -> NamesInScope) ->
+                            (ModulesInScope -> ModulesInScope) ->
+                            Scope -> Scope
+mapScope' i fd fm = mapScope (\ j -> if i == j then fd else id)
+                             (\ j -> if i == j then fm else id)
+
 -- | Map monadic functions over the names and modules in a scope.
 mapScopeM :: (Functor m, Applicative m) =>
   (NameSpaceId -> NamesInScope   -> m NamesInScope  ) ->
@@ -540,9 +548,16 @@ renameCanonicalNames renD renM = mapScope_ renameD renameM
 --   Should be a right identity for 'exportedNamesInScope'.
 --   @exportedNamesInScope . restrictPrivate == exportedNamesInScope@.
 restrictPrivate :: Scope -> Scope
-restrictPrivate s
-  = setNameSpace PrivateNS  emptyNameSpace
-  $ s { scopeImports = Map.empty }
+restrictPrivate s = setNameSpace PrivateNS emptyNameSpace
+                  $ s { scopeImports = Map.empty }
+
+-- | Remove private things from the given module from a scope.
+restrictLocalPrivate :: ModuleName -> Scope -> Scope
+restrictLocalPrivate m = mapScope' PrivateNS (Map.mapMaybe rName) (Map.mapMaybe rMod)
+  where
+    check p x = x <$ guard (p x)
+    rName as = check (not . null) $ filter (not . (`isInModule`    m) . anameName) as
+    rMod  as = check (not . null) $ filter (not . (`isSubModuleOf` m) . amodName)  as
 
 -- | Remove names that can only be used qualified (when opening a scope)
 removeOnlyQualified :: Scope -> Scope

src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs

@@ -997,7 +997,7 @@ instance ToAbstract (TopLevel [C.Declaration]) TopLevelInfo where
           outsideDecls <- toAbstract outsideDecls
           (insideScope, insideDecls) <- scopeCheckModule r m am tel $
              toAbstract insideDecls
-          let scope = mapScopeInfo restrictPrivate insideScope
+          let scope = mapScopeInfo (restrictLocalPrivate am) insideScope
           setScope scope
           return $ TopLevelInfo (outsideDecls ++ insideDecls) scope
 

test/interaction/TopScope.agda

@@ -1,8 +1,14 @@
--- Check that F is in not in scope at the top-level (but in the hole).
+
 module _ where
 
+open import Common.Bool
+
+private
+  unused = true
+  used = true
+
 private
-  postulate F : Set → Set
+ module Private where
+  not-in-scope = true
 
-Hole : Set
-Hole = {!!}
+in-scope = used

test/interaction/TopScope.in

@@ -1,3 +1,9 @@
-top_command (cmd_load currentFile [])
-goal_command 0 (cmd_infer Normalised) "F"
-top_command (cmd_infer_toplevel Normalised "F")
+top_command (cmd_load currentFile ["-i.", "-i.."])
+top_command (cmd_load currentFile ["-i.", "-i.."])
+-- These should give not in scope errors:
+top_command (cmd_infer_toplevel Normalised "unused")
+top_command (cmd_infer_toplevel Normalised "used")
+top_command (cmd_infer_toplevel Normalised "Private.not-in-scope")
+-- These should return "Bool"
+top_command (cmd_infer_toplevel Normalised "true")
+top_command (cmd_infer_toplevel Normalised "in-scope")

test/interaction/TopScope.out

@@ -2,14 +2,31 @@ Agda2> (agda2-status-action "")
 (agda2-info-action "*Type-checking*" "" nil)
 (agda2-highlight-clear)
 (agda2-info-action "*Type-checking*" "Checking TopScope (TopScope.agda). " t)
+(agda2-info-action "*Type-checking*" " Checking Common.Bool (Bool.agda). " t)
+(agda2-info-action "*Type-checking*" " Finished Common.Bool. " t)
 (agda2-info-action "*Type-checking*" "Finished TopScope. " t)
-(agda2-status-action "")
-(agda2-info-action "*All Goals*" "?0 : Set " nil)
-((last . 1) . (agda2-goals-action '(0)))
+(agda2-status-action "Checked")
+(agda2-info-action "*All Goals*" "" nil)
+((last . 1) . (agda2-goals-action '()))
 Agda2> (agda2-status-action "")
-(agda2-info-action "*Inferred Type*" "Set → Set" nil)
-((last . 1) . (agda2-goals-action '(0)))
-Agda2> (agda2-info-action "*Error*" "1,1-2 Not in scope: F at 1,1-2 when scope checking F" nil)
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-status-action "Checked")
+(agda2-info-action "*All Goals*" "" nil)
+((last . 1) . (agda2-goals-action '()))
+Agda2> Agda2> (agda2-info-action "*Error*" "1,1-7 Not in scope: unused at 1,1-7 when scope checking unused" nil)
+(agda2-highlight-load-and-delete-action)
+(agda2-status-action "")
+Agda2> (agda2-info-action "*Error*" "1,1-5 Not in scope: used at 1,1-5 when scope checking used" nil)
+(agda2-highlight-load-and-delete-action)
+(agda2-status-action "")
+Agda2> (agda2-info-action "*Error*" "1,1-21 Not in scope: Private.not-in-scope at 1,1-21 when scope checking Private.not-in-scope" nil)
 (agda2-highlight-load-and-delete-action)
 (agda2-status-action "")
+Agda2> Agda2> (agda2-status-action "Checked")
+(agda2-info-action "*Inferred Type*" "Bool" nil)
+((last . 1) . (agda2-goals-action '()))
+Agda2> (agda2-status-action "Checked")
+(agda2-info-action "*Inferred Type*" "Bool" nil)
+((last . 1) . (agda2-goals-action '()))
 Agda2>