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

Default value for external generic types #6049

Open
momvart opened this issue Jan 13, 2025 · 0 comments
Open

Default value for external generic types #6049

momvart opened this issue Jan 13, 2025 · 0 comments
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: c++ Dafny's C++ transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag

Comments

@momvart
Copy link

momvart commented Jan 13, 2025

The C++ translator assumes there's a get_XXXX_default() for each external type.

return String.Format("{1}::get_{0}_default()", IdProtect(udt.Name), udt.ResolvedClass.EnclosingModuleDefinition.GetCompileName(Options));

While this works for non-generic types, for generic ones, even if such implementation exists, it still requires the generic (template) parameters to be passed to it.

For example:

type {:extern "struct"} XXXX<T>

class A {
   var x: XXXX<B>
}

The generated code will be:

class A {
XXXX<B> x = get_XXXX_default();
}

If we provide a default function like below:

template <typename T>
XXXX<T> get_XXXX_default() {
    // ...
}

the C++ compiler does not infer B at the call site, and complains.

The solution would be to provide B to the function call, or use the same get_default so the user specializes it for the external type.

@olivier-aws olivier-aws added lang: c++ Dafny's C++ transpiler and its runtime kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag labels Jan 13, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: c++ Dafny's C++ transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
Projects
None yet
Development

No branches or pull requests

2 participants