Part of #2829: Allow instance arguments in pattern synonyms that are such in the pattern already #7173
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…aInfo
We can now remember in the abstract syntax `Underscore` which kind of
meta we want to generate: a `UnificationMeta` (default) or an
`InstanceMeta`. The latter is not used yet here but will be needed
for `{{_}}` arguments created by the expansion of pattern synonyms.
Having `data MetaKind(InstanceMeta,UnificationMeta)` we also refactor
`MetaInstantiation(Open,OpenInstance)` into a single parameterized
constructor `OpenMeta MetaKind`. This helps condensing pattern
matching in several locations, where `Open` and `OpenInstance` behaved
the same.
I considered keeping `Open` and `OpenInstance` as pattern synonym but
it wasn't worth it.
There was already a type `MetaKind` for directing eta-expansion for
metas. This is a more obscure use than specifying the solution
strategy for a meta, so I bumped this, calling it `MetaClass` now.
This type is local to a only couple of modules, so renaming seems ok.
Changing the order of arguments in `Rules.Term.checkUnderscore` and
friends seemed also natural.
Since `newInteractionMetaArg` was never used to create an instance
meta, I simplified its code.
... if they are instance arguments on the rhs as well. To check this, we equip the scope checker with `Hiding` information for `PatternBound` local variables, and propagate the hiding info from `Arg` to the pattern scope checker by means of a new throw-away type `WithHidingInfo` (to not clash with the existing `WithHiding`). This commit achieves that instance arguments that come to surface through pattern matching on a pattern synoym are available for instance search, just if one would match against the pattern the synonym stands for.
…ions.
If a pattern synonym is used in an expression, we need to make sure
that its instance arguments become instance metas.
Agda only turns an instance argument into an instance meta when the
argument is entirely omitted. That is, `{{_}}` does not create an
instance meta, but this is exactly what the pattern synonym expansion
produces in expressions.
Having added `metaKind` to the `MetaInfo` record, we can now create
instance underscores in the abstract syntax, which fixes our dilemma.
815df0f to
426d699
Compare
|
Added changelog entry. |
jespercockx
approved these changes
Mar 8, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
3 commits, checked by CI individually:
1. Refactor for #2829: Add MetaKind(InstanceMeta,UnificationMeta) to MetaInfo
We can now remember in the abstract syntax
Underscorewhich kind of meta we want to generate: aUnificationMeta(default) or anInstanceMeta. The latter is not used yet here but will be needed for{{_}}arguments created by the expansion of pattern synonyms.Having
data MetaKind(InstanceMeta,UnificationMeta)we also refactorMetaInstantiation(Open,OpenInstance)into a single parameterized constructorOpenMeta MetaKind. This helps condensing pattern matching in several locations, whereOpenandOpenInstancebehaved the same.I considered keeping
OpenandOpenInstanceas pattern synonym but it wasn't worth it.There was already a type
MetaKindfor directing eta-expansion for metas. This is a more obscure use than specifying the solution strategy for a meta, so I bumped this, calling itMetaClassnow. This type is local to a only couple of modules, so renaming seems ok.Changing the order of arguments in
Rules.Term.checkUnderscoreand friends seemed also natural.Since
newInteractionMetaArgwas never used to create an instance meta, I simplified its code.2. Allow instance arguments in pattern synonyms lhss...
... if they are instance arguments on the rhs as well.
To check this, we equip the scope checker with
Hidinginformation forPatternBoundlocal variables, and propagate the hiding info fromArgto the pattern scope checker by means of a new throw-away typeWithHidingInfo(to not clash with the existingWithHiding).This commit achieves that instance arguments that come to surface through pattern matching on a pattern synoym are available for instance search, just if one would match against the pattern the synonym stands for.
3. Make instance arguments in pattern synonyms work in expressions.
If a pattern synonym is used in an expression, we need to make sure that its instance arguments become instance metas.
Agda only turns an instance argument into an instance meta when the argument is entirely omitted. That is,
{{_}}does not create an instance meta, but this is exactly what the pattern synonym expansion produces in expressions.Having added
metaKindto theMetaInforecord, we can now create instance underscores in the abstract syntax, which fixes our dilemma.