datavtypes

[ice.r...@gmail.com]

Hi again :)

I have function

fn

  recvfrom

  {l: addr} {n: pos}

  ( buf_pf: array_v(char?, l, n)

  | socket_fd: int

  , buf: ptr l

  , sz: size_t n

  , flags: int

  , src_addr: &sockaddr_in_struct?

  , addr_sz: &size_t

  ): [m:int] ssize_t int

I want to change it's return type, such that in case of success, it should split buf_pf on 2 arrays: initialized and unintialized one and src_addr to became initialized.

In case of failure, I want to return buf_pf and src_addr of the same view (uninitialized)

How can I do it properly?

[Dambaev Alexander]

My current, not so successful try is to define result_vt:

datavtype result_vt (av: view, a:t@ype+, bv: view, b:t@ype+) =
  | Success_vt(av,a, bv, b) of (av | a)
  | Failure_vt(av,a, bv, b) of (bv | b)

and function's ftype:

fn

  recvfrom

  {l: addr} {n: pos}

  ( buf_pf: array_v(char?, l, n)

  | socket_fd: int

  , buf: ptr l

  , sz: size_t n

  , flags: int

  , src_addr: &sockaddr_in_struct?

  , addr_sz: &size_t

  ): [m:pos | m <= n] result_vt( (array_v(char,l,m), array_v(char?,l+m, n-m)), (sockaddr_in_struct, size_t m), array_v(char?,l,n), void) =

  let
    val ret = g1ofg0( $extfcall(ssize_t, "recvfrom", socket_fd, buf, sz, flags, addr@src_addr, addr@addr_sz))
  in
  if ret < 1
  then Failure_vt( buf_pf | ())
  else Success_vt( (answer_pf, rest_buf_pf) | (src_addr, ret) (*complains on this line *) ) where {
    extern praxi unnil{v:viewt0ype} ( p: &v? >> v): void
    prval () = unnil(src_addr)
    val (answer_pf, rest_buf_pf) = array_v_split( buf_pf)
  }
  end

but compiler is not happy with it, giving me errors:
error(3): the dynamic expression cannot be assigned the type [S2EVar(5259)].
error(3): mismatch of sorts in unification:
The sort of variable is: S2RTbas(S2RTBASimp(9; t@ype+))
The sort of solution is: S2RTbas(S2RTBASimp(3; viewt0ype))
error(3): mismatch of static terms (tyleq):
The actual term is: S2Etyrec(flt0; npf=-1; 0=S2EVar(5253), 1=S2Eapp(S2Ecst(g1int_int_t0ype); S2Eextkind(atstype_ssize), S2Evar(i$8638$8639(14396))))
The needed term is: S2EVar(5259)

пт, 10 июл. 2020 г. в 12:47, ice.r...@gmail.com <ice.r...@gmail.com>:

--
You received this message because you are subscribed to a topic in the Google Groups "ats-lang-users" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/ats-lang-users/O-KlWtJqq1I/unsubscribe.
To unsubscribe from this group and all its topics, send an email to ats-lang-user...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/e013b1ec-d89b-49f9-b79a-46803b480bcen%40googlegroups.com.

[gmhwxi]

Your idea is correct. Here is what I would do:

dataview
recvfrom_v(addr, int, int) =
|
{l:addr}
{n:int}
{m:int | m < 0}
recvfrom_v_fail(l, n, m) of array_v(char?, l, n)
|
{l:addr}
{n:int}
{m:nat|m <= n}
recvfrom_v_succ(l, n, m) of
(array_v(char, l, m), array_v(char?, l+m*sizeof(char), n-m))

fn
recvfrom
{l: addr} {n: pos}
( buf_pf

: array_v(char?, l, n) >> recvfrom_v(l, n, m)

| socket_fd: int
, buf: ptr l
, sz: size_t n
, flags: int

, src_addr: &sockaddr_in_struct? >> opt(sockaddr_in_struct, m >= 0)
, addr_sz: &size_t
) : #[m:int] ssize_t(m)

Please note the symbol '#' in front of the quantifer [m:int].

пт, 10 июл. 2020 г. в 12:47, ice.r...@gmail.com <...>:

Hi again :)

I have function

fn

  recvfrom

  {l: addr} {n: pos}

  ( buf_pf: array_v(char?, l, n)

  | socket_fd: int

  , buf: ptr l

  , sz: size_t n

  , flags: int

  , src_addr: &sockaddr_in_struct?

  , addr_sz: &size_t

  ): [m:int] ssize_t int

I want to change it's return type, such that in case of success, it should split buf_pf on 2 arrays: initialized and unintialized one and src_addr to became initialized.

In case of failure, I want to return buf_pf and src_addr of the same view (uninitialized)

How can I do it properly?

--
You received this message because you are subscribed to a topic in the Google Groups "ats-lang-users" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/ats-lang-users/O-KlWtJqq1I/unsubscribe.

To unsubscribe from this group and all its topics, send an email to ats-lang-users+unsubscribe@googlegroups.com.

[Dambaev Alexander]

Hi,

thanks for your advice: I think your way is much better, because it does not requires heap usage

My working code looks like this (in case if someone will struggle with similar stuff):

```

dataview recvfrom_v(addr, int, int) =

  | {l:agz}{n:pos}{m:int | m <= 0 || m > n}

    recvfrom_v_fail(l, n, m) of array_v(char?, l, n)

  | {l:agz}{n:pos}{m:pos | m <= n}
    recvfrom_v_succ(l,n,m) of ( array_v( char, l, m), array_v( char?, l+m*sizeof(char), n-m))

fn recvfrom
  {l: agz} {n: pos}
  ( buf_pf: !array_v(char?, l, n) >> recvfrom_v(l,n,m)

  | socket_fd: int
  , buf: ptr l
  , sz: size_t n
  , flags: int

  , src_addr: &sockaddr_in_struct? >> opt( sockaddr_in_struct, m > 0 && m <= n)
  , addr_sz: &size_t
  ): #[m:int | m <= n] ssize_t(m) =

  let
    val ret = g1ofg0( $extfcall(ssize_t, "recvfrom", socket_fd, buf, sz, flags, addr@src_addr, addr@addr_sz))
  in

    if ret <= 0
    then
      let
        prval () = buf_pf := recvfrom_v_fail( buf_pf)
        prval () = opt_none( src_addr)
      in
        ret
      end
    else
      let
        val uret = g1int2uint(ret)
        val () = assert_errmsg( g1int2uint(ret) <= sz, "the impossible happend: recvfrom() readed more than buffer, memory had been corrupted")
        prval (answer_nil_pf, rest_buf_pf) = array_v_split_at(buf_pf | uret)
        extern prfun array_v_unnil_nz{a:viewt0ype}{n:pos}( p: array_v(a?,l,n)): array_v(a,l,n)
        prval answer_pf = array_v_unnil_nz(answer_nil_pf)
        prval () = buf_pf := recvfrom_v_succ( answer_pf, rest_buf_pf)

        extern praxi unnil{v:viewt0ype} ( p: &v? >> v): void
        prval () = unnil(src_addr)

        prval () = opt_some(src_addr)
      in
        ret
      end
  end

```

and usage is like this:

```

                    var sin: sockaddr_in_struct?
                    var sin_sz: size_t = sizeof<sockaddr_in_struct>
                    val readed = recvfrom( recv_buf_pf|  x.fd, recv_buf, recv_sz, 0, sin, sin_sz)
                  in
                    if readed <= 0
                    then
                      let
                        val _ = $extfcall( int, "sprintf", str_buf, "unable to read from socket")
                        val () = log_error( addr@str_buf)
                        prval recvfrom_v_fail( recv_buf_pf1) = recv_buf_pf
                        prval () = recv_buf_pf := recv_buf_pf1
                        prval () = opt_unnone( sin)
                      in
                        ()
                      end
                    else
                      let
                        val ureaded = g1int2uint(readed)
                        prval recvfrom_v_succ( request_pf, rest_buf_pf) = recv_buf_pf
                        prval () = opt_unsome(sin) (* sin had been initialized *)
                       
                        (* do useful stuff here *)
                        val _ = $extfcall( int, "sprintf", str_buf, "readed %i bytes", ureaded)
                        val () = log_info( addr@str_buf)
                        val () = handle_client_packet( request_pf | x.fd, recv_buf, ureaded, sin, sin_sz)
                       
                        (* now cleanup buffers and proofs*)
                        extern prfun array_v_nil_nz{a:viewt0ype}{n:pos}( p: array_v(a,l,n)): array_v(a?,l,n) (* there is no std way to mark initialized array as uninitialized *)
                        prval request_nil_pf = array_v_nil_nz( request_pf)
                        prval () = recv_buf_pf := array_v_unsplit( request_nil_pf, rest_buf_pf)
                      in
                        ()
                      end
                  end

```

