Fix for anonymous class definition and update to Idris 0.9.20

.gitignore

@@ -0,0 +1 @@
+*.ibc

Dockerfile

@@ -0,0 +1,9 @@
+FROM aaroncr/idris-dev
+ADD . idris-java
+WORKDIR idris-java
+RUN cabal install
+WORKDIR libs
+RUN idris --install idrisjava.ipkg
+WORKDIR ../..
+
+

libs/IdrisJava.idr

@@ -1,6 +1,6 @@
 module IdrisJava
 
-%access public
+%access public export
 
 namespace FFI_Java
 
@@ -13,31 +13,35 @@ namespace FFI_Java
     ||| a foreign array type
     JavaTyArr JavaTy
 
-  instance Eq JavaTy where
+  Eq JavaTy where
     (JavaTyRef ns t) == (JavaTyRef ns' t') = ns == ns' && t == t'
     (JavaTyVal ns t) == (JavaTyVal ns' t') = ns == ns' && t == t'
     _                == _                  = False
 
-  ||| A foreign descriptor.
-  data JavaForeign =
-    ||| Read the named static field of the given foreign type.
-    JavaReadField String |
-    ||| With the named field of the given foreign type.
-    JavaWriteField String |
-    ||| Call the static method of the given foreign type.
-    JavaInvoke String |
-    ||| Call the named method of the given foreign type.
-    JavaInvokeDyn String |
-    ||| Call a constructor
-    JavaNew |
-    ||| Allocate a anonymous class
-    JavaNewAnonymous String |
-    ||| Export a function under the given name.    
-    JavaExport String |
-    ||| Export a function under its original name.
-    JavaDefault   
-
   mutual
+    ||| A foreign descriptor.
+    data JavaForeign =
+        ||| Read the named static field of the given foreign type.
+        JavaReadField String |
+        ||| With the named field of the given foreign type.
+        JavaWriteField String |
+        ||| Call the static method of the given foreign type.
+        JavaInvoke String |
+        ||| Call the named method of the given foreign type.
+        JavaInvokeDyn String |
+        ||| Call a constructor
+        JavaNew |
+        ||| Allocate a anonymous class
+        JavaNewAnonymous String |
+        ||| Check whether the value is an instance of the given foreign type
+        JavaInstanceOf (Java_Types t) |
+        ||| Generate a try-catch block
+        JavaTryCatch |
+        ||| Export a function under the given name.    
+        JavaExport String |
+        ||| Export a function under its original name.
+        JavaDefault   
+
     data JavaFn : Type -> Type where
        -- code generated can assume it's compiled just as 't'
        MkJavaFn : (x : t) -> JavaFn t
@@ -53,6 +57,7 @@ namespace FFI_Java
        Java_IntBits16 : Java_IntTypes Bits16
        Java_IntBits32 : Java_IntTypes Bits32
        Java_IntBits64 : Java_IntTypes Bits64
+       Java_IntBigInt : Java_IntTypes Integer
 
     data Java_FnTypes : Type -> Type where
        Java_Fn     : Java_Types s -> Java_FnTypes t -> Java_FnTypes (s -> t)
@@ -62,7 +67,7 @@ namespace FFI_Java
     ||| Supported Java foreign types
     data Java_Types : Type -> Type where
        Java_Str   : Java_Types String
-       Java_Float : Java_Types Float
+       Java_Float : Java_Types Double
        Java_Ptr   : Java_Types Ptr
        Java_Unit  : Java_Types ()
        Java_JavaT : Java_Types (Java a)
@@ -110,4 +115,35 @@ new ty = foreign FFI_Java JavaNew ty
 newanonymous : String -> (ty : Type) -> {auto fty : FTy FFI_Java [] ty} -> ty
 newanonymous name ty = foreign FFI_Java (JavaNewAnonymous name) ty
 
-class IsA a b where {}
+interface IsA a b where {}
+
+JavaBoolean : Type
+JavaBoolean = Java (JavaTyRef "java.lang" "Boolean")
+
+boolToJavaBoolean : Bool -> JAVA_IO JavaBoolean
+boolToJavaBoolean False = invoke "longToBool" (Int -> JAVA_IO JavaBoolean) 0
+boolToJavaBoolean True = invoke "longToBool" (Int -> JAVA_IO JavaBoolean) 1
+
+javaBooleanToBool : JavaBoolean -> JAVA_IO Bool
+javaBooleanToBool b = do
+  i <- invoke "boolToLong" (JavaBoolean -> JAVA_IO Int) b
+  return (if i <=0 then False else True)
+
+isNull : Ptr -> JAVA_IO Bool  
+isNull x = do javaBooleanToBool !(invoke "isNull" (Ptr -> JAVA_IO JavaBoolean) x)
+
+
+-- %inline
+-- instanceof :
+--   (x:t) -> {auto fty : FTy FFI_Java [] (t -> JAVA_IO JavaBoolean)} -> 
+--   (jty : Java_Types j) -> JAVA_IO Bool
+-- instanceof {t} x jty = do
+--  jbool <- foreign FFI_Java (JavaInstanceOf jty) (t -> JAVA_IO JavaBoolean) x
+
+
+-- %inline
+-- trycatch : {a:Type} -> {ex:Type} -> JAVA_IO a -> (ex -> JAVA_IO a) -> JAVA_IO a
+-- trycatch tryBlock catchBlock =
+--   foreign FFI_Java JavaTryCatch
+--     (JAVA_IO a -> (ex -> JAVA_IO a) -> JAVA_IO a)
+--     tryBlock catchBlock

libs/IdrisJava/File.idr

@@ -1,16 +1,16 @@
-{- 
+{-
   Port of the FFI_C/IO functions found in Idris' Prelude.File to
   FFI_Java/JAVA_IO.
--} 
+-}
 module IdrisJava.File
 
 import IdrisJava
 import IdrisJava.Strings
 
-%access public
+%access export
 
 ||| A file handle
-abstract
+export
 data JFile = FHandle Ptr
 
 ||| Standard input
@@ -63,6 +63,9 @@ closeFile (FHandle h) = do_fclose h
 
 -- do_fread is already lifted to IO' l String
 
+do_fread : Ptr -> IO' l String
+do_fread h = prim_fread h
+
 fgetc : JFile -> JAVA_IO Char
 fgetc (FHandle h) = return (cast !(invoke "fgetc" (Ptr -> JAVA_IO Int) h))
 
@@ -97,10 +100,10 @@ partial
 do_fwrite : Ptr -> String -> JAVA_IO ()
 do_fwrite h s = do prim_fwrite h s
                    return ()
-                   
+
 partial
 fwrite : JFile -> String -> JAVA_IO ()
-fwrite (FHandle h) s = do_fwrite h s                 
+fwrite (FHandle h) s = do_fwrite h s
 
 partial
 do_feof : Ptr -> JAVA_IO Int
@@ -144,6 +147,6 @@ readFile fn = do h <- openFile fn Read
 partial -- no error checking!
 writeFile : String -> String -> JAVA_IO ()
 writeFile fn str = do
-  h <- openFile fn Write
+  h <- openFile fn WriteTruncate
   IdrisJava.File.fwrite h str
   closeFile h

libs/IdrisJava/Interactive.idr

@@ -12,7 +12,7 @@ putChar c = invoke "putchar" (Int -> JAVA_IO ()) (cast c)
 
 ||| Write a singel character to stdout, with a trailing newline
 putCharLn : Char -> JAVA_IO ()
-putCharLn c = putStrLn (singleton c)
+putCharLn c = putStrLn' (singleton c)
 
 ||| Read a single character from stdin
 getChar : JAVA_IO Char