{-# 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 ([(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
    -- Otherwise, do the union.
    | 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
    --  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 (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__

    -- Compute a list of conflicts in a format suitable for error reporting.
    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 ]

    -- Check for no conflict.
    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)

-- | 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 = 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
    (Fixities
f1, Polarities
p1) <- MonadicFixPol m -> m (Fixities, Polarities)
forall (m :: * -> *). MonadicFixPol m -> m (Fixities, Polarities)
runMonadicFixPol MonadicFixPol m
c1
    (Fixities
f2, Polarities
p2) <- MonadicFixPol m -> m (Fixities, Polarities)
forall (m :: * -> *). MonadicFixPol m -> m (Fixities, Polarities)
runMonadicFixPol MonadicFixPol m
c2
    Fixities
f <- Fixities -> Fixities -> m Fixities
forall (m :: * -> *).
MonadFixityError m =>
Fixities -> Fixities -> m Fixities
plusFixities Fixities
f1 Fixities
f2
    Polarities
p <- Polarities -> Polarities -> m Polarities
forall {m :: * -> *} {b}.
MonadFixityError m =>
Map Name b -> Map Name b -> m (Map Name b)
mergePolarities Polarities
p1 Polarities
p2
    (Fixities, Polarities) -> m (Fixities, Polarities)
forall a. a -> m a
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
      | 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
      -- Only the keys are used.
      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)

-- | 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) <- 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 Set Name
declared Set Name
postulates Set Name
privateNames = (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
  let publicNames :: Set Name
publicNames = Set Name
declared Set Name -> Set Name -> Set Name
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 <- Set Name -> m Fixities -> (Set Name -> m Fixities) -> m Fixities
forall a b. Null a => a -> b -> (a -> b) -> b
ifNull (Fixities -> Set Name
forall k a. Map k a -> Set k
Map.keysSet Fixities
fixs Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set Name
declared) (Fixities -> m Fixities
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Fixities
fixs) ((Set Name -> m Fixities) -> m Fixities)
-> (Set Name -> m Fixities) -> m Fixities
forall a b. (a -> b) -> a -> b
$ \ 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
    -- Note: Data.Map.restrictKeys requires containers >= 0.5.8.2
    -- return $ Map.restrictKeys fixs declared
    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

  -- Same for undefined names in polarity declarations.
  Polarities
pols <- Set Name
-> m Polarities -> (Set Name -> m Polarities) -> m Polarities
forall a b. Null a => a -> b -> (a -> b) -> b
ifNull (Polarities -> Set Name
forall k a. Map k a -> Set k
Map.keysSet Polarities
pols Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set Name
declared) (Polarities -> m Polarities
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Polarities
pols) ((Set Name -> m Polarities) -> m Polarities)
-> (Set Name -> m Polarities) -> m Polarities
forall a b. (a -> b) -> a -> b
$
    \ 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
      -- Note: Data.Map.restrictKeys requires containers >= 0.5.8.2
      -- return $ Map.restrictKeys polarities declared
      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

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

  -- Check that every polarity pragma is used for a postulate.
  Set Name -> m () -> (Set Name -> m ()) -> m ()
forall a b. Null a => a -> b -> (a -> b) -> b
ifNull (Polarities -> Set Name
forall k a. Map k a -> Set k
Map.keysSet Polarities
pols Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set Name
postulates) (() -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((Set Name -> m ()) -> m ()) -> (Set Name -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$
    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 ()) -> (Set Name -> m ()) -> Set Name -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> m ()
forall (m :: * -> *).
(MonadFixityError m, HasCallStack) =>
[Name] -> m ()
warnPolarityPragmasButNotPostulates ([Name] -> m ()) -> (Set Name -> [Name]) -> Set Name -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Name -> [Name]
forall a. Set a -> [a]
Set.toList

  (Fixities, Polarities) -> m (Fixities, Polarities)
forall a. a -> m a
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' = (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
  -- These declarations define polarities:
  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
  -- These declarations define fixities:
  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)
  -- We look into these blocks:
  Mutual    Range
_ [Declaration]
ds' -> [Declaration] -> MonadicFixPol m
forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds'
  InterleavedMutual Range
_ [Declaration]
ds' -> [Declaration] -> MonadicFixPol m
forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds'
  Abstract  Range
_ [Declaration]
ds' -> [Declaration] -> MonadicFixPol m
forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds'
  Private Range
_ Origin
_ [Declaration]
ds' -> [Declaration] -> MonadicFixPol m
forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds'
  InstanceB Range
_ [Declaration]
ds' -> [Declaration] -> MonadicFixPol m
forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds'
  Macro     Range
_ [Declaration]
ds' -> [Declaration] -> MonadicFixPol m
forall (m :: * -> *).
MonadFixityError m =>
[Declaration] -> MonadicFixPol m
fixitiesAndPolarities' [Declaration]
ds'
  Opaque    Range
_ [Declaration]
ds' -> [Declaration] -> MonadicFixPol m
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         {}  -> 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
  RecordDirective {}  -> 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]

-- | 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            -> (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 RecordDirectives
d [LamBinding]
_ [Declaration]
_   -> [Name] -> DeclaredNames
declaresNames ([Name] -> DeclaredNames) -> [Name] -> DeclaredNames
forall a b. (a -> b) -> a -> b
$     (Name -> [Name]) -> Maybe Name -> [Name]
forall m a. Monoid m => (a -> m) -> Maybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[]) ((Name, IsInstance) -> Name
forall a b. (a, b) -> a
fst ((Name, IsInstance) -> Name)
-> Maybe (Name, IsInstance) -> Maybe Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecordDirectives -> Maybe (Name, IsInstance)
forall a. RecordDirectives' a -> Maybe a
recConstructor RecordDirectives
d)
  Record Range
_ Erased
_ Name
x RecordDirectives
d [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]
: (Name -> [Name]) -> Maybe Name -> [Name]
forall m a. Monoid m => (a -> m) -> Maybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[]) ((Name, IsInstance) -> Name
forall a b. (a, b) -> a
fst ((Name, IsInstance) -> Name)
-> Maybe (Name, IsInstance) -> Maybe Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RecordDirectives -> Maybe (Name, IsInstance)
forall a. RecordDirectives' a -> Maybe a
recConstructor RecordDirectives
d)
  RecordDirective RecordDirective
_     -> DeclaredNames
forall a. Monoid a => a
mempty
  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 [Arg Name]
_ Pattern
_    -> Name -> DeclaredNames
declaresName Name
x
  Mutual    Range
_ [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    Range
_ [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 Range
_ [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  Range
_ [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 Range
_ 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 Range
_ [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     Range
_ [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 Range
_ [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 Range
_ [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 Range
_ [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 Range
_ [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)
  -- BUILTIN pragmas which do not require an accompanying definition declare
  -- the (unqualified) name they mention.
  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