-- | Facility to test throwing internal errors.

module Agda.ImpossibleTest where

import Agda.TypeChecking.Monad.Base   ( TCM, ReduceM, runReduceM )
import Agda.TypeChecking.Monad.Debug  ( MonadDebug, __IMPOSSIBLE_VERBOSE__ )
import Agda.TypeChecking.Reduce.Monad ()

import Agda.Utils.CallStack           ( HasCallStack )
import Agda.Utils.Impossible          ( __IMPOSSIBLE__ )

-- | If the given list of words is non-empty, print them as debug message
--   (using '__IMPOSSIBLE_VERBOSE__') before raising the internal error.
impossibleTest :: (MonadDebug m, HasCallStack) => [String] -> m a
impossibleTest :: [String] -> m a
impossibleTest = \case
  []   -> m a
forall a. HasCallStack => a
__IMPOSSIBLE__
  [String]
strs -> String -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String]
strs

impossibleTestReduceM :: (HasCallStack) => [String] -> TCM a
impossibleTestReduceM :: [String] -> TCM a
impossibleTestReduceM = ReduceM a -> TCM a
forall a. ReduceM a -> TCM a
runReduceM (ReduceM a -> TCM a)
-> ([String] -> ReduceM a) -> [String] -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
  []   -> ReduceM a
forall a. HasCallStack => a
__IMPOSSIBLE__
  [String]
strs -> String -> ReduceM a
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ (String -> ReduceM a) -> String -> ReduceM a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String]
strs