    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | Flattened scopes.
    module Agda.Syntax.Scope.Flat
      ( FlatScope
      , flattenScope
      , getDefinedNames
      , localNames
      ) where

    import Prelude hiding ( (||) )

    import Data.Bifunctor
    import Data.Either (partitionEithers)
    import qualified Data.List as List
    import Data.Map (Map)
    import qualified Data.Map as Map

    import qualified Agda.Syntax.Abstract.Name as A

    import Agda.Syntax.Common (ExprKind(..))
    import Agda.Syntax.Common.Pretty
    import Agda.Syntax.Concrete
    import Agda.Syntax.Notation
    import Agda.Syntax.Scope.Base
    import Agda.Syntax.Scope.Monad

    import Agda.TypeChecking.Monad.Debug

    import Agda.Utils.Boolean ( (||) )
    import Agda.Utils.Function ( applyWhenJust )
    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.List1 (List1)
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Maybe

    import Agda.Utils.Impossible

    -- | Flattened scopes.
    newtype FlatScope = Flat (Map QName (List1 AbstractName))
      deriving Int -> FlatScope -> Doc
    [FlatScope] -> Doc
    FlatScope -> Doc
    (FlatScope -> Doc)
    -> (Int -> FlatScope -> Doc)
    -> ([FlatScope] -> Doc)
    -> Pretty FlatScope
    forall a.
    (a -> Doc) -> (Int -> a -> Doc) -> ([a] -> Doc) -> Pretty a
    $cpretty :: FlatScope -> Doc
    pretty :: FlatScope -> Doc
    $cprettyPrec :: Int -> FlatScope -> Doc
    prettyPrec :: Int -> FlatScope -> Doc
    $cprettyList :: [FlatScope] -> Doc
    prettyList :: [FlatScope] -> Doc
    Pretty

    -- | Compute a flattened scope. Only include unqualified names or names
    -- qualified by modules in the first argument.
    flattenScope :: [[Name]] -> ScopeInfo -> FlatScope
    flattenScope :: [[Name]] -> ScopeInfo -> FlatScope
    flattenScope [[Name]]
    ms ScopeInfo
    scope =
      Map QName (List1 AbstractName) -> FlatScope
    Flat (Map QName (List1 AbstractName) -> FlatScope)
    -> Map QName (List1 AbstractName) -> FlatScope
    forall a b. (a -> b) -> a -> b
    $
      (List1 AbstractName -> List1 AbstractName -> List1 AbstractName)
    -> Map QName (List1 AbstractName)
    -> Map QName (List1 AbstractName)
    -> Map QName (List1 AbstractName)
    forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
    Map.unionWith List1 AbstractName -> List1 AbstractName -> List1 AbstractName
    forall a. Semigroup a => a -> a -> a
    (<>)
        ([[Name]]
    -> (forall a. InScope a => Scope -> ThingsInScope a)
    -> Scope
    -> Map QName (List1 AbstractName)
    build [[Name]]
    ms Scope -> ThingsInScope a
    forall a. InScope a => Scope -> ThingsInScope a
    allNamesInScope Scope
    root)
        Map QName (List1 AbstractName)
    imported
      where
        current :: Scope
    current = ModuleName -> Scope
    moduleScope (ModuleName -> Scope) -> ModuleName -> Scope
    forall a b. (a -> b) -> a -> b
    $ ScopeInfo
    scope ScopeInfo -> Lens' ScopeInfo ModuleName -> ModuleName
    forall o i. o -> Lens' o i -> i
    ^. (ModuleName -> f ModuleName) -> ScopeInfo -> f ScopeInfo
    Lens' ScopeInfo ModuleName
    scopeCurrent
        root :: Scope
    root    = [Scope] -> Scope
    mergeScopes ([Scope] -> Scope) -> [Scope] -> Scope
    forall a b. (a -> b) -> a -> b
    $ Scope
    current Scope -> [Scope] -> [Scope]
    forall a. a -> [a] -> [a]
    : (ModuleName -> Scope) -> [ModuleName] -> [Scope]
    forall a b. (a -> b) -> [a] -> [b]
    map ModuleName -> Scope
    moduleScope (Scope -> [ModuleName]
    scopeParents Scope
    current)

        imported :: Map QName (List1 AbstractName)
    imported = (List1 AbstractName -> List1 AbstractName -> List1 AbstractName)
    -> [Map QName (List1 AbstractName)]
    -> Map QName (List1 AbstractName)
    forall (f :: * -> *) k a.
    (Foldable f, Ord k) =>
    (a -> a -> a) -> f (Map k a) -> Map k a
    Map.unionsWith List1 AbstractName -> List1 AbstractName -> List1 AbstractName
    forall a. Semigroup a => a -> a -> a
    (<>)
                   [ QName
    -> Map QName (List1 AbstractName) -> Map QName (List1 AbstractName)
    forall {a}. QName -> Map QName a -> Map QName a
    qual QName
    c ([[Name]]
    -> (forall a. InScope a => Scope -> ThingsInScope a)
    -> Scope
    -> Map QName (List1 AbstractName)
    build [[Name]]
    ms' Scope -> ThingsInScope a
    forall a. InScope a => Scope -> ThingsInScope a
    exportedNamesInScope (Scope -> Map QName (List1 AbstractName))
    -> Scope -> Map QName (List1 AbstractName)
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> Scope
    moduleScope ModuleName
    a)
                   | (QName
    c, ModuleName
    a) <- Map QName ModuleName -> [(QName, ModuleName)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (Map QName ModuleName -> [(QName, ModuleName)])
    -> Map QName ModuleName -> [(QName, ModuleName)]
    forall a b. (a -> b) -> a -> b
    $ Scope -> Map QName ModuleName
    scopeImports Scope
    root
                   , let -- get the suffixes of c in ms
                         ms' :: [[Name]]
    ms' = ([Name] -> Maybe [Name]) -> [[Name]] -> [[Name]]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe ([Name] -> [Name] -> Maybe [Name]
    forall a. Eq a => [a] -> [a] -> Maybe [a]
    List.stripPrefix ([Name] -> [Name] -> Maybe [Name])
    -> [Name] -> [Name] -> Maybe [Name]
    forall a b. (a -> b) -> a -> b
    $ List1 Name -> [Item (List1 Name)]
    forall l. IsList l => l -> [Item l]
    List1.toList (List1 Name -> [Item (List1 Name)])
    -> List1 Name -> [Item (List1 Name)]
    forall a b. (a -> b) -> a -> b
    $ QName -> List1 Name
    qnameParts QName
    c) [[Name]]
    ms
                   , Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [[Name]] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [[Name]]
    ms' ]
        qual :: QName -> Map QName a -> Map QName a
    qual QName
    c = (QName -> QName) -> Map QName a -> Map QName a
    forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
    Map.mapKeysMonotonic (QName -> QName -> QName
    q QName
    c)
          where
            q :: QName -> QName -> QName
    q (QName Name
    x)  = Name -> QName -> QName
    Qual Name
    x
            q (Qual Name
    m QName
    x) = Name -> QName -> QName
    Qual Name
    m (QName -> QName) -> (QName -> QName) -> QName -> QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> QName -> QName
    q QName
    x

        build :: [[Name]] -> (forall a. InScope a => Scope -> ThingsInScope a) -> Scope -> Map QName (List1 AbstractName)
        build :: [[Name]]
    -> (forall a. InScope a => Scope -> ThingsInScope a)
    -> Scope
    -> Map QName (List1 AbstractName)
    build [[Name]]
    ms forall a. InScope a => Scope -> ThingsInScope a
    getNames Scope
    s = (List1 AbstractName -> List1 AbstractName -> List1 AbstractName)
    -> [Map QName (List1 AbstractName)]
    -> Map QName (List1 AbstractName)
    forall (f :: * -> *) k a.
    (Foldable f, Ord k) =>
    (a -> a -> a) -> f (Map k a) -> Map k a
    Map.unionsWith List1 AbstractName -> List1 AbstractName -> List1 AbstractName
    forall a. Semigroup a => a -> a -> a
    (<>) ([Map QName (List1 AbstractName)]
     -> Map QName (List1 AbstractName))
    -> [Map QName (List1 AbstractName)]
    -> Map QName (List1 AbstractName)
    forall a b. (a -> b) -> a -> b
    $
            (Name -> QName)
    -> Map Name (List1 AbstractName) -> Map QName (List1 AbstractName)
    forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
    Map.mapKeysMonotonic Name -> QName
    QName (Scope -> Map Name (List1 AbstractName)
    forall a. InScope a => Scope -> ThingsInScope a
    getNames Scope
    s) Map QName (List1 AbstractName)
    -> [Map QName (List1 AbstractName)]
    -> [Map QName (List1 AbstractName)]
    forall a. a -> [a] -> [a]
    :
              [ (QName -> QName)
    -> Map QName (List1 AbstractName) -> Map QName (List1 AbstractName)
    forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
    Map.mapKeysMonotonic (\ QName
    y -> Name -> QName -> QName
    Qual Name
    x QName
    y) (Map QName (List1 AbstractName) -> Map QName (List1 AbstractName))
    -> Map QName (List1 AbstractName) -> Map QName (List1 AbstractName)
    forall a b. (a -> b) -> a -> b
    $
                  [[Name]]
    -> (forall a. InScope a => Scope -> ThingsInScope a)
    -> Scope
    -> Map QName (List1 AbstractName)
    build [[Name]]
    ms' Scope -> ThingsInScope a
    forall a. InScope a => Scope -> ThingsInScope a
    exportedNamesInScope (Scope -> Map QName (List1 AbstractName))
    -> Scope -> Map QName (List1 AbstractName)
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> Scope
    moduleScope ModuleName
    m
              | (Name
    x, List1 AbstractModule
    mods) <- Map Name (List1 AbstractModule) -> [(Name, List1 AbstractModule)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (Scope -> Map Name (List1 AbstractModule)
    forall a. InScope a => Scope -> ThingsInScope a
    getNames Scope
    s)
              , let ms' :: [[Name]]
    ms' = [ [Name]
    tl | Name
    hd:[Name]
    tl <- [[Name]]
    ms, Name
    hd Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    x ]
              , Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [[Name]] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [[Name]]
    ms'
              , AbsModule ModuleName
    m WhyInScope
    _ <- List1 AbstractModule -> [Item (List1 AbstractModule)]
    forall l. IsList l => l -> [Item l]
    List1.toList List1 AbstractModule
    mods
              ]

        moduleScope :: A.ModuleName -> Scope
        moduleScope :: ModuleName -> Scope
    moduleScope ModuleName
    m = Scope -> Maybe Scope -> Scope
    forall a. a -> Maybe a -> a
    fromMaybe Scope
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Scope -> Scope) -> Maybe Scope -> Scope
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> Map ModuleName Scope -> Maybe Scope
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup ModuleName
    m (Map ModuleName Scope -> Maybe Scope)
    -> Map ModuleName Scope -> Maybe Scope
    forall a b. (a -> b) -> a -> b
    $ ScopeInfo
    scope ScopeInfo
    -> Lens' ScopeInfo (Map ModuleName Scope) -> Map ModuleName Scope
    forall o i. o -> Lens' o i -> i
    ^. (Map ModuleName Scope -> f (Map ModuleName Scope))
    -> ScopeInfo -> f ScopeInfo
    Lens' ScopeInfo (Map ModuleName Scope)
    scopeModules

    -- | Compute all defined names in scope and their fixities/notations.
    -- Note that overloaded names (constructors) can have several
    -- fixities/notations. Then we 'mergeNotations'. (See issue 1194.)
    getDefinedNames' :: (AbstractName -> Bool) -> FlatScope -> [List1 NewNotation]
    getDefinedNames' :: (AbstractName -> Bool) -> FlatScope -> [List1 NewNotation]
    getDefinedNames' AbstractName -> Bool
    f (Flat Map QName (List1 AbstractName)
    names) =
      [ List1 NewNotation -> List1 NewNotation
    mergeNotations (List1 NewNotation -> List1 NewNotation)
    -> List1 NewNotation -> List1 NewNotation
    forall a b. (a -> b) -> a -> b
    $ (AbstractName -> NewNotation)
    -> List1 AbstractName -> List1 NewNotation
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (QName -> Name -> NewNotation
    namesToNotation QName
    x (Name -> NewNotation)
    -> (AbstractName -> Name) -> AbstractName -> NewNotation
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Name
    A.qnameName (QName -> Name) -> (AbstractName -> QName) -> AbstractName -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractName -> QName
    anameName) List1 AbstractName
    ds
      | (QName
    x, List1 AbstractName
    ds) <- Map QName (List1 AbstractName) -> [(QName, List1 AbstractName)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map QName (List1 AbstractName)
    names
      , (AbstractName -> Bool) -> List1 AbstractName -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any AbstractName -> Bool
    f List1 AbstractName
    ds
      ]
      -- Andreas, 2013-03-21 see Issue 822
      -- Names can have different kinds, i.e., 'defined' and 'constructor'.
      -- We need to consider all names that have *any* matching kind,
      -- not only those whose first appearing kind is matching.

    getDefinedNames :: KindsOfNames -> FlatScope -> [List1 NewNotation]
    getDefinedNames :: KindsOfNames -> FlatScope -> [List1 NewNotation]
    getDefinedNames KindsOfNames
    kinds = (AbstractName -> Bool) -> FlatScope -> [List1 NewNotation]
    getDefinedNames' (KindsOfNames -> AbstractName -> Bool
    filterByKind KindsOfNames
    kinds)

    filterByKind :: KindsOfNames -> AbstractName -> Bool
    filterByKind :: KindsOfNames -> AbstractName -> Bool
    filterByKind KindsOfNames
    kinds = (KindOfName -> KindsOfNames -> Bool
    `elemKindsOfNames` KindsOfNames
    kinds) (KindOfName -> Bool)
    -> (AbstractName -> KindOfName) -> AbstractName -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractName -> KindOfName
    anameKind

    -- | Compute all names (first component) and operators/notations
    --   (second component) in scope.
    --
    --   For 'IsPattern', only constructor-like names are returned.
    --
    localNames :: ExprKind -> Maybe QName -> FlatScope -> ScopeM ([QName], [NewNotation])
    localNames :: ExprKind
    -> Maybe QName -> FlatScope -> ScopeM ([QName], [NewNotation])
    localNames ExprKind
    k Maybe QName
    top FlatScope
    flat = do
      -- Construct a filter for the names we consider.
      let
        f :: AbstractName -> Bool
    f = case ExprKind
    k of
          ExprKind
    IsExpr    -> Bool -> AbstractName -> Bool
    forall a b. a -> b -> a
    const Bool
    True
          ExprKind
    IsPattern -> let
              -- Andreas, 2025-02-28, issue #7722
              -- Filter by kind.
              -- Just return the constructor-like operators,
              -- otherwise the pattern parser blows up.
              fk :: AbstractName -> Bool
    fk = KindsOfNames -> AbstractName -> Bool
    filterByKind ([KindOfName] -> KindsOfNames
    someKindsOfNames ([KindOfName] -> KindsOfNames) -> [KindOfName] -> KindsOfNames
    forall a b. (a -> b) -> a -> b
    $ KindOfName
    FldName KindOfName -> [KindOfName] -> [KindOfName]
    forall a. a -> [a] -> [a]
    : [KindOfName]
    conLikeNameKinds)
              -- Filter by name, keeping @top@ in.
              ft :: Maybe (AbstractName -> Bool)
    ft = Maybe QName
    top Maybe QName
    -> (QName -> AbstractName -> Bool) -> Maybe (AbstractName -> Bool)
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ QName
    y -> (QName -> Name
    unqualify QName
    y Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Name -> Bool) -> (AbstractName -> Name) -> AbstractName -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> Name
    A.nameConcrete (Name -> Name) -> (AbstractName -> Name) -> AbstractName -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Name
    A.qnameName (QName -> Name) -> (AbstractName -> QName) -> AbstractName -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractName -> QName
    anameName
            in Maybe (AbstractName -> Bool)
    -> ((AbstractName -> Bool)
        -> (AbstractName -> Bool) -> AbstractName -> Bool)
    -> (AbstractName -> Bool)
    -> AbstractName
    -> Bool
    forall b a. Maybe b -> (b -> a -> a) -> a -> a
    applyWhenJust Maybe (AbstractName -> Bool)
    ft (AbstractName -> Bool)
    -> (AbstractName -> Bool) -> AbstractName -> Bool
    forall a. Boolean a => a -> a -> a
    (||) AbstractName -> Bool
    fk

      -- Retrieve the names of interest from the flat scope.
      let defs :: [List1 NewNotation]
    defs = (AbstractName -> Bool) -> FlatScope -> [List1 NewNotation]
    getDefinedNames' AbstractName -> Bool
    f FlatScope
    flat

      locals <- ((Name, Name) -> Name) -> [(Name, Name)] -> [(Name, Name)]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn (Name, Name) -> Name
    forall a b. (a, b) -> a
    fst ([(Name, Name)] -> [(Name, Name)])
    -> (LocalVars -> [(Name, Name)]) -> LocalVars -> [(Name, Name)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LocalVars -> [(Name, Name)]
    notShadowedLocals (LocalVars -> [(Name, Name)])
    -> TCMT IO LocalVars -> TCMT IO [(Name, Name)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO LocalVars
    forall (m :: * -> *). ReadTCState m => m LocalVars
    getLocalVars
      -- Note: Debug printout aligned with the one in
      -- Agda.Syntax.Concrete.Operators.buildParsers.
      reportS "scope.operators" 50
        [ "flat  = " ++ prettyShow flat
        , "defs  = " ++ prettyShow defs
        , "locals= " ++ prettyShow locals
        ]
      let localNots  = ((Name, Name) -> NewNotation) -> [(Name, Name)] -> [NewNotation]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, Name) -> NewNotation
    localOp [(Name, Name)]
    locals
          notLocal   = Bool -> Bool
    not (Bool -> Bool) -> (NewNotation -> Bool) -> NewNotation -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [QName] -> QName -> Bool
    forall a. Ord a => [a] -> a -> Bool
    hasElem ((NewNotation -> QName) -> [NewNotation] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map NewNotation -> QName
    notaName [NewNotation]
    localNots) (QName -> Bool) -> (NewNotation -> QName) -> NewNotation -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NewNotation -> QName
    notaName
          otherNots  = (List1 NewNotation -> [NewNotation])
    -> [List1 NewNotation] -> [NewNotation]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ((NewNotation -> Bool) -> List1 NewNotation -> [NewNotation]
    forall a. (a -> Bool) -> NonEmpty a -> [a]
    List1.filter NewNotation -> Bool
    notLocal) [List1 NewNotation]
    defs
      return $ second (map useDefaultFixity) $ split $ localNots ++ otherNots
      where
        localOp :: (Name, Name) -> NewNotation
    localOp (Name
    x, Name
    y) = QName -> Name -> NewNotation
    namesToNotation (Name -> QName
    QName Name
    x) Name
    y
        split :: [NewNotation] -> ([QName], [NewNotation])
    split          = [Either QName NewNotation] -> ([QName], [NewNotation])
    forall a b. [Either a b] -> ([a], [b])
    partitionEithers ([Either QName NewNotation] -> ([QName], [NewNotation]))
    -> ([NewNotation] -> [Either QName NewNotation])
    -> [NewNotation]
    -> ([QName], [NewNotation])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (NewNotation -> [Either QName NewNotation])
    -> [NewNotation] -> [Either QName NewNotation]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap NewNotation -> [Either QName NewNotation]
    opOrNot
        opOrNot :: NewNotation -> [Either QName NewNotation]
    opOrNot NewNotation
    n      = QName -> Either QName NewNotation
    forall a b. a -> Either a b
    Left (NewNotation -> QName
    notaName NewNotation
    n) Either QName NewNotation
    -> [Either QName NewNotation] -> [Either QName NewNotation]
    forall a. a -> [a] -> [a]
    :
                         [NewNotation -> Either QName NewNotation
    forall a b. b -> Either a b
    Right NewNotation
    n | Bool -> Bool
    not ([NotationPart] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (NewNotation -> [NotationPart]
    notation NewNotation
    n))]