More string constraints

Google Group
1

Hello,

Here I try to implement a function based on the counter using closures and
a reference in the ATS book, but incorporating a string(n), to make a
"string stream"
I’ve tried several things, but my “best shot” (as far as I can tell)
results in the error: d2exp_tr_up: not implemented yet: d2e0 =
D2Esym(string_length)
Any advice would be appreciated.

Perhaps a more fruitful approach would be defining an auxiliary function
for “peek” to do the work, and just let peek be concerned with enforcing
constraints, but it wasn’t clear to me that this would work either.

//typedef sizeLte (n:int) = [i:nat | i <= n] size_t (i)
typedef sizeLteRef(n:int) = ref(sizeLte(n))

typedef strstream = '{
peek = () - char,
next = () - void
//cose() - if using ptrs
}

//Get the minimum of two sizes, assert the minimum via type
fun {m,n:nat} minim (x:size_t m, y:size_t n): size_t(min(m,n))= if x < y
then x else y

// make a “string stream” that can return the current char (peek()) or
advance
// the position in the string by 1 (next())
fun {n:nat} {i:nat | i <= n} new_strstream(astring: string(n)): strstream =
let
val posn = ref<size_t> 0
val rstring = ref<string(n)> astring
//Error: d2exp_tr_up: not implemented yet: d2e0 = D2Esym(string_length)
val sz = ref<size_t n> string_length(!rstring)
in
’{ peek = lam() => !rstring[minim(size1_of_size(!posn), sz)],
next = lam() =>
let
val+ notend = string_isnot_atend(!rstring, size1_of_size(!posn))
val _ = case+ notend of
| false => !posn
| true => !posn := !posn+1
in
()
end
}

end

2

Also, is there any relationship enforced in ATS between the “n” from
val [n:int] str = string1_of_string (str)
and the “n” from
val n = string_length (str)

Yes, the latter n is of the type size_t (n).

Would you say, as a general rule of thumb, it is best to avoid these
constraints where possible,
or when they seem to be problems, by creating additional local variables?

I would say that keeping it simple is a general rule of thumb. What I see
all the time is someone
(especially, a beginner) trying to prove so much just for the sake of
proving. This could easily lead
to frustrating experience with ATS.

3

//
// HX: this is my try.
//
// I find that programming with dependent types is
// a very tricky thing to do. The biggest problem is
// that one could easily get into a typechecking situation
// that is almost impossible to get out.
//
// It is like this: the less you know about dependent types, the harder
typechecking you will encounter.
//
staload _(anon) = “prelude/DATS/reference.dats”
//
typedef
strstream = '{
peek = () - char
, next = () - void
, prev = () - void
}

extern
fun strstream_make (str: string): strstream

implement
strstream_make (str) = let
//
#define NUL ‘\000’
//
val [n:int]
str = string1_of_string (str)
val n = string_length (str)
//
val pos = ref<sizeLte(n)> (size1_of_int1(0))
//
val fpeek =
lam () : char = let
val i = !pos in if i < n then str[i] else NUL
end // end of [lam]
val fnext =
lam () : void = let
val i = !pos in if i < n then !pos := i + 1
end // end of [lam]
val fprev =
lam () : void = let
val i = !pos in if i > 0 then !pos := i - 1
end // end of [lam]
//
in '{
peek= fpeek, next= fnext, prev= fprev
} end // end of [strstream_make]

implement
main () = () where {
val hello = strstream_make (“hello”)
val () = println! (hello.peek())
val () = hello.next()
val () = println! (hello.peek())
val () = hello.prev()
val () = println! (hello.peek())
}

4

Thanks, that is a big help. I will certainly try to read more about
dependent types and add what I can to the wiki on this topic, but probably
not right away due to some time constraints.

I guess I will prioritize learning dependent types above linear types and
proofs, since it seems all are necessary. I’m in no hurry to write kernel
code myself, as fun as that might be.

The most interesting thing to me in your code (other than the pragmatic
fact that it works) is this:

   //This works
   let
     val i = !pos 
   in if i < n then !pos := i + 1       //case1
   end // end of [lam]

  //This doesn't
  let
     val i = !pos 
   in if !pos < n then !pos := !pos + 1 //case2 
   //neither do these:
   //in if i < n then !pos := !pos + 1  //case3
   //in if !pos < n then !pos := i + 1  //cas 4
   end // end of [lam]

This gives:
error(3): unsolved constraint: C3STRprop(main; S2Eapp(S2Ecst(<=);
S2EVar(2454), S2Evar(n(5346))))

You are very much right, I never would have guessed to do this. My guess at
this point is that !pos < n and !pos := !pos + 1 (for instance) generate
two conflicting constraints:
Say i == !pos == n-1.

Case 1 constraints (possibly incomplete):
pos <= n
i < n
pos = (i+1) = n
–> pos == n
Case 2:
pos <= n
pos < n (so now ignore the weaker constraint above)
pos = (i+1) = n
–>contradition

Also, is there any relationship enforced in ATS between the “n” from
val [n:int] str = string1_of_string (str)
and the “n” from
val n = string_length (str)
(other than clearly talking about the same thing integer value)? It seems
renaming all value occurrences of “n”
(the second “n” above) works fine too. I am not sure which style is better,
but I guess having the same name makes it more readable, as long as
understanding on this point is clear.

Would you say, as a general rule of thumb, it is best to avoid these
constraints where possible, or when they seem to be problems, by creating
additional local variables?

Thanks! It is fun now that I understand a bit more… but I can see that it
will take some getting used to.