Compiles to c , but fails after that

Google Group
1

Hi,

I am unable to compile following code in ATS/Postiats version 0.0.4 :

E#include “share/atspre_define.hats”
#include "share/atspre_staload.hats"
staload
UN = “prelude/SATS/unsafe.sats”

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,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)

fun{a:t@ype}
make_nil_list () : (sl_v (a,0,null) | ptr null) =
(slseg_v_nil () | $UN.cast{ptr null}(0))

fun{a:t@ype}
con_alloc ()
: [l:agz][k:addr] ((a,ptr k) @ l , mfree_gc_v (l) | ptr l) = let

val [l:addr] (pf , pfgc | p) = malloc_gc(sizeof<{k:addr} (a,ptr k)>)
prval pf = __assert(pf) where {
extern praxi __assert {k:addr}
(pf : b0ytes (sizeof (@(a,ptr k)) ) @ l ) : (a,ptr k) @ l
}
in
(pf,pfgc | p)
end

fun{a:t@ype}
cons {n:nat}{l:addr} (pf: sl_v(a,n,l) | lstp : ptr l , x:a)
//: [ll:agz] ((a , ptr l) @ ll , sl_v(a,n+1,ll) | ptr ll) = let
: [ll:agz] (sl_v(a,n+1,ll) | ptr ll) = let

val (pfn ,_ | pn) = con_alloc ()
val () = ptr_set (pfn | pn , (x,lstp))
prval npf = slseg_v_cons (pfn , pf)
in
(npf | pn)
end

val (pf | lst_p) = make_nil_list ()
(* compiles succesfully , if I comment the line below *)
val (pf | lst_p) = cons (pf | lst_p , 100) //???

implement main0 () = ()
nter code here…

Problem seem to be in this “val (pf | lst_p) = cons (pf | lst_p , 100)
” part of the code

Thanks

2

I took a quick look at the course.

I think ATS is very well-suited for this kind of thing. I will be happy
to offer a hand if you ever get stuck.

If it is not too much of a trouble, I suggest that you make your code
publicly available. I am pretty sure that many people should be interested
in reading it.

Right now, a serious problem with ATS is that there is very little
on-line source of information for people interested in learning it. So it is
my hope that everyone learning ATS right now could also help his or her
fellow learners.

By the way, encoding proofs of theorems inside ATS is an excellent way to
gain understanding of the theorems. For instance, I had great difficulty
with
Yoneda Lemma in category theory. Once I was able to implement it in ATS
a couple days ago, I felt that I had gained solid understanding of it.
Actually,
I right now feel that Yoneda Lemma is so “trivial” :slight_smile:

Cheers!On Thursday, January 9, 2014 11:21:28 AM UTC-5, chota singh wrote:

Thanks , code now compiles

At present I am only trying to learn different concepts in ATS , I already
know functional style of programming , but have no experience with
dependent types and proofs.

I have kept whole of this year for learning ATS and Linear Algebra :slight_smile: .

At some stage I want to try to convert some example from the course
15-122: Principles of Imperative Computation (Sp'13) on my own using ATS , they are
using contracts , invariants to reason with program correctness.

(* I thing my previous(nearly same) reply was lost by google *)
Thanks

On Thursday, January 9, 2014 8:20:52 PM UTC+5:30, gmhwxi wrote:

I want to point out that doing programming in this style is very good to
learn various concepts in ATS. However, this programming style is not
meant to be practical.

On Thursday, January 9, 2014 6:07:55 AM UTC-5, chota singh wrote:

Hi,

I am unable to compile following code in ATS/Postiats version 0.0.4 :

#include “share/atspre_define.hats”
#include “share/atspre_staload.hats”
staload
UN = “prelude/SATS/unsafe.sats”

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,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)

fun{a:t@ype}
make_nil_list () : (sl_v (a,0,null) | ptr null) =
(slseg_v_nil () | $UN.cast{ptr null}(0))

fun{a:t@ype}
con_alloc ()
: [l:agz][k:addr] ((a,ptr k) @ l , mfree_gc_v (l) | ptr l) = let

val [l:addr] (pf , pfgc | p) = malloc_gc(sizeof<{k:addr} (a,ptr k)>)
prval pf = __assert(pf) where {
extern praxi __assert {k:addr}
(pf : b0ytes (sizeof (@(a,ptr k)) ) @ l ) : (a,ptr k) @ l
}
in
(pf,pfgc | p)
end

fun{a:t@ype}
cons {n:nat}{l:addr} (pf: sl_v(a,n,l) | lstp : ptr l , x:a)
//: [ll:agz] ((a , ptr l) @ ll , sl_v(a,n+1,ll) | ptr ll) = let
: [ll:agz] (sl_v(a,n+1,ll) | ptr ll) = let

