{-# LANGUAGE NondecreasingIndentation #-}

{-| The scope monad with operations.
-}

module Agda.Syntax.Scope.Monad where

import Prelude hiding (null)

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

import Data.Either ( partitionEithers )
import Data.Foldable (all, traverse_)
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Traversable hiding (for)

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

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

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

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

import Agda.Utils.Impossible

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

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

-- Debugging

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

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

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

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

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

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

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

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

withCurrentModule' :: (MonadTrans t, Monad (t ScopeM)) => A.ModuleName -> t ScopeM a -> t ScopeM a
withCurrentModule' :: forall (t :: (* -> *) -> * -> *) a.
(MonadTrans t, Monad (t (TCMT IO))) =>
ModuleName -> t (TCMT IO) a -> t (TCMT IO) a
withCurrentModule' ModuleName
new t (TCMT IO) a
action = do
  ModuleName
old <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule
  forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadTCState m => ModuleName -> m ()
setCurrentModule ModuleName
new
  a
x   <- t (TCMT IO) a
action
  forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadTCState m => ModuleName -> m ()
setCurrentModule ModuleName
old
  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 <- forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ModuleName
m (ScopeInfo
scope forall o i. o -> Lens' i o -> i
^. Lens' (Map ModuleName Scope) ScopeInfo
scopeModules) of
    Just Scope
s  -> forall (m :: * -> *) a. Monad m => a -> m a
return Scope
s
    Maybe Scope
Nothing -> do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"" Int
0 forall a b. (a -> b) -> a -> b
$ [Char]
"ERROR: In scope\n" forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow ScopeInfo
scope forall a. [a] -> [a] -> [a]
++ [Char]
"\nNO SUCH SCOPE " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow ModuleName
m
      forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | Look up the abstract name referred to by a given concrete name.
resolveName :: C.QName -> ScopeM ResolvedName
resolveName :: QName -> ScopeM ResolvedName
resolveName = KindsOfNames -> Maybe (Set Name) -> QName -> ScopeM ResolvedName
resolveName' KindsOfNames
allKindsOfNames 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 = forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (forall (m :: * -> *).
(ReadTCState m, HasBuiltins m, MonadError AmbiguousNameReason m) =>
KindsOfNames -> Maybe (Set Name) -> QName -> m ResolvedName
tryResolveName KindsOfNames
kinds Maybe (Set Name)
names QName
x) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Left AmbiguousNameReason
reason  -> do
    forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> Int -> a -> m ()
reportS [Char]
"scope.resolve" Int
60 forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines forall a b. (a -> b) -> a -> b
$
      [Char]
"resolveName': ambiguous name" forall a. a -> [a] -> [a]
:
      forall a b. (a -> b) -> [a] -> [b]
map (forall a. Show a => a -> [Char]
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName) (forall l. IsList l => l -> [Item l]
toList forall a b. (a -> b) -> a -> b
$ AmbiguousNameReason -> List2 QName
ambiguousNamesInReason AmbiguousNameReason
reason)
    forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange QName
x forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousNameReason -> TypeError
AmbiguousName QName
x AmbiguousNameReason
reason
  Right ResolvedName
x' -> forall (m :: * -> *) a. Monad m => a -> m a
return ResolvedName
x'

tryResolveName
  :: forall m. (ReadTCState m, HasBuiltins m, MonadError AmbiguousNameReason m)
  => KindsOfNames       -- ^ Restrict search to these kinds of names.
  -> Maybe (Set A.Name) -- ^ Unless 'Nothing', restrict search to match any of these names.
  -> C.QName            -- ^ Name to be resolved
  -> m ResolvedName     -- ^ If illegally ambiguous, throw error with the ambiguous name.
tryResolveName :: forall (m :: * -> *).
(ReadTCState m, HasBuiltins m, MonadError AmbiguousNameReason m) =>
KindsOfNames -> Maybe (Set Name) -> QName -> m ResolvedName
tryResolveName KindsOfNames
kinds Maybe (Set Name)
names QName
x = do
  ScopeInfo
scope <- forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  let vars :: AssocList QName LocalVar
vars     = forall k k' v. (k -> k') -> AssocList k v -> AssocList k' v
AssocList.mapKeysMonotonic Name -> QName
C.QName forall a b. (a -> b) -> a -> b
$ ScopeInfo
scope forall o i. o -> Lens' i o -> i
^. Lens' LocalVars ScopeInfo
scopeLocals
  case 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 var :: LocalVar
