Formatter pass #2715
Formatter pass #2715
Conversation
Source/DafnyCompilers/AST.dfy
Outdated
| @@ -1,350 +1,350 @@ | |||
| include "CSharpDafnyASTModel.dfy" | |||
| include "CSharpDafnyASTModel.dfy" | |||
There was a problem hiding this comment.
Why is the include indented?
There was a problem hiding this comment.
Congratulations, you found a bug 🥈
There was a problem hiding this comment.
Fixed in the new version
| | MultisetCard | ||
| | MapCard | ||
| | MemberSelect(name: string) | ||
| // Ghost operators |
There was a problem hiding this comment.
Very good finding, but that's expected.
- We plan to have docstring to be comments like this one right after a constructor, so it's correctly aligned.
- The comments just below
// |are aligned with the|above because the Dafny formatter recognizes that this is a commented case of a constructor.
| && f.requires(e) | ||
| && Deep.AllChildren_Expr(e', post) | ||
| ==> f.requires(e') | ||
| && Exprs.ConstructorsMatch(e, e') |
There was a problem hiding this comment.
I'll add this to my final survey list, as I like the one on the right.
| { | ||
| forall e: Expr | Deep.AllChildren_Expr(e, post) && f.requires(e) :: | ||
| Deep.All_Expr(f(e), post) | ||
| Deep.All_Expr(f(e), post) |
There was a problem hiding this comment.
You found a bug, congrats ! 🥉
| eq_value: (WV,WV) -> bool, ctx: Context, ctx': Context | ||
| ) | ||
| eq_value: (WV,WV) -> bool, ctx: Context, ctx': Context | ||
| ) |
There was a problem hiding this comment.
I'll add this to my final survey as I like the one on the right better. That way, arguments don't have the same indentation as the body of the predicate/function, which makes it easy to determine the limit between the two.
Source/DafnyCompilers/Interp.dfy
Outdated
| @@ -1,4 +1,4 @@ | |||
| include "Library.dfy" | |||
| include "Library.dfy" | |||
There was a problem hiding this comment.
Bug for which I pushed a fix on Friday, but I did not update this. Now it's done. Thanks
| case FunctionCall() => | ||
| InterpFunctionCall(e, env, argvs[0], argvs[1..]) | ||
| }) | ||
| case UnaryOp(op: UnaryOp) => |
There was a problem hiding this comment.
there's a code highlighting bug
There was a problem hiding this comment.
With the newest version, the code diff is no longer a problem, can you have a look and let me know if this is ok?
I still think the indentation of the match case should be more aligned.
| Success(V.BitVector(v0.width, Math.IntPow(2, v0.width) - 1 - v0.value)) | ||
| case BoolNot => :- Need(v0.Bool?, Invalid(expr)); | ||
| Success(V.Bool(!v0.b)) | ||
| case SeqLength => :- Need(v0.Seq?, Invalid(expr)); |
There was a problem hiding this comment.
could we have a linebreak after =>? Why is Success aligned with the RHS of :-?
There was a problem hiding this comment.
The scope of the formatter does not include adding newlines.
Success is now aligned with :- and nots its RHS
This PR used the formatter being developed in #2399 to format all the dafny files
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.