search

ocaml / Zarith

The Zarith library implements arithmetic and logical operations over arbitrary-precision integers and rational numbers. The implementation, based on GMP, is very efficient.
Other
231 stars 70 forks source link

Redefinition of int operators #138

Closed michel1948 closed 1 year ago

michel1948 commented 1 year ago

In all the modules of zarith, it's written, the classic prefix and infix int operators are redefined on t. This decision make difficult the simultaneous use of int and t values. For example, in the context i:int, it's impossible to type (i+1), you must write to_int ((of_int i)+(one)). Why not use a notation like (+t) to distinguish the addition between values of type t, from that noted (+), between values of type int. This would conform to the usage where we distinguish the addition between int type values, denoted (+), and that between float type values denoted (+.).

ghilesZ commented 1 year ago

Personally, I've always considered the shadowing trick to be a feature and not a bug (A feature that I take advantage of here.).

whenever i need to use simultaneously the stdlib integers and Zarith's ones i simply open locally the module i'm using by doing: Int.(x+1) instead of doing the computation using Z and then converting the result into integers.

michel1948 commented 1 year ago

Thank you for your reply. But in your solution, with Int.(x+1), you perform an addition over Z, and the result is converted to type int. I would prefer in a context where x is of type int, to be able to write of_int(x+1) and use the operation that would be denoted (+Z) to add two values of type Z. I wrote a program calculating the Goodstein sequences. In this program, I only use Z-type integers except for a few (of_int i), but I would have liked to mix Z-type and int-type values more easily.

xavierleroy commented 1 year ago

But in your solution, with Int.(x+1), you perform an addition over Z, and the result is converted to type int.

No, this is not what's happening here. Int.(x+1) is just opening the Int module locally, so that the + operator refers to the one defined in module Int, and x + 1 is computed at type int. No conversions between types Z.t and int are involved.

I think this and @ghilesZ 's reply answer the initial question of @michel1948, so I'm taking the liberty to close this issue. Please reopen it with more explanations if we missed something.