module System import Data.Soimport Data.Listimport Data.Strings support : String -> Stringsupport fn = "C:" ++ fn ++ ", libidris2_support" libc : String -> Stringlibc fn = "C:" ++ fn ++ ", libc 6" %foreign support "idris2_sleep"prim_sleep : Int -> PrimIO ()%foreign support "idris2_usleep"prim_usleep : Int -> PrimIO () exportsleep : Int -> IO ()sleep sec = primIO (prim_sleep sec) exportusleep : (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) exportgetArgs : 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 libc "setenv"prim_setEnv : String -> String -> Int -> PrimIO Int%foreign libc "setenv"prim_unsetEnv : String -> PrimIO Int exportgetEnv : 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)) exportgetEnvironment : 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) exportsetEnv : String -> String -> Bool -> IO BoolsetEnv 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 exportunsetEnv : String -> IO BoolunsetEnv 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 exportsystem : String -> IO Intsystem cmd = primIO (prim_system cmd) %foreign support "idris2_time"         "scheme:blodwen-time"prim_time : PrimIO Int exporttime : IO Integertime = pure $ cast !(primIO prim_time) %foreign libc "exit"prim_exit : Int -> PrimIO () ||| Programs can either terminate successfully, or end in a caught||| failure.public exportdata 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 exportexitWith : ExitCode -> IO aexitWith ExitSuccess = believe_me $ primIO $ prim_exit 0exitWith (ExitFailure code) = believe_me $ primIO $ prim_exit code ||| Exit the program indicating failure.exportexitFailure : IO aexitFailure = exitWith (ExitFailure 1) ||| Exit the program after a successful run.exportexitSuccess : IO aexitSuccess = exitWith ExitSuccess