{-# OPTIONS_GHC -Wunused-imports #-}

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