git.iko.soy/Idris-dev
on master help sign in
Treat (=) as a special function name.
be7d600Jan Bessai
src/Idris/ParseOps.hs+6−2
compare with master
unifiedsplit
@@ -82,12 +82,16 @@ backtick = Infix (do indentPropHolds gtProp
82 optional namespace
82 optional namespace
83
83
84@
84@
85+ OperatorFront ::=
86+ '(' '=' ')'
85− OperatorFront ::= (Identifier_t '.')? '(' Operator_t ')';
87+ | (Identifier_t '.')? '(' Operator_t ')'
88+ ;
86@
89@
87
90
88-}
91-}
89operatorFront :: IdrisParser Name
92operatorFront :: IdrisParser Name
93+operatorFront = try ((lchar '(' *> reservedOp "=" <* lchar ')') >> (return eqTy))
90−operatorFront = maybeWithNS (lchar '(' *> operator <* lchar ')') False []
94+ <|> maybeWithNS (lchar '(' *> operator <* lchar ')') False []
91
95
92{- | Parses a function (either normal name or operator)
96{- | Parses a function (either normal name or operator)
93
97
test/reg037/expectednew file

No changes to the content.

test/reg037/reg037.idrnew file+9
@@ -0,0 +1,9 @@
1+
2+--- Parser regression for (=) as a function name (fnName)
3+
4+class Foo (t : (A : Type) -> (B : Type) -> A -> B -> Type) where
5+ foo : (A : Type) -> (B : Type) -> (x : A) -> (y : B) -> t A B x y -> t A B x y
6+
7+instance Foo (=) where
8+ foo A B x y prf = prf
9+
test/reg037/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris --check reg037.idr
3+rm -f reg037 *.ibc