git.iko.soy/Idris-dev
on cd87fcd help sign in
Idris-dev/libs/base/System.idr
102 lines 3.2 kB history raw
1module System
3import public Data.So
5%include C "unistd.h"
6%default partial
7%access public export
9||| Retrieves a value from the environment if the given key is present,
10||| otherwise it returns Nothing.
11getEnv : String -> IO (Maybe String)
12getEnv key = do
13 str_ptr <- getEnv'
14 is_nil <- nullStr str_ptr
15 if is_nil
16 then pure Nothing
17 else pure (Just str_ptr)
18 where
19 getEnv' : IO String
20 getEnv' = foreign FFI_C "getenv" (String -> IO String) key
22||| Sets an environment variable with a given value.
23||| Returns true if the operation was successful.
24setEnv : String -> String -> IO Bool
25setEnv key value = do
26 ok <- foreign FFI_C "setenv" (String -> String -> Int -> IO Int) key value 1
27 pure (ok == 0)
29||| Unsets an environment variable.
30||| Returns true if the variable was able to be unset.
31unsetEnv : String -> IO Bool
32unsetEnv key = do
33 ok <- foreign FFI_C "unsetenv" (String -> IO Int) key
34 pure (ok == 0)
36getEnvironment : IO (List (String, String))
37getEnvironment = getAllPairs 0 []
38 where
39 getEnvPair : Int -> IO String
40 getEnvPair i = foreign FFI_C "getEnvPair" (Int -> IO String) i
42 splitEq : String -> (String, String)
43 splitEq str =
44 -- FIXME: There has to be a better way to split this up
45 let (k, v) = break (== '=') str in
46 let (_, v') = break (/= '=') v in
47 (k, v')
49 getAllPairs : Int -> List String -> IO (List (String, String))
50 getAllPairs n acc = do
51 envPair <- getEnvPair n
52 is_nil <- nullStr envPair
53 if is_nil
54 then pure $ reverse $ map splitEq acc
55 else getAllPairs (n + 1) (envPair :: acc)
57||| Programs can either terminate successfully, or end in a caught
58||| failure.
59data 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
70||| Quit with a particular exit code
71exit : Int -> IO a
72exit code = believe_me $ foreign FFI_C "exit" (Int -> IO ()) code
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.
79exitWith : (code : ExitCode) -> IO a
80exitWith ExitSuccess = exit 0
81exitWith (ExitFailure errNo) = exit errNo
83||| Exit the program indicating failure.
84exitFailure : IO a
85exitFailure = exitWith (ExitFailure 1)
87||| Exit the program after a successful run.
88exitSuccess : IO a
89exitSuccess = exitWith ExitSuccess
91||| Get the numbers of seconds since 1st January 1970, 00:00 UTC
92time : IO Integer
93time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))
94 pure t
96||| Specify interval to sleep for, must be in range [0, 1000000]
97usleep : (i : Int) -> { auto prf : So (i >= 0 && i <= 1000000) } -> IO ()
98usleep i = foreign FFI_C "usleep" (Int -> IO ()) i
100||| Execute a program and returns its exit status code.
101system : String -> IO Int
102system cmd = foreign FFI_C "system" (String -> IO Int) cmd