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.

Sign up for GitHub

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

Jump to bottom

Support for enumerating finite datatypes in Rust #5643

Closed
Tracked by #5561
fabiomadge opened this issue Jul 22, 2024 · 1 comment · Fixed by #5670
Closed
Tracked by #5561

Support for enumerating finite datatypes in Rust #5643

fabiomadge opened this issue Jul 22, 2024 · 1 comment · Fixed by #5670
Labels
during 2: compilation of correct program Dafny rejects a valid program during compilation has-workaround: yes There is a known workaround kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny lang: rust Dafny's transpiler to Rust and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag

Comments

@fabiomadge
Copy link
Collaborator

Dafny version

4.7.0

Code to produce this issue

datatype D = A | B

const c := set d: D | true :: d

method Main() {
  print c, "\n";
}

Command to run and resulting output

No response

What happened?

EmitDatatypeBoundedPool unsupported

What type of operating system are you experiencing the problem on?

Mac
@fabiomadge fabiomadge added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag has-workaround: yes There is a known workaround during 2: compilation of correct program Dafny rejects a valid program during compilation lang: rust Dafny's transpiler to Rust and its runtime labels Jul 22, 2024
@ssomayyajula
Copy link
Contributor

(documenting for anyone watching) workaround: declare c directly from the singleton constructors of D

@MikaelMayer MikaelMayer mentioned this issue Aug 5, 2024
Open
16 tasks
MikaelMayer added a commit that referenced this issue Aug 6, 2024
@MikaelMayer
Add test for issue #5643
dba7371
@MikaelMayer MikaelMayer mentioned this issue Aug 6, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
during 2: compilation of correct program Dafny rejects a valid program during compilation has-workaround: yes There is a known workaround kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny lang: rust Dafny's transpiler to Rust and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix: Support for enumerating datatypes in the Rust backend dafny-lang/dafny
2 participants
@fabiomadge @ssomayyajula