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