content: {-# OPTIONS_GHC -Wunused-imports #-}
  {-# OPTIONS_GHC -Wunused-matches #-}
  {-# OPTIONS_GHC -Wunused-binds #-}
  
  -- | 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 m1 m2
      -- If maps are not disjoint, report conflicts as exception.
      | Just ds <- List1.nonEmpty isect = throwMultipleFixityDecls ds
      -- Otherwise, do the union.
      | otherwise        = return $ Map.unionWithKey mergeFixites m1 m2
    where
      --  Merge two fixities, assuming there is no conflict
      mergeFixites _name (Fixity' f1 s1 r1) (Fixity' f2 s2 r2) = Fixity' f s $ fuseRange r1 r2
                where f | null f1 = f2
                        | null f2 = f1
                        | otherwise = __IMPOSSIBLE__
                      s | null s1 = s2
                        | null s2 = s1
                        | otherwise = __IMPOSSIBLE__
  
      -- Compute a list of conflicts in a format suitable for error reporting.
      isect = [ (x, fmap (Map.findWithDefault __IMPOSSIBLE__ x) $ Pair m1 m2)
              | (x, False) <- Map.assocs $ Map.intersectionWith compatible m1 m2 ]
  
      -- Check for no conflict.
      compatible (Fixity' f1 s1 _) (Fixity' f2 s2 _) =
        (null f1 || null f2) &&
        (null s1 || null 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 { runMonadicFixPol :: m (Fixities, Polarities) }
  
  returnFix :: Monad m => Fixities -> MonadicFixPol m
  returnFix fx = MonadicFixPol $ return (fx, Map.empty)
  
  returnPol :: Monad m => Polarities -> MonadicFixPol m
  returnPol pol = MonadicFixPol $ return (Map.empty, pol)
  
  instance MonadFixityError m => Semigroup (MonadicFixPol m) where
    c1 <> c2 = MonadicFixPol $ do
      (f1, p1) <- runMonadicFixPol c1
      (f2, p2) <- runMonadicFixPol c2
      f <- plusFixities f1 f2
      p <- mergePolarities p1 p2
      return (f, p)
      where
      -- Merge disjoint maps.
      mergePolarities p1 p2 =
        List1.ifNull (Map.keys $ Map.intersection p1 p2)
          {-then-} (return $ Map.union p1 p2)
          {-else-} \ ks -> throwMultiplePolarityPragmas ks
  
  instance MonadFixityError m => Monoid (MonadicFixPol m) where
    mempty  = MonadicFixPol $ return (Map.empty, Map.empty)
    mappend = (<>)
  
  data DoWarn = NoWarn | DoWarn
    deriving (Eq, 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 doWarn ds = do
    (fixs, pols) <- runMonadicFixPol $ fixitiesAndPolarities' ds
    let DeclaredNames declared postulates privateNames = foldMap declaredNames ds
    let publicNames = declared Set.\\ 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) $ \ unknownFixs -> do
      when (doWarn == DoWarn) $ warnUnknownNamesInFixityDecl unknownFixs
      -- Note: Data.Map.restrictKeys requires containers >= 0.5.8.2
      -- return $ Map.restrictKeys fixs declared
      return $ Map.filterWithKey (\ k _ -> Set.member k declared) fixs
  
    -- Same for undefined names in polarity declarations.
    pols <- Set1.ifNull (Map.keysSet pols Set.\\ declared) (return pols) $
      \ unknownPols -> do
        when (doWarn == DoWarn) $ warnUnknownNamesInPolarityPragmas unknownPols
        -- Note: Data.Map.restrictKeys requires containers >= 0.5.8.2
        -- return $ Map.restrictKeys polarities declared
        return $ Map.filterWithKey (\ k _ -> Set.member k declared) 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' = foldMap $ \case
    -- These declarations define polarities:
    Pragma (PolarityPragma r x occs) ->
      List1.ifNull occs (MonadicFixPol $ warnEmptyPolarityPragma r $> mempty) {-else-} \ occs ->
        returnPol $ Map.singleton x occs
    -- These declarations define fixities:
    Syntax x syn    -> returnFix $ Map.singleton x (Fixity' noFixity syn $ getRange x)
    Infix  f xs1    -> flip foldMap xs1 \ x ->
      -- Andreas, 2025-07-25, issue #5224: Warn when @xs1@ contains duplicates.
      -- We achieve this through 'plusFixities'.
      returnFix $ Map.singleton x $ Fixity' f noNotation $ getRange x
    -- We look into these blocks:
    Mutual    _ ds' -> fixitiesAndPolarities' ds'
    InterleavedMutual _ ds' -> fixitiesAndPolarities' ds'
    Abstract  _ ds' -> fixitiesAndPolarities' ds'
    Private _ _ ds' -> fixitiesAndPolarities' ds'
    InstanceB _ ds' -> fixitiesAndPolarities' ds'
    Macro     _ ds' -> fixitiesAndPolarities' ds'
    Opaque    _ ds' -> fixitiesAndPolarities' 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         {}  -> mempty
    FieldSig        {}  -> mempty
    Generalize      {}  -> mempty
    Field           {}  -> mempty
    FunClause       {}  -> mempty
    DataSig         {}  -> mempty
    DataDef         {}  -> mempty
    Data            {}  -> mempty
    RecordSig       {}  -> mempty
    RecordDef       {}  -> mempty
    Record          {}  -> mempty
    LoneConstructor {}  -> mempty
    PatternSyn      {}  -> mempty
    Postulate       {}  -> mempty
    Primitive       {}  -> mempty
    Open            {}  -> mempty
    Import          {}  -> mempty
    ModuleMacro     {}  -> mempty
    Module          {}  -> mempty
    UnquoteDecl     {}  -> mempty
    UnquoteDef      {}  -> mempty
    UnquoteData     {}  -> mempty
    Pragma          {}  -> mempty
    Unfolding       {}  -> mempty
  
  data DeclaredNames = DeclaredNames { _allNames, _postulates, _privateNames :: Set Name }
  
  instance Semigroup DeclaredNames where
    DeclaredNames xs ps as <> DeclaredNames ys qs bs =
      DeclaredNames (xs <> ys) (ps <> qs) (as <> bs)
  
  instance Monoid DeclaredNames where
    mempty  = DeclaredNames Set.empty Set.empty Set.empty
    mappend = (<>)
  
  allPostulates :: DeclaredNames -> DeclaredNames
  allPostulates (DeclaredNames xs ps as) = DeclaredNames xs (xs <> ps) as
  
  allPrivateNames :: DeclaredNames -> DeclaredNames
  allPrivateNames (DeclaredNames xs ps as) = DeclaredNames xs ps (xs <> as)
  
  declaresNames :: [Name] -> DeclaredNames
  declaresNames xs = DeclaredNames (Set.fromList xs) Set.empty Set.empty
  
  declaresName :: Name -> DeclaredNames
  declaresName x = declaresNames [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 = \case
    TypeSig _ _ x _       -> declaresName x
    FieldSig _ _ x _      -> declaresName x
    Field _ fs            -> foldMap declaredNames fs
    FunClause _ (LHS p [] []) _ _ _
      | IdentP _ (QName x) <- removeParenP p
                          -> declaresName x
    FunClause{}           -> mempty
    DataSig _ _ x _ _     -> declaresName x
    DataDef _ _ _ cs      -> foldMap declaredNames cs
    Data _ _ x _ _ cs     -> declaresName x <> foldMap declaredNames cs
    RecordSig _ _ x _ _   -> declaresName x
    RecordDef _ _x ds _ _ -> declaresNames $     maybeToList (recDirConstructor ds)
    Record _ _ x ds _ _ _ -> declaresNames $ x : maybeToList (recDirConstructor ds)
    Infix _ _             -> mempty
    Syntax _ _            -> mempty
    PatternSyn _ x _ _    -> declaresName x
    Mutual    _ ds        -> foldMap declaredNames ds
    InterleavedMutual    _ ds -> foldMap declaredNames ds
    LoneConstructor _ ds  -> foldMap declaredNames ds
    Abstract  _ ds        -> foldMap declaredNames ds
    Private _ _ ds        -> allPrivateNames $ foldMap declaredNames ds
    InstanceB _ ds        -> foldMap declaredNames ds
    Macro     _ ds        -> foldMap declaredNames ds
    Postulate _ ds        -> allPostulates $ foldMap declaredNames ds
    Primitive _ ds        -> foldMap declaredNames ds
    Generalize _ ds       -> foldMap declaredNames ds
    Opaque _ ds           -> foldMap declaredNames ds
    Open{}                -> mempty
    Unfolding{}           -> mempty
    Import{}              -> mempty
    ModuleMacro{}         -> mempty
    Module{}              -> mempty
    UnquoteDecl _ xs _    -> declaresNames xs
    UnquoteDef{}          -> mempty
    UnquoteData _ x cs _  -> declaresNames (x:cs)
    -- BUILTIN pragmas which do not require an accompanying definition declare
    -- the (unqualified) name they mention.
    Pragma (BuiltinPragma _ b (QName x))
      | any isBuiltinNoDef . builtinById $ rangedThing b -> declaresName x
    Pragma{}             -> mempty
  
  recDirConstructor :: [RecordDirective] -> Maybe Name
  recDirConstructor = listToMaybe . mapMaybe \case
    Constructor x _ -> Just x
    _ -> Nothing
  