@@ -1,254 +0,0 @@
1−module Data.Buffer
2−
3−import Data.Fin
4−
5−%default total
6−
7−-- !!! TODO: Open issues:
8−-- 1. It may be theoretically nice to represent Buffer size as
9−-- Fin (2 ^ WORD_BITS) instead of Nat
10−-- 2. Primitives take Bits64 when really they should take the
11−-- equivalent of C's size_t (ideally unboxed)
12−-- 3. If we had access to host system information, we could reduce
13−-- the needed primitives by implementing the LE/BE variants on
14−-- top of the native variant plus a possible swab function
15−-- 4. Would be nice to be able to peek/append Int, Char, and Float,
16−-- all have fixed (though possibly implementation-dependent) widths.
17−-- Currently not in place due to lack of host system introspection.
18−-- 5. Would be nice to be able to peek/append the vector types, but
19−-- for now I'm only touching the C backend which AFAICT doesn't
20−-- support them.
21−-- 6. Conversion from Fin to Bits64 (which, re 2, should eventually
22−-- be a fixed-width implementation-dependent type) is likely
23−-- inefficient relative to conversion from Nat to Bits64
24−-- 7. We may want to have a separate type that is a product of Buffer
25−-- and offset rather than storing the offset in Buffer itself, which
26−-- would require exposing the offset argument of prim__appendBuffer
27−
28−||| A contiguous chunk of n bytes
29−abstract
30−record Buffer : Nat -> Type where
31− MkBuffer : ( offset : Nat ) -> ( realBuffer : prim__UnsafeBuffer ) -> Buffer n
32−
33−bitsFromNat : Nat -> Bits64
34−bitsFromNat Z = 0
35−bitsFromNat (S k) = 1 + bitsFromNat k
36−
37−bitsFromFin : Fin n -> Bits64
38−bitsFromFin FZ = 0
39−bitsFromFin (FS k) = 1 + bitsFromFin k
40−
41−||| Allocate an empty Buffer. The size hint can be used to avoid
42−||| unnecessary reallocations and copies under the hood if the
43−||| approximate ultimate size of the Buffer is known. Users can assume
44−||| the new Buffer is word-aligned.
45−public
46−allocate : ( hint : Nat ) -> Buffer Z
47−allocate = MkBuffer Z . prim__allocate . bitsFromNat
48−
49−||| Append count repetitions of a Buffer to another Buffer
50−%assert_total
51−public
52−appendBuffer : Buffer n ->
53− ( count : Nat ) ->
54− Buffer m ->
55− Buffer ( n + count * m )
56−appendBuffer { n } { m } ( MkBuffer o1 r1 ) c ( MkBuffer o2 r2 ) =
57− MkBuffer o1 $ prim__appendBuffer r1 size1 count size2 off r2
58− where
59− size1 : Bits64
60− size1 = bitsFromNat ( n + o1 )
61− size2 : Bits64
62− size2 = bitsFromNat m
63− count : Bits64
64− count = bitsFromNat c
65− off : Bits64
66− off = bitsFromNat o2
67−
68−||| Copy a buffer, potentially allowing the (potentially large) space it
69−||| pointed to to be freed
70−public
71−copy : Buffer n -> Buffer n
72−copy { n } = replace ( plusZeroRightNeutral n ) . appendBuffer ( allocate n ) 1
73−
74−||| Create a view over a buffer
75−public
76−peekBuffer : { n : Nat } -> { offset : Nat } -> Buffer ( n + offset ) -> ( offset : Nat ) -> Buffer n
77−peekBuffer ( MkBuffer o r ) off = MkBuffer ( o + off ) r
78−
79−peekBits : ( prim__UnsafeBuffer -> Bits64 -> a ) ->
80− Buffer ( m + n ) ->
81− ( offset : Fin ( S n ) ) ->
82− a
83−peekBits prim ( MkBuffer o r ) = prim r . bitsFromNat . plus o . finToNat
84−
85−appendBits : ( prim__UnsafeBuffer ->
86− Bits64 ->
87− Bits64 ->
88− a ->
89− prim__UnsafeBuffer ) ->
90− Buffer n ->
91− ( count : Nat) ->
92− a ->
93− Buffer ( n + count * size )
94−appendBits { n } prim ( MkBuffer o r ) count =
95− MkBuffer o . prim r ( bitsFromNat $ n + o ) ( bitsFromNat count )
96−
97−
98−||| Read a Bits8 from a Buffer starting at offset
99−%assert_total
100−public
101−peekBits8 : Buffer ( 1 + n ) ->
102− ( offset : Fin ( S n ) ) ->
103− Bits8
104−peekBits8 = peekBits { m = 1 } prim__peekB8Native
105−
106−||| Append count repetitions of a Bits8 to a Buffer
107−%assert_total
108−public
109−appendBits8 : Buffer n ->
110− ( count : Nat ) ->
111− Bits8 ->
112− Buffer ( n + count * 1 )
113−appendBits8 = appendBits prim__appendB8Native
114−
115−||| Read a Bits16 in native byte order from a Buffer starting at offset
116−%assert_total
117−public
118−peekBits16Native : Buffer ( 2 + n ) ->
119− ( offset : Fin ( S n ) ) ->
120− Bits16
121−peekBits16Native = peekBits { m = 2 } prim__peekB16Native
122−
123−||| Read a little-endian Bits16 from a Buffer starting at offset
124−%assert_total
125−public
126−peekBits16LE : Buffer ( 2 + n ) -> ( offset : Fin ( S n ) ) -> Bits16
127−peekBits16LE = peekBits { m = 2 } prim__peekB16LE
128−
129−||| Read a big-endian Bits16 from a Buffer starting at offset
130−%assert_total
131−public
132−peekBits16BE : Buffer ( 2 + n ) -> ( offset : Fin ( S n ) ) -> Bits16
133−peekBits16BE = peekBits { m = 2 } prim__peekB16BE
134−
135−||| Append count repetitions of a Bits16 in native byte order to a Buffer
136−%assert_total
137−public
138−appendBits16Native : Buffer n ->
139− ( count : Nat ) ->
140− Bits16 ->
141− Buffer ( n + count * 2 )
142−appendBits16Native = appendBits prim__appendB16Native
143−
144−||| Append count repetitions of a little-endian Bits16 to a Buffer
145−%assert_total
146−public
147−appendBits16LE : Buffer n ->
148− ( count : Nat ) ->
149− Bits16 ->
150− Buffer ( n + count * 2 )
151−appendBits16LE = appendBits prim__appendB16LE
152−
153−||| Append count repetitions of a big-endian Bits16 to a Buffer
154−%assert_total
155−public
156−appendBits16BE : Buffer n ->
157− ( count : Nat ) ->
158− Bits16 ->
159− Buffer ( n + count * 2 )
160−appendBits16BE = appendBits prim__appendB16BE
161−
162−||| Read a Bits32 in native byte order from a Buffer starting at offset
163−%assert_total
164−public
165−peekBits32Native : Buffer ( 4 + n ) ->
166− ( offset : Fin ( S n ) ) ->
167− Bits32
168−peekBits32Native = peekBits { m = 4 } prim__peekB32Native
169−
170−||| Read a little-endian Bits32 from a Buffer starting at offset
171−%assert_total
172−public
173−peekBits32LE : Buffer ( 4 + n ) -> ( offset : Fin ( S n ) ) -> Bits32
174−peekBits32LE = peekBits { m = 4 } prim__peekB32LE
175−
176−||| Read a big-endian Bits32 from a Buffer starting at offset
177−%assert_total
178−public
179−peekBits32BE : Buffer ( 4 + n ) -> ( offset : Fin ( S n ) ) -> Bits32
180−peekBits32BE = peekBits { m = 4 } prim__peekB32BE
181−
182−||| Append count repetitions of a Bits32 in native byte order to a Buffer
183−%assert_total
184−public
185−appendBits32Native : Buffer n ->
186− ( count : Nat ) ->
187− Bits32 ->
188− Buffer ( n + count * 4 )
189−appendBits32Native = appendBits prim__appendB32Native
190−
191−||| Append count repetitions of a little-endian Bits32 to a Buffer
192−%assert_total
193−public
194−appendBits32LE : Buffer n ->
195− ( count : Nat ) ->
196− Bits32 ->
197− Buffer ( n + count * 4 )
198−appendBits32LE = appendBits prim__appendB32LE
199−
200−||| Append count repetitions of a big-endian Bits32 to a Buffer
201−%assert_total
202−public
203−appendBits32BE : Buffer n ->
204− ( count : Nat ) ->
205− Bits32 ->
206− Buffer ( n + count * 4 )
207−appendBits32BE = appendBits prim__appendB32BE
208−
209−||| Read a Bits64 in native byte order from a Buffer starting at offset
210−%assert_total
211−public
212−peekBits64Native : Buffer ( 8 + n ) ->
213− ( offset : Fin ( S n ) ) ->
214− Bits64
215−peekBits64Native = peekBits { m = 8 } prim__peekB64Native
216−
217−||| Read a little-endian Bits64 from a Buffer starting at offset
218−%assert_total
219−public
220−peekBits64LE : Buffer ( 8 + n ) -> ( offset : Fin ( S n ) ) -> Bits64
221−peekBits64LE = peekBits { m = 8 } prim__peekB64LE
222−
223−||| Read a big-endian Bits64 from a Buffer starting at offset
224−%assert_total
225−public
226−peekBits64BE : Buffer ( 8 + n ) -> ( offset : Fin ( S n ) ) -> Bits64
227−peekBits64BE = peekBits { m = 8 } prim__peekB64BE
228−
229−||| Append count repetitions of a Bits64 in native byte order to a Buffer
230−%assert_total
231−public
232−appendBits64Native : Buffer n ->
233− ( count : Nat ) ->
234− Bits64 ->
235− Buffer ( n + count * 8 )
236−appendBits64Native = appendBits prim__appendB64Native
237−
238−||| Append count repetitions of a little-endian Bits64 to a Buffer
239−%assert_total
240−public
241−appendBits64LE : Buffer n ->
242− ( count : Nat ) ->
243− Bits64 ->
244− Buffer ( n + count * 8 )
245−appendBits64LE = appendBits prim__appendB64LE
246−
247−||| Append count repetitions of a big-endian Bits64 to a Buffer
248−%assert_total
249−public
250−appendBits64BE : Buffer n ->
251− ( count : Nat ) ->
252− Bits64 ->
253− Buffer ( n + count * 8 )
254−appendBits64BE = appendBits prim__appendB64BE