{-# LANGUAGE NondecreasingIndentation #-}

{-| The scope monad with operations.
-}

module Agda.Syntax.Scope.Monad where

import Prelude hiding (null)

import Control.Arrow ((***))
import Control.Monad.Except       ( MonadError, throwError, runExceptT )
import Control.Monad.State        ( StateT, runStateT, gets, modify )
import Control.Monad.Trans        ( MonadTrans, lift )
import Control.Monad.Trans.Maybe  ( MaybeT(MaybeT), runMaybeT )
import Control.Applicative

import Data.Either ( partitionEithers )
import Data.Foldable (all, traverse_)
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.HashMap.Strict as HMap
import qualified Data.HashSet as HSet
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.Common.Pretty
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 as I
import Agda.TypeChecking.Monad.Builtin
  ( HasBuiltins, getBuiltinName'
  , builtinProp, builtinSet, builtinStrictSet, builtinPropOmega, 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.Set1 ( Set1 )
import qualified Agda.Utils.Set1 as Set1
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] -> ScopeM ()
printLocals Int
v [Char]
s = [Char] -> Int -> ScopeM () -> ScopeM ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"scope.top" Int
v (ScopeM () -> ScopeM ()) -> ScopeM () -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ do
  locals <- TCMT IO LocalVars
forall (m :: * -> *). ReadTCState m => m LocalVars
getLocalVars
  reportSLn "scope.top" v $ s ++ " " ++ prettyShow locals

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

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

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

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

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

setCurrentModule :: MonadTCState m => A.ModuleName -> m ()
setCurrentModule :: forall (m :: * -> *). MonadTCState m => ModuleName -> m ()
setCurrentModule ModuleName
m = (ScopeInfo -> ScopeInfo) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(ScopeInfo -> ScopeInfo) -> m ()
modifyScope ((ScopeInfo -> ScopeInfo) -> m ())
-> (ScopeInfo -> ScopeInfo) -> m ()
forall a b. (a -> b) -> a -> b
$ Lens' ScopeInfo ModuleName -> LensSet ScopeInfo ModuleName
forall o i. Lens' o i -> LensSet o i
set (ModuleName -> f ModuleName) -> ScopeInfo -> f ScopeInfo
Lens' ScopeInfo ModuleName
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
  old <- m ModuleName
forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule
  setCurrentModule new
  x   <- action
  setCurrentModule old
  return 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
  old <- ScopeM ModuleName -> t (TCMT IO) ModuleName
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ScopeM ModuleName
forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule
  lift $ setCurrentModule new
  x   <- action
  lift $ setCurrentModule old
  return x

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

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

-- | Create a new module with an empty scope.
--   If the module is not new (e.g. duplicate @import@),
--   don't erase its contents.
--   (@Just@ if it is a datatype or record module.)
createModule :: Maybe DataOrRecordModule -> A.ModuleName -> ScopeM ()
createModule :: Maybe DataOrRecordModule -> ModuleName -> ScopeM ()
createModule Maybe DataOrRecordModule
b ModuleName
m = do
  [Char] -> Int -> [Char] -> ScopeM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.createModule" Int
30 ([Char] -> ScopeM ()) -> [Char] -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"createModule " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow ModuleName
m
  s <- ScopeM Scope
getCurrentScope
  let parents = Scope -> ModuleName
scopeName Scope
s ModuleName -> [ModuleName] -> [ModuleName]
forall a. a -> [a] -> [a]
: Scope -> [ModuleName]
scopeParents Scope
s
      sm = Scope
emptyScope { scopeName           = m
                      , scopeParents        = parents
                      , scopeDatatypeModule = 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.
  modifyScopes $ Map.insertWith mergeScope m sm

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | After collecting some variable names in the scopeVarsToBind,
--   bind them all simultaneously.
bindVarsToBind :: ScopeM ()
bindVarsToBind :: ScopeM ()
bindVarsToBind = do
  vars <- TCMT IO LocalVars
getVarsToBind
  modifyLocalVars (vars ++)
  printLocals 30 "bound variables:"
  modifyScope_ $ setVarsToBind []

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

annotateExpr :: ReadTCState m => m A.Expr -> m A.Expr
annotateExpr :: forall (m :: * -> *). ReadTCState m => m Expr -> m Expr
annotateExpr m Expr
m = do
  e <- m Expr
m
  s <- getScope
  return $ A.ScopedExpr s 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
  i <- TCMT IO NameId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
  return $ A.Name
    { nameId          = i
    , nameConcrete    = x
    , nameCanonical   = x
    , nameBindingSite = getRange x
    , nameFixity      = fx
    , nameIsRecordName = 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
  y <- Fixity' -> Name -> ScopeM Name
freshAbstractName Fixity'
fx Name
x
  m <- getCurrentModule
  return $ A.qualify m y

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

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

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

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

-- | Look up the abstract name corresponding to a concrete name of
--   a certain kind and/or from a given set of names.
--   Sometimes we know already that we are dealing with a constructor
--   or pattern synonym (e.g. when we have parsed a pattern).
--   Then, we can ignore conflicting definitions of that name
--   of a different kind. (See issue 822.)
resolveName' ::
  KindsOfNames -> Maybe (Set1 A.Name) -> C.QName -> ScopeM ResolvedName
resolveName' :: KindsOfNames -> Maybe (Set1 Name) -> QName -> ScopeM ResolvedName
resolveName' KindsOfNames
kinds Maybe (Set1 Name)
names QName
x = ExceptT NameResolutionError (TCMT IO) ResolvedName
-> TCMT IO (Either NameResolutionError ResolvedName)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (KindsOfNames
-> Maybe (Set1 Name)
-> QName
-> ExceptT NameResolutionError (TCMT IO) ResolvedName
forall (m :: * -> *).
(ReadTCState m, HasBuiltins m, MonadError NameResolutionError m) =>
KindsOfNames -> Maybe (Set1 Name) -> QName -> m ResolvedName
tryResolveName KindsOfNames
kinds Maybe (Set1 Name)
names QName
x) TCMT IO (Either NameResolutionError ResolvedName)
-> (Either NameResolutionError ResolvedName -> ScopeM ResolvedName)
-> ScopeM ResolvedName
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Left (IllegalAmbiguity AmbiguousNameReason
reason)  -> do
    [Char] -> Int -> [Char] -> ScopeM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> Int -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportS [Char]
"scope.resolve" Int
60 ([Char] -> ScopeM ()) -> [Char] -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
      [Char]
"resolveName': ambiguous name" [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
:
      (QName -> [Char]) -> [QName] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> [Char]
forall a. Show a => a -> [Char]
show (Name -> [Char]) -> (QName -> Name) -> QName -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName) (List2 QName -> [Item (List2 QName)]
forall l. IsList l => l -> [Item l]
toList (List2 QName -> [Item (List2 QName)])
-> List2 QName -> [Item (List2 QName)]
forall a b. (a -> b) -> a -> b
$ AmbiguousNameReason -> List2 QName
ambiguousNamesInReason AmbiguousNameReason
reason)
    QName -> ScopeM ResolvedName -> ScopeM ResolvedName
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange QName
x (ScopeM ResolvedName -> ScopeM ResolvedName)
-> ScopeM ResolvedName -> ScopeM ResolvedName
forall a b. (a -> b) -> a -> b
$ TypeError -> ScopeM ResolvedName
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> ScopeM ResolvedName)
-> TypeError -> ScopeM ResolvedName
forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousNameReason -> TypeError
AmbiguousName QName
x AmbiguousNameReason
reason

  Left (ConstrOfNonRecord QName
q ResolvedName
r) -> case ResolvedName
r of
    ResolvedName
UnknownName -> QName -> ScopeM ResolvedName -> ScopeM ResolvedName
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange QName
x (ScopeM ResolvedName -> ScopeM ResolvedName)
-> ScopeM ResolvedName -> ScopeM ResolvedName
forall a b. (a -> b) -> a -> b
$ TypeError -> ScopeM ResolvedName
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> ScopeM ResolvedName)
-> TypeError -> ScopeM ResolvedName
forall a b. (a -> b) -> a -> b
$ QName -> TypeError
I.NotInScope QName
q
    ResolvedName
_ -> QName -> ScopeM ResolvedName -> ScopeM ResolvedName
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange QName
x (ScopeM ResolvedName -> ScopeM ResolvedName)
-> ScopeM ResolvedName -> ScopeM ResolvedName
forall a b. (a -> b) -> a -> b
$ TypeError -> ScopeM ResolvedName
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> ScopeM ResolvedName)
-> TypeError -> ScopeM ResolvedName
forall a b. (a -> b) -> a -> b
$ ResolvedName -> TypeError
ConstructorNameOfNonRecord ResolvedName
r

  Right ResolvedName
