refactor: Clean up resolution passes 0 and 1 #3284
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…ents into ASTVisitor
…ecks This change makes the source code more straightforward, because it eliminates a special case. It means that NonNullTypeDecl’s are now added as lone vertices into the call-graph during resolution (whereas previously they were not added at all). As far as I can tell, this does not make any difference for the verifier; it only affects the output of /rprint.
This puts type-inference checking into one visitor, instead of a top-level visitor for the declarations and a second visitor for the statements/expressions. This also changes the traversal from bottom-up to top-down, which changes the order of various error messages.
Source/DafnyCore/AST/AstVisitor.cs
Outdated
| @@ -260,18 +262,26 @@ public abstract class ASTVisitor<VisitorContext> where VisitorContext : IASTVisi | |||
|
|
|||
| // Visit subexpressions | |||
| expr.SubExpressions.Iter(ee => VisitExpression(ee, context)); | |||
|
|
|||
| // Finish by calling the post-visitor method | |||
There was a problem hiding this comment.
Comment seems redundant given the name PostVisitOneExpression
Source/DafnyCore/AST/AstVisitor.cs
Outdated
| @@ -317,17 +327,25 @@ public abstract class ASTVisitor<VisitorContext> where VisitorContext : IASTVisi | |||
|
|
|||
| // Visit substatements | |||
| stmt.SubStatements.Iter(ss => VisitStatement(ss, context)); | |||
|
|
|||
| // Finish by calling the post-visitor method | |||
There was a problem hiding this comment.
Comment seems redundant given the name PostVisitOneExpression
Source/DafnyCore/ExpressionTester.cs
Outdated
| } else if (expr is ComprehensionExpr comprehensionExpr) { | ||
| var uncompilableBoundVars = comprehensionExpr.UncompilableBoundVars(); | ||
| } else if (expr is ComprehensionExpr) { | ||
| var e = (ComprehensionExpr)expr; |
There was a problem hiding this comment.
What's the advantage of the pattern
else if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;over
if (expr is ComprehensionExpr comprehensionExpr) ?
| } | ||
| } | ||
|
|
||
| void ResolveNamesAndInferTypesForOneDeclaration(TopLevelDecl topd, bool initialRound) { |
There was a problem hiding this comment.
Seems like two methods would be better than one method with the initialRound parameter. The shared code, which seems to be very littles, can be put into methods.
| } | ||
|
|
||
| // Build call graph. |
There was a problem hiding this comment.
Comment seems redundant based on the code CallGraphBuilder.Build(declarations, reporter);
keyboardDrummer
approved these changes
Dec 29, 2022
RustanLeino
added a commit
to RustanLeino/dafny
that referenced
this pull request
Dec 29, 2022
This PR cleans up the AST traversals that occur during "pass 0" and "pass 1" of the resolver.
These now do:
* Pass 0
- resolve names and infer types
- check that type inference did not leave any types underspecified
- perform substitution for DefaultValueExpression, compute .ResolvedOp,
and some similar checks and AST updates as necessary to make the AST
coherent
* Pass 1
- discover bounds
- compute call graph
- compute and check ghost things
- determine tail recursion
Each "pass" really consists of several traversals of the AST. So,
"phase" or something like that would be a better name.
With this PR, the dependencies between pass 0 and pass 1 have been
sorted out, and so have the dependencies among the various things that
are happening in pass 1.
Pass 0 is the most delicate one, because it starts with an AST about
which very little is known. The general direction of the work in this PR
is to try to make later traversals be as independent of each other as
possible.
A few awkward dependencies remain between the passes. The one that comes
to mind is that the body of a prefix predicate/lemma cannot be filled
until the call-graph has been built. For this reason,
`CheckTypeInference` is run on these prefix bodies once they have been
constructed. It's possible that this could be improved by making sure
that the prefix bodies are created without a need to call
`CheckTypeInference` on them at all.
This PR also fixes some minor things:
* pretty-printing of `newtype` declarations
* scope and two-state checks for attributes
* inferred equality support for non-null iterators (issue dafny-lang#3273)
Fixes dafny-lang#3273
<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>
# Conflicts:
# Source/DafnyCore/Resolver/Resolver.cs
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR is the final clean-up before I can start to merge in the new type inference. It cleans up the AST traversals that occur during "pass 0" and "pass 1" of the resolver. Previously, it wasn't so clear what exactly these passes did, but now it's more clear:
Each "pass" really consists of several traversals of the AST. So, "phase" or something like that would be a better name.
With this PR, the dependencies between pass 0 and pass 1 have been sorted out, and so have the dependencies among the various things that are happening in pass 1.
Pass 0 is the most delicate one, because it starts with an AST about which very little is known. The general direction of the work in this PR is to try to make later traversals be as independent of each other as possible.
Previously, there were many special cases that have added up over time. This PR tries to use the AST Visitor to get a more uniform treatment of things in the AST. There were several places where top-level declarations include, for example, a
class, whereas its automatically declared non-null (subset type) declaration was accessible only via the class. And there were, and still are, several places where by-method declarations or prefix predicates/lemmas are not available from the standard list of.Membersbut is instead accessible only via the the function or lemma declaration that created these. The PR improves on this situation, but only as needed to disentangle passes 0 and 1. There's plenty of room for further beautification and simplification, especially in passes 2 and 3, but that's out of scope for this PR.This PR does not try to improve the tasks and traversals performed by "pass 2" and "pass 3". Indeed, it's not clear what the distinction between 2 and 3 is, but I think it's just historical that various things fell into one of these two.
A few awkward dependencies remain between the passes. The one that comes to mind is that the body of a prefix predicate/lemma cannot be filled until the call-graph has been built. For this reason,
CheckTypeInferenceis run on these prefix bodies once they have been constructed. It's possible that this could be improved by making sure that the prefix bodies are created without a need to callCheckTypeInferenceon them at all.This PR also fixes some minor things:
newtypedeclarationsFixes #3273
Breaking changes: This PR impacted the test suite primarily in these ways:
/rprintmay show things in a different order than before and may show some vertices without edges that were not shown before. I have tried to mitigate this (for now and for the future) by applying further sorting criteria when printing out the call graph information.Users who depend on the exact nature of the resolution errors or on
/rprintmay be affected by this PR.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.