Re: Why my code occurs `unsolved constraint` error?
Dear Hongwei and Artyom, On Fri, Nov 2, 2018 at 12:03 PM gmhwxi 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"? 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@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/CAEvX6dmp%3DGVgxME1_8XbdpdKMwq%2BH8rSSXwjLLoRzoM1XV6tEg%40mail.gmail.com.
Re: Why my code occurs `unsolved constraint` error?
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"
On Thursday, November 1, 2018 at 10:30:58 PM UTC-4, Kiwamu Okabe wrote:
>
> Dear Artyom,
> thanks for your kind reply.
>
> On Thu, Nov 1, 2018 at 5:12 PM Artyom Shalkhakov
> 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) )
> then 1U
> else bytes' where {
> (* Ok, it's 11xx, 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) )
> then 1U
> 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?
>
> 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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@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/a082671f-6236-4660-a55d-c45797287baa%40googlegroups.com.
Re: Why my code occurs `unsolved constraint` error?
Dear Artyom,
thanks for your kind reply.
On Thu, Nov 1, 2018 at 5:12 PM Artyom Shalkhakov
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) )
then 1U
else bytes' where {
(* Ok, it's 11xx, 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) )
then 1U
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?
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@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/CAEvX6dncwYH3vuA8NBoJ4jQ57aP2iLR%2Bz9Ak66x3hk2JN7otMw%40mail.gmail.com.
Re: Why my code occurs `unsolved constraint` error?
Hi Kiwamu, чт, 1 нояб. 2018 г. в 10:00, Kiwamu Okabe : > Dear Artyom and Hongwei, > sorry for my late reply. > > On Mon, Oct 29, 2018 at 5:17 PM Artyom Shalkhakov > 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 > > 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. :-) > > 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-users+unsubscr...@googlegroups.com. > To post to this group, send email to ats-lang-users@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 -- 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 post to this group, send email to ats-lang-users@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/CAKO6%3Dqh5yYagiaTtB32BD5RV_3ZwwMkJ4_thZ_%2BR-McjR_FjTw%40mail.gmail.com.
Re: Why my code occurs `unsolved constraint` error?
Dear Artyom and Hongwei, sorry for my late reply. On Mon, Oct 29, 2018 at 5:17 PM Artyom Shalkhakov 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 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@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.
