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

use crate::{
    _inners::{_Base, _BitLit, _BitStrLit},
    num_vals::{U0, U1},
    op_types::{AddExp, MulExp},
    val_types::{NumberVal, B, _0, _1},
    NumExpr, NumRet,
};

impl<L, R> NumExpr for MulExp<L, R>
where
    L: NumExpr,
    R: NumExpr,
    MulExp<L::Ret, R::Ret, _Base>: NumExpr,
{
    type Ret = NumRet<MulExp<L::Ret, R::Ret, _Base>>;
}
// -------------
// Hard codod base cases.
// Past attempts to coallesce these impls resulted in overlapping-impl headaches
// -------------

impl NumExpr for MulExp<U0, U1, _Base> {
    type Ret = U0;
}
impl NumExpr for MulExp<U1, U0, _Base> {
    type Ret = U0;
}
impl NumExpr for MulExp<U0, U0, _Base> {
    type Ret = U0;
}
impl NumExpr for MulExp<U1, U1, _Base> {
    type Ret = U1;
}
impl<Bs, Bt> NumExpr for MulExp<U1, B<Bs, Bt>, _Base>
where
    Bs: NumExpr,
    Bt: _BitLit,
    B<Bs, Bt>: NumberVal,
{
    type Ret = B<Bs, Bt>;
}

// (LB, U1) * Val == ((LB * Val), U0) + Val
impl<LB, Val> NumExpr for MulExp<B<LB, _1>, Val, _Base>
where
    LB: _BitStrLit,
    MulExp<LB, Val>: NumExpr,
    AddExp<B<NumRet<MulExp<LB, Val>>, _0>, Val>: NumExpr,
{
    type Ret = NumRet<AddExp<B<NumRet<MulExp<LB, Val>>, _0>, Val>>;
}
// (LB, U0) * Val == ((LB * Val), U0)
impl<LB, Val> NumExpr for MulExp<B<LB, _0>, Val, _Base>
where
    LB: _BitStrLit,
    MulExp<LB, Val>: NumExpr,
    NumRet<MulExp<LB, Val>>: _BitStrLit,
{
    type Ret = B<NumRet<MulExp<LB, Val>>, _0>;
}

#[cfg(test)]
mod test {
    use super::*;
    use crate::{
        num_vals::{U1, U2, U3, U4, U5, U6, U7, U8},
        test_res::*,
    };
    #[allow(clippy::used_underscore_items)]
    #[allow(non_upper_case_globals)]
    #[test]
    fn eval_mul() {
        const _0_MUL_0: () = _b0::<MulExp<U0, U0>>();
        const _0_MUL_1: () = _b0::<MulExp<U0, U1>>();
        const _1_MUL_0: () = _b0::<MulExp<U1, U0>>();
        const _2_MUL_1: () = _b2::<MulExp<U2, U1>>();
        const _1_MUL_2: () = _b2::<MulExp<U1, U2>>();
        const _3_MUL_1: () = _b3::<MulExp<U3, U1>>();
        const _1_MUL_3: () = _b3::<MulExp<U1, U3>>();
        const _2_MUL_2: () = _b4::<MulExp<U2, U2>>();
        const _4_MUL_1: () = _b4::<MulExp<U4, U1>>();
        const _5_MUL_1: () = _b5::<MulExp<U5, U1>>();
        const _6_MUL_1: () = _b6::<MulExp<U6, U1>>();
        const _7_MUL_1: () = _b7::<MulExp<U7, U1>>();
        const _8_MUL_1: () = _b8::<MulExp<U8, U1>>();
        const _3_MUL_3: () = _b9::<MulExp<U3, U3>>();

        const _2_MUL_2__MUL_2: () = _b8::<MulExp<MulExp<U2, U2>, U2>>();
        const _2_MUL__2_MUL_2: () = _b8::<MulExp<U2, MulExp<U2, U2>>>();
    }
}