unboxed datatypes

Dambaev Alexander

unread,

Jul 18, 2020, 2:17:57 AM7/18/20

to ats-lan...@googlegroups.com

Hi,

datatypes/datavtypes are heap-allocated, which runtime representation, I guess, is a tag and a pointer to data.

ATS has unboxed tuples and unboxed records, which runtime representation, I guess, are C's structs

Is there a way to define a stack allocated datatype?

I think, we can have them by using C's union types for runtime representation. Am I missing something?

Artyom Shalkhakov

unread,

Jul 18, 2020, 2:21:35 AM7/18/20

to ats-lang-users

Hi Alex,

сб, 18 июл. 2020 г. в 09:17, Dambaev Alexander <ice.r...@gmail.com>:

This is not supported at the moment.

I too think it would be a great addition!

--
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 view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAHjn2KzsFUPptwSPgTrWVR%3DsoA42aSEmUXv4D-MAQAR_K8f%2BKw%40mail.gmail.com.

--

Cheers,
Artyom Shalkhakov

Dambaev Alexander

unread,

Jul 18, 2020, 9:18:03 AM7/18/20

to ats-lan...@googlegroups.com

Well, let's hope, that ATS3 will have such feature

сб, 18 июл. 2020 г. в 06:21, Artyom Shalkhakov <artyom.s...@gmail.com>:

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAKO6%3DqggX%3DPE0-0FidevEnemk3JUYY6LGGD5zN5FidKNNG2Jsw%40mail.gmail.com.

Dambaev Alexander

unread,

Jul 19, 2020, 10:47:26 AM7/19/20

to ats-lan...@googlegroups.com

So I have tried to use views to replace datatypes. My idea was to pass a variable's view and address, change it's view and write different tuples at it's address (because tuples are unboxed):

```

viewdef req_v_tx_ack_v(l1: addr) = int @ l1
viewdef req_v_push_data_v(l1: addr) = (int, bool) @ l1

dataview gw_ns_request_v1_v(int, l1:addr) =
| req_v_tx_ack(0, l1) of req_v_tx_ack_v(l1)
| req_v_push_data(1, l1) of req_v_push_data_v(l1)

(* axioms to revert variable's type to original *)

extern praxi tx_ack2result
{l1:agz}{n1:pos}
( pf: !req_v_tx_ack_v(l1) >> array_v(char?, l1, n1)
): void
extern praxi push_data2result
{l1:agz}{n1:pos}
( pf: !req_v_push_data_v(l1) >> array_v(char?, l1, n1)
): void

dataview
result_vb
( bool, a:view+, b:view+) =
| result_vb_succ(true, a, b) of a
| result_vb_fail(false, a, b) of b

fn parse_request
{l1:agz}{n1:pos}
( result_pf: !array_v(char?, l1, n1) >> result_vb( tag >= 0
, gw_ns_request_v1_v( tag, l1)
, array_v(char?, l1, n1)
)
| flag: int
, result: ptr l1
): #[tag: int ] int(tag) =
case+ flag of
| 0 => 0 where {                       (* 1 *)
extern praxi result2tx_ack
{l1:agz}{n1:pos}
( pf: !array_v(char?, l1, n1) >> req_v_tx_ack_v(l1)
): void
prval () = result2tx_ack( result_pf)
val () = !result := 0
prval ret_pf = req_v_tx_ack( result_pf)
prval () = result_pf := result_vb_succ( ret_pf)
}
| 1 => 1 where {     (* 2 *)
extern praxi result2push_data
{l1:agz}{n1:pos}
( pf: !array_v(char?, l1, n1) >> req_v_push_data_v(l1)
): void
prval () = result2push_data( result_pf)
val () = !result := (0,false)
prval ret_pf = req_v_push_data( result_pf)
prval () = result_pf := result_vb_succ( ret_pf)
}
| _ => ~1 where {
prval ret_pf = result_pf
prval () = result_pf := result_vb_fail(ret_pf)
}

fn test4(): void = {
var result: @[char][1] with result_pf             (* 3 *)
var raw = addr@result (* we need ptr l ,where l == addr@result, otherwise *)
val s = parse_request( result_pf | 1, addr@result)
val () = case- s of
| 0 => () where {               (* 4 *)
prval result_vb_succ(ret_pf) = result_pf
prval req_v_tx_ack( value_pf) = ret_pf
prval () = result_pf := value_pf
val token = !raw (* here we read a tuple from result's address *)
val () = assertloc( raw = addr@result)
val () = assertloc( token = 0x0000)
(* restore types *)
prval () = tx_ack2result( result_pf)
prval () = result_pf := array_v_unnil_nz( result_pf)
}
| 1 => () where { (* 5 *)
prval result_vb_succ(ret_pf) = result_pf
prval req_v_push_data( value_pf) = ret_pf
prval () = result_pf := value_pf
val (i:int,b:bool) = !raw (* here we read a tuple from result's address *)
val () = assertloc( raw = addr@result)
val () = assertloc( i = 0)
val () = assertloc( b = false)
(* restore types *)
prval () = push_data2result( result_pf)
prval () = result_pf := array_v_unnil_nz( result_pf)
}

| _ when s < 0 => () where {
prval result_vb_fail(ret_pf) = result_pf
prval () = result_pf := array_v_unnil_nz(ret_pf)
}
}

```

And this compile, runs and valgrind and gdb has no issues. But there are catchs:

1. If I will messup int values in marks (comments) 1 and 2, then type checker will complain (as expected), but at the same time, I can replace values at marks 4 and 5 with any random integers and type checker will be fine with it;

2. if you notice at mark 5, result buffer is of size 1*sizeof(char), but program stores int and (int,int) values into it, which are bigger that char. At the same time, gdb and valgrind do not report any issues and I haven't checked generated code to see if it corrupts memory.

I guess, I can solve issue #1 by introducing a new sort, but I need a way to map sort->int values (and maybe vice verse)

Hongwei Xi

unread,

Jul 19, 2020, 12:11:06 PM7/19/20

to ats-lan...@googlegroups.com

Here is a little doc on manually constructing values of a datatype:

http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x2223.html

If you have a constructor of the name foo, then a type 'foo_pstruct' is automatically introduced

(in the same namespace). You can study the generated C code to figure out the related details.

--
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 view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAHjn2KzhGehaEwJ1K7h1yA7F_AUgM9yK-DXK8SxKXamN-29hjg%40mail.gmail.com.

Dambaev Alexander

unread,

Jul 19, 2020, 12:26:57 PM7/19/20

to ats-lan...@googlegroups.com

Thanks for idea!

вс, 19 июл. 2020 г. в 16:11, Hongwei Xi <gmh...@gmail.com>:

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLru3AW1TZprvxsaOAFZ%2BN2xQSuYyD6gstTkpi8tTkt8kg%40mail.gmail.com.

Artyom Shalkhakov

unread,

Jul 19, 2020, 2:50:21 PM7/19/20

to ats-lang-users

Hi Alex,

вс, 19 июл. 2020 г. в 17:47, Dambaev Alexander <ice.r...@gmail.com>:

Yes, you can use your own type coercions but then you will have to trust them.

If you use your own coercions, then you will have to reason about the size of the union of the two records that you have (the [n1] variable in [parse_request]), which is burdensome because it is not supported.

In your axioms, you want something like "array of bytes of length n which is the size of union of type A and type B". In your case, type A is int, type B is (int, bool), and n = sizeof(union(A,B)).

If we had something like a "union" type constructor, that would have probably made things easier for you. As I understand it, unions are unsupported because adding them is complex and not very useful, although I hope Hongwei will reconsider this at some point, in addition to flat array types. :-)

I guess, I can solve issue #1 by introducing a new sort, but I need a way to map sort->int values (and maybe vice verse)

--
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 view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAHjn2KzhGehaEwJ1K7h1yA7F_AUgM9yK-DXK8SxKXamN-29hjg%40mail.gmail.com.

--

Cheers,
Artyom Shalkhakov

Dambaev Alexander

unread,

Jul 20, 2020, 7:02:06 AM7/20/20

to ats-lan...@googlegroups.com

Hi,

I have tried to manually create datatype constructors, but such way lacks type checking completely as it consist from many unsafe casts.

I had tuned my previous example with tuples of different sizes a little bit to get a more or less type safe version:

```

typedef gw_ns_request_v1_max_t = (int, int, int) (* you have to be sure, that this is the biggest type from all constructors *)
#define gw_ns_request_v1_max_tag 2 (* do not forget to update if dataview will have more contructors *)
dataview gw_ns_request_v1_v(i:int, l:addr) =
| {i:nat | i < 0 || i > gw_ns_request_v1_max_tag }
invalid(i,l) of void (* you have to be sure, that i > maximum tag *)
| tx_ack( gw_ns_request_v1_max_tag, l) of (int @ l )
| push_data(0, l) of ((int,bool) @ l)
| pull_data(1, l) of (gw_ns_request_v1_max_t @ l)

(* this axiom restores type *)
extern
praxi
gw_ns_request_v1_result_clear
{a:t0ype}{l:agz}
( pf: a @ l
): gw_ns_request_v1_max_t @ l
fn parse_request
{l:agz}
( result_pf: !gw_ns_request_v1_max_t? @ l >> result_vb( tag >= 0
, gw_ns_request_v1_v(tag,l)
, gw_ns_request_v1_max_t? @ l

)
| flag: int
, result: ptr l

): #[tag: int | tag <= gw_ns_request_v1_max_tag] int(tag) = (* strange, but caller's case+ will not know, that tag <= gw_ns_request_v1_max_tag *)
case+ flag of
| 0 => 0 (* if I will change 0 with other, push_data will not be accepted *) where {
extern praxi result2push_data( pf: !gw_ns_request_v1_max_t? @ l >> (int,bool) @ l):void
prval () = result2push_data(result_pf)
val () = !result := (1,true)
prval () = result_pf := result_vb_succ( push_data( result_pf)) (* push_data is only accepted with result value 0 *)
}
| 1 => 1 where {
extern praxi result2pull_data( pf: !gw_ns_request_v1_max_t? @ l >> (int,int,int) @ l):void
prval () = result2pull_data(result_pf)
val () = !result := (1,2,3)
prval () = result_pf := result_vb_succ( pull_data( result_pf))
}
| 2 => 2 where {
extern praxi result2tx_ack( pf: !gw_ns_request_v1_max_t? @ l >> int @ l):void
prval () = result2tx_ack(result_pf)

val () = !result := 0

prval () = result_pf := result_vb_succ( tx_ack( result_pf))
}

| _ => ~1 where {
prval tmp = result_pf
prval () = result_pf := result_vb_fail( tmp)
}

fn test4(): void = {
var result: gw_ns_request_v1_max_t with result_pf (* you need to use the constructor of maximum size to not to corrupt memory *)
var raw = addr@result (* we need raw to read from it a values of different types. reading them from result directly will cause gcc to fail *)
val s = parse_request( result_pf | 2, addr@result)
val () = case- s of (* strange, but case+ will fail, because it does not remember, that 'tag <= gw_ns_request_v1_max_tag' *)
| 0 => {(* if we will replace 0 say with 10, then later, typechecker will ask to match tmp with invalid() *)
prval result_vb_succ(push_data(pf)) = result_pf
val (i,b) = !raw (* can't read from result directly, as it is of type struct gw_ns_request_v1_max_t in generated C code *)
val () = assertloc( i = 1)
val () = assertloc( b = true)
prval () = result_pf := gw_ns_request_v1_result_clear( pf) (* quite ugly, restore original type of result *)
}
| 1 => { (* if we will replace 1 with say 0, then compiler will not match with pull_data() *)
prval result_vb_succ(pull_data(pf)) = result_pf
val (i1, i2, i3) = !raw
val () = assertloc( i1 = 1 && i2 = 2 && i3 = 3)
prval () = result_pf := gw_ns_request_v1_result_clear( pf)
}
| 2 => { prval result_vb_succ(tx_ack(pf)) = result_pf
val () = assertloc( !raw = 0)
prval () = result_pf := gw_ns_request_v1_result_clear( pf)
}
| _ when s < 0 => { prval result_vb_fail(pf) = result_pf
prval () = result_pf := gw_ns_request_v1_result_clear( pf)
}
}

```

