search

Deducteam / lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting
Other
268 stars 35 forks source link

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

Open gabrielhdt opened 3 years ago

gabrielhdt commented 3 years ago

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 commented 2 years ago

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