diff --git a/.gitignore b/.gitignore index 3264691..e2e31c4 100644 --- a/.gitignore +++ b/.gitignore @@ -17,3 +17,12 @@ tramp /src/BlodwenPaths.idr /tests/**/output /*/build/ + +*.iml +ttimpjvm +blodwenjvmout +ttimpjvmout + +*.class +*.jar +build diff --git a/Makefile b/Makefile index 026bf8b..735468a 100644 --- a/Makefile +++ b/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 diff --git a/blodwen.ipkg b/blodwen.ipkg index 453c506..aebb011 100644 --- a/blodwen.ipkg +++ b/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 diff --git a/blodwenjvm b/blodwenjvm new file mode 100755 index 0000000..ed2b86e --- /dev/null +++ b/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 \ + "$@" diff --git a/manifest.mf b/manifest.mf new file mode 100644 index 0000000..6948c82 --- /dev/null +++ b/manifest.mf @@ -0,0 +1,3 @@ +Manifest-Version: 1.0 +Main-Class: main.Main + diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index f01ecb2..919f1fd 100644 --- a/src/Compiler/Common.idr +++ b/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,7 +63,7 @@ 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 @@ -71,10 +71,5 @@ exists f 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 diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index 75e120c..7c73a4a 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/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"]] diff --git a/src/Compiler/Scheme/Chicken.idr b/src/Compiler/Scheme/Chicken.idr index 77fc42d..8782ae5 100644 --- a/src/Compiler/Scheme/Chicken.idr +++ b/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 diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index c04df5b..ec42332 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/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 diff --git a/src/CompilerRuntime.idr b/src/CompilerRuntime.idr new file mode 100644 index 0000000..7dce671 --- /dev/null +++ b/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]) diff --git a/src/Control/Monad/StateE.idr b/src/Control/Monad/StateE.idr index 82738d9..6edadc8 100644 --- a/src/Control/Monad/StateE.idr +++ b/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)) diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 0659ffc..702adc0 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -16,7 +16,7 @@ import Core.UnifyState import public Utils.Binary -import Data.Buffer +import CompilerRuntime %default covering diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 987ddde..d49086e 100644 --- a/src/Core/Context.idr +++ b/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 ()) diff --git a/src/Core/Core.idr b/src/Core/Core.idr index cdca1cf..de3636a 100644 --- a/src/Core/Core.idr +++ b/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. diff --git a/src/Core/Directory.idr b/src/Core/Directory.idr index 2736202..c5e028a 100644 --- a/src/Core/Directory.idr +++ b/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 diff --git a/src/Core/GetType.idr b/src/Core/GetType.idr index 9f61106..3178989 100644 --- a/src/Core/GetType.idr +++ b/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 diff --git a/src/Core/Normalise.idr b/src/Core/Normalise.idr index d258d6e..8ea893f 100644 --- a/src/Core/Normalise.idr +++ b/src/Core/Normalise.idr @@ -9,6 +9,8 @@ import Core.TT import Data.List import Data.Vect +import CompilerRuntime + %default covering -- total is hard here, because the things we're evaluating -- might not themselves terminate, but covering is important. @@ -231,7 +233,7 @@ export nfAll : Defs -> Env Term free -> Term free -> NF free nfAll defs env tm = eval defs withAll env [] [] tm -genName : IORef Int -> String -> IO Name +genName : IORef Int -> String -> BIO Name genName num root = do n <- readIORef num writeIORef num (n + 1) @@ -241,7 +243,7 @@ public export interface Quote (tm : List Name -> Type) where quote : Defs -> Env Term vars -> tm vars -> Term vars quoteGen : IORef Int -> - Defs -> Env Term vars -> tm vars -> IO (Term vars) + Defs -> Env Term vars -> tm vars -> BIO (Term vars) -- Ugh. An STRef would be better (even if it would be implemented exactly -- like this, at least it would have an interface that prevented any chance @@ -252,18 +254,18 @@ interface Quote (tm : List Name -> Type) where mutual quoteArgs : IORef Int -> Defs -> Env Term free -> List (Closure free) -> - IO (List (Term free)) + BIO (List (Term free)) quoteArgs num defs env [] = pure [] quoteArgs num defs env (thunk :: args) = pure $ !(quoteGen num defs env (evalClosure defs thunk)) :: !(quoteArgs num defs env args) - quoteHead : NHead free -> IO (Term free) + quoteHead : NHead free -> BIO (Term free) quoteHead (NLocal r y) = pure $ Local r y quoteHead (NRef nt n) = pure $ Ref nt n quoteBinder : IORef Int -> Defs -> Env Term free -> Binder (NF free) -> - IO (Binder (Term free)) + BIO (Binder (Term free)) quoteBinder num defs env (Lam c x ty) = do ty' <- quoteGen num defs env ty pure (Lam c x ty') @@ -346,7 +348,7 @@ public export interface Convert (tm : List Name -> Type) where convert : Defs -> Env Term vars -> tm vars -> tm vars -> Bool convGen : IORef Int -> - Defs -> Env Term vars -> tm vars -> tm vars -> IO Bool + Defs -> Env Term vars -> tm vars -> tm vars -> BIO Bool -- Ugh. An STRef would be better (even if it would be implemented exactly -- like this, at least it would have an interface that prevented any chance @@ -357,14 +359,14 @@ interface Convert (tm : List Name -> Type) where mutual allConv : IORef Int -> Defs -> Env Term vars -> - List (Closure vars) -> List (Closure vars) -> IO Bool + List (Closure vars) -> List (Closure vars) -> BIO Bool allConv num defs env [] [] = pure True allConv num defs env (x :: xs) (y :: ys) = pure $ !(convGen num defs env x y) && !(allConv num defs env xs ys) allConv num defs env _ _ = pure False chkConvHead : Defs -> Env Term vars -> - NHead vars -> NHead vars -> IO Bool + NHead vars -> NHead vars -> BIO Bool chkConvHead defs env (NLocal _ x) (NLocal _ y) = pure $ sameVar x y chkConvHead defs env (NRef x y) (NRef x' y') = pure $ y == y' chkConvHead defs env x y = pure False @@ -375,7 +377,7 @@ mutual subRig x y = x == y -- otherwise, the multiplicities need to match up convBinders : IORef Int -> Defs -> Env Term vars -> - Binder (NF vars) -> Binder (NF vars) -> IO Bool + Binder (NF vars) -> Binder (NF vars) -> BIO Bool convBinders num defs env (Pi cx ix tx) (Pi cy iy ty) = if ix /= iy || not (subRig cx cy) then pure False diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index 8f1790b..71e6e57 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -9,7 +9,14 @@ import Utils.Binary import Data.List import Data.Vect +import CompilerRuntime + %default total +%hide Prelude.File.File +%hide Prelude.File.FileError +%hide Prelude.File.openFile +%hide Language.Reflection.NameType +%hide Language.Reflection.Binder -- TTC instances for TT primitives diff --git a/src/Core/Typecheck.idr b/src/Core/Typecheck.idr index 98bb306..20cc97b 100644 --- a/src/Core/Typecheck.idr +++ b/src/Core/Typecheck.idr @@ -9,6 +9,10 @@ import Data.List %default covering +%hide Language.Reflection.Raw +%hide Language.Reflection.Binder +%hide FFI_C.Raw + export doConvert : (Quote tm, Convert tm) => annot -> Defs -> Env Term outer -> diff --git a/src/Core/UnifyState.idr b/src/Core/UnifyState.idr index d8d4eda..efb6c0c 100644 --- a/src/Core/UnifyState.idr +++ b/src/Core/UnifyState.idr @@ -11,6 +11,8 @@ import Data.CSet import Data.List import Data.List.Views +import CompilerRuntime + %default covering public export diff --git a/src/Data/IOHash.idr b/src/Data/IOHash.idr index 74c81ee..9c81291 100644 --- a/src/Data/IOHash.idr +++ b/src/Data/IOHash.idr @@ -2,6 +2,8 @@ module Data.IOHash import Data.IOArray +import CompilerRuntime + -- A simple implementation of a mutable hash table export @@ -14,7 +16,7 @@ record IOHash key value where export new : (key -> key -> Bool) -> - (key -> Int) -> Nat -> IO (IOHash key valInt) + (key -> Int) -> Nat -> BIO (IOHash key valInt) new eq hash n = do arr <- newArray (cast n) [] pure (MkTable eq hash (cast n) arr) @@ -23,7 +25,7 @@ findPos : Int -> Int -> Int findPos hash x = assert_total $ if x <=0 then 0 else abs (hash `mod` x) export -insert : key -> value -> IOHash key value -> IO () +insert : key -> value -> IOHash key value -> BIO () insert k v table = do let arr = buckets table let pos = hash table k `findPos` numBuckets table @@ -31,7 +33,7 @@ insert k v table unsafeWriteArray arr pos ((k, v) :: row) export -update : key -> value -> IOHash key value -> IO () +update : key -> value -> IOHash key value -> BIO () update k v table = do let arr = buckets table let pos = hash table k `findPos` numBuckets table @@ -46,7 +48,7 @@ update k v table else ((k', v') :: updateVal eq k v rest) export -delete : key -> IOHash key value -> IO () +delete : key -> IOHash key value -> BIO () delete k table = do let arr = buckets table let pos = hash table k `findPos` numBuckets table @@ -60,7 +62,7 @@ delete k table = if eq k k' then rest else ((k', v') :: deleteVal eq k rest) export -lookup : key -> IOHash key value -> IO (Maybe value) +lookup : key -> IOHash key value -> BIO (Maybe value) lookup k table = do let arr = buckets table let pos = hash table k `findPos` numBuckets table diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index 36206f4..7b5b7d3 100644 --- a/src/Idris/CommandLine.idr +++ b/src/Idris/CommandLine.idr @@ -2,6 +2,8 @@ module Idris.CommandLine import Data.Vect +import CompilerRuntime + %default total public export @@ -145,7 +147,7 @@ getOpts opts = parseOpts options opts export covering -getCmdOpts : IO (Either String (List CLOpt)) +getCmdOpts : BIO (Either String (List CLOpt)) getCmdOpts = do (_ :: opts) <- getArgs | pure (Left "Invalid command line") pure $ getOpts opts diff --git a/src/Idris/IDEMode/Commands.idr b/src/Idris/IDEMode/Commands.idr index b818ecc..47af3b3 100644 --- a/src/Idris/IDEMode/Commands.idr +++ b/src/Idris/IDEMode/Commands.idr @@ -3,6 +3,9 @@ module Idris.IDEMode.Commands import Core.Core import Core.Name +import CompilerRuntime + +%hide Prelude.File.File %default covering public export @@ -146,8 +149,8 @@ export version : Int -> Int -> SExp version maj min = toSExp (SymbolAtom "protocol-version", maj, min) -hex : Int -> IO () -hex num = foreign FFI_C "printf" (String -> Int -> IO ()) "%06x" num +hex : Int -> BIO () +hex num = hexNum num export send : SExpable a => a -> Core annot () diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index c019021..d01cdde 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -33,9 +33,11 @@ import TTImp.ProcessTTImp import TTImp.Reflect import Control.Catchable -import System +-- import System -getNChars : Nat -> IO (List Char) +import CompilerRuntime + +getNChars : Nat -> BIO (List Char) getNChars Z = pure [] getNChars (S k) = do x <- getChar @@ -68,7 +70,7 @@ toHex m (d :: ds) -- Read 6 characters. If they're a hex number, read that many characters. -- Otherwise, just read to newline -getInput : IO String +getInput : BIO String getInput = do x <- getNChars 6 case toHex 1 (reverse x) of diff --git a/src/Idris/Main.idr b/src/Idris/Main.idr index fa031e4..edd3337 100644 --- a/src/Idris/Main.idr +++ b/src/Idris/Main.idr @@ -21,10 +21,12 @@ import Idris.SetOptions import Idris.Syntax import Data.Vect -import System +-- import System import BlodwenPaths +import CompilerRuntime + %default covering findInput : List CLOpt -> Maybe String @@ -125,7 +127,7 @@ stMain opts -- Run any options (such as --version or --help) which imply printing a -- message then exiting. Returns wheter the program should continue -quitOpts : List CLOpt -> IO Bool +quitOpts : List CLOpt -> BIO Bool quitOpts [] = pure True quitOpts (Version :: _) = do putStrLn versionMsg @@ -138,7 +140,7 @@ quitOpts (ShowPrefix :: _) pure False quitOpts (_ :: opts) = quitOpts opts -main : IO () +main : BIO () main = do Right opts <- getCmdOpts | Left err => do putStrLn err diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index 296ccb2..53fe516 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -6,6 +6,8 @@ import Core.Directory import Core.Options import Core.Unify +import Control.Catchable + import Idris.CommandLine import Idris.ModTree import Idris.ProcessIdr @@ -16,9 +18,11 @@ import Parser.Lexer import Parser.Support import Utils.Binary -import System +-- import System import Text.Parser +import CompilerRuntime + %default covering record PkgDesc where @@ -182,7 +186,7 @@ build pkg runScript (postbuild pkg) pure [] -copyFile : String -> String -> IO (Either FileError ()) +copyFile : String -> String -> BIO (Either FileError ()) copyFile src dest = do Right buf <- readFromFile src | Left err => pure (Left err) diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 3eb7cab..ec62c2e 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -38,7 +38,8 @@ import TTImp.Reflect import Control.Catchable -import System +-- import System +import CompilerRuntime %default covering diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 55d75ed..ac077e0 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -10,7 +10,8 @@ import Idris.CommandLine import Idris.REPL import Idris.Syntax -import System +-- import System + -- TODO: Version numbers on dependencies export diff --git a/src/Interfaces/FileIO.idr b/src/Interfaces/FileIO.idr index 8940ed8..73efcea 100644 --- a/src/Interfaces/FileIO.idr +++ b/src/Interfaces/FileIO.idr @@ -1,8 +1,8 @@ module Interfaces.FileIO import Control.Monad.StateE -import Control.IOExcept import Core.Context +import CompilerRuntime public export interface FileIO (m : Type -> Type) where @@ -12,11 +12,12 @@ interface FileIO (m : Type -> Type) where SE s err m (Either FileError ()) export -FileIO IO where +FileIO BIO where readFile f = lift (readFile f) writeFile f c = lift (writeFile f c) export -FileIO (IOExcept (Error annot)) where +FileIO (BIOExcept (Error annot)) where + -- not handling errors for now readFile f = lift (ioe_lift (readFile f)) writeFile f c = lift (ioe_lift (writeFile f c)) diff --git a/src/Interfaces/SystemIO.idr b/src/Interfaces/SystemIO.idr index edf4945..4a463a0 100644 --- a/src/Interfaces/SystemIO.idr +++ b/src/Interfaces/SystemIO.idr @@ -1,9 +1,10 @@ module Interfaces.SystemIO import Control.Monad.StateE -import Control.IOExcept import Core.Context +import CompilerRuntime + public export interface SystemIO (m : Type -> Type) where getArgs : SE s err m (List String) @@ -13,5 +14,9 @@ SystemIO IO where getArgs = lift getArgs export -SystemIO (IOExcept (Error annot)) where +SystemIO BIO where + getArgs = lift getArgs + +export +SystemIO (BIOExcept (Error annot)) where getArgs = lift (ioe_lift getArgs) diff --git a/src/Parser/Support.idr b/src/Parser/Support.idr index a5362af..d71a7b0 100644 --- a/src/Parser/Support.idr +++ b/src/Parser/Support.idr @@ -7,6 +7,12 @@ import public Text.Parser import Core.TT import Data.List.Views +import CompilerRuntime + +%hide Prelude.File.File +%hide Prelude.File.FileError +%hide Prelude.File.readFile + %default total public export @@ -57,7 +63,7 @@ runParser str p Right (val, _) => Right val export -parseFile : (fn : String) -> Rule ty -> IO (Either ParseError ty) +parseFile : (fn : String) -> Rule ty -> BIO (Either ParseError ty) parseFile fn p = do Right str <- readFile fn | Left err => pure (Left (FileFail err)) diff --git a/src/TTImp/GenerateDef.idr b/src/TTImp/GenerateDef.idr index e46543d..06ffac1 100644 --- a/src/TTImp/GenerateDef.idr +++ b/src/TTImp/GenerateDef.idr @@ -7,6 +7,8 @@ import Core.Metadata import Core.Normalise import Core.TT import Core.Unify +import Control.Monad.StateE +import Control.Catchable import TTImp.CaseSplit import TTImp.Elab diff --git a/src/TTImp/Main.idr b/src/TTImp/Main.idr index 53be7f6..16a7497 100644 --- a/src/TTImp/Main.idr +++ b/src/TTImp/Main.idr @@ -21,6 +21,8 @@ import TTImp.TTImp import Parser.RawImp +import CompilerRuntime + usageMsg : Core () () usageMsg = coreLift $ putStrLn "Usage: ttimp [source file]" @@ -49,7 +51,7 @@ stMain writeToTTC () !(getTTCFileName fname ".ttc") repl {c} {u} {m} -main : IO () +main : BIO () main = do putStrLn "Welcome to TTImp. Good luck." coreRun stMain (\err : Error () => putStrLn ("Uncaught error: " ++ show err)) diff --git a/src/TTImp/ProcessTTImp.idr b/src/TTImp/ProcessTTImp.idr index 548e1b8..898a7a7 100644 --- a/src/TTImp/ProcessTTImp.idr +++ b/src/TTImp/ProcessTTImp.idr @@ -25,6 +25,11 @@ import Control.Catchable import Control.Monad.StateE import Interfaces.FileIO + +%hide Prelude.File.File +%hide Prelude.File.FileError +%hide Prelude.File.readFile + %default covering -- Need to propagate the top level elaborator 'processDecl' throughout diff --git a/src/Utils/Binary.idr b/src/Utils/Binary.idr index d495519..275ff43 100644 --- a/src/Utils/Binary.idr +++ b/src/Utils/Binary.idr @@ -1,16 +1,19 @@ module Utils.Binary import Core.Core -import Data.Buffer import Data.List import Data.Vect import public Data.StringMap +import CompilerRuntime -- Serialising data as binary. Provides an interface TTC which allows -- reading and writing to chunks of memory, "Binary", which can be written -- to and read from files. %default covering +%hide Prelude.File.File +%hide Prelude.File.FileError +%hide Prelude.File.openFile -- A label for binary states export @@ -49,7 +52,7 @@ incLoc i c = record { loc $= (+i) } c export data Binary = MkBin (List Chunk) Chunk (List Chunk) -dumpBin : Binary -> IO () +dumpBin : Binary -> BIO () dumpBin (MkBin done chunk rest) = do printLn !(traverse bufferData (map buf done)) printLn !(bufferData (buf chunk)) @@ -76,7 +79,7 @@ req (c :: cs) -- Take all the data from the chunks in a 'Binary' and copy them into one -- single buffer, ready for writing to disk. -- TODO: YAGNI? Delete if so... -toBuffer : Binary -> IO (Maybe Buffer) +toBuffer : Binary -> BIO (Maybe Buffer) toBuffer (MkBin done cur rest) = do let chunks = reverse done ++ cur :: rest Just b <- newBuffer (req chunks) @@ -84,19 +87,19 @@ toBuffer (MkBin done cur rest) copyToBuf 0 b chunks pure (Just b) where - copyToBuf : (pos : Int) -> Buffer -> List Chunk -> IO () + copyToBuf : (pos : Int) -> Buffer -> List Chunk -> BIO () copyToBuf pos b [] = pure () copyToBuf pos b (c :: cs) = do copyData (buf c) 0 (used c) b pos copyToBuf (pos + used c) b cs -fromBuffer : Buffer -> IO Binary +fromBuffer : Buffer -> BIO Binary fromBuffer buf = do len <- rawSize buf pure (MkBin [] (MkChunk buf 0 len len) []) -- assume all used export -writeToFile : (fname : String) -> Binary -> IO (Either FileError ()) +writeToFile : (fname : String) -> Binary -> BIO (Either FileError ()) writeToFile fname (MkBin done cur rest) = do Right h <- openFile fname WriteTruncate | Left err => pure (Left err) @@ -105,21 +108,21 @@ writeToFile fname (MkBin done cur rest) closeFile h pure (Right ()) where - writeChunks : File -> List Chunk -> IO () + writeChunks : File -> List Chunk -> BIO () writeChunks h [] = pure () writeChunks h (c :: cs) = do writeBufferToFile h (resetBuffer (buf c)) (used c) writeChunks h cs export -readFromFile : (fname : String) -> IO (Either FileError Binary) +readFromFile : (fname : String) -> BIO (Either FileError Binary) readFromFile fname = do Right h <- openFile fname Read | Left err => pure (Left err) Right max <- fileSize h | Left err => pure (Left err) Just b <- newBuffer max - | Nothing => pure (Left (GenericFileError 0)) --- um, not really + | Nothing => pure (Left $ believe_me (unableToReadFile fname)) --- um, not really b <- readBufferFromFile h b max pure (Right (MkBin [] (MkChunk b 0 max max) [])) diff --git a/ttimp.ipkg b/ttimp.ipkg index f11cfde..752859c 100644 --- a/ttimp.ipkg +++ b/ttimp.ipkg @@ -86,8 +86,12 @@ modules = Compiler.Common, Utils.Binary sourcedir = src -executable = ttimp -opts = "--partial-eval" + +executable = ttimpjvmout + +opts = "--partial-eval --portable-codegen jvm" + +pkgs = idrisjvmffi main = TTImp.Main