git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:idris-lang/Idris-dev
7aeab41Edwin Brady
libs/base/Data/Fun.idr+6
compare with master
unifiedsplit
@@ -1,5 +1,7 @@
1module Data.Fun
1module Data.Fun
2
2
3+%default total
4+
3--------------------------------------------------------------------------------
5--------------------------------------------------------------------------------
4-- Build an n-ary function type from a Vect of Types and a result type
6-- Build an n-ary function type from a Vect of Types and a result type
5--------------------------------------------------------------------------------
7--------------------------------------------------------------------------------
@@ -7,6 +9,10 @@ Fun : Vect n Type -> Type -> Type
7Fun [] r = r
9Fun [] r = r
8Fun (t::ts) r = t -> Fun ts r
10Fun (t::ts) r = t -> Fun ts r
9
11
12+chain : {ts : Vect n Type} -> Fun [r] r' -> Fun ts r -> Fun ts r'
13+chain {ts = []} g r = g r
14+chain {ts = (_::_)} g f = \ x => chain g (f x)
15+
10target : {ts : Vect n Type} -> Fun ts r -> Type
16target : {ts : Vect n Type} -> Fun ts r -> Type
11target {r} _ = r
17target {r} _ = r
12
18
src/Idris/ParseOps.hs+6−2
@@ -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