nlist 0.1.1

inline-allocated list with statically tracked length
Documentation 
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

//! Contains proofs of arithmetic properties of [`PeanoInt`]s
//! 
//! These properties are useful in generic contexts, where the compiler does no
//! reasoning WRT the arithmetic properties of [`PeanoInt`]s. 
//! 
//! # Alternative
//! 
//! An easier approach is to use [`peano::eq`]`::<foo, bar>().unwrap_eq()`,
//! but this is prone to causing panics if `foo` or `bar` might change to become unequal.
//! (the proof approach is completely panic-free, though)
//! 
//! # Example
//! 
//! Defining a version of [`NList::flatten`](crate::NList::flatten) function that returns 
//! ```rust
//! # use nlist::{NList, Peano, peano}; 
//! # type T = ();
//! # type LOuter = Peano!(0);
//! # type LInner = Peano!(0);
//! # let _: 
//! NList<T, peano::Mul<LInner, LOuter>>
//! # ;
//! ```
//! instead of
//! ```rust
//! # use nlist::{NList, Peano, peano}; 
//! # type T = ();
//! # type LOuter = Peano!(0);
//! # type LInner = Peano!(0);
//! # let _: 
//! NList<T, peano::Mul<LOuter, LInner>>
//! # ;
//! ```
//! 
//! ```rust
//! use nlist::{NList, NList2D, PeanoInt, nlist, peano};
//! 
//! 
//! const fn flatten_comm<T, LOuter, LInner>(
//!     list: NList2D<T, LOuter, LInner>,
//! ) -> NList<T, peano::Mul<LInner, LOuter>>
//! where   
//!     LOuter: PeanoInt,
//!     LInner: PeanoInt,
//! {
//!     let flat: NList<T, peano::Mul<LOuter, LInner>> = list.flatten();
//!     
//!     flat.coerce_len(peano::proofs::commutative_mul::<LOuter, LInner>())
//! }
//! 
//! ```
//! [`peano::eq`]: crate::peano::eq

use super::*;


/// Proof that `L + R` == `R + L`
pub const fn commutative_add<L, R>() -> TypeEq<Add<L, R>, Add<R, L>>
where
    L: PeanoInt,
    R: PeanoInt,
{
    // axiom
    const {
        super::eq::<Add<L, R>, Add<R, L>>().unwrap_eq()        
    }
}

/// Proof that `L * R` == `R * L`
pub const fn commutative_mul<L, R>() -> TypeEq<Mul<L, R>, Mul<R, L>>
where
    L: PeanoInt,
    R: PeanoInt,
{
    // axiom
    const {
        super::eq::<Mul<L, R>, Mul<R, L>>().unwrap_eq()        
    }
}

/// Proof that `L + 0` == `L`
pub const fn add_identity<L>() -> TypeEq<Add<L, Zero>, L>
where
    L: PeanoInt,
{
    // axiom
    const {
        super::eq::<Add<L, Zero>, L>().unwrap_eq()        
    }
}

/// Proof that `SubSat<L, 0>` == `L`
pub const fn sub_identity<L>() -> TypeEq<SubSat<L, Zero>, L>
where
    L: PeanoInt,
{
    // axiom
    const {
        super::eq::<SubSat<L, Zero>, L>().unwrap_eq()        
    }
}

/// Proof that, if A < C, then`SubSat<A, B> < C`
/// 
pub const fn compose_sub_lt<A, B, C>(
    _a_is_lt_b: TypeEq<IsLt<A, C>, Bool<true>>
) -> TypeEq<IsLt<SubSat<A, B>, C>, Bool<true>>
where
    A: PeanoInt,
    B: PeanoInt,
    C: PeanoInt,
{
    // not in a const block because if this function is monomorphized
    // in a context where A >= C, it could cause a compilation error.
    match Boolean::BOOL_WIT {
        BoolWitG::True(x) => x,
        BoolWitG::False(_) => panic!("axiom"),
    }
}