066e890 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Substring as primitive

Introduce a new primitive for taking substrings. This can't really be done efficiently with strTail and strCons, so I think it deserves to exist as a primitive. Implementations are included for the evaluator as well as the C and JS backends. Other backends will need to implement it.

commit066e890a685f4f6c286cb863e2b9e86f852425b5 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 13 Sep 2015, 12:12 (11 years ago) parent6fc713d

16 files changed+147−10

compare with master

unifiedsplit

CHANGELOG+2 idris.cabal+1 libs/prelude/Prelude/Strings.idr+9−6 rts/idris_rts.c+11 rts/idris_rts.h+1 rts/idris_utf8.c+26 rts/idris_utf8.h+3−1 src/IRTS/CodegenC.hs+1 src/IRTS/CodegenJavaScript.hs+9 src/IRTS/Lang.hs+1−1 src/Idris/DeepSeq.hs+1 src/Idris/Primitives.hs+8−1 test/primitives001/expected+18 test/primitives001/input+2 test/primitives001/run+3−1 test/primitives001/substring.idr+51

CHANGELOG+2

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

77* Improved unification by implementing a pattern unification rule

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

99 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.

1012

1113Library updates

1214---------------

idris.cabal+1

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

550550 test/primitives001/run

551551 test/primitives001/*.idr

552552 test/primitives001/expected

553+ test/primitives001/input

553554 test/primitives002/run

554555 test/primitives002/expected

555556 test/primitives003/run

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

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

308308length = fromInteger . prim__zextInt_BigInt . prim_lenString

309309

310310||| Returns a substring of a given string

311−||| @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−||| @len The desired length of the substring. Truncated if this exceeds

314−||| the length of the input.

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

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

311+|||

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

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

314+||| string.

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

316+||| the length of the input.

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

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

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

317320

318321||| Lowercases all characters in the string.

319322|||

rts/idris_rts.c+11

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

594594 return MKINT((i_int)idx);

595595}

596596

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+

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

598609 char *xstr = GETSTR(str);

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

rts/idris_rts.h+1

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

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

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

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

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

317318

318319// system infox

319320// used indices:

rts/idris_utf8.c+26

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

7878 return top;

7979}

8080

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+

81107char* idris_utf8_fromChar(int x) {

82108 char* str;

83109 int bytes = 0, top = 0;

rts/idris_utf8.h+3−1

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

1818char* idris_utf8_fromChar(int x);

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

2020char* 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);

2224#endif

src/IRTS/CodegenC.hs+1

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

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

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

561561doOp 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 ++ ")"

562563

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

564565doOp 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'

11401140 JSNum (JSInt 1),

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

11421142 ]

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+ ]

11431152

11441153 | LSystemInfo <- op

11451154 , (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

7575 | LFSqrt | LFFloor | LFCeil | LFNegate

7676

7878 | LReadStr | LWriteStr

7979

8080 -- system info

src/Idris/DeepSeq.hs+1

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

8484 rnf (LStrCons) = ()

8585 rnf (LStrIndex) = ()

8686 rnf (LStrRev) = ()

87+ rnf (LStrSubstr) = ()

8788 rnf (LReadStr) = ()

8889 rnf (LWriteStr) = ()

8990 rnf (LSystemInfo) = ()

src/Idris/Primitives.hs+8−1

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

1515import Data.Function (on)

1616import qualified Data.Vector.Unboxed as V

1717

18+import Debug.Trace

19+

1820data Prim = Prim { p_name :: Name,

1921 p_type :: Type,

2022 p_arity :: Int,

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

165167 (2, LStrIndex) partial,

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

167169 (1, LStrRev) total,

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

171+ (3, LStrSubstr) total,

168172

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

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

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

493497p_floatFloor = p_fPrim (fromInteger . floor)

494498p_floatCeil = p_fPrim (fromInteger . ceiling)

495499

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

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

498502p_strLen _ = Nothing

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

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

507511p_strCons _ = Nothing

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

509513p_strRev _ = Nothing

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

515+p_strSubstr _ = Nothing

516+

510517

511518p_cantreduce :: a -> Maybe b

512519p_cantreduce _ = Nothing

test/primitives001/expected+18

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

33("abc", "123")

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

55([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 @@

11#!/usr/bin/env bash

22idris $@ test005.idr -o test005

33./test005

4−rm -f test005 test005.ibc

4+idris $@ substring.idr -o substring

5+./substring < input

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.

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+