{-# LANGUAGE CPP                        #-}
-- | 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
#if __GLASGOW_HASKELL__ < 804
import Data.Semigroup
#endif

import Agda.Syntax.Builtin (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'
  -- 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

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 (QName Name
x) <- Pattern -> Pattern
removeParenP Pattern
p
                        -> Name -> DeclaredNames
declaresName Name
x
  FunClause{}           -> forall a. Monoid a => a
mempty
  DataSig Range
_ 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
_ 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
_ 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
_ 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
  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 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))
    | String -> Bool
isBuiltinNoDef 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