[ new ] bindings for Haskell's System.Exit (#1367)

Author: gallais

CHANGELOG.md

@@ -213,6 +213,12 @@ New modules
   System.Environment.Primitive
   ```
 
+* Added bindings for Haskell's `System.Exit`:
+  ```
+  System.Exit
+  System.Exit.Primitive
+  ```
+
 * New morphisms
   ```
   Algebra.Morphism.LatticeMonomorphism

GenerateEverything.hs

@@ -43,6 +43,8 @@ unsafeModules = map modToFile
   , "Relation.Binary.PropositionalEquality.TrustMe"
   , "System.Environment"
   , "System.Environment.Primitive"
+  , "System.Exit"
+  , "System.Exit.Primitive"
   , "Text.Pretty.Core"
   , "Text.Pretty"
   ]

src/System/Exit.agda

@@ -0,0 +1,47 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Exiting the program.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K #-}
+
+module System.Exit where
+
+open import Level using (Level)
+open import Data.Nat.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
+  using ( ExitCode
+        ; ExitSuccess
+        ; ExitFailure
+        )
+  public
+
+------------------------------------------------------------------------
+-- 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 1)
+
+exitSuccess : IO A
+exitSuccess = exitWith ExitSuccess
+
+die : String → IO A
+die str = do
+  putStrLn str
+  exitFailure

src/System/Exit/Primitive.agda

@@ -0,0 +1,32 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Primitive System.Exit simple bindings to Haskell functions
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K #-}
+
+module System.Exit.Primitive where
+
+open import Data.Nat.Base using (ℕ)
+open import IO.Primitive using (IO)
+
+data ExitCode : Set where
+  ExitSuccess : ExitCode
+  ExitFailure : ℕ → ExitCode
+
+{-# FOREIGN GHC data AgdaExitCode = AgdaExitSuccess | AgdaExitFailure Integer #-}
+{-# COMPILE GHC ExitCode = data AgdaExitCode (AgdaExitSuccess | AgdaExitFailure) #-}
+
+{-# FOREIGN GHC import qualified System.Exit as SE #-}
+
+{-# FOREIGN GHC
+toExitCode :: AgdaExitCode -> SE.ExitCode
+toExitCode AgdaExitSuccess = SE.ExitSuccess
+toExitCode (AgdaExitFailure n) = SE.ExitFailure (fromIntegral n)
+#-}
+
+postulate
+  exitWith : ∀ {a} {A : Set a} → ExitCode → IO A
+
+{-# COMPILE GHC exitWith = \ _ _ -> SE.exitWith . toExitCode #-}