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
//! 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
(i32::MIN..=i32::MAX, 1_i32..=10000_i32).prop_map(|(n, d)| {
ExprData::Rational(crate::kernel::expr::BigRat(rug::Rational::from((
rug::Integer::from(n),
rug::Integer::from(d),
))))
}),
]
}
// -----------------------------------------------------------------------
// 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.
#[test]
fn round_trip(data in atom_data_strategy()) {
let p = ExprPool::new();
let id = p.intern(data.clone());
prop_assert_eq!(p.get(id), data);
}
/// 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);
}
}
}