Agda-2.6.0: src/full/Agda/Syntax/Scope/Monad.hs
{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
{-| The scope monad with operations.
-}
module Agda.Syntax.Scope.Monad where
import Prelude hiding (mapM, any, all)
import Control.Arrow (first, second, (***), (&&&))
import Control.Monad hiding (mapM, forM)
import Control.Monad.Writer hiding (mapM, forM)
import Control.Monad.State hiding (mapM, forM)
import Data.Either ( partitionEithers )
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Foldable (any, all)
import Data.Traversable hiding (for)
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Fixity
import Agda.Syntax.Abstract.Name as A
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract (ScopeCopyInfo(..), initCopyInfo)
import Agda.Syntax.Concrete as C
import Agda.Syntax.Concrete.Fixity
import Agda.Syntax.Concrete.Definitions (DeclarationWarning(..)) -- TODO: move the relevant warnings out of there
import Agda.Syntax.Scope.Base
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.Trace ( setCurrentRange )
import Agda.TypeChecking.Positivity.Occurrence (Occurrence)
import Agda.TypeChecking.Warnings ( warning )
import qualified Agda.Utils.AssocList as AssocList
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null (unlessNull)
import Agda.Utils.NonemptyList
import Agda.Utils.Pretty
import Agda.Utils.Size
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
-- * The scope checking monad
-- | To simplify interaction between scope checking and type checking (in
-- particular when chasing imports), we use the same monad.
type ScopeM = TCM
-- * Errors
isDatatypeModule :: A.ModuleName -> ScopeM (Maybe DataOrRecord)
isDatatypeModule m = do
scopeDatatypeModule . Map.findWithDefault __IMPOSSIBLE__ m . scopeModules <$> getScope
-- Debugging
printLocals :: Int -> String -> ScopeM ()
printLocals v s = verboseS "scope.top" v $ do
locals <- getLocalVars
reportSLn "scope.top" v $ s ++ " " ++ prettyShow locals
-- * General operations
getCurrentModule :: ScopeM A.ModuleName
getCurrentModule = setRange noRange . scopeCurrent <$> getScope
setCurrentModule :: A.ModuleName -> ScopeM ()
setCurrentModule m = modifyScope $ \s -> s { scopeCurrent = m }
withCurrentModule :: A.ModuleName -> ScopeM a -> ScopeM a
withCurrentModule new action = do
old <- getCurrentModule
setCurrentModule new
x <- action
setCurrentModule old
return x
withCurrentModule' :: (MonadTrans t, Monad (t ScopeM)) => A.ModuleName -> t ScopeM a -> t ScopeM a
withCurrentModule' new action = do
old <- lift getCurrentModule
lift $ setCurrentModule new
x <- action
lift $ setCurrentModule old
return x
getNamedScope :: A.ModuleName -> ScopeM Scope
getNamedScope m = do
scope <- getScope
case Map.lookup m (scopeModules scope) of
Just s -> return s
Nothing -> do
reportSLn "" 0 $ "ERROR: In scope\n" ++ prettyShow scope ++ "\nNO SUCH SCOPE " ++ prettyShow m
__IMPOSSIBLE__
getCurrentScope :: ScopeM Scope
getCurrentScope = getNamedScope =<< getCurrentModule
-- | Create a new module with an empty scope.
-- (@Just@ if it is a datatype or record module.)
createModule :: Maybe DataOrRecord -> A.ModuleName -> ScopeM ()
createModule b m = do
reportSLn "scope.createModule" 10 $ "createModule " ++ prettyShow m
s <- getCurrentScope
let parents = scopeName s : scopeParents s
sm = emptyScope { scopeName = m
, scopeParents = parents
, scopeDatatypeModule = b }
-- Andreas, 2015-07-02: internal error if module is not new.
-- Ulf, 2016-02-15: It's not new if multiple imports (#1770).
modifyScopes $ Map.insertWith const m sm
-- | Apply a function to the scope map.
modifyScopes :: (Map A.ModuleName Scope -> Map A.ModuleName Scope) -> ScopeM ()
modifyScopes f = modifyScope $ \s -> s { scopeModules = f $ scopeModules s }
-- | Apply a function to the given scope.
modifyNamedScope :: A.ModuleName -> (Scope -> Scope) -> ScopeM ()
modifyNamedScope m f = modifyScopes $ Map.adjust f m
setNamedScope :: A.ModuleName -> Scope -> ScopeM ()
setNamedScope m s = modifyNamedScope m $ const s
-- | Apply a monadic function to the top scope.
modifyNamedScopeM :: A.ModuleName -> (Scope -> ScopeM (a, Scope)) -> ScopeM a
modifyNamedScopeM m f = do
(a, s) <- f =<< getNamedScope m
setNamedScope m s
return a
-- | Apply a function to the current scope.
modifyCurrentScope :: (Scope -> Scope) -> ScopeM ()
modifyCurrentScope f = getCurrentModule >>= (`modifyNamedScope` f)
modifyCurrentScopeM :: (Scope -> ScopeM (a, Scope)) -> ScopeM a
modifyCurrentScopeM f = getCurrentModule >>= (`modifyNamedScopeM` f)
-- | Apply a function to the public or private name space.
modifyCurrentNameSpace :: NameSpaceId -> (NameSpace -> NameSpace) -> ScopeM ()
modifyCurrentNameSpace acc f = modifyCurrentScope $ updateScopeNameSpaces $
AssocList.updateAt acc f
pushContextPrecedence :: Precedence -> ScopeM PrecedenceStack
pushContextPrecedence p = do
old <- scopePrecedence <$> getScope
modifyScope_ $ \ s -> s { scopePrecedence = pushPrecedence p $ scopePrecedence s }
return old
setContextPrecedence :: PrecedenceStack -> ScopeM ()
setContextPrecedence ps = modifyScope_ $ \ s -> s { scopePrecedence = ps }
withContextPrecedence :: Precedence -> ScopeM a -> ScopeM a
withContextPrecedence p = bracket_ (pushContextPrecedence p) setContextPrecedence
getLocalVars :: ScopeM LocalVars
getLocalVars = scopeLocals <$> getScope
modifyLocalVars :: (LocalVars -> LocalVars) -> ScopeM ()
modifyLocalVars = modifyScope_ . updateScopeLocals
setLocalVars :: LocalVars -> ScopeM ()
setLocalVars vars = modifyLocalVars $ const vars
-- | Run a computation without changing the local variables.
withLocalVars :: ScopeM a -> ScopeM a
withLocalVars = bracket_ getLocalVars setLocalVars
getVarsToBind :: ScopeM LocalVars
getVarsToBind = scopeVarsToBind <$> getScope
addVarToBind :: C.Name -> LocalVar -> ScopeM ()
addVarToBind x y = modifyScope_ $ updateVarsToBind $ AssocList.insert x y
-- | After collecting some variable names in the scopeVarsToBind,
-- bind them all simultaneously.
bindVarsToBind :: ScopeM ()
bindVarsToBind = do
vars <- getVarsToBind
modifyLocalVars (vars++)
printLocals 10 "bound variables:"
modifyScope_ $ setVarsToBind []
-- * Names
-- | Create a fresh abstract name from a concrete name.
--
-- This function is used when we translate a concrete name
-- in a binder. The 'Range' of the concrete name is
-- saved as the 'nameBindingSite' of the abstract name.
freshAbstractName :: Fixity' -> C.Name -> ScopeM A.Name
freshAbstractName fx x = do
i <- fresh
return $ A.Name
{ nameId = i
, nameConcrete = x
, nameBindingSite = getRange x
, nameFixity = fx
, nameIsRecordName = False
}
-- | @freshAbstractName_ = freshAbstractName noFixity'@
freshAbstractName_ :: C.Name -> ScopeM A.Name
freshAbstractName_ = freshAbstractName noFixity'
-- | Create a fresh abstract qualified name.
freshAbstractQName :: Fixity' -> C.Name -> ScopeM A.QName
freshAbstractQName fx x = do
y <- freshAbstractName fx x
m <- getCurrentModule
return $ A.qualify m y
freshAbstractQName' :: C.Name -> ScopeM A.QName
freshAbstractQName' x = do
fx <- getConcreteFixity x
freshAbstractQName fx x
-- * Resolving names
-- | Look up the abstract name referred to by a given concrete name.
resolveName :: C.QName -> ScopeM ResolvedName
resolveName = resolveName' allKindsOfNames Nothing
-- | Look up the abstract name corresponding to a concrete name of
-- a certain kind and/or from a given set of names.
-- Sometimes we know already that we are dealing with a constructor
-- or pattern synonym (e.g. when we have parsed a pattern).
-- Then, we can ignore conflicting definitions of that name
-- of a different kind. (See issue 822.)
resolveName' ::
[KindOfName] -> Maybe (Set A.Name) -> C.QName -> ScopeM ResolvedName
resolveName' kinds names x = do
scope <- getScope
let vars = AssocList.mapKeysMonotonic C.QName $ scopeLocals scope
retVar y = return . VarName y{ nameConcrete = unqualify x }
aName = A.qnameName . anameName
case lookup x vars of
-- Case: we have a local variable x.
Just (LocalVar y b []) -> retVar y b
-- Case: ... but is (perhaps) shadowed by some imports.
Just (LocalVar y b ys) -> case names of
Nothing -> shadowed ys
Just ns -> case filter (\ y -> aName y `Set.member` ns) ys of
[] -> retVar y b
ys -> shadowed ys
where
shadowed ys =
typeError $ AmbiguousName x $ A.qualify_ y :! map anameName ys
-- Case: we do not have a local variable x.
Nothing -> do
-- Consider only names of one of the given kinds
let filtKind = filter $ \ y -> anameKind (fst y) `elem` kinds
-- Consider only names in the given set of names
filtName = filter $ \ y -> maybe True (Set.member (aName (fst y))) names
caseListNe (filtKind $ filtName $ scopeLookup' x scope) (return UnknownName) $ \ case
ds | all ((ConName ==) . anameKind . fst) ds ->
return $ ConstructorName $ fmap (upd . fst) ds
ds | all ((FldName ==) . anameKind . fst) ds ->
return $ FieldName $ fmap (upd . fst) ds
ds | all ((PatternSynName ==) . anameKind . fst) ds ->
return $ PatternSynResName $ fmap (upd . fst) ds
(d, a) :! [] ->
return $ DefinedName a $ upd d
ds -> typeError $ AmbiguousName x (fmap (anameName . fst) ds)
where
upd d = updateConcreteName d $ unqualify x
updateConcreteName :: AbstractName -> C.Name -> AbstractName
updateConcreteName d@(AbsName { anameName = A.QName qm qn }) x =
d { anameName = A.QName (setRange (getRange x) qm) (qn { nameConcrete = x }) }
-- | Look up a module in the scope.
resolveModule :: C.QName -> ScopeM AbstractModule
resolveModule x = do
ms <- scopeLookup x <$> getScope
caseListNe ms (typeError $ NoSuchModule x) $ \ case
AbsModule m why :! [] -> return $ AbsModule (m `withRangeOf` x) why
ms -> typeError $ AmbiguousModule x (fmap amodName ms)
-- | Get the fixity of a not yet bound name.
getConcreteFixity :: C.Name -> ScopeM Fixity'
getConcreteFixity x = Map.findWithDefault noFixity' x . scopeFixities <$> getScope
-- | Get the polarities of a not yet bound name.
getConcretePolarity :: C.Name -> ScopeM (Maybe [Occurrence])
getConcretePolarity x = Map.lookup x . scopePolarities <$> getScope
instance MonadFixityError ScopeM where
throwMultipleFixityDecls xs = case xs of
(x, _) : _ -> setCurrentRange (getRange x) $ typeError $ MultipleFixityDecls xs
[] -> __IMPOSSIBLE__
throwMultiplePolarityPragmas xs = case xs of
x : _ -> setCurrentRange (getRange x) $ typeError $ MultiplePolarityPragmas xs
[] -> __IMPOSSIBLE__
warnUnknownNamesInFixityDecl = warning . NicifierIssue . UnknownNamesInFixityDecl
warnUnknownNamesInPolarityPragmas = warning . NicifierIssue . UnknownNamesInPolarityPragmas
warnUnknownFixityInMixfixDecl = warning . NicifierIssue . UnknownFixityInMixfixDecl
warnPolarityPragmasButNotPostulates = warning . NicifierIssue . PolarityPragmasButNotPostulates
-- | Collect the fixity/syntax declarations and polarity pragmas from the list
-- of declarations and store them in the scope.
computeFixitiesAndPolarities :: DoWarn -> [C.Declaration] -> ScopeM a -> ScopeM a
computeFixitiesAndPolarities warn ds ret = do
(fixs0, pols0) <- (scopeFixities &&& scopePolarities) <$> getScope
(fixs, pols) <- fixitiesAndPolarities warn ds
modifyScope $ \ s -> s { scopeFixities = fixs, scopePolarities = pols }
x <- ret
modifyScope $ \ s -> s { scopeFixities = fixs0, scopePolarities = pols0 }
return x
-- | Get the notation of a name. The name is assumed to be in scope.
getNotation
:: C.QName
-> Set A.Name
-- ^ The name must correspond to one of the names in this set.
-> ScopeM NewNotation
getNotation x ns = do
r <- resolveName' allKindsOfNames (Just ns) x
case r of
VarName y _ -> return $ namesToNotation x y
DefinedName _ d -> return $ notation d
FieldName ds -> return $ oneNotation ds
ConstructorName ds -> return $ oneNotation ds
PatternSynResName n -> return $ oneNotation n
UnknownName -> __IMPOSSIBLE__
where
notation = namesToNotation x . qnameName . anameName
oneNotation ds =
case mergeNotations $ map notation $ toList ds of
[n] -> n
_ -> __IMPOSSIBLE__
-- * Binding names
-- | Bind a variable.
bindVariable
:: Binder -- ^ @λ@, @Π@, @let@, ...?
-> C.Name -- ^ Concrete name.
-> A.Name -- ^ Abstract name.
-> ScopeM ()
bindVariable b x y = modifyLocalVars $ AssocList.insert x $ LocalVar y b []
-- | Temporarily unbind a variable. Used for non-recursive lets.
unbindVariable :: C.Name -> ScopeM a -> ScopeM a
unbindVariable x = bracket_ (getLocalVars <* modifyLocalVars (AssocList.delete x)) (modifyLocalVars . const)
-- | Bind a defined name. Must not shadow anything.
bindName :: Access -> KindOfName -> C.Name -> A.QName -> ScopeM ()
bindName acc kind x y = bindName' acc kind NoMetadata x y
bindName' :: Access -> KindOfName -> NameMetadata -> C.Name -> A.QName -> ScopeM ()
bindName' acc kind meta x y = do
when (isNoName x) $ modifyScopes $ Map.map $ removeNameFromScope PrivateNS x
r <- resolveName (C.QName x)
ys <- case r of
-- Binding an anonymous declaration always succeeds.
-- In case it's not the first one, we simply remove the one that came before
_ | isNoName x -> success
DefinedName _ d -> clash $ anameName d
VarName z _ -> clash $ A.qualify (mnameFromList []) z
FieldName ds -> ambiguous FldName ds
ConstructorName ds -> ambiguous ConName ds
PatternSynResName n -> ambiguous PatternSynName n
UnknownName -> success
let ns = if isNoName x then PrivateNS else localNameSpace acc
modifyCurrentScope $ addNamesToScope ns x ys
where
success = return [ AbsName y kind Defined meta ]
clash = typeError . ClashingDefinition (C.QName x)
ambiguous k ds =
if kind == k && all ((== k) . anameKind) ds
then success else clash $ anameName (headNe ds)
-- | Rebind a name. Use with care!
-- Ulf, 2014-06-29: Currently used to rebind the name defined by an
-- unquoteDecl, which is a 'QuotableName' in the body, but a 'DefinedName'
-- later on.
rebindName :: Access -> KindOfName -> C.Name -> A.QName -> ScopeM ()
rebindName acc kind x y = do
modifyCurrentScope $ removeNameFromScope (localNameSpace acc) x
bindName acc kind x y
-- | Bind a module name.
bindModule :: Access -> C.Name -> A.ModuleName -> ScopeM ()
bindModule acc x m = modifyCurrentScope $
addModuleToScope (localNameSpace acc) x (AbsModule m Defined)
-- | Bind a qualified module name. Adds it to the imports field of the scope.
bindQModule :: Access -> C.QName -> A.ModuleName -> ScopeM ()
bindQModule acc q m = modifyCurrentScope $ \s ->
s { scopeImports = Map.insert q m (scopeImports s) }
-- * Module manipulation operations
-- | Clear the scope of any no names.
stripNoNames :: ScopeM ()
stripNoNames = modifyScopes $ Map.map $ mapScope_ stripN stripN id
where
stripN = Map.filterWithKey $ const . not . isNoName
type WSM = StateT ScopeMemo ScopeM
data ScopeMemo = ScopeMemo
{ memoNames :: A.Ren A.QName
, memoModules :: [(ModuleName, (ModuleName, Bool))]
-- ^ Bool: did we copy recursively? We need to track this because we don't
-- copy recursively when creating new modules for reexported functions
-- (issue1985), but we might need to copy recursively later.
}
memoToScopeInfo :: ScopeMemo -> ScopeCopyInfo
memoToScopeInfo (ScopeMemo names mods) =
ScopeCopyInfo { renNames = names
, renModules = [ (x, y) | (x, (y, _)) <- mods ] }
-- | Create a new scope with the given name from an old scope. Renames
-- public names in the old scope to match the new name and returns the
-- renamings.
copyScope :: C.QName -> A.ModuleName -> Scope -> ScopeM (Scope, ScopeCopyInfo)
copyScope oldc new0 s = (inScopeBecause (Applied oldc) *** memoToScopeInfo) <$> runStateT (copy new0 s) (ScopeMemo [] [])
where
copy :: A.ModuleName -> Scope -> WSM Scope
copy new s = do
lift $ reportSLn "scope.copy" 20 $ "Copying scope " ++ prettyShow old ++ " to " ++ prettyShow new
lift $ reportSLn "scope.copy" 50 $ prettyShow s
s0 <- lift $ getNamedScope new
-- Delete private names, then copy names and modules. Recompute inScope
-- set rather than trying to copy it.
s' <- recomputeInScopeSets <$> mapScopeM_ copyD copyM return (setNameSpace PrivateNS emptyNameSpace s)
-- Fix name and parent.
return $ s' { scopeName = scopeName s0
, scopeParents = scopeParents s0
}
where
rnew = getRange new
new' = killRange new
newL = A.mnameToList new'
old = scopeName s
copyD :: NamesInScope -> WSM NamesInScope
copyD = traverse $ mapM $ onName renName
copyM :: ModulesInScope -> WSM ModulesInScope
copyM = traverse $ mapM $ lensAmodName renMod
onName :: (A.QName -> WSM A.QName) -> AbstractName -> WSM AbstractName
onName f d =
case anameKind d of
PatternSynName -> return d -- Pattern synonyms are simply aliased, not renamed
_ -> lensAnameName f d
-- Adding to memo structure.
addName x y = modify $ \ i -> i { memoNames = (x, y) : memoNames i }
addMod x y rec = modify $ \ i -> i { memoModules = (x, (y, rec)) : filter ((/= x) . fst) (memoModules i) }
-- Querying the memo structure.
findName x = lookup x <$> gets memoNames
findMod x = lookup x <$> gets memoModules
refresh :: A.Name -> WSM A.Name
refresh x = do
i <- lift fresh
return $ x { A.nameId = i }
-- Change a binding M.x -> old.M'.y to M.x -> new.M'.y
renName :: A.QName -> WSM A.QName
renName x = do
-- Issue 1985: For re-exported names we can't use new' as the
-- module, since it has the wrong telescope. Example:
--
-- module M1 (A : Set) where
-- module M2 (B : Set) where
-- postulate X : Set
-- module M3 (C : Set) where
-- module M4 (D E : Set) where
-- open M2 public
--
-- module M = M1.M3 A C
--
-- Here we can't copy M1.M2.X to M.M4.X since we need
-- X : (B : Set) → Set, but M.M4 has telescope (D E : Set). Thus, we
-- would break the invariant that all functions in a module share the
-- module telescope. Instead we copy M1.M2.X to M.M2.X for a fresh
-- module M2 that gets the right telescope.
m <- case x `isInModule` old of
True -> return new'
False -> renMod' False (qnameModule x)
-- Don't copy recursively here, we only know that the
-- current name x should be copied.
-- Generate a fresh name for the target.
-- Andreas, 2015-08-11 Issue 1619:
-- Names copied by a module macro should get the module macro's
-- range as declaration range
-- (maybe rather the one of the open statement).
-- For now, we just set their range
-- to the new module name's one, which fixes issue 1619.
y <- setRange rnew . A.qualify m <$> refresh (qnameName x)
lift $ reportSLn "scope.copy" 50 $ " Copying " ++ prettyShow x ++ " to " ++ prettyShow y
addName x y
return y
-- Change a binding M.x -> old.M'.y to M.x -> new.M'.y
renMod :: A.ModuleName -> WSM A.ModuleName
renMod = renMod' True
renMod' rec x = do
-- Andreas, issue 1607:
-- If we have already copied this module, return the copy.
z <- findMod x
case z of
Just (y, False) | rec -> y <$ copyRec x y
Just (y, _) -> return y
Nothing -> do
-- Ulf (issue 1985): If copying a reexported module we put it at the
-- top-level, to make sure we don't mess up the invariant that all
-- (abstract) names M.f share the argument telescope of M.
let newM | x `isSubModuleOf` old = newL
| otherwise = mnameToList new0
y <- do
-- Andreas, Jesper, 2015-07-02: Issue 1597
-- Don't blindly drop a prefix of length of the old qualifier.
-- If things are imported by open public they do not have the old qualifier
-- as prefix. Those need just to be linked, not copied.
-- return $ A.mnameFromList $ (newL ++) $ drop (size old) $ A.mnameToList x
-- caseMaybe (stripPrefix (A.mnameToList old) (A.mnameToList x)) (return x) $ \ suffix -> do
-- return $ A.mnameFromList $ newL ++ suffix
-- Ulf, 2016-02-22: #1726
-- We still need to copy modules from 'open public'. Same as in renName.
y <- refresh (last $ A.mnameToList x)
return $ A.mnameFromList $ newM ++ [y]
-- Andreas, Jesper, 2015-07-02: Issue 1597
-- Don't copy a module over itself, it will just be emptied of its contents.
if (x == y) then return x else do
lift $ reportSLn "scope.copy" 50 $ " Copying module " ++ prettyShow x ++ " to " ++ prettyShow y
addMod x y rec
lift $ createModule Nothing y
-- We need to copy the contents of included modules recursively (only when 'rec')
when rec $ copyRec x y
return y
where
copyRec x y = do
s0 <- lift $ getNamedScope x
s <- withCurrentModule' y $ copy y s0
lift $ modifyNamedScope y (const s)
-- | Apply an import directive and check that all the names mentioned actually
-- exist.
applyImportDirectiveM :: C.QName -> C.ImportDirective -> Scope -> ScopeM (A.ImportDirective, Scope)
applyImportDirectiveM m (ImportDirective rng usn' hdn' ren' public) scope = do
-- We start by checking that all of the names talked about in the import
-- directive do exist. If some do not then we remove them and raise a warning.
let (missingExports, namesA) = checkExist $ fromUsing usn' ++ hdn' ++ map renFrom ren'
unless (null missingExports) $ setCurrentRange rng $ do
reportSLn "scope.import.apply" 20 $ "non existing names: " ++ prettyShow missingExports
warning $ ModuleDoesntExport m missingExports
-- We can now define a cleaned-up version of the input
let usn = fromUsing usn' List.\\ missingExports
let hdn = hdn' List.\\ missingExports
let ren = filter (\ r -> renFrom r `notElem` missingExports) ren'
let dir = (\ u -> ImportDirective rng u hdn ren public)
$ case usn' of { Using{} -> Using usn; _ -> UseEverything }
-- As well as convenient shorthands for defined names and names brought into scope
let names = map renFrom ren ++ hdn ++ usn
let definedNames = map renTo ren
let targetNames = usn ++ definedNames
let extraModules =
[ x | ImportedName x <- names
, let mx = ImportedModule x
, notElem mx missingExports
, notElem mx names
]
dir' = addExtraModules extraModules dir
dir' <- sanityCheck dir' names
-- Check for duplicate imports in a single import directive.
-- @dup@ : To be imported names that are mentioned more than once.
let dup = targetNames List.\\ List.nub targetNames
unless (null dup) $ typeError $ DuplicateImports m dup
-- Apply the import directive.
let scope' = applyImportDirective dir' scope
-- Look up the defined names in the new scope.
let namesInScope' = (allNamesInScope scope' :: ThingsInScope AbstractName)
let modulesInScope' = (allNamesInScope scope' :: ThingsInScope AbstractModule)
let look x = headWithDefault __IMPOSSIBLE__ . Map.findWithDefault __IMPOSSIBLE__ x
-- We set the ranges to the ranges of the concrete names in order to get
-- highlighting for the names in the import directive.
let definedA = for definedNames $ \case
ImportedName x -> ImportedName . (x,) . setRange (getRange x) . anameName $ look x namesInScope'
ImportedModule x -> ImportedModule . (x,) . setRange (getRange x) . amodName $ look x modulesInScope'
let adir = mapImportDir namesA definedA dir
return (adir, scope') -- TODO Issue 1714: adir
where
-- | Names in the @using@ directive
fromUsing :: Using' a b -> [ImportedName' a b]
fromUsing u = case u of
Using xs -> xs
UseEverything -> []
sanityCheck dir names =
case (using dir, hiding dir) of
(Using xs, ys) -> do
let uselessHiding = [ x | x@ImportedName{} <- ys ] ++
[ x | x@(ImportedModule y) <- ys, ImportedName y `notElem` names ]
unless (null uselessHiding) $ typeError $ GenericError $ "Hiding " ++ List.intercalate ", " (map prettyShow uselessHiding)
++ " has no effect"
return dir{ hiding = [] }
_ -> return dir
addExtraModules :: [C.Name] -> C.ImportDirective -> C.ImportDirective
addExtraModules extra dir =
dir{ using =
case using dir of
Using xs -> Using $ concatMap addExtra xs
UseEverything -> UseEverything
, hiding = concatMap addExtra (hiding dir)
, impRenaming = concatMap extraRenaming (impRenaming dir)
}
where
addExtra f@(ImportedName y) | elem y extra = [f, ImportedModule y]
addExtra m = [m]
extraRenaming r@(Renaming from to rng) =
case (from, to) of
(ImportedName y, ImportedName z) | elem y extra ->
[r, Renaming (ImportedModule y) (ImportedModule z) rng]
_ -> [r]
-- | Names and modules (abstract) in scope before the import.
namesInScope = (allNamesInScope scope :: ThingsInScope AbstractName)
modulesInScope = (allNamesInScope scope :: ThingsInScope AbstractModule)
-- | AST versions of the concrete names passed as an argument.
-- We get back a pair consisting of a list of missing exports first,
-- and a list of successful imports second.
checkExist :: [ImportedName] -> ([ImportedName], [ImportedName' (C.Name, A.QName) (C.Name, A.ModuleName)])
checkExist xs = partitionEithers $ for xs $ \ name -> case name of
ImportedName x -> ImportedName . (x,) . setRange (getRange x) . anameName <$> resolve name x namesInScope
ImportedModule x -> ImportedModule . (x,) . setRange (getRange x) . amodName <$> resolve name x modulesInScope
where resolve :: Ord a => err -> a -> Map a [b] -> Either err b
resolve err x m = maybe (Left err) (Right . head) $ Map.lookup x m
-- | A finite map for @ImportedName@s.
lookupImportedName
:: (Eq a, Eq b)
=> ImportedName' a b
-> [ImportedName' (a,c) (b,d)]
-> ImportedName' c d
lookupImportedName (ImportedName x) = loop where
loop [] = __IMPOSSIBLE__
loop (ImportedName (y,z) : _) | x == y = ImportedName z
loop (_ : ns) = loop ns
lookupImportedName (ImportedModule x) = loop where
loop [] = __IMPOSSIBLE__
loop (ImportedModule (y,z) : _) | x == y = ImportedModule z
loop (_ : ns) = loop ns
-- | Translation of @ImportDirective@.
mapImportDir
:: (Eq n1, Eq m1)
=> [ImportedName' (n1,n2) (m1,m2)] -- ^ Translation of imported names.
-> [ImportedName' (n1,n2) (m1,m2)] -- ^ Translation of names defined by this import.
-> ImportDirective' n1 m1
-> ImportDirective' n2 m2
mapImportDir src tgt (ImportDirective r u h ren open) =
ImportDirective r
(mapUsing src u)
(map (`lookupImportedName` src) h)
(map (mapRenaming src tgt) ren) open
-- | Translation of @Using or Hiding@.
mapUsing
:: (Eq n1, Eq m1)
=> [ImportedName' (n1,n2) (m1,m2)] -- ^ Translation of names in @using@ or @hiding@ list.
-> Using' n1 m1
-> Using' n2 m2
mapUsing src UseEverything = UseEverything
mapUsing src (Using xs) = Using $ map (`lookupImportedName` src) xs
-- | Translation of @Renaming@.
mapRenaming
:: (Eq n1, Eq m1)
=> [ImportedName' (n1,n2) (m1,m2)] -- ^ Translation of 'renFrom' names and module names.
-> [ImportedName' (n1,n2) (m1,m2)] -- ^ Translation of 'rento' names and module names.
-> Renaming' n1 m1 -- ^ Renaming before translation (1).
-> Renaming' n2 m2 -- ^ Renaming after translation (2).
mapRenaming src tgt (Renaming from to r) =
Renaming (lookupImportedName from src) (lookupImportedName to tgt) r
data OpenKind = LetOpenModule | TopOpenModule
noGeneralizedVarsIfLetOpen :: OpenKind -> Scope -> Scope
noGeneralizedVarsIfLetOpen TopOpenModule = id
noGeneralizedVarsIfLetOpen LetOpenModule = disallowGeneralizedVars
-- | Open a module.
openModule_ :: OpenKind -> C.QName -> C.ImportDirective -> ScopeM A.ImportDirective
openModule_ kind cm dir = do
current <- getCurrentModule
m <- amodName <$> resolveModule cm
let acc | not (publicOpen dir) = PrivateNS
| m `isSubModuleOf` current = PublicNS
| otherwise = ImportedNS
-- Get the scope exported by module to be opened.
(adir, s') <- applyImportDirectiveM cm dir . inScopeBecause (Opened cm) .
noGeneralizedVarsIfLetOpen kind .
removeOnlyQualified . restrictPrivate =<< getNamedScope m
let s = setScopeAccess acc s'
let ns = scopeNameSpace acc s
modifyCurrentScope (`mergeScope` s)
-- Andreas, 2018-06-03, issue #3057:
-- If we simply check for ambiguous exported identifiers _after_
-- importing the new identifiers into the current scope, we also
-- catch the case of importing an ambiguous identifier.
checkForClashes
-- Importing names might shadow existing locals.
verboseS "scope.locals" 10 $ do
locals <- mapMaybe (\ (c,x) -> c <$ notShadowedLocal x) <$> getLocalVars
let newdefs = Map.keys $ nsNames ns
shadowed = List.intersect locals newdefs
reportSLn "scope.locals" 10 $ "opening module shadows the following locals vars: " ++ prettyShow shadowed
-- Andreas, 2014-09-03, issue 1266: shadow local variables by imported defs.
modifyLocalVars $ AssocList.mapWithKey $ \ c x ->
case Map.lookup c $ nsNames ns of
Nothing -> x
Just ys -> shadowLocal ys x
return adir
where
-- Only checks for clashes that would lead to the same
-- name being exported twice from the module.
checkForClashes = when (publicOpen dir) $ do
exported <- allThingsInScope . restrictPrivate <$> (getNamedScope =<< getCurrentModule)
-- Get all exported concrete names that are mapped to at least 2 abstract names
let defClashes = filter (\ (_c, as) -> length as >= 2) $ Map.toList $ nsNames exported
modClashes = filter (\ (_c, as) -> length as >= 2) $ Map.toList $ nsModules exported
-- No ambiguity if concrete identifier is only mapped to
-- constructor names or only to projection names.
defClash (_, qs) = not $ all (== ConName) ks || all (==FldName) ks
where ks = map anameKind qs
-- We report the first clashing exported identifier.
unlessNull (filter (\ x -> defClash x) defClashes) $
\ ((x, q:_) : _) -> typeError $ ClashingDefinition (C.QName x) $ anameName q
unlessNull modClashes $ \ ((_, ms) : _) -> do
caseMaybe (last2 ms) __IMPOSSIBLE__ $ \ (m0, m1) -> do
typeError $ ClashingModule (amodName m0) (amodName m1)