How Can I Make a High Level Interface to a C library?

Google Group
1

Suppose your favorite C function does some operation with an array of
values.

node_t make_node_c (unsigned id, unsigned n,  node neighbors[]);

In the ATS portion of your program, you may want to work with an easier to
use interface
like the following to make building nodes a little less tedious.

fun make_node (id: uint, neighbors: List0 (node)): node

Using functions in the ATS2 prelude, we can easily provide this
functionality.

Assume we’ve given the C function the following type in ATS. Suppose node
is just an abstract type.

abstype node = ptr

fun make_node_c {n:nat} (id: uint, n: uint n, neighbors:

&(@[node][n])): node = “mac#”

Now, let’s implement the version that takes a list instead.

implement make_node (id, neighbors) = let
    val n = g1int2uint (length (neighbors))
    //
    val (pf , gc | p) = array_ptr_alloc<node> (u2sz (n))
    val () = array_copy_from_list<node> (!p, neighbors)
    //
    val node = make_node_c (id, n, !p)
    //
    val () = array_ptr_free{node} (pf, gc | p)
 in
     node
 end

Now, building nodes using the underlying C library should be much simpler
than before. If each node is
reference counted, you would have to make the node type linear to prevent
memory leaks. Suppose
we want the following function

absvtype node = ptr

fun make_node_vt (id: uint, neighbors: !List0_vt (node)): node

Which means that we make a new node, but preserve the linear list of nodes
(The ! operator specifies the list is not consumed).
Assuming our C function doesn’t affect the reference count of any nodes in
the array we give it, we could have the following
implementation:

 implement make_node_vt (id, neighbors) = let
    val n = g1int2uint (length (neighbors))
    //
    val (pf , gc | p) = array_ptr_alloc<node> (u2sz (n))
    val () = array_copy_from_list_vt<node> (!p, neighbors)
    //
    val node = make_node_c (id, n, !p)
    //
    val nss = array_copy_to_list_vt<node> (!p, u2sz (n))
    val () = array_ptr_free{node} (pf, gc | p)
    (* Put the nodes "back" into neighbors *)
    val () = neighbors := nss
 in
     node
 end

Which may be simpler to work with than allocating, initializing,
uninitializing (freeing nodes in the arrays), and de-allocating arrays
whenever you
want to make a node.

2

Let viewtype VT be (V | T).

Then V is the view-part of VT and T is the data-part of VT.
When a value of the type VT is passed as a call-by-value parameter, the
data part of
the value stays the same but the view part may change.On Monday, January 27, 2014 2:29:27 PM UTC-5, gmhwxi wrote:

Every viewtype VT essentially equals (V | T) for some view V and
non-linear type T.
You can use VT?! to refer to the T in (V | T).

So the following declaration

fun foo (VT): void

is semantically the same as

fun foo (!VT >> VT?!): void

On Monday, January 27, 2014 1:58:34 PM UTC-5, Brandon Barker wrote:

If it is omitted for a viewtype, this is the same as saying ~
(destroyed)? This would be like call-by-reference, but it is more of a
“free-by-reference”.

On Sunday, January 26, 2014 1:41:43 PM UTC-5, gmhwxi wrote:

! means call-by-value and & means call-by-reference.

When we write

fun foo (int, int): bool

we really mean

fun foo (!int, !int): bool

‘!’ in !T can be omitted unless T is a view or viewtype.

On Sunday, January 26, 2014 1:39:22 PM UTC-5, gmhwxi wrote:

The type for make_node_vt should be:

fun make_node_vt (id: uint, neighbors: &List0_vt (node)): node

Otherwise, the assignment (node := nss) in the code would cause a
compile-time error.

On Sunday, January 26, 2014 1:00:36 PM UTC-5, William Blair wrote:

Suppose your favorite C function does some operation with an array of
values.

node_t make_node_c (unsigned id, unsigned n,  node neighbors[]);