var@(LocalVar Name
y BindingSource
b [AbstractName]
ys) ->
      -- We may ignore the imports filtered out by the @names@ filter.
      case forall a. [a] -> Maybe (NonEmpty a)
nonEmpty forall a b. (a -> b) -> a -> b
$ forall a. (a -> AbstractName) -> [a] -> [a]
filterNames forall a. a -> a
id [AbstractName]
ys of
        Maybe (List1 AbstractName)
Nothing  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name -> BindingSource -> ResolvedName
VarName Name
y{ nameConcrete :: Name
nameConcrete = QName -> Name
unqualify QName
x } BindingSource
b
        Just List1 AbstractName
ys' -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ LocalVar -> List1 AbstractName -> AmbiguousNameReason
AmbiguousLocalVar LocalVar
var List1 AbstractName
ys'

    -- Case: we do not have a local variable x.
    Maybe LocalVar
Nothing -> do
      -- Consider only names that are in the given set of names and
      -- are of one of the given kinds
      let filtKind :: [(AbstractName, Access)] -> [(AbstractName, Access)]
filtKind = forall a. (a -> Bool) -> [a] -> [a]
filter forall a b. (a -> b) -> a -> b
$ (KindOfName -> KindsOfNames -> Bool
`elemKindsOfNames` KindsOfNames
kinds) forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> KindOfName
anameKind forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst
          possibleNames :: QName -> [(AbstractName, Access)]
possibleNames QName
z = [(AbstractName, Access)] -> [(AbstractName, Access)]
filtKind forall a b. (a -> b) -> a -> b
$ forall a. (a -> AbstractName) -> [a] -> [a]
filterNames forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. InScope a => QName -> ScopeInfo -> [(a, Access)]
scopeLookup' QName
z ScopeInfo
scope
      -- If the name has a suffix, also consider the possibility that
      -- the base name is in scope (e.g. the builtin sorts `Set` and `Prop`).
      QName -> Bool
canHaveSuffix <- forall (m :: * -> *). HasBuiltins m => m (QName -> Bool)
canHaveSuffixTest
      let (Maybe Suffix
xsuffix, QName
xbase) = (Lens' Name QName
C.lensQNameName forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' (Maybe Suffix) Name
nameSuffix) (,forall a. Maybe a
Nothing) QName
x
          possibleBaseNames :: [(AbstractName, Access)]
