I’ve probably missed something fundamental in trying to implement a
function that gets a character at a string position. When I try to compile
the code I get the following error:
/media/RAID5/share/ATS_learning/stringtest.dats: 1079(line=45, offs=24) –
1088(line=45, offs=33): error(3): unsolved constraint: C3STRprop(main;
S2Eapp(S2Ecst(<); S2EVar(2440), S2EVar(2439)))
type-checking has failed: there are some unsolved constraints: please
inspect the above reported error message(s) for information.
The code below is appended to the standard template header.
staload “prelude/SATS/string.sats”
fn loopWhite //not a loop yet
//How do we guarantee this constraint? (i<n)
//{n:nat} {i: nat | i < n}
{n:int} {i:nat}
(stri: (string n, size_t i)): (string, size_t) =
let
val strptr = stri.0
val i = stri.1
//How do we solve this constraint?
val cur_ch: char = strptr[i]
in
@(strptr, i)
end
implement main () = () where {
val initidx = size1_of_size(size_of_int(0))
val atup = @(" asfd",initidx)
val atup2 = loopWhite(atup)
}
I admit this code is bad for numerous reasons (aside from the fact it
doesn’t work), such as using unboxed strings in a function that will become
a loop, and am just trying to be able to quickly use strings for a project
I am working on. Still, I’m happy to hear any suggestions.
Thanks! This helped me figure out a few things. The rest of this post is to
belabor the points for future reference, so feel free not to read.
I should have been clear that the function loopWhite wasn’t supposed to do
anything in particular as displayed other than define cur_ch internally.
So, first of all, I was able to get it to typecheck by
1)
//val initidx = size1_of_size(size_of_int(0))
val initidx = size1_of_int1(0)
Looking at these 3 functions, it would appear that size1_of_size has a
slightly different return type ([i:nat] size_t i) than what we are looking
for (size_t i).
fun size1_of_int1 {i:nat}
(i: int i):<> size_t i = “atspre_size1_of_int1”
fun size_of_int
(i: int):<> size_t = “atspre_size_of_int”
fun size1_of_int1 {i:nat}
(i: int i):<> size_t i = “atspre_size1_of_int1”
//Do a “bounds check” in the code:
val cur_ch = let
val isnot = string_isnot_atend (astrng, i) in
if isnot then astrng[i] else '\0’
end
How does ATS perform bounds checking here? It is all black magic to me, but
I’m fine with magic if I know when to expect it. I should have realized ATS
required a check of this sort, and should have remembered
string_isnot_atend could do this from the book…
Here I found the use of sizeLte (n) unnecessary in the return type, but
it is good to know about (and I should have known about
//My mom always told me if you can’t say anything precise, don’t say
anything at all. --ATS coder
I took the liberty to re-write your code as follows:
staload “prelude/SATS/string.sats”
fun loopWhite
{n:int} {i:nat | i <=n}
(str: string n, i: size_t i): sizeLte (n) = let
val isnot = string_isnot_atend (str, i)
in
if isnot then
(if str[i] > ‘\0’ then loopWhite (str, i+1) else i)
else i
end // end of [loopWhite]
implement
main () = () where {
val i0 = size1_of_int1 (0)
val str = " asfd"
val i2 = loopWhite(str, i0)
}
Referring to the bounds checking question. The definition of
string_isnot_atend is:
fun string_isnot_atend
{n:int} {i:nat | i <= n}
(str: string n, i: size_t i):<> bool (i < n)
Note the return type which is “bool (i < n)”. This means that when the user
checks the return type of this function that in the “true” branch of the
check that the compiler knows that “i < n”, therefore the index is within
range of the string. In the false branch of the check then i must be >= n.
And because of the initial constraint “i:nat | i < = n” i must acutally be
equal to n - it can’t be greater. Any use of 'string_isnot_atend" will
apply these contrains to the values of ‘i’ and ‘n’ depending on how the
check is performed. For example:
val n = 2
val x = string_isnot_atend (mystring, n)
val () = assertloc (x)
val ch = string_get_char_at (mystring, n)
Here, ‘ch’ can be obtained because it’s known than ‘n’ is less than the
length of the string. This is because we’ve asserted that the result of
’string_isnot_atend’ is true, and that functions return result constrains
the value of ‘n’ to be less than the value of the string. Does that make
sense?
I suppose a simplified question would be, how does one use
string_get_char_at?
I have explicitly used string_get_char_at instead of [] to get cur_ch, and
it seems to be the same (no surprise there). string_get_char_at has the
following definition:
fun string_get_char_at
{n:int}
{i:nat | i < n} (
str: string n, i: size_t i
) :<> c1har
= "atspre_string_get_char_at"
overload [] with string_get_char_at
So even if I precisely modify loopWhite above to match the universal
quantifiers here (and if I use c1har) it doesn’t help. At first I wondered
if I need to prove something, but string_get_char_at is a c function, so I
don’t think that is the case.