x' -> ResolvedName -> ScopeM ResolvedName
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ResolvedName
x'

tryResolveName :: forall m. (ReadTCState m, HasBuiltins m, MonadError NameResolutionError m)
  => KindsOfNames
       -- ^ Restrict search to these kinds of names.
  -> Maybe (Set1 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 NameResolutionError m) =>
KindsOfNames -> Maybe (Set1 Name) -> QName -> m ResolvedName
tryResolveName KindsOfNames
kinds Maybe (Set1 Name)
names QName
x = do
  scope <- m ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  let
    vars = (Name -> QName) -> LocalVars -> AssocList QName LocalVar
forall k k' v. (k -> k') -> AssocList k v -> AssocList k' v
AssocList.mapKeysMonotonic Name -> QName
C.QName (LocalVars -> AssocList QName LocalVar)
-> LocalVars -> AssocList QName LocalVar
forall a b. (a -> b) -> a -> b
$ ScopeInfo
scope ScopeInfo -> Lens' ScopeInfo LocalVars -> LocalVars
forall o i. o -> Lens' o i -> i
^. (LocalVars -> f LocalVars) -> ScopeInfo -> f ScopeInfo
Lens' ScopeInfo LocalVars
scopeLocals
    throwAmb = NameResolutionError -> m a
forall a. NameResolutionError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (NameResolutionError -> m a)
-> (AmbiguousNameReason -> NameResolutionError)
-> AmbiguousNameReason
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AmbiguousNameReason -> NameResolutionError
IllegalAmbiguity
  case lookup x 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 [AbstractName] -> Maybe (NonEmpty AbstractName)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty ([AbstractName] -> Maybe (NonEmpty AbstractName))
-> [AbstractName] -> Maybe (NonEmpty AbstractName)
forall a b. (a -> b) -> a -> b
$ (AbstractName -> AbstractName) -> [AbstractName] -> [AbstractName]
forall a. (a -> AbstractName) -> [a] -> [a]
filterNames AbstractName -> AbstractName
forall a. a -> a
id [AbstractName]
ys of
        Maybe (NonEmpty AbstractName)
Nothing  -> ResolvedName -> m ResolvedName
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ResolvedName -> m ResolvedName) -> ResolvedName -> m ResolvedName
forall a b. (a -> b) -> a -> b
$ Name -> BindingSource -> ResolvedName
VarName Name
y{ nameConcrete = unqualify x } BindingSource
b
        Just NonEmpty AbstractName
ys' -> AmbiguousNameReason -> m ResolvedName
forall {a}. AmbiguousNameReason -> m a
throwAmb (AmbiguousNameReason -> m ResolvedName)
-> AmbiguousNameReason -> m ResolvedName
forall a b. (a -> b) -> a -> b
$ LocalVar -> NonEmpty AbstractName -> AmbiguousNameReason
AmbiguousLocalVar LocalVar
var NonEmpty AbstractName
ys'

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

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

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

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

        -- Name is of the form r.constructor
        Maybe (NonEmpty (AbstractName, Access))
Nothing | Just QName
r <- QName -> Maybe QName
isRecordConstructor QName
x -> do
          -- We resolve the record name r with no filter, that way we
          -- can know when printing an error message whether r is not in
          -- scope, or whether it's some other type of name, etc.
          recd <- KindsOfNames -> Maybe (Set1 Name) -> QName -> m ResolvedName
forall (m :: * -> *).
(ReadTCState m, HasBuiltins m, MonadError NameResolutionError m) =>
KindsOfNames -> Maybe (Set1 Name) -> QName -> m ResolvedName
tryResolveName KindsOfNames
AllKindsOfNames Maybe (Set1 Name)
forall a. Maybe a
Nothing QName
r

          case recd of
            DefinedName Access
acc AbstractName
abs Suffix
suf -> QName -> m (Maybe (QName, Maybe Induction))
forall (m :: * -> *).
ReadTCState m =>
QName -> m (Maybe (QName, Maybe Induction))
getRecordConstructor (AbstractName -> QName
anameName AbstractName
abs) m (Maybe (QName, Maybe Induction))
-> (Maybe (QName, Maybe Induction) -> m ResolvedName)
-> m ResolvedName
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
              Just (QName
qn, Maybe Induction
ind) -> ResolvedName -> m ResolvedName
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ResolvedName -> m ResolvedName) -> ResolvedName -> m ResolvedName
forall a b. (a -> b) -> a -> b
$ Set1 Induction -> NonEmpty AbstractName -> ResolvedName
ConstructorName (Induction -> Set1 Induction
forall a. a -> NESet a
Set1.singleton (Induction -> Set1 Induction) -> Induction -> Set1 Induction
forall a b. (a -> b) -> a -> b
$ Induction -> Maybe Induction -> Induction
forall a. a -> Maybe a -> a
fromMaybe Induction
Inductive Maybe Induction
ind) (NonEmpty AbstractName -> ResolvedName)
-> NonEmpty AbstractName -> ResolvedName
forall a b. (a -> b) -> a -> b
$
                AbstractName -> NonEmpty AbstractName
forall a. a -> NonEmpty a
List1.singleton (AbstractName -> NonEmpty AbstractName)
-> AbstractName -> NonEmpty AbstractName
forall a b. (a -> b) -> a -> b
$ AbstractName -> AbstractName
upd AbstractName
abs { anameName = qn, anameKind = ConName }
              Maybe (QName, Maybe Induction)
