Only whistle on equal integers

[hirrolot]

Right now, we use the following algorithm to decide embedding of integers:

https://github.com/mazeppa-dev/mazeppa/blob/af31d010894c7d529d59bf95e8435209a33b3ee5/lib/algebra/homeomorphic_emb.ml#L5-L17

It makes perfect sense for big integers, but in Mazeppa, we only have fixed-size integers. Since the set of all integers is finite, we can treat each integer as a unique zero-arity constructor. With this enhancement, functions could iterate in any order -- e.g., not only from N to 0, but also from 0 to N.

For example, examples/imperative-vm/main.mz specialized to Int(2i32):

main() :=
    let env := Cell("a", Int(2i32), Cell("x", Int(7u32), Nil()));
    fetchCell(evalProgram(example(), env), "out");

would be optimized into a constant:

main() := Int(128i32);

However, with our current implementation of decide_ints, Mazeppa performs over-generalization which prevents the optimization. The proposal can be summarized as follows:

let decide_ints (x, y) = Checked_oint.equal_generic x y

[hirrolot]

This enhancement allowed Mazeppa to optimize out mc91(n) for any fixed n!