How can I create a dependent size_t literal?

[Bruno Zimmermann]

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.

[Hongwei Xi]

Please use:

val zero = i2sz(0)

--
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+unsubscribe@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/7d4f8c0b-de8b-4006-8734-65f2d2a5b485%40googlegroups.com.

[Bruno Zimmermann]

Thank you very much. Now it works!

I did not knew how to search for this function.

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.

[Hongwei Xi]

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.

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@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.