fa9f021 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix silly name shadowing bug and add new test

commitfa9f021c6df0f220f744881457fa2485d876599c authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 4 Feb 2014, 18:03 (13 years ago) parentb45f766

5 files changed+27

compare with master

unifiedsplit

idris.cabal+3 src/Idris/AbsSyntax.hs+11 test/reg033/expected test/reg033/reg033.idr+10 test/reg033/run+3

idris.cabal+3

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

207207 test/reg032/run

208208 test/reg032/*.idr

209209 test/reg032/expected

210+ test/reg033/run

211+ test/reg033/*.idr

212+ test/reg033/expected

210213

211214 test/basic001/run

212215 test/basic001/*.idr

src/Idris/AbsSyntax.hs+11

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

17441744 mkUniq (PPair fc p l r)

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

17461746 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''

17471758 mkUniq (PDPair fc l t r)

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

17491760 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

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