How to use mutual struct?

[Kiwamu Okabe]

Hi all,

Now I'm trying to define mutual struct:

https://github.com/jats-ug/practice-ats/blob/master/struct/main.dats

They are defined following in C:

```
{^
struct foo;
struct bar {
int a;
struct foo *p;
};
struct foo {
int b;
struct bar *p;
};
%}
```

And they are imported into ATS world with following:

```
absvt@ype struct_foo
vtypedef struct_bar = $extype_struct"struct bar" of {
a = int,
p = [l:addr] (struct_foo@l | ptr l)
}
vtypedef struct_foo_impl = $extype_struct"struct foo" of {
a = int,
p = [l:addr] (struct_bar@l | ptr l)
}
assume struct_foo = struct_foo_impl
```

But the code using these causes compile error at ATS... What's wrong???

```
implement main0 () = {
var foo: struct_foo
var bar: struct_bar
// val () = foo.p := (view@bar | addr@bar) // Error!
// val () = bar.p := (view@foo | addr@foo) // Error!
val () = println! (foo.p)
val () = println! (bar.p)
// val () = println! (foo.a) // Error!
// val () = println! (bar.a) // Error!
}
```

Best regards,
--
Kiwamu Okabe at METASEPI DESIGN

[gmhwxi]

Recursion in views cannot be handled this way. You need to define
dataviews for this.

[Kiwamu Okabe]

Hi Hongwei,

On Sat, Aug 20, 2016 at 1:58 PM, gmhwxi <gmh...@gmail.com> wrote:
> Recursion in views cannot be handled this way. You need to define
> dataviews for this.

Umm...

Is it meaning that we can't import mutual struct directly?
I would like to translate struct definition in C into ATS, semi-automatically.

[Kiwamu Okabe]

Hi Hongwei,

On Sat, Aug 20, 2016 at 2:04 PM, Kiwamu Okabe <kiw...@debian.or.jp> wrote:
> On Sat, Aug 20, 2016 at 1:58 PM, gmhwxi <gmh...@gmail.com> wrote:
>> Recursion in views cannot be handled this way. You need to define
>> dataviews for this.
>

> Is it meaning that we can't import mutual struct directly?
> I would like to translate struct definition in C into ATS, semi-automatically.

Or, should I semi-automatically translate C struct into ATS dataview?
If I forget bit field in C language, I feel it may be reasonable...

# I hate the bit field!

[Kiwamu Okabe]

On Sat, Aug 20, 2016 at 1:58 PM, gmhwxi <gmh...@gmail.com> wrote:

> Recursion in views cannot be handled this way. You need to define
> dataviews for this.

The dataview can be used at interface between C and ATS?
Or we need cast the dataview into vtypedef at the interface?

[Kiwamu Okabe]

Hi Hongwei,

On Sun, Aug 21, 2016 at 8:16 AM, Kiwamu Okabe <kiw...@debian.or.jp> wrote:
> The dataview can be used at interface between C and ATS?
> Or we need cast the dataview into vtypedef at the interface?

Ah, dataview is algebraic data type. I think it doesn't match C
language struct...

Totally, I should use following policy to translate C interface into
ATS sats file?

* Define it as typedef $extype_struct
* Simply map primitive type
* Map array to @[TYPE][SIZE]
* Map any pointer to ptr
* Use mutual struct with casting ptr member of the struct

I'm happy, if getting your comment.

[gmhwxi]

Hi Kiwamu,

As I see it, compiling C into ATS is very meaningful but also very
challenging. At this point, it is still unclear to me what your primary
objective is for compiling C into ATS. It would definitely help if you
could present some (potential) use cases.

On Saturday, August 20, 2016 at 8:07:37 PM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

[Kiwamu Okabe]

Hi Hongwei,

On Mon, Aug 22, 2016 at 1:24 PM, gmhwxi <gmh...@gmail.com> wrote:
> As I see it, compiling C into ATS is very meaningful but also very
> challenging. At this point, it is still unclear to me what your primary
> objective is for compiling C into ATS. It would definitely help if you
> could present some (potential) use cases.

In the past, I create a tool translating Haskell into C, such like c2ats:

https://github.com/ajhc/struct2hs

With the tool, I can partly rewrite NetBSD kernel:

https://github.com/metasepi/netbsd-arafura-s1/tree/arafura-s1/metasepi/sys/hssrc

The Haskell code imports many C language interface, translated by
struct2hs tool:

Today, I would like to rewrite NetBSD kernel using ATS language with
same method.
I think the method will be like following:

$1. Choose a .c file in NetBSD kernel to rewrite.
Let's choose
https://github.com/IIJ-NetBSD/netbsd-src/blob/master/sys/ufs/ext2fs/ext2fs_vfsops.c.
$2. Translate C interface into ATS .sats file using c2ats tool,
semi-automatically.
It should make many many .sats files in output directory.
$3. Create ext2fs_vfsops.dats file include ext2fs_vfsops.c with "%{"
declaration and staload .sats files created by $2.
And check the ext2fs_vfsops.dats file is ready to be compiled.
$4. Rewrite a function in ext2fs_vfsops.dats file using some types in
.sats files.
$5. Do refactoring the ATS function. Sometimes I'll rewrite typedef in
.sats with dataview.
$6. ...

