    {-# 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 ([(Name, [Fixity'])] -> Bool
    forall a. Null a => a -> Bool
    null [(Name, [Fixity'])]
    isect) = [(Name, [Fixity'])] -> m Fixities
    forall (m :: * -> *) a.
    MonadFixityError m =>
    [(Name, [Fixity'])] -> m a
    throwMultipleFixityDecls [(Name, [Fixity'])]
    isect
        -- Otherwise, do the union.
        | Bool
    otherwise        = Fixities -> m Fixities
    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 (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 (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 :: * -> *} {a}.
    MonadFixityError m =>
    Map Name a -> Map Name a -> m (Map Name a)
    mergePolarities Polarities
    p1 Polarities
    p2
        (Fixities, Polarities) -> m (Fixities, Polarities)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Fixities
    f, Polarities
    p)
        where
        mergePolarities :: Map Name a -> Map Name a -> m (Map Name a)
    mergePolarities Map Name a
    p1 Map Name a
    p2
          | Set Name -> Bool
    forall a. Set a -> Bool
    Set.null Set Name
    i = Map Name a -> m (Map Name a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Map Name a -> Map Name a -> Map Name a
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union Map Name a
    p1 Map Name a
    p2)
          | Bool
    otherwise  = [Name] -> m (Map Name a)
    forall (m :: * -> *) a. MonadFixityError m => [Name] -> m a
    throwMultiplePolarityPragmas (Set Name -> [Name]
    forall a. Set a -> [a]
    Set.toList Set Name
    i)
          where
          i :: Set Name
    i = Set Name -> Set Name -> Set Name
    forall a. Ord a => Set a -> Set a -> Set a
    Set.intersection (Map Name a -> Set Name
    forall k a. Map k a -> Set k
    Map.keysSet Map Name a
    p1) (Map Name a -> Set Name
    forall k a. Map k a -> Set k
    Map.keysSet Map Name a
    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 (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
    /= :: DoWarn -> DoWarn -> Bool
    $c/= :: DoWarn -> DoWarn -> Bool
    == :: DoWarn -> DoWarn -> Bool
    $c== :: 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
    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) <- 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 (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 (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 (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 (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 (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 (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 (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 (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 (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 -> [Name]
    forall a. NonEmpty a -> [a]
    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'
      -- 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
      Pragma          {}  -> 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 (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{}          -> DeclaredNames
    forall a. Monoid a => a
    mempty
      DataSig Range
    _ Name
    x [LamBinding]
    _ Expr
    _      -> Name -> DeclaredNames
    declaresName Name
    x
      DataDef Range
    _ Name
    _ [LamBinding]
    _ [Declaration]
    cs     -> (Declaration -> DeclaredNames) -> [Declaration] -> DeclaredNames
    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 DeclaredNames -> DeclaredNames -> DeclaredNames
    forall a. Semigroup a => a -> a -> a
    <> (Declaration -> DeclaredNames) -> [Declaration] -> DeclaredNames
    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 ([Name] -> DeclaredNames) -> [Name] -> DeclaredNames
    forall a b. (a -> b) -> a -> b
    $     (Name -> [Name]) -> Maybe Name -> [Name]
    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
    _ 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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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
      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
      -- 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 (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