Skip to content

Commit 2a957a3

Browse files
madman-bobgallais
madman-bob
authored and
gallais
committed
Add RefC FFI header file support
1 parent 51ddcad commit 2a957a3

File tree

11 files changed

+77
-103
lines changed

11 files changed

+77
-103
lines changed

‎libs/base/Data/Buffer.idr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -230,11 +230,11 @@ copyData : HasIO io => (src : Buffer) -> (start, len : Int) ->
230230
copyData src start len dest loc
231231
= primIO (prim__copyData src start len dest loc)
232232

233-
%foreign "C:idris2_readBufferData,libidris2_support"
233+
%foreign "C:idris2_readBufferData, libidris2_support, idris_buffer.h"
234234
"node:lambda:(f,b,l,m) => BigInt(require('fs').readSync(f.fd,b,Number(l), Number(m)))"
235235
prim__readBufferData : FilePtr -> Buffer -> Int -> Int -> PrimIO Int
236236

237-
%foreign "C:idris2_writeBufferData,libidris2_support"
237+
%foreign "C:idris2_writeBufferData, libidris2_support, idris_buffer.h"
238238
"node:lambda:(f,b,l,m) => BigInt(require('fs').writeSync(f.fd,b,Number(l), Number(m)))"
239239
prim__writeBufferData : FilePtr -> Buffer -> Int -> Int -> PrimIO Int
240240

‎libs/base/System.idr

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ import Data.List
55
import Data.Strings
66

77
support : String -> String
8-
support fn = "C:" ++ fn ++ ", libidris2_support"
8+
support fn = "C:" ++ fn ++ ", libidris2_support, idris_support.h"
99

1010
libc : String -> String
1111
libc fn = "C:" ++ fn ++ ", libc 6"
@@ -15,12 +15,10 @@ libc fn = "C:" ++ fn ++ ", libc 6"
1515

1616
%foreign "scheme,racket:blodwen-sleep"
1717
support "idris2_sleep"
18-
-- "C:idris2_sleep, libidris2_support"
1918
prim__sleep : Int -> PrimIO ()
2019

2120
%foreign "scheme,racket:blodwen-usleep"
2221
support "idris2_usleep"
23-
-- "C:idris2_usleep, libidris2_support"
2422
prim__usleep : Int -> PrimIO ()
2523

2624
export

‎libs/base/System/Directory.idr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,9 +7,9 @@ DirPtr : Type
77
DirPtr = AnyPtr
88

99
support : String -> String
10-
support fn = "C:" ++ fn ++ ", libidris2_support"
10+
support fn = "C:" ++ fn ++ ", libidris2_support, idris_directory.h"
1111

12-
%foreign support "idris2_fileErrno"
12+
%foreign "C:idris2_fileErrno, libidris2_support, idris_file.h"
1313
"node:support:fileErrno,support_system_file"
1414
prim__fileErrno : PrimIO Int
1515

‎libs/base/System/File.idr

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -16,10 +16,7 @@ FilePtr : Type
1616
FilePtr = AnyPtr
1717

1818
support : String -> String
19-
support fn = "C:" ++ fn ++ ", libidris2_support"
20-
21-
libc : String -> String
22-
libc fn = "C:" ++ fn ++ ", libc 6"
19+
support fn = "C:" ++ fn ++ ", libidris2_support, idris_file.h"
2320

2421
%foreign support "idris2_openFile"
2522
"node:support:openFile,support_system_file"
@@ -97,7 +94,7 @@ prim__stdout : FilePtr
9794
"node:lambda:x=>({fd:2, buffer: Buffer.alloc(0), name:'<stderr>', eof: false})"
9895
prim__stderr : FilePtr
9996

100-
%foreign libc "chmod"
97+
%foreign "C:chmod, libc 6, sys/stat.h"
10198
"node:support:chmod,support_system_file"
10299
prim__chmod : String -> Int -> PrimIO Int
103100

