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): void
local
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))
end
implement 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
end
implement 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
end
implement main0(argc, argv) = let
val stream = create_stream_vt()
val () = inc_stream_vt(stream)
in
free_stream_vt(stream)
end
What 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 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 :
http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=http://pastebin.com/raw.php?i=4P34LVBf
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 >> _): void
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))
end
On 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))
end
thanks
Le jeudi 1 janvier 2015 11:14:24 UTC+1, Cyrille Duret a écrit :
thanks a lot
