laurel: wire old() to Core two-state semantics#1203
Conversation
keyboardDrummer
left a comment
keyboardDrummer
left a comment
There was a problem hiding this comment.
Nice!! This feature is super useful to have. Love the reliance on Core's support for old.
| | .staticProcedure proc => proc.outputs | ||
| | .instanceProcedure _ proc => proc.outputs | ||
| | _ => [] | ||
| let (calleeInputs, calleeOutputs) := match model.get callee with |
There was a problem hiding this comment.
Can you extract the duplication between the two cases that handle StaticCall, the bare call and the assigning call?
| let id ← freshId | ||
| return LExpr.fvar () (⟨s!"DUMMY_VAR_{id}", ()⟩) none | ||
|
|
||
| private def oldifyExpr (inoutNames : List String) : Core.Expression.Expr → Core.Expression.Expr |
There was a problem hiding this comment.
Should there be a warning if old is pushed inward but hits no inout parameter?
Interesting to have this transformation at the Core level. Alternatively you can have a "PushOldInward" phase at the Laurel level that pushes old inwards until it hits identifiers, so LaurelToCoreTranslator only needs to support Old that immediately wraps an identifier. I think if you use mapStmtExprM then PushOldInward could be about as short as this function.
I think I would prefer that since it would move a little code out of LaurelToCoreTranslator and I prefer to keep this transformation as dumb as possible. Computing the Core in/inout/out arguments in LaurelToCoreTranslator is unfortunate but seems unavoidable unless we change Laurel.
| @@ -0,0 +1,92 @@ | |||
| /- | |||
There was a problem hiding this comment.
Since this PR is implicitly also adding support for inout parameters to Laurel, could you add a separate test for that? Could you also check how Resolution.lean currently deals with in and out parameters that have the same name? How come it is not reporting duplicate names in this PR ?
There was a problem hiding this comment.
resolveParameter calls defineNameCheckDup on every input and output, so a user-written procedure with the same name in both does get a duplicate-definition error at the initial resolve.
Is there's a user-facing way to declare an inout parameter today? I don't really know how to add a "user-declared inout" test... @keyboardDrummer
| module | ||
|
|
||
| /- | ||
| End-to-end coverage of the two-state path that runs through Core's |
There was a problem hiding this comment.
I'm confused about this test because the programs being tested do not use the old keyword. The tests here are for things that I think are already tested in T2_ModifiesClauses. I see that this PR also simplifies the implementation of ModifiesClauses.lean, but since that's a refactoring it shouldn't need additional testing. Could you replace the tests here with tests that use StmtExpr.Old ? Also, given your implementation, you could use old both for the implicit heap parameter, and for explicit inout parameters, so we should test both.
Secondly, this comment describes part of the implementation of StmtExpr.Old, which I think shouldn't be part of a test.
There was a problem hiding this comment.
You're right that the test programs don't write old(...) — turns out .Old has no Laurel surface syntax today. My bad
|
Note: this PR should target main2 given the ongoing Strata refactoring |
julesmt
force-pushed
the
julesmt/features/laurel-old-two-state
branch
from
67e3e0e to
8a153ae
Compare
github-actions
Bot
added
Git conflicts
Python
Core
GOTO
dependencies
Modifies-clause frame conditions now flow through Core's `old`-prefixed identifiers via Core's native two-state semantics, replacing the previous synthetic `$heap_in` parameter. 1. HeapParameterization: heap-writing procedures take `$heap` as a true inout parameter (same name in inputs and outputs) rather than a `$heap_in` / `$heap` pair with a synthesized assignment prelude. 2. ModifiesClauses: frame condition references `old($heap)` via `StmtExpr.Old` instead of a separate `$heap_in` variable. 3. New PushOldInward Laurel-to-Laurel pass: distributes `StmtExpr.Old` through its sub-expressions until each `Old` immediately wraps a Local Var. Warns if `old(...)` does not mention any inout parameter. 4. LaurelToCoreTranslator: `Old (Var (Local n))` translates directly to `fvar (mkOld n)`. Inout parameters at call sites are detected and emit `.inoutArg` rather than paired `.inArg` + `.outArg`. Call-arg construction is shared between the two StaticCall sites via a new buildCallArgs helper. Tests: PushOldInwardTest exercises the new pass on hand-built ASTs covering distribution over operators, calls, conditionals, fields, quantifiers, and the warning behaviour. Existing modifies-clause coverage in T2_ModifiesClauses already drives the synthetic `Old` path end-to-end.
julesmt
force-pushed
the
julesmt/features/laurel-old-two-state
branch
2 times, most recently
from
8a153ae to
2f9dfce
Compare
github-actions
Bot
removed
Python
Core
GOTO
dependencies
|
@keyboardDrummer I added changes, let me know what you think |
2 participants
laurel: wire old() to Core two-state semantics
Modifies-clause frame conditions now flow through Core's
old-prefixedidentifiers via Core's native two-state semantics, replacing the previous
synthetic
$heap_inparameter.HeapParameterization: heap-writing procedures take
$heapas a trueinout parameter (same name in inputs and outputs) rather than a
$heap_in/$heappair with a synthesized assignment prelude.ModifiesClauses: frame condition references
old($heap)viaStmtExpr.Oldinstead of a separate$heap_invariable.New PushOldInward Laurel-to-Laurel pass: distributes
StmtExpr.Oldthrough its sub-expressions until each
Oldimmediately wraps a LocalVar. Warns if
old(...)does not mention any inout parameter.LaurelToCoreTranslator:
Old (Var (Local n))translates directly tofvar (mkOld n). Inout parameters at call sites are detected and emit.inoutArgrather than paired.inArg+.outArg. Call-argconstruction is shared between the two StaticCall sites via a new
buildCallArgs helper.
Tests: PushOldInwardTest exercises the new pass on hand-built ASTs
covering distribution over operators, calls, conditionals, fields,
quantifiers, and the warning behaviour. Existing modifies-clause coverage
in T2_ModifiesClauses already drives the synthetic
Oldpath end-to-end.