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
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153

use crate::{
    num_vals::{U0, U1},
    op_types::SubExp,
    val_types::{NumberVal, B, _0, _1},
    NumExpr, NumRet,
};
use core::ops::Sub as StSub;

impl<L, R> NumExpr for SubExp<L, R>
where
    L: NumExpr,
    R: NumExpr,
    L::Ret: StSub<R::Ret>,
    SubOut<L::Ret, R::Ret>: NumExpr,
    NumRet<SubOut<L::Ret, R::Ret>>: NumberVal,
{
    type Ret = NumRet<SubOut<L::Ret, R::Ret>>;
}

type SubOut<L, R> = <L as StSub<R>>::Output;

// ----
//  Most basic of subtraction evaluations
// ----
impl StSub<U0> for U0 {
    type Output = U0;

    fn sub(self, _rhs: U0) -> Self::Output {
        unimplemented!("type eval only")
    }
}
impl StSub<U0> for U1 {
    type Output = U1;
    fn sub(self, _rhs: U0) -> Self::Output {
        unimplemented!("type eval only")
    }
}
impl StSub<U1> for U1 {
    type Output = U0;
    fn sub(self, _rhs: U1) -> Self::Output {
        unimplemented!("type eval only")
    }
}
impl<LBs, LB> StSub<U0> for B<LBs, LB> {
    type Output = B<LBs, LB>;
    fn sub(self, _rhs: U0) -> Self::Output {
        unimplemented!("type eval only")
    }
}
// Commented out as we are not yet handling negatives
// impl Expr for Sub<_0, U1, Base> {
//     type Ret = U1;
// }

impl<Bs> StSub<_1> for B<Bs, _1> {
    type Output = B<Bs, _0>;
    fn sub(self, _rhs: U1) -> Self::Output {
        unimplemented!("type eval only")
    }
}

impl<Bs> StSub<_1> for B<Bs, _0>
where
    Bs: StSub<_1>,
    B<SubOut<Bs, _1>, _1>: NumExpr,
{
    type Output = NumRet<B<SubOut<Bs, _1>, _1>>;
    fn sub(self, _rhs: U1) -> Self::Output {
        unimplemented!("type eval only")
    }
}
/// (L)0 - (R)0 = (L - R)0
impl<LB, RB> StSub<B<RB, _0>> for B<LB, _0>
where
    // `L - R` is valid
    LB: StSub<RB>,
    // `(L - R)0` is valid as a bitstring
    B<SubOut<LB, RB>, _0>: NumExpr,
{
    type Output = NumRet<B<SubOut<LB, RB>, _0>>;
    fn sub(self, _rhs: B<RB, _0>) -> Self::Output {
        unimplemented!("type eval only")
    }
}
/// (L)0 - (R)1 = ((L - R) - 1)1
impl<LB, RB> StSub<B<RB, _1>> for B<LB, _0>
where
    // `L - R` is valid
    LB: StSub<RB>,
    // `(L - R) - 1` is a valid expression
    SubOut<LB, RB>: StSub<_1>,
    // `(L - R) - 1` Is a valid bit-string literal so can be appended with a bit to make a valid
    // number
    B<SubOut<SubOut<LB, RB>, _1>, _1>: NumExpr,
{
    type Output = NumRet<B<SubOut<SubOut<LB, RB>, _1>, _1>>;
    fn sub(self, _rhs: B<RB, _1>) -> Self::Output {
        unimplemented!("type eval only")
    }
}
/// (L)1 - (R)0 = (L - R)1
impl<LB, RB> StSub<B<RB, _0>> for B<LB, _1>
where
    // `L - R` is valid
    LB: StSub<RB>,
    B<SubOut<LB, RB>, _1>: NumExpr,
    // `(L - R)1` is valid as a bitstring
    // B<NumRet<SubExp<LB, RB>>, _1>: NumExpr,
{
    type Output = NumRet<B<SubOut<LB, RB>, _1>>;
    fn sub(self, _rhs: B<RB, _0>) -> Self::Output {
        unimplemented!("type eval only")
    }
}

/// (L)1 - (R)1 = (L - R)0
impl<LB, RB> StSub<B<RB, _1>> for B<LB, _1>
where
    // `L - R` is valid
    LB: StSub<RB>,
    // `(L - R)0` is valid as a bitstring
    B<SubOut<LB, RB>, _0>: NumExpr,
{
    type Output = NumRet<B<SubOut<LB, RB>, _0>>;
    fn sub(self, _rhs: B<RB, _1>) -> Self::Output {
        unimplemented!("type eval only")
    }
}

#[cfg(test)]
mod test {
    use super::*;
    use crate::{
        num_vals::{U0, U1, U2, U3},
        test_res::*,
    };
    #[test]
    #[allow(clippy::used_underscore_items)]
    fn eval_sub() {
        const _0_SUB_0: () = _b0::<SubExp<U0, U0>>();
        const _1_SUB_0: () = _b1::<SubExp<U1, U0>>();
        const _1_SUB_1: () = _b0::<SubExp<U1, U1>>();
        const _2_SUB_1: () = _b1::<SubExp<U2, U1>>();
        const _2_SUB_0: () = _b2::<SubExp<U2, U0>>();
        // const _1_SUB_2: () = _b3::<SubExp<_1, B<_1, _0>>>();
        const _3_SUB_1: () = _b2::<SubExp<U3, _1>>();
        const _4_SUB_1: () = _b3::<SubExp<B<B<_1, _0>, _0>, _1>>();
        // const _1_SUB_3: () = _b4::<SubExp<_1, B<_1, _1>>>();
        const _2_SUB_2: () = _b0::<SubExp<U2, U2>>();
        const _3_SUB_2: () = _b1::<SubExp<U3, U2>>();
        const _3_SUB_3: () = _b0::<SubExp<U3, U3>>();
    }
}