‎libs/base/System/Info.idr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ export
1515
isWindows : Bool
1616
isWindows = os `elem` ["windows", "mingw32", "cygwin32"]
1717

18-
%foreign "C:idris2_getNProcessors, libidris2_support"
18+
%foreign "C:idris2_getNProcessors, libidris2_support, idris_support.h"
1919
prim__getNProcessors : PrimIO Int
2020

2121
export

‎libs/network/Network/FFI.idr

Lines changed: 33 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -7,146 +7,146 @@ import Network.Socket.Data
77

88
-- From sys/socket.h
99

10-
%foreign "C:close,libidris2_support"
10+
%foreign "C:close, libc 6"
1111
export
1212
prim__socket_close : (sockdes : SocketDescriptor) -> PrimIO Int
1313

14-
%foreign "C:listen,libc 6"
14+
%foreign "C:listen, libc 6"
1515
export
1616
prim__socket_listen : (sockfd : SocketDescriptor) -> (backlog : Int) -> PrimIO Int
1717

1818

1919
-- From idris_net.h
2020

21-
%foreign "C:idrnet_socket,libidris2_support"
21+
%foreign "C:idrnet_socket, libidris2_support, idris_net.h"
2222
export
2323
prim__idrnet_socket : (domain, type, protocol : Int) -> PrimIO Int
2424

25-
%foreign "C:idrnet_bind,libidris2_support"
25+
%foreign "C:idrnet_bind, libidris2_support, idris_net.h"
2626
export
2727
prim__idrnet_bind : (sockfd : SocketDescriptor) -> (family, socket_type : Int) ->
2828
(host : String) -> (port : Port) -> PrimIO Int
2929

30-
%foreign "C:idrnet_connect,libidris2_support"
30+
%foreign "C:idrnet_connect, libidris2_support, idris_net.h"
3131
export
3232
prim__idrnet_connect : (sockfd : SocketDescriptor) -> (family, socket_type : Int) ->
3333
(host : String) -> (port : Port) -> PrimIO Int
3434

35-
%foreign "C:idrnet_sockaddr_family,libidris2_support"
35+
%foreign "C:idrnet_sockaddr_family, libidris2_support, idris_net.h"
3636
export
3737
prim__idrnet_sockaddr_family : (sockaddr : AnyPtr) -> PrimIO Int
3838

39-
%foreign "C:idrnet_sockaddr_ipv4,libidris2_support"
39+
%foreign "C:idrnet_sockaddr_ipv4, libidris2_support, idris_net.h"
4040
export
4141
prim__idrnet_sockaddr_ipv4 : (sockaddr : AnyPtr) -> PrimIO String
4242

43-
%foreign "C:idrnet_sockaddr_unix,libidris2_support"
43+
%foreign "C:idrnet_sockaddr_unix, libidris2_support, idris_net.h"
4444
export
4545
prim__idrnet_sockaddr_unix : (sockaddr : AnyPtr) -> PrimIO String
4646

47-
%foreign "C:idrnet_sockaddr_ipv4_port,libidris2_support"
47+
%foreign "C:idrnet_sockaddr_ipv4_port, libidris2_support, idris_net.h"
4848
export
4949
prim__idrnet_sockaddr_ipv4_port : (sockaddr : AnyPtr) -> PrimIO Int
5050

51-
%foreign "C:idrnet_sockaddr_port,libidris2_support"
51+
%foreign "C:idrnet_sockaddr_port, libidris2_support, idris_net.h"
5252
export
5353
prim__idrnet_sockaddr_port : (sockfd : SocketDescriptor) -> PrimIO Int
5454

5555

56-
%foreign "C:idrnet_create_sockaddr,libidris2_support"
56+
%foreign "C:idrnet_create_sockaddr, libidris2_support, idris_net.h"
5757
export
5858
prim__idrnet_create_sockaddr : PrimIO AnyPtr
5959

