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

Use refresh resolver by default #5653

Draft
wants to merge 83 commits into
base: master
Choose a base branch
from
Draft

Use refresh resolver by default #5653

wants to merge 83 commits into from

Commits on May 28, 2024

  1. Change default settings

    @RustanLeino
    RustanLeino committed May 28, 2024
    Configuration menu
    Copy the full SHA
    51e033a View commit details
    Browse the repository at this point in the history

  2. Explicitly declare trait to be a reference type

    @RustanLeino
    RustanLeino committed May 28, 2024
    Configuration menu
    Copy the full SHA
    5204eeb View commit details
    Browse the repository at this point in the history

Commits on Jun 27, 2024

  1. Make the new type system the default

    @keyboardDrummer
    keyboardDrummer committed Jun 27, 2024
    Configuration menu
    Copy the full SHA
    3bdaa87 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into refresh-by-default

    @RustanLeino
    RustanLeino committed Jun 27, 2024
    Configuration menu
    Copy the full SHA
    48a8cf4 View commit details
    Browse the repository at this point in the history

  3. Explicitly declare trait as reference type

    @RustanLeino
    RustanLeino committed Jun 27, 2024
    Configuration menu
    Copy the full SHA
    3101604 View commit details
    Browse the repository at this point in the history

Commits on Jun 28, 2024

  1. Changed from full to datatype

    @keyboardDrummer
    keyboardDrummer committed Jun 28, 2024
    Configuration menu
    Copy the full SHA
    a134465 View commit details
    Browse the repository at this point in the history

  2. Add “extends object” where it was assumed to be so before

    @RustanLeino
    RustanLeino committed Jun 28, 2024
    Configuration menu
    Copy the full SHA
    d75f39f View commit details
    Browse the repository at this point in the history

  3. Fix error location for desugared elephant assert

    @RustanLeino
    RustanLeino committed Jun 28, 2024
    Configuration menu
    Copy the full SHA
    46484e6 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'refresh-by-default' into typeSystemRefreshDefault

    @RustanLeino
    RustanLeino committed Jun 28, 2024
    Configuration menu
    Copy the full SHA
    74a49df View commit details
    Browse the repository at this point in the history

Commits on Jul 17, 2024

  1. Merge branch 'master' into refresh-by-default

    @RustanLeino
    RustanLeino committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    af730de View commit details
    Browse the repository at this point in the history

Commits on Jul 18, 2024

  1. Use explicit legacy switches in testDafnyForEach…

    @RustanLeino
    RustanLeino committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    5acc14b View commit details
    Browse the repository at this point in the history

  2. Fix missing box adjustment in verifier

    @RustanLeino
    RustanLeino committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    611ac55 View commit details
    Browse the repository at this point in the history

  3. fix: Use just one pre-type proxy for element type in array allocation

    @RustanLeino
    RustanLeino committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    4979a6e View commit details
    Browse the repository at this point in the history

Commits on Jul 30, 2024

  1. Merge branch 'master' into refresh-by-default

    @RustanLeino
    RustanLeino committed Jul 30, 2024
    Configuration menu
    Copy the full SHA
    d701a33 View commit details
    Browse the repository at this point in the history

Commits on Aug 18, 2024

  1. Fix pre-type of StaticReceiverExpr 

    comp/Class.dfy
    @RustanLeino
    RustanLeino committed Aug 18, 2024
    Configuration menu
    Copy the full SHA
    7a5d171 View commit details
    Browse the repository at this point in the history

Commits on Aug 20, 2024

  1. Update tests to support new defaults

    @RustanLeino
    RustanLeino committed Aug 20, 2024
    Configuration menu
    Copy the full SHA
    a4bf314 View commit details
    Browse the repository at this point in the history

  2. Involve compatible-type constraints in decision process

    @RustanLeino
    RustanLeino committed Aug 20, 2024
    Configuration menu
    Copy the full SHA
    18addcf View commit details
    Browse the repository at this point in the history

  3. Update test 

    The 1 more verified comes from the type of {}. It’s really inferred to be set<object?_\bot>, but this is later turned into just set<object?>.
    @RustanLeino
    RustanLeino committed Aug 20, 2024
    Configuration menu
    Copy the full SHA
    47d4abc View commit details
    Browse the repository at this point in the history

  4. Extract method SansPrintablePreType

    @RustanLeino
    RustanLeino committed Aug 20, 2024
    Configuration menu
    Copy the full SHA
    43a6a37 View commit details
    Browse the repository at this point in the history

  5. Fix type inference of seq/map/multiset update expressions

    @RustanLeino
    RustanLeino committed Aug 20, 2024
    Configuration menu
    Copy the full SHA
    a6820e1 View commit details
    Browse the repository at this point in the history

