git.iko.soy/Idris-dev
on master help sign in
Add more test cases for #729.
commit8b64f7f1a8b590bb7ece073e44c21b752188eefd authorSteven Shaw <steven@steshaw.org> dateThu 21 Jul 2016, 16:31 (10 years ago) parent368ed1d
17 files changed+185−1
compare with master
unifiedsplit
test/layout001/expected+68 test/layout001/layout001.idr → test/layout001/layout001a.idr test/layout001/layout001b.idr+6 test/layout001/layout001c.idr+3 test/layout001/layout001d.idr+3 test/layout001/layout001e.idr+6 test/layout001/layout001f.idr+6 test/layout001/layout001g.idr+6 test/layout001/layout001h.idr+6 test/layout001/layout001i.idr+6 test/layout001/layout001j.idr+6 test/layout001/layout001k.idr+6 test/layout001/mplus1.idr+17 test/layout001/mplus2.idr+17 test/layout001/mplus3.idr+17 test/layout001/passesButShouldNot.idr+6 test/layout001/run+6−1
test/layout001/expected+68
@@ -0,0 +1,68 @@
1+Checking layout001a.idr
2+Checking layout001b.idr
3+Checking layout001c.idr
4+Checking layout001d.idr
5+Checking layout001e.idr
6+./layout001e.idr:6:1: error: Wrong
7+ indention: should be greater
8+ than context
9+ indentation, expected: space
10+3
11+^
12+Checking layout001f.idr
13+./layout001f.idr:6:2: error: Wrong
14+ indention: should be greater
15+ than context
16+ indentation, expected: space
17+ 3
18+ ^
19+Checking layout001g.idr
20+./layout001g.idr:6:3: error: Wrong
21+ indention: should be greater
22+ than context
23+ indentation, expected: space
24+ 3
25+ ^
26+Checking layout001h.idr
27+./layout001h.idr:6:3: error: Wrong
28+ indention: should be greater
29+ than context
30+ indentation, expected: space
31+ 3
32+ ^
33+Checking layout001i.idr
34+./layout001i.idr:6:4: error: Wrong
35+ indention: should be greater
36+ than context
37+ indentation, expected: space
38+ 3
39+ ^
40+Checking layout001j.idr
41+./layout001j.idr:6:5: error: Wrong
42+ indention: should be greater
43+ than context
44+ indentation, expected: space
45+ 3
46+ ^
47+Checking layout001k.idr
48+Checking mplus1.idr
49+mplus1.idr:13:31:
50+When checking right hand side of term with expected type
51+ Maybe Int
52+
53+When checking an application of function Prelude.Applicative.pure:
54+ No such variable f
55+Checking mplus2.idr
56+./mplus2.idr:17:37: error: not
57+ end of block, expected: ")",
58+ "->", ";", "in",
59+ ambiguous use of a left-associative operator,
60+ ambiguous use of a non-associative operator,
61+ ambiguous use of a right-associative operator,
62+ do block expression,
63+ end of input
64+ `mplus` pure f
65+ ^
66+Checking mplus3.idr
67+mplus3.idr:11:1:warning - Unreachable case: term
68+Checking passesButShouldNot.idr
test/layout001/layout001.idr → test/layout001/layout001a.idrrenamed

The content is the same.

test/layout001/layout001b.idrnew file+6
@@ -0,0 +1,6 @@
1+-- This file passes the parser but should fail
2+f : Int -> Int
3+f x = z 1 + 1 where
4+ z : Int -> Int
5+ z y
6+= y -- FIXME: Should fail on this line with a layout-rule error.
test/layout001/layout001c.idrnew file+3
@@ -0,0 +1,3 @@
1+f : Int
2+f =
3+2
test/layout001/layout001d.idrnew file+3
@@ -0,0 +1,3 @@
1+f : Int
2+f
3+= 2
test/layout001/layout001e.idrnew file+6
@@ -0,0 +1,6 @@
1+foo : Int -> Int
2+foo a = a + b
3+ where
4+ b : Int
5+ b = 2 +
6+3
test/layout001/layout001f.idrnew file+6
@@ -0,0 +1,6 @@
1+foo : Int -> Int
2+foo a = a + b
3+ where
4+ b : Int
5+ b = 2 +
6+ 3
test/layout001/layout001g.idrnew file+6
@@ -0,0 +1,6 @@
1+foo : Int -> Int
2+foo a = a + b
3+ where
4+ b : Int
5+ b = 2 +
6+ 3
test/layout001/layout001h.idrnew file+6
@@ -0,0 +1,6 @@
1+foo : Int -> Int
2+foo a = a + b
3+ where
4+ b : Int
5+ b = 2 +
6+ 3
test/layout001/layout001i.idrnew file+6
@@ -0,0 +1,6 @@
1+foo : Int -> Int
2+foo a = a + b
3+ where
4+ b : Int
5+ b = 2 +
6+ 3
test/layout001/layout001j.idrnew file+6
@@ -0,0 +1,6 @@
1+foo : Int -> Int
2+foo a = a + b
3+ where
4+ b : Int
5+ b = 2 +
6+ 3
test/layout001/layout001k.idrnew file+6
@@ -0,0 +1,6 @@
1+foo : Int -> Int
2+foo a = a + b
3+ where
4+ b : Int
5+ b = 2 +
6+ 3
test/layout001/mplus1.idrnew file+17
@@ -0,0 +1,17 @@
1+mplus : Maybe a -> Maybe a -> Maybe a
2+mplus a b = ?mplus_rhs
3+
4+factor : Maybe Int
5+factor = ?term_rhs
6+
7+symbol : String -> Maybe Int
8+symbol = ?symbol_rhs
9+
10+term : Maybe Int
11+term = ?term_rhs
12+
13+term = do f <- factor
14+ do symbol "*"
15+ t <- term
16+ pure (f * t)
17+ `mplus` pure f
test/layout001/mplus2.idrnew file+17
@@ -0,0 +1,17 @@
1+mplus : Maybe a -> Maybe a -> Maybe a
2+mplus a b = ?mplus_rhs
3+
4+factor : Maybe Int
5+factor = ?term_rhs
6+
7+symbol : String -> Maybe Int
8+symbol = ?symbol_rhs
9+
10+term : Maybe Int
11+term = ?term_rhs
12+
13+term = do f <- factor
14+ do symbol "*"
15+ t <- term
16+ pure (f * t)
17+ `mplus` pure f
test/layout001/mplus3.idrnew file+17
@@ -0,0 +1,17 @@
1+mplus : Maybe a -> Maybe a -> Maybe a
2+mplus a b = ?mplus_rhs
3+
4+factor : Maybe Int
5+factor = ?term_rhs
6+
7+symbol : String -> Maybe Int
8+symbol = ?symbol_rhs
9+
10+term : Maybe Int
11+term = ?term_rhs
12+
13+term = do f <- factor
14+ do symbol "*"
15+ t <- term
16+ pure (f * t)
17+ `mplus` pure f
test/layout001/passesButShouldNot.idrnew file+6
@@ -0,0 +1,6 @@
1+f : Int -> Int
2+f x = z 1 + 1
3+ where
4+ z : Int -> Int
5+ z y =
6+y
test/layout001/run+6−1
@@ -1,3 +1,8 @@
11#!/usr/bin/env bash
2−${IDRIS:-idris} --check $@ layout001.idr
2+
3+for file in *.idr; do
4+ echo Checking ${file}
5+ ${IDRIS:-idris} --check $@ ${file}
6+done
7+
38rm -f *.ibc