logicaffeine_kernel/dag/
nat.rs

1//! Lean's natural numbers on top of [`logicaffeine_base::BigInt`].
2//!
3//! `BigInt` supplies the arithmetic; this wrapper supplies `Nat`'s semantics — values never go
4//! negative, subtraction truncates at zero, and `n / 0 = 0`, `n % 0 = n` — so the kernel's
5//! literal extension computes exactly what Lean's `Nat` definitions compute.
6
7use logicaffeine_base::BigInt;
8
9#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)]
10pub struct Nat(BigInt);
11
12impl Nat {
13    pub fn zero() -> Nat {
14        Nat(BigInt::zero())
15    }
16
17    pub fn from_u64(v: u64) -> Nat {
18        Nat(BigInt::from_u64(v))
19    }
20
21    /// A non-negative integer as a natural number (a LOGOS `Nat` literal holds one).
22    pub fn from_bigint(v: &BigInt) -> Nat {
23        debug_assert!(!v.is_negative(), "a natural number is not negative");
24        Nat(v.clone())
25    }
26
27    pub fn to_bigint(&self) -> BigInt {
28        self.0.clone()
29    }
30
31    pub fn parse_decimal(s: &str) -> Option<Nat> {
32        if s.is_empty() || !s.bytes().all(|b| b.is_ascii_digit()) {
33            return None;
34        }
35        BigInt::parse_decimal(s).map(Nat)
36    }
37
38    pub fn to_decimal(&self) -> String {
39        self.0.to_string()
40    }
41
42    pub fn is_zero(&self) -> bool {
43        self.0.is_zero()
44    }
45
46    pub fn to_u64(&self) -> Option<u64> {
47        self.0.to_u64()
48    }
49
50    pub fn succ(&self) -> Nat {
51        Nat(self.0.add(&BigInt::from_u64(1)))
52    }
53
54    pub fn add(&self, o: &Nat) -> Nat {
55        Nat(self.0.add(&o.0))
56    }
57
58    /// Truncated subtraction.
59    pub fn sub(&self, o: &Nat) -> Nat {
60        if self.0 <= o.0 {
61            Nat::zero()
62        } else {
63            Nat(self.0.sub(&o.0))
64        }
65    }
66
67    pub fn mul(&self, o: &Nat) -> Nat {
68        Nat(self.0.mul(&o.0))
69    }
70
71    pub fn div(&self, o: &Nat) -> Nat {
72        match self.0.div_rem(&o.0) {
73            Some((q, _)) => Nat(q),
74            None => Nat::zero(),
75        }
76    }
77
78    pub fn rem(&self, o: &Nat) -> Nat {
79        match self.0.div_rem(&o.0) {
80            Some((_, r)) => Nat(r),
81            None => self.clone(),
82        }
83    }
84
85    pub fn gcd(&self, o: &Nat) -> Nat {
86        Nat(self.0.gcd(&o.0))
87    }
88
89    /// `self ^ exp`; the caller bounds `exp` (Lean's kernel reduces `Nat.pow` only for
90    /// exponents up to 2²⁴).
91    pub fn pow(&self, exp: u32) -> Nat {
92        Nat(self.0.pow(exp))
93    }
94
95    pub fn land(&self, o: &Nat) -> Nat {
96        Nat(self
97            .0
98            .bitand_natural(&o.0)
99            .expect("naturals are non-negative"))
100    }
101
102    pub fn lor(&self, o: &Nat) -> Nat {
103        Nat(self
104            .0
105            .bitor_natural(&o.0)
106            .expect("naturals are non-negative"))
107    }
108
109    pub fn xor(&self, o: &Nat) -> Nat {
110        Nat(self
111            .0
112            .bitxor_natural(&o.0)
113            .expect("naturals are non-negative"))
114    }
115
116    pub fn shl(&self, bits: u64) -> Nat {
117        Nat(self.0.shl_bits(bits))
118    }
119
120    pub fn shr(&self, bits: u64) -> Nat {
121        Nat(self.0.shr_bits(bits).expect("naturals are non-negative"))
122    }
123
124    pub fn bit_len(&self) -> u64 {
125        self.0.bit_len()
126    }
127}
128
129#[cfg(test)]
130#[path = "../../../logicaffeine_tests/unit/logicaffeine_kernel/dag/nat/tests.rs"]
131mod tests;
logicaffeine_kernel/dag/nat.rs

logicaffeine_kernel/dag/
nat.rs
