Main.ds

module Main
import Class.Show
import Class.Monad
import Class.Applicative
import Class.Functor
import Data.Numeric.Word8
import Data.Text
import Network.Socket
import System.IO.Console
where

main : Unit -> S (SOCKET + Errno + Console + Error) Unit
main ()
  = case tryEither (box mainSocket ()) of
      Left (ExceptionSystemNetwork errno msg)
       -> do    writel $ "Failed (errno=" % show errno %% "msg=" % show msg % ")"
                writel $ errno_showMessage errno

      Left ex -> throw ex
      Right   -> ()


mainSocket : Unit -> S (SOCKET + Errno + Console) Unit
mainSocket ()
 = do
        sock = networkSocket_socket AF_INET SOCK_STREAM 0
        networkSocket_bind    sock (SockAddrInet 0w16 0w32)
        networkSocket_connect sock (SockAddrInet 1234w16 0w32)
        writel "Connected"

        nbytes
         = mutable r in
           networkSocket_write sock (vectorOfText [r] "Hello World!\n")

        writel $ "Written " % show (truncate# [Nat] nbytes) % " bytes"

        result
         = extend RegionText using mutable r in
           do   readBuf = vectorAlloc# [r] [Word8] 1024
                nBytes  = networkSocket_read sock readBuf
                (readBuf, nBytes)

        writel $ "Read " % show (truncate# [Nat] (snd result)) % " bytes"
        writel $ TextVec (fst result)


---------------------------------------------------

-- | Monadic `bind` with effectful continuation.
bindS (e : Either e a) (k: a -> S eff (Either e b)): S eff (Either e b)
  = case e of
      Left l -> Left l
      Right x -> k x

pureS (x: a): S (SOCKET + Console) (Either e a)
  = weakeff (SOCKET + Console) in Right x