search

dafny-lang / libraries

Libraries useful for Dafny programs
Other
43 stars 25 forks source link

Request: converting/adapting Dafny values to native language values #73

Open robin-aws opened 1 year ago

robin-aws commented 1 year ago

Very broad category, probably at least will become one library per target language.

Nearly all compiled Dafny code needs to convert between Dafny string values and native language string values for example. Projects like the Dafny ESDK have utilities for this, but not only is this not something Dafny users should have to implement themselves, but the linked implementation is coupled to Dafny compiler/runtime internals that are not guaranteed to remain stable across releases (and have definitely changed in the past, for good reasons).

In the long term it would be wonderful to not only provide these conversion functions, but also provide meta-utilities to generate the calls to these conversions automatically via something like annotations.

robin-aws commented 1 year ago

Also note another goal is to avoid making independent copies of data where possible. E.g. the Java backend allows you to wrap a java.lang.String as a Dafny.Sequence<Character> (with --unicode-char disabled at least).

mattmccutchen-amazon commented 1 year ago

I asked about a way to convert between a Java String and the DafnySequence<CodePoint> representing a Dafny unicode string, and Robin pointed me to this existing issue. I'm adding some keywords in the hope of making it easier for the next person to find in a web search.

In the meantime, as of this writing, the conversion can be done via DafnySequence.asUnicodeString and DafnySequence.verbatimString. Those are not officially supported APIs and may be removed at any time, but the alternative is basically to copy and paste them into your project, so pick the lesser evil between unconditionally duplicating that code now and taking the risk that your program breaks later and you have to copy/paste the code then.