type_eval 0.0.1-alpha

Type level evaluation and proof-carrying
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
122
123
124
125
126
127
128
129
130
131

use core::marker::PhantomData;

use crate::{
    num_vals::{U0, U1},
    op_types::{AddExp, LSB, MSB},
    prelude::B as BitString,
    val_types::{NumberVal, _0, _1},
    NumExpr, NumRet,
    _inners::{_BitLit, _BitStrLit},
};

impl<BS> NumExpr for MSB<BS>
where
    BS: NumExpr,
    MSBCount<U0, BS::Ret>: NumExpr,
{
    type Ret = NumRet<MSBCount<U0, BS::Ret>>;
}

#[allow(clippy::upper_case_acronyms)]
pub struct MSBCount<Idx: NumberVal, Bs: NumberVal> {
    _bits: PhantomData<Bs>,
    _idx: PhantomData<Idx>,
    // _mode: PhantomData<M>,
}

impl<Idx> NumExpr for MSBCount<Idx, U0>
where
    Idx: NumberVal,
{
    type Ret = Idx;
}
impl<Idx> NumExpr for MSBCount<Idx, U1>
where
    Idx: NumberVal,
{
    type Ret = Idx;
}
impl<Idx, BS, B> NumExpr for MSBCount<Idx, BitString<BS, B>>
where
    Idx: NumberVal,
    BS: NumberVal + _BitStrLit,
    B: _BitLit,
    AddExp<Idx, U1>: NumExpr,
    MSBCount<NumRet<AddExp<Idx, U1>>, BS>: NumExpr,
{
    type Ret = NumRet<MSBCount<NumRet<AddExp<Idx, U1>>, BS>>;
}

impl<BS> NumExpr for LSB<BS>
where
    BS: NumExpr,
    LSBCount<U0, BS::Ret>: NumExpr,
{
    type Ret = NumRet<LSBCount<U0, BS::Ret>>;
}

#[allow(clippy::upper_case_acronyms)]
pub struct LSBCount<Idx: NumberVal, Bs: NumberVal> {
    _bits: PhantomData<Bs>,
    _idx: PhantomData<Idx>,
    // _mode: PhantomData<M>,
}

impl<Idx> NumExpr for LSBCount<Idx, U0>
where
    Idx: NumberVal,
{
    type Ret = Idx;
}
impl<Idx> NumExpr for LSBCount<Idx, U1>
where
    Idx: NumberVal,
{
    type Ret = Idx;
}
impl<Idx, BS> NumExpr for LSBCount<Idx, BitString<BS, _0>>
where
    Idx: NumberVal,
    BS: NumberVal + _BitStrLit,
    AddExp<Idx, U1>: NumExpr,
    LSBCount<NumRet<AddExp<Idx, U1>>, BS>: NumExpr,
{
    type Ret = NumRet<LSBCount<NumRet<AddExp<Idx, U1>>, BS>>;
}
impl<Idx, BS> NumExpr for LSBCount<Idx, BitString<BS, _1>>
where
    Idx: NumberVal,
    BS: _BitStrLit,
{
    type Ret = Idx;
}
#[cfg(test)]
#[allow(clippy::used_underscore_items)]
mod test {
    use super::*;
    use crate::{
        num_vals::{U2, U3},
        op_types::LSB,
        test_res::*,
    };
    #[allow(non_upper_case_globals)]
    #[test]
    fn eval_msb() {
        const ___0: () = _b0::<MSB<_0>>();
        const ___1: () = _b0::<MSB<_1>>();
        const __U2: () = _b1::<MSB<U2>>();
        const __10: () = _b1::<MSB<BitString<_1, _0>>>();
        const __U3: () = _b1::<MSB<U3>>();
        const __11: () = _b1::<MSB<BitString<_1, _1>>>();
        const _100: () = _b2::<MSB<BitString<BitString<_1, _0>, _0>>>();
        const _101: () = _b2::<MSB<BitString<BitString<_1, _0>, _1>>>();
        const _110: () = _b2::<MSB<BitString<BitString<_1, _1>, _0>>>();
        const _111: () = _b2::<MSB<BitString<BitString<_1, _1>, _1>>>();
    }
    #[allow(non_upper_case_globals)]
    #[test]
    fn eval_lsb() {
        const ___0: () = _b0::<LSB<_0>>();
        const ___1: () = _b0::<LSB<_1>>();
        const __10: () = _b1::<LSB<BitString<_1, _0>>>();
        const __11: () = _b0::<LSB<BitString<_1, _1>>>();
        const _111: () = _b0::<LSB<BitString<BitString<_1, _1>, _1>>>();
        const _101: () = _b0::<LSB<BitString<BitString<_1, _0>, _1>>>();
        const _110: () = _b1::<LSB<BitString<BitString<_1, _1>, _0>>>();
        const _100: () = _b2::<LSB<BitString<BitString<_1, _0>, _0>>>();
        const _1000: () = _b1::<LSB<BitString<BitString<BitString<_1, _0>, _1>, _0>>>();
        const _1100: () = _b2::<LSB<BitString<BitString<BitString<_1, _1>, _0>, _0>>>();
        const _1010: () = _b1::<LSB<BitString<BitString<BitString<_1, _0>, _1>, _0>>>();
    }
}