Repository navigation
feat(parser): unimplemented syntax is refused by name (E7 gate) - #434
Conversation
The parser refused syntax of the v2 design that it does not have with a
plain syntax error. The v2 plan asks for a named error.
- ephapax.pest has 25 rules `unimplemented_<production>`: one for each
form of the design that the parser does not have (traits, impl,
effect and handler declarations, comptime, contracts, where clauses,
effect rows, `import X from "f"`, capabilities, annotation arguments,
`++`, deref, tuple and borrow patterns, the handler forms). A rule
finds the syntax; it accepts nothing.
- The 2 parsers walk the parse tree before they build a module. The
first such rule gives `ParseError::Unimplemented { production }`.
- Each rule stands only where no valid program can have its first
token, so no program that parsed before changes. A new test has 9
valid programs that are near these rules.
- The grammar test now asserts the name: each `[UNIMPLEMENTED]` mark
says `refused: <fixture> as <production>`, and the 2 parsers must
refuse the fixture with that production. Each rule
`unimplemented_<production>` must have its production in part 2,
refused under its own name. This answers the review finding on #432
that one fixture stood for a group with no check of the reason.
- Part 1 of spec/ephapax-v2-grammar.ebnf is written again from the
grammar, and the 57 marks have the `as <production>` part.
Tests: 615 all-target.
Co-Authored-By: Claude Fable 5.2 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0136P7ZmKrYLDC4WHi2yt11u
Finishing Touches
Warning Some tools did not complete. Review the errors below.
|
3 defects of the interpreter (`run --interp`). Wasm ran each program. - A call of a function with no parameter stopped with "Not a function", and a call of a function with 2 or more parameters stopped with "Unbound variable". A reference to a function gave its body for no parameter, and a closure for the first parameter only. A function value is now a closure for its first parameter with a lambda for each next parameter, so `f(a, b)` gives each parameter its argument. A function with no parameter takes the unit argument of `f()`. - A parameter with the name of a top-level function was read as that function. A local name now shadows a function. - `&s` on a string consumed `s`, so a later use stopped with "Linear value used after consumption". A borrow of a variable now reads the value and leaves it in place. Tests: one new test with 7 programs on both engines. 2 tests that ran on wasm only because of these defects now run on both engines. 616 all-target. Co-Authored-By: Claude Fable 5.2 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmKrYLDC4WHi2yt11u
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
Codex Review Summary: ✅ CompletedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
`let (a, b, c) = (1, 2, 3)` was a type error. The parser made a chain of pair patterns for 3 or more names, and `(1, 2, 3)` is a tuple, not a chain of pairs. - The surface parser makes a tuple pattern for 3 or more names. 2 names are a pair, as before. - The desugarer lowers a tuple pattern of variables and wildcards to a one-arm core `match` on a tuple pattern, as it does for a pair pattern. The type checker, the wasm back end and the interpreter have tuple patterns already. No `.eph` file of the repository has a binder with 3 names. Tests: 6 programs on both engines (mixed types, a linear part), and the refusal of `_` over a linear part. 617 all-target. Co-Authored-By: Claude Fable 5.2 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmKrYLDC4WHi2yt11u
`M.Ctor(x)` works as an expression since #430. The same form in a match pattern did not parse: `| shapes.Rect(w, h) => ...`. - Grammar: `constructor_pattern` takes an optional `pattern_qualifier` and a `.` before the constructor name. - The surface parser keeps the qualifier in the name (`M.Ctor`). The desugarer checks that `M` is an import of the module, and finds `Ctor` in the scope of the module. So the visibility rule of #431 holds: a private type is "unknown constructor". - The core parser fallback has no list of imports: it does not check the module there. Part 1 of spec/ephapax-v2-grammar.ebnf is written again from the grammar. Tests: 2 programs on both engines (with and without a guard) and 2 refused programs. 618 all-target. Co-Authored-By: Claude Fable 5.2 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmKrYLDC4WHi2yt11u
|
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 3c049ae98b
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Each finding is checked against the code. - The 2 entry points for one expression (`parse`, `parse_surface_expr`) did not refuse unimplemented syntax. The core parser read `1 ++ 2` as `1`, because the code that builds an expression does not know the rule for `++`. Each entry point of the 2 parsers now runs `refuse_unimplemented` on the parse tree. - The interpreter gave a top-level function the local names of its caller. Since #434 a local name shadows a function, so in `let g = 0 in f(1)` the `g()` in the body of `f` found the `g` of the caller: "Not a function"; wasm gave the right result. A top-level function value now starts from an empty environment: its body sees its parameters and the top-level functions. - The rule for `capability_annotation` was on declaration annotations. The design has it at the FFI call: `__ffi@capabilities(io)("f")`. The rule is now in `ffi_expr`, and the fixture has the design form. `@capabilities(io)` on a declaration is `annotation_args`, as each annotation with arguments is. Part 1 of spec/ephapax-v2-grammar.ebnf is written again from the grammar. Tests: one new test for the expression entry points, one more program in the interpreter test. 620 all-target. Co-Authored-By: Claude Fable 5.2 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmKrYLDC4WHi2yt11u
… doc comments (#435) ## Summary 3 commits. 1. A match with no guard no longer takes a pattern inside a constructor pattern as a wildcard. 2. 3 review findings on #434, which merged before they arrived. 2 of them are regressions of #434. 3. Doc comments for the declarations that the Docstring Coverage check listed. No behaviour changes. ## 1. A pattern inside a constructor pattern is not a wildcard In a match with no guard, the desugarer took a literal or a constructor inside a constructor pattern as a wildcard, and it kept only the last arm of each constructor. Programs gave wrong results with no error. | Program | Before | Now | |---|---|---| | `Some(0) => 1 \| Some(n) => 2 \| None => 3` on `Some(0)` | 2 | 1 | | `Some(0) => 1 \| None => 3` on `Some(5)` | 1 | refused: the match does not cover `Some(5)` | | `W(Some(x)) => 1 \| W(None) => 0` on `W(Some(9))` | 0 | refused by name | A match where an arm has a literal or a constructor inside a constructor pattern now takes the ordered path of a match with a guard (#431): each arm of a constructor, in source order, in one core `match` on the payload. - A literal inside a constructor pattern is honoured. The type checker finds a match that does not cover the payload. - A constructor inside a constructor pattern (`W(Some(x))`) has no lowering yet. It is refused by name. The error is now `NestedConstructorPattern` (it was `GuardWithNestedConstructor`). - A match with no such pattern and no guard lowers as before. ## 2. Review findings on #434 - **Expression entry points.** `parse` and `parse_surface_expr` did not refuse unimplemented syntax, and the core parser read `1 ++ 2` as `1`. Each entry point of the 2 parsers now runs `refuse_unimplemented` on the parse tree. - **Interpreter scope (regression of #434).** A top-level function took the local names of its caller. With `let g = 0 in f(1)`, the `g()` in the body of `f` found the `g` of the caller: "Not a function". A top-level function value now starts from an empty environment. - **Capability annotation.** The rule was on declaration annotations. The design has it at the FFI call: `__ffi@capabilities(io)("f")`. The rule is now in `ffi_expr`, and the fixture has the design form. Part 1 of `spec/ephapax-v2-grammar.ebnf` is written again from the grammar. ## 3. Doc comments The CodeRabbit check Docstring Coverage listed declarations with no doc comment. Each one now has a doc comment of 1 or 2 lines: - library code of the CLI, driver, interpreter, LSP, REPL, syntax, typing and wasm crates; - the grammar conformance test; - the helpers of 4 test files (`driver_agreement.rs`, `generics.rs`, `run_wasm.rs`, `typed_codegen_matrix.rs`). The commit adds 61 lines of comment in 17 files and changes no code. ## Verification - `cargo test --workspace`: 623 passed, 0 failed. No program of the corpus changed. - `cargo fmt --all --check` and `cargo clippy --workspace --all-targets`: clean. - `scripts/status-gate.sh`: 620 all-target tests. - `scripts/probe-battery.sh`: 51 SAME, 7 SKIP (the SKIP rows need the wasmtime CLI). - New tests: `a_pattern_inside_a_constructor_pattern_is_not_a_wildcard`, `an_expression_with_unimplemented_syntax_is_refused_by_name`, and one more program in `the_interpreter_calls_and_borrows_as_wasm_does`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_0136P7ZmKrYLDC4WHi2yt11u --------- Co-authored-by: Claude <noreply@anthropic.com>



Summary
The last open item of the E7 gate in the v2 plan: "productions that are not implemented must fail with a named error". Before, the parser refused such syntax with a plain syntax error.
The change
ephapax.pesthas 25 rules with the nameunimplemented_<production>, one for each form of the design that the parser does not have: traits,impl, effect and handler declarations, comptime, contracts,whereclauses, effect rows,import X from "f", capabilities, annotation arguments,++, deref, tuple and borrow patterns, and the handler forms. A rule finds the syntax; it accepts nothing.ParseError::Unimplemented { production }.handle shallow(1) with ..., whereshallowis a function).The grammar test is stronger
This also answers the review finding on #432 that one fixture stood for a group of productions, with no check of the reason.
[UNIMPLEMENTED]mark in part 2 now saysrefused: <fixture> as <production>. The 2 parsers must refuse the fixture with an error that names that production.unimplemented_<production>must have its production in part 2, refused under its own name.comptime_ifinsidecomptime_decl) has the name of the outer production in its mark.Part 1 of
spec/ephapax-v2-grammar.ebnfis written again from the grammar, and the 57 marks have the newas <production>part.Verification
cargo test --workspace: 618 passed, 0 failed.cargo fmt --all --checkandcargo clippy --workspace --all-targets: clean.scripts/status-gate.sh: 615 all-target tests.scripts/probe-battery.sh: 51 SAME, 7 SKIP (the SKIP rows need the wasmtime CLI).tests/v2-grammar/unimplementedgives the named error onephapax check.Generated by Claude Code