Stadef: are the bindings overloadable?

[Yannick Duchêne]

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?

[gmhwxi]

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.

[Yannick Duchêne]

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?

[gmhwxi]

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.

[Yannick Duchêne]

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.  

[Hongwei Xi]

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()

--
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.