git.iko.soy/Idris-dev
on master help sign in
Replace Fin ( n + 1 ), which doesn't reduce, with Fin ( S n )
5750cb5Shea Levy
libs/base/Data/Buffer.idr+16−16
compare with master
unifiedsplit
@@ -56,20 +56,20 @@ copy { n } = MkBuffer . prim__copy ( bitsFromNat n ) . realBuffer
56%assert_total
56%assert_total
57public
57public
58peekBufferNative : Buffer ( m + n ) ->
58peekBufferNative : Buffer ( m + n ) ->
59− ( offset : Fin ( n + 1 ) ) ->
59+ ( offset : Fin ( S n ) ) ->
60 Buffer m
60 Buffer m
61peekBufferNative ( MkBuffer real ) =
61peekBufferNative ( MkBuffer real ) =
62 MkBuffer . prim__peekBufferNative real . bitsFromFin
62 MkBuffer . prim__peekBufferNative real . bitsFromFin
63
63
64public
64public
65peekBufferLE : Buffer ( m + n ) ->
65peekBufferLE : Buffer ( m + n ) ->
66− ( offset : Fin ( n + 1 ) ) ->
66+ ( offset : Fin ( S n ) ) ->
67 Buffer m
67 Buffer m
68peekBufferLE = peekBufferNative
68peekBufferLE = peekBufferNative
69
69
70public
70public
71peekBufferBE : Buffer ( m + n ) ->
71peekBufferBE : Buffer ( m + n ) ->
72− ( offset : Fin ( n + 1 ) ) ->
72+ ( offset : Fin ( S n ) ) ->
73 Buffer m
73 Buffer m
74peekBufferBE = peekBufferNative
74peekBufferBE = peekBufferNative
75
75
@@ -108,7 +108,7 @@ appendBufferBE = appendBufferNative
108
108
109peekBits : ( prim__UnsafeBuffer -> Bits64 -> a ) ->
109peekBits : ( prim__UnsafeBuffer -> Bits64 -> a ) ->
110 Buffer ( m + n ) ->
110 Buffer ( m + n ) ->
111− ( offset : Fin ( n + 1 ) ) ->
111+ ( offset : Fin ( S n ) ) ->
112 a
112 a
113peekBits prim ( MkBuffer real ) = prim real . bitsFromFin
113peekBits prim ( MkBuffer real ) = prim real . bitsFromFin
114
114
@@ -129,18 +129,18 @@ appendBits { n } prim ( MkBuffer real ) count =
129%assert_total
129%assert_total
130public
130public
131peekBits8Native : Buffer ( 1 + n ) ->
131peekBits8Native : Buffer ( 1 + n ) ->
132− ( offset : Fin ( n + 1 ) ) ->
132+ ( offset : Fin ( S n ) ) ->
133 Bits8
133 Bits8
134peekBits8Native = peekBits { m = 1 } prim__peekB8Native
134peekBits8Native = peekBits { m = 1 } prim__peekB8Native
135
135
136%assert_total
136%assert_total
137public
137public
138−peekBits8LE : Buffer ( 1 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits8
138+peekBits8LE : Buffer ( 1 + n ) -> ( offset : Fin ( S n ) ) -> Bits8
139peekBits8LE = peekBits { m = 1 } prim__peekB8LE
139peekBits8LE = peekBits { m = 1 } prim__peekB8LE
140
140
141%assert_total
141%assert_total
142public
142public
143−peekBits8BE : Buffer ( 1 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits8
143+peekBits8BE : Buffer ( 1 + n ) -> ( offset : Fin ( S n ) ) -> Bits8
144peekBits8BE = peekBits { m = 1 } prim__peekB8BE
144peekBits8BE = peekBits { m = 1 } prim__peekB8BE
145
145
146-- Append count repetitions of a Bits8 to a Buffer
146-- Append count repetitions of a Bits8 to a Buffer
@@ -173,20 +173,20 @@ appendBits8BE = appendBits prim__appendB8BE
173%assert_total
173%assert_total
174public
174public
175peekBits16Native : Buffer ( 2 + n ) ->
175peekBits16Native : Buffer ( 2 + n ) ->
176− ( offset : Fin ( n + 1 ) ) ->
176+ ( offset : Fin ( S n ) ) ->
177 Bits16
177 Bits16
178peekBits16Native = peekBits { m = 2 } prim__peekB16Native
178peekBits16Native = peekBits { m = 2 } prim__peekB16Native
179
179
180-- 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
181%assert_total
182public
182public
183−peekBits16LE : Buffer ( 2 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits16
183+peekBits16LE : Buffer ( 2 + n ) -> ( offset : Fin ( S n ) ) -> Bits16
184peekBits16LE = peekBits { m = 2 } prim__peekB16LE
184peekBits16LE = peekBits { m = 2 } prim__peekB16LE
185
185
186-- 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
187%assert_total
188public
188public
189−peekBits16BE : Buffer ( 2 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits16
189+peekBits16BE : Buffer ( 2 + n ) -> ( offset : Fin ( S n ) ) -> Bits16
190peekBits16BE = peekBits { m = 2 } prim__peekB16BE
190peekBits16BE = peekBits { m = 2 } prim__peekB16BE
191
191
192-- 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
@@ -220,20 +220,20 @@ appendBits16BE = appendBits prim__appendB16BE
220%assert_total
220%assert_total
221public
221public
222peekBits32Native : Buffer ( 4 + n ) ->
222peekBits32Native : Buffer ( 4 + n ) ->
223− ( offset : Fin ( n + 1 ) ) ->
223+ ( offset : Fin ( S n ) ) ->
224 Bits32
224 Bits32
225peekBits32Native = peekBits { m = 4 } prim__peekB32Native
225peekBits32Native = peekBits { m = 4 } prim__peekB32Native
226
226
227-- 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
228%assert_total
229public
229public
230−peekBits32LE : Buffer ( 4 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits32
230+peekBits32LE : Buffer ( 4 + n ) -> ( offset : Fin ( S n ) ) -> Bits32
231peekBits32LE = peekBits { m = 4 } prim__peekB32LE
231peekBits32LE = peekBits { m = 4 } prim__peekB32LE
232
232
233-- 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
234%assert_total
235public
235public
236−peekBits32BE : Buffer ( 4 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits32
236+peekBits32BE : Buffer ( 4 + n ) -> ( offset : Fin ( S n ) ) -> Bits32
237peekBits32BE = peekBits { m = 4 } prim__peekB32BE
237peekBits32BE = peekBits { m = 4 } prim__peekB32BE
238
238
239-- 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
@@ -267,20 +267,20 @@ appendBits32BE = appendBits prim__appendB32BE
267%assert_total
267%assert_total
268public
268public
269peekBits64Native : Buffer ( 8 + n ) ->
269peekBits64Native : Buffer ( 8 + n ) ->
270− ( offset : Fin ( n + 1 ) ) ->
270+ ( offset : Fin ( S n ) ) ->
271 Bits64
271 Bits64
272peekBits64Native = peekBits { m = 8 } prim__peekB64Native
272peekBits64Native = peekBits { m = 8 } prim__peekB64Native
273
273
274-- 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
275%assert_total
276public
276public
277−peekBits64LE : Buffer ( 8 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits64
277+peekBits64LE : Buffer ( 8 + n ) -> ( offset : Fin ( S n ) ) -> Bits64
278peekBits64LE = peekBits { m = 8 } prim__peekB64LE
278peekBits64LE = peekBits { m = 8 } prim__peekB64LE
279
279
280-- 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
281%assert_total
282public
282public
283−peekBits64BE : Buffer ( 8 + n ) -> ( offset : Fin ( n + 1 ) ) -> Bits64
283+peekBits64BE : Buffer ( 8 + n ) -> ( offset : Fin ( S n ) ) -> Bits64
284peekBits64BE = peekBits { m = 8 } prim__peekB64BE
284peekBits64BE = peekBits { m = 8 } prim__peekB64BE
285
285
286-- 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