module Agda.Interaction.ExitCode (
  AgdaError(..),
  agdaErrorToInt,
  agdaErrorFromInt,
  exitSuccess,
  exitAgdaWith)
  where

import System.Exit (exitSuccess, exitWith, ExitCode(ExitFailure))

data AgdaError = UnknownError      -- ^ 1
               | TCMError          -- ^ 42
               | OptionError       -- ^ 71
               | CommandError      -- ^ 113
               | ImpossibleError   -- ^ 154
               deriving (Int -> AgdaError -> ShowS
[AgdaError] -> ShowS
AgdaError -> String
(Int -> AgdaError -> ShowS)
-> (AgdaError -> String)
-> ([AgdaError] -> ShowS)
-> Show AgdaError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AgdaError -> ShowS
showsPrec :: Int -> AgdaError -> ShowS
$cshow :: AgdaError -> String
show :: AgdaError -> String
$cshowList :: [AgdaError] -> ShowS
showList :: [AgdaError] -> ShowS
Show, AgdaError -> AgdaError -> Bool
(AgdaError -> AgdaError -> Bool)
-> (AgdaError -> AgdaError -> Bool) -> Eq AgdaError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AgdaError -> AgdaError -> Bool
== :: AgdaError -> AgdaError -> Bool
$c/= :: AgdaError -> AgdaError -> Bool
/= :: AgdaError -> AgdaError -> Bool
Eq, Int -> AgdaError
AgdaError -> Int
AgdaError -> [AgdaError]
AgdaError -> AgdaError
AgdaError -> AgdaError -> [AgdaError]
AgdaError -> AgdaError -> AgdaError -> [AgdaError]
(AgdaError -> AgdaError)
-> (AgdaError -> AgdaError)
-> (Int -> AgdaError)
-> (AgdaError -> Int)
-> (AgdaError -> [AgdaError])
-> (AgdaError -> AgdaError -> [AgdaError])
-> (AgdaError -> AgdaError -> [AgdaError])
-> (AgdaError -> AgdaError -> AgdaError -> [AgdaError])
-> Enum AgdaError
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: AgdaError -> AgdaError
succ :: AgdaError -> AgdaError
$cpred :: AgdaError -> AgdaError
pred :: AgdaError -> AgdaError
$ctoEnum :: Int -> AgdaError
toEnum :: Int -> AgdaError
$cfromEnum :: AgdaError -> Int
fromEnum :: AgdaError -> Int
$cenumFrom :: AgdaError -> [AgdaError]
enumFrom :: AgdaError -> [AgdaError]
$cenumFromThen :: AgdaError -> AgdaError -> [AgdaError]
enumFromThen :: AgdaError -> AgdaError -> [AgdaError]
$cenumFromTo :: AgdaError -> AgdaError -> [AgdaError]
enumFromTo :: AgdaError -> AgdaError -> [AgdaError]
$cenumFromThenTo :: AgdaError -> AgdaError -> AgdaError -> [AgdaError]
enumFromThenTo :: AgdaError -> AgdaError -> AgdaError -> [AgdaError]
Enum, AgdaError
AgdaError -> AgdaError -> Bounded AgdaError
forall a. a -> a -> Bounded a
$cminBound :: AgdaError
minBound :: AgdaError
$cmaxBound :: AgdaError
maxBound :: AgdaError
Bounded)

agdaErrorToInt :: AgdaError -> Int
agdaErrorToInt :: AgdaError -> Int
agdaErrorToInt AgdaError
UnknownError    = Int
1
agdaErrorToInt AgdaError
TCMError        = Int
42
agdaErrorToInt AgdaError
OptionError     = Int
71
agdaErrorToInt AgdaError
CommandError    = Int
113
agdaErrorToInt AgdaError
ImpossibleError = Int
154

-- ^ Return the error corresponding to an exit code from the
--   Agda process
agdaErrorFromInt :: Int -> Maybe AgdaError
agdaErrorFromInt :: Int -> Maybe AgdaError
agdaErrorFromInt = -- We implement this in a somewhat more inefficient
                   -- way for the sake of consistency
                   (Int -> [(Int, AgdaError)] -> Maybe AgdaError)
-> [(Int, AgdaError)] -> Int -> Maybe AgdaError
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> [(Int, AgdaError)] -> Maybe AgdaError
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [(AgdaError -> Int
agdaErrorToInt AgdaError
error, AgdaError
error)
                               | AgdaError
error  <- [AgdaError
forall a. Bounded a => a
minBound..AgdaError
forall a. Bounded a => a
maxBound]
                               ]

exitAgdaWith :: AgdaError -> IO a
exitAgdaWith :: forall a. AgdaError -> IO a
exitAgdaWith = ExitCode -> IO a
forall a. ExitCode -> IO a
exitWith (ExitCode -> IO a) -> (AgdaError -> ExitCode) -> AgdaError -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ExitCode
ExitFailure (Int -> ExitCode) -> (AgdaError -> Int) -> AgdaError -> ExitCode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AgdaError -> Int
agdaErrorToInt