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 https:/
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.