Re: Why my code occurs `unsolved constraint` error?
On Fri, Nov 9, 2018 at 1:18 PM Hongwei Xi 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. I should choose `let in` style. -- 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%3DcxZMVhY6xADP-jes%3D%3DKs%3DVC%2Btka9P7HjK7-MScZBChw%40mail.gmail.com.
Re: Why my code occurs `unsolved constraint` error?
>>I believe both styles are equivalent. >>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. On Thu, Nov 8, 2018 at 7:26 PM Kiwamu Okabe wrote: > Dear Artyom and Hongwei, > thanks for your kind reply. > > On Mon, Nov 5, 2018 at 9:51 PM Artyom Shalkhakov > 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... > > > 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. > > 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%3DuiDnjxOPG9C7a2QMB25QPrBRMYxQ7iJdC-6SSf5krGQ%40mail.gmail.com > . > -- 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/CAPPSPLpAzMd0AiSxEGwDMz1V644-9S6rSaUmZ-d_3_RMfEOC%3Dg%40mail.gmail.com.
Re: Why my code occurs `unsolved constraint` error?
Dear Artyom and Hongwei, thanks for your kind reply. On Mon, Nov 5, 2018 at 9:51 PM Artyom Shalkhakov 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... 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. 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%3DuiDnjxOPG9C7a2QMB25QPrBRMYxQ7iJdC-6SSf5krGQ%40mail.gmail.com.
Re: Why my code occurs `unsolved constraint` error?
Hi Kiwamu, Sorry for the delay, I missed your reply. On Friday, November 2, 2018 at 5:29:00 AM UTC+2, Kiwamu Okabe wrote: > > 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 > > 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. > > 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/c6f9ce31-333a-42f2-a3b4-848669066b48%40googlegroups.com.
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.
Re: Why my code occurs `unsolved constraint` error?
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); } *) val c = line[index] val () = !res := $UN.cast{unicode_t}{char} line[index] (* * 0xxx is valid utf8 * 10xx 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 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) 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 On Mon, Oct 29, 2018 at 8:14 AM Hongwei Xi wrote: > I tried and there was no problem. I used ATS2-0.3.12. > > > On Mon, Oct 29, 2018 at 2:52 AM Kiwamu Okabe wrote: > >> 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] >> >> (* >>* 0xxx is valid utf8 >>* 10xx 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 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) >> 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 >> >> -- >> 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%3DWqC8ym8KArMBvwOYi8tBqZAMJ_WwfXp0h9AgBkcO2Lw%40mail.gmail.com >> . >> > -- 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
Re: Why my code occurs `unsolved constraint` error?
I tried and there was no problem. I used ATS2-0.3.12. On Mon, Oct 29, 2018 at 2:52 AM Kiwamu Okabe wrote: > 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] > > (* >* 0xxx is valid utf8 >* 10xx 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 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) > 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 > > -- > 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%3DWqC8ym8KArMBvwOYi8tBqZAMJ_WwfXp0h9AgBkcO2Lw%40mail.gmail.com > . > -- 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/CAPPSPLrPbgvatThe-DCu%2BcdVDGKRHGTq0OCqTt4DKXC9XzgNKQ%40mail.gmail.com.
Re: Why my code occurs `unsolved constraint` error?
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. On Monday, October 29, 2018 at 8:52:33 AM UTC+2, Kiwamu Okabe wrote: > > 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] > > (* >* 0xxx is valid utf8 >* 10xx 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 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) > 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 > -- 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/7b1a17e9-afde-47de-ba5b-154fbbb2fce9%40googlegroups.com.
Why my code occurs `unsolved constraint` error?
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] (* * 0xxx is valid utf8 * 10xx 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 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) 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 -- 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%3DWqC8ym8KArMBvwOYi8tBqZAMJ_WwfXp0h9AgBkcO2Lw%40mail.gmail.com.