nice code
thanks !
Hello Cyrille,
unfortunately it does not typecheck :
Here’s something that does typecheck:
In particular, I put an assert (how do you plan to handle a broken
invariant? presently the code will simply fail) and put the linear proofs
back, so as to appease the typechecker (it complains that a linear value is
consumed, i.e. not preserved otherwise).> Le samedi 3 janvier 2015 06:38:31 UTC+1, gmhwxi a écrit :
You can declare inc_… as follows:
extern
fun
inc_stream_vt_2
(stream: !stream_vt >> _): voidimplement inc_stream_vt_2(stream) = let
val (pf, pfgc | p) = stream
val () = p->pos := p->pos + 1
in
// $UN.castvwtp0{stream_vt}((pf, pfgc | p))
endOn Friday, January 2, 2015 11:03:23 PM UTC-5, Cyrille Duret wrote:
and what would be the way accessing and modifying that structure without
consuming the linear value ?I just made it worked with this way (I have to consume the pointer at
each call)extern fun inc_stream_vt_2(stream: stream_vt): stream_vt
implement inc_stream_vt_2(stream) = let
val (pf, pfgc | p) = stream
val () = p->pos := p->pos + 1
in
$UN.castvwtp0{stream_vt}((pf, pfgc | p))
endthanks
Le jeudi 1 janvier 2015 11:14:24 UTC+1, Cyrille Duret a écrit :
thanks a lot
Please update your version of ATS2.On Wed, Jan 7, 2015 at 11:31 PM, Cyrille Duret cdu...@gmail.com wrote:
I could not compile this sample neither with gcc nor clang :
gcc says :
patscc -DATS_MEMALLOC_LIBC -o qa-list qa-list-2015-01-03.dats
qa-list-2015-01-03_dats.c: In function
‘_057_usr_057_users_057_cydu_057_programming_057_ATS_057_parser_057_test_057_qa_055_list_055_2015_055_01_055_03_056_dats__sstream_create’:
qa-list-2015-01-03_dats.c:497:1: error: request for member ‘atslab__2’ in
something not a structure or unionclang says :
patscc -DATS_MEMALLOC_LIBC -o qa-list qa-list-2015-01-03.dats
qa-list-2015-01-03_dats.c:497:1: error: member reference base type
‘atstype_ptrk’ (aka ‘void *’) is
not a structure or union
ATSINSstore_fltrec_ofs (tmpret0, atstkind_type(atstype_ptrk), atslab__2,
tmp1) ;^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/usr/local/lib/ats2-postiats-0.1.6/ccomp/runtime/pats_ccomp_instrset.h:311:60:
note: expanded from
macro ‘ATSINSstore_fltrec_ofs’
#define ATSINSstore_fltrec_ofs(tmp, tyrec, lab, val) ((tmp).lab = val)
~~~~~^
1 error generated.Le samedi 3 janvier 2015 21:28:12 UTC+1, gmhwxi a écrit :
I rewrote this example and put it on-line:
https://github.com/githwxi/ATS-Postiats/blob/master/doc/
EXAMPLE/ATS-QA-LIST/qa-list-2015-01-03.datsOn Saturday, January 3, 2015 11:56:08 AM UTC-5, gmhwxi wrote:
This one typechecks:
#include “share/atspre_staload.hats”
staload UN = “prelude/SATS/unsafe.sats”absvtype stream_vt = ptr // for string streams
extern fun create_stream_vt(): stream_vt
extern fun inc_stream_vt(stream: !stream_vt >> _): void
extern fun free_stream_vt(stream: stream_vt): voidlocal
vtypedef stream_struct_vt(n:int) = @{
data= Strptr1,
size= size_t(n),
pos= sizeLte(n)
}
vtypedef stream_struct_vt = [n:nat] stream_struct_vt(n)assume stream_vt = [l:addr;n:nat] (stream_struct_vt(n)@l, mfree_gc_v(l
) | ptr(l))
in
implement create_stream_vt() = let
val (pf, pfgc | p) = ptr_alloc<stream_struct_vt(0)> ()
val () = p->data := string0_copy(“content of a text file”)
val () = p->size := i2sz(13)
val () = p->pos := i2sz(0)
in
$UN.castvwtp0{stream_vt}((pf, pfgc | p))
endimplement inc_stream_vt(stream) = let
val p = stream.2
val pos = p->pos
val size = p->size
val () = assertloc(pos < size)
val () = p->pos := pos + 1
in
endimplement free_stream_vt(stream) = let
val (pf, pfgc | p) = stream
val () = strptr_free(p->data)
in
ptr_free{stream_struct_vt(0)?}(pfgc, pf| p)
end
endimplement main0(argc, argv) = let
val stream = create_stream_vt()
val () = inc_stream_vt(stream)
in
free_stream_vt(stream)
endWhat do you mean by broken invariant
‘p->pos := p->pos + 1’ does not typecheck when p->pos equals p->size.
On Saturday, January 3, 2015 11:13:13 AM UTC-5, Cyrille Duret wrote:
hi,
thanks it does indeed typecheck but compilation of generated C failed :linear_ref_dats.c: In function ‘057_usr_057_users_057_cydu
057_programming_057_ATS_057_parser_057_test_057_linear_
ref_056_dats__inc_stream_vt’:
linear_ref_dats.c:959:1: warning: dereferencing ‘void *’ pointer
[enabled by default]
linear_ref_dats.c:959:1: error: invalid use of void expressionWhat do you mean by broken invariant ?
Le samedi 3 janvier 2015 16:34:28 UTC+1, Artyom Shalkhakov a écrit :
Hello Cyrille,
On Saturday, January 3, 2015 8:42:02 PM UTC+6, Cyrille Duret wrote:
unfortunately it does not typecheck :
http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_
serve.php?mycode_url=http://pastebin.com/raw.php?i=4P34LVBfHere’s something that does typecheck:
#include "share/atspre_staload.hats"staload UN = "prelude/SATS/unsafe.sats" - Pastebin.com
In particular, I put an assert (how do you plan to handle a broken
invariant? presently the code will simply fail) and put the linear proofs
back, so as to appease the typechecker (it complains that a linear value is
consumed, i.e. not preserved otherwise).Le samedi 3 janvier 2015 06:38:31 UTC+1, gmhwxi a écrit :
You can declare inc_… as follows:
extern
fun
inc_stream_vt_2
(stream: !stream_vt >> _): voidimplement inc_stream_vt_2(stream) = let
val (pf, pfgc | p) = stream
val () = p->pos := p->pos + 1
in
// $UN.castvwtp0{stream_vt}((pf, pfgc | p))
endOn Friday, January 2, 2015 11:03:23 PM UTC-5, Cyrille Duret wrote:
and what would be the way accessing and modifying that structure
without consuming the linear value ?I just made it worked with this way (I have to consume the pointer
at each call)extern fun inc_stream_vt_2(stream: stream_vt): stream_vt
implement inc_stream_vt_2(stream) = let
val (pf, pfgc | p) = stream
val () = p->pos := p->pos + 1
in
$UN.castvwtp0{stream_vt}((pf, pfgc | p))
endthanks
Le jeudi 1 janvier 2015 11:14:24 UTC+1, Cyrille Duret a écrit :
thanks a lot
–
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 ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/1575acb8-570a-4e81-be69-7f2536208528%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/1575acb8-570a-4e81-be69-7f2536208528%40googlegroups.com?utm_medium=email&utm_source=footer
.
I rewrote this example and put it on-line:
https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATS-QA-LIST/qa-list-2015-01-03.datsOn Saturday, January 3, 2015 11:56:08 AM UTC-5, gmhwxi wrote:
This one typechecks:
#include “share/atspre_staload.hats”
staload UN = “prelude/SATS/unsafe.sats”absvtype stream_vt = ptr // for string streams
extern fun create_stream_vt(): stream_vt
extern fun inc_stream_vt(stream: !stream_vt >> _): void
extern fun free_stream_vt(stream: stream_vt): voidlocal
vtypedef stream_struct_vt(n:int) = @{
data= Strptr1,
size= size_t(n),
pos= sizeLte(n)
}
vtypedef stream_struct_vt = [n:nat] stream_struct_vt(n)assume stream_vt = [l:addr;n:nat] (stream_struct_vt(n)@l, mfree_gc_v(l)
| ptr(l))
in
implement create_stream_vt() = let
val (pf, pfgc | p) = ptr_alloc<stream_struct_vt(0)> ()
val () = p->data := string0_copy(“content of a text file”)
val () = p->size := i2sz(13)
val () = p->pos := i2sz(0)
in
$UN.castvwtp0{stream_vt}((pf, pfgc | p))
endimplement inc_stream_vt(stream) = let
val p = stream.2
val pos = p->pos
val size = p->size
val () = assertloc(pos < size)
val () = p->pos := pos + 1
in
endimplement free_stream_vt(stream) = let
val (pf, pfgc | p) = stream
val () = strptr_free(p->data)
in
ptr_free{stream_struct_vt(0)?}(pfgc, pf| p)
end
endimplement main0(argc, argv) = let
val stream = create_stream_vt()
val () = inc_stream_vt(stream)
in
free_stream_vt(stream)
endWhat do you mean by broken invariant
‘p->pos := p->pos + 1’ does not typecheck when p->pos equals p->size.
On Saturday, January 3, 2015 11:13:13 AM UTC-5, Cyrille Duret wrote:
hi,
thanks it does indeed typecheck but compilation of generated C failed :linear_ref_dats.c: In function
‘_057_usr_057_users_057_cydu_057_programming_057_ATS_057_parser_057_test_057_linear_ref_056_dats__inc_stream_vt’:
linear_ref_dats.c:959:1: warning: dereferencing ‘void *’ pointer [enabled
by default]
linear_ref_dats.c:959:1: error: invalid use of void expressionWhat do you mean by broken invariant ?
Le samedi 3 janvier 2015 16:34:28 UTC+1, Artyom Shalkhakov a écrit :
Hello Cyrille,
On Saturday, January 3, 2015 8:42:02 PM UTC+6, Cyrille Duret wrote:
unfortunately it does not typecheck :
Here’s something that does typecheck:
#include "share/atspre_staload.hats"staload UN = "prelude/SATS/unsafe.sats" - Pastebin.com
In particular, I put an assert (how do you plan to handle a broken
invariant? presently the code will simply fail) and put the linear proofs
back, so as to appease the typechecker (it complains that a linear value is
consumed, i.e. not preserved otherwise).Le samedi 3 janvier 2015 06:38:31 UTC+1, gmhwxi a écrit :
You can declare inc_… as follows:
extern
fun
inc_stream_vt_2
(stream: !stream_vt >> _): voidimplement inc_stream_vt_2(stream) = let
val (pf, pfgc | p) = stream
val () = p->pos := p->pos + 1
in
// $UN.castvwtp0{stream_vt}((pf, pfgc | p))
endOn Friday, January 2, 2015 11:03:23 PM UTC-5, Cyrille Duret wrote:
and what would be the way accessing and modifying that structure
without consuming the linear value ?I just made it worked with this way (I have to consume the pointer at
each call)extern fun inc_stream_vt_2(stream: stream_vt): stream_vt
implement inc_stream_vt_2(stream) = let
val (pf, pfgc | p) = stream
val () = p->pos := p->pos + 1
in
$UN.castvwtp0{stream_vt}((pf, pfgc | p))
endthanks
Le jeudi 1 janvier 2015 11:14:24 UTC+1, Cyrille Duret a écrit :
thanks a lot
hi,
thanks it does indeed typecheck but compilation of generated C failed :
linear_ref_dats.c: In function
‘_057_usr_057_users_057_cydu_057_programming_057_ATS_057_parser_057_test_057_linear_ref_056_dats__inc_stream_vt’:
linear_ref_dats.c:959:1: warning: dereferencing ‘void *’ pointer [enabled
by default]
linear_ref_dats.c:959:1: error: invalid use of void expression
What do you mean by broken invariant ?
;-)Le samedi 3 janvier 2015 16:34:28 UTC+1, Artyom Shalkhakov a écrit :
Hello Cyrille,
On Saturday, January 3, 2015 8:42:02 PM UTC+6, Cyrille Duret wrote:
unfortunately it does not typecheck :
Here’s something that does typecheck:
#include "share/atspre_staload.hats"staload UN = "prelude/SATS/unsafe.sats" - Pastebin.com
In particular, I put an assert (how do you plan to handle a broken
invariant? presently the code will simply fail) and put the linear proofs
back, so as to appease the typechecker (it complains that a linear value is
consumed, i.e. not preserved otherwise).Le samedi 3 janvier 2015 06:38:31 UTC+1, gmhwxi a écrit :
You can declare inc_… as follows:
extern
fun
inc_stream_vt_2
(stream: !stream_vt >> _): voidimplement inc_stream_vt_2(stream) = let
val (pf, pfgc | p) = stream
val () = p->pos := p->pos + 1
in
// $UN.castvwtp0{stream_vt}((pf, pfgc | p))
endOn Friday, January 2, 2015 11:03:23 PM UTC-5, Cyrille Duret wrote:
and what would be the way accessing and modifying that structure
without consuming the linear value ?I just made it worked with this way (I have to consume the pointer at
each call)extern fun inc_stream_vt_2(stream: stream_vt): stream_vt
implement inc_stream_vt_2(stream) = let
val (pf, pfgc | p) = stream
val () = p->pos := p->pos + 1
in
$UN.castvwtp0{stream_vt}((pf, pfgc | p))
endthanks
Le jeudi 1 janvier 2015 11:14:24 UTC+1, Cyrille Duret a écrit :
thanks a lot
A reference (ref) is persistent; it is non-linear and thus cannot be freed.On Thursday, January 1, 2015 12:54:22 AM UTC-5, Cyrille Duret wrote:
hello,
I am trying to implement the linear version of the proposed tokenizer here
but I have some problems.the post I am referred to :
I doing basically this :
#include “share/atspre_staload.hats”
absvtype stream_vt = ptr // for string streams
extern fun create_stream_vt(): stream_vt
//extern fun free_stream_vt(stream: stream_vt): voidlocal
staload UN = “prelude/SATS/unsafe.sats”(viewtypedef stream_struct_vt = [n:nat] @{
data= Strptr1,
size= size_t(n),
pos= sizeLte(n)
})viewtypedef stream_struct_vt = @{
data= Strptr1,
size= int,
pos= int
}assume stream_vt = ref(stream_struct_vt)
in
implement create_stream_vt() = let
val (pf, pfgc | p) = ptr_alloc<stream_struct_vt> ()
val () = p->data := string0_copy(“content of a text file”)
val () = p->size := 13
val () = p->pos := 0
in
$UN.castvwtp0{stream_vt}((pf, pfgc | p))
end(implement free_stream_vt(stream) = let
val (pf, pfgc | p) = ref_vtakeout stream
in
ptr_free(pfgc, pf| p)
end)end
implement main0(argc, argv) = ()
(implement main0(argc, argv) = let
val stream = create_stream_vt()
in
free_stream_vt(stream)
end)I have two main problems :
- when I change the definition of stream_struct_vt with [n:nat] dependent
type, I cannot typecheck this code- I cannot find a way of freeing this linear structure my function
free_stream_vt does not typecheck at all (ptr_free take only t@ype and no
version for viewt@ypethanks for your help, and happy new year