Skip to content
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.

Sign up for GitHub

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

Jump to bottom

refactor: Clean up resolution passes 0 and 1 #3284

Merged
merged 60 commits into from
Dec 29, 2022
Merged

refactor: Clean up resolution passes 0 and 1 #3284

merged 60 commits into from
Dec 29, 2022

Commits on Dec 22, 2022

  1. Introduce IASTVisitorContext

    @RustanLeino
    RustanLeino committed Dec 22, 2022
    Configuration menu
    Copy the full SHA
    9aa45b9 View commit details
    Browse the repository at this point in the history

  2. Introduce ASTVisitor

    @RustanLeino
    RustanLeino committed Dec 22, 2022
    Configuration menu
    Copy the full SHA
    e6d6bbe View commit details
    Browse the repository at this point in the history

  3. Introduce CallGraphASTVisitor

    @RustanLeino
    RustanLeino committed Dec 22, 2022
    Configuration menu
    Copy the full SHA
    f513f96 View commit details
    Browse the repository at this point in the history

  4. Use IASTVisitorContext instead of ICodeContext as CallGraphBuilderCon… 

    …text core
    @RustanLeino
    RustanLeino committed Dec 22, 2022
    Configuration menu
    Copy the full SHA
    00f1ed8 View commit details
    Browse the repository at this point in the history

  5. Move work from VisitFunction to VisitFunctionProper

    @RustanLeino
    RustanLeino committed Dec 22, 2022
    Configuration menu
    Copy the full SHA
    363b50d View commit details
    Browse the repository at this point in the history

  6. Move work from VisitMethod to VisitMethodProper

    @RustanLeino
    RustanLeino committed Dec 22, 2022
    Configuration menu
    Copy the full SHA
    5c01d60 View commit details
    Browse the repository at this point in the history

  7. Change CallGraphBuilder visitor into a subclass of ASTVisitor

    @RustanLeino
    RustanLeino committed Dec 22, 2022
    Configuration menu
    Copy the full SHA
    6b7f96e View commit details
    Browse the repository at this point in the history

  8. Remove code that moved into ASTVisitor

    @RustanLeino
    RustanLeino committed Dec 22, 2022
    Configuration menu
    Copy the full SHA
    10069f5 View commit details
    Browse the repository at this point in the history

  9. Move visitor methods from CallGraphBuilder to CallGraphASTVisitor to

    @RustanLeino
    RustanLeino committed Dec 22, 2022
    Configuration menu
    Copy the full SHA
    b500fa2 View commit details
    Browse the repository at this point in the history

  10. Generalize context parameter for ASTVisitor

    @RustanLeino
    RustanLeino committed Dec 22, 2022
    Configuration menu
    Copy the full SHA
    4598fd9 View commit details
    Browse the repository at this point in the history

  11. Move visitation of user-provided types, subexpressions, and substatem… 

    …ents into ASTVisitor
    @RustanLeino
    RustanLeino committed Dec 22, 2022
    Configuration menu
    Copy the full SHA
    1a082e9 View commit details
    Browse the repository at this point in the history

  12. Virtualize declaration/member visitation as well

    @RustanLeino
    RustanLeino committed Dec 22, 2022
    Configuration menu
    Copy the full SHA
    74b96fc View commit details
    Browse the repository at this point in the history

  13. Merge branch 'master' into AstVisitor

    @RustanLeino
    RustanLeino authored Dec 22, 2022
    Configuration menu
    Copy the full SHA
    35c70d7 View commit details
    Browse the repository at this point in the history

