Thanks for idea! вс, 19 июл. 2020 г. в 16:11, Hongwei Xi <gmh...@gmail.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. > > > On Sun, Jul 19, 2020 at 10:47 AM Dambaev Alexander <ice.redm...@gmail.com> > wrote: > >> 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 ats-lang-users+unsubscr...@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 >> <https://groups.google.com/d/msgid/ats-lang-users/CAHjn2KzhGehaEwJ1K7h1yA7F_AUgM9yK-DXK8SxKXamN-29hjg%40mail.gmail.com?utm_medium=email&utm_source=footer> >> . >> > -- > 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-users+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLru3AW1TZprvxsaOAFZ%2BN2xQSuYyD6gstTkpi8tTkt8kg%40mail.gmail.com > <https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLru3AW1TZprvxsaOAFZ%2BN2xQSuYyD6gstTkpi8tTkt8kg%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- 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-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAHjn2Kw%3DKsQXLguLu5KkFdf8oO6JuRDrttFrOWaDHBWhKxW0Ag%40mail.gmail.com.
