Dear Artyom, thanks for your kind reply. On Thu, Nov 1, 2018 at 5:12 PM Artyom Shalkhakov <artyom.shalkha...@gmail.com> 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 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):( 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.