{-# 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.Maybe
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 ([(Name, [Fixity'])] -> Bool
forall a. Null a => a -> Bool
null [(Name, [Fixity'])]
isect) = [(Name, [Fixity'])] -> m Fixities
forall a. [(Name, [Fixity'])] -> m a
forall (m :: * -> *) a.
MonadFixityError m =>
[(Name, [Fixity'])] -> m a
throwMultipleFixityDecls [(Name, [Fixity'])]
isect
| Bool
otherwise = Fixities -> m Fixities
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Fixities -> m Fixities) -> Fixities -> m Fixities
forall a b. (a -> b) -> a -> b
$ (Name -> Fixity' -> Fixity' -> Fixity')
-> Fixities -> Fixities -> Fixities
forall k a.
Ord k =>
(k -> a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWithKey Name -> Fixity' -> Fixity' -> Fixity'
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 (Range -> Fixity') -> Range -> Fixity'
forall a b. (a -> b) -> a -> b
$ Range -> Range -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Range
r1 Range
r2
where f :: Fixity
f | Fixity -> Bool
forall a. Null a => a -> Bool
null Fixity
f1 = Fixity
f2
| Fixity -> Bool
forall a. Null a => a -> Bool
null Fixity
f2 = Fixity
f1
| Bool
otherwise = Fixity
forall a. HasCallStack => a
__IMPOSSIBLE__
s :: Notation
s | Notation -> Bool
forall a. Null a => a -> Bool
null Notation
s1 = Notation
s2
| Notation -> Bool
forall a. Null a => a -> Bool
null Notation
s2 = Notation
s1
| Bool
otherwise = Notation
forall a. HasCallStack => a
__IMPOSSIBLE__
isect :: [(Name, [Fixity'])]
isect = [ (Name
x, (Fixities -> Fixity') -> [Fixities] -> [Fixity']
forall a b. (a -> b) -> [a] -> [b]
map (Fixity' -> Name -> Fixities -> Fixity'
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Fixity'
forall a. HasCallStack => a
__IMPOSSIBLE__ Name
x) [Fixities
m1,Fixities
m2])
| (Name
x, Bool
False) <- Map Name Bool -> [(Name, Bool)]
forall k a. Map k a -> [(k, a)]
Map.assocs (Map Name Bool -> [(Name, Bool)])
-> Map Name Bool -> [(Name, Bool)]
forall a b. (a -> b) -> a -> b
$ (Fixity' -> Fixity' -> Bool)
-> Fixities -> Fixities -> Map Name Bool
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
_) =
(Fixity -> Bool
forall a. Null a => a -> Bool
null Fixity
f1 Bool -> Bool -> Bool
|| Fixity -> Bool
forall a. Null a => a -> Bool
null Fixity
f2) Bool -> Bool -> Bool
&&
(Notation -> Bool
forall a. Null a => a -> Bool
null Notation
s1 Bool -> Bool -> Bool
|| Notation -> 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 = m (Fixities, Polarities) -> MonadicFixPol m
forall (m :: * -> *). m (Fixities, Polarities) -> MonadicFixPol m
MonadicFixPol (m (Fixities, Polarities) -> MonadicFixPol m)
-> m (Fixities, Polarities) -> MonadicFixPol m
forall a b. (a -> b) -> a -> b
$ (Fixities, Polarities) -> m (Fixities, Polarities)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Fixities
fx, Polarities
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 = m (Fixities, Polarities) -> MonadicFixPol m
forall (m :: * -> *). m (Fixities, Polarities) -> MonadicFixPol m
MonadicFixPol (m (Fixities, Polarities) -> MonadicFixPol m)
-> m (Fixities, Polarities) -> MonadicFixPol m
forall a b. (a -> b) -> a -> b
$ (Fixities, Polarities) -> m (Fixities, Polarities)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Fixities
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 = m (Fixities, Polarities) -> MonadicFixPol m
forall (m :: * -> *). m (Fixities, Polarities) -> MonadicFixPol m
MonadicFixPol (m (Fixities, Polarities) -> MonadicFixPol m)
-> m (Fixities, Polarities) -> MonadicFixPol m
forall a b. (a -> b) -> a -> b
$ do
(f1, p1) <- MonadicFixPol m -> m (Fixities, Polarities)
forall (m :: * -> *). MonadicFixPol m -> m (Fixities, Polarities)
runMonadicFixPol MonadicFixPol m
c1
(f2, p2) <- runMonadicFixPol c2
f <- plusFixities f1 f2
p <- mergePolarities p1 p2
return (f, p)
where
mergePolarities :: Map Name b -> Map Name b -> m (Map Name b)
mergePolarities Map Name b
p1 Map Name b
p2
| Map Name b -> Bool
forall k a. Map k a -> Bool
Map.null Map Name b
i = Map Name b -> m (Map Name b)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Name b -> Map Name b -> Map Name b
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 = [Name] -> m (Map Name b)
forall a. [Name] -> m a
forall (m :: * -> *) a. MonadFixityError m => [Name] -> m a
throwMultiplePolarityPragmas ([Name] -> m (Map Name b)) -> [Name] -> m (Map Name b)
forall a b. (a -> b) -> a -> b
$
((Name, b) -> Name) -> [(Name, b)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, b) -> Name
forall a b. (a, b) -> a
fst ([(Name, b)] -> [Name]) -> [(Name, b)] -> [Name]
forall a b. (a -> b) -> a -> b
$ Map Name b -> [(Name, b)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Name b
i
where
i :: Map Name b
i = Map Name b -> Map Name b -> Map Name b
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 = m (Fixities, Polarities) -> MonadicFixPol m
forall (m :: * -> *). m (Fixities, Polarities) -> MonadicFixPol m
MonadicFixPol (m (Fixities, Polarities) -> MonadicFixPol m)
-> m (Fixities, Polarities) -> MonadicFixPol m
forall a b. (a -> b) -> a -> b
$ (Fixities, Polarities) -> m (Fixities, Polarities)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Fixities
forall k a. Map k a
Map.empty, Polarities
forall k a. Map k a
Map.empty)
mappend :: MonadicFixPol m -> MonadicFixPol m -> MonadicFixPol m
mappend = MonadicFixPol m -> MonadicFixPol m -> MonadicFixPol m
forall a. Semigroup a => a -> a -> a
(<>)
data DoWarn = NoWarn | DoWarn
deriving (DoWarn -> DoWarn -> Bool
(DoWarn -> DoWarn -> Bool)
-> (DoWarn -> DoWarn -> Bool) -> Eq DoWarn
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DoWarn -> DoWarn -> Bool
== :: DoWarn -> DoWarn -> Bool
$c/= :: DoWarn -> DoWarn -> Bool
/= :: DoWarn -> DoWarn -> Bool
Eq, Int -> DoWarn -> ShowS
[DoWarn] -> ShowS
DoWarn -> String
(Int -> DoWarn -> ShowS)
-> (DoWarn -> String) -> ([DoWarn] -> ShowS) -> Show DoWarn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DoWarn -> ShowS
showsPrec :: Int -> DoWarn -> ShowS
$cshow :: DoWarn -> String
show :: DoWarn -> String
$cshowList :: [DoWarn] -> ShowS
showList :: [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
(fixs, pols) <- MonadicFixPol m -> m (Fixities, Polarities)
forall (m :: * -> *). MonadicFixPol m -> m (Fixities, Polarities)
runMonadicFixPol (MonadicFixPol m -> m (Fixities, Polarities))
-> MonadicFixPol m -> m (Fixities, Polarities)
forall a b. (a -> b) -> a -> b
$ [Declaration] -> MonadicFixPol m
forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds
let DeclaredNames declared postulates privateNames = foldMap declaredNames ds
let publicNames = Set Name
declared Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set Name
privateNames
fixs <- ifNull (Map.keysSet fixs Set.\\ declared) (return fixs) $ \ Set Name
unknownFixs -> do
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (DoWarn
doWarn DoWarn -> DoWarn -> Bool
forall a. Eq a => a -> a -> Bool
== DoWarn
DoWarn) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [Name] -> m ()
forall (m :: * -> *).
(MonadFixityError m, HasCallStack) =>
[Name] -> m ()
warnUnknownNamesInFixityDecl ([Name] -> m ()) -> [Name] -> m ()
forall a b. (a -> b) -> a -> b
$ Set Name -> [Name]
forall a. Set a -> [a]
Set.toList Set Name
unknownFixs
Fixities -> m Fixities
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Fixities -> m Fixities) -> Fixities -> m Fixities
forall a b. (a -> b) -> a -> b
$ (Name -> Fixity' -> Bool) -> Fixities -> Fixities
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\ Name
k Fixity'
_ -> Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Name
k Set Name
declared) Fixities
fixs
pols <- ifNull (Map.keysSet pols Set.\\ declared) (return pols) $
\ Set Name
unknownPols -> do
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (DoWarn
doWarn DoWarn -> DoWarn -> Bool
forall a. Eq a => a -> a -> Bool
== DoWarn
DoWarn) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [Name] -> m ()
forall (m :: * -> *).
(MonadFixityError m, HasCallStack) =>
[Name] -> m ()
warnUnknownNamesInPolarityPragmas ([Name] -> m ()) -> [Name] -> m ()
forall a b. (a -> b) -> a -> b
$ Set Name -> [Name]
forall a. Set a -> [a]
Set.toList Set Name
unknownPols
Polarities -> m Polarities
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Polarities -> m Polarities) -> Polarities -> m Polarities
forall a b. (a -> b) -> a -> b
$ (Name -> [Occurrence] -> Bool) -> Polarities -> Polarities
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\ Name
k [Occurrence]
_ -> Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Name
k Set Name
declared) Polarities
pols
ifNull (Set.filter isOpenMixfix publicNames Set.\\ Map.keysSet fixs) (return ()) $
when (doWarn == DoWarn) . warnUnknownFixityInMixfixDecl . Set.toList
ifNull (Map.keysSet pols Set.\\ postulates) (return ()) $
when (doWarn == DoWarn) . warnPolarityPragmasButNotPostulates . Set.toList
return (fixs, pols)
fixitiesAndPolarities' :: MonadFixityError m => [Declaration] -> MonadicFixPol m
fixitiesAndPolarities' :: forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' = (Declaration -> MonadicFixPol m)
-> [Declaration] -> MonadicFixPol m
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((Declaration -> MonadicFixPol m)
-> [Declaration] -> MonadicFixPol m)
-> (Declaration -> MonadicFixPol m)
-> [Declaration]
-> MonadicFixPol m
forall a b. (a -> b) -> a -> b
$ \case
Pragma (PolarityPragma Range
_ Name
x [Occurrence]
occs) -> Polarities -> MonadicFixPol m
forall (m :: * -> *). Monad m => Polarities -> MonadicFixPol m
returnPol (Polarities -> MonadicFixPol m) -> Polarities -> MonadicFixPol m
forall a b. (a -> b) -> a -> b
$ Name -> [Occurrence] -> Polarities
forall k a. k -> a -> Map k a
Map.singleton Name
x [Occurrence]
occs
Syntax Name
x Notation
syn -> Fixities -> MonadicFixPol m
forall (m :: * -> *). Monad m => Fixities -> MonadicFixPol m
returnFix (Fixities -> MonadicFixPol m) -> Fixities -> MonadicFixPol m
forall a b. (a -> b) -> a -> b
$ Name -> Fixity' -> Fixities
forall k a. k -> a -> Map k a
Map.singleton Name
x (Fixity -> Notation -> Range -> Fixity'
Fixity' Fixity
noFixity Notation
syn (Range -> Fixity') -> Range -> Fixity'
forall a b. (a -> b) -> a -> b
$ Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x)
Infix Fixity
f List1 Name
xs -> Fixities -> MonadicFixPol m
forall (m :: * -> *). Monad m => Fixities -> MonadicFixPol m
returnFix (Fixities -> MonadicFixPol m) -> Fixities -> MonadicFixPol m
forall a b. (a -> b) -> a -> b
$ [(Name, Fixity')] -> Fixities
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Name, Fixity')] -> Fixities) -> [(Name, Fixity')] -> Fixities
forall a b. (a -> b) -> a -> b
$ [Name] -> (Name -> (Name, Fixity')) -> [(Name, Fixity')]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for (List1 Name -> [Item (List1 Name)]
forall l. IsList l => l -> [Item l]
List1.toList List1 Name
xs) ((Name -> (Name, Fixity')) -> [(Name, Fixity')])
-> (Name -> (Name, Fixity')) -> [(Name, Fixity')]
forall a b. (a -> b) -> a -> b
$ \ Name
x -> (Name
x, Fixity -> Notation -> Range -> Fixity'
Fixity' Fixity
f Notation
noNotation (Range -> Fixity') -> Range -> Fixity'
forall a b. (a -> b) -> a -> b
$ Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x)
Mutual KwRange
_ [Declaration]
ds' -> [Declaration] -> MonadicFixPol m
forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds'
InterleavedMutual KwRange
_ [Declaration]
ds' -> [Declaration] -> MonadicFixPol m
forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds'
Abstract KwRange
_ [Declaration]
ds' -> [Declaration] -> MonadicFixPol m
forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds'
Private KwRange
_ Origin
_ [Declaration]
ds' -> [Declaration] -> MonadicFixPol m
forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds'
InstanceB KwRange
_ [Declaration]
ds' -> [Declaration] -> MonadicFixPol m
forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds'
Macro KwRange
_ [Declaration]
ds' -> [Declaration] -> MonadicFixPol m
forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds'
Opaque KwRange
_ [Declaration]
ds' -> [Declaration] -> MonadicFixPol m
forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds'
TypeSig {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
FieldSig {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
Generalize {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
Field {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
FunClause {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
DataSig {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
DataDef {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
Data {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
RecordSig {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
RecordDef {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
Record {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
LoneConstructor {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
PatternSyn {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
Postulate {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
Primitive {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
Open {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
Import {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
ModuleMacro {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
Module {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
UnquoteDecl {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
UnquoteDef {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
UnquoteData {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
Pragma {} -> MonadicFixPol m
forall a. Monoid a => a
mempty
Unfolding {} -> MonadicFixPol m
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 Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> Set Name
ys) (Set Name
ps Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> Set Name
qs) (Set Name
as Set Name -> Set Name -> Set Name
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 Set Name
forall a. Set a
Set.empty Set Name
forall a. Set a
Set.empty Set Name
forall a. Set a
Set.empty
mappend :: DeclaredNames -> DeclaredNames -> DeclaredNames
mappend = DeclaredNames -> DeclaredNames -> DeclaredNames
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 Set Name -> Set Name -> Set Name
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 Set Name -> Set Name -> Set Name
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 ([Name] -> Set Name
forall a. Ord a => [a] -> Set a
Set.fromList [Name]
xs) Set Name
forall a. Set a
Set.empty Set Name
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 KwRange
_ [Declaration]
fs -> (Declaration -> DeclaredNames) -> [Declaration] -> DeclaredNames
forall m a. Monoid m => (a -> m) -> [a] -> m
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{} -> DeclaredNames
forall a. Monoid a => a
mempty
DataSig Range
_ Erased
_ Name
x [LamBinding]
_ Expr
_ -> Name -> DeclaredNames
declaresName Name
x
DataDef Range
_ Name
_ [LamBinding]
_ [Declaration]
cs -> (Declaration -> DeclaredNames) -> [Declaration] -> DeclaredNames
forall m a. Monoid m => (a -> m) -> [a] -> m
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 DeclaredNames -> DeclaredNames -> DeclaredNames
forall a. Semigroup a => a -> a -> a
<> (Declaration -> DeclaredNames) -> [Declaration] -> DeclaredNames
forall m a. Monoid m => (a -> m) -> [a] -> m
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 [RecordDirective]
ds [LamBinding]
_ [Declaration]
_ -> [Name] -> DeclaredNames
declaresNames ([Name] -> DeclaredNames) -> [Name] -> DeclaredNames
forall a b. (a -> b) -> a -> b
$ Maybe Name -> [Name]
forall a. Maybe a -> [a]
maybeToList ([RecordDirective] -> Maybe Name
recDirConstructor [RecordDirective]
ds)
Record Range
_ Erased
_ Name
x [RecordDirective]
ds [LamBinding]
_ Expr
_ [Declaration]
_ -> [Name] -> DeclaredNames
declaresNames ([Name] -> DeclaredNames) -> [Name] -> DeclaredNames
forall a b. (a -> b) -> a -> b
$ Name
x Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: Maybe Name -> [Name]
forall a. Maybe a -> [a]
maybeToList ([RecordDirective] -> Maybe Name
recDirConstructor [RecordDirective]
ds)
Infix Fixity
_ List1 Name
_ -> DeclaredNames
forall a. Monoid a => a
mempty
Syntax Name
_ Notation
_ -> DeclaredNames
forall a. Monoid a => a
mempty
PatternSyn Range
_ Name
x [WithHiding Name]
_ Pattern
_ -> Name -> DeclaredNames
declaresName Name
x
Mutual KwRange
_ [Declaration]
ds -> (Declaration -> DeclaredNames) -> [Declaration] -> DeclaredNames
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
InterleavedMutual KwRange
_ [Declaration]
ds -> (Declaration -> DeclaredNames) -> [Declaration] -> DeclaredNames
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
LoneConstructor KwRange
_ [Declaration]
ds -> (Declaration -> DeclaredNames) -> [Declaration] -> DeclaredNames
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
Abstract KwRange
_ [Declaration]
ds -> (Declaration -> DeclaredNames) -> [Declaration] -> DeclaredNames
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
Private KwRange
_ Origin
_ [Declaration]
ds -> DeclaredNames -> DeclaredNames
allPrivateNames (DeclaredNames -> DeclaredNames) -> DeclaredNames -> DeclaredNames
forall a b. (a -> b) -> a -> b
$ (Declaration -> DeclaredNames) -> [Declaration] -> DeclaredNames
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
InstanceB KwRange
_ [Declaration]
ds -> (Declaration -> DeclaredNames) -> [Declaration] -> DeclaredNames
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
Macro KwRange
_ [Declaration]
ds -> (Declaration -> DeclaredNames) -> [Declaration] -> DeclaredNames
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
Postulate KwRange
_ [Declaration]
ds -> DeclaredNames -> DeclaredNames
allPostulates (DeclaredNames -> DeclaredNames) -> DeclaredNames -> DeclaredNames
forall a b. (a -> b) -> a -> b
$ (Declaration -> DeclaredNames) -> [Declaration] -> DeclaredNames
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
Primitive KwRange
_ [Declaration]
ds -> (Declaration -> DeclaredNames) -> [Declaration] -> DeclaredNames
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
Generalize KwRange
_ [Declaration]
ds -> (Declaration -> DeclaredNames) -> [Declaration] -> DeclaredNames
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
Opaque KwRange
_ [Declaration]
ds -> (Declaration -> DeclaredNames) -> [Declaration] -> DeclaredNames
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> DeclaredNames
declaredNames [Declaration]
ds
Open{} -> DeclaredNames
forall a. Monoid a => a
mempty
Unfolding{} -> DeclaredNames
forall a. Monoid a => a
mempty
Import{} -> DeclaredNames
forall a. Monoid a => a
mempty
ModuleMacro{} -> DeclaredNames
forall a. Monoid a => a
mempty
Module{} -> DeclaredNames
forall a. Monoid a => a
mempty
UnquoteDecl Range
_ [Name]
xs Expr
_ -> [Name] -> DeclaredNames
declaresNames [Name]
xs
UnquoteDef{} -> DeclaredNames
forall a. Monoid a => a
mempty
UnquoteData Range
_ Name
x [Name]
cs Expr
_ -> [Name] -> DeclaredNames
declaresNames (Name
xName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
cs)
Pragma (BuiltinPragma Range
_ RString
b (QName Name
x))
| (BuiltinId -> Bool) -> Maybe BuiltinId -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any BuiltinId -> Bool
isBuiltinNoDef (Maybe BuiltinId -> Bool)
-> (String -> Maybe BuiltinId) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe BuiltinId
builtinById (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ RString -> String
forall a. Ranged a -> a
rangedThing RString
b -> Name -> DeclaredNames
declaresName Name
x
Pragma{} -> DeclaredNames
forall a. Monoid a => a
mempty
recDirConstructor :: [RecordDirective] -> Maybe Name
recDirConstructor :: [RecordDirective] -> Maybe Name
recDirConstructor = [Name] -> Maybe Name
forall a. [a] -> Maybe a
listToMaybe ([Name] -> Maybe Name)
-> ([RecordDirective] -> [Name]) -> [RecordDirective] -> Maybe Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RecordDirective -> Maybe Name) -> [RecordDirective] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe \case
Constructor Name
x IsInstance
_ -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
RecordDirective
_ -> Maybe Name
forall a. Maybe a
Nothing