The following dataview strbuf_v captures the notion of a string in C, which consisits a sequence of non-null characters followed by the null character:
dataview
strbuf_v(addr, int) =
| {l:addr}
strbuf_v_nil(l, 0) of (char(0) @ l)
| {l:addr}{n:nat}
strbuf_v_cons(l, n+1) of (charNZ @ l, strbuf_v(l+sizeof(char), n))
Given a C-string, one can always access its first character; if the character is null, then the C-string is empty; if it is not, then the C-string is non-empty. The following implementation of strptr_is_nil precisely follows this simple way of testing whether a C-string is empty or not:
//
fun
strptr_is_nil
{l:addr}{n:int}
(
str: !strptr(l, n)
) : bool(n==0) = let
//
prval
(pf_at, fpf) =
strbuf_v_getfst(str.0)
// prval
val c0 = !(str.1)
prval () = str.0 := fpf(pf_at)
in
iseqz(c0) // testing whether [c0] is null
end // end of [strptr_is_nil]
//
extern
prfun
strbuf_v_getfst
{l:addr}{n:int}
(
pf: strbuf_v(l, n)
) : [
c:int | (c==0 && n==0) || (c != 0 && n > 0)
] (char(c) @ l, char(c) @ l -<lin,prf> strbuf_v(l, n))
(* ****** ****** *)
primplmnt
strbuf_v_getfst
(pf) =
(
case+ pf of
| strbuf_v_nil(pf_at) => #[.. | (pf_at, llam(pf_at) => strbuf_v_nil(pf_at))]
| strbuf_v_cons(pf_at, pf2) => #[.. | (pf_at, llam(pf_at) => strbuf_v_cons(pf_at, pf2))]
)
The following implementation gives another example of handling the dataview strbuf_v:
fun
strptr_length
{l:addr}{n:int}
(
str: !strptr(l, n)
) : size_t(n) = let
//
fun
loop
{l:addr}
{i,j:int}
(
pf: !strbuf_v(l, i)
| p0: ptr(l), j: size_t(j)
) : size_t(i+j) = let
//
prval
[c:int]
(pf_at, fpf) = strbuf_v_getfst(pf)
//
val c0 = !p0
//
prval ((*return*)) = pf := fpf(pf_at)
//
in
//
if
iseqz(c0)
then j
else res where
{
prval
strbuf_v_cons(pf_at, pf2) = pf
val res = loop(pf2 | ptr_succ<char>(p0), succ(j))
prval ((*folded*)) = pf := strbuf_v_cons(pf_at, pf2)
} (* end of [else] *)
//
end // end of [loop]
//
in
loop(str.0 | str.1, i2sz(0))
end // end of [strptr_length]
Please find the entirety of the above presented code on-line.