f0fe3ff · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add C codegen implementation of buffer primitives

commitf0fe3ff5860c3c62c733cdb6d1f4c6f53f0b0989 authorShea Levy <shea@shealevy.com> dateThu 30 Jan 2014, 17:12 (13 years ago) parent5750cb5

10 files changed+455−15

compare with master

unifiedsplit

rts/idris_gc.c+11−1 rts/idris_heap.c+9 rts/idris_rts.c+363 rts/idris_rts.h+50−1 src/IRTS/CodegenC.hs+7 src/IRTS/Lang.hs+5 src/Idris/Core/TT.hs+7 src/Idris/Primitives.hs−10 test/buffer001/buffer001.idr+1−1 test/buffer001/expected+2−2

rts/idris_gc.c+11−1

@@ -27,6 +27,12 @@ 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;

33+ case BUFOFFSET:

34+ cl = MKBUFOFFSETc(vm, x->info.buf_offset);

35+ break;

3036 case BIGINT:

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

3238 break;

@@ -63,7 +69,7 @@ void cheney(VM *vm) {

6369 while(scan < vm->heap.next) {

6470 size_t inc = *((size_t*)scan);

6571 VAL heap_item = (VAL)(scan+sizeof(size_t));

66− // If it's a CON or STROFFSET, copy its arguments

72+ // If it's a CON, STROFFSET, or BUFOFFSET, copy its arguments

6773 switch(GETTY(heap_item)) {

6874 case CON:

6975 ar = ARITY(heap_item);

@@ -78,6 +84,10 @@ void cheney(VM *vm) {

7884 heap_item->info.str_offset->str

7985 = copy(vm, heap_item->info.str_offset->str);

8086 break;

87+ case BUFOFFSET:

88+ heap_item->info.buf_offset->buf

89+ = copy(vm, heap_item->info.buf_offset->buf);

90+ break;

8191 default: // Nothing to copy

8292 break;

8393 }

rts/idris_heap.c+9

@@ -106,6 +106,15 @@ void heap_check_pointers(Heap * heap) {

106106 }

107107 break;

108108 }

109+ case BUFOFFSET:

110+ if (!ref_in_heap(heap, heap_item->info.buf_offset->buf)) {

111+ fprintf(stderr,

112+ "RTS ERROR: heap closure broken. "\

113+ "<HEAP %p %p %p> <REF %p>\n",

114+ heap->heap, heap->next, heap->end, heap_item->info.buf_offset->buf);

115+ exit(EXIT_FAILURE);

116+ }

117+ break;

109118 case FWD:

110119 // Check for artifacts after cheney gc.

111120 fprintf(stderr, "RTS ERROR: FWD in working heap.\n");

rts/idris_rts.c+363

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

475475 return cl;

476476}

477477

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 make_buf_offset(VM* vm, BufOffset* off, int outerlock) {

487+ Closure* cl = allocate(vm, sizeof(Closure) + sizeof *off, outerlock);

488+ SETTY(cl, BUFOFFSET);

489+ cl->info.buf_offset = (BufOffset*)((void*)cl + sizeof(Closure));

490+ memmove(cl->info.buf_offset, off, sizeof *off);

491+ return cl;

492+}

493+

494+static VAL MKBUFOFFSET(VM* vm, BufOffset* off) {

495+ return make_buf_offset(vm, off, 0);

496+}

497+

498+VAL MKBUFOFFSETc(VM* vm, BufOffset* off) {

499+ return make_buf_offset(vm, off, 1);

500+}

501+

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

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

504+

505+ // Round up to a power of 2

506+ --size;

507+ size_t i;

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

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

510+ ++size;

511+

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

513+ SETTY(cl, BUFFER);

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

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

516+ return cl;

517+}

518+

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

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

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

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

523+ return cl;

524+}

525+

526+VAL idris_copy(VM* vm, VAL len, VAL src) {

527+ size_t length = len->info.bits64;

528+ Closure* cl = internal_allocate(vm, length);

529+ memmove(cl->info.buf->store, (GETTY(src) == BUFOFFSET ?

530+ src->info.buf_offset->buf->info.buf->store + src->info.buf_offset->offset :

531+ src->info.buf->store

532+ ), length);

533+ cl->info.buf->fill = length;

534+ return cl;

535+}

536+

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

