oxilean_std/prod/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::functions::*;
6/// CurriedFn represents a curried function A → B → C.
7#[allow(dead_code)]
8pub struct CurriedFn<A, B, C> {
9    f: Box<dyn Fn(A, B) -> C>,
10}
11impl<A: Clone + 'static, B: 'static, C: 'static> CurriedFn<A, B, C> {
12    #[allow(dead_code)]
13    pub fn new(f: impl Fn(A, B) -> C + 'static) -> Self {
14        Self { f: Box::new(f) }
15    }
16    #[allow(dead_code)]
17    pub fn apply(&self, a: A, b: B) -> C {
18        (self.f)(a, b)
19    }
20    #[allow(dead_code)]
21    pub fn curry_apply(&self, a: A) -> impl Fn(B) -> C + '_ {
22        move |b| (self.f)(a.clone(), b)
23    }
24    #[allow(dead_code)]
25    pub fn uncurried(&self, pair: (A, B)) -> C {
26        (self.f)(pair.0, pair.1)
27    }
28}
29/// A simple association map with ordered insertion semantics.
30///
31/// Keys are maintained in insertion order; operations are O(n).
32/// Suitable for small collections used in elaboration.
33#[derive(Debug, Clone, Default)]
34pub struct AssocMap<K: PartialEq, V> {
35    data: Vec<(K, V)>,
36}
37impl<K: PartialEq, V> AssocMap<K, V> {
38    /// Create an empty `AssocMap`.
39    pub fn new() -> Self {
40        Self { data: Vec::new() }
41    }
42    /// Create an `AssocMap` with initial capacity.
43    pub fn with_capacity(cap: usize) -> Self {
44        Self {
45            data: Vec::with_capacity(cap),
46        }
47    }
48    /// Insert or update a key-value pair.
49    pub fn insert(&mut self, key: K, value: V)
50    where
51        K: Clone,
52        V: Clone,
53    {
54        assoc_insert(&mut self.data, key, value);
55    }
56    /// Look up a key.
57    pub fn get(&self, key: &K) -> Option<&V> {
58        assoc_lookup(&self.data, key)
59    }
60    /// Remove a key, returning its value.
61    pub fn remove(&mut self, key: &K) -> Option<V> {
62        assoc_remove(&mut self.data, key)
63    }
64    /// Check whether a key is present.
65    pub fn contains_key(&self, key: &K) -> bool {
66        assoc_mem(&self.data, key)
67    }
68    /// Number of entries.
69    pub fn len(&self) -> usize {
70        self.data.len()
71    }
72    /// Returns `true` if empty.
73    pub fn is_empty(&self) -> bool {
74        self.data.is_empty()
75    }
76    /// Iterate over key-value pairs.
77    pub fn iter(&self) -> impl Iterator<Item = &(K, V)> {
78        self.data.iter()
79    }
80    /// Collect all keys.
81    pub fn keys(&self) -> Vec<&K> {
82        self.data.iter().map(|(k, _)| k).collect()
83    }
84    /// Collect all values.
85    pub fn values(&self) -> Vec<&V> {
86        self.data.iter().map(|(_, v)| v).collect()
87    }
88    /// Map all values in place.
89    pub fn map_values<W>(self, f: impl Fn(V) -> W) -> AssocMap<K, W> {
90        AssocMap {
91            data: self.data.into_iter().map(|(k, v)| (k, f(v))).collect(),
92        }
93    }
94    /// Remove all entries where the predicate on keys returns `false`.
95    pub fn retain_keys(&mut self, pred: impl Fn(&K) -> bool) {
96        self.data.retain(|(k, _)| pred(k));
97    }
98}
99/// A vector of sigma pairs, grouping witnesses and their proofs.
100#[derive(Debug, Clone, Default)]
101pub struct SigmaVec<A, B> {
102    items: Vec<Sigma<A, B>>,
103}
104impl<A, B> SigmaVec<A, B> {
105    /// Create an empty `SigmaVec`.
106    pub fn new() -> Self {
107        Self { items: Vec::new() }
108    }
109    /// Push a new witness-proof pair.
110    pub fn push(&mut self, witness: A, proof: B) {
111        self.items.push(Sigma::new(witness, proof));
112    }
113    /// Number of elements.
114    pub fn len(&self) -> usize {
115        self.items.len()
116    }
117    /// Returns `true` if empty.
118    pub fn is_empty(&self) -> bool {
119        self.items.is_empty()
120    }
121    /// Get a reference to the sigma pair at `index`.
122    pub fn get(&self, index: usize) -> Option<&Sigma<A, B>> {
123        self.items.get(index)
124    }
125    /// Iterate over all sigma pairs.
126    pub fn iter(&self) -> impl Iterator<Item = &Sigma<A, B>> {
127        self.items.iter()
128    }
129    /// Collect all witnesses.
130    pub fn witnesses(&self) -> Vec<&A> {
131        self.items.iter().map(|s| &s.fst).collect()
132    }
133    /// Collect all proofs.
134    pub fn proofs(&self) -> Vec<&B> {
135        self.items.iter().map(|s| &s.snd).collect()
136    }
137}
138/// A dependent pair (sigma type) `Σ (a : A), B(a)`.
139///
140/// At the Rust meta-level, `B` is represented as a plain type `B` rather
141/// than a type family, but conceptually this encodes dependent pairs.
142#[derive(Debug, Clone, PartialEq, Eq, Hash)]
143pub struct Sigma<A, B> {
144    /// The first component (the "witness").
145    pub fst: A,
146    /// The second component (the "proof" or dependent value).
147    pub snd: B,
148}
149impl<A, B> Sigma<A, B> {
150    /// Construct a sigma pair.
151    pub fn new(fst: A, snd: B) -> Self {
152        Self { fst, snd }
153    }
154    /// Destruct into components.
155    pub fn into_parts(self) -> (A, B) {
156        (self.fst, self.snd)
157    }
158    /// Map the proof component (second element) through `f`.
159    pub fn map_snd<C>(self, f: impl FnOnce(B) -> C) -> Sigma<A, C> {
160        Sigma::new(self.fst, f(self.snd))
161    }
162    /// Map the witness (first element) through `f`.
163    pub fn map_fst<C>(self, f: impl FnOnce(A) -> C) -> Sigma<C, B> {
164        Sigma::new(f(self.fst), self.snd)
165    }
166    /// Apply a function to both components.
167    pub fn elim<C>(self, f: impl FnOnce(A, B) -> C) -> C {
168        f(self.fst, self.snd)
169    }
170}
171/// A non-empty pair iterator: iterate over a pair's components.
172#[derive(Debug, Clone)]
173pub struct PairIter<T> {
174    pub(super) first: T,
175    pub(super) second: T,
176    pub(super) idx: usize,
177}
178impl<T: Clone> PairIter<T> {
179    /// Create an iterator over the two components of a `Pair`.
180    pub fn new(fst: T, snd: T) -> Self {
181        Self {
182            first: fst,
183            second: snd,
184            idx: 0,
185        }
186    }
187}
188/// LexPair represents a lexicographically ordered pair.
189#[allow(dead_code)]
190#[derive(Debug, Clone, PartialEq, Eq)]
191pub struct LexPair<A: Ord, B: Ord> {
192    pub fst: A,
193    pub snd: B,
194}
195impl<A: Ord, B: Ord> LexPair<A, B> {
196    #[allow(dead_code)]
197    pub fn new(fst: A, snd: B) -> Self {
198        Self { fst, snd }
199    }
200}
201/// A generic ordered triple.
202#[derive(Debug, Clone, PartialEq, Eq, Hash, Default)]
203pub struct Triple<A, B, C> {
204    /// First component.
205    pub fst: A,
206    /// Second component.
207    pub snd: B,
208    /// Third component.
209    pub thd: C,
210}
211impl<A, B, C> Triple<A, B, C> {
212    /// Construct a triple.
213    pub fn new(fst: A, snd: B, thd: C) -> Self {
214        Self { fst, snd, thd }
215    }
216    /// Construct from a Rust 3-tuple.
217    pub fn from_tuple((a, b, c): (A, B, C)) -> Self {
218        Self::new(a, b, c)
219    }
220    /// Convert to a Rust 3-tuple.
221    pub fn into_tuple(self) -> (A, B, C) {
222        (self.fst, self.snd, self.thd)
223    }
224    /// Map all three components.
225    pub fn trimap<D, E, F>(
226        self,
227        f: impl FnOnce(A) -> D,
228        g: impl FnOnce(B) -> E,
229        h: impl FnOnce(C) -> F,
230    ) -> Triple<D, E, F> {
231        Triple::new(f(self.fst), g(self.snd), h(self.thd))
232    }
233    /// Project the first pair.
234    pub fn fst_pair(self) -> Pair<A, B> {
235        Pair::new(self.fst, self.snd)
236    }
237    /// Project the last pair.
238    pub fn snd_pair(self) -> Pair<B, C> {
239        Pair::new(self.snd, self.thd)
240    }
241}
242/// ProdBimap applies two functions to the two components of a product simultaneously.
243#[allow(dead_code)]
244pub struct ProdBimap<A, B, C, D> {
245    pub f: Box<dyn Fn(A) -> C>,
246    pub g: Box<dyn Fn(B) -> D>,
247}
248impl<A: 'static, B: 'static, C: 'static, D: 'static> ProdBimap<A, B, C, D> {
249    #[allow(dead_code)]
250    pub fn new(f: impl Fn(A) -> C + 'static, g: impl Fn(B) -> D + 'static) -> Self {
251        Self {
252            f: Box::new(f),
253            g: Box::new(g),
254        }
255    }
256    #[allow(dead_code)]
257    pub fn apply(&self, pair: (A, B)) -> (C, D) {
258        ((self.f)(pair.0), (self.g)(pair.1))
259    }
260}
261/// ProdCone encodes the cone of a product diagram: morphisms into both projections.
262#[allow(dead_code)]
263pub struct ProdCone<A, B, Z> {
264    /// Projection to first component.
265    pub proj1: Box<dyn Fn(Z) -> A>,
266    /// Projection to second component.
267    pub proj2: Box<dyn Fn(Z) -> B>,
268}
269impl<A: 'static, B: 'static, Z: Clone + 'static> ProdCone<A, B, Z> {
270    #[allow(dead_code)]
271    pub fn new(p1: impl Fn(Z) -> A + 'static, p2: impl Fn(Z) -> B + 'static) -> Self {
272        Self {
273            proj1: Box::new(p1),
274            proj2: Box::new(p2),
275        }
276    }
277    /// Universal mediating morphism into the product.
278    #[allow(dead_code)]
279    pub fn mediate(&self, z: Z) -> (A, B) {
280        let z2 = z.clone();
281        ((self.proj1)(z), (self.proj2)(z2))
282    }
283}
284/// A generic ordered pair.
285///
286/// This is the Rust meta-level analogue of `Prod` in Lean 4.
287#[derive(Debug, Clone, PartialEq, Eq, Hash, Default)]
288pub struct Pair<A, B> {
289    /// First component.
290    pub fst: A,
291    /// Second component.
292    pub snd: B,
293}
294impl<A, B> Pair<A, B> {
295    /// Construct a new `Pair`.
296    pub fn new(fst: A, snd: B) -> Self {
297        Self { fst, snd }
298    }
299    /// Construct from a Rust tuple.
300    pub fn from_tuple((a, b): (A, B)) -> Self {
301        Self::new(a, b)
302    }
303    /// Convert to a Rust tuple.
304    pub fn into_tuple(self) -> (A, B) {
305        (self.fst, self.snd)
306    }
307    /// Map the first component.
308    pub fn map_fst<C>(self, f: impl FnOnce(A) -> C) -> Pair<C, B> {
309        Pair::new(f(self.fst), self.snd)
310    }
311    /// Map the second component.
312    pub fn map_snd<C>(self, f: impl FnOnce(B) -> C) -> Pair<A, C> {
313        Pair::new(self.fst, f(self.snd))
314    }
315    /// Map both components.
316    pub fn bimap<C, D>(self, f: impl FnOnce(A) -> C, g: impl FnOnce(B) -> D) -> Pair<C, D> {
317        Pair::new(f(self.fst), g(self.snd))
318    }
319    /// Swap the components.
320    pub fn swap(self) -> Pair<B, A> {
321        Pair::new(self.snd, self.fst)
322    }
323    /// Apply a function expecting two arguments.
324    pub fn uncurry<C>(self, f: impl FnOnce(A, B) -> C) -> C {
325        f(self.fst, self.snd)
326    }
327    /// Get references to both components.
328    pub fn as_refs(&self) -> (&A, &B) {
329        (&self.fst, &self.snd)
330    }
331}
332impl<T: Clone> Pair<T, T> {
333    /// Iterate over the two homogeneous components.
334    pub fn iter(&self) -> PairIter<T> {
335        PairIter::new(self.fst.clone(), self.snd.clone())
336    }
337}
338/// AssocTriple provides the associativity isomorphism for products.
339#[allow(dead_code)]
340pub struct AssocTriple<A, B, C> {
341    pub value: ((A, B), C),
342}
343impl<A, B, C> AssocTriple<A, B, C> {
344    #[allow(dead_code)]
345    pub fn new(value: ((A, B), C)) -> Self {
346        Self { value }
347    }
348    /// Associate right: ((a, b), c) → (a, (b, c))
349    #[allow(dead_code)]
350    pub fn assoc_right(self) -> (A, (B, C)) {
351        let ((a, b), c) = self.value;
352        (a, (b, c))
353    }
354    #[allow(dead_code)]
355    pub fn from_right(triple: (A, (B, C))) -> Self {
356        let (a, (b, c)) = triple;
357        Self { value: ((a, b), c) }
358    }
359}
oxilean_std/prod/types.rs

oxilean_std/prod/
types.rs
