c413280 · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -342,6 +342,9 @@ Extra-source-files:

342 test/basic012/run

343 test/basic012/*.idr

344 test/basic012/expected

345+ test/basic013/run

346+ test/basic013/*.idr

347+ test/basic013/expected

345

348

346 test/buffer001-disabled/*.idr

349 test/buffer001-disabled/*.idr

347 test/buffer001-disabled/run

350 test/buffer001-disabled/run

rts/Makefile+3−2

@@ -1,9 +1,10 @@

1include ../config.mk

2

3OBJS = idris_rts.o idris_heap.o idris_gc.o idris_gmp.o idris_bitstring.o \

4− idris_opts.o idris_stats.o mini-gmp.o

4+ idris_opts.o idris_stats.o idris_utf8.o mini-gmp.o

5HDRS = idris_rts.h idris_heap.h idris_gc.h idris_gmp.h idris_bitstring.h \

6− idris_opts.h idris_stats.h mini-gmp.h idris_stdfgn.h idris_net.h

6+ idris_opts.h idris_stats.h mini-gmp.h idris_stdfgn.h idris_net.h \

7+ idris_utf8.h

7CFLAGS:=-fPIC $(CFLAGS)

8CFLAGS:=-fPIC $(CFLAGS)

8CFLAGS += $(GMP_INCLUDE_DIR) $(GMP) -DIDRIS_TARGET_OS="\"$(OS)\""

9CFLAGS += $(GMP_INCLUDE_DIR) $(GMP) -DIDRIS_TARGET_OS="\"$(OS)\""

9CFLAGS += -DIDRIS_TARGET_TRIPLE="\"$(MACHINE)\""

10CFLAGS += -DIDRIS_TARGET_TRIPLE="\"$(MACHINE)\""

rts/idris_rts.c+29−20

@@ -2,6 +2,7 @@

2

3#include "idris_rts.h"

4#include "idris_gc.h"

5+#include "idris_utf8.h"

5#include "idris_bitstring.h"

6#include "idris_bitstring.h"

6

7

7#ifdef HAS_PTHREAD

8#ifdef HAS_PTHREAD

@@ -596,7 +597,7 @@ VAL idris_streq(VM* vm, VAL l, VAL r) {

596}

597}

597

598

598VAL idris_strlen(VM* vm, VAL l) {

599VAL idris_strlen(VM* vm, VAL l) {

599− return MKINT((i_int)(strlen(GETSTR(l))));

600+ return MKINT((i_int)(idris_utf8_strlen(GETSTR(l))));

600}

601}

601

602

602#define BUFSIZE 256

603#define BUFSIZE 256

@@ -647,7 +648,7 @@ VAL idris_readStr(VM* vm, FILE* h) {

647}

648}

648

649

649VAL idris_strHead(VM* vm, VAL str) {

650VAL idris_strHead(VM* vm, VAL str) {

650− return MKINT((i_int)(GETSTR(str)[0]));

651+ return idris_strIndex(vm, str, 0);

651}

652}

652

653

653VAL MKSTROFFc(VM* vm, StrOffset* off) {

654VAL MKSTROFFc(VM* vm, StrOffset* off) {

@@ -679,27 +680,41 @@ VAL idris_strTail(VM* vm, VAL str) {

679 }

680 }

680

681

681 cl->info.str_offset->str = root;

682 cl->info.str_offset->str = root;

682− cl->info.str_offset->offset = offset+1;

683+ cl->info.str_offset->offset = offset+idris_utf8_charlen(GETSTR(str));

683

684

684 return cl;

685 return cl;

685 } else {

686 } else {

687+ char* nstr = GETSTR(str);

686− return MKSTR(vm, GETSTR(str)+1);

688+ return MKSTR(vm, nstr+idris_utf8_charlen(nstr));

687 }

689 }

688}

690}

689

691

690VAL idris_strCons(VM* vm, VAL x, VAL xs) {

692VAL idris_strCons(VM* vm, VAL x, VAL xs) {

691 char *xstr = GETSTR(xs);

693 char *xstr = GETSTR(xs);

694+ int xval = GETINT(x);

695+ if ((xval & 0x80) == 0) { // ASCII char

692− Closure* cl = allocate(sizeof(Closure) +

696+ Closure* cl = allocate(sizeof(Closure) +

693− strlen(xstr) + 2, 0);

697+ strlen(xstr) + 2, 0);

694− SETTY(cl, STRING);

698+ SETTY(cl, STRING);

695− cl -> info.str = (char*)cl + sizeof(Closure);

699+ cl -> info.str = (char*)cl + sizeof(Closure);

696− cl -> info.str[0] = (char)(GETINT(x));

700+ cl -> info.str[0] = (char)(GETINT(x));

697− strcpy(cl -> info.str+1, xstr);

701+ strcpy(cl -> info.str+1, xstr);

702+ return cl;

703+ } else {

704+ char *init = idris_utf8_fromChar(xval);

705+ Closure* cl = allocate(sizeof(Closure) + strlen(init) + strlen(xstr) + 1, 0);

706+ SETTY(cl, STRING);

707+ cl -> info.str = (char*)cl + sizeof(Closure);

708+ strcpy(cl -> info.str, init);

709+ strcat(cl -> info.str, xstr);

710+ free(init);

698− return cl;

711+ return cl;

712+ }

699}

713}

700

714

701VAL idris_strIndex(VM* vm, VAL str, VAL i) {

715VAL idris_strIndex(VM* vm, VAL str, VAL i) {

702− return MKINT((i_int)(GETSTR(str)[GETINT(i)]));

716+ int idx = idris_utf8_index(GETSTR(str), GETINT(i));

717+ return MKINT((i_int)idx);

703}

718}

704

719

705VAL idris_strRev(VM* vm, VAL str) {

720VAL idris_strRev(VM* vm, VAL str) {

@@ -707,14 +722,8 @@ VAL idris_strRev(VM* vm, VAL str) {

707 Closure* cl = allocate(sizeof(Closure) +

722 Closure* cl = allocate(sizeof(Closure) +

708 strlen(xstr) + 1, 0);

723 strlen(xstr) + 1, 0);

709 SETTY(cl, STRING);

724 SETTY(cl, STRING);

710− cl -> info.str = (char*)cl + sizeof(Closure);

725+ cl->info.str = (char*)cl + sizeof(Closure);

711− int y = 0;

712− int x = strlen(xstr);

713−

714− cl-> info.str[x+1] = '\0';

726+ idris_utf8_rev(xstr, cl->info.str);

715− while(x>0) {

716− cl -> info.str[y++] = xstr[--x];

717− }

718 return cl;

727 return cl;

719}

728}

720

729

rts/idris_rts.h+2

@@ -335,6 +335,8 @@ VAL idris_readStr(VM* vm, FILE* h);

335

336VAL idris_strHead(VM* vm, VAL str);

337VAL idris_strTail(VM* vm, VAL str);

338+// This is not expected to be efficient! Mostly we wouldn't expect to call

339+// it at all at run time.

338VAL idris_strCons(VM* vm, VAL x, VAL xs);

340VAL idris_strCons(VM* vm, VAL x, VAL xs);

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

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

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

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

rts/idris_utf8.cnew file+144

@@ -0,0 +1,144 @@

1+#include "idris_utf8.h"

2+#include <stdio.h>

3+#include <string.h>

4+#include <stdlib.h>

5+

6+int idris_utf8_strlen(char *s) {

7+ int i = 0, j = 0;

8+ while (s[i]) {

9+ if ((s[i] & 0xc0) != 0x80) j++;

10+ i++;

11+ }

12+ return j;

13+}

14+

15+int idris_utf8_charlen(char* s) {

16+ int init = (int)s[0];

17+ if ((init & 0x80) == 0) {

18+ return 1; // Top bit unset, so 1 byte

19+ }

20+ if ((init > 244 && init < 256) ||

21+ (init == 192) ||

22+ (init == 193)) {

23+ return 1; // Invalid characters

24+ }

25+ int i = 1;

26+ while ((s[i] & 0xc0) == 0x80) {

27+ i++; // Move on until top 2 bits are not 10

28+ }

29+ return i;

30+}

31+

32+unsigned idris_utf8_index(char* s, int idx) {

33+ int i = 0, j = 0;

34+ while (j < idx) {

35+ if ((s[i] & 0xc0) != 0x80) j++;

36+ i++;

37+ }

38+ // Find the start of the next character

39+ while ((s[i] & 0xc0) == 0x80) { i++; }

40+

41+ unsigned bytes = 0;

42+ unsigned top = 0;

43+

44+ int init = (int)s[1];

45+

46+ // s[i] is now the start of the character we want

47+ if ((s[i] & 0x80) == 0) {

48+ bytes = 1;

49+ top = (int)(s[i]);

50+ } else if ((init > 244 && init < 256) ||

51+ (init == 192) ||

52+ (init == 193)) {

53+ bytes = 1;

54+ top = (int)(s[i]); // Invalid characters

55+ } else if ((s[i] & 0xe0) == 0xc0) {

56+ bytes = 2;

57+ top = (int)(s[i] & 0x1f); // 5 bits

58+ } else if ((s[i] & 0xf0) == 0xe0) {

59+ bytes = 3;

60+ top = (int)(s[i] & 0x0f); // 4 bits

61+ } else if ((s[i] & 0xf8) == 0xf0) {

62+ bytes = 4;

63+ top = (int)(s[i] & 0x07); // 3 bits

64+ } else if ((s[i] & 0xfc) == 0xf8) {

65+ bytes = 5;

66+ top = (int)(s[i] & 0x03); // 2 bits

67+ } else if ((s[i] & 0xfe) == 0xfc) {

68+ bytes = 6;

69+ top = (int)(s[i] & 0x01); // 1 bits

70+ }

71+

72+ while (bytes > 1) {

73+ top = top << 6;

74+ top += s[++i] & 0x3f; // 6 bits

75+ --bytes;

76+ }

77+

78+ return top;

79+}

80+

81+char* idris_utf8_fromChar(int x) {

82+ char* str;

83+ int bytes = 0, top = 0;

84+

85+ if ((x & 0x80) == 0) {

86+ str = malloc(2);

87+ str[0] = (char)x;

88+ str[1] = '\0';

89+ return str;

90+ }

91+

92+ if (x >= 0x80 && x <= 0x7ff) {

93+ bytes = 2;

94+ top = 0xc0;

95+ } else if (x >= 0x800 && x <= 0xffff) {

96+ bytes = 3;

97+ top = 0xe0;

98+ } else if (x >= 0x10000 && x <= 0x10ffff) {

99+ bytes = 4;

100+ top = 0xf0;

101+ }

102+

103+ str = malloc(bytes + 1);

104+ str[bytes] = '\0';

105+ while(bytes > 0) {

106+ int xbits = x & 0x3f; // Next 6 bits

107+ bytes--;

108+ if (bytes > 0) {

109+ str[bytes] = (char)xbits + 0x80;

110+ } else {

111+ str[0] = (char)xbits + top;

112+ }

113+ x = x >> 6;

114+ }

115+

116+ return str;

117+}

118+

119+void reverse_range(char *start, char *end)

120+{

121+ while(start < end)

122+ {

123+ char c = *start;

124+ *start++ = *end;

125+ *end-- = c;

126+ }

127+}

128+

129+char* reverse_char(char *start)

130+{

131+ char *end = start;

132+ while((end[1] & 0xc0) == 0x80) { end++; }

133+ reverse_range(start, end);

134+ return(end + 1);

135+}

136+

137+char* idris_utf8_rev(char* s, char* result) {

138+ strcpy(result, s);

139+ char* end = result;

140+ while(*end) { end = reverse_char(end); }

141+ reverse_range(result, end-1);

142+ return result;

143+}

144+

rts/idris_utf8.hnew file+22

@@ -0,0 +1,22 @@

1+#ifndef _IDRIS_UTF8

2+#define _IDRIS_UTF8

3+

4+/* Various functions for dealing with UTF8 encoding. These are probably

5+ not very efficient (and I'm (EB) making no guarantees about their

6+ correctness.) Nevertheless, they mean that we can treat Strings as

7+ UFT8. Patches welcome :). */

