621bd1d · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -247,6 +247,9 @@ Extra-source-files:

247 test/reg049/run

248 test/reg049/*.idr

249 test/reg049/expected

250+ test/reg050/run

251+ test/reg050/*.idr

252+ test/reg050/expected

250

253

251 test/basic001/run

254 test/basic001/run

252 test/basic001/*.idr

255 test/basic001/*.idr

src/Idris/ParseExpr.hs+1−1

@@ -320,7 +320,7 @@ simpleExpr syn =

320 <|> idiom syn

321 <|> listExpr syn

322 <|> alt syn

323− <|> do lchar '!'

323+ <|> do reservedOp "!"

324 s <- simpleExpr syn

325 fc <- getFC

326 return (PAppBind fc s [])

test/reg050/badbangop.idrnew file+15

@@ -0,0 +1,15 @@

1+module badbangop

2+

3+-- Check that using "!" by itself as an operator does not work

4+

5+infixl 2 !

6+

7+(!) : List a -> Nat -> Maybe a

8+xs ! n = index' n xs

9+

10+aList : List Integer

11+aList = [1,2,3,4,5]

12+

13+opUse : Maybe Integer

14+opUse = aList ! 2

15+

test/reg050/baddoublebang.idrnew file+7

@@ -0,0 +1,7 @@

1+module baddoublebang

2+

3+-- Check that two bang bindings running together don't work

4+

5+doubleBang : Maybe (Maybe Nat) -> Maybe Nat

6+doubleBang mmn = do pure !!mmn

7+

test/reg050/expectednew file+27

@@ -0,0 +1,27 @@

1+badbangop.idr:16:1:When elaborating right hand side of opUse:

2+When elaborating an application of function Prelude.Monad.>>=:

3+ Can't unify

4+ List Integer

5+ with

6+ argTy -> retTy

7+

8+ Specifically:

9+ Can't unify

10+ List

11+ with

12+ \{uv0} => argTy -> uv

13+./baddoublebang.idr:6:26: error: not

14+ a terminator, expected: "$",

15+ "$>", "&&", "*", "+", "++", "-",

16+ "->", ".", "/", "/=", "::", ";",

17+ "<", "<$", "<$>", "<*>", "<+>",

18+ "<->", "<<", "<=", "<|>", "=",

19+ "==", ">", ">=", ">>", ">>=",

20+ "\\\\", "`", "in", "||", "~=~",

21+ ambiguous use of a left-associative operator,

22+ ambiguous use of a non-associative operator,

23+ ambiguous use of a right-associative operator,

24+ end of input, function argument,

25+ matching application expression

26+doubleBang mmn = do pure !!mmn

27+ ^

test/reg050/runnew file+5

@@ -0,0 +1,5 @@

1+#!/usr/bin/env bash

2+idris --nocolour --check $@ working.idr

3+idris --nocolour --check $@ badbangop.idr

4+idris --nocolour --check $@ baddoublebang.idr

5+rm -f *.ibc

test/reg050/working.idrnew file+21

@@ -0,0 +1,21 @@

1+module working

2+

3+-- Check that using an operator beginning with "!" works

4+

5+infixl 2 !!

6+

7+(!!) : List a -> Nat -> Maybe a

8+xs !! n = index' n xs

9+

10+aList : List Integer

11+aList = [1,2,3,4,5]

12+

13+opUse : Maybe Integer

14+opUse = aList !! 2

15+

16+opUseWithBang : Maybe Nat -> Maybe Integer

17+opUseWithBang mn = do aList !! !mn

18+

19+doubleBang : Maybe (Maybe Nat) -> Maybe Nat

20+doubleBang mmn = do pure ! !mmn

21+