Thanks for your answer.
After some retries, I had realized, that the rule of keeping
var-representation type at the exit of function requires me to define most
basic type, so instead of my first try:
```
fn
test1(): $BS.BytestringNSH0 = bs1 where {
var bs = $BS.pack "hello world"
var bs1 = $BS.take( i2sz 11, bs)
val () = $BS.decref_bs( bs, bs1) // consume bs and decref for bs1
}
```
which fails, because bs type at definition is Bytestring(11, 0, 11, 0, 0,
false, l) and should be the same at exit, so I came up to:
```
fn
test1(): $BS.BytestringNSH0 = bs1 where {
var bs: $BS.Bytestring0
val () = bs := $BS.pack "hello world"
var bs1: $BS.Bytestring0
val () = bs1 := $BS.take( i2sz 11, bs)
val () = $BS.decref_bs( bs, bs1) // consume bs and decref for bs1
}
```
which compiles, as both bs and bs1 has types defined as 'Bytestring0?',
which is easier to keep at exit, especially, as ```test1():
$BS.BytestringNSH0 = *bs1* where {``` turns type of bs1 from Bytestring0
into Bytestring0? automatuically.
So my initial issue with var-representation constraint had been solved and
I will stick with style
Thanks!
вс, 4 окт. 2020 г. в 05:10, Hongwei Xi <gmh...@gmail.com>:
> 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
> <https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrOdLXoB2DGa0xdui47Mto13iowECK%2BKem2UjjjwGuv8A%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/CAHjn2KwmgGoOuHZai5K80_nNzPwV2_xjfoqLvChD-yR3hue7fQ%40mail.gmail.com.
