Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Coq backend: handle constructors with bases (aka {field: expr, ..base} in rust) #134

Open
W95Psp opened this issue Jun 9, 2023 · 3 comments
Assignees
Labels
backend Issue in one of the backends (i.e. F*, Coq, EC...) coq Coq backend

Comments

@W95Psp
Copy link
Collaborator

W95Psp commented Jun 9, 2023

For now, the base is just skipped:

struct Foo {
    a: u8,
    b: u8,
}
fn f(x: Foo) -> Foo {
    Foo { a: 3, ..x }
}

Gets translated as:

Record Foo_tFoo : Type :={
  b : int8;
  a : int8;
}.

Definition f (x : Foo_t) : Foo_t :=
  Build_Foo_t (@repr WORDSIZE8 3).

There's also, something wrong with field projectors, related to #132

@W95Psp W95Psp added the backend Issue in one of the backends (i.e. F*, Coq, EC...) label Jun 9, 2023
W95Psp added a commit that referenced this issue Jun 9, 2023
@W95Psp W95Psp added the coq Coq backend label Jan 2, 2024
@W95Psp
Copy link
Collaborator Author

W95Psp commented Apr 18, 2024

@cmester0, is that still an issue or it's supported now?

Copy link

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

@github-actions github-actions bot added the stale label Oct 16, 2024
@franziskuskiefer
Copy link
Member

@cmester0 is this fixed by #987

@github-actions github-actions bot removed the stale label Oct 17, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
backend Issue in one of the backends (i.e. F*, Coq, EC...) coq Coq backend
Projects
No open projects
Status: Todo
Development

No branches or pull requests

3 participants