#104 Support Idris 2

Author: mmhelloworld

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

@@ -146,6 +146,9 @@ interface Inherits a b where {}
 
 Inherits (JVM_Native t) (JVM_Native t) where {}
 
+IdrisObject : Type
+IdrisObject = javaClass "io/github/mmhelloworld/idrisjvm/runtime/IdrisObject"
+
 namespace Object
   ObjectClass : JVM_NativeTy
   ObjectClass = Class "java/lang/Object"

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

@@ -33,6 +33,10 @@ export
 FileReadError : FileError
 FileReadError = believe_me $ unsafePerformIO $ IOException.new "File Read Error"
 
+export
+GenericFileError : Int -> FileError
+GenericFileError errNo = believe_me $ unsafePerformIO $ IOException.new $ "Generic File Error " ++ show errNo
+
 export
 unableToOpenFile : String -> JVM_IO IOException
 unableToOpenFile fileName = IOException.new ("Unable to open file: " ++ fileName)
@@ -208,3 +212,9 @@ socketListenAndAccept port = do
     case byteBufferIoOrError of
         Left throwable => Left <$> Objects.toString throwable
         Right byteBufferIo => pure . Right $ MkFileClientServerSocket byteBufferIo
+
+export
+fRemove : (s : String) -> JVM_IO Bool
+fRemove f = do
+    path <- Files.createPath f
+    deleteIfExists path

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

@@ -39,3 +39,6 @@ namespace Files
   createPath : String -> JVM_IO Path
   createPath = invokeStatic FilesClass "createPath" (String -> JVM_IO Path)
 
+  deleteIfExists : Path -> JVM_IO Bool
+  deleteIfExists = invokeStatic FilesClass "deleteIfExists" (Path -> JVM_IO Bool)
+

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

@@ -6,28 +6,58 @@ import Java.Util
 import Java.Math
 import Java.Lang
 
-public export
+%access public export
+
 getArgs : JVM_IO (List String)
 getArgs = do
     argsList <- invokeStatic RuntimeClass "getProgramArgs" (JVM_IO JList)
     Iterator.toList !(JList.iterator argsList)
 
-public export
 time : JVM_IO Integer
 time = believe_me <$> invokeStatic RuntimeClass "time" (JVM_IO BigInteger)
 
-public export
 getEnv : String -> JVM_IO (Maybe String)
 getEnv = System.getenv
 
-public export
 system : String -> JVM_IO Int
 system = invokeStatic RuntimeClass "runCommand" (String -> JVM_IO Int)
 
-public export
 usleep : (i : Int) -> { auto prf : So (i >= 0 && i <= 1000000) } -> JVM_IO ()
 usleep interval = invokeStatic RuntimeClass "usleep" (Int -> JVM_IO ()) interval
 
-public export
 exit : Int -> JVM_IO a
 exit = believe_me . Java.Lang.System.exit
+
+||| Programs can either terminate successfully, or end in a caught
+||| failure.
+data ExitCode : Type where
+  ||| Terminate successfully.
+  ExitSuccess : ExitCode
+  ||| Program terminated for some prescribed reason.
+  |||
+  ||| @errNo A non-zero numerical value indicating failure.
+  ||| @prf   Proof that the int value is non-zero.
+  ExitFailure : (errNo    : Int)
+             -> {auto prf : So (not $ errNo == 0)}
+             -> ExitCode
+
+||| Terminate the program with an `ExitCode`. This code indicates the
+||| success of the program's execution, and returns the success code
+||| to the program's caller.
+|||
+||| @code The `ExitCode` for program.
+exitWith : (code : ExitCode) -> JVM_IO a
+exitWith ExitSuccess         = exit 0
+exitWith (ExitFailure errNo) = exit errNo
+
+||| Wall clock time
+record Clock where
+  constructor MkClock
+  seconds : Integer
+  nanoseconds : Integer
+
+||| Get the system's wall clock time.
+clockTime : JVM_IO Clock
+clockTime =
+  believe_me <$> invokeStatic (Class "io/github/mmhelloworld/idrisjvm/runtime/IdrisSystem")
+    "getIdrisClock" (JVM_IO IdrisObject)

idris-jvm-ffi/src/main/idris/Java/Lang.idr

