{-# LANGUAGE UndecidableInstances #-}

{- |
Module: Agda.Unused.Monad.Error

An error monad for determining unused code.
-}
module Agda.Unused.Monad.Error

  ( -- * Definitions
    
    Error(..)
  , InternalError(..)
  , UnexpectedError(..)
  , UnsupportedError(..)

    -- * Lift

  , liftLookup

  ) where

import Agda.Unused.Types.Context
  (LookupError(..))
import Agda.Unused.Types.Name
  (QName)

import Agda.Interaction.FindFile
  (FindError)
import Agda.Syntax.Concrete.Definitions
  (DeclarationException)
import Agda.Syntax.Concrete.Fixity
  (MonadFixityError(..))
import Agda.Syntax.Parser
  (ParseError)
import Agda.Syntax.Position
  (Range, getRange)
import Control.Monad.Except
  (MonadError, throwError)

-- ## Definitions

-- | An error encountered while checking for unused code.
data Error where

  -- | Ambiguous lookup.
  ErrorAmbiguous
    :: !Range
    -> !QName
    -> Error

  -- | Cyclic module dependency.
  ErrorCyclic
    :: !Range
    -> !QName
    -> Error

  -- | Agda declaration exception.
  ErrorDeclaration
    :: !DeclarationException
    -> Error

  -- | File not found.
  ErrorFile
    :: !FilePath
    -> Error

  -- | Agda find error.
  ErrorFind
    :: !Range
    -> !QName
    -> !FindError
    -> Error

  -- | Agda fixity exception.
  ErrorFixity
    :: !(Maybe Range)
    -> Error

  -- | Illegal declaration in main module of global check.
  ErrorGlobal
    :: !Range
    -> Error

  -- | Error in computing include paths.
  ErrorInclude
    :: Error

  -- | Internal error; should be reported.
  ErrorInternal
    :: !InternalError
    -> Error

  -- | Module not found in open statement.
  ErrorOpen
    :: !Range
    -> !QName
    -> Error

  -- | Agda parse error.
  ErrorParse
    :: !ParseError
    -> Error
  
  -- | Agda polarity error.
  ErrorPolarity
    :: !(Maybe Range)
    -> Error

  -- | Root not found.
  ErrorRoot
    :: !QName
    -> !QName
    -> Error

  -- | Unsupported language feature.
  ErrorUnsupported
    :: !UnsupportedError
    -> !Range
    -> Error

-- | An internal error, indicating a bug in our code. This type of error should
-- be reported by filing an issue.
data InternalError where

  -- | Unexpected declaration type for constructor.
  ErrorConstructor
    :: !Range
    -> InternalError

  -- | Unexpected arguments to SectionApp constructor.
  ErrorMacro
    :: !Range
    -> InternalError

  -- | Unexpected empty top level module name.
  ErrorModuleName
    :: !FilePath
    -> InternalError

  -- | Unexpected underscore as name.
  ErrorName
    :: !Range
    -> InternalError

  -- | Unexpected name-module mismatch in renaming statement.
  ErrorRenaming
    :: !Range
    -> InternalError

  -- | Unexpected data type constructor.
  ErrorUnexpected
    :: !UnexpectedError
    -> !Range
    -> InternalError

  deriving Int -> InternalError -> ShowS
[InternalError] -> ShowS
InternalError -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [InternalError] -> ShowS
$cshowList :: [InternalError] -> ShowS
show :: InternalError -> String
$cshow :: InternalError -> String
showsPrec :: Int -> InternalError -> ShowS
$cshowsPrec :: Int -> InternalError -> ShowS
Show

-- | An error indicating that a constructor for a data type is used where it
-- should not be used.
data UnexpectedError where

  UnexpectedAbsurd
    :: UnexpectedError

  UnexpectedAs
    :: UnexpectedError

  UnexpectedDontCare
    :: UnexpectedError

  UnexpectedETel
    :: UnexpectedError

  UnexpectedEllipsis
    :: UnexpectedError

  UnexpectedEqual
    :: UnexpectedError

  UnexpectedField
    :: UnexpectedError

  UnexpectedNiceFunClause
    :: UnexpectedError

  UnexpectedOpApp
    :: UnexpectedError

  UnexpectedOpAppP
    :: UnexpectedError

  deriving Int -> UnexpectedError -> ShowS
[UnexpectedError] -> ShowS
UnexpectedError -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UnexpectedError] -> ShowS
$cshowList :: [UnexpectedError] -> ShowS
show :: UnexpectedError -> String
$cshow :: UnexpectedError -> String
showsPrec :: Int -> UnexpectedError -> ShowS
$cshowsPrec :: Int -> UnexpectedError -> ShowS
Show