I would like to choose a method to rewrite C code with ATS, ***incrementally***.

[Hongwei Xi]

I see.

I would suggest a slight different approach.

Basically, I think that every struct in C should be first mapped to an
abstract type.

Let us take the inode as an example.

absvtype inode_ptr(l:addr) = ptr(l)

For each field in inode, you can generate a get function and a set function.

For instance, imagine that the following functions are generated:

fun inode_get_i_gid{l:agz} (x: !inode_ptr(l)): gid(*type*)

fun inode_set_i_gid{l:agz} (x: !inode_ptr(l), v: gid): void

overload .i_gid with inode_get_i_gid

overload .i_gid with inode_set_i_gid

fun inode_get_i_e2fs_gid{l:agz} (x: !inode_ptr(l)): gid(*type*)
fun inode_set_i_e2fs_gid{l:agz} (x: !inode_ptr(l), v: gid): void
overload .i_gid with inode_get_i_e2fs_gid
overload .i_gid with inode_set_i_e2fs_gid

Then you can write code like:

x.i_gid(x.i_e2fs_gid()) // for x->i_gid = x.i_e2fs_gid

At the beginning, please don't try to do too much. Once you have gathered

enough experience, you can start to generate functions with more informative

types. As always, please try to find a good naming scheme to name the generated
functions.

Also, there is no need to start with C syntax. You can (and probably should) start
with some syntax of your design and then later find a way to translate C syntax into
your designed syntax. I call this doing-things-in-stages. Trying to do a complex thing

in one step usually ends up with a failure and some frustration.

--
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-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
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/CAEvX6d%3DZ8zVncN43c8rNrCBb%3D9qPDxLBxhzZzEJ%2BsdZbnTTRwg%40mail.gmail.com.

[Kiwamu Okabe]

Hi Hongwei,

On Mon, Aug 22, 2016 at 2:28 PM, Hongwei Xi <gmh...@gmail.com> wrote:
> Basically, I think that every struct in C should be first mapped to an
> abstract type.

I used mutual struct in your style:

https://github.com/jats-ug/practice-ats/blob/4af1b892edc700d33312b9289ff7a72861b9a4a1/template_struct/main.dats#L134

However, following code at line 134 causes error...

```
val foo_ptr = takeout_struct_foo_ptr (addr@foo)
val () = foo_ptr.b := 9 // error(3): the type
[S2Eapp(S2Ecst(struct_foo_ptr); S2Evar(foo(8452)))] is expected to be
a tyrec(record).
```

> Also, there is no need to start with C syntax. You can (and probably should)
> start
> with some syntax of your design and then later find a way to translate C
> syntax into
> your designed syntax. I call this doing-things-in-stages. Trying to do a
> complex thing
> in one step usually ends up with a failure and some frustration.

Yes. You know that I already made some code for kernel.

https://github.com/metasepi/linux-bohai-s2/blob/bohai-s2/metasepi/include/linux/SATS/statfs.sats#L10

Now, I need some semi-automatically-generate tool to try rewriting
such kernel widely.
Such kernel has many many interfaces written by C language!!!

[Kiwamu Okabe]

Also I have another question.

I split template_struct/main.dats file into following three files:

https://github.com/jats-ug/practice-ats/blob/ac1e4fd22035e643d5211891c16564dda6ff5fcc/template_struct/gen.sats
https://github.com/jats-ug/practice-ats/blob/ac1e4fd22035e643d5211891c16564dda6ff5fcc/template_struct/gen_tmpl.dats
https://github.com/jats-ug/practice-ats/blob/ac1e4fd22035e643d5211891c16564dda6ff5fcc/template_struct/main.dats

But I have following error on gcc side...

```
$ pwd
/home/kiwamu/src/practice-ats/template_struct
$ make
/home/kiwamu/src/ATS-Postiats/bin/patscc -o a.out main.dats -DATS_MEMALLOC_LIBC
In file included from main_dats.c:15:0:
main_dats.c: In function 'mainats_void_0':
main_dats.c:1380:21: error: unknown type name 'struct_foo'
ATStmpdec(tmpref48, struct_foo) ;
^
/home/kiwamu/src/ATS-Postiats/ccomp/runtime/pats_ccomp_instrset.h:199:29:
note: in definition of macro 'ATStmpdec'
#define ATStmpdec(tmp, hit) hit tmp
^~~
main_dats.c:1381:21: error: unknown type name 'struct_bar'
ATStmpdec(tmpref49, struct_bar) ;
^
/home/kiwamu/src/ATS-Postiats/ccomp/runtime/pats_ccomp_instrset.h:199:29:
note: in definition of macro 'ATStmpdec'
#define ATStmpdec(tmp, hit) hit tmp
^~~
Makefile:7: recipe for target 'a.out' failed
make: *** [a.out] Error 1
```

