c413280 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

String in C is now UTF8 encoded

Primitives for head/tail/index/cons/reverse/length now all assume the char* is UTF8 encoded. Also updated generation of literals to encode as UTF8. Primitives are probably not as efficient as they could be (though some of the will be used rarely) ASCII strings will work exactly as before. Everything I know about UTF8 encoding has been learned in the past few hours. Therefore, this is unlikely to be the best way to do this. Please educate me, ideally in the form of annotated Pull Requests :).

commitc4132807f03c338b7dd04282b7c2440e13ab573f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 28 Mar 2015, 17:09 (12 years ago) parentd0b8bb5

10 files changed+283−29

compare with master

unifiedsplit

idris.cabal+3 rts/Makefile+3−2 rts/idris_rts.c+29−20 rts/idris_rts.h+2 rts/idris_utf8.c+144 rts/idris_utf8.h+22 src/IRTS/CodegenC.hs+28−7 test/basic013/basic013.idr+34 test/basic013/expected+14 test/basic013/run+4

idris.cabal+3

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

342342 test/basic012/run

343343 test/basic012/*.idr

344344 test/basic012/expected

345+ test/basic013/run

346+ test/basic013/*.idr

347+ test/basic013/expected

345348

346349 test/buffer001-disabled/*.idr

347350 test/buffer001-disabled/run

rts/Makefile+3−2

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

11include ../config.mk

33OBJS = 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

55HDRS = 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

78CFLAGS:=-fPIC $(CFLAGS)

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

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

rts/idris_rts.c+29−20

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

33#include "idris_rts.h"

44#include "idris_gc.h"

5+#include "idris_utf8.h"

56#include "idris_bitstring.h"

78#ifdef HAS_PTHREAD

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

596597}

597598

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

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

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

600601}

601602

602603#define BUFSIZE 256

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

647648}

648649

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

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

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

651652}

652653

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

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

679680 }

680681

681682 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));

683684

684685 return cl;

685686 } else {

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

687+ char* nstr = GETSTR(str);

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

687689 }

688690}

689691

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

691693 char *xstr = GETSTR(xs);

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

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

694− SETTY(cl, STRING);

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

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

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

698− return cl;

694+ int xval = GETINT(x);

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

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

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

698+ SETTY(cl, STRING);

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

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

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);

711+ return cl;

712+ }

699713}

700714

701715VAL 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);

703718}

704719

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

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

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

708723 strlen(xstr) + 1, 0);

709724 SETTY(cl, STRING);

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

711− int y = 0;

712− int x = strlen(xstr);

713−

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

715− while(x>0) {

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

717− }

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

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

718727 return cl;

719728}

720729

rts/idris_rts.h+2

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

335335

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

337337VAL 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.

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

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

340342VAL 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>

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

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 :). */

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

1212

1313import Numeric

1414import Data.Char

15+import Data.Bits

1516import Data.List (intercalate)

1617import qualified Data.Vector.Unboxed as V

1718import System.Process

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

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

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

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

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

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

149+ | otherwise = showHexes (utf8bytes (ord 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 "\"\""

150169

151170bcc :: Int -> BC -> String

152171bcc 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 ++ ", " +

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

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

426445

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−

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

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

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

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

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

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

531545

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

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

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

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

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

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

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

537558

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

539560doOp 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"

4+bar : String

5+bar = "λx→x"

7+baz : Char

8+baz = 'λ'

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