Although, I am quite satisfied with this version (well, it does not require custom allocator), it is still interesting why the caller of parse_request doesn't know about #[tag: int | tag <= gw_ns_request_v1_max_tag] constraint, so case+ will ask for more clauses. I know, that I could use intLte(gw_ns_request_v1_max_tag) type, but I need to something like g1intLte(tag, gw_ns_request_v1_max_tag), but this doesn't type checks. Any ideas how to solve this?

Lot more verbose than just using datavtypes, but I haven't investigated a topic of custom allocator for ATS, but I guess, it is much harder

Artyom Shalkhakov

unread,

Jul 20, 2020, 2:21:13 PM7/20/20

to ats-lang-users

пн, 20 июл. 2020 г. в 14:02, Dambaev Alexander <ice.r...@gmail.com>:

Hi,
I have tried to manually create datatype constructors, but such way lacks type checking completely as it consist from many unsafe casts.

Precisely. It will work but requires a lot of casting and sweating.

I had tuned my previous example with tuples of different sizes a little bit to get a more or less type safe version:

```
typedef gw_ns_request_v1_max_t = (int, int, int) (* you have to be sure, that this is the biggest type from all constructors *)
#define gw_ns_request_v1_max_tag 2 (* do not forget to update if dataview will have more contructors *)
dataview gw_ns_request_v1_v(i:int, l:addr) =
| {i:nat | i < 0 || i > gw_ns_request_v1_max_tag }
invalid(i,l) of void (* you have to be sure, that i > maximum tag *)
| tx_ack( gw_ns_request_v1_max_tag, l) of (int @ l )
| push_data(0, l) of ((int,bool) @ l)
| pull_data(1, l) of (gw_ns_request_v1_max_t @ l)

As an aside, this seems like a place to create a function that maps a tag into a type. Not sure how I would write that in ATS though.

(* this axiom restores type *)
extern
praxi
gw_ns_request_v1_result_clear
{a:t0ype}{l:agz}
( pf: a @ l
): gw_ns_request_v1_max_t @ l
fn parse_request
{l:agz}
( result_pf: !gw_ns_request_v1_max_t? @ l >> result_vb( tag >= 0
, gw_ns_request_v1_v(tag,l)
, gw_ns_request_v1_max_t? @ l
)
| flag: int
, result: ptr l
): #[tag: int | tag <= gw_ns_request_v1_max_tag] int(tag) = (* strange, but caller's case+ will not know, that tag <= gw_ns_request_v1_max_tag *)

That's right, caller will not know this. This could be mitigated with an axiom like this:

extern

prfun gw_ns_request_tag_max {tag:int} {l:addr} (!gw_ns_request_v1_v(tag,l)):<> [tag>=0; tag <= gw_ns_request_v1_max_tag] void

The caller would then know, if they have gw_ns_request_v1_v, then the above axiom can be used to establish what the tag can be.

--

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 view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAHjn2KxB1YNKbcpf_m_C8ZTOojiz-y5ae4DAyY3E4L370yPeyQ%40mail.gmail.com.