... Why???

[gmhwxi]

Please try:

val () = foo_ptr.b(9)

The following article is on dot-symbol overloading:

http://ats-lang.sourceforge.net/DOCUMENT/ATS2TUTORIAL/HTML/HTMLTOC/c260.html

On Monday, August 22, 2016 at 6:00:55 AM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

[gmhwxi]

The reason is that you used:

abst@ype struct_foo

Instead, you need the following line:

abst@ype struct_foo = $extype"struct foo"

The compiler needs to know the size of struct_foo during compilation.

[gmhwxi]

A function like struct_foo_get_b can be defined (automatically) as a macro in C:

fun{}
struct_foo_get_b{l:agz}(x: !struct_foo_ptr(l)): int = ret where {
 val (pf | p) = takeout_struct_foo (x)
 val ret = p->b
 val () = addback_struct_foo (pf | p)
}

In this way, you do not need to implement struct_foo in ATS. That is, the following line is not needed:

assume struct_foo = struct_foo_impl

On Monday, August 22, 2016 at 6:00:55 AM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

[Kiwamu Okabe]

On Mon, Aug 22, 2016 at 10:53 PM, gmhwxi <gmh...@gmail.com> wrote:
> Please try:
>
> val () = foo_ptr.b(9)

Thanks. Fixed.

> The following article is on dot-symbol overloading:
>
> http://ats-lang.sourceforge.net/DOCUMENT/ATS2TUTORIAL/HTML/HTMLTOC/c260.html

For ptr, we can use "val () = p0.x := y0" style.
For absvtype, we can use "val () = p0.x(y0)" tyle.
Correct?

[Hongwei Xi]

If 'x' is a true field name in p0, then you can use p0.x.

If 'x' is an overloaded symbol, then you need to use p0.x() (to access) and p0.x(v) (to update).

--
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-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
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/CAEvX6dkHZK4bdQeN0XYhVvdPmVbD7Dy0D2j3g-Sxi_eOrNwBkQ%40mail.gmail.com.

[Kiwamu Okabe]

On Mon, Aug 22, 2016 at 11:07 PM, gmhwxi <gmh...@gmail.com> wrote:
> The reason is that you used:
>
> abst@ype struct_foo
>
> Instead, you need the following line:
>
> abst@ype struct_foo = $extype"struct foo"
>
> The compiler needs to know the size of struct_foo during compilation.

Clear. I fixed it at following patch:

https://github.com/jats-ug/practice-ats/commit/68c174df017c04135d46168070289a6c001cd49e

Thanks a lot,

[Kiwamu Okabe]

On Tue, Aug 23, 2016 at 12:00 AM, Hongwei Xi <gmh...@gmail.com> wrote:
> If 'x' is a true field name in p0, then you can use p0.x.
> If 'x' is an overloaded symbol, then you need to use p0.x() (to access) and
> p0.x(v) (to update).

Umm? Not make sense.

http://ats-lang.sourceforge.net/DOCUMENT/ATS2TUTORIAL/HTML/HTMLTOC/c260.html

This document say:

```
abstype point = ptr // boxed
extern fun point_make (x: double, y: double): point
extern fun point_set_x (p: point, x: double): void
overload .x with point_set_x
val () = p0.x := y0 // point_set_x (p0, y0)
```

I think the `x` should be overloaded symbol. But above code can use
`p0.x := y0` style...

[gmhwxi]

I see. There is a bit of subtlety here.

If you write 'p0.x := y0', then the type of 'p0' is required to be non linear.

On Monday, August 22, 2016 at 11:09:24 AM UTC-4, Kiwamu Okabe wrote:

[Kiwamu Okabe]

On Tue, Aug 23, 2016 at 12:22 AM, gmhwxi <gmh...@gmail.com> wrote:
> I see. There is a bit of subtlety here.
>
> If you write 'p0.x := y0', then the type of 'p0' is required to be non
> linear.

Uuu-n. Complex.
But I think I understand it.

Thanks,

[Kiwamu Okabe]

Hi Hongwei,

I change the code as following:

https://github.com/jats-ug/practice-ats/commit/48e2215d2017123d8eb0091f050cb95b5334a885

However, I catch error at C language side.

```
$ patscc -o a.out main.dats -DATS_MEMALLOC_LIBC

In file included from main_dats.c:15:0:
main_dats.c: In function

‘_057_home_057_kiwamu_057_src_057_practice_055_ats_057_template_struct_057_gen_056_sats__struct_foo_get_b__3__1’:
/home/kiwamu/src/ATS-Postiats/ccomp/runtime/pats_ccomp_instrset.h:207:29:
warning: dereferencing ‘void *’ pointer
#define ATSderef(pmv, hit) (*(hit*)pmv)

/home/kiwamu/src/ATS-Postiats/ccomp/runtime/pats_ccomp_instrset.h:329:34:
note: in definition of macro ‘ATSINSstore’
#define ATSINSstore(pmv1, pmv2) (pmv1 = pmv2)
^~~~
main_dats.c:1101:13: note: in expansion of macro ‘ATSderef’
ATSINSstore(ATSderef(arg0, atsvoid_t0ype),
ATSPMVcastfn(addback_struct_foo, atstkind_type(atstype_ptrk),
ATSPMVcastfn(takeout_struct_foo, atstkind_type(atstype_ptrk), ar
g0))) ;
^~~~~~~~
main_dats.c:1101:1: error: invalid use of void expression
ATSINSstore(ATSderef(arg0, atsvoid_t0ype),
ATSPMVcastfn(addback_struct_foo, atstkind_type(atstype_ptrk),
ATSPMVcastfn(takeout_struct_foo, atstkind_type(atstype_ptrk), ar
g0))) ;
^~~~~~~~~~~
```

I think the generated C code casts it into `void`. Why not `void *`?

[gmhwxi]

addback_struct_foo should be a prfun (instead of a castfn).

[Kiwamu Okabe]

On Thu, Aug 25, 2016 at 11:41 PM, gmhwxi <gmh...@gmail.com> wrote:
> addback_struct_foo should be a prfun (instead of a castfn).

I changed it as following, but the error is not fixed...

https://github.com/jats-ug/practice-ats/commit/cd3693440273ae8b7bc429a898b7ac7c52e0f233

```
$ patscc -o a.out main.dats -DATS_MEMALLOC_LIBC
In file included from main_dats.c:15:0:
main_dats.c: In function
‘_057_home_057_kiwamu_057_src_057_practice_055_ats_057_template_struct_057_gen_056_sats__struct_foo_get_b__3__1’:
/home/kiwamu/src/ATS-Postiats/ccomp/runtime/pats_ccomp_instrset.h:207:29:
warning: dereferencing ‘void *’ pointer
#define ATSderef(pmv, hit) (*(hit*)pmv)

/home/kiwamu/src/ATS-Postiats/ccomp/runtime/pats_ccomp_instrset.h:329:34:
note: in definition of macro ‘ATSINSstore’
#define ATSINSstore(pmv1, pmv2) (pmv1 = pmv2)
^~~~

main_dats.c:1114:13: note: in expansion of macro ‘ATSderef’
ATSINSstore(ATSderef(arg0, atsvoid_t0ype), tmp4__1) ;
^~~~~~~~
main_dats.c:1114:1: error: invalid use of void expression
ATSINSstore(ATSderef(arg0, atsvoid_t0ype), tmp4__1) ;
^~~~~~~~~~~

[Kiwamu Okabe]

Hi Hongwei,

On Mon, Aug 22, 2016 at 2:28 PM, Hongwei Xi <gmh...@gmail.com> wrote:
> Basically, I think that every struct in C should be first mapped to an
> abstract type.
>
> Let us take the inode as an example.
>
> absvtype inode_ptr(l:addr) = ptr(l)

I have a question about avoiding errors in ATS language. Now you
advice following code:

https://github.com/jats-ug/practice-ats/blob/cd3693440273ae8b7bc429a898b7ac7c52e0f233/template_struct/gen.sats#L25

```
absvtype struct_foo_ptr(l:addr) = ptr(l)
typedef struct_foo = $extype_struct"struct foo" of {
b = int,
p = [l:addr] ptr(l), // struct bar *p
pi = [l:addr] ptr(l) // int **pi
}
castfn takeout_struct_foo_ptr: {l:agz} (ptr(l)) -> struct_foo_ptr(l)
castfn addback_struct_foo_ptr: {l:agz} (struct_foo_ptr(l)) -> void
```

The ATS code can avoid errors caused by NULL pointer. However, it
can't catch miss cast for `ptr` type. I think the type equals `void *`
in C.

On C language side, we have following code:

```
struct bar;

struct foo {
int b;
struct bar *p;

int **pi;

};
struct bar {
int a;
struct foo *p;
};

