Fix #96, #99, Support socket for Blodwen

Author: mmhelloworld

idris-jvm-core/src/main/idris/IdrisJvm/Core/Foreign.idr

@@ -61,6 +61,7 @@ mutual
   fdescFieldDescriptor (FCon "JVM_Bool") = FieldTyDescBoolean
 
   fdescFieldDescriptor (FCon "JVM_Str") = FieldTyDescReference $ ClassDesc "java/lang/String"
+  fdescFieldDescriptor (FCon "JVM_BigInteger") = FieldTyDescReference $ ClassDesc "java/math/BigInteger"
   fdescFieldDescriptor fdesc = FieldTyDescReference $ fdescRefDescriptor fdesc
 
   fdescRefDescriptor : FDesc -> ReferenceTypeDescriptor
@@ -73,6 +74,7 @@ mutual
   fdescRefDescriptor desc@(FApp "JVM_Nullable" [FApp "Interface" [FStr typeName]]) = NullableRefDesc typeName
 
   fdescRefDescriptor (FCon "JVM_Str") = ClassDesc "java/lang/String"
+  fdescRefDescriptor (FCon "JVM_BigInteger") = ClassDesc "java/math/BigInteger"
   fdescRefDescriptor (FStr exportedType) = IdrisExportDesc exportedType
   fdescRefDescriptor (FCon "JVM_NullableStr") = NullableStrDesc
   fdescRefDescriptor desc = jerror $ "Invalid reference type descriptor: " ++ show desc

idris-jvm-ffi/pom.xml

@@ -54,5 +54,14 @@
                 </executions>
             </plugin>
         </plugins>
+
     </build>
+
+    <dependencies>
+        <dependency>
+            <groupId>io.github.mmhelloworld</groupId>
+            <artifactId>idris-jvm-io</artifactId>
+            <version>1.0-SNAPSHOT</version>
+        </dependency>
+    </dependencies>
 </project>

idris-jvm-ffi/src/main/idris/IdrisJvm/ClientServerSocket.idr

@@ -0,0 +1,34 @@
+module IdrisJvm.ClientServerSocket
+
+import IdrisJvm.IO
+import Java.Nio
+
+%access public export
+
+namespace ClientServerSocket
+  ClientServerSocketClass : JVM_NativeTy
+  ClientServerSocketClass = Class "io/github/mmhelloworld/idrisjvm/io/ClientServerSocket"
+
+  ClientServerSocket : Type
+  ClientServerSocket = JVM_Native ClientServerSocketClass
+
+  listenAndAccept : Int -> JVM_IO (Either Throwable ClientServerSocket)
+  listenAndAccept =
+    invokeStatic ClientServerSocketClass "listenAndAccept" (Int -> JVM_IO (Either Throwable ClientServerSocket))
+
+  getChar : ClientServerSocket -> JVM_IO Char
+  getChar = invokeInstance "getChar" (ClientServerSocket -> JVM_IO Char)
+
+  getLine : ClientServerSocket -> JVM_IO String
+  getLine = invokeInstance "getLine" (ClientServerSocket -> JVM_IO String)
+
+  writeString : ClientServerSocket -> String -> JVM_IO ()
+  writeString = invokeInstance "writeString" (ClientServerSocket -> String -> JVM_IO ())
+
+  close : ClientServerSocket -> JVM_IO ()
+  close = invokeInstance "close" (ClientServerSocket -> JVM_IO ())
+
+  Inherits Channel ClientServerSocket where {}
+  Inherits ReadableByteChannel ClientServerSocket where {}
+  Inherits WritableByteChannel ClientServerSocket where {}
+

idris-jvm-ffi/src/main/idris/IdrisJvm/Data/Buffer.idr

@@ -3,6 +3,8 @@ module IdrisJvm.Data.Buffer
 import IdrisJvm.IO
 import IdrisJvm.File
 import Java.Nio
+import IdrisJvm.FileChannelIo
+import IdrisJvm.ClientServerSocket
 
 %hide Prelude.File.File
 
