943b653 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'MixingImplicitArgs' of https://github.com/JanBessai/Idris-dev into JanBessai-MixingImplicitArgs

commit943b653f35ecc85776b3493a2407e8c888e47703 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 2 May 2013, 12:40 (13 years ago) parent8c25808 a0308f1

4 files changed+24−4

compare with master

unifiedsplit

src/Idris/Parser.hs+6−4 test/reg017/expected+1 test/reg017/reg017.idr+13 test/reg017/run+4

src/Idris/Parser.hs+6−4

@@ -1364,7 +1364,8 @@ pClause syn

13641364 cargs <- many (pConstraintArg syn)

13651365 iargs <- many (pImplicitArg (syn { inPattern = True } ))

13661366 fc <- pfc

1367− args <- many (pArgExpr syn)

1367+ args <- many (try (pImplicitArg (syn { inPattern = True } ))

1368+ <|> (fmap pexp (pArgExpr syn)))

13681369 wargs <- many (pWExpr syn)

13691370 rhs <- pRHS syn n

13701371 ist <- getState

@@ -1376,7 +1377,7 @@ pClause syn

13761377 do pTerminator

13771378 return ([], [])]

13781379 let capp = PApp fc (PRef fc n)

1379− (iargs ++ cargs ++ map pexp args)

1380+ (iargs ++ cargs ++ args)

13801381 ist <- getState

13811382 setState (ist { lastParse = Just n })

13821383 return $ PClause fc n capp wargs rhs wheres)

@@ -1402,10 +1403,11 @@ pClause syn

14021403 cargs <- many (pConstraintArg syn)

14031404 iargs <- many (pImplicitArg (syn { inPattern = True } ))

14041405 fc <- pfc

1405− args <- many (pArgExpr syn)

1406+ args <- many (try (pImplicitArg (syn { inPattern = True } ))

1407+ <|> (fmap pexp (pArgExpr syn)))

14061408 wargs <- many (pWExpr syn)

14071409 let capp = PApp fc (PRef fc n)

1408− (iargs ++ cargs ++ map pexp args)

1410+ (iargs ++ cargs ++ args)

14091411 ist <- getState

14101412 setState (ist { lastParse = Just n })

14111413 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

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