Overall, I found this way of handling optional cases is quite interesting, although, I had spent a half of day fighting with the type checker. But it turned out, that it was mostly complaining on my code due to usage different style of sequencing: it turned out, that it likes more

....

  ): #[m:int | m <= n] ssize_t(m) =

  let
    val ret = g1ofg0( $extfcall(ssize_t, "recvfrom", socket_fd, buf, sz, flags, addr@src_addr, addr@addr_sz))
  in

    if ret <= 0
    then
      let
        prval () = buf_pf := recvfrom_v_fail( buf_pf)
        prval () = opt_none( src_addr)
      in
        ret
      end
    else

 ....

```

instead of this (which I like more, because it is not so verbose)

```

  ): #[m:int | m <= n] ssize_t(m) = ret where {

    val ret = g1ofg0( $extfcall(ssize_t, "recvfrom", socket_fd, buf, sz, flags, addr@src_addr, addr@addr_sz))

    val () =

      if ret <= 0
      then {
        prval () = buf_pf := recvfrom_v_fail( buf_pf)
        prval () = opt_none( src_addr)
     }
    else

    ...

```

looks like it is harder to split branches for compiler in the latter case

[Dambaev Alexander]

And at the end, it turned out, that I am not required to manually write those proofs:

```

extern
fn recvfrom
  {l: agz} {n: pos}{addr_sz:pos}

  ( buf_pf: !array_v(char?, l, n) >> recvfrom_v(l,n,m)
  | socket_fd: int
  , buf: ptr l
  , sz: size_t n
  , flags: int

  , src_addr: &sockaddr_struct(addr_sz)? >> opt(sockaddr_struct(addr_sz), m > 0 && m <= n) (* technically, recvfrom expects sockaddr, not sockaddr_in here *)
  , addr_sz: &(socklen_t addr_sz)

  ): #[m:int | m <= n] ssize_t(m)

implement recvfrom{l}{n}(buf_pf | socket_fd, buf, sz, flags, src_addr, addr_sz) = c_recvfrom( buf_pf| socket_fd, buf, sz, flags, src_addr, addr_sz) where {
  (* have to define another wrapper here, as only inside this call src_addr has type sockaddr_struct, not 'incompatible' sockaddr_in like in caller and produces compiler warning *)
  extern
  fn c_recvfrom
    {l: agz} {n: pos}{addr_sz:pos}{sa_l:addr}

    ( buf_pf: !array_v(char?, l, n) >> recvfrom_v(l,n,m)
    | socket_fd: int
    , buf: ptr l
    , sz: size_t n
    , flags: int

    , src_addr: &sockaddr_struct(addr_sz)? >> opt(sockaddr_struct(addr_sz), m > 0 && m <= n)
    , addr_sz: &(socklen_t addr_sz)
    ): #[m:int | m <= n] ssize_t(m) = "mac#recvfrom"
}

```

and the usage:

```

                    var sin: sockaddr_in_struct?
                    var sin_sz: socklen_t(socklen_in) = socklen_in
                    extern castfn socklen2int{n:int}(i: socklen_t(n)): int(n)
                    val () = assert_errmsg(socklen2int(sin_sz) > 0, "sin_sz <= 0") (* should be {n:pos} socklen_t(n), to not to prove, that sockaddr size > 0 *)
                    extern praxi sockaddr_in_trans_nil( pf: !sockaddr_in_struct? @ sin >> sockaddr_struct(socklen_in)? @ sin): void
                    extern praxi sockaddr_trans_in_nil( pf: !sockaddr_struct(socklen_in)? @ sin >> sockaddr_in_struct? @ sin): void
                    prval () = sockaddr_in_trans_nil( view@sin)
                    val readed = $C.recvfrom( recv_buf_pf |  x.fd, recv_buf, recv_sz, 0, sin, sin_sz)

                  in
                    if readed <= 0
                    then let
                        val _ = $extfcall( int, "sprintf", str_buf, "unable to read from socket")

                        val () = $Log.log_error( addr@str_buf)
                        prval $C.recvfrom_v_fail( recv_buf_pf1) = recv_buf_pf

                        prval () = recv_buf_pf := recv_buf_pf1
                        prval () = opt_unnone( sin)

                        prval () = sockaddr_trans_in_nil( view@sin)

                      in () end
                    else let
                        val ureaded = g1int2uint(readed)

                        prval $C.recvfrom_v_succ( request_pf, rest_buf_pf) = recv_buf_pf

                        prval () = opt_unsome(sin) (* sin had been initialized *)
                       
                        (* do useful stuff here *)

                        val _ = $extfcall( int, "sprintf", str_buf, "readed %li bytes", ureaded)
                        val () = $Log.log_info( addr@str_buf)

                        val () = handle_client_packet( request_pf | x.fd, recv_buf, ureaded, sin, sin_sz)
                       
                        (* now cleanup buffers and proofs*)
                        extern prfun array_v_nil_nz{a:viewt0ype}{n:pos}( p: array_v(a,l,n)): array_v(a?,l,n) (* there is no std way to mark initialized array as uninitialized *)
                        prval request_nil_pf = array_v_nil_nz( request_pf)
                        prval () = recv_buf_pf := array_v_unsplit( request_nil_pf, rest_buf_pf)

                        prval () = sockaddr_trans_in(view@sin)
                      in () end

```

[gmhwxi]

Am really pleased that you figured it out :)

This is pure C-style of systems programming. While it can be done in ATS,

it is often quite involved. The recvfrom function you implemented actually shows

that it does not make use of more resources that what is given.

One possibility is to introduce a linear functional API for recvfrom:

absvtype sockaddr

datavtype
recvfrom_vt =
|
recvfrom_fail of ()
|
recvfrom_succ of
{m:nat} (arrpsz(char, m), sockaddr)

fun
ATS_recvfrom
{n:pos}
(sz: size_t(n), flags: int): recvfrom_vt

ATS_recvfrom calls malloc to obtain memory. However, we can differentiate

various malloc calls. For embedded programming, we can implement a malloc

that only allocates from statically allocated memory.

Basically, what I am saying here is that low-level systems programming can be

done in a linear functional style with customized implementations of malloc/free.

I feel that we are getting very close to this vision :)

[Dambaev Alexander]

вс, 12 июл. 2020 г. в 15:50, gmhwxi <gmh...@gmail.com>:

Am really pleased that you figured it out :)

It was pleasure for me as well :D

The first time, when I started to think about it, was when I saw that array_v_split has no parameters and I asked myself "how does it know on which parts it should be splitted". Then I saw an article https://bluishcoder.co.nz/2010/06/02/safer-c-code-using-ats.html when I was searching more info about #[] syntax of return type and I was like "wow".

This is pure C-style of systems programming. While it can be done in ATS,

it is often quite involved. The recvfrom function you implemented actually shows

that it does not make use of more resources that what is given.

yes, usually C-functions should not allocate memory themselves. Otherwise, where all those custom allocators will be used? :)

And to be serious: during the time, that I had spent with haskell and ocaml, I came to conclusion, that one of big issues in haskell, is interfacing with C/C++

to have recvfrom (as an example), you will have those options:

1. define it yourself with something like

```

foreign import "socket.h" c_recvfrom :: CInt-> Ptr a-> CLong-> CInt-> Ptr b-> Ptr c-> IO CInt

recvfrom:: Fd-> IO (SockAddr, ByteString)