possibleBaseNames = forall a. (a -> Bool) -> [a] -> [a]
filter (QName -> Bool
canHaveSuffix forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> QName
anameName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ QName -> [(AbstractName, Access)]
possibleNames QName
xbase
          suffixedNames :: Maybe (Suffix, NonEmpty (AbstractName, Access))
suffixedNames = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Suffix -> Maybe Suffix
fromConcreteSuffix Maybe Suffix
xsuffix forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. [a] -> Maybe (NonEmpty a)
nonEmpty [(AbstractName, Access)]
possibleBaseNames
      case (forall a. [a] -> Maybe (NonEmpty a)
nonEmpty forall a b. (a -> b) -> a -> b
$ QName -> [(AbstractName, Access)]
possibleNames QName
x) of
        Just NonEmpty (AbstractName, Access)
ds  | let ks :: NonEmpty (Maybe Induction)
ks = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (KindOfName -> Maybe Induction
isConName forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> KindOfName
anameKind forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) NonEmpty (AbstractName, Access)
ds
                 , forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. Maybe a -> Bool
isJust NonEmpty (Maybe Induction)
ks
                 , forall a. Maybe a -> Bool
isNothing Maybe (Suffix, NonEmpty (AbstractName, Access))
suffixedNames ->
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Set Induction -> List1 AbstractName -> ResolvedName
ConstructorName (forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a. List1 (Maybe a) -> [a]
List1.catMaybes NonEmpty (Maybe Induction)
ks) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (AbstractName -> AbstractName
upd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) NonEmpty (AbstractName, Access)
ds

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

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

        Just ((AbstractName
d, Access
a) :| [(AbstractName, Access)]
ds) -> case (Maybe (Suffix, NonEmpty (AbstractName, Access))
suffixedNames, [(AbstractName, Access)]
ds) of
          (Maybe (Suffix, NonEmpty (AbstractName, Access))
Nothing, []) ->
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Access -> AbstractName -> Suffix -> ResolvedName
DefinedName Access
a (AbstractName -> AbstractName
upd AbstractName
d) Suffix
A.NoSuffix
          (Maybe (Suffix, NonEmpty (AbstractName, Access))
Nothing, (AbstractName
d',Access
_) : [(AbstractName, Access)]
ds') ->
            forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ List2 AbstractName -> AmbiguousNameReason
AmbiguousDeclName forall a b. (a -> b) -> a -> b
$ forall a. a -> a -> [a] -> List2 a
List2 AbstractName
d AbstractName
d' forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(AbstractName, Access)]
ds'
          (Just (Suffix
_, NonEmpty (AbstractName, Access)
ss), [(AbstractName, Access)]
_) ->
            forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ List2 AbstractName -> AmbiguousNameReason
AmbiguousDeclName forall a b. (a -> b) -> a -> b
$ forall a. List1 a -> List1 a -> List2 a
List2.append (AbstractName
d forall a. a -> [a] -> NonEmpty a
:| forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(AbstractName, Access)]
ds) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst NonEmpty (AbstractName, Access)
ss)

        Maybe (NonEmpty (AbstractName, Access))
Nothing -> case Maybe (Suffix, NonEmpty (AbstractName, Access))
suffixedNames of
          Maybe (Suffix, NonEmpty (AbstractName, Access))
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ResolvedName
UnknownName
          Just (Suffix
suffix , (AbstractName
d, Access
a) :| []) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Access -> AbstractName -> Suffix -> ResolvedName
DefinedName Access
a (AbstractName -> AbstractName
upd AbstractName
d) Suffix
suffix
          Just (Suffix
suffix , (AbstractName
d1,Access
_) :| (AbstractName
d2,Access
_) : [(AbstractName, Access)]
sds) ->
            forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ List2 AbstractName -> AmbiguousNameReason
AmbiguousDeclName forall a b. (a -> b) -> a -> b
$ forall a. a -> a -> [a] -> List2 a
List2 AbstractName
d1 AbstractName
d2 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(AbstractName, Access)]
sds

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

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

-- | Look up a module in the scope.
resolveModule :: C.QName -> ScopeM AbstractModule
resolveModule :: QName -> ScopeM AbstractModule
resolveModule QName
x = do
  [AbstractModule]
ms <- forall a. InScope a => QName -> ScopeInfo -> [a]
scopeLookup QName
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (forall a. [a] -> Maybe (NonEmpty a)
nonEmpty [AbstractModule]
ms) (forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ QName -> TypeError
NoSuchModule QName
x) forall a b. (a -> b) -> a -> b
$ \ case
    AbsModule ModuleName
