Here is some code that may be helpful: https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST30/struct.dats
On Friday, August 26, 2016 at 8:36:03 AM UTC-4, Kiwamu Okabe wrote: > > So, I think I understand somethings... > > > https://github.com/jats-ug/practice-ats/blob/d19b4a2739a332158a08d1deabe25d9eef71388a/mutual_record/main.dats > > > https://github.com/jats-ug/practice-ats/blob/d19b4a2739a332158a08d1deabe25d9eef71388a/mutual_struct/main.dats > > > Following define doesn't make sense. > > ``` > vtypedef bar = @{ x= int, p= [l:addr] (foo@l | ptr(l)) } > vtypedef foo = $extype_struct"struct foo" of { > x = int, > p = [l:addr] (bar@l | ptr(l)) > } > ``` > > Following is good style: > > ``` > vtypedef foo = @{ x= int, p= [l:addr] ptr(l) } > vtypedef bar = $extype_struct"struct bar" of { > x = int, > p = [l:addr] ptr(l) > } > ``` > > Because, any function can't watch linear proof inside of vtypedef. > If we would like to specify the linear proof, we should dump the > vtypedef and add the proof as following: > > ``` > fun print_foo' {l1,l2:addr} (pffoo: !(@{ x= int, p= ptr(l2) })@l1, > pfbar: !bar@l2 | p: ptr(l1)): void = { > val () = println! ("foo.x = ", p->x) > val () = println! ("bar.x = ", p->p->x) > } > ``` > > Is it correct? > > Best regards, > -- > Kiwamu Okabe > -- 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 [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/48e83245-ece6-4ed2-a16b-1d6b47783a87%40googlegroups.com.
