Utils.Handle

Definitions

ReadHack : Type -> Type -> Bool -> Type

Visibility: public export

WriteHack : Type -> Type -> Bool -> Type

Visibility: public export

record Handle : Type -> Type -> Type -> Type -> Type

Totality: total
Visibility: public export
Constructor: 

MkHandle : (1 _ : t_ok) -> (LinearIO m => (1 _ : t_ok) -> Nat -> L1 m (Res Bool (ReadHack t_ok t_read_failed))) -> (LinearIO m => (1 _ : t_ok) -> List Bits8 -> L1 m (Res Bool (WriteHack t_ok t_write_failed))) -> (LinearIO m => (1 _ : t_ok) -> L1 m t_closed) -> Handle t_ok t_closed t_read_failed t_write_failed

Projections:

.do_close : Handle t_ok t_closed t_read_failed t_write_failed -> LinearIO m => (1 _ : t_ok) -> L1 m t_closed

.do_read : Handle t_ok t_closed t_read_failed t_write_failed -> LinearIO m => (1 _ : t_ok) -> Nat -> L1 m (Res Bool (ReadHack t_ok t_read_failed))

.do_write : Handle t_ok t_closed t_read_failed t_write_failed -> LinearIO m => (1 _ : t_ok) -> List Bits8 -> L1 m (Res Bool (WriteHack t_ok t_write_failed))

.underlying : Handle t_ok t_closed t_read_failed t_write_failed -> t_ok

.underlying : Handle t_ok t_closed t_read_failed t_write_failed -> t_ok

Visibility: public export

underlying : Handle t_ok t_closed t_read_failed t_write_failed -> t_ok

Visibility: public export

.do_read : Handle t_ok t_closed t_read_failed t_write_failed -> LinearIO m => (1 _ : t_ok) -> Nat -> L1 m (Res Bool (ReadHack t_ok t_read_failed))

Visibility: public export

do_read : Handle t_ok t_closed t_read_failed t_write_failed -> LinearIO m => (1 _ : t_ok) -> Nat -> L1 m (Res Bool (ReadHack t_ok t_read_failed))

Visibility: public export

.do_write : Handle t_ok t_closed t_read_failed t_write_failed -> LinearIO m => (1 _ : t_ok) -> List Bits8 -> L1 m (Res Bool (WriteHack t_ok t_write_failed))

Visibility: public export

do_write : Handle t_ok t_closed t_read_failed t_write_failed -> LinearIO m => (1 _ : t_ok) -> List Bits8 -> L1 m (Res Bool (WriteHack t_ok t_write_failed))

Visibility: public export

.do_close : Handle t_ok t_closed t_read_failed t_write_failed -> LinearIO m => (1 _ : t_ok) -> L1 m t_closed

Visibility: public export

do_close : Handle t_ok t_closed t_read_failed t_write_failed -> LinearIO m => (1 _ : t_ok) -> L1 m t_closed

Visibility: public export

close : LinearIO m => (1 _ : Handle t_ok t_closed t_read_failed t_write_failed) -> L1 m t_closed

Visibility: public export

read : {auto {conArg:1461} : LinearIO m} -> (1 {arg:1464} : Handle t_ok t_closed t_read_failed t_write_failed) -> (len : Nat) -> L1 m (Res Bool (\{lcase:0} => case {lcase:0} of { False => t_read_failed ; True => Res (List Bits8) (\{_:1523} => Handle t_ok t_closed t_read_failed t_write_failed) }))

Visibility: public export

write : {auto {conArg:1706} : LinearIO m} -> (1 {arg:1709} : Handle t_ok t_closed t_read_failed t_write_failed) -> (input : List Bits8) -> L1 m (Res Bool (\{lcase:0} => case {lcase:0} of { False => t_write_failed ; True => Handle t_ok t_closed t_read_failed t_write_failed }))

Visibility: public export

Handle' : Type -> Type -> Type

Visibility: public export