In the ATS portion of your program, you may want to work with an
easier to use interface
like the following to make building nodes a little less tedious.

fun make_node (id: uint, neighbors: List0 (node)): node

Using functions in the ATS2 prelude, we can easily provide this
functionality.

Assume we’ve given the C function the following type in ATS. Suppose
node is just an abstract type.

abstype node = ptr

fun make_node_c {n:nat} (id: uint, n: uint n, neighbors:

&(@[node][n])): node = “mac#”

Now, let’s implement the version that takes a list instead.

implement make_node (id, neighbors) = let
    val n = g1int2uint (length (neighbors))
    //
    val (pf , gc | p) = array_ptr_alloc<node> (u2sz (n))
    val () = array_copy_from_list<node> (!p, neighbors)
    //
    val node = make_node_c (id, n, !p)
    //
    val () = array_ptr_free{node} (pf, gc | p)
 in
     node
 end

Now, building nodes using the underlying C library should be much
simpler than before. If each node is
reference counted, you would have to make the node type linear to
prevent memory leaks. Suppose
we want the following function

absvtype node = ptr

fun make_node_vt (id: uint, neighbors: !List0_vt (node)): node

Which means that we make a new node, but preserve the linear list of
nodes (The ! operator specifies the list is not consumed).
Assuming our C function doesn’t affect the reference count of any
nodes in the array we give it, we could have the following
implementation:

 implement make_node_vt (id, neighbors) = let
    val n = g1int2uint (length (neighbors))
    //
    val (pf , gc | p) = array_ptr_alloc<node> (u2sz (n))
    val () = array_copy_from_list_vt<node> (!p, neighbors)
    //
    val node = make_node_c (id, n, !p)
    //
    val nss = array_copy_to_list_vt<node> (!p, u2sz (n))
    val () = array_ptr_free{node} (pf, gc | p)
    (* Put the nodes "back" into neighbors *)
    val () = neighbors := nss
 in
     node
 end

Which may be simpler to work with than allocating, initializing,
uninitializing (freeing nodes in the arrays), and de-allocating arrays
whenever you
want to make a node.

3

! means call-by-value and & means call-by-reference.

When we write

fun foo (int, int): bool

we really mean

fun foo (!int, !int): bool

‘!’ in !T can be omitted unless T is a view or viewtype.On Sunday, January 26, 2014 1:39:22 PM UTC-5, gmhwxi wrote:

The type for make_node_vt should be:

fun make_node_vt (id: uint, neighbors: &List0_vt (node)): node

Otherwise, the assignment (node := nss) in the code would cause a
compile-time error.

On Sunday, January 26, 2014 1:00:36 PM UTC-5, William Blair wrote:

Suppose your favorite C function does some operation with an array of
values.

node_t make_node_c (unsigned id, unsigned n,  node neighbors[]);

In the ATS portion of your program, you may want to work with an easier
to use interface
like the following to make building nodes a little less tedious.

fun make_node (id: uint, neighbors: List0 (node)): node

Using functions in the ATS2 prelude, we can easily provide this
functionality.

Assume we’ve given the C function the following type in ATS. Suppose node
is just an abstract type.

abstype node = ptr

fun make_node_c {n:nat} (id: uint, n: uint n, neighbors:

&(@[node][n])): node = “mac#”

Now, let’s implement the version that takes a list instead.

implement make_node (id, neighbors) = let
    val n = g1int2uint (length (neighbors))
    //
    val (pf , gc | p) = array_ptr_alloc<node> (u2sz (n))
    val () = array_copy_from_list<node> (!p, neighbors)
    //
    val node = make_node_c (id, n, !p)
    //
    val () = array_ptr_free{node} (pf, gc | p)
 in
     node
 end

Now, building nodes using the underlying C library should be much simpler
than before. If each node is
reference counted, you would have to make the node type linear to prevent
memory leaks. Suppose
we want the following function

absvtype node = ptr

fun make_node_vt (id: uint, neighbors: !List0_vt (node)): node

