-- | Computing scopes of names that are relevant to parsing
--   some raw expression.
module Agda.Syntax.Scope.Operator
  ( OperatorScope(..)
  , getOperatorScope
  , getDefinedNames
  , localNames
  ) where

import Prelude hiding ( (||) )

import Data.Bifunctor
import Data.Either (partitionEithers)
import Data.Foldable
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map

import Data.Set (Set)
import qualified Data.Set as Set

import qualified Agda.Syntax.Abstract.Name as A

import Agda.Syntax.Common
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, NonEmpty(..))
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.AssocList (AssocList)
import Agda.Utils.Impossible

-- | Names that are relevant to operator parsing.
data OperatorScope = OpScope {
    OperatorScope -> Bool
osHasOps :: !Bool                            -- ^ Are there any operators or notations in scope?
  , OperatorScope -> Map QName (List1 AbstractName)
osScope  :: (Map QName (List1 AbstractName)) -- ^ All relevant names in global scope.
  , OperatorScope -> AssocList Name Name
osLocals :: !(AssocList Name A.Name)         -- ^ Relevant names in local scope.
  }

instance Pretty OperatorScope where
  prettyPrec :: Int -> OperatorScope -> Doc
prettyPrec Int
x (OpScope Bool
_ Map QName (List1 AbstractName)
scope AssocList Name Name
locals) = Int -> (Map QName (List1 AbstractName), AssocList Name Name) -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
x (Map QName (List1 AbstractName)
scope, AssocList Name Name
locals)

-- | Looking up all name parts of a QName.
namePartScopeLookup :: QName -> ScopeInfo -> [Map Name (List1 AbstractName)]
namePartScopeLookup :: QName -> ScopeInfo -> [Map Name (List1 AbstractName)]
namePartScopeLookup QName
q ScopeInfo
scope = [Map Name (List1 AbstractName)]
inAllScopes [Map Name (List1 AbstractName)]
-> [Map Name (List1 AbstractName)]
-> [Map Name (List1 AbstractName)]
forall a. [a] -> [a] -> [a]
++ [Map Name (List1 AbstractName)]
imports
  where
    -- 1. Finding a name in the current scope and its parents.
    inAllScopes :: [Map Name (List1 AbstractName)]
    inAllScopes :: [Map Name (List1 AbstractName)]
inAllScopes = (Scope -> [Map Name (List1 AbstractName)])
-> [Scope] -> [Map Name (List1 AbstractName)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (QName -> Scope -> [Map Name (List1 AbstractName)]
findName QName
q) [Scope]
allScopes

    -- 2. Finding a name in the imports belonging to an initial part of the qualifier.
    imports :: [Map Name (List1 AbstractName)]
    imports :: [Map Name (List1 AbstractName)]
imports = do
      let -- return all possible splittings, e.g.
          -- splitName X.Y.Z = [(X, Y.Z), (X.Y, Z)]
          splitName :: QName -> [(QName, QName)]
          splitName :: QName -> [(QName, QName)]
splitName (QName Name
x)  = []
          splitName (Qual Name
x QName
q) =
            (Name -> QName
QName Name
x, QName
q) (QName, QName) -> [(QName, QName)] -> [(QName, QName)]
forall a. a -> [a] -> [a]
: [ (Name -> QName -> QName
Qual Name
x QName
m, QName
r) | (QName
m, QName
r) <- QName -> [(QName, QName)]
splitName QName
q ]

      (m, x) <- QName -> [(QName, QName)]
splitName QName
q
      s <- allScopes
      m <- maybeToList $ Map.lookup m $ scopeImports s
      findName x $ restrictPrivate $ moduleScope m

    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

    allScopes :: [Scope]
    allScopes :: [Scope]
allScopes = 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) 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

    findName :: QName -> Scope -> [Map Name (List1 AbstractName)]
    findName :: QName -> Scope -> [Map Name (List1 AbstractName)]
findName QName
q0 Scope
s = case QName
q0 of
      QName Name
x  -> do
        n       <- Name -> [[Char]]
nameStringParts Name
x
        (_, ns) <- scopeNameSpaces s
        maybeToList $ Map.lookup n (nsNameParts ns)
      Qual Name
x QName
q -> do
        m <- AbstractModule -> ModuleName