8+

9+// Get length of a UTF8 encoded string in characters

10+int idris_utf8_strlen(char *s);

11+// Get number of bytes the first character takes in a string

12+int idris_utf8_charlen(char* s);

13+// Return int representation of string at an index.

14+// Assumes in bounds.

15+unsigned idris_utf8_index(char* s, int j);

16+// Convert a char as an integer to a char* as a byte sequence

17+// Null terminated; caller responsible for freeing

18+char* idris_utf8_fromChar(int x);

19+// Reverse a UTF8 encoded string, putting the result in 'result'

20+char* idris_utf8_rev(char* s, char* result);

21+

22+#endif

src/IRTS/CodegenC.hs+28−7

@@ -12,6 +12,7 @@ import Util.System

12

13import Numeric

14import Data.Char

15+import Data.Bits

15import Data.List (intercalate)

16import Data.List (intercalate)

16import qualified Data.Vector.Unboxed as V

17import qualified Data.Vector.Unboxed as V

17import System.Process

18import System.Process

@@ -145,8 +146,26 @@ showCStr s = '"' : foldr ((++) . showChar) "\"" s

145 | ord c < 0x10 = "\"\"\\x0" ++ showHex (ord c) "\"\""

146 | ord c < 0x10 = "\"\"\\x0" ++ showHex (ord c) "\"\""

