As talked about offline with @bclement-ocp (cc Issue #209 ), there is small bug in the current handling of attributes in nested binders, where some attributes were duplicated before PR #207, and are now instead ignored/dropped in some cases.
For instance, if one has explicit nested forall quantifiers, and one of the intermediates quantifiers (which is therefore the body of another quantifier) has some pattern/trigger annotations, those were duplicated before (and therefore in released versions of dolmen) and are dropped on the current master branch. This PR fixes all of that.
More details
The bug is due to the typechecker of Dolmen trying to collapse together nested quantifiers. For instance if one writes forall x : Int. forall y : Int. x = y, then dolmen tries to treat that the same as it was written as forall x : Int, y : int. x = y. This is marginally useful in the quantifier case, but can save a lot of memory when dealing with let-bindings, since this allows to allocate a single expression node to bind n variables, instead of n expression nodes.
The functions that perform this collapsing have had rougly two behaviours:
drop/ignore the attribtues (this is the case for quantifiers after #207 )
duplicate the attributes on the body as well as the bound formulas (this is the case for quantifiers before #207 , and for sequential let-binders which were not touched by #207 )
While the dropping of attributes is undeniably worse that duplicating them, this PR solves the two problems and makes it so that attributes are only typed once and attached to the same formula as in the source. This is done relatively easy by simply not doing the collapsing if there are any attributes on the intermediate bindings formulas.
To help in debugging situations such as this, the first commit of this PR introduces a way to print the tags of typed expressions (which was not done/easy to do before). This required to change the implementation of heterogeneous maps, which is actually not bad since we now depend on dbunzli's hmap package instead of copying the container implementation.
TL; DR
As talked about offline with @bclement-ocp (cc Issue #209 ), there is small bug in the current handling of attributes in nested binders, where some attributes were duplicated before PR #207, and are now instead ignored/dropped in some cases.
For instance, if one has explicit nested forall quantifiers, and one of the intermediates quantifiers (which is therefore the body of another quantifier) has some pattern/trigger annotations, those were duplicated before (and therefore in released versions of dolmen) and are dropped on the current
masterbranch. This PR fixes all of that.More details
The bug is due to the typechecker of Dolmen trying to collapse together nested quantifiers. For instance if one writes
forall x : Int. forall y : Int. x = y, then dolmen tries to treat that the same as it was written asforall x : Int, y : int. x = y. This is marginally useful in the quantifier case, but can save a lot of memory when dealing with let-bindings, since this allows to allocate a single expression node to bindnvariables, instead ofnexpression nodes.The functions that perform this collapsing have had rougly two behaviours:
While the dropping of attributes is undeniably worse that duplicating them, this PR solves the two problems and makes it so that attributes are only typed once and attached to the same formula as in the source. This is done relatively easy by simply not doing the collapsing if there are any attributes on the intermediate bindings formulas.
To help in debugging situations such as this, the first commit of this PR introduces a way to print the tags of typed expressions (which was not done/easy to do before). This required to change the implementation of heterogeneous maps, which is actually not bad since we now depend on dbunzli's hmap package instead of copying the container implementation.