module Mikan.TypeChecking.Monad.Diagnostic
  ( -- * The 'Diagnostic' class
    DiagnosticReason(..)
  , Diagnostic(..)

  -- * Wrappers for ferrying diagnostic values
  -- $diagBoxes
  , SomeDiagnostic, EncodedDiagnostic(..)
  , internalErrorDiagnostic

  -- * Monads which can throw and catch diagnostics
  , MonadTCError
  , typeError, typeError', locatedTypeError
  , typeError_, typeError'_
  , syntaxError, internalError
  )
  where

import Control.Monad.Error.Class
import Control.DeepSeq

import Data.Typeable

import GHC.Generics

import Mikan.Interaction.Options.Warnings

import Mikan.Syntax.Concrete.Definitions.Errors qualified as N
import Mikan.Syntax.Position

import {-# SOURCE #-} Mikan.TypeChecking.Errors.Names (typeErrorString)
import {-# SOURCE #-} Mikan.TypeChecking.Errors () -- instance PrettyTCM TypeError
import {-# SOURCE #-} Mikan.TypeChecking.Pretty
import Mikan.TypeChecking.Monad.Base

import Mikan.Utils.CallStack

-- | The reason for raising a diagnostic.
data DiagnosticReason
  = DiagError -- ^ The diagnostic is always an error.

  | DiagWarning { DiagnosticReason -> WarningName
_warningName :: !WarningName }
  -- ^ The diagnostic is a warning with the given name.
  --
  -- This 'DiagnosticReason' should also be used for the "error
  -- warnings" which are controlled by an unsafe pragma option (like
  -- @TerminationError@, which can be turned off by
  -- @--no-termination-check@) /even if/ the diagnostic can not be
  -- turned off by a @-W@ flag.
  deriving (Int -> DiagnosticReason -> ShowS
[DiagnosticReason] -> ShowS
DiagnosticReason -> String
(Int -> DiagnosticReason -> ShowS)
-> (DiagnosticReason -> String)
-> ([DiagnosticReason] -> ShowS)
-> Show DiagnosticReason
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DiagnosticReason -> ShowS
showsPrec :: Int -> DiagnosticReason -> ShowS
$cshow :: DiagnosticReason -> String
show :: DiagnosticReason -> String
$cshowList :: [DiagnosticReason] -> ShowS
showList :: [DiagnosticReason] -> ShowS
Show, (forall x. DiagnosticReason -> Rep DiagnosticReason x)
-> (forall x. Rep DiagnosticReason x -> DiagnosticReason)
-> Generic DiagnosticReason
forall x. Rep DiagnosticReason x -> DiagnosticReason
forall x. DiagnosticReason -> Rep DiagnosticReason x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DiagnosticReason -> Rep DiagnosticReason x
from :: forall x. DiagnosticReason -> Rep DiagnosticReason x
$cto :: forall x. Rep DiagnosticReason x -> DiagnosticReason
to :: forall x. Rep DiagnosticReason x -> DiagnosticReason
Generic)

instance NFData DiagnosticReason

-- | A 'Diagnostic' is a value that can be thrown to abort elaboration
-- (see 'typeError' and variants), or logged to the set of warnings (see
-- 'Mikan.TypeChecking.Warning.warning' and variants).
--
-- New instances of 'Diagnostic' (new type errors, new warnings) should
-- be added in a support module adjacent to the component that raises
-- them. For example, errors related to execution of metaprograms
-- (implemented in "Mikan.TypeChecking.Unquote") are defined in the
-- module "Mikan.TypeChecking.Unquote.Errors".
class (NFData a, Show a, PrettyTCM a, Typeable a) => Diagnostic a where
  -- | The reason, or "intrinsic severity", of a diagnostic.
  --
  -- This is the base for computing the actual severity of the
  -- diagnostic after flags are applied.
  diagnosticReason :: a -> DiagnosticReason

  -- | Return a string that identifies the diagnostic. It is generally,
  -- but not necessarily, the name of the constructor for that value as
  -- a string. These strings are shown to the user in brackets after the
  -- diagnostic's severity.
  --
  -- TODO: This should be replaced with something that statically
  -- guarantees a unique numeric identifier for each diagnostic
  -- constructor.
  diagnosticString :: a -> String

  -- | Wrap the 'Diagnostic' into a 'SomeDiagnostic'.
  --
  -- __NOTE__: This method should not be implemented manually. It only
  -- exists to avoid repeated boxing of 'SomeDiagnostic's.
  toSomeDiagnostic :: a -> SomeDiagnostic
  toSomeDiagnostic = a -> SomeDiagnostic
forall a. Diagnostic a => a -> SomeDiagnostic
SomeDiagnostic

  -- | Attempt to recover the 'Diagnostic' from a 'SomeDiagnostic'.
  --
  -- __NOTE__: This method should not be implemented manually. It only
  -- exists to avoid repeated boxing of 'SomeDiagnostic's.
  fromSomeDiagnostic :: SomeDiagnostic -> Maybe a
  fromSomeDiagnostic (SomeDiagnostic a
err) = a -> Maybe a
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast a
err

-- | The constraints needed for 'typeError' and similar.
type MonadTCError m = (MonadTCEnv m, ReadTCState m, MonadError TCErr m)

{-# SPECIALIZE typeError :: Diagnostic e => HasCallStack => e -> TCM a #-}
-- | Throw a 'Diagnostic' in a 'MonadTCError', associating the error
-- with the source position from 'HasCallStack'.
typeError :: (HasCallStack, MonadTCError m, Diagnostic e) => e -> m a
typeError :: forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError e
err = (CallStack -> m a) -> m a
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack ((CallStack -> m a) -> m a) -> (CallStack -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \CallStack
loc -> TCErr -> m a
forall a. TCErr -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCErr -> m a) -> m TCErr -> m a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< CallStack -> e -> m TCErr
forall (m :: * -> *) e.
(MonadTCEnv m, ReadTCState m, Diagnostic e) =>
CallStack -> e -> m TCErr
typeError'_ CallStack
loc e
err

-- | Utility function for 1-arg constructed 'Diagnostic's.
-- Note that the @HasCallStack@ constraint is on the *resulting* function.
locatedTypeError :: (MonadTCError m, Diagnostic e) => (a -> e) -> (HasCallStack => a -> m b)
locatedTypeError :: forall (m :: * -> *) e a b.
(MonadTCError m, Diagnostic e) =>
(a -> e) -> HasCallStack => a -> m b
locatedTypeError a -> e
f a
e = (CallStack -> m b) -> m b
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack ((CallStack -> e -> m b) -> e -> CallStack -> m b
forall a b c. (a -> b -> c) -> b -> a -> c
flip CallStack -> e -> m b
forall (m :: * -> *) e a.
(MonadTCError m, Diagnostic e) =>
CallStack -> e -> m a
typeError' (a -> e
f a
e))

{-# SPECIALIZE typeError' :: CallStack -> TypeError -> TCM a #-}
-- | Throw a 'Diagnostic' in a 'MonadTCError' with an explicit 'CallStack'.
typeError' :: (MonadTCError m, Diagnostic e) => CallStack -> e -> m a
typeError' :: forall (m :: * -> *) e a.
(MonadTCError m, Diagnostic e) =>
CallStack -> e -> m a
typeError' CallStack
loc e
err = TCErr -> m a
forall a. TCErr -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCErr -> m a) -> m TCErr -> m a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< CallStack -> e -> m TCErr
forall (m :: * -> *) e.
(MonadTCEnv m, ReadTCState m, Diagnostic e) =>
CallStack -> e -> m TCErr
typeError'_ CallStack
loc e
err

{-# SPECIALIZE typeError'_ :: CallStack -> TypeError -> TCM TCErr #-}
-- | Construct a 'TCErr' value wrapping the given 'Diagnostic', associating it with the explicit 'CallStack'.
typeError'_ :: (MonadTCEnv m, ReadTCState m, Diagnostic e) => CallStack -> e -> m TCErr
typeError'_ :: forall (m :: * -> *) e.
(MonadTCEnv m, ReadTCState m, Diagnostic e) =>
CallStack -> e -> m TCErr
typeError'_ CallStack
loc e
err = CallStack -> TCState -> Closure SomeDiagnostic -> TCErr
TypeError CallStack
loc (TCState -> Closure SomeDiagnostic -> TCErr)
-> m TCState -> m (Closure SomeDiagnostic -> TCErr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m TCState
forall (m :: * -> *). ReadTCState m => m TCState
getTCState m (Closure SomeDiagnostic -> TCErr)
-> m (Closure SomeDiagnostic) -> m TCErr
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SomeDiagnostic -> m (Closure SomeDiagnostic)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure (e -> SomeDiagnostic
forall a. Diagnostic a => a -> SomeDiagnostic
toSomeDiagnostic e
err)

{-# SPECIALIZE typeError_ :: HasCallStack => TypeError -> TCM TCErr #-}
-- | Construct a 'TCErr' value wrapping the given 'Diagnostic',
-- associating it with the source position from 'HasCallStack'.
typeError_ :: (HasCallStack, MonadTCEnv m, ReadTCState m, Diagnostic e) => e -> m TCErr
typeError_ :: forall (m :: * -> *) e.
(HasCallStack, MonadTCEnv m, ReadTCState m, Diagnostic e) =>
e -> m TCErr
typeError_ = (CallStack -> m TCErr) -> m TCErr
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack ((CallStack -> m TCErr) -> m TCErr)
-> (e -> CallStack -> m TCErr) -> e -> m TCErr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CallStack -> e -> m TCErr) -> e -> CallStack -> m TCErr
forall a b c. (a -> b -> c) -> b -> a -> c
flip CallStack -> e -> m TCErr
forall (m :: * -> *) e.
(MonadTCEnv m, ReadTCState m, Diagnostic e) =>
CallStack -> e -> m TCErr
typeError'_

-- | Raise an internal error (used for the @'MonadFail' 'TCM'@ instance).
internalError :: (HasCallStack, MonadTCError m) => String -> m a
internalError :: forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
String -> m a
internalError = (String -> TypeError) -> HasCallStack => String -> m a
forall (m :: * -> *) e a b.
(MonadTCError m, Diagnostic e) =>
(a -> e) -> HasCallStack => a -> m b
locatedTypeError String -> TypeError
InternalError

-- | Raise a 'SyntaxError'.
syntaxError :: (HasCallStack, MonadTCError m) => String -> m a
syntaxError :: forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
String -> m a
syntaxError = (String -> TypeError) -> HasCallStack => String -> m a
forall (m :: * -> *) e a b.
(MonadTCError m, Diagnostic e) =>
(a -> e) -> HasCallStack => a -> m b
locatedTypeError String -> TypeError
SyntaxError

-- TODO: All of these instances complicate the module cycle quite a bit,
-- but they're difficult to immediately move to a different module
-- because of the PrettyTCM constraint on Diagnostic.
instance Diagnostic TypeError where
  diagnosticReason :: TypeError -> DiagnosticReason
diagnosticReason TypeError
_ = DiagnosticReason
DiagError
  diagnosticString :: TypeError -> String
diagnosticString = TypeError -> String
typeErrorString

instance PrettyTCM N.DeclarationException' where
  prettyTCM :: forall (m :: * -> *).
MonadPretty m =>
DeclarationException' -> m Doc
prettyTCM = DeclarationException' -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty

instance Diagnostic N.DeclarationException' where
  diagnosticReason :: DeclarationException' -> DiagnosticReason
diagnosticReason DeclarationException'
_ = DiagnosticReason
DiagError
  diagnosticString :: DeclarationException' -> String
diagnosticString = \case
    N.MultipleEllipses              {} -> String
"Syntax.MultipleEllipses"
    N.DuplicateDefinition           {} -> String
"Syntax.DuplicateDefinition"
    N.DuplicateAnonDeclaration      {} -> String
"Syntax.DuplicateAnonDeclaration"
    N.MissingWithClauses            {} -> String
"Syntax.MissingWithClauses"
    N.WrongDefinition               {} -> String
"Syntax.WrongDefinition"
    N.WrongContentBlock             {} -> String
"Syntax.WrongContentBlock"
    N.AmbiguousFunClauses           {} -> String
"Syntax.AmbiguousFunClauses"
    N.AmbiguousConstructor          {} -> String
"Syntax.AmbiguousConstructor"
    N.InvalidTerminationCheckMutual {} -> String
"Syntax.InvalidTerminationCheckMutual"
    N.UnquoteDefRequiresSignature   {} -> String
"Syntax.UnquoteDefRequiresSignature"
    N.BadMacroDef                   {} -> String
"Syntax.BadMacroDef"
    N.UnfoldingOutsideOpaque        {} -> String
"Syntax.UnfoldingOutsideOpaque"
    N.OpaqueInMutual                {} -> String
"Syntax.OpaqueInMutual"
    N.DisallowedInterleavedMutual   {} -> String
"Syntax.DisallowedInterleavedMutual"

-- $diagBoxes
--
-- The 'TCM' needs to store 'Diagnostic' values in two forms: for
-- control flow, in 'TCErr'; and for warning reporting, in 'TCWarning'.
-- 'TCErr's only exist during execution, and are sometimes matched on,
-- while non-fatal 'TCWarning's can persist into interface files.
-- These two needs are served by the wrapper types 'SomeDiagnostic' and
-- 'EncodedDiagnostic' respectively.

-- | A package precisely wrapping a 'Diagnostic' value.
--
-- The 'Diagnostic' methods 'toSomeDiagnostic' and 'fromSomeDiagnostic'
-- can be used to up- and down-cast between 'SomeDiagnostic' and a
-- concrete 'Diagnostic' type.
data SomeDiagnostic = forall a. Diagnostic a => SomeDiagnostic !a

instance Show SomeDiagnostic where
  show :: SomeDiagnostic -> String
show (SomeDiagnostic a
err) = a -> String
forall a. Show a => a -> String
show a
err

instance NFData SomeDiagnostic where
  rnf :: SomeDiagnostic -> ()
rnf (SomeDiagnostic a
err) = a -> ()
forall a. NFData a => a -> ()
rnf a
err

instance PrettyTCM SomeDiagnostic where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => SomeDiagnostic -> m Doc
prettyTCM (SomeDiagnostic a
err) = a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
err

instance Diagnostic SomeDiagnostic where
  diagnosticReason :: SomeDiagnostic -> DiagnosticReason
diagnosticReason (SomeDiagnostic a
r) = a -> DiagnosticReason
forall a. Diagnostic a => a -> DiagnosticReason
diagnosticReason a
r
  diagnosticString :: SomeDiagnostic -> String
diagnosticString (SomeDiagnostic a
r) = a -> String
forall a. Diagnostic a => a -> String
diagnosticString a
r

  -- avoid building a second box:
  toSomeDiagnostic :: SomeDiagnostic -> SomeDiagnostic
toSomeDiagnostic   = SomeDiagnostic -> SomeDiagnostic
forall a. a -> a
id
  fromSomeDiagnostic :: SomeDiagnostic -> Maybe SomeDiagnostic
fromSomeDiagnostic = SomeDiagnostic -> Maybe SomeDiagnostic
forall a. a -> Maybe a
Just

-- | The 'SomeDiagnostic' associated to an internal error.
--
-- __NOTE__: This is needed to break an import cycle:
-- "Mikan.Interaction.Monad.Base" needs a 'SomeDiagnostic' which can be
-- thrown for the @'MonadError' 'TCErr'@ instance for 'TCM', but it can
-- not import the 'Diagnostic' class since that depends on 'PrettyTCM'.
internalErrorDiagnostic :: String -> SomeDiagnostic
internalErrorDiagnostic :: String -> SomeDiagnostic
internalErrorDiagnostic = TypeError -> SomeDiagnostic
forall a. Diagnostic a => a -> SomeDiagnostic
SomeDiagnostic (TypeError -> SomeDiagnostic)
-> (String -> TypeError) -> String -> SomeDiagnostic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> TypeError
InternalError

-- | The serialised form of a 'Diagnostic', recording only the
-- identifying string and the intrinsic 'DiagnosticReason'.
--
-- Can not be downcast back to the 'Diagnostic' it was originally
-- encoded from.
data EncodedDiagnostic = EncodedDiagnostic
  { EncodedDiagnostic -> DiagnosticReason
_edReason :: !DiagnosticReason
  , EncodedDiagnostic -> String
_edString :: !String
  }
  deriving (Int -> EncodedDiagnostic -> ShowS
[EncodedDiagnostic] -> ShowS
EncodedDiagnostic -> String
(Int -> EncodedDiagnostic -> ShowS)
-> (EncodedDiagnostic -> String)
-> ([EncodedDiagnostic] -> ShowS)
-> Show EncodedDiagnostic
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> EncodedDiagnostic -> ShowS
showsPrec :: Int -> EncodedDiagnostic -> ShowS
$cshow :: EncodedDiagnostic -> String
show :: EncodedDiagnostic -> String
$cshowList :: [EncodedDiagnostic] -> ShowS
showList :: [EncodedDiagnostic] -> ShowS
Show, (forall x. EncodedDiagnostic -> Rep EncodedDiagnostic x)
-> (forall x. Rep EncodedDiagnostic x -> EncodedDiagnostic)
-> Generic EncodedDiagnostic
forall x. Rep EncodedDiagnostic x -> EncodedDiagnostic
forall x. EncodedDiagnostic -> Rep EncodedDiagnostic x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. EncodedDiagnostic -> Rep EncodedDiagnostic x
from :: forall x. EncodedDiagnostic -> Rep EncodedDiagnostic x
$cto :: forall x. Rep EncodedDiagnostic x -> EncodedDiagnostic
to :: forall x. Rep EncodedDiagnostic x -> EncodedDiagnostic
Generic)

instance NFData EncodedDiagnostic

instance PrettyTCM EncodedDiagnostic where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => EncodedDiagnostic -> m Doc
prettyTCM EncodedDiagnostic
_ = m Doc
"<encoded diagnostic>"

instance Diagnostic EncodedDiagnostic where
  diagnosticReason :: EncodedDiagnostic -> DiagnosticReason
diagnosticReason = EncodedDiagnostic -> DiagnosticReason
_edReason
  diagnosticString :: EncodedDiagnostic -> String
diagnosticString = EncodedDiagnostic -> String
_edString

  fromSomeDiagnostic :: SomeDiagnostic -> Maybe EncodedDiagnostic
fromSomeDiagnostic (SomeDiagnostic a
err) = EncodedDiagnostic -> Maybe EncodedDiagnostic
forall a. a -> Maybe a
Just (EncodedDiagnostic -> Maybe EncodedDiagnostic)
-> EncodedDiagnostic -> Maybe EncodedDiagnostic
forall a b. (a -> b) -> a -> b
$ EncodedDiagnostic
    { _edReason :: DiagnosticReason
_edReason = a -> DiagnosticReason
forall a. Diagnostic a => a -> DiagnosticReason
diagnosticReason a
err
    , _edString :: String
_edString = a -> String
forall a. Diagnostic a => a -> String
diagnosticString a
err
    }