Skip to content

Commit

Permalink
Support network primitives
Browse files Browse the repository at this point in the history
  • Loading branch information
@mmhelloworld
mmhelloworld committed Jan 3, 2021
1 parent c990524 commit 22c7005
Show file tree
Hide file tree
Showing 29 changed files with 931 additions and 518 deletions.
4 changes: 1 addition & 3 deletions Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ idris2: src/YafflePaths.idr check_version
idris2c: dist/idris2.c
${MAKE} -C dist

src/YafflePaths.idr: FORCE
src/YafflePaths.idr:
echo 'module YafflePaths; import IdrisJvm.IO; import Java.Lang; export yversion : ((Nat,Nat,Nat), String); yversion = ((${MAJOR},${MINOR},${PATCH}), "${GIT_SHA1}")' > src/YafflePaths.idr
echo 'export yprefix : String' >> src/YafflePaths.idr
echo 'yprefix = home ++ "/.idris2boot" where' >> src/YafflePaths.idr
Expand All @@ -84,8 +84,6 @@ src/YafflePaths.idr: FORCE
echo ' idrisHomeEnv <- System.getenv "IDRIS2_BOOT_HOME"' >> src/YafflePaths.idr
echo ' maybe (System.getPropertyWithDefault "user.home" "") pure idrisHomeEnv' >> src/YafflePaths.idr

FORCE:

prelude:
${MAKE} -C libs/prelude IDRIS2=../../idris2boot

Expand Down
23 changes: 2 additions & 21 deletions compiler/pom.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,8 @@
<properties>
<maven.compiler.source>8</maven.compiler.source>
<maven.compiler.target>8</maven.compiler.target>
<idris.tests></idris.tests>
<skipIdrisCompile>false</skipIdrisCompile>
<skipTests>false</skipTests>
<skipIdrisInstallLibrary>false</skipIdrisInstallLibrary>
</properties>

<build>
Expand All @@ -40,7 +39,6 @@
<argument>idris2</argument>
</arguments>
<environmentVariables>
<PREFIX>${project.build.directory}</PREFIX>
<IDRIS2_BOOT_HOME>${project.build.directory}</IDRIS2_BOOT_HOME>
</environmentVariables>
</configuration>
Expand All @@ -52,34 +50,17 @@
<goal>exec</goal>
</goals>
<configuration>
<skip>${skipIdrisCompile}</skip>
<skip>${skipIdrisInstallLibrary}</skip>
<executable>make</executable>
<workingDirectory>${project.parent.basedir}</workingDirectory>
<arguments>
<argument>install-libs</argument>
</arguments>
<environmentVariables>
<PREFIX>${project.build.directory}</PREFIX>
<IDRIS2_BOOT_HOME>${project.build.directory}</IDRIS2_BOOT_HOME>
</environmentVariables>
</configuration>
</execution>
<execution>
<id>idris-test</id>
<phase>test</phase>
<goals>
<goal>exec</goal>
</goals>
<configuration>
<skip>${skipTests}</skip>
<executable>make</executable>
<workingDirectory>${project.parent.basedir}</workingDirectory>
<arguments>
<argument>test</argument>
<argument>${idris.tests}</argument>
</arguments>
</configuration>
</execution>
<execution>
<id>idris-clean</id>
<phase>clean</phase>
Expand Down
34 changes: 31 additions & 3 deletions jvm-assembler/pom.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,11 @@
<artifactId>jvm-assembler</artifactId>
<name>Idris 2 JVM Bootstrap Assembler</name>

<properties>
<idris.tests></idris.tests>
<skipTests>false</skipTests>
</properties>

<build>
<plugins>
<plugin>
Expand All @@ -24,11 +29,13 @@
<goal>copy-resources</goal>
</goals>
<configuration>
<outputDirectory>${project.build.directory}/idris2-boot-jvm/.idris2boot/idris2-0.1.1</outputDirectory>
<outputDirectory>${project.build.directory}/idris2-boot-jvm/.idris2boot/idris2-0.1.1
</outputDirectory>
<overwrite>true</overwrite>
<resources>
<resource>
<directory>${user.home}/.idris2boot/idris2-0.1.1</directory>
<directory>${project.parent.basedir}/compiler/target/.idris2boot/idris2-0.1.1
</directory>
</resource>
</resources>
</configuration>
Expand Down Expand Up @@ -59,7 +66,6 @@
</execution>
</executions>
</plugin>

