Today I saw this, which surprised me:
stadef string = string1 // 2nd-select
stadef string = string0 // 1st-select
It’s in basics_sta.sats, at line 502 and 503.
it looks like an overloading, and the comment seems to confirm this (in the
spirit of “first match win”). At least, the second stadef string = …
seems to not hide the first one.
Before this, I saw it used as in
http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3039.html
, where it seems to work like a static val.
I also though one could use stadef instead of typedef, which would just
be less readable, and now I’m less sure.
What’s exactly stadef and how does it work?
I’ve seen stacst in the newsgroup. This one looks strange to me, as I can’t
see how a stadef could not be constant.
What is stacst, and how does it differs from stadef? What is constant is
constant with it which would not be otherwise?Le mercredi 13 mai 2015 03:07:25 UTC+2, gmhwxi a écrit :
First, typedef is just a special case of stadef.
If you do
typedef foo = some_def
the some_def is required to be of the sort t@ype
(type is a subsort of t@ype).
If two static constants are given the same name, ATS tries
to use their sorts to determine which one should be chosen.
If both can be chosen, then the one introduced later is actually
chosen.
On Tuesday, May 12, 2015 at 8:30:31 PM UTC-4, Yannick Duchêne wrote:
Today I saw this, which surprised me:
stadef string = string1 // 2nd-select
stadef string = string0 // 1st-select
It’s in basics_sta.sats, at line 502 and 503.
it looks like an overloading, and the comment seems to confirm this (in
the spirit of “first match win”). At least, the second stadef string = …
seems to not hide the first one.
Before this, I saw it used as in
http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3039.html
, where it seems to work like a static val.
I also though one could use stadef instead of typedef, which would
just be less readable, and now I’m less sure.
What’s exactly stadef and how does it work?
First, typedef is just a special case of stadef.
A question on the edge… When a stacst comes later after a typedef and both
have the same name and both have no parameters, the stacst always hides the
typedef or is there a way to refer to one or the other using a
disambiguation syntax?
I guess it always definitively hides, but I prefer to ask, to be sure.
First, typedef is just a special case of stadef.
If you do
typedef foo = some_def
the some_def is required to be of the sort t@ype
(type is a subsort of t@ype).
If two static constants are given the same name, ATS tries
to use their sorts to determine which one should be chosen.
If both can be chosen, then the one introduced later is actually
chosen.On Tuesday, May 12, 2015 at 8:30:31 PM UTC-4, Yannick Duchêne wrote:
Today I saw this, which surprised me:
stadef string = string1 // 2nd-select
stadef string = string0 // 1st-select
It’s in basics_sta.sats, at line 502 and 503.
it looks like an overloading, and the comment seems to confirm this (in
the spirit of “first match win”). At least, the second stadef string = …
seems to not hide the first one.
Before this, I saw it used as in
http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3039.html
, where it seems to work like a static val.
I also though one could use stadef instead of typedef, which would
just be less readable, and now I’m less sure.
What’s exactly stadef and how does it work?
A stacst is an abstract static constant;
it is supposed to be interpreted by the constraint-solver.
For instance:
stacst factorial: int → int
extern factorial_dyn{n:nat} (n: int(n)): int(factorial(n))
In order to implement factorial_dyn, you have to make sure that the
constraint-solver
understands the meaning of factorial.On Wednesday, May 13, 2015 at 11:20:12 AM UTC-4, Yannick Duchêne wrote:
I’ve seen stacst in the newsgroup. This one looks strange to me, as I
can’t see how a stadef could not be constant.
What is stacst, and how does it differs from stadef? What is constant is
constant with it which would not be otherwise?
Le mercredi 13 mai 2015 03:07:25 UTC+2, gmhwxi a écrit :
First, typedef is just a special case of stadef.
If you do
typedef foo = some_def
the some_def is required to be of the sort t@ype
(type is a subsort of t@ype).
If two static constants are given the same name, ATS tries
to use their sorts to determine which one should be chosen.
If both can be chosen, then the one introduced later is actually
chosen.
On Tuesday, May 12, 2015 at 8:30:31 PM UTC-4, Yannick Duchêne wrote:
Today I saw this, which surprised me:
stadef string = string1 // 2nd-select
stadef string = string0 // 1st-select
It’s in basics_sta.sats, at line 502 and 503.
it looks like an overloading, and the comment seems to confirm this (in
the spirit of “first match win”). At least, the second stadef string = …
seems to not hide the first one.
Before this, I saw it used as in
http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3039.html
, where it seems to work like a static val.
I also though one could use stadef instead of typedef, which would
just be less readable, and now I’m less sure.
What’s exactly stadef and how does it work?
Note that ‘typedef’ simply introduces a stacst. If there is another stacst
introduced
later of the same name and sort, then it shadows the previous one.
Technically speaking, ‘typedef’ (and ‘stadef’) can be replaced as follows:
Say you have
typedef myint = int64
You can achieve this by doing
stacst myint : t@ype
extern praxi lemma_myint(): EQTYPE(myint, int64)
Whenever you need to equate myint and int64, just do
prval EQTYPE() = lemma_myint()On Sun, May 17, 2015 at 10:34 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:
Le mercredi 13 mai 2015 03:07:25 UTC+2, gmhwxi a écrit :
First, typedef is just a special case of stadef.
A question on the edge… When a stacst comes later after a typedef and both
have the same name and both have no parameters, the stacst always hides the
typedef or is there a way to refer to one or the other using a
disambiguation syntax?
I guess it always definitively hides, but I prefer to ask, to be sure.
–
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/13740bcb-43af-4c1d-aa22-d0ec45d724d4%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/13740bcb-43af-4c1d-aa22-d0ec45d724d4%40googlegroups.com?utm_medium=email&utm_source=footer
.