Hi Alex, Ice,
вт, 29 сент. 2020 г. в 10:52, ice.r...@gmail.com <ice.redm...@gmail.com>:
> I was able to get rid of this error by replacing *reused_l* with *l_ucap
> >= r_len *and* l_ucap < r_len* So constraint solver didn't liked
> introducing reused_l. Is there a proper way to introduce a bool constraint,
> that either true in some case or false otherwise? Something like
> ```
> ...
> [reused_l: bool (l_ucap >= r_len) ]
> ...
> ```
> ?
>
Ice, this is not supported, unfortunately. It's a step in the right
direction, I think. But you could return a boolean with this index in the
proof-part of function return type.
Alex, you could also try encoding this state transition using a dataprop.
You'd require 2 indexes per static variable (one for the value of the
variable at entry into function [append], and another for the value of the
variable after the function [append] exits). You'd have one branch for the
cause of reuse (guarded by l_ucap>=r_len), and another branch for the
opposite case (guarded by the negation, i.e. l_ucap < r_len). That's quite
tedious, and since some variables don't change we don't have to add them to
indexes.
dataprop append_p (
l_len:int, l_offset:int, l_cap:int, l_ucap:int, l_refcnt: int, l_dynamic:
bool, l_p:addr,
r_len:int,
(*rl_ucap:*)int,(*rl_refcnt:*)int,(*len*)int,(*offset:*)int,(*cap:*)int,(*ucap:*)int,(*refcnt:*)int,
(*dynamic:*)bool,(*l:*)addr
) =
| {l_ucap >= r_len}
append_p_reused of (l_len, l_offset, l_cap, l_ucap, l_refcnt, l_dynamic,
l_p, r_len,
0, l_refcnt + 1, l_len + r_len, l_offset, l_cap, l_ucap - r_len, 1,
l_dynamic, l_p)
| {l:addr | l_ucap < r_len; l != l_p}
append_p_fresh of (l_len, l_offset, l_cap, l_ucap, l_refcnt, l_dynamic,
l_p, r_len,
l_ucap, l_refcnt, l_len + r_len, 0, l_len + r_len, 0, 0, true, l)
The type of append then becomes something like this:
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)
):
#[rl_ucap:int; rl_refcnt:int;len:int;offset:int;cap:int; ucap:int;
refcnt:int; dynamic:bool; l:addr] (
append_p (l_len, l_offset, l_cap, l_ucap, l_refcnt, l_dynamic, l_p,
r_len, rl_ucap,rl_refcnt,offset,cap,ucap,refcn, dynamic,l)
| Bytestring_vtype( len, offset, cap, ucap, refcnt, dynamic, l)
)
There might be some bugs here, haven't tested it, but I think this could be
made workable.
> вторник, 29 сентября 2020 г. в 07:02:02 UTC, ice.r...@gmail.com:
>
>> Hi,
>> I am starting to think, that my code's goal is to explore corner cases of
>> type checker :)
>>
>> This time, I have this error:
>> ```
>> /data/devel/ats2/bytestring/DATS/bytestring_flat.dats: 8313(line=299,
>> offs=8) -- 8316(line=299, offs=11): error(3): this constraint cannot be
>> s3exp2icnstr-handled: s3e0 = S3Eerr(S2RTbas(S2RTBASpre(bool)))
>> ```
>> with this code
>> SATS file:
>> ```
>> (* 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]
>> #[rl_ucap: nat | (reused_l && rl_ucap == 0) || (reused_l == false &&
>> rl_ucap == l_ucap)]
>> #[rl_refcnt:nat | (reused_l && rl_refcnt == l_refcnt + 1) || (reused_l
>> == false && rl_refcnt == l_refcnt)]
>> #[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)]
>> #[refcnt:nat | (reused_l && refcnt == 1) || (reused_l == false &&
>> refcnt == 0)]
>> #[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)
>>
>> (* the same as append, but consumes arguments in order to make caller's
>> code clear from bunch of val's and free()
>> *)
>> fn
>> appendC
>> {l_len, l_offset, l_cap, l_ucap: nat}{l_dynamic:bool}{l_p:addr}
>> {r_len, r_offset, r_cap, r_ucap: nat}{r_dynamic:bool}{r_p:addr}
>> ( l: Bytestring_vtype(l_len, l_offset, l_cap, l_ucap, 0, l_dynamic, l_p)
>> , r: Bytestring_vtype(r_len, r_offset, r_cap, r_ucap, 0, 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 &&
>> offset == 0)] [cap:nat | (reused_l && cap == l_cap) || (cap == l_len +
>> r_len)] [ucap:nat | (reused_l && ucap == l_ucap - r_len) || (ucap == 0)]
>> [dynamic:bool | (reused_l && dynamic == l_dynamic) || dynamic == true ]
>> [l:addr | (reused_l && l == l_p) || (reused_l == false && l != l_p) ]*
>> Bytestring_vtype( l_len+r_len, offset, cap, ucap, 0, dynamic, l)
>> ```
>>
>> DATS file:
>> ```
>> implement appendC( l, r) =
>> let
>> val res = append( l, r)
>> val () = free( r)
>> in
>> if isnot_shared res (* bool (refcnt == 0), ie 5's argument of
>> Bytestring_vtype *)
>> * then res where { (*line 299 is here *)*
>> val () = free l
>> }
>> else res where { val () = free( l, res) } (* consumes l, decrease recnt
>> of res *)
>> end
>> ```
>> I assume, that compiler has issues with some of bold constraints of
>> appendC function, but I am not sure as well as I am not sure how to debug
>> it other than changing constraints one by one
>>
> --
> 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/c88cedd9-dadb-43cb-a7d4-19e8e77774ean%40googlegroups.com
> <https://groups.google.com/d/msgid/ats-lang-users/c88cedd9-dadb-43cb-a7d4-19e8e77774ean%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
--
Cheers,
Artyom Shalkhakov
--
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/CAKO6%3Dqgt85c2q0W%3Dws0Y7SW-iCQMyNLCVN%2B3wpxs4TdCjUxAvA%40mail.gmail.com.
