@@ -5,7 +5,7 @@ module Data.Buffer
55-- !!! TODO: Open issues:
66-- 1. It may be theoretically nice to represent Buffer size as
77-- 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
99-- equivalent of C's size_t (ideally unboxed)
1010-- 3. If we had access to host system information, we could reduce
1111-- the needed primitives by implementing the LE/BE variants on
@@ -16,55 +16,80 @@ module Data.Buffer
1616-- 5. Would be nice to be able to peek/append the vector types, but
1717-- for now I'm only touching the C backend which AFAICT doesn't
1818-- 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
2020-- 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
2222
2323-- A contiguous chunk of n bytes
2424abstract
2525record Buffer : Nat -> Type where
2626 MkBuffer : ( realBuffer : prim__UnsafeBuffer ) -> Buffer n
2727
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+
2836-- Allocate an empty Buffer. The size hint can be used to avoid
2937-- 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.
3140public
3241allocate : ( hint : Nat ) -> Buffer 0
33−allocate = MkBuffer . prim__allocate . toIntegerNat
42+allocate = MkBuffer . prim__allocate . bitsFromNat
3443
3544-- Copy a buffer. Since multiple buffers can reference the same
3645-- underlying chunk of memory, it may happen that a reference to
3746-- a relatively small bit of data might be preventing the runtime
3847-- from freeing a much larger chunk. copy allows giving up references
3948-- to the larger chunk without losing the smaller one.
49+%assert_total
4050public
4151copy : Buffer n -> Buffer n
42−copy = MkBuffer . prim__copy ( toIntegerNat n ) . realBuffer
52+copy { n } = MkBuffer . prim__copy ( bitsFromNat n ) . realBuffer
4353
4454-- Read a Buffer from another Buffer starting at offset
4555-- (i.e. create a view of a subset of the Buffer)
56+%assert_total
4657public
47−peekBufferNative : Buffer ( n + m ) -> ( offset : Fin n ) -> Buffer m
58+peekBufferNative : Buffer ( m + n ) ->
59+ ( offset : Fin ( n + 1 ) ) ->
60+ Buffer m
4861peekBufferNative ( MkBuffer real ) =
49− MkBuffer . prim__peekBufferNative real . finToInteger
62+ MkBuffer . prim__peekBufferNative real . bitsFromFin
5063
5164public
52−peekBufferLE : Buffer ( n + m ) -> ( offset : Fin n ) -> Buffer m
65+peekBufferLE : Buffer ( m + n ) ->
66+ ( offset : Fin ( n + 1 ) ) ->
67+ Buffer m
5368peekBufferLE = peekBufferNative
5469
5570public
56−peekBufferBE : Buffer ( n + m ) -> ( offset : Fin n ) -> Buffer m
71+peekBufferBE : Buffer ( m + n ) ->
72+ ( offset : Fin ( n + 1 ) ) ->
73+ Buffer m
5774peekBufferBE = peekBufferNative
5875
5976-- Append count repetitions of a Buffer to another Buffer
77+%assert_total
6078public
6179appendBufferNative : Buffer n ->
6280 ( count : Nat ) ->
6381 Buffer m ->
6482 Buffer ( n + m * count )
65−appendBufferNative ( MkBuffer input ) count = MkBuffer .
66− prim__appendBufferNative input ( toIntegerNat count ) . realBuffer
67−
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
92+ app = prim__appendBufferNative input nBits cBits mBits
6893
6994public
7095appendBufferLE : Buffer n ->
@@ -80,173 +105,207 @@ appendBufferBE : Buffer n ->
80105 Buffer ( n + m * count )
81106appendBufferBE = appendBufferNative
82107
83−peekBits : ( prim__UnsafeBuffer -> Integer -> a ) ->
84− Buffer ( n + m ) ->
85− ( offset : Fin n ) ->
108+
109+peekBits : ( prim__UnsafeBuffer -> Bits64 -> a ) ->
110+ Buffer ( m + n ) ->
111+ ( offset : Fin ( n + 1 ) ) ->
86112 a
87−peekBits prim ( MkBuffer real ) = prim real . finToInteger
113+peekBits prim ( MkBuffer real ) = prim real . bitsFromFin
88114
89115appendBits : ( prim__UnsafeBuffer ->
90− Integer ->
116+ Bits64 ->
117+ Bits64 ->
91118 a ->
92119 prim__UnsafeBuffer ) ->
93120 Buffer n ->
94121 ( count : Nat) ->
95122 a ->
96123 Buffer ( n + count * size )
97−appendBits prim ( MkBuffer real ) count =
98− MkBuffer . prim real ( toIntegerNat count )
124+appendBits { n } prim ( MkBuffer real ) count =
125+ MkBuffer . prim real ( bitsFromNat n ) ( bitsFromNat count )
99126
100127
101128-- Read a Bits8 from a Buffer starting at offset
129+%assert_total
102130public
103−peekBits8Native : Buffer ( n + 1 ) -> ( offset : Fin n ) -> Bits8
104−peekBits8Native = peekBits prim__peekBits8Native
131+peekBits8Native : Buffer ( 1 + n ) ->
132+ ( offset : Fin ( n + 1 ) ) ->
133+ Bits8
134+peekBits8Native = peekBits { m = 1 } prim__peekB8Native
105135
136+%assert_total
106137public
107−peekBits8LE : Buffer ( n + 1 ) -> ( offset : Fin n ) -> Bits8
108−peekBits8LE = peekBits8Native
138+peekBits8LE : Buffer ( 1 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits8
139+peekBits8LE = peekBits { m = 1 } prim__peekB8LE
109140
141+%assert_total
110142public
111−peekBits8BE : Buffer ( n + 1 ) -> ( offset : Fin n ) -> Bits8
112−peekBits8BE = peekBits8Native
143+peekBits8BE : Buffer ( 1 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits8
144+peekBits8BE = peekBits { m = 1 } prim__peekB8BE
113145
114146-- Append count repetitions of a Bits8 to a Buffer
147+%assert_total
115148public
116149appendBits8Native : Buffer n ->
117150 ( count : Nat ) ->
118151 Bits8 ->
119− Buffer ( n + count )
120−appendBits8Native = appendBits prim__appendBits8Native
152+ Buffer ( n + count * 1 )
153+appendBits8Native = appendBits prim__appendB8Native
121154
155+%assert_total
122156public
123157appendBits8LE : Buffer n ->
124158 ( count : Nat ) ->
125159 Bits8 ->
126− Buffer ( n + count )
127−appendBits8LE = appendBits8Native
160+ Buffer ( n + count * 1 )
161+appendBits8LE = appendBits prim__appendB8LE
128162
163+%assert_total
129164public
130165appendBits8BE : Buffer n ->
131166 ( count : Nat ) ->
132167 Bits8 ->
133− Buffer ( n + count )
134−appendBits8BE = appendBits8Native
168+ Buffer ( n + count * 1 )
169+appendBits8BE = appendBits prim__appendB8BE
135170
136171
137172-- Read a Bits16 in native byte order from a Buffer starting at offset
173+%assert_total
138174public
139−peekBits16Native : Buffer ( n + 2 ) -> ( offset : Fin n ) -> Bits8
140−peekBits16Native = peekBits prim__peekBits16Native
175+peekBits16Native : Buffer ( 2 + n ) ->
176+ ( offset : Fin ( n + 1 ) ) ->
177+ Bits16
178+peekBits16Native = peekBits { m = 2 } prim__peekB16Native
141179
142180-- Read a little-endian Bits16 from a Buffer starting at offset
181+%assert_total
143182public
144−peekBits16LE : Buffer ( n + 2 ) -> ( offset : Fin n ) -> Bits8
145−peekBits16LE = peekBits prim__peekBits16LE
183+peekBits16LE : Buffer ( 2 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits16
184+peekBits16LE = peekBits { m = 2 } prim__peekB16LE
146185
147186-- Read a big-endian Bits16 from a Buffer starting at offset
187+%assert_total
148188public
149−peekBits16BE : Buffer ( n + 2 ) -> ( offset : Fin n ) -> Bits8
150−peekBits16BE = peekBits prim__peekBits16LE
189+peekBits16BE : Buffer ( 2 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits16
190+peekBits16BE = peekBits { m = 2 } prim__peekB16BE
151191
152192-- Append count repetitions of a Bits16 in native byte order to a Buffer
193+%assert_total
153194public
154195appendBits16Native : Buffer n ->
155196 ( count : Nat ) ->
156197 Bits16 ->
157− Buffer ( n + 2 * count )
158−appendBits16Native = appendBits prim__appendBits16Native
198+ Buffer ( n + count * 2 )
199+appendBits16Native = appendBits prim__appendB16Native
159200
160201-- Append count repetitions of a little-endian Bits16 to a Buffer
202+%assert_total
161203public
162204appendBits16LE : Buffer n ->
163205 ( count : Nat ) ->
164206 Bits16 ->
165− Buffer ( n + 2 * count )
166−appendBits16LE = appendBits prim__appendBits16LE
207+ Buffer ( n + count * 2 )
208+appendBits16LE = appendBits prim__appendB16LE
167209
168210-- Append count repetitions of a big-endian Bits16 to a Buffer
211+%assert_total
169212public
170213appendBits16BE : Buffer n ->
171214 ( count : Nat ) ->
172215 Bits16 ->
173− Buffer ( n + 2 * count )
174−appendBits16BE = appendBits prim__appendBits16BE
216+ Buffer ( n + count * 2 )
217+appendBits16BE = appendBits prim__appendB16BE
175218
176219-- Read a Bits32 in native byte order from a Buffer starting at offset
220+%assert_total
177221public
178−peekBits32Native : Buffer ( n + 4 ) -> ( offset : Fin n ) -> Bits8
179−peekBits32Native = peekBits prim__peekBits32Native
222+peekBits32Native : Buffer ( 4 + n ) ->
223+ ( offset : Fin ( n + 1 ) ) ->
224+ Bits32
225+peekBits32Native = peekBits { m = 4 } prim__peekB32Native
180226
181227-- Read a little-endian Bits32 from a Buffer starting at offset
228+%assert_total
182229public
183−peekBits32LE : Buffer ( n + 4 ) -> ( offset : Fin n ) -> Bits8
184−peekBits32LE = peekBits prim__peekBits32LE
230+peekBits32LE : Buffer ( 4 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits32
231+peekBits32LE = peekBits { m = 4 } prim__peekB32LE
185232
186233-- Read a big-endian Bits32 from a Buffer starting at offset
234+%assert_total
187235public
188−peekBits32BE : Buffer ( n + 4 ) -> ( offset : Fin n ) -> Bits8
189−peekBits32BE = peekBits prim__peekBits32LE
236+peekBits32BE : Buffer ( 4 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits32
237+peekBits32BE = peekBits { m = 4 } prim__peekB32BE
190238
191239-- Append count repetitions of a Bits32 in native byte order to a Buffer
240+%assert_total
192241public
193242appendBits32Native : Buffer n ->
194243 ( count : Nat ) ->
195244 Bits32 ->
196− Buffer ( n + 4 * count )
197−appendBits32Native = appendBits prim__appendBits32Native
245+ Buffer ( n + count * 4 )
246+appendBits32Native = appendBits prim__appendB32Native
198247
199248-- Append count repetitions of a little-endian Bits32 to a Buffer
249+%assert_total
200250public
201251appendBits32LE : Buffer n ->
202252 ( count : Nat ) ->
203253 Bits32 ->
204− Buffer ( n + 4 * count )
205−appendBits32LE = appendBits prim__appendBits32LE
254+ Buffer ( n + count * 4 )
255+appendBits32LE = appendBits prim__appendB32LE
206256
207257-- Append count repetitions of a big-endian Bits32 to a Buffer
258+%assert_total
208259public
209260appendBits32BE : Buffer n ->
210261 ( count : Nat ) ->
211262 Bits32 ->
212− Buffer ( n + 4 * count )
213−appendBits32BE = appendBits prim__appendBits32BE
263+ Buffer ( n + count * 4 )
264+appendBits32BE = appendBits prim__appendB32BE
214265
215266-- Read a Bits64 in native byte order from a Buffer starting at offset
267+%assert_total
216268public
217−peekBits64Native : Buffer ( n + 8 ) -> ( offset : Fin n ) -> Bits8
218−peekBits64Native = peekBits prim__peekBits64Native
269+peekBits64Native : Buffer ( 8 + n ) ->
270+ ( offset : Fin ( n + 1 ) ) ->
271+ Bits64
272+peekBits64Native = peekBits { m = 8 } prim__peekB64Native
219273
220274-- Read a little-endian Bits64 from a Buffer starting at offset
275+%assert_total
221276public
222−peekBits64LE : Buffer ( n + 8 ) -> ( offset : Fin n ) -> Bits8
223−peekBits64LE = peekBits prim__peekBits64LE
277+peekBits64LE : Buffer ( 8 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits64
278+peekBits64LE = peekBits { m = 8 } prim__peekB64LE
224279
225280-- Read a big-endian Bits64 from a Buffer starting at offset
281+%assert_total
226282public
227−peekBits64BE : Buffer ( n + 8 ) -> ( offset : Fin n ) -> Bits8
228−peekBits64BE = peekBits prim__peekBits64LE
283+peekBits64BE : Buffer ( 8 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits64
284+peekBits64BE = peekBits { m = 8 } prim__peekB64BE
229285
230286-- Append count repetitions of a Bits64 in native byte order to a Buffer
287+%assert_total
231288public
232289appendBits64Native : Buffer n ->
233290 ( count : Nat ) ->
234291 Bits64 ->
235− Buffer ( n + 8 * count )
236−appendBits64Native = appendBits prim__appendBits64Native
292+ Buffer ( n + count * 8 )
293+appendBits64Native = appendBits prim__appendB64Native
237294
238295-- Append count repetitions of a little-endian Bits64 to a Buffer
296+%assert_total
239297public
240298appendBits64LE : Buffer n ->
241299 ( count : Nat ) ->
242300 Bits64 ->
243− Buffer ( n + 8 * count )
244−appendBits64LE = appendBits prim__appendBits64LE
301+ Buffer ( n + count * 8 )
302+appendBits64LE = appendBits prim__appendB64LE
245303
246304-- Append count repetitions of a big-endian Bits64 to a Buffer
305+%assert_total
247306public
248307appendBits64BE : Buffer n ->
249308 ( count : Nat ) ->
250309 Bits64 ->
251− Buffer ( n + 8 * count )
252−appendBits64BE = appendBits prim__appendBits64BE
310+ Buffer ( n + count * 8 )
311+appendBits64BE = appendBits prim__appendB64BE