Has anyone migrated a C project to ATS in an open source repo that I can
look at? I’d love to follow along with the piecewise evolution.
martin
loc in assertloc means location.
If assertloc fails, it prints out the location of the line so as to help
debugging.On Fri, Nov 28, 2014 at 9:16 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:
Please, what is
assertloc?Le mercredi 19 novembre 2014 03:17:06 UTC+1, gmhwxi a écrit :
Try to do this in stages (even if you wrote the original C code).
At the beginning, please try to ignore error-handling. Instead, you
can use assertloc and $UN.cast to get a value of some needed type.Overly using if-then-else to handle errors is often a sure sign of failure
in waiting.On Tuesday, November 18, 2014 5:24:14 PM UTC-5, Martin DeMello wrote:
Has anyone migrated a C project to ATS in an open source repo that I can
look at? I’d love to follow along with the piecewise evolution.martin
–
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/f4a2444e-1ddd-4fc5-99a7-3253c5085c5a%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/f4a2444e-1ddd-4fc5-99a7-3253c5085c5a%40googlegroups.com?utm_medium=email&utm_source=footer
.
It is a dynamic check that returns a proof that its single argument
evaluates to true (otherwise the program exits).
I think there are a number of discussions that touch on it indirectly in
the google group.On Fri, Nov 28, 2014 at 9:16 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:
Please, what is
assertloc?Le mercredi 19 novembre 2014 03:17:06 UTC+1, gmhwxi a écrit :
Try to do this in stages (even if you wrote the original C code).
At the beginning, please try to ignore error-handling. Instead, you
can use assertloc and $UN.cast to get a value of some needed type.Overly using if-then-else to handle errors is often a sure sign of failure
in waiting.On Tuesday, November 18, 2014 5:24:14 PM UTC-5, Martin DeMello wrote:
Has anyone migrated a C project to ATS in an open source repo that I can
look at? I’d love to follow along with the piecewise evolution.martin
–
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/f4a2444e-1ddd-4fc5-99a7-3253c5085c5a%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/f4a2444e-1ddd-4fc5-99a7-3253c5085c5a%40googlegroups.com?utm_medium=email&utm_source=footer
.
Brandon Barker
brandon...@gmail.com
$extfcall allows external functions to be conveniently
called inside ATS code.
When translating ATS code into C, one may want to make
extensive use of $extfcall during the first phase. Let
me use a example to show how $extfcall is typically used.
Say that you want to print out the content of the enviroment
variable HOME, and you know that the function getenv in stdlib.h
can do the work. The following code calls [getenv] externally:
(* ****** ****** )
//
#include
“share/atspre_staload.hats”
//
( ****** ****** *)
staload “libc/SATS/stdlib.sats”
(* ****** ****** *)
implement
main0 () =
{
//
val HOME =
$extfcall(string, “getenv”, “HOME”)
//
val ((void)) = println! ("${HOME} = ", HOME)
//
} (* end of [main0] *)
(* ****** ****** *)
Essentially, the expression $extfcall(string, “getenv”, “HOME”)
translates into getenv(“HOME”), and its type is assumed to be
string.
Say that you realize later that getenv may return a NULL pointer
(in the case where HOME is undefined). Then you can change a bit:
$extfcall(Stropt0, “getenv”, “HOME”)
This change may result in type-errors that need to be fixed.
If you read the doc on getenv carefully, then you probably realize that
what is returned by
getenv is not a stropt-value in the usual (functional) sense. A common way
to handle it is
to assign it the following linear type vStrptr0:
vtypedef vStrptr(l:addr) = [l:addr] (strptr(l) - void | strptr(l))
Basically, vStrptr0 means a “borrowed string”. The above code can now be
written as follows:
implement
main0 () =
{
//
val (fpf | HOME) =
$extfcall(vStrptr0, “getenv”, “HOME”)
//
val () = assertloc(isneqz(HOME)) // HOME is not NULL
//
val ((void)) = println! ("${HOME} = ", HOME)
//
prval ((void)) = fpf (HOME) // returning the borrowed string
//
} (* end of [main0] *)
After introducing the following declaration:
extern fun getenv : string → vStrptr0 = “mac#”
you can replace $exfcall(…) with getenv(“HOME”)On Tuesday, November 18, 2014 5:24:14 PM UTC-5, Martin DeMello wrote:
Has anyone migrated a C project to ATS in an open source repo that I can
look at? I’d love to follow along with the piecewise evolution.martin
thanks! those are both excellent.
martinOn Tue, Nov 18, 2014 at 2:37 PM, Chris Double chris....@double.co.nz wrote:
On Wed, Nov 19, 2014 at 11:24 AM, Martin DeMello martin...@gmail.com wrote:
Has anyone migrated a C project to ATS in an open source repo that I can
look at? I’d love to follow along with the piecewise evolution.I didn’t migrate the whole thing but I did one function of OpenSSL,
integrated into the build system, described here:<
Preventing heartbleed bugs with safe programming languagesI also wrote a bit about converting a C HTTP server here:
http://bluishcoder.co.nz/2011/04/24/converting-c-programs-to-ats.html
–
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/CALn1vHFrHL6zfM6QfAvhOn014AoxoYRPT-Y%2BtcykgiQL7C6eMw%40mail.gmail.com
.
Please, what is assertloc?Le mercredi 19 novembre 2014 03:17:06 UTC+1, gmhwxi a écrit :
Try to do this in stages (even if you wrote the original C code).
At the beginning, please try to ignore error-handling. Instead, you
can use assertloc and $UN.cast to get a value of some needed type.Overly using if-then-else to handle errors is often a sure sign of failure
in waiting.On Tuesday, November 18, 2014 5:24:14 PM UTC-5, Martin DeMello wrote:
Has anyone migrated a C project to ATS in an open source repo that I can
look at? I’d love to follow along with the piecewise evolution.martin
By the way, you can also use $UN.cast, which is less safe but very
convenient:
(* ****** ****** )
//
#include
“share/atspre_staload.hats”
//
( ****** ****** *)
staload UN = $UNSAFE
(* ****** ****** *)
staload “libc/SATS/stdlib.sats”
(* ****** ****** *)
implement
main0 () =
{
//
val HOME =
$extfcall(ptr, “getenv”, “HOME”)
val () = assertloc(isneqz(HOME))
//
val ((void)) = println! ("${HOME} = ", $UN.cast{string}(HOME))
//
} (* end of [main0] *)
Program-first program verification puts the construction of a program first.On Tuesday, November 18, 2014 5:24:14 PM UTC-5, Martin DeMello wrote:
Has anyone migrated a C project to ATS in an open source repo that I can
look at? I’d love to follow along with the piecewise evolution.martin
Try to do this in stages (even if you wrote the original C code).
At the beginning, please try to ignore error-handling. Instead, you
can use assertloc and $UN.cast to get a value of some needed type.
Overly using if-then-else to handle errors is often a sure sign of failure
in waiting.On Tuesday, November 18, 2014 5:24:14 PM UTC-5, Martin DeMello wrote:
Has anyone migrated a C project to ATS in an open source repo that I can
look at? I’d love to follow along with the piecewise evolution.martin