0 | module System.Posix.Socket.Prim

  2 | import System.Posix.File.Prim

  4 | import public Data.Buffer

  5 | import public Data.Buffer.Core

  6 | import public Data.ByteString

  7 | import public Data.ByteVect

  8 | import public Data.C.Ptr

  9 | import public System.Posix.Errno

 10 | import public System.Posix.File.FileDesc

 11 | import public System.Posix.File.ReadRes

 12 | import public System.Posix.Socket.Struct

 13 | import public System.Posix.Socket.Types

 15 | %default total

 21 | %foreign "C:li_socket, posix-idris"

 22 | prim__socket : Bits8 -> Bits32 -> PrimIO CInt

 24 | %foreign "C:li_bind, posix-idris"

 25 | prim__bind : Bits32 -> AnyPtr -> Bits32 -> PrimIO CInt

 27 | %foreign "C:li_connect, posix-idris"

 28 | prim__connect : Bits32 -> AnyPtr -> Bits32 -> PrimIO CInt

 30 | %foreign "C:li_listen, posix-idris"

 31 | prim__listen : Bits32 -> Bits32 -> PrimIO CInt

 33 | %foreign "C:li_accept, posix-idris"

 34 | prim__accept : Bits32 -> PrimIO CInt

 36 | %foreign "C__collect_safe:li_recv, posix-idris"

 37 | prim__recvptr : (file : Bits32) -> AnyPtr -> (max : Bits32) -> Bits32 -> PrimIO SsizeT

 39 | %foreign "C:li_recv, posix-idris"

 40 | prim__recv : (file : Bits32) -> Buffer -> (max : Bits32) -> Bits32 -> PrimIO SsizeT

 42 | %foreign "C__collect_safe:li_recvfrom, posix-idris"

 43 | prim__recvfromptr : (file : Bits32) -> AnyPtr -> (max : Bits32) -> Bits32 -> AnyPtr -> Bits32 -> PrimIO SsizeT

 45 | %foreign "C:li_recvfrom, posix-idris"

 46 | prim__recvfrom : (file : Bits32) -> Buffer -> (max : Bits32) -> Bits32 -> AnyPtr -> Bits32 -> PrimIO SsizeT

 48 | %foreign "C:li_sendto, posix-idris"

 49 | prim__sendto : (file : Bits32) -> Buffer -> (off,max : Bits32) -> Bits32 -> AnyPtr -> Bits32 -> PrimIO SsizeT

 51 | %foreign "C__collect_safe:li_sendto, posix-idris"

 52 | prim__sendtoptr : (file : Bits32) -> AnyPtr -> (off,max : Bits32) -> Bits32 -> AnyPtr -> Bits32 -> PrimIO SsizeT

 54 | %foreign "C:li_getpeername, posix-idris"

 55 | prim__getpeername : Bits32 -> AnyPtr -> Bits32 -> PrimIO CInt

 57 | %foreign "C:li_getsockname, posix-idris"

 58 | prim__getsockname : Bits32 -> AnyPtr -> Bits32 -> PrimIO CInt

 60 | %foreign "C:li_setsockopt_bool, posix-idris"

 61 | prim__setsockopt_bool : Bits32 -> Bits32 -> Bits32 -> Bits8 -> PrimIO CInt

 63 | %foreign "C:li_setsockopt_linger, posix-idris"

 64 | prim__setsockopt_linger : Bits32 -> Bits32 -> Bits32 -> PrimIO CInt

 72 | export %inline

 73 | socket : (d : Domain) -> SockType -> EPrim (Socket d)

 74 | socket d (ST st) = toVal cast (prim__socket (domainCode d) st)

 80 | export %inline

 81 | listen : Socket d -> (backlog : Bits32) -> EPrim ()

 82 | listen s backlog = toUnit (prim__listen (fileDesc s) backlog)

 87 | export %inline

 88 | accept : Socket d -> EPrim (Socket d)

 89 | accept s = toVal cast (prim__accept (fileDesc s))

 94 | bind_ : {d : _} -> Socket d -> Sockaddr d -> EPrim ()

 95 | bind_ s a = toUnit $ prim__bind (fileDesc s) (ptr d a) (addrSize d)

100 | connect_ : {d : _} -> Socket d -> Sockaddr d -> EPrim ()

101 | connect_ s a = toUnit $ prim__connect (fileDesc s) (ptr d a) (addrSize d)

103 | parameters (s : Socket d)

104 |   ||| Reads at most `n` bytes from a file into an allocated pointer.

105 |   export %inline

106 |   recvPtr : (0 r : Type) -> FromPtr r => CPtr -> SockFlags -> EPrim (ReadRes r)

107 |   recvPtr r (CP sz p) (SF f) = ptrToRes p $ prim__recvptr (fileDesc s) p sz f

109 |   ||| Reads at most `n` bytes from a file into a bytestring.

110 |   export

111 |   recv : (0 r : Type) -> FromBuf r => Bits32 -> SockFlags -> EPrim (ReadRes r)

112 |   recv r n (SF f) = toRes n $ \b,x => prim__recv (fileDesc s) b x f

115 | export %inline

116 | recvFromPtr :

117 |      {d : _}

118 |   -> Socket d

