# Dataview for Linear Strings

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_nil(l, 0) of (char(0) @ l)
strbuf_v_cons(l, n+1) of (charNZ @ l, strbuf_v(l+sizeof(char), n))
```

Let us define a linear type strptr as follows:

```vtypedef strptr(l:addr, n:int) = (strbuf_v(l, n) | ptr(l))
```

Then a C-string of length N that is stored at location L can be assigned the type strptr(L, 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
(
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]
//
```

where the proof function strbuf_v_getfst is declared and implemented as follows:

```extern
prfun
strbuf_v_getfst
(
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
(
str: !strptr(l, n)
) : size_t(n) = let
//
fun
loop
{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]
```

Clearly, the implemented function strptr_length computes the length of a given C-string.

Please find the entirety of the above presented code on-line.