Merge pull request #2028 from david-christiansen/issue/1172

Prevent variable capture when desugaring custom syntax

CHANGELOG

@@ -1,3 +1,9 @@
+New in 0.9.18:
+--------------
+* Syntax rules no longer perform variable capture. Users of effects will
+  need to explicitly name results in dependent effect signatures instead
+  of using the default name "result".
+
 New in 0.9.17:
 --------------
 * The --ideslave command line option has been replaced with a --ide-mode

idris.cabal

@@ -301,6 +301,9 @@ Extra-source-files:
                        test/reg060/run
                        test/reg060/*.idr
                        test/reg060/expected
+                       test/reg061/run
+                       test/reg061/*.idr
+                       test/reg061/expected
 
                        test/basic001/run
                        test/basic001/*.idr

libs/effects/Effect/File.idr

@@ -117,9 +117,10 @@ FILE_IO t = MkEff t FileIO
 ||| @ m The file mode.
 open : (fname : String)
        -> (m : Mode)
-       -> { [FILE_IO ()] ==> [FILE_IO (if result
-                                          then OpenFile m
-                                          else ())] } Eff Bool
+       -> { [FILE_IO ()] ==> {result}
+            [FILE_IO (if result
+                        then OpenFile m
+                        else ())] } Eff Bool
 open f m = call $ Open f m
 
 

src/Idris/Parser.hs

@@ -59,6 +59,7 @@ import Data.List
 import Data.Monoid
 import Data.Char
 import Data.Ord
+import Data.Generics.Uniplate.Data (descendM)
 import qualified Data.Map as M
 import qualified Data.HashSet as HS
 import qualified Data.Text as T
@@ -276,7 +277,7 @@ syntaxRule syn
          when (length ns /= length (nub ns))
             $ unexpected "repeated variable in syntax rule"
          lchar '='
-         tm <- typeExpr (allowImp syn)
+         tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]
          terminator
          return (Rule (mkSimple syms) tm sty)
   where
@@ -297,7 +298,51 @@ syntaxRule syn
        where ts = dropWhile isSpace . dropWhileEnd isSpace $ s
     mkSimple' (e : es) = e : mkSimple' es
     mkSimple' [] = []
-
+
+    -- Prevent syntax variable capture by making all binders under syntax unique
+    -- (the ol' Common Lisp GENSYM approach)
+    uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm
+    uniquifyBinders userNames = fixBind []
+      where
+        fixBind :: [(Name, Name)] -> PTerm -> IdrisParser PTerm
+        fixBind rens (PRef fc n) | Just n' <- lookup n rens =
+          return $ PRef fc n'
+        fixBind rens (PPatvar fc n) | Just n' <- lookup n rens =
+          return $ PPatvar fc n'
+        fixBind rens (PLam fc n ty body)
+          | n `elem` userNames = liftM2 (PLam fc n) (fixBind rens ty) (fixBind rens body)
+          | otherwise =
+            do ty' <- fixBind rens ty
+               n' <- gensym n
+               body' <- fixBind ((n,n'):rens) body
+               return $ PLam fc n' ty' body'
+        fixBind rens (PPi plic n argTy body)
+          | n `elem` userNames = liftM2 (PPi plic n) (fixBind rens argTy) (fixBind rens body)
+          | otherwise =
+            do ty' <- fixBind rens argTy
+               n' <- gensym n
+               body' <- fixBind ((n,n'):rens) body
+               return $ (PPi plic n' ty' body')
+        fixBind rens (PLet fc n ty val body)
+          | n `elem` userNames = liftM3 (PLet fc n)
+                                        (fixBind rens ty)
+                                        (fixBind rens val)
+                                        (fixBind rens body)
+          | otherwise =
+            do ty' <- fixBind rens ty
+               val' <- fixBind rens val
+               n' <- gensym n
+               body' <- fixBind ((n,n'):rens) body
+               return $ (PLet fc n' ty' val' body')
+        fixBind rens (PMatchApp fc n) | Just n' <- lookup n rens =
+          return $ PMatchApp fc n'
+        fixBind rens x = descendM (fixBind rens) x
+
+        gensym :: Name -> IdrisParser Name
+        gensym n = do ist <- get
+                      let idx = idris_name ist
+                      put ist { idris_name = idx + 1 }
+                      return $ sMN idx (show n)
 
 {- | Parses a syntax symbol (either binding variable, keyword or expression)
 

test/reg061/Capture.idr

@@ -0,0 +1,9 @@
+module Capture
+
+-- Test for variable capture in syntax
+
+syntax delay  [x] = \z => case z of { () => x }
+syntax delay' [z] = delay z
+
+capture : a -> () -> a
+capture x = delay' x

test/reg061/run

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+idris $@ Capture.idr --check
+rm -f *.ibc