[Coq backend] Surjection without matching on int31 literal
Currently, the Coq backend of Menhir generates Coq programs which include pattern matching on 31-bit machine integers. The patterns are written as literal values. These literal values are syntactic sugar for their binary decompositions (using the
I31 constructor and the
D1). Thus internally, such pattern matching is represented as thirty-two nested matches (on the
I31 box and then each digit).
This feature (using literal 31-bit values as patterns) may disappear in future versions of Coq (hopefully 8.10), when primitive (63-bit) machine integers are introduced.
Therefore, this PR removes the use of this feature in Coq programs produced by Menhir. The matching on the individual bits of the 31-bit machine integers is made explicit, and the opening of the
I31 box is done through the
int31_rect eliminator of the
int31 data type.
The only noticeable change introduced by this PR is that the generated code is a bit more verbose: patterns use a binary representation instead of a decimal representation. The computational behavior of these
surj functions should be preserved.