amodName (AbstractModule -> ModuleName)
-> ((AbstractModule, Access) -> AbstractModule)
-> (AbstractModule, Access)
-> ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractModule, Access) -> AbstractModule
forall a b. (a, b) -> a
fst ((AbstractModule, Access) -> ModuleName)
-> [(AbstractModule, Access)] -> [ModuleName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Scope -> [(AbstractModule, Access)]
forall a. InScope a => Name -> Scope -> [(a, Access)]
findNameInScope Name
x Scope
s
        let ss = Scope -> Scope
restrictPrivate (Scope -> Scope) -> Maybe Scope -> Maybe Scope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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)
        s' <- maybeToList ss
        findName q s'

getOperatorScope :: Set QName -> ScopeInfo -> OperatorScope
getOperatorScope :: Set QName -> ScopeInfo -> OperatorScope
getOperatorScope Set QName
names ScopeInfo
scope = let

    nameList :: [QName]
    nameList :: [QName]
nameList = Set QName -> [QName]
forall a. Set a -> [a]
Set.toList Set QName
names

    namePartSet :: Set NameParts
    namePartSet :: Set NameParts
namePartSet = let
      getParts :: QName -> NameParts
      getParts :: QName -> NameParts
getParts (QName Name
x)  = Name -> NameParts
nameParts Name
x
      getParts (Qual Name
_ QName
x) = QName -> NameParts
getParts QName
x

      go :: Set NameParts -> QName -> Set NameParts
      go :: Set NameParts -> QName -> Set NameParts
go Set NameParts
acc QName
x = let
        parts :: NameParts
parts = QName -> NameParts
getParts QName
x
        goPart :: Set NameParts -> NamePart -> Set NameParts
goPart !Set NameParts
acc NamePart
Hole  = Set NameParts
acc
        goPart Set NameParts
acc (Id [Char]
x) = NameParts -> Set NameParts -> Set NameParts
forall a. Ord a => a -> Set a -> Set a
Set.insert ([Char] -> NamePart
Id [Char]
x NamePart -> [NamePart] -> NameParts
forall a. a -> [a] -> NonEmpty a
:| []) Set NameParts
acc
        in (Set NameParts -> NamePart -> Set NameParts)
