This PR parameterises Caesium's operators with a "boolean" result (i.e. the comparison operators as well as the derived && and || operators) by a result integer type (which was hard-coded before to i32) as a step to use Caesium for modelling other C-like languages with different modelling of boolean results (e.g. Rust, which uses single-byte booleans).
Concretely, the changes can be summarised as:
rit to the affected operators and use that for the operational semantics of these operators, replacing the
i32 used before.
lang/c_notations.v that instantiate the operators with
i32 so that the codegen for RefinedC does not need to be changed much, and change the Coq codegen to also import this new file.
i32. Possibly, it might be desirable to support other result types even for C and to generalize the proofs accordingly, but I'm not sure.
The existing examples in the repo compile with these changes, but I haven't tested more exhaustively yet.