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.