@@ -1,5 +1,7 @@
11module System
22
3+import Data.So
4+
35%include C "unistd.h"
46%default partial
57%access public export
@@ -52,11 +54,41 @@ getEnvironment = getAllPairs 0 []
5254 then pure $ reverse $ map splitEq acc
5355 else getAllPairs (n + 1) (envPair :: acc)
5456
57+||| Programs can either terminate successfully, or end in a caught
58+||| failure.
59+data ExitCode : Type where
60+ ||| Terminate successfully.
61+ ExitSuccess : ExitCode
62+ ||| Program terminated for some prescribed reason.
63+ |||
64+ ||| @errNo A non-zero numerical value indicating failure.
65+ ||| @prf Proof that the int value is non-zero.
66+ ExitFailure : (errNo : Int)
67+ -> {auto prf : So (not $ errNo == 0)}
68+ -> ExitCode
69+
5570||| Quit with a particular exit code
56−exit : Int -> IO ()
57−exit code = foreign FFI_C "exit" (Int -> IO ()) code
71+exit : Int -> IO a
72+exit code = believe_me $ foreign FFI_C "exit" (Int -> IO ()) code
73+
74+||| Terminate the program with an `ExitCode`. This code indicates the
75+||| success of the program's execution, and returns the success code
76+||| to the program's caller.
77+|||
78+||| @code The `ExitCode` for program.
79+exitWith : (code : ExitCode) -> IO a
80+exitWith ExitSuccess = exit 0
81+exitWith (ExitFailure errNo) = exit errNo
5882
59−||| Get the numbers of seconds since 1st January 1970, 00:00 UTC
83+||| Exit the program indicating failure.
84+exitFailure : IO a
85+exitFailure = exitWith (ExitFailure 1)
86+
87+||| Exit the program after a successful run.
88+exitSuccess : IO a
89+exitSuccess = exitWith ExitSuccess
90+
91+||| Get the numbers of seconds since 1st January 1970, 00:00 UTC
6092time : IO Integer
6193time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))
6294 pure t
@@ -66,4 +98,3 @@ usleep i = foreign FFI_C "usleep" (Int -> IO ()) i
6698
6799system : String -> IO Int
68100system cmd = foreign FFI_C "system" (String -> IO Int) cmd
69−