Formatter Pass #12
Formatter Pass #12
Conversation
This PR used the formatter being developed in #2399 to format all the dafny files
src/AST/Translator.dfy
Outdated
| @@ -70,8 +70,8 @@ module Bootstrap.AST.Translator { | |||
| else if ty is C.BitvectorType then | |||
| var bvTy := ty as C.BitvectorType; | |||
| :- Need(bvTy.Width >= 0, Invalid("BV width must be >= 0")); | |||
| Success(DT.BitVector(bvTy.Width as int)) | |||
| // TODO: the following could be simplified | |||
| Success(DT.BitVector(bvTy.Width as int)) | |||
There was a problem hiding this comment.
This shouldn't be indented
src/AST/Translator.dfy
Outdated
| :- Need(op in UnaryOpMap.Keys, UnsupportedExpr(u)); | ||
| var te :- TranslateExpression(e); | ||
| Success(DE.Apply(DE.Eager(DE.UnaryOp(UnaryOpMap[op])), [te])) | ||
| var u := u as C.UnaryOpExpr; |
There was a problem hiding this comment.
Wrong indentation here
| && Exprs.ConstructorsMatch(e, e') | ||
| && f.requires(e) | ||
| && Deep.AllChildren_Expr(e', post) | ||
| ==> f.requires(e') |
There was a problem hiding this comment.
You don't indent the body of forall?
There was a problem hiding this comment.
forall statements, yes, but not forall expressions.
One reason for that is that forall takes everything afterwards.
But I add this to my final survey
| @@ -47,7 +47,7 @@ module Bootstrap.Transforms.BottomUp { | |||
| // - `f(e)` deeply satisfies the post of `f` | |||
| { | |||
| 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.
This looks wrong: Deep.AllExpr is the body of the forall, it shouldn't be aligned with &&, right?
There was a problem hiding this comment.
Indeed. This is a bug.
| e: Interp.Expr, e': Interp.Expr, op: UnaryOp, v: WV, v': WV | ||
| ) | ||
| e: Interp.Expr, e': Interp.Expr, op: UnaryOp, v: WV, v': WV | ||
| ) |
There was a problem hiding this comment.
Yes. Argument lists are indented by 2 spaces in this formatter, and since arguments are inside, they are indented by 4 spaces. This also helps differentiating arguments from bodies. But I'll add this to my final survey.
| @@ -11,11 +11,11 @@ module Utils.StrTree { | |||
| { | |||
| function method ToString() : string { | |||
| match this | |||
| case Str(s) => s | |||
There was a problem hiding this comment.
Not when there are no braces { } around them.
src/Utils/StrTree.dfy
Outdated
| @@ -67,14 +67,14 @@ module Utils.StrTree { | |||
| lemma countFormat_Acc(formatString: string, start: int := 0, count: int := 0) | |||
| decreases |formatString| - start | |||
| ensures countFormat(formatString, start, count) | |||
| == countFormat(formatString, start) + count | |||
| == countFormat(formatString, start) + count | |||
There was a problem hiding this comment.
I wonder how hard this one would be to support
There was a problem hiding this comment.
Not that hard because I had already implemented this alignment behavior for chaining expressions.
I now implemented it for <, <=, ==, !=, <==>, >, >=
This PR used the formatter being developed in #2399 to format all the Dafny files