content: {-# OPTIONS_GHC -Wunused-imports #-}
  {-# OPTIONS_GHC -Wunused-matches #-}
  {-# OPTIONS_GHC -Wunused-binds #-}
  
  module Agda.Syntax.Concrete.Definitions.Monad where
  
  import Prelude hiding ( null )
  
  import Control.Monad        ( )
  import Control.Monad.Except ( MonadError(..), ExceptT, runExceptT )
  import Control.Monad.Reader ( MonadReader, ReaderT, runReaderT )
  import Control.Monad.State  ( MonadState(..), modify, State, StateT, runState )
  
  import Data.Bifunctor (second)
  import Data.Map (Map)
  import qualified Data.Map as Map
  import Data.Maybe (catMaybes)
  
  import Agda.Syntax.Position
  import Agda.Syntax.Common hiding (TerminationCheck())
  import Agda.Syntax.Concrete ( WhereClause_ )
  import Agda.Syntax.Concrete.Name
  import Agda.Syntax.Concrete.Definitions.Types
  import Agda.Syntax.Concrete.Definitions.Errors
  
  import Agda.Utils.CallStack ( CallStack, HasCallStack, withCallerCallStack )
  import Agda.Utils.Lens
  import qualified Agda.Utils.List1 as List1
  import Agda.Utils.Null (Null(..))
  
  import Agda.Utils.Impossible
  
  -- | Nicifier monad.
  --   Preserve the state when throwing an exception.
  
  newtype Nice a = Nice { unNice :: ReaderT NiceEnv (ExceptT DeclarationException (State NiceState)) a }
    deriving ( Functor, Applicative, Monad
             , MonadReader NiceEnv, MonadState NiceState, MonadError DeclarationException
             )
  
  -- | Extension of the nicifier monad with state to process interleaved mutual blocks.
  type INice = StateT InterleavedState Nice
  
  -- | Run a Nicifier computation, return result and warnings
  --   (in chronological order).
  runNice :: NiceEnv -> Nice a -> (Either DeclarationException a, NiceWarnings)
  runNice env m = second (reverse . niceWarn) $
    runExceptT (unNice m `runReaderT` env) `runState` initNiceState
  
  instance Null a => Null (Nice a) where
    empty = pure empty
    null _ = __IMPOSSIBLE__
  
  -- | Nicifier parameters.
  
  data NiceEnv = NiceEnv
    { safeButNotBuiltin :: Bool
         -- ^ We are in a module declared @--safe@ which is not a builtin module.
    , checkingWhere     :: WhereClause_
         -- ^ Are we checking a @where@ module?
    }
  
  -- | Nicifier state.
  
  data NiceState = NiceState
    { _loneSigs :: LoneSigs
      -- ^ Lone type signatures that wait for their definition.
    , _termChk  :: TerminationCheck
      -- ^ Termination checking pragma waiting for a definition.
    , _posChk   :: PositivityCheck
      -- ^ Positivity checking pragma waiting for a definition.
    , _uniChk   :: UniverseCheck
      -- ^ Universe checking pragma waiting for a data/rec signature or definition.
    , _catchall :: Catchall
      -- ^ Catchall pragma waiting for a function clause.
    , _covChk  :: CoverageCheck
      -- ^ Coverage pragma waiting for a definition.
    , niceWarn :: NiceWarnings
      -- ^ Stack of warnings. Head is last warning.
    , _nameId  :: NameId
      -- ^ We distinguish different 'NoName's (anonymous definitions) by a unique 'NameId'.
    }
  
  data LoneSig = LoneSig
    { loneSigRange :: Range
    , loneSigName  :: Name
        -- ^ If 'isNoName', this name can have a different 'NameId'
        --   than the key of 'LoneSigs' pointing to it.
    , loneSigKind  :: DataRecOrFun
    }
    deriving Show
  
  type LoneSigs     = Map Name LoneSig
       -- ^ We retain the 'Name' also in the codomain since
       --   'Name' as a key is up to @Eq Name@ which ignores the range.
       --   However, without range names are not unique in case the
       --   user gives a second definition of the same name.
       --   This causes then problems in 'replaceSigs' which might
       --   replace the wrong signature.
       --
       --   Another reason is that we want to distinguish different
       --   occurrences of 'NoName' in a mutual block (issue #4157).
       --   The 'NoName' in the codomain will have a unique 'NameId'.
  
  type NiceWarnings = [DeclarationWarning]
       -- ^ Stack of warnings. Head is last warning.
  
  -- | Initial nicifier state.
  
  initNiceState :: NiceState
  initNiceState = NiceState
    { _loneSigs = Map.empty
    , _termChk  = TerminationCheck
    , _posChk   = YesPositivityCheck
    , _uniChk   = YesUniverseCheck
    , _catchall = empty
    , _covChk   = YesCoverageCheck
    , niceWarn  = []
    , _nameId   = NameId 1 noModuleNameHash
    }
  
  lensNameId :: Lens' NiceState NameId
  lensNameId f e = f (_nameId e) <&> \ i -> e { _nameId = i }
  
  nextNameId :: Nice NameId
  nextNameId = do
    i <- use lensNameId
    lensNameId %= succ
    return i
  
  -- * Handling the lone signatures, stored to infer mutual blocks.
  
  -- | Lens for field '_loneSigs'.
  
  loneSigs :: Lens' NiceState LoneSigs
  loneSigs f e = f (_loneSigs e) <&> \ s -> e { _loneSigs = s }
  
  -- | Adding a lone signature to the state.
  --   Return the name (which is made unique if 'isNoName').
  
  addLoneSig :: Range -> Name -> DataRecOrFun -> Nice Name
  addLoneSig r x k = do
    -- Andreas, 2020-05-19, issue #4157, make '_' unique.
    x' <- case x of
      Name{}     -> pure x
      NoName r _ -> NoName r <$> nextNameId
    loneSigs %== \ s -> do
      let (mr, s') = Map.insertLookupWithKey (\ _k new _old -> new) x (LoneSig r x' k) s
      case mr of
        Nothing -> return s'
        Just y  -> declarationException $
          if not $ isNoName x then DuplicateDefinition x (loneSigRange y) else DuplicateAnonDeclaration r (loneSigRange y)
    return x'
  
  -- | Remove a lone signature from the state.
  
  removeLoneSig :: Name -> Nice ()
  removeLoneSig x = loneSigs %= Map.delete x
  
  -- | Search for forward type signature.
  
  getSig :: Name -> Nice (Maybe DataRecOrFun)
  getSig x = fmap loneSigKind . Map.lookup x <$> use loneSigs
  
  -- | Check that no lone signatures are left in the state.
  
  noLoneSigs :: Nice Bool
  noLoneSigs = null <$> use loneSigs
  
  forgetLoneSigs :: Nice ()
  forgetLoneSigs = loneSigs .= Map.empty
  
  -- | Ensure that all forward declarations have been given a definition.
  checkLoneSigs :: LoneSigs -> Nice ()
  checkLoneSigs xs = do
    forgetLoneSigs
    List1.unlessNull (Map.elems xs) \ ss -> declarationWarning $ MissingDefinitions $
      fmap (\s -> (loneSigName s , loneSigRange s)) ss
  
  -- | Ensure that all forward declarations have been given a definition,
  -- raising an error indicating *why* they would have had to have been
  -- defined.
  breakImplicitMutualBlock :: KwRange -> String -> Nice ()
  breakImplicitMutualBlock r why = do
    m <- use loneSigs
    List1.unlessNull (Map.elems m) $ \ xs ->
      declarationException $ DisallowedInterleavedMutual r why $
        -- Andreas, 2023-09-07: We discard the 'loneSigRange's because the 'Name' already has a range.
        fmap loneSigName xs
  
  -- | Get names of lone function signatures, plus their unique names.
  
  loneFuns :: LoneSigs -> [(Name, Arg Name)]
  loneFuns ls = catMaybes $
     Map.toList ls <&> \case
      (x, LoneSig _ x' (FunName ai _ _)) -> Just (x, Arg ai x')
      _ -> Nothing
  
  -- | Create a 'LoneSigs' map from an association list.
  
  loneSigsFromLoneNames :: [(Range, Name, DataRecOrFun)] -> LoneSigs
  loneSigsFromLoneNames = Map.fromListWith __IMPOSSIBLE__ . map (\(r,x,k) -> (x, LoneSig r x k))
  
  -- | Lens for field '_termChk'.
  
  terminationCheckPragma :: Lens' NiceState TerminationCheck
  terminationCheckPragma f e = f (_termChk e) <&> \ s -> e { _termChk = s }
  
  withTerminationCheckPragma :: TerminationCheck -> Nice a -> Nice a
  withTerminationCheckPragma tc f = do
    tc_old <- use terminationCheckPragma
    terminationCheckPragma .= tc
    result <- f
    terminationCheckPragma .= tc_old
    return result
  
  coverageCheckPragma :: Lens' NiceState CoverageCheck
  coverageCheckPragma f e = f (_covChk e) <&> \ s -> e { _covChk = s }
  
  withCoverageCheckPragma :: CoverageCheck -> Nice a -> Nice a
  withCoverageCheckPragma tc f = do
    tc_old <- use coverageCheckPragma
    coverageCheckPragma .= tc
    result <- f
    coverageCheckPragma .= tc_old
    return result
  
  -- | Lens for field '_posChk'.
  
  positivityCheckPragma :: Lens' NiceState PositivityCheck
  positivityCheckPragma f e = f (_posChk e) <&> \ s -> e { _posChk = s }
  
  withPositivityCheckPragma :: PositivityCheck -> Nice a -> Nice a
  withPositivityCheckPragma pc f = do
    pc_old <- use positivityCheckPragma
    positivityCheckPragma .= pc
    result <- f
    positivityCheckPragma .= pc_old
    return result
  
  -- | Lens for field '_uniChk'.
  
  universeCheckPragma :: Lens' NiceState UniverseCheck
  universeCheckPragma f e = f (_uniChk e) <&> \ s -> e { _uniChk = s }
  
  withUniverseCheckPragma :: UniverseCheck -> Nice a -> Nice a
  withUniverseCheckPragma uc f = do
    uc_old <- use universeCheckPragma
    universeCheckPragma .= uc
    result <- f
    universeCheckPragma .= uc_old
    return result
  
  -- | Get universe check pragma from a data/rec signature.
  --   Defaults to 'YesUniverseCheck'.
  
  getUniverseCheckFromSig :: Name -> Nice UniverseCheck
  getUniverseCheckFromSig x = maybe YesUniverseCheck universeCheck <$> getSig x
  
  -- | Lens for field '_catchall'.
  
  catchallPragma :: Lens' NiceState Catchall
  catchallPragma f e = f (_catchall e) <&> \ s -> e { _catchall = s }
  
  -- | Get current catchall pragma, and reset it for the next clause.
  
  popCatchallPragma :: Nice Catchall
  popCatchallPragma = do
    ca <- use catchallPragma
    catchallPragma .= empty
    return ca
  
  withCatchallPragma :: Catchall -> Nice a -> Nice a
  withCatchallPragma ca f = do
    ca_old <- use catchallPragma
    catchallPragma .= ca
    result <- f
    catchallPragma .= ca_old
    return result
  
  -- | Add a new warning.
  niceWarning :: DeclarationWarning -> Nice ()
  niceWarning w = modify $ \ st -> st { niceWarn = w : niceWarn st }
  
  declarationException :: HasCallStack => DeclarationException' -> Nice a
  declarationException e = withCallerCallStack $ throwError . flip DeclarationException e
  
  declarationWarning' :: DeclarationWarning' -> CallStack -> Nice ()
  declarationWarning' w loc = niceWarning $ DeclarationWarning loc w
  
  declarationWarning :: HasCallStack => DeclarationWarning' -> Nice ()
  declarationWarning = withCallerCallStack . declarationWarning'
  