gale: distill the review response

Claim (a) has one exception. `g4::parse` accepts a grammar whose action
body the translator cannot render; that failure is at codegen, so the
carve-out named a second exception the parser does not have, and pointed
at a file that documented neither. `README.md` and `AGENTS.md` follow.

The channel remap says what makes it correct rather than what its fallback
branch does: a `channels { }` block is the grammar's own numbering, so
inside its range an id and the name declared at that index are one channel.

`arms_are_one_level` replaces three copies of the same fold.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Q2Kw2ucQ6fpgwK1KH8CzLC

Author: claude

package-gale/AGENTS.md

@@ -23,7 +23,7 @@ Files headed `// Do not edit by hand` are generated. To change one, edit its sou
 
 ## Compatibility principle
 
-Gale targets full compatibility with the ANTLR4 `.g4` syntax. The g4 parser must accept any well-formed grammar upstream `antlr4` accepts; a real-world `.g4` that ANTLR4 accepts but Gale rejects is a Gale bug. The exceptions are enumerated under claim (a) in [`antlr4-compatibility.md`](./antlr4-compatibility.md) — today an action body Gale's translator cannot render, and `import Foo = Bar;`.
+Gale targets full compatibility with the ANTLR4 `.g4` syntax. The g4 parser must accept any well-formed grammar upstream `antlr4` accepts; a real-world `.g4` that ANTLR4 accepts but Gale rejects is a Gale bug. The one exception is `import Foo = Bar;`; claim (a) in [`antlr4-compatibility.md`](./antlr4-compatibility.md) carves it out.
 
 - Compatibility is a capability contract, not byte-for-byte output. Parse trees, tokens, and semantics must match; incidental rendering differences that carry no structure may diverge (e.g. the `<EOF>` marker in `toStringTree()`).
 - Gale is a superset: it may accept grammars ANTLR4 rejects only when the meaning is uniquely determined by Gale's language model — never an invented behavior. When accepting would require guessing, reject loudly. Examples: `.`/`~X`-led left-recursive suffixes, and a lexer `mode` inside a combined `grammar` (ANTLR4 allows modes only in a `lexer grammar`; a combined grammar already bundles a lexer, so it desugars unambiguously — still rejected in a `parser grammar`).

package-gale/README.md