146 | ord c < 0x20 = "\"\"\\x" ++ showHex (ord c) "\"\""

147 | ord c < 0x20 = "\"\"\\x" ++ showHex (ord c) "\"\""

147 | ord c < 0x7f = [c] -- 0x7f = \DEL

148 | ord c < 0x7f = [c] -- 0x7f = \DEL

148− | ord c < 0x100 = "\"\"\\x" ++ showHex (ord c) "\"\""

149+ | otherwise = showHexes (utf8bytes (ord c))

149− | otherwise = error $ "non-8-bit character in string literal: " ++ show c

150+

151+ utf8bytes :: Int -> [Int]

152+ utf8bytes x = let (h : bytes) = split [] x in

153+ headHex h (length bytes) : map toHex bytes

154+ where

155+ split acc 0 = acc

156+ split acc x = let xbits = x .&. 0x3f

157+ xrest = shiftR x 6 in

158+ split (xbits : acc) xrest

159+

160+ headHex h 1 = h + 0xc0

161+ headHex h 2 = h + 0xe0

162+ headHex h 3 = h + 0xf0

163+ headHex h n = error "Can't happen: Invalid UTF8 character"

164+

165+ toHex i = i + 0x80

166+

167+ showHexes = foldr ((++) . showUTF8) ""

