What exactly do `prfun` and `prval`?

Google Group
1

Basic questions, but I really have to ask… I’m not sure to really
understand what prfun/prfn and prval do.

What’s exactly the result of a proof function? Most seems to return void,
but some returns a result. Is this a static value? Are proof functions
simply static functions?

What happens when the result of a proof function is bound to a prval or
especially matched with ()? Does it makes ATS (the checker, not the
language) store some confirmed hypotheses internally? If yes, then is there
a way to “dump” these hypotheses?

How does a proof “returned” by a proof function differs from a proof
returned along with a result from a dynamic function?

2

I pasted an example of internal constraints:

It is incomplete. Just to give people an idea …On Monday, February 9, 2015 at 8:29:16 PM UTC-5, gmhwxi wrote:

In the following file:

https://github.com/githwxi/ATS-Postiats/blob/master/prelude/basics_dyn.sats

you will find the following functions:

prfun prop_verify{b:bool | b} (): void
prfun prop_verify_and_add{b:bool | b} (): [b] void

Say at one point, you want to know if (i==j) holds. You
do this by adding the following line:

prval () = prop_verify{i==j}()

Yes. But not in a form that is readable.

I don’t mind, this is still better than nothing :stuck_out_tongue:

It is really really not readable :slight_smile:

What you see is millions of bytes of internal syntax trees. Try
the following command line on your own:

patsopt -tc --constraint-export -d
${PATSHOME}/doc/EXAMPLE/ATSLF/sqrt2_irrat.dats

On Monday, February 9, 2015 at 8:15:19 PM UTC-5, Yannick Duchêne wrote:

Le mardi 10 février 2015 01:58:44 UTC+1, gmhwxi a écrit :

A proof-value is in the dynamics of ATS.

That was good to ask… I was so wrong…

Thanks for the notice!

If yes, then is there a way to “dump” these hypotheses?

Yes. But not in a form that is readable.

I don’t mind, this is still better than nothing :stuck_out_tongue: . Is this using a
special keyword like $showtype?

3

Yes.On Monday, February 9, 2015 at 9:03:21 PM UTC-5, Brandon Barker wrote:

So i and j are static variables in the above? Assuming so since we are
using ‘==’.

On Mon, Feb 9, 2015 at 8:29 PM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

In the following file:

https://github.com/githwxi/ATS-Postiats/blob/master/prelude/basics_dyn.sats

you will find the following functions:

prfun prop_verify{b:bool | b} (): void
prfun prop_verify_and_add{b:bool | b} (): [b] void

Say at one point, you want to know if (i==j) holds. You
do this by adding the following line:

prval () = prop_verify{i==j}()

Yes. But not in a form that is readable.

I don’t mind, this is still better than nothing :stuck_out_tongue:

It is really really not readable :slight_smile:

What you see is millions of bytes of internal syntax trees. Try
the following command line on your own:

patsopt -tc --constraint-export -d
${PATSHOME}/doc/EXAMPLE/ATSLF/sqrt2_irrat.dats

On Monday, February 9, 2015 at 8:15:19 PM UTC-5, Yannick Duchêne wrote:

Le mardi 10 février 2015 01:58:44 UTC+1, gmhwxi a écrit :

A proof-value is in the dynamics of ATS.

That was good to ask… I was so wrong…

Thanks for the notice!

If yes, then is there a way to “dump” these hypotheses?

Yes. But not in a form that is readable.

I don’t mind, this is still better than nothing :stuck_out_tongue: . Is this using a
special keyword like $showtype?

–
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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
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/7b89dc49-9b1e-4378-9d58-be334d10d7ca%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/7b89dc49-9b1e-4378-9d58-be334d10d7ca%40googlegroups.com?utm_medium=email&utm_source=footer
.

–
Brandon Barker
brand...@gmail.com <javascript:>

4

A proof-value is in the dynamics of ATS.

That was good to ask… I was so wrong…

Thanks for the notice!

If yes, then is there a way to “dump” these hypotheses?

Yes. But not in a form that is readable.

I don’t mind, this is still better than nothing :stuck_out_tongue: . Is this using a
special keyword like $showtype?

5

A proof-value is in the dynamics of ATS.

prfun/prfn/prval are used to form bindings between names and proof values.

The main difference between a proof-value and a program-value (that is,
non-proof-value)
is that the former can never have any influence the construction of the
latter. So therefore,
proof values are all erased after type-checking.

What’s exactly the result of a proof function? Most seems to return void,
but some returns a result. Is this a static value? Are proof functions
simply static functions?

