#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, forM)
import Control.Monad.Writer hiding (mapM, forM)
import Control.Monad.State hiding (mapM, forM)
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 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.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.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Null (unlessNull)
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 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 = 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" ++ show scope ++ "\nNO SUCH SCOPE " ++ show m
__IMPOSSIBLE__
getCurrentScope :: ScopeM Scope
getCurrentScope = getNamedScope =<< getCurrentModule
createModule :: Bool -> 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
setContextPrecedence :: Precedence -> ScopeM ()
setContextPrecedence p = modifyScope_ $ \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 noFixity'
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 -> do
let filtKind = filter $ \ y -> anameKind (fst y) `elem` kinds
filtName = filter $ \ y -> maybe True (Set.member (aName (fst y))) names
case filtKind $ filtName $ scopeLookup' x scope of
[] -> return UnknownName
ds | all ((==ConName) . anameKind . fst) ds ->
return $ ConstructorName $ map (upd . fst) ds
[(d, a)] | anameKind d == FldName ->
return $ FieldName $ upd d
[(d, a)] | anameKind d == PatternSynName ->
return $ PatternSynResName $ upd d
[(d, a)] ->
return $ DefinedName a $ upd d
ds -> typeError $ AmbiguousName x (map (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
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 id
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' <- 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 $ second $ ((x, y):)
addMod x y = modify $ first $ ((x, y):)
findName x = lookup x <$> gets snd
findMod x = lookup x <$> gets fst
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
y <- A.qualify new' <$> refresh (qnameName x)
lift $ reportSLn "scope.copy" 50 $ " Copying " ++ show x ++ " to " ++ show y
y <- return $ setRange rnew y
addName x y
return y
renMod :: A.ModuleName -> WSM A.ModuleName
renMod x = do
ifJustM (findMod x) return $ do
y <- do
y <- refresh (last $ A.mnameToList x)
return $ A.mnameFromList $ newL ++ [y]
if (x == y) then return x else do
lift $ reportSLn "scope.copy" 50 $ " Copying module " ++ show x ++ " to " ++ show y
addMod x y
lift $ createModule False y
s0 <- lift $ getNamedScope x
s <- withCurrentModule' y $ copy y s0
lift $ modifyNamedScope y (const s)
return y
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 \\ 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 " ++ intercalate ", " (map show 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: " ++ show 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: " ++ show 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)) =
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)