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
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

use super::*;

// Cmp(L, R) := if L < R { 0 } else if L > R { 1 } else { 2 }
//
// HL := H(L), PL := P(L), HR := H(R), PR := P(R)
// CmpHalf := Cmp(HL, HR)
//
// Cmp(L, R) = 0
// iff L < R
// iff 2 * HL + PL < 2 * HR + PR
// iff HL < HR or (HL = HR and PL < PR)
// iff Cmp(HL, HR) = 0 or (Cmp(HL, HR) = 2 and PL = 0 and PR = 1)
//
// Cmp(L, R) = 1
// iff L > R
// iff 2 * HL + PL > 2 * HR + PR
// iff Cmp(HL, HR) = 1 or (Cmp(HL, HR) = 2 and PL = 1 and PR = 0)
//
// Cmp(L, R) = 2
// iff L = R
// iff HL = HR and PL = PR
// iff Cmp(HL, HR) = 2 and PL = PR
//
// - If Cmp(HL, HR) != 2, then Cmp(L, R) = Cmp(HL, HR)
// - If Cmp(HL, HR)  = 2, then decide Cmp(L, R) based on PL, PR
#[apply(nat_expr)]
#[apply(test_op! test_cmp, {
    match L.cmp(&R) {
        core::cmp::Ordering::Less => 0,
        core::cmp::Ordering::Greater => 1,
        core::cmp::Ordering::Equal => 2,
    }
})]
pub type _Cmp<L: Nat, R: Nat> = If<
    L,
    // L != 0. If R = 0, then L > R, else recurse
    If<R, _CmpRecExpr<L, R>, crate::lit!(1)>,
    // L = 0. If R = 0, then L = R, else L < R
    If<R, crate::lit!(0), crate::lit!(2)>,
>;
// Cmp without base case
#[apply(nat_expr)]
pub type _CmpRecExpr<L: Nat, R: Nat> = _CmpInterp<
    crate::Eval<
        _Cmp<
            _H<L>, //
            _H<R>,
        >,
    >,
    _P<L>,
    _P<R>,
>;
// CmpInterp(Cmp(HL, HR), PL, PR) := Cmp(L, R)
#[apply(nat_expr)]
pub type _CmpInterp<CmpHalf: Nat, PL: Nat, PR: Nat> = If<
    // H(CmpHalf) != 0 iff Cmp(HL, HR) = 2
    _H<CmpHalf>,
    // Cmp(HL, HR) = 2
    If<
        PL,
        // PL = 1, thus
        // - If PR = 1, then PL = PR, then Cmp(L, R) = 2
        // - If PR = 0, then Cmp(L, R) = 1
        If<PR, crate::lit!(2), crate::lit!(1)>,
        // PL = 0, thus
        // - If PR = 1, then Cmp(L, R) = 0
        // - If PR = 0, then PL = PR, then Cmp(L, R) = 2
        If<PR, crate::lit!(0), crate::lit!(2)>,
    >,
    // Cmp(HL, HR) != 2, thus Cmp(L, R) = Cmp(HL, HR)
    CmpHalf,
>;

/// Type-level [`==`](core::cmp::PartialEq)
///
/// The result of this operation is either `0` or `1`.
#[doc(alias = "==")]
#[apply(opaque)]
#[apply(test_op! test_eq, (L == R) as _)]
pub type Eq<L, R> = _Eq;

#[apply(nat_expr)] // L = R iff Cmp(L, R) = 2; H(2)=1, H(0)=H(1)=0
pub type _Eq<L: NatExpr, R: NatExpr> = _H<_Cmp<L::Eval, R::Eval>>;

/// Type-level [`!=`](core::cmp::PartialEq)
///
/// The result of this operation is either `0` or `1`.
#[doc(alias = "!=")]
#[apply(opaque)]
pub type Ne<L, R> = _Ne;

#[apply(nat_expr)]
pub type _Ne<L: NatExpr, R: NatExpr> = IsZero<_Eq<L, R>>;

/// Type-level [`<`](core::cmp::PartialOrd)
///
/// The result of this operation is either `0` or `1`.
#[doc(alias = "<")]
#[apply(opaque)]
#[apply(test_op! test_lt, (L < R) as _)]
pub type Lt<L, R> = _Lt;

#[apply(nat_expr)] // L < R iff Cmp(L, R) = 0
pub type _Lt<L: NatExpr, R: NatExpr> = IsZero<_Cmp<L::Eval, R::Eval>>;

/// Type-level [`>`](core::cmp::PartialOrd)
///
/// The result of this operation is either `0` or `1`.
#[doc(alias = ">")]
pub type Gt<L, R> = Lt<R, L>;

/// Type-level [`<=`](core::cmp::PartialOrd)
///
/// The result of this operation is either `0` or `1`.
#[doc(alias = "<=")]
#[apply(opaque)]
pub type Le<L, R> = _Le;
#[apply(nat_expr)]
pub type _Le<L: NatExpr, R: NatExpr> = IsZero<Gt<L, R>>;

/// Type-level [`>=`](core::cmp::PartialOrd)
///
/// The result of this operation is either `0` or `1`.
#[doc(alias = ">=")]
pub type Ge<L, R> = Le<R, L>;

/// Type-level [`min`](core::cmp::min)
#[apply(opaque)]
pub type Min<L, R> = _Min;

#[apply(nat_expr)]
pub type _Min<L: NatExpr, R: NatExpr> = If<_Lt<L, R>, R, L>;

#[apply(nat_expr)]
pub type _Max<L: NatExpr, R: NatExpr> = If<_Lt<L, R>, L, R>;

/// Type-level [`max`](core::cmp::max)
#[apply(opaque)]
pub type Max<L, R> = _Max;