0 | module System.File.Process
  1 |
  2 | import public System.Escape
  3 | import public System.File.Error
  4 | import public System.File.Mode
  5 | import System.FFI
  6 | import System.File.Support
  7 | import public System.File.Types
  8 |
  9 | %foreign "C:fflush,libc 6"
 10 |          "node:lambda:()=>0"
 11 | prim__flush : FilePtr -> PrimIO Int
 12 | %foreign supportC "idris2_popen"
 13 |          supportNode "popen"
 14 | prim__popen : String -> String -> PrimIO FilePtr
 15 | %foreign supportC "idris2_pclose"
 16 |          supportNode "pclose"
 17 | prim__pclose : FilePtr -> PrimIO Int
 18 |
 19 | data Popen2Result : Type where [external]
 20 |
 21 | %foreign supportC "idris2_popen2"
 22 | prim__popen2 : String -> PrimIO (Ptr Popen2Result)
 23 |
 24 | %foreign supportC "idris2_popen2WaitByPid"
 25 | covering -- significantly non-total
 26 | prim__popen2WaitByPid : Int -> PrimIO Int
 27 | %foreign supportC "idris2_popen2WaitByHandler"
 28 | covering -- significantly non-total
 29 | prim__popen2WaitByHandler : AnyPtr -> PrimIO Int
 30 |
 31 | %foreign supportC "idris2_popen2ChildPid"
 32 | prim__popen2ChildPid : Ptr Popen2Result -> PrimIO Int
 33 |
 34 | %foreign supportC "idris2_popen2ChildHandler"
 35 | prim__popen2ChildHandler : Ptr Popen2Result -> PrimIO AnyPtr
 36 |
 37 | %foreign supportC "idris2_popen2FileIn"
 38 | prim__popen2FileIn : Ptr Popen2Result -> PrimIO FilePtr
 39 |
 40 | %foreign supportC "idris2_popen2FileOut"
 41 | prim__popen2FileOut : Ptr Popen2Result -> PrimIO FilePtr
 42 |
 43 | ||| Force a write of all user-space buffered data for the given `File`.
 44 | |||
 45 | ||| @ h the file handle to flush
 46 | export
 47 | fflush : HasIO io => (h : File) -> io ()
 48 | fflush (FHandle f)
 49 |     = ignore $ primIO (prim__flush f)
 50 |
 51 | ||| Create a new unidirectional pipe by invoking the shell, which is passed the
 52 | ||| given command-string using the '-c' flag, in a new process. The pipe is
 53 | ||| opened with the given mode.
 54 | |||
 55 | ||| IMPORTANT: The NodeJS backend only currently supports the Read mode. Also with
 56 | |||            the NodeJS backend, the opened process will finish execution before
 57 | |||            popen returns (it blocks on open) which is different than other
 58 | |||            backends which will block on close.
 59 | |||
 60 | ||| @ cmd the command to pass to the shell
 61 | ||| @ m   the mode the pipe should have
 62 | export
 63 | popen : HasIO io => (cmd : String) -> (m : Mode) -> io (Either FileError File)
 64 | popen cmd m = do
 65 |     ptr <- primIO (prim__popen cmd (modeStr m))
 66 |     if prim__nullAnyPtr ptr /= 0
 67 |         then returnError
 68 |         else pure (Right (FHandle ptr))
 69 |
 70 |
 71 | ||| Wait for the process associated with the pipe to terminate.
 72 | |||
 73 | ||| @ fh the file handle to the stream to close/wait on
 74 | export
 75 | pclose : HasIO io => (fh : File) -> io Int
 76 | pclose (FHandle h) = primIO (prim__pclose h)
 77 |
 78 | ||| Result of a popen2 command, containing the
 79 | public export
 80 | record SubProcess where
 81 |   constructor MkSubProcess
 82 |   ||| Process id of the spawned process
 83 |   pid : Int
 84 |   ||| The way to manipulate the spawned process, for systems where pid is not enough for this
 85 |   handler : AnyPtr
 86 |   ||| The input stream of the spawned process
 87 |   input : File
 88 |   ||| The output stream of the spawned process
 89 |   output : File
 90 |
 91 | ||| Create a new bidirectional pipe by invoking the shell, which is passed the
 92 | ||| given command-string using the '-c' flag, in a new process. On success
 93 | ||| a SubProcess is returned which holds the process id and file handles
 94 | ||| for input and output.
 95 | ||| You should call `popen2Wait` after you've done with the child process
 96 | ||| in order to clean up all system resources.
 97 | |||
 98 | ||| IMPORTANT: You may deadlock if write to a process which is waiting to flush
 99 | |||            its output.  It is recommended to read and write from separate threads.
100 | |||
101 | ||| This function is not supported on node at this time.
102 | export
103 | popen2 : HasIO io => (cmd : String) -> io (Either FileError SubProcess)
104 | popen2 cmd = do
105 |   ptr <- primIO (prim__popen2 cmd)
106 |   if prim__nullPtr ptr /= 0
107 |     then returnError
108 |     else do
109 |       pid <- primIO (prim__popen2ChildPid ptr)
110 |       handle <- primIO (prim__popen2ChildHandler ptr)
111 |       input <- primIO (prim__popen2FileIn ptr)
112 |       output <- primIO (prim__popen2FileOut ptr)
113 |       free (prim__forgetPtr ptr)
114 |       pure $ Right (MkSubProcess pid handle (FHandle input) (FHandle output))
115 |
116 | ||| Blocks and waits until the process created by `popen2` finished
117 | |||
118 | ||| This function relates to `popen2` like `pclose` relates to `popen`.
119 | ||| Returns exit code of the process being waited.
120 | ||| IMPORTANT: this function mustn't be called twice for the same argument.
121 | |||
122 | ||| Support of this function in the backends must be the same as for `popen2`.
123 | export
124 | covering -- significantly non-total
125 | popen2Wait : HasIO io => SubProcess -> io Int
126 | popen2Wait sp = primIO $
127 |   if prim__nullAnyPtr sp.handler /= 0
128 |     then prim__popen2WaitByPid sp.pid
129 |     else prim__popen2WaitByHandler sp.handler
130 |
131 | namespace Escaped
132 |   export
133 |   popen : HasIO io => (cmd : List String) -> (m : Mode) -> io (Either FileError File)
134 |   popen = popen . escapeCmd
135 |
136 |   export
137 |   popen2 : HasIO io => (cmd : List String) -> io (Either FileError SubProcess)
138 |   popen2 = popen2 . escapeCmd
139 |