When clauses
I promised Jean-Christophe I'd write this long ago..
In functional languages it's a common feature to be able to perform matches on constants. Since why3 doesn't support constant patterns, it complicates translations from languages with support for this functionality.
The challenge with adding this functionality to why3 is that patterns are desugared quite late in the compilation pipeline. Since we would like to desugar a constant pattern into an equality test, this is problematic as we must correctly resolve =
for the type of the matched constant.
An alternative approach which is also more general would be to introduce when
clauses. In this approach, match arms could be annotated with any boolean valued function. This function would have access to any binders created by the match arm's patterns. As this function would get typechecked with the rest of the AST, by the time we get to case-desugaring we should have no difficulty transforming it into a boolean test.
During a GT a few weeks ago we discussed this and several challenges and alternative solutions were proposed, unfortunately I didn't take notes at time and I no longer recall them.