0 | module System.Linux.File
  1 |
  2 | import Derive.Finite
  3 | import Derive.Prelude
  4 | import Data.Buffer
  5 | import Data.Buffer.Core
  6 | import System.Linux.Error
  7 |
  8 | %default total
  9 | %language ElabReflection
 10 |
 11 | --------------------------------------------------------------------------------
 12 | -- FFI
 13 | --------------------------------------------------------------------------------
 14 |
 15 | %foreign "C:ep_read,epoll-idris"
 16 | prim__read : Bits32 -> (buf : Buffer) -> (offset,max : Bits32) -> PrimIO Int32
 17 |
 18 | %foreign "C:ep_write,epoll-idris"
 19 | prim__write : Bits32 -> (buf : Buffer) -> (offset,max : Bits32) -> PrimIO Int32
 20 |
 21 | %foreign "C:close,epoll-idris"
 22 | prim__close : Bits32 -> PrimIO ()
 23 |
 24 | %foreign "C:ep_set_nonblocking,epoll-idris"
 25 | prim__setNonBlocking : Bits32 -> PrimIO ()
 26 |
 27 | --------------------------------------------------------------------------------
 28 | -- API
 29 | --------------------------------------------------------------------------------
 30 |
 31 | public export
 32 | interface FileDesc  a where
 33 |   fileDesc : a -> Bits32
 34 |
 35 | export %inline
 36 | FileDesc Bits32 where fileDesc x = x
 37 |
 38 | ||| Result of reading from a file descriptor
 39 | public export
 40 | data ReadRes : Type where
 41 |   ||| End of file has been reached
 42 |   EOF   : ReadRes
 43 |
 44 |   ||| This occurs when reading from a file descriptor in non-blocking mode
 45 |   ||| and there is currently no data ready.
 46 |   Again : ReadRes
 47 |
 48 |   ||| The given numbers have been read into an immutable buffer
 49 |   Bytes : (n : Nat) -> IBuffer n -> ReadRes
 50 |
 51 |   ||| An error occured
 52 |   Err   : EpollErr -> ReadRes
 53 |
 54 | toReadRes : Either EpollErr Nat -> Buffer -> ReadRes
 55 | toReadRes (Left EAGAIN)      _   = Again
 56 | toReadRes (Left x)           _   = Err x
 57 | toReadRes (Right 0)          _   = EOF
 58 | toReadRes (Right n)          buf = Bytes n (unsafeMakeBuffer buf)
 59 |
 60 | parameters {0 a : Type}
 61 |            {auto fd : FileDesc a}
 62 |
 63 |   ||| Close a file descriptor.
 64 |   export %inline
 65 |   close : a -> PrimIO ()
 66 |   close = prim__close . fileDesc
 67 |
 68 |   ||| Low-level reading of at most `max` bytes from a file into a buffer
 69 |   ||| starting at buffer offset `offset`.
 70 |   |||
 71 |   ||| See `readBytes` for a higher-level function that allocates a new buffer and
 72 |   ||| correctly interprets the result.
 73 |   export
 74 |   read : a -> Buffer -> (offset,max : Nat) -> PrimIO (Either EpollErr Nat)
 75 |   read fi buf offset max w =
 76 |     let MkIORes res w :=prim__read (fileDesc fi) buf (cast offset) (cast max) w
 77 |      in checkSize res w
 78 |
 79 |   export
 80 |   write : a -> Buffer -> (offset,max : Nat) -> PrimIO (Either EpollErr Nat)
 81 |   write fi buf offset max w =
 82 |     let MkIORes res w :=prim__write (fileDesc fi) buf (cast offset) (cast max) w
 83 |      in checkSize res w
 84 |
 85 |   ||| A higher-level alternative to `read`: It allocates a new buffer of the
 86 |   ||| given size and returns it wrapped in a `ReadRes`.
 87 |   |||
 88 |   ||| Use `read` if you want to avoid allocating a new buffer for every
 89 |   ||| data package.
 90 |   export
 91 |   readBytes : a -> (max : Nat) -> PrimIO ReadRes
 92 |   readBytes fi max w =
 93 |     let MkIORes buf w := prim__newBuf (cast max) w
 94 |         MkIORes res w := read fi buf 0 max w
 95 |      in MkIORes (toReadRes res buf) w
 96 |
 97 |   ||| Changes a file descriptor's mode to `O_NONBLOCK`.
 98 |   |||
 99 |   ||| This will not block when trying to read from a stream such as a pipe, socket, or
100 |   ||| stdin. Instead, `readBytes` will return `Again` in case no data is currently
101 |   ||| available. Use this in combination with `EPOLLET` to keep reading from a data
102 |   ||| source until it is temporarily exhausted.
103 |   export
104 |   setNonBlocking : a -> PrimIO ()
105 |   setNonBlocking = prim__setNonBlocking . fileDesc
106 |
107 | public export
108 | data StdFile : Type where
109 |   StdIn  : StdFile
110 |   StdOut : StdFile
111 |   StdErr : StdFile
112 |
113 | %runElab derive "StdFile" [Show,Eq,Ord,Finite]
114 |
115 | export %inline
116 | FileDesc StdFile where fileDesc = cast . conIndexStdFile
117 |