Commits on Dec 23, 2022

  1. Move ASTVisitor and IASTVisitorContext into a separate file

    @RustanLeino
    RustanLeino committed Dec 23, 2022
    Configuration menu
    Copy the full SHA
    33bb66c View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into AstVisitor

    @RustanLeino
    RustanLeino committed Dec 23, 2022
    Configuration menu
    Copy the full SHA
    10c2f32 View commit details
    Browse the repository at this point in the history

  3. Visit StmtExpr’s substatements before its subexpressions

    @RustanLeino
    RustanLeino committed Dec 23, 2022
    Configuration menu
    Copy the full SHA
    44dabc0 View commit details
    Browse the repository at this point in the history

  4. Move type-determined checks a little later

    @RustanLeino
    RustanLeino committed Dec 23, 2022
    Configuration menu
    Copy the full SHA
    854ee25 View commit details
    Browse the repository at this point in the history

  5. Improved names of identifiers

    @RustanLeino
    RustanLeino committed Dec 23, 2022
    Configuration menu
    Copy the full SHA
    8111b99 View commit details
    Browse the repository at this point in the history

  6. Collect code into new ResolveNamesAndInferTypes method

    @RustanLeino
    RustanLeino committed Dec 23, 2022
    Configuration menu
    Copy the full SHA
    cc7caf5 View commit details
    Browse the repository at this point in the history

  7. Improve code organization

    @RustanLeino
    RustanLeino committed Dec 23, 2022
    Configuration menu
    Copy the full SHA
    4edf858 View commit details
    Browse the repository at this point in the history

  8. Resolve attributes last

    @RustanLeino
    RustanLeino committed Dec 23, 2022
    Configuration menu
    Copy the full SHA
    a8a5766 View commit details
    Browse the repository at this point in the history

  9. Combined some post-name-resolution visitation checks

    @RustanLeino
    RustanLeino committed Dec 23, 2022
    Configuration menu
    Copy the full SHA
    b179549 View commit details
    Browse the repository at this point in the history

  10. fix: Disallow “this” in non-instance attributes

    @RustanLeino
    RustanLeino committed Dec 23, 2022
    Configuration menu
    Copy the full SHA
    a2b7d51 View commit details
    Browse the repository at this point in the history

  11. Group similar checks into the same visitation pass

    @RustanLeino
    RustanLeino committed Dec 23, 2022
    Configuration menu
    Copy the full SHA
    af01ea3 View commit details
    Browse the repository at this point in the history

  12. Do CheckTypeInference together

    @RustanLeino
    RustanLeino committed Dec 23, 2022
    Configuration menu
    Copy the full SHA
    c79e628 View commit details
    Browse the repository at this point in the history

  13. Merge branch 'master' into check-type-inference

    @RustanLeino
    RustanLeino committed Dec 23, 2022
    Configuration menu
    Copy the full SHA
    5dd1182 View commit details
    Browse the repository at this point in the history

Commits on Dec 24, 2022

  1. Separate type-inference checking, bounds discovery, and ghost checking

    @RustanLeino
    RustanLeino committed Dec 24, 2022
    Configuration menu
    Copy the full SHA
    26baac4 View commit details
    Browse the repository at this point in the history

  2. Adjust lines in test file

    @RustanLeino
    RustanLeino committed Dec 24, 2022
    Configuration menu
    Copy the full SHA
    e48f7ab View commit details
    Browse the repository at this point in the history

  3. Split test into two modules

    @RustanLeino
    RustanLeino committed Dec 24, 2022
    Configuration menu
    Copy the full SHA
    7638787 View commit details
    Browse the repository at this point in the history

  4. Adjust test to show both errors

    @RustanLeino
    RustanLeino committed Dec 24, 2022
    Configuration menu
    Copy the full SHA
    56fd78a View commit details
    Browse the repository at this point in the history

  5. Improve comments

    @RustanLeino
    RustanLeino committed Dec 24, 2022
    Configuration menu
    Copy the full SHA
    cd6055e View commit details
    Browse the repository at this point in the history

  6. Splits tests to get errors from what is now different passes

    @RustanLeino
    RustanLeino committed Dec 24, 2022
    Configuration menu
    Copy the full SHA
    ea2f677 View commit details
    Browse the repository at this point in the history

  7. Check type inference of the beginning of prefix lemmas earlier

    @RustanLeino
    RustanLeino committed Dec 24, 2022
    Configuration menu
    Copy the full SHA
    8647a91 View commit details
    Browse the repository at this point in the history

  8. Update expected test output

    @RustanLeino
    RustanLeino committed Dec 24, 2022
    Configuration menu
    Copy the full SHA
    2b41297 View commit details
    Browse the repository at this point in the history

  9. Check CheckTypeInference… to only take IASTVisitorContext, not ICodeC… 

    …ontext
    @RustanLeino
    RustanLeino committed Dec 24, 2022
    Configuration menu
    Copy the full SHA
    0e5e4d3 View commit details
    Browse the repository at this point in the history

  10. Improve CheckTypeInference for const

    @RustanLeino
    RustanLeino committed Dec 24, 2022
    Configuration menu
    Copy the full SHA
    df5a707 View commit details
    Browse the repository at this point in the history

  11. Improve code

    @RustanLeino
    RustanLeino committed Dec 24, 2022
    Configuration menu
    Copy the full SHA
    3924295 View commit details
    Browse the repository at this point in the history

