------------------------------------------------------------------------
-- The Agda standard library
--
-- Exiting the program.
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --guardedness #-}

module System.Exit where

open import Level using (Level)
open import Data.Bool.Base using (Bool; true; false; not)
open import Data.Integer.Base using (ℤ; +_)
open import Data.String.Base using (String)
open import Function.Base using (_$_; _∘′_)
open import IO using (IO; lift; _>>_; putStrLn)

------------------------------------------------------------------------
-- Re-exporting the ExitCode data structure

open import System.Exit.Primitive as Prim
  public
  using ( ExitCode
        ; ExitSuccess
        ; ExitFailure
        )

------------------------------------------------------------------------
-- Tests

isSuccess : ExitCode → Bool
isSuccess ExitSuccess     = true
isSuccess (ExitFailure _) = false

isFailure : ExitCode → Bool
isFailure  = not ∘′ isSuccess

------------------------------------------------------------------------
-- Various exiting function

private
  variable
    a : Level
    A : Set a

exitWith : ExitCode → IO A
exitWith c = lift (Prim.exitWith c)

exitFailure : IO A
exitFailure = exitWith (ExitFailure (+ ))

exitSuccess : IO A
exitSuccess = exitWith ExitSuccess

die : String → IO A
die str = do
  putStrLn str
  exitFailure