Bluish Coder

I'm back to using the ATS programming language after a bit of a break. My first thought upon getting back into the language is how easy it is to forget how to write in a language you don't use often. It's starting to come back to me though.

For my current task I needed to read string data from a file. This is a basic snippet of an approach:

%{^
#include "libc/CATS/fcntl.cats"
%}

staload "libc/SATS/fcntl.sats"

implement main() = let
  val (pf_fh | fh) = open_flag_exn("test.txt", O_RDONLY)
  var !p_buf with pf_buf = @[byte][4]()
  val n = read_exn(pf_fh | fh, !p_buf, 3)
  val () = bytes_strbuf_trans(pf_buf | p_buf, n)
  val () = print_strbuf(!p_buf)
  val () = close_exn (pf_fh | fh)
in
  pf_buf := bytes_v_of_strbuf_v (pf_buf)
end

This uses the fcntl libc routines for which ATS provides wrappers. The call to open_flag_exn returns a file handle, fh, and a proof, pf_fh. This proof needs to be passed to calls to read from the file (to ensure we're reading from an open file) and it must be consumed to ensure the file is closed.

The @[byte][4]() syntax defines a four element array, allocated on the stack, containing bytes. It returns a pointer to the array, p_buf, and a proof, pf_buf. read_exn reads three bytes from the file into this array. The size of the array is known by the type system and the definition of read_exn ensures that the number of bytes we read isn't greater than the size of the array at compile time. For example, the following would be a compile error:

val n = read_exn(pf_fh | fh, !p_buf, 5)

We have an array of bytes but I want to deal with this as a string. ATS has a number of string types, including:

• string: A non linear string that can only be free'd by the garbage collector
• strbuf: A flat array of bytes where the last byte is null
• strptr: A linear string which must be manually free'd

I want to later pass the data along to C functions that expect a null terminated C string. To do this I will convert the array of bytes into a strbuf. The function bytes_strbuf_trans converts the array in-place, adding a null terminator. The length of string is passed as an argument. The terminator is added immediately following this. That's what this line does:

val () = bytes_strbuf_trans(pf_buf | p_buf, n)

p_buf is the pointer to our buffer. pf_buf is the proof that says this is a pointer to an array of bytes. This proof is changed to be a proof that p_buf is a strbuf by the bytes_strbuf_trans call. The definition of this function shows that (from the ATS prelude):

fun bytes_strbuf_trans
  {m,n:nat | n < m} {l:addr}
  (pf: !b0ytes m @ l >> strbuf (m, n1) @ l | p: ptr l, n: size_t n)
  :<> #[n1: nat | n1 <= n] void

The type system again ensure that the size does not exceed the size of the original array we allocated on the stack. It also ensure's there is room in the buffer for the null terminator. If I change the call to the following I will get a compile error:

val () = bytes_strbuf_trans(pf_buf | p_buf, 4)

The {m,n:nat | n<m} in the bytes_strbuf_trans definition constrains the size I pass in to be less than the size of the buffer.

Now that we have a proof that p_buf is a strbuf we can use print_strbuf to print the resulting three characters read from the file. Once we've finished with the strbuf we have to change the proof back to say it's an array of bytes otherwise the type checker thinks we've consumed the byte array (as we have no proof for it). This is what the following line does:

pf_buf := bytes_v_of_strbuf_v (pf_buf)

Although this is a simple snippet of code and a simple task the type checking in ATS did save me from some errors in my larger program that this snippet can be used to demonstrate:

• The read call must not read more data than the size of the buffer allows.
• The conversion to a C string in-place means we need to read one less than the size of the buffer.
• The file must be closed after use.

All these issues resulted in compile time errors.