Commits on Dec 27, 2022

  1. Improve organization of CheckTypeInference visitor

    @RustanLeino
    RustanLeino committed Dec 27, 2022
    Configuration menu
    Copy the full SHA
    86a3369 View commit details
    Browse the repository at this point in the history

  2. fix: Infer (==) for non-null iterator type 

    Fixes dafny-lang#3273
    @RustanLeino
    RustanLeino committed Dec 27, 2022
    Configuration menu
    Copy the full SHA
    852f7fe View commit details
    Browse the repository at this point in the history

  3. To reduce special cases, also include NonNullTypeDecl in cyclicity ch… 

    …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.
    @RustanLeino
    RustanLeino committed Dec 27, 2022
    Configuration menu
    Copy the full SHA
    e0ec038 View commit details
    Browse the repository at this point in the history

Commits on Dec 28, 2022

  1. refactor: Use AST Visitor instead of BottomUp visitor 

    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.
    @RustanLeino
    RustanLeino committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    fead483 View commit details
    Browse the repository at this point in the history

  2. Make resolution/checking of attributes consistent

    @RustanLeino
    RustanLeino committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    5f678a9 View commit details
    Browse the repository at this point in the history

  3. Make recording of warnShadowing attribute consistent

    @RustanLeino
    RustanLeino committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    d2aafd0 View commit details
    Browse the repository at this point in the history

  4. Better document the pre/postcondition of ResolveParameterDefaultValues

    @RustanLeino
    RustanLeino committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    805f70d View commit details
    Browse the repository at this point in the history

  5. fix: Set scope correctly for resolving attributes of top-level declar… 

    …ations
    @RustanLeino
    RustanLeino committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    fe502c3 View commit details
    Browse the repository at this point in the history

  6. fix: Indent member block of newtypes

    @RustanLeino
    RustanLeino committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    87fb940 View commit details
    Browse the repository at this point in the history

  7. refactor: Move “(==) unnecessary” check to later pass

    @RustanLeino
    RustanLeino committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    7dae2ae View commit details
    Browse the repository at this point in the history

  8. Add post-visitor (bottom up) to ASTVisitor

    @RustanLeino
    RustanLeino committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    477b418 View commit details
    Browse the repository at this point in the history

  9. Change CheckTypeInference (back) to be a bottom-up traversal

    @RustanLeino
    RustanLeino committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    c906a0d View commit details
    Browse the repository at this point in the history

  10. Improve code

    @RustanLeino
    RustanLeino committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    85c947d View commit details
    Browse the repository at this point in the history

  11. Merge branch 'master' into check-type-inference

    @RustanLeino
    RustanLeino committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    d413947 View commit details
    Browse the repository at this point in the history

  12. Move some pass-0 code from Resolver.cs to NameResolutionAndTypeInfere… 

    …nce.cs
    @RustanLeino
    RustanLeino committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    413c75b View commit details
    Browse the repository at this point in the history

  13. Move default-parameter substitution to pass 0 from pass 1

    @RustanLeino
    RustanLeino committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    00db663 View commit details
    Browse the repository at this point in the history

  14. Add user-visible release notes

    @RustanLeino
    RustanLeino committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    4a66545 View commit details
    Browse the repository at this point in the history

  15. Rename CheckTypeInference_Visitor.cs TypeInferenceChecker.cs

    @RustanLeino
    RustanLeino committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    0e62b8c View commit details
    Browse the repository at this point in the history

  16. Fix whitespace

    @RustanLeino
    RustanLeino committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    2801491 View commit details
    Browse the repository at this point in the history

  17. Respond to review comments

    @RustanLeino
    RustanLeino committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    cd81c32 View commit details
    Browse the repository at this point in the history

  18. Split Resolve…OneDeclaration and Resolve..MemberBodies into two metho… 

    …ds according to initialRound
    @RustanLeino
    RustanLeino committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    2c7b341 View commit details
    Browse the repository at this point in the history

  19. Report type-parameter errors earlier

    @RustanLeino
    RustanLeino committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    0de1991 View commit details
    Browse the repository at this point in the history

Commits on Dec 29, 2022

  1. Merge branch 'master' into check-type-inference

    @RustanLeino
    RustanLeino committed Dec 29, 2022
    Configuration menu
    Copy the full SHA
    570abb9 View commit details
    Browse the repository at this point in the history