Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve scoping of pattern variables not used in the RHS #675

Open
gabrielhdt opened this issue May 19, 2021 · 1 comment
Open

Improve scoping of pattern variables not used in the RHS #675

gabrielhdt opened this issue May 19, 2021 · 1 comment

Comments

@gabrielhdt
Copy link
Member

The first argument of the Patt data type is an integer option which was once set to None at scoping if the variable was linear and not used in the right hand side, like in

rule $X $Y --> $Y

the variable $X was transformed to Patt(None, "X", [||]) and $Y to Patt(Some(i), "Y", [||]), where i would probably be 1.

Compilation to decision trees relies on the form of this argument for optimisation (it doesn't impact correctness): if the first argument is set to None, than there is no need to remember the subterm matched by the pattern, and it can hence be discarded.

Nowadays, the first argument of patterns is always of the form Some i after scoping. Therefore decision trees backup more terms than needed.

@fblanqui fblanqui changed the title Rewrite rule pattern data type Improve scoping of pattern variables not used in the RHS Dec 15, 2021
@fblanqui
Copy link
Member

fblanqui commented Feb 2, 2022

Note that the fact that there is currently no Patt(None,_,_) is used for computing critical pairs.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants