{-# OPTIONS_GHC -Wunused-imports #-}
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 ()
plusFixities :: MonadFixityError m => Fixities -> Fixities -> m Fixities
plusFixities :: forall (m :: * -> *).
MonadFixityError m =>
Fixities -> Fixities -> m Fixities
plusFixities Fixities
m1 Fixities
m2
| 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
| 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
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__
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 ]
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)
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
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)
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
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
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
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
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
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
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
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
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)
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'
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]
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)
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