@@ -121,28 +123,42 @@ export
 getString : Buffer -> (loc : Int) -> (len : Int) -> JVM_IO String
 getString b loc len = invokeInstance "getString" (IdrisBuffer -> Int -> Int -> JVM_IO String) (rawdata b) loc len
 
+export
+readBufferFromReadableByteChannel :
+    Inherits ReadableByteChannel channel => channel -> Buffer -> (maxbytes : Int) -> JVM_IO Buffer
+readBufferFromReadableByteChannel channel buf max = do
+    numread <- invokeInstance "readFromFile" (IdrisBuffer -> ReadableByteChannel -> Int -> Int -> JVM_IO Int)
+                       (rawdata buf) (believe_me channel) (location buf) max
+    pure (record { location $= (+numread) } buf)
+
+export
+writeBufferToWritableByteChannel :
+    Inherits WritableByteChannel channel => channel -> Buffer -> (maxbytes : Int) -> JVM_IO Buffer
+writeBufferToWritableByteChannel channel buf max = do
+    let maxwrite = size buf - location buf
+    let max' = if maxwrite < max then maxwrite else max
+    invokeInstance "writeToFile" (IdrisBuffer -> WritableByteChannel -> Int -> Int -> JVM_IO ())
+            (rawdata buf) (believe_me channel) (location buf) max'
+    pure (record { location $= (+max') } buf)
+
 ||| Read 'maxbytes' into the buffer from a file, returning a new
 ||| buffer with the 'locaton' pointer moved along
 export
 total
 readBufferFromFile : File -> Buffer -> (maxbytes : Int) -> JVM_IO Buffer
-readBufferFromFile (MkFile file path) buf max = do
-    numread <- invokeInstance "readFromFile" (IdrisBuffer -> FileChannel -> Int -> Int -> JVM_IO Int)
-                       (rawdata buf) file (location buf) max
-    pure (record { location $= (+numread) } buf)
+readBufferFromFile (MkFile fileChannelIo) buf max =
+    readBufferFromReadableByteChannel fileChannelIo buf max
+readBufferFromFile (MkFileClientServerSocket clientServerSocket) buf max =
+    readBufferFromReadableByteChannel clientServerSocket buf max
 readBufferFromFile _ buf max = pure buf
 
 ||| Write 'maxbytes' from the buffer from a file, returning a new
 ||| buffer with the 'location' pointer moved along
 export
 total
 writeBufferToFile : File -> Buffer -> (maxbytes : Int) -> JVM_IO Buffer
-writeBufferToFile (MkFile file path) buf max
-    = do let maxwrite = size buf - location buf
-         let max' = if maxwrite < max then maxwrite else max
-         invokeInstance "writeToFile" (IdrisBuffer -> FileChannel -> Int -> Int -> JVM_IO ())
-                 (rawdata buf) file (location buf) max'
-         pure (record { location $= (+max') } buf)
+writeBufferToFile (MkFile channel) buf max = writeBufferToWritableByteChannel channel buf max
+writeBufferToFile (MkFileClientServerSocket channel) buf max = writeBufferToWritableByteChannel channel buf max
 writeBufferToFile _ buf max = pure buf
 
 ||| Return the contents of the buffer as a list

idris-jvm-ffi/src/main/idris/IdrisJvm/FFI.idr

@@ -90,6 +90,7 @@ mutual
       JVM_Str         : JVM_Types String
       JVM_Double      : JVM_Types Double
       JVM_Float       : JVM_Types JFloat
+      JVM_BigInteger  : JVM_Types Integer
       JVM_Unit        : JVM_Types ()
       JVM_NullableStr : JVM_Types (Maybe String)
       JVM_Nullable    : JVM_Types (Maybe (JVM_Native t))
@@ -164,6 +165,8 @@ namespace Object
 Inherits Object String where {}
 Inherits Object (Maybe String) where {}
 
+Inherits Object Integer where {}
+
 Inherits Object (JVM_Native t) where {}
 Inherits Object (Maybe (JVM_Native t)) where {}
 

idris-jvm-ffi/src/main/idris/IdrisJvm/File.idr

@@ -9,29 +9,21 @@ import Java.Nio
 import Java.IO
 import Java.Util
 import Java.Util.Concurrent
-
-%language TypeProviders
-%language ElabReflection
+import IdrisJvm.ClientServerSocket
+import IdrisJvm.FileChannelIo
+import IdrisJvm.Files
+import IdrisJvm.System
 
 %hide Prelude.File.File
 %hide Prelude.File.FileError
 %hide Java.IO.File.File
 
-jdkimport [
-    (stringClass, ["getBytes"]),
-    (pathsClass, ["get"]),
-    (fileChannelClass, ["open"]),
-    (filesClass, ["lines", "write", "readAttributes", "createDirectory"]),
-    (fileTimeClass, ["to"]),
-    (streamClass, ["collect"]),
-    (collectorsClass, ["joining"])
-  ]
-
 public export
 data File = MkFileStdin
           | MkFileStdout
           | MkFileStderr
-          | MkFile FileChannel Path
+          | MkFile FileChannelIo
+          | MkFileClientServerSocket ClientServerSocket
 
 public export
 FileError : Type
@@ -68,14 +60,13 @@ export
 total
 openFile : (f : String) -> (m : Mode) -> JVM_IO (Either FileError File)
 openFile f m = assert_total $ do
-      path <- invokeStatic RuntimeClass "createPath" (String -> JVM_IO Path) f
+      path <- Files.createPath f
       ensureParentDir path
       openOptions <- listToArray (modeToOpenOption m)
-      exceptionOrFile <- (fileChannelClass <.> "open(java/nio/file/Path,Array 1 i java/nio/file/OpenOption)") path openOptions
+      exceptionOrFile <- FileChannelIo.open path openOptions
       case exceptionOrFile of
         Left exception => pure $ Left $ believe_me exception
-        Right Nothing => pure $ Left . believe_me $ !(unableToOpenFile f)
-        Right (Just file) => pure $ Right (MkFile file path)
+        Right file => pure $ Right (MkFile file)
    where
      hasWriteMode : Bool
      hasWriteMode = case m of
@@ -91,54 +82,75 @@ openFile f m = assert_total $ do
          case optParent of
             Nothing => pure ()
             Just pathDir => do
-              _ <- invokeStatic FilesClass "createDirectories" (Path -> JVM_Array FileAttribute -> JVM_IO Path) pathDir
-                     !(newArray FileAttribute 0)
+              Files.createDirectories pathDir
               pure ()
        else pure ()
+export
+getChar : File -> JVM_IO Char
+getChar (MkFile fileChannelIo) = getChar fileChannelIo
+getChar (MkFileClientServerSocket clientServerSocket) = getChar clientServerSocket
+getChar MkFileStdin = IO.getChar
+getChar _ = do
+    putStrLn "Unable to read a character"
+    exit 1
+
+export
+getLine : File -> JVM_IO String
+getLine (MkFile fileChannelIo) = getLine fileChannelIo
+getLine (MkFileClientServerSocket clientServerSocket) = ClientServerSocket.getLine clientServerSocket
+getLine MkFileStdin = IO.getLine
+getLine _ = do
+    putStrLn "Unable to read a line"
+    exit 1
+
+export
+writeString : File -> String -> JVM_IO ()
+writeString (MkFile fileChannelIo) str = writeString fileChannelIo str
+writeString (MkFileClientServerSocket socket) str = writeString socket str
+writeString MkFileStdout str = print str
+writeString _ _ = pure ()
 
 export
 closeFile : File -> JVM_IO ()
-closeFile (MkFile file _) = Channel.close file
+closeFile (MkFile file) = FileChannelIo.close file
+closeFile (MkFileClientServerSocket clientServerSocket) = ClientServerSocket.close clientServerSocket
 closeFile _ = pure ()
 
 export
 changeDir : String -> JVM_IO Bool
-changeDir = invokeStatic RuntimeClass "changeDir" (String -> JVM_IO Bool)
+changeDir = Files.changeDir
 
 export
 getTemporaryFileName : JVM_IO String
-getTemporaryFileName = invokeStatic RuntimeClass "getTemporaryFileName" (JVM_IO String)
+getTemporaryFileName = Files.getTemporaryFileName
 
 export
 chmod : String -> Int -> JVM_IO ()
-chmod f m = invokeStatic RuntimeClass "chmod" (String -> Int -> JVM_IO ()) f m
+chmod = Files.chmod
 
 export
 total
 createDir : String -> JVM_IO (Either FileError ())
-createDir d = assert_total $ do
-  path <- invokeStatic RuntimeClass "createPath" (String -> JVM_IO Path) d
-  exceptionOrPath <- (filesClass <.> "createDirectory") path !(newArray FileAttribute 0)
-  pure $ const () <$> exceptionOrPath
+createDir d = assert_total $ Files.createDirectory d
 
 export
 currentDir : JVM_IO String
-currentDir = invokeStatic RuntimeClass "getWorkingDir" (JVM_IO String)
+currentDir = Files.getWorkingDir
 
 -- This is returning Int to conform to Idris fileSize function type
 -- even though Java's FileChannel returns long
 export
 fileSize : File -> JVM_IO (Either FileError Int)
-fileSize (MkFile f _) = do
-  exceptionOrSize <- invokeInstance "size" (FileChannel -> JVM_IO (JVM_Throwable Bits64)) f
+fileSize (MkFile f) = do
+  exceptionOrSize <- FileChannelIo.size f
   case exceptionOrSize of
     Left exception => pure $ Left $ believe_me exception
     Right size => pure $ Right $ Long.intValue size
-fileSize _ = pure . Left . believe_me $ !(IOException.new "Cannot determine size for stdin/stdout/stderr")
+fileSize _ = pure . Left . believe_me $ !(IOException.new "Cannot determine size")
 
 export
 fflush : File -> JVM_IO ()
-fflush (MkFile file _) = invokeInstance "force" (FileChannel -> Bool -> JVM_IO ()) file True
+fflush (MkFile file) = FileChannelIo.flush file
 fflush MkFileStdout = invokeStatic RuntimeClass "flushStdout" (JVM_IO ())
 fflush MkFileStderr = invokeStatic RuntimeClass "flushStderr" (JVM_IO ())
 fflush _ = pure ()
@@ -161,61 +173,38 @@ stderr = MkFileStderr
 export
 total
 readFile : String -> JVM_IO (Either FileError String)
-readFile pathStr = assert_total $ do
-    path <- invokeStatic RuntimeClass "createPath" (String -> JVM_IO Path) pathStr
-    exceptionOrlines <- (filesClass <.> "lines(java/nio/file/Path)") path
-    case exceptionOrlines of
-      Left exception => pure $ Left exception
-      Right Nothing => pure $ Left . believe_me $ !(unableToReadFile pathStr)
-      Right (Just lines) => do
-        joiningCollector <- (collectorsClass <.!> "joining(java/lang/CharSequence)") $ believe_me !(lineSeparator)
-        pure . Right $ believe_me !((streamClass <.!> "collect(java/util/stream/Collector)") lines joiningCollector)
+readFile pathStr = assert_total $ Files.readFile pathStr
 
 export
 writeFile : String -> String -> JVM_IO (Either FileError ())
-writeFile file content = do
-  path <- invokeStatic RuntimeClass "createPath" (String -> JVM_IO Path) file
-  bytes <- (stringClass <.!> "getBytes(java/lang/String)") content "UTF-8"
-  exceptionOrPath <- (filesClass <.> "write(java/nio/file/Path,Array 1 byte,Array 1 i java/nio/file/OpenOption)") path
-            bytes !(newArray OpenOption 0)
-  pure $ either (const . Left . believe_me $ !(unableToWriteFile file)) (const $ Right ()) exceptionOrPath
+writeFile file content = Files.writeFile file content
 
 export
 fileModifiedTime : File -> JVM_IO (Either FileError Integer)
-fileModifiedTime (MkFile _ path) = do
-    attrs <- (filesClass <.!> "readAttributes(java/nio/file/Path,java/lang/Class,Array 1 java/nio/file/LinkOption)")
-               path (classLit basicFileAttributesClass) !(newArray LinkOption 0)
-    fileTime <- invokeInstance "lastModifiedTime" (BasicFileAttributes -> JVM_IO FileTime) attrs
-    seconds <- (fileTimeClass <.!> "to") fileTime TimeUnit.seconds
-    pure . Right $ believe_me $ BigInteger.valueOf seconds
-fileModifiedTime _ = pure . Left $ believe_me !(IOException.new "Cannot get file modified time for stdin, stdout or stderr")
+fileModifiedTime (MkFile file) = FileChannelIo.getFileModifiedTime file
+fileModifiedTime _ = pure . Left $ believe_me !(IOException.new "Cannot get file modified time")
 
 export
 fileAccessTime : File -> JVM_IO (Either FileError Integer)
-fileAccessTime (MkFile _ path) = do
-    attrs <- (filesClass <.!> "readAttributes(java/nio/file/Path,java/lang/Class,Array 1 java/nio/file/LinkOption)")
-                path (classLit basicFileAttributesClass) !(newArray LinkOption 0)
-    fileTime <- invokeInstance "lastAccessTime" (BasicFileAttributes -> JVM_IO FileTime) attrs
-    seconds <- (fileTimeClass <.!> "to") fileTime TimeUnit.seconds
-    pure . Right $ believe_me $ BigInteger.valueOf seconds
-fileAccessTime _ = pure . Left $ believe_me !(IOException.new "Cannot get file access time for stdin, stdout or stderr")
+fileAccessTime (MkFile file) = FileChannelIo.getFileAccessTime file
+fileAccessTime _ = pure . Left $ believe_me !(IOException.new "Cannot get file access time")
 
 export
 fileStatusTime : File -> JVM_IO (Either FileError Integer)
-fileStatusTime (MkFile _ path) = do
-    attrs <- (filesClass <.!> "readAttributes(java/nio/file/Path,java/lang/Class,Array 1 java/nio/file/LinkOption)")
-               path (classLit basicFileAttributesClass) !(newArray LinkOption 0)
-    fileTime <- invokeInstance "creationTime" (BasicFileAttributes -> JVM_IO FileTime) attrs
-    seconds <- (fileTimeClass <.!> "to") fileTime TimeUnit.seconds
-    pure . Right $ believe_me $ BigInteger.valueOf seconds
-fileStatusTime _ = pure . Left $ believe_me !(IOException.new "Cannot get file status time for stdin, stdout or stderr")
+fileStatusTime (MkFile file) = FileChannelIo.getFileStatusTime file
+fileStatusTime _ = pure . Left $ believe_me !(IOException.new "Cannot get file status time")
 
 ||| Check if a file handle has reached the end
 export
 fEOF : File -> JVM_IO Bool
-fEOF (MkFile file _) = do
-  position <- invokeInstance "position" (FileChannel -> JVM_IO Bits64) file
-  size <- invokeInstance "size" (FileChannel -> JVM_IO Bits64) file
-  pure (position == size)
+fEOF (MkFile file) = FileChannelIo.isEof file
 fEOF MkFileStdin = invokeStatic RuntimeClass "isStdinEof" (JVM_IO Bool)
 fEOF _ = pure False
+
+export
+socketListenAndAccept : Int -> JVM_IO (Either String File)
+socketListenAndAccept port = do
+    byteBufferIoOrError <- ClientServerSocket.listenAndAccept port
+    case byteBufferIoOrError of
+        Left throwable => Left <$> Objects.toString throwable
+        Right byteBufferIo => pure . Right $ MkFileClientServerSocket byteBufferIo