mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-28 02:23:44 +03:00
130 lines
3.3 KiB
Idris
130 lines
3.3 KiB
Idris
module System
|
|
|
|
import public Data.So
|
|
import Data.List
|
|
import Data.Strings
|
|
|
|
support : String -> String
|
|
support fn = "C:" ++ fn ++ ", libidris2_support"
|
|
|
|
libc : String -> String
|
|
libc fn = "C:" ++ fn ++ ", libc 6"
|
|
|
|
%foreign support "idris2_sleep"
|
|
prim_sleep : Int -> PrimIO ()
|
|
%foreign support "idris2_usleep"
|
|
prim_usleep : Int -> PrimIO ()
|
|
|
|
export
|
|
sleep : Int -> IO ()
|
|
sleep sec = primIO (prim_sleep sec)
|
|
|
|
export
|
|
usleep : (x : Int) -> So (x >= 0) => IO ()
|
|
usleep sec = primIO (prim_usleep sec)
|
|
|
|
-- This one is going to vary for different back ends. Probably needs a
|
|
-- better convention. Will revisit...
|
|
%foreign "scheme:blodwen-args"
|
|
prim__getArgs : PrimIO (List String)
|
|
|
|
export
|
|
getArgs : IO (List String)
|
|
getArgs = primIO prim__getArgs
|
|
|
|
%foreign libc "getenv"
|
|
prim_getEnv : String -> PrimIO (Ptr String)
|
|
%foreign support "idris2_getEnvPair"
|
|
prim_getEnvPair : Int -> PrimIO (Ptr String)
|
|
%foreign support "idris2_setenv"
|
|
prim_setEnv : String -> String -> Int -> PrimIO Int
|
|
%foreign support "idris2_unsetenv"
|
|
prim_unsetEnv : String -> PrimIO Int
|
|
|
|
export
|
|
getEnv : String -> IO (Maybe String)
|
|
getEnv var
|
|
= do env <- primIO $ prim_getEnv var
|
|
if prim__nullPtr env /= 0
|
|
then pure Nothing
|
|
else pure (Just (prim__getString env))
|
|
|
|
export
|
|
getEnvironment : IO (List (String, String))
|
|
getEnvironment = getAllPairs 0 []
|
|
where
|
|
splitEq : String -> (String, String)
|
|
splitEq str
|
|
= let (k, v) = break (== '=') str
|
|
(_, v') = break (/= '=') v in
|
|
(k, v')
|
|
|
|
getAllPairs : Int -> List String -> IO (List (String, String))
|
|
getAllPairs n acc = do
|
|
envPair <- primIO $ prim_getEnvPair n
|
|
if prim__nullPtr envPair /= 0
|
|
then pure $ reverse $ map splitEq acc
|
|
else getAllPairs (n + 1) (prim__getString envPair :: acc)
|
|
|
|
export
|
|
setEnv : String -> String -> Bool -> IO Bool
|
|
setEnv var val overwrite
|
|
= do ok <- primIO $ prim_setEnv var val (if overwrite then 1 else 0)
|
|
if ok == 0
|
|
then pure True
|
|
else pure False
|
|
|
|
export
|
|
unsetEnv : String -> IO Bool
|
|
unsetEnv var
|
|
= do ok <- primIO $ prim_unsetEnv var
|
|
if ok == 0
|
|
then pure True
|
|
else pure False
|
|
|
|
%foreign libc "system"
|
|
"scheme:blodwen-system"
|
|
prim_system : String -> PrimIO Int
|
|
|
|
export
|
|
system : String -> IO Int
|
|
system cmd = primIO (prim_system cmd)
|
|
|
|
%foreign support "idris2_time"
|
|
"scheme:blodwen-time"
|
|
prim_time : PrimIO Int
|
|
|
|
export
|
|
time : IO Integer
|
|
time = pure $ cast !(primIO prim_time)
|
|
|
|
%foreign libc "exit"
|
|
prim_exit : Int -> PrimIO ()
|
|
|
|
||| Programs can either terminate successfully, or end in a caught
|
|
||| failure.
|
|
public export
|
|
data ExitCode : Type where
|
|
||| Terminate successfully.
|
|
ExitSuccess : ExitCode
|
|
||| Program terminated for some prescribed reason.
|
|
|||
|
|
||| @errNo A non-zero numerical value indicating failure.
|
|
||| @prf Proof that the int value is non-zero.
|
|
ExitFailure : (errNo : Int) -> (So (not $ errNo == 0)) => ExitCode
|
|
|
|
export
|
|
exitWith : ExitCode -> IO a
|
|
exitWith ExitSuccess = believe_me $ primIO $ prim_exit 0
|
|
exitWith (ExitFailure code) = believe_me $ primIO $ prim_exit code
|
|
|
|
||| Exit the program indicating failure.
|
|
export
|
|
exitFailure : IO a
|
|
exitFailure = exitWith (ExitFailure 1)
|
|
|
|
||| Exit the program after a successful run.
|
|
export
|
|
exitSuccess : IO a
|
|
exitSuccess = exitWith ExitSuccess
|