bb3bc16 · Idris-dev · git.iko.soy

src/Idris/Unlit.hs+4−3

compare with master

unifiedsplit

@@ -19,8 +19,9 @@ unlit f s = do let s' = map ulLine (lines s)

19data LineType = Prog | Blank | Comm

20

21ulLine :: String -> (LineType, String)

22−ulLine ('>':' ':xs) = (Prog, xs)

22+ulLine ('>':' ':xs) = (Prog, ' ':' ':xs) -- Replace with spaces, otherwise text position numbers will be bogus.

23−ulLine ('>':xs) = (Prog, xs)

23+ulLine ('>':xs) = (Prog, ' ' :xs) -- The parser can deal with this, because /every/ (code) line is prefixed

24+ -- with a '>'.

24ulLine xs | all isSpace xs = (Blank, "")

25ulLine xs | all isSpace xs = (Blank, "")

25-- make sure it's not a doc comment

26-- make sure it's not a doc comment

26 | otherwise = (Comm, '-':'-':' ':'>':xs)

27 | otherwise = (Comm, '-':'-':' ':'>':xs)

@@ -29,7 +30,7 @@ check :: FilePath -> Int -> [(LineType, String)] -> TC ()

29check f l (a:b:cs) = do chkAdj f l (fst a) (fst b)

30check f l (a:b:cs) = do chkAdj f l (fst a) (fst b)

30 check f (l+1) (b:cs)

31 check f (l+1) (b:cs)

31check f l [x] = return ()

32check f l [x] = return ()

32−check f l [] = return ()

33+check f l [ ] = return ()

33

34

34-- Issue #1593 on the issue checker.

35-- Issue #1593 on the issue checker.

35--

36--

test/basic010/run+2−2

@@ -4,7 +4,7 @@ set -eu

4

5TIMEOUT=../scripts/timeout

6

7−$TIMEOUT 10 "${IDRIS:-idris}" "$@" Main.idr --nocolour --check --warnreach -o basic010

7+$TIMEOUT 20 "${IDRIS:-idris}" "$@" Main.idr --nocolour --check --warnreach -o basic010

8−$TIMEOUT 5 ./basic010

8+$TIMEOUT 20 ./basic010

9

10rm -f -- *.ibc basic010

test/regression002/expected+2−2

@@ -6,8 +6,8 @@ reg003a.idr:9:6:When checking type of Main.test:

6No such variable EvenList

7reg006.idr:17:1:

8RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup

9−reg007.lidr:8:1:A.n is already defined

9+reg007.lidr:8:3:A.n is already defined

10−reg007.lidr:12:11-17:When checking right hand side of hurrah with expected type

10+reg007.lidr:12:13-19:When checking right hand side of hurrah with expected type

11 0 = 1

12

13Type mismatch between

test/totality011/expected+1−1

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

1−totality011.lidr:22:1:

1+totality011.lidr:22:3:

2Main.weCanOnlyGetOlder is not total as there are missing cases