WIP: CompilerRuntime module encapsulates FFI

.gitignore

@@ -17,3 +17,12 @@ tramp
 /src/BlodwenPaths.idr
 /tests/**/output
 /*/build/
+
+*.iml
+ttimpjvm
+blodwenjvmout
+ttimpjvmout
+
+*.class
+*.jar
+build

Makefile

@@ -16,10 +16,10 @@ src/BlodwenPaths.idr:
 	echo 'module BlodwenPaths; export bprefix : String; bprefix = "${PREFIX}"' > src/BlodwenPaths.idr
 
 prelude:
-	make -C prelude BLODWEN=../blodwen
+	make -C prelude BLODWEN=../blodwenjvm
 
 base: prelude
-	make -C base BLODWEN=../blodwen
+	make -C base BLODWEN=../blodwenjvm
 
 libs : prelude base
 
@@ -43,8 +43,8 @@ install:
 	mkdir -p ${PREFIX}/blodwen/support/chez
 	mkdir -p ${PREFIX}/blodwen/support/chicken
 	mkdir -p ${PREFIX}/blodwen/support/racket
-	make -C prelude install BLODWEN=../blodwen
-	make -C base install BLODWEN=../blodwen
+	make -C prelude install BLODWEN=../blodwenjvm
+	make -C base install BLODWEN=../blodwenjvm
 
 	install blodwen ${PREFIX}/bin
 	install support/chez/* ${PREFIX}/blodwen/support/chez

blodwen.ipkg

@@ -26,9 +26,12 @@ modules = Idris.CommandLine,
           Idris.IDEMode.TokenLine
 
 sourcedir = src
-executable = blodwen
--- opts = "--partial-eval --cg-opt -O2"
-opts = "--partial-eval"
+
+executable = blodwenjvmout
+
+opts = "--partial-eval --portable-codegen jvm"
+
+pkgs = idrisjvmffi
 
 main = Idris.Main
 

blodwenjvm

@@ -0,0 +1,87 @@
+#!/bin/sh
+
+# resolve links - $0 may be a softlink
+PRG="$0"
+
+while [ -h "$PRG" ]; do
+  ls=`ls -ld "$PRG"`
+  link=`expr "$ls" : '.*-> \(.*\)$'`
+  if expr "$link" : '/.*' > /dev/null; then
+    PRG="$link"
+  else
+    PRG=`dirname "$PRG"`/"$link"
+  fi
+done
+
+PRGDIR=`dirname "$PRG"`
+BASEDIR=`cd "$PRGDIR/.." >/dev/null; pwd`
+
+# OS specific support.  $var _must_ be set to either true or false.
+cygwin=false;
+darwin=false;
+case "`uname`" in
+  CYGWIN*) cygwin=true ;;
+  Darwin*) darwin=true
+           if [ -z "$JAVA_VERSION" ] ; then
+             JAVA_VERSION="CurrentJDK"
+           else
+             echo "Using Java version: $JAVA_VERSION"
+           fi
+		   if [ -z "$JAVA_HOME" ]; then
+		      if [ -x "/usr/libexec/java_home" ]; then
+			      JAVA_HOME=`/usr/libexec/java_home`
+			  else
+			      JAVA_HOME=/System/Library/Frameworks/JavaVM.framework/Versions/${JAVA_VERSION}/Home
+			  fi
+           fi
+           ;;
+esac
+
+if [ -z "$JAVA_HOME" ] ; then
+  if [ -r /etc/gentoo-release ] ; then
+    JAVA_HOME=`java-config --jre-home`
+  fi
+fi
+
+# For Cygwin, ensure paths are in UNIX format before anything is touched
+if $cygwin ; then
+  [ -n "$JAVA_HOME" ] && JAVA_HOME=`cygpath --unix "$JAVA_HOME"`
+fi
+
+# If a specific java binary isn't specified search for the standard 'java' binary
+if [ -z "$JAVACMD" ] ; then
+  if [ -n "$JAVA_HOME"  ] ; then
+    if [ -x "$JAVA_HOME/jre/sh/java" ] ; then
+      # IBM's JDK on AIX uses strange locations for the executables
+      JAVACMD="$JAVA_HOME/jre/sh/java"
+    else
+      JAVACMD="$JAVA_HOME/bin/java"
+    fi
+  else
+    JAVACMD=`which java`
+  fi
+fi
+
+if [ ! -x "$JAVACMD" ] ; then
+  echo "Error: JAVA_HOME is not defined correctly." 1>&2
+  echo "  We cannot execute $JAVACMD" 1>&2
+  exit 1
+fi
+
+# For Cygwin, switch paths to Windows format before running java
+if $cygwin; then
+  [ -n "$JAVA_HOME" ] && JAVA_HOME=`cygpath --path --windows "$JAVA_HOME"`
+  [ -n "$HOME" ] && HOME=`cygpath --path --windows "$HOME"`
+  [ -n "$BASEDIR" ] && BASEDIR=`cygpath --path --windows "$BASEDIR"`
+fi
+
+exec "$JAVACMD" $JAVA_OPTS  \
+  -Xss8m \
+  -Dapp.name="blodwenjvm" \
+  -Dapp.pid="$$" \
+  -Dapp.home="$BASEDIR" \
+  -Dbasedir="$BASEDIR" \
+  -cp \
+  $BASEDIR/Blodwen/blodwenjvmout:$IDRIS_JVM_HOME/idris-jvm-runtime.jar \
+  main.Main \
+  "$@"

manifest.mf

@@ -0,0 +1,3 @@
+Manifest-Version: 1.0
+Main-Class: main.Main
+

src/Compiler/Common.idr

@@ -8,7 +8,7 @@ import Core.TT
 
 import Data.CSet
 
-%include C "sys/stat.h"
+import CompilerRuntime
 
 public export
 record Codegen annot where
@@ -63,18 +63,13 @@ findUsedNames tm
 -- Some things missing from Prelude.File
 
 export
-exists : String -> IO Bool
+exists : String -> BIO Bool
 exists f 
     = do Right ok <- openFile f Read
              | Left err => pure False
          closeFile ok
          pure True
 
 export
-tmpName : IO String
-tmpName = foreign FFI_C "tmpnam" (Ptr -> IO String) null
-
-export
-chmod : String -> Int -> IO ()
-chmod f m = foreign FFI_C "chmod" (String -> Int -> IO ()) f m
-
+tmpName : BIO String
+tmpName = tmpFileName

src/Compiler/Scheme/Chez.idr

@@ -16,13 +16,15 @@ import Data.Vect
 import System
 import System.Info
 
+import CompilerRuntime
+
 %default covering
 
-firstExists : List String -> IO (Maybe String)
+firstExists : List String -> BIO (Maybe String)
 firstExists [] = pure Nothing
 firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs
 
-findChez : IO String
+findChez : BIO String
 findChez 
     = do e <- firstExists [p ++ x | p <- ["/usr/bin/", "/usr/local/bin/"],
                                     x <- ["scheme", "chez"]]

src/Compiler/Scheme/Chicken.idr

@@ -16,16 +16,18 @@ import Data.Vect
 import System
 import System.Info
 
+import CompilerRuntime
+
 %default covering
 
-firstExists : List String -> IO (Maybe String)
+firstExists : List String -> BIO (Maybe String)
 firstExists [] = pure Nothing
 firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs
 
-findCSI : IO String
+findCSI : BIO String
 findCSI = pure "/usr/bin/env csi"
 
-findCSC : IO String
+findCSC : BIO String
 findCSC = pure "/usr/bin/env csc"
 
 schHeader : List String -> String

src/Compiler/Scheme/Racket.idr

@@ -15,16 +15,18 @@ import Data.Vect
 import System
 import System.Info
 
+import CompilerRuntime
+
 %default covering
 
-firstExists : List String -> IO (Maybe String)
+firstExists : List String -> BIO (Maybe String)
 firstExists [] = pure Nothing
 firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs
 
-findRacket : IO String
+findRacket : BIO String
 findRacket = pure "/usr/bin/env racket"
 
-findRacoExe : IO String
+findRacoExe : BIO String
 findRacoExe = pure "raco exe"
 
 schHeader : String

src/CompilerRuntime.idr

@@ -0,0 +1,23 @@
+module CompilerRuntime
+
+import Java.Lang
+import public Control.IOExcept
+import public IdrisJvm.IO
+import public IdrisJvm.File
+import public IdrisJvm.System
+import public IdrisJvm.Data.Buffer
+public export
+BIO : Type -> Type
+BIO = JVM_IO
+
+public export
+BIOExcept : Type -> Type -> Type
+BIOExcept = IOExcept' FFI_JVM
+
+public export
+tmpFileName : BIO String
+tmpFileName = getTemporaryFileName
+
+public export
+hexNum : Int -> BIO ()
+hexNum num = print $ JavaString.format "%06x" !(listToArray [the Object $ believe_me $ JInteger.valueOf num])

src/Control/Monad/StateE.idr

@@ -5,8 +5,11 @@
 module Control.Monad.StateE
 
 import public Control.Catchable
-import public Control.IOExcept
 
+import CompilerRuntime
+
+%hide Prelude.Interactive.putChar
+%hide Prelude.Interactive.getChar
 %default total
 
 infix 5 :::
@@ -240,14 +243,14 @@ interface ConsoleIO (m : Type -> Type) where
   getChar : SE s err m Char
 
 export 
-ConsoleIO IO where
+ConsoleIO BIO where
   putStr = lift . putStr
   getStr = lift getLine
   putChar = lift . putChar
   getChar = lift getChar
 
 export 
-ConsoleIO (IOExcept err) where
+ConsoleIO (BIOExcept err) where
   putStr str = lift (ioe_lift (putStr str))
   getStr = lift (ioe_lift getLine)
   putChar c = lift (ioe_lift (putChar c))

src/Core/Binary.idr

@@ -16,7 +16,7 @@ import Core.UnifyState
 
 import public Utils.Binary
 
-import Data.Buffer
+import CompilerRuntime
 
 %default covering
 

src/Core/Context.idr

@@ -17,6 +17,10 @@ import Data.StringMap
 import Data.CSet
 import Data.List
 
+import CompilerRuntime
+
+%hide Prelude.File.changeDir
+%hide Prelude.Interactive.printLn
 %default total
 
 public export
@@ -1358,7 +1362,7 @@ setDetermining loc tn args
                            ++ showSep ", " (map show ns)))
 
 export
-runWithCtxt : Show annot => Core annot () -> IO ()
+runWithCtxt : Show annot => Core annot () -> BIO ()
 runWithCtxt prog = coreRun prog 
                            (\err => printLn err)
                            (\ok => pure ())

src/Core/Core.idr

@@ -5,7 +5,7 @@ import Core.CaseTree
 import Parser.Support
 
 import public Control.Catchable
-import public Data.IORef
+import public CompilerRuntime
 
 public export
 data TTCErrorMsg
@@ -265,11 +265,11 @@ error = Left
 export
 record Core annot t where
   constructor MkCore
-  runCore : IO (Either (Error annot) t)
+  runCore : BIO (Either (Error annot) t)
 
 export
-coreRun : Core annot a -> 
-          (Error annot -> IO b) -> (a -> IO b) -> IO b
+coreRun : Core annot a ->
+          (Error annot -> BIO b) -> (a -> BIO b) -> BIO b
 coreRun (MkCore act) err ok = either err ok !act
 
 export
@@ -287,7 +287,7 @@ wrapError fe (MkCore prog)
 -- This would be better if we restrict it to a limited set of IO operations
 export
 %inline
-coreLift : IO a -> Core annot a
+coreLift : BIO a -> Core annot a
 coreLift op = MkCore $ map Right op
 
 {- Monad, Applicative, Traversable are specialised by hand for Core.

src/Core/Directory.idr

@@ -7,6 +7,8 @@ import Core.Name
 
 import System.Info
 
+import CompilerRuntime
+
 %default total
 
 isWindows : Bool
@@ -104,7 +106,7 @@ pathToNS wdir fname
 
 -- Create subdirectories, if they don't exist
 export
-mkdirs : List String -> IO (Either FileError ())
+mkdirs : List String -> BIO (Either FileError ())
 mkdirs [] = pure (Right ())
 mkdirs (d :: ds)
     = do ok <- changeDir d

src/Core/GetType.idr

@@ -8,6 +8,7 @@ import Core.CaseTree
 import Data.List
 
 %default covering
+%hide Language.Reflection.Binder
 
 -- Get the type of an already typechecked thing.
 -- We need this (occasionally) because we don't store types in subterms (e.g. on