stacst: abstract or not abstract?

[Yannick Duchêne]

I though stacst introduces abstract constants, but a simple test seems to contradict this supposition.

        absprop p

        absprop q

        assume p = q // OK.

        stacst i: int

        stacst j: int

        assume i = j // Complains “the static constant [i] is not abstract.”

I though i and j are abstract since they are not given any concrete value (neither hidden).

Where is this wrong? In supposing i and j are abstract or in supposing `assume` applies to all abstract things?

[Richard]

Here are some examples that may help clarify,

there is a mention of stacst here: https://groups.google.com/d/msg/ats-lang-users/M3ie38z1_hY/dpmMLHcwFQAJ

and an example here: https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/INTRO/fact_uninterp.dats#L8-L13

[Yannick Duchêne]

Le mardi 24 juillet 2018 18:00:59 UTC+2, Richard a écrit :

Here are some examples that may help clarify,

there is a mention of stacst here: https://groups.google.com/d/msg/ats-lang-users/M3ie38z1_hY/dpmMLHcwFQAJ

and an example here: https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/INTRO/fact_uninterp.dats#L8-L13

I’m silly, just forget to search for it here (Usually I do).

For now, I’m confused but prefer not say anything more to not say anything too stupid (shy). In few words, I though it was for versatile abstract definitions.

[Yannick Duchêne]

In https://groups.google.com/d/msg/ats-lang-users/oCr35CMrIr0/ymwJ4mUwNY4J :

> A stacst is an abstract static constant;

> it is supposed to be interpreted by the constraint-solver.

So that’s indeed abstract, but its use is just restricted, I guess.

[gmhwxi]

'stacst' is used to introduce a name for a constant of

a chosen predicative sort. For instance,

stacst pi: real

You may want to introduce some properties on 'pi'.

For instance:

praxi pi_lemma : () -> [pi > 3.14159] void

Theoretically, you can also introduce a constant of some

impredicative sort in this way. But it is not supported. You need

to use 'abstype', 'absprop', 'absview', etc.