The result of a proof function is a proof value. Proof functions are not
static functions; they are dynamic.

What happens when the result of a proof function is bound to a prval or
especially matched with ()? Does it makes ATS (the checker, not the
language) store some confirmed hypotheses internally? If yes, then is there
a way to “dump” these hypotheses?

Say we have

prfun lemma_fib{n:nat}{r:int}(FIB(n, r)): [n <= r+1] void // fib(n)+1 >= n

Suppose that pf is a proof-value of the prop FIB(N, R) for some N and R

The the following declaration adds (N <= R+1) to the internal store of
currently available assumptions:

prval () = lemma_fib(pf)

If yes, then is there a way to “dump” these hypotheses?

Yes. But not in a form that is readable.

How does a proof “returned” by a proof function differs from a proof
returned along with a result from a dynamic function?

There is no difference.On Monday, February 9, 2015 at 7:41:06 PM UTC-5, Yannick Duchêne wrote:

Basic questions, but I really have to ask… I’m not sure to really
understand what prfun/prfn and prval do.

What’s exactly the result of a proof function? Most seems to return void,
but some returns a result. Is this a static value? Are proof functions
simply static functions?

What happens when the result of a proof function is bound to a prval or
especially matched with ()? Does it makes ATS (the checker, not the
language) store some confirmed hypotheses internally? If yes, then is there
a way to “dump” these hypotheses?

How does a proof “returned” by a proof function differs from a proof
returned along with a result from a dynamic function?

6

So i and j are static variables in the above? Assuming so since we are
using ‘==’.On Mon, Feb 9, 2015 at 8:29 PM, gmhwxi gmh...@gmail.com wrote:

In the following file:

https://github.com/githwxi/ATS-Postiats/blob/master/prelude/basics_dyn.sats

you will find the following functions:

prfun prop_verify{b:bool | b} (): void
prfun prop_verify_and_add{b:bool | b} (): [b] void

Say at one point, you want to know if (i==j) holds. You
do this by adding the following line:

prval () = prop_verify{i==j}()

Yes. But not in a form that is readable.

I don’t mind, this is still better than nothing :stuck_out_tongue:

It is really really not readable :slight_smile:

What you see is millions of bytes of internal syntax trees. Try
the following command line on your own:

patsopt -tc --constraint-export -d
${PATSHOME}/doc/EXAMPLE/ATSLF/sqrt2_irrat.dats

On Monday, February 9, 2015 at 8:15:19 PM UTC-5, Yannick Duchêne wrote:

Le mardi 10 février 2015 01:58:44 UTC+1, gmhwxi a écrit :

A proof-value is in the dynamics of ATS.

That was good to ask… I was so wrong…

Thanks for the notice!

If yes, then is there a way to “dump” these hypotheses?

Yes. But not in a form that is readable.

I don’t mind, this is still better than nothing :stuck_out_tongue: . Is this using a
special keyword like $showtype?

–
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/7b89dc49-9b1e-4378-9d58-be334d10d7ca%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/7b89dc49-9b1e-4378-9d58-be334d10d7ca%40googlegroups.com?utm_medium=email&utm_source=footer
.

Brandon Barker
brandon...@gmail.com

7

A proof-value is in the dynamics of ATS.

That was good to ask… I was so wrong…

Wow, me too. So maybe I’m confused about what “dynamics” means. I was
thinking it was anything that could have a representation in the generated
code (e.g. C code).

Thanks for the notice!

If yes, then is there a way to “dump” these hypotheses?

Yes. But not in a form that is readable.

I don’t mind, this is still better than nothing :stuck_out_tongue: . Is this using a
special keyword like $showtype?

–
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/243d6361-c934-4658-a338-75d550f4eab9%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/243d6361-c934-4658-a338-75d550f4eab9%40googlegroups.com?utm_medium=email&utm_source=footer
.

Brandon Barker
brandon...@gmail.com

8

A proof-value is in the dynamics of ATS.

That was good to ask… I was so wrong…

Wow, me too. So maybe I’m confused about what “dynamics” means. I was
thinking it was anything that could have a representation in the generated
code (e.g. C code).

May be a way to help to remind what‑is‑what, is to refer to the
“constraint language” instead of to the “static language” (and what’s not
the constraint language is the dynamic language). The Bluishcoder blog use
the expressions “constraint language” before saying it is what’s also named
the “static language”.

9

Sorry, I missed a lot of your first e-mail the first time. Now that I got
it all, I think I’m a lot more clear. It makes sense, but it is one of
those things that is so different from what I think of when dealing with
programming on a day to day basis, I hope I don’t forget the distinction
between static values and proof values several months hence.On Mon, Feb 9, 2015 at 9:09 PM, gmhwxi gmh...@gmail.com wrote:

Yes.

On Monday, February 9, 2015 at 9:03:21 PM UTC-5, Brandon Barker wrote:

So i and j are static variables in the above? Assuming so since we are
using ‘==’.

On Mon, Feb 9, 2015 at 8:29 PM, gmhwxi gmh...@gmail.com wrote:

In the following file:

GitHub - githwxi/ATS-Postiats: ATS2: Unleashing the Potentials of Types and Templates
prelude/basics_dyn.sats

you will find the following functions:

prfun prop_verify{b:bool | b} (): void
prfun prop_verify_and_add{b:bool | b} (): [b] void

Say at one point, you want to know if (i==j) holds. You
do this by adding the following line:

prval () = prop_verify{i==j}()

Yes. But not in a form that is readable.

I don’t mind, this is still better than nothing :stuck_out_tongue:

It is really really not readable :slight_smile:

What you see is millions of bytes of internal syntax trees. Try
the following command line on your own:

patsopt -tc --constraint-export -d ${PATSHOME}/doc/EXAMPLE/ATSLF/
sqrt2_irrat.dats

On Monday, February 9, 2015 at 8:15:19 PM UTC-5, Yannick Duchêne wrote:

Le mardi 10 février 2015 01:58:44 UTC+1, gmhwxi a écrit :

A proof-value is in the dynamics of ATS.

That was good to ask… I was so wrong…

Thanks for the notice!

If yes, then is there a way to “dump” these hypotheses?

Yes. But not in a form that is readable.

I don’t mind, this is still better than nothing :stuck_out_tongue: . Is this using a
special keyword like $showtype?

–
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...@googlegroups.com.
To post to this group, send email to ats-l...@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/7b89dc49-9b1e-4378-9d58-be334d10d7ca%
40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/7b89dc49-9b1e-4378-9d58-be334d10d7ca%40googlegroups.com?utm_medium=email&utm_source=footer
.

–
Brandon Barker
brand...@gmail.com

–
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/6ea99d1c-42f3-4b5e-8724-4eb3d0f1bc15%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/6ea99d1c-42f3-4b5e-8724-4eb3d0f1bc15%40googlegroups.com?utm_medium=email&utm_source=footer
.

Brandon Barker
brandon...@gmail.com

10

In the following file:

you will find the following functions:

prfun prop_verify{b:bool | b} (): void
prfun prop_verify_and_add{b:bool | b} (): [b] void

Say at one point, you want to know if (i==j) holds. You
do this by adding the following line:

prval () = prop_verify{i==j}()

Yes. But not in a form that is readable.

I don’t mind, this is still better than nothing :stuck_out_tongue:

It is really really not readable :slight_smile:

What you see is millions of bytes of internal syntax trees. Try
the following command line on your own:

patsopt -tc --constraint-export -d
${PATSHOME}/doc/EXAMPLE/ATSLF/sqrt2_irrat.datsOn Monday, February 9, 2015 at 8:15:19 PM UTC-5, Yannick Duchêne wrote:

Le mardi 10 février 2015 01:58:44 UTC+1, gmhwxi a écrit :

A proof-value is in the dynamics of ATS.

That was good to ask… I was so wrong…

Thanks for the notice!

If yes, then is there a way to “dump” these hypotheses?

Yes. But not in a form that is readable.

I don’t mind, this is still better than nothing :stuck_out_tongue: . Is this using a
special keyword like $showtype?

11

Basic questions, but I really have to ask… I’m not sure to really
understand what prfun/prfn and prval do.

What’s exactly the result of a proof function? Most seems to return void,
but some returns a result. Is this a static value? Are proof functions
simply static functions?

Yes, they are both static only.

What happens when the result of a proof function is bound to a prval or
especially matched with ()? Does it makes ATS (the checker, not the
language) store some confirmed hypotheses internally? If yes, then is there
a way to “dump” these hypotheses?

How does a proof “returned” by a proof function differs from a proof
returned along with a result from a dynamic function?

IIRC, they are the same, but a dynamic function can return both dynamics
and statics. I think prfuns may be used to implement lemmas for the proof
returned from a dynamic function.

–
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/831de703-bfb8-4a02-8da3-f73de11fe62c%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/831de703-bfb8-4a02-8da3-f73de11fe62c%40googlegroups.com?utm_medium=email&utm_source=footer
.

Brandon Barker
brandon...@gmail.com