feat(parser): weave is an expression, not only a statement (#88 B) - #93
Conversation
Four of the five unparsed conformance/valid programs (v02_weave,
v08_crossing, v09_twist, v12_weave_expr) use weave as a DEFINITION BODY:
def simple_crossing =
weave strands a:Q, b:Q into
(a > b)
yield strands b:Q, a:Q
The grammar only allowed it as a top-level statement, so all four failed to
parse. Typed strands and `yield strands` were never the problem — those
already worked; only the position did.
## Why the expression form is the right fix
As a statement, weave is INERT. Evaluation is a no-op returning (env, None),
and the typechecker computes its Tangle[A,B] and then discards it:
let _weave_ty = TTangle (input_boundary, output_boundary) in
gamma
So the construct could be written but never bound, never used, never
observed. Binding it to a name is the only thing that makes it reachable —
which is exactly what the conformance corpus has always assumed.
The statement form is kept, so this is purely additive.
## Scope
Weave is OUTSIDE the mechanised core: 0 occurrences in proofs/Tangle.lean and
0 in the TG-3 corpus. So this touches no proof obligation, and Weave is listed
with the other non-core constructors in tg3_emit's explicit rejection branch.
Threaded through ast (new `Weave of weave_block`), parser (primary_expr),
typecheck (types as the Tangle[A,B] it denotes; body checked in the strand
context as the statement form does), eval (the body IS the value), and pretty
(prints in re-parseable form). `expr_calls` also traverses into a weave body,
or recursion inside one would be invisible to the #91 fixpoint search.
Two strand printers moved above pp_expr — they had no dependency on it and
pp_expr now needs them.
## What is NOT fixed: v11_add_block
`add{ 1 + 2 + 3 }` is not a missing parse rule. It is the Harvard DATA
SUB-LANGUAGE: its own expression grammar, its own type system (Int / Float /
Rational / Hex / Binary / Bool / String / Symbolic), its own environments (Pi)
and visibility rules, a separate typing judgement, Embed/Unembed between
Harvard and Tangle types, and bidirectional calling. 288 lines of
FORMAL-SEMANTICS.md across 12 sections. That is a feature, raised separately;
it stays in the corpus manifest as the single remaining known gap.
conformance: 14/19 -> 18/19. (It was reporting a fake 3/19 before #89 fixed
the runner.) Corpus manifest tightened 5 -> 1 — the ratchet demanded it, which
is what it is for.
Tests: weave as a definition body, the TG-4 round-trip property (pretty then
re-parse yields the same AST), and a guard that the statement form still
parses. spec/grammar.ebnf updated to match, with the rationale.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
|
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. Code Review ✅ Approved 1 resolved / 1 findingsExpands the parser to support weave as an expression, successfully parsing four conformance tests previously blocked by grammar limits. Consider addressing the minor finding where weave evaluation discards the yield output-strand reordering.
✅ 1 resolved✅ Edge Case: Weave evaluation discards the yield output-strand reordering
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Was this helpful? React with 👍 / 👎 | Gitar |
|
|
1 participant
Four of the five unparsed
conformance/valid/programs —v02_weave,v08_crossing,v09_twist,v12_weave_expr— use weave as a definition body:The grammar allowed weave only as a top-level statement, so all four failed. Typed strands (
a:Q) andyield strandswere never the problem — those already parsed. Only the position did.Why the expression form is the right fix, not a corpus edit
My first instinct was that the corpus was wrong, since
spec/grammar.ebnfalso said statement. Then I checked what a weave statement actually does:As a statement, weave is inert. It binds nothing, produces nothing, and its type is thrown away. The construct could be written but never used. Binding it to a name is the only thing that makes it reachable — which is precisely what the corpus assumed all along.
The statement form is kept, so this is purely additive.
Scope — no proof implications
Weave is outside the mechanised core: 0 occurrences in
proofs/Tangle.lean, 0 in the TG-3 corpus. So this touches no proof obligation, andWeavejoins the other non-core constructors intg3_emit's explicit rejection branch rather than being translated.Threaded through
ast(newWeave of weave_block),parser(primary_expr),typecheck(types as theTangle[A,B]it denotes; body checked in the strand context exactly as the statement form does),eval(the body is the value), andpretty(re-parseable form).expr_callsalso traverses into a weave body — otherwise recursion inside one would be invisible to the #91 fixpoint search.What this does NOT fix:
v11_add_blockadd{ 1 + 2 + 3 }is not a missing parse rule. It is the Harvard data sub-language:&&/||/!, calls,if/then/elseΠ, with visibility rules⊢_hd288 lines of
FORMAL-SEMANTICS.mdacross 12 sections. That is a feature, raised separately. It remains the single entry in the corpus manifest's known-gap list.Results
(It reported a fake 3/19 before #89 fixed the runner.)
The ratchet in
check-corpus.shdemanded the manifest update — it failed the build with "now parses — drop it from CONFORMANCE_KNOWN_UNPARSED" for each file. That is exactly what it was built to do.Tests
pretty.mlFull suite green, 0 failures; TG-3 still 1008/0.
spec/grammar.ebnfupdated to match, with the rationale recorded.🤖 Generated with Claude Code