    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
                   | 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
    showList :: [AgdaError] -> ShowS
    $cshowList :: [AgdaError] -> ShowS
    show :: AgdaError -> String
    $cshow :: AgdaError -> String
    showsPrec :: Int -> AgdaError -> ShowS
    $cshowsPrec :: Int -> AgdaError -> ShowS
    Show, AgdaError -> AgdaError -> Bool
    (AgdaError -> AgdaError -> Bool)
    -> (AgdaError -> AgdaError -> Bool) -> Eq AgdaError
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: AgdaError -> AgdaError -> Bool
    $c/= :: AgdaError -> AgdaError -> Bool
    == :: AgdaError -> AgdaError -> Bool
    $c== :: 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
    enumFromThenTo :: AgdaError -> AgdaError -> AgdaError -> [AgdaError]
    $cenumFromThenTo :: AgdaError -> AgdaError -> AgdaError -> [AgdaError]
    enumFromTo :: AgdaError -> AgdaError -> [AgdaError]
    $cenumFromTo :: AgdaError -> AgdaError -> [AgdaError]
    enumFromThen :: AgdaError -> AgdaError -> [AgdaError]
    $cenumFromThen :: AgdaError -> AgdaError -> [AgdaError]
    enumFrom :: AgdaError -> [AgdaError]
    $cenumFrom :: AgdaError -> [AgdaError]
    fromEnum :: AgdaError -> Int
    $cfromEnum :: AgdaError -> Int
    toEnum :: Int -> AgdaError
    $ctoEnum :: Int -> AgdaError
    pred :: AgdaError -> AgdaError
    $cpred :: AgdaError -> AgdaError
    succ :: AgdaError -> AgdaError
    $csucc :: AgdaError -> AgdaError
    Enum, AgdaError
    AgdaError -> AgdaError -> Bounded AgdaError
    forall a. a -> a -> Bounded a
    maxBound :: AgdaError
    $cmaxBound :: AgdaError
    minBound :: AgdaError
    $cminBound :: 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
    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 ()
    exitAgdaWith :: AgdaError -> IO ()
    exitAgdaWith = ExitCode -> IO ()
    forall a. ExitCode -> IO a
    exitWith (ExitCode -> IO ())
    -> (AgdaError -> ExitCode) -> AgdaError -> IO ()
    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