{-# 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 m1 m2
    -- If maps are not disjoint, report conflicts as exception.
    | not (null isect) = throwMultipleFixityDecls isect
    -- 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, map (Map.findWithDefault __IMPOSSIBLE__ x) [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
    mergePolarities p1 p2
      | Map.null i = return (Map.union p1 p2)
      | otherwise  = throwMultiplePolarityPragmas $
                     map fst $ Map.toList i
      where
      -- Only the keys are used.
      i = Map.intersection p1 p2

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 <- ifNull (Map.keysSet fixs Set.\\ declared) (return fixs) $ \ unknownFixs -> do
    when (doWarn == DoWarn) $ warnUnknownNamesInFixityDecl $ Set.toList 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 <- ifNull (Map.keysSet pols Set.\\ declared) (return pols) $
    \ unknownPols -> do
      when (doWarn == DoWarn) $ warnUnknownNamesInPolarityPragmas $ Set.toList 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
  ifNull (Set.filter isOpenMixfix publicNames Set.\\ Map.keysSet fixs) (return ()) $
    when (doWarn == DoWarn) . warnUnknownFixityInMixfixDecl . Set.toList

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

  return (fixs, pols)

fixitiesAndPolarities' :: MonadFixityError m => [Declaration] -> MonadicFixPol m
fixitiesAndPolarities' = foldMap $ \case
  -- These declarations define polarities:
  Pragma (PolarityPragma _ x occs) -> returnPol $ Map.singleton x occs
  -- These declarations define fixities:
  Syntax x syn    -> returnFix $ Map.singleton x (Fixity' noFixity syn $ getRange x)
  Infix  f xs     -> returnFix $ Map.fromList $ for (List1.toList xs) $ \ x -> (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'
  -- 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
  RecordDirective {}  -> 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

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 d _ _   -> declaresNames $     foldMap (:[]) (fst <$> recConstructor d)
  Record _ x d _ _ _    -> declaresNames $ x : foldMap (:[]) (fst <$> recConstructor d)
  RecordDirective _     -> mempty
  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
  Open{}                -> 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))
    | isBuiltinNoDef $ rangedThing b -> declaresName x
  Pragma{}             -> mempty