git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2619 from david-christiansen/substr-2

Be more thorough in substring testing

commitabc76e137afa87f3b5d5e468339690a010c084e0 authorNiklas Larsson <metaniklas@gmail.com> dateThu 17 Sep 2015, 00:41 (11 years ago) parent724e78be9d9041
2 files changed+11
compare with master
unifiedsplit
test/primitives001/expected+4 test/primitives001/substring.idr+7
test/primitives001/expected+4
@@ -15,9 +15,13 @@ is 是一个通用的依赖类型纯函数式编程语言，其类型系统与 A
151548
1616Idris 是一个通用的依赖类型纯函
171718
18+
19+0
1820is is a
19218
2022is is a general-purpose purely functional programming language with dependent types.
212385
2224Idris is a general
232518
26+
27+0
test/primitives001/substring.idr+7
@@ -25,6 +25,9 @@ negative = Refl
2525negativeEnd : prim__strSubstr 0 (-1) firstSentence = ""
2626negativeEnd = Refl
2727
28+negativeLength : prim__strSubstr 4 (-4) firstSentence = ""
29+negativeLength = Refl
30+
2831main : IO ()
2932main = do putStrLn $ prim__strSubstr 1 1004 foo
3033 printLn $ length $ prim__strSubstr 1 1000 foo
@@ -40,6 +43,8 @@ main = do putStrLn $ prim__strSubstr 1 1004 foo
4043 putStrLn $ show (length (prim__strSubstr 3 8000 input))
4144 putStrLn $ prim__strSubstr (-13) 18 input
4245 putStrLn $ show (length (prim__strSubstr (-13) 18 input))
46+ putStrLn $ prim__strSubstr 4 (-4) input
47+ putStrLn $ show (length (prim__strSubstr 4 (-4) input))
4348 -- Single-byte dynamic string
4449 input <- getLine
4550 putStrLn $ prim__strSubstr 3 8 input
@@ -48,4 +53,6 @@ main = do putStrLn $ prim__strSubstr 1 1004 foo
4853 putStrLn $ show (length (prim__strSubstr 3 8000 input))
4954 putStrLn $ prim__strSubstr (-13) 18 input
5055 putStrLn $ show (length (prim__strSubstr (-13) 18 input))
56+ putStrLn $ prim__strSubstr 4 (-4) input
57+ putStrLn $ show (length (prim__strSubstr 4 (-4) input))
5158