Which means that we make a new node, but preserve the linear list of
nodes (The ! operator specifies the list is not consumed).
Assuming our C function doesn’t affect the reference count of any nodes
in the array we give it, we could have the following
implementation:

 implement make_node_vt (id, neighbors) = let
    val n = g1int2uint (length (neighbors))
    //
    val (pf , gc | p) = array_ptr_alloc<node> (u2sz (n))
    val () = array_copy_from_list_vt<node> (!p, neighbors)
    //
    val node = make_node_c (id, n, !p)
    //
    val nss = array_copy_to_list_vt<node> (!p, u2sz (n))
    val () = array_ptr_free{node} (pf, gc | p)
    (* Put the nodes "back" into neighbors *)
    val () = neighbors := nss
 in
     node
 end

Which may be simpler to work with than allocating, initializing,
uninitializing (freeing nodes in the arrays), and de-allocating arrays
whenever you
want to make a node.

4

If it is omitted for a viewtype, this is the same as saying ~ (destroyed)?
This would be like call-by-reference, but it is more of a
“free-by-reference”.On Sunday, January 26, 2014 1:41:43 PM UTC-5, gmhwxi wrote:

! means call-by-value and & means call-by-reference.

When we write

fun foo (int, int): bool

we really mean

fun foo (!int, !int): bool

‘!’ in !T can be omitted unless T is a view or viewtype.

On Sunday, January 26, 2014 1:39:22 PM UTC-5, gmhwxi wrote:

The type for make_node_vt should be:

fun make_node_vt (id: uint, neighbors: &List0_vt (node)): node

Otherwise, the assignment (node := nss) in the code would cause a
compile-time error.

On Sunday, January 26, 2014 1:00:36 PM UTC-5, William Blair wrote:

Suppose your favorite C function does some operation with an array of
values.

node_t make_node_c (unsigned id, unsigned n,  node neighbors[]);

In the ATS portion of your program, you may want to work with an easier
to use interface
like the following to make building nodes a little less tedious.

fun make_node (id: uint, neighbors: List0 (node)): node

Using functions in the ATS2 prelude, we can easily provide this
functionality.

Assume we’ve given the C function the following type in ATS. Suppose
node is just an abstract type.

abstype node = ptr

fun make_node_c {n:nat} (id: uint, n: uint n, neighbors:

&(@[node][n])): node = “mac#”

Now, let’s implement the version that takes a list instead.

implement make_node (id, neighbors) = let
    val n = g1int2uint (length (neighbors))
    //
    val (pf , gc | p) = array_ptr_alloc<node> (u2sz (n))
    val () = array_copy_from_list<node> (!p, neighbors)
    //
    val node = make_node_c (id, n, !p)
    //
    val () = array_ptr_free{node} (pf, gc | p)
 in
     node
 end

Now, building nodes using the underlying C library should be much
simpler than before. If each node is
reference counted, you would have to make the node type linear to
prevent memory leaks. Suppose
we want the following function

absvtype node = ptr

fun make_node_vt (id: uint, neighbors: !List0_vt (node)): node

Which means that we make a new node, but preserve the linear list of
nodes (The ! operator specifies the list is not consumed).
Assuming our C function doesn’t affect the reference count of any nodes
in the array we give it, we could have the following
implementation:

 implement make_node_vt (id, neighbors) = let
    val n = g1int2uint (length (neighbors))
    //
    val (pf , gc | p) = array_ptr_alloc<node> (u2sz (n))
    val () = array_copy_from_list_vt<node> (!p, neighbors)
    //
    val node = make_node_c (id, n, !p)
    //
    val nss = array_copy_to_list_vt<node> (!p, u2sz (n))
    val () = array_ptr_free{node} (pf, gc | p)
    (* Put the nodes "back" into neighbors *)
    val () = neighbors := nss
 in
     node
 end

Which may be simpler to work with than allocating, initializing,
uninitializing (freeing nodes in the arrays), and de-allocating arrays
whenever you
want to make a node.

