次のデータ観 strbuf_v はC言語文字列の概念を補足しています。C言語文字列は NULL 文字で終端する非 NULL 文字の列から成り立っています:
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))
C言語文字列が与えられたとき、その最初の文字には常にアクセスできます; もしその文字が NULL であった場合、そのC言語文字列は空です; もしその文字が NULL でなかった場合、そのC言語文字列は空ではありません。 strptr_is_nil の次の実装は、C言語文字列が空か空でないかを判定するこの単純な方法を正確に実装しています:
// 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))] )
次の実装はデータ観 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]
上記で示したコード全体は オンライン から入手できます。