Skip to main content

oxilean_std/ordering/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::functions::*;
6/// Represents a well-quasi-order (WQO) over a finite carrier.
7///
8/// An encoding of the WQO property: every infinite sequence has a good pair
9/// (indices i < j with carrier[i] ≤ carrier[j]).
10#[allow(dead_code)]
11pub struct WqoInstance {
12    /// The elements of the carrier set (finite approximation).
13    pub carrier: Vec<u64>,
14    /// The quasi-order as a boolean matrix (le_matrix[i][j] = carrier[i] ≤ carrier[j]).
15    pub le_matrix: Vec<Vec<bool>>,
16}
17#[allow(dead_code)]
18impl WqoInstance {
19    /// Create a WQO instance from a carrier and a comparator.
20    pub fn new(carrier: Vec<u64>, le: impl Fn(u64, u64) -> bool) -> Self {
21        let n = carrier.len();
22        let mut le_matrix = vec![vec![false; n]; n];
23        for i in 0..n {
24            for j in 0..n {
25                le_matrix[i][j] = le(carrier[i], carrier[j]);
26            }
27        }
28        Self { carrier, le_matrix }
29    }
30    /// Check if a sequence (given as indices into carrier) has a good pair.
31    pub fn has_good_pair(&self, seq: &[usize]) -> bool {
32        for i in 0..seq.len() {
33            for j in (i + 1)..seq.len() {
34                if self.le_matrix[seq[i]][seq[j]] {
35                    return true;
36                }
37            }
38        }
39        false
40    }
41    /// Return the first good pair in a sequence, if one exists.
42    pub fn find_good_pair(&self, seq: &[usize]) -> Option<(usize, usize)> {
43        for i in 0..seq.len() {
44            for j in (i + 1)..seq.len() {
45                if self.le_matrix[seq[i]][seq[j]] {
46                    return Some((i, j));
47                }
48            }
49        }
50        None
51    }
52    /// Number of elements in the carrier.
53    pub fn size(&self) -> usize {
54        self.carrier.len()
55    }
56    /// Check if the relation is reflexive.
57    pub fn is_reflexive(&self) -> bool {
58        (0..self.size()).all(|i| self.le_matrix[i][i])
59    }
60    /// Check if the relation is transitive.
61    pub fn is_transitive(&self) -> bool {
62        let n = self.size();
63        for i in 0..n {
64            for j in 0..n {
65                for k in 0..n {
66                    if self.le_matrix[i][j] && self.le_matrix[j][k] && !self.le_matrix[i][k] {
67                        return false;
68                    }
69                }
70            }
71        }
72        true
73    }
74}
75/// A finite linear order (totally ordered finite set).
76///
77/// Elements are represented as indices 0..n, with a permutation defining the order.
78#[allow(dead_code)]
79pub struct FiniteLinearOrder {
80    /// Number of elements.
81    pub size: usize,
82    /// The permutation defining the order: order[i] is the i-th smallest element.
83    pub order: Vec<usize>,
84}
85#[allow(dead_code)]
86impl FiniteLinearOrder {
87    /// Create the identity linear order on {0, ..., n-1}.
88    pub fn identity(n: usize) -> Self {
89        Self {
90            size: n,
91            order: (0..n).collect(),
92        }
93    }
94    /// Create a linear order from a permutation.
95    pub fn from_permutation(perm: Vec<usize>) -> Option<Self> {
96        let n = perm.len();
97        let mut seen = vec![false; n];
98        for &x in &perm {
99            if x >= n || seen[x] {
100                return None;
101            }
102            seen[x] = true;
103        }
104        Some(Self {
105            size: n,
106            order: perm,
107        })
108    }
109    /// Compare two elements a, b (by their rank in the order).
110    pub fn compare(&self, a: usize, b: usize) -> Ordering {
111        let rank_a = self.order.iter().position(|&x| x == a);
112        let rank_b = self.order.iter().position(|&x| x == b);
113        match (rank_a, rank_b) {
114            (Some(ra), Some(rb)) => Ordering::from_std(ra.cmp(&rb)),
115            _ => Ordering::Equal,
116        }
117    }
118    /// Get the rank (0-indexed position) of an element.
119    pub fn rank(&self, a: usize) -> Option<usize> {
120        self.order.iter().position(|&x| x == a)
121    }
122    /// Get the minimum element.
123    pub fn min_elem(&self) -> Option<usize> {
124        self.order.first().copied()
125    }
126    /// Get the maximum element.
127    pub fn max_elem(&self) -> Option<usize> {
128        self.order.last().copied()
129    }
130    /// Check if the order is well-founded (always true for finite sets).
131    pub fn is_well_founded(&self) -> bool {
132        true
133    }
134    /// Reverse the order.
135    pub fn reverse_order(&self) -> FiniteLinearOrder {
136        let mut rev = self.order.clone();
137        rev.reverse();
138        FiniteLinearOrder {
139            size: self.size,
140            order: rev,
141        }
142    }
143}
144/// A builder that accumulates multiple comparison results and returns the
145/// first non-`Equal` one.
146#[derive(Clone, Debug)]
147pub struct OrderingBuilder {
148    result: Ordering,
149}
150impl OrderingBuilder {
151    /// Begin a new builder (starts as `Equal`).
152    pub fn new() -> Self {
153        Self {
154            result: Ordering::Equal,
155        }
156    }
157    /// Add another comparison step.
158    pub fn then(mut self, next: Ordering) -> Self {
159        self.result = self.result.then(next);
160        self
161    }
162    /// Add a lazily-evaluated step.
163    pub fn then_with<F: FnOnce() -> Ordering>(mut self, f: F) -> Self {
164        self.result = self.result.then_with(f);
165        self
166    }
167    /// Add a field comparison.
168    pub fn field<T: std::cmp::Ord>(self, a: &T, b: &T) -> Self {
169        self.then(cmp(a, b))
170    }
171    /// Finalise and return the accumulated ordering.
172    pub fn build(self) -> Ordering {
173        self.result
174    }
175}
176/// A range structure for ordered types.
177///
178/// Represents the interval [lo, hi] in an ordered set, supporting
179/// membership tests, containment, and iteration for integer ranges.
180#[allow(dead_code)]
181pub struct OrderedRange<T: std::cmp::Ord + Clone> {
182    /// Lower bound (inclusive).
183    pub lo: T,
184    /// Upper bound (inclusive).
185    pub hi: T,
186}
187#[allow(dead_code)]
188impl<T: std::cmp::Ord + Clone> OrderedRange<T> {
189    /// Create a new range [lo, hi]. Panics if lo > hi.
190    pub fn new(lo: T, hi: T) -> Self {
191        assert!(lo <= hi, "lower bound must not exceed upper bound");
192        Self { lo, hi }
193    }
194    /// Check if a value is within the range.
195    pub fn contains(&self, x: &T) -> bool {
196        x >= &self.lo && x <= &self.hi
197    }
198    /// Check if another range is fully contained within this range.
199    pub fn contains_range(&self, other: &OrderedRange<T>) -> bool {
200        other.lo >= self.lo && other.hi <= self.hi
201    }
202    /// Check if two ranges overlap.
203    pub fn overlaps(&self, other: &OrderedRange<T>) -> bool {
204        self.lo <= other.hi && other.lo <= self.hi
205    }
206    /// Return the lower bound.
207    pub fn lower(&self) -> &T {
208        &self.lo
209    }
210    /// Return the upper bound.
211    pub fn upper(&self) -> &T {
212        &self.hi
213    }
214}
215/// Represents an ordinal in Cantor Normal Form.
216///
217/// An ordinal in CNF is written as ω^a₁·c₁ + ω^a₂·c₂ + ... + ω^aₙ·cₙ
218/// where a₁ > a₂ > ... > aₙ and cᵢ > 0 are natural number coefficients.
219/// We represent exponents as u64 for simplicity.
220#[allow(dead_code)]
221pub struct OrdinalCnf {
222    /// Terms in the CNF representation: (exponent, coefficient).
223    /// Stored in decreasing order of exponent.
224    pub terms: Vec<(u64, u64)>,
225}
226#[allow(dead_code)]
227impl OrdinalCnf {
228    /// The ordinal zero.
229    pub fn zero() -> Self {
230        Self { terms: vec![] }
231    }
232    /// A finite ordinal n (= ω^0 · n for n > 0).
233    pub fn finite(n: u64) -> Self {
234        if n == 0 {
235            Self::zero()
236        } else {
237            Self {
238                terms: vec![(0, n)],
239            }
240        }
241    }
242    /// The ordinal ω (= ω^1 · 1).
243    pub fn omega() -> Self {
244        Self {
245            terms: vec![(1, 1)],
246        }
247    }
248    /// The ordinal ω^k.
249    pub fn omega_pow(k: u64) -> Self {
250        Self {
251            terms: vec![(k, 1)],
252        }
253    }
254    /// Check if this ordinal is zero.
255    pub fn is_zero(&self) -> bool {
256        self.terms.is_empty()
257    }
258    /// Check if this ordinal is finite.
259    pub fn is_finite(&self) -> bool {
260        self.terms.is_empty() || (self.terms.len() == 1 && self.terms[0].0 == 0)
261    }
262    /// Get the finite value, if this ordinal is finite.
263    pub fn as_finite(&self) -> Option<u64> {
264        if self.terms.is_empty() {
265            Some(0)
266        } else if self.terms.len() == 1 && self.terms[0].0 == 0 {
267            Some(self.terms[0].1)
268        } else {
269            None
270        }
271    }
272    /// Add two ordinals in CNF.
273    pub fn add(&self, other: &OrdinalCnf) -> OrdinalCnf {
274        if other.is_zero() {
275            return OrdinalCnf {
276                terms: self.terms.clone(),
277            };
278        }
279        if self.is_zero() {
280            return OrdinalCnf {
281                terms: other.terms.clone(),
282            };
283        }
284        let leading_exp = other.terms[0].0;
285        let mut result: Vec<(u64, u64)> = self
286            .terms
287            .iter()
288            .filter(|(e, _)| *e > leading_exp)
289            .cloned()
290            .collect();
291        result.extend_from_slice(&other.terms);
292        OrdinalCnf { terms: result }
293    }
294    /// Compare two ordinals in CNF lexicographically.
295    pub fn ord_cmp(&self, other: &OrdinalCnf) -> Ordering {
296        for (a, b) in self.terms.iter().zip(other.terms.iter()) {
297            match a.0.cmp(&b.0) {
298                std::cmp::Ordering::Greater => return Ordering::Greater,
299                std::cmp::Ordering::Less => return Ordering::Less,
300                std::cmp::Ordering::Equal => match a.1.cmp(&b.1) {
301                    std::cmp::Ordering::Greater => return Ordering::Greater,
302                    std::cmp::Ordering::Less => return Ordering::Less,
303                    std::cmp::Ordering::Equal => {}
304                },
305            }
306        }
307        Ordering::from_std(self.terms.len().cmp(&other.terms.len()))
308    }
309    /// Number of terms in the CNF.
310    pub fn num_terms(&self) -> usize {
311        self.terms.len()
312    }
313}
314/// A simple table that maps keys to values, sorted by a comparison function.
315///
316/// This is a lightweight alternative to `BTreeMap` using `Ordering`.
317#[allow(dead_code)]
318pub struct OrderedTable<K: std::cmp::Ord, V> {
319    entries: Vec<(K, V)>,
320}
321#[allow(dead_code)]
322impl<K: std::cmp::Ord, V> OrderedTable<K, V> {
323    /// Create an empty table.
324    pub fn new() -> Self {
325        Self {
326            entries: Vec::new(),
327        }
328    }
329    /// Insert a key-value pair.
330    pub fn insert(&mut self, key: K, value: V) {
331        let pos = self.entries.partition_point(|(k, _)| *k < key);
332        self.entries.insert(pos, (key, value));
333    }
334    /// Look up a key.
335    pub fn get(&self, key: &K) -> Option<&V> {
336        let pos = self.entries.partition_point(|(k, _)| k < key);
337        if pos < self.entries.len() && self.entries[pos].0 == *key {
338            Some(&self.entries[pos].1)
339        } else {
340            None
341        }
342    }
343    /// Remove a key, returning its value.
344    pub fn remove(&mut self, key: &K) -> Option<V> {
345        let pos = self.entries.partition_point(|(k, _)| k < key);
346        if pos < self.entries.len() && self.entries[pos].0 == *key {
347            Some(self.entries.remove(pos).1)
348        } else {
349            None
350        }
351    }
352    /// Number of entries.
353    pub fn len(&self) -> usize {
354        self.entries.len()
355    }
356    /// Whether the table is empty.
357    pub fn is_empty(&self) -> bool {
358        self.entries.is_empty()
359    }
360    /// Iterate over entries in sorted order.
361    pub fn iter(&self) -> impl Iterator<Item = (&K, &V)> {
362        self.entries.iter().map(|(k, v)| (k, v))
363    }
364    /// Check if a key exists.
365    pub fn contains_key(&self, key: &K) -> bool {
366        self.get(key).is_some()
367    }
368    /// Return all keys in sorted order.
369    pub fn keys(&self) -> Vec<&K> {
370        self.entries.iter().map(|(k, _)| k).collect()
371    }
372    /// Return all values in key-sorted order.
373    pub fn values(&self) -> Vec<&V> {
374        self.entries.iter().map(|(_, v)| v).collect()
375    }
376}
377/// A Lean 4-style ordering value (mirrors `Ordering` in the kernel env).
378#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
379pub enum Ordering {
380    /// First < second.
381    Less,
382    /// First == second.
383    Equal,
384    /// First > second.
385    Greater,
386}
387impl Ordering {
388    /// Reverse the ordering: `Less ↔ Greater`.
389    pub fn reverse(self) -> Self {
390        match self {
391            Ordering::Less => Ordering::Greater,
392            Ordering::Equal => Ordering::Equal,
393            Ordering::Greater => Ordering::Less,
394        }
395    }
396    /// Lexicographic combinator: if `self == Equal`, return `other`.
397    pub fn then(self, other: Ordering) -> Self {
398        match self {
399            Ordering::Equal => other,
400            _ => self,
401        }
402    }
403    /// `then` with a lazily-evaluated second comparison.
404    pub fn then_with<F: FnOnce() -> Ordering>(self, f: F) -> Self {
405        match self {
406            Ordering::Equal => f(),
407            _ => self,
408        }
409    }
410    /// `true` if `Less`.
411    pub fn is_lt(self) -> bool {
412        self == Ordering::Less
413    }
414    /// `true` if `Equal`.
415    pub fn is_eq(self) -> bool {
416        self == Ordering::Equal
417    }
418    /// `true` if `Greater`.
419    pub fn is_gt(self) -> bool {
420        self == Ordering::Greater
421    }
422    /// `true` if `Less` or `Equal`.
423    pub fn is_le(self) -> bool {
424        self != Ordering::Greater
425    }
426    /// `true` if `Greater` or `Equal`.
427    pub fn is_ge(self) -> bool {
428        self != Ordering::Less
429    }
430    /// Convert to a signed integer: `-1`, `0`, or `1`.
431    pub fn to_signum(self) -> i32 {
432        match self {
433            Ordering::Less => -1,
434            Ordering::Equal => 0,
435            Ordering::Greater => 1,
436        }
437    }
438    /// Construct from a signum integer.
439    ///
440    /// Negative → `Less`, zero → `Equal`, positive → `Greater`.
441    pub fn from_signum(n: i32) -> Self {
442        match n.cmp(&0) {
443            std::cmp::Ordering::Less => Ordering::Less,
444            std::cmp::Ordering::Equal => Ordering::Equal,
445            std::cmp::Ordering::Greater => Ordering::Greater,
446        }
447    }
448    /// Convert from `std::cmp::Ordering`.
449    pub fn from_std(o: std::cmp::Ordering) -> Self {
450        match o {
451            std::cmp::Ordering::Less => Ordering::Less,
452            std::cmp::Ordering::Equal => Ordering::Equal,
453            std::cmp::Ordering::Greater => Ordering::Greater,
454        }
455    }
456    /// Convert to `std::cmp::Ordering`.
457    pub fn to_std(self) -> std::cmp::Ordering {
458        match self {
459            Ordering::Less => std::cmp::Ordering::Less,
460            Ordering::Equal => std::cmp::Ordering::Equal,
461            Ordering::Greater => std::cmp::Ordering::Greater,
462        }
463    }
464}
465/// A Dedekind cut representation over the rationals (using integer pairs p/q).
466///
467/// A Dedekind cut (L, R) partitions the rationals into a lower set L and
468/// upper set R. We represent it by the cut value as a rational number p/q.
469#[allow(dead_code)]
470pub struct DedekindCutQ {
471    /// Numerator of the cut value.
472    pub numerator: i64,
473    /// Denominator of the cut value (always positive).
474    pub denominator: u64,
475}
476#[allow(dead_code)]
477impl DedekindCutQ {
478    /// Create a Dedekind cut at p/q (q > 0).
479    pub fn new(p: i64, q: u64) -> Self {
480        assert!(q > 0, "denominator must be positive");
481        Self {
482            numerator: p,
483            denominator: q,
484        }
485    }
486    /// Check if a rational number r/s is in the lower set.
487    pub fn in_lower(&self, r: i64, s: u64) -> bool {
488        r * (self.denominator as i64) < self.numerator * (s as i64)
489    }
490    /// Check if a rational number r/s is in the upper set.
491    pub fn in_upper(&self, r: i64, s: u64) -> bool {
492        r * (self.denominator as i64) > self.numerator * (s as i64)
493    }
494    /// Approximate value as f64.
495    pub fn as_f64(&self) -> f64 {
496        self.numerator as f64 / self.denominator as f64
497    }
498    /// Compare two cuts.
499    pub fn cut_cmp(&self, other: &DedekindCutQ) -> Ordering {
500        let lhs = self.numerator * (other.denominator as i64);
501        let rhs = other.numerator * (self.denominator as i64);
502        Ordering::from_std(lhs.cmp(&rhs))
503    }
504    /// Return a cut strictly between self and other.
505    pub fn mediant(&self, other: &DedekindCutQ) -> DedekindCutQ {
506        DedekindCutQ::new(
507            self.numerator + other.numerator,
508            self.denominator + other.denominator,
509        )
510    }
511}
512/// A partial order on a finite set, stored as an adjacency matrix.
513#[allow(dead_code)]
514pub struct FinitePartialOrder {
515    /// Number of elements.
516    pub size: usize,
517    /// The order relation as a boolean matrix: le[i][j] = (i ≤ j).
518    pub le: Vec<Vec<bool>>,
519}
520#[allow(dead_code)]
521impl FinitePartialOrder {
522    /// Create the discrete partial order (only x ≤ x for all x).
523    pub fn discrete(n: usize) -> Self {
524        let mut le = vec![vec![false; n]; n];
525        for i in 0..n {
526            le[i][i] = true;
527        }
528        Self { size: n, le }
529    }
530    /// Check reflexivity: x ≤ x for all x.
531    pub fn is_reflexive(&self) -> bool {
532        (0..self.size).all(|i| self.le[i][i])
533    }
534    /// Check antisymmetry: x ≤ y and y ≤ x implies x = y.
535    pub fn is_antisymmetric(&self) -> bool {
536        for i in 0..self.size {
537            for j in 0..self.size {
538                if i != j && self.le[i][j] && self.le[j][i] {
539                    return false;
540                }
541            }
542        }
543        true
544    }
545    /// Check transitivity: x ≤ y and y ≤ z implies x ≤ z.
546    pub fn is_transitive(&self) -> bool {
547        let n = self.size;
548        for i in 0..n {
549            for j in 0..n {
550                for k in 0..n {
551                    if self.le[i][j] && self.le[j][k] && !self.le[i][k] {
552                        return false;
553                    }
554                }
555            }
556        }
557        true
558    }
559    /// Check if this is a valid partial order.
560    pub fn is_valid(&self) -> bool {
561        self.is_reflexive() && self.is_antisymmetric() && self.is_transitive()
562    }
563    /// Check totality: x ≤ y or y ≤ x for all x, y.
564    pub fn is_total(&self) -> bool {
565        for i in 0..self.size {
566            for j in 0..self.size {
567                if !self.le[i][j] && !self.le[j][i] {
568                    return false;
569                }
570            }
571        }
572        true
573    }
574    /// Find all maximal elements (elements with nothing strictly above them).
575    pub fn maximal_elements(&self) -> Vec<usize> {
576        (0..self.size)
577            .filter(|&i| (0..self.size).all(|j| !self.le[i][j] || i == j || self.le[j][i]))
578            .collect()
579    }
580    /// Compute the transitive closure using Floyd-Warshall.
581    pub fn transitive_closure(&self) -> FinitePartialOrder {
582        let n = self.size;
583        let mut le = self.le.clone();
584        for k in 0..n {
585            for i in 0..n {
586                for j in 0..n {
587                    if le[i][k] && le[k][j] {
588                        le[i][j] = true;
589                    }
590                }
591            }
592        }
593        FinitePartialOrder { size: n, le }
594    }
595}