diff --git a/compiler/lib/ast.ml b/compiler/lib/ast.ml index 01bb1f0..692799e 100644 --- a/compiler/lib/ast.ml +++ 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 (** + *) diff --git a/compiler/lib/eval.ml b/compiler/lib/eval.ml index f53cf83..8d748b5 100644 --- a/compiler/lib/eval.ml +++ b/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. *) diff --git a/compiler/lib/parser.mly b/compiler/lib/parser.mly index 3e42ab6..969a2f9 100644 --- a/compiler/lib/parser.mly +++ b/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) ---- *) diff --git a/compiler/lib/pretty.ml b/compiler/lib/pretty.ml index c96db47..17eb0a9 100644 --- a/compiler/lib/pretty.ml +++ 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 *) (* ------------------------------------------------------------------ *) diff --git a/compiler/lib/typecheck.ml b/compiler/lib/typecheck.ml index 9344e62..8ed563b 100644 --- a/compiler/lib/typecheck.ml +++ b/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 diff --git a/compiler/test/test_parser.ml b/compiler/test/test_parser.ml index 2447bd5..117bdc1 100644 --- a/compiler/test/test_parser.ml +++ b/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 *) diff --git a/compiler/test/tg3/tg3_emit.ml b/compiler/test/tg3/tg3_emit.ml index 4c53009..1ac2ae7 100644 --- a/compiler/test/tg3/tg3_emit.ml +++ b/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" (* ================================================================== *) diff --git a/scripts/check-corpus.sh b/scripts/check-corpus.sh index 0627332..5946766 100755 --- a/scripts/check-corpus.sh +++ b/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 diff --git a/spec/grammar.ebnf b/spec/grammar.ebnf index c718869..6b05392 100644 --- a/spec/grammar.ebnf +++ b/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 ------------------------- )