git.iko.soy/Idris-dev
on master help sign in
New language-dependent FFI

More documentation to follow, but in brief: - IO is now a synonym of IO' FFI_C - IO' is parameterised over an ffi description, which explains which types are allowed in foreign calls, and what a foreign call target is (in C, that's a String giving the function name, for example) - New function "foreign" for building a foreign call, given an ffi description, call target, and the type of the call. The type is enough to build a structure which the compiler uses to generate the call. The type of main now needs to be IO' x (), where x can be any FFI description. There is currently only an ffi description for C; Javascript will follow. FFI_C should also work for the llvm backend (it's really about the calling convention, not the backend specifically). Small changes will be needed to the various code generators.

commitd5377be62896a459b4e0cce5686afd2846c18571 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 17 Jan 2015, 19:08 (12 years ago) parent6faa820
31 files changed+448−396
compare with master
unifiedsplit
idris.cabal+3−3 libs/base/Debug/Error.idr+1−1 libs/base/Network/Socket.idr+42−35 libs/base/System.idr+10−10 libs/base/System/Concurrency/Raw.idr+7−6 libs/effects/Effect/Memory.idr+7−7 libs/prelude/IO.idr+83−107 libs/prelude/Prelude.idr+21−21 src/IRTS/Bytecode.hs+5−6 src/IRTS/CodegenC.hs+34−6 src/IRTS/CodegenJavaScript.hs+1−1 src/IRTS/Compiler.hs+26−4 src/IRTS/Defunctionalise.hs+10−7 src/IRTS/DumpBC.hs+2−2 src/IRTS/Lang.hs+17−12 src/IRTS/LangOpts.hs+3−3 src/IRTS/Simplified.hs+7−5 src/Idris/Core/DeepSeq.hs+1−1 src/Idris/Core/Evaluate.hs+9−6 src/Idris/Core/Execute.hs+124−113 src/Idris/Elab/Clause.hs+2−1 src/Idris/Erasure.hs+7−4 src/Idris/IBC.hs+6−4 src/Idris/ParseExpr.hs+15−28 src/Idris/Parser.hs+2 src/Idris/Prover.hs+1−1 test/ffi001/run+1−1 test/ffi001/test022.idr+1−1 test/reg051/expected → test/reg051-disabled/expected test/reg051/reg051.idr → test/reg051-disabled/reg051.idr test/reg051/run → test/reg051-disabled/run
idris.cabal+3−3
@@ -265,9 +265,9 @@ Extra-source-files:
265265 test/reg050/run
266266 test/reg050/*.idr
267267 test/reg050/expected
268− test/reg051/run
269− test/reg051/*.idr
270− test/reg051/expected
268+ test/reg051-disabled/run
269+ test/reg051-disabled/*.idr
270+ test/reg051-disabled/expected
271271 test/reg052/run
272272 test/reg052/*.idr
273273 test/reg052/expected
libs/base/Debug/Error.idr+1−1
@@ -12,7 +12,7 @@ error : {default tactics {sourceLocation} loc : SourceLocation} ->
1212 (message : String) ->
1313 a
1414error {loc = FileLoc filename (line, col) _} message =
15− believe_me . unsafePerformIO $
15+ believe_me . unsafePerformIO $
1616 do let place = filename ++ " line " ++ show line ++ " column " ++ show col
1717 let message' = place ++ ": " ++ message
1818 putStrLn message'
libs/base/Network/Socket.idr+42−35
@@ -124,18 +124,18 @@ record UDPAddrInfo : Type where
124124||| Frees a given pointer
125125public
126126sock_free : BufPtr -> IO ()
127−sock_free (BPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
127+sock_free (BPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr
128128
129129public
130130sockaddr_free : SockaddrPtr -> IO ()
131−sockaddr_free (SAPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
131+sockaddr_free (SAPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr
132132
133133||| Allocates an amount of memory given by the ByteLength parameter.
134134|||
135135||| Used to allocate a mutable pointer to be given to the Recv functions.
136136public
137137sock_alloc : ByteLength -> IO BufPtr
138−sock_alloc bl = map BPtr $ mkForeign (FFun "idrnet_malloc" [FInt] FPtr) bl
138+sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl
139139
140140||| The metadata about a socket
141141record Socket : Type where
@@ -147,13 +147,13 @@ record Socket : Type where
147147
148148||| Get the C error number
149149getErrno : IO Int
150−getErrno = mkForeign (FFun "idrnet_errno" [] FInt)
150+getErrno = foreign FFI_C "idrnet_errno" (IO Int)
151151
152152||| Creates a UNIX socket with the given family, socket type and protocol
153153||| number. Returns either a socket or an error.
154154socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)
155155socket sf st pn = do
156− socket_res <- mkForeign (FFun "socket" [FInt, FInt, FInt] FInt) (toCode sf) (toCode st) pn
156+ socket_res <- foreign FFI_C "socket" (Int -> Int -> Int -> IO Int) (toCode sf) (toCode st) pn
157157 if socket_res == -1 then -- error
158158 map Left getErrno
159159 else
@@ -161,7 +161,7 @@ socket sf st pn = do
161161
162162||| Close a socket
163163close : Socket -> IO ()
164−close sock = mkForeign (FFun "close" [FInt] FUnit) (descriptor sock)
164+close sock = foreign FFI_C "close" (Int -> IO ()) (descriptor sock)
165165
166166private
167167saString : (Maybe SocketAddress) -> String
@@ -172,8 +172,10 @@ saString Nothing = ""
172172||| Returns 0 on success, an error code otherwise.
173173bind : Socket -> (Maybe SocketAddress) -> Port -> IO Int
174174bind sock addr port = do
175− bind_res <- (mkForeign (FFun "idrnet_bind" [FInt, FInt, FInt, FString, FInt] FInt)
176− (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (saString addr) port)
175+ bind_res <- foreign FFI_C "idrnet_bind"
176+ (Int -> Int -> Int -> String -> Int -> IO Int)
177+ (descriptor sock) (toCode $ family sock)
178+ (toCode $ socketType sock) (saString addr) port
177179 if bind_res == (-1) then -- error
178180 getErrno
179181 else return 0 -- Success
@@ -182,8 +184,9 @@ bind sock addr port = do
182184||| Returns 0 on success, and an error number on error.
183185connect : Socket -> SocketAddress -> Port -> IO Int
184186connect sock addr port = do
185− conn_res <- (mkForeign (FFun "idrnet_connect" [FInt, FInt, FInt, FString, FInt] FInt)
186− (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port)
187+ conn_res <- foreign FFI_C "idrnet_connect"
188+ (Int -> Int -> Int -> String -> Int -> IO Int)
189+ (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port
187190 if conn_res == (-1) then
188191 getErrno
189192 else return 0
@@ -191,7 +194,8 @@ connect sock addr port = do
191194||| Listens on a bound socket.
192195listen : Socket -> IO Int
193196listen sock = do
194− listen_res <- mkForeign (FFun "listen" [FInt, FInt] FInt) (descriptor sock) BACKLOG
197+ listen_res <- foreign FFI_C "listen" (Int -> Int -> IO Int)
198+ (descriptor sock) BACKLOG
195199 if listen_res == (-1) then
196200 getErrno
197201 else return 0
@@ -212,12 +216,12 @@ parseIPv4 str = case splitted of
212216||| Retrieves a socket address from a sockaddr pointer
213217getSockAddr : SockaddrPtr -> IO SocketAddress
214218getSockAddr (SAPtr ptr) = do
215− addr_family_int <- mkForeign (FFun "idrnet_sockaddr_family" [FPtr] FInt) ptr
219+ addr_family_int <- foreign FFI_C "idrnet_sockaddr_family" (Ptr -> IO Int) ptr
216220 -- putStrLn $ "Addr family int: " ++ (show addr_family_int)
217221 -- ASSUMPTION: Foreign call returns a valid int
218222 assert_total (case getSocketFamily addr_family_int of
219223 Just AF_INET => do
220− ipv4_addr <- mkForeign (FFun "idrnet_sockaddr_ipv4" [FPtr] FString) ptr
224+ ipv4_addr <- foreign FFI_C "idrnet_sockaddr_ipv4" (Ptr -> IO String) ptr
221225 return $ parseIPv4 ipv4_addr
222226 Just AF_INET6 => return IPv6Addr
223227 Just AF_UNSPEC => return InvalidAddress)
@@ -226,8 +230,8 @@ accept : Socket -> IO (Either SocketError (Socket, SocketAddress))
226230accept sock = do
227231 -- We need a pointer to a sockaddr structure. This is then passed into
228232 -- idrnet_accept and populated. We can then query it for the SocketAddr and free it.
229− sockaddr_ptr <- mkForeign (FFun "idrnet_create_sockaddr" [] FPtr)
230− accept_res <- mkForeign (FFun "idrnet_accept" [FInt, FPtr] FInt) (descriptor sock) sockaddr_ptr
233+ sockaddr_ptr <- foreign FFI_C "idrnet_create_sockaddr" (IO Ptr)
234+ accept_res <- foreign FFI_C "idrnet_accept" (Int -> Ptr -> IO Int) (descriptor sock) sockaddr_ptr
231235 if accept_res == (-1) then
232236 map Left getErrno
233237 else do
@@ -238,7 +242,7 @@ accept sock = do
238242
239243send : Socket -> String -> IO (Either SocketError ByteLength)
240244send sock dat = do
241− send_res <- mkForeign (FFun "idrnet_send" [FInt, FString] FInt) (descriptor sock) dat
245+ send_res <- foreign FFI_C "idrnet_send" (Int -> String -> IO Int) (descriptor sock) dat
242246 if send_res == (-1) then
243247 map Left getErrno
244248 else
@@ -246,17 +250,17 @@ send sock dat = do
246250
247251
248252freeRecvStruct : RecvStructPtr -> IO ()
249−freeRecvStruct (RSPtr p) = mkForeign (FFun "idrnet_free_recv_struct" [FPtr] FUnit) p
253+freeRecvStruct (RSPtr p) = foreign FFI_C "idrnet_free_recv_struct" (Ptr -> IO ()) p
250254
251255freeRecvfromStruct : RecvfromStructPtr -> IO ()
252−freeRecvfromStruct (RFPtr p) = mkForeign (FFun "idrnet_free_recvfrom_struct" [FPtr] FUnit) p
256+freeRecvfromStruct (RFPtr p) = foreign FFI_C "idrnet_free_recvfrom_struct" (Ptr -> IO ()) p
253257
254258recv : Socket -> Int -> IO (Either SocketError (String, ByteLength))
255259recv sock len = do
256260 -- Firstly make the request, get some kind of recv structure which
257261 -- contains the result of the recv and possibly the retrieved payload
258− recv_struct_ptr <- mkForeign (FFun "idrnet_recv" [FInt, FInt] FPtr) (descriptor sock) len
259− recv_res <- mkForeign (FFun "idrnet_get_recv_res" [FPtr] FInt) recv_struct_ptr
262+ recv_struct_ptr <- foreign FFI_C "idrnet_recv" (Int -> Int -> IO Ptr) (descriptor sock) len
263+ recv_res <- foreign FFI_C "idrnet_get_recv_res" (Ptr -> IO Int) recv_struct_ptr
260264 if recv_res == (-1) then do
261265 errno <- getErrno
262266 freeRecvStruct (RSPtr recv_struct_ptr)
@@ -266,7 +270,7 @@ recv sock len = do
266270 freeRecvStruct (RSPtr recv_struct_ptr)
267271 return $ Left 0
268272 else do
269− payload <- mkForeign (FFun "idrnet_get_recv_payload" [FPtr] FString) recv_struct_ptr
273+ payload <- foreign FFI_C "idrnet_get_recv_payload" (Ptr -> IO String) recv_struct_ptr
270274 freeRecvStruct (RSPtr recv_struct_ptr)
271275 return $ Right (payload, recv_res)
272276
@@ -274,7 +278,7 @@ recv sock len = do
274278||| Sends the data in a given memory location
275279sendBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
276280sendBuf sock (BPtr ptr) len = do
277− send_res <- mkForeign (FFun "idrnet_send_buf" [FInt, FPtr, FInt] FInt) (descriptor sock) ptr len
281+ send_res <- foreign FFI_C "idrnet_send_buf" (Int -> Ptr -> Int -> IO Int) (descriptor sock) ptr len
278282 if send_res == (-1) then
279283 map Left getErrno
280284 else
@@ -282,7 +286,7 @@ sendBuf sock (BPtr ptr) len = do
282286
283287recvBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
284288recvBuf sock (BPtr ptr) len = do
285− recv_res <- mkForeign (FFun "idrnet_recv_buf" [FInt, FPtr, FInt] FInt) (descriptor sock) ptr len
289+ recv_res <- foreign FFI_C "idrnet_recv_buf" (Int -> Ptr -> Int -> IO Int) (descriptor sock) ptr len
286290 if (recv_res == (-1)) then
287291 map Left getErrno
288292 else
@@ -290,8 +294,9 @@ recvBuf sock (BPtr ptr) len = do
290294
291295sendTo : Socket -> SocketAddress -> Port -> String -> IO (Either SocketError ByteLength)
292296sendTo sock addr p dat = do
293− sendto_res <- mkForeign (FFun "idrnet_sendto" [FInt, FString, FString, FInt, FInt] FInt)
294− (descriptor sock) dat (show addr) p (toCode $ family sock)
297+ sendto_res <- foreign FFI_C "idrnet_sendto"
298+ (Int -> String -> String -> Int -> Int -> IO Int)
299+ (descriptor sock) dat (show addr) p (toCode $ family sock)
295300 if sendto_res == (-1) then
296301 map Left getErrno
297302 else
@@ -300,8 +305,9 @@ sendTo sock addr p dat = do
300305
301306sendToBuf : Socket -> SocketAddress -> Port -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
302307sendToBuf sock addr p (BPtr dat) len = do
303− sendto_res <- mkForeign (FFun "idrnet_sendto_buf" [FInt, FPtr, FInt, FString, FInt, FInt] FInt)
304− (descriptor sock) dat len (show addr) p (toCode $ family sock)
308+ sendto_res <- foreign FFI_C "idrnet_sendto_buf"
309+ (Int -> Ptr -> Int -> String -> Int -> Int -> IO Int)
310+ (descriptor sock) dat len (show addr) p (toCode $ family sock)
305311 if sendto_res == (-1) then
306312 map Left getErrno
307313 else
@@ -309,29 +315,30 @@ sendToBuf sock addr p (BPtr dat) len = do
309315
310316
311317foreignGetRecvfromPayload : RecvfromStructPtr -> IO String
312−foreignGetRecvfromPayload (RFPtr p) = mkForeign (FFun "idrnet_get_recvfrom_payload" [FPtr] FString) p
318+foreignGetRecvfromPayload (RFPtr p)
319+ = foreign FFI_C "idrnet_get_recvfrom_payload" (Ptr -> IO String) p
313320
314321foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress
315322foreignGetRecvfromAddr (RFPtr p) = do
316− sockaddr_ptr <- map SAPtr $ mkForeign (FFun "idrnet_get_recvfrom_sockaddr" [FPtr] FPtr) p
323+ sockaddr_ptr <- map SAPtr $ foreign FFI_C "idrnet_get_recvfrom_sockaddr" (Ptr -> IO Ptr) p
317324 getSockAddr sockaddr_ptr
318325
319326
320327foreignGetRecvfromPort : RecvfromStructPtr -> IO Port
321328foreignGetRecvfromPort (RFPtr p) = do
322− sockaddr_ptr <- mkForeign (FFun "idrnet_get_recvfrom_sockaddr" [FPtr] FPtr) p
323− port <- mkForeign (FFun "idrnet_sockaddr_ipv4_port" [FPtr] FInt) sockaddr_ptr
329+ sockaddr_ptr <- foreign FFI_C "idrnet_get_recvfrom_sockaddr" (Ptr -> IO Ptr) p
330+ port <- foreign FFI_C "idrnet_sockaddr_ipv4_port" (Ptr -> IO Int) sockaddr_ptr
324331 return port
325332
326333recvFrom : Socket -> ByteLength -> IO (Either SocketError (UDPAddrInfo, String, ByteLength))
327334recvFrom sock bl = do
328− recv_ptr <- mkForeign (FFun "idrnet_recvfrom" [FInt, FInt] FPtr)
335+ recv_ptr <- foreign FFI_C "idrnet_recvfrom" (Int -> Int -> IO Ptr)
329336 (descriptor sock) bl
330337 let recv_ptr' = RFPtr recv_ptr
331338 if !(nullPtr recv_ptr) then
332339 map Left getErrno
333340 else do
334− result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr
341+ result <- foreign FFI_C "idrnet_get_recvfrom_res" (Ptr -> IO Int) recv_ptr
335342 if result == -1 then do
336343 freeRecvfromStruct recv_ptr'
337344 map Left getErrno
@@ -345,12 +352,12 @@ recvFrom sock bl = do
345352
346353recvFromBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError (UDPAddrInfo, ByteLength))
347354recvFromBuf sock (BPtr ptr) bl = do
348− recv_ptr <- mkForeign (FFun "idrnet_recvfrom_buf" [FInt, FPtr, FInt] FPtr) (descriptor sock) ptr bl
355+ recv_ptr <- foreign FFI_C "idrnet_recvfrom_buf" (Int -> Ptr -> Int -> IO Ptr) (descriptor sock) ptr bl
349356 let recv_ptr' = RFPtr recv_ptr
350357 if !(nullPtr recv_ptr) then
351358 map Left getErrno
352359 else do
353− result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr
360+ result <- foreign FFI_C "idrnet_get_recvfrom_res" (Ptr -> IO Int) recv_ptr
354361 if result == -1 then do
355362 freeRecvfromStruct recv_ptr'
356363 map Left getErrno
libs/base/System.idr+10−10
@@ -10,10 +10,10 @@ getArgs = do n <- numArgs
1010 ga' [] 0 n
1111 where
1212 numArgs : IO Int
13− numArgs = mkForeign (FFun "idris_numArgs" [] FInt)
13+ numArgs = foreign FFI_C "idris_numArgs" (IO Int)
1414
1515 getArg : Int -> IO String
16− getArg x = mkForeign (FFun "idris_getArg" [FInt] FString) x
16+ getArg x = foreign FFI_C "idris_getArg" (Int -> IO String) x
1717
1818 ga' : List String -> Int -> Int -> IO (List String)
1919 ga' acc i n = if (i == n) then (return $ reverse acc) else
@@ -31,27 +31,27 @@ getEnv key = do
3131 else pure (Just str_ptr)
3232 where
3333 getEnv' : IO String
34− getEnv' = mkForeign (FFun "getenv" [FString] FString) key
34+ getEnv' = foreign FFI_C "getenv" (String -> IO String) key
3535
3636||| Sets an environment variable with a given value.
3737||| Returns true if the operation was successful.
3838setEnv : String -> String -> IO Bool
3939setEnv key value = do
40− ok <- mkForeign (FFun "setenv" [FString, FString, FInt] FInt) key value 1
40+ ok <- foreign FFI_C "setenv" (String -> String -> Int -> IO Int) key value 1
4141 return (ok == 0)
4242
4343||| Unsets an environment variable.
4444||| Returns true if the variable was able to be unset.
4545unsetEnv : String -> IO Bool
4646unsetEnv key = do
47− ok <- mkForeign (FFun "unsetenv" [FString] FInt) key
47+ ok <- foreign FFI_C "unsetenv" (String -> IO Int) key
4848 return (ok == 0)
4949
5050getEnvironment : IO (List (String, String))
5151getEnvironment = getAllPairs 0 []
5252 where
5353 getEnvPair : Int -> IO String
54− getEnvPair i = mkForeign (FFun "getEnvPair" [FInt] FString) i
54+ getEnvPair i = foreign FFI_C "getEnvPair" (Int -> IO String) i
5555
5656 splitEq : String -> (String, String)
5757 splitEq str =
@@ -70,15 +70,15 @@ getEnvironment = getAllPairs 0 []
7070
7171||| Quit with a particular exit code
7272exit : Int -> IO ()
73−exit code = mkForeign (FFun "exit" [FInt] FUnit) code
73+exit code = foreign FFI_C "exit" (Int -> IO ()) code
7474
7575||| Get the Unix time
7676time : IO Int
77−time = mkForeign (FFun "idris_time" [] FInt)
77+time = foreign FFI_C "idris_time" (IO Int)
7878
7979usleep : Int -> IO ()
80−usleep i = mkForeign (FFun "usleep" [FInt] FUnit) i
80+usleep i = foreign FFI_C "usleep" (Int -> IO ()) i
8181
8282system : String -> IO Int
83−system cmd = mkForeign (FFun "system" [FString] FInt) cmd
83+system cmd = foreign FFI_C "system" (String -> IO Int) cmd
8484
libs/base/System/Concurrency/Raw.idr+7−6
@@ -9,16 +9,17 @@ import System
99||| Send a message of any type to the thread with the given thread id
1010sendToThread : (thread_id : Ptr) -> a -> IO ()
1111sendToThread {a} dest val
12− = mkForeign (FFun "idris_sendMessage"
13− [FPtr, FPtr, FAny a] FUnit) prim__vm dest val
12+ = foreign FFI_C "idris_sendMessage" (Ptr -> Ptr -> Raw a -> IO ())
13+ prim__vm dest (MkRaw val)
1414
1515checkMsgs : IO Bool
16−checkMsgs = do msgs <- mkForeign (FFun "idris_checkMessages"
17− [FPtr] FInt) prim__vm
16+checkMsgs = do msgs <- foreign FFI_C "idris_checkMessages" (Ptr -> IO Int)
17+ prim__vm
1818 return (intToBool msgs)
1919
2020||| Check inbox for messages. If there are none, blocks until a message
2121||| arrives.
2222getMsg : IO a
23−getMsg {a} = mkForeign (FFun "idris_recvMessage"
24− [FPtr] (FAny a)) prim__vm
23+getMsg {a} = do MkRaw x <- foreign FFI_C "idris_recvMessage"
24+ (Ptr -> IO (Raw a)) prim__vm
25+ return x
libs/effects/Effect/Memory.idr+7−7
@@ -42,7 +42,7 @@ data RawMemory : Effect where
4242private
4343do_malloc : Nat -> IOExcept String Ptr
4444do_malloc size with (fromInteger (cast size) == size)
45− | True = do ptr <- ioe_lift $ mkForeign (FFun "malloc" [FInt] FPtr) (fromInteger $ cast size)
45+ | True = do ptr <- ioe_lift $ foreign FFI_C "malloc" (Int -> IO Ptr) (fromInteger $ cast size)
4646 fail <- ioe_lift $ nullPtr ptr
4747 if fail then ioe_fail "Cannot allocate memory"
4848 else return ptr
@@ -51,24 +51,24 @@ do_malloc size with (fromInteger (cast size) == size)
5151private
5252do_memset : Ptr -> Nat -> Bits8 -> Nat -> IO ()
5353do_memset ptr offset c size
54− = mkForeign (FFun "idris_memset" [FPtr, FInt, FByte, FInt] FUnit)
54+ = foreign FFI_C "idris_memset" (Ptr -> Int -> Bits8 -> Int -> IO ())
5555 ptr (fromInteger $ cast offset) c (fromInteger $ cast size)
5656
5757private
5858do_free : Ptr -> IO ()
59−do_free ptr = mkForeign (FFun "free" [FPtr] FUnit) ptr
59+do_free ptr = foreign FFI_C "free" (Ptr -> IO ()) ptr
6060
6161private
6262do_memmove : Ptr -> Ptr -> Nat -> Nat -> Nat -> IO ()
6363do_memmove dest src dest_offset src_offset size
64− = mkForeign (FFun "idris_memmove" [FPtr, FPtr, FInt, FInt, FInt] FUnit)
65− dest src (fromInteger $ cast dest_offset) (fromInteger $ cast src_offset) (fromInteger $ cast size)
64+ = foreign FFI_C "idris_memmove" (Ptr -> Ptr -> Int -> Int -> Int -> IO ())
65+ dest src (fromInteger $ cast dest_offset) (fromInteger $ cast src_offset) (fromInteger $ cast size)
6666
6767private
6868do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect size Bits8)
6969do_peek _ _ Z = return (Vect.Nil)
7070do_peek ptr offset (S n)
71− = do b <- mkForeign (FFun "idris_peek" [FPtr, FInt] FByte) ptr (fromInteger $ cast offset)
71+ = do b <- foreign FFI_C "idris_peek" (Ptr -> Int -> IO Bits8) ptr (fromInteger $ cast offset)
7272 bs <- do_peek ptr (S offset) n
7373 Monad.return (Vect.(::) b bs)
7474
@@ -76,7 +76,7 @@ private
7676do_poke : Ptr -> Nat -> Vect size Bits8 -> IO ()
7777do_poke _ _ [] = return ()
7878do_poke ptr offset (b::bs)
79− = do mkForeign (FFun "idris_poke" [FPtr, FInt, FByte] FUnit) ptr (fromInteger $ cast offset) b
79+ = do foreign FFI_C "idris_poke" (Ptr -> Int -> Bits8 -> IO ()) ptr (fromInteger $ cast offset) b
8080 do_poke ptr (S offset) bs
8181
8282instance Handler RawMemory (IOExcept String) where
libs/prelude/IO.idr+83−107
@@ -16,11 +16,49 @@ abstract data World = TheWorld
1616abstract WorldRes : Type -> Type
1717WorldRes x = x
1818
19−-- abstract data WorldRes a = MkWR a World
19+record FFI : Type where
20+ MkFFI : (ffi_types : Type -> Type) -> (ffi_fn : Type) -> FFI
2021
2122abstract
22−data IO : Type -> Type where
23− MkIO : (World -> PrimIO (WorldRes a)) -> IO a
23+data IO' : (lang : FFI) -> Type -> Type where
24+ MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a
25+
26+data FTy : FFI -> List Type -> Type -> Type where
27+ FRet : ffi_types f t -> FTy f xs (IO' f t)
28+ FFun : ffi_types f s -> FTy f (s :: xs) t -> FTy f xs (s -> t)
29+
30+namespace ForeignEnv
31+ data FEnv : FFI -> List Type -> Type where
32+ Nil : FEnv f []
33+ (::) : (ffi_types f t, t) -> FEnv f xs -> FEnv f (t :: xs)
34+
35+ForeignPrimType : (xs : List Type) -> FEnv ffi xs -> Type -> Type
36+ForeignPrimType {ffi} [] [] t = World -> ffi_fn ffi -> ffi_types ffi t -> PrimIO t
37+ForeignPrimType {ffi} (x :: xs) ((a, _) :: env) t
38+ = (ffi_types ffi x, x) -> ForeignPrimType xs env t
39+
40+%inline
41+applyEnv : (env : FEnv ffi xs) ->
42+ ForeignPrimType xs env t ->
43+ World -> ffi_fn ffi -> ffi_types ffi t -> PrimIO t
44+applyEnv [] f = f
45+applyEnv (x@(_, _) :: xs) f = applyEnv xs (f x)
46+
47+mkForeignPrim : ForeignPrimType xs env t
48+-- compiled as primitive
49+
50+%inline
51+foreign_prim : (f : FFI) ->
52+ (fname : ffi_fn f) -> FTy f xs ty -> FEnv f xs -> ty
53+foreign_prim f fname (FRet y) env
54+ = MkIO (\w => applyEnv env mkForeignPrim w fname y)
55+foreign_prim f fname (FFun arg sc) env
56+ = \x => foreign_prim f fname sc ((arg, x) :: env)
57+
58+%inline
59+foreign : (f : FFI) -> (fname : ffi_fn f) -> (ty : Type) ->
60+ {auto fty : FTy f [] ty} -> ty
61+foreign ffi fname ty {fty} = foreign_prim ffi fname fty []
2462
2563abstract
2664prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b
@@ -33,120 +71,63 @@ abstract
3371prim_io_return : a -> PrimIO a
3472prim_io_return x = prim__IO x
3573
36−||| Descriptions of the various sorts of Ints that Idris supports
37−data IntTy = ITChar | ITNative | IT8 | IT16 | IT32 | IT64 | IT8x16 | IT16x8 | IT32x4 | IT64x2
38−
39−||| Types available for foreign function calls
40−data FTy = FIntT IntTy
41− | FFunction FTy FTy
42− | FFloat
43− | FString
44− | FPtr
45− | FManagedPtr
46− | FAny Type
47− | FUnit
48−
49−FInt : FTy
50−FInt = FIntT ITNative
51−
52−FChar : FTy
53−FChar = FIntT ITChar
54−
55−FByte : FTy
56−FByte = FIntT IT8
57−
58−FShort : FTy
59−FShort = FIntT IT16
60−
61−FLong : FTy
62−FLong = FIntT IT64
63−
64−FBits8 : FTy
65−FBits8 = FIntT IT8
66−
67−FBits16 : FTy
68−FBits16 = FIntT IT16
69−
70−FBits32 : FTy
71−FBits32 = FIntT IT32
72−
73−FBits64 : FTy
74−FBits64 = FIntT IT64
75−
76−FBits8x16 : FTy
77−FBits8x16 = FIntT IT8x16
78−
79−FBits16x8 : FTy
80−FBits16x8 = FIntT IT16x8
81−
82−FBits32x4 : FTy
83−FBits32x4 = FIntT IT32x4
84−
85−FBits64x2 : FTy
86−FBits64x2 = FIntT IT64x2
87−
88−||| Interpret an FFI type as the type of the Idris function that it will become
89−interpFTy : FTy -> Type
90−interpFTy (FIntT ITNative) = Int
91−interpFTy (FIntT ITChar) = Char
92−interpFTy (FIntT IT8) = Bits8
93−interpFTy (FIntT IT16) = Bits16
94−interpFTy (FIntT IT32) = Bits32
95−interpFTy (FIntT IT64) = Bits64
96−interpFTy (FAny t) = t
97−interpFTy FFloat = Float
98−interpFTy FString = String
99−interpFTy FPtr = Ptr
100−interpFTy FManagedPtr = ManagedPtr
101−interpFTy (FIntT IT8x16) = Bits8x16
102−interpFTy (FIntT IT16x8) = Bits16x8
103−interpFTy (FIntT IT32x4) = Bits32x4
104−interpFTy (FIntT IT64x2) = Bits64x2
105−interpFTy FUnit = ()
106−
107−interpFTy (FFunction a b) = interpFTy a -> interpFTy b
108−
109−||| Type signatures for foreign functions
110−||| @ xs the argument types
111−||| @ t the return type
112−ForeignTy : (xs : List FTy) -> (t : FTy) -> Type
113−ForeignTy Nil rt = World -> PrimIO (interpFTy rt)
114−ForeignTy (t::ts) rt = interpFTy t -> ForeignTy ts rt
115−
116−
117−data Foreign : Type -> Type where
118− FFun : String -> (xs:List FTy) -> (t:FTy) ->
119− Foreign (ForeignTy xs t)
120−
121−mkForeignPrim : Foreign x -> x
122−mkLazyForeignPrim : Foreign x -> x
123−-- mkForeign and mkLazyForeign compiled as primitives
124−
125−registerPtr : Ptr -> Int -> ManagedPtr
126−registerPtr = prim__registerPtr
127−
12874abstract
129−io_bind : IO a -> (a -> IO b) -> IO b
75+io_bind : IO' l a -> (a -> IO' l b) -> IO' l b
13076io_bind (MkIO fn) k
13177 = MkIO (\w => prim_io_bind (fn w)
13278 (\ b => case k b of
13379 MkIO fkb => fkb w))
13480
13581abstract
136−io_return : a -> IO a
82+io_return : a -> IO' l a
13783io_return x = MkIO (\w => prim_io_return x)
13884
139−liftPrimIO : (World -> PrimIO a) -> IO a
85+liftPrimIO : (World -> PrimIO a) -> IO' l a
14086liftPrimIO = MkIO
14187
142−run__IO : IO () -> PrimIO ()
88+run__IO : IO' l () -> PrimIO ()
14389run__IO (MkIO f) = f TheWorld
14490
91+unsafePerformIO : IO' ffi a -> a
92+unsafePerformIO (MkIO f) = unsafePerformPrimIO
93+ (prim_io_bind (f TheWorld) (\ b => prim_io_return b))
94+
95+--------- The C FFI
96+
97+data Raw a = MkRaw a -- code generated can assume it's compiled just as 'a'
98+
99+-- Supported C integer types
100+data C_IntTypes : Type -> Type where
101+ C_IntChar : C_IntTypes Char
102+ C_IntNative : C_IntTypes Int
103+ C_IntBits8 : C_IntTypes Bits8
104+ C_IntBits16 : C_IntTypes Bits16
105+ C_IntBits32 : C_IntTypes Bits32
106+ C_IntBits64 : C_IntTypes Bits64
107+ C_IntB8x16 : C_IntTypes Bits8x16
108+ C_IntB16x8 : C_IntTypes Bits16x8
109+ C_IntB32x4 : C_IntTypes Bits32x4
110+ C_IntB64x2 : C_IntTypes Bits64x2
111+
112+-- Supported C foreign types
113+data C_Types : Type -> Type where
114+ C_Str : C_Types String
115+ C_Float : C_Types Float
116+ C_Ptr : C_Types Ptr
117+ C_MPtr : C_Types ManagedPtr
118+ C_Unit : C_Types ()
119+ C_Any : C_Types (Raw a)
120+ C_IntT : C_IntTypes i -> C_Types i
121+
122+FFI_C : FFI
123+FFI_C = MkFFI C_Types String
124+
125+IO : Type -> Type
126+IO = IO' FFI_C
127+
145128run__provider : IO a -> PrimIO a
146129run__provider (MkIO f) = f TheWorld
147130
148−-- io_bind v (\v' => io_return v')
149−
150131prim_fork : PrimIO () -> PrimIO Ptr
151132prim_fork x = prim_io_return prim__vm -- compiled specially
152133
@@ -160,11 +141,6 @@ partial
160141prim_fread : Ptr -> IO String
161142prim_fread h = MkIO (\w => prim_io_return (prim__readString h))
162143
163−unsafePerformIO : IO a -> a
164−unsafePerformIO (MkIO f) = unsafePerformPrimIO
165− (prim_io_bind (f TheWorld) (\ b => prim_io_return b))
166−
167−
168144forceGC : IO ()
169−forceGC = mkForeign (FFun "idris_forceGC" [FPtr] FUnit) prim__vm
145+forceGC = foreign FFI_C "idris_forceGC" (Ptr -> IO ()) prim__vm
170146
libs/prelude/Prelude.idr+21−21
@@ -233,7 +233,7 @@ instance Show a => Show (Maybe a) where
233233instance Functor PrimIO where
234234 map f io = prim_io_bind io (prim_io_return . f)
235235
236−instance Functor IO where
236+instance Functor (IO' ffi) where
237237 map f io = io_bind io (\b => io_return (f b))
238238
239239instance Functor Maybe where
@@ -251,7 +251,7 @@ instance Applicative PrimIO where
251251
252252 am <$> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))
253253
254−instance Applicative IO where
254+instance Applicative (IO' ffi) where
255255 pure x = io_return x
256256 f <$> a = io_bind f (\f' =>
257257 io_bind a (\a' =>
@@ -293,7 +293,7 @@ instance Alternative List where
293293instance Monad PrimIO where
294294 b >>= k = prim_io_bind b k
295295
296−instance Monad IO where
296+instance Monad (IO' ffi) where
297297 b >>= k = io_bind b k
298298
299299instance Monad Maybe where
@@ -436,7 +436,7 @@ uniformB64x2 x = prim__mkB64x2 x x
436436||| Output a string to stdout without a trailing newline
437437partial
438438putStr : String -> IO ()
439−putStr x = mkForeign (FFun "putStr" [FString] FUnit) x
439+putStr x = foreign FFI_C "putStr" (String -> IO ()) x
440440
441441||| Output a string to stdout with a trailing newline
442442partial
@@ -456,12 +456,12 @@ getLine = prim_fread prim__stdin
456456||| Write a single character to stdout
457457partial
458458putChar : Char -> IO ()
459−putChar c = mkForeign (FFun "putchar" [FInt] FUnit) (cast c)
459+putChar c = foreign FFI_C "putchar" (Int -> IO ()) (cast c)
460460
461461||| Read a single character from stdin
462462partial
463463getChar : IO Char
464−getChar = map cast $ mkForeign (FFun "getchar" [] FInt)
464+getChar = map cast $ foreign FFI_C "getchar" (IO Int)
465465
466466---- some basic file handling
467467
@@ -484,8 +484,8 @@ stderr = FHandle prim__stderr
484484||| Call the RTS's file opening function
485485do_fopen : String -> String -> IO Ptr
486486do_fopen f m
487− = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m
488−
487+ = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m
488+
489489||| Open a file
490490||| @ f the filename
491491||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)
@@ -508,7 +508,7 @@ openFile f m = fopen f (modeStr m) where
508508
509509partial
510510do_fclose : Ptr -> IO ()
511−do_fclose h = mkForeign (FFun "fileClose" [FPtr] FUnit) h
511+do_fclose h = foreign FFI_C "fileClose" (Ptr -> IO ()) h
512512
513513partial
514514closeFile : File -> IO ()
@@ -519,19 +519,19 @@ do_fread : Ptr -> IO String
519519do_fread h = prim_fread h
520520
521521fgetc : File -> IO Char
522−fgetc (FHandle h) = return (cast !(mkForeign (FFun "fgetc" [FPtr] FInt) h))
522+fgetc (FHandle h) = return (cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h))
523523
524524fgetc' : File -> IO (Maybe Char)
525525fgetc' (FHandle h)
526− = do x <- mkForeign (FFun "fgetc" [FPtr] FInt) h
526+ = do x <- foreign FFI_C "fgetc" (Ptr -> IO Int) h
527527 if (x < 0) then return Nothing
528528 else return (Just (cast x))
529529
530530fflush : File -> IO ()
531−fflush (FHandle h) = mkForeign (FFun "fflush" [FPtr] FUnit) h
531+fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h
532532
533533do_popen : String -> String -> IO Ptr
534−do_popen f m = mkForeign (FFun "do_popen" [FString, FString] FPtr) f m
534+do_popen f m = foreign FFI_C "do_popen" (String -> String -> IO Ptr) f m
535535
536536popen : String -> Mode -> IO File
537537popen f m = do ptr <- do_popen f (modeStr m)
@@ -542,7 +542,7 @@ popen f m = do ptr <- do_popen f (modeStr m)
542542 modeStr ReadWrite = "r+"
543543
544544pclose : File -> IO ()
545−pclose (FHandle h) = mkForeign (FFun "pclose" [FPtr] FUnit) h
545+pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h
546546
547547-- mkForeign (FFun "idris_readStr" [FPtr, FPtr] (FAny String))
548548-- prim__vm h
@@ -554,7 +554,7 @@ fread (FHandle h) = do_fread h
554554partial
555555do_fwrite : Ptr -> String -> IO ()
556556do_fwrite h s
557− = mkForeign (FFun "fputStr" [FPtr, FString] FUnit) h s
557+ = foreign FFI_C "fputStr" (Ptr -> String -> IO ()) h s
558558
559559partial
560560fwrite : File -> String -> IO ()
@@ -562,7 +562,7 @@ fwrite (FHandle h) s = do_fwrite h s
562562
563563partial
564564do_feof : Ptr -> IO Int
565−do_feof h = mkForeign (FFun "fileEOF" [FPtr] FInt) h
565+do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h
566566
567567||| Check if a file handle has reached the end
568568feof : File -> IO Bool
@@ -571,31 +571,31 @@ feof (FHandle h) = do eof <- do_feof h
571571
572572partial
573573do_ferror : Ptr -> IO Int
574−do_ferror h = mkForeign (FFun "fileError" [FPtr] FInt) h
574+do_ferror h = foreign FFI_C "fileError" (Ptr -> IO Int) h
575575
576576ferror : File -> IO Bool
577577ferror (FHandle h) = do err <- do_ferror h
578578 return (not (err == 0))
579579
580580fpoll : File -> IO Bool
581−fpoll (FHandle h) = do p <- mkForeign (FFun "fpoll" [FPtr] FInt) h
581+fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h
582582 return (p > 0)
583583
584584||| Check if a foreign pointer is null
585585partial
586586nullPtr : Ptr -> IO Bool
587−nullPtr p = do ok <- mkForeign (FFun "isNull" [FPtr] FInt) p
587+nullPtr p = do ok <- foreign FFI_C "isNull" (Ptr -> IO Int) p
588588 return (ok /= 0)
589589
590590||| Check if a supposed string was actually a null pointer
591591partial
592592nullStr : String -> IO Bool
593−nullStr p = do ok <- mkForeign (FFun "isNull" [FString] FInt) p
593+nullStr p = do ok <- foreign FFI_C "isNull" (String -> IO Int) p
594594 return (ok /= 0)
595595
596596||| Pointer equality
597597eqPtr : Ptr -> Ptr -> IO Bool
598−eqPtr x y = do eq <- mkForeign (FFun "idris_eqPtr" [FPtr, FPtr] FInt) x y
598+eqPtr x y = do eq <- foreign FFI_C "idris_eqPtr" (Ptr -> Ptr -> IO Int) x y
599599 return (eq /= 0)
600600
601601||| Check whether a file handle is actually a null pointer
src/IRTS/Bytecode.hs+5−6
@@ -5,6 +5,7 @@ module IRTS.Bytecode where
55
66import IRTS.Lang
77import IRTS.Simplified
8+import IRTS.Defunctionalise
89import Idris.Core.TT
910import Data.Maybe
1011
@@ -69,10 +70,8 @@ data BC =
6970 -- same, perhaps exists just for TCO
7071 | TAILCALL Name
7172
72− -- set reg to (apply string args), FLang argument is the language to
73− -- be called. FType is the foreign language type, which may be used to
74− -- control marshaling.
75− | FOREIGNCALL Reg FLang FType String [(FType, Reg)]
73+ -- set reg to (apply string args),
74+ | FOREIGNCALL Reg FDesc DExp [(FDesc, Reg)]
7675
7776 -- move this number of elements from TOP to BASE
7877 | SLIDE Int
@@ -132,8 +131,8 @@ bc reg (SApp False f vs) r =
132131bc reg (SApp True f vs) r
133132 = RESERVE (length vs) : moveReg 0 vs
134133 ++ [SLIDE (length vs), TOPBASE (length vs), TAILCALL f]
135−bc reg (SForeign l t fname args) r
136− = FOREIGNCALL reg l t fname (map farg args) : clean r
134+bc reg (SForeign t fname args) r
135+ = FOREIGNCALL reg t fname (map farg args) : clean r
137136 where farg (ty, Loc i) = (ty, L i)
138137bc reg (SLet (Loc i) e sc) r = bc (L i) e False ++ bc reg sc r
139138bc reg (SUpdate (Loc i) sc) r = bc reg sc False ++ [ASSIGN (L i) reg]
src/IRTS/CodegenC.hs+34−6
@@ -4,6 +4,7 @@ import Idris.AbsSyntax
44import IRTS.Bytecode
55import IRTS.Lang
66import IRTS.Simplified
7+import IRTS.Defunctionalise
78import IRTS.System
89import IRTS.CodegenCommon
910import Idris.Core.TT
@@ -20,6 +21,8 @@ import System.Directory
2021import System.FilePath ((</>), (<.>))
2122import Control.Monad
2223
24+import Debug.Trace
25+
2326codegenC :: CodeGenerator
2427codegenC ci = codegenC' (simpleDecls ci)
2528 (outputFile ci)
@@ -274,16 +277,41 @@ bcc i (TOPBASE n) = indent i ++ "TOPBASE(" ++ show n ++ ");\n"
274277bcc i (BASETOP n) = indent i ++ "BASETOP(" ++ show n ++ ");\n"
275278bcc i STOREOLD = indent i ++ "STOREOLD;\n"
276279bcc i (OP l fn args) = indent i ++ doOp (creg l ++ " = ") fn args ++ ";\n"
277−bcc i (FOREIGNCALL l LANG_C rty fn args)
280+bcc i (FOREIGNCALL l rty (DConst (Str fn)) args)
278281 = indent i ++
279− c_irts rty (creg l ++ " = ")
282+ c_irts (toFType rty) (creg l ++ " = ")
280283 (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"
281− where fcall (t, arg) = irts_c t (creg arg)
284+ where fcall (t, arg) = irts_c (toFType t) (creg arg)
282285bcc i (NULL r) = indent i ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed
283286bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); fprintf(stderr, \"\\n\"); exit(-1); exit(-1);"
284−-- bcc i _ = indent i ++ "// not done yet\n"
285−
286−
287+-- bcc i c = error (show c) -- indent i ++ "// not done yet\n"
288+
289+-- Deconstruct the Foreign type in the defunctionalised expression and build
290+-- a foreign type description for c_irts and irts_c
291+toAType (FCon i)
292+ | i == sUN "C_IntChar" = ATInt ITChar
293+ | i == sUN "C_IntNative" = ATInt ITNative
294+ | i == sUN "C_IntBits8" = ATInt (ITFixed IT8)
295+ | i == sUN "C_IntBits16" = ATInt (ITFixed IT16)
296+ | i == sUN "C_IntBits32" = ATInt (ITFixed IT32)
297+ | i == sUN "C_IntBits64" = ATInt (ITFixed IT64)
298+ | i == sUN "C_IntB8x16" = ATInt (ITVec IT8 16)
299+ | i == sUN "C_IntB16x8" = ATInt (ITVec IT16 8)
300+ | i == sUN "C_IntB32x4" = ATInt (ITVec IT32 4)
301+ | i == sUN "C_IntB64x2" = ATInt (ITVec IT64 2)
302+toAType t = error (show t ++ " not defined in toAType")
303+
304+toFType (FCon c)
305+ | c == sUN "C_Str" = FString
306+ | c == sUN "C_Float" = FArith ATFloat
307+ | c == sUN "C_Ptr" = FPtr
308+ | c == sUN "C_MPtr" = FManagedPtr
309+ | c == sUN "C_Unit" = FUnit
310+toFType (FApp c [_,ity])
311+ | c == sUN "C_IntT" = FArith (toAType ity)
312+toFType (FApp c [_])
313+ | c == sUN "C_Any" = FAny
314+toFType t = error (show t ++ " not defined in toFType")
287315
288316c_irts (FArith (ATInt ITNative)) l x = l ++ "MKINT((i_int)(" ++ x ++ "))"
289317c_irts (FArith (ATInt ITChar)) l x = c_irts (FArith (ATInt ITNative)) l x
src/IRTS/CodegenJavaScript.hs+1−1
@@ -1332,7 +1332,7 @@ translateBC info bc
13321332 | NULL r <- bc = jsNULL info r
13331333 | CALL n <- bc = jsCALL info n
13341334 | TAILCALL n <- bc = jsTAILCALL info n
1335− | FOREIGNCALL r _ _ n a <- bc = jsFOREIGN info r n a
1335+ | FOREIGNCALL r _ n a <- bc = error "jsFOREIGN info r n a"
13361336 | TOPBASE n <- bc = jsTOPBASE info n
13371337 | BASETOP n <- bc = jsBASETOP info n
13381338 | STOREOLD <- bc = jsSTOREOLD info
src/IRTS/Compiler.hs+26−4
@@ -218,7 +218,7 @@ irTerm :: Vars -> [Name] -> Term -> Idris LExp
218218irTerm vs env tm@(App f a) = case unApply tm of
219219 (P _ (UN m) _, args)
220220 | m == txt "mkForeignPrim"
221− -> doForeign vs env args
221+ -> doForeign vs env (reverse (drop 4 args)) -- drop implicits
222222
223223 (P _ (UN u) _, [_, arg])
224224 | u == txt "unsafePerformPrimIO"
@@ -434,9 +434,30 @@ irTerm vs env (TType _) = return $ LNothing
434434irTerm vs env Erased = return $ LNothing
435435irTerm vs env Impossible = return $ LNothing
436436
437−doForeign :: Vars -> [Name] -> [TT Name] -> Idris LExp
438−doForeign vs env (_ : fgn : args)
439− | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
437+doForeign :: Vars -> [Name] -> [Term] -> Idris LExp
438+doForeign vs env (ret : fname : world : args)
439+ = do args' <- mapM splitArg args
440+ fname' <- irTerm vs env fname
441+ let ret' = toFDesc ret
442+ return $ LForeign ret' fname' args'
443+ where
444+ splitArg tm | (_, [_,_,l,r]) <- unApply tm -- pair, two implicits
445+ = do let l' = toFDesc l
446+ r' <- irTerm vs env r
447+ return (l', r')
448+ splitArg _ = ifail "Badly formed foreign function call"
449+
450+ toFDesc tm
451+ | (P _ n _, []) <- unApply tm = FCon (deNS n)
452+ | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDesc as)
453+ toFDesc _ = FUnknown
454+
455+ deNS (NS n _) = n
456+ deNS n = n
457+doForeign vs env xs = ifail "Badly formed foreign function call"
458+
459+{-
460+ - | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
440461 = case getFTypes fgnArgTys of
441462 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
442463 Just tys -> do
@@ -502,6 +523,7 @@ doForeign vs env (_ : fgn : args)
502523 mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
503524 mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
504525 mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
526+-}
505527
506528irTree :: [Name] -> SC -> Idris LExp
507529irTree args tree = do
src/IRTS/Defunctionalise.hs+10−7
@@ -22,7 +22,7 @@ data DExp = DV LVar
2222 | DCase CaseType DExp [DAlt]
2323 | DChkCase DExp [DAlt] -- a case where the type is unknown (for EVAL/APPLY)
2424 | DConst Const
25− | DForeign FLang FType String [(FType, DExp)]
25+ | DForeign FDesc DExp [(FDesc, DExp)]
2626 | DOp PrimFn [DExp]
2727 | DNothing -- erased value, can be compiled to anything since it'll never
2828 -- be inspected
@@ -110,7 +110,10 @@ addApps defs (n, LFun _ _ args e)
110110 alts' <- mapM (aaAlt env) alts
111111 return $ DCase up e' alts'
112112 aa env (LConst c) = return $ DConst c
113− aa env (LForeign l t n args) = liftM (DForeign l t n) (mapM (aaF env) args)
113+ aa env (LForeign t n args)
114+ = do n' <- aa env n
115+ args' <- mapM (aaF env) args
116+ return $ DForeign t n' args'
114117 aa env (LOp LFork args) = liftM (DOp LFork) (mapM (aa env) args)
115118 aa env (LOp f args) = do args' <- mapM (aa env) args
116119 return $ DOp f args'
@@ -173,7 +176,7 @@ addApps defs (n, LFun _ _ args e)
173176 needsEval x (DLet n v e)
174177 | x == n = needsEval x v
175178 | otherwise = needsEval x v || needsEval x e
176− needsEval x (DForeign _ _ _ args) = or (map (needsEval x) (map snd args))
179+ needsEval x (DForeign _ _ args) = or (map (needsEval x) (map snd args))
177180 needsEval x (DOp op args) = or (map (needsEval x) args)
178181 needsEval x (DProj (DV (Glob x')) _) = x == x'
179182 needsEval x _ = False
@@ -257,13 +260,13 @@ mkUnderCon n missing = sMN missing ("U_" ++ show n)
257260instance Show DExp where
258261 show e = show' [] e where
259262 show' env (DV (Loc i)) = "var " ++ env!!i
260− show' env (DV (Glob n)) = show n
263+ show' env (DV (Glob n)) = "GLOB " ++ show n
261264 show' env (DApp _ e args) = show e ++ "(" ++
262265 showSep ", " (map (show' env) args) ++")"
263266 show' env (DLet n v e) = "let " ++ show n ++ " = " ++ show' env v ++ " in " ++
264267 show' (env ++ [show n]) e
265268 show' env (DUpdate n e) = "!update " ++ show n ++ "(" ++ show' env e ++ ")"
266− show' env (DC loc i n args) = atloc loc ++ show n ++ "(" ++ showSep ", " (map (show' env) args) ++ ")"
269+ show' env (DC loc i n args) = atloc loc ++ "CON " ++ show n ++ "(" ++ showSep ", " (map (show' env) args) ++ ")"
267270 where atloc Nothing = ""
268271 atloc (Just l) = "@" ++ show (LV l) ++ ":"
269272 show' env (DProj t i) = show t ++ "!" ++ show i
@@ -275,8 +278,8 @@ instance Show DExp where
275278 show' env (DChkCase e alts) = "case' " ++ show' env e ++ " of {\n\t" ++
276279 showSep "\n\t| " (map (showAlt env) alts)
277280 show' env (DConst c) = show c
278− show' env (DForeign lang ty n args)
279− = "foreign " ++ n ++ "(" ++ showSep ", " (map (show' env) (map snd args)) ++ ")"
281+ show' env (DForeign ty n args)
282+ = "foreign " ++ show' env n ++ "(" ++ showSep ", " (map (show' env) (map snd args)) ++ ")"
280283 show' env (DOp f args) = show f ++ "(" ++ showSep ", " (map (show' env) args) ++ ")"
281284 show' env (DError str) = "error " ++ show str
282285 show' env DNothing = "____"
src/IRTS/DumpBC.hs+2−2
@@ -51,8 +51,8 @@ serializeBC n bc = indent n ++
5151 maybe "" (\def' -> "\n" ++ serializeDefault (n + 1) def') def
5252 CALL x -> "CALL " ++ show x
5353 TAILCALL x -> "TAILCALL " ++ show x
54− FOREIGNCALL r _ ret name args ->
55− "FOREIGNCALL " ++ serializeReg r ++ " \"" ++ name ++ "\" " ++ show ret ++
54+ FOREIGNCALL r ret name args ->
55+ "FOREIGNCALL " ++ serializeReg r ++ " \"" ++ show name ++ "\" " ++ show ret ++
5656 " [" ++ interMap args ", " (\(ty, r) -> serializeReg r ++ " : " ++ show ty) ++ "]"
5757 SLIDE n -> "SLIDE " ++ show n
5858 REBASE -> "REBASE"
src/IRTS/Lang.hs+17−12
@@ -29,12 +29,19 @@ data LExp = LV LVar
2929 Int Name [LExp]
3030 | LCase CaseType LExp [LAlt]
3131 | LConst Const
32− | LForeign FLang FType String [(FType, LExp)]
32+ | LForeign FDesc -- Function descriptor
33+ LExp -- Return type descriptor
34+ [(FDesc, LExp)] -- first LExp is the FFI type description
3335 | LOp PrimFn [LExp]
3436 | LNothing
3537 | LError String
3638 deriving Eq
3739
40+data FDesc = FCon Name
41+ | FUnknown
42+ | FApp Name [FDesc]
43+ deriving (Show, Eq)
44+
3845-- Primitive operators. Backends are not *required* to implement all
3946-- of these, but should report an error if they are unable
4047
@@ -85,9 +92,6 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy
8592data FCallType = FStatic | FObject | FConstructor
8693 deriving (Show, Eq)
8794
88−data FLang = LANG_C | LANG_JAVA FCallType
89− deriving (Show, Eq)
90−
9195data FType = FArith ArithTy
9296 | FFunction
9397 | FFunctionIO
@@ -192,8 +196,9 @@ lift env (LCase up e alts) = do alts' <- mapM liftA alts
192196 liftA (LDefaultCase e) = do e' <- lift env e
193197 return (LDefaultCase e')
194198lift env (LConst c) = return (LConst c)
195−lift env (LForeign l t s args) = do args' <- mapM (liftF env) args
196− return (LForeign l t s args')
199+lift env (LForeign t s args) = do args' <- mapM (liftF env) args
200+ s' <- lift env s
201+ return (LForeign t s' args')
197202 where
198203 liftF env (t, e) = do e' <- lift env e
199204 return (t, e')
@@ -231,9 +236,9 @@ allocUnique defs (n, LFun opts fn args e)
231236 = do avail <- get
232237 v <- findVar [] avail (length es)
233238 LCon v i n <$> mapM findUp es
234− findUp (LForeign l t s es)
235− = LForeign l t s <$> mapM (\ (t, e) -> do e' <- findUp e
236− return (t, e')) es
239+ findUp (LForeign t s es)
240+ = LForeign t s <$> mapM (\ (t, e) -> do e' <- findUp e
241+ return (t, e')) es
237242 findUp (LOp o es) = LOp o <$> mapM findUp es
238243 findUp (LCase Updatable e@(LV (Glob n)) as)
239244 = LCase Updatable e <$> mapM (doUpAlt n) as
@@ -282,7 +287,7 @@ usedIn env (LCase up e alts) = usedIn env e ++ concatMap (usedInA env) alts
282287 where usedInA env (LConCase i n ns e) = usedIn env e
283288 usedInA env (LConstCase c e) = usedIn env e
284289 usedInA env (LDefaultCase e) = usedIn env e
285−usedIn env (LForeign _ _ _ args) = concatMap (usedIn env) (map snd args)
290+usedIn env (LForeign _ _ args) = concatMap (usedIn env) (map snd args)
286291usedIn env (LOp f args) = concatMap (usedIn env) args
287292usedIn env _ = []
288293
@@ -329,9 +334,9 @@ instance Show LExp where
329334
330335 show' env ind (LConst c) = show c
331336
332− show' env ind (LForeign lang ty n args) = concat
337+ show' env ind (LForeign ty n args) = concat
333338 [ "foreign{ "
334− , n ++ "("
339+ , show' env ind n ++ "("
335340 , showSep ", " (map (\(ty,x) -> show' env ind x ++ " : " ++ show ty) args)
336341 , ") : "
337342 , show ty
src/IRTS/LangOpts.hs+3−3
@@ -64,9 +64,9 @@ doInline defs (LFun opts topn args exp)
6464 inlineWith (n : done) (zip args es' ++ env) body
6565 inlineWith done env (LApp t f es)
6666 = LApp t <$> inlineWith done env f <*> mapM (inlineWith done env) es
67− inlineWith done env (LForeign l t s args)
68− = LForeign l t s <$> mapM (\(t, e) -> do e' <- inlineWith done env e
69− return (t, e')) args
67+ inlineWith done env (LForeign t s args)
68+ = LForeign t s <$> mapM (\(t, e) -> do e' <- inlineWith done env e
69+ return (t, e')) args
7070 inlineWith done env t = return t
7171
7272 inlineWithAlt done env (LConCase i n es rhs)
src/IRTS/Simplified.hs+7−5
@@ -22,7 +22,9 @@ data SExp = SV LVar
2222 | SChkCase LVar [SAlt]
2323 | SProj LVar Int
2424 | SConst Const
25− | SForeign FLang FType String [(FType, LVar)]
25+ -- Keep DExps for describing foreign things, because they get
26+ -- translated differently
27+ | SForeign FDesc DExp [(FDesc, LVar)]
2628 | SOp PrimFn [LVar]
2729 | SNothing -- erased value, will never be inspected
2830 | SError String
@@ -54,10 +56,10 @@ simplify tl (DV (Glob x))
5456 _ -> return $ SV (Glob x)
5557simplify tl (DApp tc n args) = do args' <- mapM sVar args
5658 mkapp (SApp (tl || tc) n) args'
57−simplify tl (DForeign lang ty fn args)
59+simplify tl (DForeign ty fn args)
5860 = do args' <- mapM sVar (map snd args)
5961 let fargs = zip (map fst args) args'
60− mkfapp (SForeign lang ty fn) fargs
62+ mkfapp (SForeign ty fn) fargs
6163simplify tl (DLet n v e) = do v' <- simplify False v
6264 e' <- simplify tl e
6365 return (SLet (Glob n) v' e')
@@ -159,10 +161,10 @@ scopecheck fn ctxt envTop tm = sc envTop tm where
159161 " has arity " ++ show ar
160162 Just _ -> return $ SApp tc f args'
161163 Nothing -> failsc $ "No such variable " ++ show f
162− sc env (SForeign l ty f args)
164+ sc env (SForeign ty f args)
163165 = do args' <- mapM (\ (t, a) -> do a' <- scVar env a
164166 return (t, a')) args
165− return $ SForeign l ty f args'
167+ return $ SForeign ty f args'
166168 sc env (SCon loc tag f args)
167169 = do loc' <- case loc of
168170 Nothing -> return Nothing
src/Idris/Core/DeepSeq.hs+1−1
@@ -200,7 +200,7 @@ instance NFData Def where
200200 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
201201
202202instance NFData CaseInfo where
203− rnf (CaseInfo x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
203+ rnf (CaseInfo x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
204204
205205instance NFData CaseDefs where
206206 rnf (CaseDefs x1 x2 x3 x4)
src/Idris/Core/Evaluate.hs+9−6
@@ -208,9 +208,10 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
208208
209209 -- returns 'True' if the function should block
210210 -- normal evaluation should return false
211− blockSimplify (CaseInfo inl dict) n stk
211+ blockSimplify (CaseInfo inl always dict) n stk
212212 | RunTT `elem` opts
213− = not (inl || dict) || elem n stk
213+ = if always then False
214+ else not (inl || dict) || elem n stk
214215 | Simplify `elem` opts
215216 = (not (inl || dict) || elem n stk)
216217 || (n == sUN "prim__syntactic_eq")
@@ -679,7 +680,8 @@ data CaseDefs = CaseDefs {
679680 }
680681
681682data CaseInfo = CaseInfo {
682− case_inlinable :: Bool,
683+ case_inlinable :: Bool, -- decided by machine
684+ case_alwaysinline :: Bool, -- decided by %inline flag
683685 tc_dictionary :: Bool
684686 }
685687
@@ -706,7 +708,7 @@ instance Show Def where
706708 show (Function ty tm) = "Function: " ++ show (ty, tm)
707709 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty
708710 show (Operator ty _ _) = "Operator: " ++ show ty
709− show (CaseOp (CaseInfo inlc inlr) ty atys ps_in ps cd)
711+ show (CaseOp (CaseInfo inlc inla inlr) ty atys ps_in ps cd)
710712 = let (ns, sc) = cases_compiletime cd
711713 (ns_t, sc_t) = cases_totcheck cd
712714 (ns', sc') = cases_runtime cd in
@@ -717,7 +719,8 @@ instance Show Def where
717719 show ns ++ " " ++ show sc ++ "\n\n" ++
718720 "RUN TIME:\n\n" ++
719721 show ns' ++ " " ++ show sc' ++ "\n\n" ++
720− if inlc then "Inlinable\n" else "Not inlinable\n"
722+ if inlc then "Inlinable" else "Not inlinable" ++
723+ if inla then " Aggressively\n" else "\n"
721724
722725-------
723726
@@ -865,7 +868,7 @@ addCasedef :: Name -> ErasureInfo -> CaseInfo ->
865868 [([Name], Term, Term)] -> -- inlined
866869 [([Name], Term, Term)] -> -- run time
867870 Type -> Context -> Context
868−addCasedef n ei ci@(CaseInfo alwaysInline tcdict)
871+addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)
869872 tcase covering reflect asserted argtys inacc
870873 ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt
871874 = let ctxt = definitions uctxt
src/Idris/Core/Execute.hs+124−113
@@ -3,7 +3,7 @@ module Idris.Core.Execute (execute) where
33
44import Idris.AbsSyntax
55import Idris.AbsSyntaxTree
6−import IRTS.Lang(FType(..))
6+import IRTS.Lang(FDesc(..), FType(..))
77
88import Idris.Primitives(Prim(..), primitives)
99
@@ -231,52 +231,85 @@ execApp env ctxt con@(EP _ fp _) args@(tp:v:rest)
231231 | fp == pioret = execApp env ctxt (mkEApp con [tp, v]) rest
232232
233233-- Special cases arising from not having access to the C RTS in the interpreter
234−execApp env ctxt (EP _ fp _) (_:fn:str:_:rest)
234+execApp env ctxt f@(EP _ fp _) args@(xs:_:_:_:args')
235235 | fp == mkfprim,
236− Just (FFun "putStr" _ _) <- foreignFromTT fn
237− = case str of
238− EConstant (Str arg) -> do execIO (putStr arg)
239− execApp env ctxt ioUnit rest
240− _ -> execFail . Msg $
241− "The argument to putStr should be a constant string, but it was " ++
242− show str ++
243− ". Are all cases covered?"
244−execApp env ctxt (EP _ fp _) (_:fn:ch:_:rest)
245− | fp == mkfprim,
246− Just (FFun "putchar" _ _) <- foreignFromTT fn
236+ (ty : fn : w : rest) <- reverse args' =
237+ execForeign env ctxt getArity ty fn rest (mkEApp f args)
238+ where getArity = case unEList xs of
239+ Just as -> length as
240+ _ -> 0
241+
242+execApp env ctxt c@(EP (DCon _ arity _) n _) args =
243+ do let args' = take arity args
244+ let restArgs = drop arity args
245+ execApp env ctxt (mkEApp c args') restArgs
246+
247+execApp env ctxt c@(EP (TCon _ arity) n _) args =
248+ do let args' = take arity args
249+ let restArgs = drop arity args
250+ execApp env ctxt (mkEApp c args') restArgs
251+
252+execApp env ctxt f@(EP _ n _) args =
253+ do let val = lookupDef n ctxt
254+ case val of
255+ [Function _ tm] -> fail "should already have been eval'd"
256+ [TyDecl nt ty] -> return $ mkEApp f args
257+ [Operator tp arity op] ->
258+ if length args >= arity
259+ then let args' = take arity args in
260+ case getOp n args' of
261+ Just res -> do r <- res
262+ execApp env ctxt r (drop arity args)
263+ Nothing -> return (mkEApp f args)
264+ else return (mkEApp f args)
265+ [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
266+ do rhs <- doExec env ctxt tm
267+ execApp env ctxt rhs args
268+ [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->
269+ do res <- execCase env ctxt ns sc args
270+ return $ fromMaybe (mkEApp f args) res
271+ thing -> return $ mkEApp f args
272+execApp env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
273+ let (f', as) = unApplyV ret
274+ execApp env ctxt f' (as ++ args)
275+execApp env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp env ctxt f (args1 ++ args2)
276+execApp env ctxt f args = return (mkEApp f args)
277+
278+execForeign env ctxt arity ty fn xs onfail
279+ | Just (FFun "putStr" [(_, str)] _) <- foreignFromTT arity ty fn xs
280+ = case str of
281+ EConstant (Str arg) -> do execIO (putStr arg)
282+ execApp env ctxt ioUnit (drop arity xs)
283+ _ -> execFail . Msg $
284+ "The argument to putStr should be a constant string, but it was " ++
285+ show str ++
286+ ". Are all cases covered?"
287+ | Just (FFun "putchar" [(_, ch)] _) <- foreignFromTT arity ty fn xs
247288 = case ch of
248289 EConstant (Ch c) -> do execIO (putChar c)
249− execApp env ctxt ioUnit rest
290+ execApp env ctxt ioUnit (drop arity xs)
250291 EConstant (I i) -> do execIO (putChar (toEnum i))
251− execApp env ctxt ioUnit rest
292+ execApp env ctxt ioUnit (drop arity xs)
252293 _ -> execFail . Msg $
253294 "The argument to putchar should be a constant character, but it was " ++
254295 show str ++
255296 ". Are all cases covered?"
256−execApp env ctxt (EP _ fp _) (_:fn:_:handle:_:rest)
257− | fp == mkfprim,
258− Just (FFun "idris_readStr" _ _) <- foreignFromTT fn
297+ | Just (FFun "idris_readStr" [_, (_, handle)] _) <- foreignFromTT arity ty fn xs
259298 = case handle of
260299 EHandle h -> do contents <- execIO $ hGetLine h
261− execApp env ctxt (EConstant (Str (contents ++ "\n"))) rest
300+ execApp env ctxt (EConstant (Str (contents ++ "\n"))) (drop arity xs)
262301 _ -> execFail . Msg $
263302 "The argument to idris_readStr should be a handle, but it was " ++
264303 show handle ++
265304 ". Are all cases covered?"
266−execApp env ctxt (EP _ fp _) (_:fn:_:rest)
267− | fp == mkfprim,
268− Just (FFun "getchar" _ _) <- foreignFromTT fn
305+ | Just (FFun "getchar" _ _) <- foreignFromTT arity ty fn xs
269306 = do -- The C API returns an Int which Idris library code
270307 -- converts; thus, we must make an int here.
271308 ch <- execIO $ fmap (ioWrap . EConstant . I . fromEnum) getChar
272− execApp env ctxt ch rest
273−execApp env ctxt (EP _ fp _) (_:fn:rest)
274− | fp == mkfprim,
275− Just (FFun "idris_time" _ _) <- foreignFromTT fn
309+ execApp env ctxt ch xs
310+ | Just (FFun "idris_time" _ _) <- foreignFromTT arity ty fn xs
276311 = do execIO $ fmap (ioWrap . EConstant . I . round) getPOSIXTime
277−execApp env ctxt (EP _ fp _) (_:fn:fileStr:modeStr:rest)
278− | fp == mkfprim,
279− Just (FFun "fileOpen" _ _) <- foreignFromTT fn
312+ | Just (FFun "fileOpen" [(_,fileStr), (_,modeStr)] _) <- foreignFromTT arity ty fn xs
280313 = case (fileStr, modeStr) of
281314 (EConstant (Str f), EConstant (Str mode)) ->
282315 do f <- execIO $
@@ -291,10 +324,10 @@ execApp env ctxt (EP _ fp _) (_:fn:fileStr:modeStr:rest)
291324 case fmap (openFile f) m of
292325 Right h -> do h' <- h
293326 hSetBinaryMode h' True
294− return $ Right (ioWrap (EHandle h'), tail rest)
327+ return $ Right (ioWrap (EHandle h'), drop arity xs)
295328 Left err -> return $ Left err)
296329 (\e -> let _ = ( e::SomeException)
297− in return $ Right (ioWrap (EPtr nullPtr), tail rest))
330+ in return $ Right (ioWrap (EPtr nullPtr), drop arity xs))
298331 case f of
299332 Left err -> execFail . Msg $ err
300333 Right (res, rest) -> execApp env ctxt res rest
@@ -302,105 +335,72 @@ execApp env ctxt (EP _ fp _) (_:fn:fileStr:modeStr:rest)
302335 "The arguments to fileOpen should be constant strings, but they were " ++
303336 show fileStr ++ " and " ++ show modeStr ++
304337 ". Are all cases covered?"
305−
306−execApp env ctxt (EP _ fp _) (_:fn:handle:rest)
307− | fp == mkfprim,
308− Just (FFun "fileEOF" _ _) <- foreignFromTT fn
338+ | Just (FFun "fileEOF" [(_,handle)] _) <- foreignFromTT arity ty fn xs
309339 = case handle of
310340 EHandle h -> do eofp <- execIO $ hIsEOF h
311341 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
312− execApp env ctxt res (tail rest)
342+ execApp env ctxt res (drop arity xs)
313343 _ -> execFail . Msg $
314344 "The argument to fileEOF should be a file handle, but it was " ++
315345 show handle ++
316346 ". Are all cases covered?"
317−
318−execApp env ctxt (EP _ fp _) (_:fn:handle:rest)
319− | fp == mkfprim,
320− Just (FFun "fileClose" _ _) <- foreignFromTT fn
347+ | Just (FFun "fileClose" [(_,handle)] _) <- foreignFromTT arity ty fn xs
321348 = case handle of
322349 EHandle h -> do execIO $ hClose h
323− execApp env ctxt ioUnit (tail rest)
350+ execApp env ctxt ioUnit (drop arity xs)
324351 _ -> execFail . Msg $
325352 "The argument to fileClose should be a file handle, but it was " ++
326353 show handle ++
327354 ". Are all cases covered?"
328355
329−execApp env ctxt (EP _ fp _) (_:fn:ptr:rest)
330− | fp == mkfprim,
331− Just (FFun "isNull" _ _) <- foreignFromTT fn
356+ | Just (FFun "isNull" [(_, ptr)] _) <- foreignFromTT arity ty fn xs
332357 = case ptr of
333358 EPtr p -> let res = ioWrap . EConstant . I $
334359 if p == nullPtr then 1 else 0
335− in execApp env ctxt res (tail rest)
360+ in execApp env ctxt res (drop arity xs)
336361 -- Handles will be checked as null pointers sometimes - but if we got a
337362 -- real Handle, then it's valid, so just return 1.
338363 EHandle h -> let res = ioWrap . EConstant . I $ 0
339− in execApp env ctxt res (tail rest)
364+ in execApp env ctxt res (drop arity xs)
340365 -- A foreign-returned char* has to be tested for NULL sometimes
341366 EConstant (Str s) -> let res = ioWrap . EConstant . I $ 0
342− in execApp env ctxt res (tail rest)
367+ in execApp env ctxt res (drop arity xs)
343368 _ -> execFail . Msg $
344369 "The argument to isNull should be a pointer or file handle or string, but it was " ++
345370 show ptr ++
346371 ". Are all cases covered?"
347372
348−
349373-- Right now, there's no way to send command-line arguments to the executor,
350374-- so just return 0.
351−execApp env ctxt (EP _ fp _) (_:fn:rest)
352− | fp == mkfprim,
353− Just (FFun "idris_numArgs" _ _) <- foreignFromTT fn
375+execForeign env ctxt arity ty fn xs onfail
376+ | Just (FFun "idris_numArgs" _ _) <- foreignFromTT arity ty fn xs
354377 = let res = ioWrap . EConstant . I $ 0
355− in execApp env ctxt res (tail rest)
356−
357−execApp env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim
358− = case foreignFromTT fn of
359− Just (FFun f argTs retT) | length xs >= length argTs ->
360− do let (args', xs') = (take (length argTs) xs, -- foreign args
361− drop (length argTs + 1) xs) -- rest
362− res <- stepForeign (ty:fn:args')
378+ in execApp env ctxt res (drop arity xs)
379+
380+execForeign env ctxt arity ty fn xs onfail
381+ = case foreignFromTT arity ty fn xs of
382+ Just ffun@(FFun f argTs retT) | length xs >= arity ->
383+ do let (args', xs') = (take arity xs, -- foreign args
384+ drop arity xs) -- rest
385+ res <- call ffun (map snd argTs)
363386 case res of
364387 Nothing -> fail $ "Could not call foreign function \"" ++ f ++
365− "\" with args " ++ show args
388+ "\" with args " ++ show (map snd argTs)
366389 Just r -> return (mkEApp r xs')
367− Nothing -> return (mkEApp f args)
390+ Nothing -> return onfail
391+
368392
369−execApp env ctxt c@(EP (DCon _ arity _) n _) args =
370− do let args' = take arity args
371− let restArgs = drop arity args
372− execApp env ctxt (mkEApp c args') restArgs
393+splitArg tm | (_, [_,_,l,r]) <- unApplyV tm -- pair, two implicits
394+ = Just (toFDesc l, r)
395+splitArg _ = Nothing
373396
374−execApp env ctxt c@(EP (TCon _ arity) n _) args =
375− do let args' = take arity args
376− let restArgs = drop arity args
377− execApp env ctxt (mkEApp c args') restArgs
397+toFDesc tm
398+ | (EP _ n _, []) <- unApplyV tm = FCon (deNS n)
399+ | (EP _ n _, as) <- unApplyV tm = FApp (deNS n) (map toFDesc as)
400+toFDesc _ = FUnknown
378401
379−execApp env ctxt f@(EP _ n _) args =
380− do let val = lookupDef n ctxt
381− case val of
382− [Function _ tm] -> fail "should already have been eval'd"
383− [TyDecl nt ty] -> return $ mkEApp f args
384− [Operator tp arity op] ->
385− if length args >= arity
386− then let args' = take arity args in
387− case getOp n args' of
388− Just res -> do r <- res
389− execApp env ctxt r (drop arity args)
390− Nothing -> return (mkEApp f args)
391− else return (mkEApp f args)
392− [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
393− do rhs <- doExec env ctxt tm
394− execApp env ctxt rhs args
395− [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->
396− do res <- execCase env ctxt ns sc args
397− return $ fromMaybe (mkEApp f args) res
398− thing -> return $ mkEApp f args
399−execApp env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
400− let (f', as) = unApplyV ret
401− execApp env ctxt f' (as ++ args)
402−execApp env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp env ctxt f (args1 ++ args2)
403−execApp env ctxt f args = return (mkEApp f args)
402+deNS (NS n _) = n
403+deNS n = n
404404
405405prs = sUN "prim__readString"
406406pbm = sUN "prim__believe_me"
@@ -494,13 +494,35 @@ idrisType ft = EConstant (idr ft)
494494 idr FString = StrType
495495 idr FPtr = PtrType
496496
497−data Foreign = FFun String [FType] FType deriving Show
498−
497+data Foreign = FFun String [(FDesc, ExecVal)] FDesc deriving Show
498+
499+toFType :: FDesc -> FType
500+toFType (FCon c)
501+ | c == sUN "C_Str" = FString
502+ | c == sUN "C_Float" = FArith ATFloat
503+ | c == sUN "C_Ptr" = FPtr
504+ | c == sUN "C_MPtr" = FManagedPtr
505+ | c == sUN "C_Unit" = FUnit
506+toFType (FApp c [_,ity])
507+ | c == sUN "C_IntT" = FArith (toAType ity)
508+ where toAType (FCon i)
509+ | i == sUN "C_IntChar" = ATInt ITChar
510+ | i == sUN "C_IntNative" = ATInt ITNative
511+ | i == sUN "C_IntBits8" = ATInt (ITFixed IT8)
512+ | i == sUN "C_IntBits16" = ATInt (ITFixed IT16)
513+ | i == sUN "C_IntBits32" = ATInt (ITFixed IT32)
514+ | i == sUN "C_IntBits64" = ATInt (ITFixed IT64)
515+ toAType t = error (show t ++ " not defined in toAType")
516+
517+toFType (FApp c [_])
518+ | c == sUN "C_Any" = FAny
519+toFType t = error (show t ++ " not defined in toFType")
499520
500521call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
501522call (FFun name argTypes retType) args =
502523 do fn <- findForeign name
503− maybe (return Nothing) (\f -> Just . ioWrap <$> call' f args retType) fn
524+ maybe (return Nothing)
525+ (\f -> Just . ioWrap <$> call' f args (toFType retType)) fn
504526 where call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal
505527 call' (Fun _ h) args (FArith (ATInt ITNative)) = do
506528 res <- execIO $ callFFI h retCInt (prepArgs args)
@@ -549,15 +571,11 @@ call (FFun name argTypes retType) args =
549571 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined
550572
551573
552−
553−foreignFromTT :: ExecVal -> Maybe Foreign
554−foreignFromTT t = case (unApplyV t) of
555− (_, [(EConstant (Str name)), args, ret]) ->
556− do argTy <- unEList args
557− argFTy <- sequence $ map getFTy argTy
558− retFTy <- getFTy ret
559− return $ FFun name argFTy retFTy
560− _ -> trace ("failed to construct ffun") Nothing
574+foreignFromTT :: Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
575+foreignFromTT arity ty (EConstant (Str name)) args
576+ = do argFTyVals <- mapM splitArg (take arity args)
577+ return $ FFun name argFTyVals (toFDesc ty)
578+foreignFromTT arity ty fn args = trace ("failed to construct ffun from " ++ show (ty,fn,args)) Nothing
561579
562580getFTy :: ExecVal -> Maybe FType
563581getFTy (EApp (EP _ (UN fi) _) (EP _ (UN intTy) _))
@@ -592,13 +610,6 @@ toConst :: Term -> Maybe Const
592610toConst (Constant c) = Just c
593611toConst _ = Nothing
594612
595−stepForeign :: [ExecVal] -> Exec (Maybe ExecVal)
596−stepForeign (ty:fn:args) = let ffun = foreignFromTT fn
597− in case (call <$> ffun) of
598− Just f -> f args
599− Nothing -> return Nothing
600−stepForeign _ = fail "Tried to call foreign function that wasn't mkForeignPrim"
601−
602613mapMaybeM :: (Functor m, Monad m) => (a -> m (Maybe b)) -> [a] -> m [b]
603614mapMaybeM f [] = return []
604615mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
src/Idris/Elab/Clause.hs+2−1
@@ -222,7 +222,7 @@ elabClauses info' fc opts n_in cs =
222222 let opt = idris_optimisation ist
223223 putIState (ist { idris_patdefs = addDef n (force pdef_pe, force pmissing)
224224 (idris_patdefs ist) })
225− let caseInfo = CaseInfo (inlinable opts) (dictionary opts)
225+ let caseInfo = CaseInfo (inlinable opts) (inlinable opts) (dictionary opts)
226226 case lookupTy n ctxt of
227227 [ty] -> do updateContext (addCasedef n erInfo caseInfo
228228 tcase defaultcase
@@ -408,6 +408,7 @@ elabPE info fc caller r =
408408 _ -> True
409409 concreteTm ist (Constant _) = True
410410 concreteTm ist (Bind n (Lam _) sc) = True
411+ concreteTm ist (Bind n (Pi _ _ _) sc) = True
411412 concreteTm ist (Bind n (Let _ _) sc) = concreteTm ist sc
412413 concreteTm ist _ = False
413414
src/Idris/Erasure.hs+7−4
@@ -192,13 +192,16 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
192192 -- These two, Main.main and run__IO, are always evaluated
193193 -- but they elude analysis since they come from the seed term.
194194 [ [(mainName, Result)]
195− , [(sUN "run__IO", Result), (sUN "run__IO", Arg 0)]
195+ , [(sUN "run__IO", Result), (sUN "run__IO", Arg 1)]
196196
197197 -- MkIO is read by run__IO,
198198 -- but this cannot be observed in the source code of programs.
199− , it "MkIO" [1]
199+ , it "MkIO" [2]
200200 , it "prim__IO" [1]
201201
202+ , [(pairCon, Arg 2),
203+ (pairCon, Arg 3)] -- TMP HACK
204+
202205 -- these have been discovered as builtins but are not listed
203206 -- among Idris.Primitives.primitives
204207 --, mn "__MkPair" [2,3]
@@ -380,8 +383,8 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
380383 -- which is the (Foreign a) spec that defines the type
381384 -- and is not needed at runtime.
382385 P _ (UN n) _
383− | n `elem` map T.pack ["mkForeign", "mkForeignPrim", "mkLazyForeignPrim"]
384− -> unconditionalDeps (drop 1 args)
386+ | n `elem` map T.pack ["mkForeignPrim"]
387+ -> unconditionalDeps args -- (drop 1 args)
385388
386389 -- a bound variable might draw in additional dependencies,
387390 -- think: f x = x 0 <-- here, `x' _is_ used
src/Idris/IBC.hs+6−4
@@ -35,7 +35,7 @@ import Codec.Compression.Zlib (compress)
3535import Util.Zlib (decompressEither)
3636
3737ibcVersion :: Word8
38−ibcVersion = 93
38+ibcVersion = 94
3939
4040data IBCFile = IBCFile { ver :: Word8,
4141 sourcefile :: FilePath,
@@ -778,11 +778,13 @@ instance Binary CaseDefs where
778778 return (CaseDefs x2 x2 x2 x4)
779779
780780instance Binary CaseInfo where
781− put x@(CaseInfo x1 x2) = do put x1
782− put x2
781+ put x@(CaseInfo x1 x2 x3) = do put x1
782+ put x2
783+ put x3
783784 get = do x1 <- get
784785 x2 <- get
785− return (CaseInfo x1 x2)
786+ x3 <- get
787+ return (CaseInfo x1 x2 x3)
786788
787789instance Binary Def where
788790 put x
src/Idris/ParseExpr.hs+15−28
@@ -526,34 +526,21 @@ MatchApp ::=
526526@
527527-}
528528app :: SyntaxInfo -> IdrisParser PTerm
529−app syn = do f <- reserved "mkForeign"
529+app syn = do f <- simpleExpr syn
530+ (do try $ reservedOp "<=="
531+ fc <- getFC
532+ ff <- fnName
533+ return (PLet fc (sMN 0 "match")
534+ f
535+ (PMatchApp fc ff)
536+ (PRef fc (sMN 0 "match")))
537+ <?> "matching application expression") <|> (do
530538 fc <- getFC
531− fn <- arg syn
532− args <- many (do notEndApp; arg syn)
533539 i <- get
534− let ap = PApp fc (PRef fc (sUN "liftPrimIO"))
535− [pexp (PLam fc (sMN 0 "w")
536− Placeholder
537− (PApp fc (PRef fc (sUN "mkForeignPrim"))
538− (fn : args ++
539− [pexp (PRef fc (sMN 0 "w"))])))]
540− return (dslify i ap)
541−
542− <|> do f <- simpleExpr syn
543− (do try $ reservedOp "<=="
544− fc <- getFC
545− ff <- fnName
546− return (PLet fc (sMN 0 "match")
547− f
548− (PMatchApp fc ff)
549− (PRef fc (sMN 0 "match")))
550− <?> "matching application expression") <|> (do
551− fc <- getFC
552− i <- get
553− args <- many (do notEndApp; arg syn)
554− case args of
555− [] -> return f
556− _ -> return (dslify i (PApp fc f args)))
540+ args <- many (do notEndApp; arg syn)
541+ case args of
542+ [] -> return f
543+ _ -> return (dslify i (PApp fc f args)))
557544 <?> "function application"
558545 where
559546 dslify :: IState -> PTerm -> PTerm
@@ -868,7 +855,7 @@ pi syn =
868855 sc <- expr syn
869856 return (bindList (PPi binder) xt sc)) <|> (do
870857 (do try (lchar '{' *> reserved "auto")
871− when (st == Static) $ fail "auto type constraints can not be lazy or static"
858+ when (st == Static) $ fail "auto type constraints can not be static"
872859 xt <- typeDeclList syn
873860 lchar '}'
874861 symbol "->"
@@ -876,7 +863,7 @@ pi syn =
876863 return (bindList (PPi
877864 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)) <|> (do
878865 try (lchar '{' *> reserved "default")
879− when (st == Static) $ fail "default tactic constraints can not be lazy or static"
866+ when (st == Static) $ fail "default tactic constraints can not be static"
880867 script <- simpleExpr syn
881868 xt <- typeDeclList syn
882869 lchar '}'
src/Idris/Parser.hs+2
@@ -425,6 +425,8 @@ fnOpts opts
425425 fnOpts (CExport c : opts)
426426 <|> do try (lchar '%' *> reserved "no_implicit");
427427 fnOpts (NoImplicit : opts)
428+ <|> do try (lchar '%' *> reserved "inline");
429+ fnOpts (Inlinable : opts)
428430 <|> do try (lchar '%' *> reserved "assert_total");
429431 fnOpts (AssertTotal : opts)
430432 <|> do try (lchar '%' *> reserved "error_handler");
src/Idris/Prover.hs+1−1
@@ -86,7 +86,7 @@ prove opt ctxt lit n ty
8686 Error e -> ierror (CantUnify False ty pty e [] 0)
8787 ptm' <- applyOpts ptm
8888 ei <- getErasureInfo `fmap` getIState
89− updateContext (addCasedef n ei (CaseInfo True False) False (STerm Erased) True False
89+ updateContext (addCasedef n ei (CaseInfo True True False) False (STerm Erased) True False
9090 [] [] -- argtys, inaccArgs
9191 [Right (P Ref n ty, ptm)]
9292 [([], P Ref n ty, ptm)]
test/ffi001/run+1−1
@@ -1,3 +1,3 @@
11#!/usr/bin/env bash
22idris --quiet --nocolour test022.idr --exec main
3−rm -f test021 test021a *.ibc
3+rm -f *.ibc
test/ffi001/test022.idr+1−1
@@ -3,7 +3,7 @@ module Main
33%dynamic "dummy", "libm", "msvcrt"
44
55x : Float
6−x = unsafePerformIO (mkForeign (FFun "sin" [FFloat] FFloat) 1.6)
6+x = unsafePerformIO (foreign FFI_C "sin" (Float -> IO Float) 1.6)
77
88main : IO ()
99main = putStrLn (show x)
test/reg051/expected → test/reg051-disabled/expectedrenamed

The content is the same.

test/reg051/reg051.idr → test/reg051-disabled/reg051.idrrenamed

The content is the same.

test/reg051/run → test/reg051-disabled/runrenamed

The content is the same.