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