fa9f021 · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -207,6 +207,9 @@ Extra-source-files:

207 test/reg032/run

208 test/reg032/*.idr

209 test/reg032/expected

210+ test/reg033/run

211+ test/reg033/*.idr

212+ test/reg033/expected

210

213

211 test/basic001/run

214 test/basic001/run

212 test/basic001/*.idr

215 test/basic001/*.idr

src/Idris/AbsSyntax.hs+11

@@ -1744,6 +1744,17 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

1744 mkUniq (PPair fc p l r)

1745 = do l' <- mkUniq l; r' <- mkUniq r

1746 return $! PPair fc p l' r'

1747+ mkUniq (PDPair fc (PRef fc' n) t sc)

1748+ | t /= Placeholder

1749+ = do env <- get

1750+ (n', sc') <- if n `elem` env

1751+ then do let n' = uniqueName n (env ++ inScope)

1752+ return (n', shadow n n' sc)

1753+ else return (n, sc)

1754+ put (n' : env)

1755+ t' <- mkUniq t

1756+ sc'' <- mkUniq sc'

1757+ return $! PDPair fc (PRef fc' n') t' sc''

1747 mkUniq (PDPair fc l t r)

1758 mkUniq (PDPair fc l t r)

1748 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r

1759 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r

1749 return $! PDPair fc l' t' r'

1760 return $! PDPair fc l' t' r'

test/reg033/expectednew file

No changes to the content.

test/reg033/reg033.idrnew file+10

@@ -0,0 +1,10 @@

1+mapFilter : (alpha -> beta) ->

2+ (alpha -> Bool) ->

3+ Vect n alpha ->

4+ (n : Nat ** Vect n beta)

5+mapFilter f p Nil = (_ ** Nil)

6+mapFilter f p (a :: as) with (p a)

7+ | True = (_ ** (f a) :: (getProof (mapFilter f p as)))

8+ | False = mapFilter f p as

9+

10+

test/reg033/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ reg033.idr --check

3+rm -f reg033 *.ibc