f8cb234 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Reading from a file shouldn't strip \n

We need to get exactly what's in the file or strange things might happen and assumptions get broken. Change getLine to strip newlines itself rather than have the RTS do it, for consistency with the REPL behaviour.

commitf8cb234577c12a5ecd5b3b145feebb56be8f4c32 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 16 May 2015, 14:03 (11 years ago) parentdcdfd85

6 files changed+12−10

compare with master

unifiedsplit

libs/prelude/Prelude.idr+8−4 rts/idris_rts.c−2 test/dsl002/test014.idr+2−1 test/effects001/expected+1−1 test/io001/expected−1 test/io001/test004.idr+1−1

libs/prelude/Prelude.idr+8−4

@@ -352,7 +352,13 @@ printLn x = putStrLn (show x)

352352||| Read one line of input from stdin, without the trailing newline

353353partial

354354getLine : IO' ffi String

355−getLine = prim_read

355+getLine = do x <- prim_read

356+ return (reverse (trimNL (reverse x)))

357+ where trimNL : String -> String

358+ trimNL str with (strM str)

359+ trimNL "" | StrNil = ""

360+ trimNL (strCons '\n' xs) | StrCons _ _ = xs

361+ trimNL (strCons x xs) | StrCons _ _ = strCons x xs

356362

357363||| Write a single character to stdout

358364partial

@@ -548,7 +554,5 @@ readFile fn = do h <- openFile fn Read

548554 readFile' h contents =

549555 do x <- feof h

550556 if not x then do l <- fread h

551− case contents of

552− "" => readFile' h l

553− _ => readFile' h (contents ++ "\n" ++ l)

557+ readFile' h (contents ++ l)

554558 else return contents

rts/idris_rts.c−2

@@ -509,8 +509,6 @@ VAL idris_readStr(VM* vm, FILE* h) {

509509 size_t n = 0;

510510 ssize_t len;

511511 len = getline(&buffer, &n, h);

512− strtok(buffer, "\n");

513−

514512 if (len <= 0) {

515513 ret = MKSTR(vm, "");

516514 } else {

test/dsl002/test014.idr+2−1

@@ -34,6 +34,7 @@ syntax rreadLine [h] = Use readLine h

3434syntax reof [h] = Use eof h

3535

3636syntax rputStrLn [s] = Lift (putStrLn s)

37+syntax rputStr [s] = Lift (putStr s)

3738

3839syntax "if" "opened" [f] "then" [e] "else" [t] = Check f t e

3940

@@ -57,7 +58,7 @@ readH : String -> RES ()

5758readH fn = res (do let x = open fn Reading

5859 if opened x then

5960 do str <- rreadLine x

60− rputStrLn str

61+ rputStr str

6162 rclose x

6263 else rputStrLn "Error")

6364

test/effects001/expected+1−1

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

1−["HELLO!!!", "WORLD!!!", ""]

1+["HELLO!!!\n", "WORLD!!!\n", ""]

223

3315

44Answer: 99

test/io001/expected−1

@@ -13,5 +13,4 @@ World!

13133

14144

1515Last line

16−

1716---

test/io001/test004.idr+1−1

@@ -13,7 +13,7 @@ dumpFile fn = do { h <- openFile fn Read

1313 x <- feof h

1414 return (not x) })

1515 (do { l <- fread h

16− putStrLn l })

16+ putStr l })

1717 closeFile h }

1818

1919main : IO ()