-
Notifications
You must be signed in to change notification settings - Fork 261
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.
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
refactor: Clean up resolution passes 0 and 1 #3284
refactor: Clean up resolution passes 0 and 1 #3284
Conversation
…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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Comment seems redundant based on the code CallGraphBuilder.Build(declarations, reporter);
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
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.Members
but 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,
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 callCheckTypeInference
on them at all.This PR also fixes some minor things:
newtype
declarationsFixes #3273
Breaking changes: This PR impacted the test suite primarily in these ways:
/rprint
may 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
/rprint
may be affected by this PR.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.