-- | An error indicating that an unsupported language was found.
data UnsupportedError where

  -- | Lone constructors.
  UnsupportedLoneConstructor
    :: UnsupportedError

  -- | Record module instance applications.
  UnsupportedMacro
    :: UnsupportedError

  -- | Unquoting primitives.
  UnsupportedUnquote
    :: UnsupportedError

  deriving Int -> UnsupportedError -> ShowS
[UnsupportedError] -> ShowS
UnsupportedError -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UnsupportedError] -> ShowS
$cshowList :: [UnsupportedError] -> ShowS
show :: UnsupportedError -> String
$cshow :: UnsupportedError -> String
showsPrec :: Int -> UnsupportedError -> ShowS
$cshowsPrec :: Int -> UnsupportedError -> ShowS
Show

-- ## Fixity

instance (Monad m, MonadError Error m) => MonadFixityError m where
  throwMultipleFixityDecls :: forall a. [(Name, [Fixity'])] -> m a
throwMultipleFixityDecls []
    = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Maybe Range -> Error
ErrorFixity forall a. Maybe a
Nothing)
  throwMultipleFixityDecls ((Name
n, [Fixity']
_) : [(Name, [Fixity'])]
_)
    = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Maybe Range -> Error
ErrorFixity (forall a. a -> Maybe a
Just (forall a. HasRange a => a -> Range
getRange Name
n)))
  throwMultiplePolarityPragmas :: forall a. [Name] -> m a
throwMultiplePolarityPragmas []
    = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Maybe Range -> Error
ErrorPolarity forall a. Maybe a
Nothing)
  throwMultiplePolarityPragmas (Name
n : [Name]
_)
    = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Maybe Range -> Error
ErrorPolarity (forall a. a -> Maybe a
Just (forall a. HasRange a => a -> Range
getRange Name
n)))
  warnUnknownNamesInFixityDecl :: HasCallStack => [Name] -> m ()
warnUnknownNamesInFixityDecl [Name]
_
    = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  warnUnknownNamesInPolarityPragmas :: HasCallStack => [Name] -> m ()
warnUnknownNamesInPolarityPragmas [Name]
_
    = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  warnUnknownFixityInMixfixDecl :: HasCallStack => [Name] -> m ()
warnUnknownFixityInMixfixDecl [Name]
_
    = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  warnPolarityPragmasButNotPostulates :: HasCallStack => [Name] -> m ()
warnPolarityPragmasButNotPostulates [Name]
_
    = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- ## Lift

-- | Lift a lookup result to our error monad.
liftLookup
  :: MonadError Error m
  => Range
  -> QName
  -> Either LookupError a
  -> m a
liftLookup :: forall (m :: * -> *) a.
MonadError Error m =>
Range -> QName -> Either LookupError a -> m a
liftLookup Range
r QName
n (Left LookupError
LookupNotFound)
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Range -> QName -> Error
ErrorOpen Range
r QName
n)
liftLookup Range
r QName
n (Left LookupError
LookupAmbiguous)
  = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Range -> QName -> Error
ErrorAmbiguous Range
r QName
n)
liftLookup Range
_ QName
_ (Right a
x)
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x