[codex] Implement PR11.11a method syntax#199
Merged
berkeleynerd merged 2 commits intoberkeleynerd:mainfrom Apr 4, 2026
Merged
Conversation
Contributor
There was a problem hiding this comment.
Pull request overview
Implements PR11.11a “method syntax” as source-level sugar by adding receiver-parameter declarations and rewriting selector calls (value.method(...)) into ordinary first-parameter calls, including support for imported public functions and existing list/map builtins.
Changes:
- Extend parsing + AST/schema to represent an optional receiver parameter on subprogram specifications.
- Add resolver support to desugar
receiver.method(args)intomethod(receiver, args)with ambiguity detection and builtin participation. - Add fixtures + harness updates (tests, proofs, docs/spec) covering method syntax, builtin method sugar, and imported/ambiguous cases.
Reviewed changes
Copilot reviewed 20 out of 20 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
| tests/positive/pr1111a_method_syntax.safe | Positive fixture for receiver declarations and method-call desugaring. |
| tests/negative/neg_pr1111a_remove_stmt_method.safe | Negative fixture ensuring remove (value-returning) isn’t admitted as a call statement via method sugar. |
| tests/negative/neg_pr1111a_mut_receiver_constant.safe | Negative fixture enforcing mut receiver requires writable target. |
| tests/negative/neg_pr1111a_append_expr.safe | Negative fixture enforcing append can’t be used as an expression via method sugar. |
| tests/interfaces/client_optional_method.safe | Interface fixture: imported public function callable via method sugar. |
| tests/interfaces/client_optional_method_ambiguous.safe | Interface reject fixture: ambiguity between local and imported method candidates. |
| tests/interfaces/client_list_method.safe | Interface fixture: builtin/stdlib-like method sugar on list operations. |
| tests/interfaces/client_imported_method_observe.safe | Interface fixture: imported methods with ownership/observe patterns. |
| tests/build/pr1111a_builtin_methods_build.safe | Build fixture exercising builtin container operations using method sugar. |
| spec/08-syntax-summary.md | Spec updates documenting receiver clause syntax and selector-call sugar for builtins. |
| scripts/run_tests.py | Registers new interface cases, reject case, AST contract, and build fixture expected output. |
| scripts/run_proofs.py | Adds PR11.11a checkpoint group execution and summary reporting. |
| scripts/_lib/proof_inventory.py | Adds PR11.11a checkpoint fixture manifest and includes it in coverage paths. |
| docs/tutorial.md | Tutorial section documenting receiver declarations and method-call sugar semantics. |
| docs/PR11.x-series-proposed.md | Roadmap notes updated to reflect completed milestones + expanded PR11.11a description. |
| compiler/ast_schema.json | Adds receiver field to procedure/function specifications in the AST schema. |
| compiler_impl/src/safe_frontend-check_parse.adb | Parses optional receiver parameter clause before subprogram name. |
| compiler_impl/src/safe_frontend-check_model.ads | Adds Has_Receiver + Receiver to Subprogram_Spec. |
| compiler_impl/src/safe_frontend-check_emit.adb | Emits receiver parameter into JSON AST for procedure/function specifications. |
| compiler_impl/src/safe_frontend-check_resolve.adb | Implements method-call rewrite/desugaring and integrates it into apply resolution. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
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
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
value.method(...)onto ordinary first-parameter calls, including imported public functions and existing list/map builtinsWhy
PR11.11a is the first composition milestone slice. This keeps the implementation as source sugar over the existing function model, without changing MIR, runtime behavior, or machine-facing artifact versions.
Validation
cd compiler_impl && alr buildpython3 scripts/run_tests.py->729 passed, 1 skipped, 0 failedpython3 scripts/run_samples.py->19 passed, 0 failedpython3 scripts/run_proofs.py->178 proved, 0 failedPR11.11a checkpoint: 2 proved, 0 failed