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/CAHjn2KyTKJDmD9ttGiGJFHNFOr%2BYVRrfxgv6C_NKZcC8QUdHCQ%40mail.gmail.com.
