{-# LANGUAGE NondecreasingIndentation #-}

{-| The scope monad with operations.
-}

module Agda.Syntax.Scope.Monad where

import Prelude hiding (null)

import Control.Arrow ((***))
import Control.Monad
import Control.Monad.Except
import Control.Monad.State

import Data.Either ( partitionEithers )
import Data.Foldable (all, traverse_)
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.Traversable hiding (for)

import Agda.Interaction.Options
import Agda.Interaction.Options.Warnings

import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Abstract.Name as A
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract (ScopeCopyInfo(..))
import Agda.Syntax.Concrete as C
import Agda.Syntax.Concrete.Fixity
import Agda.Syntax.Concrete.Definitions ( DeclarationWarning(..) ,DeclarationWarning'(..) )
  -- TODO: move the relevant warnings out of there
import Agda.Syntax.Scope.Base as A

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Builtin ( HasBuiltins , getBuiltinName' , builtinSet , builtinProp , builtinSetOmega, builtinSSetOmega )
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.Trace
import Agda.TypeChecking.Positivity.Occurrence (Occurrence)
import Agda.TypeChecking.Warnings ( warning, warning' )

import qualified Agda.Utils.AssocList as AssocList
import Agda.Utils.CallStack ( CallStack, HasCallStack, withCallerCallStack )
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.List1 (List1, pattern (:|), nonEmpty)
import Agda.Utils.List2 (List2(List2))
import qualified Agda.Utils.List1 as List1
import qualified Agda.Utils.List2 as List2
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty
import Agda.Utils.Singleton
import Agda.Utils.Suffix as C

import Agda.Utils.Impossible

---------------------------------------------------------------------------
-- * The scope checking monad
---------------------------------------------------------------------------

-- | To simplify interaction between scope checking and type checking (in
--   particular when chasing imports), we use the same monad.
type ScopeM = TCM

-- Debugging

printLocals :: Int -> String -> ScopeM ()
printLocals :: Int -> [Char] -> TCMT IO ()
printLocals Int
v [Char]
s = [Char] -> Int -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"scope.top" Int
v (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
  LocalVars
locals <- TCMT IO LocalVars
forall (m :: * -> *). ReadTCState m => m LocalVars
getLocalVars
  [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.top" Int
v ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ LocalVars -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow LocalVars
locals

scopeWarning' :: CallStack -> DeclarationWarning' -> ScopeM ()
scopeWarning' :: CallStack -> DeclarationWarning' -> TCMT IO ()
scopeWarning' CallStack
loc = CallStack -> Warning -> TCMT IO ()
forall (m :: * -> *).
MonadWarning m =>
CallStack -> Warning -> m ()
warning' CallStack
loc (Warning -> TCMT IO ())
-> (DeclarationWarning' -> Warning)
-> DeclarationWarning'
-> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeclarationWarning -> Warning
NicifierIssue (DeclarationWarning -> Warning)
-> (DeclarationWarning' -> DeclarationWarning)
-> DeclarationWarning'
-> Warning
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> DeclarationWarning' -> DeclarationWarning
DeclarationWarning CallStack
loc

scopeWarning :: HasCallStack => DeclarationWarning' -> ScopeM ()
scopeWarning :: HasCallStack => DeclarationWarning' -> TCMT IO ()
scopeWarning = (CallStack -> DeclarationWarning' -> TCMT IO ())
-> DeclarationWarning' -> TCMT IO ()
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> DeclarationWarning' -> TCMT IO ()
scopeWarning'

---------------------------------------------------------------------------
-- * General operations
---------------------------------------------------------------------------

isDatatypeModule :: ReadTCState m => A.ModuleName -> m (Maybe DataOrRecordModule)
isDatatypeModule :: forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m (Maybe DataOrRecordModule)
isDatatypeModule ModuleName
m = do
   Scope -> Maybe DataOrRecordModule
scopeDatatypeModule (Scope -> Maybe DataOrRecordModule)
-> (Map ModuleName Scope -> Scope)
-> Map ModuleName Scope
-> Maybe DataOrRecordModule
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Scope -> ModuleName -> Map ModuleName Scope -> Scope
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Scope
forall a. HasCallStack => a
__IMPOSSIBLE__ ModuleName
m (Map ModuleName Scope -> Maybe DataOrRecordModule)
-> m (Map ModuleName Scope) -> m (Maybe DataOrRecordModule)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' (Map ModuleName Scope) ScopeInfo -> m (Map ModuleName Scope)
forall (m :: * -> *) a. ReadTCState m => Lens' a ScopeInfo -> m a
useScope Lens' (Map ModuleName Scope) ScopeInfo
scopeModules

getCurrentModule :: ReadTCState m => m A.ModuleName
getCurrentModule :: forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule = Range -> ModuleName -> ModuleName
forall a. SetRange a => Range -> a -> a
setRange Range
forall a. Range' a
noRange (ModuleName -> ModuleName) -> m ModuleName -> m ModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' ModuleName ScopeInfo -> m ModuleName
forall (m :: * -> *) a. ReadTCState m => Lens' a ScopeInfo -> m a
useScope Lens' ModuleName ScopeInfo
scopeCurrent

setCurrentModule :: MonadTCState m => A.ModuleName -> m ()
setCurrentModule :: forall (m :: * -> *). MonadTCState m => ModuleName -> m ()
setCurrentModule ModuleName
m = (ScopeInfo -> ScopeInfo) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(ScopeInfo -> ScopeInfo) -> m ()
modifyScope ((ScopeInfo -> ScopeInfo) -> m ())
-> (ScopeInfo -> ScopeInfo) -> m ()
forall a b. (a -> b) -> a -> b
$ Lens' ModuleName ScopeInfo -> LensSet ModuleName ScopeInfo
forall i o. Lens' i o -> LensSet i o
set Lens' ModuleName ScopeInfo
scopeCurrent ModuleName
m

withCurrentModule :: (ReadTCState m, MonadTCState m) => A.ModuleName -> m a -> m a
withCurrentModule :: forall (m :: * -> *) a.
(ReadTCState m, MonadTCState m) =>
ModuleName -> m a -> m a
withCurrentModule ModuleName
new m a
action = do
  ModuleName
old <- m ModuleName
forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule
  ModuleName -> m ()
forall (m :: * -> *). MonadTCState m => ModuleName -> m ()
setCurrentModule ModuleName
new
  a
x   <- m a
action
  ModuleName -> m ()
forall (m :: * -> *). MonadTCState m => ModuleName -> m ()
setCurrentModule ModuleName
old
  a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x

withCurrentModule' :: (MonadTrans t, Monad (t ScopeM)) => A.ModuleName -> t ScopeM a -> t ScopeM a
withCurrentModule' :: forall (t :: (* -> *) -> * -> *) a.
(MonadTrans t, Monad (t (TCMT IO))) =>
ModuleName -> t (TCMT IO) a -> t (TCMT IO) a
withCurrentModule' ModuleName
new t (TCMT IO) a
action = do
  ModuleName
old <- ScopeM ModuleName -> t (TCMT IO) ModuleName
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ScopeM ModuleName
forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule
  TCMT IO () -> t (TCMT IO) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO () -> t (TCMT IO) ()) -> TCMT IO () -> t (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ ModuleName -> TCMT IO ()
forall (m :: * -> *). MonadTCState m => ModuleName -> m ()
setCurrentModule ModuleName
new
  a
x   <- t (TCMT IO) a
action
  TCMT IO () -> t (TCMT IO) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO () -> t (TCMT IO) ()) -> TCMT IO () -> t (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ ModuleName -> TCMT IO ()
forall (m :: * -> *). MonadTCState m => ModuleName -> m ()
setCurrentModule ModuleName
old
  a -> t (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x

getNamedScope :: A.ModuleName -> ScopeM Scope
getNamedScope :: ModuleName -> ScopeM Scope
getNamedScope ModuleName
m = do
  ScopeInfo
scope <- TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  case ModuleName -> Map ModuleName Scope -> Maybe Scope
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ModuleName
m (ScopeInfo
scope ScopeInfo
-> Lens' (Map ModuleName Scope) ScopeInfo -> Map ModuleName Scope
forall o i. o -> Lens' i o -> i
^. Lens' (Map ModuleName Scope) ScopeInfo
scopeModules) of
    Just Scope
s  -> Scope -> ScopeM Scope
forall (m :: * -> *) a. Monad m => a -> m a
return Scope
s
    Maybe Scope
Nothing -> do
      [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"" Int
0 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"ERROR: In scope\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ScopeInfo -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow ScopeInfo
scope [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\nNO SUCH SCOPE " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow ModuleName
m
      ScopeM Scope
forall a. HasCallStack => a
__IMPOSSIBLE__

getCurrentScope :: ScopeM Scope
getCurrentScope :: ScopeM Scope
getCurrentScope = ModuleName -> ScopeM Scope
getNamedScope (ModuleName -> ScopeM Scope) -> ScopeM ModuleName -> ScopeM Scope
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ScopeM ModuleName
forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule

-- | Create a new module with an empty scope.
--   If the module is not new (e.g. duplicate @import@),
--   don't erase its contents.
--   (@Just@ if it is a datatype or record module.)
createModule :: Maybe DataOrRecordModule -> A.ModuleName -> ScopeM ()
createModule :: Maybe DataOrRecordModule -> ModuleName -> TCMT IO ()
createModule Maybe DataOrRecordModule
b ModuleName
m = do
  [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.createModule" Int
10 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"createModule " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow ModuleName
m
  Scope
s <- ScopeM Scope
getCurrentScope
  let parents :: [ModuleName]
parents = Scope -> ModuleName
scopeName Scope
s ModuleName -> [ModuleName] -> [ModuleName]
forall a. a -> [a] -> [a]
: Scope -> [ModuleName]
scopeParents Scope
s
      sm :: Scope
sm = Scope
emptyScope { scopeName :: ModuleName
scopeName           = ModuleName
m
                      , scopeParents :: [ModuleName]
scopeParents        = [ModuleName]
parents
                      , scopeDatatypeModule :: Maybe DataOrRecordModule
scopeDatatypeModule = Maybe DataOrRecordModule
b }
  -- Andreas, 2015-07-02: internal error if module is not new.
  -- Ulf, 2016-02-15: It's not new if multiple imports (#1770).
  -- Andreas, 2020-05-18, issue #3933:
  -- If it is not new (but apparently did not clash),
  -- we do not erase its contents for reasons of monotonicity.
  (Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ()
modifyScopes ((Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ())
-> (Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ (Scope -> Scope -> Scope)
-> ModuleName
-> Scope
-> Map ModuleName Scope
-> Map ModuleName Scope
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Scope -> Scope -> Scope
mergeScope ModuleName
m Scope
sm

-- | Apply a function to the scope map.
modifyScopes :: (Map A.ModuleName Scope -> Map A.ModuleName Scope) -> ScopeM ()
modifyScopes :: (Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ()
modifyScopes = (ScopeInfo -> ScopeInfo) -> TCMT IO ()
forall (m :: * -> *).
MonadTCState m =>
(ScopeInfo -> ScopeInfo) -> m ()
modifyScope ((ScopeInfo -> ScopeInfo) -> TCMT IO ())
-> ((Map ModuleName Scope -> Map ModuleName Scope)
    -> ScopeInfo -> ScopeInfo)
-> (Map ModuleName Scope -> Map ModuleName Scope)
-> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' (Map ModuleName Scope) ScopeInfo
-> (Map ModuleName Scope -> Map ModuleName Scope)
-> ScopeInfo
-> ScopeInfo
forall i o. Lens' i o -> LensMap i o
over Lens' (Map ModuleName Scope) ScopeInfo
scopeModules

-- | Apply a function to the given scope.
modifyNamedScope :: A.ModuleName -> (Scope -> Scope) -> ScopeM ()
modifyNamedScope :: ModuleName -> (Scope -> Scope) -> TCMT IO ()
modifyNamedScope ModuleName
m Scope -> Scope
f = (Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ()
modifyScopes ((Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ())
-> (Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ (Scope -> Scope)
-> ModuleName -> Map ModuleName Scope -> Map ModuleName Scope
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust Scope -> Scope
f ModuleName
m

setNamedScope :: A.ModuleName -> Scope -> ScopeM ()
setNamedScope :: ModuleName -> Scope -> TCMT IO ()
setNamedScope ModuleName
m Scope
s = ModuleName -> (Scope -> Scope) -> TCMT IO ()
modifyNamedScope ModuleName
m ((Scope -> Scope) -> TCMT IO ()) -> (Scope -> Scope) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Scope -> Scope -> Scope
forall a b. a -> b -> a
const Scope
s

-- | Apply a monadic function to the top scope.
modifyNamedScopeM :: A.ModuleName -> (Scope -> ScopeM (a, Scope)) -> ScopeM a
modifyNamedScopeM :: forall a. ModuleName -> (Scope -> ScopeM (a, Scope)) -> ScopeM a
modifyNamedScopeM ModuleName
m Scope -> ScopeM (a, Scope)
f = do
  (a
a, Scope
s) <- Scope -> ScopeM (a, Scope)
f (Scope -> ScopeM (a, Scope)) -> ScopeM Scope -> ScopeM (a, Scope)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ModuleName -> ScopeM Scope
getNamedScope ModuleName
m
  ModuleName -> Scope -> TCMT IO ()
setNamedScope ModuleName
m Scope
s
  a -> ScopeM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

-- | Apply a function to the current scope.
modifyCurrentScope :: (Scope -> Scope) -> ScopeM ()
modifyCurrentScope :: (Scope -> Scope) -> TCMT IO ()
modifyCurrentScope Scope -> Scope
f = ScopeM ModuleName
forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule ScopeM ModuleName -> (ModuleName -> TCMT IO ()) -> TCMT IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (ModuleName -> (Scope -> Scope) -> TCMT IO ()
`modifyNamedScope` Scope -> Scope
f)

modifyCurrentScopeM :: (Scope -> ScopeM (a, Scope)) -> ScopeM a
modifyCurrentScopeM :: forall a. (Scope -> ScopeM (a, Scope)) -> ScopeM a
modifyCurrentScopeM Scope -> ScopeM (a, Scope)
f = ScopeM ModuleName
forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule ScopeM ModuleName -> (ModuleName -> TCMT IO a) -> TCMT IO a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (ModuleName -> (Scope -> ScopeM (a, Scope)) -> TCMT IO a
forall a. ModuleName -> (Scope -> ScopeM (a, Scope)) -> ScopeM a
`modifyNamedScopeM` Scope -> ScopeM (a, Scope)
f)

-- | Apply a function to the public or private name space.
modifyCurrentNameSpace :: NameSpaceId -> (NameSpace -> NameSpace) -> ScopeM ()
modifyCurrentNameSpace :: NameSpaceId -> (NameSpace -> NameSpace) -> TCMT IO ()
modifyCurrentNameSpace NameSpaceId
acc NameSpace -> NameSpace
f = (Scope -> Scope) -> TCMT IO ()
modifyCurrentScope ((Scope -> Scope) -> TCMT IO ()) -> (Scope -> Scope) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ (ScopeNameSpaces -> ScopeNameSpaces) -> Scope -> Scope
updateScopeNameSpaces ((ScopeNameSpaces -> ScopeNameSpaces) -> Scope -> Scope)
-> (ScopeNameSpaces -> ScopeNameSpaces) -> Scope -> Scope
forall a b. (a -> b) -> a -> b
$
  NameSpaceId
-> (NameSpace -> NameSpace) -> ScopeNameSpaces -> ScopeNameSpaces
forall k v. Eq k => k -> (v -> v) -> AssocList k v -> AssocList k v
AssocList.updateAt NameSpaceId
acc NameSpace -> NameSpace
f

setContextPrecedence :: PrecedenceStack -> ScopeM ()
setContextPrecedence :: PrecedenceStack -> TCMT IO ()
setContextPrecedence = (ScopeInfo -> ScopeInfo) -> TCMT IO ()
forall (m :: * -> *).
MonadTCState m =>
(ScopeInfo -> ScopeInfo) -> m ()
modifyScope_ ((ScopeInfo -> ScopeInfo) -> TCMT IO ())
-> (PrecedenceStack -> ScopeInfo -> ScopeInfo)
-> PrecedenceStack
-> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' PrecedenceStack ScopeInfo
-> PrecedenceStack -> ScopeInfo -> ScopeInfo
forall i o. Lens' i o -> LensSet i o
set Lens' PrecedenceStack ScopeInfo
scopePrecedence

withContextPrecedence :: ReadTCState m => Precedence -> m a -> m a
withContextPrecedence :: forall (m :: * -> *) a. ReadTCState m => Precedence -> m a -> m a
withContextPrecedence Precedence
p =
  Lens' PrecedenceStack TCState
-> (PrecedenceStack -> PrecedenceStack) -> m a -> m a
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a TCState -> (a -> a) -> m b -> m b
locallyTCState ((ScopeInfo -> f ScopeInfo) -> TCState -> f TCState
Lens' ScopeInfo TCState
stScope ((ScopeInfo -> f ScopeInfo) -> TCState -> f TCState)
-> ((PrecedenceStack -> f PrecedenceStack)
    -> ScopeInfo -> f ScopeInfo)
-> (PrecedenceStack -> f PrecedenceStack)
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PrecedenceStack -> f PrecedenceStack) -> ScopeInfo -> f ScopeInfo
Lens' PrecedenceStack ScopeInfo
scopePrecedence) ((PrecedenceStack -> PrecedenceStack) -> m a -> m a)
-> (PrecedenceStack -> PrecedenceStack) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ Precedence -> PrecedenceStack -> PrecedenceStack
pushPrecedence Precedence
p

getLocalVars :: ReadTCState m => m LocalVars
getLocalVars :: forall (m :: * -> *). ReadTCState m => m LocalVars
getLocalVars = Lens' LocalVars ScopeInfo -> m LocalVars
forall (m :: * -> *) a. ReadTCState m => Lens' a ScopeInfo -> m a
useScope Lens' LocalVars ScopeInfo
scopeLocals

modifyLocalVars :: (LocalVars -> LocalVars) -> ScopeM ()
modifyLocalVars :: (LocalVars -> LocalVars) -> TCMT IO ()
modifyLocalVars = (ScopeInfo -> ScopeInfo) -> TCMT IO ()
forall (m :: * -> *).
MonadTCState m =>
(ScopeInfo -> ScopeInfo) -> m ()
modifyScope_ ((ScopeInfo -> ScopeInfo) -> TCMT IO ())
-> ((LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo)
-> (LocalVars -> LocalVars)
-> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo
updateScopeLocals

setLocalVars :: LocalVars -> ScopeM ()
setLocalVars :: LocalVars -> TCMT IO ()
setLocalVars LocalVars
vars = (LocalVars -> LocalVars) -> TCMT IO ()
modifyLocalVars ((LocalVars -> LocalVars) -> TCMT IO ())
-> (LocalVars -> LocalVars) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ LocalVars -> LocalVars -> LocalVars
forall a b. a -> b -> a
const LocalVars
vars

-- | Run a computation without changing the local variables.
withLocalVars :: ScopeM a -> ScopeM a
withLocalVars :: forall a. ScopeM a -> ScopeM a
withLocalVars = TCMT IO LocalVars
-> (LocalVars -> TCMT IO ()) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ TCMT IO LocalVars
forall (m :: * -> *). ReadTCState m => m LocalVars
getLocalVars LocalVars -> TCMT IO ()
setLocalVars

-- | Run a computation outside some number of local variables and add them back afterwards. This
--   lets you bind variables in the middle of the context and is used when binding generalizable
--   variables (#3735).
outsideLocalVars :: Int -> ScopeM a -> ScopeM a
outsideLocalVars :: forall a. Int -> ScopeM a -> ScopeM a
outsideLocalVars Int
n ScopeM a
m = do
  LocalVars
inner <- Int -> LocalVars -> LocalVars
forall a. Int -> [a] -> [a]
take Int
n (LocalVars -> LocalVars) -> TCMT IO LocalVars -> TCMT IO LocalVars
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO LocalVars
forall (m :: * -> *). ReadTCState m => m LocalVars
getLocalVars
  (LocalVars -> LocalVars) -> TCMT IO ()
modifyLocalVars (Int -> LocalVars -> LocalVars
forall a. Int -> [a] -> [a]
drop Int
n)
  a
x <- ScopeM a
m
  (LocalVars -> LocalVars) -> TCMT IO ()
modifyLocalVars (LocalVars
inner LocalVars -> LocalVars -> LocalVars
forall a. [a] -> [a] -> [a]
++)
  a -> ScopeM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x

-- | Check that the newly added variable have unique names.

withCheckNoShadowing :: ScopeM a -> ScopeM a
withCheckNoShadowing :: forall a. ScopeM a -> ScopeM a
withCheckNoShadowing = TCMT IO LocalVars
-> (LocalVars -> TCMT IO ()) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ TCMT IO LocalVars
forall (m :: * -> *). ReadTCState m => m LocalVars
getLocalVars ((LocalVars -> TCMT IO ()) -> TCMT IO a -> TCMT IO a)
-> (LocalVars -> TCMT IO ()) -> TCMT IO a -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ \ LocalVars
lvarsOld ->
  LocalVars -> LocalVars -> TCMT IO ()
checkNoShadowing LocalVars
lvarsOld (LocalVars -> TCMT IO ()) -> TCMT IO LocalVars -> TCMT IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO LocalVars
forall (m :: * -> *). ReadTCState m => m LocalVars
getLocalVars

checkNoShadowing :: LocalVars  -- ^ Old local scope
                 -> LocalVars  -- ^ New local scope
                 -> ScopeM ()
checkNoShadowing :: LocalVars -> LocalVars -> TCMT IO ()
checkNoShadowing LocalVars
old LocalVars
new = do
  PragmaOptions
opts <- TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (WarningName
ShadowingInTelescope_ WarningName -> Set WarningName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member`
          (PragmaOptions -> WarningMode
optWarningMode PragmaOptions
opts WarningMode
-> Lens' (Set WarningName) WarningMode -> Set WarningName
forall o i. o -> Lens' i o -> i
^. Lens' (Set WarningName) WarningMode
warningSet)) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
    -- LocalVars is currnently an AssocList so the difference between
    -- two local scope is the left part of the new one.
    let diff :: LocalVars
diff = Int -> LocalVars -> LocalVars
forall a. Int -> [a] -> [a]
dropEnd (LocalVars -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length LocalVars
old) LocalVars
new
    -- Filter out the underscores.
    let newNames :: [Name]
newNames = (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Name -> Bool) -> Name -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName) ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ LocalVars -> [Name]
forall k v. AssocList k v -> [k]
AssocList.keys LocalVars
diff
    -- Associate each name to its occurrences.
    let nameOccs1 :: [(C.Name, List1 Range)]
        nameOccs1 :: [(Name, NonEmpty Range)]
nameOccs1 = Map Name (NonEmpty Range) -> [(Name, NonEmpty Range)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Name (NonEmpty Range) -> [(Name, NonEmpty Range)])
-> Map Name (NonEmpty Range) -> [(Name, NonEmpty Range)]
forall a b. (a -> b) -> a -> b
$ (NonEmpty Range -> NonEmpty Range -> NonEmpty Range)
-> [(Name, NonEmpty Range)] -> Map Name (NonEmpty Range)
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith NonEmpty Range -> NonEmpty Range -> NonEmpty Range
forall a. Semigroup a => a -> a -> a
(<>) ([(Name, NonEmpty Range)] -> Map Name (NonEmpty Range))
-> [(Name, NonEmpty Range)] -> Map Name (NonEmpty Range)
forall a b. (a -> b) -> a -> b
$ (Name -> (Name, NonEmpty Range))
-> [Name] -> [(Name, NonEmpty Range)]
forall a b. (a -> b) -> [a] -> [b]
map Name -> (Name, NonEmpty Range)
pairWithRange [Name]
newNames
    -- Warn if we have two or more occurrences of the same name.
    let nameOccs2 :: [(C.Name, List2 Range)]
        nameOccs2 :: [(Name, List2 Range)]
nameOccs2 = ((Name, NonEmpty Range) -> Maybe (Name, List2 Range))
-> [(Name, NonEmpty Range)] -> [(Name, List2 Range)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((NonEmpty Range -> Maybe (List2 Range))
-> (Name, NonEmpty Range) -> Maybe (Name, List2 Range)
forall (t :: * -> *) (m :: * -> *) a b.
(Decoration t, Functor m) =>
(a -> m b) -> t a -> m (t b)
traverseF NonEmpty Range -> Maybe (List2 Range)
forall a. List1 a -> Maybe (List2 a)
List2.fromList1Maybe) [(Name, NonEmpty Range)]
nameOccs1
    [(Name, List2 Range)]
-> TCMT IO ()
-> ((Name, List2 Range) -> [(Name, List2 Range)] -> TCMT IO ())
-> TCMT IO ()
forall a b. [a] -> b -> (a -> [a] -> b) -> b
caseList [(Name, List2 Range)]
nameOccs2 (() -> TCMT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (((Name, List2 Range) -> [(Name, List2 Range)] -> TCMT IO ())
 -> TCMT IO ())
-> ((Name, List2 Range) -> [(Name, List2 Range)] -> TCMT IO ())
-> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ \ (Name, List2 Range)
c [(Name, List2 Range)]
conflicts -> do
      HasCallStack => DeclarationWarning' -> TCMT IO ()
DeclarationWarning' -> TCMT IO ()
scopeWarning (DeclarationWarning' -> TCMT IO ())
-> DeclarationWarning' -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ List1 (Name, List2 Range) -> DeclarationWarning'
ShadowingInTelescope (List1 (Name, List2 Range) -> DeclarationWarning')
-> List1 (Name, List2 Range) -> DeclarationWarning'
forall a b. (a -> b) -> a -> b
$ (Name, List2 Range)
c (Name, List2 Range)
-> [(Name, List2 Range)] -> List1 (Name, List2 Range)
forall a. a -> [a] -> NonEmpty a
:| [(Name, List2 Range)]
conflicts
  where
    pairWithRange :: C.Name -> (C.Name, List1 Range)
    pairWithRange :: Name -> (Name, NonEmpty Range)
pairWithRange Name
n = (Name
n, Range -> NonEmpty Range
forall el coll. Singleton el coll => el -> coll
singleton (Range -> NonEmpty Range) -> Range -> NonEmpty Range
forall a b. (a -> b) -> a -> b
$ Name -> Range
forall a. HasRange a => a -> Range
getRange Name
n)

getVarsToBind :: ScopeM LocalVars
getVarsToBind :: TCMT IO LocalVars
getVarsToBind = Lens' LocalVars ScopeInfo -> TCMT IO LocalVars
forall (m :: * -> *) a. ReadTCState m => Lens' a ScopeInfo -> m a
useScope Lens' LocalVars ScopeInfo
scopeVarsToBind

addVarToBind :: C.Name -> LocalVar -> ScopeM ()
addVarToBind :: Name -> LocalVar -> TCMT IO ()
addVarToBind Name
x LocalVar
y = (ScopeInfo -> ScopeInfo) -> TCMT IO ()
forall (m :: * -> *).
MonadTCState m =>
(ScopeInfo -> ScopeInfo) -> m ()
modifyScope_ ((ScopeInfo -> ScopeInfo) -> TCMT IO ())
-> (ScopeInfo -> ScopeInfo) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo
updateVarsToBind ((LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo)
-> (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo
forall a b. (a -> b) -> a -> b
$ Name -> LocalVar -> LocalVars -> LocalVars
forall k v. k -> v -> AssocList k v -> AssocList k v
AssocList.insert Name
x LocalVar
y

-- | After collecting some variable names in the scopeVarsToBind,
--   bind them all simultaneously.
bindVarsToBind :: ScopeM ()
bindVarsToBind :: TCMT IO ()
bindVarsToBind = do
  LocalVars
vars <- TCMT IO LocalVars
getVarsToBind
  (LocalVars -> LocalVars) -> TCMT IO ()
modifyLocalVars (LocalVars
varsLocalVars -> LocalVars -> LocalVars
forall a. [a] -> [a] -> [a]
++)
  Int -> [Char] -> TCMT IO ()
printLocals Int
10 [Char]
"bound variables:"
  (ScopeInfo -> ScopeInfo) -> TCMT IO ()
forall (m :: * -> *).
MonadTCState m =>
(ScopeInfo -> ScopeInfo) -> m ()
modifyScope_ ((ScopeInfo -> ScopeInfo) -> TCMT IO ())
-> (ScopeInfo -> ScopeInfo) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ LocalVars -> ScopeInfo -> ScopeInfo
setVarsToBind []

annotateDecls :: ReadTCState m => m [A.Declaration] -> m A.Declaration
annotateDecls :: forall (m :: * -> *).
ReadTCState m =>
m [Declaration] -> m Declaration
annotateDecls m [Declaration]
m = do
  [Declaration]
ds <- m [Declaration]
m
  ScopeInfo
s  <- m ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  Declaration -> m Declaration
forall (m :: * -> *) a. Monad m => a -> m a
return (Declaration -> m Declaration) -> Declaration -> m Declaration
forall a b. (a -> b) -> a -> b
$ ScopeInfo -> [Declaration] -> Declaration
A.ScopedDecl ScopeInfo
s [Declaration]
ds

annotateExpr :: ReadTCState m => m A.Expr -> m A.Expr
annotateExpr :: forall (m :: * -> *). ReadTCState m => m Expr -> m Expr
annotateExpr m Expr
m = do
  Expr
e <- m Expr
m
  ScopeInfo
s <- m ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> m Expr) -> Expr -> m Expr
forall a b. (a -> b) -> a -> b
$ ScopeInfo -> Expr -> Expr
A.ScopedExpr ScopeInfo
s Expr
e

---------------------------------------------------------------------------
-- * Names
---------------------------------------------------------------------------

-- | Create a fresh abstract name from a concrete name.
--
--   This function is used when we translate a concrete name
--   in a binder.  The 'Range' of the concrete name is
--   saved as the 'nameBindingSite' of the abstract name.
freshAbstractName :: Fixity' -> C.Name -> ScopeM A.Name
freshAbstractName :: Fixity' -> Name -> ScopeM Name
freshAbstractName Fixity'
fx Name
x = do
  NameId
i <- TCMT IO NameId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
  Name -> ScopeM Name
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> ScopeM Name) -> Name -> ScopeM Name
forall a b. (a -> b) -> a -> b
$ A.Name
    { nameId :: NameId
nameId          = NameId
i
    , nameConcrete :: Name
nameConcrete    = Name
x
    , nameCanonical :: Name
nameCanonical   = Name
x
    , nameBindingSite :: Range
nameBindingSite = Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x
    , nameFixity :: Fixity'
nameFixity      = Fixity'
fx
    , nameIsRecordName :: Bool
nameIsRecordName = Bool
False
    }

-- | @freshAbstractName_ = freshAbstractName noFixity'@
freshAbstractName_ :: C.Name -> ScopeM A.Name
freshAbstractName_ :: Name -> ScopeM Name
freshAbstractName_ = Fixity' -> Name -> ScopeM Name
freshAbstractName Fixity'
noFixity'

-- | Create a fresh abstract qualified name.
freshAbstractQName :: Fixity' -> C.Name -> ScopeM A.QName
freshAbstractQName :: Fixity' -> Name -> ScopeM QName
freshAbstractQName Fixity'
fx Name
x = do
  Name
y <- Fixity' -> Name -> ScopeM Name
freshAbstractName Fixity'
fx Name
x
  ModuleName
m <- ScopeM ModuleName
forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule
  QName -> ScopeM QName
forall (m :: * -> *) a. Monad m => a -> m a
return (QName -> ScopeM QName) -> QName -> ScopeM QName
forall a b. (a -> b) -> a -> b
$ ModuleName -> Name -> QName
A.qualify ModuleName
m Name
y

freshAbstractQName' :: C.Name -> ScopeM A.QName
freshAbstractQName' :: Name -> ScopeM QName
freshAbstractQName' Name
x = do
  Fixity'
fx <- Name -> ScopeM Fixity'
getConcreteFixity Name
x
  Fixity' -> Name -> ScopeM QName
freshAbstractQName Fixity'
fx Name
x

-- | Create a concrete name that is not yet in scope.
-- | NOTE: See @chooseName@ in @Agda.Syntax.Translation.AbstractToConcrete@ for similar logic.
-- | NOTE: See @withName@ in @Agda.Syntax.Translation.ReflectedToAbstract@ for similar logic.
freshConcreteName :: Range -> Int -> String -> ScopeM C.Name
freshConcreteName :: Range -> Int -> [Char] -> ScopeM Name
freshConcreteName Range
r Int
i [Char]
s = do
  let cname :: Name
cname = Range -> NameInScope -> NameParts -> Name
C.Name Range
r NameInScope
C.NotInScope (NameParts -> Name) -> NameParts -> Name
forall a b. (a -> b) -> a -> b
$ NamePart -> NameParts
forall el coll. Singleton el coll => el -> coll
singleton (NamePart -> NameParts) -> NamePart -> NameParts
forall a b. (a -> b) -> a -> b
$ [Char] -> NamePart
Id ([Char] -> NamePart) -> [Char] -> NamePart
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
stringToRawName ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i
  QName -> ScopeM ResolvedName
resolveName (Name -> QName
C.QName Name
cname) ScopeM ResolvedName -> (ResolvedName -> ScopeM Name) -> ScopeM Name
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    ResolvedName
UnknownName -> Name -> ScopeM Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
cname
    ResolvedName
_           -> Range -> Int -> [Char] -> ScopeM Name
freshConcreteName Range
r (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [Char]
s

---------------------------------------------------------------------------
-- * Resolving names
---------------------------------------------------------------------------

-- | Look up the abstract name referred to by a given concrete name.
resolveName :: C.QName -> ScopeM ResolvedName
resolveName :: QName -> ScopeM ResolvedName
resolveName = KindsOfNames -> Maybe (Set Name) -> QName -> ScopeM ResolvedName
resolveName' KindsOfNames
allKindsOfNames Maybe (Set Name)
forall a. Maybe a
Nothing

-- | Look up the abstract name corresponding to a concrete name of
--   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' ::
  KindsOfNames -> Maybe (Set A.Name) -> C.QName -> ScopeM ResolvedName
resolveName' :: KindsOfNames -> Maybe (Set Name) -> QName -> ScopeM ResolvedName
resolveName' KindsOfNames
kinds Maybe (Set Name)
names QName
x = ExceptT (List1 QName) (TCMT IO) ResolvedName
-> TCMT IO (Either (List1 QName) ResolvedName)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (KindsOfNames
-> Maybe (Set Name)
-> QName
-> ExceptT (List1 QName) (TCMT IO) ResolvedName
forall (m :: * -> *).
(ReadTCState m, HasBuiltins m, MonadError (List1 QName) m) =>
KindsOfNames -> Maybe (Set Name) -> QName -> m ResolvedName
tryResolveName KindsOfNames
kinds Maybe (Set Name)
names QName
x) TCMT IO (Either (List1 QName) ResolvedName)
-> (Either (List1 QName) ResolvedName -> ScopeM ResolvedName)
-> ScopeM ResolvedName
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Left List1 QName
ys  -> Call -> ScopeM ResolvedName -> ScopeM ResolvedName
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> Call
SetRange (Range -> Call) -> Range -> Call
forall a b. (a -> b) -> a -> b
$ QName -> Range
forall a. HasRange a => a -> Range
getRange QName
x) (ScopeM ResolvedName -> ScopeM ResolvedName)
-> ScopeM ResolvedName -> ScopeM ResolvedName
forall a b. (a -> b) -> a -> b
$ TypeError -> ScopeM ResolvedName
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> ScopeM ResolvedName)
-> TypeError -> ScopeM ResolvedName
forall a b. (a -> b) -> a -> b
$ QName -> List1 QName -> TypeError
AmbiguousName QName
x List1 QName
ys
  Right ResolvedName
x' -> ResolvedName -> ScopeM ResolvedName
forall (m :: * -> *) a. Monad m => a -> m a
return ResolvedName
x'

tryResolveName
  :: (ReadTCState m, HasBuiltins m, MonadError (List1 A.QName) m)
  => KindsOfNames       -- ^ Restrict search to these kinds of names.
  -> Maybe (Set A.Name) -- ^ Unless 'Nothing', restrict search to match any of these names.
  -> C.QName            -- ^ Name to be resolved
  -> m ResolvedName     -- ^ If illegally ambiguous, throw error with the ambiguous name.
tryResolveName :: forall (m :: * -> *).
(ReadTCState m, HasBuiltins m, MonadError (List1 QName) m) =>
KindsOfNames -> Maybe (Set Name) -> QName -> m ResolvedName
tryResolveName KindsOfNames
kinds Maybe (Set Name)
names QName
x = do
  ScopeInfo
scope <- m ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  let vars :: AssocList QName LocalVar
vars     = (Name -> QName) -> LocalVars -> AssocList QName LocalVar
forall k k' v. (k -> k') -> AssocList k v -> AssocList k' v
AssocList.mapKeysMonotonic Name -> QName
C.QName (LocalVars -> AssocList QName LocalVar)
-> LocalVars -> AssocList QName LocalVar
forall a b. (a -> b) -> a -> b
$ ScopeInfo
scope ScopeInfo -> Lens' LocalVars ScopeInfo -> LocalVars
forall o i. o -> Lens' i o -> i
^. Lens' LocalVars ScopeInfo
scopeLocals
  case QName -> AssocList QName LocalVar -> Maybe LocalVar
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup QName
x AssocList QName LocalVar
vars of
    -- Case: we have a local variable x, but is (perhaps) shadowed by some imports ys.
    Just (LocalVar Name
y BindingSource
b [AbstractName]
ys) ->
      -- We may ignore the imports filtered out by the @names@ filter.
      [AbstractName]
-> m ResolvedName
-> ([AbstractName] -> m ResolvedName)
-> m ResolvedName
forall a b. Null a => a -> b -> (a -> b) -> b
ifNull ((AbstractName -> AbstractName) -> [AbstractName] -> [AbstractName]
forall a. (a -> AbstractName) -> [a] -> [a]
filterNames AbstractName -> AbstractName
forall a. a -> a
id [AbstractName]
ys)
        {-then-} (ResolvedName -> m ResolvedName
forall (m :: * -> *) a. Monad m => a -> m a
return (ResolvedName -> m ResolvedName) -> ResolvedName -> m ResolvedName
forall a b. (a -> b) -> a -> b
$ Name -> BindingSource -> ResolvedName
VarName Name
y{ nameConcrete :: Name
nameConcrete = QName -> Name
unqualify QName
x } BindingSource
b)
        {-else-} (([AbstractName] -> m ResolvedName) -> m ResolvedName)
-> ([AbstractName] -> m ResolvedName) -> m ResolvedName
forall a b. (a -> b) -> a -> b
$ \ [AbstractName]
ys' ->
          List1 QName -> m ResolvedName
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (List1 QName -> m ResolvedName) -> List1 QName -> m ResolvedName
forall a b. (a -> b) -> a -> b
$ Name -> QName
A.qualify_ Name
y QName -> [QName] -> List1 QName
forall a. a -> [a] -> NonEmpty a
:| (AbstractName -> QName) -> [AbstractName] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map AbstractName -> QName
anameName [AbstractName]
ys'
    -- Case: we do not have a local variable x.
    Maybe LocalVar
Nothing -> do
      -- Consider only names that are in the given set of names and
      -- are of one of the given kinds
      let filtKind :: [(AbstractName, Access)] -> [(AbstractName, Access)]
filtKind = ((AbstractName, Access) -> Bool)
-> [(AbstractName, Access)] -> [(AbstractName, Access)]
forall a. (a -> Bool) -> [a] -> [a]
filter (((AbstractName, Access) -> Bool)
 -> [(AbstractName, Access)] -> [(AbstractName, Access)])
-> ((AbstractName, Access) -> Bool)
-> [(AbstractName, Access)]
-> [(AbstractName, Access)]
forall a b. (a -> b) -> a -> b
$ (KindOfName -> KindsOfNames -> Bool
`elemKindsOfNames` KindsOfNames
kinds) (KindOfName -> Bool)
-> ((AbstractName, Access) -> KindOfName)
-> (AbstractName, Access)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> KindOfName
anameKind (AbstractName -> KindOfName)
-> ((AbstractName, Access) -> AbstractName)
-> (AbstractName, Access)
-> KindOfName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractName, Access) -> AbstractName
forall a b. (a, b) -> a
fst
          possibleNames :: QName -> [(AbstractName, Access)]
possibleNames QName
z = [(AbstractName, Access)] -> [(AbstractName, Access)]
filtKind ([(AbstractName, Access)] -> [(AbstractName, Access)])
-> [(AbstractName, Access)] -> [(AbstractName, Access)]
forall a b. (a -> b) -> a -> b
$ ((AbstractName, Access) -> AbstractName)
-> [(AbstractName, Access)] -> [(AbstractName, Access)]
forall a. (a -> AbstractName) -> [a] -> [a]
filterNames (AbstractName, Access) -> AbstractName
forall a b. (a, b) -> a
fst ([(AbstractName, Access)] -> [(AbstractName, Access)])
-> [(AbstractName, Access)] -> [(AbstractName, Access)]
forall a b. (a -> b) -> a -> b
$ QName -> ScopeInfo -> [(AbstractName, Access)]
forall a. InScope a => QName -> ScopeInfo -> [(a, Access)]
scopeLookup' QName
z ScopeInfo
scope
      -- If the name has a suffix, also consider the possibility that
      -- the base name is in scope (e.g. the builtin sorts `Set` and `Prop`).
      QName -> Bool
canHaveSuffix <- m (QName -> Bool)
forall (m :: * -> *). HasBuiltins m => m (QName -> Bool)
canHaveSuffixTest
      let (Maybe Suffix
xsuffix, QName
xbase) = ((Name -> (Maybe Suffix, Name)) -> QName -> (Maybe Suffix, QName)
Lens' Name QName
C.lensQNameName ((Name -> (Maybe Suffix, Name)) -> QName -> (Maybe Suffix, QName))
-> ((Maybe Suffix -> (Maybe Suffix, Maybe Suffix))
    -> Name -> (Maybe Suffix, Name))
-> (Maybe Suffix -> (Maybe Suffix, Maybe Suffix))
-> QName
-> (Maybe Suffix, QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Suffix -> (Maybe Suffix, Maybe Suffix))
-> Name -> (Maybe Suffix, Name)
Lens' (Maybe Suffix) Name
nameSuffix) (,Maybe Suffix
forall a. Maybe a
Nothing) QName
x
          possibleBaseNames :: [(AbstractName, Access)]
possibleBaseNames = ((AbstractName, Access) -> Bool)
-> [(AbstractName, Access)] -> [(AbstractName, Access)]
forall a. (a -> Bool) -> [a] -> [a]
filter (QName -> Bool
canHaveSuffix (QName -> Bool)
-> ((AbstractName, Access) -> QName)
-> (AbstractName, Access)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> QName
anameName (AbstractName -> QName)
-> ((AbstractName, Access) -> AbstractName)
-> (AbstractName, Access)
-> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractName, Access) -> AbstractName
forall a b. (a, b) -> a
fst) ([(AbstractName, Access)] -> [(AbstractName, Access)])
-> [(AbstractName, Access)] -> [(AbstractName, Access)]
forall a b. (a -> b) -> a -> b
$ QName -> [(AbstractName, Access)]
possibleNames QName
xbase
          suffixedNames :: Maybe (Suffix, NonEmpty (AbstractName, Access))
suffixedNames = (,) (Suffix
 -> NonEmpty (AbstractName, Access)
 -> (Suffix, NonEmpty (AbstractName, Access)))
-> Maybe Suffix
-> Maybe
     (NonEmpty (AbstractName, Access)
      -> (Suffix, NonEmpty (AbstractName, Access)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Suffix -> Maybe Suffix
fromConcreteSuffix Maybe Suffix
xsuffix Maybe
  (NonEmpty (AbstractName, Access)
   -> (Suffix, NonEmpty (AbstractName, Access)))
-> Maybe (NonEmpty (AbstractName, Access))
-> Maybe (Suffix, NonEmpty (AbstractName, Access))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [(AbstractName, Access)] -> Maybe (NonEmpty (AbstractName, Access))
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty [(AbstractName, Access)]
possibleBaseNames
      case ([(AbstractName, Access)] -> Maybe (NonEmpty (AbstractName, Access))
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty ([(AbstractName, Access)]
 -> Maybe (NonEmpty (AbstractName, Access)))
-> [(AbstractName, Access)]
-> Maybe (NonEmpty (AbstractName, Access))
forall a b. (a -> b) -> a -> b
$ QName -> [(AbstractName, Access)]
possibleNames QName
x) of
        Just NonEmpty (AbstractName, Access)
ds  | let ks :: NonEmpty (Maybe Induction)
ks = ((AbstractName, Access) -> Maybe Induction)
-> NonEmpty (AbstractName, Access) -> NonEmpty (Maybe Induction)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (KindOfName -> Maybe Induction
isConName (KindOfName -> Maybe Induction)
-> ((AbstractName, Access) -> KindOfName)
-> (AbstractName, Access)
-> Maybe Induction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> KindOfName
anameKind (AbstractName -> KindOfName)
-> ((AbstractName, Access) -> AbstractName)
-> (AbstractName, Access)
-> KindOfName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractName, Access) -> AbstractName
forall a b. (a, b) -> a
fst) NonEmpty (AbstractName, Access)
ds
                 , (Maybe Induction -> Bool) -> NonEmpty (Maybe Induction) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Maybe Induction -> Bool
forall a. Maybe a -> Bool
isJust NonEmpty (Maybe Induction)
ks
                 , Maybe (Suffix, NonEmpty (AbstractName, Access)) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (Suffix, NonEmpty (AbstractName, Access))
suffixedNames ->
          ResolvedName -> m ResolvedName
forall (m :: * -> *) a. Monad m => a -> m a
return (ResolvedName -> m ResolvedName) -> ResolvedName -> m ResolvedName
forall a b. (a -> b) -> a -> b
$ Set Induction -> List1 AbstractName -> ResolvedName
ConstructorName ([Induction] -> Set Induction
forall a. Ord a => [a] -> Set a
Set.fromList ([Induction] -> Set Induction) -> [Induction] -> Set Induction
forall a b. (a -> b) -> a -> b
$ NonEmpty (Maybe Induction) -> [Induction]
forall a. List1 (Maybe a) -> [a]
List1.catMaybes NonEmpty (Maybe Induction)
ks) (List1 AbstractName -> ResolvedName)
-> List1 AbstractName -> ResolvedName
forall a b. (a -> b) -> a -> b
$ ((AbstractName, Access) -> AbstractName)
-> NonEmpty (AbstractName, Access) -> List1 AbstractName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (AbstractName -> AbstractName
upd (AbstractName -> AbstractName)
-> ((AbstractName, Access) -> AbstractName)
-> (AbstractName, Access)
-> AbstractName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractName, Access) -> AbstractName
forall a b. (a, b) -> a
fst) NonEmpty (AbstractName, Access)
ds

        Just NonEmpty (AbstractName, Access)
ds  | ((AbstractName, Access) -> Bool)
-> NonEmpty (AbstractName, Access) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((KindOfName
FldName KindOfName -> KindOfName -> Bool
forall a. Eq a => a -> a -> Bool
==) (KindOfName -> Bool)
-> ((AbstractName, Access) -> KindOfName)
-> (AbstractName, Access)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> KindOfName
anameKind (AbstractName -> KindOfName)
-> ((AbstractName, Access) -> AbstractName)
-> (AbstractName, Access)
-> KindOfName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractName, Access) -> AbstractName
forall a b. (a, b) -> a
fst) NonEmpty (AbstractName, Access)
ds , Maybe (Suffix, NonEmpty (AbstractName, Access)) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (Suffix, NonEmpty (AbstractName, Access))
suffixedNames ->
          ResolvedName -> m ResolvedName
forall (m :: * -> *) a. Monad m => a -> m a
return (ResolvedName -> m ResolvedName) -> ResolvedName -> m ResolvedName
forall a b. (a -> b) -> a -> b
$ List1 AbstractName -> ResolvedName
FieldName (List1 AbstractName -> ResolvedName)
-> List1 AbstractName -> ResolvedName
forall a b. (a -> b) -> a -> b
$ ((AbstractName, Access) -> AbstractName)
-> NonEmpty (AbstractName, Access) -> List1 AbstractName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (AbstractName -> AbstractName
upd (AbstractName -> AbstractName)
-> ((AbstractName, Access) -> AbstractName)
-> (AbstractName, Access)
-> AbstractName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractName, Access) -> AbstractName
forall a b. (a, b) -> a
fst) NonEmpty (AbstractName, Access)
ds

        Just NonEmpty (AbstractName, Access)
ds  | ((AbstractName, Access) -> Bool)
-> NonEmpty (AbstractName, Access) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((KindOfName
PatternSynName KindOfName -> KindOfName -> Bool
forall a. Eq a => a -> a -> Bool
==) (KindOfName -> Bool)
-> ((AbstractName, Access) -> KindOfName)
-> (AbstractName, Access)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> KindOfName
anameKind (AbstractName -> KindOfName)
-> ((AbstractName, Access) -> AbstractName)
-> (AbstractName, Access)
-> KindOfName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractName, Access) -> AbstractName
forall a b. (a, b) -> a
fst) NonEmpty (AbstractName, Access)
ds , Maybe (Suffix, NonEmpty (AbstractName, Access)) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (Suffix, NonEmpty (AbstractName, Access))
suffixedNames ->
          ResolvedName -> m ResolvedName
forall (m :: * -> *) a. Monad m => a -> m a
return (ResolvedName -> m ResolvedName) -> ResolvedName -> m ResolvedName
forall a b. (a -> b) -> a -> b
$ List1 AbstractName -> ResolvedName
PatternSynResName (List1 AbstractName -> ResolvedName)
-> List1 AbstractName -> ResolvedName
forall a b. (a -> b) -> a -> b
$ ((AbstractName, Access) -> AbstractName)
-> NonEmpty (AbstractName, Access) -> List1 AbstractName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (AbstractName -> AbstractName
upd (AbstractName -> AbstractName)
-> ((AbstractName, Access) -> AbstractName)
-> (AbstractName, Access)
-> AbstractName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractName, Access) -> AbstractName
forall a b. (a, b) -> a
fst) NonEmpty (AbstractName, Access)
ds

        Just ((AbstractName
d, Access
a) :| []) | Maybe (Suffix, NonEmpty (AbstractName, Access)) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (Suffix, NonEmpty (AbstractName, Access))
suffixedNames ->
          ResolvedName -> m ResolvedName
forall (m :: * -> *) a. Monad m => a -> m a
return (ResolvedName -> m ResolvedName) -> ResolvedName -> m ResolvedName
forall a b. (a -> b) -> a -> b
$ Access -> AbstractName -> Suffix -> ResolvedName
DefinedName Access
a (AbstractName -> AbstractName
upd AbstractName
d) Suffix
A.NoSuffix

        Just NonEmpty (AbstractName, Access)
ds -> List1 QName -> m ResolvedName
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (List1 QName -> m ResolvedName) -> List1 QName -> m ResolvedName
forall a b. (a -> b) -> a -> b
$ ((AbstractName, Access) -> QName)
-> NonEmpty (AbstractName, Access) -> List1 QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (AbstractName -> QName
anameName (AbstractName -> QName)
-> ((AbstractName, Access) -> AbstractName)
-> (AbstractName, Access)
-> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractName, Access) -> AbstractName
forall a b. (a, b) -> a
fst) (NonEmpty (AbstractName, Access) -> List1 QName)
-> NonEmpty (AbstractName, Access) -> List1 QName
forall a b. (a -> b) -> a -> b
$ Maybe (Suffix, NonEmpty (AbstractName, Access))
-> (NonEmpty (AbstractName, Access)
    -> NonEmpty (AbstractName, Access))
-> ((Suffix, NonEmpty (AbstractName, Access))
    -> NonEmpty (AbstractName, Access)
    -> NonEmpty (AbstractName, Access))
-> NonEmpty (AbstractName, Access)
-> NonEmpty (AbstractName, Access)
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Suffix, NonEmpty (AbstractName, Access))
suffixedNames NonEmpty (AbstractName, Access) -> NonEmpty (AbstractName, Access)
forall a. a -> a
id (NonEmpty (AbstractName, Access)
-> NonEmpty (AbstractName, Access)
-> NonEmpty (AbstractName, Access)
forall a. Semigroup a => a -> a -> a
(<>) (NonEmpty (AbstractName, Access)
 -> NonEmpty (AbstractName, Access)
 -> NonEmpty (AbstractName, Access))
-> ((Suffix, NonEmpty (AbstractName, Access))
    -> NonEmpty (AbstractName, Access))
-> (Suffix, NonEmpty (AbstractName, Access))
-> NonEmpty (AbstractName, Access)
-> NonEmpty (AbstractName, Access)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Suffix, NonEmpty (AbstractName, Access))
-> NonEmpty (AbstractName, Access)
forall a b. (a, b) -> b
snd) NonEmpty (AbstractName, Access)
ds

        Maybe (NonEmpty (AbstractName, Access))
Nothing -> case Maybe (Suffix, NonEmpty (AbstractName, Access))
suffixedNames of
          Maybe (Suffix, NonEmpty (AbstractName, Access))
Nothing -> ResolvedName -> m ResolvedName
forall (m :: * -> *) a. Monad m => a -> m a
return ResolvedName
UnknownName
          Just (Suffix
suffix , (AbstractName
d, Access
a) :| []) -> ResolvedName -> m ResolvedName
forall (m :: * -> *) a. Monad m => a -> m a
return (ResolvedName -> m ResolvedName) -> ResolvedName -> m ResolvedName
forall a b. (a -> b) -> a -> b
$ Access -> AbstractName -> Suffix -> ResolvedName
DefinedName Access
a (AbstractName -> AbstractName
upd AbstractName
d) Suffix
suffix
          Just (Suffix
suffix , NonEmpty (AbstractName, Access)
sds) -> List1 QName -> m ResolvedName
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (List1 QName -> m ResolvedName) -> List1 QName -> m ResolvedName
forall a b. (a -> b) -> a -> b
$ ((AbstractName, Access) -> QName)
-> NonEmpty (AbstractName, Access) -> List1 QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (AbstractName -> QName
anameName (AbstractName -> QName)
-> ((AbstractName, Access) -> AbstractName)
-> (AbstractName, Access)
-> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractName, Access) -> AbstractName
forall a b. (a, b) -> a
fst) NonEmpty (AbstractName, Access)
sds

  where
  -- @names@ intended semantics: a filter on names.
  -- @Nothing@: don't filter out anything.
  -- @Just ns@: filter by membership in @ns@.
  filterNames :: forall a. (a -> AbstractName) -> [a] -> [a]
  filterNames :: forall a. (a -> AbstractName) -> [a] -> [a]
filterNames = case Maybe (Set Name)
names of
    Maybe (Set Name)
Nothing -> \ a -> AbstractName
f -> [a] -> [a]
forall a. a -> a
id
    Just Set Name
ns -> \ a -> AbstractName
f -> (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter ((a -> Bool) -> [a] -> [a]) -> (a -> Bool) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ (Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Name
ns) (Name -> Bool) -> (a -> Name) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
A.qnameName (QName -> Name) -> (a -> QName) -> a -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> QName
anameName (AbstractName -> QName) -> (a -> AbstractName) -> a -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> AbstractName
f
    -- lambda-dropped style by intention
  upd :: AbstractName -> AbstractName
upd AbstractName
d = AbstractName -> Name -> AbstractName
updateConcreteName AbstractName
d (Name -> AbstractName) -> Name -> AbstractName
forall a b. (a -> b) -> a -> b
$ QName -> Name
unqualify QName
x
  updateConcreteName :: AbstractName -> C.Name -> AbstractName
  updateConcreteName :: AbstractName -> Name -> AbstractName
updateConcreteName d :: AbstractName
d@(AbsName { anameName :: AbstractName -> QName
anameName = A.QName ModuleName
qm Name
qn }) Name
x =
    AbstractName
d { anameName :: QName
anameName = ModuleName -> Name -> QName
A.QName (Range -> ModuleName -> ModuleName
forall a. SetRange a => Range -> a -> a
setRange (Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x) ModuleName
qm) (Name
qn { nameConcrete :: Name
nameConcrete = Name
x }) }
  fromConcreteSuffix :: Maybe Suffix -> Maybe Suffix
fromConcreteSuffix = \case
    Maybe Suffix
Nothing              -> Maybe Suffix
forall a. Maybe a
Nothing
    Just C.Prime{}       -> Maybe Suffix
forall a. Maybe a
Nothing
    Just (C.Index Integer
i)     -> Suffix -> Maybe Suffix
forall a. a -> Maybe a
Just (Suffix -> Maybe Suffix) -> Suffix -> Maybe Suffix
forall a b. (a -> b) -> a -> b
$ Integer -> Suffix
A.Suffix Integer
i
    Just (C.Subscript Integer
i) -> Suffix -> Maybe Suffix
forall a. a -> Maybe a
Just (Suffix -> Maybe Suffix) -> Suffix -> Maybe Suffix
forall a b. (a -> b) -> a -> b
$ Integer -> Suffix
A.Suffix Integer
i

-- | Test if a given abstract name can appear with a suffix. Currently
--   only true for the names of builtin sorts @Set@ and @Prop@.
canHaveSuffixTest :: HasBuiltins m => m (A.QName -> Bool)
canHaveSuffixTest :: forall (m :: * -> *). HasBuiltins m => m (QName -> Bool)
canHaveSuffixTest = do
  Maybe QName
builtinSet  <- [Char] -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getBuiltinName' [Char]
builtinSet
  Maybe QName
builtinProp <- [Char] -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getBuiltinName' [Char]
builtinProp
  Maybe QName
builtinSetOmega <- [Char] -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getBuiltinName' [Char]
builtinSetOmega
  Maybe QName
builtinSSetOmega <- [Char] -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getBuiltinName' [Char]
builtinSSetOmega
  (QName -> Bool) -> m (QName -> Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return ((QName -> Bool) -> m (QName -> Bool))
-> (QName -> Bool) -> m (QName -> Bool)
forall a b. (a -> b) -> a -> b
$ \QName
x -> QName -> Maybe QName
forall a. a -> Maybe a
Just QName
x Maybe QName -> [Maybe QName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Maybe QName
builtinSet, Maybe QName
builtinProp, Maybe QName
builtinSetOmega, Maybe QName
builtinSSetOmega]

-- | Look up a module in the scope.
resolveModule :: C.QName -> ScopeM AbstractModule
resolveModule :: QName -> ScopeM AbstractModule
resolveModule QName
x = do
  [AbstractModule]
ms <- QName -> ScopeInfo -> [AbstractModule]
forall a. InScope a => QName -> ScopeInfo -> [a]
scopeLookup QName
x (ScopeInfo -> [AbstractModule])
-> TCMT IO ScopeInfo -> TCMT IO [AbstractModule]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  Maybe (NonEmpty AbstractModule)
-> ScopeM AbstractModule
-> (NonEmpty AbstractModule -> ScopeM AbstractModule)
-> ScopeM AbstractModule
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe ([AbstractModule] -> Maybe (NonEmpty AbstractModule)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty [AbstractModule]
ms) (TypeError -> ScopeM AbstractModule
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> ScopeM AbstractModule)
-> TypeError -> ScopeM AbstractModule
forall a b. (a -> b) -> a -> b
$ QName -> TypeError
NoSuchModule QName
x) ((NonEmpty AbstractModule -> ScopeM AbstractModule)
 -> ScopeM AbstractModule)
-> (NonEmpty AbstractModule -> ScopeM AbstractModule)
-> ScopeM AbstractModule
forall a b. (a -> b) -> a -> b
$ \ case
    AbsModule ModuleName
m WhyInScope
why :| [] -> AbstractModule -> ScopeM AbstractModule
forall (m :: * -> *) a. Monad m => a -> m a
return (AbstractModule -> ScopeM AbstractModule)
-> AbstractModule -> ScopeM AbstractModule
forall a b. (a -> b) -> a -> b
$ ModuleName -> WhyInScope -> AbstractModule
AbsModule (ModuleName
m ModuleName -> QName -> ModuleName
forall t u. (SetRange t, HasRange u) => t -> u -> t
`withRangeOf` QName
x) WhyInScope
why
    NonEmpty AbstractModule
ms                    -> TypeError -> ScopeM AbstractModule
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> ScopeM AbstractModule)
-> TypeError -> ScopeM AbstractModule
forall a b. (a -> b) -> a -> b
$ QName -> List1 ModuleName -> TypeError
AmbiguousModule QName
x ((AbstractModule -> ModuleName)
-> NonEmpty AbstractModule -> List1 ModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AbstractModule -> ModuleName
amodName NonEmpty AbstractModule
ms)

-- | Get the fixity of a not yet bound name.
getConcreteFixity :: C.Name -> ScopeM Fixity'
getConcreteFixity :: Name -> ScopeM Fixity'
getConcreteFixity Name
x = Fixity' -> Name -> Map Name Fixity' -> Fixity'
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Fixity'
noFixity' Name
x (Map Name Fixity' -> Fixity')
-> TCMT IO (Map Name Fixity') -> ScopeM Fixity'
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' (Map Name Fixity') ScopeInfo -> TCMT IO (Map Name Fixity')
forall (m :: * -> *) a. ReadTCState m => Lens' a ScopeInfo -> m a
useScope Lens' (Map Name Fixity') ScopeInfo
scopeFixities

-- | Get the polarities of a not yet bound name.
getConcretePolarity :: C.Name -> ScopeM (Maybe [Occurrence])
getConcretePolarity :: Name -> ScopeM (Maybe [Occurrence])
getConcretePolarity Name
x = Name -> Map Name [Occurrence] -> Maybe [Occurrence]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x (Map Name [Occurrence] -> Maybe [Occurrence])
-> TCMT IO (Map Name [Occurrence]) -> ScopeM (Maybe [Occurrence])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' (Map Name [Occurrence]) ScopeInfo
-> TCMT IO (Map Name [Occurrence])
forall (m :: * -> *) a. ReadTCState m => Lens' a ScopeInfo -> m a
useScope Lens' (Map Name [Occurrence]) ScopeInfo
scopePolarities

instance MonadFixityError ScopeM where
  throwMultipleFixityDecls :: forall a. [(Name, [Fixity'])] -> ScopeM a
throwMultipleFixityDecls [(Name, [Fixity'])]
xs         = case [(Name, [Fixity'])]
xs of
    (Name
x, [Fixity']
_) : [(Name, [Fixity'])]
_ -> Range -> ScopeM a -> ScopeM a
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x) (ScopeM a -> ScopeM a) -> ScopeM a -> ScopeM a
forall a b. (a -> b) -> a -> b
$ TypeError -> ScopeM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> ScopeM a) -> TypeError -> ScopeM a
forall a b. (a -> b) -> a -> b
$ [(Name, [Fixity'])] -> TypeError
MultipleFixityDecls [(Name, [Fixity'])]
xs
    []         -> ScopeM a
forall a. HasCallStack => a
__IMPOSSIBLE__
  throwMultiplePolarityPragmas :: forall a. [Name] -> ScopeM a
throwMultiplePolarityPragmas [Name]
xs     = case [Name]
xs of
    Name
x : [Name]
_ -> Range -> ScopeM a -> ScopeM a
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x) (ScopeM a -> ScopeM a) -> ScopeM a -> ScopeM a
forall a b. (a -> b) -> a -> b
$ TypeError -> ScopeM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> ScopeM a) -> TypeError -> ScopeM a
forall a b. (a -> b) -> a -> b
$ [Name] -> TypeError
MultiplePolarityPragmas [Name]
xs
    []    -> ScopeM a
forall a. HasCallStack => a
__IMPOSSIBLE__
  warnUnknownNamesInFixityDecl :: HasCallStack => [Name] -> TCMT IO ()
warnUnknownNamesInFixityDecl        = HasCallStack => DeclarationWarning' -> TCMT IO ()
DeclarationWarning' -> TCMT IO ()
scopeWarning (DeclarationWarning' -> TCMT IO ())
-> ([Name] -> DeclarationWarning') -> [Name] -> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> DeclarationWarning'
UnknownNamesInFixityDecl
  warnUnknownNamesInPolarityPragmas :: HasCallStack => [Name] -> TCMT IO ()
warnUnknownNamesInPolarityPragmas   = HasCallStack => DeclarationWarning' -> TCMT IO ()
DeclarationWarning' -> TCMT IO ()
scopeWarning (DeclarationWarning' -> TCMT IO ())
-> ([Name] -> DeclarationWarning') -> [Name] -> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> DeclarationWarning'
UnknownNamesInPolarityPragmas
  warnUnknownFixityInMixfixDecl :: HasCallStack => [Name] -> TCMT IO ()
warnUnknownFixityInMixfixDecl       = HasCallStack => DeclarationWarning' -> TCMT IO ()
DeclarationWarning' -> TCMT IO ()
scopeWarning (DeclarationWarning' -> TCMT IO ())
-> ([Name] -> DeclarationWarning') -> [Name] -> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> DeclarationWarning'
UnknownFixityInMixfixDecl
  warnPolarityPragmasButNotPostulates :: HasCallStack => [Name] -> TCMT IO ()
warnPolarityPragmasButNotPostulates = HasCallStack => DeclarationWarning' -> TCMT IO ()
DeclarationWarning' -> TCMT IO ()
scopeWarning (DeclarationWarning' -> TCMT IO ())
-> ([Name] -> DeclarationWarning') -> [Name] -> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> DeclarationWarning'
PolarityPragmasButNotPostulates

-- | Collect the fixity/syntax declarations and polarity pragmas from the list
--   of declarations and store them in the scope.
computeFixitiesAndPolarities :: DoWarn -> [C.Declaration] -> ScopeM a -> ScopeM a
computeFixitiesAndPolarities :: forall a. DoWarn -> [Declaration] -> ScopeM a -> ScopeM a
computeFixitiesAndPolarities DoWarn
warn [Declaration]
ds ScopeM a
cont = do
  (Map Name Fixity', Map Name [Occurrence])
fp <- DoWarn
-> [Declaration]
-> TCMT IO (Map Name Fixity', Map Name [Occurrence])
forall (m :: * -> *).
MonadFixityError m =>
DoWarn
-> [Declaration] -> m (Map Name Fixity', Map Name [Occurrence])
fixitiesAndPolarities DoWarn
warn [Declaration]
ds
  -- Andreas, 2019-08-16:
  -- Since changing fixities and polarities does not affect the name sets,
  -- we do not need to invoke @modifyScope@ here
  -- (which does @recomputeInverseScopeMaps@).
  -- A simple @locallyScope@ is sufficient.
  Lens' (Map Name Fixity', Map Name [Occurrence]) ScopeInfo
-> ((Map Name Fixity', Map Name [Occurrence])
    -> (Map Name Fixity', Map Name [Occurrence]))
-> ScopeM a
-> ScopeM a
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a ScopeInfo -> (a -> a) -> m b -> m b
locallyScope Lens' (Map Name Fixity', Map Name [Occurrence]) ScopeInfo
scopeFixitiesAndPolarities ((Map Name Fixity', Map Name [Occurrence])
-> (Map Name Fixity', Map Name [Occurrence])
-> (Map Name Fixity', Map Name [Occurrence])
forall a b. a -> b -> a
const (Map Name Fixity', Map Name [Occurrence])
fp) ScopeM a
cont

-- | 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 :: QName -> Set Name -> ScopeM NewNotation
getNotation QName
x Set Name
ns = do
  ResolvedName
r <- KindsOfNames -> Maybe (Set Name) -> QName -> ScopeM ResolvedName
resolveName' KindsOfNames
allKindsOfNames (Set Name -> Maybe (Set Name)
forall a. a -> Maybe a
Just Set Name
ns) QName
x
  case ResolvedName
r of
    VarName Name
y BindingSource
_         -> NewNotation -> ScopeM NewNotation
forall (m :: * -> *) a. Monad m => a -> m a
return (NewNotation -> ScopeM NewNotation)
-> NewNotation -> ScopeM NewNotation
forall a b. (a -> b) -> a -> b
$ QName -> Name -> NewNotation
namesToNotation QName
x Name
y
    DefinedName Access
_ AbstractName
d Suffix
_   -> NewNotation -> ScopeM NewNotation
forall (m :: * -> *) a. Monad m => a -> m a
return (NewNotation -> ScopeM NewNotation)
-> NewNotation -> ScopeM NewNotation
forall a b. (a -> b) -> a -> b
$ AbstractName -> NewNotation
notation AbstractName
d
    FieldName List1 AbstractName
ds        -> NewNotation -> ScopeM NewNotation
forall (m :: * -> *) a. Monad m => a -> m a
return (NewNotation -> ScopeM NewNotation)
-> NewNotation -> ScopeM NewNotation
forall a b. (a -> b) -> a -> b
$ List1 AbstractName -> NewNotation
oneNotation List1 AbstractName
ds
    ConstructorName Set Induction
_ List1 AbstractName
ds-> NewNotation -> ScopeM NewNotation
forall (m :: * -> *) a. Monad m => a -> m a
return (NewNotation -> ScopeM NewNotation)
-> NewNotation -> ScopeM NewNotation
forall a b. (a -> b) -> a -> b
$ List1 AbstractName -> NewNotation
oneNotation List1 AbstractName
ds
    PatternSynResName List1 AbstractName
n -> NewNotation -> ScopeM NewNotation
forall (m :: * -> *) a. Monad m => a -> m a
return (NewNotation -> ScopeM NewNotation)
-> NewNotation -> ScopeM NewNotation
forall a b. (a -> b) -> a -> b
$ List1 AbstractName -> NewNotation
oneNotation List1 AbstractName
n
    ResolvedName
UnknownName         -> ScopeM NewNotation
forall a. HasCallStack => a
__IMPOSSIBLE__
  where
    notation :: AbstractName -> NewNotation
notation = QName -> Name -> NewNotation
namesToNotation QName
x (Name -> NewNotation)
-> (AbstractName -> Name) -> AbstractName -> NewNotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName (QName -> Name) -> (AbstractName -> QName) -> AbstractName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> QName
anameName
    oneNotation :: List1 AbstractName -> NewNotation
oneNotation List1 AbstractName
ds =
      case [NewNotation] -> [NewNotation]
mergeNotations ([NewNotation] -> [NewNotation]) -> [NewNotation] -> [NewNotation]
forall a b. (a -> b) -> a -> b
$ (AbstractName -> NewNotation) -> [AbstractName] -> [NewNotation]
forall a b. (a -> b) -> [a] -> [b]
map AbstractName -> NewNotation
notation ([AbstractName] -> [NewNotation])
-> [AbstractName] -> [NewNotation]
forall a b. (a -> b) -> a -> b
$ List1 AbstractName -> [AbstractName]
forall a. NonEmpty a -> [a]
List1.toList List1 AbstractName
ds of
        [NewNotation
n] -> NewNotation
n
        [NewNotation]
_   -> NewNotation
forall a. HasCallStack => a
__IMPOSSIBLE__

---------------------------------------------------------------------------
-- * Binding names
---------------------------------------------------------------------------

-- | Bind a variable.
bindVariable
  :: A.BindingSource -- ^ @λ@, @Π@, @let@, ...?
  -> C.Name          -- ^ Concrete name.
  -> A.Name          -- ^ Abstract name.
  -> ScopeM ()
bindVariable :: BindingSource -> Name -> Name -> TCMT IO ()
bindVariable BindingSource
b Name
x Name
y = (LocalVars -> LocalVars) -> TCMT IO ()
modifyLocalVars ((LocalVars -> LocalVars) -> TCMT IO ())
-> (LocalVars -> LocalVars) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Name -> LocalVar -> LocalVars -> LocalVars
forall k v. k -> v -> AssocList k v -> AssocList k v
AssocList.insert Name
x (LocalVar -> LocalVars -> LocalVars)
-> LocalVar -> LocalVars -> LocalVars
forall a b. (a -> b) -> a -> b
$ Name -> BindingSource -> [AbstractName] -> LocalVar
LocalVar Name
y BindingSource
b []

-- | Temporarily unbind a variable. Used for non-recursive lets.
unbindVariable :: C.Name -> ScopeM a -> ScopeM a
unbindVariable :: forall a. Name -> ScopeM a -> ScopeM a
unbindVariable Name
x = TCMT IO LocalVars
-> (LocalVars -> TCMT IO ()) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ (TCMT IO LocalVars
forall (m :: * -> *). ReadTCState m => m LocalVars
getLocalVars TCMT IO LocalVars -> TCMT IO () -> TCMT IO LocalVars
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* (LocalVars -> LocalVars) -> TCMT IO ()
modifyLocalVars (Name -> LocalVars -> LocalVars
forall k v. Eq k => k -> AssocList k v -> AssocList k v
AssocList.delete Name
x)) ((LocalVars -> LocalVars) -> TCMT IO ()
modifyLocalVars ((LocalVars -> LocalVars) -> TCMT IO ())
-> (LocalVars -> LocalVars -> LocalVars) -> LocalVars -> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocalVars -> LocalVars -> LocalVars
forall a b. a -> b -> a
const)

-- | Bind a defined name. Must not shadow anything.
bindName :: Access -> KindOfName -> C.Name -> A.QName -> ScopeM ()
bindName :: Access -> KindOfName -> Name -> QName -> TCMT IO ()
bindName Access
acc KindOfName
kind Name
x QName
y = Access -> KindOfName -> NameMetadata -> Name -> QName -> TCMT IO ()
bindName' Access
acc KindOfName
kind NameMetadata
NoMetadata Name
x QName
y

bindName' :: Access -> KindOfName -> NameMetadata -> C.Name -> A.QName -> ScopeM ()
bindName' :: Access -> KindOfName -> NameMetadata -> Name -> QName -> TCMT IO ()
bindName' Access
acc KindOfName
kind NameMetadata
meta Name
x QName
y = TCMT IO (Maybe TypeError)
-> (TypeError -> TCMT IO ()) -> TCMT IO ()
forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (Access
-> KindOfName
-> NameMetadata
-> Name
-> QName
-> TCMT IO (Maybe TypeError)
bindName'' Access
acc KindOfName
kind NameMetadata
meta Name
x QName
y) TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError

-- | Bind a name. Returns the 'TypeError' if exists, but does not throw it.
bindName'' :: Access -> KindOfName -> NameMetadata -> C.Name -> A.QName -> ScopeM (Maybe TypeError)
bindName'' :: Access
-> KindOfName
-> NameMetadata
-> Name
-> QName
-> TCMT IO (Maybe TypeError)
bindName'' Access
acc KindOfName
kind NameMetadata
meta Name
x QName
y = do
  Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ (Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ()
modifyScopes ((Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ())
-> (Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ (Scope -> Scope) -> Map ModuleName Scope -> Map ModuleName Scope
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((Scope -> Scope) -> Map ModuleName Scope -> Map ModuleName Scope)
-> (Scope -> Scope) -> Map ModuleName Scope -> Map ModuleName Scope
forall a b. (a -> b) -> a -> b
$ NameSpaceId -> Name -> Scope -> Scope
removeNameFromScope NameSpaceId
PrivateNS Name
x
  ResolvedName
r  <- QName -> ScopeM ResolvedName
resolveName (Name -> QName
C.QName Name
x)
  let y' :: Either TypeError AbstractName
      y' :: Either TypeError AbstractName
y' = case ResolvedName
r of
        -- Binding an anonymous declaration always succeeds.
        -- In case it's not the first one, we simply remove the one that came before
        ResolvedName
_ | Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x      -> Either TypeError AbstractName
success
        DefinedName Access
_ AbstractName
d Suffix
_   -> QName -> Either TypeError AbstractName
clash (QName -> Either TypeError AbstractName)
-> QName -> Either TypeError AbstractName
forall a b. (a -> b) -> a -> b
$ AbstractName -> QName
anameName AbstractName
d
        VarName Name
z BindingSource
_         -> QName -> Either TypeError AbstractName
clash (QName -> Either TypeError AbstractName)
-> QName -> Either TypeError AbstractName
forall a b. (a -> b) -> a -> b
$ Name -> QName
A.qualify_ Name
z
        FieldName       List1 AbstractName
ds  -> (KindOfName -> Bool)
-> List1 AbstractName -> Either TypeError AbstractName
ambiguous (KindOfName -> KindOfName -> Bool
forall a. Eq a => a -> a -> Bool
== KindOfName
FldName) List1 AbstractName
ds
        ConstructorName Set Induction
i List1 AbstractName
ds-> (KindOfName -> Bool)
-> List1 AbstractName -> Either TypeError AbstractName
ambiguous (Maybe Induction -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Induction -> Bool)
-> (KindOfName -> Maybe Induction) -> KindOfName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KindOfName -> Maybe Induction
isConName) List1 AbstractName
ds
        PatternSynResName List1 AbstractName
n -> (KindOfName -> Bool)
-> List1 AbstractName -> Either TypeError AbstractName
ambiguous (KindOfName -> KindOfName -> Bool
forall a. Eq a => a -> a -> Bool
== KindOfName
PatternSynName) List1 AbstractName
n
        ResolvedName
UnknownName         -> Either TypeError AbstractName
success
  let ns :: NameSpaceId
ns = if Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x then NameSpaceId
PrivateNS else Access -> NameSpaceId
localNameSpace Access
acc
  (AbstractName -> TCMT IO ())
-> Either TypeError AbstractName -> TCMT IO ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ ((Scope -> Scope) -> TCMT IO ()
modifyCurrentScope ((Scope -> Scope) -> TCMT IO ())
-> (AbstractName -> Scope -> Scope) -> AbstractName -> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NameSpaceId -> Name -> AbstractName -> Scope -> Scope
addNameToScope NameSpaceId
ns Name
x) Either TypeError AbstractName
y'
  Maybe TypeError -> TCMT IO (Maybe TypeError)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe TypeError -> TCMT IO (Maybe TypeError))
-> Maybe TypeError -> TCMT IO (Maybe TypeError)
forall a b. (a -> b) -> a -> b
$ (TypeError -> Maybe TypeError)
-> (AbstractName -> Maybe TypeError)
-> Either TypeError AbstractName
-> Maybe TypeError
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either TypeError -> Maybe TypeError
forall a. a -> Maybe a
Just (Maybe TypeError -> AbstractName -> Maybe TypeError
forall a b. a -> b -> a
const Maybe TypeError
forall a. Maybe a
Nothing) Either TypeError AbstractName
y'
  where
    success :: Either TypeError AbstractName
success = AbstractName -> Either TypeError AbstractName
forall a b. b -> Either a b
Right (AbstractName -> Either TypeError AbstractName)
-> AbstractName -> Either TypeError AbstractName
forall a b. (a -> b) -> a -> b
$ QName -> KindOfName -> WhyInScope -> NameMetadata -> AbstractName
AbsName QName
y KindOfName
kind WhyInScope
Defined NameMetadata
meta
    clash :: QName -> Either TypeError AbstractName
clash QName
n = TypeError -> Either TypeError AbstractName
forall a b. a -> Either a b
Left (TypeError -> Either TypeError AbstractName)
-> TypeError -> Either TypeError AbstractName
forall a b. (a -> b) -> a -> b
$ QName -> QName -> Maybe NiceDeclaration -> TypeError
ClashingDefinition (Name -> QName
C.QName Name
x) QName
n Maybe NiceDeclaration
forall a. Maybe a
Nothing

    ambiguous :: (KindOfName -> Bool)
-> List1 AbstractName -> Either TypeError AbstractName
ambiguous KindOfName -> Bool
f List1 AbstractName
ds =
      if KindOfName -> Bool
f KindOfName
kind Bool -> Bool -> Bool
&& (AbstractName -> Bool) -> List1 AbstractName -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (KindOfName -> Bool
f (KindOfName -> Bool)
-> (AbstractName -> KindOfName) -> AbstractName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> KindOfName
anameKind) List1 AbstractName
ds
      then Either TypeError AbstractName
success else QName -> Either TypeError AbstractName
clash (QName -> Either TypeError AbstractName)
-> QName -> Either TypeError AbstractName
forall a b. (a -> b) -> a -> b
$ AbstractName -> QName
anameName (List1 AbstractName -> AbstractName
forall a. NonEmpty a -> a
List1.head List1 AbstractName
ds)

-- | Rebind a name. Use with care!
--   Ulf, 2014-06-29: Currently used to rebind the name defined by an
--   unquoteDecl, which is a 'QuotableName' in the body, but a 'DefinedName'
--   later on.
rebindName :: Access -> KindOfName -> C.Name -> A.QName -> ScopeM ()
rebindName :: Access -> KindOfName -> Name -> QName -> TCMT IO ()
rebindName Access
acc KindOfName
kind Name
x QName
y = do
  (Scope -> Scope) -> TCMT IO ()
modifyCurrentScope ((Scope -> Scope) -> TCMT IO ()) -> (Scope -> Scope) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ NameSpaceId -> Name -> Scope -> Scope
removeNameFromScope (Access -> NameSpaceId
localNameSpace Access
acc) Name
x
  Access -> KindOfName -> Name -> QName -> TCMT IO ()
bindName Access
acc KindOfName
kind Name
x QName
y

-- | Bind a module name.
bindModule :: Access -> C.Name -> A.ModuleName -> ScopeM ()
bindModule :: Access -> Name -> ModuleName -> TCMT IO ()
bindModule Access
acc Name
x ModuleName
m = (Scope -> Scope) -> TCMT IO ()
modifyCurrentScope ((Scope -> Scope) -> TCMT IO ()) -> (Scope -> Scope) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
  NameSpaceId -> Name -> AbstractModule -> Scope -> Scope
addModuleToScope (Access -> NameSpaceId
localNameSpace Access
acc) Name
x (ModuleName -> WhyInScope -> AbstractModule
AbsModule ModuleName
m WhyInScope
Defined)

-- | Bind a qualified module name. Adds it to the imports field of the scope.
bindQModule :: Access -> C.QName -> A.ModuleName -> ScopeM ()
bindQModule :: Access -> QName -> ModuleName -> TCMT IO ()
bindQModule Access
acc QName
q ModuleName
m = (Scope -> Scope) -> TCMT IO ()
modifyCurrentScope ((Scope -> Scope) -> TCMT IO ()) -> (Scope -> Scope) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ \Scope
s ->
  Scope
s { scopeImports :: Map QName ModuleName
scopeImports = QName -> ModuleName -> Map QName ModuleName -> Map QName ModuleName
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert QName
q ModuleName
m (Scope -> Map QName ModuleName
scopeImports Scope
s) }

---------------------------------------------------------------------------
-- * Module manipulation operations
---------------------------------------------------------------------------

-- | Clear the scope of any no names.
stripNoNames :: ScopeM ()
stripNoNames :: TCMT IO ()
stripNoNames = (Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ()
modifyScopes ((Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ())
-> (Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ (Scope -> Scope) -> Map ModuleName Scope -> Map ModuleName Scope
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((Scope -> Scope) -> Map ModuleName Scope -> Map ModuleName Scope)
-> (Scope -> Scope) -> Map ModuleName Scope -> Map ModuleName Scope
forall a b. (a -> b) -> a -> b
$ (NamesInScope -> NamesInScope)
-> (ModulesInScope -> ModulesInScope)
-> (InScopeSet -> InScopeSet)
-> Scope
-> Scope
mapScope_ NamesInScope -> NamesInScope
forall {a}. Map Name a -> Map Name a
stripN ModulesInScope -> ModulesInScope
forall {a}. Map Name a -> Map Name a
stripN InScopeSet -> InScopeSet
forall a. a -> a
id
  where
    stripN :: Map Name a -> Map Name a
stripN = (Name -> a -> Bool) -> Map Name a -> Map Name a
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey ((Name -> a -> Bool) -> Map Name a -> Map Name a)
-> (Name -> a -> Bool) -> Map Name a -> Map Name a
forall a b. (a -> b) -> a -> b
$ Bool -> a -> Bool
forall a b. a -> b -> a
const (Bool -> a -> Bool) -> (Name -> Bool) -> Name -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not (Bool -> Bool) -> (Name -> Bool) -> Name -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName

type WSM = StateT ScopeMemo ScopeM

data ScopeMemo = ScopeMemo
  { ScopeMemo -> Ren QName
memoNames   :: A.Ren A.QName
  , ScopeMemo -> Map ModuleName (ModuleName, Bool)
memoModules :: Map ModuleName (ModuleName, Bool)
    -- ^ Bool: did we copy recursively? We need to track this because we don't
    --   copy recursively when creating new modules for reexported functions
    --   (issue1985), but we might need to copy recursively later.
  }

memoToScopeInfo :: ScopeMemo -> ScopeCopyInfo
memoToScopeInfo :: ScopeMemo -> ScopeCopyInfo
memoToScopeInfo (ScopeMemo Ren QName
names Map ModuleName (ModuleName, Bool)
mods) =
  ScopeCopyInfo { renNames :: Ren QName
renNames   = Ren QName
names
                , renModules :: Ren ModuleName
renModules = ((ModuleName, Bool) -> List1 ModuleName)
-> Map ModuleName (ModuleName, Bool) -> Ren ModuleName
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (ModuleName -> List1 ModuleName
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ModuleName -> List1 ModuleName)
-> ((ModuleName, Bool) -> ModuleName)
-> (ModuleName, Bool)
-> List1 ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleName, Bool) -> ModuleName
forall a b. (a, b) -> a
fst) Map ModuleName (ModuleName, Bool)
mods }

-- | Create a new scope with the given name from an old scope. Renames
--   public names in the old scope to match the new name and returns the
--   renamings.
copyScope :: C.QName -> A.ModuleName -> Scope -> ScopeM (Scope, ScopeCopyInfo)
copyScope :: QName -> ModuleName -> Scope -> ScopeM (Scope, ScopeCopyInfo)
copyScope QName
oldc ModuleName
new0 Scope
s = ((WhyInScope -> WhyInScope) -> Scope -> Scope
inScopeBecause (QName -> WhyInScope -> WhyInScope
Applied QName
oldc) (Scope -> Scope)
-> (ScopeMemo -> ScopeCopyInfo)
-> (Scope, ScopeMemo)
-> (Scope, ScopeCopyInfo)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** ScopeMemo -> ScopeCopyInfo
memoToScopeInfo) ((Scope, ScopeMemo) -> (Scope, ScopeCopyInfo))
-> TCMT IO (Scope, ScopeMemo) -> ScopeM (Scope, ScopeCopyInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ScopeMemo (TCMT IO) Scope
-> ScopeMemo -> TCMT IO (Scope, ScopeMemo)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (ModuleName -> Scope -> StateT ScopeMemo (TCMT IO) Scope
copy ModuleName
new0 Scope
s) (Ren QName -> Map ModuleName (ModuleName, Bool) -> ScopeMemo
ScopeMemo Ren QName
forall a. Monoid a => a
mempty Map ModuleName (ModuleName, Bool)
forall a. Monoid a => a
mempty)
  where
    copy :: A.ModuleName -> Scope -> WSM Scope
    copy :: ModuleName -> Scope -> StateT ScopeMemo (TCMT IO) Scope
copy ModuleName
new Scope
s = do
      TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO () -> StateT ScopeMemo (TCMT IO) ())
-> TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.copy" Int
20 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Copying scope " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow ModuleName
old [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" to " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow ModuleName
new
      TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO () -> StateT ScopeMemo (TCMT IO) ())
-> TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.copy" Int
50 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Scope -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Scope
s
      Scope
s0 <- ScopeM Scope -> StateT ScopeMemo (TCMT IO) Scope
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ScopeM Scope -> StateT ScopeMemo (TCMT IO) Scope)
-> ScopeM Scope -> StateT ScopeMemo (TCMT IO) Scope
forall a b. (a -> b) -> a -> b
$ ModuleName -> ScopeM Scope
getNamedScope ModuleName
new
      -- Delete private names, then copy names and modules. Recompute inScope
      -- set rather than trying to copy it.
      Scope
s' <- Scope -> Scope
recomputeInScopeSets (Scope -> Scope)
-> StateT ScopeMemo (TCMT IO) Scope
-> StateT ScopeMemo (TCMT IO) Scope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NamesInScope -> StateT ScopeMemo (TCMT IO) NamesInScope)
-> (ModulesInScope -> StateT ScopeMemo (TCMT IO) ModulesInScope)
-> (InScopeSet -> StateT ScopeMemo (TCMT IO) InScopeSet)
-> Scope
-> StateT ScopeMemo (TCMT IO) Scope
forall (m :: * -> *).
Applicative m =>
(NamesInScope -> m NamesInScope)
-> (ModulesInScope -> m ModulesInScope)
-> (InScopeSet -> m InScopeSet)
-> Scope
-> m Scope
mapScopeM_ NamesInScope -> StateT ScopeMemo (TCMT IO) NamesInScope
copyD ModulesInScope -> StateT ScopeMemo (TCMT IO) ModulesInScope
copyM InScopeSet -> StateT ScopeMemo (TCMT IO) InScopeSet
forall (m :: * -> *) a. Monad m => a -> m a
return (NameSpaceId -> NameSpace -> Scope -> Scope
setNameSpace NameSpaceId
PrivateNS NameSpace
emptyNameSpace Scope
s)
      -- Fix name and parent.
      Scope -> StateT ScopeMemo (TCMT IO) Scope
forall (m :: * -> *) a. Monad m => a -> m a
return (Scope -> StateT ScopeMemo (TCMT IO) Scope)
-> Scope -> StateT ScopeMemo (TCMT IO) Scope
forall a b. (a -> b) -> a -> b
$ Scope
s' { scopeName :: ModuleName
scopeName    = Scope -> ModuleName
scopeName Scope
s0
                  , scopeParents :: [ModuleName]
scopeParents = Scope -> [ModuleName]
scopeParents Scope
s0
                  }
      where
        rnew :: Range
rnew = ModuleName -> Range
forall a. HasRange a => a -> Range
getRange ModuleName
new
        new' :: ModuleName
new' = ModuleName -> ModuleName
forall a. KillRange a => KillRangeT a
killRange ModuleName
new
        newL :: [Name]
newL = ModuleName -> [Name]
A.mnameToList ModuleName
new'
        old :: ModuleName
old  = Scope -> ModuleName
scopeName Scope
s

        copyD :: NamesInScope -> WSM NamesInScope
        copyD :: NamesInScope -> StateT ScopeMemo (TCMT IO) NamesInScope
copyD = ([AbstractName] -> StateT ScopeMemo (TCMT IO) [AbstractName])
-> NamesInScope -> StateT ScopeMemo (TCMT IO) NamesInScope
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (([AbstractName] -> StateT ScopeMemo (TCMT IO) [AbstractName])
 -> NamesInScope -> StateT ScopeMemo (TCMT IO) NamesInScope)
-> ([AbstractName] -> StateT ScopeMemo (TCMT IO) [AbstractName])
-> NamesInScope
-> StateT ScopeMemo (TCMT IO) NamesInScope
forall a b. (a -> b) -> a -> b
$ (AbstractName -> StateT ScopeMemo (TCMT IO) AbstractName)
-> [AbstractName] -> StateT ScopeMemo (TCMT IO) [AbstractName]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((AbstractName -> StateT ScopeMemo (TCMT IO) AbstractName)
 -> [AbstractName] -> StateT ScopeMemo (TCMT IO) [AbstractName])
-> (AbstractName -> StateT ScopeMemo (TCMT IO) AbstractName)
-> [AbstractName]
-> StateT ScopeMemo (TCMT IO) [AbstractName]
forall a b. (a -> b) -> a -> b
$ (QName -> WSM QName)
-> AbstractName -> StateT ScopeMemo (TCMT IO) AbstractName
onName QName -> WSM QName
renName

        copyM :: ModulesInScope -> WSM ModulesInScope
        copyM :: ModulesInScope -> StateT ScopeMemo (TCMT IO) ModulesInScope
copyM = ([AbstractModule] -> StateT ScopeMemo (TCMT IO) [AbstractModule])
-> ModulesInScope -> StateT ScopeMemo (TCMT IO) ModulesInScope
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (([AbstractModule] -> StateT ScopeMemo (TCMT IO) [AbstractModule])
 -> ModulesInScope -> StateT ScopeMemo (TCMT IO) ModulesInScope)
-> ([AbstractModule]
    -> StateT ScopeMemo (TCMT IO) [AbstractModule])
-> ModulesInScope
-> StateT ScopeMemo (TCMT IO) ModulesInScope
forall a b. (a -> b) -> a -> b
$ (AbstractModule -> StateT ScopeMemo (TCMT IO) AbstractModule)
-> [AbstractModule] -> StateT ScopeMemo (TCMT IO) [AbstractModule]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((AbstractModule -> StateT ScopeMemo (TCMT IO) AbstractModule)
 -> [AbstractModule] -> StateT ScopeMemo (TCMT IO) [AbstractModule])
-> (AbstractModule -> StateT ScopeMemo (TCMT IO) AbstractModule)
-> [AbstractModule]
-> StateT ScopeMemo (TCMT IO) [AbstractModule]
forall a b. (a -> b) -> a -> b
$ (ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName)
-> AbstractModule -> StateT ScopeMemo (TCMT IO) AbstractModule
Lens' ModuleName AbstractModule
lensAmodName ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
renMod

        onName :: (A.QName -> WSM A.QName) -> AbstractName -> WSM AbstractName
        onName :: (QName -> WSM QName)
-> AbstractName -> StateT ScopeMemo (TCMT IO) AbstractName
onName QName -> WSM QName
f AbstractName
d =
          case AbstractName -> KindOfName
anameKind AbstractName
d of
            KindOfName
PatternSynName -> AbstractName -> StateT ScopeMemo (TCMT IO) AbstractName
forall (m :: * -> *) a. Monad m => a -> m a
return AbstractName
d  -- Pattern synonyms are simply aliased, not renamed
            KindOfName
_ -> (QName -> WSM QName)
-> AbstractName -> StateT ScopeMemo (TCMT IO) AbstractName
Lens' QName AbstractName
lensAnameName QName -> WSM QName
f AbstractName
d

        -- Adding to memo structure.
        addName :: QName -> QName -> m ()
addName QName
x QName
y     = (ScopeMemo -> ScopeMemo) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((ScopeMemo -> ScopeMemo) -> m ())
-> (ScopeMemo -> ScopeMemo) -> m ()
forall a b. (a -> b) -> a -> b
$ \ ScopeMemo
i -> ScopeMemo
i { memoNames :: Ren QName
memoNames   = (List1 QName -> List1 QName -> List1 QName)
-> QName -> List1 QName -> Ren QName -> Ren QName
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith List1 QName -> List1 QName -> List1 QName
forall a. Semigroup a => a -> a -> a
(<>) QName
x (QName -> List1 QName
forall (f :: * -> *) a. Applicative f => a -> f a
pure QName
y) (ScopeMemo -> Ren QName
memoNames ScopeMemo
i) }
        addMod :: ModuleName -> ModuleName -> Bool -> m ()
addMod  ModuleName
x ModuleName
y Bool
rec = (ScopeMemo -> ScopeMemo) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((ScopeMemo -> ScopeMemo) -> m ())
-> (ScopeMemo -> ScopeMemo) -> m ()
forall a b. (a -> b) -> a -> b
$ \ ScopeMemo
i -> ScopeMemo
i { memoModules :: Map ModuleName (ModuleName, Bool)
memoModules = ModuleName
-> (ModuleName, Bool)
-> Map ModuleName (ModuleName, Bool)
-> Map ModuleName (ModuleName, Bool)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ModuleName
x (ModuleName
y, Bool
rec) (ScopeMemo -> Map ModuleName (ModuleName, Bool)
memoModules ScopeMemo
i) }

        -- Querying the memo structure.
        findName :: QName -> m (Maybe (List1 QName))
findName QName
x = (ScopeMemo -> Maybe (List1 QName)) -> m (Maybe (List1 QName))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (QName -> Ren QName -> Maybe (List1 QName)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
x (Ren QName -> Maybe (List1 QName))
-> (ScopeMemo -> Ren QName) -> ScopeMemo -> Maybe (List1 QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeMemo -> Ren QName
memoNames) -- NB:: Defined but not used
        findMod :: ModuleName -> m (Maybe (ModuleName, Bool))
findMod  ModuleName
x = (ScopeMemo -> Maybe (ModuleName, Bool))
-> m (Maybe (ModuleName, Bool))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (ModuleName
-> Map ModuleName (ModuleName, Bool) -> Maybe (ModuleName, Bool)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ModuleName
x (Map ModuleName (ModuleName, Bool) -> Maybe (ModuleName, Bool))
-> (ScopeMemo -> Map ModuleName (ModuleName, Bool))
-> ScopeMemo
-> Maybe (ModuleName, Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeMemo -> Map ModuleName (ModuleName, Bool)
memoModules)

        refresh :: A.Name -> WSM A.Name
        refresh :: Name -> WSM Name
refresh Name
x = do
          NameId
i <- TCMT IO NameId -> StateT ScopeMemo (TCMT IO) NameId
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCMT IO NameId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
          Name -> WSM Name
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> WSM Name) -> Name -> WSM Name
forall a b. (a -> b) -> a -> b
$ Name
x { nameId :: NameId
A.nameId = NameId
i }

        -- Change a binding M.x -> old.M'.y to M.x -> new.M'.y
        renName :: A.QName -> WSM A.QName
        renName :: QName -> WSM QName
renName QName
x = do
          -- Issue 1985: For re-exported names we can't use new' as the
          -- module, since it has the wrong telescope. Example:
          --
          --    module M1 (A : Set) where
          --      module M2 (B : Set) where
          --        postulate X : Set
          --      module M3 (C : Set) where
          --        module M4 (D E : Set) where
          --          open M2 public
          --
          --    module M = M1.M3 A C
          --
          -- Here we can't copy M1.M2.X to M.M4.X since we need
          -- X : (B : Set) → Set, but M.M4 has telescope (D E : Set). Thus, we
          -- would break the invariant that all functions in a module share the
          -- module telescope. Instead we copy M1.M2.X to M.M2.X for a fresh
          -- module M2 that gets the right telescope.
          ModuleName
m <- if QName
x QName -> ModuleName -> Bool
`isInModule` ModuleName
old
                 then ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleName
new'
                 else Bool -> ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
renMod' Bool
False (QName -> ModuleName
qnameModule QName
x)
                          -- Don't copy recursively here, we only know that the
                          -- current name x should be copied.
          -- Generate a fresh name for the target.
          -- Andreas, 2015-08-11 Issue 1619:
          -- Names copied by a module macro should get the module macro's
          -- range as declaration range
          -- (maybe rather the one of the open statement).
          -- For now, we just set their range
          -- to the new module name's one, which fixes issue 1619.
          QName
y <- Range -> QName -> QName
forall a. SetRange a => Range -> a -> a
setRange Range
rnew (QName -> QName) -> (Name -> QName) -> Name -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> Name -> QName
A.qualify ModuleName
m (Name -> QName) -> WSM Name -> WSM QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> WSM Name
refresh (QName -> Name
qnameName QName
x)
          TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO () -> StateT ScopeMemo (TCMT IO) ())
-> TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.copy" Int
50 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  Copying " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" to " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
y
          QName -> QName -> StateT ScopeMemo (TCMT IO) ()
forall {m :: * -> *}.
MonadState ScopeMemo m =>
QName -> QName -> m ()
addName QName
x QName
y
          QName -> WSM QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
y

        -- Change a binding M.x -> old.M'.y to M.x -> new.M'.y
        renMod :: A.ModuleName -> WSM A.ModuleName
        renMod :: ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
renMod = Bool -> ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
renMod' Bool
True

        renMod' :: Bool -> ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
renMod' Bool
rec ModuleName
x = do
          -- Andreas, issue 1607:
          -- If we have already copied this module, return the copy.
          Maybe (ModuleName, Bool)
z <- ModuleName -> StateT ScopeMemo (TCMT IO) (Maybe (ModuleName, Bool))
forall {m :: * -> *}.
MonadState ScopeMemo m =>
ModuleName -> m (Maybe (ModuleName, Bool))
findMod ModuleName
x
          case Maybe (ModuleName, Bool)
z of
            Just (ModuleName
y, Bool
False) | Bool
rec -> ModuleName
y ModuleName
-> StateT ScopeMemo (TCMT IO) ()
-> StateT ScopeMemo (TCMT IO) ModuleName
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ModuleName -> ModuleName -> StateT ScopeMemo (TCMT IO) ()
copyRec ModuleName
x ModuleName
y
            Just (ModuleName
y, Bool
_)           -> ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleName
y
            Maybe (ModuleName, Bool)
Nothing -> do
            -- Ulf (issue 1985): If copying a reexported module we put it at the
            -- top-level, to make sure we don't mess up the invariant that all
            -- (abstract) names M.f share the argument telescope of M.
            let newM :: [Name]
newM = if ModuleName
x ModuleName -> ModuleName -> Bool
`isLtChildModuleOf` ModuleName
old then [Name]
newL else ModuleName -> [Name]
mnameToList ModuleName
new0

            ModuleName
y <- do
               -- Andreas, Jesper, 2015-07-02: Issue 1597
               -- Don't blindly drop a prefix of length of the old qualifier.
               -- If things are imported by open public they do not have the old qualifier
               -- as prefix.  Those need just to be linked, not copied.
               -- return $ A.mnameFromList $ (newL ++) $ drop (size old) $ A.mnameToList x
               -- caseMaybe (stripPrefix (A.mnameToList old) (A.mnameToList x)) (return x) $ \ suffix -> do
               --   return $ A.mnameFromList $ newL ++ suffix
               -- Ulf, 2016-02-22: #1726
               -- We still need to copy modules from 'open public'. Same as in renName.
               Name
y <- Name -> WSM Name
refresh (Name -> WSM Name) -> Name -> WSM Name
forall a b. (a -> b) -> a -> b
$ Name -> [Name] -> Name
forall a. a -> [a] -> a
lastWithDefault Name
forall a. HasCallStack => a
__IMPOSSIBLE__ ([Name] -> Name) -> [Name] -> Name
forall a b. (a -> b) -> a -> b
$ ModuleName -> [Name]
A.mnameToList ModuleName
x
               ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName)
-> ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
forall a b. (a -> b) -> a -> b
$ [Name] -> ModuleName
A.mnameFromList ([Name] -> ModuleName) -> [Name] -> ModuleName
forall a b. (a -> b) -> a -> b
$ [Name]
newM [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name
y]
            -- Andreas, Jesper, 2015-07-02: Issue 1597
            -- Don't copy a module over itself, it will just be emptied of its contents.
            if (ModuleName
x ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleName
y) then ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleName
x else do
            TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO () -> StateT ScopeMemo (TCMT IO) ())
-> TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.copy" Int
50 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  Copying module " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow ModuleName
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" to " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow ModuleName
y
            ModuleName -> ModuleName -> Bool -> StateT ScopeMemo (TCMT IO) ()
forall {m :: * -> *}.
MonadState ScopeMemo m =>
ModuleName -> ModuleName -> Bool -> m ()
addMod ModuleName
x ModuleName
y Bool
rec
            TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO () -> StateT ScopeMemo (TCMT IO) ())
-> TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Maybe DataOrRecordModule -> ModuleName -> TCMT IO ()
createModule Maybe DataOrRecordModule
forall a. Maybe a
Nothing ModuleName
y
            -- We need to copy the contents of included modules recursively (only when 'rec')
            Bool
-> StateT ScopeMemo (TCMT IO) () -> StateT ScopeMemo (TCMT IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
rec (StateT ScopeMemo (TCMT IO) () -> StateT ScopeMemo (TCMT IO) ())
-> StateT ScopeMemo (TCMT IO) () -> StateT ScopeMemo (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ ModuleName -> ModuleName -> StateT ScopeMemo (TCMT IO) ()
copyRec ModuleName
x ModuleName
y
            ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleName
y
          where
            copyRec :: ModuleName -> ModuleName -> StateT ScopeMemo (TCMT IO) ()
copyRec ModuleName
x ModuleName
y = do
              Scope
s0 <- ScopeM Scope -> StateT ScopeMemo (TCMT IO) Scope
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ScopeM Scope -> StateT ScopeMemo (TCMT IO) Scope)
-> ScopeM Scope -> StateT ScopeMemo (TCMT IO) Scope
forall a b. (a -> b) -> a -> b
$ ModuleName -> ScopeM Scope
getNamedScope ModuleName
x
              Scope
s  <- ModuleName
-> StateT ScopeMemo (TCMT IO) Scope
-> StateT ScopeMemo (TCMT IO) Scope
forall (t :: (* -> *) -> * -> *) a.
(MonadTrans t, Monad (t (TCMT IO))) =>
ModuleName -> t (TCMT IO) a -> t (TCMT IO) a
withCurrentModule' ModuleName
y (StateT ScopeMemo (TCMT IO) Scope
 -> StateT ScopeMemo (TCMT IO) Scope)
-> StateT ScopeMemo (TCMT IO) Scope
-> StateT ScopeMemo (TCMT IO) Scope
forall a b. (a -> b) -> a -> b
$ ModuleName -> Scope -> StateT ScopeMemo (TCMT IO) Scope
copy ModuleName
y Scope
s0
              TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO () -> StateT ScopeMemo (TCMT IO) ())
-> TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ ModuleName -> (Scope -> Scope) -> TCMT IO ()
modifyNamedScope ModuleName
y (Scope -> Scope -> Scope
forall a b. a -> b -> a
const Scope
s)

---------------------------------------------------------------------------
-- * Import directives
---------------------------------------------------------------------------

-- | Warn about useless fixity declarations in @renaming@ directives.
--   Monadic for the sake of error reporting.
checkNoFixityInRenamingModule :: [C.Renaming] -> ScopeM ()
checkNoFixityInRenamingModule :: [Renaming] -> TCMT IO ()
checkNoFixityInRenamingModule [Renaming]
ren = do
  Maybe (NonEmpty Range)
-> (NonEmpty Range -> TCMT IO ()) -> TCMT IO ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust ([Range] -> Maybe (NonEmpty Range)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty ([Range] -> Maybe (NonEmpty Range))
-> [Range] -> Maybe (NonEmpty Range)
forall a b. (a -> b) -> a -> b
$ (Renaming -> Maybe Range) -> [Renaming] -> [Range]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Renaming -> Maybe Range
rangeOfUselessInfix [Renaming]
ren) ((NonEmpty Range -> TCMT IO ()) -> TCMT IO ())
-> (NonEmpty Range -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ \ NonEmpty Range
rs -> do
    NonEmpty Range -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange NonEmpty Range
rs (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
      Warning -> TCMT IO ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCMT IO ()) -> Warning -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ NonEmpty Range -> Warning
FixityInRenamingModule NonEmpty Range
rs
  where
  rangeOfUselessInfix :: C.Renaming -> Maybe Range
  rangeOfUselessInfix :: Renaming -> Maybe Range
rangeOfUselessInfix = \case
    Renaming ImportedModule{} ImportedName
_ Maybe Fixity
mfx Range
_ -> Fixity -> Range
forall a. HasRange a => a -> Range
getRange (Fixity -> Range) -> Maybe Fixity -> Maybe Range
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Fixity
mfx
    Renaming
_ -> Maybe Range
forall a. Maybe a
Nothing

-- Moved here carefully from Parser.y to preserve the archaeological artefact
-- dating from Oct 2005 (5ba14b647b9bd175733f9563e744176425c39126).
-- | Check that an import directive doesn't contain repeated names.
verifyImportDirective :: [C.ImportedName] -> C.HidingDirective -> C.RenamingDirective -> ScopeM ()
verifyImportDirective :: [ImportedName] -> [ImportedName] -> [Renaming] -> TCMT IO ()
verifyImportDirective [ImportedName]
usn [ImportedName]
hdn [Renaming]
ren =
    case ([ImportedName] -> Bool) -> [[ImportedName]] -> [[ImportedName]]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>Int
1) (Int -> Bool) -> ([ImportedName] -> Int) -> [ImportedName] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ImportedName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length)
         ([[ImportedName]] -> [[ImportedName]])
-> [[ImportedName]] -> [[ImportedName]]
forall a b. (a -> b) -> a -> b
$ [ImportedName] -> [[ImportedName]]
forall a. Eq a => [a] -> [[a]]
List.group
         ([ImportedName] -> [[ImportedName]])
-> [ImportedName] -> [[ImportedName]]
forall a b. (a -> b) -> a -> b
$ [ImportedName] -> [ImportedName]
forall a. Ord a => [a] -> [a]
List.sort [ImportedName]
xs
    of
        []  -> () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        [[ImportedName]]
yss -> [[ImportedName]] -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange [[ImportedName]]
yss (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
                [Char]
"Repeated name" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" in import directive: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
List.intersperse [Char]
", " ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ ([ImportedName] -> [Char]) -> [[ImportedName]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (ImportedName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (ImportedName -> [Char])
-> ([ImportedName] -> ImportedName) -> [ImportedName] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ImportedName] -> ImportedName
forall a. [a] -> a
head) [[ImportedName]]
yss)
            where
                s :: [Char]
s = case [[ImportedName]]
yss of
                        [[ImportedName]
_] -> [Char]
""
                        [[ImportedName]]
_   -> [Char]
"s"
    where
        xs :: [ImportedName]
xs = [ImportedName]
usn [ImportedName] -> [ImportedName] -> [ImportedName]
forall a. [a] -> [a] -> [a]
++ [ImportedName]
hdn [ImportedName] -> [ImportedName] -> [ImportedName]
forall a. [a] -> [a] -> [a]
++ (Renaming -> ImportedName) -> [Renaming] -> [ImportedName]
forall a b. (a -> b) -> [a] -> [b]
map Renaming -> ImportedName
forall n m. Renaming' n m -> ImportedName' n m
renFrom [Renaming]
ren

-- | Apply an import directive and check that all the names mentioned actually
--   exist.
--
--   Monadic for the sake of error reporting.
applyImportDirectiveM
  :: C.QName                           -- ^ Name of the scope, only for error reporting.
  -> C.ImportDirective                 -- ^ Description of how scope is to be modified.
  -> Scope                             -- ^ Input scope.
  -> ScopeM (A.ImportDirective, Scope) -- ^ Scope-checked description, output scope.
applyImportDirectiveM :: QName
-> ImportDirective -> Scope -> ScopeM (ImportDirective, Scope)
applyImportDirectiveM QName
m (ImportDirective Range
rng Using' Name Name
usn' [ImportedName]
hdn' [Renaming]
ren' Maybe Range
public) Scope
scope0 = do

    -- Module names do not come with fixities, thus, we should complain if the
    -- user has supplied fixity annotations to @renaming module@ clauses.
    [Renaming] -> TCMT IO ()
checkNoFixityInRenamingModule [Renaming]
ren'

    -- Andreas, 2020-06-06, issue #4707
    -- Duplicates in @using@ directive are dropped with a warning.
    [ImportedName]
usingList <- Using' Name Name -> ScopeM [ImportedName]
discardDuplicatesInUsing Using' Name Name
usn'

    -- The following check was originally performed by the parser.
    -- The Great Ulf Himself added the check back in the dawn of time
    -- (5ba14b647b9bd175733f9563e744176425c39126)
    -- when Agda 2 wasn't even believed to exist yet.
    [ImportedName] -> [ImportedName] -> [Renaming] -> TCMT IO ()
verifyImportDirective [ImportedName]
usingList [ImportedName]
hdn' [Renaming]
ren'

    -- We start by checking that all of the names talked about in the import
    -- directive do exist.  If some do not then we remove them and raise a warning.
    let ([ImportedName]
missingExports, [ImportedName' (Name, QName) (Name, ModuleName)]
namesA) = [ImportedName]
-> ([ImportedName],
    [ImportedName' (Name, QName) (Name, ModuleName)])
checkExist ([ImportedName]
 -> ([ImportedName],
     [ImportedName' (Name, QName) (Name, ModuleName)]))
-> [ImportedName]
-> ([ImportedName],
    [ImportedName' (Name, QName) (Name, ModuleName)])
forall a b. (a -> b) -> a -> b
$ [ImportedName]
usingList [ImportedName] -> [ImportedName] -> [ImportedName]
forall a. [a] -> [a] -> [a]
++ [ImportedName]
hdn' [ImportedName] -> [ImportedName] -> [ImportedName]
forall a. [a] -> [a] -> [a]
++ (Renaming -> ImportedName) -> [Renaming] -> [ImportedName]
forall a b. (a -> b) -> [a] -> [b]
map Renaming -> ImportedName
forall n m. Renaming' n m -> ImportedName' n m
renFrom [Renaming]
ren'
    Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([ImportedName] -> Bool
forall a. Null a => a -> Bool
null [ImportedName]
missingExports) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Range -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range
rng (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
      [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.import.apply" Int
20 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"non existing names: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [ImportedName] -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow [ImportedName]
missingExports
      Warning -> TCMT IO ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCMT IO ()) -> Warning -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ QName -> [Name] -> [Name] -> [ImportedName] -> Warning
ModuleDoesntExport QName
m (NamesInScope -> [Name]
forall k a. Map k a -> [k]
Map.keys NamesInScope
namesInScope) (ModulesInScope -> [Name]
forall k a. Map k a -> [k]
Map.keys ModulesInScope
modulesInScope) [ImportedName]
missingExports

    -- We can now define a cleaned-up version of the import directive.
    let notMissing :: ImportedName -> Bool
notMissing = Bool -> Bool
not (Bool -> Bool) -> (ImportedName -> Bool) -> ImportedName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([ImportedName]
missingExports [ImportedName] -> ImportedName -> Bool
forall a. Ord a => [a] -> a -> Bool
`hasElem`)  -- #3997, efficient lookup in missingExports
    let usn :: [ImportedName]
usn = (ImportedName -> Bool) -> [ImportedName] -> [ImportedName]
forall a. (a -> Bool) -> [a] -> [a]
filter ImportedName -> Bool
notMissing [ImportedName]
usingList        -- remove missingExports from usn'
    let hdn :: [ImportedName]
hdn = (ImportedName -> Bool) -> [ImportedName] -> [ImportedName]
forall a. (a -> Bool) -> [a] -> [a]
filter ImportedName -> Bool
notMissing [ImportedName]
hdn'             -- remove missingExports from hdn'
    let ren :: [Renaming]
ren = (Renaming -> Bool) -> [Renaming] -> [Renaming]
forall a. (a -> Bool) -> [a] -> [a]
filter (ImportedName -> Bool
notMissing (ImportedName -> Bool)
-> (Renaming -> ImportedName) -> Renaming -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Renaming -> ImportedName
forall n m. Renaming' n m -> ImportedName' n m
renFrom) [Renaming]
ren'                   -- and from ren'
    let dir :: ImportDirective
dir = Range
-> Using' Name Name
-> [ImportedName]
-> [Renaming]
-> Maybe Range
-> ImportDirective
forall n m.
Range
-> Using' n m
-> HidingDirective' n m
-> RenamingDirective' n m
-> Maybe Range
-> ImportDirective' n m
ImportDirective Range
rng (([ImportedName] -> [ImportedName])
-> Using' Name Name -> Using' Name Name
forall n1 m1 n2 m2.
([ImportedName' n1 m1] -> [ImportedName' n2 m2])
-> Using' n1 m1 -> Using' n2 m2
mapUsing ([ImportedName] -> [ImportedName] -> [ImportedName]
forall a b. a -> b -> a
const [ImportedName]
usn) Using' Name Name
usn') [ImportedName]
hdn [Renaming]
ren Maybe Range
public

    -- Convenient shorthands for defined names and names brought into scope:
    let names :: [ImportedName]
names        = (Renaming -> ImportedName) -> [Renaming] -> [ImportedName]
forall a b. (a -> b) -> [a] -> [b]
map Renaming -> ImportedName
forall n m. Renaming' n m -> ImportedName' n m
renFrom [Renaming]
ren [ImportedName] -> [ImportedName] -> [ImportedName]
forall a. [a] -> [a] -> [a]
++ [ImportedName]
hdn [ImportedName] -> [ImportedName] -> [ImportedName]
forall a. [a] -> [a] -> [a]
++ [ImportedName]
usn
    let definedNames :: [ImportedName]
definedNames = (Renaming -> ImportedName) -> [Renaming] -> [ImportedName]
forall a b. (a -> b) -> [a] -> [b]
map Renaming -> ImportedName
forall n m. Renaming' n m -> ImportedName' n m
renTo [Renaming]
ren
    let targetNames :: [ImportedName]
targetNames  = [ImportedName]
usn [ImportedName] -> [ImportedName] -> [ImportedName]
forall a. [a] -> [a] -> [a]
++ [ImportedName]
definedNames

    -- Efficient test of (`elem` names):
    let inNames :: ImportedName -> Bool
inNames      = ([ImportedName]
names [ImportedName] -> ImportedName -> Bool
forall a. Ord a => [a] -> a -> Bool
`hasElem`)

    -- Efficient test of whether a module import should be added to the import
    -- of a definition (like a data or record definition).
    let extra :: Name -> Bool
extra Name
x = ImportedName -> Bool
inNames (Name -> ImportedName
forall n m. n -> ImportedName' n m
ImportedName   Name
x)
               Bool -> Bool -> Bool
&& ImportedName -> Bool
notMissing (Name -> ImportedName
forall n m. m -> ImportedName' n m
ImportedModule Name
x)
               Bool -> Bool -> Bool
&& (Bool -> Bool
not (Bool -> Bool) -> (ImportedName -> Bool) -> ImportedName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ImportedName -> Bool
inNames (ImportedName -> Bool) -> ImportedName -> Bool
forall a b. (a -> b) -> a -> b
$ Name -> ImportedName
forall n m. m -> ImportedName' n m
ImportedModule Name
x)
                  -- The last test implies that @hiding (module M)@ prevents @module M@
                  -- from entering the @using@ list in @addExtraModule@.

    ImportDirective
dir' <- (ImportedName -> Bool)
-> ImportDirective -> TCMT IO ImportDirective
forall {m :: * -> *} {m}.
MonadWarning m =>
(ImportedName' Name m -> Bool)
-> ImportDirective -> m ImportDirective
sanityCheck (Bool -> Bool
not (Bool -> Bool) -> (ImportedName -> Bool) -> ImportedName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ImportedName -> Bool
inNames) (ImportDirective -> TCMT IO ImportDirective)
-> ImportDirective -> TCMT IO ImportDirective
forall a b. (a -> b) -> a -> b
$ (Name -> Bool) -> ImportDirective -> ImportDirective
addExtraModules Name -> Bool
extra ImportDirective
dir

    -- Check for duplicate imports in a single import directive.
    -- @dup@ : To be imported names that are mentioned more than once.
    [ImportedName] -> ([ImportedName] -> TCMT IO ()) -> TCMT IO ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull ([ImportedName] -> [ImportedName]
forall a. Ord a => [a] -> [a]
allDuplicates [ImportedName]
targetNames) (([ImportedName] -> TCMT IO ()) -> TCMT IO ())
-> ([ImportedName] -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ \ [ImportedName]
dup ->
      TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ QName -> [ImportedName] -> TypeError
DuplicateImports QName
m [ImportedName]
dup

    -- Apply the import directive.
    let (Scope
scope', (Set Name
nameClashes, Set Name
moduleClashes)) = ImportDirective -> Scope -> (Scope, (Set Name, Set Name))
applyImportDirective_ ImportDirective
dir' Scope
scope

    -- Andreas, 2019-11-08, issue #4154, report clashes
    -- introduced by the @renaming@.
    Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set Name -> Bool
forall a. Null a => a -> Bool
null Set Name
nameClashes) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
      Warning -> TCMT IO ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCMT IO ()) -> Warning -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ NameOrModule -> [Name] -> Warning
ClashesViaRenaming NameOrModule
NameNotModule ([Name] -> Warning) -> [Name] -> Warning
forall a b. (a -> b) -> a -> b
$ Set Name -> [Name]
forall a. Set a -> [a]
Set.toList Set Name
nameClashes
    Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set Name -> Bool
forall a. Null a => a -> Bool
null Set Name
moduleClashes) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
      Warning -> TCMT IO ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCMT IO ()) -> Warning -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ NameOrModule -> [Name] -> Warning
ClashesViaRenaming NameOrModule
ModuleNotName ([Name] -> Warning) -> [Name] -> Warning
forall a b. (a -> b) -> a -> b
$ Set Name -> [Name]
forall a. Set a -> [a]
Set.toList Set Name
moduleClashes

    -- Look up the defined names in the new scope.
    let namesInScope' :: NamesInScope
namesInScope'   = (Scope -> NamesInScope
forall a. InScope a => Scope -> ThingsInScope a
allNamesInScope Scope
scope' :: ThingsInScope AbstractName)
    let modulesInScope' :: ModulesInScope
modulesInScope' = (Scope -> ModulesInScope
forall a. InScope a => Scope -> ThingsInScope a
allNamesInScope Scope
scope' :: ThingsInScope AbstractModule)
    let look :: k -> Map k [c] -> c
look k
x = c -> [c] -> c
forall a. a -> [a] -> a
headWithDefault c
forall a. HasCallStack => a
__IMPOSSIBLE__ ([c] -> c) -> (Map k [c] -> [c]) -> Map k [c] -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [c] -> k -> Map k [c] -> [c]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [c]
forall a. HasCallStack => a
__IMPOSSIBLE__ k
x
    -- We set the ranges to the ranges of the concrete names in order to get
    -- highlighting for the names in the import directive.
    let definedA :: [ImportedName' (Name, QName) (Name, ModuleName)]
definedA = [ImportedName]
-> (ImportedName -> ImportedName' (Name, QName) (Name, ModuleName))
-> [ImportedName' (Name, QName) (Name, ModuleName)]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [ImportedName]
definedNames ((ImportedName -> ImportedName' (Name, QName) (Name, ModuleName))
 -> [ImportedName' (Name, QName) (Name, ModuleName)])
-> (ImportedName -> ImportedName' (Name, QName) (Name, ModuleName))
-> [ImportedName' (Name, QName) (Name, ModuleName)]
forall a b. (a -> b) -> a -> b
$ \case
          ImportedName   Name
x -> (Name, QName) -> ImportedName' (Name, QName) (Name, ModuleName)
forall n m. n -> ImportedName' n m
ImportedName   ((Name, QName) -> ImportedName' (Name, QName) (Name, ModuleName))
-> (AbstractName -> (Name, QName))
-> AbstractName
-> ImportedName' (Name, QName) (Name, ModuleName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name
x,) (QName -> (Name, QName))
-> (AbstractName -> QName) -> AbstractName -> (Name, QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> QName -> QName
forall a. SetRange a => Range -> a -> a
setRange (Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x) (QName -> QName)
-> (AbstractName -> QName) -> AbstractName -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> QName
anameName (AbstractName -> ImportedName' (Name, QName) (Name, ModuleName))
-> AbstractName -> ImportedName' (Name, QName) (Name, ModuleName)
forall a b. (a -> b) -> a -> b
$ Name -> NamesInScope -> AbstractName
forall {k} {c}. Ord k => k -> Map k [c] -> c
look Name
x NamesInScope
namesInScope'
          ImportedModule Name
x -> (Name, ModuleName)
-> ImportedName' (Name, QName) (Name, ModuleName)
forall n m. m -> ImportedName' n m
ImportedModule ((Name, ModuleName)
 -> ImportedName' (Name, QName) (Name, ModuleName))
-> (AbstractModule -> (Name, ModuleName))
-> AbstractModule
-> ImportedName' (Name, QName) (Name, ModuleName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name
x,) (ModuleName -> (Name, ModuleName))
-> (AbstractModule -> ModuleName)
-> AbstractModule
-> (Name, ModuleName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> ModuleName -> ModuleName
forall a. SetRange a => Range -> a -> a
setRange (Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x) (ModuleName -> ModuleName)
-> (AbstractModule -> ModuleName) -> AbstractModule -> ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractModule -> ModuleName
amodName  (AbstractModule -> ImportedName' (Name, QName) (Name, ModuleName))
-> AbstractModule -> ImportedName' (Name, QName) (Name, ModuleName)
forall a b. (a -> b) -> a -> b
$ Name -> ModulesInScope -> AbstractModule
forall {k} {c}. Ord k => k -> Map k [c] -> c
look Name
x ModulesInScope
modulesInScope'

    let adir :: ImportDirective
adir = [ImportedName' (Name, QName) (Name, ModuleName)]
-> [ImportedName' (Name, QName) (Name, ModuleName)]
-> ImportDirective
-> ImportDirective
forall n1 m1 n2 m2.
(Ord n1, Ord m1) =>
[ImportedName' (n1, n2) (m1, m2)]
-> [ImportedName' (n1, n2) (m1, m2)]
-> ImportDirective' n1 m1
-> ImportDirective' n2 m2
mapImportDir [ImportedName' (Name, QName) (Name, ModuleName)]
namesA [ImportedName' (Name, QName) (Name, ModuleName)]
definedA ImportDirective
dir
    (ImportDirective, Scope) -> ScopeM (ImportDirective, Scope)
forall (m :: * -> *) a. Monad m => a -> m a
return (ImportDirective
adir, Scope
scope') -- TODO Issue 1714: adir

  where
    -- Andreas, 2020-06-23, issue #4773, fixing regression in 2.5.1.
    -- Import directive may not mention private things.
    -- ```agda
    --   module M where private X = Set
    --   module N = M using (X)
    -- ```
    -- Further, modules (N) need not copy private things (X) from other
    -- modules (M) ever, since they cannot legally referred to
    -- (neither through qualification (N.X) nor open N).
    -- Thus, we can unconditionally remove private definitions
    -- before we apply the import directive.
    scope :: Scope
scope = Scope -> Scope
restrictPrivate Scope
scope0

    -- Return names in the @using@ directive, discarding duplicates.
    -- Monadic for the sake of throwing warnings.
    discardDuplicatesInUsing :: C.Using -> ScopeM [C.ImportedName]
    discardDuplicatesInUsing :: Using' Name Name -> ScopeM [ImportedName]
discardDuplicatesInUsing = \case
      Using' Name Name
UseEverything -> [ImportedName] -> ScopeM [ImportedName]
forall (m :: * -> *) a. Monad m => a -> m a
return []
      Using  [ImportedName]
xs     -> do
        let ([ImportedName]
ys, [ImportedName]
dups) = (ImportedName -> ImportedName)
-> [ImportedName] -> ([ImportedName], [ImportedName])
forall b a. Ord b => (a -> b) -> [a] -> ([a], [a])
nubAndDuplicatesOn ImportedName -> ImportedName
forall a. a -> a
id [ImportedName]
xs
        [ImportedName] -> (List1 ImportedName -> TCMT IO ()) -> TCMT IO ()
forall m a. Null m => [a] -> (List1 a -> m) -> m
List1.unlessNull [ImportedName]
dups ((List1 ImportedName -> TCMT IO ()) -> TCMT IO ())
-> (List1 ImportedName -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Warning -> TCMT IO ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCMT IO ())
-> (List1 ImportedName -> Warning)
-> List1 ImportedName
-> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 ImportedName -> Warning
DuplicateUsing
        [ImportedName] -> ScopeM [ImportedName]
forall (m :: * -> *) a. Monad m => a -> m a
return [ImportedName]
ys

    -- If both @using@ and @hiding@ directive are present,
    -- the hiding directive may only contain modules whose twins are mentioned.
    -- Monadic for the sake of error reporting.
    sanityCheck :: (ImportedName' Name m -> Bool)
-> ImportDirective -> m ImportDirective
sanityCheck ImportedName' Name m -> Bool
notMentioned = \case
      dir :: ImportDirective
dir@(ImportDirective{ using :: forall n m. ImportDirective' n m -> Using' n m
using = Using{}, hiding :: forall n m. ImportDirective' n m -> HidingDirective' n m
hiding = [ImportedName]
ys }) -> do
          let useless :: ImportedName -> Bool
useless = \case
                ImportedName{}   -> Bool
True
                ImportedModule Name
y -> ImportedName' Name m -> Bool
notMentioned (Name -> ImportedName' Name m
forall n m. n -> ImportedName' n m
ImportedName Name
y)
          [ImportedName] -> ([ImportedName] -> m ()) -> m ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull ((ImportedName -> Bool) -> [ImportedName] -> [ImportedName]
forall a. (a -> Bool) -> [a] -> [a]
filter ImportedName -> Bool
useless [ImportedName]
ys) (([ImportedName] -> m ()) -> m ())
-> ([ImportedName] -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ Warning -> m ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> m ())
-> ([ImportedName] -> Warning) -> [ImportedName] -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ImportedName] -> Warning
UselessHiding
          -- We can empty @hiding@ now, since there is an explicit @using@ directive
          -- and @hiding@ served its purpose to prevent modules to enter the @Using@ list.
          ImportDirective -> m ImportDirective
forall (m :: * -> *) a. Monad m => a -> m a
return ImportDirective
dir{ hiding :: [ImportedName]
hiding = [] }
      ImportDirective
dir -> ImportDirective -> m ImportDirective
forall (m :: * -> *) a. Monad m => a -> m a
return ImportDirective
dir

    addExtraModules :: (C.Name -> Bool) -> C.ImportDirective -> C.ImportDirective
    addExtraModules :: (Name -> Bool) -> ImportDirective -> ImportDirective
addExtraModules Name -> Bool
extra ImportDirective
dir =
      ImportDirective
dir{ using :: Using' Name Name
using       = ([ImportedName] -> [ImportedName])
-> Using' Name Name -> Using' Name Name
forall n1 m1 n2 m2.
([ImportedName' n1 m1] -> [ImportedName' n2 m2])
-> Using' n1 m1 -> Using' n2 m2
mapUsing ((ImportedName -> [ImportedName])
-> [ImportedName] -> [ImportedName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ImportedName -> [ImportedName]
addExtra) (Using' Name Name -> Using' Name Name)
-> Using' Name Name -> Using' Name Name
forall a b. (a -> b) -> a -> b
$ ImportDirective -> Using' Name Name
forall n m. ImportDirective' n m -> Using' n m
using ImportDirective
dir
         , hiding :: [ImportedName]
hiding      = (ImportedName -> [ImportedName])
-> [ImportedName] -> [ImportedName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ImportedName -> [ImportedName]
addExtra            ([ImportedName] -> [ImportedName])
-> [ImportedName] -> [ImportedName]
forall a b. (a -> b) -> a -> b
$ ImportDirective -> [ImportedName]
forall n m. ImportDirective' n m -> HidingDirective' n m
hiding ImportDirective
dir
         , impRenaming :: [Renaming]
impRenaming = (Renaming -> [Renaming]) -> [Renaming] -> [Renaming]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Renaming -> [Renaming]
extraRenaming       ([Renaming] -> [Renaming]) -> [Renaming] -> [Renaming]
forall a b. (a -> b) -> a -> b
$ ImportDirective -> [Renaming]
forall n m. ImportDirective' n m -> RenamingDirective' n m
impRenaming ImportDirective
dir
         }
      where
        addExtra :: ImportedName -> [ImportedName]
addExtra f :: ImportedName
f@(ImportedName Name
y) | Name -> Bool
extra Name
y = [ImportedName
f, Name -> ImportedName
forall n m. m -> ImportedName' n m
ImportedModule Name
y]
        addExtra ImportedName
m = [ImportedName
m]

        extraRenaming :: Renaming -> [Renaming]
extraRenaming = \case
          r :: Renaming
r@(Renaming (ImportedName Name
y) (ImportedName Name
z) Maybe Fixity
_fixity Range
rng) | Name -> Bool
extra Name
y ->
             [ Renaming
r , ImportedName -> ImportedName -> Maybe Fixity -> Range -> Renaming
forall n m.
ImportedName' n m
-> ImportedName' n m -> Maybe Fixity -> Range -> Renaming' n m
Renaming (Name -> ImportedName
forall n m. m -> ImportedName' n m
ImportedModule Name
y) (Name -> ImportedName
forall n m. m -> ImportedName' n m
ImportedModule Name
z) Maybe Fixity
forall a. Maybe a
Nothing Range
rng ]
          Renaming
r -> [Renaming
r]

    -- Names and modules (abstract) in scope before the import.
    namesInScope :: NamesInScope
namesInScope   = (Scope -> NamesInScope
forall a. InScope a => Scope -> ThingsInScope a
allNamesInScope Scope
scope :: ThingsInScope AbstractName)
    modulesInScope :: ModulesInScope
modulesInScope = (Scope -> ModulesInScope
forall a. InScope a => Scope -> ThingsInScope a
allNamesInScope Scope
scope :: ThingsInScope AbstractModule)
    concreteNamesInScope :: [Name]
concreteNamesInScope = (NamesInScope -> [Name]
forall k a. Map k a -> [k]
Map.keys NamesInScope
namesInScope [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ ModulesInScope -> [Name]
forall k a. Map k a -> [k]
Map.keys ModulesInScope
modulesInScope :: [C.Name])

    -- AST versions of the concrete names passed as an argument.
    -- We get back a pair consisting of a list of missing exports first,
    -- and a list of successful imports second.
    checkExist :: [ImportedName] -> ([ImportedName], [ImportedName' (C.Name, A.QName) (C.Name, A.ModuleName)])
    checkExist :: [ImportedName]
-> ([ImportedName],
    [ImportedName' (Name, QName) (Name, ModuleName)])
checkExist [ImportedName]
xs = [Either
   ImportedName (ImportedName' (Name, QName) (Name, ModuleName))]
-> ([ImportedName],
    [ImportedName' (Name, QName) (Name, ModuleName)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either
    ImportedName (ImportedName' (Name, QName) (Name, ModuleName))]
 -> ([ImportedName],
     [ImportedName' (Name, QName) (Name, ModuleName)]))
-> [Either
      ImportedName (ImportedName' (Name, QName) (Name, ModuleName))]
-> ([ImportedName],
    [ImportedName' (Name, QName) (Name, ModuleName)])
forall a b. (a -> b) -> a -> b
$ [ImportedName]
-> (ImportedName
    -> Either
         ImportedName (ImportedName' (Name, QName) (Name, ModuleName)))
-> [Either
      ImportedName (ImportedName' (Name, QName) (Name, ModuleName))]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [ImportedName]
xs ((ImportedName
  -> Either
       ImportedName (ImportedName' (Name, QName) (Name, ModuleName)))
 -> [Either
       ImportedName (ImportedName' (Name, QName) (Name, ModuleName))])
-> (ImportedName
    -> Either
         ImportedName (ImportedName' (Name, QName) (Name, ModuleName)))
-> [Either
      ImportedName (ImportedName' (Name, QName) (Name, ModuleName))]
forall a b. (a -> b) -> a -> b
$ \ ImportedName
name -> case ImportedName
name of
      ImportedName Name
x   -> (Name, QName) -> ImportedName' (Name, QName) (Name, ModuleName)
forall n m. n -> ImportedName' n m
ImportedName   ((Name, QName) -> ImportedName' (Name, QName) (Name, ModuleName))
-> (AbstractName -> (Name, QName))
-> AbstractName
-> ImportedName' (Name, QName) (Name, ModuleName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name
x,) (QName -> (Name, QName))
-> (AbstractName -> QName) -> AbstractName -> (Name, QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> QName -> QName
forall a. SetRange a => Range -> a -> a
setRange (Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x) (QName -> QName)
-> (AbstractName -> QName) -> AbstractName -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> QName
anameName (AbstractName -> ImportedName' (Name, QName) (Name, ModuleName))
-> Either ImportedName AbstractName
-> Either
     ImportedName (ImportedName' (Name, QName) (Name, ModuleName))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ImportedName
-> Name -> NamesInScope -> Either ImportedName AbstractName
forall a err b. Ord a => err -> a -> Map a [b] -> Either err b
resolve ImportedName
name Name
x NamesInScope
namesInScope
      ImportedModule Name
x -> (Name, ModuleName)
-> ImportedName' (Name, QName) (Name, ModuleName)
forall n m. m -> ImportedName' n m
ImportedModule ((Name, ModuleName)
 -> ImportedName' (Name, QName) (Name, ModuleName))
-> (AbstractModule -> (Name, ModuleName))
-> AbstractModule
-> ImportedName' (Name, QName) (Name, ModuleName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name
x,) (ModuleName -> (Name, ModuleName))
-> (AbstractModule -> ModuleName)
-> AbstractModule
-> (Name, ModuleName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> ModuleName -> ModuleName
forall a. SetRange a => Range -> a -> a
setRange (Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x) (ModuleName -> ModuleName)
-> (AbstractModule -> ModuleName) -> AbstractModule -> ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractModule -> ModuleName
amodName  (AbstractModule -> ImportedName' (Name, QName) (Name, ModuleName))
-> Either ImportedName AbstractModule
-> Either
     ImportedName (ImportedName' (Name, QName) (Name, ModuleName))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ImportedName
-> Name -> ModulesInScope -> Either ImportedName AbstractModule
forall a err b. Ord a => err -> a -> Map a [b] -> Either err b
resolve ImportedName
name Name
x ModulesInScope
modulesInScope

      where resolve :: Ord a => err -> a -> Map a [b] -> Either err b
            resolve :: forall a err b. Ord a => err -> a -> Map a [b] -> Either err b
resolve err
err a
x Map a [b]
m = Either err b -> ([b] -> Either err b) -> Maybe [b] -> Either err b
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (err -> Either err b
forall a b. a -> Either a b
Left err
err) (b -> Either err b
forall a b. b -> Either a b
Right (b -> Either err b) -> ([b] -> b) -> [b] -> Either err b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [b] -> b
forall a. [a] -> a
head) (Maybe [b] -> Either err b) -> Maybe [b] -> Either err b
forall a b. (a -> b) -> a -> b
$ a -> Map a [b] -> Maybe [b]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
x Map a [b]
m

-- | Translation of @ImportDirective@.
mapImportDir
  :: (Ord n1, Ord m1)
  => [ImportedName' (n1,n2) (m1,m2)]  -- ^ Translation of imported names.
  -> [ImportedName' (n1,n2) (m1,m2)]  -- ^ Translation of names defined by this import.
  -> ImportDirective' n1 m1
  -> ImportDirective' n2 m2
mapImportDir :: forall n1 m1 n2 m2.
(Ord n1, Ord m1) =>
[ImportedName' (n1, n2) (m1, m2)]
-> [ImportedName' (n1, n2) (m1, m2)]
-> ImportDirective' n1 m1
-> ImportDirective' n2 m2
mapImportDir [ImportedName' (n1, n2) (m1, m2)]
src0 [ImportedName' (n1, n2) (m1, m2)]
tgt0 (ImportDirective Range
r Using' n1 m1
u HidingDirective' n1 m1
h RenamingDirective' n1 m1
ren Maybe Range
open) =
  Range
-> Using' n2 m2
-> HidingDirective' n2 m2
-> RenamingDirective' n2 m2
-> Maybe Range
-> ImportDirective' n2 m2
forall n m.
Range
-> Using' n m
-> HidingDirective' n m
-> RenamingDirective' n m
-> Maybe Range
-> ImportDirective' n m
ImportDirective Range
r
    ((HidingDirective' n1 m1 -> HidingDirective' n2 m2)
-> Using' n1 m1 -> Using' n2 m2
forall n1 m1 n2 m2.
([ImportedName' n1 m1] -> [ImportedName' n2 m2])
-> Using' n1 m1 -> Using' n2 m2
mapUsing ((ImportedName' n1 m1 -> ImportedName' n2 m2)
-> HidingDirective' n1 m1 -> HidingDirective' n2 m2
forall a b. (a -> b) -> [a] -> [b]
map (ImportedNameMap n1 n2 m1 m2
-> ImportedName' n1 m1 -> ImportedName' n2 m2
forall n1 m1 n2 m2.
(Ord n1, Ord m1) =>
ImportedNameMap n1 n2 m1 m2
-> ImportedName' n1 m1 -> ImportedName' n2 m2
lookupImportedName ImportedNameMap n1 n2 m1 m2
src)) Using' n1 m1
u)
    ((ImportedName' n1 m1 -> ImportedName' n2 m2)
-> HidingDirective' n1 m1 -> HidingDirective' n2 m2
forall a b. (a -> b) -> [a] -> [b]
map (ImportedNameMap n1 n2 m1 m2
-> ImportedName' n1 m1 -> ImportedName' n2 m2
forall n1 m1 n2 m2.
(Ord n1, Ord m1) =>
ImportedNameMap n1 n2 m1 m2
-> ImportedName' n1 m1 -> ImportedName' n2 m2
lookupImportedName ImportedNameMap n1 n2 m1 m2
src) HidingDirective' n1 m1
h)
    ((Renaming' n1 m1 -> Renaming' n2 m2)
-> RenamingDirective' n1 m1 -> RenamingDirective' n2 m2
forall a b. (a -> b) -> [a] -> [b]
map (ImportedNameMap n1 n2 m1 m2
-> ImportedNameMap n1 n2 m1 m2
-> Renaming' n1 m1
-> Renaming' n2 m2
forall n1 m1 n2 m2.
(Ord n1, Ord m1) =>
ImportedNameMap n1 n2 m1 m2
-> ImportedNameMap n1 n2 m1 m2
-> Renaming' n1 m1
-> Renaming' n2 m2
mapRenaming ImportedNameMap n1 n2 m1 m2
src ImportedNameMap n1 n2 m1 m2
tgt) RenamingDirective' n1 m1
ren)
    Maybe Range
open
  where
  src :: ImportedNameMap n1 n2 m1 m2
src = [ImportedName' (n1, n2) (m1, m2)] -> ImportedNameMap n1 n2 m1 m2
forall n1 m1 n2 m2.
(Ord n1, Ord m1) =>
[ImportedName' (n1, n2) (m1, m2)] -> ImportedNameMap n1 n2 m1 m2
importedNameMapFromList [ImportedName' (n1, n2) (m1, m2)]
src0
  tgt :: ImportedNameMap n1 n2 m1 m2
tgt = [ImportedName' (n1, n2) (m1, m2)] -> ImportedNameMap n1 n2 m1 m2
forall n1 m1 n2 m2.
(Ord n1, Ord m1) =>
[ImportedName' (n1, n2) (m1, m2)] -> ImportedNameMap n1 n2 m1 m2
importedNameMapFromList [ImportedName' (n1, n2) (m1, m2)]
tgt0

-- | A finite map for @ImportedName@s.

data ImportedNameMap n1 n2 m1 m2 = ImportedNameMap
  { forall n1 n2 m1 m2. ImportedNameMap n1 n2 m1 m2 -> Map n1 n2
inameMap   :: Map n1 n2
  , forall n1 n2 m1 m2. ImportedNameMap n1 n2 m1 m2 -> Map m1 m2
imoduleMap :: Map m1 m2
  }

-- | Create a 'ImportedNameMap'.
importedNameMapFromList
  :: (Ord n1, Ord m1)
  => [ImportedName' (n1,n2) (m1,m2)]
  -> ImportedNameMap n1 n2 m1 m2
importedNameMapFromList :: forall n1 m1 n2 m2.
(Ord n1, Ord m1) =>
[ImportedName' (n1, n2) (m1, m2)] -> ImportedNameMap n1 n2 m1 m2
importedNameMapFromList = (ImportedName' (n1, n2) (m1, m2)
 -> ImportedNameMap n1 n2 m1 m2 -> ImportedNameMap n1 n2 m1 m2)
-> ImportedNameMap n1 n2 m1 m2
-> [ImportedName' (n1, n2) (m1, m2)]
-> ImportedNameMap n1 n2 m1 m2
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((ImportedNameMap n1 n2 m1 m2
 -> ImportedName' (n1, n2) (m1, m2) -> ImportedNameMap n1 n2 m1 m2)
-> ImportedName' (n1, n2) (m1, m2)
-> ImportedNameMap n1 n2 m1 m2
-> ImportedNameMap n1 n2 m1 m2
forall a b c. (a -> b -> c) -> b -> a -> c
flip ImportedNameMap n1 n2 m1 m2
-> ImportedName' (n1, n2) (m1, m2) -> ImportedNameMap n1 n2 m1 m2
forall {n1} {m1} {n2} {m2}.
(Ord n1, Ord m1) =>
ImportedNameMap n1 n2 m1 m2
-> ImportedName' (n1, n2) (m1, m2) -> ImportedNameMap n1 n2 m1 m2
add) (ImportedNameMap n1 n2 m1 m2
 -> [ImportedName' (n1, n2) (m1, m2)]
 -> ImportedNameMap n1 n2 m1 m2)
-> ImportedNameMap n1 n2 m1 m2
-> [ImportedName' (n1, n2) (m1, m2)]
-> ImportedNameMap n1 n2 m1 m2
forall a b. (a -> b) -> a -> b
$ Map n1 n2 -> Map m1 m2 -> ImportedNameMap n1 n2 m1 m2
forall n1 n2 m1 m2.
Map n1 n2 -> Map m1 m2 -> ImportedNameMap n1 n2 m1 m2
ImportedNameMap Map n1 n2
forall k a. Map k a
Map.empty Map m1 m2
forall k a. Map k a
Map.empty
  where
  add :: ImportedNameMap n1 n2 m1 m2
-> ImportedName' (n1, n2) (m1, m2) -> ImportedNameMap n1 n2 m1 m2
add (ImportedNameMap Map n1 n2
nm Map m1 m2
mm) = \case
    ImportedName   (n1
x,n2
y) -> Map n1 n2 -> Map m1 m2 -> ImportedNameMap n1 n2 m1 m2
forall n1 n2 m1 m2.
Map n1 n2 -> Map m1 m2 -> ImportedNameMap n1 n2 m1 m2
ImportedNameMap (n1 -> n2 -> Map n1 n2 -> Map n1 n2
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert n1
x n2
y Map n1 n2
nm) Map m1 m2
mm
    ImportedModule (m1
x,m2
y) -> Map n1 n2 -> Map m1 m2 -> ImportedNameMap n1 n2 m1 m2
forall n1 n2 m1 m2.
Map n1 n2 -> Map m1 m2 -> ImportedNameMap n1 n2 m1 m2
ImportedNameMap Map n1 n2
nm (m1 -> m2 -> Map m1 m2 -> Map m1 m2
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert m1
x m2
y Map m1 m2
mm)

-- | Apply a 'ImportedNameMap'.
lookupImportedName
  :: (Ord n1, Ord m1)
  => ImportedNameMap n1 n2 m1 m2
  -> ImportedName' n1 m1
  -> ImportedName' n2 m2
lookupImportedName :: forall n1 m1 n2 m2.
(Ord n1, Ord m1) =>
ImportedNameMap n1 n2 m1 m2
-> ImportedName' n1 m1 -> ImportedName' n2 m2
lookupImportedName (ImportedNameMap Map n1 n2
nm Map m1 m2
mm) = \case
    ImportedName   n1
x -> n2 -> ImportedName' n2 m2
forall n m. n -> ImportedName' n m
ImportedName   (n2 -> ImportedName' n2 m2) -> n2 -> ImportedName' n2 m2
forall a b. (a -> b) -> a -> b
$ n2 -> n1 -> Map n1 n2 -> n2
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault n2
forall a. HasCallStack => a
__IMPOSSIBLE__ n1
x Map n1 n2
nm
    ImportedModule m1
x -> m2 -> ImportedName' n2 m2
forall n m. m -> ImportedName' n m
ImportedModule (m2 -> ImportedName' n2 m2) -> m2 -> ImportedName' n2 m2
forall a b. (a -> b) -> a -> b
$ m2 -> m1 -> Map m1 m2 -> m2
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault m2
forall a. HasCallStack => a
__IMPOSSIBLE__ m1
x Map m1 m2
mm

-- | Translation of @Renaming@.
mapRenaming
  ::  (Ord n1, Ord m1)
  => ImportedNameMap n1 n2 m1 m2  -- ^ Translation of 'renFrom' names and module names.
  -> ImportedNameMap n1 n2 m1 m2  -- ^ Translation of 'rento'   names and module names.
  -> Renaming' n1 m1  -- ^ Renaming before translation (1).
  -> Renaming' n2 m2  -- ^ Renaming after  translation (2).
mapRenaming :: forall n1 m1 n2 m2.
(Ord n1, Ord m1) =>
ImportedNameMap n1 n2 m1 m2
-> ImportedNameMap n1 n2 m1 m2
-> Renaming' n1 m1
-> Renaming' n2 m2
mapRenaming ImportedNameMap n1 n2 m1 m2
src ImportedNameMap n1 n2 m1 m2
tgt (Renaming ImportedName' n1 m1
from ImportedName' n1 m1
to Maybe Fixity
fixity Range
r) =
  ImportedName' n2 m2
-> ImportedName' n2 m2 -> Maybe Fixity -> Range -> Renaming' n2 m2
forall n m.
ImportedName' n m
-> ImportedName' n m -> Maybe Fixity -> Range -> Renaming' n m
Renaming (ImportedNameMap n1 n2 m1 m2
-> ImportedName' n1 m1 -> ImportedName' n2 m2
forall n1 m1 n2 m2.
(Ord n1, Ord m1) =>
ImportedNameMap n1 n2 m1 m2
-> ImportedName' n1 m1 -> ImportedName' n2 m2
lookupImportedName ImportedNameMap n1 n2 m1 m2
src ImportedName' n1 m1
from) (ImportedNameMap n1 n2 m1 m2
-> ImportedName' n1 m1 -> ImportedName' n2 m2
forall n1 m1 n2 m2.
(Ord n1, Ord m1) =>
ImportedNameMap n1 n2 m1 m2
-> ImportedName' n1 m1 -> ImportedName' n2 m2
lookupImportedName ImportedNameMap n1 n2 m1 m2
tgt ImportedName' n1 m1
to) Maybe Fixity
fixity Range
r

---------------------------------------------------------------------------
-- * Opening a module
---------------------------------------------------------------------------

data OpenKind = LetOpenModule | TopOpenModule

noGeneralizedVarsIfLetOpen :: OpenKind -> Scope -> Scope
noGeneralizedVarsIfLetOpen :: OpenKind -> Scope -> Scope
noGeneralizedVarsIfLetOpen OpenKind
TopOpenModule = Scope -> Scope
forall a. a -> a
id
noGeneralizedVarsIfLetOpen OpenKind
LetOpenModule = Scope -> Scope
disallowGeneralizedVars

-- | Open a module.
openModule_ :: OpenKind -> C.QName -> C.ImportDirective -> ScopeM A.ImportDirective
openModule_ :: OpenKind -> QName -> ImportDirective -> ScopeM ImportDirective
openModule_ OpenKind
kind QName
cm ImportDirective
dir = OpenKind
-> Maybe ModuleName
-> QName
-> ImportDirective
-> ScopeM ImportDirective
openModule OpenKind
kind Maybe ModuleName
forall a. Maybe a
Nothing QName
cm ImportDirective
dir

-- | Open a module, possibly given an already resolved module name.
openModule :: OpenKind -> Maybe A.ModuleName  -> C.QName -> C.ImportDirective -> ScopeM A.ImportDirective
openModule :: OpenKind
-> Maybe ModuleName
-> QName
-> ImportDirective
-> ScopeM ImportDirective
openModule OpenKind
kind Maybe ModuleName
mam QName
cm ImportDirective
dir = do
  ModuleName
current <- ScopeM ModuleName
forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule
  ModuleName
m <- Maybe ModuleName
-> ScopeM ModuleName
-> (ModuleName -> ScopeM ModuleName)
-> ScopeM ModuleName
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe ModuleName
mam (AbstractModule -> ModuleName
amodName (AbstractModule -> ModuleName)
-> ScopeM AbstractModule -> ScopeM ModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ScopeM AbstractModule
resolveModule QName
cm) ModuleName -> ScopeM ModuleName
forall (m :: * -> *) a. Monad m => a -> m a
return
  let acc :: NameSpaceId
acc | Maybe Range
Nothing <- ImportDirective -> Maybe Range
forall n m. ImportDirective' n m -> Maybe Range
publicOpen ImportDirective
dir     = NameSpaceId
PrivateNS
          | ModuleName
m ModuleName -> ModuleName -> Bool
`isLtChildModuleOf` ModuleName
current = NameSpaceId
PublicNS
          | Bool
otherwise                     = NameSpaceId
ImportedNS

  -- Get the scope exported by module to be opened.
  (ImportDirective
adir, Scope
s') <- QName
-> ImportDirective -> Scope -> ScopeM (ImportDirective, Scope)
applyImportDirectiveM QName
cm ImportDirective
dir (Scope -> ScopeM (ImportDirective, Scope))
-> (Scope -> Scope) -> Scope -> ScopeM (ImportDirective, Scope)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WhyInScope -> WhyInScope) -> Scope -> Scope
inScopeBecause (QName -> WhyInScope -> WhyInScope
Opened QName
cm) (Scope -> Scope) -> (Scope -> Scope) -> Scope -> Scope
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                OpenKind -> Scope -> Scope
noGeneralizedVarsIfLetOpen OpenKind
kind (Scope -> ScopeM (ImportDirective, Scope))
-> ScopeM Scope -> ScopeM (ImportDirective, Scope)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ModuleName -> ScopeM Scope
getNamedScope ModuleName
m
  let s :: Scope
s  = NameSpaceId -> Scope -> Scope
setScopeAccess NameSpaceId
acc Scope
s'
  let ns :: NameSpace
ns = NameSpaceId -> Scope -> NameSpace
scopeNameSpace NameSpaceId
acc Scope
s
  (Scope -> Scope) -> TCMT IO ()
modifyCurrentScope (Scope -> Scope -> Scope
`mergeScope` Scope
s)
  -- Andreas, 2018-06-03, issue #3057:
  -- If we simply check for ambiguous exported identifiers _after_
  -- importing the new identifiers into the current scope, we also
  -- catch the case of importing an ambiguous identifier.
  TCMT IO ()
checkForClashes

  -- Importing names might shadow existing locals.
  [Char] -> Int -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"scope.locals" Int
10 (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
    [Name]
locals <- ((Name, LocalVar) -> Maybe Name) -> LocalVars -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ (Name
c,LocalVar
x) -> Name
c Name -> Maybe Name -> Maybe Name
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ LocalVar -> Maybe Name
notShadowedLocal LocalVar
x) (LocalVars -> [Name]) -> TCMT IO LocalVars -> TCMT IO [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO LocalVars
forall (m :: * -> *). ReadTCState m => m LocalVars
getLocalVars
    let newdefs :: [Name]
newdefs = NamesInScope -> [Name]
forall k a. Map k a -> [k]
Map.keys (NamesInScope -> [Name]) -> NamesInScope -> [Name]
forall a b. (a -> b) -> a -> b
$ NameSpace -> NamesInScope
nsNames NameSpace
ns
        shadowed :: [Name]
shadowed = [Name]
locals [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
`List.intersect` [Name]
newdefs
    [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.locals" Int
10 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"opening module shadows the following locals vars: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Name] -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow [Name]
shadowed
  -- Andreas, 2014-09-03, issue 1266: shadow local variables by imported defs.
  (LocalVars -> LocalVars) -> TCMT IO ()
modifyLocalVars ((LocalVars -> LocalVars) -> TCMT IO ())
-> (LocalVars -> LocalVars) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ (Name -> LocalVar -> LocalVar) -> LocalVars -> LocalVars
forall k v. (k -> v -> v) -> AssocList k v -> AssocList k v
AssocList.mapWithKey ((Name -> LocalVar -> LocalVar) -> LocalVars -> LocalVars)
-> (Name -> LocalVar -> LocalVar) -> LocalVars -> LocalVars
forall a b. (a -> b) -> a -> b
$ \ Name
c LocalVar
x ->
    case Name -> NamesInScope -> Maybe [AbstractName]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
c (NamesInScope -> Maybe [AbstractName])
-> NamesInScope -> Maybe [AbstractName]
forall a b. (a -> b) -> a -> b
$ NameSpace -> NamesInScope
nsNames NameSpace
ns of
      Maybe [AbstractName]
Nothing -> LocalVar
x
      Just [AbstractName]
ys -> [AbstractName] -> LocalVar -> LocalVar
shadowLocal [AbstractName]
ys LocalVar
x

  ImportDirective -> ScopeM ImportDirective
forall (m :: * -> *) a. Monad m => a -> m a
return ImportDirective
adir

  where
    -- Only checks for clashes that would lead to the same
    -- name being exported twice from the module.
    checkForClashes :: TCMT IO ()
checkForClashes = Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe Range -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Range -> Bool) -> Maybe Range -> Bool
forall a b. (a -> b) -> a -> b
$ ImportDirective -> Maybe Range
forall n m. ImportDirective' n m -> Maybe Range
publicOpen ImportDirective
dir) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do

        NameSpace
exported <- Scope -> NameSpace
allThingsInScope (Scope -> NameSpace) -> (Scope -> Scope) -> Scope -> NameSpace
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Scope -> Scope
restrictPrivate (Scope -> NameSpace) -> ScopeM Scope -> TCMT IO NameSpace
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ModuleName -> ScopeM Scope
getNamedScope (ModuleName -> ScopeM Scope) -> ScopeM ModuleName -> ScopeM Scope
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ScopeM ModuleName
forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule)

        -- Get all exported concrete names that are mapped to at least 2 abstract names
        let defClashes :: [(Name, [AbstractName])]
defClashes = ((Name, [AbstractName]) -> Bool)
-> [(Name, [AbstractName])] -> [(Name, [AbstractName])]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
_c, [AbstractName]
as) -> [AbstractName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [AbstractName]
as Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2) ([(Name, [AbstractName])] -> [(Name, [AbstractName])])
-> [(Name, [AbstractName])] -> [(Name, [AbstractName])]
forall a b. (a -> b) -> a -> b
$ NamesInScope -> [(Name, [AbstractName])]
forall k a. Map k a -> [(k, a)]
Map.toList (NamesInScope -> [(Name, [AbstractName])])
-> NamesInScope -> [(Name, [AbstractName])]
forall a b. (a -> b) -> a -> b
$ NameSpace -> NamesInScope
nsNames NameSpace
exported
            modClashes :: [(Name, [AbstractModule])]
modClashes = ((Name, [AbstractModule]) -> Bool)
-> [(Name, [AbstractModule])] -> [(Name, [AbstractModule])]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
_c, [AbstractModule]
as) -> [AbstractModule] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [AbstractModule]
as Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2) ([(Name, [AbstractModule])] -> [(Name, [AbstractModule])])
-> [(Name, [AbstractModule])] -> [(Name, [AbstractModule])]
forall a b. (a -> b) -> a -> b
$ ModulesInScope -> [(Name, [AbstractModule])]
forall k a. Map k a -> [(k, a)]
Map.toList (ModulesInScope -> [(Name, [AbstractModule])])
-> ModulesInScope -> [(Name, [AbstractModule])]
forall a b. (a -> b) -> a -> b
$ NameSpace -> ModulesInScope
nsModules NameSpace
exported

            -- No ambiguity if concrete identifier is only mapped to
            -- constructor names or only to projection names.
            defClash :: (a, [AbstractName]) -> Bool
defClash (a
_, [AbstractName]
qs) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (KindOfName -> Bool) -> [KindOfName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe Induction -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Induction -> Bool)
-> (KindOfName -> Maybe Induction) -> KindOfName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KindOfName -> Maybe Induction
isConName) [KindOfName]
ks Bool -> Bool -> Bool
|| (KindOfName -> Bool) -> [KindOfName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (KindOfName -> KindOfName -> Bool
forall a. Eq a => a -> a -> Bool
==KindOfName
FldName) [KindOfName]
ks
              where ks :: [KindOfName]
ks = (AbstractName -> KindOfName) -> [AbstractName] -> [KindOfName]
forall a b. (a -> b) -> [a] -> [b]
map AbstractName -> KindOfName
anameKind [AbstractName]
qs
        -- We report the first clashing exported identifier.
        [(Name, [AbstractName])]
-> ([(Name, [AbstractName])] -> TCMT IO ()) -> TCMT IO ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull (((Name, [AbstractName]) -> Bool)
-> [(Name, [AbstractName])] -> [(Name, [AbstractName])]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name, [AbstractName])
x -> (Name, [AbstractName]) -> Bool
forall {a}. (a, [AbstractName]) -> Bool
defClash (Name, [AbstractName])
x) [(Name, [AbstractName])]
defClashes) (([(Name, [AbstractName])] -> TCMT IO ()) -> TCMT IO ())
-> ([(Name, [AbstractName])] -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
          \ ((Name
x, AbstractName
q:[AbstractName]
_) : [(Name, [AbstractName])]
_) -> TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ QName -> QName -> Maybe NiceDeclaration -> TypeError
ClashingDefinition (Name -> QName
C.QName Name
x) (AbstractName -> QName
anameName AbstractName
q) Maybe NiceDeclaration
forall a. Maybe a
Nothing

        [(Name, [AbstractModule])]
-> ([(Name, [AbstractModule])] -> TCMT IO ()) -> TCMT IO ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull [(Name, [AbstractModule])]
modClashes (([(Name, [AbstractModule])] -> TCMT IO ()) -> TCMT IO ())
-> ([(Name, [AbstractModule])] -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ \ ((Name
_, [AbstractModule]
ms) : [(Name, [AbstractModule])]
_) -> do
          Maybe (AbstractModule, AbstractModule)
-> TCMT IO ()
-> ((AbstractModule, AbstractModule) -> TCMT IO ())
-> TCMT IO ()
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe ([AbstractModule] -> Maybe (AbstractModule, AbstractModule)
forall a. [a] -> Maybe (a, a)
last2 [AbstractModule]
ms) TCMT IO ()
forall a. HasCallStack => a
__IMPOSSIBLE__ (((AbstractModule, AbstractModule) -> TCMT IO ()) -> TCMT IO ())
-> ((AbstractModule, AbstractModule) -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ \ (AbstractModule
m0, AbstractModule
m1) -> do
            TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ ModuleName -> ModuleName -> TypeError
ClashingModule (AbstractModule -> ModuleName
amodName AbstractModule
m0) (AbstractModule -> ModuleName
amodName AbstractModule
m1)