-> Set NameParts -> NameParts -> Set NameParts
forall b a. (b -> a -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Set NameParts -> NamePart -> Set NameParts
goPart (NameParts -> Set NameParts -> Set NameParts
forall a. Ord a => a -> Set a -> Set a
Set.insert NameParts
parts Set NameParts
acc) NameParts
parts

      in (Set NameParts -> QName -> Set NameParts)
-> Set NameParts -> [QName] -> Set NameParts
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Set NameParts -> QName -> Set NameParts
go Set NameParts
forall a. Monoid a => a
mempty [QName]
nameList

    -- look up the name as a full identifier
    fullNameLookups :: [(QName, List1 AbstractName)]
    fullNameLookups :: [(QName, List1 AbstractName)]
fullNameLookups = do
      qname <- [QName]
nameList
      case scopeLookup qname scope of
        []   -> []
        AbstractName
a:[AbstractName]
as -> [(QName
qname, AbstractName
a AbstractName -> [AbstractName] -> List1 AbstractName
forall a. a -> [a] -> NonEmpty a
:| [AbstractName]
as)]

    requalify :: QName -> Name -> QName
    requalify :: QName -> Name -> QName
requalify QName
qn Name
n = case QName
qn of
      QName Name
_   -> Name -> QName
QName Name
n
      Qual Name
x QName
qn -> Name -> QName -> QName
Qual Name
x (QName -> QName) -> QName -> QName
forall a b. (a -> b) -> a -> b
$! QName -> Name -> QName
requalify QName
qn Name
n

    -- lookup all parts of a name as operator/notation parts
    namePartLookups :: [(QName, List1 AbstractName)]
    namePartLookups :: [(QName, List1 AbstractName)]
namePartLookups = do
      qname      <- [QName]
nameList
      map        <- namePartScopeLookup qname scope
      (name, as) <- Map.toList map
      let !name' = QName -> Name -> QName
requalify QName
qname Name
name
      pure (name', as)

    goLocals :: LocalVars -> (AssocList Name A.Name, Bool)
    goLocals :: LocalVars -> (AssocList Name Name, Bool)
goLocals LocalVars
ls = LocalVars -> Set Name -> (AssocList Name Name, Bool)
go LocalVars
ls Set Name
forall a. Monoid a => a
mempty where
      go :: LocalVars -> Set Name -> (AssocList Name A.Name, Bool)
      go :: LocalVars -> Set Name -> (AssocList Name Name, Bool)
go [] !Set Name
seen = ([], Bool
False)
      go ((Name
x, LocalVar
a):LocalVars
ls) Set Name
seen | Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Name
x Set Name
seen = LocalVars -> Set Name -> (AssocList Name Name, Bool)
go LocalVars
ls Set Name
seen
      go ((Name
x, LocalVar
a):LocalVars
ls) Set Name
seen = case LocalVar -> Maybe Name
notShadowedLocal LocalVar
a of
        Maybe Name
Nothing -> LocalVars -> Set Name -> (AssocList Name Name, Bool)
go LocalVars
ls Set Name
seen
        Just Name
a  ->
          let goNamePart :: NamePart -> Bool
goNamePart = \case
                Id [Char]
x -> NameParts -> Set NameParts -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member ([Char] -> NamePart
Id [Char]
x NamePart -> [NamePart] -> NameParts
forall a. a -> [a] -> NonEmpty a
:| []) Set NameParts
namePartSet
                NamePart
_    -> Bool
False
              goNotPart :: NotationPart -> Bool
goNotPart = \case
                IdPart RString
x -> NameParts -> Set NameParts -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member ([Char] -> NamePart
Id (RString -> [Char]
forall a. Ranged a -> a
rangedThing RString
x) NamePart -> [NamePart] -> NameParts
forall a. a -> [a] -> NonEmpty a
:| []) Set NameParts
namePartSet
                NotationPart
_        -> Bool
False
              not :: Notation
not           = Fixity' -> Notation
theNotation (Name -> Fixity'
A.nameFixity Name
a)
              parts :: NameParts
parts         = Name -> NameParts
nameParts Name
x
              anyOp :: Bool
anyOp         = ((NamePart -> Bool) -> NameParts -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (NamePart -> NamePart -> Bool
forall a. Eq a => a -> a -> Bool
== NamePart
Hole) NameParts
parts Bool -> Bool -> Bool
&& (NamePart -> Bool) -> NameParts -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any NamePart -> Bool
goNamePart NameParts
parts) Bool -> Bool -> Bool
forall a. Boolean a => a -> a -> a
|| (NotationPart -> Bool) -> Notation -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any NotationPart -> Bool
goNotPart Notation
not
              anyName :: Bool
anyName       = NameParts -> Set NameParts -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member NameParts
parts Set NameParts
namePartSet
              (AssocList Name Name
ls', Bool
anyOp') = LocalVars -> Set Name -> (AssocList Name Name, Bool)
go LocalVars
ls (Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
Set.insert Name
x Set Name
seen)
              !anyOp'' :: Bool
anyOp''      = Bool
anyOp Bool -> Bool -> Bool
forall a. Boolean a => a -> a -> a
|| Bool
anyOp'
              !ls'' :: AssocList Name Name
ls''         = if Bool
anyOp Bool -> Bool -> Bool
forall a. Boolean a => a -> a -> a
|| Bool
anyName then (Name
x, Name
a)(Name, Name) -> AssocList Name Name -> AssocList Name Name
forall a. a -> [a] -> [a]
:AssocList Name Name
ls' else AssocList Name Name
ls'
          in (AssocList Name Name
ls'', Bool
anyOp'')

    (AssocList Name Name
locals, Bool
hasLocalOp) = LocalVars -> (AssocList Name Name, Bool)
goLocals (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)

  in if [(QName, List1 AbstractName)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(QName, List1 AbstractName)]
namePartLookups Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
hasLocalOp
    then Bool
-> Map QName (List1 AbstractName)
-> AssocList Name Name
-> OperatorScope
OpScope Bool
False ((List1 AbstractName -> List1 AbstractName -> List1 AbstractName)
-> [(QName, List1 AbstractName)] -> Map QName (List1 AbstractName)
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith ((List1 AbstractName -> List1 AbstractName -> List1 AbstractName)
-> List1 AbstractName -> List1 AbstractName -> List1 AbstractName
forall a b c. (a -> b -> c) -> b -> a -> c
flip List1 AbstractName -> List1 AbstractName -> List1 AbstractName
forall a. Eq a => List1 a -> List1 a -> List1 a
List1.union) [(QName, List1 AbstractName)]
fullNameLookups) AssocList Name Name
locals
    else Bool
-> Map QName (List1 AbstractName)
-> AssocList Name Name
-> OperatorScope
OpScope Bool
True  ((List1 AbstractName -> List1 AbstractName -> List1 AbstractName)
-> [(QName, List1 AbstractName)] -> Map QName (List1 AbstractName)
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith ((List1 AbstractName -> List1 AbstractName -> List1 AbstractName)
-> List1 AbstractName -> List1 AbstractName -> List1 AbstractName
forall a b c. (a -> b -> c) -> b -> a -> c
flip List1 AbstractName -> List1 AbstractName -> List1 AbstractName
forall a. Eq a => List1 a -> List1 a -> List1 a
List1.union) ([(QName, List1 AbstractName)]
fullNameLookups [(QName, List1 AbstractName)]
-> [(QName, List1 AbstractName)] -> [(QName, List1 AbstractName)]
forall a. [a] -> [a] -> [a]
++ [(QName, List1 AbstractName)]
namePartLookups)) AssocList Name Name
locals


-- | 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) -> OperatorScope -> [List1 NewNotation]
getDefinedNames' :: (AbstractName -> Bool) -> OperatorScope -> [List1 NewNotation]
getDefinedNames' AbstractName -> Bool
f (OpScope Bool
_ Map QName (List1 AbstractName)
names AssocList Name Name
_) =
  [ 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 -> OperatorScope -> [List1 NewNotation]
getDefinedNames :: KindsOfNames -> OperatorScope -> [List1 NewNotation]
getDefinedNames KindsOfNames
kinds = (AbstractName -> Bool) -> OperatorScope -> [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 -> OperatorScope -> ScopeM ([QName], [NewNotation])
localNames :: ExprKind
-> Maybe QName -> OperatorScope -> ScopeM ([QName], [NewNotation])
localNames ExprKind
k Maybe QName
top opScope :: OperatorScope
opScope@(OpScope Bool
_ Map QName (List1 AbstractName)
_ AssocList Name Name
locals) = 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) -> OperatorScope -> [List1 NewNotation]
getDefinedNames' AbstractName -> Bool
f OperatorScope
opScope

  -- Note: Debug printout aligned with the one in
  -- Agda.Syntax.Concrete.Operators.buildParsers.
  [Char] -> Int -> [[Char]] -> TCMT IO ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> Int -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [[Char]] -> m ()
reportS [Char]
"scope.operators" Int
50
    [ [Char]
"opScope  = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ OperatorScope -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow OperatorScope
opScope
    , [Char]
"defs     = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [List1 NewNotation] -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow [List1 NewNotation]
defs
    , [Char]
"locals   = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ AssocList Name Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow AssocList Name Name
locals
    ]
  let localNots :: [NewNotation]
localNots  = ((Name, Name) -> NewNotation)
-> AssocList Name Name -> [NewNotation]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Name) -> NewNotation
localOp AssocList Name Name
locals
      notLocal :: NewNotation -> Bool
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 :: [NewNotation]
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
  ([QName], [NewNotation]) -> ScopeM ([QName], [NewNotation])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (([QName], [NewNotation]) -> ScopeM ([QName], [NewNotation]))
-> ([QName], [NewNotation]) -> ScopeM ([QName], [NewNotation])
forall a b. (a -> b) -> a -> b
$ ([NewNotation] -> [NewNotation])
-> ([QName], [NewNotation]) -> ([QName], [NewNotation])
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((NewNotation -> NewNotation) -> [NewNotation] -> [NewNotation]
forall a b. (a -> b) -> [a] -> [b]
map NewNotation -> NewNotation
useDefaultFixity) (([QName], [NewNotation]) -> ([QName], [NewNotation]))
-> ([QName], [NewNotation]) -> ([QName], [NewNotation])
forall a b. (a -> b) -> a -> b
$ [NewNotation] -> ([QName], [NewNotation])
split ([NewNotation] -> ([QName], [NewNotation]))
-> [NewNotation] -> ([QName], [NewNotation])
forall a b. (a -> b) -> a -> b
$ [NewNotation]
localNots [NewNotation] -> [NewNotation] -> [NewNotation]
forall a. [a] -> [a] -> [a]
++ [NewNotation]
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 (Notation -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (NewNotation -> Notation
notation NewNotation
n))]