I myself usually just do:
val zero = $UN.cast{size_t}(0)
It may look a bit uglier but it is really just the same thing.
On Sat, Aug 4, 2018 at 6:20 PM, Bruno Zimmermann <brunoc...@gmail.com>
wrote:
> 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>
>> 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_2pa
>>> ts_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_2pa
>>> ts_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.
>>> To post to this group, send email to ats-lan...@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/ms
>>> gid/ats-lang-users/7d4f8c0b-de8b-4006-8734-65f2d2a5b485%40go
>>> oglegroups.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
> <https://groups.google.com/d/msgid/ats-lang-users/45194efc-7dae-4f13-b470-0758358d1d72%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/CAPPSPLrC%2BNHmJgLeps7NT19htxqQFrxWPoLVkMp%3Dz6SsJkPyug%40mail.gmail.com.
