How to return proof function using vtakeout?

Google Group
1

Suppose I want a function that given a proof of non empty list return a
tuple consisting of proof of at-view of first node and a proof function
that takes that at-view and returns the original list.

I am unable to make such function , here is the code for my attempt :

dataview slseg_v (a:t@ype, int(len) , addr(beg) , addr(end)) =
| {l:addr} slseg_v_nil(a,0,l,l) of ()
| {n:nat} {l_fst : agz} {l_nxt :addr} {l_end : addr}
slseg_v_cons (a,n+1,l_fst,l_end) of
( (a,ptr l_nxt) @ l_fst , slseg_v(a , n , l_nxt , l_end))

viewdef sl_v
(a:t@ype , n:int, l:addr) = slseg_v(a,n,l,null)

extern
prfun lst2at{a:t@ype} {l:agz} {n:nat | n > 0}
(pf1: sl_v(a,n,l) ) :
vtakeout (sl_v (a,n,l) , [m:addr] (a,ptr m) @ l)
// ((a,ptr m) @ l , (a,ptr m) @ l -> sl_v (a,n,l))

primplement
lst2at (pf1) = let
prval slseg_v_cons (pf_at , pf_lst) = pf1
in
(pf_at , llam pf_at = (pf_at , pf_lst))
end

Thanks

2

Following is a version that type-checks. The syntax #[… | …] is for
forming a value of existential type.

dataview
slseg_v
(
a:t@ype, int(len) , addr(beg) , addr(end)
) =
| {l:addr} slseg_v_nil(a,0,l,l) of ()
| {n:nat} {l_fst : agz} {l_nxt :addr} {l_end : addr}
slseg_v_cons (a,n+1,l_fst,l_end) of
( (a,ptr l_nxt) @ l_fst , slseg_v(a , n , l_nxt , l_end))

viewdef sl_v (a:t@ype , n:int, l:addr) = slseg_v(a,n,l,null)

extern
prfun
lst2at{a:t@ype}{l:agz}{n:int | n > 0}
(pf1: sl_v(a,n,l)) : [m:addr] vtakeout (sl_v (a,n,l), (a,ptr m) @ l)

primplement
lst2at (pf1) = let
prval slseg_v_cons (pf_at , pf_lst) = pf1
in
#[… | (pf_at , llam pf_at = slseg_v_cons (pf_at , pf_lst))]
end // end of [lst2at]On Sunday, January 12, 2014 8:38:50 AM UTC-5, chota singh wrote:

Suppose I want a function that given a proof of non empty list return a
tuple consisting of proof of at-view of first node and a proof function
that takes that at-view and returns the original list.

I am unable to make such function , here is the code for my attempt :

dataview slseg_v (a:t@ype, int(len) , addr(beg) , addr(end)) =
| {l:addr} slseg_v_nil(a,0,l,l) of ()
| {n:nat} {l_fst : agz} {l_nxt :addr} {l_end : addr}
slseg_v_cons (a,n+1,l_fst,l_end) of
( (a,ptr l_nxt) @ l_fst , slseg_v(a , n , l_nxt , l_end))

viewdef sl_v
(a:t@ype , n:int, l:addr) = slseg_v(a,n,l,null)

extern
prfun lst2at{a:t@ype} {l:agz} {n:nat | n > 0}
(pf1: sl_v(a,n,l) ) :
vtakeout (sl_v (a,n,l) , [m:addr] (a,ptr m) @ l)
// ((a,ptr m) @ l , (a,ptr m) @ l → sl_v (a,n,l))

primplement
lst2at (pf1) = let
prval slseg_v_cons (pf_at , pf_lst) = pf1
in
(pf_at , llam pf_at = (pf_at , pf_lst))
end

Thanks

3

Thanks it now compiles . I just realize that I had also forgot to put the
constructor in my original post :slight_smile: .On Sunday, January 12, 2014 10:09:47 PM UTC+5:30, gmhwxi wrote:

Following is a version that type-checks. The syntax #[… | …] is for
forming a value of existential type.

dataview
slseg_v
(
a:t@ype, int(len) , addr(beg) , addr(end)
) =
| {l:addr} slseg_v_nil(a,0,l,l) of ()
| {n:nat} {l_fst : agz} {l_nxt :addr} {l_end : addr}
slseg_v_cons (a,n+1,l_fst,l_end) of
( (a,ptr l_nxt) @ l_fst , slseg_v(a , n , l_nxt , l_end))

viewdef sl_v (a:t@ype , n:int, l:addr) = slseg_v(a,n,l,null)

extern
prfun
lst2at{a:t@ype}{l:agz}{n:int | n > 0}
(pf1: sl_v(a,n,l)) : [m:addr] vtakeout (sl_v (a,n,l), (a,ptr m) @ l
)

primplement
lst2at (pf1) = let
prval slseg_v_cons (pf_at , pf_lst) = pf1
in
#[… | (pf_at , llam pf_at = slseg_v_cons (pf_at , pf_lst))]
end // end of [lst2at]

On Sunday, January 12, 2014 8:38:50 AM UTC-5, chota singh wrote:

Suppose I want a function that given a proof of non empty list return a
tuple consisting of proof of at-view of first node and a proof function
that takes that at-view and returns the original list.

I am unable to make such function , here is the code for my attempt :

dataview slseg_v (a:t@ype, int(len) , addr(beg) , addr(end)) =
| {l:addr} slseg_v_nil(a,0,l,l) of ()
| {n:nat} {l_fst : agz} {l_nxt :addr} {l_end : addr}
slseg_v_cons (a,n+1,l_fst,l_end) of
( (a,ptr l_nxt) @ l_fst , slseg_v(a , n , l_nxt , l_end))

viewdef sl_v
(a:t@ype , n:int, l:addr) = slseg_v(a,n,l,null)

extern
prfun lst2at{a:t@ype} {l:agz} {n:nat | n > 0}
(pf1: sl_v(a,n,l) ) :
vtakeout (sl_v (a,n,l) , [m:addr] (a,ptr m) @ l)
// ((a,ptr m) @ l , (a,ptr m) @ l → sl_v (a,n,l))

primplement
lst2at (pf1) = let
prval slseg_v_cons (pf_at , pf_lst) = pf1
in
(pf_at , llam pf_at = (pf_at , pf_lst))
end

Thanks