Why my code occurs `unsolved constraint` error?
111 views
Skip to first unread message
Kiwamu Okabe
Oct 29, 2018, 2:52:33 AM10/29/18
to ats-lan...@googlegroups.com
Dear all,
Why following code occurs `unsolved constraint` error?
https://github.com/metasepi/uemacs-bohai/blob/8b2b657c829be1025433f3083aa5cf3b1d040cb6/DATS/utf8.dats#L60
```
$ vi DATS/utf8.dats
--snip--
implement utf8_to_unicode (pf | line, index, len, res) = bytes where {
fun loop1 (c: char, mask: uint, bytes: uint): (uint, uint) =
if ((($UN.cast{uint}{char} c) land mask) != 0U)
then loop1 (c, mask >> 1, bytes + 1U)
else (mask, bytes)
fun loop2 {m:nat} (line: !strnptr(m), i: int, len: int(m), bytes:
uint, value: uint): uint =
undefined()
val c = line[index]
val () = !res := $UN.cast{unicode_t}{char} line[index]
(*
* 0xxxxxxx is valid utf8
* 10xxxxxx is invalid UTF-8, we assume it is Latin1
*)
val bytes = if (c < $UN.cast{char}{int} 0xc0)
then 1U
else bytes' where {
(* Ok, it's 11xxxxxx, do a stupid decode *)
val (mask, bytes'') = loop1 (c, 0x20U, 0x2U)
(* Invalid? Do it as a single byte Latin1 *)
val bytes' = if (bytes'' > 6 || bytes'' > len)
then 1U
else bytes'' where {
(* Ok, do the bytes *)
val value = loop2 (line, 1, len, bytes'',
($UN.cast{uint}{char} c) land (mask - 1U))
val () = !res := $UN.cast{unicode_t}{uint} value
}
}
}
--snip--
$ pwd
/home/kiwamu/src/uemacs-bohai
$ make
ATS utf8.dats.c
/home/kiwamu/src/uemacs-bohai/DATS/utf8.dats: 929(line=23, offs=58) --
934(line=23, offs=63): error(3): unsolved constraint:
C3NSTRprop(C3TKmain(); S2Eeqeq(S2Evar(l$8600$8666(14318));
S2Evar(l$8600$8601(14253))))
/home/kiwamu/src/uemacs-bohai/DATS/utf8.dats: 929(line=23, offs=58) --
934(line=23, offs=63): error(3): unsolved constraint for var
preservation
typechecking has failed: there are some unsolved constraints: please
inspect the above reported error message(s) for information.
exit(ATS): uncaught exception:
_2home_2kiwamu_2src_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
make: *** [Makefile:75: utf8.dats.c] Error 1
```
Best regards,
--
Kiwamu Okabe at METASEPI DESIGN
Why following code occurs `unsolved constraint` error?
https://github.com/metasepi/uemacs-bohai/blob/8b2b657c829be1025433f3083aa5cf3b1d040cb6/DATS/utf8.dats#L60
```
$ vi DATS/utf8.dats
--snip--
implement utf8_to_unicode (pf | line, index, len, res) = bytes where {
fun loop1 (c: char, mask: uint, bytes: uint): (uint, uint) =
if ((($UN.cast{uint}{char} c) land mask) != 0U)
then loop1 (c, mask >> 1, bytes + 1U)
else (mask, bytes)
fun loop2 {m:nat} (line: !strnptr(m), i: int, len: int(m), bytes:
uint, value: uint): uint =
undefined()
val c = line[index]
val () = !res := $UN.cast{unicode_t}{char} line[index]
(*
* 0xxxxxxx is valid utf8
* 10xxxxxx is invalid UTF-8, we assume it is Latin1
*)
val bytes = if (c < $UN.cast{char}{int} 0xc0)
then 1U
else bytes' where {
(* Ok, it's 11xxxxxx, do a stupid decode *)
val (mask, bytes'') = loop1 (c, 0x20U, 0x2U)
(* Invalid? Do it as a single byte Latin1 *)
val bytes' = if (bytes'' > 6 || bytes'' > len)
then 1U
else bytes'' where {
(* Ok, do the bytes *)
val value = loop2 (line, 1, len, bytes'',
($UN.cast{uint}{char} c) land (mask - 1U))
val () = !res := $UN.cast{unicode_t}{uint} value
}
}
}
--snip--
$ pwd
/home/kiwamu/src/uemacs-bohai
$ make
ATS utf8.dats.c
/home/kiwamu/src/uemacs-bohai/DATS/utf8.dats: 929(line=23, offs=58) --
934(line=23, offs=63): error(3): unsolved constraint:
C3NSTRprop(C3TKmain(); S2Eeqeq(S2Evar(l$8600$8666(14318));
S2Evar(l$8600$8601(14253))))
/home/kiwamu/src/uemacs-bohai/DATS/utf8.dats: 929(line=23, offs=58) --
934(line=23, offs=63): error(3): unsolved constraint for var
preservation
typechecking has failed: there are some unsolved constraints: please
inspect the above reported error message(s) for information.
exit(ATS): uncaught exception:
_2home_2kiwamu_2src_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
make: *** [Makefile:75: utf8.dats.c] Error 1
```
Best regards,
--
Kiwamu Okabe at METASEPI DESIGN
Artyom Shalkhakov
Oct 29, 2018, 4:17:40 AM10/29/18
to ats-lang-users
Hi Kiwamu,
While I'm not sure why your code fails, it's an interesting project you've started. Please don't hesitate telling us more about it!
Actually, I have an idea about your code. You may have to an annotation like if :( line: strnptr(m) ) => .. then ... else ... onto your conditionals.
Hongwei Xi
Oct 29, 2018, 8:14:17 AM10/29/18
to ats-lan...@googlegroups.com
I tried and there was no problem. I used ATS2-0.3.12.
--
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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6d%3DWqC8ym8KArMBvwOYi8tBqZAMJ_WwfXp0h9AgBkcO2Lw%40mail.gmail.com.
Hongwei Xi
Oct 29, 2018, 8:19:47 AM10/29/18
to ats-lan...@googlegroups.com
Forgot to uncomment.
Artyom is right. You could write the code as follows
(so as to avoid the need for type annotation):
implement utf8_to_unicode (pf | line, index, len, res) =
let
fun loop1 (c: char, mask: uint, bytes: uint): (uint, uint) =
if ((($UN.cast{uint}{char} c) land mask) != 0U)
then loop1 (c, mask >> 1, bytes + 1U)
else (mask, bytes)
fun loop2 {m:nat} (line: !strnptr(m), i: int, len: int(m), bytes: uint, value: uint): uint =
undefined()
(* (* xxx TODO: Should implement following: *)
for (i = 1; i < bytes; i++) {
c = line[i];
if ((c & 0xc0) != 0x80)
return 1;
value = (value << 6) | (c & 0x3f);
}
*)
for (i = 1; i < bytes; i++) {
c = line[i];
if ((c & 0xc0) != 0x80)
return 1;
value = (value << 6) | (c & 0x3f);
}
*)
val c = line[index]
val () = !res := $UN.cast{unicode_t}{char} line[index]
(*
* 0xxxxxxx is valid utf8
* 10xxxxxx is invalid UTF-8, we assume it is Latin1
*)
in
if (c < $UN.cast{char}{int} 0xc0)
then 1U
else bytes' where {
(* Ok, it's 11xxxxxx, do a stupid decode *)
val (mask, bytes'') = loop1 (c, 0x20U, 0x2U)
(* Invalid? Do it as a single byte Latin1 *)
val bytes' = if (bytes'' > 6 || bytes'' > len)
then 1U
else bytes'' where {
(* Ok, do the bytes *)
val value = ($UN.cast{uint}{char} c) land (mask - 1U) // xxx TODO
val value = loop2 (line, 1, len, bytes'',
($UN.cast{uint}{char} c) land (mask - 1U))
val () = !res := $UN.cast{unicode_t}{uint} value
}
}
end
Kiwamu Okabe
Nov 1, 2018, 4:00:57 AM11/1/18
to ats-lan...@googlegroups.com
Dear Artyom and Hongwei,
sorry for my late reply.
On Mon, Oct 29, 2018 at 5:17 PM Artyom Shalkhakov
<artyom.s...@gmail.com> wrote:
> While I'm not sure why your code fails, it's an interesting project you've started.
Thanks. It's very fun and good exercise for me.
> Actually, I have an idea about your code. You may have to an annotation like...
Thanks for your advice. But it's not clear for me...
> if :( line: strnptr(m) ) => .. then ... else ... onto your conditionals.
Where line of my code should follow your advice?
https://github.com/metasepi/uemacs-bohai/blob/9ecdd06fe09e6433ed0fb4271c0e5b44d2ad8f8d/DATS/utf8.dats
sorry for my late reply.
On Mon, Oct 29, 2018 at 5:17 PM Artyom Shalkhakov
<artyom.s...@gmail.com> wrote:
> While I'm not sure why your code fails, it's an interesting project you've started.
> Actually, I have an idea about your code. You may have to an annotation like...
Thanks for your advice. But it's not clear for me...
> if :( line: strnptr(m) ) => .. then ... else ... onto your conditionals.
https://github.com/metasepi/uemacs-bohai/blob/9ecdd06fe09e6433ed0fb4271c0e5b44d2ad8f8d/DATS/utf8.dats
Artyom Shalkhakov
Nov 1, 2018, 4:12:58 AM11/1/18
to ats-lan...@googlegroups.com
You should put at at every branch (so on every [if] and on every [case]). That's because the variable [line] is of linear type, and the annotation basically says that in every alternative of the branch it's going to be preserved (so, after the evaluation of an [if] or a [case] the type of [line] is going to still be [strnptr(m)]). I think the reason for having to annotate it is due to a hit on performance in constraint solving. I think I read about this in one of HX's papers.
I think in your case, you'll have to annotate two [if]s:
Could you try it? You could also try to annotate only one [if] to find a minimal required annotation that keeps the typechecker silent. :-)
Best regards,
--
Kiwamu Okabe at METASEPI DESIGN
--
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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6d%3Dsb8%3DkqyLc0j3bipb16_zp26FsdZ%3DfD5Q0g5k7f9ZM3g%40mail.gmail.com.
--
Cheers,
Artyom Shalkhakov
Artyom Shalkhakov
Kiwamu Okabe
Nov 1, 2018, 10:30:58 PM11/1/18
to ats-lan...@googlegroups.com
Dear Artyom,
thanks for your kind reply.
On Thu, Nov 1, 2018 at 5:12 PM Artyom Shalkhakov
<artyom.s...@gmail.com> wrote:
> You should put at at every branch (so on every [if] and on every [case]). That's because the
> variable [line] is of linear type, and the annotation basically says that in every alternative of
> the branch it's going to be preserved (so, after the evaluation of an [if] or a [case] the type of
> [line] is going to still be [strnptr(m)]). I think the reason for having to annotate it is due to a hit
> on performance in constraint solving. I think I read about this in one of HX's papers.
>
> I think in your case, you'll have to annotate two [if]s:
>
> https://github.com/metasepi/uemacs-bohai/blob/9ecdd06fe09e6433ed0fb4271c0e5b44d2ad8f8d/DATS/utf8.dats#L48
> https://github.com/metasepi/uemacs-bohai/blob/9ecdd06fe09e6433ed0fb4271c0e5b44d2ad8f8d/DATS/utf8.dats#L55
>
> Could you try it? You could also try to annotate only one [if] to find a minimal required annotation that keeps the typechecker silent. :-)
Sorry. I think it doesn't make sense...
I have an stupid question. I wrote following code:
```
val bytes = if ($UN.cast{int}{char} c < 0xc0):( line: strnptr(m) )
But above causes following errors:
```
$ make
ATS utf8.dats.c
/home/kiwamu/src/uemacs-bohai/DATS/utf8.dats: 1645(line=48, offs=57)
-- 1654(line=48, offs=66): error(2): sort application is not
supported.
/home/kiwamu/src/uemacs-bohai/DATS/utf8.dats: 1639(line=48, offs=51)
-- 1643(line=48, offs=55): error(2): the static identifier [line] is
unrecognized.
/home/kiwamu/src/uemacs-bohai/DATS/utf8.dats: 1639(line=48, offs=51)
-- 1643(line=48, offs=55): error(2): the static expression is of the
sort [S2RTerr()] but it is expected to be of the sort [S2RTerr()].
/home/kiwamu/src/uemacs-bohai/DATS/utf8.dats: 1639(line=48, offs=51)
-- 1655(line=48, offs=67): error(2): the static expression needs to be
impredicative but is assigned the sort [S2RTerr()].
/home/kiwamu/src/uemacs-bohai/DATS/utf8.dats: 1908(line=55, offs=62)
-- 1917(line=55, offs=71): error(2): sort application is not
supported.
/home/kiwamu/src/uemacs-bohai/DATS/utf8.dats: 1902(line=55, offs=56)
-- 1906(line=55, offs=60): error(2): the static identifier [line] is
unrecognized.
/home/kiwamu/src/uemacs-bohai/DATS/utf8.dats: 1902(line=55, offs=56)
-- 1906(line=55, offs=60): error(2): the static expression is of the
sort [S2RTerr()] but it is expected to be of the sort [S2RTerr()].
/home/kiwamu/src/uemacs-bohai/DATS/utf8.dats: 1902(line=55, offs=56)
-- 1918(line=55, offs=72): error(2): the static expression needs to be
impredicative but is assigned the sort [S2RTerr()].
patsopt(TRANS2): there are [8] errors in total.
exit(ATS): uncaught exception:
_2home_2kiwamu_2src_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
```
Where and what should I inject your annotation?
thanks for your kind reply.
On Thu, Nov 1, 2018 at 5:12 PM Artyom Shalkhakov
<artyom.s...@gmail.com> wrote:
> You should put at at every branch (so on every [if] and on every [case]). That's because the
> variable [line] is of linear type, and the annotation basically says that in every alternative of
> the branch it's going to be preserved (so, after the evaluation of an [if] or a [case] the type of
> [line] is going to still be [strnptr(m)]). I think the reason for having to annotate it is due to a hit
> on performance in constraint solving. I think I read about this in one of HX's papers.
>
> I think in your case, you'll have to annotate two [if]s:
>
> https://github.com/metasepi/uemacs-bohai/blob/9ecdd06fe09e6433ed0fb4271c0e5b44d2ad8f8d/DATS/utf8.dats#L48
> https://github.com/metasepi/uemacs-bohai/blob/9ecdd06fe09e6433ed0fb4271c0e5b44d2ad8f8d/DATS/utf8.dats#L55
>
> Could you try it? You could also try to annotate only one [if] to find a minimal required annotation that keeps the typechecker silent. :-)
I have an stupid question. I wrote following code:
```
val bytes = if ($UN.cast{int}{char} c < 0xc0):( line: strnptr(m) )
then 1U
else bytes' where {
(* Ok, it's 11xxxxxx, do a stupid decode *)
val (mask, bytes'') = loop1 (c, 0x20U, 0x2U)
(* Invalid? Do it as a single byte Latin1 *)
val bytes' = if (bytes'' > 6 || bytes'' > len):( line: strnptr(m) )
else bytes' where {
(* Ok, it's 11xxxxxx, do a stupid decode *)
val (mask, bytes'') = loop1 (c, 0x20U, 0x2U)
(* Invalid? Do it as a single byte Latin1 *)
then 1U
else bytes'' where {
```
else bytes'' where {
But above causes following errors:
```
$ make
ATS utf8.dats.c
/home/kiwamu/src/uemacs-bohai/DATS/utf8.dats: 1645(line=48, offs=57)
-- 1654(line=48, offs=66): error(2): sort application is not
supported.
/home/kiwamu/src/uemacs-bohai/DATS/utf8.dats: 1639(line=48, offs=51)
-- 1643(line=48, offs=55): error(2): the static identifier [line] is
unrecognized.
/home/kiwamu/src/uemacs-bohai/DATS/utf8.dats: 1639(line=48, offs=51)
-- 1643(line=48, offs=55): error(2): the static expression is of the
sort [S2RTerr()] but it is expected to be of the sort [S2RTerr()].
/home/kiwamu/src/uemacs-bohai/DATS/utf8.dats: 1639(line=48, offs=51)
-- 1655(line=48, offs=67): error(2): the static expression needs to be
impredicative but is assigned the sort [S2RTerr()].
/home/kiwamu/src/uemacs-bohai/DATS/utf8.dats: 1908(line=55, offs=62)
-- 1917(line=55, offs=71): error(2): sort application is not
supported.
/home/kiwamu/src/uemacs-bohai/DATS/utf8.dats: 1902(line=55, offs=56)
-- 1906(line=55, offs=60): error(2): the static identifier [line] is
unrecognized.
/home/kiwamu/src/uemacs-bohai/DATS/utf8.dats: 1902(line=55, offs=56)
-- 1906(line=55, offs=60): error(2): the static expression is of the
sort [S2RTerr()] but it is expected to be of the sort [S2RTerr()].
/home/kiwamu/src/uemacs-bohai/DATS/utf8.dats: 1902(line=55, offs=56)
-- 1918(line=55, offs=72): error(2): the static expression needs to be
impredicative but is assigned the sort [S2RTerr()].
patsopt(TRANS2): there are [8] errors in total.
exit(ATS): uncaught exception:
_2home_2kiwamu_2src_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
```
Where and what should I inject your annotation?
gmhwxi
Nov 1, 2018, 11:03:52 PM11/1/18
to ats-lang-users
The way you wrote the code makes it a bit difficult to
do typechecking. Try to change the interface for utf8_to_unicode
as follows:
extern
fun
utf8_to_unicode
{l1:addr}
{i,m:nat | i < m}
{l2:addr}
( pf: !unicode_t@l1
| line: !strnptr(l2,m), index: int(i), len: int(m), res: ptr(l1)): uint = "ext#utf8_to_unicode"
Kiwamu Okabe
Nov 1, 2018, 11:29:00 PM11/1/18
to ats-lan...@googlegroups.com
Dear Hongwei and Artyom,
On Fri, Nov 2, 2018 at 12:03 PM gmhwxi <gmh...@gmail.com> wrote:
> The way you wrote the code makes it a bit difficult to
> do typechecking. Try to change the interface for utf8_to_unicode
> as follows:
Thanks! It's fixed!
https://travis-ci.org/metasepi/uemacs-bohai/builds/449662253
> I think the reason for having to annotate it is due to a hit on performance in
> constraint solving. I think I read about this in one of HX's papers.
Could you tell me where is the paper? > Artyom
What do I think such `unsolved constraint` error?
How to approach it?
Should I think "Umm it may needs more addr annotation"?
On Fri, Nov 2, 2018 at 12:03 PM gmhwxi <gmh...@gmail.com> wrote:
> The way you wrote the code makes it a bit difficult to
> do typechecking. Try to change the interface for utf8_to_unicode
> as follows:
https://travis-ci.org/metasepi/uemacs-bohai/builds/449662253
> I think the reason for having to annotate it is due to a hit on performance in
> constraint solving. I think I read about this in one of HX's papers.
What do I think such `unsolved constraint` error?
How to approach it?
Should I think "Umm it may needs more addr annotation"?
Artyom Shalkhakov
Nov 5, 2018, 7:51:19 AM11/5/18
to ats-lang-users
Hi Kiwamu,
Sorry for the delay, I missed your reply.
Dear Hongwei and Artyom,
On Fri, Nov 2, 2018 at 12:03 PM gmhwxi <gmh...@gmail.com> wrote:
> The way you wrote the code makes it a bit difficult to
> do typechecking. Try to change the interface for utf8_to_unicode
> as follows:
Thanks! It's fixed!
https://travis-ci.org/metasepi/uemacs-bohai/builds/449662253
> I think the reason for having to annotate it is due to a hit on performance in
> constraint solving. I think I read about this in one of HX's papers.
Could you tell me where is the paper? > Artyom
The "state types" are described here:
section 4.3. The section talks about synthesizing these state types. I guess that ATS2 and ATS3 still follow a similar approach (since sometimes it's OK to drop the annotations completely and sometimes not).
I can't source my claim about performance though, sorry about that.
Kiwamu Okabe
Nov 8, 2018, 7:26:50 PM11/8/18
to ats-lan...@googlegroups.com
Dear Artyom and Hongwei,
BTW, I can fix this issue with `let in end` style code without
`l2:addr` static value:
https://github.com/metasepi/uemacs-bohai/commit/9d52514601151fb0887a436f2e1680be09b0cddd
I think it means:
A. `value where {}` style code needs `l2:addr` static value
B. `let in` style code needs no `l2:addr` static value
I believe both styles are equivalent.
Are there some difference on type inference? > Hongwei
I love A style, but I should choose B if it has better inference.
thanks for your kind reply.
On Mon, Nov 5, 2018 at 9:51 PM Artyom Shalkhakov
<artyom.s...@gmail.com> wrote:
> The "state types" are described here:
>
> http://www.ats-lang.org/MYDATA/Xanadu-lics00.pdf
>
> section 4.3. The section talks about synthesizing these state types. I guess that ATS2 and ATS3 still follow a similar approach (since sometimes it's OK to drop the annotations completely and sometimes not).
>
> I can't source my claim about performance though, sorry about that.
Thanks. I should read the detail...
<artyom.s...@gmail.com> wrote:
> The "state types" are described here:
>
> http://www.ats-lang.org/MYDATA/Xanadu-lics00.pdf
>
> section 4.3. The section talks about synthesizing these state types. I guess that ATS2 and ATS3 still follow a similar approach (since sometimes it's OK to drop the annotations completely and sometimes not).
>
> I can't source my claim about performance though, sorry about that.
BTW, I can fix this issue with `let in end` style code without
`l2:addr` static value:
https://github.com/metasepi/uemacs-bohai/commit/9d52514601151fb0887a436f2e1680be09b0cddd
I think it means:
A. `value where {}` style code needs `l2:addr` static value
B. `let in` style code needs no `l2:addr` static value
I believe both styles are equivalent.
Are there some difference on type inference? > Hongwei
I love A style, but I should choose B if it has better inference.
Hongwei Xi
Nov 8, 2018, 11:18:49 PM11/8/18
to ats-lan...@googlegroups.com
>>I believe both styles are equivalent.
>>Are there some difference on type inference? > Hongwei
>>Are there some difference on type inference? > Hongwei
There are equivalent in terms of dynamic semantics.
They are not equivalent with respect to the way in which
type inference is handled.
--
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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6d%3DuiDnjxOPG9C7a2QMB25QPrBRMYxQ7iJdC-6SSf5krGQ%40mail.gmail.com.
Kiwamu Okabe
Nov 8, 2018, 11:22:08 PM11/8/18
to ats-lan...@googlegroups.com
On Fri, Nov 9, 2018 at 1:18 PM Hongwei Xi <gmh...@gmail.com> wrote:
> >>Are there some difference on type inference? > Hongwei
>
> There are equivalent in terms of dynamic semantics.
> They are not equivalent with respect to the way in which
> type inference is handled.
Thanks. Clear for me.
> >>Are there some difference on type inference? > Hongwei
>
> There are equivalent in terms of dynamic semantics.
> They are not equivalent with respect to the way in which
> type inference is handled.
I should choose `let in` style.
Reply all
Reply to author
Forward
0 new messages