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

Implement variable scopes, declarations and updates #5

Open
wants to merge 76 commits into
base: main
Choose a base branch
from
Open

Implement variable scopes, declarations and updates #5

wants to merge 76 commits into from

Commits on Aug 15, 2022

  1. Remove Expr.Bind and introduce Expr.VarDecl and Expr.Update

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    32b7c4a View commit details
    Browse the repository at this point in the history

  2. Update InterpExpr for VarDecl and Update

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    c138d9e View commit details
    Browse the repository at this point in the history

  3. Start updating the proofs in BottomUp

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    5c764d9 View commit details
    Browse the repository at this point in the history

  4. Prove the map lifting theorem for the Var, VarDecl and Update cases

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    927114f View commit details
    Browse the repository at this point in the history

  5. Update the definition of EqState and fix the proofs

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    c0fff19 View commit details
    Browse the repository at this point in the history

  6. Make blocks behave like variable scopes and start updating proofs

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    8bfc11e View commit details
    Browse the repository at this point in the history

  7. Factorize code a bit

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    621fc6f View commit details
    Browse the repository at this point in the history

  8. Detail a comment about a problematic proof (EqInterp_Expr_EqState)

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    2fb8ab4 View commit details
    Browse the repository at this point in the history

  9. Change the decreases measure in BottomUp

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    2c8c9df View commit details
    Browse the repository at this point in the history

  10. Simplify the proofs in BottomUp

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    05dfee4 View commit details
    Browse the repository at this point in the history

  11. Start working on an induction principle for Interp

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    756a2cf View commit details
    Browse the repository at this point in the history

  12. Factorize some proofs in ExprInduction

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    3390532 View commit details
    Browse the repository at this point in the history

  13. Factorize some proofs and make progress on ExprInduction

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    05844d9 View commit details
    Browse the repository at this point in the history

  14. Make more progress on the proofs of ExprInduction.EqInterpRefl

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    edaecaf View commit details
    Browse the repository at this point in the history

  15. Make progress on the proofs of ExprInduction

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    5ecacfe View commit details
    Browse the repository at this point in the history

  16. Simplify InductIf_Succ

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    0bf0167 View commit details
    Browse the repository at this point in the history

  17. Prove the ApplyLazy lemmas in ExprInduction.EqInterpRefl

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    77ab624 View commit details
    Browse the repository at this point in the history

  18. Simplify the InductAbs proofs

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    a3ca9d2 View commit details
    Browse the repository at this point in the history

  19. Make progress on ExprInduction

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    cfb1e78 View commit details
    Browse the repository at this point in the history

  20. Prove the Pes_Satisfied lemma in ExprInduction

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    842118b View commit details
    Browse the repository at this point in the history

  21. Fix a termination proof in ExprInduction

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    96e8288 View commit details
    Browse the repository at this point in the history

  22. Add a comment

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    91c0f93 View commit details
    Browse the repository at this point in the history

  23. Cleanup a bit

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    b3a05ad View commit details
    Browse the repository at this point in the history

  24. Start working on EqInterp_Scopes

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    b2ddeae View commit details
    Browse the repository at this point in the history

  25. Finish the proofs for EqInterp_Scopes

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    7c9d8fe View commit details
    Browse the repository at this point in the history

  26. Add a comment for InterpBlock_Exprs

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    8bfb290 View commit details
    Browse the repository at this point in the history

  27. Make minor modifications

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    8612210 View commit details
    Browse the repository at this point in the history

  28. Identify failing proofs in BottomUp

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    b7d863f View commit details
    Browse the repository at this point in the history

  29. Fix BottomUp.dfy

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    9b25ae1 View commit details
    Browse the repository at this point in the history

  30. Start fixing the proofs in SimplifyEmptyBlocks

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    d915a81 View commit details
    Browse the repository at this point in the history

  31. Fix a small mistake

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    28f9735 View commit details
    Browse the repository at this point in the history

  32. Make progress on updating SimplifyEmptyBlocks

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    86a4441 View commit details
    Browse the repository at this point in the history

  33. Make progress on EqInterpScopes

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    3b4348f View commit details
    Browse the repository at this point in the history

  34. Finish fixing the proofs in SimplifyEmptyBlocks

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    d72a822 View commit details
    Browse the repository at this point in the history

  35. Make minor modifications

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    7ed8fe5 View commit details
    Browse the repository at this point in the history

  36. Make minor modifications

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    aa8049f View commit details
    Browse the repository at this point in the history

  37. Add a comment

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    68b9c8a View commit details
    Browse the repository at this point in the history

  38. Factorize EqInterpRefl and EqInterpScopes

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    f64bca8 View commit details
    Browse the repository at this point in the history

  39. Add comments

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    ae13d93 View commit details
    Browse the repository at this point in the history

  40. Inline InterpBlock in InterpExpr cleanup some proofs

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    fb9d581 View commit details
    Browse the repository at this point in the history

  41. Inline InterpLazy in InterpExpr and cleanup a bit ExprInduction

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    ffdd9a2 View commit details
    Browse the repository at this point in the history

  42. Update some lemmas in ExprInduction

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    a230df2 View commit details
    Browse the repository at this point in the history

  43. Update a comment

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    e3edb4f View commit details
    Browse the repository at this point in the history

  44. Denest some modules

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    eb0e35f View commit details
    Browse the repository at this point in the history

  45. Change some names

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    e383151 View commit details
    Browse the repository at this point in the history

  46. Update some comments

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    20bab4e View commit details
    Browse the repository at this point in the history

  47. Update EqValue and fix an issue with InterpTernaryOp_Eq

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    d0afed7 View commit details
    Browse the repository at this point in the history

  48. Make minor modifications

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    09d79da View commit details
    Browse the repository at this point in the history

  49. Update Compiler.dfy

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    eaafcd2 View commit details
    Browse the repository at this point in the history

  50. Add a comment

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    aa040b3 View commit details
    Browse the repository at this point in the history

  51. Update Value.HasType

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    482b0c3 View commit details
    Browse the repository at this point in the history

  52. readme: Improve build instructions

    @cpitclaudel @sonmarcho
    cpitclaudel authored and sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    13a69ee View commit details
    Browse the repository at this point in the history

  53. Update Compiler.dfy to use SimplifyEmptyBlocks

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    e10c056 View commit details
    Browse the repository at this point in the history

  54. Update InterpLazy

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    dbf6284 View commit details
    Browse the repository at this point in the history

  55. Put Bind back in the AST

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    b1c4ec1 View commit details
    Browse the repository at this point in the history

  56. Add a comment

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    9078e5b View commit details
    Browse the repository at this point in the history

  57. Make minor modifications

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    926640b View commit details
    Browse the repository at this point in the history

  58. Make minor modifications

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    5af24e4 View commit details
    Browse the repository at this point in the history

  59. Update the translation

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    a2b3b9c View commit details
    Browse the repository at this point in the history

  60. Update src/AST/Translator.dfy 

    Co-authored-by: Clément Pit-Claudel <[email protected]>
    @sonmarcho @cpitclaudel
    sonmarcho and cpitclaudel committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    86a4f28 View commit details
    Browse the repository at this point in the history

  61. Update src/Semantics/Interp.dfy 

    Co-authored-by: Clément Pit-Claudel <[email protected]>
    @sonmarcho @cpitclaudel
    sonmarcho and cpitclaudel committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    31370cb View commit details
    Browse the repository at this point in the history

  62. Update src/Semantics/Interp.dfy 

    Co-authored-by: Clément Pit-Claudel <[email protected]>
    @sonmarcho @cpitclaudel
    sonmarcho and cpitclaudel committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    bcbd5bc View commit details
    Browse the repository at this point in the history

  63. Rewrite Expr.Size in a recursive manner and make minor cleanup

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    ae6859b View commit details
    Browse the repository at this point in the history

  64. Cleanup

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    ac02249 View commit details
    Browse the repository at this point in the history

  65. Remove the bind to vardecl desugaring from Translator.dfy

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    881231b View commit details
    Browse the repository at this point in the history

  66. Fix the compiled code

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    5409f32 View commit details
    Browse the repository at this point in the history

  67. Cleanup

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    81b7a69 View commit details
    Browse the repository at this point in the history

  68. Rename HasEqValue to ValueHasEq

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    b8623af View commit details
    Browse the repository at this point in the history

  69. Cleanup

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    3953e63 View commit details
    Browse the repository at this point in the history

  70. Add a comment to InterpBlock_Exprs

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    9e1af92 View commit details
    Browse the repository at this point in the history

  71. Cleanup

    @sonmarcho
    sonmarcho committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    68ab8a6 View commit details
    Browse the repository at this point in the history

Commits on Aug 18, 2022

  1. Add more cases to Translator.dfy

    @sonmarcho
    sonmarcho committed Aug 18, 2022
    Configuration menu
    Copy the full SHA
    0d9dfba View commit details
    Browse the repository at this point in the history

  2. Fix TranslateVarDeclStmt

    @sonmarcho
    sonmarcho committed Aug 18, 2022
    Configuration menu
    Copy the full SHA
    bc2dc8e View commit details
    Browse the repository at this point in the history

  3. Add loops to the AST and update the proofs

    @sonmarcho
    sonmarcho committed Aug 18, 2022
    Configuration menu
    Copy the full SHA
    8e05617 View commit details
    Browse the repository at this point in the history

  4. Update Translator to handle conversions

    @sonmarcho
    sonmarcho committed Aug 18, 2022
    Configuration menu
    Copy the full SHA
    b94c363 View commit details
    Browse the repository at this point in the history

Commits on Aug 25, 2022

  1. Update the project hierarchy in the README

    @sonmarcho
    sonmarcho committed Aug 25, 2022
    Configuration menu
    Copy the full SHA
    c231d58 View commit details
    Browse the repository at this point in the history