Implement variable scopes, declarations and updates #5
Conversation
| // because we desugar let-bindings to a scope containing an initialized variable declaration. | ||
| // We could make ``Pure1`` pattern match on `VarDecl` followed by `Update` operating on the | ||
| // same variables, but then we couldn't use the `Predicates.Deep.All_Expr` function to lift | ||
| // this definition. |
There was a problem hiding this comment.
Do we actually want to treat vardecls as pure?
There was a problem hiding this comment.
At the time I wrote this comment, I had removed the Bind construct from the AST (before putting it back later).
Following the discussion we had this morning about using let-bindings to make the proofs simpler, then converting them to scope + vardecl later in the compilation process: this comment is even less relevant now.
I didn't have much problems with the fact that this duplicates a bit Update so far (the additional work is limited), but today I see no problem in removing the optional initialization values from VarDecl.
There was a problem hiding this comment.
Note from chat: can't always decompose (var x := x + 1)
| // DISCUSS: we need to check that the variables have been declared, but there is actually | ||
| // no way to do that for now (a variable declared but not initialized doesn't appear in the | ||
| // environment - a variable declaration may only update the rollback context). But is not | ||
| // checking that variables have been declared really a problem? |
There was a problem hiding this comment.
I think it is a problem: accepting programs with undeclared variables means that we won't catch passes that fail to declare their variables.
Of course it's not an issue if we separately check that, but if we make this an invariant of the expr type then local transformations become complicated.
There was a problem hiding this comment.
Let's discuss that: I can easily update the context to track this.
There was a problem hiding this comment.
Let's table this for later; can you create an issue?
Co-authored-by: Clément Pit-Claudel <[email protected]>
Co-authored-by: Clément Pit-Claudel <[email protected]>
Co-authored-by: Clément Pit-Claudel <[email protected]>
sonmarcho
force-pushed
the
sonmho-scope
branch
from
c4eefc7
to
5409f32
Compare
This PR implements variable scopes, declarations and updates.
It also implements an induction principle for the interpreter (see
ExprInduction), which was necessary to update the proofs inSimplifyEmptyBlocks.