------------------------------------------------------------------------
-- | An interface for reporting \"impossible\" errors
------------------------------------------------------------------------


module Agda.Utils.Impossible where

import Control.Exception (Exception(..), throw, catchJust)
import GHC.Stack
  (CallStack, HasCallStack, callStack, getCallStack, freezeCallStack
  , srcLocModule, srcLocFile, srcLocStartLine)

-- | \"Impossible\" errors, annotated with a file name and a line
-- number corresponding to the source code location of the error.

data Impossible

  = Impossible  String Integer
    -- ^ We reached a program point which should be unreachable.

  | Unreachable String Integer
    -- ^ @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 [String] String
    -- ^ We reached a program point without all the required
    -- primitives or BUILTIN to proceed forward.
    -- @ImpMissingDefinitions neededDefs forThis@

instance Show Impossible where
  show :: Impossible -> String
show (Impossible String
file Integer
line) = [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]
++ String
file String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
line
    ]
  show (Unreachable String
file Integer
line) = [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]
++ String
file String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
line
    ]
  show (ImpMissingDefinitions [String]
needed String
forthis) = [String] -> String
unlines
    [ String
"The following builtins or primitives need to be bound to use " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
forthis String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":"]
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
needed

instance Exception Impossible

-- | Abort by throwing an \"impossible\" error. You should not use
-- this function directly. Instead use __IMPOSSIBLE__

throwImpossible :: Impossible -> a
throwImpossible :: Impossible -> a
throwImpossible = Impossible -> a
forall a e. Exception e => e -> a
throw

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

class CatchImpossible m where

  -- | Catch any 'Impossible' exception.
  catchImpossible :: m a -> (Impossible -> m a) -> m a
  catchImpossible = (Impossible -> Maybe Impossible)
-> m a -> (Impossible -> 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 '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 (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 (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 (m :: * -> *) b a.
CatchImpossible m =>
(Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
catchImpossibleJust

  {-# MINIMAL catchImpossibleJust | handleImpossibleJust #-}

instance CatchImpossible IO where
  catchImpossibleJust :: (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

-- | Create something with a callstack's file and line number

withFileAndLine' :: Integral a => CallStack -> (String -> a -> b) -> b
withFileAndLine' :: CallStack -> (String -> a -> b) -> b
withFileAndLine' CallStack
cs String -> a -> b
ctor = String -> a -> b
ctor String
file a
line
  where
    callSiteList :: [(String, SrcLoc)]
callSiteList = CallStack -> [(String, SrcLoc)]
getCallStack CallStack
cs
    notHere :: (a, SrcLoc) -> Bool
notHere (a
_, SrcLoc
loc) = SrcLoc -> String
srcLocModule SrcLoc
loc String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
"Agda.Utils.Impossible"
    stackLocations :: [(String, SrcLoc)]
stackLocations = ((String, SrcLoc) -> Bool)
-> [(String, SrcLoc)] -> [(String, SrcLoc)]
forall a. (a -> Bool) -> [a] -> [a]
filter (String, SrcLoc) -> Bool
forall a. (a, SrcLoc) -> Bool
notHere [(String, SrcLoc)]
callSiteList
    (String
file, a
line) = case [(String, SrcLoc)]
stackLocations of
      (String
_, SrcLoc
loc) : [(String, SrcLoc)]
_ -> (SrcLoc -> String
srcLocFile SrcLoc
loc, Int -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (SrcLoc -> Int
srcLocStartLine SrcLoc
loc))
      [] -> (String
"?", -a
1)

-- | Create something with the call site's file and line number

withFileAndLine :: (HasCallStack, Integral a) => (String -> a -> b) -> b
withFileAndLine :: (String -> a -> b) -> b
withFileAndLine = CallStack -> (String -> a -> b) -> b
forall a b. Integral a => CallStack -> (String -> a -> b) -> b
withFileAndLine' (CallStack -> CallStack
freezeCallStack CallStack
HasCallStack => CallStack
callStack)

-- | Throw an "Impossible" error reporting the *caller's* call site.

__IMPOSSIBLE__ :: HasCallStack => a
__IMPOSSIBLE__ :: a
__IMPOSSIBLE__ = Impossible -> a
forall a. Impossible -> a
throwImpossible ((String -> Integer -> Impossible) -> Impossible
forall a b. (HasCallStack, Integral a) => (String -> a -> b) -> b
withFileAndLine String -> Integer -> Impossible
Impossible)

-- | Throw an "Unreachable" error reporting the *caller's* call site.
-- Note that this call to "withFileAndLine" will be filtered out
-- due its filter on the srcLocModule.

__UNREACHABLE__ :: HasCallStack => a
__UNREACHABLE__ :: a
__UNREACHABLE__ = Impossible -> a
forall a. Impossible -> a
throwImpossible ((String -> Integer -> Impossible) -> Impossible
forall a b. (HasCallStack, Integral a) => (String -> a -> b) -> b
withFileAndLine String -> Integer -> Impossible
Unreachable)