val (pfn ,_ | pn) = con_alloc ()
val () = ptr_set (pfn | pn , (x,lstp))
prval npf = slseg_v_cons (pfn , pf)
in
(npf | pn)
end

val (pf | lst_p) = make_nil_list ()
(* compiles succesfully , if I comment the line below *)
val (pf | lst_p) = cons (pf | lst_p , 100) //???

implement main0 () = ()
nter code here…

Problem seem to be in this "val (pf | lst_p) = cons (pf | lst_p ,
100) " part of the code

Thanks

3

I want to point out that doing programming in this style is very good to
learn various concepts in ATS. However, this programming style is not
meant to be practical.On Thursday, January 9, 2014 6:07:55 AM UTC-5, chota singh wrote:

Hi,

I am unable to compile following code in ATS/Postiats version 0.0.4 :

#include “share/atspre_define.hats”
#include “share/atspre_staload.hats”
staload
UN = “prelude/SATS/unsafe.sats”

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,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)

fun{a:t@ype}
make_nil_list () : (sl_v (a,0,null) | ptr null) =
(slseg_v_nil () | $UN.cast{ptr null}(0))

fun{a:t@ype}
con_alloc ()
: [l:agz][k:addr] ((a,ptr k) @ l , mfree_gc_v (l) | ptr l) = let

val [l:addr] (pf , pfgc | p) = malloc_gc(sizeof<{k:addr} (a,ptr k)>)
prval pf = __assert(pf) where {
extern praxi __assert {k:addr}
(pf : b0ytes (sizeof (@(a,ptr k)) ) @ l ) : (a,ptr k) @ l
}
in
(pf,pfgc | p)
end

fun{a:t@ype}
cons {n:nat}{l:addr} (pf: sl_v(a,n,l) | lstp : ptr l , x:a)
//: [ll:agz] ((a , ptr l) @ ll , sl_v(a,n+1,ll) | ptr ll) = let
: [ll:agz] (sl_v(a,n+1,ll) | ptr ll) = let

val (pfn ,_ | pn) = con_alloc ()
val () = ptr_set (pfn | pn , (x,lstp))
prval npf = slseg_v_cons (pfn , pf)
in
(npf | pn)
end

val (pf | lst_p) = make_nil_list ()
(* compiles succesfully , if I comment the line below *)
val (pf | lst_p) = cons (pf | lst_p , 100) //???

implement main0 () = ()
nter code here…

Problem seem to be in this "val (pf | lst_p) = cons (pf | lst_p ,
100) " part of the code

Thanks

4

Suppose that the code is contained in a file of the
name ‘abcde.dats’. Here is the command-line I used to compile it:

patscc -DATS_MEMALLOC_LIBC -o abcde abcde.dats

Changes needed:

con_alloc () → con_alloc () // without , the compiler cannot figure
out how much memory is needed.

Suggestions:

sizeof<{k:addr} (a,ptr k)>)

should be changed into

sizeof<[k:addr] (a, ptr(k))>

which should be changed into

sizeof<(a, ptr)>

because ptr(k) and ptr have the same size.On Thursday, January 9, 2014 6:07:55 AM UTC-5, chota singh wrote:

Hi,

I am unable to compile following code in ATS/Postiats version 0.0.4 :

E#include “share/atspre_define.hats”
#include “share/atspre_staload.hats”
staload
UN = “prelude/SATS/unsafe.sats”

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,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)

fun{a:t@ype}
make_nil_list () : (sl_v (a,0,null) | ptr null) =
(slseg_v_nil () | $UN.cast{ptr null}(0))

fun{a:t@ype}
con_alloc ()
: [l:agz][k:addr] ((a,ptr k) @ l , mfree_gc_v (l) | ptr l) = let

val [l:addr] (pf , pfgc | p) = malloc_gc(sizeof<{k:addr} (a,ptr k)>)
prval pf = __assert(pf) where {
extern praxi __assert {k:addr}
(pf : b0ytes (sizeof (@(a,ptr k)) ) @ l ) : (a,ptr k) @ l
}
in
(pf,pfgc | p)
end

fun{a:t@ype}
cons {n:nat}{l:addr} (pf: sl_v(a,n,l) | lstp : ptr l , x:a)
//: [ll:agz] ((a , ptr l) @ ll , sl_v(a,n+1,ll) | ptr ll) = let
: [ll:agz] (sl_v(a,n+1,ll) | ptr ll) = let

val (pfn ,_ | pn) = con_alloc ()
val () = ptr_set (pfn | pn , (x,lstp))
prval npf = slseg_v_cons (pfn , pf)
in
(npf | pn)
end

val (pf | lst_p) = make_nil_list ()
(* compiles succesfully , if I comment the line below *)
val (pf | lst_p) = cons (pf | lst_p , 100) //???

implement main0 () = ()
nter code here…

