|
| 1 | +// SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | +// (MPL-2.0 is automatic legal fallback until PMPL is formally recognised) |
| 3 | +// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 4 | + |
| 5 | +//! JtV v2 reversibility Phase 1 tests. |
| 6 | +//! |
| 7 | +//! Verifies that `reverse { x += v }` IS subtraction (x = x - v), per the |
| 8 | +//! canonical design in `docs/language/DESIGN-JTV-V2-REVERSIBILITY.md`. |
| 9 | +//! |
| 10 | +//! Subtraction is not a grammar primitive in JtV v2. It arises from |
| 11 | +//! reversing addition. `reverse { x += v }` does NOT do a forward pass — |
| 12 | +//! it applies the INVERSE of each operation in reverse declaration order. |
| 13 | +//! |
| 14 | +//! RV1 — single add: reverse { x += 5 } → x = x - 5 |
| 15 | +//! RV2 — single sub: reverse { x -= 3 } → x = x + 3 |
| 16 | +//! RV3 — chain: reverse { x += 5; y += 3 } → y -= 3 first, then x -= 5 |
| 17 | +//! RV4 — cross-var: reverse { x += y } → x = x - y |
| 18 | +//! RV5 — CNO via execute_and_reverse: net effect is identity |
| 19 | +//! RV6 — full-program parse + run with reverse { } |
| 20 | +//! RV7 — reverse is left-inverse of forward: (forward; reverse) = identity |
| 21 | +
|
| 22 | +use jtv_core::{ |
| 23 | + ast::{DataExpr, Number, ReverseBlock, ReversibleStmt}, |
| 24 | + number::Value, |
| 25 | + parser::parse_program, |
| 26 | + reversible::ReversibleInterpreter, |
| 27 | + Interpreter, |
| 28 | +}; |
| 29 | + |
| 30 | +// ── RV1: reverse add is subtract ──────────────────────────────────────────── |
| 31 | + |
| 32 | +#[test] |
| 33 | +fn rv1_reverse_add_is_subtract() { |
| 34 | + let mut interp = Interpreter::new(); |
| 35 | + let src = r#" |
| 36 | +x = 10 |
| 37 | +reverse { x += 5 } |
| 38 | +"#; |
| 39 | + let prog = parse_program(src).expect("should parse"); |
| 40 | + interp.run(&prog).expect("should run"); |
| 41 | + |
| 42 | + let x = interp.get_variables().into_iter() |
| 43 | + .find(|(k, _)| k == "x").map(|(_, v)| v); |
| 44 | + assert_eq!(x, Some(Value::Int(5)), |
| 45 | + "reverse {{ x += 5 }} with x=10 should give x=5 (subtraction)"); |
| 46 | +} |
| 47 | + |
| 48 | +// ── RV2: reverse sub is add ────────────────────────────────────────────────── |
| 49 | + |
| 50 | +#[test] |
| 51 | +fn rv2_reverse_sub_is_add() { |
| 52 | + let mut interp = Interpreter::new(); |
| 53 | + let src = r#" |
| 54 | +x = 10 |
| 55 | +reverse { x -= 3 } |
| 56 | +"#; |
| 57 | + let prog = parse_program(src).expect("should parse"); |
| 58 | + interp.run(&prog).expect("should run"); |
| 59 | + |
| 60 | + let x = interp.get_variables().into_iter() |
| 61 | + .find(|(k, _)| k == "x").map(|(_, v)| v); |
| 62 | + assert_eq!(x, Some(Value::Int(13)), |
| 63 | + "reverse {{ x -= 3 }} with x=10 should give x=13 (inverse of subtraction is addition)"); |
| 64 | +} |
| 65 | + |
| 66 | +// ── RV3: multi-op chain inverts in reverse order ───────────────────────────── |
| 67 | + |
| 68 | +#[test] |
| 69 | +fn rv3_chain_inverts_in_reverse_declaration_order() { |
| 70 | + // reverse { x += 5 ; y += 3 } |
| 71 | + // Should apply: y -= 3 first, then x -= 5 |
| 72 | + // Both are independent, so order doesn't matter here; test values confirm semantics. |
| 73 | + let mut interp = Interpreter::new(); |
| 74 | + let src = r#" |
| 75 | +x = 10 |
| 76 | +y = 20 |
| 77 | +reverse { x += 5 y += 3 } |
| 78 | +"#; |
| 79 | + let prog = parse_program(src).expect("should parse"); |
| 80 | + interp.run(&prog).expect("should run"); |
| 81 | + |
| 82 | + let vars: std::collections::HashMap<String, Value> = |
| 83 | + interp.get_variables().into_iter().collect(); |
| 84 | + assert_eq!(vars.get("x"), Some(&Value::Int(5)), |
| 85 | + "x should be 10-5=5"); |
| 86 | + assert_eq!(vars.get("y"), Some(&Value::Int(17)), |
| 87 | + "y should be 20-3=17"); |
| 88 | +} |
| 89 | + |
| 90 | +// ── RV4: cross-variable: reverse { x += y } → x = x - y ──────────────────── |
| 91 | + |
| 92 | +#[test] |
| 93 | +fn rv4_cross_variable_reverse() { |
| 94 | + let mut interp = Interpreter::new(); |
| 95 | + let src = r#" |
| 96 | +x = 10 |
| 97 | +y = 3 |
| 98 | +reverse { x += y } |
| 99 | +"#; |
| 100 | + let prog = parse_program(src).expect("should parse"); |
| 101 | + interp.run(&prog).expect("should run"); |
| 102 | + |
| 103 | + let x = interp.get_variables().into_iter() |
| 104 | + .find(|(k, _)| k == "x").map(|(_, v)| v); |
| 105 | + assert_eq!(x, Some(Value::Int(7)), |
| 106 | + "reverse {{ x += y }} with x=10, y=3 should give x=7"); |
| 107 | +} |
| 108 | + |
| 109 | +// ── RV5: CNO via execute_and_reverse ──────────────────────────────────────── |
| 110 | + |
| 111 | +#[test] |
| 112 | +fn rv5_cno_execute_and_reverse_is_identity() { |
| 113 | + let mut interp = ReversibleInterpreter::new(); |
| 114 | + interp.set("x".to_string(), Value::Int(42)); |
| 115 | + interp.set("y".to_string(), Value::Int(100)); |
| 116 | + |
| 117 | + let block = ReverseBlock { |
| 118 | + body: vec![ |
| 119 | + ReversibleStmt::AddAssign("x".to_string(), DataExpr::Number(Number::Int(7))), |
| 120 | + ReversibleStmt::AddAssign("y".to_string(), DataExpr::Number(Number::Int(15))), |
| 121 | + ], |
| 122 | + }; |
| 123 | + |
| 124 | + interp.execute_and_reverse(&block).expect("CNO should not fail"); |
| 125 | + |
| 126 | + assert_eq!(interp.get("x"), Some(&Value::Int(42)), "x must be unchanged after CNO"); |
| 127 | + assert_eq!(interp.get("y"), Some(&Value::Int(100)), "y must be unchanged after CNO"); |
| 128 | +} |
| 129 | + |
| 130 | +// ── RV6: full-program parse + run ──────────────────────────────────────────── |
| 131 | + |
| 132 | +#[test] |
| 133 | +fn rv6_full_program_with_reverse_block() { |
| 134 | + // A meaningful program: accumulate a total, then reverse one step. |
| 135 | + // JtV top-level uses `x = expr` for assignment; `+=` is reverse-block only. |
| 136 | + let src = r#" |
| 137 | +total = 100 |
| 138 | +bonus = 25 |
| 139 | +total = total + bonus |
| 140 | +reverse { total += bonus } |
| 141 | +"#; |
| 142 | + // After: total = 100 + 25 = 125; then reverse { total += 25 } → total = 125 - 25 = 100 |
| 143 | + let mut interp = Interpreter::new(); |
| 144 | + let prog = parse_program(src).expect("should parse"); |
| 145 | + interp.run(&prog).expect("should run"); |
| 146 | + |
| 147 | + let vars: std::collections::HashMap<String, Value> = |
| 148 | + interp.get_variables().into_iter().collect(); |
| 149 | + assert_eq!(vars.get("total"), Some(&Value::Int(100)), |
| 150 | + "forward +25 then reverse -25 returns total to 100"); |
| 151 | + assert_eq!(vars.get("bonus"), Some(&Value::Int(25)), "bonus unchanged"); |
| 152 | +} |
| 153 | + |
| 154 | +// ── RV7: forward then reverse is left-inverse ──────────────────────────────── |
| 155 | + |
| 156 | +#[test] |
| 157 | +fn rv7_forward_then_reverse_is_left_inverse() { |
| 158 | + // `execute_forward` then `execute_inverse` on same block = identity. |
| 159 | + // This is distinct from `execute_and_reverse` (CNO): here we call |
| 160 | + // forward on one interpreter, then inverse on another starting from |
| 161 | + // the FORWARD state — proving they are mutual inverses. |
| 162 | + let block = ReverseBlock { |
| 163 | + body: vec![ |
| 164 | + ReversibleStmt::AddAssign("x".to_string(), DataExpr::Number(Number::Int(11))), |
| 165 | + ], |
| 166 | + }; |
| 167 | + |
| 168 | + let mut fwd = ReversibleInterpreter::new(); |
| 169 | + fwd.set("x".to_string(), Value::Int(5)); |
| 170 | + fwd.execute_forward(&block).expect("forward"); |
| 171 | + assert_eq!(fwd.get("x"), Some(&Value::Int(16)), "forward: x = 5 + 11 = 16"); |
| 172 | + |
| 173 | + // Now apply inverse starting from the forward state |
| 174 | + let mut inv = ReversibleInterpreter::with_state(fwd.get_state().clone()); |
| 175 | + inv.execute_inverse(&block).expect("inverse"); |
| 176 | + assert_eq!(inv.get("x"), Some(&Value::Int(5)), |
| 177 | + "inverse of forward restores original: 16 - 11 = 5"); |
| 178 | +} |
0 commit comments