gnat 0.1.9

Type-level numbers without extra bounds
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

use super::*;

// Inc(N) := N + 1
//
// H := H(N), P := P(N).
//
// N + 1 = 2 * H + P + 1
//       = if P { 2 * H + 2 } else { 2 * H + 1 }
//       = if P { 2 * (H + 1) } else { 2 * H + 1 }
//       = if P { PushBit(H + 1, 0) } else { PushBit(H, 1) }
#[apply(nat_expr)]
pub type _Inc<N: NatExpr> = If<
    _P<N>, //
    PushBit<_Inc<_H<N>>, crate::lit!(0)>,
    PushBit<_H<N>, crate::lit!(1)>,
>;

pub(crate) type _PlusBit<N, C> = If<C, _Inc<N>, N>;

// This is just binary addition.
//
// Add(L, R, C) := L + R + C, where C <= 1.
//
// HL := H(L), PL := P(L), HR := H(R), PR := P(R)
//
//   L + R + C
// = (2 * LH + LP) + (2 * RH + RP) + C
// = 2 * (LH + RH) + (LP + RP + C)
//
// X := LP + RP + C. Since X = 2 * (X / 2) + X % 2, we get
//   L + R + C
// = 2 * (LH + RH + X / 2) + X % 2
// = Append(LH + RH + X / 2, X % 2)
#[apply(nat_expr)]
pub type _Add<L: NatExpr, R: NatExpr, C: NatExpr = crate::lit!(0)> = If<
    L,
    PushBit<
        // LH + RH + X / 2
        _Add<
            _H<R>, // swap args to converge faster, since A + B = B + A
            _H<L>,
            // Normalize recursive argument
            crate::Eval<
                // Since X = LP + RP + C <= 3, we have X / 2 being either 0 or 1,
                // and therefore X / 2 = 1 iff LP + RP + C >= 2, else X / 2 = 0.
                If<
                    _P<L>,
                    // LP = 1, so LP + RP + C >= 2 iff RP + C >= 1 iff RP = 1 or  C = 1
                    _Or<_P<R>, C>,
                    // LP = 0, so LP + RP + C >= 2 iff RP + C >= 2 iff RP = 1 and C = 1
                    _And<_P<R>, C>,
                >,
            >,
        >,
        // X % 2 is 1 iff X is odd, i.e. if an odd number of LP, RP, C are 1.
        // Hence X % 2 = Xor(LP, RP, C).
        _Xor3<_P<L>, _P<R>, C>,
    >,
    // 0 + R + C = R + C
    _PlusBit<R, C>,
>;

/// Type-level [`+`](Add)
#[apply(opaque)]
#[apply(test_op! test_add, L + R)]
pub type Add<L, R> = _Add;