{-# LANGUAGE NondecreasingIndentation #-}

{-| The scope monad with operations.
-}

module Agda.Syntax.Scope.Monad where

import Prelude hiding (mapM, any, all, null)

import Control.Arrow ((***))
import Control.Monad hiding (mapM, forM)
import Control.Monad.Writer hiding (mapM, forM)
import Control.Monad.State hiding (mapM, forM)

import Data.Either ( partitionEithers )
import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty(..), nonEmpty)
import qualified Data.List.NonEmpty as NonEmpty
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Foldable (all)
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(..)) -- TODO: move the relevant warnings out of there
import Agda.Syntax.Scope.Base as A

import Agda.TypeChecking.Monad.Base
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 )

import qualified Agda.Utils.AssocList as AssocList
import Agda.Utils.Except
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty

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

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

isDatatypeModule :: ReadTCState m => A.ModuleName -> m (Maybe DataOrRecord)
isDatatypeModule :: ModuleName -> m (Maybe DataOrRecord)
isDatatypeModule ModuleName
m = do
   Scope -> Maybe DataOrRecord
scopeDatatypeModule (Scope -> Maybe DataOrRecord)
-> (Map ModuleName Scope -> Scope)
-> Map ModuleName Scope
-> Maybe DataOrRecord
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 DataOrRecord)
-> m (Map ModuleName Scope) -> m (Maybe DataOrRecord)
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 :: m ModuleName
getCurrentModule = Range -> ModuleName -> ModuleName
forall t. SetRange t => Range -> t -> t
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 :: 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 :: 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' :: ModuleName -> t ScopeM a -> t ScopeM a
withCurrentModule' ModuleName
new t ScopeM a
action = do
  ModuleName
old <- ScopeM ModuleName -> t ScopeM ModuleName
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ScopeM ModuleName
forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule
  ScopeM () -> t ScopeM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ScopeM () -> t ScopeM ()) -> ScopeM () -> t ScopeM ()
forall a b. (a -> b) -> a -> b
$ ModuleName -> ScopeM ()
forall (m :: * -> *). MonadTCState m => ModuleName -> m ()
setCurrentModule ModuleName
new
  a
x   <- t ScopeM a
action
  ScopeM () -> t ScopeM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ScopeM () -> t ScopeM ()) -> ScopeM () -> t ScopeM ()
forall a b. (a -> b) -> a -> b
$ ModuleName -> ScopeM ()
forall (m :: * -> *). MonadTCState m => ModuleName -> m ()
setCurrentModule ModuleName
old
  a -> t ScopeM 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
      String -> Int -> String -> ScopeM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"" Int
0 (String -> ScopeM ()) -> String -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ String
"ERROR: In scope\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ ScopeInfo -> String
forall a. Pretty a => a -> String
prettyShow ScopeInfo
scope String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\nNO SUCH SCOPE " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ModuleName -> String
forall a. Pretty a => a -> String
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.
--   (@Just@ if it is a datatype or record module.)
createModule :: Maybe DataOrRecord -> A.ModuleName -> ScopeM ()
createModule :: Maybe DataOrRecord -> ModuleName -> ScopeM ()
createModule Maybe DataOrRecord
b ModuleName
m = do
  String -> Int -> String -> ScopeM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"scope.createModule" Int
10 (String -> ScopeM ()) -> String -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ String
"createModule " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ModuleName -> String
forall a. Pretty a => a -> String
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 DataOrRecord
scopeDatatypeModule = Maybe DataOrRecord
b }
  -- Andreas, 2015-07-02: internal error if module is not new.
  -- Ulf, 2016-02-15: It's not new if multiple imports (#1770).
  (Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ()
modifyScopes ((Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ())
-> (Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ()
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
forall a b. a -> b -> a
const 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) -> ScopeM ()
modifyScopes = (ScopeInfo -> ScopeInfo) -> ScopeM ()
forall (m :: * -> *).
MonadTCState m =>
(ScopeInfo -> ScopeInfo) -> m ()
modifyScope ((ScopeInfo -> ScopeInfo) -> ScopeM ())
-> ((Map ModuleName Scope -> Map ModuleName Scope)
    -> ScopeInfo -> ScopeInfo)
-> (Map ModuleName Scope -> Map ModuleName Scope)
-> ScopeM ()
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) -> ScopeM ()
modifyNamedScope ModuleName
m Scope -> Scope
f = (Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ()
modifyScopes ((Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ())
-> (Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ()
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 -> ScopeM ()
setNamedScope ModuleName
m Scope
s = ModuleName -> (Scope -> Scope) -> ScopeM ()
modifyNamedScope ModuleName
m ((Scope -> Scope) -> ScopeM ()) -> (Scope -> Scope) -> ScopeM ()
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 :: 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 -> ScopeM ()
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) -> ScopeM ()
modifyCurrentScope Scope -> Scope
f = ScopeM ModuleName
forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule ScopeM ModuleName -> (ModuleName -> ScopeM ()) -> ScopeM ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (ModuleName -> (Scope -> Scope) -> ScopeM ()
`modifyNamedScope` Scope -> Scope
f)

modifyCurrentScopeM :: (Scope -> ScopeM (a, Scope)) -> ScopeM a
modifyCurrentScopeM :: (Scope -> ScopeM (a, Scope)) -> ScopeM a
modifyCurrentScopeM Scope -> ScopeM (a, Scope)
f = ScopeM ModuleName
forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule ScopeM ModuleName -> (ModuleName -> ScopeM a) -> ScopeM a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (ModuleName -> (Scope -> ScopeM (a, Scope)) -> ScopeM 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) -> ScopeM ()
modifyCurrentNameSpace NameSpaceId
acc NameSpace -> NameSpace
f = (Scope -> Scope) -> ScopeM ()
modifyCurrentScope ((Scope -> Scope) -> ScopeM ()) -> (Scope -> Scope) -> ScopeM ()
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 -> ScopeM ()
setContextPrecedence = (ScopeInfo -> ScopeInfo) -> ScopeM ()
forall (m :: * -> *).
MonadTCState m =>
(ScopeInfo -> ScopeInfo) -> m ()
modifyScope_ ((ScopeInfo -> ScopeInfo) -> ScopeM ())
-> (PrecedenceStack -> ScopeInfo -> ScopeInfo)
-> PrecedenceStack
-> ScopeM ()
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 :: 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 :: 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) -> ScopeM ()
modifyLocalVars = (ScopeInfo -> ScopeInfo) -> ScopeM ()
forall (m :: * -> *).
MonadTCState m =>
(ScopeInfo -> ScopeInfo) -> m ()
modifyScope_ ((ScopeInfo -> ScopeInfo) -> ScopeM ())
-> ((LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo)
-> (LocalVars -> LocalVars)
-> ScopeM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo
updateScopeLocals

setLocalVars :: LocalVars -> ScopeM ()
setLocalVars :: LocalVars -> ScopeM ()
setLocalVars LocalVars
vars = (LocalVars -> LocalVars) -> ScopeM ()
modifyLocalVars ((LocalVars -> LocalVars) -> ScopeM ())
-> (LocalVars -> LocalVars) -> ScopeM ()
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 :: ScopeM a -> ScopeM a
withLocalVars = TCMT IO LocalVars
-> (LocalVars -> ScopeM ()) -> ScopeM a -> ScopeM 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 -> ScopeM ()
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 :: 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) -> ScopeM ()
modifyLocalVars (Int -> LocalVars -> LocalVars
forall a. Int -> [a] -> [a]
drop Int
n)
  a
x <- ScopeM a
m
  (LocalVars -> LocalVars) -> ScopeM ()
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 :: ScopeM a -> ScopeM a
withCheckNoShadowing = TCMT IO LocalVars
-> (LocalVars -> ScopeM ()) -> ScopeM a -> ScopeM 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 -> ScopeM ()) -> ScopeM a -> ScopeM a)
-> (LocalVars -> ScopeM ()) -> ScopeM a -> ScopeM a
forall a b. (a -> b) -> a -> b
$ \ LocalVars
lvarsOld ->
  LocalVars -> LocalVars -> ScopeM ()
checkNoShadowing LocalVars
lvarsOld (LocalVars -> ScopeM ()) -> TCMT IO LocalVars -> ScopeM ()
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 -> ScopeM ()
checkNoShadowing LocalVars
old LocalVars
new = do
  PragmaOptions
opts <- TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  Bool -> ScopeM () -> ScopeM ()
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)) (ScopeM () -> ScopeM ()) -> ScopeM () -> ScopeM ()
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 nameOccs :: [(Name, [Range])]
nameOccs = Map Name [Range] -> [(Name, [Range])]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Name [Range] -> [(Name, [Range])])
-> Map Name [Range] -> [(Name, [Range])]
forall a b. (a -> b) -> a -> b
$ ([Range] -> [Range] -> [Range])
-> [(Name, [Range])] -> Map Name [Range]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith [Range] -> [Range] -> [Range]
forall a. [a] -> [a] -> [a]
(++) ([(Name, [Range])] -> Map Name [Range])
-> [(Name, [Range])] -> Map Name [Range]
forall a b. (a -> b) -> a -> b
$ (Name -> (Name, [Range])) -> [Name] -> [(Name, [Range])]
forall a b. (a -> b) -> [a] -> [b]
map Name -> (Name, [Range])
pairWithRange [Name]
newNames
    -- Warn if we have two or more occurrences of the same name.
    [(Name, [Range])] -> ([(Name, [Range])] -> ScopeM ()) -> ScopeM ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull (((Name, [Range]) -> Bool) -> [(Name, [Range])] -> [(Name, [Range])]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Range] -> Bool
forall a. [a] -> Bool
atLeastTwo ([Range] -> Bool)
-> ((Name, [Range]) -> [Range]) -> (Name, [Range]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, [Range]) -> [Range]
forall a b. (a, b) -> b
snd) [(Name, [Range])]
nameOccs) (([(Name, [Range])] -> ScopeM ()) -> ScopeM ())
-> ([(Name, [Range])] -> ScopeM ()) -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ \ [(Name, [Range])]
conflicts -> do
      Warning -> ScopeM ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning (Warning -> ScopeM ()) -> Warning -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Warning
NicifierIssue (DeclarationWarning -> Warning) -> DeclarationWarning -> Warning
forall a b. (a -> b) -> a -> b
$ [(Name, [Range])] -> DeclarationWarning
ShadowingInTelescope [(Name, [Range])]
conflicts
  where
    pairWithRange :: C.Name -> (C.Name, [Range])
    pairWithRange :: Name -> (Name, [Range])
pairWithRange Name
n = (Name
n, [Name -> Range
forall t. HasRange t => t -> Range
getRange Name
n])

    atLeastTwo :: [a] -> Bool
    atLeastTwo :: [a] -> Bool
atLeastTwo (a
_ : a
_ : [a]
_) = Bool
True
    atLeastTwo [a]
_ = Bool
False

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 -> ScopeM ()
addVarToBind Name
x LocalVar
y = (ScopeInfo -> ScopeInfo) -> ScopeM ()
forall (m :: * -> *).
MonadTCState m =>
(ScopeInfo -> ScopeInfo) -> m ()
modifyScope_ ((ScopeInfo -> ScopeInfo) -> ScopeM ())
-> (ScopeInfo -> ScopeInfo) -> ScopeM ()
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 :: ScopeM ()
bindVarsToBind = do
  LocalVars
vars <- TCMT IO LocalVars
getVarsToBind
  (LocalVars -> LocalVars) -> ScopeM ()
modifyLocalVars (LocalVars
varsLocalVars -> LocalVars -> LocalVars
forall a. [a] -> [a] -> [a]
++)
  Int -> String -> ScopeM ()
printLocals Int
10 String
"bound variables:"
  (ScopeInfo -> ScopeInfo) -> ScopeM ()
forall (m :: * -> *).
MonadTCState m =>
(ScopeInfo -> ScopeInfo) -> m ()
modifyScope_ ((ScopeInfo -> ScopeInfo) -> ScopeM ())
-> (ScopeInfo -> ScopeInfo) -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ LocalVars -> ScopeInfo -> ScopeInfo
setVarsToBind []

---------------------------------------------------------------------------
-- * 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
$ Name :: NameId -> Name -> Range -> Fixity' -> Bool -> Name
A.Name
    { nameId :: NameId
nameId          = NameId
i
    , nameConcrete :: Name
nameConcrete    = Name
x
    , nameBindingSite :: Range
nameBindingSite = Name -> Range
forall t. HasRange t => t -> 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.
freshConcreteName :: Range -> Int -> String -> ScopeM C.Name
freshConcreteName :: Range -> Int -> String -> ScopeM Name
freshConcreteName Range
r Int
i String
s = do
  let cname :: Name
cname = Range -> NameInScope -> [NamePart] -> Name
C.Name Range
r NameInScope
C.NotInScope [String -> NamePart
Id (String -> NamePart) -> String -> NamePart
forall a b. (a -> b) -> a -> b
$ String -> String
stringToRawName (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i]
  ResolvedName
rn <- QName -> ScopeM ResolvedName
resolveName (QName -> ScopeM ResolvedName) -> QName -> ScopeM ResolvedName
forall a b. (a -> b) -> a -> b
$ Name -> QName
C.QName Name
cname
  case ResolvedName
rn of
    ResolvedName
UnknownName -> Name -> ScopeM Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
cname
    ResolvedName
_           -> Range -> Int -> String -> ScopeM Name
freshConcreteName Range
r (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) String
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 (NonEmpty QName) ScopeM ResolvedName
-> TCMT IO (Either (NonEmpty QName) ResolvedName)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (KindsOfNames
-> Maybe (Set Name)
-> QName
-> ExceptT (NonEmpty QName) ScopeM ResolvedName
forall (m :: * -> *).
(ReadTCState m, MonadError (NonEmpty QName) m) =>
KindsOfNames -> Maybe (Set Name) -> QName -> m ResolvedName
tryResolveName KindsOfNames
kinds Maybe (Set Name)
names QName
x) TCMT IO (Either (NonEmpty QName) ResolvedName)
-> (Either (NonEmpty QName) ResolvedName -> ScopeM ResolvedName)
-> ScopeM ResolvedName
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Left NonEmpty QName
ys  -> Call -> ScopeM ResolvedName -> ScopeM ResolvedName
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (Range -> Call
SetRange (Range -> Call) -> Range -> Call
forall a b. (a -> b) -> a -> b
$ QName -> Range
forall t. HasRange t => t -> 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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> ScopeM ResolvedName)
-> TypeError -> ScopeM ResolvedName
forall a b. (a -> b) -> a -> b
$ QName -> NonEmpty QName -> TypeError
AmbiguousName QName
x NonEmpty QName
ys
  Right ResolvedName
x' -> ResolvedName -> ScopeM ResolvedName
forall (m :: * -> *) a. Monad m => a -> m a
return ResolvedName
x'

tryResolveName
  :: (ReadTCState m, MonadError (NonEmpty 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 :: 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' ->
          NonEmpty QName -> m ResolvedName
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (NonEmpty QName -> m ResolvedName)
-> NonEmpty QName -> m ResolvedName
forall a b. (a -> b) -> a -> b
$ Name -> QName
A.qualify_ Name
y QName -> [QName] -> NonEmpty 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 of one of the given kinds
      let filtKind :: [(AbstractName, b)] -> [(AbstractName, b)]
filtKind = ((AbstractName, b) -> Bool)
-> [(AbstractName, b)] -> [(AbstractName, b)]
forall a. (a -> Bool) -> [a] -> [a]
filter (((AbstractName, b) -> Bool)
 -> [(AbstractName, b)] -> [(AbstractName, b)])
-> ((AbstractName, b) -> Bool)
-> [(AbstractName, b)]
-> [(AbstractName, b)]
forall a b. (a -> b) -> a -> b
$ (KindOfName -> KindsOfNames -> Bool
`elemKindsOfNames` KindsOfNames
kinds) (KindOfName -> Bool)
-> ((AbstractName, b) -> KindOfName) -> (AbstractName, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> KindOfName
anameKind (AbstractName -> KindOfName)
-> ((AbstractName, b) -> AbstractName)
-> (AbstractName, b)
-> KindOfName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractName, b) -> AbstractName
forall a b. (a, b) -> a
fst
      -- Consider only names in the given set of names
      Maybe (NonEmpty (AbstractName, Access))
-> m ResolvedName
-> (NonEmpty (AbstractName, Access) -> m ResolvedName)
-> m ResolvedName
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe ([(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
$ [(AbstractName, Access)] -> [(AbstractName, Access)]
forall b. [(AbstractName, b)] -> [(AbstractName, b)]
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
x ScopeInfo
scope) (ResolvedName -> m ResolvedName
forall (m :: * -> *) a. Monad m => a -> m a
return ResolvedName
UnknownName) ((NonEmpty (AbstractName, Access) -> m ResolvedName)
 -> m ResolvedName)
-> (NonEmpty (AbstractName, Access) -> m ResolvedName)
-> m ResolvedName
forall a b. (a -> b) -> a -> b
$ \ case
        NonEmpty (AbstractName, Access)
ds       | ((AbstractName, Access) -> Bool)
-> NonEmpty (AbstractName, Access) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((KindOfName
ConName 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 ->
          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
$ NonEmpty AbstractName -> ResolvedName
ConstructorName (NonEmpty AbstractName -> ResolvedName)
-> NonEmpty AbstractName -> ResolvedName
forall a b. (a -> b) -> a -> b
$ ((AbstractName, Access) -> AbstractName)
-> NonEmpty (AbstractName, Access) -> NonEmpty 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

        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 ->
          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
$ NonEmpty AbstractName -> ResolvedName
FieldName (NonEmpty AbstractName -> ResolvedName)
-> NonEmpty AbstractName -> ResolvedName
forall a b. (a -> b) -> a -> b
$ ((AbstractName, Access) -> AbstractName)
-> NonEmpty (AbstractName, Access) -> NonEmpty 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

        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 ->
          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
$ NonEmpty AbstractName -> ResolvedName
PatternSynResName (NonEmpty AbstractName -> ResolvedName)
-> NonEmpty AbstractName -> ResolvedName
forall a b. (a -> b) -> a -> b
$ ((AbstractName, Access) -> AbstractName)
-> NonEmpty (AbstractName, Access) -> NonEmpty 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

        (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 -> ResolvedName
DefinedName Access
a (AbstractName -> ResolvedName) -> AbstractName -> ResolvedName
forall a b. (a -> b) -> a -> b
$ AbstractName -> AbstractName
upd AbstractName
d

        NonEmpty (AbstractName, Access)
ds -> NonEmpty QName -> m ResolvedName
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (NonEmpty QName -> m ResolvedName)
-> NonEmpty QName -> m ResolvedName
forall a b. (a -> b) -> a -> b
$ ((AbstractName, Access) -> QName)
-> NonEmpty (AbstractName, Access) -> NonEmpty 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)
ds
  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 :: (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 t. SetRange t => Range -> t -> t
setRange (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
x) ModuleName
qm) (Name
qn { nameConcrete :: Name
nameConcrete = Name
x }) }

-- | 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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> ScopeM AbstractModule)
-> TypeError -> ScopeM AbstractModule
forall a b. (a -> b) -> a -> b
$ QName -> NonEmpty ModuleName -> TypeError
AmbiguousModule QName
x ((AbstractModule -> ModuleName)
-> NonEmpty AbstractModule -> NonEmpty 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 :: [(Name, [Fixity'])] -> ScopeM a
throwMultipleFixityDecls [(Name, [Fixity'])]
xs         = case [(Name, [Fixity'])]
xs of
    (Name
x, [Fixity']
_) : [(Name, [Fixity'])]
_ -> Range -> ScopeM a -> ScopeM a
forall (tcm :: * -> *) x a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) =>
x -> tcm a -> tcm a
setCurrentRange (Name -> Range
forall t. HasRange t => t -> 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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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 :: [Name] -> ScopeM a
throwMultiplePolarityPragmas [Name]
xs     = case [Name]
xs of
    Name
x : [Name]
_ -> Range -> ScopeM a -> ScopeM a
forall (tcm :: * -> *) x a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) =>
x -> tcm a -> tcm a
setCurrentRange (Name -> Range
forall t. HasRange t => t -> 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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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 :: [Name] -> ScopeM ()
warnUnknownNamesInFixityDecl        = Warning -> ScopeM ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning   (Warning -> ScopeM ())
-> ([Name] -> Warning) -> [Name] -> ScopeM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeclarationWarning -> Warning
NicifierIssue (DeclarationWarning -> Warning)
-> ([Name] -> DeclarationWarning) -> [Name] -> Warning
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> DeclarationWarning
UnknownNamesInFixityDecl
  warnUnknownNamesInPolarityPragmas :: [Name] -> ScopeM ()
warnUnknownNamesInPolarityPragmas   = Warning -> ScopeM ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning   (Warning -> ScopeM ())
-> ([Name] -> Warning) -> [Name] -> ScopeM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeclarationWarning -> Warning
NicifierIssue (DeclarationWarning -> Warning)
-> ([Name] -> DeclarationWarning) -> [Name] -> Warning
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> DeclarationWarning
UnknownNamesInPolarityPragmas
  warnUnknownFixityInMixfixDecl :: [Name] -> ScopeM ()
warnUnknownFixityInMixfixDecl       = Warning -> ScopeM ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning   (Warning -> ScopeM ())
-> ([Name] -> Warning) -> [Name] -> ScopeM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeclarationWarning -> Warning
NicifierIssue (DeclarationWarning -> Warning)
-> ([Name] -> DeclarationWarning) -> [Name] -> Warning
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> DeclarationWarning
UnknownFixityInMixfixDecl
  warnPolarityPragmasButNotPostulates :: [Name] -> ScopeM ()
warnPolarityPragmasButNotPostulates = Warning -> ScopeM ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning   (Warning -> ScopeM ())
-> ([Name] -> Warning) -> [Name] -> ScopeM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeclarationWarning -> Warning
NicifierIssue (DeclarationWarning -> Warning)
-> ([Name] -> DeclarationWarning) -> [Name] -> Warning
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 :: 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     -> 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 NonEmpty 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
$ NonEmpty AbstractName -> NewNotation
oneNotation NonEmpty AbstractName
ds
    ConstructorName NonEmpty 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
$ NonEmpty AbstractName -> NewNotation
oneNotation NonEmpty AbstractName
ds
    PatternSynResName NonEmpty 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
$ NonEmpty AbstractName -> NewNotation
oneNotation NonEmpty 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 :: NonEmpty AbstractName -> NewNotation
oneNotation NonEmpty 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
$ NonEmpty AbstractName -> [AbstractName]
forall a. NonEmpty a -> [a]
NonEmpty.toList NonEmpty 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 -> ScopeM ()
bindVariable BindingSource
b Name
x Name
y = (LocalVars -> LocalVars) -> ScopeM ()
modifyLocalVars ((LocalVars -> LocalVars) -> ScopeM ())
-> (LocalVars -> LocalVars) -> ScopeM ()
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 :: Name -> ScopeM a -> ScopeM a
unbindVariable Name
x = TCMT IO LocalVars
-> (LocalVars -> ScopeM ()) -> ScopeM a -> ScopeM 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 -> ScopeM () -> TCMT IO LocalVars
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* (LocalVars -> LocalVars) -> ScopeM ()
modifyLocalVars (Name -> LocalVars -> LocalVars
forall k v. Eq k => k -> AssocList k v -> AssocList k v
AssocList.delete Name
x)) ((LocalVars -> LocalVars) -> ScopeM ()
modifyLocalVars ((LocalVars -> LocalVars) -> ScopeM ())
-> (LocalVars -> LocalVars -> LocalVars) -> LocalVars -> ScopeM ()
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 -> ScopeM ()
bindName Access
acc KindOfName
kind Name
x QName
y = Access -> KindOfName -> NameMetadata -> Name -> QName -> ScopeM ()
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 -> ScopeM ()
bindName' Access
acc KindOfName
kind NameMetadata
meta Name
x QName
y = do
  Bool -> ScopeM () -> ScopeM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x) (ScopeM () -> ScopeM ()) -> ScopeM () -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ (Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ()
modifyScopes ((Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ())
-> (Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ()
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)
  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      -> TCMT IO AbstractName
success
    DefinedName Access
_ AbstractName
d     -> QName -> TCMT IO AbstractName
forall a. QName -> TCMT IO a
clash (QName -> TCMT IO AbstractName) -> QName -> TCMT IO AbstractName
forall a b. (a -> b) -> a -> b
$ AbstractName -> QName
anameName AbstractName
d
    VarName Name
z BindingSource
_         -> QName -> TCMT IO AbstractName
forall a. QName -> TCMT IO a
clash (QName -> TCMT IO AbstractName) -> QName -> TCMT IO AbstractName
forall a b. (a -> b) -> a -> b
$ ModuleName -> Name -> QName
A.qualify ([Name] -> ModuleName
mnameFromList []) Name
z
    FieldName       NonEmpty AbstractName
ds  -> KindOfName -> NonEmpty AbstractName -> TCMT IO AbstractName
ambiguous KindOfName
FldName NonEmpty AbstractName
ds
    ConstructorName NonEmpty AbstractName
ds  -> KindOfName -> NonEmpty AbstractName -> TCMT IO AbstractName
ambiguous KindOfName
ConName NonEmpty AbstractName
ds
    PatternSynResName NonEmpty AbstractName
n -> KindOfName -> NonEmpty AbstractName -> TCMT IO AbstractName
ambiguous KindOfName
PatternSynName NonEmpty AbstractName
n
    ResolvedName
UnknownName         -> TCMT IO 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
  (Scope -> Scope) -> ScopeM ()
modifyCurrentScope ((Scope -> Scope) -> ScopeM ()) -> (Scope -> Scope) -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ NameSpaceId -> Name -> AbstractName -> Scope -> Scope
addNameToScope NameSpaceId
ns Name
x AbstractName
y'
  where
    success :: TCMT IO AbstractName
success = AbstractName -> TCMT IO AbstractName
forall (m :: * -> *) a. Monad m => a -> m a
return (AbstractName -> TCMT IO AbstractName)
-> AbstractName -> TCMT IO AbstractName
forall a b. (a -> b) -> a -> b
$ QName -> KindOfName -> WhyInScope -> NameMetadata -> AbstractName
AbsName QName
y KindOfName
kind WhyInScope
Defined NameMetadata
meta
    clash :: QName -> TCMT IO a
clash   = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a)
-> (QName -> TypeError) -> QName -> TCMT IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> QName -> TypeError
ClashingDefinition (Name -> QName
C.QName Name
x)

    ambiguous :: KindOfName -> NonEmpty AbstractName -> TCMT IO AbstractName
ambiguous KindOfName
k NonEmpty AbstractName
ds =
      if KindOfName
kind KindOfName -> KindOfName -> Bool
forall a. Eq a => a -> a -> Bool
== KindOfName
k Bool -> Bool -> Bool
&& (AbstractName -> Bool) -> NonEmpty AbstractName -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((KindOfName -> KindOfName -> Bool
forall a. Eq a => a -> a -> Bool
== KindOfName
k) (KindOfName -> Bool)
-> (AbstractName -> KindOfName) -> AbstractName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> KindOfName
anameKind) NonEmpty AbstractName
ds
      then TCMT IO AbstractName
success else QName -> TCMT IO AbstractName
forall a. QName -> TCMT IO a
clash (QName -> TCMT IO AbstractName) -> QName -> TCMT IO AbstractName
forall a b. (a -> b) -> a -> b
$ AbstractName -> QName
anameName (NonEmpty AbstractName -> AbstractName
forall a. NonEmpty a -> a
NonEmpty.head NonEmpty 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 -> ScopeM ()
rebindName Access
acc KindOfName
kind Name
x QName
y = do
  (Scope -> Scope) -> ScopeM ()
modifyCurrentScope ((Scope -> Scope) -> ScopeM ()) -> (Scope -> Scope) -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ NameSpaceId -> Name -> Scope -> Scope
removeNameFromScope (Access -> NameSpaceId
localNameSpace Access
acc) Name
x
  Access -> KindOfName -> Name -> QName -> ScopeM ()
bindName Access
acc KindOfName
kind Name
x QName
y

-- | Bind a module name.
bindModule :: Access -> C.Name -> A.ModuleName -> ScopeM ()
bindModule :: Access -> Name -> ModuleName -> ScopeM ()
bindModule Access
acc Name
x ModuleName
m = (Scope -> Scope) -> ScopeM ()
modifyCurrentScope ((Scope -> Scope) -> ScopeM ()) -> (Scope -> Scope) -> ScopeM ()
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 -> ScopeM ()
bindQModule Access
acc QName
q ModuleName
m = (Scope -> Scope) -> ScopeM ()
modifyCurrentScope ((Scope -> Scope) -> ScopeM ()) -> (Scope -> Scope) -> ScopeM ()
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 :: ScopeM ()
stripNoNames = (Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ()
modifyScopes ((Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ())
-> (Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ()
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 b. Map Name b -> Map Name b
stripN ModulesInScope -> ModulesInScope
forall b. Map Name b -> Map Name b
stripN InScopeSet -> InScopeSet
forall a. a -> a
id
  where
    stripN :: Map Name b -> Map Name b
stripN = (Name -> b -> Bool) -> Map Name b -> Map Name b
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey ((Name -> b -> Bool) -> Map Name b -> Map Name b)
-> (Name -> b -> Bool) -> Map Name b -> Map Name b
forall a b. (a -> b) -> a -> b
$ Bool -> b -> Bool
forall a b. a -> b -> a
const (Bool -> b -> Bool) -> (Name -> Bool) -> Name -> b -> 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 -> [(ModuleName, (ModuleName, Bool))]
memoModules :: [(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 [(ModuleName, (ModuleName, Bool))]
mods) =
  ScopeCopyInfo :: Ren ModuleName -> Ren QName -> ScopeCopyInfo
ScopeCopyInfo { renNames :: Ren QName
renNames   = Ren QName
names
                , renModules :: Ren ModuleName
renModules = [ (ModuleName
x, ModuleName
y) | (ModuleName
x, (ModuleName
y, Bool
_)) <- [(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))
-> ScopeM (Scope, ScopeMemo) -> ScopeM (Scope, ScopeCopyInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ScopeMemo ScopeM Scope
-> ScopeMemo -> ScopeM (Scope, ScopeMemo)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (ModuleName -> Scope -> StateT ScopeMemo ScopeM Scope
copy ModuleName
new0 Scope
s) (Ren QName -> [(ModuleName, (ModuleName, Bool))] -> ScopeMemo
ScopeMemo [] [])
  where
    copy :: A.ModuleName -> Scope -> WSM Scope
    copy :: ModuleName -> Scope -> StateT ScopeMemo ScopeM Scope
copy ModuleName
new Scope
s = do
      ScopeM () -> StateT ScopeMemo ScopeM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ScopeM () -> StateT ScopeMemo ScopeM ())
-> ScopeM () -> StateT ScopeMemo ScopeM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> String -> ScopeM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"scope.copy" Int
20 (String -> ScopeM ()) -> String -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ String
"Copying scope " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ModuleName -> String
forall a. Pretty a => a -> String
prettyShow ModuleName
old String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ModuleName -> String
forall a. Pretty a => a -> String
prettyShow ModuleName
new
      ScopeM () -> StateT ScopeMemo ScopeM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ScopeM () -> StateT ScopeMemo ScopeM ())
-> ScopeM () -> StateT ScopeMemo ScopeM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> String -> ScopeM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"scope.copy" Int
50 (String -> ScopeM ()) -> String -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ Scope -> String
forall a. Pretty a => a -> String
prettyShow Scope
s
      Scope
s0 <- ScopeM Scope -> StateT ScopeMemo ScopeM Scope
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ScopeM Scope -> StateT ScopeMemo ScopeM Scope)
-> ScopeM Scope -> StateT ScopeMemo ScopeM 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 ScopeM Scope -> StateT ScopeMemo ScopeM Scope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NamesInScope -> StateT ScopeMemo ScopeM NamesInScope)
-> (ModulesInScope -> StateT ScopeMemo ScopeM ModulesInScope)
-> (InScopeSet -> StateT ScopeMemo ScopeM InScopeSet)
-> Scope
-> StateT ScopeMemo ScopeM Scope
forall (m :: * -> *).
Applicative m =>
(NamesInScope -> m NamesInScope)
-> (ModulesInScope -> m ModulesInScope)
-> (InScopeSet -> m InScopeSet)
-> Scope
-> m Scope
mapScopeM_ NamesInScope -> StateT ScopeMemo ScopeM NamesInScope
copyD ModulesInScope -> StateT ScopeMemo ScopeM ModulesInScope
copyM InScopeSet -> StateT ScopeMemo ScopeM 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 ScopeM Scope
forall (m :: * -> *) a. Monad m => a -> m a
return (Scope -> StateT ScopeMemo ScopeM Scope)
-> Scope -> StateT ScopeMemo ScopeM 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 t. HasRange t => t -> 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 ScopeM NamesInScope
copyD = ([AbstractName] -> StateT ScopeMemo ScopeM [AbstractName])
-> NamesInScope -> StateT ScopeMemo ScopeM NamesInScope
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (([AbstractName] -> StateT ScopeMemo ScopeM [AbstractName])
 -> NamesInScope -> StateT ScopeMemo ScopeM NamesInScope)
-> ([AbstractName] -> StateT ScopeMemo ScopeM [AbstractName])
-> NamesInScope
-> StateT ScopeMemo ScopeM NamesInScope
forall a b. (a -> b) -> a -> b
$ (AbstractName -> StateT ScopeMemo ScopeM AbstractName)
-> [AbstractName] -> StateT ScopeMemo ScopeM [AbstractName]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((AbstractName -> StateT ScopeMemo ScopeM AbstractName)
 -> [AbstractName] -> StateT ScopeMemo ScopeM [AbstractName])
-> (AbstractName -> StateT ScopeMemo ScopeM AbstractName)
-> [AbstractName]
-> StateT ScopeMemo ScopeM [AbstractName]
forall a b. (a -> b) -> a -> b
$ (QName -> WSM QName)
-> AbstractName -> StateT ScopeMemo ScopeM AbstractName
onName QName -> WSM QName
renName

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

        onName :: (A.QName -> WSM A.QName) -> AbstractName -> WSM AbstractName
        onName :: (QName -> WSM QName)
-> AbstractName -> StateT ScopeMemo ScopeM AbstractName
onName QName -> WSM QName
f AbstractName
d =
          case AbstractName -> KindOfName
anameKind AbstractName
d of
            KindOfName
PatternSynName -> AbstractName -> StateT ScopeMemo ScopeM 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 ScopeM AbstractName
forall (m :: * -> *).
Functor m =>
(QName -> m QName) -> AbstractName -> m 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   = (QName
x, QName
y)        (QName, QName) -> Ren QName -> Ren QName
forall a. a -> [a] -> [a]
: 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 :: [(ModuleName, (ModuleName, Bool))]
memoModules = (ModuleName
x, (ModuleName
y, Bool
rec)) (ModuleName, (ModuleName, Bool))
-> [(ModuleName, (ModuleName, Bool))]
-> [(ModuleName, (ModuleName, Bool))]
forall a. a -> [a] -> [a]
: ((ModuleName, (ModuleName, Bool)) -> Bool)
-> [(ModuleName, (ModuleName, Bool))]
-> [(ModuleName, (ModuleName, Bool))]
forall a. (a -> Bool) -> [a] -> [a]
filter ((ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
/= ModuleName
x) (ModuleName -> Bool)
-> ((ModuleName, (ModuleName, Bool)) -> ModuleName)
-> (ModuleName, (ModuleName, Bool))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleName, (ModuleName, Bool)) -> ModuleName
forall a b. (a, b) -> a
fst) (ScopeMemo -> [(ModuleName, (ModuleName, Bool))]
memoModules ScopeMemo
i) }

        -- Querying the memo structure.
        findName :: QName -> f (Maybe QName)
findName QName
x = QName -> Ren QName -> Maybe QName
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup QName
x (Ren QName -> Maybe QName) -> f (Ren QName) -> f (Maybe QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ScopeMemo -> Ren QName) -> f (Ren QName)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ScopeMemo -> Ren QName
memoNames
        findMod :: ModuleName -> f (Maybe (ModuleName, Bool))
findMod  ModuleName
x = ModuleName
-> [(ModuleName, (ModuleName, Bool))] -> Maybe (ModuleName, Bool)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup ModuleName
x ([(ModuleName, (ModuleName, Bool))] -> Maybe (ModuleName, Bool))
-> f [(ModuleName, (ModuleName, Bool))]
-> f (Maybe (ModuleName, Bool))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ScopeMemo -> [(ModuleName, (ModuleName, Bool))])
-> f [(ModuleName, (ModuleName, Bool))]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ScopeMemo -> [(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 ScopeM 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 <- case QName
x QName -> ModuleName -> Bool
`isInModule` ModuleName
old of
                 Bool
True  -> ModuleName -> StateT ScopeMemo ScopeM ModuleName
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleName
new'
                 Bool
False -> Bool -> ModuleName -> StateT ScopeMemo ScopeM 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 t. SetRange t => Range -> t -> t
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)
          ScopeM () -> StateT ScopeMemo ScopeM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ScopeM () -> StateT ScopeMemo ScopeM ())
-> ScopeM () -> StateT ScopeMemo ScopeM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> String -> ScopeM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"scope.copy" Int
50 (String -> ScopeM ()) -> String -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ String
"  Copying " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
y
          QName -> QName -> StateT ScopeMemo ScopeM ()
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 ScopeM ModuleName
renMod = Bool -> ModuleName -> StateT ScopeMemo ScopeM ModuleName
renMod' Bool
True

        renMod' :: Bool -> ModuleName -> StateT ScopeMemo ScopeM 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 ScopeM (Maybe (ModuleName, Bool))
forall (f :: * -> *).
MonadState ScopeMemo f =>
ModuleName -> f (Maybe (ModuleName, Bool))
findMod ModuleName
x
          case Maybe (ModuleName, Bool)
z of
            Just (ModuleName
y, Bool
False) | Bool
rec -> ModuleName
y ModuleName
-> StateT ScopeMemo ScopeM () -> StateT ScopeMemo ScopeM ModuleName
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ModuleName -> ModuleName -> StateT ScopeMemo ScopeM ()
copyRec ModuleName
x ModuleName
y
            Just (ModuleName
y, Bool
_)           -> ModuleName -> StateT ScopeMemo ScopeM 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] -> Name
forall a. [a] -> a
last ([Name] -> Name) -> [Name] -> Name
forall a b. (a -> b) -> a -> b
$ ModuleName -> [Name]
A.mnameToList ModuleName
x)
               ModuleName -> StateT ScopeMemo ScopeM ModuleName
forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleName -> StateT ScopeMemo ScopeM ModuleName)
-> ModuleName -> StateT ScopeMemo ScopeM 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 ScopeM ModuleName
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleName
x else do
            ScopeM () -> StateT ScopeMemo ScopeM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ScopeM () -> StateT ScopeMemo ScopeM ())
-> ScopeM () -> StateT ScopeMemo ScopeM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> String -> ScopeM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"scope.copy" Int
50 (String -> ScopeM ()) -> String -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ String
"  Copying module " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ModuleName -> String
forall a. Pretty a => a -> String
prettyShow ModuleName
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ModuleName -> String
forall a. Pretty a => a -> String
prettyShow ModuleName
y
            ModuleName -> ModuleName -> Bool -> StateT ScopeMemo ScopeM ()
forall (m :: * -> *).
MonadState ScopeMemo m =>
ModuleName -> ModuleName -> Bool -> m ()
addMod ModuleName
x ModuleName
y Bool
rec
            ScopeM () -> StateT ScopeMemo ScopeM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ScopeM () -> StateT ScopeMemo ScopeM ())
-> ScopeM () -> StateT ScopeMemo ScopeM ()
forall a b. (a -> b) -> a -> b
$ Maybe DataOrRecord -> ModuleName -> ScopeM ()
createModule Maybe DataOrRecord
forall a. Maybe a
Nothing ModuleName
y
            -- We need to copy the contents of included modules recursively (only when 'rec')
            Bool -> StateT ScopeMemo ScopeM () -> StateT ScopeMemo ScopeM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
rec (StateT ScopeMemo ScopeM () -> StateT ScopeMemo ScopeM ())
-> StateT ScopeMemo ScopeM () -> StateT ScopeMemo ScopeM ()
forall a b. (a -> b) -> a -> b
$ ModuleName -> ModuleName -> StateT ScopeMemo ScopeM ()
copyRec ModuleName
x ModuleName
y
            ModuleName -> StateT ScopeMemo ScopeM ModuleName
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleName
y
          where
            copyRec :: ModuleName -> ModuleName -> StateT ScopeMemo ScopeM ()
copyRec ModuleName
x ModuleName
y = do
              Scope
s0 <- ScopeM Scope -> StateT ScopeMemo ScopeM Scope
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ScopeM Scope -> StateT ScopeMemo ScopeM Scope)
-> ScopeM Scope -> StateT ScopeMemo ScopeM Scope
forall a b. (a -> b) -> a -> b
$ ModuleName -> ScopeM Scope
getNamedScope ModuleName
x
              Scope
s  <- ModuleName
-> StateT ScopeMemo ScopeM Scope -> StateT ScopeMemo ScopeM Scope
forall (t :: (* -> *) -> * -> *) a.
(MonadTrans t, Monad (t ScopeM)) =>
ModuleName -> t ScopeM a -> t ScopeM a
withCurrentModule' ModuleName
y (StateT ScopeMemo ScopeM Scope -> StateT ScopeMemo ScopeM Scope)
-> StateT ScopeMemo ScopeM Scope -> StateT ScopeMemo ScopeM Scope
forall a b. (a -> b) -> a -> b
$ ModuleName -> Scope -> StateT ScopeMemo ScopeM Scope
copy ModuleName
y Scope
s0
              ScopeM () -> StateT ScopeMemo ScopeM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ScopeM () -> StateT ScopeMemo ScopeM ())
-> ScopeM () -> StateT ScopeMemo ScopeM ()
forall a b. (a -> b) -> a -> b
$ ModuleName -> (Scope -> Scope) -> ScopeM ()
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.
checkNoFixityInRenamingModule :: [C.Renaming] -> ScopeM ()
checkNoFixityInRenamingModule :: [Renaming] -> ScopeM ()
checkNoFixityInRenamingModule [Renaming]
ren = do
  Maybe (NonEmpty Range)
-> (NonEmpty Range -> ScopeM ()) -> ScopeM ()
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 -> ScopeM ()) -> ScopeM ())
-> (NonEmpty Range -> ScopeM ()) -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ \ NonEmpty Range
rs -> do
    Call -> ScopeM () -> ScopeM ()
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (Range -> Call
SetRange (Range -> Call) -> Range -> Call
forall a b. (a -> b) -> a -> b
$ NonEmpty Range -> Range
forall t. HasRange t => t -> Range
getRange NonEmpty Range
rs) (ScopeM () -> ScopeM ()) -> ScopeM () -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ do
      Warning -> ScopeM ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning (Warning -> ScopeM ()) -> Warning -> ScopeM ()
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' Name Name
_ Maybe Fixity
mfx Range
_ -> Fixity -> Range
forall t. HasRange t => t -> 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

-- | Apply an import directive and check that all the names mentioned actually
--   exist.
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' Name Name]
hdn' [Renaming]
ren' Maybe Range
public) Scope
scope = do

    -- Modules names do not come with fixities, thus, we should complain if the
    -- user supplied fixity annotations to renaming-module clauses.
    [Renaming] -> ScopeM ()
checkNoFixityInRenamingModule [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 usingList :: [ImportedName' Name Name]
usingList = Using' Name Name -> [ImportedName' Name Name]
forall a b. Using' a b -> [ImportedName' a b]
fromUsing Using' Name Name
usn'
    let ([ImportedName' Name Name]
missingExports, [ImportedName' (Name, QName) (Name, ModuleName)]
namesA) = [ImportedName' Name Name]
-> ([ImportedName' Name Name],
    [ImportedName' (Name, QName) (Name, ModuleName)])
checkExist ([ImportedName' Name Name]
 -> ([ImportedName' Name Name],
     [ImportedName' (Name, QName) (Name, ModuleName)]))
-> [ImportedName' Name Name]
-> ([ImportedName' Name Name],
    [ImportedName' (Name, QName) (Name, ModuleName)])
forall a b. (a -> b) -> a -> b
$ [ImportedName' Name Name]
usingList [ImportedName' Name Name]
-> [ImportedName' Name Name] -> [ImportedName' Name Name]
forall a. [a] -> [a] -> [a]
++ [ImportedName' Name Name]
hdn' [ImportedName' Name Name]
-> [ImportedName' Name Name] -> [ImportedName' Name Name]
forall a. [a] -> [a] -> [a]
++ (Renaming -> ImportedName' Name Name)
-> [Renaming] -> [ImportedName' Name Name]
forall a b. (a -> b) -> [a] -> [b]
map Renaming -> ImportedName' Name Name
forall n m. Renaming' n m -> ImportedName' n m
renFrom [Renaming]
ren'
    Bool -> ScopeM () -> ScopeM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([ImportedName' Name Name] -> Bool
forall a. Null a => a -> Bool
null [ImportedName' Name Name]
missingExports) (ScopeM () -> ScopeM ()) -> ScopeM () -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ Range -> ScopeM () -> ScopeM ()
forall (tcm :: * -> *) x a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) =>
x -> tcm a -> tcm a
setCurrentRange Range
rng (ScopeM () -> ScopeM ()) -> ScopeM () -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ do
      String -> Int -> String -> ScopeM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"scope.import.apply" Int
20 (String -> ScopeM ()) -> String -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ String
"non existing names: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [ImportedName' Name Name] -> String
forall a. Pretty a => a -> String
prettyShow [ImportedName' Name Name]
missingExports
      Warning -> ScopeM ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning (Warning -> ScopeM ()) -> Warning -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ QName -> [ImportedName' Name Name] -> Warning
ModuleDoesntExport QName
m [ImportedName' Name Name]
missingExports

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

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

    -- Efficient test of (`elem` names):
    let inNames :: ImportedName' Name Name -> Bool
inNames      = ([ImportedName' Name Name]
names [ImportedName' Name Name] -> ImportedName' Name Name -> 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 = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
          [ ImportedName' Name Name -> Bool
inNames       (ImportedName' Name Name -> Bool)
-> ImportedName' Name Name -> Bool
forall a b. (a -> b) -> a -> b
$ Name -> ImportedName' Name Name
forall n m. n -> ImportedName' n m
ImportedName   Name
x
          , ImportedName' Name Name -> Bool
notMissing    (ImportedName' Name Name -> Bool)
-> ImportedName' Name Name -> Bool
forall a b. (a -> b) -> a -> b
$ Name -> ImportedName' Name Name
forall n m. m -> ImportedName' n m
ImportedModule Name
x
          , Bool -> Bool
not (Bool -> Bool)
-> (ImportedName' Name Name -> Bool)
-> ImportedName' Name Name
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ImportedName' Name Name -> Bool
inNames (ImportedName' Name Name -> Bool)
-> ImportedName' Name Name -> Bool
forall a b. (a -> b) -> a -> b
$ Name -> ImportedName' Name Name
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' Name Name -> Bool)
-> ImportDirective -> TCMT IO ImportDirective
forall (m :: * -> *) n m m.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m, Pretty n,
 Pretty m) =>
(ImportedName' m m -> Bool)
-> ImportDirective' n m -> m (ImportDirective' n m)
sanityCheck (Bool -> Bool
not (Bool -> Bool)
-> (ImportedName' Name Name -> Bool)
-> ImportedName' Name Name
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ImportedName' Name Name -> 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' Name Name]
-> ([ImportedName' Name Name] -> ScopeM ()) -> ScopeM ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull ([ImportedName' Name Name] -> [ImportedName' Name Name]
forall a. Ord a => [a] -> [a]
allDuplicates [ImportedName' Name Name]
targetNames) (([ImportedName' Name Name] -> ScopeM ()) -> ScopeM ())
-> ([ImportedName' Name Name] -> ScopeM ()) -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ \ [ImportedName' Name Name]
dup ->
      TypeError -> ScopeM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> ScopeM ()) -> TypeError -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ QName -> [ImportedName' Name Name] -> TypeError
DuplicateImports QName
m [ImportedName' Name Name]
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 -> ScopeM () -> ScopeM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set Name -> Bool
forall a. Null a => a -> Bool
null Set Name
nameClashes) (ScopeM () -> ScopeM ()) -> ScopeM () -> ScopeM ()
forall a b. (a -> b) -> a -> b
$
      Warning -> ScopeM ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning (Warning -> ScopeM ()) -> Warning -> ScopeM ()
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 -> ScopeM () -> ScopeM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set Name -> Bool
forall a. Null a => a -> Bool
null Set Name
moduleClashes) (ScopeM () -> ScopeM ()) -> ScopeM () -> ScopeM ()
forall a b. (a -> b) -> a -> b
$
      Warning -> ScopeM ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning (Warning -> ScopeM ()) -> Warning -> ScopeM ()
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' Name Name]
-> (ImportedName' Name Name
    -> ImportedName' (Name, QName) (Name, ModuleName))
-> [ImportedName' (Name, QName) (Name, ModuleName)]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [ImportedName' Name Name]
definedNames ((ImportedName' Name Name
  -> ImportedName' (Name, QName) (Name, ModuleName))
 -> [ImportedName' (Name, QName) (Name, ModuleName)])
-> (ImportedName' Name Name
    -> 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 t. SetRange t => Range -> t -> t
setRange (Name -> Range
forall t. HasRange t => t -> 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 t. SetRange t => Range -> t -> t
setRange (Name -> Range
forall t. HasRange t => t -> 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
    -- | Names in the @using@ directive
    fromUsing :: Using' a b -> [ImportedName' a b]
    fromUsing :: Using' a b -> [ImportedName' a b]
fromUsing = \case
      Using  [ImportedName' a b]
xs     -> [ImportedName' a b]
xs
      Using' a b
UseEverything -> []

    -- If both @using@ and @hiding@ directive are present,
    -- the hiding directive may only contain modules whose twins are mentioned.
    sanityCheck :: (ImportedName' m m -> Bool)
-> ImportDirective' n m -> m (ImportDirective' n m)
sanityCheck ImportedName' m m -> Bool
notMentioned = \case
      dir :: ImportDirective' n m
dir@(ImportDirective{ using :: forall n m. ImportDirective' n m -> Using' n m
using = Using{}, hiding :: forall n m. ImportDirective' n m -> [ImportedName' n m]
hiding = [ImportedName' n m]
ys }) -> do
          let useless :: ImportedName' n m -> Bool
useless = \case
                ImportedName{}   -> Bool
True
                ImportedModule m
y -> ImportedName' m m -> Bool
notMentioned (m -> ImportedName' m m
forall n m. n -> ImportedName' n m
ImportedName m
y)
          [ImportedName' n m] -> ([ImportedName' n m] -> m ()) -> m ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull ((ImportedName' n m -> Bool)
-> [ImportedName' n m] -> [ImportedName' n m]
forall a. (a -> Bool) -> [a] -> [a]
filter ImportedName' n m -> Bool
forall n. ImportedName' n m -> Bool
useless [ImportedName' n m]
ys) (([ImportedName' n m] -> m ()) -> m ())
-> ([ImportedName' n m] -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ [ImportedName' n m]
uselessHiding -> do
            TypeError -> m ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
              [ String
"Hiding"
              , String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
", " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (ImportedName' n m -> String) -> [ImportedName' n m] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ImportedName' n m -> String
forall a. Pretty a => a -> String
prettyShow [ImportedName' n m]
uselessHiding
              , String
"has no effect"
              ]
          -- 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' n m -> m (ImportDirective' n m)
forall (m :: * -> *) a. Monad m => a -> m a
return ImportDirective' n m
dir{ hiding :: [ImportedName' n m]
hiding = [] }
      ImportDirective' n m
dir -> ImportDirective' n m -> m (ImportDirective' n m)
forall (m :: * -> *) a. Monad m => a -> m a
return ImportDirective' n m
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' Name Name] -> [ImportedName' Name Name])
-> 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' Name Name -> [ImportedName' Name Name])
-> [ImportedName' Name Name] -> [ImportedName' Name Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ImportedName' Name Name -> [ImportedName' Name Name]
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' Name Name]
hiding      = (ImportedName' Name Name -> [ImportedName' Name Name])
-> [ImportedName' Name Name] -> [ImportedName' Name Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ImportedName' Name Name -> [ImportedName' Name Name]
addExtra            ([ImportedName' Name Name] -> [ImportedName' Name Name])
-> [ImportedName' Name Name] -> [ImportedName' Name Name]
forall a b. (a -> b) -> a -> b
$ ImportDirective -> [ImportedName' Name Name]
forall n m. ImportDirective' n m -> [ImportedName' 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 -> [Renaming' n m]
impRenaming ImportDirective
dir
         }
      where
        addExtra :: ImportedName' Name Name -> [ImportedName' Name Name]
addExtra f :: ImportedName' Name Name
f@(ImportedName Name
y) | Name -> Bool
extra Name
y = [ImportedName' Name Name
f, Name -> ImportedName' Name Name
forall n m. m -> ImportedName' n m
ImportedModule Name
y]
        addExtra ImportedName' Name Name
m = [ImportedName' Name Name
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' Name Name
-> ImportedName' Name Name -> Maybe Fixity -> Range -> Renaming
forall n m.
ImportedName' n m
-> ImportedName' n m -> Maybe Fixity -> Range -> Renaming' n m
Renaming (Name -> ImportedName' Name Name
forall n m. m -> ImportedName' n m
ImportedModule Name
y) (Name -> ImportedName' Name Name
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)

    -- | 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' Name Name]
-> ([ImportedName' Name Name],
    [ImportedName' (Name, QName) (Name, ModuleName)])
checkExist [ImportedName' Name Name]
xs = [Either
   (ImportedName' Name Name)
   (ImportedName' (Name, QName) (Name, ModuleName))]
-> ([ImportedName' Name Name],
    [ImportedName' (Name, QName) (Name, ModuleName)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either
    (ImportedName' Name Name)
    (ImportedName' (Name, QName) (Name, ModuleName))]
 -> ([ImportedName' Name Name],
     [ImportedName' (Name, QName) (Name, ModuleName)]))
-> [Either
      (ImportedName' Name Name)
      (ImportedName' (Name, QName) (Name, ModuleName))]
-> ([ImportedName' Name Name],
    [ImportedName' (Name, QName) (Name, ModuleName)])
forall a b. (a -> b) -> a -> b
$ [ImportedName' Name Name]
-> (ImportedName' Name Name
    -> Either
         (ImportedName' Name Name)
         (ImportedName' (Name, QName) (Name, ModuleName)))
-> [Either
      (ImportedName' Name Name)
      (ImportedName' (Name, QName) (Name, ModuleName))]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [ImportedName' Name Name]
xs ((ImportedName' Name Name
  -> Either
       (ImportedName' Name Name)
       (ImportedName' (Name, QName) (Name, ModuleName)))
 -> [Either
       (ImportedName' Name Name)
       (ImportedName' (Name, QName) (Name, ModuleName))])
-> (ImportedName' Name Name
    -> Either
         (ImportedName' Name Name)
         (ImportedName' (Name, QName) (Name, ModuleName)))
-> [Either
      (ImportedName' Name Name)
      (ImportedName' (Name, QName) (Name, ModuleName))]
forall a b. (a -> b) -> a -> b
$ \ ImportedName' Name Name
name -> case ImportedName' Name Name
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 t. SetRange t => Range -> t -> t
setRange (Name -> Range
forall t. HasRange t => t -> 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' Name Name) AbstractName
-> Either
     (ImportedName' Name Name)
     (ImportedName' (Name, QName) (Name, ModuleName))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ImportedName' Name Name
-> Name
-> NamesInScope
-> Either (ImportedName' Name Name) AbstractName
forall a err b. Ord a => err -> a -> Map a [b] -> Either err b
resolve ImportedName' Name Name
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 t. SetRange t => Range -> t -> t
setRange (Name -> Range
forall t. HasRange t => t -> 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' Name Name) AbstractModule
-> Either
     (ImportedName' Name Name)
     (ImportedName' (Name, QName) (Name, ModuleName))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ImportedName' Name Name
-> Name
-> ModulesInScope
-> Either (ImportedName' Name Name) AbstractModule
forall a err b. Ord a => err -> a -> Map a [b] -> Either err b
resolve ImportedName' Name Name
name Name
x ModulesInScope
modulesInScope

      where resolve :: Ord a => err -> a -> Map a [b] -> Either err b
            resolve :: 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 :: [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 [ImportedName' n1 m1]
h [Renaming' n1 m1]
ren Maybe Range
open) =
  Range
-> Using' n2 m2
-> [ImportedName' n2 m2]
-> [Renaming' n2 m2]
-> Maybe Range
-> ImportDirective' n2 m2
forall n m.
Range
-> Using' n m
-> [ImportedName' n m]
-> [Renaming' n m]
-> Maybe Range
-> ImportDirective' n m
ImportDirective Range
r
    (([ImportedName' n1 m1] -> [ImportedName' 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)
-> [ImportedName' n1 m1] -> [ImportedName' 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)
-> [ImportedName' n1 m1] -> [ImportedName' 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) [ImportedName' n1 m1]
h)
    ((Renaming' n1 m1 -> Renaming' n2 m2)
-> [Renaming' n1 m1] -> [Renaming' 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) [Renaming' 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
  { ImportedNameMap n1 n2 m1 m2 -> Map n1 n2
inameMap   :: Map n1 n2
  , 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 :: [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 :: 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 :: 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 -> Scope) -> (Scope -> Scope) -> Scope -> Scope
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                Scope -> Scope
restrictPrivate (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) -> ScopeM ()
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.
  ScopeM ()
checkForClashes

  -- Importing names might shadow existing locals.
  String -> Int -> ScopeM () -> ScopeM ()
forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
verboseS String
"scope.locals" Int
10 (ScopeM () -> ScopeM ()) -> ScopeM () -> ScopeM ()
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] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
List.intersect [Name]
locals [Name]
newdefs
    String -> Int -> String -> ScopeM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"scope.locals" Int
10 (String -> ScopeM ()) -> String -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ String
"opening module shadows the following locals vars: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Pretty a => a -> String
prettyShow [Name]
shadowed
  -- Andreas, 2014-09-03, issue 1266: shadow local variables by imported defs.
  (LocalVars -> LocalVars) -> ScopeM ()
modifyLocalVars ((LocalVars -> LocalVars) -> ScopeM ())
-> (LocalVars -> LocalVars) -> ScopeM ()
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 :: ScopeM ()
checkForClashes = Bool -> ScopeM () -> ScopeM ()
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) (ScopeM () -> ScopeM ()) -> ScopeM () -> ScopeM ()
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 (KindOfName -> KindOfName -> Bool
forall a. Eq a => a -> a -> Bool
== KindOfName
ConName) [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])] -> ScopeM ()) -> ScopeM ()
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])] -> ScopeM ()) -> ScopeM ())
-> ([(Name, [AbstractName])] -> ScopeM ()) -> ScopeM ()
forall a b. (a -> b) -> a -> b
$
          \ ((Name
x, AbstractName
q:[AbstractName]
_) : [(Name, [AbstractName])]
_) -> TypeError -> ScopeM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> ScopeM ()) -> TypeError -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ QName -> QName -> TypeError
ClashingDefinition (Name -> QName
C.QName Name
x) (QName -> TypeError) -> QName -> TypeError
forall a b. (a -> b) -> a -> b
$ AbstractName -> QName
anameName AbstractName
q

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