m WhyInScope
why :| [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ModuleName -> WhyInScope -> AbstractModule
AbsModule (ModuleName
m forall t u. (SetRange t, HasRange u) => t -> u -> t
`withRangeOf` QName
x) WhyInScope
why
    NonEmpty AbstractModule
ms                    -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ QName -> List1 ModuleName -> TypeError
AmbiguousModule QName
x (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 = forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Fixity'
noFixity' Name
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a ScopeInfo -> m a
useScope Lens' Fixities 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 = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a ScopeInfo -> m a
useScope Lens' Polarities ScopeInfo
scopePolarities

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

-- | Collect the fixity/syntax declarations and polarity pragmas from the list
--   of declarations and store them in the scope.
computeFixitiesAndPolarities :: DoWarn -> [C.Declaration] -> ScopeM a -> ScopeM a
computeFixitiesAndPolarities :: forall a. DoWarn -> [Declaration] -> ScopeM a -> ScopeM a
computeFixitiesAndPolarities DoWarn
warn [Declaration]
ds ScopeM a
cont = do
  (Fixities, Polarities)
fp <- forall (m :: * -> *).
MonadFixityError m =>
DoWarn -> [Declaration] -> m (Fixities, Polarities)
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.
  forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a ScopeInfo -> (a -> a) -> m b -> m b
locallyScope Lens' (Fixities, Polarities) ScopeInfo
scopeFixitiesAndPolarities (forall a b. a -> b -> a
const (Fixities, Polarities)
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 (forall a. a -> Maybe a
Just Set Name
ns) QName
x
  case ResolvedName
r of
    VarName Name
y BindingSource
_         -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Name -> NewNotation
namesToNotation QName
x Name
y
    DefinedName Access
_ AbstractName
d Suffix
_   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AbstractName -> NewNotation
notation AbstractName
d
    FieldName List1 AbstractName
ds        -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ List1 AbstractName -> NewNotation
oneNotation List1 AbstractName
ds
    ConstructorName Set Induction
_ List1 AbstractName
ds-> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ List1 AbstractName -> NewNotation
oneNotation List1 AbstractName
ds
    PatternSynResName List1 AbstractName
n -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ List1 AbstractName -> NewNotation
oneNotation List1 AbstractName
n
    ResolvedName
UnknownName         -> forall a. HasCallStack => a
__IMPOSSIBLE__
  where
    notation :: AbstractName -> NewNotation
notation = QName -> Name -> NewNotation
namesToNotation QName
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> QName
anameName
    oneNotation :: List1 AbstractName -> NewNotation
oneNotation List1 AbstractName
ds =
      case [NewNotation] -> [NewNotation]
mergeNotations forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map AbstractName -> NewNotation
notation forall a b. (a -> b) -> a -> b
$ forall l. IsList l => l -> [Item l]
List1.toList List1 AbstractName
ds of
        [NewNotation
n] -> NewNotation
n
        [NewNotation]
_   -> forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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

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

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

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

-- | Rebind a name. Use with care!
--   Ulf, 2014-06-29: Currently used to rebind the name defined by an
--   unquoteDecl, which is a 'QuotableName' in the body, but a 'DefinedName'
--   later on.
rebindName :: Access -> KindOfName -> C.Name -> A.QName -> ScopeM ()
rebindName :: Access -> KindOfName -> Name -> QName -> TCMT IO ()
rebindName Access
acc KindOfName
kind Name
x QName
y = do
  if KindOfName
kind forall a. Eq a => a -> a -> Bool
== KindOfName
ConName
    then (Scope -> Scope) -> TCMT IO ()
modifyCurrentScope forall a b. (a -> b) -> a -> b
$
           NameSpaceId
-> (NamesInScope -> NamesInScope)
-> (ModulesInScope -> ModulesInScope)
-> (InScopeSet -> InScopeSet)
-> Scope
-> Scope
mapScopeNS (Access -> NameSpaceId
localNameSpace Access
acc)
                      (forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update (forall l. IsList l => l -> [Item l]
toList forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall a. [a] -> Maybe (NonEmpty a)
nonEmpty forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
(==) KindOfName
ConName forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> KindOfName
anameKind))) Name
x)
                      forall a. a -> a
id
                      forall a. a -> a
id
    else (Scope -> Scope) -> TCMT IO ()
modifyCurrentScope forall a b. (a -> b) -> a -> b
$ NameSpaceId -> Name -> Scope -> Scope
removeNameFromScope (Access -> NameSpaceId
localNameSpace Access
acc) Name
x
  Access -> KindOfName -> Name -> QName -> TCMT IO ()
bindName Access
acc KindOfName
kind Name
x QName
y

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

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

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

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

type WSM = StateT ScopeMemo ScopeM

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

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

-- | Create a new scope with the given name from an old scope. Renames
--   public names in the old scope to match the new name and returns the
--   renamings.
copyScope :: C.QName -> A.ModuleName -> Scope -> ScopeM (Scope, ScopeCopyInfo)
copyScope :: QName -> ModuleName -> Scope -> ScopeM (Scope, ScopeCopyInfo)
copyScope QName
oldc ModuleName
new0 Scope
s = ((WhyInScope -> WhyInScope) -> Scope -> Scope
inScopeBecause (QName -> WhyInScope -> WhyInScope
Applied QName
oldc) forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** ScopeMemo -> ScopeCopyInfo
memoToScopeInfo) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (ModuleName -> Scope -> WSM Scope
copy ModuleName
new0 Scope
s) (Ren QName -> Map ModuleName (ModuleName, Bool) -> ScopeMemo
ScopeMemo forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty)
  where
    copy :: A.ModuleName -> Scope -> WSM Scope
    copy :: ModuleName -> Scope -> WSM Scope
copy ModuleName
new Scope
s = do
      forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.copy" Int
20 forall a b. (a -> b) -> a -> b
$ [Char]
"Copying scope " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow ModuleName
old forall a. [a] -> [a] -> [a]
++ [Char]
" to " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow ModuleName
new
      forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.copy" Int
50 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> [Char]
prettyShow Scope
s
      Scope
s0 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
Applicative m =>
(NamesInScope -> m NamesInScope)
-> (ModulesInScope -> m ModulesInScope)
-> (InScopeSet -> m InScopeSet)
-> Scope
-> m Scope
mapScopeM_ NamesInScope -> WSM NamesInScope
copyD ModulesInScope -> WSM ModulesInScope
copyM forall (m :: * -> *) a. Monad m => a -> m a
return (NameSpaceId -> NameSpace -> Scope -> Scope
setNameSpace NameSpaceId
PrivateNS NameSpace
emptyNameSpace Scope
s)
      -- Fix name and parent.
      forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall a. HasRange a => a -> Range
getRange ModuleName
new
        new' :: ModuleName
new' = 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 -> WSM NamesInScope
copyD = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a b. (a -> b) -> a -> b
$ (QName -> WSM QName) -> AbstractName -> WSM AbstractName
onName QName -> WSM QName
renName

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

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

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

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

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

        -- Change a binding M.x -> old.M'.y to M.x -> new.M'.y
        renName :: A.QName -> WSM A.QName
        renName :: QName -> WSM QName
renName QName
x = do
          -- Issue 1985: For re-exported names we can't use new' as the
          -- module, since it has the wrong telescope. Example:
          --
          --    module M1 (A : Set) where
          --      module M2 (B : Set) where
          --        postulate X : Set
          --      module M3 (C : Set) where
          --        module M4 (D E : Set) where
          --          open M2 public
          --
          --    module M = M1.M3 A C
          --
          -- Here we can't copy M1.M2.X to M.M4.X since we need
          -- X : (B : Set) → Set, but M.M4 has telescope (D E : Set). Thus, we
          -- would break the invariant that all functions in a module share the
          -- module telescope. Instead we copy M1.M2.X to M.M2.X for a fresh
          -- module M2 that gets the right telescope.
          ModuleName
m <- if QName
x QName -> ModuleName -> Bool
`isInModule` ModuleName
old
                 then forall (m :: * -> *) a. Monad m => a -> m a
return ModuleName
new'
                 else Bool -> ModuleName -> WSM 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 <- forall a. SetRange a => Range -> a -> a
setRange Range
rnew forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> Name -> QName
A.qualify ModuleName
m forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> WSM Name
refresh (QName -> Name
qnameName QName
x)
          forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.copy" Int
50 forall a b. (a -> b) -> a -> b
$ [Char]
"  Copying " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
x forall a. [a] -> [a] -> [a]
++ [Char]
" to " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
y
          forall {m :: * -> *}.
MonadState ScopeMemo m =>
QName -> QName -> m ()
addName QName
x QName
y
          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 -> WSM ModuleName
renMod = Bool -> ModuleName -> WSM ModuleName
renMod' Bool
True

        renMod' :: Bool -> ModuleName -> WSM ModuleName
renMod' Bool
rec ModuleName
x = do
          -- Andreas, issue 1607:
          -- If we have already copied this module, return the copy.
          Maybe (ModuleName, Bool)
z <- forall {m :: * -> *}.
MonadState ScopeMemo m =>
ModuleName -> m (Maybe (ModuleName, Bool))
findMod ModuleName
x
          case Maybe (ModuleName, Bool)
z of
            Just (ModuleName
y, Bool
False) | Bool
rec -> ModuleName
y forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ModuleName -> ModuleName -> StateT ScopeMemo (TCMT IO) ()
copyRec ModuleName
x ModuleName
y
            Just (ModuleName
y, Bool
_)           -> 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 forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> a
lastWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ ModuleName -> [Name]
A.mnameToList ModuleName
x
               forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Name] -> ModuleName
