#if __GLASGOW_HASKELL__ >= 710
#endif
module Agda.Syntax.Scope.Monad where
import Prelude hiding (mapM)
import Control.Arrow ((***), first, second)
import Control.Applicative
import Control.Monad hiding (mapM)
import Control.Monad.Writer hiding (mapM)
import Control.Monad.State hiding (mapM)
import 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.Traversable
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.Concrete as C
import Agda.Syntax.Scope.Base
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.Options
import qualified Agda.Utils.AssocList as AssocList
import Agda.Utils.Function
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Null (unlessNull)
import Agda.Utils.Size
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
type ScopeM = TCM
isDatatypeModule :: A.ModuleName -> ScopeM Bool
isDatatypeModule m = do
sc <- getScope
return $ maybe __IMPOSSIBLE__ scopeDatatypeModule (Map.lookup m (scopeModules sc))
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 :: Bool -> A.ModuleName -> ScopeM ()
createModule b m = do
s <- getCurrentScope
let parents = scopeName s : scopeParents s
modifyScopes $ Map.insert m emptyScope { scopeName = m
, scopeParents = parents
, scopeDatatypeModule = b }
modifyScopeInfo :: (ScopeInfo -> ScopeInfo) -> ScopeM ()
modifyScopeInfo = modifyScope
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.adjust f m
setNamedScope :: A.ModuleName -> Scope -> ScopeM ()
setNamedScope m s = modifyNamedScope m $ const s
modifyNamedScopeM :: A.ModuleName -> (Scope -> ScopeM Scope) -> ScopeM ()
modifyNamedScopeM m f = setNamedScope m =<< f =<< getNamedScope m
modifyCurrentScope :: (Scope -> Scope) -> ScopeM ()
modifyCurrentScope f = getCurrentModule >>= (`modifyNamedScope` f)
modifyCurrentScopeM :: (Scope -> ScopeM Scope) -> ScopeM ()
modifyCurrentScopeM f = getCurrentModule >>= (`modifyNamedScopeM` f)
modifyCurrentNameSpace :: NameSpaceId -> (NameSpace -> NameSpace) -> ScopeM ()
modifyCurrentNameSpace acc f = modifyCurrentScope $ updateScopeNameSpaces $
AssocList.updateAt acc 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
modifyLocalVars :: (LocalVars -> LocalVars) -> ScopeM ()
modifyLocalVars = modifyScope . updateScopeLocals
setLocalVars :: LocalVars -> ScopeM ()
setLocalVars vars = modifyLocalVars $ const 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
{ nameId = i
, nameConcrete = x
, nameBindingSite = getRange x
, nameFixity = 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
| FieldName AbstractName
| ConstructorName [AbstractName]
| PatternSynResName AbstractName
| UnknownName
deriving (Show, Eq)
resolveName :: C.QName -> ScopeM ResolvedName
resolveName = resolveName' allKindsOfNames Nothing
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
Just (LocalVar y) -> retVar y
Just (ShadowedVar y ys) -> case names of
Nothing -> shadowed ys
Just ns -> case filter (\y -> aName y `Set.member` ns) ys of
[] -> retVar y
ys -> shadowed ys
where
shadowed ys =
typeError $ AmbiguousName x $ A.qualify_ y : map anameName ys
Nothing -> case filter (\y -> anameKind (fst y) `elem` kinds
&&
maybe True (Set.member (aName (fst y)))
names)
(scopeLookup' x scope) of
[] -> return UnknownName
ds | all ((==ConName) . anameKind . fst) ds ->
return $ ConstructorName
$ map (\ (d, _) -> updateConcreteName d $ unqualify x) ds
[(d, a)] | anameKind d == FldName -> return $ FieldName $ updateConcreteName d (unqualify x)
[(d, a)] | anameKind d == PatternSynName ->
return $ PatternSynResName (updateConcreteName d $ unqualify x)
[(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 why] -> return $ AbsModule (m `withRangesOfQ` x) why
[] -> typeError $ NoSuchModule x
ms -> typeError $ AmbiguousModule x (map amodName ms)
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 d -> return $ notation d
ConstructorName ds -> case mergeNotations $ map notation ds of
[n] -> return n
_ -> __IMPOSSIBLE__
PatternSynResName n -> return $ notation n
UnknownName -> __IMPOSSIBLE__
where
notation = namesToNotation x . qnameName . anameName
bindVariable :: C.Name -> A.Name -> ScopeM ()
bindVariable x y = modifyScope $ updateScopeLocals $ AssocList.insert x $ LocalVar y
bindName :: Access -> KindOfName -> C.Name -> A.QName -> ScopeM ()
bindName acc kind x y = do
r <- resolveName (C.QName x)
ys <- case r of
FieldName d -> typeError $ ClashingDefinition (C.QName x) $ anameName d
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 Defined ]
| otherwise -> typeError $ ClashingDefinition (C.QName x) $ anameName (headWithDefault __IMPOSSIBLE__ ds)
PatternSynResName n -> typeError $ ClashingDefinition (C.QName x) $ anameName n
UnknownName -> return [AbsName y kind Defined]
modifyCurrentScope $ addNamesToScope (localNameSpace acc) x ys
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
where
stripN = Map.filterWithKey $ const . not . isNoName
type Out = (A.Ren A.ModuleName, A.Ren A.QName)
type WSM = StateT Out ScopeM
copyScope :: C.QName -> A.ModuleName -> Scope -> ScopeM (Scope, (A.Ren A.ModuleName, A.Ren A.QName))
copyScope oldc new s = first (inScopeBecause $ Applied oldc) <$> runStateT (copy new s) ([], [])
where
copy :: A.ModuleName -> Scope -> StateT (A.Ren A.ModuleName, A.Ren A.QName) ScopeM Scope
copy new s = do
lift $ reportSLn "scope.copy" 20 $ "Copying scope " ++ show old ++ " to " ++ show new
lift $ reportSLn "scope.copy" 50 $ show s
s0 <- lift $ getNamedScope new
s' <- mapScopeM_ copyD copyM $ setNameSpace PrivateNS emptyNameSpace s
return $ s' { scopeName = scopeName s0
, scopeParents = scopeParents s0
}
where
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 $ second $ ((x, y):)
addMod x y = modify $ first $ ((x, y):)
findName x = lookup x <$> gets snd
findMod x = lookup x <$> gets fst
renName :: A.QName -> WSM A.QName
renName x = do
y <- ifJustM (findMod $ qnameToMName x) (return . mnameToQName) $ do
i <- lift fresh
return $ A.qualify new' $ (qnameName x) { nameId = i }
lift $ reportSLn "scope.copy" 50 $ " Copying " ++ show x ++ " to " ++ show y
addName x y
return y
renMod :: A.ModuleName -> WSM A.ModuleName
renMod x = do
y <- ifJustM (findName $ mnameToQName x) (return . qnameToMName) $ do
return $ A.mnameFromList $ (newL ++) $ drop (size old) $ A.mnameToList x
addMod x y
s0 <- lift $ createModule False y >> getNamedScope x
s <- withCurrentModule' y $ copy y s0
lift $ modifyNamedScope y (const s)
return y
applyImportDirectiveM :: C.QName -> ImportDirective -> Scope -> ScopeM Scope
applyImportDirectiveM m dir scope = do
let xs = filter doesntExist names
reportSLn "scope.import.apply" 20 $ "non existing names: " ++ show xs
unless (null xs) $ typeError $ ModuleDoesntExport m xs
let dup = targetNames \\ nub targetNames
unless (null dup) $ typeError $ DuplicateImports m dup
return $ applyImportDirective dir scope
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) = isNothing $
Map.lookup x (allNamesInScope scope :: ThingsInScope AbstractName)
doesntExist (ImportedModule x) = isNothing $
Map.lookup x (allNamesInScope scope :: ThingsInScope AbstractModule)
openModule_ :: C.QName -> ImportDirective -> ScopeM ()
openModule_ cm dir = do
current <- getCurrentModule
m <- amodName <$> resolveModule cm
let acc = namespace current m
s <- setScopeAccess acc <$>
(applyImportDirectiveM cm dir . inScopeBecause (Opened cm) . removeOnlyQualified . restrictPrivate =<< getNamedScope m)
let ns = scopeNameSpace acc s
checkForClashes ns
modifyCurrentScope (`mergeScope` s)
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: " ++ show shadowed
modifyLocalVars $ AssocList.mapWithKey $ \ c x ->
case Map.lookup c $ nsNames ns of
Nothing -> x
Just ys -> shadowLocal ys x
where
namespace m0 m1
| not (publicOpen dir) = PrivateNS
| m1 `isSubModuleOf` m0 = PublicNS
| otherwise = ImportedNS
checkForClashes new = when (publicOpen dir) $ 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)
unlessNull (filter (\ x -> realClash x && defClash x) defClashes) $
\ ((x, (_, q:_)) : _) -> typeError $ ClashingDefinition (C.QName x) (anameName q)
unlessNull (filter realClash modClashes) $ \ ((_, (m0:_, m1:_)) : _) ->
typeError $ ClashingModule (amodName m0) (amodName m1)