Universals/predicates in absview declaration

Google Group
1

Hi all,

Currently, my ‘filedes’ view is declared:

absview filedes (fd: int)

Really, though, a valid file descriptor has to be a nat. If I try

absview filedes (fd: nat)

compliation fails with

the identifier [nat] is expected to refer to a sort (instead of a subset sort)

and all attempts to spell out a universal like

absview filedes {n: nat} (fd: int n)

fail to parse. Is it possible to constrain an absview in this way?

~Shea

2

Ah I see, thanks!

~SheaOn Sat, Aug 30, 2014 at 06:20:48PM -0700, gmhwxi wrote:

Really, though, a valid file descriptor has to be a nat.

This piece of knowledge can be encoded in a lemma:

prfun lemma_filedes_param {n:int} (pf: !filedes(n)): [n >= 0] void

When you need the knowledge in your reasoning, you can do

prval () = lemma_filedes_param (pf) // assume [pf] is available at this
point

On Saturday, August 30, 2014 8:52:58 PM UTC-4, Shea Levy wrote:

Hi all,

Currently, my ‘filedes’ view is declared:

absview filedes (fd: int)

Really, though, a valid file descriptor has to be a nat. If I try

absview filedes (fd: nat)

compliation fails with

the identifier [nat] is expected to refer to a sort (instead of a subset
sort)

and all attempts to spell out a universal like

absview filedes {n: nat} (fd: int n)

fail to parse. Is it possible to constrain an absview in this way?

~Shea

–
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/a5bf98ac-a353-4472-a300-30bf1d5847da%40googlegroups.com.

3

Really, though, a valid file descriptor has to be a nat.

This piece of knowledge can be encoded in a lemma:

prfun lemma_filedes_param {n:int} (pf: !filedes(n)): [n >= 0] void

When you need the knowledge in your reasoning, you can do

prval () = lemma_filedes_param (pf) // assume [pf] is available at this
pointOn Saturday, August 30, 2014 8:52:58 PM UTC-4, Shea Levy wrote:

Hi all,

Currently, my ‘filedes’ view is declared:

absview filedes (fd: int)

Really, though, a valid file descriptor has to be a nat. If I try

absview filedes (fd: nat)

compliation fails with

the identifier [nat] is expected to refer to a sort (instead of a subset
sort)

and all attempts to spell out a universal like

absview filedes {n: nat} (fd: int n)

fail to parse. Is it possible to constrain an absview in this way?

~Shea