feat(parser): weave is an expression, not only a statement (#88 B) (#93)

Four of the five unparsed `conformance/valid/` programs — `v02_weave`,
`v08_crossing`, `v09_twist`, `v12_weave_expr` — use weave as a
**definition body**:

```tangle
def simple_crossing =
  weave strands a:Q, b:Q into
    (a > b)
  yield strands b:Q, a:Q
```

The grammar allowed weave only as a top-level statement, so all four
failed. Typed strands (`a:Q`) and `yield strands` were 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.ebnf` also said statement. Then I checked what a weave
statement actually *does*:

```ocaml
(* eval.ml *)
| WeaveBlock _wb -> (env, None)          (* no-op *)

(* typecheck.ml *)
let _weave_ty = TTangle (input_boundary, output_boundary) in
gamma                                     (* type computed, then DISCARDED *)
```

**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, and `Weave` joins the other non-core constructors in
`tg3_emit`'s explicit rejection branch rather than being translated.

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 exactly as the statement form does),
`eval` (the body *is* the value), and `pretty` (re-parseable form).
`expr_calls` also traverses into a weave body — otherwise recursion
inside one would be invisible to the #91 fixpoint search.

## What this does NOT fix: `v11_add_block`

`add{ 1 + 2 + 3 }` is **not a missing parse rule**. It is the **Harvard
data sub-language**:

| | |
|---|---|
| own expression grammar | literals, vars, arithmetic, equality,
`&&`/`\|\|`/`!`, calls, `if/then/else` |
| own type system | Int, Float, Rational, Hex, Binary, Bool, String,
Symbolic |
| own environments | `Π`, with visibility rules |
| own typing judgement | `⊢_hd` |
| conversion layer | Embed / Unembed |
| calling | bidirectional with Tangle |

**288 lines of `FORMAL-SEMANTICS.md` across 12 sections.** That is a
feature, raised separately. It remains the single entry in the corpus
manifest's known-gap list.

## Results

| | before | after |
|---|---|---|
| conformance | 14/19 | **18/19** |
| corpus manifest known-unparsed | 5 | **1** |

(It reported a *fake* 3/19 before #89 fixed the runner.)

The ratchet in `check-corpus.sh` **demanded** 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

- weave as a definition body (the conformance form)
- **TG-4 round-trip**: pretty-print then re-parse yields the same AST —
needed because I changed `pretty.ml`
- guard that the statement form still parses (the change is additive)

Full suite green, 0 failures; TG-3 still 1008/0. `spec/grammar.ebnf`
updated to match, with the rationale recorded.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

Author: hyperpolymath

compiler/lib/ast.ml

@@ -108,6 +108,18 @@ and expr =
   (* ---- Crossings (weave context) ---- *)
   | Crossing  of string * crossing_op * string
 
+  (* ---- Weave as an EXPRESSION ----
+   * `weave ... into ... yield ...` was a statement only, per spec/grammar.ebnf.
+   * As a statement it is inert: eval returns (env, None) and the typechecker
+   * discards the Tangle[A,B] it computes, so the construct could be written
+   * but never bound or used.  Allowing it in expression position is what makes
+   * it reachable — and is how conformance/valid/v02, v08, v09 and v12 have
+   * always been written (`def x = weave ...`).  The statement form is kept, so
+   * this is purely additive.  Weave is outside the mechanised Lean core (0
+   * occurrences in proofs/Tangle.lean) and outside the TG-3 corpus, so this
+   * touches no proof obligation. *)
+  | Weave     of weave_block
+
 (** Binary operator tag. *)
 and binop =
   | Add       (** + *)

compiler/lib/eval.ml

@@ -384,6 +384,18 @@ let rec eval_expr (env : env) (e : expr) : value =
     | _ -> eval_error "Cannot simplify %s" (pp_value v)
     end
 
+  | Weave wb ->
+    (* The statement form is a no-op returning (env, None) — the value was
+       unreachable, which is what made weave inert.  In expression position the
+       body IS the value: it denotes the morphism from the input strands to the
+       output strands, so evaluate it and present it as a tangle. *)
+    begin match eval_expr env wb.weave_body with
+    | VTangle _ as t -> t
+    | VBraid gens    -> VTangle { tv_word = gens; tv_closed = false }
+    | v -> eval_error "Weave body must evaluate to a braid or tangle, got %s"
+             (pp_value v)
+    end
+
   | Cap (_e1, _e2) ->
     (* Cap creates a tangle that absorbs two strands — a single-crossing
        cup/cap pair.  Represented as an empty closed tangle. *)

compiler/lib/parser.mly

@@ -321,6 +321,8 @@ primary_expr:
     { e }
   | LBRACE e = expr RBRACE
     { e }
+  | w = weave_block
+    { Weave w }
   ;
 
 (* ---- Crossings: (a > b) or (a < b) ---- *)

compiler/lib/pretty.ml

@@ -88,6 +88,18 @@ let rec pp_pattern ctx = function
 (*  Expressions                                                        *)
 (* ------------------------------------------------------------------ *)
 
+let pp_typed_strand ctx ts =
+  emit ctx ts.strand_name;
+  match ts.strand_type with
+  | Some t -> emit ctx ": "; emit ctx t
+  | None -> ()
+
+let pp_strand_list ctx strands =
+  List.iteri (fun i s ->
+    if i > 0 then emit ctx ", ";
+    pp_typed_strand ctx s
+  ) strands
+
 let rec pp_expr ctx = function
   | Match (scrut, arms) ->
     emit ctx "match ";
@@ -254,6 +266,16 @@ let rec pp_expr ctx = function
     ) args;
     emit ctx ")"
 
+  | Weave w ->
+    (* Same surface syntax as the statement form; in expression position it
+       re-parses via primary_expr, so TG-4's round-trip property holds. *)
+    emit ctx "weave strands ";
+    pp_strand_list ctx w.weave_inputs;
+    emit ctx " into ";
+    pp_expr ctx w.weave_body;
+    emit ctx " yield strands ";
+    pp_strand_list ctx w.weave_outputs
+
   | Crossing (a, op, b) ->
     emit ctx "(";
     emit ctx a;
@@ -267,18 +289,6 @@ let rec pp_expr ctx = function
 (*  Typed strands                                                      *)
 (* ------------------------------------------------------------------ *)
 
-let pp_typed_strand ctx ts =
-  emit ctx ts.strand_name;
-  match ts.strand_type with
-  | Some t -> emit ctx ": "; emit ctx t
-  | None -> ()
-
-let pp_strand_list ctx strands =
-  List.iteri (fun i s ->
-    if i > 0 then emit ctx ", ";
-    pp_typed_strand ctx s
-  ) strands
-
 (* ------------------------------------------------------------------ *)
 (*  Statements                                                         *)
 (* ------------------------------------------------------------------ *)

compiler/lib/typecheck.ml

@@ -189,6 +189,35 @@ let rec infer_expr (gamma : env) (sigma : strand_ctx) (e : expr) : ty =
     let n = width_of_generators gens in
     TWord n
 
+  (* [T-Weave] in expression position.
+     The statement form computed this same Tangle[A,B] and then DISCARDED it
+     (`let _weave_ty = ... in gamma`), which is why weave was inert.  Here the
+     type is the expression's type, so the result can be bound and used. *)
+  | Weave wb ->
+    let sigma' = List.mapi (fun i ts ->
+      let sty = match ts.strand_type with
+        | Some name -> StrandNamed name
+        | None      -> StrandDefault
+      in
+      (ts.strand_name, { strand_pos = i + 1; strand_ty = sty })
+    ) wb.weave_inputs in
+    let input_boundary = List.map (fun (_, se) -> se.strand_ty) sigma' in
+    (* The body is checked in the strand context, exactly as the statement
+       form does — strand names are only meaningful there. *)
+    let body_ty = infer_expr gamma sigma' wb.weave_body in
+    begin match body_ty with
+    | TTangle (_, _) | TWord _ -> ()   (* words coerce to tangles *)
+    | _ ->
+      type_error "Weave body must produce a Word or Tangle type, got %s"
+        (pp_ty body_ty)
+    end;
+    let output_boundary = List.map (fun ts ->
+      match ts.strand_type with
+      | Some name -> StrandNamed name
+      | None      -> StrandDefault
+    ) wb.weave_outputs in
+    TTangle (input_boundary, output_boundary)
+
   (* ---- Variables [T-Var] ---- *)
 
   | Var name ->
@@ -668,6 +697,7 @@ let rec expr_calls (f : string) (e : expr) : bool =
   | EchoAdd (e1, e2) | EchoEq (e1, e2) -> go e1 || go e2
   | UnaryOp (_, e1) | Close e1 | Mirror e1 | Reverse e1 | Simplify e1
   | Twist e1 | EchoClose e1 | Lower e1 | Residue e1 | Fst e1 | Snd e1 -> go e1
+  | Weave wb -> go wb.weave_body
   | BraidLit _ | Identity | BoolLit _ | IntLit _ | FloatLit _
   | StringLit _ | Var _ | Crossing _ -> false
 

compiler/test/test_parser.ml

@@ -176,7 +176,47 @@ let test_weave_blocks () =
         (List.nth w.weave_inputs 0).strand_type;
       assert_eq "output1 type" (Some "Strand")
         (List.nth w.weave_outputs 0).strand_type
-    | _ -> failwith "expected single WeaveBlock")
+    | _ -> failwith "expected single WeaveBlock");
+
+  (* ---------------------------------------------------------------- *)
+  (* #88(B): weave in EXPRESSION position.                             *)
+  (* It was a statement only, and as a statement it is inert — eval     *)
+  (* returns (env, None) and the typechecker discards the Tangle[A,B]   *)
+  (* it computes, so the construct could be written but never bound.    *)
+  (* conformance/valid/v02, v08, v09 and v12 have always used the       *)
+  (* `def x = weave ...` form; they could not parse until now.          *)
+  (* ---------------------------------------------------------------- *)
+
+  test "#88 weave as a definition body (the conformance form)" (fun () ->
+    let prog = parse_ok
+      "def simple_crossing = weave strands a:Q, b:Q into (a > b) yield strands b:Q, a:Q" in
+    match prog with
+    | [Definition d] ->
+      (match d.def_body with
+       | Weave w ->
+         assert_eq "inputs" 2 (List.length w.weave_inputs);
+         assert_eq "outputs" 2 (List.length w.weave_outputs);
+         assert_eq "input1 type" (Some "Q") (List.nth w.weave_inputs 0).strand_type
+       | _ -> failwith "expected the body to be a Weave expression")
+    | _ -> failwith "expected a single Definition");
+
+  test "#88 weave expression round-trips (TG-4 property)" (fun () ->
+    (* The pretty-printed form must re-parse to the same AST, or TG-4's
+       parse(pretty(e)) = e obligation would no longer hold for weave. *)
+    let src =
+      "def x = weave strands a: Q, b: Q into (a > b) yield strands b: Q, a: Q" in
+    let p1 = parse_ok src in
+    let printed = Tangle.Pretty.program_to_string p1 in
+    let p2 = parse_ok printed in
+    assert_eq "pretty then re-parse yields the same AST" p1 p2);
+
+  test "#88 weave is still valid as a statement" (fun () ->
+    (* Regression guard: the change is additive. *)
+    let prog = parse_ok
+      "weave strands a, b into (a > b) yield strands c" in
+    match prog with
+    | [WeaveBlock _] -> ()
+    | _ -> failwith "expected the statement form to still parse")
 
 (* ================================================================== *)
 (*  3. Invariant computations                                          *)

compiler/test/tg3/tg3_emit.ml

@@ -133,7 +133,7 @@ let rec lean_expr (scope : string list) (e : expr) : string =
   (* Non-core: must never appear in the corpus (close is the boundary gateway). *)
   | FloatLit _ | BinOp ((Sub | Mul | Div | Isotopy), _, _) | UnaryOp _
   | Close _ | Mirror _ | Reverse _ | Simplify _ | Cap _ | Cup _ | Twist _
-  | Match _ | Call _ | Crossing _ ->
+  | Match _ | Call _ | Crossing _ | Weave _ ->
     failwith "TG-3: non-core constructor in corpus term"
 
 (* ================================================================== *)

scripts/check-corpus.sh

@@ -62,16 +62,18 @@ EXAMPLES_KNOWN_UNTYPED=(
   turing_complete.tangle
 )
 
-# conformance/valid programs the parser does not yet accept. These specify
-# language surface that exists in the spec but not in parser.mly. Tracked in #88.
-#   v02/v08/v09/v12 : `weave strands a:Q, b:Q into (...) yield strands ...`
-#   v11             : `add{ ... }` blocks (JTV data injection)
+# conformance/valid programs the parser does not yet accept.
+#   v11 : `add{ ... }` — the Harvard DATA SUB-LANGUAGE, not a parse rule. It has
+#         its own expression grammar, type system (Int/Float/Rational/Hex/
+#         Binary/Bool/String/Symbolic), environments (Pi), visibility rules, a
+#         separate typing judgement, Embed/Unembed, and bidirectional calling
+#         with Tangle — 288 lines of FORMAL-SEMANTICS.md across 12 sections.
+#         A feature, tracked separately.
+#
+# v02/v08/v09/v12 were here for `weave ... into ... yield ...` used as a
+# DEFINITION BODY. Fixed: weave is now an expression as well as a statement.
 CONFORMANCE_KNOWN_UNPARSED=(
-  v02_weave.tangle
-  v08_crossing.tangle
-  v09_twist.tangle
   v11_add_block.tangle
-  v12_weave_expr.tangle
 )
 
 fail=0

spec/grammar.ebnf

@@ -121,8 +121,16 @@ primary = braid_literal
 | crossing
 | identifier, [ "(", arg_list, ")" ]
 | literal
+| weave_block
 | "(", expr, ")" ;
 
+(* weave_block appears BOTH as a statement (above) and as a primary
+   expression. As a statement alone it was inert: its Tangle[A,B] type was
+   computed and discarded, and evaluation was a no-op, so the construct could
+   be written but never bound or used. In expression position it denotes the
+   morphism, which is how `def x = weave ... into ... yield ...` works and how
+   conformance/valid/v02, v08, v09 and v12 have always been written. *)
+
 arg_list = expr, { ",", expr } ;
 
 (* -------------------- Braid Literals ------------------------- )