538+ while (num--) {

539+ memmove(dest, src, size);

540+ dest += size;

541+ }

542+}

543+

544+static void internal_prepare_append(VM* vm, VAL buf, size_t bufLen, size_t appLen, void** storePtr, Closure** valPtr) {

545+ size_t totalLen = bufLen + appLen;

546+ // Might be able to get rid of some duplication here...

547+ if (GETTY(buf) == BUFOFFSET) {

548+ if (buf->info.buf_offset->offset + bufLen !=

549+ buf->info.buf_offset->buf->info.buf->fill ||

550+ buf->info.buf_offset->offset + totalLen >

551+ buf->info.buf_offset->buf->info.buf->cap) {

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

553+ *valPtr = internal_allocate(vm, totalLen);

554+ memmove((*valPtr)->info.buf->store,

555+ buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset,

556+ bufLen);

557+ (*valPtr)->info.buf->fill = totalLen;

558+ *storePtr = (*valPtr)->info.buf->store + bufLen;

559+ } else {

560+ // Hooray, can just bump the fill

561+ *valPtr = MKBUFOFFSET(vm, buf->info.buf_offset);

562+ buf->info.buf_offset->buf->info.buf->fill += appLen;

563+ *storePtr = buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + bufLen;

564+ }

565+ } else {

566+ Buffer* newBuf;

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

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

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

570+ *valPtr = internal_allocate(vm, totalLen);

571+ newBuf = (*valPtr)->info.buf;

572+ memmove(newBuf->store,

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

574+ bufLen);

575+ newBuf->fill = totalLen;

576+ } else {

577+ // Hooray, can just bump the fill

578+ BufOffset off = { buf, 0 };

579+ *valPtr = MKBUFOFFSET(vm, &off);

580+ newBuf = buf->info.buf;

581+ newBuf->fill += appLen;

582+ }

583+ *storePtr = newBuf->store + bufLen;

584+ }

585+}

586+

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

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

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

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

591+ void* store;

592+ Closure *cl;

593+ internal_prepare_append(vm, fst, firstLength, count * secondLength, &store, &cl);

594+ internal_memset(store, GETTY(snd) == BUFOFFSET ?

595+ snd->info.buf_offset->buf->info.buf->store + snd->info.buf_offset->offset :

596+ snd->info.buf->store

597+ , secondLength, count);

598+ return cl;

599+}

600+

601+VAL idris_peekBuffer(VM* vm, VAL src, VAL off) {

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

603+ BufOffset b;

604+ if (GETTY(src) == BUFOFFSET) {

605+ b.buf = src->info.buf_offset->buf;

606+ b.offset = src->info.buf_offset->offset + offset;

607+ } else {

608+ b.buf = src;

609+ b.offset = offset;

610+ }

611+ return MKBUFOFFSET(vm, &b);

612+}

613+

614+// Special cased because we can use memset

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

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

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

618+ void* store;

619+ Closure* cl;

620+ internal_prepare_append(vm, buf, bufLen, count, &store, &cl);

621+ memset(store, val->info.bits8, count);

622+ return cl;

623+}

624+

625+VAL idris_appendB8LE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val) {

626+ return idris_appendB8Native(vm, buf, len, cnt, val);

627+}

628+

629+VAL idris_appendB8BE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val) {

630+ return idris_appendB8Native(vm, buf, len, cnt, val);

631+}

632+

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

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

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

636+ void* store;

637+ Closure* cl;

638+ internal_prepare_append(vm, buf, len, count * val_len, &store, &cl);

639+ internal_memset(store, val, val_len, count);

640+ return cl;

641+}

642+

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

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

645+}

646+

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

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

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

650+ // conversly on BE systems

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

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

653+ };

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

655+}

656+

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

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

659+ , val->info.bits16

660+ };

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

662+}

663+

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

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

666+}

667+

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

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

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

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

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

673+ };

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

675+}

676+

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

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

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

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

681+ , val->info.bits32

682+ };

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

684+}

685+

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

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

688+}

689+

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

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

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

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

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

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

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

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

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

699+ };

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

701+}

702+

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

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

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

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

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

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

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

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

711+ , val->info.bits64

712+ };

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

714+}

715+

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

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

718+ uint8_t* val = GETTY(buf) == BUFOFFSET ?

719+ buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + offset :

