d5377be · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

New language-dependent FFI

d5377beEdwin Brady12 years ago

idris.cabal+3−3

compare with master

unifiedsplit

@@ -265,9 +265,9 @@ Extra-source-files:

265 test/reg050/run

266 test/reg050/*.idr

267 test/reg050/expected

268− test/reg051/run

268+ test/reg051-disabled/run

269− test/reg051/*.idr

269+ test/reg051-disabled/*.idr

270− test/reg051/expected

270+ test/reg051-disabled/expected

271 test/reg052/run

272 test/reg052/*.idr

273 test/reg052/expected

libs/base/Debug/Error.idr+1−1

@@ -12,7 +12,7 @@ error : {default tactics {sourceLocation} loc : SourceLocation} ->

12 (message : String) ->

13 a

14error {loc = FileLoc filename (line, col) _} message =

15− believe_me . unsafePerformIO $

15+ believe_me . unsafePerformIO $

16 do let place = filename ++ " line " ++ show line ++ " column " ++ show col

17 let message' = place ++ ": " ++ message

18 putStrLn message'

libs/base/Network/Socket.idr+42−35

@@ -124,18 +124,18 @@ record UDPAddrInfo : Type where

124||| Frees a given pointer

125public

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

128

129public

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

132

133||| Allocates an amount of memory given by the ByteLength parameter.

134|||

135||| Used to allocate a mutable pointer to be given to the Recv functions.

136public

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

139

140||| The metadata about a socket

141record Socket : Type where

@@ -147,13 +147,13 @@ record Socket : Type where

147

148||| Get the C error number

149getErrno : IO Int

150−getErrno = mkForeign (FFun "idrnet_errno" [] FInt)

150+getErrno = foreign FFI_C "idrnet_errno" (IO Int)

151

152||| Creates a UNIX socket with the given family, socket type and protocol

153||| number. Returns either a socket or an error.

154socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)

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

157 if socket_res == -1 then -- error

158 map Left getErrno

159 else

@@ -161,7 +161,7 @@ socket sf st pn = do

161

162||| Close a socket

163close : Socket -> IO ()

164−close sock = mkForeign (FFun "close" [FInt] FUnit) (descriptor sock)

164+close sock = foreign FFI_C "close" (Int -> IO ()) (descriptor sock)

165

166private

167saString : (Maybe SocketAddress) -> String

@@ -172,8 +172,10 @@ saString Nothing = ""

172||| Returns 0 on success, an error code otherwise.

173bind : Socket -> (Maybe SocketAddress) -> Port -> IO Int

174bind sock addr port = do

175− bind_res <- (mkForeign (FFun "idrnet_bind" [FInt, FInt, FInt, FString, FInt] FInt)

175+ bind_res <- foreign FFI_C "idrnet_bind"

176+ (Int -> Int -> Int -> String -> Int -> IO Int)

177+ (descriptor sock) (toCode $ family sock)

176− (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (saString addr) port)

178+ (toCode $ socketType sock) (saString addr) port

177 if bind_res == (-1) then -- error

179 if bind_res == (-1) then -- error

178 getErrno

180 getErrno

179 else return 0 -- Success

181 else return 0 -- Success

@@ -182,8 +184,9 @@ bind sock addr port = do

182||| Returns 0 on success, and an error number on error.

184||| Returns 0 on success, and an error number on error.

183connect : Socket -> SocketAddress -> Port -> IO Int

185connect : Socket -> SocketAddress -> Port -> IO Int

184connect sock addr port = do

186connect sock addr port = do

185− conn_res <- (mkForeign (FFun "idrnet_connect" [FInt, FInt, FInt, FString, FInt] FInt)

187+ conn_res <- foreign FFI_C "idrnet_connect"

188+ (Int -> Int -> Int -> String -> Int -> IO Int)

186− (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port)

189+ (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port

187 if conn_res == (-1) then

190 if conn_res == (-1) then

188 getErrno

191 getErrno

189 else return 0

192 else return 0

@@ -191,7 +194,8 @@ connect sock addr port = do

191||| Listens on a bound socket.

194||| Listens on a bound socket.

192listen : Socket -> IO Int

195listen : Socket -> IO Int

193listen sock = do

196listen sock = do

197+ listen_res <- foreign FFI_C "listen" (Int -> Int -> IO Int)

194− listen_res <- mkForeign (FFun "listen" [FInt, FInt] FInt) (descriptor sock) BACKLOG

198+ (descriptor sock) BACKLOG

195 if listen_res == (-1) then

199 if listen_res == (-1) then

196 getErrno

200 getErrno

197 else return 0

201 else return 0

@@ -212,12 +216,12 @@ parseIPv4 str = case splitted of

212||| Retrieves a socket address from a sockaddr pointer

216||| Retrieves a socket address from a sockaddr pointer

213getSockAddr : SockaddrPtr -> IO SocketAddress

217getSockAddr : SockaddrPtr -> IO SocketAddress

214getSockAddr (SAPtr ptr) = do

218getSockAddr (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

216 -- putStrLn $ "Addr family int: " ++ (show addr_family_int)

220 -- putStrLn $ "Addr family int: " ++ (show addr_family_int)

217 -- ASSUMPTION: Foreign call returns a valid int

221 -- ASSUMPTION: Foreign call returns a valid int

218 assert_total (case getSocketFamily addr_family_int of

222 assert_total (case getSocketFamily addr_family_int of

219 Just AF_INET => do

223 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

221 return $ parseIPv4 ipv4_addr

225 return $ parseIPv4 ipv4_addr

222 Just AF_INET6 => return IPv6Addr

226 Just AF_INET6 => return IPv6Addr

223 Just AF_UNSPEC => return InvalidAddress)

227 Just AF_UNSPEC => return InvalidAddress)

@@ -226,8 +230,8 @@ accept : Socket -> IO (Either SocketError (Socket, SocketAddress))

226accept sock = do

230accept sock = do

227 -- We need a pointer to a sockaddr structure. This is then passed into

231 -- We need a pointer to a sockaddr structure. This is then passed into

228 -- idrnet_accept and populated. We can then query it for the SocketAddr and free it.

232 -- idrnet_accept and populated. We can then query it for the SocketAddr and free it.

229− sockaddr_ptr <- mkForeign (FFun "idrnet_create_sockaddr" [] FPtr)

233+ sockaddr_ptr <- foreign FFI_C "idrnet_create_sockaddr" (IO Ptr)

230− accept_res <- mkForeign (FFun "idrnet_accept" [FInt, FPtr] FInt) (descriptor sock) sockaddr_ptr

234+ accept_res <- foreign FFI_C "idrnet_accept" (Int -> Ptr -> IO Int) (descriptor sock) sockaddr_ptr

231 if accept_res == (-1) then

235 if accept_res == (-1) then

232 map Left getErrno

236 map Left getErrno

233 else do

237 else do

@@ -238,7 +242,7 @@ accept sock = do

238

242

239send : Socket -> String -> IO (Either SocketError ByteLength)

243send : Socket -> String -> IO (Either SocketError ByteLength)

240send sock dat = do

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

242 if send_res == (-1) then

246 if send_res == (-1) then

243 map Left getErrno

247 map Left getErrno

244 else

248 else

@@ -246,17 +250,17 @@ send sock dat = do

246

250

247

251

248freeRecvStruct : RecvStructPtr -> IO ()

252freeRecvStruct : 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

250

254

251freeRecvfromStruct : RecvfromStructPtr -> IO ()

255freeRecvfromStruct : 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

253

257

254recv : Socket -> Int -> IO (Either SocketError (String, ByteLength))

258recv : Socket -> Int -> IO (Either SocketError (String, ByteLength))

255recv sock len = do

259recv sock len = do

256 -- Firstly make the request, get some kind of recv structure which

260 -- Firstly make the request, get some kind of recv structure which

257 -- contains the result of the recv and possibly the retrieved payload

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

262+ recv_struct_ptr <- foreign FFI_C "idrnet_recv" (Int -> Int -> IO Ptr) (descriptor sock) len

259− recv_res <- mkForeign (FFun "idrnet_get_recv_res" [FPtr] FInt) recv_struct_ptr

263+ recv_res <- foreign FFI_C "idrnet_get_recv_res" (Ptr -> IO Int) recv_struct_ptr

260 if recv_res == (-1) then do

264 if recv_res == (-1) then do

261 errno <- getErrno

265 errno <- getErrno

262 freeRecvStruct (RSPtr recv_struct_ptr)

266 freeRecvStruct (RSPtr recv_struct_ptr)

@@ -266,7 +270,7 @@ recv sock len = do

266 freeRecvStruct (RSPtr recv_struct_ptr)

270 freeRecvStruct (RSPtr recv_struct_ptr)

267 return $ Left 0

271 return $ Left 0

268 else do

272 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

270 freeRecvStruct (RSPtr recv_struct_ptr)

274 freeRecvStruct (RSPtr recv_struct_ptr)

271 return $ Right (payload, recv_res)

275 return $ Right (payload, recv_res)

272

276

@@ -274,7 +278,7 @@ recv sock len = do

274||| Sends the data in a given memory location

278||| Sends the data in a given memory location

275sendBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)

279sendBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)

276sendBuf sock (BPtr ptr) len = do

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

278 if send_res == (-1) then

282 if send_res == (-1) then

279 map Left getErrno

283 map Left getErrno

280 else

284 else

@@ -282,7 +286,7 @@ sendBuf sock (BPtr ptr) len = do

282

286

283recvBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)

287recvBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)

284recvBuf sock (BPtr ptr) len = do

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

286 if (recv_res == (-1)) then

290 if (recv_res == (-1)) then

287 map Left getErrno

291 map Left getErrno

288 else

292 else

@@ -290,8 +294,9 @@ recvBuf sock (BPtr ptr) len = do

290

294

291sendTo : Socket -> SocketAddress -> Port -> String -> IO (Either SocketError ByteLength)

295sendTo : Socket -> SocketAddress -> Port -> String -> IO (Either SocketError ByteLength)

292sendTo sock addr p dat = do

296sendTo sock addr p dat = do

293− sendto_res <- mkForeign (FFun "idrnet_sendto" [FInt, FString, FString, FInt, FInt] FInt)

297+ sendto_res <- foreign FFI_C "idrnet_sendto"

298+ (Int -> String -> String -> Int -> Int -> IO Int)

294− (descriptor sock) dat (show addr) p (toCode $ family sock)

299+ (descriptor sock) dat (show addr) p (toCode $ family sock)

295 if sendto_res == (-1) then

300 if sendto_res == (-1) then

296 map Left getErrno

301 map Left getErrno

297 else

302 else

@@ -300,8 +305,9 @@ sendTo sock addr p dat = do

300

305

301sendToBuf : Socket -> SocketAddress -> Port -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)

306sendToBuf : Socket -> SocketAddress -> Port -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)

302sendToBuf sock addr p (BPtr dat) len = do

307sendToBuf sock addr p (BPtr dat) len = do

303− sendto_res <- mkForeign (FFun "idrnet_sendto_buf" [FInt, FPtr, FInt, FString, FInt, FInt] FInt)

308+ sendto_res <- foreign FFI_C "idrnet_sendto_buf"

309+ (Int -> Ptr -> Int -> String -> Int -> Int -> IO Int)

304− (descriptor sock) dat len (show addr) p (toCode $ family sock)

310+ (descriptor sock) dat len (show addr) p (toCode $ family sock)

305 if sendto_res == (-1) then

311 if sendto_res == (-1) then

306 map Left getErrno

312 map Left getErrno

307 else

313 else

@@ -309,29 +315,30 @@ sendToBuf sock addr p (BPtr dat) len = do

309

315

310

316

311foreignGetRecvfromPayload : RecvfromStructPtr -> IO String

317foreignGetRecvfromPayload : 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

313

320

314foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress

321foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress

315foreignGetRecvfromAddr (RFPtr p) = do

322foreignGetRecvfromAddr (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

317 getSockAddr sockaddr_ptr

324 getSockAddr sockaddr_ptr

318

325

319

326

320foreignGetRecvfromPort : RecvfromStructPtr -> IO Port

327foreignGetRecvfromPort : RecvfromStructPtr -> IO Port

321foreignGetRecvfromPort (RFPtr p) = do

328foreignGetRecvfromPort (RFPtr p) = do

322− sockaddr_ptr <- mkForeign (FFun "idrnet_get_recvfrom_sockaddr" [FPtr] FPtr) p

329+ sockaddr_ptr <- foreign FFI_C "idrnet_get_recvfrom_sockaddr" (Ptr -> IO Ptr) p

323− port <- mkForeign (FFun "idrnet_sockaddr_ipv4_port" [FPtr] FInt) sockaddr_ptr

330+ port <- foreign FFI_C "idrnet_sockaddr_ipv4_port" (Ptr -> IO Int) sockaddr_ptr

324 return port

331 return port

325

332

326recvFrom : Socket -> ByteLength -> IO (Either SocketError (UDPAddrInfo, String, ByteLength))

333recvFrom : Socket -> ByteLength -> IO (Either SocketError (UDPAddrInfo, String, ByteLength))

327recvFrom sock bl = do

334recvFrom 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)

329 (descriptor sock) bl

336 (descriptor sock) bl

330 let recv_ptr' = RFPtr recv_ptr

337 let recv_ptr' = RFPtr recv_ptr

331 if !(nullPtr recv_ptr) then

338 if !(nullPtr recv_ptr) then

332 map Left getErrno

339 map Left getErrno

333 else do

340 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

335 if result == -1 then do

342 if result == -1 then do

336 freeRecvfromStruct recv_ptr'

343 freeRecvfromStruct recv_ptr'

337 map Left getErrno

344 map Left getErrno

@@ -345,12 +352,12 @@ recvFrom sock bl = do

345

352

346recvFromBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError (UDPAddrInfo, ByteLength))

353recvFromBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError (UDPAddrInfo, ByteLength))

347recvFromBuf sock (BPtr ptr) bl = do

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

349 let recv_ptr' = RFPtr recv_ptr

356 let recv_ptr' = RFPtr recv_ptr

350 if !(nullPtr recv_ptr) then

357 if !(nullPtr recv_ptr) then

351 map Left getErrno

358 map Left getErrno

352 else do

359 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

354 if result == -1 then do

361 if result == -1 then do

355 freeRecvfromStruct recv_ptr'

362 freeRecvfromStruct recv_ptr'

356 map Left getErrno

363 map Left getErrno

libs/base/System.idr+10−10

@@ -10,10 +10,10 @@ getArgs = do n <- numArgs

10 ga' [] 0 n

11 where

12 numArgs : IO Int

13− numArgs = mkForeign (FFun "idris_numArgs" [] FInt)

13+ numArgs = foreign FFI_C "idris_numArgs" (IO Int)

15 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

18 ga' : List String -> Int -> Int -> IO (List String)

19 ga' acc i n = if (i == n) then (return $ reverse acc) else

@@ -31,27 +31,27 @@ getEnv key = do

31 else pure (Just str_ptr)

32 where

33 getEnv' : IO String

34− getEnv' = mkForeign (FFun "getenv" [FString] FString) key

34+ getEnv' = foreign FFI_C "getenv" (String -> IO String) key

36||| Sets an environment variable with a given value.

37||| Returns true if the operation was successful.

38setEnv : String -> String -> IO Bool

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

41 return (ok == 0)

43||| Unsets an environment variable.

44||| Returns true if the variable was able to be unset.

45unsetEnv : String -> IO Bool

46unsetEnv key = do

47− ok <- mkForeign (FFun "unsetenv" [FString] FInt) key

47+ ok <- foreign FFI_C "unsetenv" (String -> IO Int) key

48 return (ok == 0)

50getEnvironment : IO (List (String, String))

51getEnvironment = getAllPairs 0 []

52 where

53 getEnvPair : Int -> IO String

54− getEnvPair i = mkForeign (FFun "getEnvPair" [FInt] FString) i

54+ getEnvPair i = foreign FFI_C "getEnvPair" (Int -> IO String) i

56 splitEq : String -> (String, String)

57 splitEq str =

@@ -70,15 +70,15 @@ getEnvironment = getAllPairs 0 []

71||| Quit with a particular exit code

72exit : Int -> IO ()

73−exit code = mkForeign (FFun "exit" [FInt] FUnit) code

73+exit code = foreign FFI_C "exit" (Int -> IO ()) code

75||| Get the Unix time

76time : IO Int

77−time = mkForeign (FFun "idris_time" [] FInt)

77+time = foreign FFI_C "idris_time" (IO Int)

79usleep : Int -> IO ()

80−usleep i = mkForeign (FFun "usleep" [FInt] FUnit) i

80+usleep i = foreign FFI_C "usleep" (Int -> IO ()) i

82system : String -> IO Int

83−system cmd = mkForeign (FFun "system" [FString] FInt) cmd

83+system cmd = foreign FFI_C "system" (String -> IO Int) cmd

libs/base/System/Concurrency/Raw.idr+7−6

@@ -9,16 +9,17 @@ import System

9||| Send a message of any type to the thread with the given thread id

10sendToThread : (thread_id : Ptr) -> a -> IO ()

11sendToThread {a} dest val

12− = mkForeign (FFun "idris_sendMessage"

12+ = foreign FFI_C "idris_sendMessage" (Ptr -> Ptr -> Raw a -> IO ())

13− [FPtr, FPtr, FAny a] FUnit) prim__vm dest val

13+ prim__vm dest (MkRaw val)

15checkMsgs : IO Bool

16−checkMsgs = do msgs <- mkForeign (FFun "idris_checkMessages"

16+checkMsgs = do msgs <- foreign FFI_C "idris_checkMessages" (Ptr -> IO Int)

17− [FPtr] FInt) prim__vm

17+ prim__vm

18 return (intToBool msgs)

20||| Check inbox for messages. If there are none, blocks until a message

21||| arrives.

22getMsg : IO a

23−getMsg {a} = mkForeign (FFun "idris_recvMessage"

23+getMsg {a} = do MkRaw x <- foreign FFI_C "idris_recvMessage"

24− [FPtr] (FAny a)) prim__vm

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

42private

43do_malloc : Nat -> IOExcept String Ptr

44do_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)

46 fail <- ioe_lift $ nullPtr ptr

47 if fail then ioe_fail "Cannot allocate memory"

48 else return ptr

@@ -51,24 +51,24 @@ do_malloc size with (fromInteger (cast size) == size)

51private

52do_memset : Ptr -> Nat -> Bits8 -> Nat -> IO ()

53do_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 ())

55 ptr (fromInteger $ cast offset) c (fromInteger $ cast size)

57private

58do_free : Ptr -> IO ()

59−do_free ptr = mkForeign (FFun "free" [FPtr] FUnit) ptr

59+do_free ptr = foreign FFI_C "free" (Ptr -> IO ()) ptr

61private

62do_memmove : Ptr -> Ptr -> Nat -> Nat -> Nat -> IO ()

63do_memmove dest src dest_offset src_offset size

64− = mkForeign (FFun "idris_memmove" [FPtr, FPtr, FInt, FInt, FInt] FUnit)

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)

65+ dest src (fromInteger $ cast dest_offset) (fromInteger $ cast src_offset) (fromInteger $ cast size)

67private

68do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect size Bits8)

69do_peek _ _ Z = return (Vect.Nil)

70do_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)

72 bs <- do_peek ptr (S offset) n

73 Monad.return (Vect.(::) b bs)

@@ -76,7 +76,7 @@ private

76do_poke : Ptr -> Nat -> Vect size Bits8 -> IO ()

77do_poke _ _ [] = return ()

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

80 do_poke ptr (S offset) bs

82instance Handler RawMemory (IOExcept String) where

libs/prelude/IO.idr+83−107

@@ -16,11 +16,49 @@ abstract data World = TheWorld

16abstract WorldRes : Type -> Type

17WorldRes x = x

19−-- abstract data WorldRes a = MkWR a World

19+record FFI : Type where

20+ MkFFI : (ffi_types : Type -> Type) -> (ffi_fn : Type) -> FFI

21abstract

22abstract

22−data IO : Type -> Type where

23+data IO' : (lang : FFI) -> Type -> Type where

23− MkIO : (World -> PrimIO (WorldRes a)) -> IO a

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

25abstract

63abstract

26prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b

64prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b

@@ -33,120 +71,63 @@ abstract

33prim_io_return : a -> PrimIO a

71prim_io_return : a -> PrimIO a

34prim_io_return x = prim__IO x

72prim_io_return x = prim__IO x

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−

128abstract

74abstract

129−io_bind : IO a -> (a -> IO b) -> IO b

75+io_bind : IO' l a -> (a -> IO' l b) -> IO' l b

130io_bind (MkIO fn) k

76io_bind (MkIO fn) k

131 = MkIO (\w => prim_io_bind (fn w)

77 = MkIO (\w => prim_io_bind (fn w)

132 (\ b => case k b of

78 (\ b => case k b of

133 MkIO fkb => fkb w))

79 MkIO fkb => fkb w))

134

135abstract

81abstract

136−io_return : a -> IO a

82+io_return : a -> IO' l a

137io_return x = MkIO (\w => prim_io_return x)

83io_return x = MkIO (\w => prim_io_return x)

138

139−liftPrimIO : (World -> PrimIO a) -> IO a

85+liftPrimIO : (World -> PrimIO a) -> IO' l a

140liftPrimIO = MkIO

86liftPrimIO = MkIO

141

142−run__IO : IO () -> PrimIO ()

88+run__IO : IO' l () -> PrimIO ()

143run__IO (MkIO f) = f TheWorld

89run__IO (MkIO f) = f TheWorld

144

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+

145run__provider : IO a -> PrimIO a

128run__provider : IO a -> PrimIO a

146run__provider (MkIO f) = f TheWorld

129run__provider (MkIO f) = f TheWorld

147

130

148−-- io_bind v (\v' => io_return v')

149−

150prim_fork : PrimIO () -> PrimIO Ptr

131prim_fork : PrimIO () -> PrimIO Ptr

151prim_fork x = prim_io_return prim__vm -- compiled specially

132prim_fork x = prim_io_return prim__vm -- compiled specially

152

133

@@ -160,11 +141,6 @@ partial

160prim_fread : Ptr -> IO String

141prim_fread : Ptr -> IO String

161prim_fread h = MkIO (\w => prim_io_return (prim__readString h))

142prim_fread h = MkIO (\w => prim_io_return (prim__readString h))

162

143

163−unsafePerformIO : IO a -> a

164−unsafePerformIO (MkIO f) = unsafePerformPrimIO

165− (prim_io_bind (f TheWorld) (\ b => prim_io_return b))

166−

167−

168forceGC : IO ()

144forceGC : IO ()

169−forceGC = mkForeign (FFun "idris_forceGC" [FPtr] FUnit) prim__vm

145+forceGC = foreign FFI_C "idris_forceGC" (Ptr -> IO ()) prim__vm

170

146

libs/prelude/Prelude.idr+21−21

@@ -233,7 +233,7 @@ instance Show a => Show (Maybe a) where

233instance Functor PrimIO where

234 map f io = prim_io_bind io (prim_io_return . f)

235

236−instance Functor IO where

236+instance Functor (IO' ffi) where

237 map f io = io_bind io (\b => io_return (f b))

238

239instance Functor Maybe where

@@ -251,7 +251,7 @@ instance Applicative PrimIO where

251

252 am <$> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))

253

254−instance Applicative IO where

254+instance Applicative (IO' ffi) where

255 pure x = io_return x

256 f <$> a = io_bind f (\f' =>

257 io_bind a (\a' =>

@@ -293,7 +293,7 @@ instance Alternative List where

293instance Monad PrimIO where

294 b >>= k = prim_io_bind b k

295

296−instance Monad IO where

296+instance Monad (IO' ffi) where

297 b >>= k = io_bind b k

298

299instance Monad Maybe where

@@ -436,7 +436,7 @@ uniformB64x2 x = prim__mkB64x2 x x

436||| Output a string to stdout without a trailing newline

437partial

438putStr : String -> IO ()

439−putStr x = mkForeign (FFun "putStr" [FString] FUnit) x

439+putStr x = foreign FFI_C "putStr" (String -> IO ()) x

440

441||| Output a string to stdout with a trailing newline

442partial

@@ -456,12 +456,12 @@ getLine = prim_fread prim__stdin

456||| Write a single character to stdout

457partial

458putChar : Char -> IO ()

459−putChar c = mkForeign (FFun "putchar" [FInt] FUnit) (cast c)

459+putChar c = foreign FFI_C "putchar" (Int -> IO ()) (cast c)

460

461||| Read a single character from stdin

462partial

463getChar : IO Char

464−getChar = map cast $ mkForeign (FFun "getchar" [] FInt)

464+getChar = map cast $ foreign FFI_C "getchar" (IO Int)

465

466---- some basic file handling

467

@@ -484,8 +484,8 @@ stderr = FHandle prim__stderr

484||| Call the RTS's file opening function

485do_fopen : String -> String -> IO Ptr

486do_fopen f m

487− = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m

487+ = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m

488−

488+

489||| Open a file

490||| @ f the filename

491||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)

@@ -508,7 +508,7 @@ openFile f m = fopen f (modeStr m) where

508

509partial

510do_fclose : Ptr -> IO ()

511−do_fclose h = mkForeign (FFun "fileClose" [FPtr] FUnit) h

511+do_fclose h = foreign FFI_C "fileClose" (Ptr -> IO ()) h

512

513partial

514closeFile : File -> IO ()

@@ -519,19 +519,19 @@ do_fread : Ptr -> IO String

519do_fread h = prim_fread h

520

521fgetc : 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))

523

524fgetc' : File -> IO (Maybe Char)

525fgetc' (FHandle h)

526− = do x <- mkForeign (FFun "fgetc" [FPtr] FInt) h

526+ = do x <- foreign FFI_C "fgetc" (Ptr -> IO Int) h

527 if (x < 0) then return Nothing

528 else return (Just (cast x))

529

530fflush : File -> IO ()

531−fflush (FHandle h) = mkForeign (FFun "fflush" [FPtr] FUnit) h

531+fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h

532

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

535

536popen : String -> Mode -> IO File

537popen f m = do ptr <- do_popen f (modeStr m)

@@ -542,7 +542,7 @@ popen f m = do ptr <- do_popen f (modeStr m)

542 modeStr ReadWrite = "r+"

543

544pclose : File -> IO ()

545−pclose (FHandle h) = mkForeign (FFun "pclose" [FPtr] FUnit) h

545+pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h

546

547-- mkForeign (FFun "idris_readStr" [FPtr, FPtr] (FAny String))

548-- prim__vm h

@@ -554,7 +554,7 @@ fread (FHandle h) = do_fread h

554partial

555do_fwrite : Ptr -> String -> IO ()

556do_fwrite h s

557− = mkForeign (FFun "fputStr" [FPtr, FString] FUnit) h s

557+ = foreign FFI_C "fputStr" (Ptr -> String -> IO ()) h s

558

559partial

560fwrite : File -> String -> IO ()

@@ -562,7 +562,7 @@ fwrite (FHandle h) s = do_fwrite h s

562

563partial

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

566

567||| Check if a file handle has reached the end

568feof : File -> IO Bool

@@ -571,31 +571,31 @@ feof (FHandle h) = do eof <- do_feof h

571

572partial

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

575

576ferror : File -> IO Bool

577ferror (FHandle h) = do err <- do_ferror h

578 return (not (err == 0))

579

580fpoll : 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

582 return (p > 0)

583

584||| Check if a foreign pointer is null

585partial

586nullPtr : 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

588 return (ok /= 0)

589

590||| Check if a supposed string was actually a null pointer

591partial

592nullStr : 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

594 return (ok /= 0)

595

596||| Pointer equality

597eqPtr : 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

599 return (eq /= 0)

600

601||| Check whether a file handle is actually a null pointer

src/IRTS/Bytecode.hs+5−6

@@ -5,6 +5,7 @@ module IRTS.Bytecode where

6import IRTS.Lang

7import IRTS.Simplified

8+import IRTS.Defunctionalise

8import Idris.Core.TT

9import Idris.Core.TT

9import Data.Maybe

10import Data.Maybe

@@ -69,10 +70,8 @@ data BC =

69 -- same, perhaps exists just for TCO

70 -- same, perhaps exists just for TCO

70 | TAILCALL Name

71 | TAILCALL Name

72− -- set reg to (apply string args), FLang argument is the language to

73+ -- set reg to (apply string args),

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

74+ | FOREIGNCALL Reg FDesc DExp [(FDesc, Reg)]

77 -- move this number of elements from TOP to BASE

76 -- move this number of elements from TOP to BASE

78 | SLIDE Int

77 | SLIDE Int

@@ -132,8 +131,8 @@ bc reg (SApp False f vs) r =

132bc reg (SApp True f vs) r

131bc reg (SApp True f vs) r

133 = RESERVE (length vs) : moveReg 0 vs

132 = RESERVE (length vs) : moveReg 0 vs

134 ++ [SLIDE (length vs), TOPBASE (length vs), TAILCALL f]

133 ++ [SLIDE (length vs), TOPBASE (length vs), TAILCALL f]

135−bc reg (SForeign l t fname args) r

134+bc reg (SForeign t fname args) r

136− = FOREIGNCALL reg l t fname (map farg args) : clean r

135+ = FOREIGNCALL reg t fname (map farg args) : clean r

137 where farg (ty, Loc i) = (ty, L i)

136 where farg (ty, Loc i) = (ty, L i)

138bc reg (SLet (Loc i) e sc) r = bc (L i) e False ++ bc reg sc r

137bc reg (SLet (Loc i) e sc) r = bc (L i) e False ++ bc reg sc r

139bc reg (SUpdate (Loc i) sc) r = bc reg sc False ++ [ASSIGN (L i) reg]

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

4import IRTS.Bytecode

5import IRTS.Lang

6import IRTS.Simplified

7+import IRTS.Defunctionalise

7import IRTS.System

8import IRTS.System

8import IRTS.CodegenCommon

9import IRTS.CodegenCommon

9import Idris.Core.TT

10import Idris.Core.TT

@@ -20,6 +21,8 @@ import System.Directory

20import System.FilePath ((</>), (<.>))

21import System.FilePath ((</>), (<.>))

21import Control.Monad

22import Control.Monad

24+import Debug.Trace

25+

23codegenC :: CodeGenerator

26codegenC :: CodeGenerator

24codegenC ci = codegenC' (simpleDecls ci)

27codegenC ci = codegenC' (simpleDecls ci)

25 (outputFile ci)

28 (outputFile ci)

@@ -274,16 +277,41 @@ bcc i (TOPBASE n) = indent i ++ "TOPBASE(" ++ show n ++ ");\n"

274bcc i (BASETOP n) = indent i ++ "BASETOP(" ++ show n ++ ");\n"

277bcc i (BASETOP n) = indent i ++ "BASETOP(" ++ show n ++ ");\n"

275bcc i STOREOLD = indent i ++ "STOREOLD;\n"

278bcc i STOREOLD = indent i ++ "STOREOLD;\n"

276bcc i (OP l fn args) = indent i ++ doOp (creg l ++ " = ") fn args ++ ";\n"

279bcc 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)

278 = indent i ++

281 = indent i ++

279− c_irts rty (creg l ++ " = ")

282+ c_irts (toFType rty) (creg l ++ " = ")

280 (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"

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

282bcc i (NULL r) = indent i ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed

285bcc i (NULL r) = indent i ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed

283bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); fprintf(stderr, \"\\n\"); exit(-1); exit(-1);"

286bcc 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"

287+-- bcc i c = error (show c) -- indent i ++ "// not done yet\n"

285−

288+

286−

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

287

315

288c_irts (FArith (ATInt ITNative)) l x = l ++ "MKINT((i_int)(" ++ x ++ "))"

316c_irts (FArith (ATInt ITNative)) l x = l ++ "MKINT((i_int)(" ++ x ++ "))"

289c_irts (FArith (ATInt ITChar)) l x = c_irts (FArith (ATInt ITNative)) l x

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

1332 | NULL r <- bc = jsNULL info r

1333 | CALL n <- bc = jsCALL info n

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

1336 | TOPBASE n <- bc = jsTOPBASE info n

1337 | BASETOP n <- bc = jsBASETOP info n

1338 | STOREOLD <- bc = jsSTOREOLD info

src/IRTS/Compiler.hs+26−4

@@ -218,7 +218,7 @@ irTerm :: Vars -> [Name] -> Term -> Idris LExp

218irTerm vs env tm@(App f a) = case unApply tm of

219 (P _ (UN m) _, args)

220 | m == txt "mkForeignPrim"

221− -> doForeign vs env args

221+ -> doForeign vs env (reverse (drop 4 args)) -- drop implicits

222

223 (P _ (UN u) _, [_, arg])

224 | u == txt "unsafePerformPrimIO"

@@ -434,9 +434,30 @@ irTerm vs env (TType _) = return $ LNothing

434irTerm vs env Erased = return $ LNothing

435irTerm vs env Impossible = return $ LNothing

436

437−doForeign :: Vars -> [Name] -> [TT Name] -> Idris LExp

437+doForeign :: Vars -> [Name] -> [Term] -> Idris LExp

438−doForeign vs env (_ : fgn : args)

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

439− | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn

460+ - | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn

440 = case getFTypes fgnArgTys of

461 = case getFTypes fgnArgTys of

441 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)

462 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)

442 Just tys -> do

463 Just tys -> do

@@ -502,6 +523,7 @@ doForeign vs env (_ : fgn : args)

502 mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))

523 mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))

503 mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))

524 mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))

504 mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))

525 mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))

526+-}

505

527

506irTree :: [Name] -> SC -> Idris LExp

528irTree :: [Name] -> SC -> Idris LExp

507irTree args tree = do

529irTree args tree = do

src/IRTS/Defunctionalise.hs+10−7

@@ -22,7 +22,7 @@ data DExp = DV LVar

22 | DCase CaseType DExp [DAlt]

23 | DChkCase DExp [DAlt] -- a case where the type is unknown (for EVAL/APPLY)

24 | DConst Const

25− | DForeign FLang FType String [(FType, DExp)]

25+ | DForeign FDesc DExp [(FDesc, DExp)]

26 | DOp PrimFn [DExp]

27 | DNothing -- erased value, can be compiled to anything since it'll never

28 -- be inspected

@@ -110,7 +110,10 @@ addApps defs (n, LFun _ _ args e)

110 alts' <- mapM (aaAlt env) alts

111 return $ DCase up e' alts'

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

114 aa env (LOp LFork args) = liftM (DOp LFork) (mapM (aa env) args)

117 aa env (LOp LFork args) = liftM (DOp LFork) (mapM (aa env) args)

115 aa env (LOp f args) = do args' <- mapM (aa env) args

118 aa env (LOp f args) = do args' <- mapM (aa env) args

116 return $ DOp f args'

119 return $ DOp f args'

@@ -173,7 +176,7 @@ addApps defs (n, LFun _ _ args e)

173 needsEval x (DLet n v e)

176 needsEval x (DLet n v e)

174 | x == n = needsEval x v

177 | x == n = needsEval x v

175 | otherwise = needsEval x v || needsEval x e

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

177 needsEval x (DOp op args) = or (map (needsEval x) args)

180 needsEval x (DOp op args) = or (map (needsEval x) args)

178 needsEval x (DProj (DV (Glob x')) _) = x == x'

181 needsEval x (DProj (DV (Glob x')) _) = x == x'

179 needsEval x _ = False

182 needsEval x _ = False

@@ -257,13 +260,13 @@ mkUnderCon n missing = sMN missing ("U_" ++ show n)

257instance Show DExp where

260instance Show DExp where

258 show e = show' [] e where

261 show e = show' [] e where

259 show' env (DV (Loc i)) = "var " ++ env!!i

262 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

261 show' env (DApp _ e args) = show e ++ "(" ++

264 show' env (DApp _ e args) = show e ++ "(" ++

262 showSep ", " (map (show' env) args) ++")"

265 showSep ", " (map (show' env) args) ++")"

263 show' env (DLet n v e) = "let " ++ show n ++ " = " ++ show' env v ++ " in " ++

266 show' env (DLet n v e) = "let " ++ show n ++ " = " ++ show' env v ++ " in " ++

264 show' (env ++ [show n]) e

267 show' (env ++ [show n]) e

265 show' env (DUpdate n e) = "!update " ++ show n ++ "(" ++ show' env e ++ ")"

268 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) ++ ")"

267 where atloc Nothing = ""

270 where atloc Nothing = ""

268 atloc (Just l) = "@" ++ show (LV l) ++ ":"

271 atloc (Just l) = "@" ++ show (LV l) ++ ":"

269 show' env (DProj t i) = show t ++ "!" ++ show i

272 show' env (DProj t i) = show t ++ "!" ++ show i

@@ -275,8 +278,8 @@ instance Show DExp where

275 show' env (DChkCase e alts) = "case' " ++ show' env e ++ " of {\n\t" ++

278 show' env (DChkCase e alts) = "case' " ++ show' env e ++ " of {\n\t" ++

276 showSep "\n\t| " (map (showAlt env) alts)

279 showSep "\n\t| " (map (showAlt env) alts)

277 show' env (DConst c) = show c

280 show' env (DConst c) = show c

278− show' env (DForeign lang ty n args)

281+ show' env (DForeign ty n args)

279− = "foreign " ++ n ++ "(" ++ showSep ", " (map (show' env) (map snd args)) ++ ")"

282+ = "foreign " ++ show' env n ++ "(" ++ showSep ", " (map (show' env) (map snd args)) ++ ")"

280 show' env (DOp f args) = show f ++ "(" ++ showSep ", " (map (show' env) args) ++ ")"

283 show' env (DOp f args) = show f ++ "(" ++ showSep ", " (map (show' env) args) ++ ")"

281 show' env (DError str) = "error " ++ show str

284 show' env (DError str) = "error " ++ show str

282 show' env DNothing = "____"

285 show' env DNothing = "____"

src/IRTS/DumpBC.hs+2−2

@@ -51,8 +51,8 @@ serializeBC n bc = indent n ++

51 maybe "" (\def' -> "\n" ++ serializeDefault (n + 1) def') def

52 CALL x -> "CALL " ++ show x

53 TAILCALL x -> "TAILCALL " ++ show x

54− FOREIGNCALL r _ ret name args ->

54+ FOREIGNCALL r ret name args ->

55− "FOREIGNCALL " ++ serializeReg r ++ " \"" ++ name ++ "\" " ++ show ret ++

55+ "FOREIGNCALL " ++ serializeReg r ++ " \"" ++ show name ++ "\" " ++ show ret ++

56 " [" ++ interMap args ", " (\(ty, r) -> serializeReg r ++ " : " ++ show ty) ++ "]"

57 SLIDE n -> "SLIDE " ++ show n

58 REBASE -> "REBASE"

src/IRTS/Lang.hs+17−12

@@ -29,12 +29,19 @@ data LExp = LV LVar

29 Int Name [LExp]

30 | LCase CaseType LExp [LAlt]

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

33 | LOp PrimFn [LExp]

35 | LOp PrimFn [LExp]

34 | LNothing

36 | LNothing

35 | LError String

37 | LError String

36 deriving Eq

38 deriving Eq

40+data FDesc = FCon Name

41+ | FUnknown

42+ | FApp Name [FDesc]

43+ deriving (Show, Eq)

44+

38-- Primitive operators. Backends are not *required* to implement all

45-- Primitive operators. Backends are not *required* to implement all

39-- of these, but should report an error if they are unable

46-- of these, but should report an error if they are unable

@@ -85,9 +92,6 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

85data FCallType = FStatic | FObject | FConstructor

92data FCallType = FStatic | FObject | FConstructor

86 deriving (Show, Eq)

93 deriving (Show, Eq)

88−data FLang = LANG_C | LANG_JAVA FCallType

89− deriving (Show, Eq)

90−

91data FType = FArith ArithTy

95data FType = FArith ArithTy

92 | FFunction

96 | FFunction

93 | FFunctionIO

97 | FFunctionIO

@@ -192,8 +196,9 @@ lift env (LCase up e alts) = do alts' <- mapM liftA alts

192 liftA (LDefaultCase e) = do e' <- lift env e

196 liftA (LDefaultCase e) = do e' <- lift env e

193 return (LDefaultCase e')

197 return (LDefaultCase e')

194lift env (LConst c) = return (LConst c)

198lift env (LConst c) = return (LConst c)

195−lift env (LForeign l t s args) = do args' <- mapM (liftF env) args

199+lift env (LForeign t s args) = do args' <- mapM (liftF env) args

200+ s' <- lift env s

196− return (LForeign l t s args')

201+ return (LForeign t s' args')

197 where

202 where

198 liftF env (t, e) = do e' <- lift env e

203 liftF env (t, e) = do e' <- lift env e

199 return (t, e')

204 return (t, e')

@@ -231,9 +236,9 @@ allocUnique defs (n, LFun opts fn args e)

231 = do avail <- get

236 = do avail <- get

232 v <- findVar [] avail (length es)

237 v <- findVar [] avail (length es)

233 LCon v i n <$> mapM findUp es

238 LCon v i n <$> mapM findUp es

234− findUp (LForeign l t s es)

239+ findUp (LForeign t s es)

235− = LForeign l t s <$> mapM (\ (t, e) -> do e' <- findUp e

240+ = LForeign t s <$> mapM (\ (t, e) -> do e' <- findUp e

236− return (t, e')) es

241+ return (t, e')) es

237 findUp (LOp o es) = LOp o <$> mapM findUp es

242 findUp (LOp o es) = LOp o <$> mapM findUp es

238 findUp (LCase Updatable e@(LV (Glob n)) as)

243 findUp (LCase Updatable e@(LV (Glob n)) as)

239 = LCase Updatable e <$> mapM (doUpAlt n) as

244 = LCase Updatable e <$> mapM (doUpAlt n) as

@@ -282,7 +287,7 @@ usedIn env (LCase up e alts) = usedIn env e ++ concatMap (usedInA env) alts

282 where usedInA env (LConCase i n ns e) = usedIn env e

287 where usedInA env (LConCase i n ns e) = usedIn env e

283 usedInA env (LConstCase c e) = usedIn env e

288 usedInA env (LConstCase c e) = usedIn env e

284 usedInA env (LDefaultCase e) = usedIn env e

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

286usedIn env (LOp f args) = concatMap (usedIn env) args

291usedIn env (LOp f args) = concatMap (usedIn env) args

287usedIn env _ = []

292usedIn env _ = []

288

293

@@ -329,9 +334,9 @@ instance Show LExp where

329

334

330 show' env ind (LConst c) = show c

335 show' env ind (LConst c) = show c

331

336

332− show' env ind (LForeign lang ty n args) = concat

337+ show' env ind (LForeign ty n args) = concat

333 [ "foreign{ "

338 [ "foreign{ "

334− , n ++ "("

339+ , show' env ind n ++ "("

335 , showSep ", " (map (\(ty,x) -> show' env ind x ++ " : " ++ show ty) args)

340 , showSep ", " (map (\(ty,x) -> show' env ind x ++ " : " ++ show ty) args)

336 , ") : "

341 , ") : "

337 , show ty

342 , show ty

src/IRTS/LangOpts.hs+3−3

@@ -64,9 +64,9 @@ doInline defs (LFun opts topn args exp)

64 inlineWith (n : done) (zip args es' ++ env) body

65 inlineWith done env (LApp t f es)

66 = LApp t <$> inlineWith done env f <*> mapM (inlineWith done env) es

67− inlineWith done env (LForeign l t s args)

67+ inlineWith done env (LForeign t s args)

68− = LForeign l t s <$> mapM (\(t, e) -> do e' <- inlineWith done env e

68+ = LForeign t s <$> mapM (\(t, e) -> do e' <- inlineWith done env e

69− return (t, e')) args

69+ return (t, e')) args

70 inlineWith done env t = return t

72 inlineWithAlt done env (LConCase i n es rhs)

src/IRTS/Simplified.hs+7−5

@@ -22,7 +22,9 @@ data SExp = SV LVar

22 | SChkCase LVar [SAlt]

23 | SProj LVar Int

24 | SConst Const

25+ -- Keep DExps for describing foreign things, because they get

26+ -- translated differently

25− | SForeign FLang FType String [(FType, LVar)]

27+ | SForeign FDesc DExp [(FDesc, LVar)]

26 | SOp PrimFn [LVar]

28 | SOp PrimFn [LVar]

27 | SNothing -- erased value, will never be inspected

29 | SNothing -- erased value, will never be inspected

28 | SError String

30 | SError String

@@ -54,10 +56,10 @@ simplify tl (DV (Glob x))

54 _ -> return $ SV (Glob x)

56 _ -> return $ SV (Glob x)

55simplify tl (DApp tc n args) = do args' <- mapM sVar args

57simplify tl (DApp tc n args) = do args' <- mapM sVar args

56 mkapp (SApp (tl || tc) n) args'

58 mkapp (SApp (tl || tc) n) args'

57−simplify tl (DForeign lang ty fn args)

59+simplify tl (DForeign ty fn args)

58 = do args' <- mapM sVar (map snd args)

60 = do args' <- mapM sVar (map snd args)

59 let fargs = zip (map fst args) args'

61 let fargs = zip (map fst args) args'

60− mkfapp (SForeign lang ty fn) fargs

62+ mkfapp (SForeign ty fn) fargs

61simplify tl (DLet n v e) = do v' <- simplify False v

63simplify tl (DLet n v e) = do v' <- simplify False v

62 e' <- simplify tl e

64 e' <- simplify tl e

63 return (SLet (Glob n) v' e')

65 return (SLet (Glob n) v' e')

@@ -159,10 +161,10 @@ scopecheck fn ctxt envTop tm = sc envTop tm where

159 " has arity " ++ show ar

161 " has arity " ++ show ar

160 Just _ -> return $ SApp tc f args'

162 Just _ -> return $ SApp tc f args'

161 Nothing -> failsc $ "No such variable " ++ show f

163 Nothing -> failsc $ "No such variable " ++ show f

162− sc env (SForeign l ty f args)

164+ sc env (SForeign ty f args)

163 = do args' <- mapM (\ (t, a) -> do a' <- scVar env a

165 = do args' <- mapM (\ (t, a) -> do a' <- scVar env a

164 return (t, a')) args

166 return (t, a')) args

165− return $ SForeign l ty f args'

167+ return $ SForeign ty f args'

166 sc env (SCon loc tag f args)

168 sc env (SCon loc tag f args)

167 = do loc' <- case loc of

169 = do loc' <- case loc of

168 Nothing -> return Nothing

170 Nothing -> return Nothing

src/Idris/Core/DeepSeq.hs+1−1

@@ -200,7 +200,7 @@ instance NFData Def where

200 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

201

202instance 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` ()

204

205instance NFData CaseDefs where

206 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

208

209 -- returns 'True' if the function should block

210 -- normal evaluation should return false

211− blockSimplify (CaseInfo inl dict) n stk

211+ blockSimplify (CaseInfo inl always dict) n stk

212 | RunTT `elem` opts

213+ = if always then False

213− = not (inl || dict) || elem n stk

214+ else not (inl || dict) || elem n stk

214 | Simplify `elem` opts

215 | Simplify `elem` opts

215 = (not (inl || dict) || elem n stk)

216 = (not (inl || dict) || elem n stk)

216 || (n == sUN "prim__syntactic_eq")

217 || (n == sUN "prim__syntactic_eq")

@@ -679,7 +680,8 @@ data CaseDefs = CaseDefs {

679 }

680 }

680

681

681data CaseInfo = CaseInfo {

682data CaseInfo = CaseInfo {

682− case_inlinable :: Bool,

683+ case_inlinable :: Bool, -- decided by machine

684+ case_alwaysinline :: Bool, -- decided by %inline flag

683 tc_dictionary :: Bool

685 tc_dictionary :: Bool

684 }

686 }

685

687

@@ -706,7 +708,7 @@ instance Show Def where

706 show (Function ty tm) = "Function: " ++ show (ty, tm)

708 show (Function ty tm) = "Function: " ++ show (ty, tm)

707 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty

709 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty

708 show (Operator ty _ _) = "Operator: " ++ show ty

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

710 = let (ns, sc) = cases_compiletime cd

712 = let (ns, sc) = cases_compiletime cd

711 (ns_t, sc_t) = cases_totcheck cd

713 (ns_t, sc_t) = cases_totcheck cd

712 (ns', sc') = cases_runtime cd in

714 (ns', sc') = cases_runtime cd in

@@ -717,7 +719,8 @@ instance Show Def where

717 show ns ++ " " ++ show sc ++ "\n\n" ++

719 show ns ++ " " ++ show sc ++ "\n\n" ++

718 "RUN TIME:\n\n" ++

720 "RUN TIME:\n\n" ++

719 show ns' ++ " " ++ show sc' ++ "\n\n" ++

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

721

724

722-------

725-------

723

726

@@ -865,7 +868,7 @@ addCasedef :: Name -> ErasureInfo -> CaseInfo ->

865 [([Name], Term, Term)] -> -- inlined

868 [([Name], Term, Term)] -> -- inlined

866 [([Name], Term, Term)] -> -- run time

869 [([Name], Term, Term)] -> -- run time

867 Type -> Context -> Context

870 Type -> Context -> Context

868−addCasedef n ei ci@(CaseInfo alwaysInline tcdict)

871+addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)

869 tcase covering reflect asserted argtys inacc

872 tcase covering reflect asserted argtys inacc

870 ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt

873 ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt

871 = let ctxt = definitions uctxt

874 = let ctxt = definitions uctxt

src/Idris/Core/Execute.hs+124−113

@@ -3,7 +3,7 @@ module Idris.Core.Execute (execute) where

4import Idris.AbsSyntax

5import Idris.AbsSyntaxTree

6−import IRTS.Lang(FType(..))

6+import IRTS.Lang(FDesc(..), FType(..))

8import Idris.Primitives(Prim(..), primitives)

@@ -231,52 +231,85 @@ execApp env ctxt con@(EP _ fp _) args@(tp:v:rest)

231 | fp == pioret = execApp env ctxt (mkEApp con [tp, v]) rest

232

233-- 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')

235 | fp == mkfprim,

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

236− Just (FFun "putStr" _ _) <- foreignFromTT fn

279+ | Just (FFun "putStr" [(_, str)] _) <- foreignFromTT arity ty fn xs

237− = case str of

280+ = case str of

238− EConstant (Str arg) -> do execIO (putStr arg)

281+ EConstant (Str arg) -> do execIO (putStr arg)

239− execApp env ctxt ioUnit rest

282+ execApp env ctxt ioUnit (drop arity xs)

240− _ -> execFail . Msg $

283+ _ -> execFail . Msg $

241− "The argument to putStr should be a constant string, but it was " ++

284+ "The argument to putStr should be a constant string, but it was " ++

242− show str ++

285+ show str ++

243− ". Are all cases covered?"

286+ ". Are all cases covered?"

244−execApp env ctxt (EP _ fp _) (_:fn:ch:_:rest)

245− | fp == mkfprim,

246− Just (FFun "putchar" _ _) <- foreignFromTT fn

287+ | Just (FFun "putchar" [(_, ch)] _) <- foreignFromTT arity ty fn xs

247 = case ch of

288 = case ch of

248 EConstant (Ch c) -> do execIO (putChar c)

289 EConstant (Ch c) -> do execIO (putChar c)

249− execApp env ctxt ioUnit rest

290+ execApp env ctxt ioUnit (drop arity xs)

250 EConstant (I i) -> do execIO (putChar (toEnum i))

291 EConstant (I i) -> do execIO (putChar (toEnum i))

251− execApp env ctxt ioUnit rest

292+ execApp env ctxt ioUnit (drop arity xs)

252 _ -> execFail . Msg $

293 _ -> execFail . Msg $

253 "The argument to putchar should be a constant character, but it was " ++

294 "The argument to putchar should be a constant character, but it was " ++

254 show str ++

295 show str ++

255 ". Are all cases covered?"

296 ". 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

259 = case handle of

298 = case handle of

260 EHandle h -> do contents <- execIO $ hGetLine h

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

262 _ -> execFail . Msg $

301 _ -> execFail . Msg $

263 "The argument to idris_readStr should be a handle, but it was " ++

302 "The argument to idris_readStr should be a handle, but it was " ++

264 show handle ++

303 show handle ++

265 ". Are all cases covered?"

304 ". 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

269 = do -- The C API returns an Int which Idris library code

306 = do -- The C API returns an Int which Idris library code

270 -- converts; thus, we must make an int here.

307 -- converts; thus, we must make an int here.

271 ch <- execIO $ fmap (ioWrap . EConstant . I . fromEnum) getChar

308 ch <- execIO $ fmap (ioWrap . EConstant . I . fromEnum) getChar

272− execApp env ctxt ch rest

309+ execApp env ctxt ch xs

273−execApp env ctxt (EP _ fp _) (_:fn:rest)

274− | fp == mkfprim,

275− Just (FFun "idris_time" _ _) <- foreignFromTT fn

310+ | Just (FFun "idris_time" _ _) <- foreignFromTT arity ty fn xs

276 = do execIO $ fmap (ioWrap . EConstant . I . round) getPOSIXTime

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

280 = case (fileStr, modeStr) of

313 = case (fileStr, modeStr) of

281 (EConstant (Str f), EConstant (Str mode)) ->

314 (EConstant (Str f), EConstant (Str mode)) ->

282 do f <- execIO $

315 do f <- execIO $

@@ -291,10 +324,10 @@ execApp env ctxt (EP _ fp _) (_:fn:fileStr:modeStr:rest)

291 case fmap (openFile f) m of

324 case fmap (openFile f) m of

292 Right h -> do h' <- h

325 Right h -> do h' <- h

293 hSetBinaryMode h' True

326 hSetBinaryMode h' True

294− return $ Right (ioWrap (EHandle h'), tail rest)

327+ return $ Right (ioWrap (EHandle h'), drop arity xs)

295 Left err -> return $ Left err)

328 Left err -> return $ Left err)

296 (\e -> let _ = ( e::SomeException)

329 (\e -> let _ = ( e::SomeException)

297− in return $ Right (ioWrap (EPtr nullPtr), tail rest))

330+ in return $ Right (ioWrap (EPtr nullPtr), drop arity xs))

298 case f of

331 case f of

299 Left err -> execFail . Msg $ err

332 Left err -> execFail . Msg $ err

300 Right (res, rest) -> execApp env ctxt res rest

333 Right (res, rest) -> execApp env ctxt res rest

@@ -302,105 +335,72 @@ execApp env ctxt (EP _ fp _) (_:fn:fileStr:modeStr:rest)

302 "The arguments to fileOpen should be constant strings, but they were " ++

335 "The arguments to fileOpen should be constant strings, but they were " ++

303 show fileStr ++ " and " ++ show modeStr ++

336 show fileStr ++ " and " ++ show modeStr ++

304 ". Are all cases covered?"

337 ". 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

309 = case handle of

339 = case handle of

310 EHandle h -> do eofp <- execIO $ hIsEOF h

340 EHandle h -> do eofp <- execIO $ hIsEOF h

311 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))

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

313 _ -> execFail . Msg $

343 _ -> execFail . Msg $

314 "The argument to fileEOF should be a file handle, but it was " ++

344 "The argument to fileEOF should be a file handle, but it was " ++

315 show handle ++

345 show handle ++

316 ". Are all cases covered?"

346 ". 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

321 = case handle of

348 = case handle of

322 EHandle h -> do execIO $ hClose h

349 EHandle h -> do execIO $ hClose h

323− execApp env ctxt ioUnit (tail rest)

350+ execApp env ctxt ioUnit (drop arity xs)

324 _ -> execFail . Msg $

351 _ -> execFail . Msg $

325 "The argument to fileClose should be a file handle, but it was " ++

352 "The argument to fileClose should be a file handle, but it was " ++

326 show handle ++

353 show handle ++

327 ". Are all cases covered?"

354 ". Are all cases covered?"

328

355

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

332 = case ptr of

357 = case ptr of

333 EPtr p -> let res = ioWrap . EConstant . I $

358 EPtr p -> let res = ioWrap . EConstant . I $

334 if p == nullPtr then 1 else 0

359 if p == nullPtr then 1 else 0

335− in execApp env ctxt res (tail rest)

360+ in execApp env ctxt res (drop arity xs)

336 -- Handles will be checked as null pointers sometimes - but if we got a

361 -- Handles will be checked as null pointers sometimes - but if we got a

337 -- real Handle, then it's valid, so just return 1.

362 -- real Handle, then it's valid, so just return 1.

338 EHandle h -> let res = ioWrap . EConstant . I $ 0

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

340 -- A foreign-returned char* has to be tested for NULL sometimes

365 -- A foreign-returned char* has to be tested for NULL sometimes

341 EConstant (Str s) -> let res = ioWrap . EConstant . I $ 0

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

343 _ -> execFail . Msg $

368 _ -> execFail . Msg $

344 "The argument to isNull should be a pointer or file handle or string, but it was " ++

369 "The argument to isNull should be a pointer or file handle or string, but it was " ++

345 show ptr ++

370 show ptr ++

346 ". Are all cases covered?"

371 ". Are all cases covered?"

347

372

348−

349-- Right now, there's no way to send command-line arguments to the executor,

373-- Right now, there's no way to send command-line arguments to the executor,

350-- so just return 0.

374-- so just return 0.

351−execApp env ctxt (EP _ fp _) (_:fn:rest)

375+execForeign env ctxt arity ty fn xs onfail

352− | fp == mkfprim,

353− Just (FFun "idris_numArgs" _ _) <- foreignFromTT fn

376+ | Just (FFun "idris_numArgs" _ _) <- foreignFromTT arity ty fn xs

354 = let res = ioWrap . EConstant . I $ 0

377 = let res = ioWrap . EConstant . I $ 0

355− in execApp env ctxt res (tail rest)

378+ in execApp env ctxt res (drop arity xs)

356−

379+

357−execApp env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim

380+execForeign env ctxt arity ty fn xs onfail

358− = case foreignFromTT fn of

381+ = case foreignFromTT arity ty fn xs of

359− Just (FFun f argTs retT) | length xs >= length argTs ->

382+ Just ffun@(FFun f argTs retT) | length xs >= arity ->

360− do let (args', xs') = (take (length argTs) xs, -- foreign args

383+ do let (args', xs') = (take arity xs, -- foreign args

361− drop (length argTs + 1) xs) -- rest

384+ drop arity xs) -- rest

362− res <- stepForeign (ty:fn:args')

385+ res <- call ffun (map snd argTs)

363 case res of

386 case res of

364 Nothing -> fail $ "Could not call foreign function \"" ++ f ++

387 Nothing -> fail $ "Could not call foreign function \"" ++ f ++

365− "\" with args " ++ show args

388+ "\" with args " ++ show (map snd argTs)

366 Just r -> return (mkEApp r xs')

389 Just r -> return (mkEApp r xs')

367− Nothing -> return (mkEApp f args)

390+ Nothing -> return onfail

391+

368

392

369−execApp env ctxt c@(EP (DCon _ arity _) n _) args =

393+splitArg tm | (_, [_,_,l,r]) <- unApplyV tm -- pair, two implicits

370− do let args' = take arity args

394+ = Just (toFDesc l, r)

371− let restArgs = drop arity args

395+splitArg _ = Nothing

372− execApp env ctxt (mkEApp c args') restArgs

373

396

374−execApp env ctxt c@(EP (TCon _ arity) n _) args =

397+toFDesc tm

375− do let args' = take arity args

398+ | (EP _ n _, []) <- unApplyV tm = FCon (deNS n)

376− let restArgs = drop arity args

399+ | (EP _ n _, as) <- unApplyV tm = FApp (deNS n) (map toFDesc as)

377− execApp env ctxt (mkEApp c args') restArgs

400+toFDesc _ = FUnknown

378

401

379−execApp env ctxt f@(EP _ n _) args =

402+deNS (NS n _) = n

380− do let val = lookupDef n ctxt

403+deNS n = n

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)

404

405prs = sUN "prim__readString"

406pbm = sUN "prim__believe_me"

@@ -494,13 +494,35 @@ idrisType ft = EConstant (idr ft)

494 idr FString = StrType

495 idr FPtr = PtrType

496

497−data Foreign = FFun String [FType] FType deriving Show

497+data Foreign = FFun String [(FDesc, ExecVal)] FDesc deriving Show

498−

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

499

520

500call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)

521call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)

501call (FFun name argTypes retType) args =

522call (FFun name argTypes retType) args =

502 do fn <- findForeign name

523 do fn <- findForeign name

524+ maybe (return Nothing)

503− maybe (return Nothing) (\f -> Just . ioWrap <$> call' f args retType) fn

525+ (\f -> Just . ioWrap <$> call' f args (toFType retType)) fn

504 where call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal

526 where call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal

505 call' (Fun _ h) args (FArith (ATInt ITNative)) = do

527 call' (Fun _ h) args (FArith (ATInt ITNative)) = do

506 res <- execIO $ callFFI h retCInt (prepArgs args)

528 res <- execIO $ callFFI h retCInt (prepArgs args)

@@ -549,15 +571,11 @@ call (FFun name argTypes retType) args =

549 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined

571 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined

550

572

551

573

552−

553−foreignFromTT :: ExecVal -> Maybe Foreign

574+foreignFromTT :: Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign

554−foreignFromTT t = case (unApplyV t) of

555− (_, [(EConstant (Str name)), args, ret]) ->

575+foreignFromTT arity ty (EConstant (Str name)) args

556− do argTy <- unEList args

576+ = do argFTyVals <- mapM splitArg (take arity args)

557− argFTy <- sequence $ map getFTy argTy

558− retFTy <- getFTy ret

559− return $ FFun name argFTy retFTy

577+ return $ FFun name argFTyVals (toFDesc ty)

560− _ -> trace ("failed to construct ffun") Nothing

578+foreignFromTT arity ty fn args = trace ("failed to construct ffun from " ++ show (ty,fn,args)) Nothing

561

579

562getFTy :: ExecVal -> Maybe FType

580getFTy :: ExecVal -> Maybe FType

563getFTy (EApp (EP _ (UN fi) _) (EP _ (UN intTy) _))

581getFTy (EApp (EP _ (UN fi) _) (EP _ (UN intTy) _))

@@ -592,13 +610,6 @@ toConst :: Term -> Maybe Const

592toConst (Constant c) = Just c

610toConst (Constant c) = Just c

593toConst _ = Nothing

611toConst _ = Nothing

594

612

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−

602mapMaybeM :: (Functor m, Monad m) => (a -> m (Maybe b)) -> [a] -> m [b]

613mapMaybeM :: (Functor m, Monad m) => (a -> m (Maybe b)) -> [a] -> m [b]

603mapMaybeM f [] = return []

614mapMaybeM f [] = return []

604mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs

615mapMaybeM 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 =

222 let opt = idris_optimisation ist

223 putIState (ist { idris_patdefs = addDef n (force pdef_pe, force pmissing)

224 (idris_patdefs ist) })

225− let caseInfo = CaseInfo (inlinable opts) (dictionary opts)

225+ let caseInfo = CaseInfo (inlinable opts) (inlinable opts) (dictionary opts)

226 case lookupTy n ctxt of

227 [ty] -> do updateContext (addCasedef n erInfo caseInfo

228 tcase defaultcase

@@ -408,6 +408,7 @@ elabPE info fc caller r =

408 _ -> True

409 concreteTm ist (Constant _) = True

410 concreteTm ist (Bind n (Lam _) sc) = True

411+ concreteTm ist (Bind n (Pi _ _ _) sc) = True

411 concreteTm ist (Bind n (Let _ _) sc) = concreteTm ist sc

412 concreteTm ist (Bind n (Let _ _) sc) = concreteTm ist sc

412 concreteTm ist _ = False

413 concreteTm ist _ = False

413

414

src/Idris/Erasure.hs+7−4

@@ -192,13 +192,16 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

192 -- These two, Main.main and run__IO, are always evaluated

193 -- but they elude analysis since they come from the seed term.

194 [ [(mainName, Result)]

195− , [(sUN "run__IO", Result), (sUN "run__IO", Arg 0)]

195+ , [(sUN "run__IO", Result), (sUN "run__IO", Arg 1)]

196

197 -- MkIO is read by run__IO,

198 -- but this cannot be observed in the source code of programs.

199− , it "MkIO" [1]

199+ , it "MkIO" [2]

200 , it "prim__IO" [1]

201

202+ , [(pairCon, Arg 2),

203+ (pairCon, Arg 3)] -- TMP HACK

204+

202 -- these have been discovered as builtins but are not listed

205 -- these have been discovered as builtins but are not listed

203 -- among Idris.Primitives.primitives

206 -- among Idris.Primitives.primitives

204 --, mn "__MkPair" [2,3]

207 --, mn "__MkPair" [2,3]

@@ -380,8 +383,8 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

380 -- which is the (Foreign a) spec that defines the type

383 -- which is the (Foreign a) spec that defines the type

381 -- and is not needed at runtime.

384 -- and is not needed at runtime.

382 P _ (UN n) _

385 P _ (UN n) _

383− | n `elem` map T.pack ["mkForeign", "mkForeignPrim", "mkLazyForeignPrim"]

386+ | n `elem` map T.pack ["mkForeignPrim"]

384− -> unconditionalDeps (drop 1 args)

387+ -> unconditionalDeps args -- (drop 1 args)

385

388

386 -- a bound variable might draw in additional dependencies,

389 -- a bound variable might draw in additional dependencies,

387 -- think: f x = x 0 <-- here, `x' _is_ used

390 -- think: f x = x 0 <-- here, `x' _is_ used

src/Idris/IBC.hs+6−4

@@ -35,7 +35,7 @@ import Codec.Compression.Zlib (compress)

35import Util.Zlib (decompressEither)

37ibcVersion :: Word8

38−ibcVersion = 93

38+ibcVersion = 94

40data IBCFile = IBCFile { ver :: Word8,

41 sourcefile :: FilePath,

@@ -778,11 +778,13 @@ instance Binary CaseDefs where

778 return (CaseDefs x2 x2 x2 x4)

779

780instance Binary CaseInfo where

781− put x@(CaseInfo x1 x2) = do put x1

781+ put x@(CaseInfo x1 x2 x3) = do put x1

782− put x2

782+ put x2

783+ put x3

783 get = do x1 <- get

784 get = do x1 <- get

784 x2 <- get

785 x2 <- get

786+ x3 <- get

785− return (CaseInfo x1 x2)

787+ return (CaseInfo x1 x2 x3)

786

788

787instance Binary Def where

789instance Binary Def where

788 put x

790 put x

src/Idris/ParseExpr.hs+15−28

@@ -526,34 +526,21 @@ MatchApp ::=

526@

527-}

528app :: 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

530 fc <- getFC

538 fc <- getFC

531− fn <- arg syn

532− args <- many (do notEndApp; arg syn)

533 i <- get

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

540+ args <- many (do notEndApp; arg syn)

554− case args of

541+ case args of

555− [] -> return f

542+ [] -> return f

556− _ -> return (dslify i (PApp fc f args)))

543+ _ -> return (dslify i (PApp fc f args)))

557 <?> "function application"

544 <?> "function application"

558 where

545 where

559 dslify :: IState -> PTerm -> PTerm

546 dslify :: IState -> PTerm -> PTerm

@@ -868,7 +855,7 @@ pi syn =

868 sc <- expr syn

855 sc <- expr syn

869 return (bindList (PPi binder) xt sc)) <|> (do

856 return (bindList (PPi binder) xt sc)) <|> (do

870 (do try (lchar '{' *> reserved "auto")

857 (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"

872 xt <- typeDeclList syn

859 xt <- typeDeclList syn

873 lchar '}'

860 lchar '}'

874 symbol "->"

861 symbol "->"

@@ -876,7 +863,7 @@ pi syn =

876 return (bindList (PPi

863 return (bindList (PPi

877 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)) <|> (do

864 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)) <|> (do

878 try (lchar '{' *> reserved "default")

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

880 script <- simpleExpr syn

867 script <- simpleExpr syn

881 xt <- typeDeclList syn

868 xt <- typeDeclList syn

882 lchar '}'

869 lchar '}'

src/Idris/Parser.hs+2

@@ -425,6 +425,8 @@ fnOpts opts

425 fnOpts (CExport c : opts)

426 <|> do try (lchar '%' *> reserved "no_implicit");

427 fnOpts (NoImplicit : opts)

428+ <|> do try (lchar '%' *> reserved "inline");

429+ fnOpts (Inlinable : opts)

428 <|> do try (lchar '%' *> reserved "assert_total");

430 <|> do try (lchar '%' *> reserved "assert_total");

429 fnOpts (AssertTotal : opts)

431 fnOpts (AssertTotal : opts)

430 <|> do try (lchar '%' *> reserved "error_handler");

432 <|> do try (lchar '%' *> reserved "error_handler");

src/Idris/Prover.hs+1−1

@@ -86,7 +86,7 @@ prove opt ctxt lit n ty

86 Error e -> ierror (CantUnify False ty pty e [] 0)

87 ptm' <- applyOpts ptm

88 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

90 [] [] -- argtys, inaccArgs

91 [Right (P Ref n ty, ptm)]

92 [([], P Ref n ty, ptm)]

test/ffi001/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

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

3%dynamic "dummy", "libm", "msvcrt"

5x : Float

6−x = unsafePerformIO (mkForeign (FFun "sin" [FFloat] FFloat) 1.6)

6+x = unsafePerformIO (foreign FFI_C "sin" (Float -> IO Float) 1.6)

8main : IO ()

9main = 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.