Thank you very much. Now it works!
I did not knew how to search for this function.
Em sábado, 4 de agosto de 2018 19:18:40 UTC-3, gmhwxi escreveu:
>
> Please use:
>
> val zero = i2sz(0)
>
> On Sat, Aug 4, 2018 at 6:03 PM, Bruno Zimmermann <brun...@gmail.com
> <javascript:>> wrote:
>
>> Suppose these files:
>>
>> 1. list.sats:
>> #include "share/atspre_define.hats"
>> #include "share/atspre_staload.hats"
>>
>> #define :: list_cons
>>
>> datatype list (t@ype+, int) =
>> | {a : t@ype} list_nil (a, 0) of ()
>> | {a : t@ype} {n : nat} list_cons (a, n + 1) of (a, list (a, n))
>>
>> fun {a : t@ype} list_length {n : nat} (xs : list (a, n)) : size_t n
>>
>> 2. list.dats:
>> #include "share/atspre_define.hats"
>> #include "share/atspre_staload.hats"
>>
>> staload "list.sats"
>>
>> implement {a} list_length {n} (xs) = let
>> val zero : size_t 0 = 0UL
>> fun loop {
>> i, j : nat
>> } .<i>. (xs: list (a, i), count: size_t j) : size_t (i + j) =
>> case+ xs of
>> | list_nil () => count
>> | list_cons (_, xs0) => loop (xs0, count + 1)
>> in
>> loop (xs, zero)
>> end
>>
>> I get the following error:
>>
>> /home/bruno/prog/ats/mylib/list.dats: 143(line=7, offs=7) -- 158(line=7,
>> offs=22): warning(3): the constraint [S2Eeqeq(S2Eextkind(atstype_ulint);
>> S2Eextkind(atstype_size))] cannot be translated into a form accepted by the
>> constraint solver.
>> /home/bruno/prog/ats/mylib/list.dats: 143(line=7, offs=7) -- 158(line=7,
>> offs=22): error(3): unsolved constraint: C3NSTRprop(C3TKmain();
>> S2Eeqeq(S2Eextkind(atstype_ulint); S2Eextkind(atstype_size)))
>> /home/bruno/prog/ats/mylib/list.dats: 365(line=15, offs=13) --
>> 369(line=15, offs=17): warning(3): the constraint
>> [S2Eeqeq(S2Eextkind(atstype_ulint); S2Eextkind(atstype_size))] cannot be
>> translated into a form accepted by the constraint solver.
>> typechecking has failed: there are some unsolved constraints: please
>> inspect the above reported error message(s) for information.
>> exit(ATS): uncaught exception:
>> _2tmp_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
>>
>> If I remove the suffix on the zero literal 0UL, I get the following error:
>>
>> /home/bruno/prog/ats/mylib/list.dats: 143(line=7, offs=7) -- 158(line=7,
>> offs=22): error(3): the pattern cannot be given the ascribed type.
>> /home/bruno/prog/ats/mylib/list.dats: 143(line=7, offs=7) -- 158(line=7,
>> offs=22): error(3): mismatch of static terms (tyleq):
>> The actual term is: S2Eapp(S2Ecst(g1int_int_t0ype);
>> S2Eextkind(atstype_int), S2Eintinf(0))
>> The needed term is: S2Eapp(S2Ecst(g1uint_int_t0ype);
>> S2Eextkind(atstype_size), S2Eintinf(0))
>> /home/bruno/prog/ats/mylib/list.dats: 363(line=15, offs=13) --
>> 367(line=15, offs=17): error(3): the dynamic expression cannot be assigned
>> the type [S2Eapp(S2Ecst(g1uint_int_t0ype); S2Eextkind(atstype_size),
>> S2EVar(5243))].
>> /home/bruno/prog/ats/mylib/list.dats: 363(line=15, offs=13) --
>> 367(line=15, offs=17): error(3): mismatch of static terms (tyleq):
>> The actual term is: S2Eapp(S2Ecst(g1int_int_t0ype);
>> S2Eextkind(atstype_int), S2Eintinf(0))
>> The needed term is: S2Eapp(S2Ecst(g1uint_int_t0ype);
>> S2Eextkind(atstype_size), S2EVar(5243))
>> patsopt(TRANS3): there are [2] errors in total.
>> exit(ATS): uncaught exception:
>> _2tmp_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
>>
>> If I change the type from size_t to int (and also the suffix in the
>> literal), the code typechecks.
>>
>> --
>> 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-user...@googlegroups.com <javascript:>.
>> To post to this group, send email to ats-lan...@googlegroups.com
>> <javascript:>.
>> 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/7d4f8c0b-de8b-4006-8734-65f2d2a5b485%40googlegroups.com
>>
>> <https://groups.google.com/d/msgid/ats-lang-users/7d4f8c0b-de8b-4006-8734-65f2d2a5b485%40googlegroups.com?utm_medium=email&utm_source=footer>
>> .
>>
>
>
--
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/45194efc-7dae-4f13-b470-0758358d1d72%40googlegroups.com.
