Duplicate getters for take and member

[amblafont]

Consider the cogent program (this example is probably not minimal)

type Easy =
  { aa : { cc : U8} }
    layout
      record { aa : pointer at 1B }  at 0B

stupid : Easy -> Easy
stupid (r {aa}) = r {aa}

main : Easy! -> U8
main x = x.aa.cc

with stupid and main in the list of entry points. The generated C code has two different getters and setters for the aa field, which do exactly the same thing.

[zilinc]

@amblafont what's in the top-level .ac file?

[amblafont]

I don't have a .ac file, but I used the option --entry-funcs=entrypoints.cfg with stupid and main inside.

[zilinc]

Just OoC, why would you need --entry-funcs at all, if you don't have a .ac flie? Can you elaborate on your use case?

[amblafont]

I am testing examples of dargent programs to see how to adapt the formalized correspondence proof between the generated C program and the cogent program

[zilinc]

The bug seems to have nothing to do with the use of --entry-funcs flag. Even without it, it has that duplicate getter.

[zilinc]

I am testing examples of dargent programs to see how to adapt the formalized correspondence proof between the generated C program and the cogent program

The --entry-funcs flag without an antiquoted C just does literally nothing.

[zilinc]

In fact, it's not a bug. One version is generated for the "take" operation, and another one for the "member" operation. They just happen to be the same.

[zilinc]

But there might be some optimisations that we may (or may not for verification reasons) want to do to reuse the getters.

[amblafont]

Ah ok, so I guess our suggested format for the table file is not completely adequate. btw, do you have an example where member and take operations differ ?

[zilinc]

I can't think of any case in which they can be different, but will need to read the code to see if there's any reason the getters are not reused.