168+ showUTF8 c = "\"\"\\x" ++ showHex c "\"\""

150

169

151bcc :: Int -> BC -> String

170bcc :: Int -> BC -> String

152bcc i (ASSIGN l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"

171bcc i (ASSIGN l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"

@@ -424,11 +443,6 @@ doOp v (LSLe (ATInt ITBig)) [l, r] = v ++ "idris_bigLe(vm, " ++ creg l ++ ", " +

424doOp v (LSGt (ATInt ITBig)) [l, r] = v ++ "idris_bigGt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

443doOp v (LSGt (ATInt ITBig)) [l, r] = v ++ "idris_bigGt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

425doOp v (LSGe (ATInt ITBig)) [l, r] = v ++ "idris_bigGe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

444doOp v (LSGe (ATInt ITBig)) [l, r] = v ++ "idris_bigGe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

426

445

427−doOp v LStrConcat [l,r] = v ++ "idris_concat(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

428−doOp v LStrLt [l,r] = v ++ "idris_strlt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

429−doOp v LStrEq [l,r] = v ++ "idris_streq(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

430−doOp v LStrLen [x] = v ++ "idris_strlen(vm, " ++ creg x ++ ")"

431−

432doOp v (LIntFloat ITNative) [x] = v ++ "idris_castIntFloat(" ++ creg x ++ ")"

446doOp v (LIntFloat ITNative) [x] = v ++ "idris_castIntFloat(" ++ creg x ++ ")"

433doOp v (LFloatInt ITNative) [x] = v ++ "idris_castFloatInt(" ++ creg x ++ ")"

447doOp v (LFloatInt ITNative) [x] = v ++ "idris_castFloatInt(" ++ creg x ++ ")"

434doOp v (LSExt ITNative ITBig) [x] = v ++ "idris_castIntBig(vm, " ++ creg x ++ ")"

448doOp v (LSExt ITNative ITBig) [x] = v ++ "idris_castIntBig(vm, " ++ creg x ++ ")"

@@ -529,11 +543,18 @@ doOp v LFFloor [x] = v ++ flUnOp "floor" (creg x)

529doOp v LFCeil [x] = v ++ flUnOp "ceil" (creg x)

543doOp v LFCeil [x] = v ++ flUnOp "ceil" (creg x)

530doOp v LFNegate [x] = v ++ "MKFLOAT(vm, -GETFLOAT(" ++ (creg x) ++ "))"

544doOp v LFNegate [x] = v ++ "MKFLOAT(vm, -GETFLOAT(" ++ (creg x) ++ "))"

531

545

546+-- String functions which don't need to know we're UTF8

547+doOp v LStrConcat [l,r] = v ++ "idris_concat(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

548+doOp v LStrLt [l,r] = v ++ "idris_strlt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

549+doOp v LStrEq [l,r] = v ++ "idris_streq(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

550+

551+-- String functions which need to know we're UTF8

532doOp v LStrHead [x] = v ++ "idris_strHead(vm, " ++ creg x ++ ")"

552doOp v LStrHead [x] = v ++ "idris_strHead(vm, " ++ creg x ++ ")"

533doOp v LStrTail [x] = v ++ "idris_strTail(vm, " ++ creg x ++ ")"

553doOp v LStrTail [x] = v ++ "idris_strTail(vm, " ++ creg x ++ ")"

534doOp v LStrCons [x, y] = v ++ "idris_strCons(vm, " ++ creg x ++ "," ++ creg y ++ ")"

554doOp v LStrCons [x, y] = v ++ "idris_strCons(vm, " ++ creg x ++ "," ++ creg y ++ ")"

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

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

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

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

557+doOp v LStrLen [x] = v ++ "idris_strlen(vm, " ++ creg x ++ ")"

537

558

538doOp v LAllocate [x] = v ++ "idris_buffer_allocate(vm, " ++ creg x ++ ")"

559doOp v LAllocate [x] = v ++ "idris_buffer_allocate(vm, " ++ creg x ++ ")"

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

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

test/basic013/basic013.idrnew file+34

@@ -0,0 +1,34 @@

1+foo : String

2+foo = "λx→x"

3+

4+bar : String

5+bar = "λx→x"

6+

7+baz : Char

8+baz = 'λ'

9+

10+quux : String

11+quux = "\x0a\x80\xC9\xFF\n3\n4"

12+

13+appMany : Nat -> String

14+appMany Z = foo

15+appMany (S k) = bar ++ appMany k

16+

17+main : IO ()

18+main = do putStrLn foo

19+ putStrLn (foo ++ bar)

20+ putStrLn (reverse (foo ++ bar))

21+ printLn (length foo)

22+ printLn baz

23+ let x = 4

24+ let newstr = appMany (toNat x)

25+ putStrLn newstr

26+ printLn (strHead newstr)

27+ printLn (length newstr)

28+ printLn (strIndex newstr 4)

29+ putStrLn (strCons (strIndex newstr 4) "")

30+ putStrLn ("Tail: " ++ strTail newstr)

31+ putStrLn ("Tail Tail: " ++ strTail (strTail newstr))

32+ putStrLn ("Cons: " ++ strCons 'λ' newstr)

33+ putStrLn ("Reverse: " ++ reverse newstr)

34+

test/basic013/expectednew file+14

@@ -0,0 +1,14 @@

1+λx→x

2+λx→xλx→x

3+x→xλx→xλ

4+4

5+'\955'

6+λx→xλx→xλx→xλx→xλx→x

7+'\955'

8+20

9+'\955'

10+λ

11+Tail: x→xλx→xλx→xλx→xλx→x

12+Tail Tail: →xλx→xλx→xλx→xλx→x

13+Cons: λλx→xλx→xλx→xλx→xλx→x

14+Reverse: x→xλx→xλx→xλx→xλx→xλ

test/basic013/runnew file+4

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

1+#!/usr/bin/env bash

2+idris $@ basic013.idr -o basic013

3+./basic013

4+rm -f basic013 *.ibc