I'm trying to use dataviewtypes to implement a growable, malloc allocated
vector type.
I defined the vector type like so:
dataview vector_v (a:vt@ype+, addr, int) =
| {l:addr} vector_v_nil (a, l, 0)
| {l:addr} {n:nat} vector_v_cons (a, l, n+1) of (a? @ l, vector_v (a,
l+sizeof(a), n))
datavtype vector_vt (a:vt@ype+, addr, int) =
| {l:addr} {n:nat} vector_vt(a, l, n) of (vector_v (a, l, n) | ptr(l))
I want to write a proof function to convert the view bytes_v(l, n *
sizeof(a)) (= @[byte?][n] @ l) to vector_v (a, l, n),
but I'm confused by some conflicting requirements given by patscc. I've
written these functions:
praxi bytes_v_to_at_view :
{a:vt0p}{l:addr}
( bytes_v(l, sizeof(a)) ) -> a? @ l
prfun bytes_v_to_vector_v{a:vt0p}{l:agz}{n:pos} (
pf: bytes_v (l, n * sizeof(a))
):<> vector_v (a, l, n)
primplement bytes_v_to_vector_v{a}{l}{n} (pf) = let
prfun loop{n:nat} .<n>. ( pf: bytes_v(l, n * sizeof(a)) ): vector_v(a, l,
n) =
sif n > 0 then let
prval (pf1, pf2bytes) =
bytes_v_split{l}{n*sizeof(a)}{sizeof(a)}(pf) // should return (pf1: bytes_v
(l, sizeof(a)), pf2bytes: bytes_v (l+sizeof(a), (n-1)*sizeof(a)))
prval pfa = bytes_v_to_at_view(pf1)
in
vector_v_cons (pfa, loop(pf2bytes))
end
else
vector_v_nil ()
in
loop(pf)
end
First, I'm not sure how else to write bytes_v_to_at_view. Is a praxi
appropriate here? Wouldn't a
castfn make more sense since what I'm after is a pointer cast? I thought
praxi was intended for
stating axioms.
Second, patscc reports two error messages regarding bytes_v_to_vector_v.
The first is that the dynamic variable
pf is consumed but needs to be retained by bytes_v_to_vector_v, and the
second is that pf is retained but needs to
be consumed by loop. pf is described as a "dynamic variable" of
bytes_v_to_vector_v, but a "linear dynamic variable"
of loop.
This is all very confusing. Is pf a linear variable in one context, but not
the other? Shouldn't it be a static variable?
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/4820775f-70d0-4578-b42b-1643908b29c8%40googlegroups.com.
