a2332b0 · Idris-dev · git.iko.soy

libs/base/Data/Buffer.idr+9−36

compare with master

unifiedsplit

@@ -102,46 +102,19 @@ appendBits { n } prim ( MkBuffer real ) count =

102-- Read a Bits8 from a Buffer starting at offset

103%assert_total

104public

105−peekBits8Native : Buffer ( 1 + n ) ->

105+peekBits8 : Buffer ( 1 + n ) ->

106− ( offset : Fin ( S n ) ) ->

106+ ( offset : Fin ( S n ) ) ->

107− Bits8

107+ Bits8

108−peekBits8Native = peekBits { m = 1 } prim__peekB8Native

108+peekBits8 = peekBits { m = 1 } prim__peekB8Native

109−

110−%assert_total

111−public

112−peekBits8LE : Buffer ( 1 + n ) -> ( offset : Fin ( S n ) ) -> Bits8

113−peekBits8LE = peekBits { m = 1 } prim__peekB8LE

114−

115−%assert_total

116−public

117−peekBits8BE : Buffer ( 1 + n ) -> ( offset : Fin ( S n ) ) -> Bits8

118−peekBits8BE = peekBits { m = 1 } prim__peekB8BE

119

109

120-- Append count repetitions of a Bits8 to a Buffer

110-- Append count repetitions of a Bits8 to a Buffer

121%assert_total

111%assert_total

122public

112public

123−appendBits8Native : Buffer n ->

113+appendBits8 : Buffer n ->

124− ( count : Nat ) ->

114+ ( count : Nat ) ->

125− Bits8 ->

115+ Bits8 ->

126− Buffer ( n + count * 1 )

116+ Buffer ( n + count * 1 )

127−appendBits8Native = appendBits prim__appendB8Native

117+appendBits8 = appendBits prim__appendB8Native

128−

129−%assert_total

130−public

131−appendBits8LE : Buffer n ->

132− ( count : Nat ) ->

133− Bits8 ->

134− Buffer ( n + count * 1 )

135−appendBits8LE = appendBits prim__appendB8LE

136−

137−%assert_total

138−public

139−appendBits8BE : Buffer n ->

140− ( count : Nat ) ->

141− Bits8 ->

142− Buffer ( n + count * 1 )

143−appendBits8BE = appendBits prim__appendB8BE

144−

145

118

146-- Read a Bits16 in native byte order from a Buffer starting at offset

119-- Read a Bits16 in native byte order from a Buffer starting at offset

147%assert_total

120%assert_total

rts/idris_rts.c−16

@@ -623,14 +623,6 @@ VAL idris_appendB8Native(VM* vm, VAL buf, VAL len, VAL cnt, VAL val) {

623 return cl;

624}

625

626−VAL idris_appendB8LE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val) {

627− return idris_appendB8Native(vm, buf, len, cnt, val);

628−}

629−

630−VAL idris_appendB8BE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val) {

631− return idris_appendB8Native(vm, buf, len, cnt, val);

632−}

633−

634static VAL internal_append_bits(VM* vm, VAL buf, VAL bufLen, VAL cnt, const void* val, size_t val_len) {

626static VAL internal_append_bits(VM* vm, VAL buf, VAL bufLen, VAL cnt, const void* val, size_t val_len) {

635 size_t len = bufLen->info.bits64;

627 size_t len = bufLen->info.bits64;

636 size_t count = cnt->info.bits64;

628 size_t count = cnt->info.bits64;

@@ -722,14 +714,6 @@ VAL idris_peekB8Native(VM* vm, VAL buf, VAL off) {

722 return MKB8(vm, *val);

714 return MKB8(vm, *val);

723}

715}

724

716

725−VAL idris_peekB8LE(VM* vm, VAL buf, VAL off) {

726− return idris_peekB8Native(vm, buf, off);

727−}

728−

729−VAL idris_peekB8BE(VM* vm, VAL buf, VAL off) {

730− return idris_peekB8Native(vm, buf, off);

731−}

732−

733VAL idris_peekB16Native(VM* vm, VAL buf, VAL off) {

717VAL idris_peekB16Native(VM* vm, VAL buf, VAL off) {

734 size_t offset = off->info.bits64;

718 size_t offset = off->info.bits64;

735 uint16_t* val = (uint16_t *) ((GETTY(buf) == BUFOFFSET) ?

719 uint16_t* val = (uint16_t *) ((GETTY(buf) == BUFOFFSET) ?

rts/idris_rts.h−4

@@ -259,8 +259,6 @@ VAL idris_copy(VM* vm, VAL len, VAL src);

259VAL idris_appendBuffer(VM* vm, VAL fst, VAL fstLen, VAL count, VAL sndLen, VAL snd);

260VAL idris_peekBuffer(VM* vm, VAL src, VAL off);

261VAL idris_appendB8Native(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

262−VAL idris_appendB8LE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

263−VAL idris_appendB8BE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

264VAL idris_appendB16Native(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

262VAL idris_appendB16Native(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

265VAL idris_appendB16LE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

263VAL idris_appendB16LE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

266VAL idris_appendB16BE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

264VAL idris_appendB16BE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

@@ -271,8 +269,6 @@ VAL idris_appendB64Native(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

271VAL idris_appendB64LE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

269VAL idris_appendB64LE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

272VAL idris_appendB64BE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

270VAL idris_appendB64BE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

273VAL idris_peekB8Native(VM* vm, VAL buf, VAL off);

271VAL idris_peekB8Native(VM* vm, VAL buf, VAL off);

274−VAL idris_peekB8LE(VM* vm, VAL buf, VAL off);

275−VAL idris_peekB8BE(VM* vm, VAL buf, VAL off);

276VAL idris_peekB16Native(VM* vm, VAL buf, VAL off);

272VAL idris_peekB16Native(VM* vm, VAL buf, VAL off);

277VAL idris_peekB16LE(VM* vm, VAL buf, VAL off);

273VAL idris_peekB16LE(VM* vm, VAL buf, VAL off);

278VAL idris_peekB16BE(VM* vm, VAL buf, VAL off);

274VAL idris_peekB16BE(VM* vm, VAL buf, VAL off);

src/IRTS/Lang.hs+3

@@ -62,6 +62,9 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

62 | LCopy

63 | LAppendBuffer

64 | LPeekBuffer

65+ -- Note that for Bits8 only Native endianness is actually used

66+ -- and the user-exposed interface for Bits8 doesn't mention

67+ -- endianness

65 | LAppend IntTy Endianness

68 | LAppend IntTy Endianness

66 | LPeek IntTy Endianness

69 | LPeek IntTy Endianness

67

70

test/buffer001/buffer001.idr+2−2

@@ -15,10 +15,10 @@ firstHalf : Buffer 4

15firstHalf = appendBits32LE em 1 one

16

17full : Buffer 8

18−full = appendBits8LE firstHalf 4 two

18+full = appendBits8 firstHalf 4 two

19

20firstByte : Bits8

21−firstByte = peekBits8LE full 0

21+firstByte = peekBits8 full 0

22

23firstHalfView : Buffer 4

24firstHalfView = peekBuffer full 0