9633fd7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Syntax hygiene for resolved quoted names

When quoting a name that's locally bound by a syntax rule, resolved name quotations should be renamed along with the binder. This allows syntax rules to contain reflected references to names that they introduce, which enables some nice metaprogramming idioms and, among other things, makes an analog of Agda's quoteGoal expressible.

commit9633fd7b4a84928169b33bd7d0bd4120aa928ffd authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 29 Jan 2016, 13:14 (11 years ago) parentc4c7802

1 file changed+7−1

compare with master

unifiedsplit

src/Idris/Parser.hs+7−1

src/Idris/Parser.hs+7−1

@@ -502,7 +502,9 @@ syntaxRule syn

502502 body' <- fixBind ((n,n'):rens) body

503503 return $ PLam fc n' nfc ty' body'

504504 fixBind rens (PPi plic n nfc argTy body)

505− | n `elem` userNames = liftM2 (PPi plic n nfc) (fixBind rens argTy) (fixBind rens body)

505+ | n `elem` userNames = liftM2 (PPi plic n nfc)

506+ (fixBind rens argTy)

507+ (fixBind rens body)

506508 | otherwise =

507509 do ty' <- fixBind rens argTy

508510 n' <- gensym n

@@ -521,6 +523,10 @@ syntaxRule syn

521523 return $ PLet fc n' nfc ty' val' body'

522524 fixBind rens (PMatchApp fc n) | Just n' <- lookup n rens =

523525 return $ PMatchApp fc n'

526+ -- Also rename resolved quotations, to allow syntax rules to

527+ -- have quoted references to their own bindings.

528+ fixBind rens (PQuoteName n True fc) | Just n' <- lookup n rens =

529+ return $ PQuoteName n' True fc

524530 fixBind rens x = descendM (fixBind rens) x

525531

526532 gensym :: Name -> IdrisParser Name