```

The C code can avoid miss cast for `void *` type. However, it can't
catch errors caused by NULL pointer.

Truly, we have no method to avoid both miss cast and NULL pointer???
Or we can avoid them, if drop mutual struct/record and use
singly-pointer-linked struct/record?

[Kiwamu Okabe]

And I tried to shape mutual record as following:

https://github.com/jats-ug/practice-ats/blob/8bfb41366de6517d4dfe84bc8fe2d9866664311e/mutual_record/main.dats

However, I can't write it like following...

vtypedef foo = @{ x= int, p= [l:addr] (bar@l | ptr(l)) }
and bar = @{ x= int, p= [l:addr] (foo@l | ptr(l)) }

Is it impossible to be supported by ATS compiler?

[Kiwamu Okabe]

On Fri, Aug 26, 2016 at 7:17 PM, Kiwamu Okabe <kiw...@debian.or.jp> wrote:
> And I tried to shape mutual record as following:

And also I can define mutual struct as following:

https://github.com/jats-ug/practice-ats/blob/cb17e34bbb03f45f4ce556196f86c1babd1d2b86/mutual_struct/main.dats

But I would like to write like this...

```
vtypedef bar = $extype_struct"struct bar" of {
x = int,
p = [l:addr] (foo@l | ptr(l))
}
and foo = $extype_struct"struct foo" of {
x = int,
p = [l:addr] (bar@l | ptr(l))
}
```

Best regards,
--
Kiwamu Okabe at METASEPI DESIGN

[Kiwamu Okabe]

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?

[gmhwxi]

There were several mistakes. For instance, the following line:

x := addback_struct_foo(...)

caused the error of dereferencing a void pointer.

I suggest that you use the following style:

(* ****** ****** *)

extern
castfn
takeout_struct_foo
  {l:agz}
  (
    !struct_foo_ptr(l)
  ): (struct_foo@l, struct_foo@l -<lin,prf> void | ptr(l))

(* ****** ****** *)
//
extern
fun
struct_foo_get_b:
  {l:agz}(!struct_foo_ptr(l)) -> int
//
implement
struct_foo_get_b (x) = ret where {
  val (pf, fpf | p) = takeout_struct_foo (x)
  val ret = p->b
  prval () = fpf(pf)
}
//
(* ****** ****** *)

On Thursday, August 25, 2016 at 11:23:39 PM UTC-4, Kiwamu Okabe wrote:

[Kiwamu Okabe]

Hi Hongwei,

On Sat, Aug 27, 2016 at 1:47 AM, gmhwxi <gmh...@gmail.com> wrote:
> There were several mistakes. For instance, the following line:
>
> x := addback_struct_foo(...)
>
> caused the error of dereferencing a void pointer.
>
> I suggest that you use the following style:

I see the style at your prelude.

```
castfn ptr0_vtake
{a:vt0p} (ptr):<> [l:addr] (a@l, a@l -<lin,prf> void | ptr l)
```

Then I fixed it as following code:

https://github.com/jats-ug/practice-ats/commit/bb6850e062bd0258c5499b7664d380b3c7fd2b32

```
castfn takeout_struct_foo: {l:agz} (!struct_foo_ptr(l)) ->

(struct_foo@l, struct_foo@l -<lin,prf> void | ptr(l))

```

Thanks a lot,

[Kiwamu Okabe]

Hi Hongwei,

On Fri, Aug 26, 2016 at 6:38 PM, Kiwamu Okabe <kiw...@debian.or.jp> wrote:
> Truly, we have no method to avoid both miss cast and NULL pointer???
> Or we can avoid them, if drop mutual struct/record and use
> singly-pointer-linked struct/record?

I think the Rust language has a method to avoid both of them:

https://github.com/redox-os/redox/blob/1ce61c3833b55d4724f9a920ce13f637d6faca74/kernel/audio/ac97.rs#L26

If so, Rust is more better than ATS to maintain pointer in struct.

Of course, Rust doesn't have any dependent types, however I think the
language is more safe to maintain memory.

[gmhwxi]

It is not clear to me what you mean by 'miss cast'.

Maybe you should use cptr (instead of ptr):

typedef struct_foo = $extype_struct"struct foo" of {
  b = int,

  p = cPtr0(struct_bool)
  pi = cPtr0(cPtr0(int))
}

Honestly, I think 'struct_foo' should be abstract. Functions
like struct_foo_get_b can and probably should be implemented in C directly.

On Friday, August 26, 2016 at 9:46:13 PM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

[Kiwamu Okabe]

Hi Hongwei,

On Sat, Aug 27, 2016 at 12:05 PM, gmhwxi <gmh...@gmail.com> wrote:>
> It is not clear to me what you mean by 'miss cast'.

My 'miss cast' is meaning... If we have following code:

```
absvtype struct_foo_ptr(l:addr) = ptr(l)

typedef struct_foo = $extype_struct"struct foo" of {
b = int,

p = [l:addr] ptr(l), // struct bar *p
pi = [l:addr] ptr(l) // int **pi
}
castfn takeout_struct_foo_ptr: {l:agz} (ptr(l)) -> struct_foo_ptr(l)

