Merge branch 'master' of github.com:idris-lang/Idris-dev
commit7aeab41b9bbb5abf2a8d9e5ee320f335164c551a
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateThu 6 Mar 2014, 00:14 (13 years ago)
parentf52eafde237954
libs/base/Data/Fun.idr+6
@@ -1,5 +1,7 @@
11module Data.Fun
22
3+%default total
4+
35--------------------------------------------------------------------------------
46-- Build an n-ary function type from a Vect of Types and a result type
57--------------------------------------------------------------------------------
@@ -7,6 +9,10 @@ Fun : Vect n Type -> Type -> Type
79Fun [] r = r
810Fun (t::ts) r = t -> Fun ts r
911
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+
1016target : {ts : Vect n Type} -> Fun ts r -> Type
1117target {r} _ = r
1218
src/Idris/ParseOps.hs+6−2
@@ -82,12 +82,16 @@ backtick = Infix (do indentPropHolds gtProp
8282 optional namespace
8383
8484@
85− OperatorFront ::= (Identifier_t '.')? '(' Operator_t ')';
85+ OperatorFront ::=
86+ '(' '=' ')'
87+ | (Identifier_t '.')? '(' Operator_t ')'
88+ ;
8689@
8790
8891-}
8992operatorFront :: IdrisParser Name
90−operatorFront = maybeWithNS (lchar '(' *> operator <* lchar ')') False []
93+operatorFront = try ((lchar '(' *> reservedOp "=" <* lchar ')') >> (return eqTy))
94+ <|> maybeWithNS (lchar '(' *> operator <* lchar ')') False []
9195
9296{- | Parses a function (either normal name or operator)
9397
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