{-# LANGUAGE CPP #-}

{-# OPTIONS_GHC -Wunused-imports #-}

-- | An interface for reporting \"impossible\" errors.
module Mikan.Utils.Impossible
  ( Impossible(..)
  -- * Throwing impossible errors
  , impossible
  , __IMPOSSIBLE__
  , __IMPOSSIBLE__1
  , __UNREACHABLE__
  , throwImpossible
  -- * Catching impossible errors
  , CatchImpossible(..)
  )
  where

import Control.Exception (Exception(..), throw, catchJust)
import Control.DeepSeq

import Data.Text.Short (ShortText)
import Data.Text.Short qualified as TS

import Mikan.Utils.CallStack.Base
    ( CallStack
    , HasCallStack
    , prettyCallStack
    , withCallerCallStack
    , withNBackCallStack
    )

-- | \"Impossible\" errors, annotated with a file name and a line
-- number corresponding to the source code location of the error.
data Impossible
  = Impossible CallStack
    -- ^ We reached a program point which should be unreachable.
  | Unreachable CallStack
    -- ^ @Impossible@ with a different error message.
    --   Used when we reach a program point which can in principle
    --   be reached, but not for a certain run.
  | ImpMissingDefinitions [ShortText] ShortText
    -- ^ We reached a program point without all the required
    -- primitives or BUILTIN to proceed forward.
    -- @ImpMissingDefinitions neededDefs forThis@

-- Identify all values of Impossible. We use Impossible as a stand-in for the empty type, so all
-- values are morally equal.
instance Eq Impossible where
  Impossible
_ == :: Impossible -> Impossible -> Bool
== Impossible
_ = Bool
True

instance Ord Impossible where
  compare :: Impossible -> Impossible -> Ordering
compare Impossible
_ Impossible
_ = Ordering
EQ

instance NFData Impossible where
  rnf :: Impossible -> ()
rnf Impossible
_ = ()

instance Show Impossible where
  show :: Impossible -> String
show (Impossible CallStack
loc) = [String] -> String
unlines
    [ String
"An internal error has occurred. Please report this as a bug."
    , String
"Location of the error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CallStack -> String
prettyCallStack CallStack
loc
    ]
  show (Unreachable CallStack
loc) = [String] -> String
unlines
    [ String
"We reached a program point we did not want to reach."
    , String
"Location of the error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CallStack -> String
prettyCallStack CallStack
loc
    ]
  show (ImpMissingDefinitions [ShortText]
needed ShortText
forthis) = [String] -> String
unlines
    [ String
"The following builtins or primitives need to be bound to use " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShortText -> String
TS.unpack ShortText
forthis String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":"
    , [String] -> String
unwords (ShortText -> String
TS.unpack (ShortText -> String) -> [ShortText] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ShortText]
needed)
    ]

instance Exception Impossible where
#if MIN_VERSION_base(4,20,0)
  -- Andreas, 2024-07-05, issue #7299;
  -- Turn off the (here useless) backtrace introduced in GHC 9.10.
  -- Besides spamming us with useless info, it changes the golden
  -- value, introducing incompatibilities in the test-suite.
  backtraceDesired :: Impossible -> Bool
backtraceDesired Impossible
_ = Bool
False
#endif

-- | Abort by throwing an \"impossible\" error. You should not use
-- this function directly; use '__IMPOSSIBLE__' instead.
throwImpossible :: Impossible -> a
throwImpossible :: forall a. Impossible -> a
throwImpossible = Impossible -> a
forall a e. (HasCallStack, Exception e) => e -> a
throw

-- | Monads in which we can catch an \"impossible\" error, if possible.
class CatchImpossible m where

  -- | Catch any t'Impossible' exception.
  catchImpossible :: m a -> (Impossible -> m a) -> m a
  catchImpossible = (Impossible -> Maybe Impossible)
-> m a -> (Impossible -> m a) -> m a
forall b a. (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
forall (m :: * -> *) b a.
CatchImpossible m =>
(Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
catchImpossibleJust Impossible -> Maybe Impossible
forall a. a -> Maybe a
Just

  -- | Catch only t'Impossible' exceptions selected by the filter.
  catchImpossibleJust :: (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
  catchImpossibleJust = ((b -> m a) -> m a -> m a) -> m a -> (b -> m a) -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((b -> m a) -> m a -> m a) -> m a -> (b -> m a) -> m a)
-> ((Impossible -> Maybe b) -> (b -> m a) -> m a -> m a)
-> (Impossible -> Maybe b)
-> m a
-> (b -> m a)
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Impossible -> Maybe b) -> (b -> m a) -> m a -> m a
forall b a. (Impossible -> Maybe b) -> (b -> m a) -> m a -> m a
forall (m :: * -> *) b a.
CatchImpossible m =>
(Impossible -> Maybe b) -> (b -> m a) -> m a -> m a
handleImpossibleJust

  -- | Version of 'catchImpossible' with argument order suiting short handlers.
  handleImpossible :: (Impossible -> m a) -> m a -> m a
  handleImpossible = (m a -> (Impossible -> m a) -> m a)
-> (Impossible -> m a) -> m a -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip m a -> (Impossible -> m a) -> m a
forall a. m a -> (Impossible -> m a) -> m a
forall (m :: * -> *) a.
CatchImpossible m =>
m a -> (Impossible -> m a) -> m a
catchImpossible

  -- | Version of 'catchImpossibleJust' with argument order suiting short handlers.
  handleImpossibleJust :: (Impossible -> Maybe b) -> (b -> m a) -> m a -> m a
  handleImpossibleJust = (m a -> (b -> m a) -> m a) -> (b -> m a) -> m a -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((m a -> (b -> m a) -> m a) -> (b -> m a) -> m a -> m a)
-> ((Impossible -> Maybe b) -> m a -> (b -> m a) -> m a)
-> (Impossible -> Maybe b)
-> (b -> m a)
-> m a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
forall b a. (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
forall (m :: * -> *) b a.
CatchImpossible m =>
(Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
catchImpossibleJust

  {-# MINIMAL catchImpossibleJust | handleImpossibleJust #-}

instance CatchImpossible IO where
  catchImpossibleJust :: forall b a. (Impossible -> Maybe b) -> IO a -> (b -> IO a) -> IO a
catchImpossibleJust = (Impossible -> Maybe b) -> IO a -> (b -> IO a) -> IO a
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> (b -> IO a) -> IO a
catchJust

-- | Construct a value of v'Impossible' reporting the location where you call
--   this function.
impossible :: HasCallStack => Impossible
impossible :: HasCallStack => Impossible
impossible = (CallStack -> Impossible) -> Impossible
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Impossible
Impossible

-- | Throw an v'Impossible' error reporting the location where you
--   place '__IMPOSSIBLE__'.
__IMPOSSIBLE__ :: HasCallStack => a
__IMPOSSIBLE__ :: forall a. HasCallStack => a
__IMPOSSIBLE__ = Word -> (CallStack -> a) -> a
forall b. HasCallStack => Word -> (CallStack -> b) -> b
withNBackCallStack Word
0 ((CallStack -> a) -> a) -> (CallStack -> a) -> a
forall a b. (a -> b) -> a -> b
$ Impossible -> a
forall a. Impossible -> a
throwImpossible (Impossible -> a) -> (CallStack -> Impossible) -> CallStack -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> Impossible
Impossible

-- | Throw an v'Impossible' error reporting the /caller's/ call site.
__IMPOSSIBLE__1 :: HasCallStack => a
__IMPOSSIBLE__1 :: forall a. HasCallStack => a
__IMPOSSIBLE__1 = Word -> (CallStack -> a) -> a
forall b. HasCallStack => Word -> (CallStack -> b) -> b
withNBackCallStack Word
1 ((CallStack -> a) -> a) -> (CallStack -> a) -> a
forall a b. (a -> b) -> a -> b
$ Impossible -> a
forall a. Impossible -> a
throwImpossible (Impossible -> a) -> (CallStack -> Impossible) -> CallStack -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> Impossible
Impossible

-- | Throw an 'Unreachable' error reporting the /caller's/ call site.
__UNREACHABLE__ :: HasCallStack => a
__UNREACHABLE__ :: forall a. HasCallStack => a
__UNREACHABLE__ = (CallStack -> a) -> a
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack ((CallStack -> a) -> a) -> (CallStack -> a) -> a
forall a b. (a -> b) -> a -> b
$ Impossible -> a
forall a. Impossible -> a
throwImpossible (Impossible -> a) -> (CallStack -> Impossible) -> CallStack -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> Impossible
Unreachable