119 |   -> (0 r : Type)

120 |   -> {auto frp : FromPtr r}

121 |   -> CPtr

122 |   -> SockFlags

123 |   -> Sockaddr d

124 |   -> EPrim r

125 | recvFromPtr s r (CP sz pt) (SF f) p =

126 |   ptrRead pt $ prim__recvfromptr (fileDesc s) pt sz f (ptr d p) (addrSize d)

129 | export %inline

130 | recvFrom :

131 |      {d : _}

132 |   -> Socket d

133 |   -> (0 r : Type)

134 |   -> {auto frb : FromBuf r}

135 |   -> (n : Bits32)

136 |   -> SockFlags

137 |   -> Sockaddr d

138 |   -> EPrim r

139 | recvFrom s r n (SF f) p =

140 |   allocRead n $ \buf,x => prim__recvfrom (fileDesc s) buf x f (ptr d p) (addrSize d)

144 | export %inline

145 | sendto :

146 |      {d : _}

147 |   -> {auto tob : ToBuf r}

148 |   -> Socket d

149 |   -> r

150 |   -> SockFlags

151 |   -> Sockaddr d

152 |   -> EPrim Bits32

153 | sendto s v (SF f) p =

154 |   case unsafeToBuf v of

155 |     Left (CP sz pt) =>

156 |       toSize $ prim__sendtoptr (fileDesc s) pt 0 sz f (ptr d p) (addrSize d)

157 |     Right (BS n $ BV b o _) =>

158 |       toSize $ prim__sendto

159 |         (fileDesc s)

160 |         (unsafeGetBuffer b)

161 |         (cast o)

162 |         (cast n)

163 |         f

164 |         (ptr d p)

165 |         (addrSize d)

173 | bind : {d : _} -> Socket d -> Addr d -> EPrim ()

174 | bind s a t =

175 |   let addr # t := sockaddr d a t

176 |    in finally (prim__free $ ptr d addr) (bind_ s addr) t

180 | connect : {d : _} -> Socket d -> Addr d -> EPrim ()

181 | connect s a t =

182 |   let addr # t := sockaddr d a t

183 |    in finally (prim__free $ ptr d addr) (connect_ s addr) t

188 | getpeername_ : {d : _} -> Socket d -> Sockaddr d -> EPrim ()

189 | getpeername_ s a = toUnit $ prim__getpeername (fileDesc s) (ptr d a) (addrSize d)

194 | getsockname_ : {d : _} -> Socket d -> Sockaddr d -> EPrim ()

195 | getsockname_ s a = toUnit $ prim__getsockname (fileDesc s) (ptr d a) (addrSize d)

199 | getpeername : {d : _} -> Socket d -> EPrim (Addr d)

200 | getpeername {d = AF_UNIX} s = withStruct SSockaddrUn $ \a,t =>

201 |   let R _ t := getpeername_ s a t | E x t => E x t

202 |       p # t := path a t

203 |     in R p t

204 | getpeername {d = AF_INET} s = withStruct SSockaddrIn $ \a,t =>

205 |   let R _   t := getpeername_ s a t | E x t => E x t

206 |       ipp # t := SockaddrIn.addrIP4Addr a t

207 |     in R ipp t

208 | getpeername {d = AF_INET6} s = withStruct SSockaddrIn6 $ \a,t =>

209 |   let R _  t := getpeername_ s a t | E x t => E x t

210 |       ipp # t := SockaddrIn6.addrIP6Addr a t

211 |     in R ipp t

215 | getsockname : {d : _} -> Socket d -> EPrim (Addr d)

216 | getsockname {d = AF_UNIX} s = withStruct SSockaddrUn $ \a,t =>

217 |   let R _ t := getsockname_ s a t | E x t => E x t

218 |       p # t := path a t

219 |     in R p t

220 | getsockname {d = AF_INET} s = withStruct SSockaddrIn $ \a,t =>

221 |   let R _   t := getsockname_ s a t | E x t => E x t

222 |       ipp # t := SockaddrIn.addrIP4Addr a t

223 |     in R ipp t

224 | getsockname {d = AF_INET6} s = withStruct SSockaddrIn6 $ \a,t =>

225 |   let R _  t := getsockname_ s a t | E x t => E x t

226 |       ipp # t := SockaddrIn6.addrIP6Addr a t

227 |     in R ipp t

233 | boolToInt : Bool -> Bits8

234 | boolToInt False = 0

235 | boolToInt True  = 1

239 | setNoDelay : Socket d -> Bool -> EPrim ()

240 | setNoDelay s b = toUnit $ prim__setsockopt_bool (fileDesc s) IPPROTO_TCP TCP_NODELAY (boolToInt b)

244 | setReuseAddress : Socket d -> Bool -> EPrim ()

245 | setReuseAddress s b = toUnit $ prim__setsockopt_bool (fileDesc s) SOL_SOCKET SO_REUSEADDR (boolToInt b)

253 | setLinger : Socket d -> Maybe Bits32 -> EPrim ()

254 | setLinger s Nothing  = toUnit $ prim__setsockopt_linger (fileDesc s) 0 0

255 | setLinger s (Just t) = toUnit $ prim__setsockopt_linger (fileDesc s) 1 t