git.iko.soy/Idris-dev
on master help sign in
Improve `System.Exit` Fixes #3488.
0ba2ce6Jan de Muijnck-Hughes
libs/base/Debug/Error.idr+1−2
compare with master
unifiedsplit
@@ -12,9 +12,8 @@ error : {default (%runElab sourceLocation) loc : SourceLocation} ->
12 (message : String) ->
12 (message : String) ->
13 a
13 a
14error {loc = FileLoc filename (line, col) _} message =
14error {loc = FileLoc filename (line, col) _} message =
15− believe_me . unsafePerformIO $
15+ unsafePerformIO $
16 do let place = filename ++ " line " ++ show line ++ " column " ++ show col
16 do let place = filename ++ " line " ++ show line ++ " column " ++ show col
17 let message' = place ++ ": " ++ message
17 let message' = place ++ ": " ++ message
18 putStrLn message'
18 putStrLn message'
19 exit 1
19 exit 1
20−
libs/base/System.idr+35−4
@@ -1,5 +1,7 @@
1module System
1module System
2
2
3+import Data.So
4+
3%include C "unistd.h"
5%include C "unistd.h"
4%default partial
6%default partial
5%access public export
7%access public export
@@ -52,11 +54,41 @@ getEnvironment = getAllPairs 0 []
52 then pure $ reverse $ map splitEq acc
54 then pure $ reverse $ map splitEq acc
53 else getAllPairs (n + 1) (envPair :: acc)
55 else getAllPairs (n + 1) (envPair :: acc)
54
56
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+
55||| Quit with a particular exit code
70||| Quit with a particular exit code
56−exit : Int -> IO ()
71+exit : Int -> IO a
57−exit code = foreign FFI_C "exit" (Int -> IO ()) code
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
58
82
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+
59−||| Get the numbers of seconds since 1st January 1970, 00:00 UTC
91+||| Get the numbers of seconds since 1st January 1970, 00:00 UTC
60time : IO Integer
92time : IO Integer
61time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))
93time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))
62 pure t
94 pure t
@@ -66,4 +98,3 @@ usleep i = foreign FFI_C "usleep" (Int -> IO ()) i
66
98
67system : String -> IO Int
99system : String -> IO Int
68system cmd = foreign FFI_C "system" (String -> IO Int) cmd
100system cmd = foreign FFI_C "system" (String -> IO Int) cmd
69−
libs/effects/Effect/Exception.idr+1−2
@@ -17,7 +17,7 @@ implementation Handler (Exception a) List where
17
17
18implementation Show a => Handler (Exception a) IO where
18implementation Show a => Handler (Exception a) IO where
19 handle _ (Raise e) k = do printLn e
19 handle _ (Raise e) k = do printLn e
20− believe_me (exit 1)
20+ (exit 1)
21
21
22implementation Handler (Exception a) (IOExcept a) where
22implementation Handler (Exception a) (IOExcept a) where
23 handle _ (Raise e) k = ioe_fail e
23 handle _ (Raise e) k = ioe_fail e
@@ -30,4 +30,3 @@ EXCEPTION t = MkEff () (Exception t)
30
30
31raise : a -> Eff b [EXCEPTION a]
31raise : a -> Eff b [EXCEPTION a]
32raise err = call $ Raise err
32raise err = call $ Raise err
33−