Nothing -> NameResolutionError -> m ResolvedName
forall a. NameResolutionError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (NameResolutionError -> m ResolvedName)
-> NameResolutionError -> m ResolvedName
forall a b. (a -> b) -> a -> b
$ QName -> ResolvedName -> NameResolutionError
ConstrOfNonRecord QName
r ResolvedName
recd
            ResolvedName
_ -> NameResolutionError -> m ResolvedName
forall a. NameResolutionError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (NameResolutionError -> m ResolvedName)
-> NameResolutionError -> m ResolvedName
forall a b. (a -> b) -> a -> b
$ QName -> ResolvedName -> NameResolutionError
ConstrOfNonRecord QName
r ResolvedName
recd

        Maybe (NonEmpty (AbstractName, Access))
Nothing -> case Maybe (Suffix, NonEmpty (AbstractName, Access))
suffixedNames of
          Maybe (Suffix, NonEmpty (AbstractName, Access))
Nothing -> ResolvedName -> m ResolvedName
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ResolvedName
UnknownName
          Just (Suffix
suffix , (AbstractName
d, Access
a) :| []) -> ResolvedName -> m ResolvedName
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ResolvedName -> m ResolvedName) -> ResolvedName -> m ResolvedName
forall a b. (a -> b) -> a -> b
$ Access -> AbstractName -> Suffix -> ResolvedName
DefinedName Access
a (AbstractName -> AbstractName
upd AbstractName
d) Suffix
suffix
          Just (Suffix
suffix , (AbstractName
d1,Access
_) :| (AbstractName
d2,Access
_) : [(AbstractName, Access)]
sds) ->
            AmbiguousNameReason -> m ResolvedName
forall {a}. AmbiguousNameReason -> m a
throwAmb (AmbiguousNameReason -> m ResolvedName)
-> AmbiguousNameReason -> m ResolvedName
forall a b. (a -> b) -> a -> b
$ List2 AbstractName -> AmbiguousNameReason
AmbiguousDeclName (List2 AbstractName -> AmbiguousNameReason)
-> List2 AbstractName -> AmbiguousNameReason
forall a b. (a -> b) -> a -> b
$ AbstractName
-> AbstractName -> [AbstractName] -> List2 AbstractName
forall a. a -> a -> [a] -> List2 a
List2 AbstractName
d1 AbstractName
d2 ([AbstractName] -> List2 AbstractName)
-> [AbstractName] -> List2 AbstractName
forall a b. (a -> b) -> a -> b
$ ((AbstractName, Access) -> AbstractName)
-> [(AbstractName, Access)] -> [AbstractName]
forall a b. (a -> b) -> [a] -> [b]
map (AbstractName, Access) -> AbstractName
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 (Set1 Name)
names of
    Maybe (Set1 Name)
Nothing -> \ a -> AbstractName
f -> [a] -> [a]
forall a. a -> a
id
    Just Set1 Name
