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

Introduce support for closures #479

Merged
merged 74 commits into from
Aug 2, 2022
Merged

Introduce support for closures #479

merged 74 commits into from
Aug 2, 2022

Commits on Jun 16, 2022

  1. Extend parser with closure literal

    @stefanomil
    stefanomil committed Jun 16, 2022
    Configuration menu
    Copy the full SHA
    a124382 View commit details
    Browse the repository at this point in the history

  2. Temporary

    Stefano Milizia committed Jun 16, 2022
    Configuration menu
    Copy the full SHA
    196f21d View commit details
    Browse the repository at this point in the history

  3. Type checking for function literals

    @stefanomil
    stefanomil committed Jun 16, 2022
    Configuration menu
    Copy the full SHA
    9e51fcd View commit details
    Browse the repository at this point in the history

Commits on Jun 20, 2022

  1. Internal Program object

    @stefanomil
    stefanomil committed Jun 20, 2022
    Configuration menu
    Copy the full SHA
    3e88b91 View commit details
    Browse the repository at this point in the history

  2. Use correct substitutions within function literals

    Stefano Milizia committed Jun 20, 2022
    Configuration menu
    Copy the full SHA
    81f23af View commit details
    Browse the repository at this point in the history

Commits on Jun 22, 2022

  1. Within desugaring, replace captured variables with their reference

    @stefanomil
    stefanomil committed Jun 22, 2022
    Configuration menu
    Copy the full SHA
    8074c58 View commit details
    Browse the repository at this point in the history

  2. Fix Ghostless printer

    @stefanomil
    stefanomil committed Jun 22, 2022
    Configuration menu
    Copy the full SHA
    5899a4b View commit details
    Browse the repository at this point in the history

Commits on Jun 23, 2022

  1. Implement parsing, type checking and desugaring of function literals

    @stefanomil
    stefanomil committed Jun 23, 2022
    Configuration menu
    Copy the full SHA
    58e97e6 View commit details
    Browse the repository at this point in the history

  2. Fix warnings, finish implementation of desugarer

    @stefanomil
    stefanomil committed Jun 23, 2022
    Configuration menu
    Copy the full SHA
    3f06a40 View commit details
    Browse the repository at this point in the history

Commits on Jun 24, 2022

  1. Implement encoding of function literals, including encoding of closur… 

    …e domain, satisfies functions, default getter
    @stefanomil
    stefanomil committed Jun 24, 2022
    Configuration menu
    Copy the full SHA
    6461255 View commit details
    Browse the repository at this point in the history

Commits on Jun 25, 2022

  1. Small refactorings

    @stefanomil
    stefanomil committed Jun 25, 2022
    Configuration menu
    Copy the full SHA
    1843cfb View commit details
    Browse the repository at this point in the history

Commits on Jun 26, 2022

  1. Implement parsing and type checking of closure spec instances and imp… 

    …lements expressions
    @stefanomil
    stefanomil committed Jun 26, 2022
    Configuration menu
    Copy the full SHA
    5ad042f View commit details
    Browse the repository at this point in the history

  2. Implement desugaring and encoding of spec instance literals and imple… 

    …ments assertion
    @stefanomil
    stefanomil committed Jun 26, 2022
    Configuration menu
    Copy the full SHA
    d9aab4d View commit details
    Browse the repository at this point in the history

Commits on Jun 28, 2022

  1. Add support for treating method members as closures

    @stefanomil
    stefanomil committed Jun 28, 2022
    Configuration menu
    Copy the full SHA
    3c84e74 View commit details
    Browse the repository at this point in the history

Commits on Jun 30, 2022

  1. Implement encoding of closure calls

    @stefanomil
    stefanomil committed Jun 30, 2022
    Configuration menu
    Copy the full SHA
    abbd708 View commit details
    Browse the repository at this point in the history

Commits on Jul 1, 2022

  1. Implement parsing and type checking of closure implementation proofs

    @stefanomil
    stefanomil committed Jul 1, 2022
    Configuration menu
    Copy the full SHA
    281e332 View commit details
    Browse the repository at this point in the history

Commits on Jul 4, 2022

  1. Introduce desugaring and encoding of spec proof statements

    @stefanomil
    stefanomil committed Jul 4, 2022
    Configuration menu
    Copy the full SHA
    d7d2c32 View commit details
    Browse the repository at this point in the history

  2. In spec implementation proofs, introduce an alias for the closure to … 

    …avoid access permissions problems
    Stefano Milizia committed Jul 4, 2022
    Configuration menu
    Copy the full SHA
    6cdef71 View commit details
    Browse the repository at this point in the history

  3. Fixes

    Stefano Milizia committed Jul 4, 2022
    Configuration menu
    Copy the full SHA
    f46a039 View commit details
    Browse the repository at this point in the history

Commits on Jul 5, 2022

  1. Introduce closure objects, fix ghostness of function and method const… 

    …ants
    Stefano Milizia committed Jul 5, 2022
    Configuration menu
    Copy the full SHA
    af1f7f7 View commit details
    Browse the repository at this point in the history

Commits on Jul 6, 2022

  1. Add ghost erasure tests

    Stefano Milizia committed Jul 6, 2022
    Configuration menu
    Copy the full SHA
    d4cbe30 View commit details
    Browse the repository at this point in the history

  2. Try to support importing packages

    Stefano Milizia committed Jul 6, 2022
    Configuration menu
    Copy the full SHA
    e5a63fa View commit details
    Browse the repository at this point in the history

Commits on Jul 8, 2022

  1. Add fixes to support closures when importing packages

    @stefanomil
    stefanomil committed Jul 8, 2022
    Configuration menu
    Copy the full SHA
    f881c5e View commit details
    Browse the repository at this point in the history

  2. Extend type checking to make sure that closure names are not use impr… 

    …operly
    @stefanomil
    stefanomil committed Jul 8, 2022
    Configuration menu
    Copy the full SHA
    19097a3 View commit details
    Browse the repository at this point in the history

  3. Refactor name resolution

    @stefanomil
    stefanomil committed Jul 8, 2022
    Configuration menu
    Copy the full SHA
    e18eab5 View commit details
    Browse the repository at this point in the history

  4. Fix ghostness checks for closure calls and spec implementation proofs

    @stefanomil
    stefanomil committed Jul 8, 2022
    Configuration menu
    Copy the full SHA
    0396833 View commit details
    Browse the repository at this point in the history

  5. Fix warnings

    @stefanomil
    stefanomil committed Jul 8, 2022
    Configuration menu
    Copy the full SHA
    debbd03 View commit details
    Browse the repository at this point in the history

  6. Fix errors if spec name not found

    @stefanomil
    stefanomil committed Jul 8, 2022
    Configuration menu
    Copy the full SHA
    febcb34 View commit details
    Browse the repository at this point in the history

  7. Fix error, improve how the encoding deals with pure functions or lite… 

    …rals
    @stefanomil
    stefanomil committed Jul 8, 2022
    Configuration menu
    Copy the full SHA
    7e92e3e View commit details
    Browse the repository at this point in the history

Commits on Jul 9, 2022

  1. Fix bugs, add examples

    @stefanomil
    stefanomil committed Jul 9, 2022
    Configuration menu
    Copy the full SHA
    5b20bad View commit details
    Browse the repository at this point in the history

  2. add closure import tests

    @stefanomil
    stefanomil committed Jul 9, 2022
    Configuration menu
    Copy the full SHA
    d9aaccc View commit details
    Browse the repository at this point in the history

Commits on Jul 10, 2022

  1. Fix bugs

    @stefanomil
    stefanomil committed Jul 10, 2022
    Configuration menu
    Copy the full SHA
    482fec2 View commit details
    Browse the repository at this point in the history

  2. Add comments

    @stefanomil
    stefanomil committed Jul 10, 2022
    Configuration menu
    Copy the full SHA
    6cc4157 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into closures

    @stefanomil
    stefanomil committed Jul 10, 2022
    Configuration menu
    Copy the full SHA
    8f931b9 View commit details
    Browse the repository at this point in the history

  4. Fix bug

    @stefanomil
    stefanomil committed Jul 10, 2022
    Configuration menu
    Copy the full SHA
    8142a05 View commit details
    Browse the repository at this point in the history

Commits on Jul 11, 2022

  1. Add comments, fix parser

    @stefanomil
    stefanomil committed Jul 11, 2022
    Configuration menu
    Copy the full SHA
    324b81e View commit details
    Browse the repository at this point in the history

  2. Rename some files/classes

    @stefanomil
    stefanomil committed Jul 11, 2022
    Configuration menu
    Copy the full SHA
    7005e55 View commit details
    Browse the repository at this point in the history

  3. Fix Goification, add copyright headers to all new files

    @stefanomil
    stefanomil committed Jul 11, 2022
    Configuration menu
    Copy the full SHA
    225aa9b View commit details
    Browse the repository at this point in the history

  4. Fix test

    @stefanomil
    stefanomil committed Jul 11, 2022
    Configuration menu
    Copy the full SHA
    226fdc4 View commit details
    Browse the repository at this point in the history

Commits on Jul 12, 2022

  1. Fix custom error condition

    @stefanomil
    stefanomil committed Jul 12, 2022
    Configuration menu
    Copy the full SHA
    40dac97 View commit details
    Browse the repository at this point in the history

  2. Remove blank line

    @stefanomil
    stefanomil committed Jul 12, 2022
    Configuration menu
    Copy the full SHA
    ba8354e View commit details
    Browse the repository at this point in the history

  3. Fix bug causing violation

    @stefanomil
    stefanomil committed Jul 12, 2022
    Configuration menu
    Copy the full SHA
    97e7ce0 View commit details
    Browse the repository at this point in the history

Commits on Jul 14, 2022

  1. Encode function nil, fix error message for closure calls

    @stefanomil
    stefanomil committed Jul 14, 2022
    Configuration menu
    Copy the full SHA
    e3da4e2 View commit details
    Browse the repository at this point in the history

  2. Add test examples, fix bug causing crash while type checking

    @stefanomil
    stefanomil committed Jul 14, 2022
    Configuration menu
    Copy the full SHA
    65178dc View commit details
    Browse the repository at this point in the history

Commits on Jul 15, 2022

  1. More test cases (including examples with call descriptions)

    @stefanomil
    stefanomil committed Jul 15, 2022
    Configuration menu
    Copy the full SHA
    23194c8 View commit details
    Browse the repository at this point in the history

Commits on Jul 17, 2022

  1. Fix encoding of captured variables as domain functions (allowing type… 

    …s different from Ref)
    @stefanomil
    stefanomil committed Jul 17, 2022
    Configuration menu
    Copy the full SHA
    c9135d5 View commit details
    Browse the repository at this point in the history

Commits on Jul 18, 2022

  1. Remove changes made for debugging and left there by mistake

    @stefanomil
    stefanomil committed Jul 18, 2022
    Configuration menu
    Copy the full SHA
    3b4e853 View commit details
    Browse the repository at this point in the history

  2. Make ClosureImplements a ghost expression (instead of an assertion), … 

    …allow shareable closure arguments
    @stefanomil
    stefanomil committed Jul 18, 2022
    Configuration menu
    Copy the full SHA
    4d6a5a6 View commit details
    Browse the repository at this point in the history

  3. Address some comments (mainly refactorings)

    @stefanomil
    stefanomil committed Jul 18, 2022
    Configuration menu
    Copy the full SHA
    e4a5522 View commit details
    Browse the repository at this point in the history

  4. Remove PClosureNamedDecl

    @stefanomil
    stefanomil committed Jul 18, 2022
    Configuration menu
    Copy the full SHA
    e173a2b View commit details
    Browse the repository at this point in the history

Commits on Jul 19, 2022

  1. Address typing comments (name resolution in proofs, closure spec used… 

    … as operand)
    @stefanomil
    stefanomil committed Jul 19, 2022
    Configuration menu
    Copy the full SHA
    29d011d View commit details
    Browse the repository at this point in the history

  2. Delete PClosureSpecParameter, use PKeyedElement instead; regenerate A… 

    …NTLR sources
    @stefanomil
    stefanomil committed Jul 19, 2022
    Configuration menu
    Copy the full SHA
    e53eb54 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into closures

    @stefanomil
    stefanomil committed Jul 19, 2022
    Configuration menu
    Copy the full SHA
    7026797 View commit details
    Browse the repository at this point in the history

  4. Solve bug caused by merge

    @stefanomil
    stefanomil committed Jul 19, 2022
    Configuration menu
    Copy the full SHA
    b0f247f View commit details
    Browse the repository at this point in the history

  5. Remove PCallWithSpec and internal.CallWithSpec, use PInvoke and metho… 

    …d, function calls instead
    @stefanomil
    stefanomil committed Jul 19, 2022
    Configuration menu
    Copy the full SHA
    91b9076 View commit details
    Browse the repository at this point in the history

Commits on Jul 21, 2022

  1. Change one of the test examples to make it shorter

    @stefanomil
    stefanomil committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    2253a17 View commit details
    Browse the repository at this point in the history

  2. Fix bug causing crash (wrong value passed to error message)

    @stefanomil
    stefanomil committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    a2ff559 View commit details
    Browse the repository at this point in the history

Commits on Jul 23, 2022

  1. Introduce ClosureCall and PureClosureCall

    @stefanomil
    stefanomil committed Jul 23, 2022
    Configuration menu
    Copy the full SHA
    4d5c101 View commit details
    Browse the repository at this point in the history

Commits on Jul 24, 2022

  1. Fix termination-related problems with proof and function/method objects

    @stefanomil
    stefanomil committed Jul 24, 2022
    Configuration menu
    Copy the full SHA
    fbdab5d View commit details
    Browse the repository at this point in the history

  2. Fix bug

    @stefanomil
    stefanomil committed Jul 24, 2022
    Configuration menu
    Copy the full SHA
    26f551a View commit details
    Browse the repository at this point in the history

  3. Improve documentation of the encoding

    @stefanomil
    stefanomil committed Jul 24, 2022
    Configuration menu
    Copy the full SHA
    95756a5 View commit details
    Browse the repository at this point in the history

  4. Change a word in a comment

    @stefanomil
    stefanomil committed Jul 24, 2022
    Configuration menu
    Copy the full SHA
    be0165a View commit details
    Browse the repository at this point in the history

  5. Remove default value for info parameter in Desugar, other minor changes

    @stefanomil
    stefanomil committed Jul 24, 2022
    Configuration menu
    Copy the full SHA
    e8ef809 View commit details
    Browse the repository at this point in the history

Commits on Jul 25, 2022

  1. Change proof loop so that it actually terminates

    @stefanomil
    stefanomil committed Jul 25, 2022
    Configuration menu
    Copy the full SHA
    1c2e81c View commit details
    Browse the repository at this point in the history

  2. Simplify genConversion function in MethodObjectEncoder

    @stefanomil
    stefanomil committed Jul 25, 2022
    Configuration menu
    Copy the full SHA
    c494492 View commit details
    Browse the repository at this point in the history

Commits on Jul 27, 2022

  1. Fix ambiguity resolution between ClosureCall and FunctionCall, remove… 

    … termination measures when unnecessary
    @stefanomil
    stefanomil committed Jul 27, 2022
    Configuration menu
    Copy the full SHA
    2293edd View commit details
    Browse the repository at this point in the history

  2. Turn closureImplements$... functions into domain functions

    @stefanomil
    stefanomil committed Jul 27, 2022
    Configuration menu
    Copy the full SHA
    22fba67 View commit details
    Browse the repository at this point in the history

  3. Simplify preconditions for closureCall$ of closure obtained from func… 

    …tion literal
    @stefanomil
    stefanomil committed Jul 27, 2022
    Configuration menu
    Copy the full SHA
    c24fdb6 View commit details
    Browse the repository at this point in the history

  4. Refactor following advice in the comments, fix error message for clos… 

    …ure calls
    @stefanomil
    stefanomil committed Jul 27, 2022
    Configuration menu
    Copy the full SHA
    e10ad82 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'master' into closures

    @stefanomil
    stefanomil committed Jul 27, 2022
    Configuration menu
    Copy the full SHA
    d00566f View commit details
    Browse the repository at this point in the history

Commits on Aug 2, 2022

  1. Implement suggestions

    @stefanomil
    stefanomil committed Aug 2, 2022
    Configuration menu
    Copy the full SHA
    1ea27f3 View commit details
    Browse the repository at this point in the history

  2. Add comment from suggestion 

    Co-authored-by: Felix Wolf <[email protected]>
    @stefanomil @Felalolf
    stefanomil and Felalolf authored Aug 2, 2022
    Configuration menu
    Copy the full SHA
    f096233 View commit details
    Browse the repository at this point in the history

  3. Add suggested Experimental feature warning 

    Co-authored-by: Felix Wolf <[email protected]>
    @stefanomil @Felalolf
    stefanomil and Felalolf authored Aug 2, 2022
    Configuration menu
    Copy the full SHA
    b27ba31 View commit details
    Browse the repository at this point in the history

  4. Ensure that the Closure domain is only generated if there are closures

    @stefanomil
    stefanomil committed Aug 2, 2022
    Configuration menu
    Copy the full SHA
    35a4e8a View commit details
    Browse the repository at this point in the history