So, I'm trying to implement the following hash function:
fn hash {n:int | n > 0}
( s: string(n), size: int(n) ) : [o:int | o >= 0; o < n] int o = let
fun hash_num {i:nat | i <= n}
( i: int i, h: int ) : int =
if i < size then let
val c_at_i = string_get_at_gint(s, i)
in
hash_num(i+1, h * 101 + g0int_of_char(c_at_i))
end else h
in
abs( hash_num(0, 0) ) % size
end
Which produces the following error message:
/home/tmj90/Goldelish-Engine/source/data/dict.dats: 381(line=21, offs=2) --
409(line=21, offs=30): error(3): the dynamic expression cannot be assigned
the type [S2Eexi(o(8727); S2Eapp(S2Ecst(>=); S2Evar(o(8727)),
S2Eintinf(0)), S2Eapp(S2Ecst(<); S2Evar(o(8727)), S2Evar(n(8725)));
S2Eapp(S2Ecst(g1int_int_t0ype); S2Eextkind(atstype_int), S2Evar(o(8727))))].
/home/tmj90/Goldelish-Engine/source/data/dict.dats: 381(line=21, offs=2) --
409(line=21, offs=30): error(3): mismatch of static terms (tyleq):
The actual term is: S2Eapp(S2Ecst(g0int_t0ype); S2Eextkind(atstype_int))
The needed term is: S2Eapp(S2Ecst(g1int_int_t0ype);
S2Eextkind(atstype_int), S2EVar(5314))
/home/tmj90/Goldelish-Engine/source/data/dict.dats: 381(line=21, offs=2) --
409(line=21, offs=30): error(3): mismatch of static terms (tyleq):
The actual term is: S2Eapp(S2Ecst(g0int_t0ype); S2Eextkind(atstype_int))
The needed term is: S2Eexi(o(8727); S2Eapp(S2Ecst(>=); S2Evar(o(8727)),
S2Eintinf(0)), S2Eapp(S2Ecst(<); S2Evar(o(8727)), S2Evar(n(8725)));
S2Eapp(S2Ecst(g1int_int_t0ype); S2Eextkind(atstype_int), S2Evar(o(8727))))
My question is, how do I tell the typechecker that this code works
fine? The abs() ensures that the result is positive, and the '%' (modulo)
operation will always return positive/zero because neither input can be
negative. Is there some way that I can express this to the typechecker?
Did I make a mistake in my code that I missed?
Based on the info that I can find, I think the solution to my problem
either relies on the use of the '#[ | ]' syntax, or the 'praxi' keyword,
but I'm not fully clear on how either work/when to use them. Any help is
appreciated, and if the issue seems connected to code that I didn't show
here, please let me know and I will be happy to provide more source code.
--
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 view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/99521a07-3fc9-4607-bdc3-e347c83d9531n%40googlegroups.com.