60-
%foreign "C:idrnet_accept,libidris2_support"
60+
%foreign "C:idrnet_accept, libidris2_support, idris_net.h"
6161
export
6262
prim__idrnet_accept : (sockfd : SocketDescriptor) -> (sockaddr : AnyPtr) -> PrimIO Int
6363

64-
%foreign "C:idrnet_send,libidris2_support"
64+
%foreign "C:idrnet_send, libidris2_support, idris_net.h"
6565
export
6666
prim__idrnet_send : (sockfd : SocketDescriptor) -> (dataString : String) -> PrimIO Int
6767

68-
%foreign "C:idrnet_send_buf,libidris2_support"
68+
%foreign "C:idrnet_send_buf, libidris2_support, idris_net.h"
6969
export
7070
prim__idrnet_send_buf : (sockfd : SocketDescriptor) -> (dataBuffer : AnyPtr) -> (len : Int) -> PrimIO Int
7171

7272

73-
%foreign "C:idrnet_recv,libidris2_support"
73+
%foreign "C:idrnet_recv, libidris2_support, idris_net.h"
7474
export
7575
prim__idrnet_recv : (sockfd : SocketDescriptor) -> (len : Int) -> PrimIO AnyPtr
7676

77-
%foreign "C:idrnet_recv_buf,libidris2_support"
77+
%foreign "C:idrnet_recv_buf, libidris2_support, idris_net.h"
7878
export
7979
prim__idrnet_recv_buf : (sockfd : SocketDescriptor) -> (buf : AnyPtr) -> (len : Int) -> PrimIO Int
8080

81-
%foreign "C:idrnet_sendto,libidris2_support"
81+
%foreign "C:idrnet_sendto, libidris2_support, idris_net.h"
8282
export
8383
prim__idrnet_sendto : (sockfd : SocketDescriptor) -> (dataString,host : String) ->
8484
(port : Port) -> (family : Int) -> PrimIO Int
8585

86-
%foreign "C:idrnet_sendto_buf,libidris2_support"
86+
%foreign "C:idrnet_sendto_buf, libidris2_support, idris_net.h"
8787
export
8888
prim__idrnet_sendto_buf : (sockfd : SocketDescriptor) -> (dataBuf : AnyPtr) ->
8989
(buf_len : Int) -> (host : String) -> (port : Port) ->
9090
(family : Int) -> PrimIO Int
9191

92-
%foreign "C:idrnet_recvfrom,libidris2_support"
92+
%foreign "C:idrnet_recvfrom, libidris2_support, idris_net.h"
9393
export
9494
prim__idrnet_recvfrom : (sockfd : SocketDescriptor) -> (len : Int) -> PrimIO AnyPtr
9595

96-
%foreign "C:idrnet_recvfrom_buf,libidris2_support"
96+
%foreign "C:idrnet_recvfrom_buf, libidris2_support, idris_net.h"
9797
export
9898
prim__idrnet_recvfrom_buf : (sockfd : SocketDescriptor) -> (buf : AnyPtr) -> (len : Int) -> PrimIO AnyPtr
9999

100-
%foreign "C:idrnet_get_recv_res,libidris2_support"
100+
%foreign "C:idrnet_get_recv_res, libidris2_support, idris_net.h"
101101
export
102102
prim__idrnet_get_recv_res : (res_struct : AnyPtr) -> PrimIO Int
103103

104-
%foreign "C:idrnet_get_recv_payload,libidris2_support"
104+
%foreign "C:idrnet_get_recv_payload, libidris2_support, idris_net.h"
105105
export
106106
prim__idrnet_get_recv_payload : (res_struct : AnyPtr) -> PrimIO String
107107

108-
%foreign "C:idrnet_free_recv_struct,libidris2_support"
108+
%foreign "C:idrnet_free_recv_struct, libidris2_support, idris_net.h"
109109
export
110110
prim__idrnet_free_recv_struct : (res_struct : AnyPtr) -> PrimIO ()
111111

