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?
> --
> 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/02d1f7bd-2dc4-4603-a2e2-4cd09a9c1349%40googlegroups.com.