@@ -487,47 +487,56 @@ syntaxRule syn
487 -- Prevent syntax variable capture by making all binders under syntax unique
487 -- Prevent syntax variable capture by making all binders under syntax unique
488 -- (the ol' Common Lisp GENSYM approach)
488 -- (the ol' Common Lisp GENSYM approach)
489 uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm
489 uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm
490− uniquifyBinders userNames = fixBind []
490+ uniquifyBinders userNames = fixBind 0 []
492− fixBind :: [(Name, Name)] -> PTerm -> IdrisParser PTerm
492+ fixBind :: Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
493− fixBind rens (PRef fc hls n) | Just n' <- lookup n rens =
493+ fixBind 0 rens (PRef fc hls n) | Just n' <- lookup n rens =
494 return $ PRef fc hls n'
494 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 =
496 return $ PPatvar fc n'
496 return $ PPatvar fc n'
497− fixBind rens (PLam fc n nfc ty body)
497+ fixBind 0 rens (PLam fc n nfc ty body)
498− | n `elem` userNames = liftM2 (PLam fc n nfc) (fixBind rens ty) (fixBind rens body)
498+ | n `elem` userNames = liftM2 (PLam fc n nfc)
500+ (fixBind 0 rens body)
499 | otherwise =
501 | otherwise =
500− do ty' <- fixBind rens ty
502+ do ty' <- fixBind 0 rens ty
501 n' <- gensym n
503 n' <- gensym n
502− body' <- fixBind ((n,n'):rens) body
504+ body' <- fixBind 0 ((n,n'):rens) body
503 return $ PLam fc n' nfc ty' body'
505 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)
505 | n `elem` userNames = liftM2 (PPi plic n nfc)
507 | n `elem` userNames = liftM2 (PPi plic n nfc)
506− (fixBind rens argTy)
508+ (fixBind 0 rens argTy)
507− (fixBind rens body)
509+ (fixBind 0 rens body)
508 | otherwise =
510 | otherwise =
509− do ty' <- fixBind rens argTy
511+ do ty' <- fixBind 0 rens argTy
510 n' <- gensym n
512 n' <- gensym n
511− body' <- fixBind ((n,n'):rens) body
513+ body' <- fixBind 0 ((n,n'):rens) body
512 return $ (PPi plic n' nfc ty' body')
514 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)
514 | n `elem` userNames = liftM3 (PLet fc n nfc)
516 | n `elem` userNames = liftM3 (PLet fc n nfc)
515− (fixBind rens ty)
517+ (fixBind 0 rens ty)
516− (fixBind rens val)
518+ (fixBind 0 rens val)
517− (fixBind rens body)
519+ (fixBind 0 rens body)
518 | otherwise =
520 | otherwise =
519− do ty' <- fixBind rens ty
521+ do ty' <- fixBind 0 rens ty
520− val' <- fixBind rens val
522+ val' <- fixBind 0 rens val
521 n' <- gensym n
523 n' <- gensym n
522− body' <- fixBind ((n,n'):rens) body
524+ body' <- fixBind 0 ((n,n'):rens) body
523 return $ PLet fc n' nfc ty' val' body'
525 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 =
525 return $ PMatchApp fc n'
527 return $ PMatchApp fc n'
526 -- Also rename resolved quotations, to allow syntax rules to
528 -- Also rename resolved quotations, to allow syntax rules to
527 -- have quoted references to their own bindings.
529 -- 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 =
529 return $ PQuoteName n' True fc
531 return $ PQuoteName n' True fc
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
530− fixBind rens x = descendM (fixBind rens) x
539+ fixBind q rens x = descendM (fixBind q rens) x
532 gensym :: Name -> IdrisParser Name
541 gensym :: Name -> IdrisParser Name
533 gensym n = do ist <- get
542 gensym n = do ist <- get