gnat 0.1.10

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

// All bitwise operations are implemented the same way:
//
// Let Bitwise(Op, L, R) be the result of all Op(L(i), R(i)) appended to each other.
//
// Then we observe
// Bitwise(Op, L, R) = Bitwise(Op, Append(H(L), P(L)), Append(H(R), P(R)))
//                   = Append(Bitwise(Op, H(L), H(R)), Op(P(L), P(R))
//
// Because H and P split the number into the part before and after the last bit.

use super::*;

// BitAnd(L, R) := Bitwise(And, L, R), see module level
#[apply(nat_expr)]
pub type _BitAnd<L: NatExpr, R: NatExpr> = If<
    L,
    PushBit<
        _BitAnd<_H<R>, _H<L>>, // A & B = B & A, switching will terminate faster
        _And<_P<L>, _P<R>>,
    >,
    // 0 & R = 0
    crate::lit!(0),
>;

/// Type-level [`&`](https://en.wikipedia.org/wiki/Bitwise_operation#AND)
#[doc(alias = "&")]
#[apply(opaque)]
#[apply(test_op! test_bit_and, L & R)]
pub type BitAnd<L, R> = _BitAnd;

// BitOr(L, R) := Bitwise(Or, L, R), see module level
#[apply(nat_expr)]
pub type _BitOr<L: NatExpr, R: NatExpr> = If<
    L,
    PushBit<
        _BitOr<_H<R>, _H<L>>, // A | B = B | A
        _Or<_P<L>, _P<R>>,
    >,
    // 0 | R = R
    R,
>;

/// Type-level [`|`](https://en.wikipedia.org/wiki/Bitwise_operation#OR)
#[doc(alias = "|")]
#[apply(opaque)]
#[apply(test_op! test_bit_or, L | R)]
// BitOr(L, R) := Bitwise(Or, L, R), see above
pub type BitOr<L, R> = _BitOr;

// BitXor(L, R) = Bitwise(Xor, L, R), see module level
#[apply(nat_expr)]
pub type _BitXor<L: NatExpr, R: NatExpr> = If<
    L,
    PushBit<
        _BitXor<_H<R>, _H<L>>, // A ^ B = B ^ A
        _Xor<_P<L>, _P<R>>,
    >,
    // 0 ^ R = R
    R,
>;

/// Type-level [`^`](https://en.wikipedia.org/wiki/Bitwise_operation#XOR)
#[doc(alias = "^")]
#[apply(opaque)]
#[apply(test_op! test_bit_xor, L ^ R)]
pub type BitXor<L, R> = _BitXor;