@@ -270,7 +270,7 @@ vectToArray {elemTy} xs
 %inline
 listToArray : List elemTy -> {auto jvmType: JVM_Types elemTy} -> JVM_IO (JVM_Array elemTy)
 listToArray {elemTy} xs
-    = listToArray' xs
+    = assert_total $ listToArray' xs
         (newArray elemTy (length xs))
         (setArray (JVM_Array elemTy -> Int -> elemTy -> JVM_IO ()))
   where

idris-jvm-integration-test/pom.xml

@@ -86,6 +86,13 @@
             <artifactId>junit</artifactId>
             <scope>test</scope>
         </dependency>
+
+        <dependency>
+            <groupId>org.assertj</groupId>
+            <artifactId>assertj-core</artifactId>
+            <scope>test</scope>
+        </dependency>
+
     </dependencies>
 
 </project>

idris-jvm-integration-test/src/test/java/idrisjvm/integrationtest/IdrisJvmTest.java

@@ -33,14 +33,13 @@
 import static java.util.Objects.requireNonNull;
 import static java.util.concurrent.TimeUnit.MINUTES;
 import static java.util.stream.Collectors.toList;
-import static org.hamcrest.CoreMatchers.hasItems;
-import static org.junit.Assert.assertThat;
+import static org.assertj.core.api.Assertions.assertThat;
 
 @RunWith(Parameterized.class)
 public class IdrisJvmTest {
     private static final String IDRIS_JVM_HOME = Optional.ofNullable(System.getProperty("IDRIS_JVM_HOME"))
-        .orElseGet(() -> Optional.ofNullable(System.getenv("IDRIS_JVM_HOME"))
-            .orElseGet(() -> System.getProperty("user.home")));
+            .orElseGet(() -> Optional.ofNullable(System.getenv("IDRIS_JVM_HOME"))
+                    .orElseGet(() -> System.getProperty("user.home")));
 
     private static File testOutputRootDir;
     private static String runtimeJarPath;
@@ -65,7 +64,7 @@ private void printCodegenServerLog() {
             Path logPath = Paths.get(IDRIS_JVM_HOME, "codegen", "idris-jvm-server.log");
             try {
                 Files.lines(logPath)
-                    .forEach(System.err::println);
+                        .forEach(System.err::println);
             } catch (IOException e) {
                 e.printStackTrace();
             }
@@ -86,9 +85,9 @@ public static Collection<Object[]> data() throws IOException {
         final PathMatchingResourcePatternResolver resolver = new PathMatchingResourcePatternResolver();
         final Resource[] resources = resolver.getResources("idris-test-sources");
         return Arrays.stream(resources)
-            .flatMap(IdrisJvmTest::getTestDirs)
-            .map(IdrisJvmTest::getTestFiles)
-            .collect(toList());
+                .flatMap(IdrisJvmTest::getTestDirs)
+                .map(IdrisJvmTest::getTestFiles)
+                .collect(toList());
     }
 
     @BeforeClass
@@ -116,7 +115,8 @@ public void test() throws IOException, InterruptedException {
         List<String> actualOutput = readFile(jvmOut);
         List<String> expectedOutput = readFile(expectedOutputFile);
 
-        assertThat(actualOutput, hasItems(expectedOutput.toArray(new String[0])));
+        assertThat(actualOutput)
+                .containsExactlyInAnyOrder(expectedOutput.toArray(new String[0]));
     }
 
     private static boolean shouldStartIdrisJvmServer() {
@@ -125,7 +125,7 @@ private static boolean shouldStartIdrisJvmServer() {
 
     private void compile(final File testOutputDir, final File compilerOut) throws IOException, InterruptedException {
         ProcessBuilder idrisCompilerProcessBuilder = new ProcessBuilder("idris", "--portable-codegen", "jvm", "-p",
-            "idrisjvmffi", "-p", "effects", sourceFile.getPath(), "-o", testOutputDir.getPath());
+                "idrisjvmffi", "-p", "effects", sourceFile.getPath(), "-o", testOutputDir.getPath());
         idrisCompilerProcessBuilder.directory(testOutputDir);
 
         idrisCompilerProcessBuilder.redirectErrorStream(true);

idris-jvm-io/src/main/java/io/github/mmhelloworld/idrisjvm/io/Files.java

@@ -1,5 +1,6 @@
 package io.github.mmhelloworld.idrisjvm.io;
 
+import java.io.File;
 import java.io.IOException;
 import java.nio.file.FileSystems;
 import java.nio.file.Path;
@@ -59,18 +60,34 @@ public static void writeFile(String pathString, String content) throws IOExcepti
     }
 
     public static Path createPath(String pathStr) {
+        return createPath(pathStr, workingDir);
+    }
+
+    private static Path createPath(String pathStr, String workingDir) {
+        if (pathStr.isEmpty()) {
+            return Paths.get(workingDir);
+        }
+
         Path path = Paths.get(pathStr);
+        final Path resolvedPath;
         if (path.isAbsolute()) {
-            return path;
+            resolvedPath = path;
         } else {
-            if (pathStr.equals(".")) {
-                return Paths.get(workingDir);
-            } else if (pathStr.equals("..")) {
-                return Paths.get(workingDir).getParent();
+            if (pathStr.startsWith("../")) {
+                resolvedPath = createPath(pathStr.substring("../".length()),
+                        Paths.get(workingDir).getParent().toString());
+            } else if (pathStr.startsWith("..")) {
+                resolvedPath = createPath(pathStr.substring("..".length()),
+                        Paths.get(workingDir).getParent().toString());
+            } else if (pathStr.startsWith("./")) {
+                resolvedPath = createPath(pathStr.substring("./".length()), workingDir);
+            } else if (pathStr.startsWith(".")) {
+                resolvedPath = createPath(pathStr.substring(".".length()), workingDir);
             } else {
-                return Paths.get(workingDir, pathStr);
+                resolvedPath = Paths.get(workingDir, pathStr);
             }
         }
+        return resolvedPath;
     }
 
     public static void createDirectory(String pathString) throws IOException {

idris-jvm-runtime/src/main/java/io/github/mmhelloworld/idrisjvm/runtime/IdrisSystem.java

@@ -0,0 +1,15 @@
+package io.github.mmhelloworld.idrisjvm.runtime;
+
+import java.math.BigInteger;
+
+import static java.lang.System.currentTimeMillis;
+import static java.lang.System.nanoTime;
+import static java.util.concurrent.TimeUnit.MILLISECONDS;
+
+public class IdrisSystem {
+    public static IdrisObject getIdrisClock() {
+        BigInteger seconds = BigInteger.valueOf(MILLISECONDS.toSeconds(currentTimeMillis()));
+        BigInteger nanoSeconds = BigInteger.valueOf(nanoTime());
+        return new IdrisObject(0, seconds, nanoSeconds);
+    }
+}

idris-jvm-runtime/src/main/java/io/github/mmhelloworld/idrisjvm/runtime/Runtime.java

@@ -1,6 +1,9 @@
 package io.github.mmhelloworld.idrisjvm.runtime;
 
+import io.github.mmhelloworld.idrisjvm.io.Files;
+
 import java.io.BufferedReader;
+import java.io.File;
 import java.io.IOException;
 import java.io.InputStreamReader;
 import java.io.PrintWriter;
@@ -131,7 +134,8 @@ public static BigInteger time() {
 
     public static int runCommand(String command) throws IOException, InterruptedException {
         String[] cmdarray = parseCommand(command).toArray(new String[0]);
-        ProcessBuilder processBuilder = new ProcessBuilder(cmdarray).inheritIO();
+        ProcessBuilder processBuilder = new ProcessBuilder(cmdarray)
+                .directory(new File(Files.getWorkingDir()));
         return processBuilder.start().waitFor();
     }
 

pom.xml

@@ -36,6 +36,7 @@
         <exec-maven-plugin.version>1.5.0</exec-maven-plugin.version>
         <maven-assembly-plugin.version>3.0.0</maven-assembly-plugin.version>
         <spring-boot-dependencies.version>1.5.3.RELEASE</spring-boot-dependencies.version>
+        <assertj.version>3.12.2</assertj.version>
     </properties>
 
     <dependencyManagement>
@@ -60,6 +61,14 @@
                 <version>${lombok.version}</version>
                 <scope>provided</scope>
             </dependency>
+
+            <dependency>
+                <groupId>org.assertj</groupId>
+                <artifactId>assertj-core</artifactId>
+                <version>${assertj.version}</version>
+                <scope>test</scope>
+            </dependency>
+
         </dependencies>
     </dependencyManagement>