<plugin>
<artifactId>maven-assembly-plugin</artifactId>
<configuration>
Expand All @@ -78,6 +84,28 @@
</execution>
</executions>
</plugin>
<plugin>
<groupId>org.codehaus.mojo</groupId>
<artifactId>exec-maven-plugin</artifactId>
<executions>
<execution>
<id>idris-test</id>
<phase>integration-test</phase>
<goals>
<goal>exec</goal>
</goals>
<configuration>
<skip>${skipTests}</skip>
<executable>make</executable>
<workingDirectory>${project.parent.basedir}</workingDirectory>
<arguments>
<argument>test</argument>
<argument>${idris.tests}</argument>
</arguments>
</configuration>
</execution>
</executions>
</plugin>
</plugins>
</build>

Expand Down
14 changes: 7 additions & 7 deletions libs/base/System/File.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,16 +35,16 @@ prim_error : FilePtr -> PrimIO Int
prim_fileErrno : PrimIO Int

%foreign support "idris2_readLine"
jvm' fileClass "getLine" fileClass "String"
jvm' fileClass "readLine" fileClass "String"
prim__readLine : FilePtr -> PrimIO (Ptr String)
%foreign support "idris2_readChars"
jvm' fileClass "getChars" ("int " ++ fileClass) "String"
jvm' fileClass "readChars" ("int " ++ fileClass) "String"
prim__readChars : Int -> FilePtr -> PrimIO (Ptr String)
%foreign support "fgetc"
jvm' fileClass "getChar" fileClass "char"
jvm' fileClass "readChar" fileClass "char"
prim__readChar : FilePtr -> PrimIO Char
%foreign support "idris2_writeLine"
jvm' fileClass "writeString" (fileClass ++ " String") "int"
jvm' fileClass "writeLine" (fileClass ++ " String") "int"
prim__writeLine : FilePtr -> String -> PrimIO Int
%foreign support "idris2_eof"
jvm' fileClass "isEof" fileClass "int"
Expand All @@ -63,13 +63,13 @@ prim__fileSize : FilePtr -> PrimIO Int
prim__fPoll : FilePtr -> PrimIO Int

%foreign support "idris2_fileAccessTime"
jvm' fileClass "getFileAccessTime" fileClass "int"
jvm' fileClass "getAccessTime" fileClass "int"
prim__fileAccessTime : FilePtr -> PrimIO Int
%foreign support "idris2_fileModifiedTime"
jvm' fileClass "getFileModifiedTime" fileClass "int"
jvm' fileClass "getModifiedTime" fileClass "int"
prim__fileModifiedTime : FilePtr -> PrimIO Int
%foreign support "idris2_fileStatusTime"
jvm' fileClass "getFileStatusTime" fileClass "int"
jvm' fileClass "getStatusTime" fileClass "int"
prim__fileStatusTime : FilePtr -> PrimIO Int

%foreign support "idris2_stdin"
Expand Down
100 changes: 65 additions & 35 deletions libs/network/Network/Socket.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,42 @@ module Network.Socket
import public Network.Socket.Data
import Network.Socket.Raw
import Data.List
import System.FFI

idrisSocketClass : String
idrisSocketClass = "io/github/mmhelloworld/idris2boot/runtime/IdrisSocket"

-- ----------------------------------------------------- [ Network Socket API. ]
%foreign
jvm' idrisSocketClass "create" "int int int" idrisSocketClass
prim_createSocket : Int -> Int -> Int -> PrimIO SocketDescriptor

%foreign
jvm' idrisSocketClass ".close" idrisSocketClass "void"
prim_closeSocket : AnyPtr -> PrimIO ()

