git.iko.soy/Idris-dev
on master help sign in
Parser improvement to allow mixing of implicit and non implicit Arguments
a0308f1Jan Bessai
src/Idris/Parser.hs+6−4
compare with master
unifiedsplit
@@ -1348,7 +1348,8 @@ pClause syn
1348 cargs <- many (pConstraintArg syn)
1348 cargs <- many (pConstraintArg syn)
1349 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1349 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1350 fc <- pfc
1350 fc <- pfc
1351+ args <- many (try (pImplicitArg (syn { inPattern = True } ))
1351− args <- many (pArgExpr syn)
1352+ <|> (fmap pexp (pArgExpr syn)))
1352 wargs <- many (pWExpr syn)
1353 wargs <- many (pWExpr syn)
1353 rhs <- pRHS syn n
1354 rhs <- pRHS syn n
1354 ist <- getState
1355 ist <- getState
@@ -1360,7 +1361,7 @@ pClause syn
1360 do pTerminator
1361 do pTerminator
1361 return ([], [])]
1362 return ([], [])]
1362 let capp = PApp fc (PRef fc n)
1363 let capp = PApp fc (PRef fc n)
1363− (iargs ++ cargs ++ map pexp args)
1364+ (iargs ++ cargs ++ args)
1364 ist <- getState
1365 ist <- getState
1365 setState (ist { lastParse = Just n })
1366 setState (ist { lastParse = Just n })
1366 return $ PClause fc n capp wargs rhs wheres)
1367 return $ PClause fc n capp wargs rhs wheres)
@@ -1386,10 +1387,11 @@ pClause syn
1386 cargs <- many (pConstraintArg syn)
1387 cargs <- many (pConstraintArg syn)
1387 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1388 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1388 fc <- pfc
1389 fc <- pfc
1390+ args <- many (try (pImplicitArg (syn { inPattern = True } ))
1389− args <- many (pArgExpr syn)
1391+ <|> (fmap pexp (pArgExpr syn)))
1390 wargs <- many (pWExpr syn)
1392 wargs <- many (pWExpr syn)
1391 let capp = PApp fc (PRef fc n)
1393 let capp = PApp fc (PRef fc n)
1392− (iargs ++ cargs ++ map pexp args)
1394+ (iargs ++ cargs ++ args)
1393 ist <- getState
1395 ist <- getState
1394 setState (ist { lastParse = Just n })
1396 setState (ist { lastParse = Just n })
1395 reserved "with"
1397 reserved "with"
test/reg017/expectednew file+1
@@ -0,0 +1 @@
1+ssssO
test/reg017/reg017.idrnew file+13
@@ -0,0 +1,13 @@
1+module Main
2+
3+foo : { t : Type } ->
4+ (a : t) ->
5+ { default tactics { refine refl; solve; } prfA : a = a } ->
6+ (b : Nat) ->
7+ (c : Nat) ->
8+ { default tactics { refine refl; solve; } prfBC : b = c } ->
9+ Nat
10+foo {t} a {prfA = p} b c {prfBC} = b
11+
12+main : IO ()
13+main = print $ foo 3 4 4
test/reg017/runnew file+4
@@ -0,0 +1,4 @@
1+#!/bin/bash
2+idris $@ reg017.idr -o reg017
3+./reg017
4+rm -f reg017 *.ibc