112-
%foreign "C:idrnet_get_recvfrom_res,libidris2_support"
112+
%foreign "C:idrnet_get_recvfrom_res, libidris2_support, idris_net.h"
113113
export
114114
prim__idrnet_get_recvfrom_res : (res_struct : AnyPtr) -> PrimIO Int
115115

116-
%foreign "C:idrnet_get_recvfrom_payload,libidris2_support"
116+
%foreign "C:idrnet_get_recvfrom_payload, libidris2_support, idris_net.h"
117117
export
118118
prim__idrnet_get_recvfrom_payload : (res_struct : AnyPtr) -> PrimIO String
119119

120-
%foreign "C:idrnet_get_recvfrom_sockaddr,libidris2_support"
120+
%foreign "C:idrnet_get_recvfrom_sockaddr, libidris2_support, idris_net.h"
121121
export
122122
prim__idrnet_get_recvfrom_sockaddr : (res_struct : AnyPtr) -> PrimIO AnyPtr
123123

124-
%foreign "C:idrnet_free_recvfrom_struct,libidris2_support"
124+
%foreign "C:idrnet_free_recvfrom_struct, libidris2_support, idris_net.h"
125125
export
126126
prim__idrnet_free_recvfrom_struct : (res_struct : AnyPtr) -> PrimIO ()
127127

128128

129-
%foreign "C:idrnet_geteagain,libidris2_support"
129+
%foreign "C:idrnet_geteagain, libidris2_support, idris_net.h"
130130
export
131131
prim__idrnet_geteagain : PrimIO Int
132132

133-
%foreign "C:idrnet_errno,libidris2_support"
133+
%foreign "C:idrnet_errno, libidris2_support, idris_net.h"
134134
export
135135
prim__idrnet_errno : PrimIO Int
136136

137-
%foreign "C:idrnet_malloc,libidris2_support"
137+
%foreign "C:idrnet_malloc, libidris2_support, idris_net.h"
138138
export
139139
prim__idrnet_malloc : (size : Int) -> PrimIO AnyPtr
140140

141-
%foreign "C:idrnet_free,libidris2_support"
141+
%foreign "C:idrnet_free, libidris2_support, idris_net.h"
142142
export
143143
prim__idrnet_free : (ptr : AnyPtr) -> PrimIO ()
144144

145-
%foreign "C:idrnet_peek,libidris2_support"
145+
%foreign "C:idrnet_peek, libidris2_support, idris_net.h"
146146
export
147147
prim__idrnet_peek : (ptr : AnyPtr) -> (offset : {-Unsigned-} Int) -> PrimIO {-Unsigned-} Int
148148

149-
%foreign "C:idrnet_poke,libidris2_support"
149+
%foreign "C:idrnet_poke, libidris2_support, idris_net.h"
150150
export
151151
prim__idrnet_poke : (ptr : AnyPtr) -> (offset : {-Unsigned-} Int) ->
152152
(val : Int {- should be Char? -}) -> PrimIO ()

‎libs/network/Network/Socket/Data.idr

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ BACKLOG : Int
4848
BACKLOG = 20
4949

5050
-- Repeat to avoid a dependency cycle
51-
%foreign "C:idrnet_geteagain,libidris2_support"
51+
%foreign "C:idrnet_geteagain, libidris2_support, idris_net.h"
5252
prim__idrnet_geteagain : PrimIO Int
5353

5454
export
@@ -61,10 +61,10 @@ EAGAIN =
6161
-- ---------------------------------------------------------------- [ Error Code ]
6262

6363
-- repeat without export to avoid dependency cycles
64-
%foreign "C:idrnet_errno,libidris2_support"
64+
%foreign "C:idrnet_errno, libidris2_support, idris_net.h"
6565
prim__idrnet_errno : PrimIO Int
6666

67-
%foreign "C:isNull,libidris2_support"
67+
%foreign "C:isNull, libidris2_support, idris_support.h"
6868
prim__idrnet_isNull : (ptr : AnyPtr) -> PrimIO Int
6969

7070

@@ -113,16 +113,16 @@ Show SocketFamily where
113113
-- This is a bit of a hack to get the OS-dependent magic constants out of C and
114114
-- into Idris without having to faff around on the preprocessor on the Idris
115115
-- side.
116-
%foreign "C:idrnet_af_unspec,libidris2_support"
116+
%foreign "C:idrnet_af_unspec, libidris2_support, idris_net.h"
117117
prim__idrnet_af_unspec : PrimIO Int
118118

119-
%foreign "C:idrnet_af_unix,libidris2_support"
119+
%foreign "C:idrnet_af_unix, libidris2_support, idris_net.h"
120120
prim__idrnet_af_unix : PrimIO Int
121121

122-
%foreign "C:idrnet_af_inet,libidris2_support"
122+
%foreign "C:idrnet_af_inet, libidris2_support, idris_net.h"
123123
prim__idrnet_af_inet : PrimIO Int
124124

125-
%foreign "C:idrnet_af_inet6,libidris2_support"
125+
%foreign "C:idrnet_af_inet6, libidris2_support, idris_net.h"
126126
prim__idrnet_af_inet6 : PrimIO Int
127127

128128
export

‎libs/prelude/Prelude/IO.idr

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ export
6969
onCollect : Ptr t -> (Ptr t -> IO ()) -> IO (GCPtr t)
7070
onCollect ptr c = fromPrim (prim__onCollect ptr (\x => toPrim (c x)))
7171

72-
%foreign "C:idris2_getString, libidris2_support"
72+
%foreign "C:idris2_getString, libidris2_support, idris_support.h"
7373
"javascript:lambda:x=>x"
7474
export
7575
prim__getString : Ptr String -> String
@@ -79,11 +79,11 @@ prim__putChar : Char -> (1 x : %World) -> IORes ()
7979
%foreign "C:getchar,libc 6"
8080
%extern prim__getChar : (1 x : %World) -> IORes Char
8181

82-
%foreign "C:idris2_getStr,libidris2_support"
82+
%foreign "C:idris2_getStr, libidris2_support, idris_support.h"
8383
"node:support:getStr,support_system_file"
8484
prim__getStr : PrimIO String
8585

86-
%foreign "C:idris2_putStr,libidris2_support"
86+
%foreign "C:idris2_putStr, libidris2_support, idris_support.h"
8787
"node:lambda:x=>process.stdout.write(x)"
8888
prim__putStr : String -> PrimIO ()
8989

@@ -133,7 +133,7 @@ export
133133
threadWait : (1 threadID : ThreadID) -> IO ()
134134
threadWait threadID = fromPrim (prim__threadWait threadID)
135135

136-
%foreign "C:idris2_readString, libidris2_support"
136+
%foreign "C:idris2_readString, libidris2_support, idris_support.h"
137137
export
138138
prim__getErrno : Int
139139

‎libs/prelude/PrimIO.idr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -70,12 +70,12 @@ export %inline
7070
toPrim : (1 act : IO a) -> PrimIO a
7171
toPrim (MkIO fn) = fn
7272

73-
%foreign "C:idris2_isNull, libidris2_support"
73+
%foreign "C:idris2_isNull, libidris2_support, idris_support.h"
7474
"javascript:lambda:x=>x===undefined||x===null?1n:0n"
7575
export
7676
prim__nullAnyPtr : AnyPtr -> Int
7777

78-
%foreign "C:idris2_getNull,libidris2_support"
78+
%foreign "C:idris2_getNull, libidris2_support, idris_support.h"
7979
export
8080
prim__getNullAnyPtr : AnyPtr
8181

0 commit comments

Comments
 (0)