Implement GetAssertedExpr for DecreasesBoundedBelow
#5489
Conversation
Things remaining: * Better syntax * Fill in error messages * Ensure correct parameters to DecreasesCheck * Figure out why most proof obligation descriptions aren't really useful
This has shortcomings, and in particular is only allowed in `assert` statements at the moment. Making it fully general may require some more parser refactoring.
|
|
||
| namespace Microsoft.Dafny; | ||
|
|
||
| public class DecreasesToExpr : Expression, ICloneable<DecreasesToExpr> { |
There was a problem hiding this comment.
Although not a tradition yet, it could be nice to add a syntax example as a comment above this class. I hope that somewhere in the future we'll also be able to define the grammar for this type inside the file that defines the type.
There was a problem hiding this comment.
One thing to mention, though: that change is part of #5367. This PR is still a draft because it builds on that PR, and it isn't merged yet.
| namespace Microsoft.Dafny; | ||
|
|
||
| public class DecreasesToExpr : Expression, ICloneable<DecreasesToExpr> { | ||
| public IEnumerable<Expression> OldExpressions { get; } |
There was a problem hiding this comment.
It seems wrong to have IEnumerable as a field, since this implies computation has to be done each time you iterate of the IEnumerable. If you want it to be immutable, use IReadOnlyList or ImmutableList
|
|
||
| public class DecreasesToExpr : Expression, ICloneable<DecreasesToExpr> { | ||
| public IEnumerable<Expression> OldExpressions { get; } | ||
| public IEnumerable<Expression> NewExpressions { get; } |
There was a problem hiding this comment.
Old already has a meaning in the Dafny context that's different from the meaning here. Could you use a different name? Either something generic like Lhs and Rhs, or Caller/Callee or Large/Small
Source/DafnyCore/Dafny.atg
Outdated
| [ ( "decreases" (. allowNoChange = false; .) | ||
| | "nonincreases" (. allowNoChange = true; .) | ||
| ) (. x = t; .) | ||
| ident |
There was a problem hiding this comment.
How come you can't write "to" here?
Also, have you considered not having to at all? Having two keywords that always follow each other with a space in between is something that I do not think we have anywhere else it the language. It looks like we're trying to mimic natural language, which I don't think is our goal.
If you want to keep the to, I would remove the space, so you get decreasesto, similar to nonincreases, but I would prefer decreases.
To be honest, actually I would prefer introducing built-in functions decreasesTo and decreasesOrEqualTo. Having a keyword as an infix operator feels off for the language. Do we do that anywhere else? Also, for something that occurs so little, I do not see a reason to have special syntax for it.
Also, your implementation always requires decreases to be surrounded by parenthesis. Is that what we settled on? It looks unnecessary: assert (true decreases to false);. If you're requiring parenthesis anyways, then why not make it look like a function call: assert decreasesTo(true, false); ?
There was a problem hiding this comment.
How come you can't write "to" here?
We could only do that if we make it a keyword, which I'd rather not do. The parsing for ranges in things like for var x := 0 to 10 works like this, too.
Also, have you considered not having
toat all? Having two keywords that always follow each other with a space in between is something that I do not think we have anywhere else it the language. It looks like we're trying to mimic natural language, which I don't think is our goal.
To me, it seems much harder to understand without the "to".
If you want to keep the
to, I would remove the space, so you getdecreasesto, similar tononincreases, but I would preferdecreases.
I originally implemented it that way, for simplicity, but we had agreed on having the space in earlier discussions, so I migrated to that syntax.
To be honest, actually I would prefer introducing built-in functions
decreasesToanddecreasesOrEqualTo. Having a keyword as an infix operator feels off for the language. Do we do that anywhere else? Also, for something that occurs so little, I do not see a reason to have special syntax for it.
There needs to be some degree of special syntax because there are two arbitrarily long tuples of expressions on either side. For ease of parsing, my initial experiments used decreases[a, b ; a', b'], but that feels very clunky to me.
Also, your implementation always requires
decreasesto be surrounded by parenthesis. Is that what we settled on? It looks unnecessary:assert (true decreases to false);. If you're requiring parenthesis anyways, then why not make it look like a function call:assert decreasesTo(true, false);?
It's close to necessary because of the fact that you can have an arbitrary number of commas on either side of decreases to. It would be possible to allow it as the top level expression without parentheses in things like assert, assume, requires, and ensures, though I believe it would require substantial duplication in the grammar to do that. I was on the fence about whether to implement that or not. Doing so would be entirely backward-compatible with what's in this PR, though, so I'd prefer to make smaller changes per PR and do it as a separate one (if at all).
There was a problem hiding this comment.
There needs to be some degree of special syntax because there are two arbitrarily long tuples of expressions on either side. For ease of parsing, my initial experiments used decreases[a, b ; a', b'], but that feels very clunky to me.
I see, you need a divider for the two lists.
It's close to necessary because of the fact...
I think at this point I'm in favor of using tuple syntax on both sides if there is more than one item to be compared, so (a,b) decreases to (c,d), instead of (a, b decreases to c, d) (which reads like a 3-tuple with b decreases to c in the middle), and a decreases to b instead of (a decreases to b). Part of the reason I prefer this is because it's most similar to (a,b) > (c,d). I vaguely recall we decided on (a, b decreases to c, d) in the syntax discussion meeting, and that I was also in favor of this, but looking at it now I'm not in favor.
If you want to keep the to, I would remove the space, so you get decreasesto, similar to nonincreases, but I would prefer decreases.
I originally implemented it that way, for simplicity, but we had agreed on having the space in earlier discussions, so I migrated to that syntax.
What's your opinion? Would you be willing to still do a tiny poll amongst the team? I recall we had group discussion on the syntax already, but it might be easier to weigh small choices such as this one separately.
There was a problem hiding this comment.
What's your opinion? Would you be willing to still do a tiny poll amongst the team? I recall we had group discussion on the syntax already, but it might be easier to weigh small choices such as this one separately.
Oh, yeah, I'm definitely up for changing it if the general consensus is toward a different syntax. I implemented this as the closest feasible thing to what we'd agreed on.
The code we're discussing here has already been merged, but changes are very unlikely to break anything if we do them relatively soon.
There was a problem hiding this comment.
I get the issue of the 3-tuple here, but at the same time (a, b) would feel like a tuple which has different decreases to rules. At this point, I prefer the syntax that looks like the 3-tuple here, although in practice I'll surely format it as
(a, b
decreases to
c, d)
or
(a, b
decreases to c, d)
the same way we usually do for other infixes operators.
There was a problem hiding this comment.
Yeah, exactly. Said a different way, and using the syntax I implemented, the semantics of (a, b decreases to c, d) are different than the semantics of ((a, b) decreases to (c, d)). So how would we write the second one if we represented both sides as tuples? Would we do (((a, b)) decreases to ((c, d)))? That seems weird, because normally parentheses are intended to modify only syntax, not semantics.
There was a problem hiding this comment.
I get the issue of the 3-tuple here, but at the same time
(a, b)would feel like a tuple which has different decreases to rules.
Indeed (a, b) looks like a tuple. decreases to would then be an operator that takes two tuples as arguments, applies Dafny's < operator on the tuple elements, and does a lexicographic comparison on those results.
So how would we write the second one if we represented both sides as tuples? Would we do
(((a, b)) decreases to ((c, d)))That seems weird, because normally parentheses are intended to modify only syntax, not semantics.
True.
What about
decreases(a, b, c).to(x, y, z) ?
Or decreasesTo(a, x).then(b, y).then(c, z)
Source/DafnyCore/Dafny.atg
Outdated
| .) | ||
| TupleArgs<args> | ||
| [ ( "decreases" (. allowNoChange = false; .) | ||
| | "nonincreases" (. allowNoChange = true; .) |
There was a problem hiding this comment.
Have you considered not instead of non ? Does non occur anywhere else? Not is what I first think of for negation.
There was a problem hiding this comment.
"nondecreasing" is a word, but "notdecreasing" isn't
| @@ -35,6 +35,7 @@ public partial class BoogieGenerator { | |||
| void CheckCallTermination(IToken tok, List<Expression> contextDecreases, List<Expression> calleeDecreases, | |||
| Expression allowance, | |||
|
|
||
| namespace Microsoft.Dafny; | ||
|
|
||
| public class DecreasesToExpr : Expression, ICloneable<DecreasesToExpr> { |
There was a problem hiding this comment.
Are you using DecreasesToExpr also as a target for a Rewriter, to generate implicit decreases expressions? That might simplify code in BoogieGenerator
There was a problem hiding this comment.
I think that's a good long-term goal, but it would substantially change the shape of the proof obligations for termination that we send to the verifier. I don't want to make that change without evaluating the impact on brittleness.
| @@ -1193,6 +1193,28 @@ void PrintCasePattern<VT>(CasePattern<VT> pat) | |||
| wr.Write("[BoogieFunctionCall]"); // this prevents debugger watch window crash | |||
| } else if (expr is Resolver_IdentifierExpr) { | |||
| wr.Write("[Resolver_IdentifierExpr]"); // we can get here in the middle of a debugging session | |||
| } else if (expr is DecreasesToExpr decreasesToExpr) { | |||
There was a problem hiding this comment.
Out of scope: Looking forward to us setting up a framework so new AST types can group all their code into a single location. Also, I think a single grammar definition should define both the parser and printer.
Did you add a test for this printer? Seems like a test that does parse->printToA->parseFromA->printToB->diffAagainstB that takes a Dafny program containing all AST node types, would be good to have.
There was a problem hiding this comment.
Out of scope: Looking forward to us setting up a framework so new AST types can group all their code into a single location. Also, I think a single grammar definition should define both the parser and printer.
I agree!
Did you add a test for this printer? Seems like a test that does parse->printToA->parseFromA->printToB->diffAagainstB that takes a Dafny program containing all AST node types, would be good to have.
The tests I've added do test this printer. And, yes, I think it would be great to have such a test for the entire parser and pretty-printer.
| ResolveExpression(e, resolutionContext); | ||
| } | ||
|
|
||
| decreasesToExpr.PreType = ConstrainResultToBoolFamilyOperator(decreasesToExpr.tok, "decreasesto"); |
There was a problem hiding this comment.
How come this can't be Type.Bool ?
There was a problem hiding this comment.
It's possible to have subtypes of bool now, and this allows decreases to to operate in those contexts (and it's symmetrical with what's done for other constructs in this method).
| @@ -1485,6 +1485,32 @@ public ExpressionTranslator(ExpressionTranslator etran, Boogie.Expr heap) | |||
| UnboxingCastExpr e = castExpr; | |||
| return BoogieGenerator.CondApplyUnbox(GetToken(e), TrExpr(e.E), e.FromType, e.ToType); | |||
| } | |||
| case DecreasesToExpr decreasesToExpr: | |||
| var oldArray = decreasesToExpr.OldExpressions.ToArray(); | |||
There was a problem hiding this comment.
Once these fields are no longer IEnumerable, you won't need the ToArray here.
### Description - No longer show generated symbols as workspace symbols ### How has this been tested? - Added more assertions to test `AllRelevantSymbolKindsDetected` <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>
…nsions (dafny-lang#5402) To fail early, we split the guard of the comprehension and pull out conjuncts as far out as possible. This should also help with performance. Fixes dafny-lang#3320.
…unction or method (dafny-lang#5474) Fixes dafny-lang#4684 --------- Co-authored-by: Aaron Tomb <[email protected]>
Description
This implements
GetAssertedExprforDecreasesBoundedBelowto be used by--show-proof-obligation-expressions.How has this been tested?
Added
Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/bounded-below.dfy.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.