17ddd68 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #816 from shlevy/buffer

17ddd68Edwin Brady13 years ago

CONTRIBUTORS+1

compare with master

unifiedsplit

@@ -27,4 +27,5 @@ Leif Warner

27Daniel Waterworth

28Jonas Westerlund

29Reynir Reynisson

30+Shea Levy

idris.cabal+4

@@ -236,6 +236,10 @@ Extra-source-files:

236 test/basic009/expected

237 test/basic009/B/*.idr

238

239+ test/buffer001/*.idr

240+ test/buffer001/run

241+ test/buffer001/expected

242+

239 test/dsl001/run

243 test/dsl001/run

240 test/dsl001/*.idr

244 test/dsl001/*.idr

241 test/dsl001/expected

245 test/dsl001/expected

libs/base/Data/Buffer.idrnew file+252

@@ -0,0 +1,252 @@

1+module Data.Buffer

3+%default total

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

@@ -24,7 +24,7 @@ modules = System,

24 Data.SortedMap, Data.SortedSet, Data.BoundedList,

25 Data.Vect, Data.HVect, Data.Vect.Quantifiers,

26 Data.Floats, Data.Complex, Data.Heap, Data.Fun,

27− Data.Rel,

27+ Data.Rel, Data.Buffer,

29 Control.Isomorphism,

30 Control.Monad.Identity,

rts/idris_gc.c+3

@@ -27,6 +27,9 @@ VAL copy(VM* vm, VAL x) {

27 case STROFFSET:

28 cl = MKSTROFFc(vm, x->info.str_offset);

29 break;

30+ case BUFFER:

31+ cl = MKBUFFERc(vm, x->info.buf);

32+ break;

30 case BIGINT:

33 case BIGINT:

31 cl = MKBIGMc(vm, x->info.ptr);

34 cl = MKBIGMc(vm, x->info.ptr);

32 break;

35 break;

rts/idris_rts.c+237

@@ -475,6 +475,240 @@ VAL idris_strRev(VM* vm, VAL str) {

475 return cl;

476}

477

478+VAL MKBUFFERc(VM* vm, Buffer* buf) {

479+ Closure* cl = allocate(vm, sizeof(Closure) + sizeof *buf + buf->cap, 1);

480+ SETTY(cl, BUFFER);

481+ cl->info.buf = (Buffer*)((void*)cl + sizeof(Closure));

482+ memmove(cl->info.buf, buf, sizeof *buf + buf->fill);

483+ return cl;

484+}

485+

486+static VAL internal_allocate(VM *vm, size_t hint) {

487+ size_t size = hint + sizeof(Closure) + sizeof(Buffer);

488+

489+ // Round up to a power of 2

490+ --size;

491+ size_t i;

492+ for (i = 0; i <= sizeof size; ++i)

493+ size |= size >> (1 << i);

494+ ++size;

495+

496+ Closure* cl = allocate(vm, size, 0);

497+ SETTY(cl, BUFFER);

498+ cl->info.buf = (Buffer*)((void*)cl + sizeof(Closure));

499+ cl->info.buf->cap = size - (sizeof(Closure) + sizeof(Buffer));

500+ return cl;

501+}

502+

503+// Following functions cast uint64_t to size_t, which may narrow!

504+VAL idris_allocate(VM* vm, VAL hint) {

505+ Closure* cl = internal_allocate(vm, hint->info.bits64);

506+ cl->info.buf->fill = 0;

507+ return cl;

508+}

509+

510+static void internal_memset(void *dest, const void *src, size_t size, size_t num) {

511+ while (num--) {

512+ memmove(dest, src, size);

513+ dest += size;

514+ }

515+}

516+

517+static VAL internal_prepare_append(VM* vm, VAL buf, size_t bufLen, size_t appLen) {

518+ size_t totalLen = bufLen + appLen;

519+ Closure* cl;

520+ if (bufLen != buf->info.buf->fill ||

521+ totalLen > buf->info.buf->cap) {

522+ // We're not at the fill or are over cap, so need a new buffer

523+ cl = internal_allocate(vm, totalLen);

524+ memmove(cl->info.buf->store,

525+ buf->info.buf->store,

526+ bufLen);

527+ cl->info.buf->fill = totalLen;

528+ } else {

529+ // Hooray, can just bump the fill

530+ cl = buf;

531+ cl->info.buf->fill += appLen;

532+ }

533+ return cl;

534+}

535+

536+VAL idris_appendBuffer(VM* vm, VAL fst, VAL fstLen, VAL cnt, VAL sndLen, VAL sndOff, VAL snd) {

537+ size_t firstLength = fstLen->info.bits64;

538+ size_t secondLength = sndLen->info.bits64;

539+ size_t count = cnt->info.bits64;

540+ size_t offset = sndOff->info.bits64;

541+ Closure* cl = internal_prepare_append(vm, fst, firstLength, count * secondLength);

542+ internal_memset(cl->info.buf->store + firstLength, snd->info.buf->store + offset, secondLength, count);

543+ return cl;

544+}

545+

546+// Special cased because we can use memset

547+VAL idris_appendB8Native(VM* vm, VAL buf, VAL len, VAL cnt, VAL val) {

548+ size_t bufLen = len->info.bits64;

549+ size_t count = cnt->info.bits64;

550+ Closure* cl = internal_prepare_append(vm, buf, bufLen, count);

551+ memset(cl->info.buf->store + bufLen, val->info.bits8, count);

552+ return cl;

553+}

554+

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

556+ size_t len = bufLen->info.bits64;

557+ size_t count = cnt->info.bits64;

558+ Closure* cl = internal_prepare_append(vm, buf, len, count * val_len);

559+ internal_memset(cl->info.buf->store + len, val, val_len, count);

560+ return cl;

561+}

562+

563+VAL idris_appendB16Native(VM* vm, VAL buf, VAL len, VAL cnt, VAL val) {

564+ return internal_append_bits(vm, buf, len, cnt, &val->info.bits16, sizeof val->info.bits16);

565+}

566+

567+VAL idris_appendB16LE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val) {

568+ // On gcc 4.8 -O3 compiling for x86_64, using leVal like this is

569+ // optimized away. Presumably the same holds for other sizes and

570+ // conversly on BE systems

571+ unsigned char leVal[sizeof val] = { val->info.bits16

572+ , (val->info.bits16 >> 8)

573+ };

574+ return internal_append_bits(vm, buf, len, cnt, leVal, sizeof leVal);

575+}

576+

577+VAL idris_appendB16BE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val) {

578+ unsigned char beVal[sizeof val] = { (val->info.bits16 >> 8)

579+ , val->info.bits16

580+ };

581+ return internal_append_bits(vm, buf, len, cnt, beVal, sizeof beVal);

582+}

583+

584+VAL idris_appendB32Native(VM* vm, VAL buf, VAL len, VAL cnt, VAL val) {

585+ return internal_append_bits(vm, buf, len, cnt, &val->info.bits32, sizeof val->info.bits32);

586+}

587+

588+VAL idris_appendB32LE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val) {

589+ unsigned char leVal[sizeof val] = { val->info.bits32

590+ , (val->info.bits32 >> 8)

591+ , (val->info.bits32 >> 16)

592+ , (val->info.bits32 >> 24)

593+ };

594+ return internal_append_bits(vm, buf, len, cnt, leVal, sizeof leVal);

595+}

596+

597+VAL idris_appendB32BE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val) {

598+ unsigned char beVal[sizeof val] = { (val->info.bits32 >> 24)

599+ , (val->info.bits32 >> 16)

600+ , (val->info.bits32 >> 8)

601+ , val->info.bits32

602+ };

603+ return internal_append_bits(vm, buf, len, cnt, beVal, sizeof beVal);

604+}

605+

606+VAL idris_appendB64Native(VM* vm, VAL buf, VAL len, VAL cnt, VAL val) {

607+ return internal_append_bits(vm, buf, len, cnt, &val->info.bits64, sizeof val->info.bits64);

608+}

609+

610+VAL idris_appendB64LE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val) {

611+ unsigned char leVal[sizeof val] = { val->info.bits64

612+ , (val->info.bits64 >> 8)

613+ , (val->info.bits64 >> 16)

614+ , (val->info.bits64 >> 24)

615+ , (val->info.bits64 >> 32)

616+ , (val->info.bits64 >> 40)

617+ , (val->info.bits64 >> 48)

618+ , (val->info.bits64 >> 56)

619+ };

620+ return internal_append_bits(vm, buf, len, cnt, leVal, sizeof leVal);

621+}

622+

623+VAL idris_appendB64BE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val) {

624+ unsigned char beVal[sizeof val] = { (val->info.bits64 >> 56)

625+ , (val->info.bits64 >> 48)

626+ , (val->info.bits64 >> 40)

627+ , (val->info.bits64 >> 32)

628+ , (val->info.bits64 >> 24)

629+ , (val->info.bits64 >> 16)

630+ , (val->info.bits64 >> 8)

631+ , val->info.bits64

632+ };

633+ return internal_append_bits(vm, buf, len, cnt, beVal, sizeof beVal);

634+}

635+

636+VAL idris_peekB8Native(VM* vm, VAL buf, VAL off) {

637+ size_t offset = off->info.bits64;

638+ uint8_t *val = buf->info.buf->store + offset;

639+ return MKB8(vm, *val);

640+}

641+

642+VAL idris_peekB16Native(VM* vm, VAL buf, VAL off) {

643+ size_t offset = off->info.bits64;

644+ uint16_t *val = (uint16_t *) (buf->info.buf->store + offset);

645+ return MKB16(vm, *val);

646+}

647+

648+VAL idris_peekB16LE(VM* vm, VAL buf, VAL off) {

649+ size_t offset = off->info.bits64;

650+ return MKB16(vm, ((uint16_t) buf->info.buf->store[offset]) +

651+ (((uint16_t) buf->info.buf->store[offset + 1]) << 8));

652+}

653+

654+VAL idris_peekB16BE(VM* vm, VAL buf, VAL off) {

655+ size_t offset = off->info.bits64;

656+ return MKB16(vm, ((uint16_t) buf->info.buf->store[offset + 1]) +

657+ (((uint16_t) buf->info.buf->store[offset]) << 8));

658+}

659+

660+VAL idris_peekB32Native(VM* vm, VAL buf, VAL off) {

661+ size_t offset = off->info.bits64;

662+ uint32_t *val = (uint32_t *) (buf->info.buf->store + offset);

663+ return MKB32(vm, *val);

664+}

665+

666+VAL idris_peekB32LE(VM* vm, VAL buf, VAL off) {

667+ size_t offset = off->info.bits64;

668+ return MKB32(vm, ((uint32_t) buf->info.buf->store[offset]) +

669+ (((uint32_t) buf->info.buf->store[offset + 1]) << 8) +

670+ (((uint32_t) buf->info.buf->store[offset + 2]) << 16) +

671+ (((uint32_t) buf->info.buf->store[offset + 3]) << 24));

672+}

673+

674+VAL idris_peekB32BE(VM* vm, VAL buf, VAL off) {

675+ size_t offset = off->info.bits64;

676+ return MKB32(vm, ((uint32_t) buf->info.buf->store[offset + 3]) +

677+ (((uint32_t) buf->info.buf->store[offset + 2]) << 8) +

678+ (((uint32_t) buf->info.buf->store[offset + 1]) << 16) +

679+ (((uint32_t) buf->info.buf->store[offset]) << 24));

680+}

681+

682+VAL idris_peekB64Native(VM* vm, VAL buf, VAL off) {

683+ size_t offset = off->info.bits64;

684+ uint64_t *val = (uint64_t *) (buf->info.buf->store + offset);

685+ return MKB64(vm, *val);

686+}

687+

688+VAL idris_peekB64LE(VM* vm, VAL buf, VAL off) {

689+ size_t offset = off->info.bits64;

690+ return MKB64(vm, ((uint64_t) buf->info.buf->store[offset]) +

691+ (((uint64_t) buf->info.buf->store[offset + 1]) << 8) +

692+ (((uint64_t) buf->info.buf->store[offset + 2]) << 16) +

693+ (((uint64_t) buf->info.buf->store[offset + 3]) << 24) +

694+ (((uint64_t) buf->info.buf->store[offset + 4]) << 32) +

695+ (((uint64_t) buf->info.buf->store[offset + 5]) << 40) +

696+ (((uint64_t) buf->info.buf->store[offset + 6]) << 48) +

697+ (((uint64_t) buf->info.buf->store[offset + 7]) << 56));

698+}

699+

700+VAL idris_peekB64BE(VM* vm, VAL buf, VAL off) {

701+ size_t offset = off->info.bits64;

702+ return MKB64(vm, ((uint64_t) buf->info.buf->store[offset + 7]) +

703+ (((uint64_t) buf->info.buf->store[offset + 6]) << 8) +

704+ (((uint64_t) buf->info.buf->store[offset + 5]) << 16) +

705+ (((uint64_t) buf->info.buf->store[offset + 4]) << 24) +

706+ (((uint64_t) buf->info.buf->store[offset + 3]) << 32) +

707+ (((uint64_t) buf->info.buf->store[offset + 2]) << 40) +

708+ (((uint64_t) buf->info.buf->store[offset + 1]) << 48) +

709+ (((uint64_t) buf->info.buf->store[offset]) << 56));

710+}

711+

478typedef struct {

712typedef struct {

479 VM* vm; // thread's VM

713 VM* vm; // thread's VM

480 VM* callvm; // calling thread's VM

714 VM* callvm; // calling thread's VM

@@ -552,6 +786,9 @@ VAL copyTo(VM* vm, VAL x) {

552 case STRING:

786 case STRING:

553 cl = MKSTRc(vm, x->info.str);

787 cl = MKSTRc(vm, x->info.str);

554 break;

788 break;

789+ case BUFFER:

790+ cl = MKBUFFERc(vm, x->info.buf);

791+ break;

555 case BIGINT:

792 case BIGINT:

556 cl = MKBIGMc(vm, x->info.ptr);

793 cl = MKBIGMc(vm, x->info.ptr);

557 break;

794 break;

rts/idris_rts.h+37−1

@@ -16,7 +16,8 @@

17typedef enum {

18 CON, INT, BIGINT, FLOAT, STRING, STROFFSET,

19− BITS8, BITS16, BITS32, BITS64, UNIT, PTR, FWD

19+ BITS8, BITS16, BITS32, BITS64, UNIT, PTR, FWD,

20+ BUFFER

20} ClosureType;

21} ClosureType;

22typedef struct Closure *VAL;

23typedef struct Closure *VAL;

@@ -31,6 +32,15 @@ typedef struct {

31 int offset;

32 int offset;

32} StrOffset;

33} StrOffset;

35+typedef struct {

36+ // If we ever have multithreaded access to the same heap,

37+ // fill is mutable so needs synchronization!

38+ size_t fill;

39+ size_t cap;

40+ unsigned char store[];

41+} Buffer;

42+

43+

34typedef struct Closure {

44typedef struct Closure {

35// Use top 16 bits of ty for saying which heap value is in

45// Use top 16 bits of ty for saying which heap value is in

36// Bottom 16 bits for closure type

46// Bottom 16 bits for closure type

@@ -46,6 +56,7 @@ typedef struct Closure {

46 uint16_t bits16;

56 uint16_t bits16;

47 uint32_t bits32;

57 uint32_t bits32;

48 uint64_t bits64;

58 uint64_t bits64;

59+ Buffer* buf;

49 } info;

60 } info;

50} Closure;

61} Closure;

@@ -162,6 +173,7 @@ VAL MKFLOATc(VM* vm, double val);

162VAL MKSTROFFc(VM* vm, StrOffset* off);

173VAL MKSTROFFc(VM* vm, StrOffset* off);

163VAL MKSTRc(VM* vm, char* str);

174VAL MKSTRc(VM* vm, char* str);

164VAL MKPTRc(VM* vm, void* ptr);

175VAL MKPTRc(VM* vm, void* ptr);

176+VAL MKBUFFERc(VM* vm, Buffer* buf);

165

177

166char* GETSTROFF(VAL stroff);

178char* GETSTROFF(VAL stroff);

167

179

@@ -234,6 +246,30 @@ VAL idris_strCons(VM* vm, VAL x, VAL xs);

234VAL idris_strIndex(VM* vm, VAL str, VAL i);

246VAL idris_strIndex(VM* vm, VAL str, VAL i);

235VAL idris_strRev(VM* vm, VAL str);

247VAL idris_strRev(VM* vm, VAL str);

236

248

249+// Buffer primitives

250+VAL idris_allocate(VM* vm, VAL hint);

251+VAL idris_appendBuffer(VM* vm, VAL fst, VAL fstLen, VAL cnt, VAL sndLen, VAL sndOff, VAL snd);

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

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

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

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

256+VAL idris_appendB32Native(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

257+VAL idris_appendB32LE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

258+VAL idris_appendB32BE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

259+VAL idris_appendB64Native(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

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

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

262+VAL idris_peekB8Native(VM* vm, VAL buf, VAL off);

263+VAL idris_peekB16Native(VM* vm, VAL buf, VAL off);

264+VAL idris_peekB16LE(VM* vm, VAL buf, VAL off);

265+VAL idris_peekB16BE(VM* vm, VAL buf, VAL off);

266+VAL idris_peekB32Native(VM* vm, VAL buf, VAL off);

267+VAL idris_peekB32LE(VM* vm, VAL buf, VAL off);

268+VAL idris_peekB32BE(VM* vm, VAL buf, VAL off);

269+VAL idris_peekB64Native(VM* vm, VAL buf, VAL off);

270+VAL idris_peekB64LE(VM* vm, VAL buf, VAL off);

271+VAL idris_peekB64BE(VM* vm, VAL buf, VAL off);

272+

237// Command line args

273// Command line args

238

274

239extern int __idris_argc;

275extern int __idris_argc;

src/IRTS/CodegenC.hs+5

@@ -457,6 +457,11 @@ doOp v LStrCons [x, y] = v ++ "idris_strCons(vm, " ++ creg x ++ "," ++ creg y ++

457doOp v LStrIndex [x, y] = v ++ "idris_strIndex(vm, " ++ creg x ++ "," ++ creg y ++ ")"

458doOp v LStrRev [x] = v ++ "idris_strRev(vm, " ++ creg x ++ ")"

459

460+doOp v LAllocate [x] = v ++ "idris_allocate(vm, " ++ creg x ++ ")"

461+doOp v LAppendBuffer [a, b, c, d, e, f] = v ++ "idris_appendBuffer(vm, " ++ creg a ++ "," ++ creg b ++ "," ++ creg c ++ "," ++ creg d ++ "," ++ creg e ++ "," ++ creg f ++ ")"

462+doOp v (LAppend ity en) [a, b, c, d] = v ++ "idris_append" ++ intTyName ity ++ show en ++ "(vm, " ++ creg a ++ "," ++ creg b ++ "," ++ creg c ++ "," ++ creg d ++ ")"

463+doOp v (LPeek ity en) [x, y] = v ++ "idris_peek" ++ intTyName ity ++ show en ++ "(vm, " ++ creg x ++ "," ++ creg y ++ ")"

464+

460doOp v LStdIn [] = v ++ "MKPTR(vm, stdin)"

465doOp v LStdIn [] = v ++ "MKPTR(vm, stdin)"

461doOp v LStdOut [] = v ++ "MKPTR(vm, stdout)"

466doOp v LStdOut [] = v ++ "MKPTR(vm, stdout)"

462doOp v LStdErr [] = v ++ "MKPTR(vm, stderr)"

467doOp v LStdErr [] = v ++ "MKPTR(vm, stderr)"

src/IRTS/Lang.hs+11

@@ -5,6 +5,8 @@ import Idris.Core.TT

5import Data.List

6import Debug.Trace

8+data Endianness = Native | BE | LE deriving (Show, Eq)

8data LVar = Loc Int | Glob Name

10data LVar = Loc Int | Glob Name

9 deriving (Show, Eq)

11 deriving (Show, Eq)

@@ -50,6 +52,15 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

51 | LStdIn | LStdOut | LStdErr

53 | LStdIn | LStdOut | LStdErr

55+ -- Buffers

56+ | LAllocate

57+ | LAppendBuffer

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

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

60+ -- endianness

61+ | LAppend IntTy Endianness

62+ | LPeek IntTy Endianness

63+

53 | LFork

64 | LFork

54 | LPar -- evaluate argument anywhere, possibly on another

65 | LPar -- evaluate argument anywhere, possibly on another

55 -- core or another machine. 'id' is a valid implementation

66 -- core or another machine. 'id' is a valid implementation

src/Idris/Core/TT.hs+10−1

@@ -434,6 +434,13 @@ data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar

434 | ITVec NativeTy Int

435 deriving (Show, Eq, Ord)

436

437+intTyName :: IntTy -> String

438+intTyName ITNative = "Int"

439+intTyName ITBig = "BigInt"

440+intTyName (ITFixed sized) = "B" ++ show (nativeTyWidth sized)

441+intTyName (ITChar) = "Char"

442+intTyName (ITVec ity count) = "B" ++ show (nativeTyWidth ity) ++ "x" ++ show count

443+

437data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors

444data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors

438 deriving (Show, Eq, Ord)

445 deriving (Show, Eq, Ord)

439{-!

446{-!

@@ -468,7 +475,7 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

468 | B8V (Vector Word8) | B16V (Vector Word16)

475 | B8V (Vector Word8) | B16V (Vector Word16)

469 | B32V (Vector Word32) | B64V (Vector Word64)

476 | B32V (Vector Word32) | B64V (Vector Word64)

470 | AType ArithTy | StrType

477 | AType ArithTy | StrType

471− | PtrType | VoidType | Forgot

478+ | PtrType | BufferType | VoidType | Forgot

472 deriving (Eq, Ord)

479 deriving (Eq, Ord)

473{-!

480{-!

474deriving instance Binary Const

481deriving instance Binary Const

@@ -486,6 +493,7 @@ instance Pretty Const OutputAnnotation where

486 pretty (Str s) = text s

493 pretty (Str s) = text s

487 pretty (AType a) = pretty a

494 pretty (AType a) = pretty a

488 pretty StrType = text "String"

495 pretty StrType = text "String"

496+ pretty BufferType = text "prim__UnsafeBuffer"

489 pretty PtrType = text "Ptr"

497 pretty PtrType = text "Ptr"

490 pretty VoidType = text "Void"

498 pretty VoidType = text "Void"

491 pretty Forgot = text "Forgot"

499 pretty Forgot = text "Forgot"

@@ -1031,6 +1039,7 @@ instance Show Const where

1031 show (AType (ATInt (ITFixed it))) = itBitsName it

1039 show (AType (ATInt (ITFixed it))) = itBitsName it

1032 show (AType (ATInt (ITVec it c))) = itBitsName it ++ "x" ++ show c

1040 show (AType (ATInt (ITVec it c))) = itBitsName it ++ "x" ++ show c

1033 show StrType = "String"

1041 show StrType = "String"

1042+ show BufferType = "prim__UnsafeBuffer"

1034 show PtrType = "Ptr"

1043 show PtrType = "Ptr"

1035 show VoidType = "Void"

1044 show VoidType = "Void"

1036

1045

src/Idris/IBC.hs+2

@@ -606,6 +606,7 @@ instance Binary Const where

606 B16V x1 -> putWord8 22 >> put x1

607 B32V x1 -> putWord8 23 >> put x1

608 B64V x1 -> putWord8 24 >> put x1

609+ BufferType -> putWord8 25

609 get

610 get

610 = do i <- getWord8

611 = do i <- getWord8

611 case i of

612 case i of

@@ -646,6 +647,7 @@ instance Binary Const where

646 22 -> fmap B16V get

647 22 -> fmap B16V get

647 23 -> fmap B32V get

648 23 -> fmap B32V get

648 24 -> fmap B64V get

649 24 -> fmap B64V get

650+ 25 -> return BufferType

649

651

650 _ -> error "Corrupted binary data for Const"

652 _ -> error "Corrupted binary data for Const"

651

653

src/Idris/ParseExpr.hs+8−6

@@ -992,6 +992,7 @@ Constant ::=

992 | 'Float'

993 | 'String'

994 | 'Ptr'

995+ | 'prim__UnsafeBuffer'

995 | 'Bits8'

996 | 'Bits8'

996 | 'Bits16'

997 | 'Bits16'

997 | 'Bits32'

998 | 'Bits32'

@@ -1009,12 +1010,13 @@ Constant ::=

1009@

1010@

1010-}

1011-}

1011constant :: IdrisParser Idris.Core.TT.Const

1012constant :: IdrisParser Idris.Core.TT.Const

1012−constant = do reserved "Integer";return (AType (ATInt ITBig))

1013+constant = do reserved "Integer"; return (AType (ATInt ITBig))

1013− <|> do reserved "Int"; return (AType (ATInt ITNative))

1014+ <|> do reserved "Int"; return (AType (ATInt ITNative))

1014− <|> do reserved "Char"; return (AType (ATInt ITChar))

1015+ <|> do reserved "Char"; return (AType (ATInt ITChar))

1015− <|> do reserved "Float"; return (AType ATFloat)

1016+ <|> do reserved "Float"; return (AType ATFloat)

1016− <|> do reserved "String"; return StrType

1017+ <|> do reserved "String"; return StrType

1017− <|> do reserved "Ptr"; return PtrType

1018+ <|> do reserved "Ptr"; return PtrType

1019+ <|> do reserved "prim__UnsafeBuffer"; return BufferType

1018 <|> do reserved "Bits8"; return (AType (ATInt (ITFixed IT8)))

1020 <|> do reserved "Bits8"; return (AType (ATInt (ITFixed IT8)))

1019 <|> do reserved "Bits16"; return (AType (ATInt (ITFixed IT16)))

1021 <|> do reserved "Bits16"; return (AType (ATInt (ITFixed IT16)))

1020 <|> do reserved "Bits32"; return (AType (ATInt (ITFixed IT32)))

1022 <|> do reserved "Bits32"; return (AType (ATInt (ITFixed IT32)))

src/Idris/Primitives.hs+24−9

@@ -171,9 +171,16 @@ primitives =

171 Prim (sUN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)

172 (0, LStdIn) partial,

173 Prim (sUN "prim__null") (ty [] PtrType) 0 (p_cantreduce)

174− (0, LNullPtr) total

174+ (0, LNullPtr) total,

175+

176+ -- Buffers

177+ Prim (sUN "prim__allocate") (ty [AType (ATInt (ITFixed IT64))] BufferType) 1 (p_cantreduce)

178+ (1, LAllocate) total,

179+ Prim (sUN "prim__appendBuffer") (ty [BufferType, AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), BufferType] BufferType) 6 (p_cantreduce)

180+ (6, LAppendBuffer) partial

175 ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative, ITChar]

181 ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative, ITChar]

176 ++ concatMap vecOps vecTypes

182 ++ concatMap vecOps vecTypes

183+ ++ concatMap fixedOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64] -- ITNative, ITChar, ATFloat ] ++ vecTypes

177 ++ vecBitcasts vecTypes

184 ++ vecBitcasts vecTypes

178

185

179vecTypes :: [IntTy]

186vecTypes :: [IntTy]

@@ -267,6 +274,22 @@ vecBitcasts :: [IntTy] -> [Prim]

267vecBitcasts tys = [bitcastPrim from to bitcastVec (LBitCast from to)

274vecBitcasts tys = [bitcastPrim from to bitcastVec (LBitCast from to)

268 | from <- map ATInt vecTypes, to <- map ATInt vecTypes, from /= to]

275 | from <- map ATInt vecTypes, to <- map ATInt vecTypes, from /= to]

269

276

277+fixedOps :: IntTy -> [Prim]

278+fixedOps ity@(ITFixed _) =

279+ map appendFun endiannesses ++

280+ map peekFun endiannesses

281+ where

282+ endiannesses = [ Native, LE, BE ]

283+ tyName = intTyName ity

284+ b64 = AType (ATInt (ITFixed IT64))

285+ thisTy = AType $ ATInt ity

286+ appendFun en = Prim (sUN $ "prim__append" ++ tyName ++ show en)

287+ (ty [BufferType, b64, b64, thisTy] BufferType)

288+ 4 (p_cantreduce) (4, LAppend ity en) partial

289+ peekFun en = Prim (sUN $ "prim__peek" ++ tyName ++ show en)

290+ (ty [BufferType, b64] thisTy)

291+ 2 (p_cantreduce) (2, LPeek ity en) partial

292+

270mapHalf :: (V.Unbox a, V.Unbox b) => ((a, a) -> b) -> Vector a -> Vector b

293mapHalf :: (V.Unbox a, V.Unbox b) => ((a, a) -> b) -> Vector a -> Vector b

271mapHalf f xs = V.generate (V.length xs `div` 2) (\i -> f (xs V.! (i*2), xs V.! (i*2+1)))

294mapHalf f xs = V.generate (V.length xs `div` 2) (\i -> f (xs V.! (i*2), xs V.! (i*2+1)))

272

295

@@ -368,13 +391,6 @@ aTyName :: ArithTy -> String

368aTyName (ATInt t) = intTyName t

391aTyName (ATInt t) = intTyName t

369aTyName ATFloat = "Float"

392aTyName ATFloat = "Float"

370

393

371−intTyName :: IntTy -> String

372−intTyName ITNative = "Int"

373−intTyName ITBig = "BigInt"

374−intTyName (ITFixed sized) = "B" ++ show (nativeTyWidth sized)

375−intTyName (ITChar) = "Char"

376−intTyName (ITVec ity count) = "B" ++ show (nativeTyWidth ity) ++ "x" ++ show count

377−

378iCmp :: IntTy -> String -> Bool -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim

394iCmp :: IntTy -> String -> Bool -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim

379iCmp ity op self impl irop totality

395iCmp ity op self impl irop totality

380 = Prim (sUN $ "prim__" ++ op ++ intTyName ity)

396 = Prim (sUN $ "prim__" ++ op ++ intTyName ity)

@@ -678,4 +694,3 @@ p_strRev _ = Nothing

678p_cantreduce :: a -> Maybe b

694p_cantreduce :: a -> Maybe b

679p_cantreduce _ = Nothing

695p_cantreduce _ = Nothing

680

696

681−

test/Makefile+3−3

@@ -8,13 +8,13 @@ test: $(TESTS)

8 @perl ./runtest.pl $(patsubst %.test,%,$@)

10test_java:

11− perl ./runtest.pl all --codegen Java

11+ perl ./runtest.pl without buffer001 --codegen Java

13test_js:

14− @perl ./runtest.pl without reg029 reg031 io001 dsl002 io003 effects001 effects002 basic007 --codegen node

14+ @perl ./runtest.pl without reg029 reg031 io001 dsl002 io003 effects001 effects002 basic007 buffer001 --codegen node

16test_llvm:

17− @perl ./runtest.pl without io003 basic007 --codegen llvm

17+ @perl ./runtest.pl without io003 basic007 buffer001 --codegen llvm

19update:

20 /usr/bin/env perl ./runtest.pl all -u

test/buffer001/buffer001.idrnew file+45

@@ -0,0 +1,45 @@

1+module Main

3+import Data.Buffer

5+em : Buffer 0

6+em = allocate 4

8+one : Bits32

9+one = 1

10+

11+two : Bits8

12+two = 2

13+

14+firstHalf : Buffer 4

15+firstHalf = appendBits32LE em 1 one

16+

17+full : Buffer 8

18+full = appendBits8 firstHalf 4 two

19+

20+firstByte : Bits8

21+firstByte = peekBits8 full 0

22+

23+firstHalfView : Buffer 4

24+firstHalfView = peekBuffer full 0

25+

26+firstHalfCopy : Buffer 4

27+firstHalfCopy = copy firstHalfView

28+

29+oneFromFirstHalf : Bits32

30+oneFromFirstHalf = peekBits32LE firstHalf 0

31+

32+oneFromFirstHalfCopy : Bits32

33+oneFromFirstHalfCopy = peekBits32LE firstHalfCopy 0

34+

35+viewsAndCopiesPreserveEquality : Bool

36+viewsAndCopiesPreserveEquality = ( oneFromFirstHalf == one ) && ( oneFromFirstHalfCopy == one )

37+

38+secondHalfWord : Bits32

39+secondHalfWord = peekBits32LE full 4

40+

41+main : IO ()

42+main = do

43+ putStrLn $ show firstByte

44+ putStrLn $ show viewsAndCopiesPreserveEquality

45+ putStrLn $ show secondHalfWord

test/buffer001/expectednew file+3

@@ -0,0 +1,3 @@

1+01

2+True

3+02020202

test/buffer001/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ buffer001.idr -o buffer001

3+./buffer001

4+rm -f buffer001 *.ibc