summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Scope/Monad.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax/Scope/Monad.hs')
-rw-r--r--src/full/Agda/Syntax/Scope/Monad.hs84
1 files changed, 52 insertions, 32 deletions
diff --git a/src/full/Agda/Syntax/Scope/Monad.hs b/src/full/Agda/Syntax/Scope/Monad.hs
index 0b7f399..c4fb90f 100644
--- a/src/full/Agda/Syntax/Scope/Monad.hs
+++ b/src/full/Agda/Syntax/Scope/Monad.hs
@@ -1,5 +1,9 @@
{-# LANGUAGE CPP #-}
+#if __GLASGOW_HASKELL__ >= 710
+{-# LANGUAGE FlexibleContexts #-}
+#endif
+
{-| The scope monad with operations.
-}
@@ -16,6 +20,8 @@ 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
@@ -197,29 +203,43 @@ data ResolvedName = VarName A.Name
| ConstructorName [AbstractName]
| PatternSynResName AbstractName
| UnknownName
- deriving (Show)
+ deriving (Show, Eq)
-- | Look up the abstract name referred to by a given concrete name.
resolveName :: C.QName -> ScopeM ResolvedName
-resolveName = resolveName' allKindsOfNames
+resolveName = resolveName' allKindsOfNames Nothing
-- | Look up the abstract name corresponding to a concrete name of
--- a certain kind.
+-- a certain kind and/or from a given set of names.
-- Sometimes we know already that we are dealing with a constructor
-- or pattern synonym (e.g. when we have parsed a pattern).
-- Then, we can ignore conflicting definitions of that name
-- of a different kind. (See issue 822.)
-resolveName' :: [KindOfName] -> C.QName -> ScopeM ResolvedName
-resolveName' kinds x = do
+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
+ 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
-- Case: we have a local variable x.
- Just (LocalVar y) -> return $ VarName $ y { nameConcrete = unqualify x }
- -- Case: ... but is shadowed by some imports.
- Just (ShadowedVar y ys) -> typeError $ AmbiguousName x $ A.qualify_ y : map anameName ys
+ Just (LocalVar y) -> retVar y
+ -- Case: ... but is (perhaps) shadowed by some imports.
+ 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
-- Case: we do not have a local variable x.
- Nothing -> case filter ((`elem` kinds) . anameKind . fst) $ scopeLookup' x scope of
+ 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
@@ -243,19 +263,25 @@ resolveModule x = do
[] -> typeError $ NoSuchModule x
ms -> typeError $ AmbiguousModule x (map amodName ms)
--- | Get the fixity of a name. The name is assumed to be in scope.
-getFixity :: C.QName -> ScopeM Fixity'
-getFixity x = do
- r <- resolveName x
+-- | Get the notation of a name. The name is assumed to be in scope.
+getNotation
+ :: C.QName
+ -> Set A.Name
+ -- ^ The name must correspond to one of the names in this set.
+ -> ScopeM NewNotation
+getNotation x ns = do
+ r <- resolveName' allKindsOfNames (Just ns) x
case r of
- VarName y -> return $ nameFixity y
- DefinedName _ d -> return $ aFixity d
- FieldName d -> return $ aFixity d
- ConstructorName ds -> return $ chooseFixity $ map aFixity ds
- PatternSynResName n -> return $ aFixity n
+ 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
- aFixity = nameFixity . qnameName . anameName
+ notation = namesToNotation x . qnameName . anameName
-- * Binding names
@@ -319,7 +345,7 @@ type WSM = StateT Out ScopeM
-- alternative to qualification by their module).
-- (See Issue 836).
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) (Map.empty, Map.empty)
+copyScope oldc new s = first (inScopeBecause $ Applied oldc) <$> runStateT (copy new s) ([], [])
where
-- | A memoizing algorithm, the renamings serving as memo structure.
copy :: A.ModuleName -> Scope -> StateT (A.Ren A.ModuleName, A.Ren A.QName) ScopeM Scope
@@ -351,35 +377,29 @@ copyScope oldc new s = first (inScopeBecause $ Applied oldc) <$> runStateT (copy
_ -> lensAnameName f d
-- Adding to memo structure.
- addName x y = modify $ second $ Map.insert x y
- addMod x y = modify $ first $ Map.insert x y
+ addName x y = modify $ second $ ((x, y):)
+ addMod x y = modify $ first $ ((x, y):)
-- Querying the memo structure.
- findName x = Map.lookup x <$> gets snd
- findMod x = Map.lookup x <$> gets fst
+ findName x = lookup x <$> gets snd
+ findMod x = lookup x <$> gets fst
-- Change a binding M.x -> old.M'.y to M.x -> new.M'.y
renName :: A.QName -> WSM A.QName
renName x = do
- lift $ reportSLn "scope.copy" 50 $ " Copying " ++ show x
- -- If we've seen it already, just return its copy.
- (`fromMaybeM` findName x) $ do
- -- We have not processed this name @x@, so copy it to some @y@.
-- Check whether we have already seen a module of the same name.
-- If yes, use its copy as @y@.
y <- ifJustM (findMod $ qnameToMName x) (return . mnameToQName) $ {- else -} do
-- First time, generate a fresh name for it.
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
-- Change a binding M.x -> old.M'.y to M.x -> new.M'.y
renMod :: A.ModuleName -> WSM A.ModuleName
renMod x = do
- -- If we've seen it already, just return its copy.
- (`fromMaybeM` findMod x) $ do
- -- We have not processed this name @x@, so copy it to some @y@.
-- Check whether we have seen it already, yet as name.
-- If yes, use its copy as @y@.
y <- ifJustM (findName $ mnameToQName x) (return . qnameToMName) $ {- else -} do