feat(laurel): Adding surface syntax for calling instance procedures & lowering to Core#1328
Merged
olivier-aws merged 13 commits intoJun 16, 2026
Conversation
Adds a new Laurel-to-Laurel pass that lifts every procedure defined inside a `composite` block to a top-level static procedure named `<CompositeName>_<methodName>` and rewrites every call site whose callee resolved to an instance procedure to use the lifted name. The pass runs before HeapParameterization, so by the time downstream passes run, every composite's `instanceProcedures` is empty. Removes the blocking NotYetImplemented diagnostic in LaurelToCoreTranslator and simplifies HeapParameterization's per-composite branch. Surface syntax already declares `self` explicitly, so the pass does not rewrite procedure bodies. uniqueIds on the cloned procedure are cleared so the pipeline's post-pass `resolve` can mint fresh ids.
Adds method-call syntax that parses as an `InstanceCall` AST node, then flows through resolution and the existing `LiftInstanceProcedures` pass to a real top-level static call. Pipeline changes: - Parser: `q\`Laurel.call\`` recognizes a `fieldAccess` callee and emits `InstanceCall target method args` instead of dropping the receiver. - Grammar: `call` callee position is parsed at prec 89 so `c#m(args)` parses as `call(fieldAccess(c, m), args)` without extra parens. - Resolution: instance procedures are pre-registered in the global scope under their lifted key `<CompositeName>$<methodName>`; two composites can now share a method name. `InstanceCall` resolution looks up the receiver's type and stamps the resolved uniqueId on the original callee identifier, preserving the user-facing name in diagnostics. - `liftedProcName` helper moved to `Laurel.lean` so it's reachable from both `Resolution` and `LiftInstanceProcedures`. Tests: - Six in T7_InstanceProcedures cover basic calls, same-method names across composites, multi-arg methods, and parameterized calls. - DuplicateNameTests updated for the new lifted-name format.
keyboardDrummer
left a comment
keyboardDrummer
left a comment
Contributor
There was a problem hiding this comment.
Really nice, thanks! Just A FYI: what should be done still, in another PR, by whomever is up to it, is add support for dynamic dispatch when calling abstract instance procedures. That feature is the main reason Laurel has instance procedures, since otherwise you could easily use static procedures instead of instance ones.
Author
|
Thanks for your feedback Remi! For your second point, I definitely agree that the rewrite passes need refactor. Maybe we can factor this out to another PR? What do you think. |
keyboardDrummer
left a comment
keyboardDrummer
left a comment
Contributor
There was a problem hiding this comment.
Really nice! Left one more comment.
Contributor
|
For the build feature, I think I have a fix here: #1313 |
Contributor
|
For the build issue. I don't think it's caused by this PR. I hope #1313 will fix that. |
Author
|
Thanks! I found one more issue (calls on nested objects) when using this PR'a feature. Trying to fix it. |
…roc-lowering # Conflicts: # Strata/Languages/Laurel/LaurelCompilationPipeline.lean # Strata/Languages/Laurel/LaurelToCoreTranslator.lean # StrataTest/Languages/Laurel/DuplicateNameTests.lean
keyboardDrummer
previously approved these changes
Jun 12, 2026
…roc-lowering # Conflicts: # StrataTest/Languages/Laurel/DuplicateNameTests.lean # StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean
Author
|
FIxed the conflicts and redirect the merge to the backlog branch. |
keyboardDrummer
previously approved these changes
Jun 16, 2026
ssomayyajula
approved these changes
Jun 16, 2026
keyboardDrummer
approved these changes
Jun 16, 2026
github-merge-queue
Bot
removed this pull request from the merge queue due to failed status checks
Merged
via the queue into
strata-org:reviewed-kbd-will-merge-to-main
with commit Jun 16, 2026
4d3cbac
15 checks passed
This was referenced Jun 17, 2026
fabiomadge
added a commit
that referenced
this pull request
Jun 20, 2026
…iagnostics Adds Seq<T> and Array<T> types with subscript read/write, a SubscriptElim lowering pass, and a ValidateSubscriptUsage diagnostics pass. Rebased onto reviewed-kbd-will-merge-to-main, which had advanced past the branch point with the bidirectional type checker (#1121), Java-style ++/-- (#1320), instance-procedure lowering (#1328/#1381), old()/heap rework (#1203/#1349), and diagnostics plumbing. Squashed into one commit. The feature was originally written against the pre-#1121 single-pass resolver, so bringing it up to date was more than a textual merge: - Resolution: the old single-pass `resolveStmtExpr` no longer exists. Subscript typing is re-expressed in the Synth/Check architecture as `Synth.subscript` (a value: read synthesizes the element type, functional update synthesizes the sequence type) and `Check.subscriptWrite` (a statement: TVoid), each with the lexicographic `(exprMd, n)` termination metric. Seq/Array misuse and bounds checks stay in ValidateSubscriptUsage; resolution emits no new diagnostics. - Synth.staticCall: extended the existing polymorphic-primitive escape hatch (select/update/const) to the Sequence.*/Array.* ops, which carry placeholder `int` signatures the strict checker would otherwise reject. Result types are inferred structurally (e.g. `Sequence.build(s, v) : Seq<typeof v>`, so `[1, 2, 3] : Seq<int>`; `Sequence.empty() : Unknown`). - LaurelAST: `Array<T>` is a surface type whose lowered forms differ — `$Array` after SubscriptElim, `Composite` after TypeHierarchy — while its declaration type is never rewritten. Added a narrow carve-out so the surface and lowered forms interoperate: `isConsistent` treats `Array<T>` as consistent with `$Array`/`Composite` (covers the `$obj != a` modifies-clause guard), and `isArrayInitCompatible` admits the element-checked `Seq<U> -> Array<T>` initialization (`var a: Array<int> := [1, 2, 3]`). - LaurelCompilationPipeline: ported the inline SubscriptElim pass to the named-`def` LaurelPass architecture (`subscriptElimPass`); added `validateSubscriptUsage` after the initial `resolve` (it imports Resolution, so it can't fold into `resolve` like the diamond validator). When a program already failed subscript validation, a post-pass re-resolution failure is expected fallout, not a compiler bug, so the StrataBug guard drops it instead of mislabeling it. - Exhaustiveness: the new Subscript/SubscriptWrite constructors and base's IncrDecr both needed arms in every wildcard-free StmtExpr walker (`StmtExpr.constrName`, `mapStmtExprPrePostM`, `SubscriptElim.elimExpr`, `ValidateSubscriptUsage.validateStmtExpr`). Dropped the stale `.THeap`/ `.TTypedField` arms the new HighType no longer has. - Docs: added a Subscript section and Seq/Array typing rules to LaurelDoc.
fabiomadge
added a commit
that referenced
this pull request
Jun 20, 2026
…iagnostics Adds Seq<T> and Array<T> types with subscript read/write, a SubscriptElim lowering pass, and a ValidateSubscriptUsage diagnostics pass. Rebased onto reviewed-kbd-will-merge-to-main, which had advanced past the branch point with the bidirectional type checker (#1121), Java-style ++/-- (#1320), instance-procedure lowering (#1328/#1381), old()/heap rework (#1203/#1349), and diagnostics plumbing. Squashed into one commit. The feature was originally written against the pre-#1121 single-pass resolver, so bringing it up to date was more than a textual merge: - Resolution: the old single-pass `resolveStmtExpr` no longer exists. Subscript typing is re-expressed in the Synth/Check architecture as `Synth.subscript` (a value: read synthesizes the element type, functional update synthesizes the sequence type) and `Check.subscriptWrite` (a statement: TVoid), each with the lexicographic `(exprMd, n)` termination metric. Seq/Array misuse and bounds checks stay in ValidateSubscriptUsage; resolution emits no new diagnostics. - Synth.staticCall: extended the existing polymorphic-primitive escape hatch (select/update/const) to the Sequence.*/Array.* ops, which carry placeholder `int` signatures the strict checker would otherwise reject. Result types are inferred structurally (e.g. `Sequence.build(s, v) : Seq<typeof v>`, so `[1, 2, 3] : Seq<int>`; `Sequence.empty() : Unknown`). - LaurelAST: `Array<T>` is a surface type whose lowered forms differ — `$Array` after SubscriptElim, `Composite` after TypeHierarchy — while its declaration type is never rewritten. Added a narrow carve-out so the surface and lowered forms interoperate: `isConsistent` treats `Array<T>` as consistent with `$Array`/`Composite` (covers the `$obj != a` modifies-clause guard), and `isArrayInitCompatible` admits the element-checked `Seq<U> -> Array<T>` initialization (`var a: Array<int> := [1, 2, 3]`). - LaurelCompilationPipeline: ported the inline SubscriptElim pass to the named-`def` LaurelPass architecture (`subscriptElimPass`); added `validateSubscriptUsage` after the initial `resolve` (it imports Resolution, so it can't fold into `resolve` like the diamond validator). When a program already failed subscript validation, a post-pass re-resolution failure is expected fallout, not a compiler bug, so the StrataBug guard drops it instead of mislabeling it. - Exhaustiveness: the new Subscript/SubscriptWrite constructors and base's IncrDecr both needed arms in every wildcard-free StmtExpr walker (`StmtExpr.constrName`, `mapStmtExprPrePostM`, `SubscriptElim.elimExpr`, `ValidateSubscriptUsage.validateStmtExpr`). Dropped the stale `.THeap`/ `.TTypedField` arms the new HighType no longer has. - Docs: added a Subscript section and Seq/Array typing rules to LaurelDoc.
fabiomadge
added a commit
that referenced
this pull request
Jun 20, 2026
…iagnostics Adds Seq<T> and Array<T> types with subscript read/write, a SubscriptElim lowering pass, and a ValidateSubscriptUsage diagnostics pass. Rebased onto reviewed-kbd-will-merge-to-main, which had advanced past the branch point with the bidirectional type checker (#1121), Java-style ++/-- (#1320), instance-procedure lowering (#1328/#1381), old()/heap rework (#1203/#1349), and diagnostics plumbing. Squashed into one commit. The feature was originally written against the pre-#1121 single-pass resolver, so bringing it up to date was more than a textual merge: - Resolution: the old single-pass `resolveStmtExpr` no longer exists. Subscript typing is re-expressed in the Synth/Check architecture as `Synth.subscript` (a value: read synthesizes the element type, functional update synthesizes the sequence type) and `Check.subscriptWrite` (a statement: TVoid), each with the lexicographic `(exprMd, n)` termination metric. Both check the index against `TInt` and the written/update value against the collection's element type (e.g. `a[0] := true` on an `Array<int>` is rejected). The Seq-vs-Array mutability rules and bounds checks stay in ValidateSubscriptUsage. - Synth.staticCall: extended the existing polymorphic-primitive escape hatch (select/update/const) to the Sequence.*/Array.* ops, which carry placeholder `int` signatures the strict checker would otherwise reject. Result types are inferred structurally (e.g. `Sequence.build(s, v) : Seq<typeof v>`, so `[1, 2, 3] : Seq<int>`; `Sequence.empty() : Unknown`). - LaurelAST: `Array<T>` is a surface type whose lowered forms differ — `$Array` after SubscriptElim, `Composite` after TypeHierarchy — while its declaration type is never rewritten. Added a narrow carve-out so the surface and lowered forms interoperate: `isConsistent` treats `Array<T>` as consistent with `$Array`/`Composite` (covers the `$obj != a` modifies-clause guard), and `isArrayInitCompatible` admits the element-checked `Seq<U> -> Array<T>` initialization (`var a: Array<int> := [1, 2, 3]`). - LaurelCompilationPipeline: ported the inline SubscriptElim pass to the named-`def` LaurelPass architecture (`subscriptElimPass`); added `validateSubscriptUsage` after the initial `resolve` (it imports Resolution, so it can't fold into `resolve` like the diamond validator). When a program already failed subscript validation, a post-pass re-resolution failure is expected fallout, not a compiler bug, so the StrataBug guard drops it instead of mislabeling it. - Exhaustiveness: the new Subscript/SubscriptWrite constructors and base's IncrDecr both needed arms in every wildcard-free StmtExpr walker (`StmtExpr.constrName`, `mapStmtExprPrePostM`, `SubscriptElim.elimExpr`, `ValidateSubscriptUsage.validateStmtExpr`). Dropped the stale `.THeap`/ `.TTypedField` arms the new HighType no longer has. - Docs: added a Subscript section and Seq/Array typing rules to LaurelDoc.
fabiomadge
added a commit
that referenced
this pull request
Jun 21, 2026
…iagnostics Adds Seq<T> and Array<T> types with subscript read/write, a SubscriptElim lowering pass, and a ValidateSubscriptUsage diagnostics pass. Rebased onto reviewed-kbd-will-merge-to-main, which had advanced past the branch point with the bidirectional type checker (#1121), Java-style ++/-- (#1320), instance-procedure lowering (#1328/#1381), old()/heap rework (#1203/#1349), and diagnostics plumbing. Squashed into one commit. The feature was originally written against the pre-#1121 single-pass resolver, so bringing it up to date was more than a textual merge: - Resolution: the old single-pass `resolveStmtExpr` no longer exists. Subscript typing is re-expressed in the Synth/Check architecture as `Synth.subscript` (a value: read synthesizes the element type, functional update synthesizes the sequence type) and `Check.subscriptWrite` (a statement: TVoid), each with the lexicographic `(exprMd, n)` termination metric. Both check the index against `TInt` and the written/update value against the collection's element type (e.g. `a[0] := true` on an `Array<int>` is rejected). The Seq-vs-Array mutability rules and bounds checks stay in ValidateSubscriptUsage. - Synth.staticCall: extended the existing polymorphic-primitive escape hatch (select/update/const) to the Sequence.*/Array.* ops, which carry placeholder `int` signatures the strict checker would otherwise reject. Result types are inferred structurally (e.g. `Sequence.build(s, v) : Seq<typeof v>`, so `[1, 2, 3] : Seq<int>`; `Sequence.empty() : Unknown`). - LaurelAST: `Array<T>` is a surface type whose lowered forms differ — `$Array` after SubscriptElim, `Composite` after TypeHierarchy — while its declaration type is never rewritten. Added a narrow carve-out so the surface and lowered forms interoperate: `isConsistent` treats `Array<T>` as consistent with `$Array`/`Composite` (covers the `$obj != a` modifies-clause guard), and `isArrayInitCompatible` admits the element-checked `Seq<U> -> Array<T>` initialization (`var a: Array<int> := [1, 2, 3]`). - LaurelCompilationPipeline: ported the inline SubscriptElim pass to the named-`def` LaurelPass architecture (`subscriptElimPass`); added `validateSubscriptUsage` after the initial `resolve` (it imports Resolution, so it can't fold into `resolve` like the diamond validator). When a program already failed subscript validation, a post-pass re-resolution failure is expected fallout, not a compiler bug, so the StrataBug guard drops it instead of mislabeling it. - Exhaustiveness: the new Subscript/SubscriptWrite constructors and base's IncrDecr both needed arms in every wildcard-free StmtExpr walker (`StmtExpr.constrName`, `mapStmtExprPrePostM`, `SubscriptElim.elimExpr`, `ValidateSubscriptUsage.validateStmtExpr`). Dropped the stale `.THeap`/ `.TTypedField` arms the new HighType no longer has. - Docs: added a Subscript section and Seq/Array typing rules to LaurelDoc.
fabiomadge
added a commit
that referenced
this pull request
Jun 21, 2026
…iagnostics Adds Seq<T> and Array<T> types with subscript read/write, a SubscriptElim lowering pass, and a ValidateSubscriptUsage diagnostics pass. Rebased onto reviewed-kbd-will-merge-to-main, which had advanced past the branch point with the bidirectional type checker (#1121), Java-style ++/-- (#1320), instance-procedure lowering (#1328/#1381), old()/heap rework (#1203/#1349), and diagnostics plumbing. Squashed into one commit. The feature was originally written against the pre-#1121 single-pass resolver, so bringing it up to date was more than a textual merge: - Resolution: the old single-pass `resolveStmtExpr` no longer exists. Subscript typing is re-expressed in the Synth/Check architecture as `Synth.subscript` (a value: read synthesizes the element type, functional update synthesizes the sequence type) and `Check.subscriptWrite` (a statement: TVoid), each with the lexicographic `(exprMd, n)` termination metric. Both check the index against `TInt` and the written/update value against the collection's element type (e.g. `a[0] := true` on an `Array<int>` is rejected), and reject a concrete non-collection target (`5[0]` -> "expected a sequence or array") while letting gradual `Unknown`/unresolved targets flow, mirroring `Fresh`/`ReferenceEquals`. The Seq-vs-Array mutability rules and bounds checks stay in ValidateSubscriptUsage. - Synth.staticCall: extended the existing polymorphic-primitive escape hatch (select/update/const) to the Sequence.*/Array.* ops, which carry placeholder `int` signatures the strict checker would otherwise reject. Result types are inferred structurally (e.g. `Sequence.build(s, v) : Seq<typeof v>`, so `[1, 2, 3] : Seq<int>`; `Sequence.empty() : Unknown`). - LaurelAST: `Array<T>` is a surface type whose lowered forms differ — `$Array` after SubscriptElim, `Composite` after TypeHierarchy — while its declaration type is never rewritten. Added a narrow carve-out so the surface and lowered forms interoperate: `isConsistent` treats `Array<T>` as consistent with `$Array`/`Composite` (covers the `$obj != a` modifies-clause guard), and `isArrayInitCompatible` admits the element-checked `Seq<U> -> Array<T>` initialization (`var a: Array<int> := [1, 2, 3]`). - LaurelCompilationPipeline: ported the inline SubscriptElim pass to the named-`def` LaurelPass architecture (`subscriptElimPass`); added `validateSubscriptUsage` after the initial `resolve` (it imports Resolution, so it can't fold into `resolve` like the diamond validator). When a program already failed subscript validation, a post-pass re-resolution failure is expected fallout, not a compiler bug, so the StrataBug guard drops it instead of mislabeling it. - Exhaustiveness: the new Subscript/SubscriptWrite constructors and base's IncrDecr both needed arms in every wildcard-free StmtExpr walker (`StmtExpr.constrName`, `mapStmtExprPrePostM`, `SubscriptElim.elimExpr`, `ValidateSubscriptUsage.validateStmtExpr`). Dropped the stale `.THeap`/ `.TTypedField` arms the new HighType no longer has. - Docs: added a Subscript section and Seq/Array typing rules to LaurelDoc.
fabiomadge
added a commit
that referenced
this pull request
Jun 21, 2026
…iagnostics Adds Seq<T> and Array<T> types with subscript read/write, a SubscriptElim lowering pass, and a ValidateSubscriptUsage diagnostics pass. Rebased onto reviewed-kbd-will-merge-to-main, which had advanced past the branch point with the bidirectional type checker (#1121), Java-style ++/-- (#1320), instance-procedure lowering (#1328/#1381), old()/heap rework (#1203/#1349), and diagnostics plumbing. Squashed into one commit. The feature was originally written against the pre-#1121 single-pass resolver, so bringing it up to date was more than a textual merge: - Resolution: the old single-pass `resolveStmtExpr` no longer exists. Subscript typing is re-expressed in the Synth/Check architecture as `Synth.subscript` (a value: read synthesizes the element type, functional update synthesizes the sequence type) and `Check.subscriptWrite` (a statement: TVoid), each with the lexicographic `(exprMd, n)` termination metric. Both check the index against `TInt` and the written/update value against the collection's element type (e.g. `a[0] := true` on an `Array<int>` is rejected), and reject a concrete non-collection target (`5[0]` -> "expected a sequence or array") while letting gradual `Unknown`/unresolved targets flow, mirroring `Fresh`/`ReferenceEquals`. The Seq-vs-Array mutability rules and bounds checks stay in ValidateSubscriptUsage. - Synth.staticCall: extended the existing polymorphic-primitive escape hatch (select/update/const) to the Sequence.*/Array.* ops, which carry placeholder `int` signatures the strict checker would otherwise reject. Result types are inferred structurally (e.g. `Sequence.build(s, v) : Seq<typeof v>`, so `[1, 2, 3] : Seq<int>`; `Sequence.empty() : Unknown`). - LaurelAST: `Array<T>` is a surface type whose lowered forms differ — `$Array` after SubscriptElim, `Composite` after TypeHierarchy — while its declaration type is never rewritten. Added a narrow carve-out so the surface and lowered forms interoperate: `isConsistent` treats `Array<T>` as consistent with `$Array`/`Composite` (covers the `$obj != a` modifies-clause guard), and `isArrayInitCompatible` admits the element-checked `Seq<U> -> Array<T>` initialization (`var a: Array<int> := [1, 2, 3]`). - LaurelCompilationPipeline: ported the inline SubscriptElim pass to the named-`def` LaurelPass architecture (`subscriptElimPass`); added `validateSubscriptUsage` after the initial `resolve` (it imports Resolution, so it can't fold into `resolve` like the diamond validator). When a program already failed subscript validation, a post-pass re-resolution failure is expected fallout, not a compiler bug, so the StrataBug guard drops it instead of mislabeling it. - Exhaustiveness: the new Subscript/SubscriptWrite constructors and base's IncrDecr both needed arms in every wildcard-free StmtExpr walker (`StmtExpr.constrName`, `mapStmtExprPrePostM`, `SubscriptElim.elimExpr`, `ValidateSubscriptUsage.validateStmtExpr`). Dropped the stale `.THeap`/ `.TTypedField` arms the new HighType no longer has. - Docs: added a Subscript section and Seq/Array typing rules to LaurelDoc.
fabiomadge
added a commit
that referenced
this pull request
Jun 21, 2026
…iagnostics Adds Seq<T> and Array<T> types with subscript read/write, a SubscriptElim lowering pass, and a ValidateSubscriptUsage diagnostics pass. Rebased onto reviewed-kbd-will-merge-to-main, which had advanced past the branch point with the bidirectional type checker (#1121), Java-style ++/-- (#1320), instance-procedure lowering (#1328/#1381), old()/heap rework (#1203/#1349), and diagnostics plumbing. Squashed into one commit. The feature was originally written against the pre-#1121 single-pass resolver, so bringing it up to date was more than a textual merge: - Resolution: the old single-pass `resolveStmtExpr` no longer exists. Subscript typing is re-expressed in the Synth/Check architecture as `Synth.subscript` (a value: read synthesizes the element type, functional update synthesizes the sequence type) and `Check.subscriptWrite` (a statement: TVoid), each with the lexicographic `(exprMd, n)` termination metric. Both check the index against `TInt` and the written/update value against the collection's element type (e.g. `a[0] := true` on an `Array<int>` is rejected), and reject a concrete non-collection target (`5[0]` -> "expected a sequence or array") while letting gradual `Unknown`/unresolved targets flow, mirroring `Fresh`/`ReferenceEquals`. The Seq-vs-Array mutability rules and bounds checks stay in ValidateSubscriptUsage. - Synth.staticCall: extended the existing polymorphic-primitive escape hatch (select/update/const) to the Sequence.*/Array.* ops, which carry placeholder `int` signatures the strict checker would otherwise reject. Result types are inferred structurally (e.g. `Sequence.build(s, v) : Seq<typeof v>`, so `[1, 2, 3] : Seq<int>`; `Sequence.empty() : Unknown`). - LaurelAST: `Array<T>` is a surface type whose lowered forms differ — `$Array` after SubscriptElim, `Composite` after TypeHierarchy — while its declaration type is never rewritten. Added a narrow carve-out so the surface and lowered forms interoperate: `isConsistent` treats `Array<T>` as consistent with `$Array`/`Composite` (covers the `$obj != a` modifies-clause guard), and `isArrayInitCompatible` admits the element-checked `Seq<U> -> Array<T>` initialization (`var a: Array<int> := [1, 2, 3]`). - LaurelCompilationPipeline: ported the inline SubscriptElim pass to the named-`def` LaurelPass architecture (`subscriptElimPass`); added `validateSubscriptUsage` after the initial `resolve` (it imports Resolution, so it can't fold into `resolve` like the diamond validator). When a program already failed subscript validation, a post-pass re-resolution failure is expected fallout, not a compiler bug, so the StrataBug guard drops it instead of mislabeling it. - Exhaustiveness: the new Subscript/SubscriptWrite constructors and base's IncrDecr both needed arms in every wildcard-free StmtExpr walker (`StmtExpr.constrName`, `mapStmtExprPrePostM`, `SubscriptElim.elimExpr`, `ValidateSubscriptUsage.validateStmtExpr`). Dropped the stale `.THeap`/ `.TTypedField` arms the new HighType no longer has. - Docs: added a Subscript section and Seq/Array typing rules to LaurelDoc.
fabiomadge
added a commit
that referenced
this pull request
Jun 21, 2026
…iagnostics Adds Seq<T> and Array<T> types with subscript read/write, a SubscriptElim lowering pass, and a ValidateSubscriptUsage diagnostics pass. Rebased onto reviewed-kbd-will-merge-to-main, which had advanced past the branch point with the bidirectional type checker (#1121), Java-style ++/-- (#1320), instance-procedure lowering (#1328/#1381), old()/heap rework (#1203/#1349), and diagnostics plumbing. Squashed into one commit. The feature was originally written against the pre-#1121 single-pass resolver, so bringing it up to date was more than a textual merge: - Resolution: the old single-pass `resolveStmtExpr` no longer exists. Subscript typing is re-expressed in the Synth/Check architecture as `Synth.subscript` (a value: read synthesizes the element type, functional update synthesizes the sequence type) and `Check.subscriptWrite` (a statement: TVoid), each with the lexicographic `(exprMd, n)` termination metric. Both check the index against `TInt` and the written/update value against the collection's element type (e.g. `a[0] := true` on an `Array<int>` is rejected), and reject a concrete non-collection target (`5[0]` -> "expected a sequence or array") while letting gradual `Unknown`/unresolved targets flow, mirroring `Fresh`/`ReferenceEquals`. The Seq-vs-Array mutability rules and bounds checks stay in ValidateSubscriptUsage. - Synth.staticCall: extended the existing polymorphic-primitive escape hatch (select/update/const) to the Sequence.*/Array.* ops, which carry placeholder `int` signatures the strict checker would otherwise reject. Result types are inferred structurally (e.g. `Sequence.build(s, v) : Seq<typeof v>`, so `[1, 2, 3] : Seq<int>`; `Sequence.empty() : Unknown`). - LaurelAST: `Array<T>` is a surface type whose lowered forms differ — `$Array` after SubscriptElim, `Composite` after TypeHierarchy — while its declaration type is never rewritten. Added a narrow carve-out so the surface and lowered forms interoperate: `isConsistent` treats `Array<T>` as consistent with `$Array`/`Composite` (covers the `$obj != a` modifies-clause guard), and `isArrayInitCompatible` admits the element-checked `Seq<U> -> Array<T>` initialization (`var a: Array<int> := [1, 2, 3]`). - LaurelCompilationPipeline: ported the inline SubscriptElim pass to the named-`def` LaurelPass architecture (`subscriptElimPass`); added `validateSubscriptUsage` after the initial `resolve` (it imports Resolution, so it can't fold into `resolve` like the diamond validator). When a program already failed subscript validation, a post-pass re-resolution failure is expected fallout, not a compiler bug, so the StrataBug guard drops it instead of mislabeling it. - Exhaustiveness: the new Subscript/SubscriptWrite constructors and base's IncrDecr both needed arms in every wildcard-free StmtExpr walker (`StmtExpr.constrName`, `mapStmtExprPrePostM`, `SubscriptElim.elimExpr`, `ValidateSubscriptUsage.validateStmtExpr`). Dropped the stale `.THeap`/ `.TTypedField` arms the new HighType no longer has. - Docs: added a Subscript section and Seq/Array typing rules to LaurelDoc.
fabiomadge
added a commit
that referenced
this pull request
Jun 21, 2026
…iagnostics Adds Seq<T> and Array<T> types with subscript read/write, a SubscriptElim lowering pass, and a ValidateSubscriptUsage diagnostics pass. Rebased onto reviewed-kbd-will-merge-to-main, which had advanced past the branch point with the bidirectional type checker (#1121), Java-style ++/-- (#1320), instance-procedure lowering (#1328/#1381), old()/heap rework (#1203/#1349), and diagnostics plumbing. Squashed into one commit. The feature was originally written against the pre-#1121 single-pass resolver, so bringing it up to date was more than a textual merge: - Resolution: the old single-pass `resolveStmtExpr` no longer exists. Subscript typing is re-expressed in the Synth/Check architecture as `Synth.subscript` (a value: read synthesizes the element type, functional update synthesizes the sequence type) and `Check.subscriptWrite` (a statement: TVoid), each with the lexicographic `(exprMd, n)` termination metric. Both check the index against `TInt` and the written/update value against the collection's element type (e.g. `a[0] := true` on an `Array<int>` is rejected), and reject a concrete non-collection target (`5[0]` -> "expected a sequence or array") while letting gradual `Unknown`/unresolved targets flow, mirroring `Fresh`/`ReferenceEquals`. The Seq-vs-Array mutability rules and bounds checks stay in ValidateSubscriptUsage. - Synth.staticCall: extended the existing polymorphic-primitive escape hatch (select/update/const) to the Sequence.*/Array.* ops, which carry placeholder `int` signatures the strict checker would otherwise reject. Result types are inferred structurally (e.g. `Sequence.build(s, v) : Seq<typeof v>`, so `[1, 2, 3] : Seq<int>`; `Sequence.empty() : Unknown`). - LaurelAST: `Array<T>` is a surface type whose lowered forms differ — `$Array` after SubscriptElim, `Composite` after TypeHierarchy — while its declaration type is never rewritten. Added a narrow carve-out so the surface and lowered forms interoperate: `isConsistent` treats `Array<T>` as consistent with `$Array`/`Composite` (covers the `$obj != a` modifies-clause guard), and `isArrayInitCompatible` admits the element-checked `Seq<U> -> Array<T>` initialization (`var a: Array<int> := [1, 2, 3]`). - LaurelCompilationPipeline: ported the inline SubscriptElim pass to the named-`def` LaurelPass architecture (`subscriptElimPass`); added `validateSubscriptUsage` after the initial `resolve` (it imports Resolution, so it can't fold into `resolve` like the diamond validator). When a program already failed subscript validation, a post-pass re-resolution failure is expected fallout, not a compiler bug, so the StrataBug guard drops it instead of mislabeling it. - Exhaustiveness: the new Subscript/SubscriptWrite constructors and base's IncrDecr both needed arms in every wildcard-free StmtExpr walker (`StmtExpr.constrName`, `mapStmtExprPrePostM`, `SubscriptElim.elimExpr`, `ValidateSubscriptUsage.validateStmtExpr`). Dropped the stale `.THeap`/ `.TTypedField` arms the new HighType no longer has. - Docs: added a Subscript section and Seq/Array typing rules to LaurelDoc.
fabiomadge
added a commit
that referenced
this pull request
Jun 21, 2026
…iagnostics Adds Seq<T> and Array<T> types with subscript read/write, a SubscriptElim lowering pass, and a ValidateSubscriptUsage diagnostics pass. Rebased onto reviewed-kbd-will-merge-to-main, which had advanced past the branch point with the bidirectional type checker (#1121), Java-style ++/-- (#1320), instance-procedure lowering (#1328/#1381), old()/heap rework (#1203/#1349), and diagnostics plumbing. Squashed into one commit. The feature was originally written against the pre-#1121 single-pass resolver, so bringing it up to date was more than a textual merge: - Resolution: the old single-pass `resolveStmtExpr` no longer exists. Subscript typing is re-expressed in the Synth/Check architecture as `Synth.subscript` (a value: read synthesizes the element type, functional update synthesizes the sequence type) and `Check.subscriptWrite` (a statement: TVoid), each with the lexicographic `(exprMd, n)` termination metric. Both check the index against `TInt` and the written/update value against the collection's element type (e.g. `a[0] := true` on an `Array<int>` is rejected), and reject a concrete non-collection target (`5[0]` -> "expected a sequence or array") while letting gradual `Unknown`/unresolved targets flow, mirroring `Fresh`/`ReferenceEquals`. The Seq-vs-Array mutability rules and bounds checks stay in ValidateSubscriptUsage. - Synth.staticCall: extended the existing polymorphic-primitive escape hatch (select/update/const) to the Sequence.*/Array.* ops, which carry placeholder `int` signatures the strict checker would otherwise reject. Result types are inferred structurally (e.g. `Sequence.build(s, v) : Seq<typeof v>`, so `[1, 2, 3] : Seq<int>`; `Sequence.empty() : Unknown`). - LaurelAST: `Array<T>` is a surface type whose lowered forms differ — `$Array` after SubscriptElim, `Composite` after TypeHierarchy — while its declaration type is never rewritten. Added a narrow carve-out so the surface and lowered forms interoperate: `isConsistent` treats `Array<T>` as consistent with `$Array`/`Composite` (covers the `$obj != a` modifies-clause guard), and `isArrayInitCompatible` admits the element-checked `Seq<U> -> Array<T>` initialization (`var a: Array<int> := [1, 2, 3]`). - LaurelCompilationPipeline: ported the inline SubscriptElim pass to the named-`def` LaurelPass architecture (`subscriptElimPass`); added `validateSubscriptUsage` after the initial `resolve` (it imports Resolution, so it can't fold into `resolve` like the diamond validator). When a program already failed subscript validation, a post-pass re-resolution failure is expected fallout, not a compiler bug, so the StrataBug guard drops it instead of mislabeling it. - Exhaustiveness: the new Subscript/SubscriptWrite constructors and base's IncrDecr both needed arms in every wildcard-free StmtExpr walker (`StmtExpr.constrName`, `mapStmtExprPrePostM`, `SubscriptElim.elimExpr`, `ValidateSubscriptUsage.validateStmtExpr`). Dropped the stale `.THeap`/ `.TTypedField` arms the new HighType no longer has. - Docs: added a Subscript section and Seq/Array typing rules to LaurelDoc.
fabiomadge
added a commit
that referenced
this pull request
Jun 21, 2026
…iagnostics Adds Seq<T> and Array<T> types with subscript read/write, a SubscriptElim lowering pass, and a ValidateSubscriptUsage diagnostics pass. Rebased onto reviewed-kbd-will-merge-to-main, which had advanced past the branch point with the bidirectional type checker (#1121), Java-style ++/-- (#1320), instance-procedure lowering (#1328/#1381), old()/heap rework (#1203/#1349), and diagnostics plumbing. Squashed into one commit. The feature was originally written against the pre-#1121 single-pass resolver, so bringing it up to date was more than a textual merge: - Resolution: the old single-pass `resolveStmtExpr` no longer exists. Subscript typing is re-expressed in the Synth/Check architecture as `Synth.subscript` (a value: read synthesizes the element type, functional update synthesizes the sequence type) and `Check.subscriptWrite` (a statement: TVoid), each with the lexicographic `(exprMd, n)` termination metric. Both check the index against `TInt` and the written/update value against the collection's element type (e.g. `a[0] := true` on an `Array<int>` is rejected), and reject a concrete non-collection target (`5[0]` -> "expected a sequence or array") while letting gradual `Unknown`/unresolved targets flow, mirroring `Fresh`/`ReferenceEquals`. The Seq-vs-Array mutability rules and bounds checks stay in ValidateSubscriptUsage. - Synth.staticCall: extended the existing polymorphic-primitive escape hatch (select/update/const) to the Sequence.*/Array.* ops, which carry placeholder `int` signatures the strict checker would otherwise reject. Result types are inferred structurally (e.g. `Sequence.build(s, v) : Seq<typeof v>`, so `[1, 2, 3] : Seq<int>`; `Sequence.empty() : Unknown`). - LaurelAST: `Array<T>` is a surface type whose lowered forms differ — `$Array` after SubscriptElim, `Composite` after TypeHierarchy — while its declaration type is never rewritten. Added a narrow carve-out so the surface and lowered forms interoperate: `isConsistent` treats `Array<T>` as consistent with `$Array`/`Composite` (covers the `$obj != a` modifies-clause guard), and `isArrayInitCompatible` admits the element-checked `Seq<U> -> Array<T>` initialization (`var a: Array<int> := [1, 2, 3]`). - LaurelCompilationPipeline: ported the inline SubscriptElim pass to the named-`def` LaurelPass architecture (`subscriptElimPass`); added `validateSubscriptUsage` after the initial `resolve` (it imports Resolution, so it can't fold into `resolve` like the diamond validator). When a program already failed subscript validation, a post-pass re-resolution failure is expected fallout, not a compiler bug, so the StrataBug guard drops it instead of mislabeling it. - Exhaustiveness: the new Subscript/SubscriptWrite constructors and base's IncrDecr both needed arms in every wildcard-free StmtExpr walker (`StmtExpr.constrName`, `mapStmtExprPrePostM`, `SubscriptElim.elimExpr`, `ValidateSubscriptUsage.validateStmtExpr`). Dropped the stale `.THeap`/ `.TTypedField` arms the new HighType no longer has. - Docs: added a Subscript section and Seq/Array typing rules to LaurelDoc.
fabiomadge
added a commit
that referenced
this pull request
Jun 21, 2026
…iagnostics Adds Seq<T> and Array<T> types with subscript read/write, a SubscriptElim lowering pass, and a ValidateSubscriptUsage diagnostics pass. Rebased onto reviewed-kbd-will-merge-to-main, which had advanced past the branch point with the bidirectional type checker (#1121), Java-style ++/-- (#1320), instance-procedure lowering (#1328/#1381), old()/heap rework (#1203/#1349), and diagnostics plumbing. Squashed into one commit. The feature was originally written against the pre-#1121 single-pass resolver, so bringing it up to date was more than a textual merge: - Resolution: the old single-pass `resolveStmtExpr` no longer exists. Subscript typing is re-expressed in the Synth/Check architecture as `Synth.subscript` (a value: read synthesizes the element type, functional update synthesizes the sequence type) and `Check.subscriptWrite` (a statement: TVoid), each with the lexicographic `(exprMd, n)` termination metric. Both check the index against `TInt` and the written/update value against the collection's element type (e.g. `a[0] := true` on an `Array<int>` is rejected), and reject a concrete non-collection target (`5[0]` -> "expected a sequence or array") while letting gradual `Unknown`/unresolved targets flow, mirroring `Fresh`/`ReferenceEquals`. The Seq-vs-Array mutability rules and bounds checks stay in ValidateSubscriptUsage. - Synth.staticCall: extended the existing polymorphic-primitive escape hatch (select/update/const) to the Sequence.*/Array.* ops, which carry placeholder `int` signatures the strict checker would otherwise reject. Result types are inferred structurally (e.g. `Sequence.build(s, v) : Seq<typeof v>`, so `[1, 2, 3] : Seq<int>`; `Sequence.empty() : Unknown`). - LaurelAST: `Array<T>` is a surface type whose lowered forms differ — `$Array` after SubscriptElim, `Composite` after TypeHierarchy — while its declaration type is never rewritten. Added a narrow carve-out so the surface and lowered forms interoperate: `isConsistent` treats `Array<T>` as consistent with `$Array`/`Composite` (covers the `$obj != a` modifies-clause guard), and `isArrayInitCompatible` admits the element-checked `Seq<U> -> Array<T>` initialization (`var a: Array<int> := [1, 2, 3]`). - LaurelCompilationPipeline: ported the inline SubscriptElim pass to the named-`def` LaurelPass architecture (`subscriptElimPass`); added `validateSubscriptUsage` after the initial `resolve` (it imports Resolution, so it can't fold into `resolve` like the diamond validator). When a program already failed subscript validation, a post-pass re-resolution failure is expected fallout, not a compiler bug, so the StrataBug guard drops it instead of mislabeling it. - Exhaustiveness: the new Subscript/SubscriptWrite constructors and base's IncrDecr both needed arms in every wildcard-free StmtExpr walker (`StmtExpr.constrName`, `mapStmtExprPrePostM`, `SubscriptElim.elimExpr`, `ValidateSubscriptUsage.validateStmtExpr`). Dropped the stale `.THeap`/ `.TTypedField` arms the new HighType no longer has. - Docs: added a Subscript section and Seq/Array typing rules to LaurelDoc.
fabiomadge
added a commit
that referenced
this pull request
Jun 21, 2026
…iagnostics Adds Seq<T> and Array<T> types with subscript read/write, a SubscriptElim lowering pass, and a ValidateSubscriptUsage diagnostics pass. Rebased onto reviewed-kbd-will-merge-to-main, which had advanced past the branch point with the bidirectional type checker (#1121), Java-style ++/-- (#1320), instance-procedure lowering (#1328/#1381), old()/heap rework (#1203/#1349), and diagnostics plumbing. Squashed into one commit. The feature was originally written against the pre-#1121 single-pass resolver, so bringing it up to date was more than a textual merge: - Resolution: the old single-pass `resolveStmtExpr` no longer exists. Subscript typing is re-expressed in the Synth/Check architecture as `Synth.subscript` (a value: read synthesizes the element type, functional update synthesizes the sequence type) and `Check.subscriptWrite` (a statement: TVoid), each with the lexicographic `(exprMd, n)` termination metric. Both check the index against `TInt` and the written/update value against the collection's element type (e.g. `a[0] := true` on an `Array<int>` is rejected), and reject a concrete non-collection target (`5[0]` -> "expected a sequence or array") while letting gradual `Unknown`/unresolved targets flow, mirroring `Fresh`/`ReferenceEquals`. The Seq-vs-Array mutability rules and bounds checks stay in ValidateSubscriptUsage. - Synth.staticCall: extended the existing polymorphic-primitive escape hatch (select/update/const) to the Sequence.*/Array.* ops, which carry placeholder `int` signatures the strict checker would otherwise reject. Result types are inferred structurally (e.g. `Sequence.build(s, v) : Seq<typeof v>`, so `[1, 2, 3] : Seq<int>`; `Sequence.empty() : Unknown`). - LaurelAST: `Array<T>` is a surface type whose lowered forms differ — `$Array` after SubscriptElim, `Composite` after TypeHierarchy — while its declaration type is never rewritten. Added a narrow carve-out so the surface and lowered forms interoperate: `isConsistent` treats `Array<T>` as consistent with `$Array`/`Composite` (covers the `$obj != a` modifies-clause guard), and `isArrayInitCompatible` admits the element-checked `Seq<U> -> Array<T>` initialization (`var a: Array<int> := [1, 2, 3]`). - LaurelCompilationPipeline: ported the inline SubscriptElim pass to the named-`def` LaurelPass architecture (`subscriptElimPass`); added `validateSubscriptUsage` after the initial `resolve` (it imports Resolution, so it can't fold into `resolve` like the diamond validator). When a program already failed subscript validation, a post-pass re-resolution failure is expected fallout, not a compiler bug, so the StrataBug guard drops it instead of mislabeling it. - Exhaustiveness: the new Subscript/SubscriptWrite constructors and base's IncrDecr both needed arms in every wildcard-free StmtExpr walker (`StmtExpr.constrName`, `mapStmtExprPrePostM`, `SubscriptElim.elimExpr`, `ValidateSubscriptUsage.validateStmtExpr`). Dropped the stale `.THeap`/ `.TTypedField` arms the new HighType no longer has. - Docs: added a Subscript section and Seq/Array typing rules to LaurelDoc.
fabiomadge
added a commit
that referenced
this pull request
Jun 21, 2026
…iagnostics Adds Seq<T> and Array<T> types with subscript read/write, a SubscriptElim lowering pass, and a ValidateSubscriptUsage diagnostics pass. Rebased onto reviewed-kbd-will-merge-to-main, which had advanced past the branch point with the bidirectional type checker (#1121), Java-style ++/-- (#1320), instance-procedure lowering (#1328/#1381), old()/heap rework (#1203/#1349), and diagnostics plumbing. Squashed into one commit. The feature was originally written against the pre-#1121 single-pass resolver, so bringing it up to date was more than a textual merge: - Resolution: the old single-pass `resolveStmtExpr` no longer exists. Subscript typing is re-expressed in the Synth/Check architecture as `Synth.subscript` (a value: read synthesizes the element type, functional update synthesizes the sequence type) and `Check.subscriptWrite` (a statement: TVoid), each with the lexicographic `(exprMd, n)` termination metric. Both check the index against `TInt` and the written/update value against the collection's element type (e.g. `a[0] := true` on an `Array<int>` is rejected), and reject a concrete non-collection target (`5[0]` -> "expected a sequence or array") while letting gradual `Unknown`/unresolved targets flow, mirroring `Fresh`/`ReferenceEquals`. The Seq-vs-Array mutability rules and bounds checks stay in ValidateSubscriptUsage. - Synth.staticCall: extended the existing polymorphic-primitive escape hatch (select/update/const) to the Sequence.*/Array.* ops, which carry placeholder `int` signatures the strict checker would otherwise reject. Result types are inferred structurally (e.g. `Sequence.build(s, v) : Seq<typeof v>`, so `[1, 2, 3] : Seq<int>`; `Sequence.empty() : Unknown`). - LaurelAST: `Array<T>` is a surface type whose lowered forms differ — `$Array` after SubscriptElim, `Composite` after TypeHierarchy — while its declaration type is never rewritten. Added a narrow carve-out so the surface and lowered forms interoperate: `isConsistent` treats `Array<T>` as consistent with `$Array`/`Composite` (covers the `$obj != a` modifies-clause guard), and `isArrayInitCompatible` admits the element-checked `Seq<U> -> Array<T>` initialization (`var a: Array<int> := [1, 2, 3]`). - LaurelCompilationPipeline: ported the inline SubscriptElim pass to the named-`def` LaurelPass architecture (`subscriptElimPass`); added `validateSubscriptUsage` after the initial `resolve` (it imports Resolution, so it can't fold into `resolve` like the diamond validator). When a program already failed subscript validation, a post-pass re-resolution failure is expected fallout, not a compiler bug, so the StrataBug guard drops it instead of mislabeling it. - Exhaustiveness: the new Subscript/SubscriptWrite constructors and base's IncrDecr both needed arms in every wildcard-free StmtExpr walker (`StmtExpr.constrName`, `mapStmtExprPrePostM`, `SubscriptElim.elimExpr`, `ValidateSubscriptUsage.validateStmtExpr`). Dropped the stale `.THeap`/ `.TTypedField` arms the new HighType no longer has. - Docs: added a Subscript section and Seq/Array typing rules to LaurelDoc.
keyboardDrummer
pushed a commit
to keyboardDrummer/Strata
that referenced
this pull request
Jun 23, 2026
…overage (strata-org#1382) Two field-access improvements on the single `fieldAccess` grammar op, plus test coverage that closes out strata-org#1371. Note: the chained-field-access *capability* (`a#b#c` parsing, resolution, and heap elimination) already landed via strata-org#1328. This PR adds the one missing ergonomic piece, hardens the chained-access machinery with the tests it was missing, and a small refactor. **Grammar — paren-free field `++`/`--`.** `fieldAccess` precedence is raised 90 → 95. At 90 it tied with the postfix `++`/`--` ops (also 90), forcing `(c#n)++`; at 95 it binds tighter, so `c#n++` parses paren-free as `(c#n)++`. (`leftassoc`, already present from strata-org#1328, is unchanged.) Note the new precedence is shared with `call` (also 95, via its `callee:89`) — the two must stay equal or `a#b(x)` parsing shifts; documented at the op. **Resolution — refactor only.** The duplicated type-scope field lookup in `targetTypeName` and `incrDecrTargetType` is factored into a shared `fieldTypeInScope` helper. No behavior change. (This helper is also a dependency of the stacked compound-assignment PR.) **Tests — fill the chained-access coverage gap.** strata-org#1328 shipped chained access with only a read-side smoke test (no assertions). This adds: - `T9_ChainedFieldAccess`: chained **write** (`o#inner#count := …`), read-after-inner-assign, must-alias, depth-3 (`a#mid#inner#count`), chained reads on both sides of `==`, and paren-free chained `o#inner#count++` (the one test that exercises this PR's grammar change), plus three **negative** tests (unconstrained read, two-object may-alias, write isolation) that pin the encoding as non-vacuous and frame-sound. - `T23b_IncrDecrField`: paren-free single-level field `++`/`--`. Full `lake build` and `lake test` pass.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This PR addresses the problem that Laurel composite types could declare instance procedures inside
composite { ... }blocks, but they couldn't be compiled or called. The Laurel→Core translator unconditionally rejected every instance procedure with aNotYetImplementeddiagnostic, and even without that block they would have been silently dropped: the SCC ordering inCoreGroupingAndOrdering.leanonly enumeratesprogram.staticProcedures, so anything onCompositeType.instanceProceduresnever reached Strata Core.1. Surface syntax of instance procedure calls:
obj#method(args)ConcreteToAbstractTreeTranslator.lean): when the callee ofcall(...)is afieldAccessnode, emitInstanceCall target method argsinstead of dropping the receiver into an empty-string static call.LaurelGrammar.st): adjustcall's precedence soc#m(args)parses ascall(fieldAccess(c, m), args).Resolution.lean): pre-register instance procedures in the global scope under their lifted key (<CompositeName>$<methodName>). Two composites can now share a method name without colliding (Note: this change seems to resolve Laurel resolution pass should allow instance procedures on different composite types with the same name #1321 but the the issue of the Resolver still exists - variable scope should be carefully refactored for the resolution pass).InstanceCallresolution looks up the receiver's composite type, builds the lifted key, and stamps the resolveduniqueIdon the original callee identifier.2. Laurel-to-Laurel pass:
LiftInstanceProceduresA new pass under
Strata/Languages/Laurel/LiftInstanceProcedures.lean, wired intoLaurelCompilationPipeline.leanwithneedsResolves := truebetweenEliminateValueReturnsandHeapParameterization. The pass:.Composite ctinprogram.typesand clones eachproc ∈ ct.instanceProceduresinto a fresh top-level static procedure named<CompositeName>$<methodName>. Body, parameters, contracts, andinvokeOnare copied verbatim.InstanceCallwhose callee so it points at the lifted name (with the receiver prepended as the first argument to match the lifted procedure'sself : <CompositeName>parameter).ct.instanceProcedures := []on every composite and appends the lifted procedures toprogram.staticProcedures.Downstream simplifications:
HeapParameterization.leandrops its secondary traversal ofinstanceProcedures(now always empty), and theNotYetImplementedblock inLaurelToCoreTranslator.leanis replaced by a defensiveStrataBugassertion that fires only on a pass-ordering regression (all instance procedures should already be lifted and rewritten at this point).