@@ -277,7 +277,7 @@ syntaxRule syn
277277 when (length ns /= length (nub ns))
278278 $ unexpected "repeated variable in syntax rule"
279279 lchar '='
280− tm <- typeExpr (allowImp syn) >>= uniquifyBinders
280+ tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]
281281 terminator
282282 return (Rule (mkSimple syms) tm sty)
283283 where
@@ -301,39 +301,48 @@ syntaxRule syn
301301
302302 -- Prevent syntax variable capture by making all binders under syntax unique
303303 -- (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)
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)
337346
338347{- | Parses a syntax symbol (either binding variable, keyword or expression)
339348