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] > > (* > * 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 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.