A.mnameFromList forall a b. (a -> b) -> a -> b
$ [Name]
newM 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 forall a. Eq a => a -> a -> Bool
== ModuleName
y) then forall (m :: * -> *) a. Monad m => a -> m a
return ModuleName
x else do
            forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.copy" Int
50 forall a b. (a -> b) -> a -> b
$ [Char]
"  Copying module " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow ModuleName
x forall a. [a] -> [a] -> [a]
++ [Char]
" to " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow ModuleName
y
            forall {m :: * -> *}.
MonadState ScopeMemo m =>
ModuleName -> ModuleName -> Bool -> m ()
addMod ModuleName
x ModuleName
y Bool
rec
            forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Maybe DataOrRecordModule -> ModuleName -> TCMT IO ()
createModule forall a. Maybe a
Nothing ModuleName
y
            -- We need to copy the contents of included modules recursively (only when 'rec')
            forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
rec forall a b. (a -> b) -> a -> b
$ ModuleName -> ModuleName -> StateT ScopeMemo (TCMT IO) ()
copyRec ModuleName
x ModuleName
y
            forall (m :: * -> *) a. Monad m => a -> m a
return ModuleName
y
          where
            copyRec :: ModuleName -> ModuleName -> StateT ScopeMemo (TCMT IO) ()
