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

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>

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 ------------------------- )