Declaring a static constant with an external name

In ATS2-0.2.8, a static constant can now be declared with an external name:

For instance:

stacst sine_of_real : real -> real = “ext#sin”

This is useful when constraints generated during typechecking are to be
exported
for solving externally. If a static constant is given an external name,
then the external
name is used in exported constraints (otherwise, a name like
sine_of_real!12345 is
used, where 12345 is the stamp attached to the static constant).

Here are some examples that you can try (using the given Makefile):

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST

Cheers!

This is so cool!On Wednesday, June 29, 2016 at 1:24:12 PM UTC-4, gmhwxi wrote:

In ATS2-0.2.8, a static constant can now be declared with an external name:

For instance:

stacst sine_of_real : real → real = “ext#sin”

This is useful when constraints generated during typechecking are to be
exported
for solving externally. If a static constant is given an external name,
then the external
name is used in exported constraints (otherwise, a name like
sine_of_real!12345 is
used, where 12345 is the stamp attached to the static constant).

Here are some examples that you can try (using the given Makefile):

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST

Cheers!