I believe that #[...] must be at the leading position. Please try to change
each [...] to #[...].
On Mon, Sep 28, 2020 at 11:16 PM Dambaev Alexander <ice.redm...@gmail.com>
wrote:
> Hi.
>
> I want to write a spec for a function 'append', which purpose is to append
> content of the second argument into the end of the content of the first one.
> I came to this:
> ```
> (* creates new bytestring with content of r appended to l. does not
> consumes l and r
> in case if 'l' has enough unused capacity to fit 'r', it will copy
> content of 'r' into this unused space, incrementing reference counter of l
> and result
> *)
> fn
> append
> {l_len, l_offset, l_cap, l_ucap, l_refcnt: nat}{l_dynamic:bool}{l_p:addr}
> {r_len, r_offset, r_cap, r_ucap, r_refcnt: nat}{r_dynamic:bool}{r_p:addr}
> ( l: !Bytestring_vtype(l_len, l_offset, l_cap, l_ucap, l_refcnt,
> l_dynamic, l_p) >> Bytestring_vtype( l_len, l_offset, l_cap, *rl_ucap*,
> *rl_refcnt*, l_dynamic, l_p)
> , r: !Bytestring_vtype(r_len, r_offset, r_cap, r_ucap, r_refcnt,
> r_dynamic, r_p)
> ):
> [reused_l: bool | (l_ucap >= r_len && reused_l == true) || reused_l ==
> false]
> [offset:nat | (reused_l && offset == l_offset) || (reused_l == false &&
> offset == 0)]
> [cap:nat | (reused_l && cap == l_cap) || (reused_l == false && cap ==
> l_len + r_len)]
> [ucap:nat | (reused_l && ucap == l_ucap - r_len) || (reused_l == false
> && ucap == 0)]
> *#[rl_ucap: nat | (reused_l && rl_ucap == 0) || (reused_l == false &&
> rl_ucap == l_ucap)]*
> [refcnt:nat | (reused_l && refcnt == l_refcnt + 1) || (reused_l == false
> && refcnt == 0)]
>
> *#[rl_refcnt:nat | (reused_l && rl_refcnt == l_refcnt + 1) || (reused_l ==
> false && rl_refcnt == l_refcnt)]* [dynamic:bool | (reused_l && dynamic
> == l_dynamic) || (reused_l == false && dynamic == true) ]
> [l:addr | (reused_l && l == l_p) || (reused_l == false && l != l_p) ]
> Bytestring_vtype( l_len+r_len, offset, cap, ucap, refcnt, dynamic, l)
> ```
> but compiler says, that I can't do it:
>
> ```
> /data/devel/ats2/bytestring/SATS/bytestring.sats: 6235(line=195, offs=3)
> -- 6765(line=200, offs=72): error(2): incorrect use of the existential
> quantifier #[...]
> /data/devel/ats2/bytestring/SATS/bytestring.sats: 6418(line=197, offs=3)
> -- 6765(line=200, offs=72): error(2): incorrect use of the existential
> quantifier #[...]
> /data/devel/ats2/bytestring/SATS/bytestring.sats: 5764(line=188, offs=129)
> -- 5771(line=188, offs=136): error(2): the static identifier [rl_ucap] is
> unrecognized.
> /data/devel/ats2/bytestring/SATS/bytestring.sats: 5773(line=188, offs=138)
> -- 5782(line=188, offs=147): error(2): the static identifier [rl_refcnt] is
> unrecognized.
> ```
> I guess, that rl_ucap and rl_refcnt have to be actually used in the type
> of the result, right?
>
> --
> 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/CAHjn2KwK0mE2DnApk9vMPkPZHGn3T0ELSyMr9pt4qDYc4hgiAw%40mail.gmail.com
> <https://groups.google.com/d/msgid/ats-lang-users/CAHjn2KwK0mE2DnApk9vMPkPZHGn3T0ELSyMr9pt4qDYc4hgiAw%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/CAPPSPLr70JeoTC6fmesLpgYH1kfPyLA95p36p_XtecVbEijsGQ%40mail.gmail.com.
