By the way, if 'i' is call-by-value, then it cannot be updated. If it needs to be updated, then it cannot be call-by-value.
On Sun, Oct 4, 2020 at 1:01 AM Hongwei Xi <gmh...@gmail.com> wrote: > The following line caused the issue: > > val () = i := build( () | (len, offset, cap, i2sz 0, refcnt + i2sz 1, > dynamic, p)) // restore i > > It should be changed to > > prval () = i := build( () | (len, offset, cap, i2sz 0, refcnt + i2sz 1, > dynamic, p)) // restore i > > Only a linear proof call-by-value argument can be a left-value. So 'i' is > treated as a proof, > and its erasure is of the type 'void'. > > > On Sat, Oct 3, 2020 at 11:32 PM Dambaev Alexander <ice.redm...@gmail.com> > wrote: > >> Hi, >> >> I have a viewtype, defined like this: >> ``` >> absvt0ype >> Bytestring_vtype >> ( len:int (* size in bytes, which occupied by data *) >> , offset: int (* the offset from base pointer at which data of length >> len starts *) >> , cap: int (* capacity of the buffer *) >> , ucap: int (* how much unused bytes of buffer available after this >> bytestring *) >> , refcnt:int (* how many other bytestrings refer to this bytestring *) >> , dynamically_allocated: bool (* if false, then base pointer is >> statically allocated *) >> , base: addr (* base pointer *) >> ) = >> ( void >> | ( size_t (* len *) >> , size_t (* offset *) >> , size_t (* capacity *) >> , size_t (* available capacity *) >> , size_t (* refcnt *) >> , bool (* is dynamically allocated *) >> , ptr >> ) >> ) >> >> (* bytestring, which backend memory is not shared with other bytestrings >> *) >> vtypedef >> BytestringNSH0 = >> [len: nat][offset,cap,ucap:nat][dynamically_allocated:bool][l:agz] >> Bytestring_vtype( len, offset, cap, ucap, 0, dynamically_allocated,l) >> >> ``` >> >> In many functions, I would like to modify argument's type and value in >> order to modify reference count, the simplified example of usage is: >> ``` >> fn >> test1(): $BS.BytestringNSH0 = bs1 where { >> val bs = $BS.pack "hello world" >> val bs1 = $BS.incref_bs bs >> // do some stuff like val bs2 = $BS.take( i2sz 2, bs1)... >> val () = $BS.decref_bs( bs, bs1) // consume bs and decref for bs1 >> } >> ``` >> where incref_bs and decref_bs defined like this: >> ``` >> fn >> decref_bs >> {c_len, c_offset, cap, c_ucap: nat}{dynamic:bool}{l:addr} >> {p_len, p_offset, p_ucap, p_refcnt: nat | *p_refcnt > 0*} >> ( consume: Bytestring_vtype( c_len, c_offset, cap, c_ucap, *1*, >> dynamic, l) // consume bytestring with refcounter = 1 >> , preserve: !Bytestring_vtype( p_len, p_offset, cap, p_ucap, *p_refcnt*, >> dynamic, l) >> Bytestring_vtype( p_len, p_offset, cap, p_ucap, *p_refcnt >> - 1*, dynamic, l) // and decrease refcounter for one, that should be >> preserved >> ):<!wrt> >> void >> fn >> incref_bs >> {len, offset, cap, ucap, refcnt: nat}{dynamic:bool}{l:addr} >> ( i: !Bytestring_vtype( len, offset, cap, ucap, *refcnt*, dynamic, l) >> >> Bytestring_vtype( len, offset, cap, 0, *refcnt + 1*, dynamic, l) // >> increase reference counter on original bytestring >> ):<!wrt> >> Bytestring_vtype( len, offset, cap, ucap, *1*, dynamic, l) // produce >> the same string with refcount == 1 >> ``` >> and the implementation of incref_bs is (decref_bs is similar to it): >> ``` >> implement incref_bs( i) = res where { >> extern castfn >> explode >> { len, offset, cap, ucap, refcnt:nat}{dynamic:bool}{l:addr} >> ( i: Bytestring_vtype( len, offset, cap, ucap, refcnt, dynamic, l) >> ):<> ( size_t(len), size_t(offset), size_t(cap), size_t(ucap), >> size_t(refcnt), bool(dynamic) ptr(l)) >> extern castfn >> build >> { len, offset, cap, ucap, refcnt:nat}{dynamic:bool}{l:addr} >> ( void >> | ( size_t(len), size_t(offset), size_t(cap), size_t(ucap), >> size_t(refcnt), bool(dynamic), ptr(l) ) >> ):<> Bytestring_vtype( len, offset, cap, ucap, refcnt, dynamic, l) >> val (len, offset, cap, ucap, refcnt, dynamic, p) = explode(i) // >> consume i >> val res = build( () | (len, offset, cap, ucap, i2sz 1, dynamic, p)) >> val () = i := build( () | (len, offset, cap, i2sz 0, refcnt + i2sz 1, >> dynamic, p)) // restore i >> } >> ``` >> this implementation typechecks, but C's generated code can't be compiled >> with error: >> ``` >> >> /nix/store/cqynqsas6nwk3gbn8m2pi9lx4m0shr0y-ats2-0.3.13/lib/ats2-postiats-0.3.13/ccomp/runtime/pats_ccomp_instrset.h:339:39:* >> error: invalid use of void expression* >> #define ATSINSstore(pmv1, pmv2) (pmv1 = pmv2) >> ^ >> bytestring_flat_dats.c:5417:1: note: in expansion of macro ‘ATSINSstore’ >> ATSINSstore(ATSderef(arg0, atsvoid_t0ype), ATSPMVcastfn(build, >> postiats_tyrec_0, tmp311)) ; >> ``` >> and the generated code for incref_bs is: >> ``` >> /* >> local: >> global: incref_bs$80$0(level=0) >> local: >> global: >> */ >> ATSextern() >> postiats_tyrec_0 >> bytestring__incref_bs(*atsrefarg0_type*(postiats_tyrec_0) arg0) >> { >> /* tmpvardeclst(beg) */ >> ATStmpdec(tmpret301, postiats_tyrec_0) ; >> ATStmpdec(tmp302, atstkind_t0ype(atstype_size)) ; >> ATStmpdec(tmp303, atstkind_t0ype(atstype_size)) ; >> ATStmpdec(tmp304, atstkind_t0ype(atstype_size)) ; >> ATStmpdec(tmp305, atstkind_t0ype(atstype_size)) ; >> ATStmpdec(tmp306, atstkind_t0ype(atstype_size)) ; >> ATStmpdec(tmp307, atstkind_t0ype(atstype_bool)) ; >> ATStmpdec(tmp308, atstkind_type(atstype_ptrk)) ; >> ATStmpdec(tmp309, postiats_tyrec_0) ; >> ATStmpdec(tmp310, atstkind_t0ype(atstype_size)) ; >> ATStmpdec(tmp311, postiats_tyrec_0) ; >> ATStmpdec(tmp312, atstkind_t0ype(atstype_size)) ; >> ATStmpdec(tmp313, atstkind_t0ype(atstype_size)) ; >> ATStmpdec(tmp314, atstkind_t0ype(atstype_size)) ; >> /* tmpvardeclst(end) */ >> ATSfunbody_beg() >> ATSINSflab(__patsflab_incref_bs): >> ATSINSmove(tmp302, ATSSELfltrec(ATSPMVcastfn(explode, postiats_tyrec_0, >> arg0), postiats_tyrec_0, atslab__0)) ; >> ATSINSmove(tmp303, ATSSELfltrec(ATSPMVcastfn(explode, postiats_tyrec_0, >> arg0), postiats_tyrec_0, atslab__1)) ; >> ATSINSmove(tmp304, ATSSELfltrec(ATSPMVcastfn(explode, postiats_tyrec_0, >> arg0), postiats_tyrec_0, atslab__2)) ; >> ATSINSmove(tmp305, ATSSELfltrec(ATSPMVcastfn(explode, postiats_tyrec_0, >> arg0), postiats_tyrec_0, atslab__3)) ; >> ATSINSmove(tmp306, ATSSELfltrec(ATSPMVcastfn(explode, postiats_tyrec_0, >> arg0), postiats_tyrec_0, atslab__4)) ; >> ATSINSmove(tmp307, ATSSELfltrec(ATSPMVcastfn(explode, postiats_tyrec_0, >> arg0), postiats_tyrec_0, atslab__5)) ; >> ATSINSmove(tmp308, ATSSELfltrec(ATSPMVcastfn(explode, postiats_tyrec_0, >> arg0), postiats_tyrec_0, atslab__6)) ; >> ATSINSmove(tmp310, atspre_g1int2uint_int_size(ATSPMVi0nt(1))) ; >> ATSINSmove_fltrec_beg() >> ATSINSstore_fltrec_ofs(tmp309, postiats_tyrec_0, atslab__0, tmp302) ; >> ATSINSstore_fltrec_ofs(tmp309, postiats_tyrec_0, atslab__1, tmp303) ; >> ATSINSstore_fltrec_ofs(tmp309, postiats_tyrec_0, atslab__2, tmp304) ; >> ATSINSstore_fltrec_ofs(tmp309, postiats_tyrec_0, atslab__3, tmp305) ; >> ATSINSstore_fltrec_ofs(tmp309, postiats_tyrec_0, atslab__4, tmp310) ; >> ATSINSstore_fltrec_ofs(tmp309, postiats_tyrec_0, atslab__5, tmp307) ; >> ATSINSstore_fltrec_ofs(tmp309, postiats_tyrec_0, atslab__6, tmp308) ; >> ATSINSmove_fltrec_end() >> ATSINSmove(tmp312, atspre_g1int2uint_int_size(ATSPMVi0nt(0))) ; >> >> ATSINSmove(tmp314, atspre_g1int2uint_int_size(ATSPMVi0nt(1))) ; >> >> ATSINSmove(tmp313, atspre_g1uint_add_size(tmp306, tmp314)) ; >> >> ATSINSmove_fltrec_beg() >> ATSINSstore_fltrec_ofs(tmp311, postiats_tyrec_0, atslab__0, tmp302) ; >> ATSINSstore_fltrec_ofs(tmp311, postiats_tyrec_0, atslab__1, tmp303) ; >> ATSINSstore_fltrec_ofs(tmp311, postiats_tyrec_0, atslab__2, tmp304) ; >> ATSINSstore_fltrec_ofs(tmp311, postiats_tyrec_0, atslab__3, tmp312) ; >> ATSINSstore_fltrec_ofs(tmp311, postiats_tyrec_0, atslab__4, tmp313) ; >> ATSINSstore_fltrec_ofs(tmp311, postiats_tyrec_0, atslab__5, tmp307) ; >> ATSINSstore_fltrec_ofs(tmp311, postiats_tyrec_0, atslab__6, tmp308) ; >> ATSINSmove_fltrec_end() >> *ATSINSstore(ATSderef(arg0, atsvoid_t0ype), ATSPMVcastfn(build, >> postiats_tyrec_0, tmp311)) ;* >> ``` >> So, althought, 'build' has the same return type as arg0, I assume, that >> compiler generates type 'void' for arg0 because it had been consumed during >> call to 'explode'. >> >> So the question is: is there a way to overcome this issue? >> >> There are alternative ways exist: >> 1. 'explode' should not consume, but preserve it's argument. In this >> case, type checker will complain, that ```val () = i := build( () | (len, >> offset, cap, i2sz 0, refcnt + i2sz 1, dynamic, p)) // restore i``` will >> loose linear component of the original value of i >> 2. use variables for arguments of incref_bs and decref_bs, like this: >> ``` >> fn >> incref_bs >> {len, offset, cap, ucap, refcnt: nat}{dynamic:bool}{l:addr} >> ( i: *&*Bytestring_vtype( len, offset, cap, ucap, *refcnt*, dynamic, >> l) >> Bytestring_vtype( len, offset, cap, 0, *refcnt + 1*, dynamic, l) >> // increase reference counter on original bytestring >> ):<!wrt> >> Bytestring_vtype( len, offset, cap, ucap, *1*, dynamic, l) // produce >> the same string with refcount == 1 >> ``` >> but in this case, test1() won't compile. because of the requirement to >> restore type of var, passed to incref_bs >> 1. consume arguments of incref_bs and decref_bs and return tuples, like >> this >> ``` >> fn >> incref_bs >> {len, offset, cap, ucap, refcnt: nat}{dynamic:bool}{l:addr} >> ( i: Bytestring_vtype( len, offset, cap, ucap, *refcnt*, dynamic, l) >> ):<!wrt> >> ( Bytestring_vtype( len, offset, cap, 0, *refcnt + 1*, dynamic, l) // >> increase reference counter on original bytestring >> , Bytestring_vtype( len, offset, cap, ucap, *1*, dynamic, l) // >> produce the same string with refcount == 1 >> ) >> ``` >> but this is much verbose and require tracking of resource names manually >> in order to not to mess things up. >> >> -- >> 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/CAHjn2Ky2gr53BoRhEO50XXX9DQTw2Evees%3DmtQMS%2BosghcDNdw%40mail.gmail.com >> <https://groups.google.com/d/msgid/ats-lang-users/CAHjn2Ky2gr53BoRhEO50XXX9DQTw2Evees%3DmtQMS%2BosghcDNdw%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/CAPPSPLrOdLXoB2DGa0xdui47Mto13iowECK%2BKem2UjjjwGuv8A%40mail.gmail.com.