a0308f1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Parser improvement to allow mixing of implicit and non implicit Arguments

commita0308f19aec694f9d1cd83bb1b1f22a40a3d0e4e authorJan Bessai <Jan.Bessai@tu-dortmund.de> dateWed 1 May 2013, 14:14 (13 years ago) parentf1e61da

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

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

13481348 cargs <- many (pConstraintArg syn)

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

13501350 fc <- pfc

1351− args <- many (pArgExpr syn)

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

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

13521353 wargs <- many (pWExpr syn)

13531354 rhs <- pRHS syn n

13541355 ist <- getState

@@ -1360,7 +1361,7 @@ pClause syn

13601361 do pTerminator

13611362 return ([], [])]

13621363 let capp = PApp fc (PRef fc n)

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

1364+ (iargs ++ cargs ++ args)

13641365 ist <- getState

13651366 setState (ist { lastParse = Just n })

13661367 return $ PClause fc n capp wargs rhs wheres)

@@ -1386,10 +1387,11 @@ pClause syn

13861387 cargs <- many (pConstraintArg syn)

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

13881389 fc <- pfc

1389− args <- many (pArgExpr syn)

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

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

13901392 wargs <- many (pWExpr syn)

13911393 let capp = PApp fc (PRef fc n)

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

1394+ (iargs ++ cargs ++ args)

13931395 ist <- getState

13941396 setState (ist { lastParse = Just n })

13951397 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