recvfrom fd =

  alloca $ \src_sz ->  do

    pending_bytes <- ioctl fd FIONREAD

    buf <- mallocBytes pending_bytes

    src_addr <- malloc

    poke src_sz (sizeOf (undefined::SockAddr))

    ret <- c_recvfrom fd buf pending_bytes src_addr src_sz

    if ret >= 0

    then (peek src_addr, packCStringLen buf pending_bytes)

    else throwIO $ userError "recvfrom failed"

```

seems not difficult, unless you need to define an instance of Storable for SockAddr, for which you should know memory layout of SockAddr, including size, alignment and so on. Fast way, but mastering your own wrapper for GTK or QT is not a good idea.

2. use third-party library, which has all the dirty stuff, but it will add dependencies, which will affect build times, binary size, can grow occupied space due to cross dependencies and it will be pain when you need to cross compile, but, hopefully, it will contain everything you ever need

3. master things like c2hs

I was thinking, that I am struggling with haskell's FFI, until I had to use OCaml's FFI like this:

```

external recvfrom: int-> (sockaddr_t, bytes) = "c_recvfrom"

//caml_stub.c

value c_recvfrom(value _fd){

  CAMLparams1(_fd);

  CAMLlocal2(buf, tuple. sa);

  int ret = 0;

  int fd = 0;

  int buf_sz = 0;

  sockaddr_in src_addr;

  size_t sa_sz = sizeof( src_addr);

  fd = Int_val( _fd);

  ioctl(fd, FIONREAD, &buf_sz);

  buf = malloc( buf_sz);

  ret = recvfrom( Int_val(fd), buf, buf_sz, 0, &src_addr, &sa_sz);

  buf = caml_copy_string( buf, buf_sz);

  sa = caml_alloc_custom( &default_pointers, sizeof(void*), 0, 1);

  tuple = caml_alloc(1, 0);

   Store_field( tuple, 0, sa);

  Store_field( tuple, 1, buf);

  CAMLreturn(tuple);

}

```

so OCaml's FFI is basically untyped C, in which you have to operate with variables of type 'value' and bunch of macroses and hope that you haven't messed up anything.

In this regard, ATS's way of interfacing is like a breath of fresh air for me :)

 

One possibility is to introduce a linear functional API for recvfrom:

absvtype sockaddr

datavtype
recvfrom_vt =
|
recvfrom_fail of ()
|
recvfrom_succ of
{m:nat} (arrpsz(char, m), sockaddr)

fun
ATS_recvfrom
{n:pos}
(sz: size_t(n), flags: int): recvfrom_vt

ATS_recvfrom calls malloc to obtain memory. However, we can differentiate

various malloc calls. For embedded programming, we can implement a malloc

that only allocates from statically allocated memory.

Basically, what I am saying here is that low-level systems programming can be

done in a linear functional style with customized implementations of malloc/free.

Are there any examples of implementations of such custom allocators for ATS?

 

I feel that we are getting very close to this vision :)

Do you mean that you are working on such stuff? Or do you mean, that the progress of recvfrom() implementation is following a route to implement a custom allocator? :) In this case, I will delay it a bit, as my current project has time boundaries.

But overall: the more I dive into ATS the more I like it

[gmhwxi]

>>Do you mean that you are working on such stuff? Or do you mean, that the progress of recvfrom() implementation is following a route to implement a custom allocator? :) In this case, I will delay it a bit, as my current project has time boundaries.

It is just a general comment :)

I did use the Arduino platform for experimenting linear functional programming

in an embedded setting. It was just a proof-of-concept as I did not have enough

time to pursue this idea further.

If you look at a typical embedded program, functions do not perform dynamic

allocations. Most likely, the memory needed during the execution of such a program

is all statically allocated (e.g., by declaring some top-level arrays). This simply means

that we can implement a memory allocator (e.g., one based on the buddy algorithm)

to manage the statically allocated memory and use it for linear functional programming.

In short, with a memory allocator for managing a chunk of statically allocated memory,

we should be able to effectively apply linear functional programing to the construction of

embedded programs.

On Sunday, July 12, 2020 at 2:20:48 PM UTC-4, Dambaev Alexander wrote:

вс, 12 июл. 2020 г. в 15:50, gmhwxi <...>: