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

Treat the erased soft keyword as Stainless @ghost #1522

Open
vkuncak opened this issue May 8, 2024 · 0 comments
Open

Treat the erased soft keyword as Stainless @ghost #1522

vkuncak opened this issue May 8, 2024 · 0 comments

Comments

@vkuncak
Copy link
Collaborator

vkuncak commented May 8, 2024

Scala 3 has erased definitions: https://dotty.epfl.ch/docs/reference/experimental/erased-defs.html

We can presumably extract erased parameter keyword and map it to Stainless @ghost.

First, introduce ErasedChecks that has require, ensuring, assert, etc. all expecting erased parameters.
We need to keep StaticChecks for legacy reasons.

We should start by writing some code that uses erased instead of ghost and compiles with Scala 3 (even without Stainless).

There are differences between erased, including the fact that var-s are possibly not marked by erased. Still, being able to remove immutable parameters of defs and case classes is already useful, as it allows to not rely on our own ghost code elimination.

@vkuncak vkuncak changed the title Map erased to @ghost Treat the erased soft keyword as Stainless @ghost May 27, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant