search

tweag / pirouette

Language-generic workbench for building static analysis
MIT License
47 stars 2 forks source link

Modified constraint trees to avoid duplication #18

Closed GuillaumeGen closed 3 years ago

GuillaumeGen commented 3 years ago

Currently the ConstraintTree has a node Choose which takes only a list of Match x ty c args :&: tr which means "If x of type ty is the constructor c, then let args be the name of its arguments and output tr". This implies that the x and ty are declared once for each constructors, whereas they should be common to all branches of the Choose. In particular, if x is a complex term, a new free name fn and a new binding LET fn == x is generated in each branch. This PR redesigns ConstraintTree to eliminate this duplication of code.

VictorCMiraldo commented 3 years ago

This makes sense. Originally, I was expecting that we would use the Fact constraint a little more, hence, Choose was meant not as in "choose constructor" but "choose execution branch". As it turns out, the ConstraintTree is used way less than anticipated, which is a good think! :)