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?
%{^ #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 endOn Saturday, August 30, 2014 10:44:03 PM UTC-4, Shea Levy wrote:
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?
~Shea
On Sat, Aug 30, 2014 at 10:09:11PM -0400, Hongwei Xi wrote:
The code should be in a DATS file.
On Sat, Aug 30, 2014 at 10:06 PM, Shea Levy <sh...@shealevy.com <javascript:>> wrote:
Hm, this fails with
error(parsing): the syntactic entity [colonwith] is needed.
~Shea
On Sat, Aug 30, 2014 at 06:16:13PM -0700, gmhwxi wrote:
If I understand your situation correctly, I would do something like
this:
prval
stderr_fileno_pf = __assert () where
{
extern praxi __assert (): filedes(2)
}
On Saturday, August 30, 2014 7:31:53 PM UTC-4, Shea Levy wrote:
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
–
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
–
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
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.On Saturday, August 30, 2014 11:01:29 PM UTC-4, Shea Levy wrote:
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?
On Sat, Aug 30, 2014 at 07:56:25PM -0700, gmhwxi wrote:
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
On Saturday, August 30, 2014 10:44:03 PM UTC-4, Shea Levy wrote:
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?
On Sat, Aug 30, 2014 at 10:09:11PM -0400, Hongwei Xi wrote:
The code should be in a DATS file.
On Sat, Aug 30, 2014 at 10:06 PM, Shea Levy <sh...@shealevy.com <javascript:>> wrote:
Hm, this fails with
error(parsing): the syntactic entity [colonwith] is needed.
~Shea
On Sat, Aug 30, 2014 at 06:16:13PM -0700, gmhwxi wrote:
If I understand your situation correctly, I would do something
like
this:
prval
stderr_fileno_pf = __assert () where
{
extern praxi __assert (): filedes(2)
}
On Saturday, August 30, 2014 7:31:53 PM UTC-4, Shea Levy wrote:
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
–
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
–
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
The code should be in a DATS file.On Sat, Aug 30, 2014 at 10:06 PM, Shea Levy sh...@shealevy.com wrote:
Hm, this fails with
error(parsing): the syntactic entity [colonwith] is needed.
~Shea
On Sat, Aug 30, 2014 at 06:16:13PM -0700, gmhwxi wrote:
If I understand your situation correctly, I would do something like this:
prval
stderr_fileno_pf = __assert () where
{
extern praxi __assert (): filedes(2)
}
On Saturday, August 30, 2014 7:31:53 PM UTC-4, Shea Levy wrote:
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?
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?
~SheaOn Sat, Aug 30, 2014 at 10:09:11PM -0400, Hongwei Xi wrote:
error(parsing): the syntactic entity [colonwith] is needed.
~Shea
On Sat, Aug 30, 2014 at 06:16:13PM -0700, gmhwxi wrote:
If I understand your situation correctly, I would do something like this:
prval
stderr_fileno_pf = __assert () where
{
extern praxi __assert (): filedes(2)
}
On Saturday, August 30, 2014 7:31:53 PM UTC-4, Shea Levy wrote:
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?
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?On Sat, Aug 30, 2014 at 07:56:25PM -0700, gmhwxi wrote:
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
On Saturday, August 30, 2014 10:44:03 PM UTC-4, Shea Levy wrote:
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?
~Shea
On Sat, Aug 30, 2014 at 10:09:11PM -0400, Hongwei Xi wrote:
The code should be in a DATS file.
On Sat, Aug 30, 2014 at 10:06 PM, Shea Levy <sh...@shealevy.com <javascript:>> wrote:
Hm, this fails with
error(parsing): the syntactic entity [colonwith] is needed.
~Shea
On Sat, Aug 30, 2014 at 06:16:13PM -0700, gmhwxi wrote:
If I understand your situation correctly, I would do something like
this:
prval
stderr_fileno_pf = __assert () where
{
extern praxi __assert (): filedes(2)
}
On Saturday, August 30, 2014 7:31:53 PM UTC-4, Shea Levy wrote:
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
–
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
–
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
OK, thanks! I’ve now got something working.On Sat, Aug 30, 2014 at 08:09:39PM -0700, gmhwxi wrote:
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.
On Saturday, August 30, 2014 11:01:29 PM UTC-4, Shea Levy wrote:
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?
On Sat, Aug 30, 2014 at 07:56:25PM -0700, gmhwxi wrote:
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
On Saturday, August 30, 2014 10:44:03 PM UTC-4, Shea Levy wrote:
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?
On Sat, Aug 30, 2014 at 10:09:11PM -0400, Hongwei Xi wrote:
The code should be in a DATS file.
On Sat, Aug 30, 2014 at 10:06 PM, Shea Levy <sh...@shealevy.com <javascript:>> wrote:
Hm, this fails with
error(parsing): the syntactic entity [colonwith] is needed.
~Shea
On Sat, Aug 30, 2014 at 06:16:13PM -0700, gmhwxi wrote:
If I understand your situation correctly, I would do something
like
this:
prval
stderr_fileno_pf = __assert () where
{
extern praxi __assert (): filedes(2)
}
On Saturday, August 30, 2014 7:31:53 PM UTC-4, Shea Levy wrote:
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
–
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
–
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
error(parsing): the syntactic entity [colonwith] is needed.
~SheaOn Sat, Aug 30, 2014 at 06:16:13PM -0700, gmhwxi wrote:
If I understand your situation correctly, I would do something like this:
prval
stderr_fileno_pf = __assert () where
{
extern praxi __assert (): filedes(2)
}
On Saturday, August 30, 2014 7:31:53 PM UTC-4, Shea Levy wrote:
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?
If I understand your situation correctly, I would do something like this:
prval
stderr_fileno_pf = __assert () where
{
extern praxi __assert (): filedes(2)
}On Saturday, August 30, 2014 7:31:53 PM UTC-4, Shea Levy wrote:
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?