-- | 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 Agda.Syntax.Abstract.Name (AbstractName (..), AbstractModule (..), KindOfName(..))
import Agda.Syntax.Abstract.Name qualified 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

-- | 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
      IsPattern DisplayLHS
YesDisplayLHS -> Bool -> AbstractName -> Bool
forall a b. a -> b -> a
const Bool
True
        -- #8228: Non-constructor-like operators are useful in DISPLAY
        -- pragmas.
      IsPattern DisplayLHS
NoDisplayLHS -> 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] -> VerboseLevel -> [[Char]] -> TCMT IO ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> VerboseLevel -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [[Char]] -> m ()
reportS [Char]
"scope.operators" VerboseLevel
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))]