Problem seem to be in this "val (pf | lst_p) = cons (pf | lst_p ,
100) " part of the code

Thanks
5

Thanks , code now compiles

At present I am only trying to learn different concepts in ATS , I already
know functional style of programming , but have no experience with
dependent types and proofs.

I have kept whole of this year for learning ATS and Linear Algebra :slight_smile: .

At some stage I want to try to convert some example from the course
15-122: Principles of Imperative Computation (Sp'13) on my own using ATS , they are
using contracts , invariants to reason with program correctness.

(* I thing my previous(nearly same) reply was lost by google *)
ThanksOn Thursday, January 9, 2014 8:20:52 PM UTC+5:30, gmhwxi wrote:

I want to point out that doing programming in this style is very good to
learn various concepts in ATS. However, this programming style is not
meant to be practical.

On Thursday, January 9, 2014 6:07:55 AM UTC-5, chota singh wrote:

Hi,

I am unable to compile following code in ATS/Postiats version 0.0.4 :

#include “share/atspre_define.hats”
#include “share/atspre_staload.hats”
staload
UN = “prelude/SATS/unsafe.sats”

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,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)

fun{a:t@ype}
make_nil_list () : (sl_v (a,0,null) | ptr null) =
(slseg_v_nil () | $UN.cast{ptr null}(0))

fun{a:t@ype}
con_alloc ()
: [l:agz][k:addr] ((a,ptr k) @ l , mfree_gc_v (l) | ptr l) = let

val [l:addr] (pf , pfgc | p) = malloc_gc(sizeof<{k:addr} (a,ptr k)>)
prval pf = __assert(pf) where {
extern praxi __assert {k:addr}
(pf : b0ytes (sizeof (@(a,ptr k)) ) @ l ) : (a,ptr k) @ l
}
in
(pf,pfgc | p)
end

fun{a:t@ype}
cons {n:nat}{l:addr} (pf: sl_v(a,n,l) | lstp : ptr l , x:a)
//: [ll:agz] ((a , ptr l) @ ll , sl_v(a,n+1,ll) | ptr ll) = let
: [ll:agz] (sl_v(a,n+1,ll) | ptr ll) = let

val (pfn ,_ | pn) = con_alloc ()
val () = ptr_set (pfn | pn , (x,lstp))
prval npf = slseg_v_cons (pfn , pf)
in
(npf | pn)
end

val (pf | lst_p) = make_nil_list ()
(* compiles succesfully , if I comment the line below *)
val (pf | lst_p) = cons (pf | lst_p , 100) //???

implement main0 () = ()
nter code here…

Problem seem to be in this "val (pf | lst_p) = cons (pf | lst_p ,
100) " part of the code

Thanks

6

Here is a simpler way to implement con_alloc:

fun{a:@ype}
con_alloc (): [l:agz] ((a, ptr)? @ l, mfree_gc_v (l) | ptr (l)) =
ptr_alloc<(a,ptr)> ()On Thursday, January 9, 2014 6:07:55 AM UTC-5, chota singh wrote:

Hi,

I am unable to compile following code in ATS/Postiats version 0.0.4 :

#include “share/atspre_define.hats”
#include “share/atspre_staload.hats”
staload
UN = “prelude/SATS/unsafe.sats”

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,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)

fun{a:t@ype}
make_nil_list () : (sl_v (a,0,null) | ptr null) =
(slseg_v_nil () | $UN.cast{ptr null}(0))

fun{a:t@ype}
con_alloc ()
: [l:agz][k:addr] ((a,ptr k) @ l , mfree_gc_v (l) | ptr l) = let

val [l:addr] (pf , pfgc | p) = malloc_gc(sizeof<{k:addr} (a,ptr k)>)
prval pf = __assert(pf) where {
extern praxi __assert {k:addr}
(pf : b0ytes (sizeof (@(a,ptr k)) ) @ l ) : (a,ptr k) @ l
}
in
(pf,pfgc | p)
end

fun{a:t@ype}
cons {n:nat}{l:addr} (pf: sl_v(a,n,l) | lstp : ptr l , x:a)
//: [ll:agz] ((a , ptr l) @ ll , sl_v(a,n+1,ll) | ptr ll) = let
: [ll:agz] (sl_v(a,n+1,ll) | ptr ll) = let

val (pfn ,_ | pn) = con_alloc ()
val () = ptr_set (pfn | pn , (x,lstp))
prval npf = slseg_v_cons (pfn , pf)
in
(npf | pn)
end

val (pf | lst_p) = make_nil_list ()
(* compiles succesfully , if I comment the line below *)
val (pf | lst_p) = cons (pf | lst_p , 100) //???

implement main0 () = ()
nter code here…

Problem seem to be in this "val (pf | lst_p) = cons (pf | lst_p ,
100) " part of the code

Thanks