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

Malformed Python code for some functions involving lambdas #5092

Closed
fabiomadge opened this issue Feb 15, 2024 · 2 comments · Fixed by #5093
Closed

Malformed Python code for some functions involving lambdas #5092

fabiomadge opened this issue Feb 15, 2024 · 2 comments · Fixed by #5093
Labels
during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: python Dafny's Python transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag priority: next Will consider working on this after in progress work is done

Comments

@fabiomadge
Copy link
Collaborator

Dafny version

4.4.0

Code to produce this issue

function True(): bool {
  if false 
    then false
    else if (_ => false)(false)
      then false 
      else true
}

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

Command to run and resulting output

dafny /compile:4 /compileTarget:py git-issue-5092.dfy

What happened?

The lambda is in the wrong place.

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 part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag lang: python Dafny's Python transpiler and its runtime during 2: compilation of correct program Dafny rejects a valid program during compilation labels Feb 15, 2024
@fabiomadge fabiomadge mentioned this issue Feb 15, 2024
Merged
@keyboardDrummer keyboardDrummer added the priority: next Will consider working on this after in progress work is done label Feb 21, 2024
@robin-aws
Copy link
Member

Label nit-picking: shouldn't this be during 3: execution of incorrect program instead?

@fabiomadge
Copy link
Collaborator Author

I don't think so. We emit invalid Python, which the validation that we run if no code gets executed catches.

fabiomadge added a commit that referenced this issue Feb 22, 2024
@fabiomadge
fix: Malformed Python code for some functions involving lambdas (#5093)
dda2500 
Fixes #5092
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 kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: python Dafny's Python transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag priority: next Will consider working on this after in progress work is done
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: Malformed Python code for some functions involving lambdas fabiomadge/dafny
3 participants
@fabiomadge @keyboardDrummer @robin-aws