@@ -277,7 +277,7 @@ syntaxRule syn
277 when (length ns /= length (nub ns))
277 when (length ns /= length (nub ns))
278 $ unexpected "repeated variable in syntax rule"
278 $ unexpected "repeated variable in syntax rule"
279 lchar '='
279 lchar '='
280− tm <- typeExpr (allowImp syn) >>= uniquifyBinders
280+ tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]
281 terminator
281 terminator
282 return (Rule (mkSimple syms) tm sty)
282 return (Rule (mkSimple syms) tm sty)
@@ -301,39 +301,48 @@ syntaxRule syn
302 -- Prevent syntax variable capture by making all binders under syntax unique
302 -- Prevent syntax variable capture by making all binders under syntax unique
303 -- (the ol' Common Lisp GENSYM approach)
303 -- (the ol' Common Lisp GENSYM approach)
304− uniquifyBinders :: PTerm -> IdrisParser PTerm
304+ uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm
305− uniquifyBinders = fixBind []
305+ uniquifyBinders userNames = fixBind []
307− fixBind :: [(Name, Name)] -> PTerm -> IdrisParser PTerm
307+ fixBind :: [(Name, Name)] -> PTerm -> IdrisParser PTerm
308− fixBind rens (PRef fc n) | Just n' <- lookup n rens =
308+ fixBind rens (PRef fc n) | Just n' <- lookup n rens =
309− return $ PRef fc n'
309+ return $ PRef fc n'
310− fixBind rens (PPatvar fc n) | Just n' <- lookup n rens =
310+ fixBind rens (PPatvar fc n) | Just n' <- lookup n rens =
311− return $ PPatvar fc n'
311+ return $ PPatvar fc n'
312− fixBind rens (PLam fc n ty body) =
312+ fixBind rens (PLam fc n ty body)
313+ | n `elem` userNames = liftM2 (PLam fc n) (fixBind rens ty) (fixBind rens body)
313− do ty' <- fixBind rens ty
315+ do ty' <- fixBind rens ty
314− n' <- gensym n
316+ n' <- gensym n
315− body' <- fixBind ((n,n'):rens) body
317+ body' <- fixBind ((n,n'):rens) body
316− return $ PLam fc n' ty' body'
318+ return $ PLam fc n' ty' body'
317− fixBind rens (PPi plic n argTy body) =
319+ fixBind rens (PPi plic n argTy body)
320+ | n `elem` userNames = liftM2 (PPi plic n) (fixBind rens argTy) (fixBind rens body)
318− do ty' <- fixBind rens argTy
322+ do ty' <- fixBind rens argTy
319− n' <- gensym n
323+ n' <- gensym n
320− body' <- fixBind ((n,n'):rens) body
324+ body' <- fixBind ((n,n'):rens) body
321− return $ (PPi plic n' ty' body')
325+ return $ (PPi plic n' ty' body')
322− fixBind rens (PLet fc n ty val body) =
326+ fixBind rens (PLet fc n ty val body)
327+ | n `elem` userNames = liftM3 (PLet fc n)
323− do ty' <- fixBind rens ty
332+ do ty' <- fixBind rens ty
324− val' <- fixBind rens val
333+ val' <- fixBind rens val
325− n' <- gensym n
334+ n' <- gensym n
326− body' <- fixBind ((n,n'):rens) body
335+ body' <- fixBind ((n,n'):rens) body
327− return $ (PLet fc n' ty' val' body')
336+ return $ (PLet fc n' ty' val' body')
328− fixBind rens (PMatchApp fc n) | Just n' <- lookup n rens =
337+ fixBind rens (PMatchApp fc n) | Just n' <- lookup n rens =
329− return $ PMatchApp fc n'
338+ return $ PMatchApp fc n'
330− fixBind rens x = descendM (fixBind rens) x
339+ fixBind rens x = descendM (fixBind rens) x
332− gensym :: Name -> IdrisParser Name
341+ gensym :: Name -> IdrisParser Name
333− gensym n = do ist <- get
342+ gensym n = do ist <- get
334− let idx = idris_name ist
343+ let idx = idris_name ist
335− put ist { idris_name = idx + 1 }
344+ put ist { idris_name = idx + 1 }
336− return $ sMN idx (show n)
345+ return $ sMN idx (show n)
338{- | Parses a syntax symbol (either binding variable, keyword or expression)
347{- | Parses a syntax symbol (either binding variable, keyword or expression)