{-# LANGUAGE Safe #-}

-- | Custom functions to report error messages to users.
module Copilot.Theorem.Misc.Error
  ( badUse
  , impossible
  , impossible_
  , fatal
  ) where

-- | Tag used with error messages to help users locate the component that
-- failed or reports the error.
errorHeader :: String
errorHeader :: String
errorHeader = String
"[Copilot-kind ERROR]  "

-- | Report an error due to an error detected by Copilot (e.g., user error).
badUse :: String -- ^ Description of the error.
       -> a
badUse :: forall a. String -> a
badUse String
s = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
errorHeader String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s

-- | Report an error due to a bug in Copilot.
impossible :: String -- ^ Error information to attach to the message.
           -> a
impossible :: forall a. String -> a
impossible String
s = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
errorHeader String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Unexpected internal error : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s

-- | Report an error due to a bug in Copilot.
impossible_ :: a
impossible_ :: forall a. a
impossible_ = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
errorHeader String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Unexpected internal error"

-- | Report an unrecoverable error (e.g., incorrect format).
fatal :: String -> a
fatal :: forall a. String -> a
fatal = String -> a
forall a. HasCallStack => String -> a
error