@@ -7,8 +7,8 @@ with no runtime to install and no version to keep in sync.
 
 The `.g4` format is ANTLR4's; for the full grammar language, see ANTLR4's
 [documentation](https://github.com/antlr/antlr4/tree/master/doc). Gale accepts
-every grammar ANTLR4 accepts bar a short list — and a few it rejects, where the
-meaning is unambiguous (see [Design](#design)).
+every grammar ANTLR4 accepts bar one — and a few it rejects, where the meaning
+is unambiguous (see [Design](#design)).
 
 ## Design
 
@@ -21,9 +21,9 @@ with no remaining choice — e.g. a `.`- or `~X`-led left-recursive suffix like
 `e ~';' e`, which ANTLR4 errors on (no operator token to climb); or a lexer
 `mode` inside a combined `grammar`, which ANTLR4 restricts to a `lexer grammar`
 but which is unambiguous since a combined grammar already bundles a lexer. Where
-the meaning is not uniquely determined, Gale rejects loudly rather than guessing
-— including a handful of grammars ANTLR4 accepts, listed under claim (a) in
-[`antlr4-compatibility.md`](./antlr4-compatibility.md).
+the meaning is not uniquely determined, Gale rejects loudly rather than guessing.
+That costs it one grammar ANTLR4 accepts, `import Foo = Bar;`, carved out under
+claim (a) in [`antlr4-compatibility.md`](./antlr4-compatibility.md).
 
 Self-contained output, no version drift. Gale inlines its entire runtime into
 every generated parser. There is no `gale-runtime` package to keep aligned with

package-gale/antlr4-compatibility.md

@@ -123,12 +123,14 @@ that should be fixed before Stage C lands.
 > **Claim:** the generated code satisfies each of these independently:
 >
 > - **(a)** Every well-formed `.g4` file accepted by upstream `antlr4`
->   is accepted by Gale's `g4::parse`, with two exceptions: the
->   action-body one documented in [`AGENTS.md`](./AGENTS.md), and
+>   is accepted by Gale's `g4::parse`, with one exception:
 >   `import Foo = Bar;`, whose alias names the delegate for qualified
 >   action references Gale has no counterpart for
->   ([`import.md`](./import.md)). A descriptor bringing slave grammars
->   claims (a) of the whole composition, through `assemble_grammar`.
+>   ([`import.md`](./import.md)). An action body the translator cannot
+>   render parses fine and fails later, at codegen, with a diagnostic
+>   naming it ([`action.md`](./action.md)), so it is not an exception
+>   here. A descriptor bringing slave grammars claims (a) of the whole
+>   composition, through `assemble_grammar`.
 > - **(b)** For every descriptor whose upstream `[output]` describes a
 >   _successful_ parse, the parser generated by Gale accepts the
 >   descriptor's `[input]` without returning an error.

package-gale/import.md

@@ -69,15 +69,14 @@ it, given four conventions in the delegate:
   the delegate's mode, never produces that token. The gate is deliberate: a
   parser rule is reached in whatever mode its caller pushed, and nothing records
   that, so a literal is read as the mode the parser starts in.
-- No token of its own may span the host's terminator. A composite has one lexer,
-  so inside the mode a delegate rule is matched like any other: a
-  `JS_COMMENT : '//' ~[\r\n]*` runs straight through `</script>`, the mode never
-  pops, and the rest of the document is lexed as JavaScript. A mode cannot
-  express HTML's rule that a closing tag ends raw text whatever the embedded
-  language thinks — deciding that needs lookahead a mode does not have. So a
-  scanning rule stops at `<`, and the `<` it then rejects inside a string or a
-  comment is a stated hole in the delegate rather than a document in the wrong
-  mode.
+- No token of its own may span the host's terminator. Inside the mode a delegate
+  rule is matched like any other, so a `JS_COMMENT : '//' ~[\r\n]*` runs straight
+  through `</script>`. The mode then never pops, and the rest of the document is
+  lexed as JavaScript. A lexer mode cannot express HTML's rule that a closing tag
+  ends raw text whatever the embedded language thinks, because deciding that
+  needs lookahead the mode does not have. So a scanning rule stops at `<`, and
+  the `<` it then rejects inside a string or a comment is a stated hole in the
+  delegate rather than a document in the wrong mode.
 
 The host declares the same mode name for the token that leaves it
 (`STYLE_CLOSE : '</style>' -> popMode ;` under its own `mode CSS;`), and the

package-gale/src/ir.wado

@@ -1539,8 +1539,10 @@ fn rebase_lexer_rules(g: &Grammar, modes: &mut List<String>, channels: &mut List
         if r.set_mode >= 0 {
             r.set_mode = mode_remap[r.set_mode];
         }
-        // A numeric `channel(N)` literal is an explicit id with no
-        // `channels { }` entry behind it, so it has no remap slot.
+        // A `channels { }` block is the grammar's own numbering, so inside its
+        // range an id and the name declared at that index are one channel and
+        // rebasing carries both. Past the range a numeric `channel(N)` has no
+        // entry behind it and stays as written.
         if r.channel >= 2 {
             let src_idx = r.channel - 2;
             if src_idx < chan_remap.len() {

wado-compiler/src/optimize/sroa_variant_return.rs

@@ -105,11 +105,8 @@ impl Layout {
             .map(|i| u32::try_from(i).expect("variant case index overflow"))
     }
 
-    /// The payload a binding for `case_index` receives, `None` for a unit case,
-    /// which has no slot to read. The slot's own type can be the nullable
-    /// widening [`slot_shape`] chose for it, which `wir_build` bridges; a
-    /// wrapper around the payload it never bridges, so that is what the binding
-    /// has to be measured against.
+    /// The payload a binding for `case_index` receives. `None` for a unit case,
+    /// which has no slot to read.
     fn payload_read_type(&self, case_index: u32) -> Option<TypeId> {
         self.case_slots[case_index as usize].flat()?;
         Some(self.case_payloads[case_index as usize])
@@ -1608,10 +1605,7 @@ fn check_uses(
                         let rewritable = via_temp
                             .or(via_call)
                             .and_then(|f| candidates.get(&f))
-                            .is_some_and(|c| {
-                                arms.iter()
-                                    .all(|a| arm_is_one_level(body, a, rebind, &c.layout))
-                            });
+                            .is_some_and(|c| arms_are_one_level(body, &arms, rebind, &c.layout));
                         if !rewritable {
                             invalid.extend(via_temp.into_iter().chain(via_call));
                         }
@@ -1699,26 +1693,18 @@ enum Rebound<'a> {
     Boxed { box_type: TypeId, name: &'a str },
 }
 
-fn peel_refs(mut ty: TypeId, type_table: &TypeTable) -> TypeId {
-    while let ResolvedType::Ref(inner) | ResolvedType::MutRef(inner) = type_table.get(ty) {
-        ty = *inner;
-    }
-    ty
-}
-
 /// Per-function facts deciding whether a payload binding can be re-minted, and
 /// in what form. A local a `stores` parameter aliases cannot: the alias is
 /// established outside this body, and the `let` would not re-establish it.
-/// Neither can one whose declared type is neither the pattern's own type nor a
-/// `Box` of it — local indices are pooled, so a declaration that matches
-/// nothing the pattern names belongs to another binding.
+/// Neither can one whose declared type is neither the payload nor a `Box` of it
+/// — local indices are pooled, so a declaration matching neither belongs to
+/// another binding.
 struct Rebind {
     aliased: IndexSet<u32>,
     local_types: Vec<TypeId>,
-    /// Each declared local type with its `&` / `&mut` layers stripped. `&T` is
-    /// `T` at WIR level (`wir_build::context`), and everything needing a cell
-    /// reaches here already rewritten to `Box<T>`, so a reference binding takes
-    /// the payload as it stands.
+    /// Each declared local type with its `&` / `&mut` layers stripped: `&T` is
+    /// `T` at WIR level (`wir_build::context`), what needs a cell arriving as
+    /// `Box<T>` instead.
     peeled_types: Vec<TypeId>,
     /// Declared `Box<T>` local type → (`T`, the struct's rendered name).
     boxes: IndexMap<TypeId, (TypeId, String)>,
@@ -1760,10 +1746,9 @@ impl Rebind {
         }
     }
 
-    /// `payload_type` is what the slot read produces, never what the pattern
-    /// spells: `lower::plan::boxing` rewrites an address-taken binding's pattern
-    /// type along with its local, so the two agreeing proves nothing about the
-    /// value that arrives.
+    /// `payload_type` is what the slot read produces. Never pass the pattern's
+    /// own type: `lower::plan::boxing` rewrites it along with the local, so the
+    /// two agreeing says nothing about the value that arrives.
     fn rebound(&self, local: u32, payload_type: TypeId) -> Option<Rebound<'_>> {
         if self.aliased.contains(&local) {
             return None;
@@ -1782,6 +1767,18 @@ impl Rebind {
     }
 }
 
+fn peel_refs(mut ty: TypeId, type_table: &TypeTable) -> TypeId {
+    while let ResolvedType::Ref(inner) | ResolvedType::MutRef(inner) = type_table.get(ty) {
+        ty = *inner;
+    }
+    ty
+}
+
+fn arms_are_one_level(body: &Body, arms: &[ArmData], rebind: &Rebind, layout: &Layout) -> bool {
+    arms.iter()
+        .all(|a| arm_is_one_level(body, a, rebind, layout))
+}
+
 /// One level deep over the scrutinee's own variant, binding at most one name
 /// the rewrite can re-mint. A nested pattern (`Ok(Some(x))`) is rejected rather
 /// than peeled — peeling is where the WIR pass's complexity lives.
@@ -2313,9 +2310,7 @@ fn collect_call_scrutinees(
     if let NodeRef::Expr(e) = node
         && let ExprKind::Match { expr: scrut, arms } = &body.exprs[e].kind
         && let Some(cand) = call_callee(body, *scrut).and_then(|f| candidates.get(&f))
-        && arms
-            .iter()
-            .all(|a| arm_is_one_level(body, a, rebind, &cand.layout))
+        && arms_are_one_level(body, arms, rebind, &cand.layout)
     {
         out.push(e);
     }
@@ -2458,10 +2453,7 @@ fn check_temp_uses(
             }
             ExprKind::Match { expr: scrut, arms } => {
                 if is_local(body, *scrut, local) {
-                    if !arms
-                        .iter()
-                        .all(|a| arm_is_one_level(body, a, rebind, layout))
-                    {
+                    if !arms_are_one_level(body, arms, rebind, layout) {
                         *ok = false;
                         return;
                     }

wado-compiler/tests/fixtures/bug_sroa_variant_return_boxed_payload_binding.wado

@@ -3,10 +3,10 @@
 // `make` returns `Result<Big, Failure>`, which variant-return SROA flattens to
 // `[tag, Option<Big>, Option<Failure>]`. `err` is address-taken by `${err:?}`,
 // so lowering promotes its local to `Box<Failure>` and rewrites the pattern's
-// own type to match. The rewrite asked whether the local's declared type equals
-// the pattern's, which both hold after that promotion, and bound the raw slot
-// read into a `Box<Failure>` local: "type mismatch: expected (ref null $type),
-// found (ref $type)" at codegen. The question is what the slot read produces.
+// own type to match. Measuring the local against the pattern rather than
+// against the payload the slot yields therefore passed, and the raw read landed
+// in a `Box<Failure>` local: "type mismatch: expected (ref null $type), found
+// (ref $type)" at codegen.
 use { println, Stdout } from "core:cli";
 
 variant Failure {