Commits on Aug 21, 2024

  1. Merge branch 'master' into refresh-by-default

    @RustanLeino
    RustanLeino committed Aug 21, 2024
    Configuration menu
    Copy the full SHA
    99fbb08 View commit details
    Browse the repository at this point in the history

  2. Fix asserted-expression output for frames

    @RustanLeino
    RustanLeino committed Aug 21, 2024
    Configuration menu
    Copy the full SHA
    5026519 View commit details
    Browse the repository at this point in the history

  3. Fix creation of yield-identifier expression

    @RustanLeino
    RustanLeino committed Aug 21, 2024
    Configuration menu
    Copy the full SHA
    dab7870 View commit details
    Browse the repository at this point in the history

  4. Update expect files

    @RustanLeino
    RustanLeino committed Aug 21, 2024
    Configuration menu
    Copy the full SHA
    8028152 View commit details
    Browse the repository at this point in the history

  5. Fix pre-type resolution of export-provided members/types 

    Found via traits/TraitResolution1.dfy
    @RustanLeino
    RustanLeino committed Aug 21, 2024
    Configuration menu
    Copy the full SHA
    86e2312 View commit details
    Browse the repository at this point in the history

  6. Improve formatting

    @RustanLeino
    RustanLeino committed Aug 21, 2024
    Configuration menu
    Copy the full SHA
    bb2d519 View commit details
    Browse the repository at this point in the history

  7. Adjust tests and expected test output

    @RustanLeino
    RustanLeino committed Aug 21, 2024
    Configuration menu
    Copy the full SHA
    d2624ee View commit details
    Browse the repository at this point in the history

  8. Fix parameter order

    @RustanLeino
    RustanLeino committed Aug 21, 2024
    Configuration menu
    Copy the full SHA
    456afc5 View commit details
    Browse the repository at this point in the history

Commits on Aug 22, 2024

  1. Adjust tests and expected test output

    @RustanLeino
    RustanLeino committed Aug 22, 2024
    Configuration menu
    Copy the full SHA
    954dd42 View commit details
    Browse the repository at this point in the history

  2. Fix Boogie type of receiver in function-valued members

    @RustanLeino
    RustanLeino committed Aug 22, 2024
    Configuration menu
    Copy the full SHA
    3d617aa View commit details
    Browse the repository at this point in the history

  3. chore: Improve code

    @RustanLeino
    RustanLeino committed Aug 22, 2024
    Configuration menu
    Copy the full SHA
    fbec421 View commit details
    Browse the repository at this point in the history

  4. Add tests

    @RustanLeino
    RustanLeino committed Aug 22, 2024
    Configuration menu
    Copy the full SHA
    6ec3676 View commit details
    Browse the repository at this point in the history

  5. fix: Pass in original (overridden) member 

    This was discovered via Go compilation of traits/TraitCompile.dfy
    @RustanLeino
    RustanLeino committed Aug 22, 2024
    Configuration menu
    Copy the full SHA
    68ce112 View commit details
    Browse the repository at this point in the history

  6. Pass CLI parameter values explicitly

    @RustanLeino
    RustanLeino committed Aug 22, 2024
    Configuration menu
    Copy the full SHA
    2d45cf6 View commit details
    Browse the repository at this point in the history

  7. Prescribe type-refinement flows for SeqUpdateExpr

    @RustanLeino
    RustanLeino committed Aug 22, 2024
    Configuration menu
    Copy the full SHA
    867a207 View commit details
    Browse the repository at this point in the history

  8. Add some temporary casts, waiting for flows to do more with bounded p… 

    …olymorphism
    @RustanLeino
    RustanLeino committed Aug 22, 2024
    Configuration menu
    Copy the full SHA
    289a996 View commit details
    Browse the repository at this point in the history

  9. Update tests and results

    @RustanLeino
    RustanLeino committed Aug 22, 2024
    Configuration menu
    Copy the full SHA
    785e4cc View commit details
    Browse the repository at this point in the history

  10. Update tests and expected results

    @RustanLeino
    RustanLeino committed Aug 22, 2024
    Configuration menu
    Copy the full SHA
    a442d33 View commit details
    Browse the repository at this point in the history

  11. Update tests and expected test output

    @RustanLeino
    RustanLeino committed Aug 22, 2024
    Configuration menu
    Copy the full SHA
    bddc2ce View commit details
    Browse the repository at this point in the history

  12. fix: Fix a printing crash 

    Detected by dafny4/Lucas-down.legacy.dfy and dafny4/Lucas-up.legacy.dfy
    @RustanLeino
    RustanLeino committed Aug 22, 2024
    Configuration menu
    Copy the full SHA
    cec4940 View commit details
    Browse the repository at this point in the history

