fn close {fd: nat} (filedes fd | int fd):
[res: int] (option_v(errno_obligation, res == ~1) | int res)
and in my dats file:
implement close (prf | fd) = let
extern fun unsafe_close (int): int = “ext#close”
val res = unsafe_close(fd)
prval filedes_impl fd = prf
prval prf = (if res = ~1 then let
prval e_obl = require_errno_check ()
in Some_v e_obl end
else None_v ()): [res: int] (option_v(errno_obligation, res == ~1))
in (prf | res) end
This fails to compile due to a mismatch in static terms on the last
line:
The actual term is: S2Etyrec(flt0; npf=1; 0=S2Eapp(S2Ecst(option_view_bool_view); S2Ecst(errno_obligation), S2Eapp(S2Ecst(==); S2Evar(res$868(3851)), S2Eapp(S2Ecst(~); S2Eintinf(1)))), 1=S2Eapp(S2Ecst(g0int_t0ype); S2Ecst(int_kind)))
The needed term is: S2Eexi(res$860(3842); ; S2Etyrec(flt0; npf=1; 0=S2Eapp(S2Ecst(option_v); S2Ecst(errno_obligation), S2Eapp(S2Ecst(==); S2Evar(res$860(3842)), S2Eapp(S2Ecst(~); S2Eintinf(1)))), 1=S2Eapp(S2Ecst(int); S2Evar(res$860(3842)))))
My guess is that this is due to the fact that the compiler doesn’t know
that the ‘res’ existential in the type of prf is the same as the res val
being returned. I know that they match because of the if statement, but
how can I tell the compiler this?
Thanks! I got my code to type-check by making unsafe_close return an Int
instead of an int (which in retrospect makes sense), but I’ve added a
few questions in-line as I’m worried I may have missed a more
fundamental point:
There reason for typechecking failure is that the compiler
could not figure out what [res] is. But there are other problems with
your
code that are more serious.
Can you explain a bit what the problems are?
In your previous version of the code, you constructed a proof first and
then paired it with the return value. It would not work since the
typechecker
cannot tell if the proof and the value match.
I sketched a way to make your code typecheck:
absview filedes (int)
(* ****** ****** *)
absview errno_obligation
(* ****** ****** *)
extern
praxi require_errno_check (): errno_obligation
Is it generally preferable to use a praxi here instead of implementing
the absview in a separate dynamic file and actually implementing the
function?
There is really no difference between praxi and prfun as of now.
(* ****** ****** *)
extern
fun close {fd: nat} (filedes fd | int fd):
[res: int] (option_v(errno_obligation, res == ~1) | int res)
(* ****** ****** *)
implement
close{fd}(prf | fd) = let
//
val res =
$extfcall (Int, “close”, fd)
Ah, I forgot about extfcall. Is it preferable to a local ext# fun
declaration?
It is concise but probably more error-prone.
prval () = __free (prf) where
{
extern praxi __free (filedes(fd)): void
Similar question to above, is a praxi here preferable to implementing
the absview and consuming the proof directly
It is just a quicker way of doing things. At this stage, the focus should
probably
be on getting the code to work. You can always try to fix proofs later.
Just like
doing proofs in mathematics.
Thanks! I got my code to type-check by making unsafe_close return an Int
instead of an int (which in retrospect makes sense), but I’ve added a
few questions in-line as I’m worried I may have missed a more
fundamental point:
There reason for typechecking failure is that the compiler
could not figure out what [res] is. But there are other problems with your
code that are more serious.
Can you explain a bit what the problems are?
I sketched a way to make your code typecheck:
absview filedes (int)
(* ****** ****** *)
absview errno_obligation
(* ****** ****** *)
extern
praxi require_errno_check (): errno_obligation
Is it generally preferable to use a praxi here instead of implementing
the absview in a separate dynamic file and actually implementing the
function?
(* ****** ****** *)
extern
fun close {fd: nat} (filedes fd | int fd):
[res: int] (option_v(errno_obligation, res == ~1) | int res)
(* ****** ****** *)
implement
close{fd}(prf | fd) = let
//
val res =
$extfcall (Int, “close”, fd)
Ah, I forgot about extfcall. Is it preferable to a local ext# fun
declaration?
prval () = __free (prf) where
{
extern praxi __free (filedes(fd)): void
Similar question to above, is a praxi here preferable to implementing
the absview and consuming the proof directly?
Before answering your questions, could I take a look at your new code
that has passed typechecking?On Sunday, August 31, 2014 1:54:23 PM UTC-4, Shea Levy wrote:
Thanks! I got my code to type-check by making unsafe_close return an Int
instead of an int (which in retrospect makes sense), but I’ve added a
few questions in-line as I’m worried I may have missed a more
fundamental point:
On Sun, Aug 31, 2014 at 10:29:46AM -0700, gmhwxi wrote:
There reason for typechecking failure is that the compiler
could not figure out what [res] is. But there are other problems with
your
code that are more serious.
Can you explain a bit what the problems are?
I sketched a way to make your code typecheck:
absview filedes (int)
(* ****** ****** *)
absview errno_obligation
(* ****** ****** *)
extern
praxi require_errno_check (): errno_obligation
Is it generally preferable to use a praxi here instead of implementing
the absview in a separate dynamic file and actually implementing the
function?
(* ****** ****** *)
extern
fun close {fd: nat} (filedes fd | int fd):
[res: int] (option_v(errno_obligation, res == ~1) | int res)
(* ****** ****** *)
implement
close{fd}(prf | fd) = let
//
val res =
$extfcall (Int, “close”, fd)
Ah, I forgot about extfcall. Is it preferable to a local ext# fun
declaration?
prval () = __free (prf) where
{
extern praxi __free (filedes(fd)): void
Similar question to above, is a praxi here preferable to implementing
the absview and consuming the proof directly?
}
//
in
//
if
res = ~1
then let
prval e_obl = require_errno_check ()
in
(Some_v e_obl | res)
end // end of [then]
else (None_v () | res)
//
end // end of [close]
ATS can be a very demanding language if you try to do everything by the
“rule”.
At this stage, I suggest that you use assertions (like __assert and
__free)
amply
in your code. Otherwise, you could quickly get bogged down due to proof
details, losing
focus or interest as a consequence.
On Sunday, August 31, 2014 12:30:21 PM UTC-4, Shea Levy wrote:
Hi all,
I have in my sats file:
fn close {fd: nat} (filedes fd | int fd):
[res: int] (option_v(errno_obligation, res == ~1) | int res)
and in my dats file:
implement close (prf | fd) = let
extern fun unsafe_close (int): int = “ext#close”
val res = unsafe_close(fd)
prval filedes_impl fd = prf
prval prf = (if res = ~1 then let
prval e_obl = require_errno_check ()
in Some_v e_obl end
else None_v ()): [res: int] (option_v(errno_obligation, res ==
~1))
in (prf | res) end
This fails to compile due to a mismatch in static terms on the last
line:
The actual term is: S2Etyrec(flt0; npf=1;
0=S2Eapp(S2Ecst(option_view_bool_view); S2Ecst(errno_obligation),
S2Eapp(S2Ecst(==); S2Evar(res$868(3851)), S2Eapp(S2Ecst(~);
S2Eintinf(1)))), 1=S2Eapp(S2Ecst(g0int_t0ype); S2Ecst(int_kind)))
The needed term is: S2Eexi(res$860(3842); ; S2Etyrec(flt0; npf=1;
0=S2Eapp(S2Ecst(option_v); S2Ecst(errno_obligation),
S2Eapp(S2Ecst(==);
S2Evar(res$860(3842)), S2Eapp(S2Ecst(~); S2Eintinf(1)))),
1=S2Eapp(S2Ecst(int); S2Evar(res$860(3842)))))
My guess is that this is due to the fact that the compiler doesn’t
know
that the ‘res’ existential in the type of prf is the same as the res
val
being returned. I know that they match because of the if statement,
but
how can I tell the compiler this?
There is really no difference between praxi and prfun as of now.
Ah, really? Do prfuns not have to be implemented? I suppose there’s no
good way to check given separate compilation…
Indeed. It is a bit involved to implement. However, it is conceptually
straightforward.
I did support a flag in ATS1 to ensure that proof functions are all
implemented. I left
it out in ATS2 as I don’t feel it is worth the effort. ATS is first and
foremost a programming
language; support for theorem-proving in ATS has been a secondary issue
from the very
beginning.On Sun, Aug 31, 2014 at 5:23 PM, Shea Levy sh...@shealevy.com wrote:
On Sun, Aug 31, 2014 at 11:36:06AM -0700, gmhwxi wrote:
On Sunday, August 31, 2014 1:54:23 PM UTC-4, Shea Levy wrote:
Thanks! I got my code to type-check by making unsafe_close return an
Int
instead of an int (which in retrospect makes sense), but I’ve added a
few questions in-line as I’m worried I may have missed a more
fundamental point:
On Sun, Aug 31, 2014 at 10:29:46AM -0700, gmhwxi wrote:
There reason for typechecking failure is that the compiler
could not figure out what [res] is. But there are other problems with
your
code that are more serious.
Can you explain a bit what the problems are?
In your previous version of the code, you constructed a proof first and
then paired it with the return value. It would not work since the
typechecker
cannot tell if the proof and the value match.
Ah, yes, I had tried both versions but because of the int instead of Int
neither worked.
I sketched a way to make your code typecheck:
absview filedes (int)
(* ****** ****** *)
absview errno_obligation
(* ****** ****** *)
extern
praxi require_errno_check (): errno_obligation
Is it generally preferable to use a praxi here instead of implementing
the absview in a separate dynamic file and actually implementing the
function?
There is really no difference between praxi and prfun as of now.
Ah, really? Do prfuns not have to be implemented? I suppose there’s no
good way to check given separate compilation…
(* ****** ****** *)
extern
fun close {fd: nat} (filedes fd | int fd):
[res: int] (option_v(errno_obligation, res == ~1) | int res)
(* ****** ****** *)
implement
close{fd}(prf | fd) = let
//
val res =
$extfcall (Int, “close”, fd)
Ah, I forgot about extfcall. Is it preferable to a local ext# fun
declaration?
It is concise but probably more error-prone.
I see, thanks.
prval () = __free (prf) where
{
extern praxi __free (filedes(fd)): void
Similar question to above, is a praxi here preferable to implementing
the absview and consuming the proof directly
It is just a quicker way of doing things. At this stage, the focus should
probably
be on getting the code to work. You can always try to fix proofs later.
Just like
doing proofs in mathematics.
}
//
in
//
if
res = ~1
then let
prval e_obl = require_errno_check ()
in
(Some_v e_obl | res)
end // end of [then]
else (None_v () | res)
//
end // end of [close]
ATS can be a very demanding language if you try to do everything by
the
“rule”.
At this stage, I suggest that you use assertions (like __assert and
__free)
amply
in your code. Otherwise, you could quickly get bogged down due to
proof
details, losing
focus or interest as a consequence.
On Sunday, August 31, 2014 12:30:21 PM UTC-4, Shea Levy wrote:
Hi all,
I have in my sats file:
fn close {fd: nat} (filedes fd | int fd):
[res: int] (option_v(errno_obligation, res == ~1) | int res)
and in my dats file:
implement close (prf | fd) = let
extern fun unsafe_close (int): int = “ext#close”
val res = unsafe_close(fd)
prval filedes_impl fd = prf
prval prf = (if res = ~1 then let
prval e_obl = require_errno_check ()
in Some_v e_obl end
else None_v ()): [res: int] (option_v(errno_obligation, res ==
~1))
in (prf | res) end
This fails to compile due to a mismatch in static terms on the last
line:
The actual term is: S2Etyrec(flt0; npf=1;
0=S2Eapp(S2Ecst(option_view_bool_view); S2Ecst(errno_obligation),
S2Eapp(S2Ecst(==); S2Evar(res$868(3851)), S2Eapp(S2Ecst(~);
S2Eintinf(1)))), 1=S2Eapp(S2Ecst(g0int_t0ype); S2Ecst(int_kind)))
The needed term is: S2Eexi(res$860(3842); ; S2Etyrec(flt0; npf=1;
0=S2Eapp(S2Ecst(option_v); S2Ecst(errno_obligation),
S2Eapp(S2Ecst(==);
S2Evar(res$860(3842)), S2Eapp(S2Ecst(~); S2Eintinf(1)))),
1=S2Eapp(S2Ecst(int); S2Evar(res$860(3842)))))
My guess is that this is due to the fact that the compiler doesn’t
know
that the ‘res’ existential in the type of prf is the same as the
res
val
being returned. I know that they match because of the if statement,
but
how can I tell the compiler this?
–
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
Thanks! I got my code to type-check by making unsafe_close return an Int
instead of an int (which in retrospect makes sense), but I’ve added a
few questions in-line as I’m worried I may have missed a more
fundamental point:
There reason for typechecking failure is that the compiler
could not figure out what [res] is. But there are other problems with
your
code that are more serious.
Can you explain a bit what the problems are?
In your previous version of the code, you constructed a proof first and
then paired it with the return value. It would not work since the
typechecker
cannot tell if the proof and the value match.
Ah, yes, I had tried both versions but because of the int instead of Int
neither worked.
I sketched a way to make your code typecheck:
absview filedes (int)
(* ****** ****** *)
absview errno_obligation
(* ****** ****** *)
extern
praxi require_errno_check (): errno_obligation
Is it generally preferable to use a praxi here instead of implementing
the absview in a separate dynamic file and actually implementing the
function?
There is really no difference between praxi and prfun as of now.
Ah, really? Do prfuns not have to be implemented? I suppose there’s no
good way to check given separate compilation…
(* ****** ****** *)
extern
fun close {fd: nat} (filedes fd | int fd):
[res: int] (option_v(errno_obligation, res == ~1) | int res)
(* ****** ****** *)
implement
close{fd}(prf | fd) = let
//
val res =
$extfcall (Int, “close”, fd)
Ah, I forgot about extfcall. Is it preferable to a local ext# fun
declaration?
Sure, the repo is at 1, the specific file in question at 2.
~SheaOn Sun, Aug 31, 2014 at 11:17:56AM -0700, gmhwxi wrote:
Before answering your questions, could I take a look at your new code
that has passed typechecking?
On Sunday, August 31, 2014 1:54:23 PM UTC-4, Shea Levy wrote:
Thanks! I got my code to type-check by making unsafe_close return an Int
instead of an int (which in retrospect makes sense), but I’ve added a
few questions in-line as I’m worried I may have missed a more
fundamental point:
On Sun, Aug 31, 2014 at 10:29:46AM -0700, gmhwxi wrote:
There reason for typechecking failure is that the compiler
could not figure out what [res] is. But there are other problems with
your
code that are more serious.
Can you explain a bit what the problems are?
I sketched a way to make your code typecheck:
absview filedes (int)
(* ****** ****** *)
absview errno_obligation
(* ****** ****** *)
extern
praxi require_errno_check (): errno_obligation
Is it generally preferable to use a praxi here instead of implementing
the absview in a separate dynamic file and actually implementing the
function?
(* ****** ****** *)
extern
fun close {fd: nat} (filedes fd | int fd):
[res: int] (option_v(errno_obligation, res == ~1) | int res)
(* ****** ****** *)
implement
close{fd}(prf | fd) = let
//
val res =
$extfcall (Int, “close”, fd)
Ah, I forgot about extfcall. Is it preferable to a local ext# fun
declaration?
prval () = __free (prf) where
{
extern praxi __free (filedes(fd)): void
Similar question to above, is a praxi here preferable to implementing
the absview and consuming the proof directly?
}
//
in
//
if
res = ~1
then let
prval e_obl = require_errno_check ()
in
(Some_v e_obl | res)
end // end of [then]
else (None_v () | res)
//
end // end of [close]
ATS can be a very demanding language if you try to do everything by the
“rule”.
At this stage, I suggest that you use assertions (like __assert and
__free)
amply
in your code. Otherwise, you could quickly get bogged down due to proof
details, losing
focus or interest as a consequence.
On Sunday, August 31, 2014 12:30:21 PM UTC-4, Shea Levy wrote:
Hi all,
I have in my sats file:
fn close {fd: nat} (filedes fd | int fd):
[res: int] (option_v(errno_obligation, res == ~1) | int res)
and in my dats file:
implement close (prf | fd) = let
extern fun unsafe_close (int): int = “ext#close”
val res = unsafe_close(fd)
prval filedes_impl fd = prf
prval prf = (if res = ~1 then let
prval e_obl = require_errno_check ()
in Some_v e_obl end
else None_v ()): [res: int] (option_v(errno_obligation, res ==
~1))
in (prf | res) end
This fails to compile due to a mismatch in static terms on the last
line:
The actual term is: S2Etyrec(flt0; npf=1;
0=S2Eapp(S2Ecst(option_view_bool_view); S2Ecst(errno_obligation),
S2Eapp(S2Ecst(==); S2Evar(res$868(3851)), S2Eapp(S2Ecst(~);
S2Eintinf(1)))), 1=S2Eapp(S2Ecst(g0int_t0ype); S2Ecst(int_kind)))
The needed term is: S2Eexi(res$860(3842); ; S2Etyrec(flt0; npf=1;
0=S2Eapp(S2Ecst(option_v); S2Ecst(errno_obligation),
S2Eapp(S2Ecst(==);
S2Evar(res$860(3842)), S2Eapp(S2Ecst(~); S2Eintinf(1)))),
1=S2Eapp(S2Ecst(int); S2Evar(res$860(3842)))))
My guess is that this is due to the fact that the compiler doesn’t
know
that the ‘res’ existential in the type of prf is the same as the res
val
being returned. I know that they match because of the if statement,
but
how can I tell the compiler this?
There reason for typechecking failure is that the compiler
could not figure out what [res] is. But there are other problems with your
code that are more serious. I sketched a way to make your code typecheck:
absview filedes (int)
(* ****** ****** *)
absview errno_obligation
(* ****** ****** *)
extern
praxi require_errno_check (): errno_obligation
(* ****** ****** *)
extern
fun close {fd: nat} (filedes fd | int fd):
[res: int] (option_v(errno_obligation, res == ~1) | int res)
(* ****** ****** *)
implement
close{fd}(prf | fd) = let
//
val res =
$extfcall (Int, “close”, fd)
prval () = __free (prf) where
{
extern praxi __free (filedes(fd)): void
}
//
in
//
if
res = ~1
then let
prval e_obl = require_errno_check ()
in
(Some_v e_obl | res)
end // end of [then]
else (None_v () | res)
//
end // end of [close]
ATS can be a very demanding language if you try to do everything by the
“rule”.
At this stage, I suggest that you use assertions (like __assert and __free)
amply
in your code. Otherwise, you could quickly get bogged down due to proof
details, losing
focus or interest as a consequence.On Sunday, August 31, 2014 12:30:21 PM UTC-4, Shea Levy wrote:
Hi all,
I have in my sats file:
fn close {fd: nat} (filedes fd | int fd):
[res: int] (option_v(errno_obligation, res == ~1) | int res)
and in my dats file:
implement close (prf | fd) = let
extern fun unsafe_close (int): int = “ext#close”
val res = unsafe_close(fd)
prval filedes_impl fd = prf
prval prf = (if res = ~1 then let
prval e_obl = require_errno_check ()
in Some_v e_obl end
else None_v ()): [res: int] (option_v(errno_obligation, res == ~1))
in (prf | res) end
This fails to compile due to a mismatch in static terms on the last
line:
The actual term is: S2Etyrec(flt0; npf=1;
0=S2Eapp(S2Ecst(option_view_bool_view); S2Ecst(errno_obligation),
S2Eapp(S2Ecst(==); S2Evar(res$868(3851)), S2Eapp(S2Ecst(~);
S2Eintinf(1)))), 1=S2Eapp(S2Ecst(g0int_t0ype); S2Ecst(int_kind)))
The needed term is: S2Eexi(res$860(3842); ; S2Etyrec(flt0; npf=1;
0=S2Eapp(S2Ecst(option_v); S2Ecst(errno_obligation), S2Eapp(S2Ecst(==);
S2Evar(res$860(3842)), S2Eapp(S2Ecst(~); S2Eintinf(1)))),
1=S2Eapp(S2Ecst(int); S2Evar(res$860(3842)))))
My guess is that this is due to the fact that the compiler doesn’t know
that the ‘res’ existential in the type of prf is the same as the res val
being returned. I know that they match because of the if statement, but
how can I tell the compiler this?