
  0 | module Utils.Handle.C
  1 | 
  2 | import Control.Linear.LIO
  3 | import Control.Monad.Error.Either
  4 | import Data.Nat
  5 | import Data.Vect
  6 | import Network.Socket
  7 | import Utils.Handle
  8 | 
  9 | -- Needed for some reason, sometimes the socket does not read enough bytes
 10 | recv_n_bytes : HasIO m => Socket -> Nat -> List Bits8 -> m (Either SocketError (List Bits8))
 11 | recv_n_bytes sock Z buf = pure (Right [])
 12 | recv_n_bytes sock size buf = do
 13 |   Right response <- recvBytes sock $ cast $ minus size $ length buf
 14 |   | error => pure error
 15 |   let buf = buf <+> response
 16 |   if (length buf) >= size
 17 |     then pure $ Right buf
 18 |     else recv_n_bytes sock size buf
 19 | 
 20 | ||| Turning a non-linear socket from Network.Socket into a Handle tailored for Network.TLS.Handle
 21 | export
 22 | socket_to_handle : Socket -> Handle' Socket ()
 23 | socket_to_handle sock = MkHandle
 24 |   sock
 25 |   (\(MkSocket _ _ _ _), wanted => do
 26 |     Right output <- recv_n_bytes sock wanted []
 27 |     | Left code => pure1 $ False # ("recv_bytes failed with code " <+> show code # ())
 28 |     pure1 $ True # (output # sock)
 29 |   )
 30 |   (\(MkSocket _ _ _ _), input => do
 31 |     Right _ <- sendBytes sock input
 32 |     | Left code => pure1 $ False # ("send_bytes failed with code " <+> show code # ())
 33 |     pure1 $ True # sock
 34 |   )
 35 |   (\(MkSocket _ _ _ _) => do
 36 |     Socket.close sock
 37 |     pure1 ()
 38 |   )
 39 |