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.
