Fix a bug in assignment extraction logic, and enable heap mutations in expression positions #358
Conversation
keyboardDrummer
changed the title
|
|
||
| def heapTransformProcedure (proc : Procedure) : TransformM Procedure := do | ||
| let heapName := "$heap" | ||
| let heapInName := "heap_in" |
There was a problem hiding this comment.
We may want to use some names that aren't legal variable names for user-written code.
| 3. Procedure calls are transformed: | ||
| - Calls to heap-writing procedures in expressions: | ||
| `f()` => `(var freshVar: type; freshVar, heap := f(heap); freshVar)` |
There was a problem hiding this comment.
Based on what you wrote below, should this be heap, freshVar := f(heap)?
| | Assign (target : StmtExpr) (value : StmtExpr) (md : Imperative.MetaData Core.Expression) | ||
| /- Assign is only allowed in an impure context. | ||
| For single target assignments, use a single-element list. | ||
| Multiple targets are only allowed when the value is a StaticCall to a procedure |
There was a problem hiding this comment.
Eventually, this should be enforced by a WF predicate or similar.
| for target in targets do | ||
| match target with | ||
| | .Identifier varName => | ||
| let snapshotName ← SequenceM.freshTempFor varName |
There was a problem hiding this comment.
How do you ensure there is not already a variable with this name?
| Returns the transformed expression with assignments replaced by variable references. | ||
| -/ | ||
| def transformExpr (expr : StmtExpr) : SequenceM StmtExpr := do | ||
| partial def transformExpr (expr : StmtExpr) : SequenceM StmtExpr := do |
| | [] => return .Block [] metadata | ||
| | [last] => transformExpr last | ||
| | _ => | ||
| -- Process all but the last statement |
There was a problem hiding this comment.
I am unclear on why you needed to change the let rec next ... structure. The head :: tail case there already handles all but the last statement (which matches the first case).
| -- For assignments in block context, we need to set snapshots | ||
| -- so that subsequent expressions see the correct values | ||
| -- IMPORTANT: Use transformTarget for targets (no snapshot substitution) | ||
| -- and transformExpr for values (with snapshot substitution) |
There was a problem hiding this comment.
I don't quite understand what this comment means. What is a snapshot exactly?
| Returns a list of statements (the original one may be split into multiple). | ||
| -/ | ||
| def transformStmt (stmt : StmtExpr) : SequenceM (List StmtExpr) := do | ||
| partial def transformStmt (stmt : StmtExpr) : SequenceM (List StmtExpr) := do |
There was a problem hiding this comment.
Same thing, we should avoid making things partial unless there is a good reason.
MikaelMayer
left a comment
MikaelMayer
left a comment
There was a problem hiding this comment.
I think it would be worth it to prove the termination of the function you annotated as partial. We have other cases in the codebase which have proof templates for proving termination easily, I hope you can apply one of them here.
| let postcond' ← heapTransformExpr heapInName postcond | ||
| let impl' ← impl.mapM (heapTransformExpr heapInName) | ||
| let modif' ← modif.mapM (heapTransformExpr heapInName) | ||
| pure (.Opaque postcond' impl' modif') |
There was a problem hiding this comment.
If you ever wanted to avoid parentheses, you could use the following idiom
| pure (.Opaque postcond' impl' modif') | |
| return .Opaque postcond' impl' modif' |
|
|
||
| def formatStmtExpr (s:StmtExpr) : Format := | ||
| match h: s with | ||
| match s with |
There was a problem hiding this comment.
Note: I don't know if it applies here but if you ever need to do termination proofs and naming the matches causes a spurious "unused variable" despite the variable being used in automatic proofs, you could also use '_' for the variable name.
| match s with | |
| match _: s with |
| Returns a list of statements (the original one may be split into multiple). | ||
| -/ | ||
| def transformStmt (stmt : StmtExpr) : SequenceM (List StmtExpr) := do | ||
| partial def transformStmt (stmt : StmtExpr) : SequenceM (List StmtExpr) := do |
There was a problem hiding this comment.
Can you try to prove termination?
4 participants
Changes
Testing
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.