From b50ca3cf713f9393e337dbc8b245fb2d0ae2cb87 Mon Sep 17 00:00:00 2001 From: Marimuthu Madasamy Date: Thu, 5 Sep 2019 00:36:27 -0400 Subject: [PATCH] idrisjvm-104 compile to JVM --- .gitignore | 5 ++ CONTRIBUTING.md | 2 +- Notes/implementation-notes.md | 2 +- TypeDD.md | 2 +- idris2.ipkg | 8 +-- libs/base/Data/Buffer.idr | 28 ++++---- libs/base/Data/IORef.idr | 8 +-- libs/base/System.idr | 8 +-- libs/base/System/Concurrency/Raw.idr | 22 +++---- libs/base/System/File.idr | 20 +++--- libs/base/System/REPL.idr | 4 +- libs/network/Echo.idr | 8 +-- libs/network/Network/Socket.idr | 24 +++---- libs/network/Network/Socket/Data.idr | 4 +- libs/network/Network/Socket/Raw.idr | 28 ++++---- libs/prelude/Prelude.idr | 12 ++-- libs/prelude/PrimIO.idr | 40 ++++++------ src/Compiler/Common.idr | 15 +++-- src/Compiler/Scheme/Chez.idr | 10 ++- src/Compiler/Scheme/Chicken.idr | 10 ++- src/Compiler/Scheme/Racket.idr | 10 ++- src/Core/Binary.idr | 3 +- src/Core/Context.idr | 8 ++- src/Core/Core.idr | 16 +++-- src/Core/Directory.idr | 5 +- src/Core/Metadata.idr | 2 + src/Core/Normalise.idr | 2 + src/Core/TTC.idr | 9 +++ src/Data/IOArray.idr | 52 +++++++-------- src/Idris/CommandLine.idr | 5 +- src/Idris/Error.idr | 3 + src/Idris/IDEMode/CaseSplit.idr | 3 + src/Idris/IDEMode/Commands.idr | 16 +++-- src/Idris/IDEMode/REPL.idr | 65 +++++++------------ src/Idris/Main.idr | 14 ++-- src/Idris/ModTree.idr | 3 + src/Idris/Package.idr | 13 ++-- src/Idris/ProcessIdr.idr | 3 + src/Idris/REPL.idr | 6 +- src/Idris/REPLCommon.idr | 2 + src/Idris/REPLOpts.idr | 3 +- src/Idris/SetOptions.idr | 3 +- src/Idris/Socket.idr | 52 +++++++-------- src/Idris/Socket/Data.idr | 2 +- src/Idris/Socket/Raw.idr | 58 ++++++++--------- src/Parser/Support.idr | 9 ++- src/TTImp/ProcessDecls.idr | 2 + src/Utils/Binary.idr | 17 +++-- src/Yaffle/Main.idr | 5 +- src/Yaffle/REPL.idr | 2 + tests.ipkg | 4 +- tests/Main.idr | 30 +++++---- tests/chez/chez001/Total.idr | 2 +- tests/chez/chez001/expected | 4 +- tests/chez/chez002/expected | 4 +- tests/chez/chez003/IORef.idr | 2 +- tests/chez/chez003/expected | 8 +-- tests/chez/chez004/Buffer.idr | 2 +- tests/chez/chez004/expected | 8 +-- tests/chez/chez005/expected | 4 +- tests/chez/chez006/TypeCase.idr | 2 +- tests/chez/chez006/expected | 8 +-- tests/chez/chez007/TypeCase.idr | 2 +- tests/chez/chez007/expected | 8 +-- tests/idris2/basic019/expected | 4 +- tests/idris2/error008/expected | 25 ++++++- tests/idris2/perf001/Big.idr | 2 +- tests/idris2/perf002/Big.idr | 4 +- tests/idris2/total006/Total.idr | 2 +- tests/typedd-book/chapter01/Hello.idr | 2 +- tests/typedd-book/chapter01/HelloHole.idr | 2 +- tests/typedd-book/chapter01/HoleFix.idr | 2 +- tests/typedd-book/chapter02/AveMain.idr | 2 +- tests/typedd-book/chapter02/Reverse.idr | 2 +- tests/typedd-book/chapter04/DataStore.idr | 2 +- tests/typedd-book/chapter04/SumInputs.idr | 2 +- tests/typedd-book/chapter05/DepPairs.idr | 4 +- tests/typedd-book/chapter05/Do.idr | 6 +- tests/typedd-book/chapter05/Hello.idr | 2 +- tests/typedd-book/chapter05/Loops.idr | 6 +- tests/typedd-book/chapter05/PrintLength.idr | 2 +- tests/typedd-book/chapter05/ReadNum.idr | 10 +-- tests/typedd-book/chapter05/ReadVect.idr | 6 +- tests/typedd-book/chapter06/DataStore.idr | 2 +- .../typedd-book/chapter06/DataStoreHoles.idr | 2 +- tests/typedd-book/chapter09/Hangman.idr | 6 +- tests/typedd-book/chapter11/Arith.idr | 4 +- tests/typedd-book/chapter11/ArithCmd.idr | 6 +- tests/typedd-book/chapter11/ArithCmdDo.idr | 6 +- tests/typedd-book/chapter11/ArithTotal.idr | 8 +-- tests/typedd-book/chapter11/Greet.idr | 4 +- tests/typedd-book/chapter11/InfIO.idr | 10 +-- tests/typedd-book/chapter11/RunIO.idr | 8 +-- tests/typedd-book/chapter12/ArithState.idr | 6 +- tests/typedd-book/chapter12/Traverse.idr | 2 +- 95 files changed, 496 insertions(+), 396 deletions(-) diff --git a/.gitignore b/.gitignore index a9ebdc606..da6eaa9b1 100644 --- a/.gitignore +++ b/.gitignore @@ -12,3 +12,8 @@ libs/**/build tests/**/output src/YafflePaths.idr + +*.iml +classes/** +*-classes/** +output diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index fdc031054..9da6cde08 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -40,7 +40,7 @@ Some language extensions from Idris 1 have not yet been implemented. Most notably: * Type providers - - Perhaps consider safety - do we allow arbitrary IO operations, or is + - Perhaps consider safety - do we allow arbitrary JVM_IO operations, or is there a way to restrict them so that they can't, for example, delete files or run executables. * Elaborator reflection diff --git a/Notes/implementation-notes.md b/Notes/implementation-notes.md index 62fc620d4..6eb0e420a 100644 --- a/Notes/implementation-notes.md +++ b/Notes/implementation-notes.md @@ -46,7 +46,7 @@ Where to find things: The Core Type, and Ref ---------------------- Core is a "monad" (not really, for efficiency reasons, at the moment...) -supporting Errors and IO [TODO: Allow restricting to specific IO operations] +supporting Errors and JVM_IO [TODO: Allow restricting to specific JVM_IO operations] The raw syntax is defined by a type RawImp which has a source location at each node, and any errors in elaboration note the location at the point where the error occurred. diff --git a/TypeDD.md b/TypeDD.md index 120567c5f..391e3477d 100644 --- a/TypeDD.md +++ b/TypeDD.md @@ -121,7 +121,7 @@ In `Hangman.idr`: definition, so add them to its type: game : {guesses : _} -> {letters : _} -> - WordState (S guesses) (S letters) -> IO Finished + WordState (S guesses) (S letters) -> JVM_IO Finished Chapter 10 ---------- diff --git a/idris2.ipkg b/idris2.ipkg index 4fe358187..137ed6ad2 100644 --- a/idris2.ipkg +++ b/idris2.ipkg @@ -66,9 +66,6 @@ modules = Idris.REPLOpts, Idris.Resugar, Idris.SetOptions, - Idris.Socket, - Idris.Socket.Data, - Idris.Socket.Raw, Idris.Syntax, Parser.Lexer, @@ -122,10 +119,13 @@ modules = sourcedir = src executable = idris2 + -- opts = "--cg-opt -O2 --partial-eval" -- opts = "--cg-opt -pg --partial-eval" -opts = "--partial-eval" +opts = "--partial-eval --portable-codegen jvm" -- opts = "--partial-eval --cg-opt -lws2_32" -- windows +pkgs = idrisjvmffi + main = Idris.Main diff --git a/libs/base/Data/Buffer.idr b/libs/base/Data/Buffer.idr index 30bf3c667..1d6700944 100644 --- a/libs/base/Data/Buffer.idr +++ b/libs/base/Data/Buffer.idr @@ -7,13 +7,13 @@ data Buffer : Type where MkBuffer : Ptr -> (size : Int) -> (loc : Int) -> Buffer export -newBuffer : Int -> IO Buffer +newBuffer : Int -> JVM_IO Buffer newBuffer size = do buf <- schemeCall Ptr "blodwen-new-buffer" [size] pure (MkBuffer buf size 0) export -rawSize : Buffer -> IO Int +rawSize : Buffer -> JVM_IO Int rawSize (MkBuffer buf _ _) = schemeCall Int "blodwen-buffer-size" [buf] @@ -23,65 +23,65 @@ size (MkBuffer _ s _) = s -- Assumes val is in the range 0-255 export -setByte : Buffer -> (loc : Int) -> (val : Int) -> IO () +setByte : Buffer -> (loc : Int) -> (val : Int) -> JVM_IO () setByte (MkBuffer buf _ _) loc val = schemeCall () "blodwen-buffer-setbyte" [buf, loc, val] export -getByte : Buffer -> (loc : Int) -> IO Int +getByte : Buffer -> (loc : Int) -> JVM_IO Int getByte (MkBuffer buf _ _) loc = schemeCall Int "blodwen-buffer-getbyte" [buf, loc] export -setInt : Buffer -> (loc : Int) -> (val : Int) -> IO () +setInt : Buffer -> (loc : Int) -> (val : Int) -> JVM_IO () setInt (MkBuffer buf _ _) loc val = schemeCall () "blodwen-buffer-setint" [buf, loc, val] export -getInt : Buffer -> (loc : Int) -> IO Int +getInt : Buffer -> (loc : Int) -> JVM_IO Int getInt (MkBuffer buf _ _) loc = schemeCall Int "blodwen-buffer-getint" [buf, loc] export -setDouble : Buffer -> (loc : Int) -> (val : Double) -> IO () +setDouble : Buffer -> (loc : Int) -> (val : Double) -> JVM_IO () setDouble (MkBuffer buf _ _) loc val = schemeCall () "blodwen-buffer-setdouble" [buf, loc, val] export -getDouble : Buffer -> (loc : Int) -> IO Double +getDouble : Buffer -> (loc : Int) -> JVM_IO Double getDouble (MkBuffer buf _ _) loc = schemeCall Double "blodwen-buffer-getdouble" [buf, loc] export -setString : Buffer -> (loc : Int) -> (val : String) -> IO () +setString : Buffer -> (loc : Int) -> (val : String) -> JVM_IO () setString (MkBuffer buf _ _) loc val = schemeCall () "blodwen-buffer-setstring" [buf, loc, val] export -getString : Buffer -> (loc : Int) -> (len : Int) -> IO String +getString : Buffer -> (loc : Int) -> (len : Int) -> JVM_IO String getString (MkBuffer buf _ _) loc len = schemeCall String "blodwen-buffer-getstring" [buf, loc, len] export -bufferData : Buffer -> IO (List Int) +bufferData : Buffer -> JVM_IO (List Int) bufferData buf = do len <- rawSize buf unpackTo [] len where - unpackTo : List Int -> Int -> IO (List Int) + unpackTo : List Int -> Int -> JVM_IO (List Int) unpackTo acc 0 = pure acc unpackTo acc loc = do val <- getByte buf (loc - 1) unpackTo (val :: acc) (loc - 1) export -readBufferFromFile : BinaryFile -> Buffer -> (maxbytes : Int) -> IO Buffer +readBufferFromFile : BinaryFile -> Buffer -> (maxbytes : Int) -> JVM_IO Buffer readBufferFromFile (FHandle h) (MkBuffer buf size loc) max = do read <- schemeCall Int "blodwen-readbuffer" [h, buf, loc, max] pure (MkBuffer buf size (loc + read)) export -writeBufferToFile : BinaryFile -> Buffer -> (maxbytes : Int) -> IO Buffer +writeBufferToFile : BinaryFile -> Buffer -> (maxbytes : Int) -> JVM_IO Buffer writeBufferToFile (FHandle h) (MkBuffer buf size loc) max = do let maxwrite = size - loc let max' = if maxwrite < max then maxwrite else max diff --git a/libs/base/Data/IORef.idr b/libs/base/Data/IORef.idr index 930855ad8..223e73dac 100644 --- a/libs/base/Data/IORef.idr +++ b/libs/base/Data/IORef.idr @@ -15,21 +15,21 @@ data IORef : Type -> Type where MkRef : Mut a -> IORef a export -newIORef : a -> IO (IORef a) +newIORef : a -> JVM_IO (IORef a) newIORef val = do m <- primIO (prim__newIORef val) pure (MkRef m) export -readIORef : IORef a -> IO a +readIORef : IORef a -> JVM_IO a readIORef (MkRef m) = primIO (prim__readIORef m) export -writeIORef : IORef a -> (1 val : a) -> IO () +writeIORef : IORef a -> (1 val : a) -> JVM_IO () writeIORef (MkRef m) val = primIO (prim__writeIORef m val) export -modifyIORef : IORef a -> (a -> a) -> IO () +modifyIORef : IORef a -> (a -> a) -> JVM_IO () modifyIORef ref f = do val <- readIORef ref writeIORef ref (f val) diff --git a/libs/base/System.idr b/libs/base/System.idr index a6e9b906d..96bf254d5 100644 --- a/libs/base/System.idr +++ b/libs/base/System.idr @@ -5,17 +5,17 @@ import Data.So %cg chicken (use posix) export -sleep : Int -> IO () +sleep : Int -> JVM_IO () sleep sec = schemeCall () "blodwen-sleep" [sec] export -usleep : (x : Int) -> So (x >= 0) => IO () +usleep : (x : Int) -> So (x >= 0) => JVM_IO () usleep usec = schemeCall () "blodwen-usleep" [usec] export -getArgs : IO (List String) +getArgs : JVM_IO (List String) getArgs = schemeCall (List String) "blodwen-args" [] export -time : IO Integer +time : JVM_IO Integer time = schemeCall Integer "blodwen-time" [] diff --git a/libs/base/System/Concurrency/Raw.idr b/libs/base/System/Concurrency/Raw.idr index ef32f5a67..2e7e532a2 100644 --- a/libs/base/System/Concurrency/Raw.idr +++ b/libs/base/System/Concurrency/Raw.idr @@ -5,53 +5,53 @@ module System.Concurrency.Raw %cg chicken (use srfi-18) export -threadID : IO ThreadID +threadID : JVM_IO ThreadID threadID = schemeCall ThreadID "blodwen-thisthread" [] export -setThreadData : {a : Type} -> a -> IO () +setThreadData : {a : Type} -> a -> JVM_IO () setThreadData val = schemeCall () "blodwen-set-thread-data" [val] export -getThreadData : (a : Type) -> IO a +getThreadData : (a : Type) -> JVM_IO a getThreadData a = schemeCall a "blodwen-get-thread-data" [] export data Mutex : Type where export -makeMutex : IO Mutex +makeMutex : JVM_IO Mutex makeMutex = schemeCall Mutex "blodwen-mutex" [] export -mutexAcquire : Mutex -> IO () +mutexAcquire : Mutex -> JVM_IO () mutexAcquire m = schemeCall () "blodwen-lock" [m] export -mutexRelease : Mutex -> IO () +mutexRelease : Mutex -> JVM_IO () mutexRelease m = schemeCall () "blodwen-unlock" [m] export data Condition : Type where export -makeCondition : IO Condition +makeCondition : JVM_IO Condition makeCondition = schemeCall Condition "blodwen-condition" [] export -conditionWait : Condition -> Mutex -> IO () +conditionWait : Condition -> Mutex -> JVM_IO () conditionWait c m = schemeCall () "blodwen-condition-wait" [c, m] export -conditionWaitTimeout : Condition -> Mutex -> Int -> IO () +conditionWaitTimeout : Condition -> Mutex -> Int -> JVM_IO () conditionWaitTimeout c m t = schemeCall () "blodwen-condition-wait-timeout" [c, m, t] export -conditionSignal : Condition -> IO () +conditionSignal : Condition -> JVM_IO () conditionSignal c = schemeCall () "blodwen-condition-signal" [c] export -conditionBroadcast : Condition -> IO () +conditionBroadcast : Condition -> JVM_IO () conditionBroadcast c = schemeCall () "blodwen-condition-broadcast" [c] diff --git a/libs/base/System/File.idr b/libs/base/System/File.idr index f660fef0f..f3903aff9 100644 --- a/libs/base/System/File.idr +++ b/libs/base/System/File.idr @@ -50,7 +50,7 @@ toFileError 3 = FileNotFound toFileError 4 = PermissionDenied toFileError x = GenericFileError x -fpure : Either Int a -> IO (Either FileError a) +fpure : Either Int a -> JVM_IO (Either FileError a) fpure (Left err) = pure (Left (toFileError err)) fpure (Right x) = pure (Right x) @@ -79,45 +79,45 @@ stderr : File stderr = FHandle prim__stderr export -openFile : String -> Mode -> IO (Either FileError File) +openFile : String -> Mode -> JVM_IO (Either FileError File) openFile f m = do res <- primIO (prim__open f (modeStr m) 0) fpure (map FHandle res) export -openBinaryFile : String -> Mode -> IO (Either FileError BinaryFile) +openBinaryFile : String -> Mode -> JVM_IO (Either FileError BinaryFile) openBinaryFile f m = do res <- primIO (prim__open f (modeStr m) 1) fpure (map FHandle res) export -closeFile : FileT t -> IO () +closeFile : FileT t -> JVM_IO () closeFile (FHandle f) = primIO (prim__close f) export -fGetLine : (h : File) -> IO (Either FileError String) +fGetLine : (h : File) -> JVM_IO (Either FileError String) fGetLine (FHandle f) = do res <- primIO (prim__readLine f) fpure res export -fPutStr : (h : File) -> String -> IO (Either FileError ()) +fPutStr : (h : File) -> String -> JVM_IO (Either FileError ()) fPutStr (FHandle f) str = do res <- primIO (prim__writeLine f str) fpure res export -fPutStrLn : (h : File) -> String -> IO (Either FileError ()) +fPutStrLn : (h : File) -> String -> JVM_IO (Either FileError ()) fPutStrLn f str = fPutStr f (str ++ "\n") export -fEOF : (h : File) -> IO Bool +fEOF : (h : File) -> JVM_IO Bool fEOF (FHandle f) = do res <- primIO (prim__eof f) pure (res /= 0) export -readFile : String -> IO (Either FileError String) +readFile : String -> JVM_IO (Either FileError String) readFile file = do Right h <- openFile file Read | Left err => pure (Left err) @@ -127,7 +127,7 @@ readFile file closeFile h pure (Right (fastAppend content)) where - read : List String -> File -> IO (Either FileError (List String)) + read : List String -> File -> JVM_IO (Either FileError (List String)) read acc h = do eof <- fEOF h if eof diff --git a/libs/base/System/REPL.idr b/libs/base/System/REPL.idr index fa23b8052..503a70ec1 100644 --- a/libs/base/System/REPL.idr +++ b/libs/base/System/REPL.idr @@ -9,7 +9,7 @@ import System.File ||| output and a new state. Returns Nothing if the repl should exit export replWith : (state : a) -> (prompt : String) -> - (onInput : a -> String -> Maybe (String, a)) -> IO () + (onInput : a -> String -> Maybe (String, a)) -> JVM_IO () replWith acc prompt fn = do putStr prompt eof <- fEOF stdin @@ -28,7 +28,7 @@ replWith acc prompt fn ||| output export repl : (prompt : String) -> - (onInput : String -> String) -> IO () + (onInput : String -> String) -> JVM_IO () repl prompt fn = replWith () prompt (\x, s => Just (fn s, ())) diff --git a/libs/network/Echo.idr b/libs/network/Echo.idr index b5a5a2438..64cc603d8 100644 --- a/libs/network/Echo.idr +++ b/libs/network/Echo.idr @@ -7,7 +7,7 @@ import Network.Socket.Raw %cg chez libidris_net.so -runServer : IO (Either String (Port, ThreadID)) +runServer : JVM_IO (Either String (Port, ThreadID)) runServer = do Right sock <- socket AF_INET Stream 0 | Left fail => pure (Left $ "Failed to open socket: " ++ show fail) @@ -24,7 +24,7 @@ runServer = do pure $ Right (port, forked) where - serve : Port -> Socket -> IO () + serve : Port -> Socket -> JVM_IO () serve port sock = do Right (s, _) <- accept sock | Left err => putStrLn ("Failed to accept on socket with error: " ++ show err) @@ -41,7 +41,7 @@ runServer = do -- putStrLn ("Server sent " ++ show n ++ " bytes") pure () -runClient : Port -> IO () +runClient : Port -> JVM_IO () runClient serverPort = do Right sock <- socket AF_INET Stream 0 | Left fail => putStrLn ("Failed to open socket: " ++ show fail) @@ -56,7 +56,7 @@ runClient serverPort = do | Left err => putStrLn ("Client failed to receive on socket with error: " ++ show err) putStrLn ("Received: " ++ str) -main : IO () +main : JVM_IO () main = do Right (serverPort, tid) <- runServer | Left err => putStrLn $ "[server] " ++ err diff --git a/libs/network/Network/Socket.idr b/libs/network/Network/Socket.idr index e255f584b..113186271 100644 --- a/libs/network/Network/Socket.idr +++ b/libs/network/Network/Socket.idr @@ -15,7 +15,7 @@ import Data.List socket : (fam : SocketFamily) -> (ty : SocketType) -> (pnum : ProtocolNumber) - -> IO (Either SocketError Socket) + -> JVM_IO (Either SocketError Socket) socket sf st pn = do socket_res <- cCall Int "idrnet_socket" [toCode sf, toCode st, pn] @@ -24,7 +24,7 @@ socket sf st pn = do else pure $ Right (MkSocket socket_res sf st pn) ||| Close a socket -close : Socket -> IO () +close : Socket -> JVM_IO () close sock = cCall () "close" [descriptor sock] ||| Binds a socket to the given socket address and port. @@ -32,7 +32,7 @@ close sock = cCall () "close" [descriptor sock] bind : (sock : Socket) -> (addr : Maybe SocketAddress) -> (port : Port) - -> IO Int + -> JVM_IO Int bind sock addr port = do bind_res <- cCall Int "idrnet_bind" [ descriptor sock, toCode $ family sock @@ -51,7 +51,7 @@ bind sock addr port = do connect : (sock : Socket) -> (addr : SocketAddress) -> (port : Port) - -> IO ResultCode + -> JVM_IO ResultCode connect sock addr port = do conn_res <- cCall Int "idrnet_connect" [ descriptor sock, toCode $ family sock, toCode $ socketType sock, show addr, port] @@ -63,7 +63,7 @@ connect sock addr port = do ||| Listens on a bound socket. ||| ||| @sock The socket to listen on. -listen : (sock : Socket) -> IO Int +listen : (sock : Socket) -> JVM_IO Int listen sock = do listen_res <- cCall Int "listen" [ descriptor sock, BACKLOG ] if listen_res == (-1) @@ -79,7 +79,7 @@ listen sock = do ||| ||| @sock The socket used to establish connection. accept : (sock : Socket) - -> IO (Either SocketError (Socket, SocketAddress)) + -> JVM_IO (Either SocketError (Socket, SocketAddress)) accept sock = do -- We need a pointer to a sockaddr structure. This is then passed into @@ -105,7 +105,7 @@ accept sock = do ||| @msg The data to send. send : (sock : Socket) -> (msg : String) - -> IO (Either SocketError ResultCode) + -> JVM_IO (Either SocketError ResultCode) send sock dat = do send_res <- cCall Int "idrnet_send" [ descriptor sock, dat ] @@ -124,7 +124,7 @@ send sock dat = do ||| @len How much of the data to receive. recv : (sock : Socket) -> (len : ByteLength) - -> IO (Either SocketError (String, ResultCode)) + -> JVM_IO (Either SocketError (String, ResultCode)) recv sock len = do -- Firstly make the request, get some kind of recv structure which -- contains the result of the recv and possibly the retrieved payload @@ -153,11 +153,11 @@ recv sock len = do ||| ||| @sock The socket on which to receive the message. partial -recvAll : (sock : Socket) -> IO (Either SocketError String) +recvAll : (sock : Socket) -> JVM_IO (Either SocketError String) recvAll sock = recvRec sock [] 64 where partial - recvRec : Socket -> List String -> ByteLength -> IO (Either SocketError String) + recvRec : Socket -> List String -> ByteLength -> JVM_IO (Either SocketError String) recvRec sock acc n = do res <- recv sock n case res of Left 0 => pure (Right $ concat $ reverse acc) @@ -178,7 +178,7 @@ sendTo : (sock : Socket) -> (addr : SocketAddress) -> (port : Port) -> (msg : String) - -> IO (Either SocketError ByteLength) + -> JVM_IO (Either SocketError ByteLength) sendTo sock addr p dat = do sendto_res <- cCall Int "idrnet_sendto" [ descriptor sock, dat, show addr, p ,toCode $ family sock ] @@ -200,7 +200,7 @@ sendTo sock addr p dat = do ||| recvFrom : (sock : Socket) -> (len : ByteLength) - -> IO (Either SocketError (UDPAddrInfo, String, ResultCode)) + -> JVM_IO (Either SocketError (UDPAddrInfo, String, ResultCode)) recvFrom sock bl = do recv_ptr <- cCall Ptr "idrnet_recvfrom" [ descriptor sock, bl ] diff --git a/libs/network/Network/Socket/Data.idr b/libs/network/Network/Socket/Data.idr index 70c4f1f44..905ec8bec 100644 --- a/libs/network/Network/Socket/Data.idr +++ b/libs/network/Network/Socket/Data.idr @@ -59,11 +59,11 @@ EAGAIN = -- ---------------------------------------------------------------- [ Error Code ] export -getErrno : IO SocketError +getErrno : JVM_IO SocketError getErrno = cCall Int "idrnet_errno" [] export -nullPtr : Ptr -> IO Bool +nullPtr : Ptr -> JVM_IO Bool nullPtr p = cCall Bool "isNull" [p] -- -------------------------------------------------------------- [ Interfaces ] diff --git a/libs/network/Network/Socket/Raw.idr b/libs/network/Network/Socket/Raw.idr index 41515f38b..e02cbde6e 100644 --- a/libs/network/Network/Socket/Raw.idr +++ b/libs/network/Network/Socket/Raw.idr @@ -24,28 +24,28 @@ data SockaddrPtr = SAPtr Ptr -- ---------------------------------------------------------- [ Socket Utilies ] ||| Frees a given pointer -sock_free : BufPtr -> IO () +sock_free : BufPtr -> JVM_IO () sock_free (BPtr ptr) = cCall () "idrnet_free" [ptr] export -sockaddr_free : SockaddrPtr -> IO () +sockaddr_free : SockaddrPtr -> JVM_IO () sockaddr_free (SAPtr ptr) = cCall () "idrnet_free" [ptr] ||| Allocates an amount of memory given by the ByteLength parameter. ||| ||| Used to allocate a mutable pointer to be given to the Recv functions. -sock_alloc : ByteLength -> IO BufPtr +sock_alloc : ByteLength -> JVM_IO BufPtr sock_alloc bl = map BPtr $ cCall Ptr "idrnet_malloc" [bl] ||| Retrieves the port the given socket is bound to export -getSockPort : Socket -> IO Port +getSockPort : Socket -> JVM_IO Port getSockPort sock = cCall Int "idrnet_sockaddr_port" [descriptor sock] ||| Retrieves a socket address from a sockaddr pointer export -getSockAddr : SockaddrPtr -> IO SocketAddress +getSockAddr : SockaddrPtr -> JVM_IO SocketAddress getSockAddr (SAPtr ptr) = do addr_family_int <- cCall Int "idrnet_sockaddr_family" [ptr] @@ -59,12 +59,12 @@ getSockAddr (SAPtr ptr) = do Just AF_UNSPEC => pure InvalidAddress) export -freeRecvStruct : RecvStructPtr -> IO () +freeRecvStruct : RecvStructPtr -> JVM_IO () freeRecvStruct (RSPtr p) = cCall () "idrnet_free_recv_struct" [p] ||| Utility to extract data. export -freeRecvfromStruct : RecvfromStructPtr -> IO () +freeRecvfromStruct : RecvfromStructPtr -> JVM_IO () freeRecvfromStruct (RFPtr p) = cCall () "idrnet_free_recvfrom_struct" [p] ||| Sends the data in a given memory location @@ -79,7 +79,7 @@ export sendBuf : (sock : Socket) -> (ptr : BufPtr) -> (len : ByteLength) - -> IO (Either SocketError ResultCode) + -> JVM_IO (Either SocketError ResultCode) sendBuf sock (BPtr ptr) len = do send_res <- cCall Int "idrnet_send_buf" [ descriptor sock, ptr, len] @@ -99,7 +99,7 @@ export recvBuf : (sock : Socket) -> (ptr : BufPtr) -> (len : ByteLength) - -> IO (Either SocketError ResultCode) + -> JVM_IO (Either SocketError ResultCode) recvBuf sock (BPtr ptr) len = do recv_res <- cCall Int "idrnet_recv_buf" [ descriptor sock, ptr, len ] @@ -123,7 +123,7 @@ sendToBuf : (sock : Socket) -> (port : Port) -> (ptr : BufPtr) -> (len : ByteLength) - -> IO (Either SocketError ResultCode) + -> JVM_IO (Either SocketError ResultCode) sendToBuf sock addr p (BPtr dat) len = do sendto_res <- cCall Int "idrnet_sendto_buf" [ descriptor sock, dat, len, show addr, p, toCode $ family sock ] @@ -134,19 +134,19 @@ sendToBuf sock addr p (BPtr dat) len = do ||| Utility function to get the payload of the sent message as a `String`. export -foreignGetRecvfromPayload : RecvfromStructPtr -> IO String +foreignGetRecvfromPayload : RecvfromStructPtr -> JVM_IO String foreignGetRecvfromPayload (RFPtr p) = cCall String "idrnet_get_recvfrom_payload" [ p ] ||| Utility function to return senders socket address. export -foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress +foreignGetRecvfromAddr : RecvfromStructPtr -> JVM_IO SocketAddress foreignGetRecvfromAddr (RFPtr p) = do sockaddr_ptr <- map SAPtr $ cCall Ptr "idrnet_get_recvfrom_sockaddr" [p] getSockAddr sockaddr_ptr ||| Utility function to return sender's IPV4 port. export -foreignGetRecvfromPort : RecvfromStructPtr -> IO Port +foreignGetRecvfromPort : RecvfromStructPtr -> JVM_IO Port foreignGetRecvfromPort (RFPtr p) = do sockaddr_ptr <- cCall Ptr "idrnet_get_recvfrom_sockaddr" [p] port <- cCall Int "idrnet_sockaddr_ipv4_port" [sockaddr_ptr] @@ -167,7 +167,7 @@ export recvFromBuf : (sock : Socket) -> (ptr : BufPtr) -> (len : ByteLength) - -> IO (Either SocketError (UDPAddrInfo, ResultCode)) + -> JVM_IO (Either SocketError (UDPAddrInfo, ResultCode)) recvFromBuf sock (BPtr ptr) bl = do recv_ptr <- cCall Ptr "idrnet_recvfrom_buf" [ descriptor sock, ptr, bl] diff --git a/libs/prelude/Prelude.idr b/libs/prelude/Prelude.idr index 5c8b571b4..3aba6ceda 100644 --- a/libs/prelude/Prelude.idr +++ b/libs/prelude/Prelude.idr @@ -1109,15 +1109,15 @@ Show a => Show (Maybe a) where showPrec d (Just x) = showCon d "Just" (showArg x) -------- --- IO -- +-- JVM_IO -- -------- public export -Functor IO where +Functor JVM_IO where map f io = io_bind io (\b => io_pure (f b)) public export -Applicative IO where +Applicative JVM_IO where pure x = io_pure x f <*> a = io_bind f (\f' => @@ -1125,15 +1125,15 @@ Applicative IO where io_pure (f' a'))) public export -Monad IO where +Monad JVM_IO where b >>= k = io_bind b k export -print : Show a => a -> IO () +print : Show a => a -> JVM_IO () print x = putStr $ show x export -printLn : Show a => a -> IO () +printLn : Show a => a -> JVM_IO () printLn x = putStrLn $ show x ----------------------- diff --git a/libs/prelude/PrimIO.idr b/libs/prelude/PrimIO.idr index 55f719be2..7f7bd6b6e 100644 --- a/libs/prelude/PrimIO.idr +++ b/libs/prelude/PrimIO.idr @@ -7,19 +7,19 @@ data IORes : Type -> Type where MkIORes : (result : a) -> (1 x : %World) -> IORes a export -data IO : Type -> Type where - MkIO : (1 fn : (1 x : %World) -> IORes a) -> IO a +data JVM_IO : Type -> Type where + MkJVM_IO : (1 fn : (1 x : %World) -> IORes a) -> JVM_IO a export -io_pure : a -> IO a -io_pure x = MkIO (\w => MkIORes x w) +io_pure : a -> JVM_IO a +io_pure x = MkJVM_IO (\w => MkIORes x w) export -io_bind : (1 act : IO a) -> (1 k : a -> IO b) -> IO b -io_bind (MkIO fn) - = \k => MkIO (\w => let MkIORes x' w' = fn w - MkIO res = k x' in - res w') +io_bind : (1 act : JVM_IO a) -> (1 k : a -> JVM_IO b) -> JVM_IO b +io_bind (MkJVM_IO fn) + = \k => MkJVM_IO (\w => let MkIORes x' w' = fn w + MkJVM_IO res = k x' in + res w') %extern prim__putStr : String -> (1 x : %World) -> IORes () %extern prim__getStr : (1 x : %World) -> IORes String @@ -41,32 +41,32 @@ data FArgList : Type where (1 x : %World) -> IORes ret export %inline -primIO : (1 fn : (1 x : %World) -> IORes a) -> IO a -primIO op = MkIO op +primIO : (1 fn : (1 x : %World) -> IORes a) -> JVM_IO a +primIO op = MkJVM_IO op export %inline -schemeCall : (ret : Type) -> String -> (1 args : FArgList) -> IO ret +schemeCall : (ret : Type) -> String -> (1 args : FArgList) -> JVM_IO ret schemeCall ret fn args = primIO (prim__schemeCall ret fn args) export %inline -cCall : (ret : Type) -> String -> FArgList -> IO ret +cCall : (ret : Type) -> String -> FArgList -> JVM_IO ret cCall ret fn args = primIO (prim__cCall ret fn args) export -putStr : String -> IO () +putStr : String -> JVM_IO () putStr str = primIO (prim__putStr str) export -putStrLn : String -> IO () +putStrLn : String -> JVM_IO () putStrLn str = putStr (prim__strAppend str "\n") export -getLine : IO String +getLine : JVM_IO String getLine = primIO prim__getStr export -fork : (1 prog : IO ()) -> IO ThreadID -fork (MkIO act) = schemeCall ThreadID "blodwen-thread" [act] +fork : (1 prog : JVM_IO ()) -> JVM_IO ThreadID +fork (MkJVM_IO act) = schemeCall ThreadID "blodwen-thread" [act] unsafeCreateWorld : (1 f : (1 x : %World) -> a) -> a unsafeCreateWorld f = f %MkWorld @@ -75,7 +75,7 @@ unsafeDestroyWorld : (1 x : %World) -> a -> a unsafeDestroyWorld %MkWorld x = x export -unsafePerformIO : IO a -> a -unsafePerformIO (MkIO f) +unsafePerformIO : JVM_IO a -> a +unsafePerformIO (MkJVM_IO f) = unsafeCreateWorld (\w => case f w of MkIORes res w' => unsafeDestroyWorld w' res) diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index 28dcc5761..42649ac5f 100644 --- a/src/Compiler/Common.idr +++ b/src/Compiler/Common.idr @@ -8,7 +8,8 @@ import Core.TT import Data.NameMap -%include C "sys/stat.h" +import IdrisJvm.IO +import IdrisJvm.File ||| Generic interface to some code generator public export @@ -104,7 +105,7 @@ findUsedNames tm ||| check to see if a given file exists export -exists : String -> IO Bool +exists : String -> JVM_IO Bool exists f = do Right ok <- openFile f Read | Left err => pure False @@ -113,10 +114,12 @@ exists f ||| generate a temporary file/name export -tmpName : IO String -tmpName = foreign FFI_C "tmpnam" (Ptr -> IO String) null +tmpName : JVM_IO String +tmpName = getTemporaryFileName +{- ||| change the access rights for a file export -chmod : String -> Int -> IO () -chmod f m = foreign FFI_C "chmod" (String -> Int -> IO ()) f m +chmod : String -> Int -> JVM_IO () +chmod f m = foreign FFI_C "chmod" (String -> Int -> JVM_IO ()) f m +-} \ No newline at end of file diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index 8c894f7b3..57103a04c 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -13,16 +13,20 @@ import Core.TT import Data.NameMap import Data.Vect -import System +-- import System import System.Info +import IdrisJvm.IO +import IdrisJvm.File +import IdrisJvm.System + %default covering -firstExists : List String -> IO (Maybe String) +firstExists : List String -> JVM_IO (Maybe String) firstExists [] = pure Nothing firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs -findChez : IO String +findChez : JVM_IO String findChez = do env <- getEnv "CHEZ" case env of diff --git a/src/Compiler/Scheme/Chicken.idr b/src/Compiler/Scheme/Chicken.idr index dbbcf0443..999143760 100644 --- a/src/Compiler/Scheme/Chicken.idr +++ b/src/Compiler/Scheme/Chicken.idr @@ -16,16 +16,20 @@ import Data.Vect import System import System.Info +import IdrisJvm.IO +import IdrisJvm.File +import IdrisJvm.System + %default covering -firstExists : List String -> IO (Maybe String) +firstExists : List String -> JVM_IO (Maybe String) firstExists [] = pure Nothing firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs -findCSI : IO String +findCSI : JVM_IO String findCSI = pure "/usr/bin/env csi" -findCSC : IO String +findCSC : JVM_IO 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 0fec85091..4c59d2797 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -15,16 +15,20 @@ import Data.Vect import System import System.Info +import IdrisJvm.IO +import IdrisJvm.File +import IdrisJvm.System + %default covering -firstExists : List String -> IO (Maybe String) +firstExists : List String -> JVM_IO (Maybe String) firstExists [] = pure Nothing firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs -findRacket : IO String +findRacket : JVM_IO String findRacket = pure "/usr/bin/env racket" -findRacoExe : IO String +findRacoExe : JVM_IO String findRacoExe = pure "raco exe" schHeader : String diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 8b9acbe76..a3dad548c 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -19,7 +19,8 @@ import Data.NameMap import public Utils.Binary -import Data.Buffer +import IdrisJvm.IO +import IdrisJvm.Data.Buffer %default covering diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 5ab2578f9..a6dd6fa67 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -16,7 +16,11 @@ import Data.NameMap import Data.StringMap import Data.IntMap -import System +import IdrisJvm.IO +import IdrisJvm.File +import IdrisJvm.System + +%hide Prelude.File.changeDir %default covering @@ -406,7 +410,7 @@ commitCtxt ctxt where -- We know the array must be big enough, because it will have been resized -- if necessary in the branch to fit the index we've been given here - commitStaged : List (Int, ContextEntry) -> IOArray ContextEntry -> IO () + commitStaged : List (Int, ContextEntry) -> IOArray ContextEntry -> JVM_IO () commitStaged [] arr = pure () commitStaged ((idx, val) :: rest) arr = do writeArray arr idx val diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 48d2bd792..c3e795ba9 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -5,8 +5,10 @@ import Core.TT import Parser.Support import public Control.Catchable -import public Data.IORef -import System +import public IdrisJvm.Data.IORef +import IdrisJvm.IO +import IdrisJvm.File +import IdrisJvm.System %default covering @@ -308,15 +310,15 @@ getErrorLoc (InCon x y err) = getErrorLoc err getErrorLoc (InLHS x y err) = getErrorLoc err getErrorLoc (InRHS x y err) = getErrorLoc err --- Core is a wrapper around IO that is specialised for efficiency. +-- Core is a wrapper around JVM_IO that is specialised for efficiency. export record Core t where constructor MkCore - runCore : IO (Either Error t) + runCore : JVM_IO (Either Error t) export coreRun : Core a -> - (Error -> IO b) -> (a -> IO b) -> IO b + (Error -> JVM_IO b) -> (a -> JVM_IO b) -> JVM_IO b coreRun (MkCore act) err ok = either err ok !act @@ -332,10 +334,10 @@ wrapError fe (MkCore prog) Left err => pure (Left (fe err)) Right val => pure (Right val))) --- This would be better if we restrict it to a limited set of IO operations +-- This would be better if we restrict it to a limited set of JVM_IO operations export %inline -coreLift : IO a -> Core a +coreLift : JVM_IO a -> Core a coreLift op = MkCore (do op' <- op pure (Right op')) diff --git a/src/Core/Directory.idr b/src/Core/Directory.idr index d27f370a3..106aaff63 100644 --- a/src/Core/Directory.idr +++ b/src/Core/Directory.idr @@ -8,6 +8,9 @@ import Core.Options import System.Info +import IdrisJvm.IO +import IdrisJvm.File + %default total isWindows : Bool @@ -124,7 +127,7 @@ pathToNS wdir fname -- Create subdirectories, if they don't exist export -mkdirs : List String -> IO (Either FileError ()) +mkdirs : List String -> JVM_IO (Either FileError ()) mkdirs [] = pure (Right ()) mkdirs (d :: ds) = do ok <- changeDir d diff --git a/src/Core/Metadata.idr b/src/Core/Metadata.idr index e72c02156..ef6444eb5 100644 --- a/src/Core/Metadata.idr +++ b/src/Core/Metadata.idr @@ -9,6 +9,8 @@ import Core.Normalise import Core.TT import Core.TTC +import IdrisJvm.IO + -- Additional data we keep about the context to support interactive editing public export diff --git a/src/Core/Normalise.idr b/src/Core/Normalise.idr index 2da26cca7..b06877fcd 100644 --- a/src/Core/Normalise.idr +++ b/src/Core/Normalise.idr @@ -12,6 +12,8 @@ import Core.Value import Data.IntMap import Data.Vect +import IdrisJvm.IO + %default covering -- A pair of a term and its normal form. This could be constructed either diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index c0ee3a5ce..d6331e91f 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -15,6 +15,15 @@ import Data.Vect import Utils.Binary +import IdrisJvm.Data.Buffer +import IdrisJvm.IO +import IdrisJvm.File + +%default total +%hide Prelude.File.File +%hide Prelude.File.FileError +%hide Prelude.File.openFile + %default covering export diff --git a/src/Data/IOArray.idr b/src/Data/IOArray.idr index 96d5a289c..2ec1dbd3d 100644 --- a/src/Data/IOArray.idr +++ b/src/Data/IOArray.idr @@ -1,5 +1,9 @@ module Data.IOArray +import IdrisJvm.IO +import Java.Lang +import Java.Util + %default total -- Raw access to IOArrays. This interface is unsafe because there's no @@ -16,36 +20,28 @@ data IORawArray elem = MkIORawArray (ArrayData elem) ||| Create a new array of the given size, with all entries set to the ||| given default element. export -newRawArray : Int -> elem -> IO (IORawArray elem) -newRawArray size default - = do vm <- getMyVM - MkRaw p <- foreign FFI_C "idris_newArray" - (Ptr -> Int -> Raw elem -> IO (Raw (ArrayData elem))) - vm size (MkRaw default) - pure (MkIORawArray p) +newRawArray : Int -> elem -> JVM_IO (IORawArray elem) +newRawArray size default = do + arr <- listToArray $ replicate (cast size) (the Object $ believe_me default) + pure (MkIORawArray (believe_me arr)) ||| Write an element at a location in an array. ||| There is *no* bounds checking, hence this is unsafe. Safe interfaces can ||| be implemented on top of this, either with a run time or compile time ||| check. export -unsafeWriteArray : IORawArray elem -> Int -> elem -> IO () -unsafeWriteArray (MkIORawArray p) i val - = foreign FFI_C "idris_arraySet" - (Raw (ArrayData elem) -> Int -> Raw elem -> IO ()) - (MkRaw p) i (MkRaw val) +unsafeWriteArray : IORawArray elem -> Int -> elem -> JVM_IO () +unsafeWriteArray (MkIORawArray arr) i val + = assert_total $ setArray (JVM_Array Object -> Int -> Object -> JVM_IO ()) (believe_me arr) i (believe_me val) -||| Read the element at a location in an array. +||| Read the element at a location in an array. ||| There is *no* bounds checking, hence this is unsafe. Safe interfaces can ||| be implemented on top of this, either with a run time or compile time ||| check. export -unsafeReadArray : IORawArray elem -> Int -> IO elem -unsafeReadArray (MkIORawArray p) i - = do MkRaw val <- foreign FFI_C "idris_arrayGet" - (Raw (ArrayData elem) -> Int -> IO (Raw elem)) - (MkRaw p) i - pure val +unsafeReadArray : IORawArray elem -> Int -> JVM_IO elem +unsafeReadArray (MkIORawArray arr) i + = assert_total $ believe_me <$> getArray (JVM_Array Object -> Int -> JVM_IO Object) (believe_me arr) i -- As IORawArray, but wrapped in dynamic checks that elements exist and -- are in bounds @@ -56,19 +52,19 @@ record IOArray elem where content : IORawArray (Maybe elem) export -newArray : Int -> IO (IOArray elem) +newArray : Int -> JVM_IO (IOArray elem) newArray size = pure (MkIOArray size !(newRawArray size Nothing)) export -writeArray : IOArray elem -> Int -> elem -> IO () +writeArray : IOArray elem -> Int -> elem -> JVM_IO () writeArray arr pos el = if pos < 0 || pos >= max arr then pure () else unsafeWriteArray (content arr) pos (Just el) export -readArray : IOArray elem -> Int -> IO (Maybe elem) +readArray : IOArray elem -> Int -> JVM_IO (Maybe elem) readArray arr pos = if pos < 0 || pos >= max arr then pure Nothing @@ -77,7 +73,7 @@ readArray arr pos -- Make a new array of the given size with the elements copied from the -- other array export -newArrayCopy : (newsize : Int) -> IOArray elem -> IO (IOArray elem) +newArrayCopy : (newsize : Int) -> IOArray elem -> JVM_IO (IOArray elem) newArrayCopy newsize arr = do let newsize' = if newsize < max arr then max arr else newsize arr' <- newArray newsize' @@ -86,7 +82,7 @@ newArrayCopy newsize arr where copyFrom : IORawArray (Maybe elem) -> IORawArray (Maybe elem) -> - Int -> IO () + Int -> JVM_IO () copyFrom old new pos = if pos < 0 then pure () @@ -95,10 +91,10 @@ newArrayCopy newsize arr assert_total (copyFrom old new (pos - 1)) export -toList : IOArray elem -> IO (List (Maybe elem)) +toList : IOArray elem -> JVM_IO (List (Maybe elem)) toList arr = iter 0 (max arr) [] where - iter : Int -> Int -> List (Maybe elem) -> IO (List (Maybe elem)) + iter : Int -> Int -> List (Maybe elem) -> JVM_IO (List (Maybe elem)) iter pos end acc = if pos >= end then pure (reverse acc) @@ -106,13 +102,13 @@ toList arr = iter 0 (max arr) [] assert_total (iter (pos + 1) end (el :: acc)) export -fromList : List (Maybe elem) -> IO (IOArray elem) +fromList : List (Maybe elem) -> JVM_IO (IOArray elem) fromList ns = do arr <- newArray (cast (length ns)) addToArray 0 ns arr pure arr where - addToArray : Int -> List (Maybe elem) -> IOArray elem -> IO () + addToArray : Int -> List (Maybe elem) -> IOArray elem -> JVM_IO () addToArray loc [] arr = pure () addToArray loc (Nothing :: ns) arr = assert_total (addToArray (loc + 1) ns arr) diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index ea6157acb..7ec994d9f 100644 --- a/src/Idris/CommandLine.idr +++ b/src/Idris/CommandLine.idr @@ -1,5 +1,8 @@ module Idris.CommandLine +import IdrisJvm.IO +import IdrisJvm.System + %default total public export @@ -178,7 +181,7 @@ getOpts opts = parseOpts options opts export covering -getCmdOpts : IO (Either String (List CLOpt)) +getCmdOpts : JVM_IO (Either String (List CLOpt)) getCmdOpts = do (_ :: opts) <- getArgs | pure (Left "Invalid command line") pure $ getOpts opts diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index 6d2986063..51cc93c97 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -11,6 +11,9 @@ import Idris.Syntax import Parser.Support +import IdrisJvm.IO +import IdrisJvm.File + %default covering pshow : {auto c : Ref Ctxt Defs} -> diff --git a/src/Idris/IDEMode/CaseSplit.idr b/src/Idris/IDEMode/CaseSplit.idr index 44b2af783..4fefa298a 100644 --- a/src/Idris/IDEMode/CaseSplit.idr +++ b/src/Idris/IDEMode/CaseSplit.idr @@ -15,6 +15,9 @@ import Idris.REPLOpts import Idris.Resugar import Idris.Syntax +import IdrisJvm.IO +import IdrisJvm.File + %default covering getLine : Nat -> List String -> Maybe String diff --git a/src/Idris/IDEMode/Commands.idr b/src/Idris/IDEMode/Commands.idr index ac56125da..25341a1e5 100644 --- a/src/Idris/IDEMode/Commands.idr +++ b/src/Idris/IDEMode/Commands.idr @@ -4,6 +4,12 @@ import Core.Core import Core.Name import public Idris.REPLOpts +import IdrisJvm.IO +import IdrisJvm.File +import Java.Lang + +%hide Prelude.File.File + %default covering public export @@ -147,12 +153,12 @@ export version : Int -> Int -> SExp version maj min = toSExp (SymbolAtom "protocol-version", maj, min) -hex : File -> Int -> IO () -hex (FHandle h) num = foreign FFI_C "fprintf" (Ptr -> String -> Int -> IO ()) h "%06x" num +hex : File -> Int -> JVM_IO () +hex file num = writeString file $ + JavaString.format "%06x" !(listToArray [the Object $ believe_me $ JInteger.valueOf num]) -sendLine : File -> String -> IO () -sendLine (FHandle h) st = - map (const ()) (prim_fwrite h st) +sendLine : File -> String -> JVM_IO () +sendLine file st = writeString file st export send : SExpable a => File -> a -> Core () diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index 124bd6d41..d048c251f 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -32,47 +32,30 @@ import TTImp.TTImp import TTImp.ProcessDecls import Control.Catchable -import System -import Idris.Socket -import Idris.Socket.Data +-- import System +-- import Idris.Socket +-- import Idris.Socket.Data +import IdrisJvm.IO +import IdrisJvm.File +import IdrisJvm.System + +{- export -socketToFile : Socket -> IO (Either String File) +socketToFile : Socket -> JVM_IO (Either String File) socketToFile (MkSocket f _ _ _) = do - file <- map FHandle $ foreign FFI_C "fdopen" (Int -> String -> IO Ptr) f "r+" + file <- map FHandle $ foreign FFI_C "fdopen" (Int -> String -> JVM_IO Ptr) f "r+" if !(ferror file) then do pure (Left "Failed to fdopen socket file descriptor") else pure (Right file) - +-} + export -initIDESocketFile : Int -> IO (Either String File) -initIDESocketFile p = do - osock <- socket AF_INET Stream 0 - case osock of - Left fail => do - putStrLn (show fail) - putStrLn "Failed to open socket" - exit 1 - Right sock => do - res <- bind sock (Just (Hostname "localhost")) p - if res /= 0 - then - pure (Left ("Failed to bind socket with error: " ++ show res)) - else do - res <- listen sock - if res /= 0 - then - pure (Left ("Failed to listen on socket with error: " ++ show res)) - else do - putStrLn (show p) - res <- accept sock - case res of - Left err => - pure (Left ("Failed to accept on socket with error: " ++ show err)) - Right (s, _) => - socketToFile s +initIDESocketFile : Int -> JVM_IO (Either String File) +initIDESocketFile p = socketListenAndAccept p -getChar : File -> IO Char +{- +getChar : File -> JVM_IO Char getChar (FHandle h) = do if !(fEOF (FHandle h)) then do putStrLn "Alas the file is done, aborting" @@ -83,16 +66,12 @@ getChar (FHandle h) = do putStrLn "Failed to read a character" exit 1 else pure chr - -getFLine : File -> IO String -getFLine (FHandle h) = do - str <- prim_fread h - if !(ferror (FHandle h)) then do - putStrLn "Failed to read a line" - exit 1 - else pure str +-} + +getFLine : File -> JVM_IO String +getFLine file = getLine file -getNChars : File -> Nat -> IO (List Char) +getNChars : File -> Nat -> JVM_IO (List Char) getNChars i Z = pure [] getNChars i (S k) = do x <- getChar i @@ -125,7 +104,7 @@ toHex m (d :: ds) -- Read 6 characters. If they're a hex number, read that many characters. -- Otherwise, just read to newline -getInput : File -> IO String +getInput : File -> JVM_IO String getInput f = do x <- getNChars f 6 case toHex 1 (reverse x) of diff --git a/src/Idris/Main.idr b/src/Idris/Main.idr index f46f9069d..4c868d5be 100644 --- a/src/Idris/Main.idr +++ b/src/Idris/Main.idr @@ -20,15 +20,19 @@ import Idris.REPL import Idris.SetOptions import Idris.Syntax -import Idris.Socket -import Idris.Socket.Data +-- import Idris.Socket +-- import Idris.Socket.Data import Data.Vect -import System +-- import System import Yaffle.Main import YafflePaths +import IdrisJvm.IO +import IdrisJvm.System +import IdrisJvm.File + %default covering findInput : List CLOpt -> Maybe String @@ -166,7 +170,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 -> JVM_IO Bool quitOpts [] = pure True quitOpts (Version :: _) = do putStrLn versionMsg @@ -179,7 +183,7 @@ quitOpts (ShowPrefix :: _) pure False quitOpts (_ :: opts) = quitOpts opts -main : IO () +main : JVM_IO () main = do Right opts <- getCmdOpts | Left err => do putStrLn err diff --git a/src/Idris/ModTree.idr b/src/Idris/ModTree.idr index 18c6b4ead..f2914a993 100644 --- a/src/Idris/ModTree.idr +++ b/src/Idris/ModTree.idr @@ -17,6 +17,9 @@ import Idris.ProcessIdr import Idris.REPLCommon import Idris.Syntax +import IdrisJvm.IO +import IdrisJvm.File + %default covering record ModTree where diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index dd8e5295b..38e6b364e 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -20,9 +20,15 @@ import Parser.Lexer import Parser.Support import Utils.Binary -import System +-- import System import Text.Parser +import IdrisJvm.IO +import IdrisJvm.System +import IdrisJvm.File + +%hide Prelude.File.GenericFileError + %default covering record PkgDesc where @@ -224,7 +230,7 @@ build pkg runScript (postbuild pkg) pure [] -copyFile : String -> String -> IO (Either FileError ()) +copyFile : String -> String -> JVM_IO (Either FileError ()) copyFile src dest = do Right buf <- readFromFile src | Left err => pure (Left err) @@ -336,8 +342,7 @@ clean pkg where delete : String -> Core () delete path = do True <- coreLift $ fRemove path - | False => do err <- coreLift getErrno - coreLift $ putStrLn $ path ++ ": " ++ show (GenericFileError err) + | False => do coreLift $ putStrLn $ path ++ ": " ++ show (GenericFileError (-1)) coreLift $ putStrLn $ "Removed: " ++ path deleteFolder : String -> List String -> Core () deleteFolder builddir ns = delete $ builddir ++ dirSep ++ showSep "/" (reverse ns) diff --git a/src/Idris/ProcessIdr.idr b/src/Idris/ProcessIdr.idr index c23681014..3af2ff0a6 100644 --- a/src/Idris/ProcessIdr.idr +++ b/src/Idris/ProcessIdr.idr @@ -22,6 +22,9 @@ import Data.NameMap import Control.Catchable +import IdrisJvm.IO +import IdrisJvm.File + processDecl : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> {auto s : Ref Syn SyntaxInfo} -> diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 75ad18007..271e64edd 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -42,7 +42,11 @@ import TTImp.ProcessDecls import Control.Catchable import Data.NameMap -import System +import IdrisJvm.System + +import IdrisJvm.IO +import IdrisJvm.File +import IdrisJvm.System %default covering diff --git a/src/Idris/REPLCommon.idr b/src/Idris/REPLCommon.idr index a31ae5723..98c5fce89 100644 --- a/src/Idris/REPLCommon.idr +++ b/src/Idris/REPLCommon.idr @@ -11,6 +11,8 @@ import Idris.IDEMode.Commands import public Idris.REPLOpts import Idris.Syntax +import IdrisJvm.IO +import IdrisJvm.File -- Output informational messages, unless quiet flag is set export diff --git a/src/Idris/REPLOpts.idr b/src/Idris/REPLOpts.idr index be35ff03b..a68bc3b68 100644 --- a/src/Idris/REPLOpts.idr +++ b/src/Idris/REPLOpts.idr @@ -1,7 +1,8 @@ module Idris.REPLOpts import Idris.Syntax -import Idris.Socket +-- import Idris.Socket +import IdrisJvm.File public export data OutputMode diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 6698acea9..769e70408 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 IdrisJvm.System +import IdrisJvm.IO -- TODO: Version numbers on dependencies export diff --git a/src/Idris/Socket.idr b/src/Idris/Socket.idr index b5fb5d64c..46a4de803 100644 --- a/src/Idris/Socket.idr +++ b/src/Idris/Socket.idr @@ -18,10 +18,10 @@ import Idris.Socket.Raw socket : (fam : SocketFamily) -> (ty : SocketType) -> (pnum : ProtocolNumber) - -> IO (Either SocketError Socket) + -> JVM_IO (Either SocketError Socket) socket sf st pn = do socket_res <- foreign FFI_C "idrnet_socket" - (Int -> Int -> Int -> IO Int) + (Int -> Int -> Int -> JVM_IO Int) (toCode sf) (toCode st) pn if socket_res == -1 @@ -29,18 +29,18 @@ socket sf st pn = do else pure $ Right (MkSocket socket_res sf st pn) ||| Close a socket -close : Socket -> IO () -close sock = foreign FFI_C "close" (Int -> IO ()) (descriptor sock) +close : Socket -> JVM_IO () +close sock = foreign FFI_C "close" (Int -> JVM_IO ()) (descriptor sock) ||| Binds a socket to the given socket address and port. ||| Returns 0 on success, an error code otherwise. bind : (sock : Socket) -> (addr : Maybe SocketAddress) -> (port : Port) - -> IO Int + -> JVM_IO Int bind sock addr port = do bind_res <- foreign FFI_C "idrnet_bind" - (Int -> Int -> Int -> String -> Int -> IO Int) + (Int -> Int -> Int -> String -> Int -> JVM_IO Int) (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (saString addr) port if bind_res == (-1) @@ -56,10 +56,10 @@ bind sock addr port = do connect : (sock : Socket) -> (addr : SocketAddress) -> (port : Port) - -> IO ResultCode + -> JVM_IO ResultCode connect sock addr port = do conn_res <- foreign FFI_C "idrnet_connect" - (Int -> Int -> Int -> String -> Int -> IO Int) + (Int -> Int -> Int -> String -> Int -> JVM_IO Int) (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port if conn_res == (-1) @@ -69,9 +69,9 @@ connect sock addr port = do ||| Listens on a bound socket. ||| ||| @sock The socket to listen on. -listen : (sock : Socket) -> IO Int +listen : (sock : Socket) -> JVM_IO Int listen sock = do - listen_res <- foreign FFI_C "listen" (Int -> Int -> IO Int) + listen_res <- foreign FFI_C "listen" (Int -> Int -> JVM_IO Int) (descriptor sock) BACKLOG if listen_res == (-1) then getErrno @@ -86,17 +86,17 @@ listen sock = do ||| ||| @sock The socket used to establish connection. accept : (sock : Socket) - -> IO (Either SocketError (Socket, SocketAddress)) + -> JVM_IO (Either SocketError (Socket, SocketAddress)) accept sock = do -- We need a pointer to a sockaddr structure. This is then passed into -- idrnet_accept and populated. We can then query it for the SocketAddr and free it. sockaddr_ptr <- foreign FFI_C "idrnet_create_sockaddr" - (IO Ptr) + (JVM_IO Ptr) accept_res <- foreign FFI_C "idrnet_accept" - (Int -> Ptr -> IO Int) + (Int -> Ptr -> JVM_IO Int) (descriptor sock) sockaddr_ptr if accept_res == (-1) then map Left getErrno @@ -115,10 +115,10 @@ accept sock = do ||| @msg The data to send. send : (sock : Socket) -> (msg : String) - -> IO (Either SocketError ResultCode) + -> JVM_IO (Either SocketError ResultCode) send sock dat = do send_res <- foreign FFI_C "idrnet_send" - (Int -> String -> IO Int) + (Int -> String -> JVM_IO Int) (descriptor sock) dat if send_res == (-1) @@ -136,15 +136,15 @@ send sock dat = do ||| @len How much of the data to receive. recv : (sock : Socket) -> (len : ByteLength) - -> IO (Either SocketError (String, ResultCode)) + -> JVM_IO (Either SocketError (String, ResultCode)) recv sock len = do -- Firstly make the request, get some kind of recv structure which -- contains the result of the recv and possibly the retrieved payload recv_struct_ptr <- foreign FFI_C "idrnet_recv" - (Int -> Int -> IO Ptr) + (Int -> Int -> JVM_IO Ptr) (descriptor sock) len recv_res <- foreign FFI_C "idrnet_get_recv_res" - (Ptr -> IO Int) + (Ptr -> JVM_IO Int) recv_struct_ptr if recv_res == (-1) @@ -159,7 +159,7 @@ recv sock len = do pure $ Left 0 else do payload <- foreign FFI_C "idrnet_get_recv_payload" - (Ptr -> IO String) + (Ptr -> JVM_IO String) recv_struct_ptr freeRecvStruct (RSPtr recv_struct_ptr) pure $ Right (payload, recv_res) @@ -171,11 +171,11 @@ recv sock len = do ||| ||| @sock The socket on which to receive the message. partial -recvAll : (sock : Socket) -> IO (Either SocketError String) +recvAll : (sock : Socket) -> JVM_IO (Either SocketError String) recvAll sock = recvRec sock [] 64 where partial - recvRec : Socket -> List String -> ByteLength -> IO (Either SocketError String) + recvRec : Socket -> List String -> ByteLength -> JVM_IO (Either SocketError String) recvRec sock acc n = do res <- recv sock n case res of Left 0 => pure (Right $ concat $ reverse acc) @@ -196,10 +196,10 @@ sendTo : (sock : Socket) -> (addr : SocketAddress) -> (port : Port) -> (msg : String) - -> IO (Either SocketError ByteLength) + -> JVM_IO (Either SocketError ByteLength) sendTo sock addr p dat = do sendto_res <- foreign FFI_C "idrnet_sendto" - (Int -> String -> String -> Int -> Int -> IO Int) + (Int -> String -> String -> Int -> Int -> JVM_IO Int) (descriptor sock) dat (show addr) p (toCode $ family sock) if sendto_res == (-1) @@ -219,10 +219,10 @@ sendTo sock addr p dat = do ||| recvFrom : (sock : Socket) -> (len : ByteLength) - -> IO (Either SocketError (UDPAddrInfo, String, ResultCode)) + -> JVM_IO (Either SocketError (UDPAddrInfo, String, ResultCode)) recvFrom sock bl = do recv_ptr <- foreign FFI_C "idrnet_recvfrom" - (Int -> Int -> IO Ptr) + (Int -> Int -> JVM_IO Ptr) (descriptor sock) bl let recv_ptr' = RFPtr recv_ptr @@ -231,7 +231,7 @@ recvFrom sock bl = do then map Left getErrno else do result <- foreign FFI_C "idrnet_get_recvfrom_res" - (Ptr -> IO Int) + (Ptr -> JVM_IO Int) recv_ptr if result == -1 then do diff --git a/src/Idris/Socket/Data.idr b/src/Idris/Socket/Data.idr index 02b9699b8..1b3de2df8 100644 --- a/src/Idris/Socket/Data.idr +++ b/src/Idris/Socket/Data.idr @@ -42,7 +42,7 @@ EAGAIN : Int EAGAIN = -- I'm sorry -- maybe - unsafePerformIO $ foreign FFI_C "idrnet_geteagain" (() -> IO Int) () + unsafePerformIO $ foreign FFI_C "idrnet_geteagain" (() -> JVM_IO Int) () -- -------------------------------------------------------------- [ Interfaces ] diff --git a/src/Idris/Socket/Raw.idr b/src/Idris/Socket/Raw.idr index 21e3075b7..90c88f80a 100644 --- a/src/Idris/Socket/Raw.idr +++ b/src/Idris/Socket/Raw.idr @@ -23,47 +23,47 @@ data SockaddrPtr = SAPtr Ptr -- ---------------------------------------------------------- [ Socket Utilies ] ||| Frees a given pointer -sock_free : BufPtr -> IO () -sock_free (BPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr +sock_free : BufPtr -> JVM_IO () +sock_free (BPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> JVM_IO ()) ptr -sockaddr_free : SockaddrPtr -> IO () -sockaddr_free (SAPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr +sockaddr_free : SockaddrPtr -> JVM_IO () +sockaddr_free (SAPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> JVM_IO ()) ptr ||| Allocates an amount of memory given by the ByteLength parameter. ||| ||| Used to allocate a mutable pointer to be given to the Recv functions. -sock_alloc : ByteLength -> IO BufPtr -sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl +sock_alloc : ByteLength -> JVM_IO BufPtr +sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> JVM_IO Ptr) bl ||| Retrieves a socket address from a sockaddr pointer -getSockAddr : SockaddrPtr -> IO SocketAddress +getSockAddr : SockaddrPtr -> JVM_IO SocketAddress getSockAddr (SAPtr ptr) = do addr_family_int <- foreign FFI_C "idrnet_sockaddr_family" - (Ptr -> IO Int) + (Ptr -> JVM_IO Int) ptr -- ASSUMPTION: Foreign call returns a valid int assert_total (case getSocketFamily addr_family_int of Just AF_INET => do ipv4_addr <- foreign FFI_C "idrnet_sockaddr_ipv4" - (Ptr -> IO String) + (Ptr -> JVM_IO String) ptr pure $ parseIPv4 ipv4_addr Just AF_INET6 => pure IPv6Addr Just AF_UNSPEC => pure InvalidAddress) -freeRecvStruct : RecvStructPtr -> IO () +freeRecvStruct : RecvStructPtr -> JVM_IO () freeRecvStruct (RSPtr p) = foreign FFI_C "idrnet_free_recv_struct" - (Ptr -> IO ()) + (Ptr -> JVM_IO ()) p ||| Utility to extract data. -freeRecvfromStruct : RecvfromStructPtr -> IO () +freeRecvfromStruct : RecvfromStructPtr -> JVM_IO () freeRecvfromStruct (RFPtr p) = foreign FFI_C "idrnet_free_recvfrom_struct" - (Ptr -> IO ()) + (Ptr -> JVM_IO ()) p ||| Sends the data in a given memory location @@ -77,10 +77,10 @@ freeRecvfromStruct (RFPtr p) = sendBuf : (sock : Socket) -> (ptr : BufPtr) -> (len : ByteLength) - -> IO (Either SocketError ResultCode) + -> JVM_IO (Either SocketError ResultCode) sendBuf sock (BPtr ptr) len = do send_res <- foreign FFI_C "idrnet_send_buf" - (Int -> Ptr -> Int -> IO Int) + (Int -> Ptr -> Int -> JVM_IO Int) (descriptor sock) ptr len if send_res == (-1) @@ -98,10 +98,10 @@ sendBuf sock (BPtr ptr) len = do recvBuf : (sock : Socket) -> (ptr : BufPtr) -> (len : ByteLength) - -> IO (Either SocketError ResultCode) + -> JVM_IO (Either SocketError ResultCode) recvBuf sock (BPtr ptr) len = do recv_res <- foreign FFI_C "idrnet_recv_buf" - (Int -> Ptr -> Int -> IO Int) + (Int -> Ptr -> Int -> JVM_IO Int) (descriptor sock) ptr len if (recv_res == (-1)) @@ -123,10 +123,10 @@ sendToBuf : (sock : Socket) -> (port : Port) -> (ptr : BufPtr) -> (len : ByteLength) - -> IO (Either SocketError ResultCode) + -> JVM_IO (Either SocketError ResultCode) sendToBuf sock addr p (BPtr dat) len = do sendto_res <- foreign FFI_C "idrnet_sendto_buf" - (Int -> Ptr -> Int -> String -> Int -> Int -> IO Int) + (Int -> Ptr -> Int -> String -> Int -> Int -> JVM_IO Int) (descriptor sock) dat len (show addr) p (toCode $ family sock) if sendto_res == (-1) @@ -134,28 +134,28 @@ sendToBuf sock addr p (BPtr dat) len = do else pure $ Right sendto_res ||| Utility function to get the payload of the sent message as a `String`. -foreignGetRecvfromPayload : RecvfromStructPtr -> IO String +foreignGetRecvfromPayload : RecvfromStructPtr -> JVM_IO String foreignGetRecvfromPayload (RFPtr p) = foreign FFI_C "idrnet_get_recvfrom_payload" - (Ptr -> IO String) + (Ptr -> JVM_IO String) p ||| Utility function to return senders socket address. -foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress +foreignGetRecvfromAddr : RecvfromStructPtr -> JVM_IO SocketAddress foreignGetRecvfromAddr (RFPtr p) = do sockaddr_ptr <- map SAPtr $ foreign FFI_C "idrnet_get_recvfrom_sockaddr" - (Ptr -> IO Ptr) + (Ptr -> JVM_IO Ptr) p getSockAddr sockaddr_ptr ||| Utility function to return sender's IPV4 port. -foreignGetRecvfromPort : RecvfromStructPtr -> IO Port +foreignGetRecvfromPort : RecvfromStructPtr -> JVM_IO Port foreignGetRecvfromPort (RFPtr p) = do sockaddr_ptr <- foreign FFI_C "idrnet_get_recvfrom_sockaddr" - (Ptr -> IO Ptr) + (Ptr -> JVM_IO Ptr) p port <- foreign FFI_C "idrnet_sockaddr_ipv4_port" - (Ptr -> IO Int) + (Ptr -> JVM_IO Int) sockaddr_ptr pure port @@ -173,10 +173,10 @@ foreignGetRecvfromPort (RFPtr p) = do recvFromBuf : (sock : Socket) -> (ptr : BufPtr) -> (len : ByteLength) - -> IO (Either SocketError (UDPAddrInfo, ResultCode)) + -> JVM_IO (Either SocketError (UDPAddrInfo, ResultCode)) recvFromBuf sock (BPtr ptr) bl = do recv_ptr <- foreign FFI_C "idrnet_recvfrom_buf" - (Int -> Ptr -> Int -> IO Ptr) + (Int -> Ptr -> Int -> JVM_IO Ptr) (descriptor sock) ptr bl let recv_ptr' = RFPtr recv_ptr @@ -185,7 +185,7 @@ recvFromBuf sock (BPtr ptr) bl = do then map Left getErrno else do result <- foreign FFI_C "idrnet_get_recvfrom_res" - (Ptr -> IO Int) + (Ptr -> JVM_IO Int) recv_ptr if result == -1 then do diff --git a/src/Parser/Support.idr b/src/Parser/Support.idr index 52de7973f..7516778f9 100644 --- a/src/Parser/Support.idr +++ b/src/Parser/Support.idr @@ -7,6 +7,13 @@ import public Text.Parser import Core.TT import Data.List.Views +import IdrisJvm.IO +import IdrisJvm.File + +%hide Prelude.File.File +%hide Prelude.File.FileError +%hide Prelude.File.readFile + %default total public export @@ -62,7 +69,7 @@ runParser : String -> Grammar (TokenData Token) e ty -> Either ParseError ty runParser = runParserTo (const False) export -parseFile : (fn : String) -> Rule ty -> IO (Either ParseError ty) +parseFile : (fn : String) -> Rule ty -> JVM_IO (Either ParseError ty) parseFile fn p = do Right str <- readFile fn | Left err => pure (Left (FileFail err)) diff --git a/src/TTImp/ProcessDecls.idr b/src/TTImp/ProcessDecls.idr index 005d93dbf..6efaddbb4 100644 --- a/src/TTImp/ProcessDecls.idr +++ b/src/TTImp/ProcessDecls.idr @@ -17,6 +17,8 @@ import TTImp.ProcessRecord import TTImp.ProcessType import TTImp.TTImp +import IdrisJvm.IO + -- Implements processDecl, declared in TTImp.Elab.Check process : {vars : _} -> {auto c : Ref Ctxt Defs} -> diff --git a/src/Utils/Binary.idr b/src/Utils/Binary.idr index 7f2387827..675174573 100644 --- a/src/Utils/Binary.idr +++ b/src/Utils/Binary.idr @@ -3,11 +3,12 @@ module Utils.Binary import Core.Core import Core.Name -import Data.Buffer import public Data.IOArray import Data.List import Data.Vect - +import IdrisJvm.Data.Buffer +import IdrisJvm.IO +import IdrisJvm.File -- Serialising data as binary. Provides an interface TTC which allows -- reading and writing to chunks of memory, "Binary", which can be written @@ -15,6 +16,10 @@ import Data.Vect %default covering +%hide Prelude.File.File +%hide Prelude.File.FileError +%hide Prelude.File.openFile + -- A label for binary states export data Bin : Type where @@ -49,7 +54,7 @@ appended i (MkBin b loc s used) = MkBin b (loc+i) s (used + i) incLoc : Int -> Binary -> Binary incLoc i c = record { loc $= (+i) } c -dumpBin : Binary -> IO () +dumpBin : Binary -> JVM_IO () dumpBin chunk = do -- printLn !(traverse bufferData (map buf done)) printLn !(bufferData (buf chunk)) @@ -59,13 +64,13 @@ nonEmptyRev : NonEmpty (xs ++ y :: ys) nonEmptyRev {xs = []} = IsNonEmpty nonEmptyRev {xs = (x :: xs)} = IsNonEmpty -fromBuffer : Buffer -> IO Binary +fromBuffer : Buffer -> JVM_IO Binary fromBuffer buf = do len <- rawSize buf pure (MkBin buf 0 len len) export -writeToFile : (fname : String) -> Binary -> IO (Either FileError ()) +writeToFile : (fname : String) -> Binary -> JVM_IO (Either FileError ()) writeToFile fname c = do Right h <- openFile fname WriteTruncate | Left err => pure (Left err) @@ -74,7 +79,7 @@ writeToFile fname c pure (Right ()) export -readFromFile : (fname : String) -> IO (Either FileError Binary) +readFromFile : (fname : String) -> JVM_IO (Either FileError Binary) readFromFile fname = do Right h <- openFile fname Read | Left err => pure (Left err) diff --git a/src/Yaffle/Main.idr b/src/Yaffle/Main.idr index dd0133c1d..2be1a6da8 100644 --- a/src/Yaffle/Main.idr +++ b/src/Yaffle/Main.idr @@ -20,7 +20,8 @@ import TTImp.TTImp import Yaffle.REPL -import System +import IdrisJvm.IO +import IdrisJvm.System usage : String usage = "Usage: yaffle [--timing]" @@ -62,7 +63,7 @@ yaffleMain fname args repl {c} {u} {- -main : IO () +main : JVM_IO () main = do (_ :: fname :: rest) <- getArgs | _ => do putStrLn usage diff --git a/src/Yaffle/REPL.idr b/src/Yaffle/REPL.idr index 157745fc1..5ba0966f4 100644 --- a/src/Yaffle/REPL.idr +++ b/src/Yaffle/REPL.idr @@ -25,6 +25,8 @@ import Parser.Support import Control.Catchable +import IdrisJvm.IO + %default covering showInfo : (Name, Int, GlobalDef) -> Core () diff --git a/tests.ipkg b/tests.ipkg index 1fd28200c..abe5f9867 100644 --- a/tests.ipkg +++ b/tests.ipkg @@ -1,11 +1,11 @@ package runtests -pkgs = contrib +pkgs = contrib, idrisjvmffi sourcedir = tests executable = runtests -opts = "--warnreach --partial-eval" +opts = "--warnreach --partial-eval --portable-codegen jvm" main = Main diff --git a/tests/Main.idr b/tests/Main.idr index 862ce54f1..d655627b9 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -1,6 +1,9 @@ module Main -import System +-- import System +import IdrisJvm.IO +import IdrisJvm.File +import IdrisJvm.System %default covering @@ -64,26 +67,27 @@ chezTests = ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006", "chez007"] -chdir : String -> IO Bool -chdir dir - = do ok <- foreign FFI_C "chdir" (String -> IO Int) dir - pure (ok == 0) +chdir : String -> JVM_IO Bool +chdir dir + = changeDir dir -fail : String -> IO () +fail : String -> JVM_IO () fail err = do putStrLn err exitWith (ExitFailure 1) -runTest : String -> String -> IO Bool +runTest : String -> String -> JVM_IO Bool runTest prog testPath = do chdir testPath putStr $ testPath ++ ": " - system $ "sh ./run " ++ prog ++ " | tr -d '\\r' > output" + system $ "sh -c \"./run " ++ prog ++ " | tr -d '\\r' > output\"" Right out <- readFile "output" | Left err => do print err + chdir "../.." pure False Right exp <- readFile "expected" | Left err => do print err + chdir "../.." pure False if (out == exp) @@ -97,18 +101,18 @@ runTest prog testPath chdir "../.." pure (out == exp) -exists : String -> IO Bool +exists : String -> JVM_IO Bool exists f = do Right ok <- openFile f Read | Left err => pure False closeFile ok pure True -firstExists : List String -> IO (Maybe String) +firstExists : List String -> JVM_IO (Maybe String) firstExists [] = pure Nothing firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs -findChez : IO (Maybe String) +findChez : JVM_IO (Maybe String) findChez = do env <- getEnv "CHEZ" case env of @@ -116,7 +120,7 @@ findChez Nothing => firstExists [p ++ x | p <- ["/usr/bin/", "/usr/local/bin/"], x <- ["scheme", "chez", "chezscheme9.5"]] -runChezTests : String -> List String -> IO (List Bool) +runChezTests : String -> List String -> JVM_IO (List Bool) runChezTests prog tests = do chexec <- findChez maybe (do putStrLn "Chez Scheme not found" @@ -125,7 +129,7 @@ runChezTests prog tests traverse (runTest prog) tests) chexec -main : IO () +main : JVM_IO () main = do args <- getArgs let (_ :: idris2 :: _) = args diff --git a/tests/chez/chez001/Total.idr b/tests/chez/chez001/Total.idr index 05d1e043f..3a092b5ba 100644 --- a/tests/chez/chez001/Total.idr +++ b/tests/chez/chez001/Total.idr @@ -26,5 +26,5 @@ doubleInt = Get (\x => Put (the Integer (cast x)) countStream : Nat -> Stream Nat countStream x = x :: countStream (x + 1) -main : IO () +main : JVM_IO () main = printLn (take 10 (process doubleInt (countStream 1))) diff --git a/tests/chez/chez001/expected b/tests/chez/chez001/expected index b3d035488..251b5d6bf 100644 --- a/tests/chez/chez001/expected +++ b/tests/chez/chez001/expected @@ -1,4 +1,4 @@ -[1, 2, 2, 4, 3, 6, 4, 8, 5, 10] 1/1: Building Total (Total.idr) Welcome to Idris 2 version 0.0. Enjoy yourself! -Main> Main> Bye for now! +Main> [1, 2, 2, 4, 3, 6, 4, 8, 5, 10] +Main> Bye for now! diff --git a/tests/chez/chez002/expected b/tests/chez/chez002/expected index 580fd898a..8d21e51ef 100644 --- a/tests/chez/chez002/expected +++ b/tests/chez/chez002/expected @@ -1,4 +1,4 @@ -[(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50)), (24, (45, 51)), (20, (48, 52)), (28, (45, 53)), (33, (44, 55)), (40, (42, 58)), (36, (48, 60)), (11, (60, 61)), (39, (52, 65)), (33, (56, 65)), (25, (60, 65)), (16, (63, 65)), (32, (60, 68)), (42, (56, 70)), (48, (55, 73)), (24, (70, 74)), (45, (60, 75)), (21, (72, 75)), (30, (72, 78)), (48, (64, 80)), (18, (80, 82)), (51, (68, 85)), (40, (75, 85)), (36, (77, 85)), (13, (84, 85)), (60, (63, 87)), (39, (80, 89)), (54, (72, 90)), (35, (84, 91)), (57, (76, 95)), (65, (72, 97)), (60, (80, 100)), (28, (96, 100)), (20, (99, 101)), (48, (90, 102)), (40, (96, 104)), (63, (84, 105)), (56, (90, 106)), (60, (91, 109)), (66, (88, 110)), (36, (105, 111)), (15, (112, 113)), (69, (92, 115)), (80, (84, 116)), (45, (108, 117)), (56, (105, 119)), (72, (96, 120)), (22, (120, 122)), (27, (120, 123)), (75, (100, 125)), (44, (117, 125)), (35, (120, 125)), (78, (104, 130)), (66, (112, 130)), (50, (120, 130)), (32, (126, 130)), (81, (108, 135)), (64, (120, 136)), (88, (105, 137)), (84, (112, 140)), (55, (132, 143)), (100, (105, 145)), (87, (116, 145)), (24, (143, 145)), (17, (144, 145)), (96, (110, 146)), (48, (140, 148)), (51, (140, 149)), (90, (120, 150)), (42, (144, 150)), (72, (135, 153)), (93, (124, 155)), (60, (144, 156)), (85, (132, 157)), (84, (135, 159)), (96, (128, 160)), (36, (160, 164)), (99, (132, 165)), (119, (120, 169)), (65, (156, 169)), (102, (136, 170)), (80, (150, 170)), (72, (154, 170)), (26, (168, 170)), (52, (165, 173)), (120, (126, 174)), (105, (140, 175)), (49, (168, 175)), (78, (160, 178)), (108, (144, 180)), (19, (180, 181)), (70, (168, 182)), (33, (180, 183)), (111, (148, 185)), (104, (153, 185)), (60, (175, 185)), (57, (176, 185)), (88, (165, 187)), (114, (152, 190)), (95, (168, 193)), (130, (144, 194)), (117, (156, 195)), (99, (168, 195)), (75, (180, 195)), (48, (189, 195)), (28, (195, 197)), (120, (160, 200)), (56, (192, 200))] 1/1: Building Pythag (Pythag.idr) Welcome to Idris 2 version 0.0. Enjoy yourself! -Main> Main> Bye for now! +Main> [(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50)), (24, (45, 51)), (20, (48, 52)), (28, (45, 53)), (33, (44, 55)), (40, (42, 58)), (36, (48, 60)), (11, (60, 61)), (39, (52, 65)), (33, (56, 65)), (25, (60, 65)), (16, (63, 65)), (32, (60, 68)), (42, (56, 70)), (48, (55, 73)), (24, (70, 74)), (45, (60, 75)), (21, (72, 75)), (30, (72, 78)), (48, (64, 80)), (18, (80, 82)), (51, (68, 85)), (40, (75, 85)), (36, (77, 85)), (13, (84, 85)), (60, (63, 87)), (39, (80, 89)), (54, (72, 90)), (35, (84, 91)), (57, (76, 95)), (65, (72, 97)), (60, (80, 100)), (28, (96, 100)), (20, (99, 101)), (48, (90, 102)), (40, (96, 104)), (63, (84, 105)), (56, (90, 106)), (60, (91, 109)), (66, (88, 110)), (36, (105, 111)), (15, (112, 113)), (69, (92, 115)), (80, (84, 116)), (45, (108, 117)), (56, (105, 119)), (72, (96, 120)), (22, (120, 122)), (27, (120, 123)), (75, (100, 125)), (44, (117, 125)), (35, (120, 125)), (78, (104, 130)), (66, (112, 130)), (50, (120, 130)), (32, (126, 130)), (81, (108, 135)), (64, (120, 136)), (88, (105, 137)), (84, (112, 140)), (55, (132, 143)), (100, (105, 145)), (87, (116, 145)), (24, (143, 145)), (17, (144, 145)), (96, (110, 146)), (48, (140, 148)), (51, (140, 149)), (90, (120, 150)), (42, (144, 150)), (72, (135, 153)), (93, (124, 155)), (60, (144, 156)), (85, (132, 157)), (84, (135, 159)), (96, (128, 160)), (36, (160, 164)), (99, (132, 165)), (119, (120, 169)), (65, (156, 169)), (102, (136, 170)), (80, (150, 170)), (72, (154, 170)), (26, (168, 170)), (52, (165, 173)), (120, (126, 174)), (105, (140, 175)), (49, (168, 175)), (78, (160, 178)), (108, (144, 180)), (19, (180, 181)), (70, (168, 182)), (33, (180, 183)), (111, (148, 185)), (104, (153, 185)), (60, (175, 185)), (57, (176, 185)), (88, (165, 187)), (114, (152, 190)), (95, (168, 193)), (130, (144, 194)), (117, (156, 195)), (99, (168, 195)), (75, (180, 195)), (48, (189, 195)), (28, (195, 197)), (120, (160, 200)), (56, (192, 200))] +Main> Bye for now! diff --git a/tests/chez/chez003/IORef.idr b/tests/chez/chez003/IORef.idr index d44964a57..3caa43650 100644 --- a/tests/chez/chez003/IORef.idr +++ b/tests/chez/chez003/IORef.idr @@ -1,6 +1,6 @@ import Data.IORef -main : IO () +main : JVM_IO () main = do x <- newIORef 42 let y = x diff --git a/tests/chez/chez003/expected b/tests/chez/chez003/expected index 295913f34..2e515d345 100644 --- a/tests/chez/chez003/expected +++ b/tests/chez/chez003/expected @@ -1,7 +1,7 @@ -94 +1/1: Building IORef (IORef.idr) +Welcome to Idris 2 version 0.0. Enjoy yourself! +Main> 94 94 188 188 -1/1: Building IORef (IORef.idr) -Welcome to Idris 2 version 0.0. Enjoy yourself! -Main> Main> Bye for now! +Main> Bye for now! diff --git a/tests/chez/chez004/Buffer.idr b/tests/chez/chez004/Buffer.idr index 177136695..05ac9ab60 100644 --- a/tests/chez/chez004/Buffer.idr +++ b/tests/chez/chez004/Buffer.idr @@ -1,7 +1,7 @@ import Data.Buffer import System.File -main : IO () +main : JVM_IO () main = do buf <- newBuffer 100 s <- rawSize buf diff --git a/tests/chez/chez004/expected b/tests/chez/chez004/expected index f0fe9d5e7..3634aaae0 100644 --- a/tests/chez/chez004/expected +++ b/tests/chez/chez004/expected @@ -1,10 +1,10 @@ -100 +1/1: Building Buffer (Buffer.idr) +Welcome to Idris 2 version 0.0. Enjoy yourself! +Main> 100 94 94.42 "Hello" "there!" [0, 94, 0, 0, 0, 0, 0, 0, 0, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] [0, 94, 0, 0, 0, 0, 0, 0, 0, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] -1/1: Building Buffer (Buffer.idr) -Welcome to Idris 2 version 0.0. Enjoy yourself! -Main> Main> Bye for now! +Main> Bye for now! diff --git a/tests/chez/chez005/expected b/tests/chez/chez005/expected index 1921229aa..bd1f0c029 100644 --- a/tests/chez/chez005/expected +++ b/tests/chez/chez005/expected @@ -1,4 +1,4 @@ -(3 ** [2, 4, 6]) 1/1: Building Filter (Filter.idr) Welcome to Idris 2 version 0.0. Enjoy yourself! -Main> Main> Bye for now! +Main> (3 ** [2, 4, 6]) +Main> Bye for now! diff --git a/tests/chez/chez006/TypeCase.idr b/tests/chez/chez006/TypeCase.idr index caf2229d3..4715ee6df 100644 --- a/tests/chez/chez006/TypeCase.idr +++ b/tests/chez/chez006/TypeCase.idr @@ -16,7 +16,7 @@ strangeId x = x strangeId' : {a : Type} -> a -> a strangeId' {a=Integer} x = x+1 -main : IO () +main : JVM_IO () main = do printLn (foo Nat) printLn (foo (List Nat)) printLn (foo (List Bar)) diff --git a/tests/chez/chez006/expected b/tests/chez/chez006/expected index 2168dfce3..0c6c6f2c6 100644 --- a/tests/chez/chez006/expected +++ b/tests/chez/chez006/expected @@ -1,4 +1,6 @@ -"Nat" +1/1: Building TypeCase (TypeCase.idr) +Welcome to Idris 2 version 0.0. Enjoy yourself! +Main> "Nat" "List of Nat" "List of Something else" "List of Something else" @@ -9,9 +11,7 @@ "List of Int" 43 42 -1/1: Building TypeCase (TypeCase.idr) -Welcome to Idris 2 version 0.0. Enjoy yourself! -Main> Main> Main.strangeId is total +Main> Main.strangeId is total Main> Main.strangeId': strangeId' _ Main> Bye for now! diff --git a/tests/chez/chez007/TypeCase.idr b/tests/chez/chez007/TypeCase.idr index 026199d97..3bf1aa457 100644 --- a/tests/chez/chez007/TypeCase.idr +++ b/tests/chez/chez007/TypeCase.idr @@ -20,7 +20,7 @@ descFn ((x : Nat) -> b) = descNat (b Z) descFn (a -> b) = "Function on " ++ desc a descFn x = desc x -main : IO () +main : JVM_IO () main = do printLn (descFn (Nat -> Nat)) printLn (descFn ((x : Nat) -> Vect x Int)) printLn (descFn (Type -> Int)) diff --git a/tests/chez/chez007/expected b/tests/chez/chez007/expected index e13db1a4a..f1b44dae0 100644 --- a/tests/chez/chez007/expected +++ b/tests/chez/chez007/expected @@ -1,6 +1,6 @@ -"Function from Nat to Nat" -"Function from Nat to Vector of 0 Int" -"Function on Type" 1/1: Building TypeCase (TypeCase.idr) Welcome to Idris 2 version 0.0. Enjoy yourself! -Main> Main> Bye for now! +Main> "Function from Nat to Nat" +"Function from Nat to Vector of 0 Int" +"Function on Type" +Main> Bye for now! diff --git a/tests/idris2/basic019/expected b/tests/idris2/basic019/expected index 1e08f56f4..93d45d64c 100644 --- a/tests/idris2/basic019/expected +++ b/tests/idris2/basic019/expected @@ -4,6 +4,6 @@ Main> Main.foo : (x : Nat) -> (case x of { Z => Nat -> Nat ; S k => Nat }) Main> Prelude.elem : Eq a => a -> List a -> Bool elem x [] = False elem x (y :: ys) = if x == y then True else elem x ys -Main> PrimIO.io_bind : (1 act : IO a) -> (1 k : (a -> IO b)) -> IO b -io_bind (MkIO fn) = \1 k => MkIO (\1 w => (case fn w of { MkIORes x' w' => case k x' of { MkIO res => res w' } })) +Main> PrimIO.io_bind : (1 act : JVM_IO a) -> (1 k : (a -> JVM_IO b)) -> JVM_IO b +io_bind (MkJVM_IO fn) = \1 k => MkJVM_IO (\1 w => (case fn w of { MkIORes x' w' => case k x' of { MkJVM_IO res => res w' } })) Main> Bye for now! diff --git a/tests/idris2/error008/expected b/tests/idris2/error008/expected index 7b57aebfd..d8be9e7b6 100644 --- a/tests/idris2/error008/expected +++ b/tests/idris2/error008/expected @@ -1,3 +1,26 @@ -File error in DoesntExist.idr: File Not Found +File error in DoesntExist.idr: java.nio.file.NoSuchFileException: /home/marimuthu/workspace/Idris2/tests/idris2/error008/DoesntExist.idr + at sun.nio.fs.UnixException.translateToIOException(UnixException.java:86) + at sun.nio.fs.UnixException.rethrowAsIOException(UnixException.java:102) + at sun.nio.fs.UnixException.rethrowAsIOException(UnixException.java:107) + at sun.nio.fs.UnixFileSystemProvider.newByteChannel(UnixFileSystemProvider.java:214) + at java.nio.file.Files.newByteChannel(Files.java:361) + at java.nio.file.Files.newByteChannel(Files.java:407) + at java.nio.file.Files.readAllBytes(Files.java:3152) + at io.github.mmhelloworld.idrisjvm.io.Files.readFile(Files.java:52) + at I_IdrisJvm.I_Files.Files.lambda$readFile$2(Files.idr) + at io.github.mmhelloworld.idrisjvm.runtime.Util.throwable(Util.java:38) + at I_IdrisJvm.I_Files.Files.readFile(Files.idr) + at I_Idris.REPL.loadMainFile(REPL.idr) + at main.Main.lambda$$lbraceAPPLY_0$rbrace$18$1898(Main.idr) + at io.github.mmhelloworld.idrisjvm.runtime.Runtime.unwrap(Runtime.java:116) + at main.Main.stMain(Main.idr) + at main.Main.lambda$$lbraceAPPLY_0$rbrace$19$2057(Main.idr) + at io.github.mmhelloworld.idrisjvm.runtime.Runtime.unwrap(Runtime.java:116) + at I_Core.Core.coreRun(Core.idr) + at main.Main.lambda$$lbraceAPPLY_0$rbrace$3$389(Main.idr) + at io.github.mmhelloworld.idrisjvm.runtime.Runtime.unwrap(Runtime.java:116) + at main.Main.$lbracerunMain_0$rbrace(Main.idr) + at main.Main.main(Main.idr) + Welcome to Idris 2 version 0.0. Enjoy yourself! Main> Bye for now! diff --git a/tests/idris2/perf001/Big.idr b/tests/idris2/perf001/Big.idr index 9706bedf8..f00c69740 100644 --- a/tests/idris2/perf001/Big.idr +++ b/tests/idris2/perf001/Big.idr @@ -1,6 +1,6 @@ import Data.Vect -test : Vect 33 Int -> IO Int +test : Vect 33 Int -> JVM_IO Int test bytes_list = do let int1 = (index 0 bytes_list * 8) + (index 1 bytes_list * 4) + diff --git a/tests/idris2/perf002/Big.idr b/tests/idris2/perf002/Big.idr index 3c8bf1598..827124a57 100644 --- a/tests/idris2/perf002/Big.idr +++ b/tests/idris2/perf002/Big.idr @@ -1,6 +1,6 @@ import Data.Vect -test : Vect 2 () -> IO () +test : Vect 2 () -> JVM_IO () test b = let i = index 1 b in let i = index 1 b in @@ -30,6 +30,6 @@ test b = let i = index 1 b in pure () -main : IO () +main : JVM_IO () main = do pure () diff --git a/tests/idris2/total006/Total.idr b/tests/idris2/total006/Total.idr index 05d1e043f..3a092b5ba 100644 --- a/tests/idris2/total006/Total.idr +++ b/tests/idris2/total006/Total.idr @@ -26,5 +26,5 @@ doubleInt = Get (\x => Put (the Integer (cast x)) countStream : Nat -> Stream Nat countStream x = x :: countStream (x + 1) -main : IO () +main : JVM_IO () main = printLn (take 10 (process doubleInt (countStream 1))) diff --git a/tests/typedd-book/chapter01/Hello.idr b/tests/typedd-book/chapter01/Hello.idr index 18a585653..f09ce953e 100644 --- a/tests/typedd-book/chapter01/Hello.idr +++ b/tests/typedd-book/chapter01/Hello.idr @@ -1,4 +1,4 @@ module Main -main : IO () +main : JVM_IO () main = putStrLn "Hello, Idris world!" diff --git a/tests/typedd-book/chapter01/HelloHole.idr b/tests/typedd-book/chapter01/HelloHole.idr index 36acdbe83..4fbd6fe4c 100644 --- a/tests/typedd-book/chapter01/HelloHole.idr +++ b/tests/typedd-book/chapter01/HelloHole.idr @@ -1,6 +1,6 @@ module Main -main : IO () +main : JVM_IO () main = putStrLn ?greeting diff --git a/tests/typedd-book/chapter01/HoleFix.idr b/tests/typedd-book/chapter01/HoleFix.idr index 9088154e8..4561213fe 100644 --- a/tests/typedd-book/chapter01/HoleFix.idr +++ b/tests/typedd-book/chapter01/HoleFix.idr @@ -1,4 +1,4 @@ module Main -main : IO () +main : JVM_IO () main = putStrLn (?convert 'x') diff --git a/tests/typedd-book/chapter02/AveMain.idr b/tests/typedd-book/chapter02/AveMain.idr index 95bf4fe75..cdf56e698 100644 --- a/tests/typedd-book/chapter02/AveMain.idr +++ b/tests/typedd-book/chapter02/AveMain.idr @@ -7,5 +7,5 @@ showAverage : String -> String showAverage str = "The average word length is: " ++ show (average str) ++ "\n" -main : IO () +main : JVM_IO () main = repl "Enter a string: " showAverage diff --git a/tests/typedd-book/chapter02/Reverse.idr b/tests/typedd-book/chapter02/Reverse.idr index d3a5b2f66..481b9b0da 100644 --- a/tests/typedd-book/chapter02/Reverse.idr +++ b/tests/typedd-book/chapter02/Reverse.idr @@ -2,5 +2,5 @@ module Main import System.REPL -main : IO () +main : JVM_IO () main = repl "> " reverse diff --git a/tests/typedd-book/chapter04/DataStore.idr b/tests/typedd-book/chapter04/DataStore.idr index 19493a373..4b40fe6b5 100644 --- a/tests/typedd-book/chapter04/DataStore.idr +++ b/tests/typedd-book/chapter04/DataStore.idr @@ -54,5 +54,5 @@ processInput store input Just (Get pos) => getEntry pos store Just Quit => Nothing -main : IO () +main : JVM_IO () main = replWith (MkData _ []) "Command: " processInput diff --git a/tests/typedd-book/chapter04/SumInputs.idr b/tests/typedd-book/chapter04/SumInputs.idr index ed537769c..a26b04fb2 100644 --- a/tests/typedd-book/chapter04/SumInputs.idr +++ b/tests/typedd-book/chapter04/SumInputs.idr @@ -8,5 +8,5 @@ sumInputs tot inp else let newVal = tot + val in Just ("Subtotal: " ++ show newVal ++ "\n", newVal) -main : IO () +main : JVM_IO () main = replWith 0 "Value: " sumInputs diff --git a/tests/typedd-book/chapter05/DepPairs.idr b/tests/typedd-book/chapter05/DepPairs.idr index 241b5c5e7..3d10c08f7 100644 --- a/tests/typedd-book/chapter05/DepPairs.idr +++ b/tests/typedd-book/chapter05/DepPairs.idr @@ -3,14 +3,14 @@ import Data.Vect anyVect : (n ** Vect n String) anyVect = (3 ** ["Rod", "Jane", "Freddy"]) -readVect : IO (len ** Vect len String) +readVect : JVM_IO (len ** Vect len String) readVect = do x <- getLine if (x == "") then pure (Z ** []) else do (_ ** xs) <- readVect pure (_ ** x :: xs) -zipInputs : IO () +zipInputs : JVM_IO () zipInputs = do putStrLn "Enter first vector (blank line to end):" (len1 ** vec1) <- readVect putStrLn "Enter second vector (blank line to end):" diff --git a/tests/typedd-book/chapter05/Do.idr b/tests/typedd-book/chapter05/Do.idr index 5fc7ea9c5..dbcb1b80a 100644 --- a/tests/typedd-book/chapter05/Do.idr +++ b/tests/typedd-book/chapter05/Do.idr @@ -1,12 +1,12 @@ -printTwoThings : IO () +printTwoThings : JVM_IO () printTwoThings = do putStrLn "Hello" putStrLn "World" -printInput : IO () +printInput : JVM_IO () printInput = do x <- getLine putStrLn x -printLength : IO () +printLength : JVM_IO () printLength = do putStr "Input string: " input <- getLine let len = length input diff --git a/tests/typedd-book/chapter05/Hello.idr b/tests/typedd-book/chapter05/Hello.idr index 05e5d1de4..9ab5e8b0c 100644 --- a/tests/typedd-book/chapter05/Hello.idr +++ b/tests/typedd-book/chapter05/Hello.idr @@ -1,6 +1,6 @@ module Main -main : IO () +main : JVM_IO () main = do putStr "Enter your name: " x <- getLine diff --git a/tests/typedd-book/chapter05/Loops.idr b/tests/typedd-book/chapter05/Loops.idr index ebe850b2d..b1d7394d6 100644 --- a/tests/typedd-book/chapter05/Loops.idr +++ b/tests/typedd-book/chapter05/Loops.idr @@ -3,20 +3,20 @@ module Main import Data.Strings import System -countdown : (secs : Nat) -> IO () +countdown : (secs : Nat) -> JVM_IO () countdown Z = putStrLn "Lift off!" countdown (S secs) = do putStrLn (show (S secs)) usleep 1000000 countdown secs -readNumber : IO (Maybe Nat) +readNumber : JVM_IO (Maybe Nat) readNumber = do input <- getLine if all isDigit (unpack input) then pure (Just (stringToNatOrZ input)) else pure Nothing -countdowns : IO () +countdowns : JVM_IO () countdowns = do putStr "Enter starting number: " Just startNum <- readNumber | Nothing => do putStrLn "Invalid input" diff --git a/tests/typedd-book/chapter05/PrintLength.idr b/tests/typedd-book/chapter05/PrintLength.idr index 58aa343b3..b80ddd247 100644 --- a/tests/typedd-book/chapter05/PrintLength.idr +++ b/tests/typedd-book/chapter05/PrintLength.idr @@ -1,4 +1,4 @@ -printLength : IO () +printLength : JVM_IO () printLength = putStr "Input string: " >>= \_ => getLine >>= \input => let len = length input in diff --git a/tests/typedd-book/chapter05/ReadNum.idr b/tests/typedd-book/chapter05/ReadNum.idr index 3d1a97216..995e6ae13 100644 --- a/tests/typedd-book/chapter05/ReadNum.idr +++ b/tests/typedd-book/chapter05/ReadNum.idr @@ -1,13 +1,13 @@ import Data.Strings -readNumber : IO (Maybe Nat) +readNumber : JVM_IO (Maybe Nat) readNumber = do input <- getLine if all isDigit (unpack input) then pure (Just (stringToNatOrZ input)) else pure Nothing -readNumbers_v1 : IO (Maybe (Nat, Nat)) +readNumbers_v1 : JVM_IO (Maybe (Nat, Nat)) readNumbers_v1 = do num1 <- readNumber case num1 of @@ -18,18 +18,18 @@ readNumbers_v1 = Nothing => pure Nothing Just num2_ok => pure (Just (num1_ok, num2_ok)) -readPair : IO (String, String) +readPair : JVM_IO (String, String) readPair = do str1 <- getLine str2 <- getLine pure (str1, str2) -readNumbers_v2 : IO (Maybe (Nat, Nat)) +readNumbers_v2 : JVM_IO (Maybe (Nat, Nat)) readNumbers_v2 = do Just num1_ok <- readNumber Just num2_ok <- readNumber pure (Just (num1_ok, num2_ok)) -readNumbers : IO (Maybe (Nat, Nat)) +readNumbers : JVM_IO (Maybe (Nat, Nat)) readNumbers = do Just num1_ok <- readNumber | Nothing => pure Nothing Just num2_ok <- readNumber | Nothing => pure Nothing diff --git a/tests/typedd-book/chapter05/ReadVect.idr b/tests/typedd-book/chapter05/ReadVect.idr index 96f18f8db..93485af4c 100644 --- a/tests/typedd-book/chapter05/ReadVect.idr +++ b/tests/typedd-book/chapter05/ReadVect.idr @@ -1,6 +1,6 @@ import Data.Vect -readVectLen : (len : Nat) -> IO (Vect len String) +readVectLen : (len : Nat) -> JVM_IO (Vect len String) readVectLen Z = pure [] readVectLen (S k) = do x <- getLine xs <- readVectLen k @@ -9,13 +9,13 @@ readVectLen (S k) = do x <- getLine data VectUnknown : Type -> Type where MkVect : (len : Nat) -> Vect len a -> VectUnknown a -readVect : IO (VectUnknown String) +readVect : JVM_IO (VectUnknown String) readVect = do x <- getLine if (x == "") then pure (MkVect _ []) else do MkVect _ xs <- readVect pure (MkVect _ (x :: xs)) -printVect : Show a => VectUnknown a -> IO () +printVect : Show a => VectUnknown a -> JVM_IO () printVect (MkVect len xs) = putStrLn (show xs ++ " (length " ++ show len ++ ")") diff --git a/tests/typedd-book/chapter06/DataStore.idr b/tests/typedd-book/chapter06/DataStore.idr index 95b0dc48d..0d19d37ca 100644 --- a/tests/typedd-book/chapter06/DataStore.idr +++ b/tests/typedd-book/chapter06/DataStore.idr @@ -126,5 +126,5 @@ processInput store input Just (Get pos) => getEntry pos store Just Quit => Nothing -main : IO () +main : JVM_IO () main = replWith (MkData (SString .+. SString .+. SInt) _ []) "Command: " processInput diff --git a/tests/typedd-book/chapter06/DataStoreHoles.idr b/tests/typedd-book/chapter06/DataStoreHoles.idr index 5daf8079d..bb5fce248 100644 --- a/tests/typedd-book/chapter06/DataStoreHoles.idr +++ b/tests/typedd-book/chapter06/DataStoreHoles.idr @@ -60,5 +60,5 @@ processInput store input Just (Get pos) => getEntry pos store Just Quit => Nothing -main : IO () +main : JVM_IO () main = replWith (MkData SString _ []) "Command: " processInput diff --git a/tests/typedd-book/chapter09/Hangman.idr b/tests/typedd-book/chapter09/Hangman.idr index 40dfbba65..1b4dd7ef0 100644 --- a/tests/typedd-book/chapter09/Hangman.idr +++ b/tests/typedd-book/chapter09/Hangman.idr @@ -45,7 +45,7 @@ isValidInput (x :: (y :: xs)) = No isValidTwo isValidString : (s : String) -> Dec (ValidInput (unpack s)) isValidString s = isValidInput (unpack s) -readGuess : IO (x ** ValidInput x) +readGuess : JVM_IO (x ** ValidInput x) readGuess = do putStr "Guess: " x <- getLine case isValidString (toUpper x) of @@ -54,7 +54,7 @@ readGuess = do putStr "Guess: " readGuess game : {guesses : _} -> {letters : _} -> - WordState (S guesses) (S letters) -> IO Finished + WordState (S guesses) (S letters) -> JVM_IO Finished game {guesses} {letters} st = do (_ ** Letter letter) <- readGuess case processGuess letter st of @@ -68,7 +68,7 @@ game {guesses} {letters} st Z => pure (Won r) S k => game r -main : IO () +main : JVM_IO () main = do result <- game {guesses=2} (MkWordState "Test" ['T', 'E', 'S']) case result of Lost (MkWordState word missing) => diff --git a/tests/typedd-book/chapter11/Arith.idr b/tests/typedd-book/chapter11/Arith.idr index dce03a208..fac532ffd 100644 --- a/tests/typedd-book/chapter11/Arith.idr +++ b/tests/typedd-book/chapter11/Arith.idr @@ -1,7 +1,7 @@ import Data.Primitives.Views import System -quiz : Stream Int -> (score : Nat) -> IO () +quiz : Stream Int -> (score : Nat) -> JVM_IO () quiz (num1 :: num2 :: nums) score = do putStrLn ("Score so far: " ++ show score) putStr (show num1 ++ " * " ++ show num2 ++ "? ") @@ -23,6 +23,6 @@ arithInputs seed = map bound (randoms seed) bound x with (divides x 12) bound ((12 * div) + rem) | (DivBy div rem prf) = rem + 1 -main : IO () +main : JVM_IO () main = do seed <- time quiz (arithInputs (fromInteger seed)) 0 diff --git a/tests/typedd-book/chapter11/ArithCmd.idr b/tests/typedd-book/chapter11/ArithCmd.idr index bc8d78988..e6afc9596 100644 --- a/tests/typedd-book/chapter11/ArithCmd.idr +++ b/tests/typedd-book/chapter11/ArithCmd.idr @@ -17,11 +17,11 @@ data ConsoleIO : Type -> Type where data Fuel = Dry | More (Lazy Fuel) -runCommand : Command a -> IO a +runCommand : Command a -> JVM_IO a runCommand (PutStr x) = putStr x runCommand GetLine = getLine -run : Fuel -> ConsoleIO a -> IO (Maybe a) +run : Fuel -> ConsoleIO a -> JVM_IO (Maybe a) run fuel (Quit val) = do pure (Just val) run (More fuel) (Do c f) = do res <- runCommand c run fuel (f res) @@ -64,7 +64,7 @@ forever : Fuel forever = More forever partial -main : IO () +main : JVM_IO () main = do seed <- time Just score <- run forever (quiz (arithInputs (fromInteger seed)) 0) | Nothing => putStrLn "Ran out of fuel" diff --git a/tests/typedd-book/chapter11/ArithCmdDo.idr b/tests/typedd-book/chapter11/ArithCmdDo.idr index 36d0ecf8f..639aa4a01 100644 --- a/tests/typedd-book/chapter11/ArithCmdDo.idr +++ b/tests/typedd-book/chapter11/ArithCmdDo.idr @@ -27,14 +27,14 @@ namespace ConsoleDo data Fuel = Dry | More (Lazy Fuel) -runCommand : Command a -> IO a +runCommand : Command a -> JVM_IO a runCommand (PutStr x) = putStr x runCommand GetLine = getLine runCommand (Pure val) = pure val runCommand (Bind c f) = do res <- runCommand c runCommand (f res) -run : Fuel -> ConsoleIO a -> IO (Maybe a) +run : Fuel -> ConsoleIO a -> JVM_IO (Maybe a) run fuel (Quit val) = do pure (Just val) run (More fuel) (Do c f) = do res <- runCommand c run fuel (f res) @@ -88,7 +88,7 @@ forever : Fuel forever = More forever partial -main : IO () +main : JVM_IO () main = do seed <- time Just score <- run forever (quiz (arithInputs (fromInteger seed)) 0) | Nothing => putStrLn "Ran out of fuel" diff --git a/tests/typedd-book/chapter11/ArithTotal.idr b/tests/typedd-book/chapter11/ArithTotal.idr index bdf9c0683..3fe9d93fd 100644 --- a/tests/typedd-book/chapter11/ArithTotal.idr +++ b/tests/typedd-book/chapter11/ArithTotal.idr @@ -4,14 +4,14 @@ import System -- %default total data InfIO : Type where - Do : IO a -> (a -> Inf InfIO) -> InfIO + Do : JVM_IO a -> (a -> Inf InfIO) -> InfIO -(>>=) : IO a -> (a -> Inf InfIO) -> InfIO +(>>=) : JVM_IO a -> (a -> Inf InfIO) -> InfIO (>>=) = Do data Fuel = Dry | More (Lazy Fuel) -run : Fuel -> InfIO -> IO () +run : Fuel -> InfIO -> JVM_IO () run (More fuel) (Do c f) = do res <- c run fuel (f res) run Dry p = putStrLn "Out of fuel" @@ -43,6 +43,6 @@ forever : Fuel forever = More forever partial -main : IO () +main : JVM_IO () main = do seed <- time run forever (quiz (arithInputs (fromInteger seed)) 0) diff --git a/tests/typedd-book/chapter11/Greet.idr b/tests/typedd-book/chapter11/Greet.idr index 3df0daec3..24dacc951 100644 --- a/tests/typedd-book/chapter11/Greet.idr +++ b/tests/typedd-book/chapter11/Greet.idr @@ -1,9 +1,9 @@ -- %default total data InfIO : Type where - Do : IO a -> (a -> Inf InfIO) -> InfIO + Do : JVM_IO a -> (a -> Inf InfIO) -> InfIO -(>>=) : IO a -> (a -> Inf InfIO) -> InfIO +(>>=) : JVM_IO a -> (a -> Inf InfIO) -> InfIO (>>=) = Do greet : InfIO diff --git a/tests/typedd-book/chapter11/InfIO.idr b/tests/typedd-book/chapter11/InfIO.idr index 486410653..9aaff28a7 100644 --- a/tests/typedd-book/chapter11/InfIO.idr +++ b/tests/typedd-book/chapter11/InfIO.idr @@ -1,9 +1,9 @@ -- %default total data InfIO : Type where - Do : IO a -> (a -> Inf InfIO) -> InfIO + Do : JVM_IO a -> (a -> Inf InfIO) -> InfIO -(>>=) : IO a -> (a -> Inf InfIO) -> InfIO +(>>=) : JVM_IO a -> (a -> Inf InfIO) -> InfIO (>>=) = Do loopPrint : String -> InfIO @@ -17,11 +17,11 @@ tank Z = Dry tank (S k) = More (tank k) partial -runPartial : InfIO -> IO () +runPartial : InfIO -> JVM_IO () runPartial (Do action f) = do res <- action runPartial (f res) -run : Fuel -> InfIO -> IO () +run : Fuel -> InfIO -> JVM_IO () run (More fuel) (Do c f) = do res <- c run fuel (f res) run Dry p = putStrLn "Out of fuel" @@ -31,5 +31,5 @@ forever : Fuel forever = More forever partial -main : IO () +main : JVM_IO () main = run (tank 10) (loopPrint "vroom") diff --git a/tests/typedd-book/chapter11/RunIO.idr b/tests/typedd-book/chapter11/RunIO.idr index 47bd4d96e..8578ea1fe 100644 --- a/tests/typedd-book/chapter11/RunIO.idr +++ b/tests/typedd-book/chapter11/RunIO.idr @@ -2,9 +2,9 @@ data RunIO : Type -> Type where Quit : a -> RunIO a - Do : IO a -> (a -> Inf (RunIO b)) -> RunIO b + Do : JVM_IO a -> (a -> Inf (RunIO b)) -> RunIO b -(>>=) : IO a -> (a -> Inf (RunIO b)) -> RunIO b +(>>=) : JVM_IO a -> (a -> Inf (RunIO b)) -> RunIO b (>>=) = Do greet : RunIO () @@ -18,7 +18,7 @@ greet = do putStr "Enter your name: " data Fuel = Dry | More (Lazy Fuel) -run : Fuel -> RunIO a -> IO (Maybe a) +run : Fuel -> RunIO a -> JVM_IO (Maybe a) run fuel (Quit val) = do pure (Just val) run (More fuel) (Do c f) = do res <- c run fuel (f res) @@ -29,6 +29,6 @@ forever : Fuel forever = More forever partial -main : IO () +main : JVM_IO () main = do run forever greet pure () diff --git a/tests/typedd-book/chapter12/ArithState.idr b/tests/typedd-book/chapter12/ArithState.idr index 86a50971d..b804312bf 100644 --- a/tests/typedd-book/chapter12/ArithState.idr +++ b/tests/typedd-book/chapter12/ArithState.idr @@ -62,7 +62,7 @@ randoms seed = let seed' = 1664525 * seed + 1013904223 in (seed' `shiftR` 2) :: randoms seed' runCommand : Stream Int -> GameState -> Command a -> - IO (a, Stream Int, GameState) + JVM_IO (a, Stream Int, GameState) runCommand rnds state (PutStr x) = do putStr x pure ((), rnds, state) runCommand rnds state GetLine = do str <- getLine @@ -92,7 +92,7 @@ forever : Fuel forever = More forever run : Fuel -> Stream Int -> GameState -> ConsoleIO a -> - IO (Maybe a, Stream Int, GameState) + JVM_IO (Maybe a, Stream Int, GameState) run fuel rnds state (Quit val) = do pure (Just val, rnds, state) run (More fuel) rnds state (Do c f) = do (res, newRnds, newState) <- runCommand rnds state c @@ -138,7 +138,7 @@ mutual QuitCmd => Quit st partial -main : IO () +main : JVM_IO () main = do seed <- time (Just score, _, state) <- run forever (randoms (fromInteger seed)) initState quiz diff --git a/tests/typedd-book/chapter12/Traverse.idr b/tests/typedd-book/chapter12/Traverse.idr index aa5278bef..287fb4c92 100644 --- a/tests/typedd-book/chapter12/Traverse.idr +++ b/tests/typedd-book/chapter12/Traverse.idr @@ -1,7 +1,7 @@ crew : List String crew = ["Lister", "Rimmer", "Kryten", "Cat"] -main : IO () +main : JVM_IO () main = do putStr "Display Crew? " x <- getLine when (x == "yes") $