System.Posix.File.ReadRes

Reexports

import public Control.Monad.Resource
import public Data.Buffer
import public Data.Buffer.Core
import public Data.ByteString
import public Data.C.Ptr
import public System.Posix.Errno

Definitions

data ReadRes : Type -> Type

  Result of a (potentially non-blocking) read, typically from a pipe
  or socket.

Totality: total
Visibility: public export
Constructors:

Interrupted : ReadRes a

  The system call was interrupted by a signal.

NoData : ReadRes a

  There is currently no data avialable (this will only be a possible
  outcome when reading in non-blocking mode).

Closed : ReadRes a

  Tried to read from a closed connection or pipe.

EOI : ReadRes a

  We reached the end of input.

Res : a -> ReadRes a

  We got `n` bytes of data.

Hints:

Eq {arg:6194} => Eq (ReadRes {arg:6194})
Foldable ReadRes
Functor ReadRes
Show {arg:6194} => Show (ReadRes {arg:6194})
Traversable ReadRes

fromErr : Errno -> EPrim (ReadRes a)

Totality: total
Visibility: export

record CPtr : Type

Totality: total
Visibility: public export
Constructor:

CP : Bits32 -> AnyPtr -> CPtr

Projections:

.ptr : CPtr -> AnyPtr
.size : CPtr -> Bits32

Hints:

FromBuf CPtr
FromPtr CPtr
ELift1 World f => Resource f CPtr
ToBuf CPtr

.size : CPtr -> Bits32

Totality: total
Visibility: public export

size : CPtr -> Bits32

Totality: total
Visibility: public export

.ptr : CPtr -> AnyPtr

Totality: total
Visibility: public export

ptr : CPtr -> AnyPtr

Totality: total
Visibility: public export

cptrOf1 : (0 a : Type) -> SizeOf a => Nat -> F1 World CPtr

Totality: total
Visibility: export

cptrOf : HasIO io => (0 a : Type) -> SizeOf a => Nat -> io CPtr

Totality: total
Visibility: export

cptr1 : Nat -> F1 World CPtr

Totality: total
Visibility: export

cptr : HasIO io => Nat -> io CPtr

Totality: total
Visibility: export

freePtr1 : CPtr -> F1' World

Totality: total
Visibility: export

freePtr : HasIO io => CPtr -> io ()

Totality: total
Visibility: export

record Buf : Type

Totality: total
Visibility: public export
Constructor:

B : Bits32 -> Buffer -> Buf

Projections:

.buf : Buf -> Buffer
.size : Buf -> Bits32

Hint:

FromBuf Buf

.size : Buf -> Bits32

Totality: total
Visibility: public export

size : Buf -> Bits32

Totality: total
Visibility: public export

.buf : Buf -> Buffer

Totality: total
Visibility: public export

buf : Buf -> Buffer

Totality: total
Visibility: public export

buf : Bits32 -> F1 World Buf

Totality: total
Visibility: export

interface FromBuf : Type -> Type

  Interface for wrapping or converting a freshly allocated buffer
  for reading, or an already allocated C-pointer for streaming
  data (typically from a file descriptor).
  
  Please note that not all conversions are guaranteed to be
  lossless. For instance, converting a buffer to a (UTF-8) string
  will only be safe if the byte array does not end in the middle of
  a codepoint consisting of several bytes.

Parameters: a
Methods:

fromBuf : Buf -> F1 World a

Implementations:

FromBuf Buf
FromBuf EMBuffer
FromBuf EBuffer
FromBuf ByteString
FromBuf String
FromBuf CPtr
SizeOf a => FromBuf (ECArrayIO a)
Convert t => FromBuf (List t)

fromBuf : FromBuf a => Buf -> F1 World a

Totality: total
Visibility: public export

0 EMBuffer : Type

Totality: total
Visibility: public export

0 EBuffer : Type

Totality: total
Visibility: public export

0 ECArrayIO : Type -> Type

Totality: total
Visibility: public export

interface ToBuf : Type -> Type

  Interface for converting a value for writing.
  
  We distinguis between three situations:
  
    a) The value is converted to a `ByteString`. In this case
       the value can be directly written and the runtime will take
       care of collecting its memory.
  
    b) The value is converted to a `CPtr`, which has been allocated
       elsewhere. We are not responsible for freeing the pointer as
       it might be reused for streaming.

Parameters: a
Methods:

unsafeToBuf : a -> Either CPtr ByteString

Implementations:

ToBuf ByteString
ToBuf String
ToBuf (IBuffer n)
ToBuf (MBuffer t n)
ToBuf CPtr
SizeOf a => ToBuf (CArray t n a)
SizeOf a => ToBuf (ECArrayIO a)
SizeOf a => SetPtr a => ToBuf (Vect n a)
SizeOf a => SetPtr a => ToBuf (List a)

unsafeToBuf : ToBuf a => a -> Either CPtr ByteString

Totality: total
Visibility: public export

record Convert : Type -> Type

Totality: total
Visibility: public export
Constructor:

C : (0 source : Type) -> SizeOf source => Deref source => (source -> F1 World t) -> Convert t

Projections:

.convert : ({rec:0} : Convert t) -> source {rec:0} -> F1 World t
.derf : ({rec:0} : Convert t) -> Deref (source {rec:0})
.sof : ({rec:0} : Convert t) -> SizeOf (source {rec:0})
0 .source : Convert t -> Type

Hints:

Convert t => FromBuf (List t)
Convert t => FromPtr (List t)

0 .source : Convert t -> Type

Totality: total
Visibility: public export

0 source : Convert t -> Type

Totality: total
Visibility: public export

.sof : ({rec:0} : Convert t) -> SizeOf (source {rec:0})

Totality: total
Visibility: public export

sof : ({rec:0} : Convert t) -> SizeOf (source {rec:0})

Totality: total
Visibility: public export

.derf : ({rec:0} : Convert t) -> Deref (source {rec:0})

Totality: total
Visibility: public export

derf : ({rec:0} : Convert t) -> Deref (source {rec:0})

Totality: total
Visibility: public export

.convert : ({rec:0} : Convert t) -> source {rec:0} -> F1 World t

Totality: total
Visibility: public export

convert : ({rec:0} : Convert t) -> source {rec:0} -> F1 World t

Totality: total
Visibility: public export

convStruct : (0 f : (Type -> Type)) -> Struct f => SizeOf (f World) => (f World -> F1 World t) -> Convert t

Totality: total
Visibility: public export

interface FromPtr : Type -> Type

  Interface for wrapping or converting a c-land pointer.
  
  This is useful for streaming data from a file descriptor.
  Idris (garbage collected) values are generated by copying the given
  number of bytes.
  
  Please note that not all conversions are guaranteed to be
  lossless. For instance, converting a buffer to a (UTF-8) string
  will only be safe if the byte array does not end in the middle of
  a codepoint consisting of several bytes.

Parameters: a
Methods:

fromPtr : CPtr -> F1 World a

Implementations:

FromPtr CPtr
SizeOf a => FromPtr (ECArrayIO a)
FromPtr EBuffer
FromPtr EMBuffer
FromPtr ByteString
FromPtr String
Convert t => FromPtr (List t)
SizeOf a => Deref a => FromPtr (List a)

fromPtr : FromPtr a => CPtr -> F1 World a

Totality: total
Visibility: public export

viaPtrFromBuf : FromPtr r => Buf -> F1 World r

Totality: total
Visibility: export