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.
