This is certainly a big issue for people to learn ATS.
g0: ‘g’ for generic; ‘0’ for un-indexed
g1: ‘g’ for generic’ ‘1’ for indexed
So g0int2uint_int_size means it is for turning a signed integer (int) into
an unsigned integer (size_t).
So g1int2uint_int_size means it is also for turning a signed integer (int)
into an unsigned integer (size_t).
However, the type for the latter is more accurate:
{n:nat} int(i) → size_t(i)
which states that the signed integer is a natural number and the returned
unsigned integer has the same value as the signed one.
As you can see, there is a lot to memorize. When you write ATS code, I
suggest that you use $UN.cast (and various variants of it):
staload UN = “prelude/SATS/unsafe.sats”
val x = $UN.cast{size_t}(31415926)
Of course, $UN.cast is unsafe but it can get you going very quickly.
Also, there are many overloaded names.
For instance, g0i2u for g0int2uint_…; g0u2i for g0uint2int …; g0i2f for
g0int2float_…; g0f2i for g0float2int_…
But $UN.cast is your swiss army knife :)On Wednesday, January 28, 2015 at 8:43:56 AM UTC-5, Andrea Ferretti wrote:
Hello, I am trying to learn ATS following the official book, and I am
finding some difficulties with the names chosen. For instance, a sort for
types of variable dimension is called t@ype, the type of arrays of type T
is arrszref[T], and the function to convert between int and size_t is
called g0int2uint_int_size.
I know it is quite a trivial matter, but I find it very difficult to
follow the code examples without remembering these names. Is there some
naming convention or scheme behind this?
