f4352a7 · Idris-dev · git.iko.soy

CHANGELOG+2

compare with master

unifiedsplit

@@ -7,6 +7,8 @@ Language updates

7* Improved unification by implementing a pattern unification rule

8* The syntax `{{n}} quotes n without resolving it, allowing short syntax

9 for defining new names. `{n} still quotes n to an existing name in scope.

10+* A new primitive operator prim__strSubstr for more efficient extraction of

11+ substrings. External code generators should implement this.

10

12

11Library updates

13Library updates

12---------------

14---------------

idris.cabal+1

@@ -550,6 +550,7 @@ Extra-source-files:

550 test/primitives001/run

551 test/primitives001/*.idr

552 test/primitives001/expected

553+ test/primitives001/input

553 test/primitives002/run

554 test/primitives002/run

554 test/primitives002/expected

555 test/primitives002/expected

555 test/primitives003/run

556 test/primitives003/run

libs/prelude/Prelude/Strings.idr+9−6

@@ -308,12 +308,15 @@ length : String -> Nat

308length = fromInteger . prim__zextInt_BigInt . prim_lenString

309

310||| Returns a substring of a given string

311+|||

311−||| @index The (zero based) index of the string to extract. If this is

312+||| @ index The (zero based) index of the string to extract. If this is

312−||| beyond the end of the String, the function returns the empty string.

313+||| beyond the end of the string, the function returns the empty

314+||| string.

313−||| @len The desired length of the substring. Truncated if this exceeds

315+||| @ len The desired length of the substring. Truncated if this exceeds

314−||| the length of the input.

316+||| the length of the input.

317+||| @ subject The string to return a portion of

315−substr : (index : Nat) -> (len : Nat) -> String -> String

318+substr : (index : Nat) -> (len : Nat) -> (subject : String) -> String

316−substr i len = pack . List.take len . drop i . unpack

319+substr i len subject = prim__strSubstr (cast i) (cast len) subject

317

320

318||| Lowercases all characters in the string.

321||| Lowercases all characters in the string.

319|||

322|||

rts/idris_rts.c+11

@@ -594,6 +594,17 @@ VAL idris_strIndex(VM* vm, VAL str, VAL i) {

594 return MKINT((i_int)idx);

595}

596

597+VAL idris_substr(VM* vm, VAL offset, VAL length, VAL str) {

598+ char *start = idris_utf8_advance(GETSTR(str), GETINT(offset));

599+ char *end = idris_utf8_advance(start, GETINT(length));

600+ Closure* newstr = allocate(sizeof(Closure) + (end - start) +1, 0);

601+ SETTY(newstr, STRING);

602+ newstr -> info.str = (char*)newstr + sizeof(Closure);

603+ memcpy(newstr -> info.str, start, end - start);

604+ *(newstr -> info.str + (end - start) + 1) = '\0';

605+ return newstr;

606+}

607+

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

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

598 char *xstr = GETSTR(str);

609 char *xstr = GETSTR(str);

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

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

rts/idris_rts.h+1

@@ -314,6 +314,7 @@ VAL idris_strTail(VM* vm, VAL str);

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

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

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

317+VAL idris_substr(VM* vm, VAL offset, VAL length, VAL str);

317

318

318// system infox

319// system infox

319// used indices:

320// used indices:

rts/idris_utf8.c+26

@@ -78,6 +78,32 @@ unsigned idris_utf8_index(char* s, int idx) {

78 return top;

79}

80

81+char* idris_utf8_advance(char* str, int i) {

82+ while (i > 0 && *str != '\0') {

83+ // In a UTF8 single-byte char, the highest bit is 0. In the

84+ // first byte of a multi-byte char, the highest two bits are

85+ // 11, but the rest of the bytes start with 10. So we can

86+ // decrement our character counter when we see something other

87+ // than 10 at the front.

88+

89+ // This is a bit of an overapproximation, as invalid multibyte

90+ // sequences that are too long will be treated as if they are

91+ // OK, but it's always paying attention to null-termination.

92+ if ((*str & 0xc0) != 0x80) {

93+ i--;

94+ }

95+ str++;

96+ }

97+ // Now we've found the first byte of the last character. Advance

98+ // to the end of it, or the end of the string, whichever is first.

99+ // Here, we don't risk overrunning the end of the string because

100+ // ('\0' & 0xc0) != 0x80.

101+ while ((*str & 0xc0) == 0x80) { str++; }

102+

103+ return str;

104+}

105+

106+

81char* idris_utf8_fromChar(int x) {

107char* idris_utf8_fromChar(int x) {

82 char* str;

108 char* str;

83 int bytes = 0, top = 0;

109 int bytes = 0, top = 0;

rts/idris_utf8.h+3−1

@@ -18,5 +18,7 @@ unsigned idris_utf8_index(char* s, int j);

18char* idris_utf8_fromChar(int x);

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

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

21−

21+// Advance a pointer into a string by i UTF8 characters.

22+// Return original pointer if i <= 0.

23+char* idris_utf8_advance(char* str, int i);

22#endif

24#endif

src/IRTS/CodegenC.hs+1

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

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

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

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

562+doOp v LStrSubstr [x,y,z] = v ++ "idris_substr(vm, " ++ creg x ++ "," ++ creg y ++ "," ++ creg z ++ ")"

562

563

563doOp v LFork [x] = v ++ "MKPTR(vm, vmThread(vm, " ++ cname (sMN 0 "EVAL") ++ ", " ++ creg x ++ "))"

564doOp v LFork [x] = v ++ "MKPTR(vm, vmThread(vm, " ++ cname (sMN 0 "EVAL") ++ ", " ++ creg x ++ "))"

564doOp v LPar [x] = v ++ creg x -- "MKPTR(vm, vmThread(vm, " ++ cname (MN 0 "EVAL") ++ ", " ++ creg x ++ "))"

565doOp v LPar [x] = v ++ creg x -- "MKPTR(vm, vmThread(vm, " ++ cname (MN 0 "EVAL") ++ ", " ++ creg x ++ "))"

src/IRTS/CodegenJavaScript.hs+9

@@ -1140,6 +1140,15 @@ jsOP _ reg op args = JSAssign (translateReg reg) jsOP'

1140 JSNum (JSInt 1),

1141 JSBinOp "-" (JSProj v "length") (JSNum (JSInt 1))

1142 ]

1143+ | LStrSubstr <- op

1144+ , (offset:length:string:_) <- args =

1145+ let off = translateReg offset

1146+ len = translateReg length

1147+ str = translateReg string

1148+ in JSApp (JSProj str "substr") [

1149+ jsCall "Math.max" [JSNum (JSInt 0), off],

1150+ jsCall "Math.max" [JSNum (JSInt 0), len]

1151+ ]

1143

1152

1144 | LSystemInfo <- op

1153 | LSystemInfo <- op

1145 , (arg:_) <- args = jsCall "i$systemInfo" [translateReg arg]

1154 , (arg:_) <- args = jsCall "i$systemInfo" [translateReg arg]

src/IRTS/Lang.hs+1−1

@@ -74,7 +74,7 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

75 | LFSqrt | LFFloor | LFCeil | LFNegate

76

78 | LReadStr | LWriteStr

79

80 -- system info

src/Idris/DeepSeq.hs+1

@@ -84,6 +84,7 @@ instance NFData PrimFn where

84 rnf (LStrCons) = ()

85 rnf (LStrIndex) = ()

86 rnf (LStrRev) = ()

87+ rnf (LStrSubstr) = ()

87 rnf (LReadStr) = ()

88 rnf (LReadStr) = ()

88 rnf (LWriteStr) = ()

89 rnf (LWriteStr) = ()

89 rnf (LSystemInfo) = ()

90 rnf (LSystemInfo) = ()

src/Idris/Primitives.hs+8−1

@@ -15,6 +15,8 @@ import Data.Char

15import Data.Function (on)

16import qualified Data.Vector.Unboxed as V

17

18+import Debug.Trace

19+

18data Prim = Prim { p_name :: Name,

20data Prim = Prim { p_name :: Name,

19 p_type :: Type,

21 p_type :: Type,

20 p_arity :: Int,

22 p_arity :: Int,

@@ -165,6 +167,8 @@ primitives =

165 (2, LStrIndex) partial,

167 (2, LStrIndex) partial,

166 Prim (sUN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

168 Prim (sUN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

167 (1, LStrRev) total,

169 (1, LStrRev) total,

170+ Prim (sUN "prim__strSubstr") (ty [AType (ATInt ITNative), AType (ATInt ITNative), StrType] StrType) 3 (p_strSubstr)

171+ (3, LStrSubstr) total,

168

172

169 Prim (sUN "prim__readString") (ty [WorldType] StrType) 1 (p_cantreduce)

173 Prim (sUN "prim__readString") (ty [WorldType] StrType) 1 (p_cantreduce)

170 (1, LReadStr) total, -- total is okay, because we have 'WorldType'

174 (1, LReadStr) total, -- total is okay, because we have 'WorldType'

@@ -493,7 +497,7 @@ p_floatSqrt = p_fPrim sqrt

493p_floatFloor = p_fPrim (fromInteger . floor)

497p_floatFloor = p_fPrim (fromInteger . floor)

494p_floatCeil = p_fPrim (fromInteger . ceiling)

498p_floatCeil = p_fPrim (fromInteger . ceiling)

495

499

496−p_strLen, p_strHead, p_strTail, p_strIndex, p_strCons, p_strRev :: [Const] -> Maybe Const

500+p_strLen, p_strHead, p_strTail, p_strIndex, p_strCons, p_strRev, p_strSubstr :: [Const] -> Maybe Const

497p_strLen [Str xs] = Just $ I (length xs)

501p_strLen [Str xs] = Just $ I (length xs)

498p_strLen _ = Nothing

502p_strLen _ = Nothing

499p_strHead [Str (x:xs)] = Just $ Ch x

503p_strHead [Str (x:xs)] = Just $ Ch x

@@ -507,6 +511,9 @@ p_strCons [Ch x, Str xs] = Just $ Str (x:xs)

507p_strCons _ = Nothing

511p_strCons _ = Nothing

508p_strRev [Str xs] = Just $ Str (reverse xs)

512p_strRev [Str xs] = Just $ Str (reverse xs)

509p_strRev _ = Nothing

513p_strRev _ = Nothing

514+p_strSubstr [I offset, I length, Str input] = Just $ Str (take length (drop offset input))

515+p_strSubstr _ = Nothing

516+

510

517

511p_cantreduce :: a -> Maybe b

518p_cantreduce :: a -> Maybe b

512p_cantreduce _ = Nothing

519p_cantreduce _ = Nothing

test/primitives001/expected+18

@@ -3,3 +3,21 @@

3("abc", "123")

4([1, 2], [3, 4, 5])

5([1, 2], [3, 4, 5])

6+ello! here's the thing

7+22

8+0

9+用的依赖类

10+Idris

11+[]

12+is 是一个通用

13+8

14+is 是一个通用的依赖类型纯函数式编程语言，其类型系统与 Agda 以及 Epigram 相似。

15+48

16+Idris 是一个通用的依赖类型纯函

17+18

18+is is a

19+8

20+is is a general-purpose purely functional programming language with dependent types.

21+85

22+Idris is a general

23+18

test/primitives001/inputnew file+2

@@ -0,0 +1,2 @@

1+Idris 是一个通用的依赖类型纯函数式编程语言，其类型系统与 Agda 以及 Epigram 相似。

2+Idris is a general-purpose purely functional programming language with dependent types.

test/primitives001/run+3−1

@@ -1,4 +1,6 @@

1#!/usr/bin/env bash

2idris $@ test005.idr -o test005

3./test005

4+idris $@ substring.idr -o substring

5+./substring < input

4−rm -f test005 test005.ibc

6+rm -f test005 substring *.ibc

test/primitives001/substring.idrnew file+51

@@ -0,0 +1,51 @@

1+-- This is a test of the substring primitive, both in the Idris

2+-- evaluator and in some backend. It attempts to exercise that

3+-- negative indices are equivalent to 0, that it works for mixed

4+-- single- and multi-byte characters, and that overshooting the end

5+-- doesn't break things.

6+

7+-- Single byte test

8+foo : String

9+foo = "Hello! here's the thing"

10+

11+-- The first sentence of the Chinese wikipedia article on Idris (to

12+-- get mixed single-and-multibyte chars)

13+firstSentence : String

14+firstSentence = "Idris 是一个通用的依赖类型纯函数式编程语言，其类型系统与 Agda 以及 Epigram 相似。"

15+

16+emptyTest : prim__strSubstr 100000 14 firstSentence = ""

17+emptyTest = Refl

18+

19+multiTest : prim__strSubstr 10 5 firstSentence = "用的依赖类"

20+multiTest = Refl

21+

22+negative : prim__strSubstr (-10) 5 firstSentence = "Idris"

23+negative = Refl

24+

25+negativeEnd : prim__strSubstr 0 (-1) firstSentence = ""

26+negativeEnd = Refl

27+

28+main : IO ()

29+main = do putStrLn $ prim__strSubstr 1 1004 foo

30+ printLn $ length $ prim__strSubstr 1 1000 foo

31+ printLn $ length $ prim__strSubstr 1000 2 firstSentence

32+ putStrLn $ prim__strSubstr 10 5 firstSentence

33+ putStrLn $ prim__strSubstr (-10) 5 firstSentence

34+ putStrLn $ "[" ++ prim__strSubstr 0 (-1) firstSentence ++ "]"

35+ -- Multi-byte dynamic string

36+ input <- getLine

37+ putStrLn $ prim__strSubstr 3 8 input

38+ putStrLn $ show (length (prim__strSubstr 3 8 input))

39+ putStrLn $ prim__strSubstr 3 8000 input

40+ putStrLn $ show (length (prim__strSubstr 3 8000 input))

41+ putStrLn $ prim__strSubstr (-13) 18 input

42+ putStrLn $ show (length (prim__strSubstr (-13) 18 input))

43+ -- Single-byte dynamic string

44+ input <- getLine

45+ putStrLn $ prim__strSubstr 3 8 input

46+ putStrLn $ show (length (prim__strSubstr 3 8 input))

47+ putStrLn $ prim__strSubstr 3 8000 input

48+ putStrLn $ show (length (prim__strSubstr 3 8000 input))

49+ putStrLn $ prim__strSubstr (-13) 18 input

50+ putStrLn $ show (length (prim__strSubstr (-13) 18 input))

51+