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

Format lemma in the IDE #4269

Closed
seebees opened this issue Jul 8, 2023 · 1 comment · Fixed by #4274
Closed

Format lemma in the IDE #4269

seebees opened this issue Jul 8, 2023 · 1 comment · Fixed by #4274
Labels
part: formatter Code formatter for Dafny source code

Comments

@seebees
Copy link

seebees commented Jul 8, 2023

The following is what the IDE Format Document does.

The CLI does what you would expect.
(tested on both latest and nightly)

Note the indentation of { on lemma

module Foo {

  function Baz()
    :(a: string)
    ensures a == "asdf"
  {
    "asdf"
  }

  lemma Bar(t: string)
    requires t == Baz()
    ensures t == "asdf"
    {}
}
@seebees
Copy link
Author

seebees commented Jul 8, 2023

Likely related to #4270

@MikaelMayer MikaelMayer transferred this issue from dafny-lang/ide-vscode Jul 10, 2023
@MikaelMayer MikaelMayer added the part: formatter Code formatter for Dafny source code label Jul 10, 2023
MikaelMayer added a commit that referenced this issue Jul 10, 2023
@MikaelMayer
Add test for issue #4269
b5dd9dd
@MikaelMayer MikaelMayer mentioned this issue Jul 11, 2023
Merged
MikaelMayer added a commit that referenced this issue Jul 14, 2023
@MikaelMayer
Fix: Formatting within the IDE wasn't working anymore (#4274)
d8c1135 
This PR fixes #4269 and fixes #4270
I first added unit tests for the cases that were failing. What really
solved the issue was that I had to implement proper cloning for
- methods, that were not keeping BodyStartTok
- formals, that were not keeping RangeToken

Then I also added for all formatting test a case when it tries to clone
all members before formatting, like VSCode does, which unveiled 3 more
formatting issues:
```
method Test() {
  g := new ClassName.ConstructorName(
      argument1b, // Two extra spaces
      argument2b,
      argument3b
    );
  var g := new ClassName.ConstructorName(
           argument1, // Missing two extra spaces (when block mode activated)
           argument2,
           argument3
         );
...
  && unchanged(
       this,
       c
     )
     && old( // Extra undesired space here
         c.c
       ) == c.c
  && fresh(
       c.c
     )
```
I also solved the above issues by:
* Ensuring the `RangeToken` of `TypeRHS` is preserved after cloning by
modifying its topmost cloning parent `AssignmentRHS`
* Ensure we iterate on pre resolved children to get `OwnedToken`
(otherwise some cloned expressions were crashing)
* Ensure `UnchangedExpr` is cloned with the same pattern as everyone
else (otherwise the `RangeToken` wasn't kept)


<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
@ZhongRuoyu ZhongRuoyu mentioned this issue Jul 20, 2023
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
part: formatter Code formatter for Dafny source code
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix: Formatting within the IDE wasn't working anymore dafny-lang/dafny
2 participants
@seebees @MikaelMayer