nx_probe_lone_operator.nx source
↩ module page · 26 lines · 1549 B
1// nx_probe_lone_operator.nx -- MUST-REFUSE WITNESS for spec clause LS-SYN-030 (discarded pure
2// expressions), and the fixture that clause NEEDS now that LN15 exists.
3//
4// WHY IT WAS WRITTEN, 2026-08-25. LS-SYN-030 says an expression statement that computes a value
5// with no side effect and never uses it is REFUSED rather than silently discarded. That clause is
6// still exactly true. Its old witness was nx_probe_mlneg_live.nx -- `let c = a` then a line opening
7// with `- b` -- which stopped exercising the clause the moment LN15 shipped, because that line now
8// JOINS the expression above it and the program is simply correct. The clause did not change; its
9// fixture stopped reaching the condition, which is the quietest way for a conformance case to go
10// vacuous: it keeps passing for a while and then keeps failing, and neither state is about the rule.
11//
12// THIS fixture cannot be joined to anything. The `- a` is the FIRST statement of its block, so there
13// is no expression above it to continue; it can only reach parse_stmt_expr_fallback, compute a value
14// and throw it away. That is the discarded-pure-expression class in its irreducible form.
15//
16// EXPECT: COMPILE-FAIL, exit 2, with 'computes a value and never uses it'. If this ever BUILDS, the
17// discarded-pure-expression refusal has been lost -- and unlike the two multi-line witnesses, there
18// is no benign reading of that: nothing here could have become correct instead.
19
20func main(argc: i64, argv: *u8) -> i64 {
21 let a: i64 = 1
22 if a == 1 {
23 - a
24 }
25 return 0
26}