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

use core::fmt::{self, Debug};

use typewit::TypeEq;

use crate::peano::{PeanoInt, PlusOne, Zero};


/// A type witness for whether `L` (a [peano integer](PeanoInt)) is [`Zero`] or [`PlusOne`]
/// 
/// # Example
/// 
/// Constructing a `&str` or `u8` depending on whether `L` is zero
/// 
/// ```rust
/// use nlist::{PeanoInt, PeanoWit, Peano, peano};
/// use nlist::typewit::{CallFn, TypeEq};
/// 
/// assert_eq!(make::<Peano!(0)>(), "hello");
/// assert_eq!(make::<Peano!(1)>(), 0);
/// assert_eq!(make::<Peano!(2)>(), 1);
/// assert_eq!(make::<Peano!(3)>(), 2);
/// 
/// 
/// // Function which returns different types depending on the value of `L`
/// // 
/// // If L == 0, this returns a &'static str
/// // If L > 0, this returns a usize
/// // 
/// // The `-> CallFn<StrOrUsize, L>` return type calls the `StrOrUsize` type-level function 
/// // with `L` as an argument.
/// const fn make<L: PeanoInt>() -> CallFn<StrOrUsize, L> {
///     match L::PEANO_WIT {
///         // len_te is a proof that `L == PlusOne<L::SubOneSat>`
///         // len_te: TypeEq<L, PlusOne<L::SubOneSat>>
///         PeanoWit::PlusOne(len_te) => {
///             // te is a proof that `CallFn<StrOrUsize, L> == usize`
///             let te: TypeEq<CallFn<StrOrUsize, L>, usize> = len_te.project::<StrOrUsize>();
///             te.to_left(<L::SubOneSat>::USIZE)
///         }
/// 
///         // len_te is a proof that `L == Zero`
///         // len_te: TypeEq<L, Zero>
///         PeanoWit::Zero(len_te) => {
///             // te is a proof that `CallFn<StrOrUsize, L> == &'static str`
///             let te: TypeEq<CallFn<StrOrUsize, L>, &'static str> = 
///                 len_te.project::<StrOrUsize>();
///
///             te.to_left("hello")
///         }
///     }
/// }
/// 
/// // StrOrUsize is a type-level function (`typewit::TypeFn` implementor),
/// // which takes a PeanoInt parameter.
/// // 
/// // In pseudocode, this is what it does on the type level:
/// // fn StrOrUsize(L: PeanoInt) -> type {
/// //      if L == 0 { &'static str } else { usize }  
/// // }
/// type StrOrUsize = peano::IfZeroAltFn<&'static str, usize>;
/// 
/// ```
pub enum PeanoWit<L: PeanoInt> {
    /// Proof that `L == PlusOne<L::SubOneSat>`
    PlusOne(TypeEq<L, PlusOne<L::SubOneSat>>),
    /// Proof that `L == Zero`
    Zero(TypeEq<L, Zero>),
}



impl<L: PeanoInt> Debug for PeanoWit<L> {
    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
        fmt.debug_tuple("PeanoWit").field(&L::USIZE).finish()        
    }
}

impl<L: PeanoInt> Copy for PeanoWit<L> {}

impl<L: PeanoInt> Clone for PeanoWit<L> {
    fn clone(&self) -> Self {
        *self
    }
}