Add `define ..` in Pancake

[JunmingZhao42]

Currently it seems that there isn't a way to specify some constants for the transpiler to pick up. For example if someone needs to have a predicate for some EIR register it'd look like this:

/* @ predicate eir_value(eir: Int) {
    (eir == (134217728 | 33554432)) ||
    (eir == 134217728) ||
    (eir == 33554432) ||
    (eir == 0)
}
@*/
// this means EIR should only have its 25 or 27-ith bit set/unset

where the values are sort of hard-coded. And if the same constants need to be used in other pre/post-conditions later, the user would also have to manually type in those constants, which is likely to cause some bugs sometimes.

It'd be nice to be able to specify constants using define ... or something similar in Pancake annotations, such that these constants can be used in predicates and other assertions without writing explicit values.

Anyways, this is more of a feature enhancement request.

[alegnani]

I think the main question here would be were we want this feature and how it should be implemented:

• Using the C preprocessor. Unfortunately it will not perform substitution in comments (we could change the annotation syntax from /*@ ... @*/ to something different)
• In Pancake itself as it might be a useful feature given the very low-level nature of Pancake. This could also be fixed by inline functions.
• In the transpiler

[JunmingZhao42]

I agree it makes sense if this feature can be in Pancake rather than only in the transpiler. I'll follow this up with the Pancake team.