2 | import public Data.So
5 | import public System.Escape
13 | supportC : (fn : String) -> String
14 | supportC fn = "C:\{fn}, libidris2_support, idris_support.h"
19 | supportNode : (fn : String) -> String
20 | supportNode fn = "node:support:\{fn},support_system"
25 | libc : (fn : String) -> String
26 | libc fn = "C:" ++ fn ++ ", libc 6"
31 | %foreign "scheme,racket:blodwen-sleep"
32 | supportC "idris2_sleep"
33 | prim__sleep : Int -> PrimIO ()
35 | %foreign "scheme,racket:blodwen-usleep"
36 | supportC "idris2_usleep"
37 | prim__usleep : Int -> PrimIO ()
46 | sleep : HasIO io => (sec : Int) -> io ()
47 | sleep sec = primIO (prim__sleep sec)
56 | usleep : HasIO io => (usec : Int) -> So (usec >= 0) => io ()
57 | usleep usec = primIO (prim__usleep usec)
66 | %foreign "scheme:blodwen-arg-count"
67 | supportC "idris2_getArgCount"
68 | "node:lambda:() => process.argv.length - 1"
69 | prim__getArgCount : PrimIO Int
73 | %foreign "scheme:blodwen-arg"
74 | supportC "idris2_getArg"
75 | "node:lambda:n => process.argv[n + 1]"
76 | prim__getArg : Int -> PrimIO String
80 | getArgs : HasIO io => io (List String)
82 | n <- primIO prim__getArgCount
84 | then for [0..n-1] $
primIO . prim__getArg
87 | %foreign libc "getenv"
88 | "node:lambda: n => process.env[n]"
89 | prim__getEnv : String -> PrimIO (Ptr String)
91 | %foreign supportC "idris2_getEnvPair"
92 | prim__getEnvPair : Int -> PrimIO (Ptr String)
93 | %foreign supportC "idris2_setenv"
94 | supportNode "setEnv"
95 | prim__setEnv : String -> String -> Int -> PrimIO Int
96 | %foreign supportC "idris2_unsetenv"
97 | supportNode "unsetEnv"
98 | prim__unsetEnv : String -> PrimIO Int
100 | %foreign "C:idris2_enableRawMode, libidris2_support, idris_support.h"
101 | prim__enableRawMode : (1 x : %World) -> IORes Int
103 | %foreign "C:idris2_resetRawMode, libidris2_support, idris_support.h"
104 | prim__resetRawMode : (1 x : %World) -> IORes ()
113 | enableRawMode : HasIO io => io (Either FileError ())
115 | case !(primIO prim__enableRawMode) of
116 | 0 => pure $
Right ()
122 | resetRawMode : HasIO io => io ()
123 | resetRawMode = primIO prim__resetRawMode
130 | withRawMode : HasIO io =>
131 | (onError : FileError -> io a) ->
132 | (onSuccess : () -> io a) ->
134 | withRawMode onError onSuccess = do
135 | Right () <- enableRawMode
136 | | Left err => onError err
137 | result <- onSuccess ()
146 | getEnv : HasIO io => (var : String) -> io (Maybe String)
148 | = do env <- primIO $
prim__getEnv var
149 | if prim__nullPtr env /= 0
151 | else pure (Just (prim__getString env))
157 | getEnvironment : HasIO io => io (List (String, String))
158 | getEnvironment = getAllPairs 0 []
160 | splitEq : String -> (String, String)
162 | = let (k, v) = break (== '=') str
163 | (_, v') = break (/= '=') v in
166 | getAllPairs : Int -> List String -> io (List (String, String))
167 | getAllPairs n acc = do
168 | envPair <- primIO $
prim__getEnvPair n
169 | if prim__nullPtr envPair /= 0
170 | then pure $
reverse $
map splitEq acc
171 | else getAllPairs (n + 1) (prim__getString envPair :: acc)
184 | setEnv : HasIO io => (var : String) -> (val : String) -> (overwrite : Bool) ->
186 | setEnv var val overwrite
187 | = do ok <- primIO $
prim__setEnv var val (if overwrite then 1 else 0)
194 | unsetEnv : HasIO io => (var : String) -> io Bool
196 | = do ok <- primIO $
prim__unsetEnv var
199 | %foreign "C:idris2_system, libidris2_support, idris_system.h"
200 | supportNode "spawnSync"
201 | prim__system : String -> PrimIO Int
206 | system : HasIO io => String -> io Int
207 | system cmd = primIO (prim__system cmd)
211 | system : HasIO io => List String -> io Int
212 | system = system . escapeCmd
217 | run : HasIO io => (cmd : String) -> io (String, Int)
219 | Right f <- popen cmd Read
220 | | Left err => pure ("", 1)
221 | Right resp <- fRead f
222 | | Left err => pure ("", 1)
223 | exitCode <- pclose f
224 | pure (resp, exitCode)
229 | run : HasIO io => (cmd : List String) -> io (String, Int)
230 | run = run . escapeCmd
240 | runProcessingOutput : HasIO io => (String -> io ()) -> (cmd : String) -> io Int
241 | runProcessingOutput pr cmd = do
242 | Right f <- popen cmd Read
243 | | Left err => pure 1
249 | process : File -> io Bool
250 | process h = if !(fEOF h) then pure True else do
251 | Right line <- fGetLine h
252 | | Left err => pure False
259 | runProcessingOutput : HasIO io => (String -> io ()) -> (cmd : List String) -> io Int
260 | runProcessingOutput pr = runProcessingOutput pr . escapeCmd
262 | %foreign supportC "idris2_time"
263 | "javascript:lambda:() => Math.floor(new Date().getTime() / 1000)"
264 | prim__time : PrimIO Int
268 | time : HasIO io => io Integer
269 | time = pure $
cast !(primIO prim__time)
271 | %foreign supportC "idris2_getPID"
272 | "node:lambda:() => process.pid"
273 | prim__getPID : PrimIO Int
277 | getPID : HasIO io => io Int
278 | getPID = primIO prim__getPID
280 | %foreign libc "exit"
281 | "node:lambda:c => process.exit(c)"
282 | prim__exit : Int -> PrimIO ()
287 | data ExitCode : Type where
289 | ExitSuccess : ExitCode
294 | ExitFailure : (errNo : Int) -> (So (not $
errNo == 0)) => ExitCode
297 | Cast Int ExitCode where
298 | cast 0 = ExitSuccess
299 | cast code = ExitFailure code @{believe_me Oh}
302 | Cast ExitCode Int where
303 | cast ExitSuccess = 0
304 | cast (ExitFailure code) = code
308 | exitWith : HasIO io => ExitCode -> io a
309 | exitWith = primIO . believe_me . prim__exit . cast
314 | exitFailure : HasIO io => io a
315 | exitFailure = exitWith (ExitFailure 1)
319 | exitSuccess : HasIO io => io a
320 | exitSuccess = exitWith ExitSuccess
324 | die : HasIO io => String -> io a
326 | = do ignore $
fPutStrLn stderr str