1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
//! Property-based tests for the expression kernel.
//!
//! Invariants verified:
//! 1. Same data → same ExprId (intern is idempotent)
//! 2. Different data → different ExprId
//! 3. get(intern(data)) == data (round-trip)
#[cfg(test)]
mod tests {
use crate::kernel::{domain::Domain, expr::ExprData, pool::ExprPool};
use proptest::prelude::*;
// -----------------------------------------------------------------------
// Strategies
// -----------------------------------------------------------------------
fn domain_strategy() -> impl Strategy<Value = Domain> {
prop_oneof![
Just(Domain::Real),
Just(Domain::Complex),
Just(Domain::Integer),
Just(Domain::Positive),
Just(Domain::NonNegative),
Just(Domain::NonZero),
]
}
fn name_strategy() -> impl Strategy<Value = String> {
// Short alpha identifiers to keep expression trees readable in failures.
"[a-z]{1,4}".prop_map(|s| s)
}
/// Generates a flat ExprData (atoms only) to avoid needing a pool in the
/// strategy itself (compound nodes require valid ExprIds).
fn atom_data_strategy() -> impl Strategy<Value = ExprData> {
prop_oneof![
(name_strategy(), domain_strategy()).prop_map(|(n, d)| ExprData::Symbol {
name: n,
domain: d,
commutative: true,
}),
(i64::MIN..=i64::MAX).prop_map(|n| ExprData::Integer(crate::kernel::expr::BigInt(
rug::Integer::from(n)
))),
// Rationals: denom must be non-zero; use 1..1000 to avoid division
// A ratio that reduces to an integer is generated as the Integer
// node: the pool canonicalises a denominator-1 Rational to it, so
// `n/d` with `d | n` would not round-trip as a Rational.
(i32::MIN..=i32::MAX, 1_i32..=10000_i32).prop_map(|(n, d)| {
let r = rug::Rational::from((rug::Integer::from(n), rug::Integer::from(d)));
if *r.denom() == 1 {
ExprData::Integer(crate::kernel::expr::BigInt(r.numer().clone()))
} else {
ExprData::Rational(crate::kernel::expr::BigRat(r))
}
}),
]
}
// -----------------------------------------------------------------------
// Properties
// -----------------------------------------------------------------------
proptest! {
/// Same data interned twice yields the same ExprId.
#[test]
fn same_data_same_id(data in atom_data_strategy()) {
let p = ExprPool::new();
let id1 = p.intern(data.clone());
let id2 = p.intern(data);
prop_assert_eq!(id1, id2);
}
/// After interning, the pool size grows by 1 for a fresh entry.
#[test]
fn fresh_intern_grows_pool(data in atom_data_strategy()) {
let p = ExprPool::new();
let before = p.len();
p.intern(data.clone());
let after_first = p.len();
p.intern(data);
let after_second = p.len();
// first intern must add exactly one node
prop_assert_eq!(after_first, before + 1);
// second intern of the same data must not add a node
prop_assert_eq!(after_second, after_first);
}
/// Round-trip: get(intern(data)) == data, up to the canonicalisation
/// `intern` performs — a rational whose denominator is 1 is stored as
/// the integer (#424), so the strategy's `Rational(n/1)` reads back
/// as `Integer(n)`.
#[test]
fn round_trip(data in atom_data_strategy()) {
let p = ExprPool::new();
let id = p.intern(data.clone());
let expected = match &data {
ExprData::Rational(r) if *r.0.denom() == 1 => ExprData::Integer(
crate::kernel::expr::BigInt(r.0.numer().clone()),
),
_ => data,
};
prop_assert_eq!(p.get(id), expected);
}
/// Two distinct symbols (different names or domains) produce distinct ids.
#[test]
fn distinct_symbols_distinct_ids(
name1 in name_strategy(),
name2 in name_strategy(),
d1 in domain_strategy(),
d2 in domain_strategy(),
) {
// Only assert when the two symbols are structurally different.
if name1 == name2 && d1 == d2 {
return Ok(());
}
let p = ExprPool::new();
let id1 = p.symbol(&name1, d1);
let id2 = p.symbol(&name2, d2);
if name1 != name2 || d1 != d2 {
prop_assert_ne!(id1, id2);
}
}
/// ExprId comparison mirrors structural equality for atom symbols.
#[test]
fn id_equality_mirrors_structural_equality(
n in name_strategy(),
d in domain_strategy(),
) {
let p = ExprPool::new();
let id_a = p.symbol(&n, d);
let id_b = p.symbol(&n, d);
// Same structure → same id → equal
prop_assert_eq!(id_a, id_b);
}
}
}