absvtype struct_bar_ptr(l:addr) = ptr(l)
typedef struct_bar = $extype_struct"struct bar" of {
a = int,
p = [l:addr] ptr(l) // struct foo *p
}
castfn takeout_struct_bar_ptr: {l1:agz} (ptr(l1)) -> struct_bar_ptr(l1)
```

then we can write following code with some mistake that cast pointer
to foo as bar:

```
var foo: struct_foo
// ...
val bar_ptr = takeout_struct_bar_ptr (addr@foo)
val () = print_bar bar_ptr
val () = addback_struct_bar_ptr bar_ptr
```

> Maybe you should use cptr (instead of ptr):
>
> typedef struct_foo = $extype_struct"struct foo" of {
> b = int,
> p = cPtr0(struct_bool)
> pi = cPtr0(cPtr0(int))
> }

Umm......... I think we can't get this style.
Because we can't directly specify struct implemetation in the struct,
while using mutual struct.

> Honestly, I think 'struct_foo' should be abstract. Functions
> like struct_foo_get_b can and probably should be implemented in C directly.

Ah, it's also another simple solution.
I have not yet my feeling to decide using either ATS or C language in
such situation...

Thanks a lot,

[gmhwxi]

Here is some code that may be helpful:

https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST30/struct.dats

[Kiwamu Okabe]

On Sat, Aug 27, 2016 at 4:54 PM, gmhwxi <gmh...@gmail.com> wrote:
> Here is some code that may be helpful:
>
> https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST30/struct.dats

Thanks a lot.
Now, I'm writing the other solution...

[Kiwamu Okabe]

Hi Hongwei,

On Sat, Aug 27, 2016 at 5:07 PM, Kiwamu Okabe <kiw...@debian.or.jp> wrote:
> Now, I'm writing the other solution...

My answer is following:

https://github.com/jats-ug/practice-ats/blob/334c41e981a67153d92fcca25130533c86277619/mutual_struct2/gen.sats
https://github.com/jats-ug/practice-ats/blob/334c41e981a67153d92fcca25130533c86277619/mutual_struct2/main.dats

I like this style, because...

Pros:
* Most pointer access is under at-view.
* Checking NULL pointer is captured by `fun take_struct_foo_p: {l1:agz}`.
* Non-pointer struct member can be easily touched by `->`.
* Easily support double pointer struct member such like `struct foo **p;`.

Cons:
* Writing pointer may cause miss cast such like `pfoo->p := pfoo`.

Best regards,

[Kiwamu Okabe]

On Sat, Aug 27, 2016 at 8:38 PM, Kiwamu Okabe <kiw...@debian.or.jp> wrote:
> * Easily support double pointer struct member such like `struct foo **p;`.

I tried to write that as following:

https://github.com/jats-ug/practice-ats/blob/a3cfedca36459d7fb5b26ddfbba62de237900902/mutual_struct2/gen.sats
https://github.com/jats-ug/practice-ats/blob/a3cfedca36459d7fb5b26ddfbba62de237900902/mutual_struct2/main.dats

However, I have a question. It can dereference pointer without
checking that it doesn't equal NULL:

https://github.com/jats-ug/practice-ats/blob/a3cfedca36459d7fb5b26ddfbba62de237900902/mutual_struct2/main.dats#L23

```
val () = if !pbarptr > 0 then print_bar (pfbar | !pbarptr) // Why need
no checking `pbarptr > 0`?
```

I think `pbarptr` should depends on `{l:agz}`, not `{l:addr}`. Isn't it?

[gmhwxi]

With this style, you do not really need the following types:

absvtype struct_foo_ptr(l:addr) = ptr l
absvtype struct_bar_ptr(l:addr) = ptr l

If an at-view T@l for a pointer ptr(l) can be found, the system assumes
that the pointer is not NULL. You may use a run-time check to solve this
issue (or use optional views).

My concern with this style is that it is still very verbose in practice.
To get something closer to the C style, I think that having abstract types like
struct_foo_ptr and struct_bar_ptr is a better way to go.

On Saturday, August 27, 2016 at 8:44:44 AM UTC-4, Kiwamu Okabe wrote:

[gmhwxi]

I also tried a style involving linear pointers:

https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST30/struct1.dats

The type of a linear pointer is aptr(T, L), where T is the type of the content and L is the address.

With this style, there seems to be adequate safety checking. Of course. it needs to be put into
practice to see how it actually fares.

[Kiwamu Okabe]

On Sun, Aug 28, 2016 at 12:54 AM, gmhwxi <gmh...@gmail.com> wrote:
> If an at-view T@l for a pointer ptr(l) can be found, the system assumes
> that the pointer is not NULL. You may use a run-time check to solve this
> issue (or use optional views).

I think I understand it, now.

> My concern with this style is that it is still very verbose in practice.

Yes... you are right...

[Kiwamu Okabe]

On Sun, Aug 28, 2016 at 3:18 AM, gmhwxi <gmh...@gmail.com> wrote:
> I also tried a style involving linear pointers:
>
> https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST30/struct1.dats

Thanks a lot! It seems good balance between safe and unsafe for me.
However, where is `vtget`?

```
$ pwd
/home/kiwamu/src/ATS-Postiats-test/contrib/hwxi/TEST30
$ patscc -o struct1 struct1.dats
/home/kiwamu/src/ATS-Postiats-test/contrib/hwxi/TEST30/struct1.dats:
2641(line=137, offs=26) -- 2646(line=137, offs=31): error(2): the
dynamic identifier [vtget] is unrecognized.
patsopt(TRANS2): there are [1] errors in total.
exit(ATS): uncaught exception:
_2home_2kiwamu_2src_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
```

[Kiwamu Okabe]

Hi Honwei,

On Tue, Aug 30, 2016 at 7:48 PM, Kiwamu Okabe <kiw...@debian.or.jp> wrote:
> However, where is `vtget`?

I believe it's `vtget1`.
My code is found at following:

https://github.com/jats-ug/practice-ats/tree/0289f470bc5cf694ec60f074a7a6102ae35b6f1f/mutual_struct3

By the way, the "aPtr1 style" code is more large than "at-view style" code:

$ wc -l mutual_struct{2,3}/main.dats
44 mutual_struct2/main.dats
53 mutual_struct3/main.dats

I would like to think more, about ATS language code for C language interface...

Thanks a lot,

[Kiwamu Okabe]

On Tue, Aug 30, 2016 at 8:18 PM, Kiwamu Okabe <kiw...@debian.or.jp> wrote:
> By the way, the "aPtr1 style" code is more large than "at-view style" code:
>
> $ wc -l mutual_struct{2,3}/main.dats
> 44 mutual_struct2/main.dats
> 53 mutual_struct3/main.dats

Ah, "at-view style" code grows more large, if support `opt`.
I think I agree your "aPtr1 style" code has good balance.

By the way, I have another question. If we support ATS's record such
like no-mutual but including pointer, we should also choose same
method as supporting struct?

Best regards,

[gmhwxi]

I thinks it all depends...

What kind of records do you have in mind?

On Tuesday, August 30, 2016 at 7:37:38 AM UTC-4, Kiwamu Okabe wrote:

[Kiwamu Okabe]

Hi Hongwei,

On Wed, Aug 31, 2016 at 3:35 AM, gmhwxi <gmh...@gmail.com> wrote:
> What kind of records do you have in mind?

Sorry for my poor explanation. I wrote following code using ATS record
and "at-view style":

https://github.com/jats-ug/practice-ats/blob/6f663912d6118899861889f4ef3b835d3ceb5774/mutual_record/main.dats

Above code has following unsafe points:

A. Create at-view from nothing.
https://github.com/jats-ug/practice-ats/blob/6f663912d6118899861889f4ef3b835d3ceb5774/mutual_record/main.dats#L11
B. Assign raw pointer.
https://github.com/jats-ug/practice-ats/blob/6f663912d6118899861889f4ef3b835d3ceb5774/mutual_record/main.dats#L25

I think these unsafe things is coming from that ATS record can't
maintain at-view in.

My motivation is re-writing C language code using ATS language, and
getting more safe code. I'll rewrite the C code little by little.
At first stage, the ATS code includes some structs from C code.
At second state, should I re-write the struct as ATS record? If
re-write, I'll get more safe design in ATS code? Or which choose
struct/record is not important thing?

[gmhwxi]

Well, I do *not* think that translating a struct in C into ATS record
can bring more safety. I suggest the following strategy:

1. Translating each struct in C into an abstract type in ATS and generating
    a generic programming interface for this abstract type. For instance, the
    style involving aptr I showed is a reasonable way to get started.

2. For a particular C struct (say, inode). you can adapt/adjust the generic interface
    to make it better suited for capturing programming invariants. For instance, you
    may need to introduce abstract views to properly handle reference counting.

Given the complexity of the C code you are to re-write, it is only realistic to expect
that you need to make use of unsafe features. The objective here is to minimize the
use of such features.

---Hongwei

On Wednesday, August 31, 2016 at 7:07:22 AM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

[Kiwamu Okabe]

Hi Hongwei,

On Thu, Sep 1, 2016 at 12:51 AM, gmhwxi <gmh...@gmail.com> wrote:
> 1. Translating each struct in C into an abstract type in ATS and generating
> a generic programming interface for this abstract type. For instance,
> the
> style involving aptr I showed is a reasonable way to get started.
>
> 2. For a particular C struct (say, inode). you can adapt/adjust the generic
> interface
> to make it better suited for capturing programming invariants. For
> instance, you
> may need to introduce abstract views to properly handle reference
> counting.

You mean I should not choose "at-view style" for this purpose.
The style is not good for re-design after re-written.

> Given the complexity of the C code you are to re-write, it is only realistic
> to expect
> that you need to make use of unsafe features. The objective here is to
> minimize the
> use of such features.

Yes. I can agree. < minimized unsafe things at re-writing state

Thanks a lot,

[gmhwxi]

I think you need to try it on a realistic example in order to get a sense
as to how it works in practice. My suspicion is that the at-view style may
not be adequate for a "complex" struct. I would go with the aptr-style, which
allows you to take advantage of the support for overloading in ATS.

On Wednesday, August 31, 2016 at 11:33:44 PM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

[Kiwamu Okabe]

On Thu, Sep 1, 2016 at 1:02 PM, gmhwxi <gmh...@gmail.com> wrote:
> I think you need to try it on a realistic example in order to get a sense
> as to how it works in practice. My suspicion is that the at-view style may
> not be adequate for a "complex" struct. I would go with the aptr-style,
> which
> allows you to take advantage of the support for overloading in ATS.

Yes. Thanks for careful advice. But I can easily choose the style,
because I re-choose it by changing c2ats utility the other day.

Easy come, easy go.
Thanks,

[Kiwamu Okabe]

Hi Hongwei,

On Thu, Sep 1, 2016 at 1:02 PM, gmhwxi <gmh...@gmail.com> wrote:

> I think you need to try it on a realistic example in order to get a sense
> as to how it works in practice. My suspicion is that the at-view style may
> not be adequate for a "complex" struct. I would go with the aptr-style,
> which
> allows you to take advantage of the support for overloading in ATS.

I think I should firstly choose at-view-style, because it's good for a
struct has another struct as member.

Using aptr-style, the code having such struct is following:

https://github.com/jats-ug/practice-ats/tree/53cffb10c1f46603201fbff178e6c1a43eb20e85/mutual_struct3
https://github.com/jats-ug/practice-ats/blob/53cffb10c1f46603201fbff178e6c1a43eb20e85/mutual_struct3/main.dats#L43

Above code read whole struct member `f` in `struct bar` to read int
member `b` in `struct foo`. It can not access the member only. It
means needing much memory access. If using the other style of
setter/getter for struct in struct, this problem may be fixed.
However, It will drop coherence on getter/settter.

On the other side, using at-view-style, the code having such struct is
following:

https://github.com/jats-ug/practice-ats/tree/53cffb10c1f46603201fbff178e6c1a43eb20e85/mutual_struct2
https://github.com/jats-ug/practice-ats/blob/53cffb10c1f46603201fbff178e6c1a43eb20e85/mutual_struct2/main.dats#L31

Above code can directly read/write int member `b` in `struct foo` in
`struct bar`.

I think this problem has its roots in ATS record/struct can't keep
at-view for pointer member in themselves. Then we only need
setter/getter for pointer member in the record/struct. Members without
pointer should be accessed by normal method in ATS language.

Of course, if I know mistake on choosing at-view-style, I'll secondly
choose your aptr-style.

Best regards,

[gmhwxi]

For the field 'f', you can provide a getref function (instead of a get function),
which returns the pointer to the field (instead of the content of the field).

>>I think this problem has its roots in ATS record/struct can't keep
at-view for pointer member in themselves. Then we only need
setter/getter for pointer member in the record/struct. Members without
pointer should be accessed by normal method in ATS language.

A record in ATS CAN keep the proof of an at-view inside a record. However,
doing so would complicate programming quite a lot; it may not be suitable
for translating C code into ATS.

On Saturday, September 3, 2016 at 4:45:13 AM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

[gmhwxi]

Here is some code that may be helpful:

https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST30/struct1.dats

[Kiwamu Okabe]

On Sat, Sep 3, 2016 at 10:16 PM, gmhwxi <gmh...@gmail.com> wrote:
> For the field 'f', you can provide a getref function (instead of a get
> function),
> which returns the pointer to the field (instead of the content of the
> field).

Yes. However, I think it's not direct method.

On aptr-style:

1. Get pointer to field
2. Access member

On at-view style:

1. Access member directly

> A record in ATS CAN keep the proof of an at-view inside a record. However,
> doing so would complicate programming quite a lot; it may not be suitable
> for translating C code into ATS.

Sorry for my mis-understanding. But how to use it on pure ATS
language? Could you point some code about it?

[gmhwxi]

Well, I think that a compiler may be optimize away
the inefficiency due to indirectness. If not, you can always do
it on your own. For instance, I introduced .f_x in the following code
for accessing .f.x directly:

https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST30/struct1.dats

>>Sorry for my mis-understanding. But how to use it on pure ATS language? Could you point
some code about it?

To be honest, I do not really know what you want to do exactly. If you can use a simple
example to illustrate it, then I will try to show the example in ATS.


On Saturday, September 3, 2016 at 10:50:32 AM UTC-4, Kiwamu Okabe wrote:

[Kiwamu Okabe]

Hi Hongwei,

On Sun, Sep 4, 2016 at 2:25 AM, gmhwxi <gmh...@gmail.com> wrote:
> Well, I think that a compiler may be optimize away
> the inefficiency due to indirectness. If not, you can always do
> it on your own. For instance, I introduced .f_x in the following code
> for accessing .f.x directly:
>
> https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST30/struct1.dats

Yes... But it should need more setter/getter. Many many...

> To be honest, I do not really know what you want to do exactly. If you can
> use a simple
> example to illustrate it, then I will try to show the example in ATS.

O.K. Please give me some time. Now I'm building c2ats as at-view-style.

https://travis-ci.org/metasepi/c2ats/builds/157327190#L534

I know your advice is choosing aptr-style. But it's more suitable for
me, today. I write some code in NetBSD kernel using the c2ats. Then
I'll show you some concrete examples. Please discuss more at the day.
Because my ability to explain something is very poor. I would like to
write something and explain it.