Naming convention
139 views
Skip to first unread message
Andrea Ferretti
Jan 28, 2015, 8:43:56 AM1/28/15
to ats-lan...@googlegroups.com
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?
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?
Brandon Barker
Jan 28, 2015, 10:00:32 AM1/28/15
to ats-lang-users
This seems to be a common problem, though I'm not sure if it is totally circumventable due to the wide variety of types in ATS. I hope it can be improved.
The first part, 'g0', denotes we are dealing with non-indexed types (int instead of int (i)).
The second part, I think, is showing the general class of type conversion: int 2 uint
The third part shows the actual ats types ... somewhat. The latter is size_t instead of size, so this mix of highly systematic and somewhat lax naming is a bit disconcerting if I'm reading it right.
On Wed, Jan 28, 2015 at 8:43 AM, Andrea Ferretti <ferrett...@gmail.com> 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?
--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/e7afa080-5e5f-4709-8f2d-199df647469e%40googlegroups.com.
Brandon Barker
Jan 28, 2015, 10:01:10 AM1/28/15
to ats-lang-users
Also you can generally find more insight by looking int he sats file where it is defined:
$ find ./ -name '*.sats' | xargs grep g0int2uint_int_size
./prelude/SATS/CODEGEN/integer.sats:fun g0int2uint_int_size (x: int):<> size_t = "mac#%"
./prelude/SATS/integer.sats:fun g0int2uint_int_size (x: int):<> size_t = "mac#%"
--
Andrea Ferretti
Jan 28, 2015, 10:12:07 AM1/28/15
to ats-lan...@googlegroups.com
I am speculating, since I have not read that far: but maybe the naming
could be improved by having a module (namespacing) system? If I
understand correctly your response, the naming scheme seems to arise
to have a global naming scheme without conflicts.
Has some namespacing mechanism been proposed for ATS?
> You received this message because you are subscribed to a topic in the
> Google Groups "ats-lang-users" group.
> To unsubscribe from this topic, visit
> https://groups.google.com/d/topic/ats-lang-users/4djRxVNHAys/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to
could be improved by having a module (namespacing) system? If I
understand correctly your response, the naming scheme seems to arise
to have a global naming scheme without conflicts.
Has some namespacing mechanism been proposed for ATS?
> Google Groups "ats-lang-users" group.
> To unsubscribe from this topic, visit
> https://groups.google.com/d/topic/ats-lang-users/4djRxVNHAys/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to
> ats-lang-user...@googlegroups.com.
> To post to this group, send email to ats-lan...@googlegroups.com.
> Visit this group at http://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/CAORbNRqbZwtAr%2BQ2XdRAVeFP-ztaDE5UUkPcXByVXzvdF2C3uw%40mail.gmail.com.
> To post to this group, send email to ats-lan...@googlegroups.com.
> Visit this group at http://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
Brandon Barker
Jan 28, 2015, 10:15:38 AM1/28/15
to ats-lang-users
Yes, this functionality exist through named importing (staloading). I'm not certain it would help as you'd still have to keep track of many namespaces.
staload UN = "predude/SATS/unsafe.sats"
$UN.cast(...)
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAMF%3D6sJ97eicPGtBdMn13uCEMu%3DN8E%3D9D5itipk2-cVCPeWc5w%40mail.gmail.com.
Brandon Barker
Jan 28, 2015, 10:16:23 AM1/28/15
to ats-lang-users
--
Andrea Ferretti
Jan 28, 2015, 10:17:41 AM1/28/15
to ats-lan...@googlegroups.com
Thank you, this clarifies quite a bit
> https://groups.google.com/d/msgid/ats-lang-users/CAORbNRqqN4W3weYkPofY2U9sMOo_bTdWw_uv5GX7vBKBrTMMGQ%40mail.gmail.com.
Shea Levy
Jan 28, 2015, 11:56:22 AM1/28/15
to ats-lan...@googlegroups.com
On Jan 28, 2015, at 3:00 PM, Brandon Barker <brandon...@gmail.com> wrote:$ find ./ -name '*.sats' | xargs grep g0int2uint_int_size
FYI, git grep is a nicer way to do this if you’re in a git checkout.
Brandon Barker
Jan 28, 2015, 12:06:39 PM1/28/15
to ats-lang-users
Thanks for the tip! Learning git is also a long process for me. FYI these will show the atxt files which are used by Hongwei to generate the .sats files while also being used to generate documentation (so I guess you'd say it is a form of literate programming):
[brandon@localhost ATS-Postiats]$ git grep g0int2uint_int_size
doc/BOOK/INT2PROGINATS/CHAP_EFFECTFUL/main.atxt:#stacode("size_t") are #dyncode("g0int2uint_int_size") and
doc/BOOK/INT2PROGINATS/CHAP_EFFECTFUL/main.atxt: \#define i2sz g0int2uint_int_size
doc/BOOK/INT2PROGINATS/CODE/CHAP_EFFECTFUL/permord.dats: #define i2sz g0int2uint_int_size
prelude/CATS/CODEGEN/integer.atxt:\#define atspre_g0int2uint_int_size(x) ((atstype_size)(x))
prelude/CATS/CODEGEN/integer.atxt:\#define atspre_g1int2uint_int_size atspre_g0int2uint_int_size
prelude/DATS/CODEGEN/integer.atxt:g0int2uint<intknd,sizeknd> = g0int2uint_int_size
prelude/SATS/CODEGEN/integer.atxt:fun g0int2uint_int_size (x: int):<> size_t = "mac\#%"
--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/68F72F48-5E9C-49F4-9049-964EA6705A4E%40shealevy.com.
Shea Levy
Jan 28, 2015, 12:11:36 PM1/28/15
to ats-lan...@googlegroups.com
You can also limit searched files with something like
$ git grep g0int2uint_int_size -- '*.sats’
But of course since those files are generated they don’t exist in my tree :)
~Shea
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAORbNRoygifiPUejpoUMquB-XYD2woY1n36XJjrYbNm%2B6_v2hw%40mail.gmail.com.
gmhwxi
Jan 28, 2015, 12:28:11 PM1/28/15
to ats-lan...@googlegroups.com
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 :)
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 :)
Andrea Ferretti
Jan 28, 2015, 12:39:27 PM1/28/15
to ats-lan...@googlegroups.com
Ok, I am starting to see the rationale. Still, I am under the
impression that making the prelude more modular would have allowed
such uses as
staload UN = "prelude/SATS/unindexed-cast.sats"
staload IN = "prelude/SATS/indexed-cast.sats"
$UN.int2size_t(x) // = g0int2uint_int_size(x)
$UN.size_t2int(x) // = g0uint2int_size_int(x)
$IN.int2size_t(x) // = g1int2uint_int_size(x)
$IN.size_t2int(x) // = g1uint2int_size_int(x)
Anyway, I am looking forward to learning more while using $UN.cast in
the meantime! :-)
> --
> You received this message because you are subscribed to a topic in the
> Google Groups "ats-lang-users" group.
> To unsubscribe from this topic, visit
> https://groups.google.com/d/topic/ats-lang-users/4djRxVNHAys/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to
impression that making the prelude more modular would have allowed
such uses as
staload UN = "prelude/SATS/unindexed-cast.sats"
staload IN = "prelude/SATS/indexed-cast.sats"
$UN.int2size_t(x) // = g0int2uint_int_size(x)
$UN.size_t2int(x) // = g0uint2int_size_int(x)
$IN.int2size_t(x) // = g1int2uint_int_size(x)
$IN.size_t2int(x) // = g1uint2int_size_int(x)
Anyway, I am looking forward to learning more while using $UN.cast in
the meantime! :-)
> You received this message because you are subscribed to a topic in the
> Google Groups "ats-lang-users" group.
> To unsubscribe from this topic, visit
> https://groups.google.com/d/topic/ats-lang-users/4djRxVNHAys/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to
> ats-lang-user...@googlegroups.com.
> To post to this group, send email to ats-lan...@googlegroups.com.
> Visit this group at http://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/0e005458-c775-4a31-a2c0-4751442d3560%40googlegroups.com.
> To post to this group, send email to ats-lan...@googlegroups.com.
> Visit this group at http://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
Yannick Duchêne
Feb 1, 2015, 1:20:57 PM2/1/15
to ats-lan...@googlegroups.com
I have a related question: is this on purpose if the sort `t0p` cannot be written as `t@p`?
Hongwei Xi
Feb 1, 2015, 1:41:11 PM2/1/15
to ats-lan...@googlegroups.com
t@p is not a valid identifier.
The parser can only recognize t@ype, which can also be written as t0ype.
The parser can only recognize t@ype, which can also be written as t0ype.
--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/f16ae971-c0be-462a-af1b-2b0497fde96b%40googlegroups.com.
Reply all
Reply to author
Forward
0 new messages