{-# LANGUAGE NondecreasingIndentation #-}
module Agda.Syntax.Scope.Monad where
import Prelude hiding (mapM, any, all, null)
import Control.Arrow ((***))
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.List.NonEmpty (NonEmpty(..), nonEmpty)
import qualified Data.List.NonEmpty as NonEmpty
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 (all)
import Data.Traversable hiding (for)
import Agda.Interaction.Options
import Agda.Interaction.Options.Warnings
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Abstract.Name as A
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract (ScopeCopyInfo(..))
import Agda.Syntax.Concrete as C
import Agda.Syntax.Concrete.Fixity
import Agda.Syntax.Concrete.Definitions (DeclarationWarning(..))
import Agda.Syntax.Scope.Base as A
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.Trace
import Agda.TypeChecking.Positivity.Occurrence (Occurrence)
import Agda.TypeChecking.Warnings ( warning )
import qualified Agda.Utils.AssocList as AssocList
import Agda.Utils.Except
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty
import Agda.Utils.Impossible
type ScopeM = TCM
printLocals :: Int -> String -> ScopeM ()
printLocals v s = verboseS "scope.top" v $ do
locals <- getLocalVars
reportSLn "scope.top" v $ s ++ " " ++ prettyShow locals
isDatatypeModule :: ReadTCState m => A.ModuleName -> m (Maybe DataOrRecord)
isDatatypeModule m = do
scopeDatatypeModule . Map.findWithDefault __IMPOSSIBLE__ m <$> useScope scopeModules
getCurrentModule :: ReadTCState m => m A.ModuleName
getCurrentModule = setRange noRange <$> useScope scopeCurrent
setCurrentModule :: MonadTCState m => A.ModuleName -> m ()
setCurrentModule m = modifyScope $ set scopeCurrent m
withCurrentModule :: (ReadTCState m, MonadTCState m) => A.ModuleName -> m a -> m 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 (scope ^. scopeModules) 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
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 }
modifyScopes $ Map.insertWith const m sm
modifyScopes :: (Map A.ModuleName Scope -> Map A.ModuleName Scope) -> ScopeM ()
modifyScopes = modifyScope . over scopeModules
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
modifyNamedScopeM :: A.ModuleName -> (Scope -> ScopeM (a, Scope)) -> ScopeM a
modifyNamedScopeM m f = do
(a, s) <- f =<< getNamedScope m
setNamedScope m s
return a
modifyCurrentScope :: (Scope -> Scope) -> ScopeM ()
modifyCurrentScope f = getCurrentModule >>= (`modifyNamedScope` f)
modifyCurrentScopeM :: (Scope -> ScopeM (a, Scope)) -> ScopeM a
modifyCurrentScopeM f = getCurrentModule >>= (`modifyNamedScopeM` f)
modifyCurrentNameSpace :: NameSpaceId -> (NameSpace -> NameSpace) -> ScopeM ()
modifyCurrentNameSpace acc f = modifyCurrentScope $ updateScopeNameSpaces $
AssocList.updateAt acc f
setContextPrecedence :: PrecedenceStack -> ScopeM ()
setContextPrecedence = modifyScope_ . set scopePrecedence
withContextPrecedence :: ReadTCState m => Precedence -> m a -> m a
withContextPrecedence p =
locallyTCState (stScope . scopePrecedence) $ pushPrecedence p
getLocalVars :: ReadTCState m => m LocalVars
getLocalVars = useScope scopeLocals
modifyLocalVars :: (LocalVars -> LocalVars) -> ScopeM ()
modifyLocalVars = modifyScope_ . updateScopeLocals
setLocalVars :: LocalVars -> ScopeM ()
setLocalVars vars = modifyLocalVars $ const vars
withLocalVars :: ScopeM a -> ScopeM a
withLocalVars = bracket_ getLocalVars setLocalVars
outsideLocalVars :: Int -> ScopeM a -> ScopeM a
outsideLocalVars n m = do
inner <- take n <$> getLocalVars
modifyLocalVars (drop n)
x <- m
modifyLocalVars (inner ++)
return x
withCheckNoShadowing :: ScopeM a -> ScopeM a
withCheckNoShadowing = bracket_ getLocalVars $ \ lvarsOld ->
checkNoShadowing lvarsOld =<< getLocalVars
checkNoShadowing :: LocalVars
-> LocalVars
-> ScopeM ()
checkNoShadowing old new = do
opts <- pragmaOptions
when (ShadowingInTelescope_ `Set.member`
(optWarningMode opts ^. warningSet)) $ do
let diff = dropEnd (length old) new
let newNames = filter (not . isNoName) $ AssocList.keys diff
let nameOccs = Map.toList $ Map.fromListWith (++) $ map pairWithRange newNames
unlessNull (filter (atLeastTwo . snd) nameOccs) $ \ conflicts -> do
warning $ NicifierIssue $ ShadowingInTelescope conflicts
where
pairWithRange :: C.Name -> (C.Name, [Range])
pairWithRange n = (n, [getRange n])
atLeastTwo :: [a] -> Bool
atLeastTwo (_ : _ : _) = True
atLeastTwo _ = False
getVarsToBind :: ScopeM LocalVars
getVarsToBind = useScope scopeVarsToBind
addVarToBind :: C.Name -> LocalVar -> ScopeM ()
addVarToBind x y = modifyScope_ $ updateVarsToBind $ AssocList.insert x y
bindVarsToBind :: ScopeM ()
bindVarsToBind = do
vars <- getVarsToBind
modifyLocalVars (vars++)
printLocals 10 "bound variables:"
modifyScope_ $ setVarsToBind []
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_ :: C.Name -> ScopeM A.Name
freshAbstractName_ = freshAbstractName noFixity'
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
freshConcreteName :: Range -> Int -> String -> ScopeM C.Name
freshConcreteName r i s = do
let cname = C.Name r C.NotInScope [Id $ stringToRawName $ s ++ show i]
rn <- resolveName $ C.QName cname
case rn of
UnknownName -> return cname
_ -> freshConcreteName r (i+1) s
resolveName :: C.QName -> ScopeM ResolvedName
resolveName = resolveName' allKindsOfNames Nothing
resolveName' ::
KindsOfNames -> Maybe (Set A.Name) -> C.QName -> ScopeM ResolvedName
resolveName' kinds names x = runExceptT (tryResolveName kinds names x) >>= \case
Left ys -> traceCall (SetRange $ getRange x) $ typeError $ AmbiguousName x ys
Right x' -> return x'
tryResolveName
:: (ReadTCState m, MonadError (NonEmpty A.QName) m)
=> KindsOfNames
-> Maybe (Set A.Name)
-> C.QName
-> m ResolvedName
tryResolveName kinds names x = do
scope <- getScope
let vars = AssocList.mapKeysMonotonic C.QName $ scope ^. scopeLocals
case lookup x vars of
Just (LocalVar y b ys) ->
ifNull (filterNames id ys)
(return $ VarName y{ nameConcrete = unqualify x } b)
$ \ ys' ->
throwError $ A.qualify_ y :| map anameName ys'
Nothing -> do
let filtKind = filter $ (`elemKindsOfNames` kinds) . anameKind . fst
caseMaybe (nonEmpty $ filtKind $ filterNames fst $ 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 -> throwError $ fmap (anameName . fst) ds
where
filterNames :: forall a. (a -> AbstractName) -> [a] -> [a]
filterNames = case names of
Nothing -> \ f -> id
Just ns -> \ f -> filter $ (`Set.member` ns) . A.qnameName . anameName . f
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 }) }
resolveModule :: C.QName -> ScopeM AbstractModule
resolveModule x = do
ms <- scopeLookup x <$> getScope
caseMaybe (nonEmpty ms) (typeError $ NoSuchModule x) $ \ case
AbsModule m why :| [] -> return $ AbsModule (m `withRangeOf` x) why
ms -> typeError $ AmbiguousModule x (fmap amodName ms)
getConcreteFixity :: C.Name -> ScopeM Fixity'
getConcreteFixity x = Map.findWithDefault noFixity' x <$> useScope scopeFixities
getConcretePolarity :: C.Name -> ScopeM (Maybe [Occurrence])
getConcretePolarity x = Map.lookup x <$> useScope scopePolarities
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
computeFixitiesAndPolarities :: DoWarn -> [C.Declaration] -> ScopeM a -> ScopeM a
computeFixitiesAndPolarities warn ds cont = do
fp <- fixitiesAndPolarities warn ds
locallyScope scopeFixitiesAndPolarities (const fp) cont
getNotation
:: C.QName
-> Set A.Name
-> 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 $ NonEmpty.toList ds of
[n] -> n
_ -> __IMPOSSIBLE__
bindVariable
:: A.BindingSource
-> C.Name
-> A.Name
-> ScopeM ()
bindVariable b x y = modifyLocalVars $ AssocList.insert x $ LocalVar y b []
unbindVariable :: C.Name -> ScopeM a -> ScopeM a
unbindVariable x = bracket_ (getLocalVars <* modifyLocalVars (AssocList.delete x)) (modifyLocalVars . const)
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)
y' <- case r of
_ | 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 $ addNameToScope ns x y'
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 (NonEmpty.head ds)
rebindName :: Access -> KindOfName -> C.Name -> A.QName -> ScopeM ()
rebindName acc kind x y = do
modifyCurrentScope $ removeNameFromScope (localNameSpace acc) x
bindName acc kind x y
bindModule :: Access -> C.Name -> A.ModuleName -> ScopeM ()
bindModule acc x m = modifyCurrentScope $
addModuleToScope (localNameSpace acc) x (AbsModule m Defined)
bindQModule :: Access -> C.QName -> A.ModuleName -> ScopeM ()
bindQModule acc q m = modifyCurrentScope $ \s ->
s { scopeImports = Map.insert q m (scopeImports s) }
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))]
}
memoToScopeInfo :: ScopeMemo -> ScopeCopyInfo
memoToScopeInfo (ScopeMemo names mods) =
ScopeCopyInfo { renNames = names
, renModules = [ (x, y) | (x, (y, _)) <- mods ] }
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
s' <- recomputeInScopeSets <$> mapScopeM_ copyD copyM return (setNameSpace PrivateNS emptyNameSpace s)
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
_ -> lensAnameName f d
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) }
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 }
renName :: A.QName -> WSM A.QName
renName x = do
m <- case x `isInModule` old of
True -> return new'
False -> renMod' False (qnameModule x)
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
renMod :: A.ModuleName -> WSM A.ModuleName
renMod = renMod' True
renMod' rec x = do
z <- findMod x
case z of
Just (y, False) | rec -> y <$ copyRec x y
Just (y, _) -> return y
Nothing -> do
let newM = if x `isLtChildModuleOf` old then newL else mnameToList new0
y <- do
y <- refresh (last $ A.mnameToList x)
return $ A.mnameFromList $ newM ++ [y]
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
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)
checkNoFixityInRenamingModule :: [C.Renaming] -> ScopeM ()
checkNoFixityInRenamingModule ren = do
whenJust (nonEmpty $ mapMaybe rangeOfUselessInfix ren) $ \ rs -> do
traceCall (SetRange $ getRange rs) $ do
warning $ FixityInRenamingModule rs
where
rangeOfUselessInfix :: C.Renaming -> Maybe Range
rangeOfUselessInfix = \case
Renaming ImportedModule{} _ mfx _ -> getRange <$> mfx
_ -> Nothing
applyImportDirectiveM
:: C.QName
-> C.ImportDirective
-> Scope
-> ScopeM (A.ImportDirective, Scope)
applyImportDirectiveM m (ImportDirective rng usn' hdn' ren' public) scope = do
checkNoFixityInRenamingModule ren'
let usingList = fromUsing usn'
let (missingExports, namesA) = checkExist $ usingList ++ hdn' ++ map renFrom ren'
unless (null missingExports) $ setCurrentRange rng $ do
reportSLn "scope.import.apply" 20 $ "non existing names: " ++ prettyShow missingExports
warning $ ModuleDoesntExport m missingExports
let notMissing = not . (missingExports `hasElem`)
let usn = filter notMissing usingList
let hdn = filter notMissing hdn'
let ren = filter (notMissing . renFrom) ren'
let dir = ImportDirective rng (mapUsing (const usn) usn') hdn ren public
let names = map renFrom ren ++ hdn ++ usn
let definedNames = map renTo ren
let targetNames = usn ++ definedNames
let inNames = (names `hasElem`)
let extra x = and
[ inNames $ ImportedName x
, notMissing $ ImportedModule x
, not . inNames $ ImportedModule x
]
dir' <- sanityCheck (not . inNames) $ addExtraModules extra dir
unlessNull (allDuplicates targetNames) $ \ dup ->
typeError $ DuplicateImports m dup
let (scope', (nameClashes, moduleClashes)) = applyImportDirective_ dir' scope
unless (null nameClashes) $
warning $ ClashesViaRenaming NameNotModule $ Set.toList nameClashes
unless (null moduleClashes) $
warning $ ClashesViaRenaming ModuleNotName $ Set.toList moduleClashes
let namesInScope' = (allNamesInScope scope' :: ThingsInScope AbstractName)
let modulesInScope' = (allNamesInScope scope' :: ThingsInScope AbstractModule)
let look x = headWithDefault __IMPOSSIBLE__ . Map.findWithDefault __IMPOSSIBLE__ x
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')
where
fromUsing :: Using' a b -> [ImportedName' a b]
fromUsing = \case
Using xs -> xs
UseEverything -> []
sanityCheck notMentioned = \case
dir@(ImportDirective{ using = Using{}, hiding = ys }) -> do
let useless = \case
ImportedName{} -> True
ImportedModule y -> notMentioned (ImportedName y)
unlessNull (filter useless ys) $ \ uselessHiding -> do
typeError $ GenericError $ unwords $
[ "Hiding"
, List.intercalate ", " $ map prettyShow uselessHiding
, "has no effect"
]
return dir{ hiding = [] }
dir -> return dir
addExtraModules :: (C.Name -> Bool) -> C.ImportDirective -> C.ImportDirective
addExtraModules extra dir =
dir{ using = mapUsing (concatMap addExtra) $ using dir
, hiding = concatMap addExtra $ hiding dir
, impRenaming = concatMap extraRenaming $ impRenaming dir
}
where
addExtra f@(ImportedName y) | extra y = [f, ImportedModule y]
addExtra m = [m]
extraRenaming = \case
r@(Renaming (ImportedName y) (ImportedName z) _fixity rng) | extra y ->
[ r , Renaming (ImportedModule y) (ImportedModule z) Nothing rng ]
r -> [r]
namesInScope = (allNamesInScope scope :: ThingsInScope AbstractName)
modulesInScope = (allNamesInScope scope :: ThingsInScope AbstractModule)
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
mapImportDir
:: (Ord n1, Ord m1)
=> [ImportedName' (n1,n2) (m1,m2)]
-> [ImportedName' (n1,n2) (m1,m2)]
-> ImportDirective' n1 m1
-> ImportDirective' n2 m2
mapImportDir src0 tgt0 (ImportDirective r u h ren open) =
ImportDirective r
(mapUsing (map (lookupImportedName src)) u)
(map (lookupImportedName src) h)
(map (mapRenaming src tgt) ren)
open
where
src = importedNameMapFromList src0
tgt = importedNameMapFromList tgt0
data ImportedNameMap n1 n2 m1 m2 = ImportedNameMap
{ inameMap :: Map n1 n2
, imoduleMap :: Map m1 m2
}
importedNameMapFromList
:: (Ord n1, Ord m1)
=> [ImportedName' (n1,n2) (m1,m2)]
-> ImportedNameMap n1 n2 m1 m2
importedNameMapFromList = foldr (flip add) $ ImportedNameMap Map.empty Map.empty
where
add (ImportedNameMap nm mm) = \case
ImportedName (x,y) -> ImportedNameMap (Map.insert x y nm) mm
ImportedModule (x,y) -> ImportedNameMap nm (Map.insert x y mm)
lookupImportedName
:: (Ord n1, Ord m1)
=> ImportedNameMap n1 n2 m1 m2
-> ImportedName' n1 m1
-> ImportedName' n2 m2
lookupImportedName (ImportedNameMap nm mm) = \case
ImportedName x -> ImportedName $ Map.findWithDefault __IMPOSSIBLE__ x nm
ImportedModule x -> ImportedModule $ Map.findWithDefault __IMPOSSIBLE__ x mm
mapRenaming
:: (Ord n1, Ord m1)
=> ImportedNameMap n1 n2 m1 m2
-> ImportedNameMap n1 n2 m1 m2
-> Renaming' n1 m1
-> Renaming' n2 m2
mapRenaming src tgt (Renaming from to fixity r) =
Renaming (lookupImportedName src from) (lookupImportedName tgt to) fixity r
data OpenKind = LetOpenModule | TopOpenModule
noGeneralizedVarsIfLetOpen :: OpenKind -> Scope -> Scope
noGeneralizedVarsIfLetOpen TopOpenModule = id
noGeneralizedVarsIfLetOpen LetOpenModule = disallowGeneralizedVars
openModule_ :: OpenKind -> C.QName -> C.ImportDirective -> ScopeM A.ImportDirective
openModule_ kind cm dir = openModule kind Nothing cm dir
openModule :: OpenKind -> Maybe A.ModuleName -> C.QName -> C.ImportDirective -> ScopeM A.ImportDirective
openModule kind mam cm dir = do
current <- getCurrentModule
m <- caseMaybe mam (amodName <$> resolveModule cm) return
let acc | Nothing <- publicOpen dir = PrivateNS
| m `isLtChildModuleOf` current = PublicNS
| otherwise = ImportedNS
(adir, s') <- applyImportDirectiveM cm dir . inScopeBecause (Opened cm) .
noGeneralizedVarsIfLetOpen kind .
restrictPrivate =<< getNamedScope m
let s = setScopeAccess acc s'
let ns = scopeNameSpace acc s
modifyCurrentScope (`mergeScope` s)
checkForClashes
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
modifyLocalVars $ AssocList.mapWithKey $ \ c x ->
case Map.lookup c $ nsNames ns of
Nothing -> x
Just ys -> shadowLocal ys x
return adir
where
checkForClashes = when (isJust $ publicOpen dir) $ do
exported <- allThingsInScope . restrictPrivate <$> (getNamedScope =<< getCurrentModule)
let defClashes = filter (\ (_c, as) -> length as >= 2) $ Map.toList $ nsNames exported
modClashes = filter (\ (_c, as) -> length as >= 2) $ Map.toList $ nsModules exported
defClash (_, qs) = not $ all (== ConName) ks || all (==FldName) ks
where ks = map anameKind qs
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)