%foreign
jvm' idrisSocketClass ".bind"
"io/github/mmhelloworld/idris2boot/runtime/IdrisSocket int int java/lang/String int" "int"
prim_bindSocket : AnyPtr -> Int -> Int -> String -> Int -> PrimIO Int

%foreign
jvm' idrisSocketClass ".connect"
"io/github/mmhelloworld/idris2boot/runtime/IdrisSocket int int java/lang/String int" "int"
prim_connectSocket : AnyPtr -> Int -> Int -> String -> Int -> PrimIO Int

%foreign
jvm' idrisSocketClass ".listen" "io/github/mmhelloworld/idris2boot/runtime/IdrisSocket int" "int"
prim_listenSocket : AnyPtr -> Int -> PrimIO Int

%foreign
jvm' idrisSocketClass ".accept"
"io/github/mmhelloworld/idris2boot/runtime/IdrisSocket java/lang/Object" idrisSocketClass
prim_acceptSocket : AnyPtr -> AnyPtr -> PrimIO SocketDescriptor

%foreign
jvm idrisSocketClass "createSocketAddress"
prim_createSocketAddress : PrimIO AnyPtr

||| Creates a UNIX socket with the given family, socket type and protocol
||| number. Returns either a socket or an error.
Expand All @@ -18,16 +52,16 @@ socket : (fam : SocketFamily)
-> (pnum : ProtocolNumber)
-> IO (Either SocketError Socket)
socket sf st pn = do
socket_res <- cCall Int "idrnet_socket" [toCode sf, toCode st, pn]

if socket_res == -1
then map Left getErrno
socket_res <- primIO $ prim_createSocket (toCode sf) (toCode st) pn
errorNumber <- getErrno
if errorNumber /= 0
then pure $ Left errorNumber
else pure $ Right (MkSocket socket_res sf st pn)

||| Close a socket
export
close : Socket -> IO ()
close sock = cCall () "close" [descriptor sock]
close sock = primIO $ prim_closeSocket (descriptor sock)

||| Binds a socket to the given socket address and port.
||| Returns 0 on success, an error code otherwise.
Expand All @@ -37,10 +71,8 @@ bind : (sock : Socket)
-> (port : Port)
-> IO Int
bind sock addr port = do
bind_res <- cCall Int "idrnet_bind"
[ descriptor sock, toCode $ family sock
, toCode $ socketType sock, saString addr, port
]
bind_res <- primIO $ prim_bindSocket (descriptor sock) (toCode $ family sock) (toCode $ socketType sock)
(saString addr) port
if bind_res == (-1)
then getErrno
else pure 0
Expand All @@ -57,9 +89,8 @@ connect : (sock : Socket)
-> (port : Port)
-> IO ResultCode
connect sock addr port = do
conn_res <- cCall Int "idrnet_connect"
[ descriptor sock, toCode $ family sock, toCode $ socketType sock, show addr, port]

conn_res <- primIO $ prim_connectSocket (descriptor sock) (toCode $ family sock) (toCode $ socketType sock)
(show addr) port
if conn_res == (-1)
then getErrno
else pure 0
Expand All @@ -70,7 +101,7 @@ connect sock addr port = do
export
listen : (sock : Socket) -> IO Int
listen sock = do
listen_res <- cCall Int "listen" [ descriptor sock, BACKLOG ]
listen_res <- primIO $ prim_listenSocket (descriptor sock) BACKLOG
if listen_res == (-1)
then getErrno
else pure 0
Expand All @@ -91,17 +122,23 @@ accept sock = do
-- We need a pointer to a sockaddr structure. This is then passed into
-- idrnet_accept and populated. We can then query it for the SocketAddr and free it.

sockaddr_ptr <- cCall AnyPtr "idrnet_create_sockaddr" []
sockaddr_ptr <- primIO prim_createSocketAddress

