Patterns define new local variables.
This module collect them and preprocess
_ occurring in patterns.
Recall that an
_ may represent anonymous variables or inaccessible terms
that are implied by typing constraints. Thus, we represent them with fresh named holes
After we elaborate the pattern, if the metavariable remains unassigned, we transform it into
a regular pattern variable. Otherwise, it becomes an inaccessible term.
Macros occurring in patterns are expanded before the
collectPatternVars method is executed.
The following kinds of Syntax are handled by this module
- Constructor applications
- Applications of functions tagged with the
- Anonymous constructors
- Structure instances
- Inaccessible terms
- Named patterns
- Tuple literals
- Type ascriptions
- Literals: num, string and char
An application in a pattern can be
1- A constructor application The elaborator assumes fields are accessible and inductive parameters are not accessible.
2- A regular application
(f ...) where
f is tagged with
The elaborator assumes implicit arguments are not accessible and explicit ones are accessible.
stx is a pattern variable or constructor-like (i.e., constructor or constant tagged with
Return the pattern variables in the given pattern.
Remark: this method is not used by the main
match elaborator, but in the precheck hook and other macros (e.g., at