20c71b0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Change implicit bind notation to a postfix !

commit20c71b0ae98228ee98f94da70bc328fe4e3926a0 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 18 Oct 2013, 00:30 (13 years ago) parent8c9ec38

2 files changed+8−3

unifiedsplit

effects/Effects.idr+1−1

@@ -130,7 +130,7 @@ data EffM : (m : Type -> Type) ->

130130 EffM m xs xs' a

131131 (:-) : (l : ty) -> EffM m [x] [y] t -> EffM m [l ::: x] [l ::: y] t

132132

133−syntax [tag] ":!" [val] = !(tag :- val)

133+syntax [tag] ":!" [val] = (tag :- val)!

134134

135135-- Eff : List (EFFECT m) -> Type -> Type

136136

src/Idris/ParseExpr.hs+7−2

@@ -186,7 +186,12 @@ internalExpr syn =

186186 <|> rewriteTerm syn

187187 <|> try(pi syn)

188188 <|> doBlock syn

189− <|> do simpleExpr syn

189+ <|> do s <- simpleExpr syn

190+ fc <- getFC

191+ bang <- option False (do lchar '!'; return True)

192+ if bang then return (PAppBind fc s [])

193+ else return s

194+

190195 <?> "expression"

191196

192197{- | Parses a case expression

@@ -269,8 +274,8 @@ simpleExpr syn =

269274 <|> caseExpr syn

270275 <|> do reserved "Type"; return PType

271276 <|> do fc <- getFC

272− bang <- option False (do lchar '!'; return True)

273277 x <- fnName

278+ bang <- option False (do lchar '!'; return True)

274279 if bang then return (PAppBind fc (PRef fc x) [])

275280 else return (PRef fc x)

276281 <|> try (listExpr syn)