accept_res <- cCall Int "idrnet_accept" [ descriptor sock, sockaddr_ptr ]
if accept_res == (-1)
then map Left getErrno
accept_res <- primIO $ prim_acceptSocket (descriptor sock) sockaddr_ptr
errorNumber <- getErrno
if errorNumber /= 0
then pure $ Left errorNumber
else do
let (MkSocket _ fam ty p_num) = sock
sockaddr <- getSockAddr (SAPtr sockaddr_ptr)
sockaddr_free (SAPtr sockaddr_ptr)
pure $ Right ((MkSocket accept_res fam ty p_num), sockaddr)

%foreign
jvm' idrisSocketClass ".send"
"io/github/mmhelloworld/idris2boot/runtime/IdrisSocket java/lang/String" "int"
prim_sendSocket : SocketDescriptor -> String -> PrimIO Int

||| Send data on the specified socket.
|||
||| Returns on failure a `SocketError`.
Expand All @@ -114,12 +151,17 @@ send : (sock : Socket)
-> (msg : String)
-> IO (Either SocketError ResultCode)
send sock dat = do
send_res <- cCall Int "idrnet_send" [ descriptor sock, dat ]
send_res <- primIO $ prim_sendSocket (descriptor sock) dat

if send_res == (-1)
then map Left getErrno
else pure $ Right send_res

%foreign
jvm' idrisSocketClass ".receive"
"io/github/mmhelloworld/idris2boot/runtime/IdrisSocket int" "java/lang/String"
prim_receiveSocket : SocketDescriptor -> Int -> PrimIO String

||| Receive data on the specified socket.
|||
||| Returns on failure a `SocketError`
Expand All @@ -136,23 +178,11 @@ recv : (sock : Socket)
recv sock len = do
-- Firstly make the request, get some kind of recv structure which
-- contains the result of the recv and possibly the retrieved payload
recv_struct_ptr <- cCall AnyPtr "idrnet_recv" [ descriptor sock, len]
recv_res <- cCall Int "idrnet_get_recv_res" [ recv_struct_ptr ]

if recv_res == (-1)
then do
errno <- getErrno
freeRecvStruct (RSPtr recv_struct_ptr)
pure $ Left errno
else
if recv_res == 0
then do
freeRecvStruct (RSPtr recv_struct_ptr)
pure $ Left 0
else do
payload <- cCall String "idrnet_get_recv_payload" [ recv_struct_ptr ]
freeRecvStruct (RSPtr recv_struct_ptr)
pure $ Right (payload, recv_res)
payload <- primIO $ prim_receiveSocket (descriptor sock) len
errorNumber <- getErrno
if errorNumber /= 0
then pure $ Left errorNumber
else pure $ Right (payload, len)

||| Receive all the remaining data on the specified socket.
|||
Expand Down
15 changes: 8 additions & 7 deletions libs/network/Network/Socket/Data.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ module Network.Socket.Data
import Data.List
import Data.List1
import Data.Strings
import System.FFI

-- ------------------------------------------------------------ [ Type Aliases ]

Expand Down Expand Up @@ -36,7 +37,7 @@ SocketError = Int
||| SocketDescriptor: Native C Socket Descriptor
public export
SocketDescriptor : Type
SocketDescriptor = Int
SocketDescriptor = AnyPtr

public export
Port : Type
Expand All @@ -51,20 +52,20 @@ BACKLOG = 20

export
EAGAIN : Int
EAGAIN =
-- I'm sorry
-- maybe
unsafePerformIO $ cCall Int "idrnet_geteagain" []
EAGAIN = 11

-- ---------------------------------------------------------------- [ Error Code ]
%foreign
jvm runtimeClass "getErrorNumber"
prim_getSocketErrorNumber : PrimIO Int

export
getErrno : IO SocketError
getErrno = cCall Int "idrnet_errno" []
getErrno = primIO prim_getSocketErrorNumber

export
nullPtr : AnyPtr -> IO Bool
nullPtr p = cCall Bool "isNull" [p]
nullPtr p = pure $ prim__nullAnyPtr p /= 0

-- -------------------------------------------------------------- [ Interfaces ]

Expand Down
Loading

0 comments on commit 22c7005

Please sign in to comment.