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 Control.Monad.State 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.Notation
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
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" ++ 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 { scopeNameSpaces = [ (nsid, f' nsid ns) | (nsid, ns) <- scopeNameSpaces s ] }
f' a | a == acc = f
| otherwise = id
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 Access 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 . fst) ds ->
return $ ConstructorName
$ map (\ (d, _) -> updateConcreteName d $ unqualify x) ds
[(d, a)] -> return $ DefinedName a $ updateConcreteName d (unqualify x)
ds -> typeError $ AmbiguousName x (map (anameName . fst) 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
where
head' [] = __IMPOSSIBLE__
head' (x:_) = x
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
type Ren a = Map a a
type Out = (Ren A.ModuleName, Ren A.QName)
type WSM = StateT Out ScopeM
copyScope :: A.ModuleName -> Scope -> ScopeM (Scope, (Ren A.ModuleName, Ren A.QName))
copyScope new s = runStateT (copy new s) (Map.empty, Map.empty)
where
copy new s = do
s0 <- lift $ getNamedScope new
s' <- mapScopeM copyD copyM s
return $ s' { scopeName = scopeName s0
, scopeParents = scopeParents s0
}
new' = killRange new
old = scopeName s
copyM :: NameSpaceId -> ModulesInScope -> WSM ModulesInScope
copyM ImportedNS ms = return ms
copyM PrivateNS _ = return Map.empty
copyM PublicNS ms = traverse (mapM $ onMod renMod) ms
copyM OnlyQualifiedNS 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
copyD OnlyQualifiedNS 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 }
addName x y = addNames (Map.singleton x y)
addMod x y = addMods (Map.singleton x y)
addNames rd' = modify $ \(rm, rd) -> (rm, Map.union rd rd')
addMods rm' = modify $ \(rm, rd) -> (Map.union rm rm', rd)
findName x = Map.lookup x <$> gets snd
findMod x = Map.lookup x <$> gets fst
renName :: A.QName -> WSM A.QName
renName x = do
my <- findName x
case my of
Just y -> return y
Nothing -> do
i <- lift fresh
let y = qualifyQ new' . dequalify
$ x { qnameName = (qnameName x) { nameId = i } }
addName x y
return y
where
dequalify = A.qnameFromList . drop (size old) . A.qnameToList
renMod :: A.ModuleName -> WSM A.ModuleName
renMod x = do
my <- findMod x
case my of
Just y -> return y
Nothing -> do
let y = qualifyM new' $ dequalify x
addMod x y
s0 <- lift $ createModule y >> getNamedScope x
s <- withCurrentModule' y $ copy y s0
lift $ modifyNamedScope y (const s)
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
[] -> case targetNames \\ nub targetNames of
[] -> return $ applyImportDirective dir scope
dup -> typeError $ DuplicateImports m dup
_ -> typeError $ ModuleDoesntExport m xs
where
names :: [ImportedName]
names = map renFrom (renaming dir) ++ case usingOrHiding dir of
Using xs -> xs
Hiding xs -> xs
targetNames :: [ImportedName]
targetNames = map renName (renaming dir) ++ case usingOrHiding dir of
Using xs -> xs
Hiding{} -> []
where
renName r = (renFrom r) { importedName = renTo r }
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 . removeOnlyQualified . 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 ()