Functions apply_sigma_uf and up_uf_rs are used to update the internal state of the union-find when applying a substitution sigma (a substitution ((p, v, ex) as sigma) represents the substitution p := v with justification ex).
The first function, apply_sigma_uf, is responsible for actually applying the substitution p := v. The second function, up_uf_rs, is responsible for computing normal forms w.r.t. AC rules once the substitution p := v has been applied.
When up_uf_rs finds new representatives, it currently adds them with the explanation justifying p := v, but this is not enough to actually ensure the equality between the old and new representative: it can depend on arbitrary explanations picked up by in the environment by the call to normal_form env rr.
This patch changes up_uf_rs to add the proper explanation in neqs_to_up.
Functions
apply_sigma_uf
andup_uf_rs
are used to update the internal state of the union-find when applying a substitutionsigma
(a substitution((p, v, ex) as sigma)
represents the substitutionp := v
with justificationex
).The first function,
apply_sigma_uf
, is responsible for actually applying the substitutionp := v
. The second function,up_uf_rs
, is responsible for computing normal forms w.r.t. AC rules once the substitutionp := v
has been applied.When
up_uf_rs
finds new representatives, it currently adds them with the explanation justifyingp := v
, but this is not enough to actually ensure the equality between the old and new representative: it can depend on arbitrary explanations picked up by in the environment by the call tonormal_form env rr
.This patch changes
up_uf_rs
to add the proper explanation inneqs_to_up
.