git.iko.soy/Idris-dev
on master help sign in
Add Buffer type and primitives to the core
149e816Shea Levy
libs/base/Data/Buffer.idr+127−68
compare with master
unifiedsplit
@@ -5,7 +5,7 @@ module Data.Buffer
5-- !!! TODO: Open issues:
5-- !!! TODO: Open issues:
6-- 1. It may be theoretically nice to represent Buffer size as
6-- 1. It may be theoretically nice to represent Buffer size as
7-- Fin (2 ^ WORD_BITS) instead of Nat
7-- Fin (2 ^ WORD_BITS) instead of Nat
8−-- 2. Primitives take Integers when really they should take the
8+-- 2. Primitives take Bits64 when really they should take the
9-- equivalent of C's size_t (ideally unboxed)
9-- equivalent of C's size_t (ideally unboxed)
10-- 3. If we had access to host system information, we could reduce
10-- 3. If we had access to host system information, we could reduce
11-- the needed primitives by implementing the LE/BE variants on
11-- the needed primitives by implementing the LE/BE variants on
@@ -16,55 +16,80 @@ module Data.Buffer
16-- 5. Would be nice to be able to peek/append the vector types, but
16-- 5. Would be nice to be able to peek/append the vector types, but
17-- for now I'm only touching the C backend which AFAICT doesn't
17-- for now I'm only touching the C backend which AFAICT doesn't
18-- support them.
18-- support them.
19−-- 6. Conversion from Fin to Integer (which, re 2, should eventually
19+-- 6. Conversion from Fin to Bits64 (which, re 2, should eventually
20-- be a fixed-width implementation-dependent type) is likely
20-- be a fixed-width implementation-dependent type) is likely
21−-- inefficient relative to conversion from Nat to Integer
21+-- inefficient relative to conversion from Nat to Bits64
22
22
23-- A contiguous chunk of n bytes
23-- A contiguous chunk of n bytes
24abstract
24abstract
25record Buffer : Nat -> Type where
25record Buffer : Nat -> Type where
26 MkBuffer : ( realBuffer : prim__UnsafeBuffer ) -> Buffer n
26 MkBuffer : ( realBuffer : prim__UnsafeBuffer ) -> Buffer n
27
27
28+bitsFromNat : Nat -> Bits64
29+bitsFromNat Z = 0
30+bitsFromNat (S k) = 1 + bitsFromNat k
31+
32+bitsFromFin : Fin n -> Bits64
33+bitsFromFin fZ = 0
34+bitsFromFin (fS k) = 1 + bitsFromFin k
35+
28-- Allocate an empty Buffer. The size hint can be used to avoid
36-- Allocate an empty Buffer. The size hint can be used to avoid
29-- unnecessary reallocations and copies under the hood if the
37-- unnecessary reallocations and copies under the hood if the
30−-- approximate ultimate size of the Buffer is known
38+-- approximate ultimate size of the Buffer is known. Users can assume
39+-- the new Buffer is word-aligned.
31public
40public
32allocate : ( hint : Nat ) -> Buffer 0
41allocate : ( hint : Nat ) -> Buffer 0
33−allocate = MkBuffer . prim__allocate . toIntegerNat
42+allocate = MkBuffer . prim__allocate . bitsFromNat
34
43
35-- Copy a buffer. Since multiple buffers can reference the same
44-- Copy a buffer. Since multiple buffers can reference the same
36-- underlying chunk of memory, it may happen that a reference to
45-- underlying chunk of memory, it may happen that a reference to
37-- a relatively small bit of data might be preventing the runtime
46-- a relatively small bit of data might be preventing the runtime
38-- from freeing a much larger chunk. copy allows giving up references
47-- from freeing a much larger chunk. copy allows giving up references
39-- to the larger chunk without losing the smaller one.
48-- to the larger chunk without losing the smaller one.
49+%assert_total
40public
50public
41copy : Buffer n -> Buffer n
51copy : Buffer n -> Buffer n
42−copy = MkBuffer . prim__copy ( toIntegerNat n ) . realBuffer
52+copy { n } = MkBuffer . prim__copy ( bitsFromNat n ) . realBuffer
43
53
44-- Read a Buffer from another Buffer starting at offset
54-- Read a Buffer from another Buffer starting at offset
45-- (i.e. create a view of a subset of the Buffer)
55-- (i.e. create a view of a subset of the Buffer)
56+%assert_total
46public
57public
47−peekBufferNative : Buffer ( n + m ) -> ( offset : Fin n ) -> Buffer m
58+peekBufferNative : Buffer ( m + n ) ->
59+ ( offset : Fin ( n + 1 ) ) ->
60+ Buffer m
48peekBufferNative ( MkBuffer real ) =
61peekBufferNative ( MkBuffer real ) =
49− MkBuffer . prim__peekBufferNative real . finToInteger
62+ MkBuffer . prim__peekBufferNative real . bitsFromFin
50
63
51public
64public
52−peekBufferLE : Buffer ( n + m ) -> ( offset : Fin n ) -> Buffer m
65+peekBufferLE : Buffer ( m + n ) ->
66+ ( offset : Fin ( n + 1 ) ) ->
67+ Buffer m
53peekBufferLE = peekBufferNative
68peekBufferLE = peekBufferNative
54
69
55public
70public
56−peekBufferBE : Buffer ( n + m ) -> ( offset : Fin n ) -> Buffer m
71+peekBufferBE : Buffer ( m + n ) ->
72+ ( offset : Fin ( n + 1 ) ) ->
73+ Buffer m
57peekBufferBE = peekBufferNative
74peekBufferBE = peekBufferNative
58
75
59-- Append count repetitions of a Buffer to another Buffer
76-- Append count repetitions of a Buffer to another Buffer
77+%assert_total
60public
78public
61appendBufferNative : Buffer n ->
79appendBufferNative : Buffer n ->
62 ( count : Nat ) ->
80 ( count : Nat ) ->
63 Buffer m ->
81 Buffer m ->
64 Buffer ( n + m * count )
82 Buffer ( n + m * count )
65−appendBufferNative ( MkBuffer input ) count = MkBuffer .
83+appendBufferNative { n } { m } ( MkBuffer input ) count =
84+ MkBuffer . app . realBuffer
85+ where
86+ nBits : Bits64
87+ nBits = bitsFromNat n
88+ mBits : Bits64
89+ mBits = bitsFromNat m
90+ cBits : Bits64
91+ cBits = bitsFromNat count
66− prim__appendBufferNative input ( toIntegerNat count ) . realBuffer
92+ app = prim__appendBufferNative input nBits cBits mBits
67−
68
93
69public
94public
70appendBufferLE : Buffer n ->
95appendBufferLE : Buffer n ->
@@ -80,173 +105,207 @@ appendBufferBE : Buffer n ->
80 Buffer ( n + m * count )
105 Buffer ( n + m * count )
81appendBufferBE = appendBufferNative
106appendBufferBE = appendBufferNative
82
107
108+
83−peekBits : ( prim__UnsafeBuffer -> Integer -> a ) ->
109+peekBits : ( prim__UnsafeBuffer -> Bits64 -> a ) ->
84− Buffer ( n + m ) ->
110+ Buffer ( m + n ) ->
85− ( offset : Fin n ) ->
111+ ( offset : Fin ( n + 1 ) ) ->
86 a
112 a
87−peekBits prim ( MkBuffer real ) = prim real . finToInteger
113+peekBits prim ( MkBuffer real ) = prim real . bitsFromFin
88
114
89appendBits : ( prim__UnsafeBuffer ->
115appendBits : ( prim__UnsafeBuffer ->
90− Integer ->
116+ Bits64 ->
117+ Bits64 ->
91 a ->
118 a ->
92 prim__UnsafeBuffer ) ->
119 prim__UnsafeBuffer ) ->
93 Buffer n ->
120 Buffer n ->
94 ( count : Nat) ->
121 ( count : Nat) ->
95 a ->
122 a ->
96 Buffer ( n + count * size )
123 Buffer ( n + count * size )
97−appendBits prim ( MkBuffer real ) count =
124+appendBits { n } prim ( MkBuffer real ) count =
98− MkBuffer . prim real ( toIntegerNat count )
125+ MkBuffer . prim real ( bitsFromNat n ) ( bitsFromNat count )
99
126
100
127
101-- Read a Bits8 from a Buffer starting at offset
128-- Read a Bits8 from a Buffer starting at offset
129+%assert_total
102public
130public
103−peekBits8Native : Buffer ( n + 1 ) -> ( offset : Fin n ) -> Bits8
131+peekBits8Native : Buffer ( 1 + n ) ->
132+ ( offset : Fin ( n + 1 ) ) ->
133+ Bits8
104−peekBits8Native = peekBits prim__peekBits8Native
134+peekBits8Native = peekBits { m = 1 } prim__peekB8Native
105
135
136+%assert_total
106public
137public
107−peekBits8LE : Buffer ( n + 1 ) -> ( offset : Fin n ) -> Bits8
138+peekBits8LE : Buffer ( 1 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits8
108−peekBits8LE = peekBits8Native
139+peekBits8LE = peekBits { m = 1 } prim__peekB8LE
109
140
141+%assert_total
110public
142public
111−peekBits8BE : Buffer ( n + 1 ) -> ( offset : Fin n ) -> Bits8
143+peekBits8BE : Buffer ( 1 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits8
112−peekBits8BE = peekBits8Native
144+peekBits8BE = peekBits { m = 1 } prim__peekB8BE
113
145
114-- Append count repetitions of a Bits8 to a Buffer
146-- Append count repetitions of a Bits8 to a Buffer
147+%assert_total
115public
148public
116appendBits8Native : Buffer n ->
149appendBits8Native : Buffer n ->
117 ( count : Nat ) ->
150 ( count : Nat ) ->
118 Bits8 ->
151 Bits8 ->
119− Buffer ( n + count )
152+ Buffer ( n + count * 1 )
120−appendBits8Native = appendBits prim__appendBits8Native
153+appendBits8Native = appendBits prim__appendB8Native
121
154
155+%assert_total
122public
156public
123appendBits8LE : Buffer n ->
157appendBits8LE : Buffer n ->
124 ( count : Nat ) ->
158 ( count : Nat ) ->
125 Bits8 ->
159 Bits8 ->
126− Buffer ( n + count )
160+ Buffer ( n + count * 1 )
127−appendBits8LE = appendBits8Native
161+appendBits8LE = appendBits prim__appendB8LE
128
162
163+%assert_total
129public
164public
130appendBits8BE : Buffer n ->
165appendBits8BE : Buffer n ->
131 ( count : Nat ) ->
166 ( count : Nat ) ->
132 Bits8 ->
167 Bits8 ->
133− Buffer ( n + count )
168+ Buffer ( n + count * 1 )
134−appendBits8BE = appendBits8Native
169+appendBits8BE = appendBits prim__appendB8BE
135
170
136
171
137-- Read a Bits16 in native byte order from a Buffer starting at offset
172-- Read a Bits16 in native byte order from a Buffer starting at offset
173+%assert_total
138public
174public
139−peekBits16Native : Buffer ( n + 2 ) -> ( offset : Fin n ) -> Bits8
175+peekBits16Native : Buffer ( 2 + n ) ->
176+ ( offset : Fin ( n + 1 ) ) ->
177+ Bits16
140−peekBits16Native = peekBits prim__peekBits16Native
178+peekBits16Native = peekBits { m = 2 } prim__peekB16Native
141
179
142-- Read a little-endian Bits16 from a Buffer starting at offset
180-- Read a little-endian Bits16 from a Buffer starting at offset
181+%assert_total
143public
182public
144−peekBits16LE : Buffer ( n + 2 ) -> ( offset : Fin n ) -> Bits8
183+peekBits16LE : Buffer ( 2 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits16
145−peekBits16LE = peekBits prim__peekBits16LE
184+peekBits16LE = peekBits { m = 2 } prim__peekB16LE
146
185
147-- Read a big-endian Bits16 from a Buffer starting at offset
186-- Read a big-endian Bits16 from a Buffer starting at offset
187+%assert_total
148public
188public
149−peekBits16BE : Buffer ( n + 2 ) -> ( offset : Fin n ) -> Bits8
189+peekBits16BE : Buffer ( 2 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits16
150−peekBits16BE = peekBits prim__peekBits16LE
190+peekBits16BE = peekBits { m = 2 } prim__peekB16BE
151
191
152-- Append count repetitions of a Bits16 in native byte order to a Buffer
192-- Append count repetitions of a Bits16 in native byte order to a Buffer
193+%assert_total
153public
194public
154appendBits16Native : Buffer n ->
195appendBits16Native : Buffer n ->
155 ( count : Nat ) ->
196 ( count : Nat ) ->
156 Bits16 ->
197 Bits16 ->
157− Buffer ( n + 2 * count )
198+ Buffer ( n + count * 2 )
158−appendBits16Native = appendBits prim__appendBits16Native
199+appendBits16Native = appendBits prim__appendB16Native
159
200
160-- Append count repetitions of a little-endian Bits16 to a Buffer
201-- Append count repetitions of a little-endian Bits16 to a Buffer
202+%assert_total
161public
203public
162appendBits16LE : Buffer n ->
204appendBits16LE : Buffer n ->
163 ( count : Nat ) ->
205 ( count : Nat ) ->
164 Bits16 ->
206 Bits16 ->
165− Buffer ( n + 2 * count )
207+ Buffer ( n + count * 2 )
166−appendBits16LE = appendBits prim__appendBits16LE
208+appendBits16LE = appendBits prim__appendB16LE
167
209
168-- Append count repetitions of a big-endian Bits16 to a Buffer
210-- Append count repetitions of a big-endian Bits16 to a Buffer
211+%assert_total
169public
212public
170appendBits16BE : Buffer n ->
213appendBits16BE : Buffer n ->
171 ( count : Nat ) ->
214 ( count : Nat ) ->
172 Bits16 ->
215 Bits16 ->
173− Buffer ( n + 2 * count )
216+ Buffer ( n + count * 2 )
174−appendBits16BE = appendBits prim__appendBits16BE
217+appendBits16BE = appendBits prim__appendB16BE
175
218
176-- Read a Bits32 in native byte order from a Buffer starting at offset
219-- Read a Bits32 in native byte order from a Buffer starting at offset
220+%assert_total
177public
221public
178−peekBits32Native : Buffer ( n + 4 ) -> ( offset : Fin n ) -> Bits8
222+peekBits32Native : Buffer ( 4 + n ) ->
223+ ( offset : Fin ( n + 1 ) ) ->
224+ Bits32
179−peekBits32Native = peekBits prim__peekBits32Native
225+peekBits32Native = peekBits { m = 4 } prim__peekB32Native
180
226
181-- Read a little-endian Bits32 from a Buffer starting at offset
227-- Read a little-endian Bits32 from a Buffer starting at offset
228+%assert_total
182public
229public
183−peekBits32LE : Buffer ( n + 4 ) -> ( offset : Fin n ) -> Bits8
230+peekBits32LE : Buffer ( 4 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits32
184−peekBits32LE = peekBits prim__peekBits32LE
231+peekBits32LE = peekBits { m = 4 } prim__peekB32LE
185
232
186-- Read a big-endian Bits32 from a Buffer starting at offset
233-- Read a big-endian Bits32 from a Buffer starting at offset
234+%assert_total
187public
235public
188−peekBits32BE : Buffer ( n + 4 ) -> ( offset : Fin n ) -> Bits8
236+peekBits32BE : Buffer ( 4 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits32
189−peekBits32BE = peekBits prim__peekBits32LE
237+peekBits32BE = peekBits { m = 4 } prim__peekB32BE
190
238
191-- Append count repetitions of a Bits32 in native byte order to a Buffer
239-- Append count repetitions of a Bits32 in native byte order to a Buffer
240+%assert_total
192public
241public
193appendBits32Native : Buffer n ->
242appendBits32Native : Buffer n ->
194 ( count : Nat ) ->
243 ( count : Nat ) ->
195 Bits32 ->
244 Bits32 ->
196− Buffer ( n + 4 * count )
245+ Buffer ( n + count * 4 )
197−appendBits32Native = appendBits prim__appendBits32Native
246+appendBits32Native = appendBits prim__appendB32Native
198
247
199-- Append count repetitions of a little-endian Bits32 to a Buffer
248-- Append count repetitions of a little-endian Bits32 to a Buffer
249+%assert_total
200public
250public
201appendBits32LE : Buffer n ->
251appendBits32LE : Buffer n ->
202 ( count : Nat ) ->
252 ( count : Nat ) ->
203 Bits32 ->
253 Bits32 ->
204− Buffer ( n + 4 * count )
254+ Buffer ( n + count * 4 )
205−appendBits32LE = appendBits prim__appendBits32LE
255+appendBits32LE = appendBits prim__appendB32LE
206
256
207-- Append count repetitions of a big-endian Bits32 to a Buffer
257-- Append count repetitions of a big-endian Bits32 to a Buffer
258+%assert_total
208public
259public
209appendBits32BE : Buffer n ->
260appendBits32BE : Buffer n ->
210 ( count : Nat ) ->
261 ( count : Nat ) ->
211 Bits32 ->
262 Bits32 ->
212− Buffer ( n + 4 * count )
263+ Buffer ( n + count * 4 )
213−appendBits32BE = appendBits prim__appendBits32BE
264+appendBits32BE = appendBits prim__appendB32BE
214
265
215-- Read a Bits64 in native byte order from a Buffer starting at offset
266-- Read a Bits64 in native byte order from a Buffer starting at offset
267+%assert_total
216public
268public
217−peekBits64Native : Buffer ( n + 8 ) -> ( offset : Fin n ) -> Bits8
269+peekBits64Native : Buffer ( 8 + n ) ->
270+ ( offset : Fin ( n + 1 ) ) ->
271+ Bits64
218−peekBits64Native = peekBits prim__peekBits64Native
272+peekBits64Native = peekBits { m = 8 } prim__peekB64Native
219
273
220-- Read a little-endian Bits64 from a Buffer starting at offset
274-- Read a little-endian Bits64 from a Buffer starting at offset
275+%assert_total
221public
276public
222−peekBits64LE : Buffer ( n + 8 ) -> ( offset : Fin n ) -> Bits8
277+peekBits64LE : Buffer ( 8 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits64
223−peekBits64LE = peekBits prim__peekBits64LE
278+peekBits64LE = peekBits { m = 8 } prim__peekB64LE
224
279
225-- Read a big-endian Bits64 from a Buffer starting at offset
280-- Read a big-endian Bits64 from a Buffer starting at offset
281+%assert_total
226public
282public
227−peekBits64BE : Buffer ( n + 8 ) -> ( offset : Fin n ) -> Bits8
283+peekBits64BE : Buffer ( 8 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits64
228−peekBits64BE = peekBits prim__peekBits64LE
284+peekBits64BE = peekBits { m = 8 } prim__peekB64BE
229
285
230-- Append count repetitions of a Bits64 in native byte order to a Buffer
286-- Append count repetitions of a Bits64 in native byte order to a Buffer
287+%assert_total
231public
288public
232appendBits64Native : Buffer n ->
289appendBits64Native : Buffer n ->
233 ( count : Nat ) ->
290 ( count : Nat ) ->
234 Bits64 ->
291 Bits64 ->
235− Buffer ( n + 8 * count )
292+ Buffer ( n + count * 8 )
236−appendBits64Native = appendBits prim__appendBits64Native
293+appendBits64Native = appendBits prim__appendB64Native
237
294
238-- Append count repetitions of a little-endian Bits64 to a Buffer
295-- Append count repetitions of a little-endian Bits64 to a Buffer
296+%assert_total
239public
297public
240appendBits64LE : Buffer n ->
298appendBits64LE : Buffer n ->
241 ( count : Nat ) ->
299 ( count : Nat ) ->
242 Bits64 ->
300 Bits64 ->
243− Buffer ( n + 8 * count )
301+ Buffer ( n + count * 8 )
244−appendBits64LE = appendBits prim__appendBits64LE
302+appendBits64LE = appendBits prim__appendB64LE
245
303
246-- Append count repetitions of a big-endian Bits64 to a Buffer
304-- Append count repetitions of a big-endian Bits64 to a Buffer
305+%assert_total
247public
306public
248appendBits64BE : Buffer n ->
307appendBits64BE : Buffer n ->
249 ( count : Nat ) ->
308 ( count : Nat ) ->
250 Bits64 ->
309 Bits64 ->
251− Buffer ( n + 8 * count )
310+ Buffer ( n + count * 8 )
252−appendBits64BE = appendBits prim__appendBits64BE
311+appendBits64BE = appendBits prim__appendB64BE
src/IRTS/Lang.hs+10
@@ -5,6 +5,8 @@ import Idris.Core.TT
5import Data.List
5import Data.List
6import Debug.Trace
6import Debug.Trace
7
7
8+data Endianness = Native | BE | LE deriving (Show, Eq)
9+
8data LVar = Loc Int | Glob Name
10data LVar = Loc Int | Glob Name
9 deriving (Show, Eq)
11 deriving (Show, Eq)
10
12
@@ -50,6 +52,14 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy
50 | LStrHead | LStrTail | LStrCons | LStrIndex | LStrRev
52 | LStrHead | LStrTail | LStrCons | LStrIndex | LStrRev
51 | LStdIn | LStdOut | LStdErr
53 | LStdIn | LStdOut | LStdErr
52
54
55+ -- Buffers
56+ | LAllocate
57+ | LCopy
58+ | LAppendBufferNative
59+ | LPeekBufferNative
60+ | LAppend IntTy Endianness
61+ | LPeek IntTy Endianness
62+
53 | LFork
63 | LFork
54 | LPar -- evaluate argument anywhere, possibly on another
64 | LPar -- evaluate argument anywhere, possibly on another
55 -- core or another machine. 'id' is a valid implementation
65 -- core or another machine. 'id' is a valid implementation
src/Idris/Core/TT.hs+3−1
@@ -468,7 +468,7 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String
468 | B8V (Vector Word8) | B16V (Vector Word16)
468 | B8V (Vector Word8) | B16V (Vector Word16)
469 | B32V (Vector Word32) | B64V (Vector Word64)
469 | B32V (Vector Word32) | B64V (Vector Word64)
470 | AType ArithTy | StrType
470 | AType ArithTy | StrType
471− | PtrType | VoidType | Forgot
471+ | PtrType | BufferType | VoidType | Forgot
472 deriving (Eq, Ord)
472 deriving (Eq, Ord)
473{-!
473{-!
474deriving instance Binary Const
474deriving instance Binary Const
@@ -486,6 +486,7 @@ instance Pretty Const OutputAnnotation where
486 pretty (Str s) = text s
486 pretty (Str s) = text s
487 pretty (AType a) = pretty a
487 pretty (AType a) = pretty a
488 pretty StrType = text "String"
488 pretty StrType = text "String"
489+ pretty BufferType = text "prim__UnsafeBuffer"
489 pretty PtrType = text "Ptr"
490 pretty PtrType = text "Ptr"
490 pretty VoidType = text "Void"
491 pretty VoidType = text "Void"
491 pretty Forgot = text "Forgot"
492 pretty Forgot = text "Forgot"
@@ -1031,6 +1032,7 @@ instance Show Const where
1031 show (AType (ATInt (ITFixed it))) = itBitsName it
1032 show (AType (ATInt (ITFixed it))) = itBitsName it
1032 show (AType (ATInt (ITVec it c))) = itBitsName it ++ "x" ++ show c
1033 show (AType (ATInt (ITVec it c))) = itBitsName it ++ "x" ++ show c
1033 show StrType = "String"
1034 show StrType = "String"
1035+ show BufferType = "prim__UnsafeBuffer"
1034 show PtrType = "Ptr"
1036 show PtrType = "Ptr"
1035 show VoidType = "Void"
1037 show VoidType = "Void"
1036
1038
src/Idris/IBC.hs+2
@@ -606,6 +606,7 @@ instance Binary Const where
606 B16V x1 -> putWord8 22 >> put x1
606 B16V x1 -> putWord8 22 >> put x1
607 B32V x1 -> putWord8 23 >> put x1
607 B32V x1 -> putWord8 23 >> put x1
608 B64V x1 -> putWord8 24 >> put x1
608 B64V x1 -> putWord8 24 >> put x1
609+ BufferType -> putWord8 25
609 get
610 get
610 = do i <- getWord8
611 = do i <- getWord8
611 case i of
612 case i of
@@ -646,6 +647,7 @@ instance Binary Const where
646 22 -> fmap B16V get
647 22 -> fmap B16V get
647 23 -> fmap B32V get
648 23 -> fmap B32V get
648 24 -> fmap B64V get
649 24 -> fmap B64V get
650+ 25 -> return BufferType
649
651
650 _ -> error "Corrupted binary data for Const"
652 _ -> error "Corrupted binary data for Const"
651
653
src/Idris/ParseExpr.hs+8−6
@@ -992,6 +992,7 @@ Constant ::=
992 | 'Float'
992 | 'Float'
993 | 'String'
993 | 'String'
994 | 'Ptr'
994 | 'Ptr'
995+ | 'prim__UnsafeBuffer'
995 | 'Bits8'
996 | 'Bits8'
996 | 'Bits16'
997 | 'Bits16'
997 | 'Bits32'
998 | 'Bits32'
@@ -1009,12 +1010,13 @@ Constant ::=
1009@
1010@
1010-}
1011-}
1011constant :: IdrisParser Idris.Core.TT.Const
1012constant :: IdrisParser Idris.Core.TT.Const
1012−constant = do reserved "Integer";return (AType (ATInt ITBig))
1013+constant = do reserved "Integer"; return (AType (ATInt ITBig))
1013− <|> do reserved "Int"; return (AType (ATInt ITNative))
1014+ <|> do reserved "Int"; return (AType (ATInt ITNative))
1014− <|> do reserved "Char"; return (AType (ATInt ITChar))
1015+ <|> do reserved "Char"; return (AType (ATInt ITChar))
1015− <|> do reserved "Float"; return (AType ATFloat)
1016+ <|> do reserved "Float"; return (AType ATFloat)
1016− <|> do reserved "String"; return StrType
1017+ <|> do reserved "String"; return StrType
1017− <|> do reserved "Ptr"; return PtrType
1018+ <|> do reserved "Ptr"; return PtrType
1019+ <|> do reserved "prim__UnsafeBuffer"; return BufferType
1018 <|> do reserved "Bits8"; return (AType (ATInt (ITFixed IT8)))
1020 <|> do reserved "Bits8"; return (AType (ATInt (ITFixed IT8)))
1019 <|> do reserved "Bits16"; return (AType (ATInt (ITFixed IT16)))
1021 <|> do reserved "Bits16"; return (AType (ATInt (ITFixed IT16)))
1020 <|> do reserved "Bits32"; return (AType (ATInt (ITFixed IT32)))
1022 <|> do reserved "Bits32"; return (AType (ATInt (ITFixed IT32)))
src/Idris/Primitives.hs+31−2
@@ -171,9 +171,20 @@ primitives =
171 Prim (sUN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)
171 Prim (sUN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)
172 (0, LStdIn) partial,
172 (0, LStdIn) partial,
173 Prim (sUN "prim__null") (ty [] PtrType) 0 (p_cantreduce)
173 Prim (sUN "prim__null") (ty [] PtrType) 0 (p_cantreduce)
174− (0, LNullPtr) total
174+ (0, LNullPtr) total,
175+
176+ -- Buffers
177+ Prim (sUN "prim__allocate") (ty [AType (ATInt (ITFixed IT64))] BufferType) 1 (p_cantreduce)
178+ (1, LAllocate) total,
179+ Prim (sUN "prim__copy") (ty [AType (ATInt (ITFixed IT64)), BufferType] BufferType) 2 (p_cantreduce)
180+ (2, LCopy) partial,
181+ Prim (sUN "prim__peekBufferNative") (ty [BufferType, AType (ATInt (ITFixed IT64))] BufferType) 2 (p_cantreduce)
182+ (2, LPeekBufferNative) partial,
183+ Prim (sUN "prim__appendBufferNative") (ty [BufferType, AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), BufferType] BufferType) 5 (p_cantreduce)
184+ (5, LAppendBufferNative) partial
175 ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative, ITChar]
185 ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative, ITChar]
176 ++ concatMap vecOps vecTypes
186 ++ concatMap vecOps vecTypes
187+ ++ concatMap fixedOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64] -- ITNative, ITChar, ATFloat ] ++ vecTypes
177 ++ vecBitcasts vecTypes
188 ++ vecBitcasts vecTypes
178
189
179vecTypes :: [IntTy]
190vecTypes :: [IntTy]
@@ -267,6 +278,25 @@ vecBitcasts :: [IntTy] -> [Prim]
267vecBitcasts tys = [bitcastPrim from to bitcastVec (LBitCast from to)
278vecBitcasts tys = [bitcastPrim from to bitcastVec (LBitCast from to)
268 | from <- map ATInt vecTypes, to <- map ATInt vecTypes, from /= to]
279 | from <- map ATInt vecTypes, to <- map ATInt vecTypes, from /= to]
269
280
281+fixedOps :: IntTy -> [Prim]
282+fixedOps ity@(ITFixed _) =
283+ map appendFun endiannesses ++
284+ map peekFun endiannesses
285+ where
286+ endiannesses = [ Native, LE, BE ]
287+ enName LE = "LE"
288+ enName BE = "BE"
289+ enName Native = "Native"
290+ tyName = intTyName ity
291+ b64 = AType (ATInt (ITFixed IT64))
292+ thisTy = AType $ ATInt ity
293+ appendFun en = Prim (sUN $ "prim__append" ++ tyName ++ enName en)
294+ (ty [BufferType, b64, b64, thisTy] BufferType)
295+ 4 (p_cantreduce) (4, LAppend ity en) partial
296+ peekFun en = Prim (sUN $ "prim__peek" ++ tyName ++ enName en)
297+ (ty [BufferType, b64] thisTy)
298+ 2 (p_cantreduce) (2, LPeek ity en) partial
299+
270mapHalf :: (V.Unbox a, V.Unbox b) => ((a, a) -> b) -> Vector a -> Vector b
300mapHalf :: (V.Unbox a, V.Unbox b) => ((a, a) -> b) -> Vector a -> Vector b
271mapHalf f xs = V.generate (V.length xs `div` 2) (\i -> f (xs V.! (i*2), xs V.! (i*2+1)))
301mapHalf f xs = V.generate (V.length xs `div` 2) (\i -> f (xs V.! (i*2), xs V.! (i*2+1)))
272
302
@@ -678,4 +708,3 @@ p_strRev _ = Nothing
678p_cantreduce :: a -> Maybe b
708p_cantreduce :: a -> Maybe b
679p_cantreduce _ = Nothing
709p_cantreduce _ = Nothing
680
710
681−
test/buffer001/buffer001.idr+5−5
@@ -3,7 +3,7 @@ module Main
3import Data.Buffer
3import Data.Buffer
4
4
5em : Buffer 0
5em : Buffer 0
6−em = allocate 32
6+em = allocate 4
7
7
8one : Bits32
8one : Bits32
9one = 1
9one = 1
@@ -11,19 +11,19 @@ one = 1
11two : Bits8
11two : Bits8
12two = 2
12two = 2
13
13
14−firstHalf : Buffer 32
14+firstHalf : Buffer 4
15firstHalf = appendBits32LE em 1 one
15firstHalf = appendBits32LE em 1 one
16
16
17−full : Buffer 64
17+full : Buffer 8
18full = appendBits8LE firstHalf 4 two
18full = appendBits8LE firstHalf 4 two
19
19
20firstByte : Bits8
20firstByte : Bits8
21firstByte = peekBits8LE full 0
21firstByte = peekBits8LE full 0
22
22
23−firstHalfView : Buffer 32
23+firstHalfView : Buffer 4
24firstHalfView = peekBufferLE full 0
24firstHalfView = peekBufferLE full 0
25
25
26−firstHalfCopy : Buffer 32
26+firstHalfCopy : Buffer 4
27firstHalfCopy = copy firstHalfView
27firstHalfCopy = copy firstHalfView
28
28
29oneFromFirstHalf : Bits32
29oneFromFirstHalf : Bits32