{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
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 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.Scope.Base
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.Options
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
type ScopeM = TCM
isDatatypeModule :: A.ModuleName -> ScopeM (Maybe DataOrRecord)
isDatatypeModule m = do
scopeDatatypeModule . Map.findWithDefault __IMPOSSIBLE__ m . scopeModules <$> getScope
printLocals :: Int -> String -> ScopeM ()
printLocals v s = verboseS "scope.top" v $ do
locals <- getLocalVars
reportSLn "scope.top" v $ s ++ " " ++ prettyShow locals
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
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 f = modifyScope $ \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 (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
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
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
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
}
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
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 b []) -> retVar y b
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
Nothing -> do
let filtKind = filter $ \ y -> anameKind (fst y) `elem` kinds
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 }) }
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)
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 $ toList ds of
[n] -> n
_ -> __IMPOSSIBLE__
bindVariable
:: Binder
-> 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 = do
r <- resolveName (C.QName x)
ys <- case r of
UnknownName | isNoName x -> success
DefinedName{} | isNoName x -> success <* modifyCurrentScope (removeNameFromScope PrivateNS x)
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 ]
clash = typeError . ClashingDefinition (C.QName x)
ambiguous k ds =
if kind == k && all ((== k) . anameKind) ds
then success else clash $ anameName (headNe 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 { 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 | x `isSubModuleOf` old = newL
| otherwise = 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)
applyImportDirectiveM :: C.QName -> C.ImportDirective -> Scope -> ScopeM (A.ImportDirective, Scope)
applyImportDirectiveM m dir@ImportDirective{ impRenaming = ren, using = u, hiding = h } scope = do
caseMaybe mNamesA doesntExport $ \ namesA -> do
let extraModules =
[ x | ImportedName x <- names,
let mx = ImportedModule x,
not $ doesntExist mx,
notElem mx names ]
dir' = addExtraModules extraModules dir
dir' <- sanityCheck dir'
let dup = targetNames List.\\ List.nub targetNames
unless (null dup) $ typeError $ DuplicateImports m dup
let scope' = applyImportDirective dir' scope
let namesInScope' = (allNamesInScope scope' :: ThingsInScope AbstractName)
let modulesInScope' = (allNamesInScope scope' :: ThingsInScope AbstractModule)
let look x = head . 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
usingNames :: [ImportedName]
usingNames = case u of
Using xs -> xs
UseEverything -> []
names :: [ImportedName]
names = map renFrom ren ++ h ++ usingNames
definedNames :: [ImportedName]
definedNames = map renTo ren
targetNames :: [ImportedName]
targetNames = definedNames ++ usingNames
sanityCheck dir =
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]
namesInScope = (allNamesInScope scope :: ThingsInScope AbstractName)
modulesInScope = (allNamesInScope scope :: ThingsInScope AbstractModule)
mNamesA = forM names $ \case
ImportedName x -> ImportedName . (x,) . setRange (getRange x) . anameName . head <$> Map.lookup x namesInScope
ImportedModule x -> ImportedModule . (x,) . setRange (getRange x) . amodName . head <$> Map.lookup x modulesInScope
head = headWithDefault __IMPOSSIBLE__
doesntExport = do
let xs = filter doesntExist names
reportSLn "scope.import.apply" 20 $ "non existing names: " ++ prettyShow xs
typeError $ ModuleDoesntExport m xs
doesntExist (ImportedName x) = isNothing $ Map.lookup x namesInScope
doesntExist (ImportedModule x) = isNothing $ Map.lookup x modulesInScope
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
mapImportDir
:: (Eq a, Eq b)
=> [ImportedName' (a,c) (b,d)]
-> [ImportedName' (a,c) (b,d)]
-> ImportDirective' a b
-> ImportDirective' c d
mapImportDir src tgt (ImportDirective r u h ren open) =
ImportDirective r
(mapUsing src u)
(map (`lookupImportedName` src) h)
(map (mapRenaming src tgt) ren) open
mapUsing
:: (Eq a, Eq b)
=> [ImportedName' (a,c) (b,d)]
-> Using' a b
-> Using' c d
mapUsing src UseEverything = UseEverything
mapUsing src (Using xs) = Using $ map (`lookupImportedName` src) xs
mapRenaming
:: (Eq a, Eq b)
=> [ImportedName' (a,c) (b,d)]
-> [ImportedName' (a,c) (b,d)]
-> Renaming' a b
-> Renaming' c d
mapRenaming src tgt (Renaming from to r) =
Renaming (lookupImportedName from src) (lookupImportedName to tgt) r
openModule_ :: C.QName -> C.ImportDirective -> ScopeM A.ImportDirective
openModule_ cm dir = do
current <- getCurrentModule
m <- amodName <$> resolveModule cm
let acc | not (publicOpen dir) = PrivateNS
| m `isSubModuleOf` current = PublicNS
| otherwise = ImportedNS
(adir, s') <- applyImportDirectiveM cm dir . inScopeBecause (Opened cm) . removeOnlyQualified . restrictPrivate =<< getNamedScope m
let s = setScopeAccess acc s'
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: " ++ 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 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)) = not $ all (== ConName) ks || all (==FldName) ks
where ks = map 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)