Merge pull request #1 from mmhelloworld/feature/idrisjvm-104

Compile to JVM

.gitignore

@@ -12,3 +12,8 @@ libs/**/build
 tests/**/output
 
 src/YafflePaths.idr
+
+*.iml
+classes/**
+*-classes/**
+output

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

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.

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
 ----------

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
 

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

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)

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" []

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]
 

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

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, ()))
 

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