implementation of linear tokenizer

[Cyrille Duret]

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 :

https://groups.google.com/forum/?fromgroups#!searchin/ats-lang-users/Tokenizer/ats-lang-users/SeVHXg8jcxA/ySwKcmvxbJsJ

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): void

local

  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@ype

thanks for your help, and happy new year ;-)

[gmhwxi]

Here is a version that typechecks:

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=http://pastebin.com/raw.php?i=9KdhUff3

I would prefer using datavtype (that is, dataviewtype) to implement stream_vt.

[gmhwxi]

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:

[Cyrille Duret]

thanks a lot ;-)

[Cyrille Duret]

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

[gmhwxi]

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

[Cyrille Duret]

unfortunately it does not typecheck :

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=http://pastebin.com/raw.php?i=4P34LVBf

[Cyrille Duret]

unfortunately it does not typecheck :

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=http://pastebin.com/raw.php?i=4P34LVBf

Le samedi 3 janvier 2015 06:38:31 UTC+1, gmhwxi a écrit :

[Artyom Shalkhakov]

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:

http://pastebin.com/AK84nLWt

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

[Cyrille Duret]

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 ?

;-)

[gmhwxi]

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.

[Hongwei Xi]

The following should fail at compile-time:

  implement inc_stream_vt(stream) = let

    val (pf, pfgc | p) = stream

    val () = p->pos := p->pos + 1

    val () = assertloc (p->pos <= p->size)

    val () = stream := (pf, pfgc | p) // this is incorrect as 'stream' is call-by-value

  in

  end

--
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/b65029d7-4f3c-4f19-a2ae-dbdbf64b272f%40googlegroups.com.

[gmhwxi]

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.dats

[Cyrille Duret]

nice code
thanks !

[Cyrille Duret]

nice code
thanks !

[Cyrille Duret]

nice code
thanks !

[Cyrille Duret]

nice code
thanks !

[Cyrille Duret]

nice code
thanks !

[Cyrille Duret]

nice code
thanks !

[Cyrille Duret]

nice code
thanks !

[gmhwxi]

Here is a dataviewtype-based implementation:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATS-QA-LIST/qa-list-2015-01-03-2.dats

What is nice here is that one does not need to deal with the free-view explicitly.

You need ATS2-github to test these examples.

On Saturday, January 3, 2015 9:22:41 PM UTC-5, Cyrille Duret wrote:

nice code
thanks !

[Cyrille Duret]

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 union

clang 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.

[Hongwei Xi]

Please update your version of ATS2.

--

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.

[Cyrille Duret]

Probably because I have the version from sourceforge : http://sourceforge.net/p/ats2-lang/code/ci/master/tree/

What are difference with https://github.com/githwxi/ATS-Postiats ?

the install of ATS2-github seems a bit painfull (have to install ATS1 before)

[Hongwei Xi]

What is your version of ATS2? ATS2-0.1.6 should work.

--

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/b0af2572-d40d-4c2f-b3a9-7cba8c3ef4aa%40googlegroups.com.

[Cyrille Duret]

yes I updated to 0.1.6 now and its fine