Declaring an external view prval

[Shea Levy]

Hi all,

I have an abstract view 'filedes' parameterized by an int file
descriptor. I want to declare that, at the beginning of the program,
stderr is an open file, so I have this line in fd.sats:

> prval stderr_fileno_pf : filedes(2)

Typechecking fails with

> the static expression is of the sort [S2RTbas(S2RTBASimp(7; view))] but it is expectecd to be of the sort [S2RTbas(S2RTBASimp(5; prop))]

which is clear enough, but if prval is not the right way to go how do I
declare a view proof value?

~Shea

[gmhwxi]

If I understand your situation correctly, I would do something like this:

prval
stderr_fileno_pf = __assert () where
{
  extern praxi __assert (): filedes(2)

[Shea Levy]

Hm, this fails with

> error(parsing): the syntactic entity [colonwith] is needed.

~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/e05c4c07-2cc3-4586-8d12-22f818f5043f%40googlegroups.com.

[Hongwei Xi]

The code should be in a DATS file.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/20140831020626.GD7772%40nixos.hsd1.nh.comcast.net.

[Shea Levy]

Ah, I see. I'm now stuck at an error I don't understand. My code is at
[1], [2], and [3], and the errors I get are:

> /home/shlevy/src/socket-activate/dynamic/socket-activate.dats: 129(line=9, offs=17) -- 145(line=9, offs=33): error(3): the linear dynamic variable [stderr_fileno_pf$63(-1)] is expected to be local but it is not.
> /home/shlevy/src/socket-activate/dynamic/socket-activate.dats: 129(line=9, offs=17) -- 145(line=9, offs=33): error(3): [/home/hwxi/research/Postiats/git/src/pats_trans3_util.dats]: d3exp_trdn: the dynamic expression cannot be assigned the type [S2Eapp(S2Ecst(filedes); S2EVar(1))].
> /home/shlevy/src/socket-activate/dynamic/socket-activate.dats: 129(line=9, offs=17) -- 145(line=9, offs=33): error(3): mismatch of static terms (tyleq):
> The actual term is: S2Eapp(S2Ecst(filedes_impl); S2Eintinf(2))
> The needed term is: S2Eapp(S2Ecst(filedes); S2EVar(1))

I'm afraid I'm lost for both of these. Why is the proof expected to be
local? And why is filedes_impl being exposed?

[1]: https://github.com/shlevy/socket-activate/blob/WIP/dynamic/socket-activate.dats
[2]: https://github.com/shlevy/socket-activate/blob/WIP/static/fd.sats
[3]: https://github.com/shlevy/socket-activate/blob/WIP/dynamic/fd.dats

~Shea

> > https://groups.google.com/d/msgid/ats-lang-users/20140831020626.GD7772%40nixos.hsd1.nh.comcast.net
> > .

> >
>
> --
> 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/CAPPSPLr4npLL9EzmQE3eEL4%3DG1EaPn%3DKfUDkdx86ukXVp%3DC8RA%40mail.gmail.com.

[gmhwxi]

First,

%{# should be changed to %{^

%{# should only be used in a SATS file.

You code should look like this:

%{^ #include "include/common.h" %} staload "static/fd.sats" // // staload "dynamic/fd.dats" // implement main () = let prval pf = make () where {   extern make (): filedes(2) } val _ = close(stderr_fileno_pf | 2) in 0 end

[Shea Levy]

Ah, I see, so is there no way to modularly declare a linear proof like
this? I have to have a praxi in every function that uses it?

> > > > an email to ats-lang-user...@googlegroups.com <javascript:>.

> > > > > To post to this group, send email to ats-lan...@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/e05c4c07-2cc3-4586-8d12-22f818f5043f%40googlegroups.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 <javascript:>.

> > > > To post to this group, send email to ats-lan...@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/20140831020626.GD7772%40nixos.hsd1.nh.comcast.net
> > > > .
> > > >
> > >
> > > --
> > > 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 <javascript:>.

> > > To post to this group, send email to ats-lan...@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/CAPPSPLr4npLL9EzmQE3eEL4%3DG1EaPn%3DKfUDkdx86ukXVp%3DC8RA%40mail.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/fb4aefb5-a045-4bf7-8163-9a950ed8b6bd%40googlegroups.com.

[gmhwxi]

A linear proof cannot be shared; it can only be borrowed.
This is a complicated issue. For now, the shortcut I showed is
probably the easiest way to take.

[Shea Levy]

OK, thanks! I've now got something working.

> > https://groups.google.com/d/msgid/ats-lang-users/fb4aefb5-a045-4bf7-8163-9a950ed8b6bd%40googlegroups.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/53567894-42a1-4851-a29f-f6643ebff311%40googlegroups.com.