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

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