new feature: quote metas

[rybla]

Currently, in Agda.TypeChecking.Rules.doQuoteTerm, if a term contains any metas, then the corresponding quoteTerm constraint is delayed. As suggested here, relaxing this constraint allows for quoted metas, where an interactive hole gets quoted and spliced by the macro, and the type constraints at the splice site are propagated back to the interactive hole. This is useful for interactively writing tactics one macro at a time.

This PR adds this feature behind a pragma flag --quoted-holes. Turning on this feature allows doQuoteTerm to continue regardless of whether the term to quote contains any metas.

Tasks:

• [x] implement quoted holes feature
• [x] put quoted holes feature behind pragma option --quote-metas
• [x] update documentation
• [x] update release notes, including link to documentation

[rybla]

Thanks for the review @andreasabel, I'll make the changes you requested soon.

[rybla]

My 50cent bikeshedding: --quoted-metas would have a more grammatical negation --no-quoted-metas.

It seems like the flags don't have a fully standardized part-of-speech form.

I'm happy with either --quote-metas or --quoted-metas for the reasons you both expressed, so just let me know if you've resolved amongst yourselves.

There is a slight majority among other options to be phrased as an active part of speech, so I'm going to stick with --quote-metas unless you've changed your minds.

[rybla]

Thanks for the new feature!

It should be advertised in a CHANGELOG entry, linking to the documentation. Examples can be found in older release notes, see doc/release-notes.

addressed by 383a2338f62121e3905572d525e44ec2153dc683

[rybla]

I found a last little thing I was missing here (3f8ca87b3dadae9ad8ff908288d4789e0621ca10), and I think this PR looks good to go now! It took me a few tries to make sure I was adding the option in all the correct ways. Thanks again @andreasabel for pointing out things like pragmaFlag. Pinging again for final review.

[andreasabel]

Documentation currently rendered at: https://agda--8235.org.readthedocs.build/en/8235/language/quote-metas.html

[rybla]

@andreasabel thanks for all the feedback. I will get around to addressing everything soon, within the next week or so.