git.iko.soy/Idris-dev
on master help sign in
Merge branch 'MixingImplicitArgs' of https://github.com/JanBessai/Idris-dev into JanBessai-MixingImplicitArgs
943b653Edwin Brady
src/Idris/Parser.hs+6−4
compare with master
unifiedsplit
@@ -1364,7 +1364,8 @@ pClause syn
1364 cargs <- many (pConstraintArg syn)
1364 cargs <- many (pConstraintArg syn)
1365 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1365 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1366 fc <- pfc
1366 fc <- pfc
1367+ args <- many (try (pImplicitArg (syn { inPattern = True } ))
1367− args <- many (pArgExpr syn)
1368+ <|> (fmap pexp (pArgExpr syn)))
1368 wargs <- many (pWExpr syn)
1369 wargs <- many (pWExpr syn)
1369 rhs <- pRHS syn n
1370 rhs <- pRHS syn n
1370 ist <- getState
1371 ist <- getState
@@ -1376,7 +1377,7 @@ pClause syn
1376 do pTerminator
1377 do pTerminator
1377 return ([], [])]
1378 return ([], [])]
1378 let capp = PApp fc (PRef fc n)
1379 let capp = PApp fc (PRef fc n)
1379− (iargs ++ cargs ++ map pexp args)
1380+ (iargs ++ cargs ++ args)
1380 ist <- getState
1381 ist <- getState
1381 setState (ist { lastParse = Just n })
1382 setState (ist { lastParse = Just n })
1382 return $ PClause fc n capp wargs rhs wheres)
1383 return $ PClause fc n capp wargs rhs wheres)
@@ -1402,10 +1403,11 @@ pClause syn
1402 cargs <- many (pConstraintArg syn)
1403 cargs <- many (pConstraintArg syn)
1403 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1404 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1404 fc <- pfc
1405 fc <- pfc
1406+ args <- many (try (pImplicitArg (syn { inPattern = True } ))
1405− args <- many (pArgExpr syn)
1407+ <|> (fmap pexp (pArgExpr syn)))
1406 wargs <- many (pWExpr syn)
1408 wargs <- many (pWExpr syn)
1407 let capp = PApp fc (PRef fc n)
1409 let capp = PApp fc (PRef fc n)
1408− (iargs ++ cargs ++ map pexp args)
1410+ (iargs ++ cargs ++ args)
1409 ist <- getState
1411 ist <- getState
1410 setState (ist { lastParse = Just n })
1412 setState (ist { lastParse = Just n })
1411 reserved "with"
1413 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