git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3282 from steshaw/bug/master/729-layout-rule
9c32ab6Jan de Muijnck-Hughes
idris.cabal+4
compare with master
unifiedsplit
@@ -607,6 +607,10 @@ Extra-source-files:
607 test/io003/*.idr
607 test/io003/*.idr
608 test/io003/expected
608 test/io003/expected
609
609
610+ test/layout001/expected
611+ test/layout001/*.idr
612+ test/layout001/run
613+
610 test/literate001/run
614 test/literate001/run
611 test/literate001/*.lidr
615 test/literate001/*.lidr
612 test/literate001/expected
616 test/literate001/expected
src/Idris/Parser.hs+3−1
@@ -1116,7 +1116,9 @@ RHSName ::= '{' FnName '}';
1116@
1116@
1117-}
1117-}
1118rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
1118rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
1119−rhs syn n = do lchar '='; expr syn
1119+rhs syn n = do lchar '='
1120+ indentPropHolds gtProp
1121+ expr syn
1120 <|> do symbol "?=";
1122 <|> do symbol "?=";
1121 fc <- getFC
1123 fc <- getFC
1122 name <- option n' (do symbol "{"; n <- fst <$> fnName; symbol "}";
1124 name <- option n' (do symbol "{"; n <- fst <$> fnName; symbol "}";
test/TestData.hs+2
@@ -158,6 +158,8 @@ testFamiliesData = [
158 [ ( 1, C_CG ),
158 [ ( 1, C_CG ),
159 ( 2, ANY ),
159 ( 2, ANY ),
160 ( 3, C_CG )]),
160 ( 3, C_CG )]),
161+ ("layout", "Layout",
162+ [ ( 1, ANY )]),
161 ("literate", "Literate programming",
163 ("literate", "Literate programming",
162 [ ( 1, ANY )]),
164 [ ( 1, ANY )]),
163 ("meta", "Meta-programming",
165 ("meta", "Meta-programming",
test/layout001/expectednew file+93
@@ -0,0 +1,93 @@
1+Checking layout001a.idr
2+./layout001a.idr:5:1: error: Wrong
3+ indention: should be greater
4+ than context
5+ indentation, expected: space
6+y
7+^
8+Checking layout001b.idr
9+./layout001b.idr:5:3: error: Wrong
10+ indention: should be greater
11+ than context
12+ indentation, expected: space
13+= y
14+ ^
15+Checking layout001c.idr
16+./layout001c.idr:3:1: error: Wrong
17+ indention: should be greater
18+ than context
19+ indentation, expected: space
20+2
21+^
22+Checking layout001d.idr
23+Checking layout001e.idr
24+./layout001e.idr:6:1: error: Wrong
25+ indention: should be greater
26+ than context
27+ indentation, expected: space
28+3
29+^
30+Checking layout001f.idr
31+./layout001f.idr:6:2: error: Wrong
32+ indention: should be greater
33+ than context
34+ indentation, expected: space
35+ 3
36+ ^
37+Checking layout001g.idr
38+./layout001g.idr:6:3: error: Wrong
39+ indention: should be greater
40+ than context
41+ indentation, expected: space
42+ 3
43+ ^
44+Checking layout001h.idr
45+./layout001h.idr:6:3: error: Wrong
46+ indention: should be greater
47+ than context
48+ indentation, expected: space
49+ 3
50+ ^
51+Checking layout001i.idr
52+./layout001i.idr:6:4: error: Wrong
53+ indention: should be greater
54+ than context
55+ indentation, expected: space
56+ 3
57+ ^
58+Checking layout001j.idr
59+./layout001j.idr:6:5: error: Wrong
60+ indention: should be greater
61+ than context
62+ indentation, expected: space
63+ 3
64+ ^
65+Checking layout001k.idr
66+Checking layout001l.idr
67+./layout001l.idr:6:1: error: Wrong
68+ indention: should be greater
69+ than context
70+ indentation, expected: space
71+y
72+^
73+Checking layout001n.idr
74+Checking mplus1.idr
75+mplus1.idr:13:31:
76+When checking right hand side of term with expected type
77+ Maybe Int
78+
79+When checking an application of function Prelude.Applicative.pure:
80+ No such variable f
81+Checking mplus2.idr
82+./mplus2.idr:17:37: error: not
83+ end of block, expected: ")",
84+ "->", ";", "in",
85+ ambiguous use of a left-associative operator,
86+ ambiguous use of a non-associative operator,
87+ ambiguous use of a right-associative operator,
88+ do block expression,
89+ end of input
90+ `mplus` pure f
91+ ^
92+Checking mplus3.idr
93+mplus3.idr:11:1:warning - Unreachable case: term
test/layout001/layout001a.idrnew file+5
@@ -0,0 +1,5 @@
1+f : Int -> Int
2+f x = z 1 + 1 where
3+ z : Int -> Int
4+ z y =
5+y
test/layout001/layout001b.idrnew file+5
@@ -0,0 +1,5 @@
1+f : Int -> Int
2+f x = z 1 + 1 where
3+ z : Int -> Int
4+ z y
5+= y
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/layout001l.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/layout001n.idrnew file+33
@@ -0,0 +1,33 @@
1+module NonLayout
2+
3+{-
4+Haskell and Idris use indentation for grouping in the concrete syntax.
5+How this works is defined as an automatic translation to the equivalent
6+syntax using { ; and }, which you are free to use yourself.
7+
8+In Idris specifically, if let or where is followed by { then indentation no
9+longer matters for the following definitions until a balanced } appears. To
10+put multiple declarations on one line within the { } you put semicolons between
11+them: one ; for let declarations and ;; for where declarations. Whether this
12+discrepancy is a bug I don't know.
13+-}
14+
15+average : String -> Double
16+average str = answer where
17+ wordCount : String -> Nat
18+ wordCount str = length (words str)
19+ wordLengths : List String -> List Nat
20+ wordLengths strs = map length strs
21+ answer =
22+ let numWords = wordCount str in
23+ let totalLength = sum (wordLengths (words str)) in
24+ cast totalLength / cast numWords
25+
26+average' : String -> Double
27+average' str = answer where {
28+ wordCount : String -> Nat ;; wordCount str = length (words str)
29+ wordLengths : List String -> List Nat ;; wordLengths strs = map length strs
30+ answer = let {
31+ numWords = wordCount str; totalLength = sum (wordLengths (words str))
32+ } in cast totalLength / cast numWords
33+}
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/runnew file+8
@@ -0,0 +1,8 @@
1+#!/usr/bin/env bash
2+
3+for file in *.idr; do
4+ echo Checking ${file}
5+ ${IDRIS:-idris} --check $@ ${file}
6+done
7+
8+rm -f *.ibc