git.iko.soy/Idris-dev
on master help sign in
Merge pull request #504 from david-christiansen/with-parser

Make parens mandatory after with - vastly improving the error message

commit45e0a55701c303b7616f531357701107552f5b2d authorEdwin Brady <edwin.brady@gmail.com> dateTue 1 Oct 2013, 07:50 (13 years ago) parent27ed67d4ed09e4
2 files changed+10−8
compare with master
unifiedsplit
lib/Data/Bits.idr+6−6 src/Idris/Parser.hs+4−2
lib/Data/Bits.idr+6−6
@@ -32,7 +32,7 @@ bitsUsed n = 8 * (2 `power` n)
3232%assert_total
3333natToBits' : machineTy n -> Nat -> machineTy n
3434natToBits' a Z = a
35−natToBits' {n=n} a x with n
35+natToBits' {n=n} a x with (n)
3636 -- it seems I have to manually recover the value of n here, instead of being able to reference it
3737 natToBits' a (S x') | Z = natToBits' {n=0} (prim__addB8 a (prim__truncInt_B8 1)) x'
3838 natToBits' a (S x') | S Z = natToBits' {n=1} (prim__addB16 a (prim__truncInt_B16 1)) x'
@@ -40,7 +40,7 @@ natToBits' {n=n} a x with n
4040 natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x'
4141
4242natToBits : Nat -> machineTy n
43−natToBits {n=n} x with n
43+natToBits {n=n} x with (n)
4444 | Z = natToBits' {n=0} (prim__truncInt_B8 0) x
4545 | S Z = natToBits' {n=1} (prim__truncInt_B16 0) x
4646 | S (S Z) = natToBits' {n=2} (prim__truncInt_B32 0) x
@@ -106,7 +106,7 @@ shiftLeft : Bits n -> Bits n -> Bits n
106106shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)
107107
108108shiftRightLogical' : machineTy n -> machineTy n -> machineTy n
109−shiftRightLogical' {n=n} x c with n
109+shiftRightLogical' {n=n} x c with (n)
110110 | Z = prim__lshrB8 x c
111111 | S Z = prim__lshrB16 x c
112112 | S (S Z) = prim__lshrB32 x c
@@ -129,7 +129,7 @@ shiftRightArithmetic : Bits n -> Bits n -> Bits n
129129shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)
130130
131131and' : machineTy n -> machineTy n -> machineTy n
132−and' {n=n} x y with n
132+and' {n=n} x y with (n)
133133 | Z = prim__andB8 x y
134134 | S Z = prim__andB16 x y
135135 | S (S Z) = prim__andB32 x y
@@ -140,7 +140,7 @@ and : Bits n -> Bits n -> Bits n
140140and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)
141141
142142or' : machineTy n -> machineTy n -> machineTy n
143−or' {n=n} x y with n
143+or' {n=n} x y with (n)
144144 | Z = prim__orB8 x y
145145 | S Z = prim__orB16 x y
146146 | S (S Z) = prim__orB32 x y
@@ -151,7 +151,7 @@ or : Bits n -> Bits n -> Bits n
151151or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)
152152
153153xor' : machineTy n -> machineTy n -> machineTy n
154−xor' {n=n} x y with n
154+xor' {n=n} x y with (n)
155155 | Z = prim__xorB8 x y
156156 | S Z = prim__xorB16 x y
157157 | S (S Z) = prim__xorB32 x y
src/Idris/Parser.hs+4−2
@@ -2240,7 +2240,8 @@ clause syn
22402240 return $ PClause fc n capp wargs rs wheres) <|> (do
22412241 popIndent
22422242 reserved "with"
2243− wval <- simpleExpr syn
2243+ lchar '(' <?> "parenthesized expression"
2244+ wval <- bracketed syn
22442245 openBlock
22452246 ds <- some $ fnDecl syn
22462247 closeBlock
@@ -2273,7 +2274,8 @@ clause syn
22732274 reserved "with"
22742275 ist <- get
22752276 put (ist { lastParse = Just n })
2276− wval <- simpleExpr syn
2277+ lchar '(' <?> "parenthesized expression"
2278+ wval <- bracketed syn
22772279 openBlock
22782280 ds <- some $ fnDecl syn
22792281 let withs = map (fillLHSD n capp wargs) $ concat ds