I tried and there was no problem. I used ATS2-0.3.12.
On Mon, Oct 29, 2018 at 2:52 AM Kiwamu Okabe <[email protected]> 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] > > (* > * 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 > > -- > 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 [email protected]. > To post to this group, send email to [email protected]. > 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 [email protected]. To post to this group, send email to [email protected]. 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.