ns -> \ a -> AbstractName
f -> (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter ((a -> Bool) -> [a] -> [a]) -> (a -> Bool) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ (Name -> Set1 Name -> Bool
forall a. Ord a => a -> NESet a -> Bool
`Set1.member` Set1 Name
ns) (Name -> Bool) -> (a -> Name) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
A.qnameName (QName -> Name) -> (a -> QName) -> a -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> QName
anameName (AbstractName -> QName) -> (a -> AbstractName) -> a -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> AbstractName
f
    -- lambda-dropped style by intention
  upd :: AbstractName -> AbstractName
upd AbstractName
d = AbstractName -> Name -> AbstractName
updateConcreteName AbstractName
d (Name -> AbstractName) -> Name -> AbstractName
forall a b. (a -> b) -> a -> b
$ QName -> Name
unqualify QName
x
  updateConcreteName :: AbstractName -> C.Name -> AbstractName
  updateConcreteName :: AbstractName -> Name -> AbstractName
updateConcreteName d :: AbstractName
d@(AbsName { anameName :: AbstractName -> QName
anameName = A.QName ModuleName
qm Name
qn }) Name
x =
    AbstractName
d { anameName = A.QName (setRange (getRange x) qm) (qn { nameConcrete = x }) }
  fromConcreteSuffix :: Maybe Suffix -> Maybe Suffix
fromConcreteSuffix = \case
    Maybe Suffix
Nothing              -> Maybe Suffix
forall a. Maybe a
Nothing
    Just C.Prime{}       -> Maybe Suffix
forall a. Maybe a
Nothing
    Just (C.Index Integer
i)     -> Suffix -> Maybe Suffix
forall a. a -> Maybe a
Just (Suffix -> Maybe Suffix) -> Suffix -> Maybe Suffix
forall a b. (a -> b) -> a -> b
$ Integer -> Suffix
A.Suffix Integer
i
    Just (C.Subscript Integer
i) -> Suffix -> Maybe Suffix
forall a. a -> Maybe a
Just (Suffix -> Maybe Suffix) -> Suffix -> Maybe Suffix
forall a b. (a -> b) -> a -> b
$ Integer -> Suffix
A.Suffix Integer
i

-- | Test if a given abstract name can appear with a suffix. Currently
--   only true for the names of builtin sorts.
canHaveSuffixTest :: HasBuiltins m => m (A.QName -> Bool)
canHaveSuffixTest :: forall (m :: * -> *). HasBuiltins m => m (QName -> Bool)
canHaveSuffixTest = do
  builtinProp <- BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinProp
  builtinSet  <- getBuiltinName' builtinSet
  builtinSSet <- getBuiltinName' builtinStrictSet
  builtinPropOmega <- getBuiltinName' builtinPropOmega
  builtinSetOmega <- getBuiltinName' builtinSetOmega
  builtinSSetOmega <- getBuiltinName' builtinSSetOmega
  return $ \QName
x -> QName -> Maybe QName
forall a. a -> Maybe a
Just QName
x Maybe QName -> [Maybe QName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Maybe QName
builtinProp, Maybe QName
builtinSet, Maybe QName
builtinSSet, Maybe QName
builtinPropOmega, 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
  ms <- QName -> ScopeInfo -> [AbstractModule]
forall a. InScope a => QName -> ScopeInfo -> [a]
scopeLookup QName
x (ScopeInfo -> [AbstractModule])
-> TCMT IO ScopeInfo -> TCMT IO [AbstractModule]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  caseMaybe (nonEmpty ms) (typeError $ NoSuchModule x) $ \ case
    AbsModule ModuleName
m WhyInScope
why :| [] -> AbstractModule -> ScopeM AbstractModule
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (AbstractModule -> ScopeM AbstractModule)
-> AbstractModule -> ScopeM AbstractModule
forall a b. (a -> b) -> a -> b
$ ModuleName -> WhyInScope -> AbstractModule
AbsModule (ModuleName
m ModuleName -> QName -> ModuleName
forall t u. (SetRange t, HasRange u) => t -> u -> t
`withRangeOf` QName
x) WhyInScope
why
    NonEmpty AbstractModule
ms                    -> TypeError -> ScopeM AbstractModule
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> ScopeM AbstractModule)
-> TypeError -> ScopeM AbstractModule
forall a b. (a -> b) -> a -> b
$ QName -> List1 ModuleName -> TypeError
AmbiguousModule QName
x ((AbstractModule -> ModuleName)
-> NonEmpty AbstractModule -> List1 ModuleName
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AbstractModule -> ModuleName
amodName NonEmpty AbstractModule
ms)

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

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

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

-- | 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
  fp <- DoWarn
-> [Declaration]
-> TCMT IO (Map Name Fixity', Map Name (List1 Occurrence))
forall (m :: * -> *).
MonadFixityError m =>
DoWarn
-> [Declaration]
-> m (Map Name Fixity', Map Name (List1 Occurrence))
fixitiesAndPolarities DoWarn
warn [Declaration]
ds
  -- Andreas, 2019-08-16:
  -- Since changing fixities and polarities does not affect the name sets,
  -- we do not need to invoke @modifyScope@ here
  -- (which does @recomputeInverseScopeMaps@).
  -- A simple @locallyScope@ is sufficient.
  locallyScope scopeFixitiesAndPolarities (const fp) cont

-- | Get the notation of a name. The name is assumed to be in scope.
getNotation
  :: C.QName
  -> Set1 A.Name
     -- ^ The name must correspond to one of the names in this set.
  -> ScopeM NewNotation
getNotation :: QName -> Set1 Name -> ScopeM NewNotation
getNotation QName
x Set1 Name
ns = do
  r <- KindsOfNames -> Maybe (Set1 Name) -> QName -> ScopeM ResolvedName
resolveName' KindsOfNames
allKindsOfNames (Set1 Name -> Maybe (Set1 Name)
forall a. a -> Maybe a
Just Set1 Name
ns) QName
x
  case r of
    VarName Name
y BindingSource
_         -> NewNotation -> ScopeM NewNotation
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (NewNotation -> ScopeM NewNotation)
-> NewNotation -> ScopeM NewNotation
forall a b. (a -> b) -> a -> b
$ QName -> Name -> NewNotation
namesToNotation QName
x Name
y
    DefinedName Access
_ AbstractName
d Suffix
_   -> NewNotation -> ScopeM NewNotation
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (NewNotation -> ScopeM NewNotation)
-> NewNotation -> ScopeM NewNotation
forall a b. (a -> b) -> a -> b
$ AbstractName -> NewNotation
notation AbstractName
d
    FieldName NonEmpty AbstractName
ds        -> NewNotation -> ScopeM NewNotation
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (NewNotation -> ScopeM NewNotation)
-> NewNotation -> ScopeM NewNotation
forall a b. (a -> b) -> a -> b
$ NonEmpty AbstractName -> NewNotation
oneNotation NonEmpty AbstractName
ds
    ConstructorName Set1 Induction
_ NonEmpty AbstractName
ds-> NewNotation -> ScopeM NewNotation
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (NewNotation -> ScopeM NewNotation)
-> NewNotation -> ScopeM NewNotation
forall a b. (a -> b) -> a -> b
$ NonEmpty AbstractName -> NewNotation
oneNotation NonEmpty AbstractName
ds
    PatternSynResName NonEmpty AbstractName
n -> NewNotation -> ScopeM NewNotation
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (NewNotation -> ScopeM NewNotation)
-> NewNotation -> ScopeM NewNotation
forall a b. (a -> b) -> a -> b
$ NonEmpty AbstractName -> NewNotation
oneNotation NonEmpty AbstractName
n
    ResolvedName
UnknownName         -> ScopeM NewNotation
forall a. HasCallStack => a
__IMPOSSIBLE__
  where
    notation :: AbstractName -> NewNotation
notation = QName -> Name -> NewNotation
namesToNotation QName
x (Name -> NewNotation)
-> (AbstractName -> Name) -> AbstractName -> NewNotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName (QName -> Name) -> (AbstractName -> QName) -> AbstractName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> QName
anameName
    oneNotation :: NonEmpty AbstractName -> NewNotation
oneNotation = NonEmpty NewNotation -> NewNotation
forall a. NonEmpty a -> a
List1.head (NonEmpty NewNotation -> NewNotation)
-> (NonEmpty AbstractName -> NonEmpty NewNotation)
-> NonEmpty AbstractName
-> NewNotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty NewNotation -> NonEmpty NewNotation
mergeNotations (NonEmpty NewNotation -> NonEmpty NewNotation)
-> (NonEmpty AbstractName -> NonEmpty NewNotation)
-> NonEmpty AbstractName
-> NonEmpty NewNotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractName -> NewNotation)
-> NonEmpty AbstractName -> NonEmpty NewNotation
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AbstractName -> NewNotation
notation

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

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

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

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

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

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

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

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

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

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

---------------------------------------------------
-- * Operations to do with record constructor names
---------------------------------------------------

-- | Record (ha) that a given record has the specified constructor name.
setRecordConstructor :: A.QName -> (A.QName, Maybe Induction) -> ScopeM ()
setRecordConstructor :: QName -> (QName, Maybe Induction) -> ScopeM ()
setRecordConstructor QName
recr (QName, Maybe Induction)
con = (ScopeInfo -> ScopeInfo) -> ScopeM ()
forall (m :: * -> *).
MonadTCState m =>
(ScopeInfo -> ScopeInfo) -> m ()
modifyScope_ ((ScopeInfo -> ScopeInfo) -> ScopeM ())
-> (ScopeInfo -> ScopeInfo) -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ Lens' ScopeInfo (Map QName (QName, Maybe Induction))
-> LensMap ScopeInfo (Map QName (QName, Maybe Induction))
forall o i. Lens' o i -> LensMap o i
over (Map QName (QName, Maybe Induction)
 -> f (Map QName (QName, Maybe Induction)))
-> ScopeInfo -> f ScopeInfo
Lens' ScopeInfo (Map QName (QName, Maybe Induction))
scopeRecords LensMap ScopeInfo (Map QName (QName, Maybe Induction))
-> LensMap ScopeInfo (Map QName (QName, Maybe Induction))
forall a b. (a -> b) -> a -> b
$ QName
-> (QName, Maybe Induction)
-> Map QName (QName, Maybe Induction)
-> Map QName (QName, Maybe Induction)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert QName
recr (QName, Maybe Induction)
con

-- | Get the internal 'QName' for the  name of a record constructor. If
-- the name does not refer to a record type, 'Nothing' is returned.
getRecordConstructor :: ReadTCState m => A.QName -> m (Maybe (A.QName, Maybe Induction))
getRecordConstructor :: forall (m :: * -> *).
ReadTCState m =>
QName -> m (Maybe (QName, Maybe Induction))
getRecordConstructor QName
recr = MaybeT m (QName, Maybe Induction)
-> m (Maybe (QName, Maybe Induction))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT m (QName, Maybe Induction)
 -> m (Maybe (QName, Maybe Induction)))
-> MaybeT m (QName, Maybe Induction)
-> m (Maybe (QName, Maybe Induction))
forall a b. (a -> b) -> a -> b
$ MaybeT m (QName, Maybe Induction)
local MaybeT m (QName, Maybe Induction)
-> MaybeT m (QName, Maybe Induction)
-> MaybeT m (QName, Maybe Induction)
forall a. MaybeT m a -> MaybeT m a -> MaybeT m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> MaybeT m (QName, Maybe Induction)
imported where
  local :: MaybeT m (QName, Maybe Induction)
local = do
    recs <- Lens' ScopeInfo (Map QName (QName, Maybe Induction))
-> MaybeT m (Map QName (QName, Maybe Induction))
forall (m :: * -> *) a. ReadTCState m => Lens' ScopeInfo a -> m a
useScope (Map QName (QName, Maybe Induction)
 -> f (Map QName (QName, Maybe Induction)))
-> ScopeInfo -> f ScopeInfo
Lens' ScopeInfo (Map QName (QName, Maybe Induction))
scopeRecords
    MaybeT $ pure $ Map.lookup recr recs
  imported :: MaybeT m (QName, Maybe Induction)
imported = do
    idefs <- Lens' TCState (HashMap QName Definition)
-> MaybeT m (HashMap QName Definition)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC ((Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stImports ((Signature -> f Signature) -> TCState -> f TCState)
-> ((HashMap QName Definition -> f (HashMap QName Definition))
    -> Signature -> f Signature)
-> (HashMap QName Definition -> f (HashMap QName Definition))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature
Lens' Signature (HashMap QName Definition)
sigDefinitions)
    case theDef <$> HMap.lookup recr idefs of
      Just def :: Defn
def@I.Record{} -> (QName, Maybe Induction) -> MaybeT m (QName, Maybe Induction)
forall a. a -> MaybeT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Defn -> QName
I.recCon Defn
def, Defn -> Maybe Induction
I.recInduction Defn
def)
      Maybe Defn
_ -> m (Maybe (QName, Maybe Induction))
-> MaybeT m (QName, Maybe Induction)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe (QName, Maybe Induction))
 -> MaybeT m (QName, Maybe Induction))