copyRec ModuleName
x ModuleName
y = do
              Scope
s0 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ ModuleName -> ScopeM Scope
getNamedScope ModuleName
x
              Scope
s  <- forall (t :: (* -> *) -> * -> *) a.
(MonadTrans t, Monad (t (TCMT IO))) =>
ModuleName -> t (TCMT IO) a -> t (TCMT IO) a
withCurrentModule' ModuleName
y forall a b. (a -> b) -> a -> b
$ ModuleName -> Scope -> WSM Scope
copy ModuleName
y Scope
s0
              forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ ModuleName -> (Scope -> Scope) -> TCMT IO ()
modifyNamedScope ModuleName
y (forall a b. a -> b -> a
const Scope
s)

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

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

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

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

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

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

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

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

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

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

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

    -- Efficient test of whether a module import should be added to the import
    -- of a definition (like a data or record definition).
    let extra :: Name -> Bool
extra Name
x = ImportedName -> Bool
inNames (forall n m. n -> ImportedName' n m
ImportedName   Name
x)
               Bool -> Bool -> Bool
&& ImportedName -> Bool
notMissing (forall n m. m -> ImportedName' n m
ImportedModule Name
x)
               Bool -> Bool -> Bool
&& (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. ImportedName -> Bool
inNames forall a b. (a -> b) -> a -> b
$ 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' <- forall {m :: * -> *} {m}.
MonadWarning m =>
(ImportedName' Name m -> Bool)
-> ImportDirective -> m ImportDirective
sanityCheck (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. ImportedName -> Bool
inNames) 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.
    forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull (forall a. Ord a => [a] -> [a]
allDuplicates [ImportedName]
targetNames) forall a b. (a -> b) -> a -> b
$ \ [ImportedName]
dup ->
      forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ QName -> [ImportedName] -> TypeError
DuplicateImports QName
m [ImportedName]
dup

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

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

    -- Look up the defined names in the new scope.
    let namesInScope' :: NamesInScope
namesInScope'   = (forall a. InScope a => Scope -> ThingsInScope a
allNamesInScope Scope
scope' :: ThingsInScope AbstractName)
    let modulesInScope' :: ModulesInScope
modulesInScope' = (forall a. InScope a => Scope -> ThingsInScope a
allNamesInScope Scope
scope' :: ThingsInScope AbstractModule)
    let look :: k -> Map k [c] -> c
look k
x = forall a. a -> [a] -> a
headWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault 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 = forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [ImportedName]
definedNames forall a b. (a -> b) -> a -> b
$ \case
          ImportedName   Name
x -> forall n m. n -> ImportedName' n m
ImportedName   forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name
x,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SetRange a => Range -> a -> a
setRange (forall a. HasRange a => a -> Range
getRange Name
x) forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> QName
anameName forall a b. (a -> b) -> a -> b
$ forall {k} {c}. Ord k => k -> Map k [c] -> c
look Name
x NamesInScope
namesInScope'
          ImportedModule Name
x -> forall n m. m -> ImportedName' n m
ImportedModule forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name
x,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SetRange a => Range -> a -> a
setRange (forall a. HasRange a => a -> Range
getRange Name
x) forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractModule -> ModuleName
amodName  forall a b. (a -> b) -> a -> b
$ forall {k} {c}. Ord k => k -> Map k [c] -> c
look Name
x ModulesInScope
modulesInScope'

    let adir :: ImportDirective
adir = 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
    forall (m :: * -> *) a. Monad m => a -> m a
return (ImportDirective
adir, Scope
scope') -- TODO Issue 1714: adir

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

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

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

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

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

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

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

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

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

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

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

-- | Create a 'ImportedNameMap'.
importedNameMapFromList
  :: (Ord n1, Ord m1)
  => [ImportedName' (n1,n2) (m1,m2)]
  -> ImportedNameMap n1 n2 m1 m2
importedNameMapFromList :: forall n1 m1 n2 m2.
(Ord n1, Ord m1) =>
[ImportedName' (n1, n2) (m1, m2)] -> ImportedNameMap n1 n2 m1 m2
importedNameMapFromList = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a b c. (a -> b -> c) -> b -> a -> c
flip 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) forall a b. (a -> b) -> a -> b
$ forall n1 n2 m1 m2.
Map n1 n2 -> Map m1 m2 -> ImportedNameMap n1 n2 m1 m2
ImportedNameMap forall k a. Map k a
Map.empty 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) -> forall n1 n2 m1 m2.
Map n1 n2 -> Map m1 m2 -> ImportedNameMap n1 n2 m1 m2
ImportedNameMap (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) -> forall n1 n2 m1 m2.
Map n1 n2 -> Map m1 m2 -> ImportedNameMap n1 n2 m1 m2
ImportedNameMap Map n1 n2
nm (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert m1
x m2
y Map m1 m2
mm)

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

-- | Translation of @Renaming@.
mapRenaming
  ::  (Ord n1, Ord m1)
  => ImportedNameMap n1 n2 m1 m2  -- ^ Translation of 'renFrom' names and module names.
  -> ImportedNameMap n1 n2 m1 m2  -- ^ Translation of 'rento'   names and module names.
  -> Renaming' n1 m1  -- ^ Renaming before translation (1).
  -> Renaming' n2 m2  -- ^ Renaming after  translation (2).
mapRenaming :: forall n1 m1 n2 m2.
(Ord n1, Ord m1) =>
ImportedNameMap n1 n2 m1 m2
-> ImportedNameMap n1 n2 m1 m2
-> Renaming' n1 m1
-> Renaming' n2 m2
mapRenaming ImportedNameMap n1 n2 m1 m2
src ImportedNameMap n1 n2 m1 m2
tgt (Renaming ImportedName' n1 m1
from ImportedName' n1 m1
to Maybe Fixity
fixity Range
r) =
  forall n m.
ImportedName' n m
-> ImportedName' n m -> Maybe Fixity -> Range -> Renaming' n m
Renaming (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) (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 = 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 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 <- forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule
  ModuleName
m <- forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe ModuleName
mam (AbstractModule -> ModuleName
amodName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ScopeM AbstractModule
resolveModule QName
cm) forall (m :: * -> *) a. Monad m => a -> m a
return
  let acc :: NameSpaceId
acc | Maybe Range
Nothing <- 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WhyInScope -> WhyInScope) -> Scope -> Scope
inScopeBecause (QName -> WhyInScope -> WhyInScope
Opened QName
cm) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                OpenKind -> Scope -> Scope
noGeneralizedVarsIfLetOpen OpenKind
kind forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ModuleName -> ScopeM Scope
getNamedScope ModuleName
m
  let s :: Scope
s  = NameSpaceId -> Scope -> Scope
setScopeAccess NameSpaceId
acc Scope
s'
  let ns :: NameSpace
ns = NameSpaceId -> Scope -> NameSpace
scopeNameSpace NameSpaceId
acc Scope
s
  (Scope -> Scope) -> TCMT IO ()
modifyCurrentScope (Scope -> Scope -> Scope
`mergeScope` Scope
s)
  -- Andreas, 2018-06-03, issue #3057:
  -- If we simply check for ambiguous exported identifiers _after_
  -- importing the new identifiers into the current scope, we also
  -- catch the case of importing an ambiguous identifier.
  TCMT IO ()
checkForClashes

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

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

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

        NameSpace
exported <- Scope -> NameSpace
allThingsInScope forall b c a. (b -> c) -> (a -> b) -> a -> c
. Scope -> Scope
restrictPrivate forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ModuleName -> ScopeM Scope
getNamedScope forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 = forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
_c, [AbstractName]
as) -> forall (t :: * -> *) a. Foldable t => t a -> Int
length [AbstractName]
as forall a. Ord a => a -> a -> Bool
>= Int
2) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList forall a b. (a -> b) -> a -> b
$ NameSpace -> NamesInScope
nsNames NameSpace
exported
            modClashes :: [(Name, [AbstractModule])]
modClashes = forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
_c, [AbstractModule]
as) -> forall (t :: * -> *) a. Foldable t => t a -> Int
length [AbstractModule]
as forall a. Ord a => a -> a -> Bool
>= Int
2) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList 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 or only to pattern synonyms.
            defClash :: (a, [AbstractName]) -> Bool
defClash (a
_, [AbstractName]
qs) = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Bool -> Bool
or
              [ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. KindOfName -> Maybe Induction
isConName) [KindOfName]
ks
              , forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => a -> a -> Bool
== KindOfName
FldName)         [KindOfName]
ks
              , forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => a -> a -> Bool
== KindOfName
PatternSynName)  [KindOfName]
ks
              ]
              where ks :: [KindOfName]
ks = forall a b. (a -> b) -> [a] -> [b]
map AbstractName -> KindOfName
anameKind [AbstractName]
qs
        -- We report the first clashing exported identifier.
        forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull (forall a. (a -> Bool) -> [a] -> [a]
filter forall {a}. (a, [AbstractName]) -> Bool
defClash [(Name, [AbstractName])]
defClashes) forall a b. (a -> b) -> a -> b
$
          \ ((Name
x, AbstractName
q:[AbstractName]
_) : [(Name, [AbstractName])]
_) -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ QName -> QName -> Maybe NiceDeclaration -> TypeError
ClashingDefinition (Name -> QName
C.QName Name
x) (AbstractName -> QName
anameName AbstractName
q) forall a. Maybe a
Nothing

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