50af5aa · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Make the parentheses around a with-rule scrutinee mandatory

Right now, parentheses are required around any non-atomic expressions that are the scrutinee of a with-rule. In practice, this means that almost all expressions require parentheses, as with is typically used to introduce more information that was not available in the outer pattern match. In the standard library, the only place where with rules occur without parentheses is in Data.Bits. Making the parentheses mandatory vastly improves parser errors in case they are forgotten, RE #166 . Sample of current message: ./WithRule.idr:4:14: error: expected: "{", function declaration foo x with x == 0 ^ Sample of message with this patch: ./WithRule.idr:4:12: error: expected: "(" foo x with x == 0 ^

commit50af5aa2c988bd3c0fe8968bb3b4f1859770c556 authorDavid Christiansen <david@davidchristiansen.dk> dateSat 28 Sep 2013, 21:27 (13 years ago) parent70a041f

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 '('

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 '('

2278+ wval <- bracketed syn

22772279 openBlock

22782280 ds <- some $ fnDecl syn

22792281 let withs = map (fillLHSD n capp wargs) $ concat ds