-> m (Maybe (QName, Maybe Induction))
-> MaybeT m (QName, Maybe Induction)
forall a b. (a -> b) -> a -> b
$ Maybe (QName, Maybe Induction)
-> m (Maybe (QName, Maybe Induction))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (QName, Maybe Induction)
forall a. Maybe a
Nothing


-- | Is this the qualified name which refers to the constructor of an
-- anonymous record (like @Foo.constructor@)?
--
-- If so, return the part of the name referring to the record (@Foo@).
isRecordConstructor :: C.QName -> Maybe C.QName
isRecordConstructor :: QName -> Maybe QName
isRecordConstructor = ([Name] -> QName) -> Maybe [Name] -> Maybe QName
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Name] -> QName
to (Maybe [Name] -> Maybe QName)
-> (QName -> Maybe [Name]) -> QName -> Maybe QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Maybe [Name]
toplevel where
  toplevel, is :: C.QName -> Maybe [C.Name]
  toplevel :: QName -> Maybe [Name]
toplevel (Qual Name
r QName
n) = (Name
rName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:) ([Name] -> [Name]) -> Maybe [Name] -> Maybe [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> Maybe [Name]
is QName
n
  toplevel QName
_          = Maybe [Name]
forall a. Maybe a
Nothing

  is :: QName -> Maybe [Name]
is (C.Qual Name
r QName
n) = (Name
rName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:) ([Name] -> [Name]) -> Maybe [Name] -> Maybe [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> Maybe [Name]
is QName
n
  is (C.QName Name
n)  = case Name
n of
    C.Name Range
_ NameInScope
_ (Id [Char]
w :| [])
      | [Char]
w [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
"constructor" -> [Name] -> Maybe [Name]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    Name
_ -> Maybe [Name]
forall a. Maybe a
Nothing

  to :: [Name] -> QName
to []     = QName
forall a. HasCallStack => a
__IMPOSSIBLE__
  to [Name
x]    = Name -> QName
C.QName Name
x
  to (Name
x:[Name]
xs) = Name -> QName -> QName
C.Qual Name
x ([Name] -> QName
to [Name]
xs)

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

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

type WSM = StateT ScopeMemo ScopeM

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

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

-- | Mark a name as being a copy in the TC state.
copyName :: A.QName -> A.QName -> ScopeM ()
copyName :: QName -> QName -> ScopeM ()
copyName QName
from QName
to = do
  from <- QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
from (Maybe QName -> QName)
-> (HashMap QName QName -> Maybe QName)
-> HashMap QName QName
-> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> HashMap QName QName -> Maybe QName
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
from (HashMap QName QName -> QName)
-> TCMT IO (HashMap QName QName) -> ScopeM QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState (HashMap QName QName)
-> TCMT IO (HashMap QName QName)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (HashMap QName QName -> f (HashMap QName QName))
-> TCState -> f TCState
Lens' TCState (HashMap QName QName)
stCopiedNames
  modifyTCLens stCopiedNames $ HMap.insert to from
  let
    k Maybe (HashSet QName)
Nothing  = HashSet QName -> Maybe (HashSet QName)
forall a. a -> Maybe a
Just (QName -> HashSet QName
forall a. Hashable a => a -> HashSet a
HSet.singleton QName
to)
    k (Just HashSet QName
s) = HashSet QName -> Maybe (HashSet QName)
forall a. a -> Maybe a
Just (QName -> HashSet QName -> HashSet QName
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HSet.insert QName
to HashSet QName
s)
  modifyTCLens stNameCopies $ HMap.alter k from

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

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

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

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

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

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

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

        copyRecordConstr :: A.QName -> A.QName -> WSM ()
        copyRecordConstr :: QName -> QName -> StateT ScopeMemo (TCMT IO) ()
copyRecordConstr QName
from QName
to = QName
-> StateT ScopeMemo (TCMT IO) (Maybe (QName, Maybe Induction))
forall (m :: * -> *).
ReadTCState m =>
QName -> m (Maybe (QName, Maybe Induction))
getRecordConstructor QName
from StateT ScopeMemo (TCMT IO) (Maybe (QName, Maybe Induction))
-> (Maybe (QName, Maybe Induction)
    -> StateT ScopeMemo (TCMT IO) ())
-> StateT ScopeMemo (TCMT IO) ()
forall a b.
StateT ScopeMemo (TCMT IO) a
-> (a -> StateT ScopeMemo (TCMT IO) b)
-> StateT ScopeMemo (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Just (QName
con, Maybe Induction
ind) -> do
            con' <- QName -> WSM QName
renName QName
con
            lift $ setRecordConstructor to (con', ind)
          Maybe (QName, Maybe Induction)
Nothing  -> () -> StateT ScopeMemo (TCMT IO) ()
forall a. a -> StateT ScopeMemo (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

        -- 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.
          m <- if QName
x QName -> ModuleName -> Bool
`isInModule` ModuleName
old
                 then ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
forall a. a -> StateT ScopeMemo (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleName
new'
                 else Bool -> ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
renMod' Bool
False (QName -> ModuleName
qnameModule QName
x)
                          -- Don't copy recursively here, we only know that the
                          -- current name x should be copied.
          -- Generate a fresh name for the target.
          -- Andreas, 2015-08-11 Issue 1619:
          -- Names copied by a module macro should get the module macro's
          -- range as declaration range
          -- (maybe rather the one of the open statement).
          -- For now, we just set their range
          -- to the new module name's one, which fixes issue 1619.
          y <- setRange rnew . A.qualify m <$> refresh (qnameName x)
          lift $ reportSLn "scope.copy" 50 $ "  Copying " ++ prettyShow x ++ " to " ++ prettyShow y
          addName x y
          lift (copyName x y)
          copyRecordConstr x y
          return y

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

        renMod' :: Bool -> ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
renMod' Bool
rec ModuleName
x = do
          -- Andreas, issue 1607:
          -- If we have already copied this module, return the copy.
          z <- ModuleName -> StateT ScopeMemo (TCMT IO) (Maybe (ModuleName, Bool))
forall {m :: * -> *}.
MonadState ScopeMemo m =>
ModuleName -> m (Maybe (ModuleName, Bool))
findMod ModuleName
x
          case z of
            Just (ModuleName
y, Bool
False) | Bool
rec -> ModuleName
y ModuleName
-> StateT ScopeMemo (TCMT IO) ()
-> StateT ScopeMemo (TCMT IO) ModuleName
forall a b.
a -> StateT ScopeMemo (TCMT IO) b -> StateT ScopeMemo (TCMT IO) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ModuleName -> ModuleName -> StateT ScopeMemo (TCMT IO) ()
copyRec ModuleName
x ModuleName
y
            Just (ModuleName
y, Bool
_)           -> ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
forall a. a -> StateT ScopeMemo (TCMT IO) a
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

            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.
               y <- Name -> WSM Name
refresh (Name -> WSM Name) -> Name -> WSM Name
forall a b. (a -> b) -> a -> b
$ Name -> [Name] -> Name
forall a. a -> [a] -> a
lastWithDefault Name
forall a. HasCallStack => a
__IMPOSSIBLE__ ([Name] -> Name) -> [Name] -> Name
forall a b. (a -> b) -> a -> b
$ ModuleName -> [Name]
A.mnameToList ModuleName
x
               return $ A.mnameFromList $ newM ++ [y]
            -- Andreas, Jesper, 2015-07-02: Issue 1597
            -- Don't copy a module over itself, it will just be emptied of its contents.
            if (x == y) then return x else do
            lift $ reportSLn "scope.copy" 50 $ "  Copying module " ++ prettyShow x ++ " to " ++ prettyShow y
            addMod x y rec
            lift $ createModule Nothing y
            -- We need to copy the contents of included modules recursively (only when 'rec')
            when rec $ copyRec x y
            return y
          where
            copyRec :: ModuleName -> ModuleName -> StateT ScopeMemo (TCMT IO) ()
copyRec ModuleName
x ModuleName
y = do
              s0 <- ScopeM Scope -> StateT ScopeMemo (TCMT IO) Scope
forall (m :: * -> *) a. Monad m => m a -> StateT ScopeMemo m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ScopeM Scope -> StateT ScopeMemo (TCMT IO) Scope)
-> ScopeM Scope -> StateT ScopeMemo (TCMT IO) Scope
forall a b. (a -> b) -> a -> b
$ ModuleName -> ScopeM Scope
getNamedScope ModuleName
x
              s  <- withCurrentModule' y $ copy y s0
              lift $ modifyNamedScope y (const s)

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

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

-- | Check that an import directive doesn't contain repeated names.
verifyImportDirective :: [C.ImportedName] -> C.HidingDirective -> C.RenamingDirective -> ScopeM ()
verifyImportDirective :: [ImportedName] -> [ImportedName] -> [Renaming] -> ScopeM ()
verifyImportDirective [ImportedName]
usn [ImportedName]
hdn [Renaming]
ren =
  [List2 ImportedName]
-> (List1 (List2 ImportedName) -> ScopeM ()) -> ScopeM ()
forall (m :: * -> *) a.
Applicative m =>
[a] -> (List1 a -> m ()) -> m ()
List1.unlessNull
    ((List1 ImportedName -> Maybe (List2 ImportedName))
-> [List1 ImportedName] -> [List2 ImportedName]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe List1 ImportedName -> Maybe (List2 ImportedName)
forall a. List1 a -> Maybe (List2 a)
List2.fromList1Maybe ([List1 ImportedName] -> [List2 ImportedName])
-> ([ImportedName] -> [List1 ImportedName])
-> [ImportedName]
-> [List2 ImportedName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ImportedName] -> [List1 ImportedName]
forall (f :: * -> *) a. (Foldable f, Eq a) => f a -> [NonEmpty a]
List1.group ([ImportedName] -> [List1 ImportedName])
-> ([ImportedName] -> [ImportedName])
-> [ImportedName]
-> [List1 ImportedName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ImportedName] -> [ImportedName]
forall a. Ord a => [a] -> [a]
List.sort ([ImportedName] -> [List2 ImportedName])
-> [ImportedName] -> [List2 ImportedName]
forall a b. (a -> b) -> a -> b
$ [ImportedName]
usn [ImportedName] -> [ImportedName] -> [ImportedName]
forall a. [a] -> [a] -> [a]
++ [ImportedName]
hdn [ImportedName] -> [ImportedName] -> [ImportedName]
forall a. [a] -> [a] -> [a]
++ (Renaming -> ImportedName) -> [Renaming] -> [ImportedName]
forall a b. (a -> b) -> [a] -> [b]
map Renaming -> ImportedName
forall n m. Renaming' n m -> ImportedName' n m
renFrom [Renaming]
ren)
    \ List1 (List2 ImportedName)
yss -> List1 (List2 ImportedName) -> ScopeM () -> ScopeM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange List1 (List2 ImportedName)
yss (ScopeM () -> ScopeM ()) -> ScopeM () -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> ScopeM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> ScopeM ()) -> TypeError -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ List1 (List2 ImportedName) -> TypeError
RepeatedNamesInImportDirective List1 (List2 ImportedName)
yss

-- | 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 KwRange
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] -> ScopeM ()
checkNoFixityInRenamingModule [Renaming]
ren'

    -- Andreas, 2020-06-06, issue #4707
    -- Duplicates in @using@ directive are dropped with a warning.
    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.
    verifyImportDirective usingList hdn' 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 (missingExports, namesA) = checkExist $ usingList ++ hdn' ++ map renFrom ren'
    () <- List1.unlessNull missingExports \ List1 ImportedName
missingExports1 -> Range -> ScopeM () -> ScopeM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range
rng do
      [Char] -> Int -> [Char] -> ScopeM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.import.apply" Int
30 ([Char] -> ScopeM ()) -> [Char] -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"non existing names: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [ImportedName] -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow [ImportedName]
missingExports
      Warning -> ScopeM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> ScopeM ()) -> Warning -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ QName -> [Name] -> [Name] -> List1 ImportedName -> Warning
ModuleDoesntExport QName
m (NamesInScope -> [Name]
forall k a. Map k a -> [k]
Map.keys NamesInScope
namesInScope) (ModulesInScope -> [Name]
forall k a. Map k a -> [k]
Map.keys ModulesInScope
modulesInScope) List1 ImportedName
missingExports1

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

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

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

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

    dir' <- sanityCheck (not . inNames) $ addExtraModules extra dir

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

    -- Apply the import directive.
    let (scope', (nameClashes, moduleClashes)) = applyImportDirective_ dir' scope

    -- Andreas, 2019-11-08, issue #4154, report clashes
    -- introduced by the @renaming@.
    Set1.unlessNull nameClashes \ Set1 Name
nameClashes ->
      Warning -> ScopeM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> ScopeM ()) -> Warning -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ NameOrModule -> Set1 Name -> Warning
ClashesViaRenaming NameOrModule
NameNotModule Set1 Name
nameClashes
    Set1.unlessNull moduleClashes \ Set1 Name
moduleClashes ->
      Warning -> ScopeM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> ScopeM ()) -> Warning -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ NameOrModule -> Set1 Name -> Warning
ClashesViaRenaming NameOrModule
ModuleNotName Set1 Name
moduleClashes

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

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

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

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

    -- If both @using@ and @hiding@ directive are present,
    -- the hiding directive may only contain modules whose twins are mentioned.
    -- Monadic for the sake of error reporting.
    sanityCheck :: (ImportedName' Name m -> Bool)
-> ImportDirective -> m ImportDirective
sanityCheck ImportedName' Name m -> Bool
notMentioned = \case
      dir :: ImportDirective
dir@(ImportDirective{ using :: forall n m. ImportDirective' n m -> Using' n m
using = Using{}, hiding :: forall n m. ImportDirective' n m -> HidingDirective' n m
hiding = [ImportedName]
ys }) -> do
          let useless :: ImportedName -> Bool
useless = \case
                ImportedName{}   -> Bool
True
                ImportedModule Name
y -> ImportedName' Name m -> Bool
notMentioned (Name -> ImportedName' Name m
forall n m. n -> ImportedName' n m
ImportedName Name
y)
          () <- [ImportedName] -> (List1 ImportedName -> m ()) -> m ()
forall (m :: * -> *) a.
Applicative m =>
[a] -> (List1 a -> m ()) -> m ()
List1.unlessNull ((ImportedName -> Bool) -> [ImportedName] -> [ImportedName]
forall a. (a -> Bool) -> [a] -> [a]
filter ImportedName -> Bool
useless [ImportedName]
ys) ((List1 ImportedName -> m ()) -> m ())
-> (List1 ImportedName -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ Warning -> m ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> m ())
-> (List1 ImportedName -> Warning) -> List1 ImportedName -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 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.
          return dir{ hiding = [] }
      ImportDirective
dir -> ImportDirective -> m ImportDirective
forall a. a -> m a
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       = mapUsing (concatMap addExtra) $ using dir
         , hiding      = concatMap addExtra            $ hiding dir
         , impRenaming = concatMap extraRenaming       $ impRenaming dir
         }
      where
        addExtra :: ImportedName -> [ImportedName]
addExtra f :: ImportedName
f@(ImportedName Name
y) | Name -> Bool
extra Name
y = [ImportedName
f, Name -> ImportedName
forall n m. m -> ImportedName' n m
ImportedModule Name
y]
        addExtra ImportedName
m = [ImportedName
m]

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

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

    -- AST versions of the concrete names passed as an argument.
    -- We get back a pair consisting of a list of missing exports first,
    -- and a list of successful imports second.
    checkExist :: [ImportedName] -> ([ImportedName], [ImportedName' (C.Name, A.QName) (C.Name, A.ModuleName)])
    checkExist :: [ImportedName]
-> ([ImportedName],
    [ImportedName' (Name, QName) (Name, ModuleName)])
checkExist [ImportedName]
xs = [Either
   ImportedName (ImportedName' (Name, QName) (Name, ModuleName))]
-> ([ImportedName],
    [ImportedName' (Name, QName) (Name, ModuleName)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either
    ImportedName (ImportedName' (Name, QName) (Name, ModuleName))]
 -> ([ImportedName],
     [ImportedName' (Name, QName) (Name, ModuleName)]))
-> [Either
      ImportedName (ImportedName' (Name, QName) (Name, ModuleName))]
-> ([ImportedName],
    [ImportedName' (Name, QName) (Name, ModuleName)])
forall a b. (a -> b) -> a -> b
$ [ImportedName]
-> (ImportedName
    -> Either
         ImportedName (ImportedName' (Name, QName) (Name, ModuleName)))
-> [Either
      ImportedName (ImportedName' (Name, QName) (Name, ModuleName))]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [ImportedName]
xs ((ImportedName
  -> Either
       ImportedName (ImportedName' (Name, QName) (Name, ModuleName)))
 -> [Either
       ImportedName (ImportedName' (Name, QName) (Name, ModuleName))])
-> (ImportedName
    -> Either
         ImportedName (ImportedName' (Name, QName) (Name, ModuleName)))
-> [Either
      ImportedName (ImportedName' (Name, QName) (Name, ModuleName))]
forall a b. (a -> b) -> a -> b
$ \ ImportedName
name -> case ImportedName
name of
      ImportedName Name
x   -> (Name, QName) -> ImportedName' (Name, QName) (Name, ModuleName)
forall n m. n -> ImportedName' n m
ImportedName   ((Name, QName) -> ImportedName' (Name, QName) (Name, ModuleName))
-> (AbstractName -> (Name, QName))
-> AbstractName
-> ImportedName' (Name, QName) (Name, ModuleName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name
x,) (QName -> (Name, QName))
-> (AbstractName -> QName) -> AbstractName -> (Name, QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> QName -> QName
forall a. SetRange a => Range -> a -> a
setRange (Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x) (QName -> QName)
-> (AbstractName -> QName) -> AbstractName -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> QName
anameName (AbstractName -> ImportedName' (Name, QName) (Name, ModuleName))
-> Either ImportedName AbstractName
-> Either
     ImportedName (ImportedName' (Name, QName) (Name, ModuleName))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ImportedName
-> Name -> NamesInScope -> Either ImportedName AbstractName
forall a err b.
Ord a =>
err -> a -> Map a (List1 b) -> Either err b
resolve ImportedName
name Name
x NamesInScope
namesInScope
      ImportedModule Name
x -> (Name, ModuleName)
-> ImportedName' (Name, QName) (Name, ModuleName)
forall n m. m -> ImportedName' n m
ImportedModule ((Name, ModuleName)
 -> ImportedName' (Name, QName) (Name, ModuleName))
-> (AbstractModule -> (Name, ModuleName))
-> AbstractModule
-> ImportedName' (Name, QName) (Name, ModuleName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name
x,) (ModuleName -> (Name, ModuleName))
-> (AbstractModule -> ModuleName)
-> AbstractModule
-> (Name, ModuleName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> ModuleName -> ModuleName
forall a. SetRange a => Range -> a -> a
setRange (Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x) (ModuleName -> ModuleName)
-> (AbstractModule -> ModuleName) -> AbstractModule -> ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractModule -> ModuleName
amodName  (AbstractModule -> ImportedName' (Name, QName) (Name, ModuleName))
-> Either ImportedName AbstractModule
-> Either
     ImportedName (ImportedName' (Name, QName) (Name, ModuleName))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ImportedName
-> Name -> ModulesInScope -> Either ImportedName AbstractModule
forall a err b.
Ord a =>
err -> a -> Map a (List1 b) -> Either err b
resolve ImportedName
name Name
x ModulesInScope
modulesInScope
      where
        resolve :: Ord a => err -> a -> Map a (List1 b) -> Either err b
        resolve :: forall a err b.
Ord a =>
err -> a -> Map a (List1 b) -> Either err b
resolve err
err a
x Map a (List1 b)
m = Either err b
-> (List1 b -> Either err b) -> Maybe (List1 b) -> Either err b
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (err -> Either err b
forall a b. a -> Either a b
Left err
err) (b -> Either err b
forall a b. b -> Either a b
Right (b -> Either err b) -> (List1 b -> b) -> List1 b -> Either err b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 b -> b
forall a. NonEmpty a -> a
List1.head) (Maybe (List1 b) -> Either err b)
-> Maybe (List1 b) -> Either err b
forall a b. (a -> b) -> a -> b
$ a -> Map a (List1 b) -> Maybe (List1 b)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
x Map a (List1 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 KwRange
open) =
  Range
-> Using' n2 m2
-> HidingDirective' n2 m2
-> RenamingDirective' n2 m2
-> Maybe KwRange
-> ImportDirective' n2 m2
forall n m.
Range
-> Using' n m
-> HidingDirective' n m
-> RenamingDirective' n m
-> Maybe KwRange
-> ImportDirective' n m
ImportDirective Range
r
    ((HidingDirective' n1 m1 -> HidingDirective' n2 m2)
-> Using' n1 m1 -> Using' n2 m2
forall n1 m1 n2 m2.
([ImportedName' n1 m1] -> [ImportedName' n2 m2])
-> Using' n1 m1 -> Using' n2 m2
mapUsing ((ImportedName' n1 m1 -> ImportedName' n2 m2)
-> HidingDirective' n1 m1 -> HidingDirective' n2 m2
forall a b. (a -> b) -> [a] -> [b]
map (ImportedNameMap n1 n2 m1 m2
-> ImportedName' n1 m1 -> ImportedName' n2 m2
forall n1 m1 n2 m2.
(Ord n1, Ord m1) =>
ImportedNameMap n1 n2 m1 m2
-> ImportedName' n1 m1 -> ImportedName' n2 m2
lookupImportedName ImportedNameMap n1 n2 m1 m2
src)) Using' n1 m1
u)
    ((ImportedName' n1 m1 -> ImportedName' n2 m2)
-> HidingDirective' n1 m1 -> HidingDirective' n2 m2
forall a b. (a -> b) -> [a] -> [b]
map (ImportedNameMap n1 n2 m1 m2
-> ImportedName' n1 m1 -> ImportedName' n2 m2
forall n1 m1 n2 m2.
(Ord n1, Ord m1) =>
ImportedNameMap n1 n2 m1 m2
-> ImportedName' n1 m1 -> ImportedName' n2 m2
lookupImportedName ImportedNameMap n1 n2 m1 m2
src) HidingDirective' n1 m1
h)
    ((Renaming' n1 m1 -> Renaming' n2 m2)
-> RenamingDirective' n1 m1 -> RenamingDirective' n2 m2
forall a b. (a -> b) -> [a] -> [b]
map (ImportedNameMap n1 n2 m1 m2
-> ImportedNameMap n1 n2 m1 m2
-> Renaming' n1 m1
-> Renaming' n2 m2
forall n1 m1 n2 m2.
(Ord n1, Ord m1) =>
ImportedNameMap n1 n2 m1 m2
-> ImportedNameMap n1 n2 m1 m2
-> Renaming' n1 m1
-> Renaming' n2 m2
mapRenaming ImportedNameMap n1 n2 m1 m2
src ImportedNameMap n1 n2 m1 m2
tgt) RenamingDirective' n1 m1
ren)
    Maybe KwRange
open
  where
  src :: ImportedNameMap n1 n2 m1 m2
src = [ImportedName' (n1, n2) (m1, m2)] -> ImportedNameMap n1 n2 m1 m2
forall n1 m1 n2 m2.
(Ord n1, Ord m1) =>
[ImportedName' (n1, n2) (m1, m2)] -> ImportedNameMap n1 n2 m1 m2
importedNameMapFromList [ImportedName' (n1, n2) (m1, m2)]
src0
  tgt :: ImportedNameMap n1 n2 m1 m2
tgt = [ImportedName' (n1, n2) (m1, m2)] -> ImportedNameMap n1 n2 m1 m2
forall n1 m1 n2 m2.
(Ord n1, Ord m1) =>
[ImportedName' (n1, n2) (m1, m2)] -> ImportedNameMap n1 n2 m1 m2
importedNameMapFromList [ImportedName' (n1, n2) (m1, m2)]
tgt0

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

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

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

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

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

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

data OpenKind = LetOpenModule | TopOpenModule

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

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

-- | Open a module, possibly given an already resolved module name.
openModule :: OpenKind -> Maybe A.ModuleName  -> C.QName -> C.ImportDirective -> ScopeM A.ImportDirective
openModule :: OpenKind
-> Maybe ModuleName
-> QName
-> ImportDirective
-> ScopeM ImportDirective
openModule OpenKind
kind Maybe ModuleName
mam QName
cm ImportDirective
dir = do
  current <- ScopeM ModuleName
forall (m :: * -> *). ReadTCState m => m ModuleName
getCurrentModule
  m <- caseMaybe mam (amodName <$> resolveModule cm) return
  let acc | Maybe KwRange
Nothing <- ImportDirective -> Maybe KwRange
forall n m. ImportDirective' n m -> Maybe KwRange
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.
  (adir, s') <- applyImportDirectiveM cm dir . inScopeBecause (Opened cm) .
                noGeneralizedVarsIfLetOpen kind =<< getNamedScope m
  let s  = NameSpaceId -> Scope -> Scope
setScopeAccess NameSpaceId
acc Scope
s'
  let ns = NameSpaceId -> Scope -> NameSpace
scopeNameSpace NameSpaceId
acc Scope
s
  modifyCurrentScope (`mergeScope` 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.
  checkForClashes

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

  return adir

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

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

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

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

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