I went ahead to fix several issues.
1)
The built-in constraint-solver of ATS cannot handle integer inequality
involving
multiplication. You may want to use Z3 for constriant-solving. It should
give you a much
better experience.
2)
The typechecker does not know that a zero-length bytes_v contains no
resources.
It is the programmers obligation to eliminate it.
3. The original loop did not work (as it was not polymorphic on 'l'); it
has been fixed.
In practice, I would just skip proving bytes_v_to_vector and treat it as a
praxi instead:
Theorems are "always" correctly stated but implementations "always" contain
bugs :)
############
staload UN = "prelude/SATS/unsafe.sats"
extern
praxi
bytes_v_to_at_view :
{a:vt0p}{l:addr}
( bytes_v(l, sizeof(a)) ) -> a? @ l
extern
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
stadef asz = sizeof(a)
prval () = $UN.prop_assert{asz >= 0}()
prfun
loop{l:addr}{n:nat} .<n>.
(pf: bytes_v(l, n * sizeof(a)) ): vector_v(a, l, n) =
sif n > 0 then
let
prval () = $UN.prop_assert{n*asz >= asz}()
prval (pf1, pf2bytes) =
bytes_v_split{l}{n*asz}{asz}(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{l+asz}{n-1}(pf2bytes))
end
else
let
prval () =
$UN.prop_assert{n*asz==0}()
prval () = array_v_unnil(pf)
in
vector_v_nil ()
end
in
loop(pf)
end
On Sun, Mar 3, 2019 at 11:13 AM Mark Thom <[email protected]> wrote:
> 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
> <https://groups.google.com/d/msgid/ats-lang-users/4820775f-70d0-4578-b42b-1643908b29c8%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
--
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/CAPPSPLoZXfbVycEwQ5ocBDBDkid9ufPxEQWWQbcgOJLzCOXeWw%40mail.gmail.com.
