0 | module System.Linux.Error
  1 |
  2 | import Data.Maybe
  3 | import Data.List
  4 | import Derive.Finite
  5 | import Derive.Prelude
  6 |
  7 | %default total
  8 | %language ElabReflection
  9 |
 10 | export %foreign "C:ep_eagain,epoll-idris"
 11 | eagain : Bits32
 12 |
 13 | export %foreign "C:ep_ebadf,epoll-idris"
 14 | ebadf : Bits32
 15 |
 16 | export %foreign "C:ep_eexist,epoll-idris"
 17 | eexist : Bits32
 18 |
 19 | export %foreign "C:ep_efault,epoll-idris"
 20 | efault : Bits32
 21 |
 22 | export %foreign "C:ep_einval,epoll-idris"
 23 | einval : Bits32
 24 |
 25 | export %foreign "C:ep_eisdir,epoll-idris"
 26 | eisdir : Bits32
 27 |
 28 | export %foreign "C:ep_eio,epoll-idris"
 29 | eio : Bits32
 30 |
 31 | export %foreign "C:ep_eloop,epoll-idris"
 32 | eloop : Bits32
 33 |
 34 | export %foreign "C:ep_enoent,epoll-idris"
 35 | enoent : Bits32
 36 |
 37 | export %foreign "C:ep_enomem,epoll-idris"
 38 | enomem : Bits32
 39 |
 40 | export %foreign "C:ep_enospc,epoll-idris"
 41 | enospc : Bits32
 42 |
 43 | export %foreign "C:ep_eperm,epoll-idris"
 44 | eperm : Bits32
 45 |
 46 | export %foreign "C:ep_ewouldblock,epoll-idris"
 47 | ewouldblock : Bits32
 48 |
 49 | export %foreign "C:ep_eintr,epoll-idris"
 50 | eintr : Bits32
 51 |
 52 | export %foreign "C:ep_edestaddrreq,epoll-idris"
 53 | edestaddrreq : Bits32
 54 |
 55 | export %foreign "C:ep_efbig,epoll-idris"
 56 | efbig : Bits32
 57 |
 58 | export %foreign "C:ep_edquot,epoll-idris"
 59 | edquot : Bits32
 60 |
 61 | export %foreign "C:ep_epipe,epoll-idris"
 62 | epipe : Bits32
 63 |
 64 | %foreign  "C:ep_errno,epoll-idris"
 65 | prim__errno : PrimIO Bits32
 66 |
 67 | public export
 68 | data EpollErr : Type where
 69 |   EAGAIN       : EpollErr
 70 |   EBADF        : EpollErr
 71 |   EDESTADDRREQ : EpollErr
 72 |   EDQUOT       : EpollErr
 73 |   EEXIST       : EpollErr
 74 |   EFAULT       : EpollErr
 75 |   EFBIG        : EpollErr
 76 |   EINTR        : EpollErr
 77 |   EINVAL       : EpollErr
 78 |   EIO          : EpollErr
 79 |   EISDIR       : EpollErr
 80 |   ELOOP        : EpollErr
 81 |   ENOENT       : EpollErr
 82 |   ENOMEM       : EpollErr
 83 |   ENOSPC       : EpollErr
 84 |   EPERM        : EpollErr
 85 |   EPIPE        : EpollErr
 86 |
 87 | %runElab derive "EpollErr" [Show,Eq,Finite]
 88 |
 89 | export
 90 | Interpolation EpollErr where interpolate = show
 91 |
 92 | export
 93 | errCode : EpollErr -> Bits32
 94 | errCode EAGAIN       = eagain
 95 | errCode EBADF        = ebadf
 96 | errCode EDQUOT       = edquot
 97 | errCode EDESTADDRREQ = edestaddrreq
 98 | errCode EEXIST       = eexist
 99 | errCode EFAULT       = efault
100 | errCode EFBIG        = efbig
101 | errCode EISDIR       = eisdir
102 | errCode EINTR        = eintr
103 | errCode EINVAL       = einval
104 | errCode EIO          = eio
105 | errCode ELOOP        = eloop
106 | errCode ENOENT       = enoent
107 | errCode ENOMEM       = enomem
108 | errCode ENOSPC       = enospc
109 | errCode EPERM        = eperm
110 | errCode EPIPE        = epipe
111 |
112 | pairs : List (Bits32,EpollErr)
113 | pairs = (ewouldblock, EAGAIN) :: map (\x => (errCode x, x)) values
114 |
115 | export
116 | fromCode : Bits32 -> EpollErr
117 | fromCode x = fromMaybe EINVAL $ lookup x pairs
118 |
119 | export
120 | getErr : PrimIO (Either EpollErr a)
121 | getErr w =
122 |   let MkIORes v w := prim__errno w
123 |    in MkIORes (Left $ fromCode v) w
124 |
125 | export
126 | checkErr : Int32 -> PrimIO (Either EpollErr ())
127 | checkErr n w = if n < 0 then getErr w else MkIORes (Right ()) w
128 |
129 | export
130 | checkSize : Int32 -> PrimIO (Either EpollErr Nat)
131 | checkSize n w = if n < 0 then getErr w else MkIORes (Right $ cast n) w
132 |