@@ -487,47 +487,56 @@ syntaxRule syn
487487 -- Prevent syntax variable capture by making all binders under syntax unique
488488 -- (the ol' Common Lisp GENSYM approach)
489489 uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm
490− uniquifyBinders userNames = fixBind []
490+ uniquifyBinders userNames = fixBind 0 []
491491 where
492− fixBind :: [(Name, Name)] -> PTerm -> IdrisParser PTerm
493− fixBind rens (PRef fc hls n) | Just n' <- lookup n rens =
492+ fixBind :: Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
493+ fixBind 0 rens (PRef fc hls n) | Just n' <- lookup n rens =
494494 return $ PRef fc hls n'
495− fixBind rens (PPatvar fc n) | Just n' <- lookup n rens =
495+ fixBind 0 rens (PPatvar fc n) | Just n' <- lookup n rens =
496496 return $ PPatvar fc n'
497− fixBind rens (PLam fc n nfc ty body)
498− | n `elem` userNames = liftM2 (PLam fc n nfc) (fixBind rens ty) (fixBind rens body)
497+ fixBind 0 rens (PLam fc n nfc ty body)
498+ | n `elem` userNames = liftM2 (PLam fc n nfc)
499+ (fixBind 0 rens ty)
500+ (fixBind 0 rens body)
499501 | otherwise =
500− do ty' <- fixBind rens ty
502+ do ty' <- fixBind 0 rens ty
501503 n' <- gensym n
502− body' <- fixBind ((n,n'):rens) body
504+ body' <- fixBind 0 ((n,n'):rens) body
503505 return $ PLam fc n' nfc ty' body'
504− fixBind rens (PPi plic n nfc argTy body)
506+ fixBind 0 rens (PPi plic n nfc argTy body)
505507 | n `elem` userNames = liftM2 (PPi plic n nfc)
506− (fixBind rens argTy)
507− (fixBind rens body)
508+ (fixBind 0 rens argTy)
509+ (fixBind 0 rens body)
508510 | otherwise =
509− do ty' <- fixBind rens argTy
511+ do ty' <- fixBind 0 rens argTy
510512 n' <- gensym n
511− body' <- fixBind ((n,n'):rens) body
513+ body' <- fixBind 0 ((n,n'):rens) body
512514 return $ (PPi plic n' nfc ty' body')
513− fixBind rens (PLet fc n nfc ty val body)
515+ fixBind 0 rens (PLet fc n nfc ty val body)
514516 | n `elem` userNames = liftM3 (PLet fc n nfc)
515− (fixBind rens ty)
516− (fixBind rens val)
517− (fixBind rens body)
517+ (fixBind 0 rens ty)
518+ (fixBind 0 rens val)
519+ (fixBind 0 rens body)
518520 | otherwise =
519− do ty' <- fixBind rens ty
520− val' <- fixBind rens val
521+ do ty' <- fixBind 0 rens ty
522+ val' <- fixBind 0 rens val
521523 n' <- gensym n
522− body' <- fixBind ((n,n'):rens) body
524+ body' <- fixBind 0 ((n,n'):rens) body
523525 return $ PLet fc n' nfc ty' val' body'
524− fixBind rens (PMatchApp fc n) | Just n' <- lookup n rens =
526+ fixBind 0 rens (PMatchApp fc n) | Just n' <- lookup n rens =
525527 return $ PMatchApp fc n'
526528 -- Also rename resolved quotations, to allow syntax rules to
527529 -- have quoted references to their own bindings.
528− fixBind rens (PQuoteName n True fc) | Just n' <- lookup n rens =
530+ fixBind 0 rens (PQuoteName n True fc) | Just n' <- lookup n rens =
529531 return $ PQuoteName n' True fc
530− fixBind rens x = descendM (fixBind rens) x
532+
533+ -- Don't mess with quoted terms
534+ fixBind q rens (PQuasiquote tm goal) =
535+ flip PQuasiquote goal <$> fixBind (q + 1) rens tm
536+ fixBind q rens (PUnquote tm) =
537+ PUnquote <$> fixBind (q - 1) rens tm
538+
539+ fixBind q rens x = descendM (fixBind q rens) x
531540
532541 gensym :: Name -> IdrisParser Name
533542 gensym n = do ist <- get