Skip to content

Commit 17ddd68

Browse files
edwinbedwinb
committed
Merge pull request #816 from shlevy/buffer
Buffer
2 parents d95808e + 6efa70d commit 17ddd68

17 files changed

+650
-21
lines changed

‎CONTRIBUTORS

+1
Original file line numberDiff line numberDiff line change
@@ -27,4 +27,5 @@ Leif Warner
2727
Daniel Waterworth
2828
Jonas Westerlund
2929
Reynir Reynisson
30+
Shea Levy
3031

‎idris.cabal

+4
Original file line numberDiff line numberDiff line change
@@ -236,6 +236,10 @@ Extra-source-files:
236236
test/basic009/expected
237237
test/basic009/B/*.idr
238238

239+
test/buffer001/*.idr
240+
test/buffer001/run
241+
test/buffer001/expected
242+
239243
test/dsl001/run
240244
test/dsl001/*.idr
241245
test/dsl001/expected

‎libs/base/Data/Buffer.idr

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

‎libs/base/base.ipkg

+1-1
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ modules = System,
2424
Data.SortedMap, Data.SortedSet, Data.BoundedList,
2525
Data.Vect, Data.HVect, Data.Vect.Quantifiers,
2626
Data.Floats, Data.Complex, Data.Heap, Data.Fun,
27-
Data.Rel,
27+
Data.Rel, Data.Buffer,
2828

2929
Control.Isomorphism,
3030
Control.Monad.Identity,

‎rts/idris_gc.c

+3
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,9 @@ VAL copy(VM* vm, VAL x) {
2727
case STROFFSET:
2828
cl = MKSTROFFc(vm, x->info.str_offset);
2929
break;
30+
case BUFFER:
31+
cl = MKBUFFERc(vm, x->info.buf);
32+
break;
3033
case BIGINT:
3134
cl = MKBIGMc(vm, x->info.ptr);
3235
break;

0 commit comments

Comments
 (0)