fix(typecheck): implement [T-Twist-Strand] — (~a) on a named strand (#96)

[hyperpolymath]

conformance/valid/v09_twist.tangle parsed but failed to typecheck:

def twisted =
  weave strands a:Q into
    (~a)
  yield strands a:Q

Strand name 'a' cannot be used as a standalone expression

The spec licenses it explicitly

FORMAL-SEMANTICS.md §3.10:

Σ(a) = (i, T)
───────────────────────────────────  [T-Twist-Strand]
Γ; Σ ⊢ (~a) : Tangle[[T], [T]]

and spec/grammar.ebnf: "In weave context: (~a) twists named strand a."

The Twist case inferred its operand as an ordinary expression, and the Var rule rejects strand names outright — so the strand-name guard fired before the twist rule could apply. [T-Twist-Strand] is now tried first, leaving [T-Twist-Word]/[T-Twist-Tangle] to the standalone forms.

One of a matched pair was missing

The spec presents this rule immediately alongside [T-Self-Cross]:

Σ(a) = (i, T)                          Σ(a) = (i, T)
─────────────────────────────────      ─────────────────────────────────
Γ; Σ ⊢ (~a) : Tangle[[T], [T]]         Γ; Σ ⊢ (a > a) : Tangle[[T], [T]]

[T-Self-Cross] was already implemented; its twin was not. A test now pins that the two agree, so they can't drift apart again.

Evaluation

Mirrors Crossing: structural, yielding the empty word. Weave bodies only became evaluable in #93, so this construct had never run.

That's also defensible mathematically — a single-strand twist is invisible to the braid word: it's a framing change (Reidemeister I) that the braid group doesn't see.

Detecting it as "a Var the environment doesn't bind" is safe because typechecking runs first and admits Twist (Var a) only when a is a strand.

Result

conformance 16/19 → 17/19 evaluating (18/19 parse). The corpus ratchet demanded the manifest update — exactly what it's for. v11_add_block (#94, the Harvard sub-language) is now the only remaining gap.

Tests: the rule itself; agreement with [T-Self-Cross]; a regression guard that standalone twist on a Word is unchanged; and that a nonsense twist still fails.

All suites green; corpus and RSR gates pass.

🤖 Generated with Claude Code

[gitar-bot]

Note

Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime.
Learn more

Code Review ✅ Approved 1 resolved / 1 findings

Implements the [T-Twist-Strand] typechecking and evaluation rule for named strands in weave contexts, advancing the conformance suite to 17/19. Consider aligning the twist evaluation guard with typechecking to prevent divergence under name shadowing.

Auto-approved and auto-merge armed: No blocking issues found.
Please see Auto-approve Docs for details on setting custom approval criteria. — merges when pipeline and required approvals pass.

✅ 1 resolved

✅ Edge Case: Twist eval guard diverges from typecheck under name shadowing

📄 compiler/lib/eval.ml:440-441 📄 compiler/lib/typecheck.ml:390-393
In eval.ml the [T-Twist-Strand] case is detected by Twist (Var a) when env_lookup env a = None, whereas the typechecker prioritizes the strand context (strand_lookup sigma a) over gamma. If a weave strand a shares a name with a top-level def a, typecheck classifies (~a) as a strand twist (Tangle[[T],[T]]) but eval finds a bound in env and falls through to the general Twist e1 branch, twisting the def's braid/tangle value instead of producing the structural empty word. The two phases then disagree on the meaning of the same expression. The neighboring Crossing case avoids this by ignoring env entirely; consider mirroring that (or checking the strand context) so eval and typecheck agree regardless of shadowing.

Options

Display: compact → Showing less information.

Comment with these commands to change the behavior for this request:

Compact

gitar display:verbose

_{Was this helpful? React with 👍 / 👎 | Gitar}

[gitar-bot]

⚠️ Gitar auto-approved this PR but could not enable auto-merge: auto-merge is disabled for this repository — enable "Allow auto-merge" in the repository settings.

[gitar-bot]

Gitar has auto-approved this PR and enabled auto-merge (configure)