cea7870 · Idris-dev · git.iko.soy

CHANGELOG+6

compare with master

unifiedsplit

@@ -1,3 +1,9 @@

1+New in 0.9.18:

2+--------------

3+* Syntax rules no longer perform variable capture. Users of effects will

4+ need to explicitly name results in dependent effect signatures instead

5+ of using the default name "result".

6+

1New in 0.9.17:

7New in 0.9.17:

2--------------

8--------------

3* The --ideslave command line option has been replaced with a --ide-mode

9* The --ideslave command line option has been replaced with a --ide-mode

idris.cabal+3

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

301 test/reg060/run

302 test/reg060/*.idr

303 test/reg060/expected

304+ test/reg061/run

305+ test/reg061/*.idr

306+ test/reg061/expected

304

307

305 test/basic001/run

308 test/basic001/run

306 test/basic001/*.idr

309 test/basic001/*.idr

libs/effects/Effect/File.idr+4−3

@@ -117,9 +117,10 @@ FILE_IO t = MkEff t FileIO

117||| @ m The file mode.

118open : (fname : String)

119 -> (m : Mode)

120+ -> { [FILE_IO ()] ==> {result}

120− -> { [FILE_IO ()] ==> [FILE_IO (if result

121+ [FILE_IO (if result

121− then OpenFile m

122+ then OpenFile m

122− else ())] } Eff Bool

123+ else ())] } Eff Bool

123open f m = call $ Open f m

124open f m = call $ Open f m

124

125

126

src/Idris/Parser.hs+47−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 [n | Binding n <- syms]

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,51 @@ 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 :: [Name] -> PTerm -> IdrisParser PTerm

305+ uniquifyBinders userNames = fixBind []

306+ where

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+ | n `elem` userNames = liftM2 (PLam fc n) (fixBind rens ty) (fixBind rens body)

314+ | otherwise =

315+ do ty' <- fixBind rens ty

316+ n' <- gensym n

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

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

319+ fixBind rens (PPi plic n argTy body)

320+ | n `elem` userNames = liftM2 (PPi plic n) (fixBind rens argTy) (fixBind rens body)

321+ | otherwise =

322+ do ty' <- fixBind rens argTy

323+ n' <- gensym n

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

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

326+ fixBind rens (PLet fc n ty val body)

327+ | n `elem` userNames = liftM3 (PLet fc n)

328+ (fixBind rens ty)

329+ (fixBind rens val)

330+ (fixBind rens body)

331+ | otherwise =

332+ do ty' <- fixBind rens ty

333+ val' <- fixBind rens val

334+ n' <- gensym n

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

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

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

338+ return $ PMatchApp fc n'

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

340+

341+ gensym :: Name -> IdrisParser Name

342+ gensym n = do ist <- get

343+ let idx = idris_name ist

344+ put ist { idris_name = idx + 1 }

345+ return $ sMN idx (show n)

301

346

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

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

303

348

test/reg061/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/reg061/expectednew file

No changes to the content.

test/reg061/runnew file+3

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

1+#!/usr/bin/env bash

2+idris $@ Capture.idr --check

3+rm -f *.ibc