Declaring a static constant with an external name

[gmhwxi]

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!

[Steinway Wu]

This is so cool!

[Steinway Wu]

I encountered a problem.

Say I have this in the ATS code

stacst set_emp: set = "ext@smt_set_emp"

and this in the smt2 code

(define-const smt_set_emp (Set) ((as const (Set)) false))

`--constraint-export` is able to translate all static applications of `smt_emp` to `smt_set_emp`. 

However, it emits an extra definition which I don't want to have. 

(declare-fun smt_set_emp () Set)

What is your usual use case? Maybe we should remove this from emitted code. 

On Wednesday, June 29, 2016 at 1:24:12 PM UTC-4, gmhwxi wrote:

[Steinway Wu]

I put up a PR for your consideration. https://github.com/githwxi/ATS-Postiats/pull/170