50d7dce · Idris-dev · git.iko.soy

idris.cabal+4

compare with master

unifiedsplit

@@ -298,6 +298,10 @@ Extra-source-files:

298 test/reg059/run

299 test/reg059/*.idr

300 test/reg059/expected

301+ test/reg060/run

302+ test/reg060/*.idr

303+ test/reg060/expected

304+

301

305

302 test/basic001/run

306 test/basic001/run

303 test/basic001/*.idr

307 test/basic001/*.idr

src/Idris/Parser.hs+38−2

@@ -59,6 +59,7 @@ import Data.List

59import Data.Monoid

60import Data.Char

61import Data.Ord

62+import Data.Generics.Uniplate.Data (descendM)

62import qualified Data.Map as M

63import qualified Data.Map as M

63import qualified Data.HashSet as HS

64import qualified Data.HashSet as HS

64import qualified Data.Text as T

65import qualified Data.Text as T

@@ -276,7 +277,7 @@ syntaxRule syn

276 when (length ns /= length (nub ns))

277 when (length ns /= length (nub ns))

277 $ unexpected "repeated variable in syntax rule"

278 $ unexpected "repeated variable in syntax rule"

278 lchar '='

279 lchar '='

279− tm <- typeExpr (allowImp syn)

280+ tm <- typeExpr (allowImp syn) >>= uniquifyBinders

280 terminator

281 terminator

281 return (Rule (mkSimple syms) tm sty)

282 return (Rule (mkSimple syms) tm sty)

282 where

283 where

@@ -297,7 +298,42 @@ syntaxRule syn

297 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s

298 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s

298 mkSimple' (e : es) = e : mkSimple' es

299 mkSimple' (e : es) = e : mkSimple' es

299 mkSimple' [] = []

300 mkSimple' [] = []

300−

301+

302+ -- Prevent syntax variable capture by making all binders under syntax unique

303+ -- (the ol' Common Lisp GENSYM approach)

304+ uniquifyBinders :: PTerm -> IdrisParser PTerm

305+ uniquifyBinders = fixBind []

306+

307+ fixBind :: [(Name, Name)] -> PTerm -> IdrisParser PTerm

308+ fixBind rens (PRef fc n) | Just n' <- lookup n rens =

309+ return $ PRef fc n'

310+ fixBind rens (PPatvar fc n) | Just n' <- lookup n rens =

311+ return $ PPatvar fc n'

312+ fixBind rens (PLam fc n ty body) =

313+ do ty' <- fixBind rens ty

314+ n' <- gensym n

315+ body' <- fixBind ((n,n'):rens) body

316+ return $ PLam fc n' ty' body'

317+ fixBind rens (PPi plic n argTy body) =

318+ do ty' <- fixBind rens argTy

319+ n' <- gensym n

320+ body' <- fixBind ((n,n'):rens) body

321+ return $ (PPi plic n' ty' body')

322+ fixBind rens (PLet fc n ty val body) =

323+ do ty' <- fixBind rens ty

324+ val' <- fixBind rens val

325+ n' <- gensym n

326+ body' <- fixBind ((n,n'):rens) body

327+ return $ (PLet fc n' ty' val' body')

328+ fixBind rens (PMatchApp fc n) | Just n' <- lookup n rens =

329+ return $ PMatchApp fc n'

330+ fixBind rens x = descendM (fixBind rens) x

331+

332+ gensym :: Name -> IdrisParser Name

333+ gensym n = do ist <- get

334+ let idx = idris_name ist

335+ put ist { idris_name = idx + 1 }

336+ return $ sMN idx (show n)

301

337

302{- | Parses a syntax symbol (either binding variable, keyword or expression)

338{- | Parses a syntax symbol (either binding variable, keyword or expression)

303

339

test/reg060/Capture.idrnew file+9

@@ -0,0 +1,9 @@

1+module Capture

2+

3+-- Test for variable capture in syntax

4+

5+syntax delay [x] = \z => case z of { () => x }

6+syntax delay' [z] = delay z

7+

8+capture : a -> () -> a

9+capture x = delay' x

test/reg060/expectednew file

No changes to the content.

test/reg060/runnew file+3

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

1+#!/usr/bin/env bash

2+idris $@ Capture.idr --check

3+rm -f *.ibc