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

feat: Datatype ghost constructors #2666

Merged
merged 47 commits into from
Sep 20, 2022
Merged

feat: Datatype ghost constructors #2666

merged 47 commits into from
Sep 20, 2022

Commits on Aug 31, 2022

  1. Add syntax for ghost constructors

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    6bcd5d5 View commit details
    Browse the repository at this point in the history

  2. Improve error messages

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    6e9681c View commit details
    Browse the repository at this point in the history

  3. Use subclass to distinguish discriminators from other SpecialFields

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    3aa3b15 View commit details
    Browse the repository at this point in the history

  4. Mark ghost-variant datatypes as not supporting equality

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    f4b39bd View commit details
    Browse the repository at this point in the history

  5. Add resolution tests

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    796cc09 View commit details
    Browse the repository at this point in the history

  6. Add resolution checks for match

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    affcac1 View commit details
    Browse the repository at this point in the history

  7. Check ghost constructors are used only in ghost contexts

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    3091bf1 View commit details
    Browse the repository at this point in the history

  8. Improve resolution

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    b1cab13 View commit details
    Browse the repository at this point in the history

  9. fix: Check expressions to be compilable

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    7c20ade View commit details
    Browse the repository at this point in the history

  10. Check precondition of discriminators and destructors in ghost-variant… 

    … datatypes
    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    3c4219f View commit details
    Browse the repository at this point in the history

  11. Add more bookkeeping info for DatatypeUpdateExpr

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    9fcfa34 View commit details
    Browse the repository at this point in the history

  12. Add verification tests for datatype update

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    4e784b1 View commit details
    Browse the repository at this point in the history

  13. Add additional test

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    429ec6c View commit details
    Browse the repository at this point in the history

  14. Reformat test

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    cb850d7 View commit details
    Browse the repository at this point in the history

  15. fix: datatype update resolution re ghosts

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    5746e9d View commit details
    Browse the repository at this point in the history

  16. Improve resolution checks for select/update

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    61c9a2f View commit details
    Browse the repository at this point in the history

  17. Update tests

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    09dbf9b View commit details
    Browse the repository at this point in the history

  18. Add compilation tests

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    aaf6d93 View commit details
    Browse the repository at this point in the history

  19. fix: Java compilation of array allocation must erase type args

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    8e968f8 View commit details
    Browse the repository at this point in the history

  20. Add motivating test program for ghost constructors

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    276200e View commit details
    Browse the repository at this point in the history

  21. Support partial equality (for ghost-variant datatypes)

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    dee6160 View commit details
    Browse the repository at this point in the history

  22. Don’t generate code for ghost constructors

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    14d65b9 View commit details
    Browse the repository at this point in the history

  23. Desugar DatatypeUpdateExpr twice (ghost and compiled)

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    2826da5 View commit details
    Browse the repository at this point in the history

  24. Compile

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    0c6bfff View commit details
    Browse the repository at this point in the history

  25. Take steps toward Python supporting ghost constructors 

    By trimming down the test file to features that the Python compiler currently support, I was able to make some changes to support ghost constructors. However, full support requires other features of the language that haven’t been addressed in the Python compiler yet.
    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    e8db13a View commit details
    Browse the repository at this point in the history

  26. Add release notes

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    d0c0177 View commit details
    Browse the repository at this point in the history

  27. Update release notes with PR number

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    843d27e View commit details
    Browse the repository at this point in the history

  28. Refactor to share more code

    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    2b299cc View commit details
    Browse the repository at this point in the history

  29. Merge branch 'master' into ghost-constructors-rfc-11 

    # Conflicts:
#	Source/Dafny/Compilers/Compiler-python.cs
    @RustanLeino
    RustanLeino committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    e715df5 View commit details
    Browse the repository at this point in the history

Commits on Sep 5, 2022

  1. Merge branch 'master' into ghost-constructors-rfc-11

    @fabiomadge
    fabiomadge authored Sep 5, 2022
    Configuration menu
    Copy the full SHA
    6b1c000 View commit details
    Browse the repository at this point in the history

Commits on Sep 6, 2022

  1. Python: it just works

    @fabiomadge
    fabiomadge committed Sep 6, 2022
    Configuration menu
    Copy the full SHA
    d0c9cfc View commit details
    Browse the repository at this point in the history

Commits on Sep 12, 2022

  1. Update Source/Dafny/Compilers/Compiler-python.cs 

    Co-authored-by: Fabio Madge <fabio@madge.me>
    @RustanLeino @fabiomadge
    RustanLeino and fabiomadge authored Sep 12, 2022
    Configuration menu
    Copy the full SHA
    9457cf7 View commit details
    Browse the repository at this point in the history

  2. Improve code as suggested by review comments

    @RustanLeino
    RustanLeino committed Sep 12, 2022
    Configuration menu
    Copy the full SHA
    913e9cd View commit details
    Browse the repository at this point in the history

  3. Merge branch 'ghost-constructors-rfc-11' of https://github.com/Rustan… 

    …Leino/dafny into ghost-constructors-rfc-11
    @RustanLeino
    RustanLeino committed Sep 12, 2022
    Configuration menu
    Copy the full SHA
    50979c5 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'master' into ghost-constructors-rfc-11 

    # Conflicts:
#	Source/Dafny/AST/DafnyAst.cs
    @RustanLeino
    RustanLeino committed Sep 12, 2022
    Configuration menu
    Copy the full SHA
    2420aa4 View commit details
    Browse the repository at this point in the history

Commits on Sep 13, 2022

  1. Fix merge

    @RustanLeino
    RustanLeino committed Sep 13, 2022
    Configuration menu
    Copy the full SHA
    2385b03 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into ghost-constructors-rfc-11

    @RustanLeino
    RustanLeino authored Sep 13, 2022
    Configuration menu
    Copy the full SHA
    a6bc864 View commit details
    Browse the repository at this point in the history

Commits on Sep 19, 2022

  1. Update Source/DafnyCore/Compilers/Compiler-Csharp.cs 

    Co-authored-by: Fabio Madge <fabio@madge.me>
    @RustanLeino @fabiomadge
    RustanLeino and fabiomadge authored Sep 19, 2022
    Configuration menu
    Copy the full SHA
    7bcc607 View commit details
    Browse the repository at this point in the history

  2. Improve comment

    @RustanLeino
    RustanLeino committed Sep 19, 2022
    Configuration menu
    Copy the full SHA
    e1e2f5c View commit details
    Browse the repository at this point in the history

  3. Use better C#

    @RustanLeino
    RustanLeino committed Sep 19, 2022
    Configuration menu
    Copy the full SHA
    b839f62 View commit details
    Browse the repository at this point in the history

  4. fix: Check for custom-receiver methods when emitting “this”

    @RustanLeino
    RustanLeino committed Sep 19, 2022
    Configuration menu
    Copy the full SHA
    5315dcd View commit details
    Browse the repository at this point in the history

  5. fix: Remove incorrect precondition

    @RustanLeino
    RustanLeino committed Sep 19, 2022
    Configuration menu
    Copy the full SHA
    c9d2255 View commit details
    Browse the repository at this point in the history

  6. Improve code based on review comments

    @RustanLeino
    RustanLeino committed Sep 19, 2022
    Configuration menu
    Copy the full SHA
    9ad188d View commit details
    Browse the repository at this point in the history

  7. Add sanity-check asserts

    @RustanLeino
    RustanLeino committed Sep 19, 2022
    Configuration menu
    Copy the full SHA
    0eb89dc View commit details
    Browse the repository at this point in the history

Commits on Sep 20, 2022

  1. Merge branch 'master' into ghost-constructors-rfc-11

    @RustanLeino
    RustanLeino committed Sep 20, 2022
    Configuration menu
    Copy the full SHA
    8112da5 View commit details
    Browse the repository at this point in the history

  2. Don’t emit unused Go variable for String() and Equals()

    @RustanLeino
    RustanLeino committed Sep 20, 2022
    Configuration menu
    Copy the full SHA
    72b919c View commit details
    Browse the repository at this point in the history

  3. Update .InCompiledContext only for serious CheckIsCompilable calls (n… 

    …ot querying calls)
    @RustanLeino
    RustanLeino committed Sep 20, 2022
    Configuration menu
    Copy the full SHA
    e067070 View commit details
    Browse the repository at this point in the history