720+ buf->info.buf->store + offset;

721+ return MKB8(vm, *val);

722+}

723+

724+VAL idris_peekB8LE(VM* vm, VAL buf, VAL off) {

725+ return idris_peekB8Native(vm, buf, off);

726+}

727+

728+VAL idris_peekB8BE(VM* vm, VAL buf, VAL off) {

729+ return idris_peekB8Native(vm, buf, off);

730+}

731+

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

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

734+ uint16_t* val = (uint16_t *) ((GETTY(buf) == BUFOFFSET) ?

735+ buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + offset :

736+ buf->info.buf->store + offset);

737+ return MKB16(vm, *val);

738+}

739+

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

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

742+ unsigned char* val = (GETTY(buf) == BUFOFFSET) ?

743+ buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + offset :

744+ buf->info.buf->store + offset;

745+ return MKB16(vm, ((uint16_t) val[0]) +

746+ (((uint16_t) val[1]) << 8));

747+}

748+

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

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

751+ unsigned char* val = (GETTY(buf) == BUFOFFSET) ?

752+ buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + offset :

753+ buf->info.buf->store + offset;

754+ return MKB16(vm, ((uint16_t) val[1]) +

755+ (((uint16_t) val[0]) << 8));

756+}

757+

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

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

760+ uint32_t* val = (uint32_t *) ((GETTY(buf) == BUFOFFSET) ?

761+ buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + offset :

762+ buf->info.buf->store + offset);

763+ return MKB32(vm, *val);

764+}

765+

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

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

768+ unsigned char* val = (GETTY(buf) == BUFOFFSET) ?

769+ buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + offset :

770+ buf->info.buf->store + offset;

771+ return MKB32(vm, ((uint32_t) val[0]) +

772+ (((uint32_t) val[1]) << 8) +

773+ (((uint32_t) val[2]) << 16) +

774+ (((uint32_t) val[3]) << 24));

775+}

776+

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

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

779+ unsigned char* val = (GETTY(buf) == BUFOFFSET) ?

780+ buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + offset :

781+ buf->info.buf->store + offset;

782+ return MKB32(vm, ((uint32_t) val[3]) +

783+ (((uint32_t) val[2]) << 8) +

784+ (((uint32_t) val[1]) << 16) +

785+ (((uint32_t) val[0]) << 24));

786+}

787+

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

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

790+ uint64_t* val = (uint64_t *) ((GETTY(buf) == BUFOFFSET) ?

791+ buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + offset :

792+ buf->info.buf->store + offset);

793+ return MKB64(vm, *val);

794+}

795+

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

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

798+ unsigned char* val = (GETTY(buf) == BUFOFFSET) ?

799+ buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + offset :

800+ buf->info.buf->store + offset;

801+ return MKB64(vm, ((uint64_t) val[0]) +

802+ (((uint64_t) val[1]) << 8) +

803+ (((uint64_t) val[2]) << 16) +

804+ (((uint64_t) val[3]) << 24) +

805+ (((uint64_t) val[4]) << 32) +

806+ (((uint64_t) val[5]) << 40) +

807+ (((uint64_t) val[6]) << 48) +

808+ (((uint64_t) val[7]) << 56));

809+}

810+

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

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

813+ unsigned char* val = (GETTY(buf) == BUFOFFSET) ?

814+ buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + offset :

815+ buf->info.buf->store + offset;

816+ return MKB64(vm, ((uint64_t) val[7]) +

817+ (((uint64_t) val[6]) << 8) +

818+ (((uint64_t) val[5]) << 16) +

819+ (((uint64_t) val[4]) << 24) +

820+ (((uint64_t) val[3]) << 32) +

821+ (((uint64_t) val[2]) << 40) +

822+ (((uint64_t) val[1]) << 48) +

823+ (((uint64_t) val[0]) << 56));

824+}

825+

