d3adb11 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allow argument lists in lambda and pis

d3adb11Edwin Brady15 years ago

src/Idris/Parser.hs+18−8

compare with master

unifiedsplit

@@ -86,8 +86,7 @@ pUsing :: SyntaxInfo -> IParser [PDecl]

86pUsing syn =

87 do reserved "using";

88 lchar '('

89− ns <- sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))

89+ ns <- tyDeclList syn

90− (lchar ',')

91 lchar ')'

90 lchar ')'

92 lchar '{'

91 lchar '{'

93 let uvars = using syn

92 let uvars = using syn

@@ -153,19 +152,30 @@ pImplicitArg syn = do lchar '{'; n <- iName

153pTSig syn = do lchar ':'

152pTSig syn = do lchar ':'

154 pExpr syn

153 pExpr syn

155

154

156−pLambda syn = do lchar '\\'; x <- iName; t <- option Placeholder (pTSig syn)

155+pLambda syn = do lchar '\\';

156+ xt <- tyOptDeclList syn

157 symbol "=>"

158 sc <- pExpr syn

159− return (PLam x t sc)

159+ return (bindList PLam xt sc)

160

161−pPi syn = do lchar '('; x <- iName; t <- pTSig syn; lchar ')'

161+pPi syn = do lchar '('; xt <- tyDeclList syn; lchar ')'

162 symbol "->"

163 sc <- pExpr syn

164− return (PPi Exp x t sc)

164+ return (bindList (PPi Exp) xt sc)

165− <|> do lchar '{'; x <- iName; t <- pTSig syn; lchar '}'

165+ <|> do lchar '{'; xt <- tyDeclList syn; lchar '}'

166 symbol "->"

167 sc <- pExpr syn

168− return (PPi Imp x t sc)

168+ return (bindList (PPi Imp) xt sc)

169+

170+tyDeclList syn = sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))

171+ (lchar ',')

172+

173+tyOptDeclList syn = sepBy1 (do x <- pfName; t <- option Placeholder (pTSig syn)

174+ return (x,t))

175+ (lchar ',')

176+

177+bindList b [] sc = sc

178+bindList b ((n, t):bs) sc = b n t (bindList b bs sc)

169

179

170table fixes

180table fixes

171 = toTable (reverse fixes) ++

181 = toTable (reverse fixes) ++