{-# OPTIONS_GHC -Wunused-imports #-}

-- | Collecting fixity declarations (and polarity pragmas) for concrete
--   declarations.

module Agda.Syntax.Concrete.Fixity
  ( Fixities, Polarities, MonadFixityError(..)
  , DoWarn(..)
  , fixitiesAndPolarities
  ) where

import Prelude hiding (null)

import Control.Monad
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set

import Agda.Syntax.Builtin (builtinById, isBuiltinNoDef)
import Agda.Syntax.Common
import Agda.Syntax.Concrete
import Agda.Syntax.Position
import Agda.TypeChecking.Positivity.Occurrence (Occurrence)

import Agda.Utils.CallStack (HasCallStack)
import Agda.Utils.Functor
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Null
import Agda.Utils.Impossible


type Fixities   = Map Name Fixity'
type Polarities = Map Name [Occurrence]

class Monad m => MonadFixityError m where
  throwMultipleFixityDecls            :: [(Name, [Fixity'])] -> m a
  throwMultiplePolarityPragmas        :: [Name] -> m a
  warnUnknownNamesInFixityDecl        :: HasCallStack => [Name] -> m ()
  warnUnknownNamesInPolarityPragmas   :: HasCallStack => [Name] -> m ()
  warnUnknownFixityInMixfixDecl       :: HasCallStack => [Name] -> m ()
  warnPolarityPragmasButNotPostulates :: HasCallStack => [Name] -> m ()

-- | Add more fixities. Throw an exception for multiple fixity declarations.
--   OR:  Disjoint union of fixity maps.  Throws exception if not disjoint.

plusFixities :: MonadFixityError m => Fixities -> Fixities -> m Fixities
plusFixities :: forall (m :: * -> *).
MonadFixityError m =>
Fixities -> Fixities -> m Fixities
plusFixities Fixities
m1 Fixities
m2
    -- If maps are not disjoint, report conflicts as exception.
    | Bool -> Bool
not (forall a. Null a => a -> Bool
null [(Name, [Fixity'])]
isect) = forall (m :: * -> *) a.
MonadFixityError m =>
[(Name, [Fixity'])] -> m a
throwMultipleFixityDecls [(Name, [Fixity'])]
isect
    -- Otherwise, do the union.
    | Bool
otherwise        = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k a.
Ord k =>
(k -> a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWithKey forall {p}. p -> Fixity' -> Fixity' -> Fixity'
mergeFixites Fixities
m1 Fixities
m2
  where
    --  Merge two fixities, assuming there is no conflict
    mergeFixites :: p -> Fixity' -> Fixity' -> Fixity'
mergeFixites p
name (Fixity' Fixity
f1 Notation
s1 Range
r1) (Fixity' Fixity
f2 Notation
s2 Range
r2) = Fixity -> Notation -> Range -> Fixity'
Fixity' Fixity
f Notation
s forall a b. (a -> b) -> a -> b
$ forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Range
r1 Range
r2
              where f :: Fixity
f | forall a. Null a => a -> Bool
null Fixity
f1 = Fixity
f2
                      | forall a. Null a => a -> Bool
null Fixity
f2 = Fixity
f1
                      | Bool
otherwise = forall a. HasCallStack => a
__IMPOSSIBLE__
                    s :: Notation
s | forall a. Null a => a -> Bool
null Notation
s1 = Notation
s2
                      | forall a. Null a => a -> Bool
null Notation
s2 = Notation
s1
                      | Bool
otherwise = forall a. HasCallStack => a
__IMPOSSIBLE__

    -- Compute a list of conflicts in a format suitable for error reporting.
    isect :: [(Name, [Fixity'])]
isect = [ (Name
x, forall a b. (a -> b) -> [a] -> [b]
map (forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ Name
x) [Fixities
m1,Fixities
m2])
            | (Name
x, Bool
False) <- forall k a. Map k a -> [(k, a)]
Map.assocs forall a b. (a -> b) -> a -> b
$ forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith Fixity' -> Fixity' -> Bool
compatible Fixities
m1 Fixities
m2 ]

    -- Check for no conflict.
    compatible :: Fixity' -> Fixity' -> Bool
compatible (Fixity' Fixity
f1 Notation
s1 Range
_) (Fixity' Fixity
f2 Notation
s2 Range
_) =
      (forall a. Null a => a -> Bool
null Fixity
f1 Bool -> Bool -> Bool
|| forall a. Null a => a -> Bool
null Fixity
f2) Bool -> Bool -> Bool
&&
      (forall a. Null a => a -> Bool
null Notation
s1 Bool -> Bool -> Bool
|| forall a. Null a => a -> Bool
null Notation
s2)

-- | While 'Fixities' and Polarities are not semigroups under disjoint
--   union (which might fail), we get a semigroup instance for the
--   monadic @m (Fixities, Polarities)@ which propagates the first
--   error.
newtype MonadicFixPol m = MonadicFixPol { forall (m :: * -> *). MonadicFixPol m -> m (Fixities, Polarities)
runMonadicFixPol :: m (Fixities, Polarities) }

returnFix :: Monad m => Fixities -> MonadicFixPol m
returnFix :: forall (m :: * -> *). Monad m => Fixities -> MonadicFixPol m
returnFix Fixities
fx = forall (m :: * -> *). m (Fixities, Polarities) -> MonadicFixPol m
MonadicFixPol forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return (Fixities
fx, forall k a. Map k a
Map.empty)

returnPol :: Monad m => Polarities -> MonadicFixPol m
returnPol :: forall (m :: * -> *). Monad m => Polarities -> MonadicFixPol m
returnPol Polarities
pol = forall (m :: * -> *). m (Fixities, Polarities) -> MonadicFixPol m
MonadicFixPol forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return (forall k a. Map k a
Map.empty, Polarities
pol)

instance MonadFixityError m => Semigroup (MonadicFixPol m) where
  MonadicFixPol m
c1 <> :: MonadicFixPol m -> MonadicFixPol m -> MonadicFixPol m
<> MonadicFixPol m
c2 = forall (m :: * -> *). m (Fixities, Polarities) -> MonadicFixPol m
MonadicFixPol forall a b. (a -> b) -> a -> b
$ do
    (Fixities
f1, Polarities
p1) <- forall (m :: * -> *). MonadicFixPol m -> m (Fixities, Polarities)
runMonadicFixPol MonadicFixPol m
c1
    (Fixities
f2, Polarities
p2) <- forall (m :: * -> *). MonadicFixPol m -> m (Fixities, Polarities)
runMonadicFixPol MonadicFixPol m
c2
    Fixities
f <- forall (m :: * -> *).
MonadFixityError m =>
Fixities -> Fixities -> m Fixities
plusFixities Fixities
f1 Fixities
f2
    Polarities
p <- forall {m :: * -> *} {b}.
MonadFixityError m =>
Map Name b -> Map Name b -> m (Map Name b)
mergePolarities Polarities
p1 Polarities
p2
    forall (m :: * -> *) a. Monad m => a -> m a
return (Fixities
f, Polarities
p)
    where
    mergePolarities :: Map Name b -> Map Name b -> m (Map Name b)
mergePolarities Map Name b
p1 Map Name b
p2
      | forall k a. Map k a -> Bool
Map.null Map Name b
i = forall (m :: * -> *) a. Monad m => a -> m a
return (forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Name b
p1 Map Name b
p2)
      | Bool
otherwise  = forall (m :: * -> *) a. MonadFixityError m => [Name] -> m a
throwMultiplePolarityPragmas forall a b. (a -> b) -> a -> b
$
                     forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList Map Name b
i
      where
      -- Only the keys are used.
      i :: Map Name b
i = forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection Map Name b
p1 Map Name b
p2

instance MonadFixityError m => Monoid (MonadicFixPol m) where
  mempty :: MonadicFixPol m
mempty  = forall (m :: * -> *). m (Fixities, Polarities) -> MonadicFixPol m
MonadicFixPol forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return (forall k a. Map k a
Map.empty, forall k a. Map k a
Map.empty)
  mappend :: MonadicFixPol m -> MonadicFixPol m -> MonadicFixPol m
mappend = forall a. Semigroup a => a -> a -> a
(<>)

data DoWarn = NoWarn | DoWarn
  deriving (DoWarn -> DoWarn -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DoWarn -> DoWarn -> Bool
$c/= :: DoWarn -> DoWarn -> Bool
== :: DoWarn -> DoWarn -> Bool
$c== :: DoWarn -> DoWarn -> Bool
Eq, Int -> DoWarn -> ShowS
[DoWarn] -> ShowS
DoWarn -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DoWarn] -> ShowS
$cshowList :: [DoWarn] -> ShowS
show :: DoWarn -> String
$cshow :: DoWarn -> String
showsPrec :: Int -> DoWarn -> ShowS
$cshowsPrec :: Int -> DoWarn -> ShowS
Show)

-- | Get the fixities and polarity pragmas from the current block.
--   Doesn't go inside modules and where blocks.
--   The reason for this is that these declarations have to appear at the same
--   level (or possibly outside an abstract or mutual block) as their target
--   declaration.
fixitiesAndPolarities :: MonadFixityError m => DoWarn -> [Declaration] -> m (Fixities, Polarities)
fixitiesAndPolarities :: forall (m :: * -> *).
MonadFixityError m =>
DoWarn -> [Declaration] -> m (Fixities, Polarities)
fixitiesAndPolarities DoWarn
doWarn [Declaration]
ds = do
  (Fixities
fixs, Polarities
pols) <- forall (m :: * -> *). MonadicFixPol m -> m (Fixities, Polarities)
runMonadicFixPol forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds
  let DeclaredNames Set Name
declared Set Name
postulates Set Name
privateNames = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
  let publicNames :: Set Name
publicNames = Set Name
declared forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set Name
privateNames

  -- If we have names in fixity declarations which are not defined in the
  -- appropriate scope, raise a warning and delete them from fixs.
  Fixities
fixs <- forall a b. Null a => a -> b -> (a -> b) -> b
ifNull (forall k a. Map k a -> Set k
Map.keysSet Fixities
fixs forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set Name
declared) (forall (m :: * -> *) a. Monad m => a -> m a
return Fixities
fixs) forall a b. (a -> b) -> a -> b
$ \ Set Name
unknownFixs -> do
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (DoWarn
doWarn forall a. Eq a => a -> a -> Bool
== DoWarn
DoWarn) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadFixityError m, HasCallStack) =>
[Name] -> m ()
warnUnknownNamesInFixityDecl forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set Name
unknownFixs
    -- Note: Data.Map.restrictKeys requires containers >= 0.5.8.2
    -- return $ Map.restrictKeys fixs declared
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\ Name
k Fixity'
_ -> forall a. Ord a => a -> Set a -> Bool
Set.member Name
k Set Name
declared) Fixities
fixs

  -- Same for undefined names in polarity declarations.
  Polarities
pols <- forall a b. Null a => a -> b -> (a -> b) -> b
ifNull (forall k a. Map k a -> Set k
Map.keysSet Polarities
pols forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set Name
declared) (forall (m :: * -> *) a. Monad m => a -> m a
return Polarities
pols) forall a b. (a -> b) -> a -> b
$
    \ Set Name
unknownPols -> do
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (DoWarn
doWarn forall a. Eq a => a -> a -> Bool
== DoWarn
DoWarn) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadFixityError m, HasCallStack) =>
[Name] -> m ()
warnUnknownNamesInPolarityPragmas forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set Name
unknownPols
      -- Note: Data.Map.restrictKeys requires containers >= 0.5.8.2
      -- return $ Map.restrictKeys polarities declared
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\ Name
k [Occurrence]
_ -> forall a. Ord a => a -> Set a -> Bool
Set.member Name
k Set Name
declared) Polarities
pols

  -- If we have public mixfix identifiers without a corresponding fixity
  -- declaration, we raise a warning
  forall a b. Null a => a -> b -> (a -> b) -> b
ifNull (forall a. (a -> Bool) -> Set a -> Set a
Set.filter Name -> Bool
isOpenMixfix Set Name
publicNames forall a. Ord a => Set a -> Set a -> Set a
Set.\\ forall k a. Map k a -> Set k
Map.keysSet Fixities
fixs) (forall (m :: * -> *) a. Monad m => a -> m a
return ()) forall a b. (a -> b) -> a -> b
$
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (DoWarn
doWarn forall a. Eq a => a -> a -> Bool
== DoWarn
DoWarn) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
(MonadFixityError m, HasCallStack) =>
[Name] -> m ()
warnUnknownFixityInMixfixDecl forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList

  -- Check that every polarity pragma is used for a postulate.
  forall a b. Null a => a -> b -> (a -> b) -> b
ifNull (forall k a. Map k a -> Set k
Map.keysSet Polarities
pols forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set Name
postulates) (forall (m :: * -> *) a. Monad m => a -> m a
return ()) forall a b. (a -> b) -> a -> b
$
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (DoWarn
doWarn forall a. Eq a => a -> a -> Bool
== DoWarn
DoWarn) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
(MonadFixityError m, HasCallStack) =>
[Name] -> m ()
warnPolarityPragmasButNotPostulates forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList

  forall (m :: * -> *) a. Monad m => a -> m a
return (Fixities
fixs, Polarities
pols)

fixitiesAndPolarities' :: MonadFixityError m => [Declaration] -> MonadicFixPol m
fixitiesAndPolarities' :: forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a b. (a -> b) -> a -> b
$ \case
  -- These declarations define polarities:
  Pragma (PolarityPragma Range
_ Name
x [Occurrence]
occs) -> forall (m :: * -> *). Monad m => Polarities -> MonadicFixPol m
returnPol forall a b. (a -> b) -> a -> b
$ forall k a. k -> a -> Map k a
Map.singleton Name
x [Occurrence]
occs
  -- These declarations define fixities:
  Syntax Name
x Notation
syn    -> forall (m :: * -> *). Monad m => Fixities -> MonadicFixPol m
returnFix forall a b. (a -> b) -> a -> b
$ forall k a. k -> a -> Map k a
Map.singleton Name
x (Fixity -> Notation -> Range -> Fixity'
Fixity' Fixity
noFixity Notation
syn forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange Name
x)
  Infix  Fixity
f List1 Name
xs     -> forall (m :: * -> *). Monad m => Fixities -> MonadicFixPol m
returnFix forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for (forall l. IsList l => l -> [Item l]
List1.toList List1 Name
xs) forall a b. (a -> b) -> a -> b
$ \ Name
x -> (Name
x, Fixity -> Notation -> Range -> Fixity'
Fixity' Fixity
f Notation
noNotation forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange Name
x)
  -- We look into these blocks:
  Mutual    Range
_ [Declaration]
ds' -> forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds'
  InterleavedMutual Range
_ [Declaration]
ds' -> forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds'
  Abstract  Range
_ [Declaration]
ds' -> forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds'
  Private Range
_ Origin
_ [Declaration]
ds' -> forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds'
  InstanceB Range
_ [Declaration]
ds' -> forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds'
  Macro     Range
_ [Declaration]
ds' -> forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds'
  Opaque    Range
_ [Declaration]
ds' -> forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds'
  -- All other declarations are ignored.
  -- We expand these boring cases to trigger a revisit
  -- in case the @Declaration@ type is extended in the future.
  TypeSig         {}  -> forall a. Monoid a => a
mempty
  FieldSig        {}  -> forall a. Monoid a => a
mempty
  Generalize      {}  -> forall a. Monoid a => a
mempty
  Field           {}  -> forall a. Monoid a => a
mempty
  FunClause       {}  -> forall a. Monoid a => a
mempty
  DataSig         {}  -> forall a. Monoid a => a
mempty
  DataDef         {}  -> forall a. Monoid a => a
mempty
  Data            {}  -> forall a. Monoid a => a
mempty
  RecordSig       {}  -> forall a. Monoid a => a
mempty
  RecordDef       {}  -> forall a. Monoid a => a
mempty
  Record          {}  -> forall a. Monoid a => a
mempty
  RecordDirective {}  -> forall a. Monoid a => a
mempty
  LoneConstructor {}  -> forall a. Monoid a => a
mempty
  PatternSyn      {}  -> forall a. Monoid a => a
mempty
  Postulate       {}  -> forall a. Monoid a => a
mempty
  Primitive       {}  -> forall a. Monoid a => a
mempty
  Open            {}  -> forall a. Monoid a => a
mempty
  Import          {}  -> forall a. Monoid a => a
mempty
  ModuleMacro     {}  -> forall a. Monoid a => a
mempty
  Module          {}  -> forall a. Monoid a => a
mempty
  UnquoteDecl     {}  -> forall a. Monoid a => a
mempty
  UnquoteDef      {}  -> forall a. Monoid a => a
mempty
  UnquoteData     {}  -> forall a. Monoid a => a
mempty
  Pragma          {}  -> forall a. Monoid a => a
mempty
  Unfolding       {}  -> forall a. Monoid a => a
mempty

data DeclaredNames = DeclaredNames { DeclaredNames -> Set Name
_allNames, DeclaredNames -> Set Name
_postulates, DeclaredNames -> Set Name
_privateNames :: Set Name }

instance Semigroup DeclaredNames where
  DeclaredNames Set Name
xs Set Name
ps Set Name
as <> :: DeclaredNames -> DeclaredNames -> DeclaredNames
<> DeclaredNames Set Name
ys Set Name
qs Set Name
bs =
    Set Name -> Set Name -> Set Name -> DeclaredNames
DeclaredNames (Set Name
xs forall a. Semigroup a => a -> a -> a
<> Set Name
ys) (Set Name
ps forall a. Semigroup a => a -> a -> a
<> Set Name
qs) (Set Name
as forall a. Semigroup a => a -> a -> a
<> Set Name
bs)

instance Monoid DeclaredNames where
  mempty :: DeclaredNames
mempty  = Set Name -> Set Name -> Set Name -> DeclaredNames
DeclaredNames forall a. Set a
Set.empty forall a. Set a
Set.empty forall a. Set a
Set.empty
  mappend :: DeclaredNames -> DeclaredNames -> DeclaredNames
mappend = forall a. Semigroup a => a -> a -> a
(<>)

allPostulates :: DeclaredNames -> DeclaredNames
allPostulates :: DeclaredNames -> DeclaredNames
allPostulates (DeclaredNames Set Name
xs Set Name
ps Set Name
as) = Set Name -> Set Name -> Set Name -> DeclaredNames
DeclaredNames Set Name
xs (Set Name
xs forall a. Semigroup a => a -> a -> a
<> Set Name
ps) Set Name
as

allPrivateNames :: DeclaredNames -> DeclaredNames
allPrivateNames :: DeclaredNames -> DeclaredNames
allPrivateNames (DeclaredNames Set Name
xs Set Name
ps Set Name
as) = Set Name -> Set Name -> Set Name -> DeclaredNames
DeclaredNames Set Name
xs Set Name
ps (Set Name
xs forall a. Semigroup a => a -> a -> a
<> Set Name
as)

declaresNames :: [Name] -> DeclaredNames
declaresNames :: [Name] -> DeclaredNames
declaresNames [Name]
xs = Set Name -> Set Name -> Set Name -> DeclaredNames
DeclaredNames (forall a. Ord a => [a] -> Set a
Set.fromList [Name]
xs) forall a. Set a
Set.empty forall a. Set a
Set.empty

declaresName :: Name -> DeclaredNames
declaresName :: Name -> DeclaredNames
declaresName Name
x = [Name] -> DeclaredNames
declaresNames [Name
x]

-- | Compute the names defined in a declaration. We stay in the current scope,
--   i.e., do not go into modules.
declaredNames :: Declaration -> DeclaredNames
declaredNames :: Declaration -> DeclaredNames
declaredNames = \case
  TypeSig ArgInfo
_ TacticAttribute
_ Name
x Expr
_       -> Name -> DeclaredNames
declaresName Name
x
  FieldSig IsInstance
_ TacticAttribute
_ Name
x Arg Expr
_      -> Name -> DeclaredNames
declaresName Name
x
  Field Range
_ [Declaration]
fs            -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
fs
  FunClause (LHS Pattern
p [] []) RHS
_ WhereClause
_ Bool
_
    | IdentP Bool
_ (QName Name
x) <- Pattern -> Pattern
removeParenP Pattern
p
                        -> Name -> DeclaredNames
declaresName Name
x
  FunClause{}           -> forall a. Monoid a => a
mempty
  DataSig Range
_ Erased
_ Name
x [LamBinding]
_ Expr
_     -> Name -> DeclaredNames
declaresName Name
x
  DataDef Range
_ Name
_ [LamBinding]
_ [Declaration]
cs      -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
cs
  Data Range
_ Erased
_ Name
x [LamBinding]
_ Expr
_ [Declaration]
cs     -> Name -> DeclaredNames
declaresName Name
x forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
cs
  RecordSig Range
_ Erased
_ Name
x [LamBinding]
_ Expr
_   -> Name -> DeclaredNames
declaresName Name
x
  RecordDef Range
_ Name
x RecordDirectives
d [LamBinding]
_ [Declaration]
_   -> [Name] -> DeclaredNames
declaresNames forall a b. (a -> b) -> a -> b
$     forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall a. a -> [a] -> [a]
:[]) (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. RecordDirectives' a -> Maybe a
recConstructor RecordDirectives
d)
  Record Range
_ Erased
_ Name
x RecordDirectives
d [LamBinding]
_ Expr
_ [Declaration]
_  -> [Name] -> DeclaredNames
declaresNames forall a b. (a -> b) -> a -> b
$ Name
x forall a. a -> [a] -> [a]
: forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall a. a -> [a] -> [a]
:[]) (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. RecordDirectives' a -> Maybe a
recConstructor RecordDirectives
d)
  RecordDirective RecordDirective
_     -> forall a. Monoid a => a
mempty
  Infix Fixity
_ List1 Name
_             -> forall a. Monoid a => a
mempty
  Syntax Name
_ Notation
_            -> forall a. Monoid a => a
mempty
  PatternSyn Range
_ Name
x [Arg Name]
_ Pattern
_    -> Name -> DeclaredNames
declaresName Name
x
  Mutual    Range
_ [Declaration]
ds        -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
  InterleavedMutual    Range
_ [Declaration]
ds -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
  LoneConstructor Range
_ [Declaration]
ds  -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
  Abstract  Range
_ [Declaration]
ds        -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
  Private Range
_ Origin
_ [Declaration]
ds        -> DeclaredNames -> DeclaredNames
allPrivateNames forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
  InstanceB Range
_ [Declaration]
ds        -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
  Macro     Range
_ [Declaration]
ds        -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
  Postulate Range
_ [Declaration]
ds        -> DeclaredNames -> DeclaredNames
allPostulates forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
  Primitive Range
_ [Declaration]
ds        -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
  Generalize Range
_ [Declaration]
ds       -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
  Opaque Range
_ [Declaration]
ds           -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
  Open{}                -> forall a. Monoid a => a
mempty
  Unfolding{}           -> forall a. Monoid a => a
mempty
  Import{}              -> forall a. Monoid a => a
mempty
  ModuleMacro{}         -> forall a. Monoid a => a
mempty
  Module{}              -> forall a. Monoid a => a
mempty
  UnquoteDecl Range
_ [Name]
xs Expr
_    -> [Name] -> DeclaredNames
declaresNames [Name]
xs
  UnquoteDef{}          -> forall a. Monoid a => a
mempty
  UnquoteData Range
_ Name
x [Name]
cs Expr
_  -> [Name] -> DeclaredNames
declaresNames (Name
xforall a. a -> [a] -> [a]
:[Name]
cs)
  -- BUILTIN pragmas which do not require an accompanying definition declare
  -- the (unqualified) name they mention.
  Pragma (BuiltinPragma Range
_ RString
b (QName Name
x))
    | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any BuiltinId -> Bool
isBuiltinNoDef forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe BuiltinId
builtinById forall a b. (a -> b) -> a -> b
$ forall a. Ranged a -> a
rangedThing RString
b -> Name -> DeclaredNames
declaresName Name
x
  Pragma{}             -> forall a. Monoid a => a
mempty