478826typedef struct {

479827 VM* vm; // thread's VM

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

@@ -552,6 +900,21 @@ VAL copyTo(VM* vm, VAL x) {

552900 case STRING:

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

554902 break;

903+ case BUFFER:

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

905+ break;

906+ case BUFOFFSET:

907+ // The underlying Buffer might already exist in the new heap

908+ // but we can't do anything reasonable about it

909+ if (x->info.buf_offset->offset == 0)

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

911+ else {

912+ // Could theoretically make this a bit more efficient

913+ // by allocating the BufOffset and Buffer together

914+ cl = MKBUFOFFSETc(vm, x->info.buf_offset);

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

916+ }

917+ break;

555918 case BIGINT:

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

557920 break;

rts/idris_rts.h+50−1

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

1616

1717typedef enum {

1818 CON, INT, BIGINT, FLOAT, STRING, STROFFSET,

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

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

20+ BUFFER, BUFOFFSET

2021} ClosureType;

2122

2223typedef struct Closure *VAL;

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

3132 int offset;

3233} StrOffset;

3334

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+typedef struct {

44+ VAL buf;

45+ size_t offset;

46+} BufOffset;

47+

48+

3449typedef struct Closure {

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

3651// Bottom 16 bits for closure type

@@ -46,6 +61,8 @@ typedef struct Closure {

4661 uint16_t bits16;

4762 uint32_t bits32;

4863 uint64_t bits64;

64+ Buffer* buf;

65+ BufOffset* buf_offset;

4966 } info;

5067} Closure;

5168

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

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

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

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

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

183+VAL MKBUFOFFSETc(VM* vm, BufOffset* off);

165184

166185char* GETSTROFF(VAL stroff);

167186

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

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

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

236255

256+// Buffer primitives

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

258+VAL idris_copy(VM* vm, VAL len, VAL src);

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

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

261+VAL 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);

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

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

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

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

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

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

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

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

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

273+VAL 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);

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

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

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

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

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

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

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

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

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

285+

237286// Command line args

238287

239288extern int __idris_argc;

src/IRTS/CodegenC.hs+7

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

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

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

459459

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

461+doOp v LCopy [x, y] = v ++ "idris_copy(vm, " ++ creg x ++ "," ++ creg y ++ ")"

462+doOp v LAppendBufferNative [a, b, c, d, e] = v ++ "idris_appendBuffer(vm, " ++ creg a ++ "," ++ creg b ++ "," ++ creg c ++ "," ++ creg d ++ "," ++ creg e ++ ")"

463+doOp v LPeekBufferNative [x, y] = v ++ "idris_peekBuffer(vm, " ++ creg x ++ "," ++ creg y ++ ")"

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

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

466+

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

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

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

src/IRTS/Lang.hs+5

@@ -7,6 +7,11 @@ import Debug.Trace

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

10+enName :: Endianness -> String

11+enName Native = "Native"

12+enName BE = "BE"

13+enName LE = "LE"

14+

1015data LVar = Loc Int | Glob Name

1116 deriving (Show, Eq)

1217

src/Idris/Core/TT.hs+7

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

434434 | ITVec NativeTy Int

435435 deriving (Show, Eq, Ord)

436436

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+

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

438445 deriving (Show, Eq, Ord)

439446{-!

src/Idris/Primitives.hs−10

@@ -284,9 +284,6 @@ fixedOps ity@(ITFixed _) =

284284 map peekFun endiannesses

285285 where

286286 endiannesses = [ Native, LE, BE ]

287− enName LE = "LE"

288− enName BE = "BE"

289− enName Native = "Native"

290287 tyName = intTyName ity

291288 b64 = AType (ATInt (ITFixed IT64))

292289 thisTy = AType $ ATInt ity

@@ -398,13 +395,6 @@ aTyName :: ArithTy -> String

398395aTyName (ATInt t) = intTyName t

399396aTyName ATFloat = "Float"

400397

401−intTyName :: IntTy -> String

402−intTyName ITNative = "Int"

403−intTyName ITBig = "BigInt"

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

405−intTyName (ITChar) = "Char"

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

407−

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

409399iCmp ity op self impl irop totality

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

test/buffer001/buffer001.idr+1−1

@@ -36,7 +36,7 @@ viewsAndCopiesPreserveEquality : Bool

3636viewsAndCopiesPreserveEquality = ( oneFromFirstHalf == one ) && ( oneFromFirstHalfCopy == one )

3737

3838secondHalfWord : Bits32

39−secondHalfWord = peekBits32LE full 1

39+secondHalfWord = peekBits32LE full 4

4040

4141main : IO ()

4242main = do

test/buffer001/expected+2−2

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

1−1

1+01

22True

3−33686018

3+02020202