5

That is a good point. To do it safely requires a lot of proof code.
Here is what I would do:

val () = array_copy_from_list<node?>
(!p, $UN.castvwtp1{list(node?,n)}(neighbours) // copy the data
prval pf = $UN.cast{array(l,node,n)}(pf) // borrow the view
(*
// process the array
*)
prval pf = $UN.castview1{array(l,node?,n)}(pf) // return the view
val () = array_ptr_free (pf, pfgc | p) // free the array

This one assumes that process the array does not alter the data.

If data is altered, then the data needs to be copied back into the list.
For instance, this is how list_vt_quicksort is implemented based on
array_quicksort:

http://www.ats-lang.org/DOCUMENT/ATS-Postiats/prelude/DATS/list_vt_quicksort.datsOn Wednesday, January 29, 2014 12:24:31 AM UTC-5, Zhiqiang Ren wrote:

In " make_node_vt (id, neighbors)" we actually destroy the old linear list
and create a new one, which seems a little bit waste. Any way to avoid it?

On Sunday, January 26, 2014 1:00:36 PM UTC-5, William Blair wrote:

Suppose your favorite C function does some operation with an array of
values.

node_t make_node_c (unsigned id, unsigned n,  node neighbors[]);

In the ATS portion of your program, you may want to work with an easier
to use interface
like the following to make building nodes a little less tedious.

fun make_node (id: uint, neighbors: List0 (node)): node

Using functions in the ATS2 prelude, we can easily provide this
functionality.

Assume we’ve given the C function the following type in ATS. Suppose node
is just an abstract type.

abstype node = ptr

fun make_node_c {n:nat} (id: uint, n: uint n, neighbors:

&(@[node][n])): node = “mac#”

Now, let’s implement the version that takes a list instead.

implement make_node (id, neighbors) = let
    val n = g1int2uint (length (neighbors))
    //
    val (pf , gc | p) = array_ptr_alloc<node> (u2sz (n))
    val () = array_copy_from_list<node> (!p, neighbors)
    //
    val node = make_node_c (id, n, !p)
    //
    val () = array_ptr_free{node} (pf, gc | p)
 in
     node
 end

Now, building nodes using the underlying C library should be much simpler
than before. If each node is
reference counted, you would have to make the node type linear to prevent
memory leaks. Suppose
we want the following function

absvtype node = ptr

fun make_node_vt (id: uint, neighbors: !List0_vt (node)): node

Which means that we make a new node, but preserve the linear list of
nodes (The ! operator specifies the list is not consumed).
Assuming our C function doesn’t affect the reference count of any nodes
in the array we give it, we could have the following
implementation:

 implement make_node_vt (id, neighbors) = let
    val n = g1int2uint (length (neighbors))
    //
    val (pf , gc | p) = array_ptr_alloc<node> (u2sz (n))
    val () = array_copy_from_list_vt<node> (!p, neighbors)
    //
    val node = make_node_c (id, n, !p)
    //
    val nss = array_copy_to_list_vt<node> (!p, u2sz (n))
    val () = array_ptr_free{node} (pf, gc | p)
    (* Put the nodes "back" into neighbors *)
    val () = neighbors := nss
 in
     node
 end

Which may be simpler to work with than allocating, initializing,
uninitializing (freeing nodes in the arrays), and de-allocating arrays
whenever you
want to make a node.

6

Every viewtype VT essentially equals (V | T) for some view V and non-linear
type T.
You can use VT?! to refer to the T in (V | T).

So the following declaration

fun foo (VT): void

is semantically the same as

fun foo (!VT >> VT?!): voidOn Monday, January 27, 2014 1:58:34 PM UTC-5, Brandon Barker wrote:

If it is omitted for a viewtype, this is the same as saying ~ (destroyed)?
This would be like call-by-reference, but it is more of a
“free-by-reference”.

On Sunday, January 26, 2014 1:41:43 PM UTC-5, gmhwxi wrote:

! means call-by-value and & means call-by-reference.

When we write

fun foo (int, int): bool

we really mean

fun foo (!int, !int): bool

‘!’ in !T can be omitted unless T is a view or viewtype.

On Sunday, January 26, 2014 1:39:22 PM UTC-5, gmhwxi wrote:

The type for make_node_vt should be:

fun make_node_vt (id: uint, neighbors: &List0_vt (node)): node

Otherwise, the assignment (node := nss) in the code would cause a
compile-time error.

On Sunday, January 26, 2014 1:00:36 PM UTC-5, William Blair wrote:

Suppose your favorite C function does some operation with an array of
values.

node_t make_node_c (unsigned id, unsigned n,  node neighbors[]);

In the ATS portion of your program, you may want to work with an easier
to use interface
like the following to make building nodes a little less tedious.

fun make_node (id: uint, neighbors: List0 (node)): node

Using functions in the ATS2 prelude, we can easily provide this
functionality.

Assume we’ve given the C function the following type in ATS. Suppose
node is just an abstract type.

abstype node = ptr

fun make_node_c {n:nat} (id: uint, n: uint n, neighbors:

&(@[node][n])): node = “mac#”

Now, let’s implement the version that takes a list instead.

implement make_node (id, neighbors) = let
    val n = g1int2uint (length (neighbors))
    //
    val (pf , gc | p) = array_ptr_alloc<node> (u2sz (n))
    val () = array_copy_from_list<node> (!p, neighbors)
    //
    val node = make_node_c (id, n, !p)
    //
    val () = array_ptr_free{node} (pf, gc | p)
 in
     node
 end

Now, building nodes using the underlying C library should be much
simpler than before. If each node is
reference counted, you would have to make the node type linear to
prevent memory leaks. Suppose
we want the following function

absvtype node = ptr

fun make_node_vt (id: uint, neighbors: !List0_vt (node)): node

Which means that we make a new node, but preserve the linear list of
nodes (The ! operator specifies the list is not consumed).
Assuming our C function doesn’t affect the reference count of any nodes
in the array we give it, we could have the following
implementation:

 implement make_node_vt (id, neighbors) = let
    val n = g1int2uint (length (neighbors))
    //
    val (pf , gc | p) = array_ptr_alloc<node> (u2sz (n))
    val () = array_copy_from_list_vt<node> (!p, neighbors)
    //
    val node = make_node_c (id, n, !p)
    //
    val nss = array_copy_to_list_vt<node> (!p, u2sz (n))
    val () = array_ptr_free{node} (pf, gc | p)
    (* Put the nodes "back" into neighbors *)
    val () = neighbors := nss
 in
     node
 end

Which may be simpler to work with than allocating, initializing,
uninitializing (freeing nodes in the arrays), and de-allocating arrays
whenever you
want to make a node.

7

In " make_node_vt (id, neighbors)" we actually destroy the old linear list
and create a new one, which seems a little bit waste. Any way to avoid it?On Sunday, January 26, 2014 1:00:36 PM UTC-5, William Blair wrote:

Suppose your favorite C function does some operation with an array of
values.

node_t make_node_c (unsigned id, unsigned n,  node neighbors[]);

In the ATS portion of your program, you may want to work with an easier to
use interface
like the following to make building nodes a little less tedious.

fun make_node (id: uint, neighbors: List0 (node)): node

Using functions in the ATS2 prelude, we can easily provide this
functionality.

Assume we’ve given the C function the following type in ATS. Suppose node
is just an abstract type.

abstype node = ptr

fun make_node_c {n:nat} (id: uint, n: uint n, neighbors:

&(@[node][n])): node = “mac#”

Now, let’s implement the version that takes a list instead.

implement make_node (id, neighbors) = let
    val n = g1int2uint (length (neighbors))
    //
    val (pf , gc | p) = array_ptr_alloc<node> (u2sz (n))
    val () = array_copy_from_list<node> (!p, neighbors)
    //
    val node = make_node_c (id, n, !p)
    //
    val () = array_ptr_free{node} (pf, gc | p)
 in
     node
 end

Now, building nodes using the underlying C library should be much simpler
than before. If each node is
reference counted, you would have to make the node type linear to prevent
memory leaks. Suppose
we want the following function

absvtype node = ptr

fun make_node_vt (id: uint, neighbors: !List0_vt (node)): node

Which means that we make a new node, but preserve the linear list of nodes
(The ! operator specifies the list is not consumed).
Assuming our C function doesn’t affect the reference count of any nodes in
the array we give it, we could have the following
implementation:

 implement make_node_vt (id, neighbors) = let
    val n = g1int2uint (length (neighbors))
    //
    val (pf , gc | p) = array_ptr_alloc<node> (u2sz (n))
    val () = array_copy_from_list_vt<node> (!p, neighbors)
    //
    val node = make_node_c (id, n, !p)
    //
    val nss = array_copy_to_list_vt<node> (!p, u2sz (n))
    val () = array_ptr_free{node} (pf, gc | p)
    (* Put the nodes "back" into neighbors *)
    val () = neighbors := nss
 in
     node
 end

Which may be simpler to work with than allocating, initializing,
uninitializing (freeing nodes in the arrays), and de-allocating arrays
whenever you
want to make a node.

8

The type for make_node_vt should be:

fun make_node_vt (id: uint, neighbors: &List0_vt (node)): node

Otherwise, the assignment (node := nss) in the code would cause a
compile-time error.On Sunday, January 26, 2014 1:00:36 PM UTC-5, William Blair wrote:

Suppose your favorite C function does some operation with an array of
values.

node_t make_node_c (unsigned id, unsigned n,  node neighbors[]);

In the ATS portion of your program, you may want to work with an easier to
use interface
like the following to make building nodes a little less tedious.

fun make_node (id: uint, neighbors: List0 (node)): node

Using functions in the ATS2 prelude, we can easily provide this
functionality.

Assume we’ve given the C function the following type in ATS. Suppose node
is just an abstract type.

abstype node = ptr

fun make_node_c {n:nat} (id: uint, n: uint n, neighbors:

&(@[node][n])): node = “mac#”

Now, let’s implement the version that takes a list instead.

implement make_node (id, neighbors) = let
    val n = g1int2uint (length (neighbors))
    //
    val (pf , gc | p) = array_ptr_alloc<node> (u2sz (n))
    val () = array_copy_from_list<node> (!p, neighbors)
    //
    val node = make_node_c (id, n, !p)
    //
    val () = array_ptr_free{node} (pf, gc | p)
 in
     node
 end

Now, building nodes using the underlying C library should be much simpler
than before. If each node is
reference counted, you would have to make the node type linear to prevent
memory leaks. Suppose
we want the following function

absvtype node = ptr

fun make_node_vt (id: uint, neighbors: !List0_vt (node)): node

Which means that we make a new node, but preserve the linear list of nodes
(The ! operator specifies the list is not consumed).
Assuming our C function doesn’t affect the reference count of any nodes in
the array we give it, we could have the following
implementation:

 implement make_node_vt (id, neighbors) = let
    val n = g1int2uint (length (neighbors))
    //
    val (pf , gc | p) = array_ptr_alloc<node> (u2sz (n))
    val () = array_copy_from_list_vt<node> (!p, neighbors)
    //
    val node = make_node_c (id, n, !p)
    //
    val nss = array_copy_to_list_vt<node> (!p, u2sz (n))
    val () = array_ptr_free{node} (pf, gc | p)
    (* Put the nodes "back" into neighbors *)
    val () = neighbors := nss
 in
     node
 end

Which may be simpler to work with than allocating, initializing,
uninitializing (freeing nodes in the arrays), and de-allocating arrays
whenever you
want to make a node.