|
Dear devs, in an attempt to simplify the code of intro patterns we came up with a proposal that:
- simplifies the code of the plugin
- breaks only one line in the entire mathcomp, the one fixed by this patch.
The code we want to simplify is the one deferring clear switches inside an intro pattern.
The implementation is tricky because just delaying the clear switch until the end of the pattern is not enough, for example:
```
move=> {x} /andP[x y].
```
In this case `x` is both cleared and used. In order to be able to use `x`, given that the clear has not been performed yet, we rename `x` into `_x_` (when `{x}` is executed) so that when `x` is later executed we can use the name `x`, and then `.` is executed clear `_x_` instead of `x`.
So systematically "always rename now & clear later" seem to be OK, but it is not. The extra complication is that "rename" may break later intro pattern using terms as views. Eg
```
move=> {x} /andP[Ha Hb] /x.
```
What the code does today is:
- when `{x}` is execute look-ahead in the patter and see if `x` is used as a name to be introduced
- if so, "rename"
- otherwise don't rename (just delay)
This way of doing things is not only complicated but also incomplete, Eg
```
move=> {x} /orP[x | /x].
```
would misbehave, since the look-ahead is not "semantic".
Anyway, the proposed behavior is:
- `{x}` always renames now and clears (the renamed) later
- `{clears}/views` is always "compiled" as `/views{clears}` (most of the occurrences in the library are ok with this simpler rule, but for the one fixed in this PR).
- bonus: support `{}/view` (as in `rewrite {}rule`) to signal that the immediately following `view` has to be cleared, that is `{}/v` compiled as `/v{v}`.
What do you think?
```
```
|