Commits on Aug 23, 2024

  1. Update tests and expected output

    @RustanLeino
    RustanLeino committed Aug 23, 2024
    Configuration menu
    Copy the full SHA
    272bfe4 View commit details
    Browse the repository at this point in the history

  2. Update tests

    @RustanLeino
    RustanLeino committed Aug 23, 2024
    Configuration menu
    Copy the full SHA
    35f4877 View commit details
    Browse the repository at this point in the history

  3. Use basename for filename in %translate test

    @RustanLeino
    RustanLeino committed Aug 23, 2024
    Configuration menu
    Copy the full SHA
    a6bebff View commit details
    Browse the repository at this point in the history

  4. Update test output

    @RustanLeino
    RustanLeino committed Aug 23, 2024
    Configuration menu
    Copy the full SHA
    c44b7f8 View commit details
    Browse the repository at this point in the history

  5. fix: Report error (and don’t crash) on disjunctive patterns inside ot… 

    …her patterns
    @RustanLeino
    RustanLeino committed Aug 23, 2024
    Configuration menu
    Copy the full SHA
    044d6e6 View commit details
    Browse the repository at this point in the history

  6. Expect errors for missing parentheses of non-nullary constructors in … 

    …match-case
    @RustanLeino
    RustanLeino committed Aug 23, 2024
    Configuration menu
    Copy the full SHA
    f35922c View commit details
    Browse the repository at this point in the history

  7. Move {:only} warnings from pass 0 to pass 3

    @RustanLeino
    RustanLeino committed Aug 23, 2024
    Configuration menu
    Copy the full SHA
    af98137 View commit details
    Browse the repository at this point in the history

  8. Adjust tests and answers

    @RustanLeino
    RustanLeino committed Aug 23, 2024
    Configuration menu
    Copy the full SHA
    8eadfea View commit details
    Browse the repository at this point in the history

  9. Use nested comparable-types constraints as default advice

    @RustanLeino
    RustanLeino committed Aug 23, 2024
    Configuration menu
    Copy the full SHA
    2beb41f View commit details
    Browse the repository at this point in the history

Commits on Aug 24, 2024

  1. fix: Subrange check and conversions to arrow types

    @RustanLeino
    RustanLeino committed Aug 24, 2024
    Configuration menu
    Copy the full SHA
    f9ca74e View commit details
    Browse the repository at this point in the history

  2. Handle “as” for datatypes and arrows in compilers and verifier

    @RustanLeino
    RustanLeino committed Aug 24, 2024
    Configuration menu
    Copy the full SHA
    be77ce8 View commit details
    Browse the repository at this point in the history

  3. Adjust tests

    @RustanLeino
    RustanLeino committed Aug 24, 2024
    Configuration menu
    Copy the full SHA
    8dcd806 View commit details
    Browse the repository at this point in the history

  4. Adjust tests and answers

    @RustanLeino
    RustanLeino committed Aug 24, 2024
    Configuration menu
    Copy the full SHA
    50c4987 View commit details
    Browse the repository at this point in the history

  5. Adjust tests and outputs

    @RustanLeino
    RustanLeino committed Aug 24, 2024
    Configuration menu
    Copy the full SHA
    d46da94 View commit details
    Browse the repository at this point in the history

  6. Adjust tests and outputs

    @RustanLeino
    RustanLeino committed Aug 24, 2024
    Configuration menu
    Copy the full SHA
    138b341 View commit details
    Browse the repository at this point in the history

  7. fix: Support “assigned” in new resolver

    @RustanLeino
    RustanLeino committed Aug 24, 2024
    Configuration menu
    Copy the full SHA
    a73d698 View commit details
    Browse the repository at this point in the history

Commits on Aug 27, 2024

  1. Fill in missing case in type cloning

    @RustanLeino
    RustanLeino committed Aug 27, 2024
    Configuration menu
    Copy the full SHA
    bfb9100 View commit details
    Browse the repository at this point in the history

Commits on Aug 28, 2024

  1. fix: Print DecreasesToExpr with parentheses

    @RustanLeino
    RustanLeino committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    5cb67b9 View commit details
    Browse the repository at this point in the history

  2. Don’t update RangeToken when resolving ParensExpression

    @RustanLeino
    RustanLeino committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    2c3db7b View commit details
    Browse the repository at this point in the history

  3. Use sub/equal constraints to make type decisions

    @RustanLeino
    RustanLeino committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    b0739ec View commit details
    Browse the repository at this point in the history

  4. Update improved (reduced) error messages

    @RustanLeino
    RustanLeino committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    32a995a View commit details
    Browse the repository at this point in the history

  5. Update test and answers

    @RustanLeino
    RustanLeino committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    04be175 View commit details
    Browse the repository at this point in the history

  6. Merge branch 'master' into refresh-by-default 

    # Conflicts:
#	Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy.expect
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect
    @RustanLeino
    RustanLeino committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    c940168 View commit details
    Browse the repository at this point in the history

Commits on Sep 3, 2024

  1. Validate resolution CLI options (at a terrible place in the code)

    @RustanLeino
    RustanLeino committed Sep 3, 2024
    Configuration menu
    Copy the full SHA
    e29ded6 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into refresh-by-default 

    # Conflicts:
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect
    @RustanLeino
    RustanLeino committed Sep 3, 2024
    Configuration menu
    Copy the full SHA
    16a91fe View commit details
    Browse the repository at this point in the history

  3. Correct previous compensation

    @RustanLeino
    RustanLeino committed Sep 3, 2024
    Configuration menu
    Copy the full SHA
    5a7f699 View commit details
    Browse the repository at this point in the history

Commits on Sep 4, 2024

  1. Merge branch 'master' into refresh-by-default

    @RustanLeino
    RustanLeino committed Sep 4, 2024
    Configuration menu
    Copy the full SHA
    6bc0bab View commit details
    Browse the repository at this point in the history

  2. Fix test script for git-issue-321

    @RustanLeino
    RustanLeino committed Sep 4, 2024
    Configuration menu
    Copy the full SHA
    8d83506 View commit details
    Browse the repository at this point in the history

  3. fix: Include case for BVNot

    @RustanLeino
    RustanLeino committed Sep 4, 2024
    Configuration menu
    Copy the full SHA
    110ff22 View commit details
    Browse the repository at this point in the history

  4. Adjust test outputs

    @RustanLeino
    RustanLeino committed Sep 4, 2024
    Configuration menu
    Copy the full SHA
    ba1b866 View commit details
    Browse the repository at this point in the history

Commits on Sep 5, 2024

  1. Merge branch 'master' into refresh-by-default 

    # Conflicts:
#	Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs
#	Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/AsIs-Compile-Expanded.dfy
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismCompilation.dfy
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismVerification.dfy
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy.expect
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefreshErrors.dfy.expect
    @RustanLeino
    RustanLeino committed Sep 5, 2024
    Configuration menu
    Copy the full SHA
    e691271 View commit details
    Browse the repository at this point in the history

Commits on Sep 26, 2024

  1. Adjust tests

    @RustanLeino
    RustanLeino committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    4ba909c View commit details
    Browse the repository at this point in the history

  2. Adjust tests

    @RustanLeino
    RustanLeino committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    3dbd746 View commit details
    Browse the repository at this point in the history

Commits on Sep 27, 2024

  1. Start adjusting test

    @RustanLeino
    RustanLeino committed Sep 27, 2024
    Configuration menu
    Copy the full SHA
    737c57c View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into refresh-by-default

    @RustanLeino
    RustanLeino committed Sep 27, 2024
    Configuration menu
    Copy the full SHA
    3b54b7e View commit details
    Browse the repository at this point in the history

Commits on Oct 4, 2024

  1. Merge branch 'master' into refresh-by-default

    @RustanLeino
    RustanLeino committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    27faf49 View commit details
    Browse the repository at this point in the history

  2. Adjust tests and answers

    @RustanLeino
    RustanLeino committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    feeaa06 View commit details
    Browse the repository at this point in the history

Commits on Oct 5, 2024

  1. Adjust tests and answers

    @RustanLeino
    RustanLeino committed Oct 5, 2024
    Configuration menu
    Copy the full SHA
    6652b68 View commit details
    Browse the repository at this point in the history

  2. chore: Improve C#

    @RustanLeino
    RustanLeino committed Oct 5, 2024
    Configuration menu
    Copy the full SHA
    006c8af View commit details
    Browse the repository at this point in the history

  3. fix: Incorporate explicit type arguments for function calls and datat… 

    …ype values
    @RustanLeino
    RustanLeino committed Oct 5, 2024
    Configuration menu
    Copy the full SHA
    ad77757 View commit details
    Browse the repository at this point in the history

Commits on Oct 7, 2024

  1. Merge branch 'master' into refresh-by-default 

    # Conflicts:
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect
    @RustanLeino
    RustanLeino committed Oct 7, 2024
    Configuration menu
    Copy the full SHA
    1a6ea55 View commit details
    Browse the repository at this point in the history

Commits on Oct 8, 2024

  1. Adjust tests

    @RustanLeino
    RustanLeino committed Oct 8, 2024
    Configuration menu
    Copy the full SHA
    a79a23e View commit details
    Browse the repository at this point in the history

  2. Add “extends object” to tests

    @RustanLeino
    RustanLeino committed Oct 8, 2024
    Configuration menu
    Copy the full SHA
    7466e28 View commit details
    Browse the repository at this point in the history