-
Notifications
You must be signed in to change notification settings - Fork 256
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
Dafny 4.0 suggestion: Break up {:extern} and support language specificities #2397
Comments
I like the name changes. While I can see some benefit for
|
I have no strong feelings, but we should be careful to not create more confusing terminology do we know other languages that use "export" and "import" in this sense? C uses For me the main issue with Dafny's extern/compile attributes today is that |
Related prior discussion: #469 |
I agree the FFI badly needs an overhaul in general. Another aspect you don't mention is the common use case, not directly supported at all, of wanting to expose a Dafny-idiomatic signature as a target language-idiomatic signature (e.g. mapping a Dafny Given this is a highly complex design space, I'd prefer not to rush getting it right so that it can make the Dafny 4.0 train. It looks like we're leaning towards fresh terms and deprecating the existing ones anyway, which we can do with deprecation and doesn't require an immediate major version bump. |
Currently, the annotation
{:extern}
and{:compile false}
are used intertwined in three different cases{:extern "newName"}
Here is how this method, module or function name should be compiled and accessed externally (this is what we export){:extern}
This method or function is defined externally, here is their signature, don't compile it. (this is what we import){:extern "newName"} {:compile false}
: this weird case is that, if we want to import a method or function with a different Dafny name that the real name, we need to use the export syntax but indicate we are not compiling it. Why we are not compiling it? It's not primarly because we want to deactivate compilation. It's because we want to import the definition.My point is, it looks like hot and cold taps: We all want to adjust temperature and pressure independently, not the individual amounts of hot and hold. In our case, "hot" is
{:extern}
and "cold" is{:compile false}
, and "temperature" is "I want to import this from external Dafny code" and "pressure" is "I want to export this". Moreover, in both cases, we want to be able to specify language-specific names.Here is my breaking proposal for Dafny 4. We get rid of the existing
{:extern [[<string>,] <string>]}
and{:compile false}
, and instead rely on two new attributes{:compile <string>}
and{:import [[<string>,] <string|map<string,string>>]}
, like this:{:compile "name"}
At the time of compilation, replaces Dafny's symbol by "name" at definition site and at call site. Should work for any language. Previously{:extern "name"}
.{:compile map["csharp" := "name"]}
Same as before, except that we can associate a name for every language, and fail if the compile target does not support that language. Did not exist previously.{:import}
to import an existing external symbol in Dafny with the same name. Should work for any language. Previously{:extern}
(which has an implicit{:compile false}
).{:import "F"}
to import the existing external symbol F in Dafny, overriding Dafny's symbol "name". Should work for any language. Previously{:extern "F"} {:compile false}
.{:import map["csharp", "name"]}
same as before, except we restrict the languages target from which we can import the symbol "name". Did not exist previously.{:import "Module", "F"}
to import the existing external symbol Module.F in Dafny. Should work for any language. Previously{:extern "Module", "F"} {:compile false}
.The text was updated successfully, but these errors were encountered: