module Agda.Syntax.Scope.Monad where
import Prelude hiding (mapM)
import Control.Applicative
import Control.Monad hiding (mapM)
import Control.Monad.Writer hiding (mapM)
import Data.Map (Map)
import Data.Traversable
import Data.List
import qualified Data.Map as Map
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Fixity
import Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Concrete as C
import Agda.Syntax.Scope.Base
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.Options
import Agda.Utils.Tuple
import Agda.Utils.Fresh
import Agda.Utils.Size
import Agda.Utils.List
#include "../../undefined.h"
import Agda.Utils.Impossible
type ScopeM = TCM
notInScope :: C.QName -> ScopeM a
notInScope x = typeError $ NotInScope [x]
getCurrentModule :: ScopeM A.ModuleName
getCurrentModule = setRange noRange . scopeCurrent <$> getScope
setCurrentModule :: A.ModuleName -> ScopeM ()
setCurrentModule m = modifyScopeInfo $ \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
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" ++ show scope ++ "\nNO SUCH SCOPE " ++ show m
__IMPOSSIBLE__
getCurrentScope :: ScopeM Scope
getCurrentScope = getNamedScope =<< getCurrentModule
createModule :: A.ModuleName -> ScopeM ()
createModule m = do
s <- getCurrentScope
let parents = scopeName s : scopeParents s
modifyScopes $ Map.insert m emptyScope { scopeName = m, scopeParents = parents }
modifyScopeInfo :: (ScopeInfo -> ScopeInfo) -> ScopeM ()
modifyScopeInfo f = do
scope <- getScope
setScope $ f scope
modifyScopes :: (Map A.ModuleName Scope -> Map A.ModuleName Scope) -> ScopeM ()
modifyScopes f = modifyScopeInfo $ \s -> s { scopeModules = f $ scopeModules s }
modifyNamedScope :: A.ModuleName -> (Scope -> Scope) -> ScopeM ()
modifyNamedScope m f = modifyScopes $ Map.mapWithKey f'
where
f' m' s | m' == m = f s
| otherwise = s
modifyCurrentScope :: (Scope -> Scope) -> ScopeM ()
modifyCurrentScope f = do
m <- getCurrentModule
modifyNamedScope m f
modifyNamedScopeM :: A.ModuleName -> (Scope -> ScopeM Scope) -> ScopeM ()
modifyNamedScopeM m f = do
s <- getNamedScope m
s' <- f s
modifyNamedScope m (const s')
modifyCurrentScopeM :: (Scope -> ScopeM Scope) -> ScopeM ()
modifyCurrentScopeM f = do
m <- getCurrentModule
modifyNamedScopeM m f
modifyCurrentNameSpace :: NameSpaceId -> (NameSpace -> NameSpace) -> ScopeM ()
modifyCurrentNameSpace acc f = modifyCurrentScope action
where
action s = s { scopePublic = pub $ scopePublic s
, scopePrivate = pri $ scopePrivate s
, scopeImported = imp $ scopeImported s
}
(pub, pri, imp) = case acc of
PublicNS -> (f, id, id)
PrivateNS -> (id, f, id)
ImportedNS -> (id, id, f)
setContextPrecedence :: Precedence -> ScopeM ()
setContextPrecedence p = modifyScopeInfo $ \s -> s { scopePrecedence = p }
getContextPrecedence :: ScopeM Precedence
getContextPrecedence = scopePrecedence <$> getScope
withContextPrecedence :: Precedence -> ScopeM a -> ScopeM a
withContextPrecedence p m = do
p' <- getContextPrecedence
setContextPrecedence p
x <- m
setContextPrecedence p'
return x
getLocalVars :: ScopeM LocalVars
getLocalVars = scopeLocals <$> getScope
setLocalVars :: LocalVars -> ScopeM ()
setLocalVars vars = modifyScope $ \s -> s { scopeLocals = vars }
withLocalVars :: ScopeM a -> ScopeM a
withLocalVars m = do
vars <- getLocalVars
x <- m
setLocalVars vars
return x
freshAbstractName :: Fixity -> C.Name -> ScopeM A.Name
freshAbstractName fx x = do
i <- fresh
return $ A.Name i x (getRange x) fx
freshAbstractName_ :: C.Name -> ScopeM A.Name
freshAbstractName_ = freshAbstractName defaultFixity
freshAbstractQName :: Fixity -> C.Name -> ScopeM A.QName
freshAbstractQName fx x = do
y <- freshAbstractName fx x
m <- getCurrentModule
return $ A.qualify m y
data ResolvedName = VarName A.Name
| DefinedName AbstractName
| ConstructorName [AbstractName]
| UnknownName
deriving (Show)
resolveName :: C.QName -> ScopeM ResolvedName
resolveName x = do
scope <- getScope
let vars = map (C.QName -*- id) $ scopeLocals scope
case lookup x vars of
Just y -> return $ VarName $ y { nameConcrete = unqualify x }
Nothing -> case scopeLookup x scope of
[] -> return UnknownName
ds | all ((==ConName) . anameKind) ds ->
return $ ConstructorName
$ map (\d -> updateConcreteName d $ unqualify x) ds
[d] -> return $ DefinedName $ updateConcreteName d (unqualify x)
ds -> typeError $ AmbiguousName x (map anameName ds)
where
updateConcreteName :: AbstractName -> C.Name -> AbstractName
updateConcreteName d@(AbsName { anameName = an@(A.QName { qnameName = qn }) }) x =
d { anameName = an { qnameName = qn { nameConcrete = x } } }
resolveModule :: C.QName -> ScopeM AbstractModule
resolveModule x = do
ms <- scopeLookup x <$> getScope
case ms of
[AbsModule m] -> return $ AbsModule (m `withRangesOfQ` x)
[] -> typeError $ NoSuchModule x
ms -> typeError $ AmbiguousModule x (map amodName ms)
getFixity :: C.QName -> ScopeM Fixity
getFixity x = do
r <- resolveName x
case r of
VarName y -> return $ nameFixity y
DefinedName d -> return $ nameFixity $ qnameName $ anameName d
ConstructorName ds
| null fs -> __IMPOSSIBLE__
| allEqual fs -> return $ head fs
| otherwise -> return defaultFixity
where
fs = map (nameFixity . qnameName . anameName) ds
UnknownName -> __IMPOSSIBLE__
bindVariable :: C.Name -> A.Name -> ScopeM ()
bindVariable x y = do
scope <- getScope
setScope scope { scopeLocals = (x, y) : scopeLocals scope }
bindName :: Access -> KindOfName -> C.Name -> A.QName -> ScopeM ()
bindName acc kind x y = do
r <- resolveName (C.QName x)
ys <- case r of
DefinedName d -> typeError $ ClashingDefinition (C.QName x) $ anameName d
VarName z -> typeError $ ClashingDefinition (C.QName x) $ A.qualify (mnameFromList []) z
ConstructorName [] -> __IMPOSSIBLE__
ConstructorName ds
| kind == ConName && all ((==ConName) . anameKind) ds -> return [ AbsName y kind ]
| otherwise -> typeError $ ClashingDefinition (C.QName x) $ anameName (head ds)
UnknownName -> return [AbsName y kind]
modifyCurrentScope $ addNamesToScope (localNameSpace acc) x ys
bindModule :: Access -> C.Name -> A.ModuleName -> ScopeM ()
bindModule acc x m = modifyCurrentScope $
addModuleToScope (localNameSpace acc) x (AbsModule m)
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 strip
where
strip = mapScope (\_ -> stripN) (\_ -> stripN)
stripN m = Map.filterWithKey (const . notNoName) m
notNoName = not . isNoName
renamedCanonicalNames :: ModuleName -> ModuleName -> Scope ->
ScopeM (Map A.QName A.QName, Map A.ModuleName A.ModuleName)
renamedCanonicalNames old new s = (,) <$> renamedNames names <*> renamedMods mods
where
ns = allThingsInScope s
names = nsNames ns
mods = nsModules ns
renamedNames ds = Map.fromList <$> zip xs <$> mapM renName xs
where
xs = filter (`isInModule` old) $ map anameName $ concat $ Map.elems ds
renamedMods ms = Map.fromList <$> zip xs <$> mapM renMod xs
where
xs = filter (`isSubModuleOf` old) $ map amodName $ concat $ Map.elems ms
renName :: A.QName -> ScopeM A.QName
renName y = do
i <- fresh
return . qualifyQ new . dequalify
$ y { qnameName = (qnameName y) { nameId = i } }
where
dequalify = A.qnameFromList . drop (size old) . A.qnameToList
renMod :: A.ModuleName -> ScopeM A.ModuleName
renMod = return . qualifyM new . dequalify
where
dequalify = A.mnameFromList . drop (size old) . A.mnameToList
type Ren a = Map a a
type Out = [Either (Ren A.ModuleName) (Ren A.QName)]
type WSM = WriterT Out ScopeM
copyScope :: A.ModuleName -> Scope -> ScopeM (Scope, Ren A.ModuleName, Ren A.QName)
copyScope new s = do
s0 <- getNamedScope new
(s', rho) <- runWriterT $ mapScopeM copyD copyM s
let s'' = s' { scopeName = scopeName s0
, scopeParents = scopeParents s0
}
return (s'', modRenaming rho, defRenaming rho)
where
new' = killRange new
old = scopeName s
modRenaming rho = Map.unions [ m | Left m <- rho ]
defRenaming rho = Map.unions [ m | Right m <- rho ]
copyM :: NameSpaceId -> ModulesInScope -> WSM ModulesInScope
copyM ImportedNS ms = return ms
copyM PrivateNS _ = return Map.empty
copyM PublicNS ms = traverse (mapM $ onMod renMod) ms
copyD :: NameSpaceId -> NamesInScope -> WSM NamesInScope
copyD ImportedNS ds = return ds
copyD PrivateNS _ = return Map.empty
copyD PublicNS ds = traverse (mapM $ onName renName) ds
onMod f m = do
x <- f $ amodName m
return m { amodName = x }
onName f d = do
x <- f $ anameName d
return d { anameName = x }
renName :: A.QName -> WSM A.QName
renName x = do
i <- lift fresh
let y = qualifyQ new' . dequalify
$ x { qnameName = (qnameName x) { nameId = i } }
tell [Right $ Map.singleton x y]
return y
where
dequalify = A.qnameFromList . drop (size old) . A.qnameToList
renMod :: A.ModuleName -> WSM A.ModuleName
renMod x = do
let y = qualifyM new' $ dequalify x
tell [Left $ Map.singleton x y]
(s, renM, renD) <- lift $ do
createModule y
s0 <- getNamedScope x
withCurrentModule y $ copyScope y s0
lift $ modifyNamedScope y (const s)
tell [Left renM, Right renD]
return y
where
dequalify = A.mnameFromList . drop (size old) . A.mnameToList
applyImportDirectiveM :: C.QName -> ImportDirective -> Scope -> ScopeM Scope
applyImportDirectiveM m dir scope = do
xs <- filterM doesntExist names
reportSLn "scope.import.apply" 20 $ "non existing names: " ++ show xs
case xs of
[] -> return $ applyImportDirective dir scope
_ -> typeError $ ModuleDoesntExport m xs
where
names :: [ImportedName]
names = map renFrom (renaming dir) ++ case usingOrHiding dir of
Using xs -> xs
Hiding xs -> xs
doesntExist (ImportedName x) =
case Map.lookup x (allNamesInScope scope :: ThingsInScope AbstractName) of
Just _ -> return False
Nothing -> return True
doesntExist (ImportedModule x) =
case Map.lookup x (allNamesInScope scope :: ThingsInScope AbstractModule) of
Just _ -> return False
Nothing -> return True
openModule_ :: C.QName -> ImportDirective -> ScopeM ()
openModule_ cm dir = do
current <- getCurrentModule
m <- amodName <$> resolveModule cm
let ns = namespace current m
s <- setScopeAccess ns <$>
(applyImportDirectiveM cm dir . restrictPrivate =<< getNamedScope m)
checkForClashes (scopeNameSpace ns s)
modifyCurrentScope (`mergeScope` s)
where
namespace m0 m1
| not (publicOpen dir) = PrivateNS
| m1 `isSubModuleOf` m0 = PublicNS
| otherwise = ImportedNS
checkForClashes new
| not (publicOpen dir) = return ()
| otherwise = do
old <- allThingsInScope . restrictPrivate <$> (getNamedScope =<< getCurrentModule)
let defClashes = Map.toList $ Map.intersectionWith (,) (nsNames new) (nsNames old)
modClashes = Map.toList $ Map.intersectionWith (,) (nsModules new) (nsModules old)
realClash (_, ([x],[y])) = x /= y
realClash _ = True
defClash (_, (qs0, qs1)) =
any ((/= ConName) . anameKind) (qs0 ++ qs1)
(f & g) x = f x && g x
case filter (realClash & defClash) defClashes of
(x, (_, q:_)):_ -> typeError $ ClashingDefinition (C.QName x) (anameName q)
_ -> return ()
case filter realClash modClashes of
(_, (m0:_, m1:_)):_ -> typeError $ ClashingModule (amodName m0) (amodName m1)
_ -> return ()