    {-# 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.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 (PragmaPolarities)

    import Agda.Utils.CallStack (HasCallStack)
    import Agda.Utils.Functor
    import Agda.Utils.List1 (List1)
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Null
    import Agda.Utils.Set1 (Set1)
    import qualified Agda.Utils.Set1 as Set1
    import Agda.Utils.Tuple (Pair(Pair))

    import Agda.Utils.Impossible

    type Fixities   = Map Name Fixity'
    type Polarities = Map Name PragmaPolarities

    class Monad m => MonadFixityError m where
      throwMultipleFixityDecls            :: List1 (Name, Pair Fixity') -> m a
      throwMultiplePolarityPragmas        :: List1 Name -> m a
      warnUnknownNamesInFixityDecl        :: HasCallStack => Set1 Name -> m ()
      warnUnknownNamesInPolarityPragmas   :: HasCallStack => Set1 Name -> m ()
      warnUnknownFixityInMixfixDecl       :: HasCallStack => Set1 Name -> m ()
      warnPolarityPragmasButNotPostulates :: HasCallStack => Set1 Name -> m ()
      warnEmptyPolarityPragma             :: HasCallStack => Range -> 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.
        | Just NonEmpty (Name, Pair Fixity')
    ds <- [(Name, Pair Fixity')] -> Maybe (NonEmpty (Name, Pair Fixity'))
    forall a. [a] -> Maybe (NonEmpty a)
    List1.nonEmpty [(Name, Pair Fixity')]
    isect = NonEmpty (Name, Pair Fixity') -> m Fixities
    forall a. NonEmpty (Name, Pair Fixity') -> m a
    forall (m :: * -> *) a.
    MonadFixityError m =>
    NonEmpty (Name, Pair Fixity') -> m a
    throwMultipleFixityDecls NonEmpty (Name, Pair Fixity')
    ds
        -- 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, Pair Fixity')]
    isect = [ (Name
    x, (Fixities -> Fixity') -> Pair Fixities -> Pair Fixity'
    forall a b. (a -> b) -> Pair a -> Pair b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (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) (Pair Fixities -> Pair Fixity') -> Pair Fixities -> Pair Fixity'
    forall a b. (a -> b) -> a -> b
    $ Fixities -> Fixities -> Pair Fixities
    forall a. a -> a -> Pair a
    Pair 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
        (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
        -- Merge disjoint maps.
        mergePolarities :: Map Name a -> Map Name a -> m (Map Name a)
    mergePolarities Map Name a
    p1 Map Name a
    p2 =
          [Name]
    -> m (Map Name a)
    -> (List1 Name -> m (Map Name a))
    -> m (Map Name a)
    forall a b. [a] -> b -> (List1 a -> b) -> b
    List1.ifNull (Map Name a -> [Name]
    forall k a. Map k a -> [k]
    Map.keys (Map Name a -> [Name]) -> Map Name a -> [Name]
    forall a b. (a -> b) -> a -> b
    $ Map Name a -> Map Name a -> Map Name a
    forall k a b. Ord k => Map k a -> Map k b -> Map k a
    Map.intersection Map Name a
    p1 Map Name a
    p2)
            {-then-} (Map Name a -> m (Map Name a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Map Name a -> m (Map Name a)) -> Map Name a -> m (Map Name a)
    forall a b. (a -> b) -> a -> b
    $ 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)
            {-else-} \ List1 Name
    ks -> List1 Name -> m (Map Name a)
    forall a. List1 Name -> m a
    forall (m :: * -> *) a. MonadFixityError m => List1 Name -> m a
    throwMultiplePolarityPragmas List1 Name
    ks

    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
      (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

      -- If we have names in fixity declarations which are not defined in the
      -- appropriate scope, raise a warning and delete them from fixs.
      fixs <- Set1.ifNull (Map.keysSet fixs Set.\\ declared) (return fixs) $ \ Set1 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
    $ Set1 Name -> m ()
    forall (m :: * -> *).
    (MonadFixityError m, HasCallStack) =>
    Set1 Name -> m ()
    warnUnknownNamesInFixityDecl Set1 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.
      pols <- Set1.ifNull (Map.keysSet pols Set.\\ declared) (return pols) $
        \ Set1 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
    $ Set1 Name -> m ()
    forall (m :: * -> *).
    (MonadFixityError m, HasCallStack) =>
    Set1 Name -> m ()
    warnUnknownNamesInPolarityPragmas Set1 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 -> PragmaPolarities -> Bool) -> Polarities -> Polarities
    forall k a. (k -> a -> Bool) -> Map k a -> Map k a
    Map.filterWithKey (\ Name
    k PragmaPolarities
    _ -> 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
      Set1.unlessNull (Set.filter isOpenMixfix publicNames Set.\\ Map.keysSet fixs) $
        when (doWarn == DoWarn) . warnUnknownFixityInMixfixDecl

      -- Check that every polarity pragma is used for a postulate.
      Set1.unlessNull (Map.keysSet pols Set.\\ postulates) $
        when (doWarn == DoWarn) . warnPolarityPragmasButNotPostulates

      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
      -- These declarations define polarities:
      Pragma (PolarityPragma Range
    r Name
    x [Ranged Occurrence]
    occs) ->
        [Ranged Occurrence]
    -> MonadicFixPol m
    -> (PragmaPolarities -> MonadicFixPol m)
    -> MonadicFixPol m
    forall a b. [a] -> b -> (List1 a -> b) -> b
    List1.ifNull [Ranged Occurrence]
    occs (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
    $ Range -> m ()
    forall (m :: * -> *).
    (MonadFixityError m, HasCallStack) =>
    Range -> m ()
    warnEmptyPolarityPragma Range
    r m () -> (Fixities, Polarities) -> m (Fixities, Polarities)
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> (Fixities, Polarities)
    forall a. Monoid a => a
    mempty) {-else-} \ PragmaPolarities
    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 -> PragmaPolarities -> Polarities
    forall k a. k -> a -> Map k a
    Map.singleton Name
    x PragmaPolarities
    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    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'
      -- 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
      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 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
    _ Catchall
    _
        | 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)
      -- 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

    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