gnat 0.1.8

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

use super::*;

/// Pops the last bit of a [`Nat`], thereby getting half its value.
///
/// This is a primitive operation.
///
/// Effectively a more efficient implementation of [`Div<N, _2>`] or [`Shr<N, _1>`].
/// This, together with [`LastBit`] and [`If`], can be used to implement operations that
/// recursively destructure a number and accumulate a result.
///
/// See the [module level documentation](mod@crate::expr) for details on how to combine
/// primitive operations.
#[apply(nat_expr!
    eval_attrs = { #[doc(hidden)] },
)]
pub type PopBit<N: NatExpr> = InternalOp!(crate::Eval<N>, PopBit);

/// Gets the last bit of a [`Nat`], thereby getting its parity.
///
/// This is a primitive operation.
///
/// Effectively a more efficient implementation of [`Rem<N, _2>`] or [`BitAnd<N, _1>`].
/// This, together with [`PopBit`] and [`If`], can be used to implement operations that
/// recursively destructure a number and accumulate a result.
///
/// See the [module level documentation](mod@crate::expr) for details on how to combine
/// primitive operations.
#[apply(nat_expr!
    eval_attrs = { #[doc(hidden)] },
)]
pub type LastBit<N: NatExpr> = InternalOp!(crate::Eval<N>, LastBit);

/// Pushes a single bit to the end of a [`Nat`].
///
/// This is a primitive operation.
///
/// Effectively a more efficient implementation of `Add<Mul<N, _2>, IsNonzero<P>>`,
/// or `BitOr<Shl<N, _1>, IsNonzero<P>>`. It is meant to be used for building the
/// output of an operation recursively bit-by-bit.
///
/// See the [module level documentation](mod@crate::expr) for details on how to combine
/// primitive operations.
#[apply(nat_expr!
    eval_attrs = { #[doc(hidden)] },
)]
pub type PushBit<N: NatExpr, P: NatExpr> =
    InternalOp!(crate::Eval<P>, PushSelfAsBit<crate::Eval<N>>);

/// Ternary operation
///
/// This is a primitive operation.
///
/// If `Cond` is truthy (nonzero), then `crate::Eval<If<Cond, Then, Else>>` is the same as
/// `crate::Eval<Then>`. Otherwise, it is the same as `crate::Eval<Else>`.
/// Only the resulting argument has its [`NatExpr::Eval`] implementation accessed,
/// i.e. the other branch is not evaluated and thus cannot lead to cycles. This allows
/// breaking out of recursively implemented operations.
///
/// See the [module level documentation](mod@crate::expr) for details on how to combine
/// primitive operations.
///
/// # Opaqueness
/// This operation is not opaque in `Then` and `Else`. If `Cond` is known, then
/// `crate::Eval<If<Cond, Then, Else>>` normalizes as specified above.
#[apply(nat_expr!
    eval_attrs = { #[doc(hidden)] },
)]
pub type If<C: NatExpr, T: NatExpr, F: NatExpr> = InternalOp!(crate::Eval<C>, If<T, F>);

/// Makes a [`NatExpr`] opaque with respect to the value of a parameter.
///
/// This is a primitive operation.
///
/// `Opaque<P, Out>` evaluates to the same [`Nat`] as `Out`, but only after
/// going through a projection via an internal associated type on
/// [`P::Eval`](NatExpr).
///
/// See the [module level documentation](mod@crate::expr) for details on opaqueness.
#[apply(nat_expr!
    eval_attrs = { #[doc(hidden)] },
)]
pub type Opaque<P: NatExpr, Out: NatExpr> = crate::Eval<InternalOp!(crate::Eval<P>, Opaque<Out>)>;

#[test]
fn opaqueness_tests() {
    struct Namespace<L, R>(L, R);
    trait Fallback {
        const PROVEN_IDENTICAL: bool;
    }
    // `Wat` has a trait const
    impl<X> Namespace<X, X> {
        const PROVEN_IDENTICAL: bool = true;
    }
    impl<L, R> Fallback for Namespace<L, R> {
        const PROVEN_IDENTICAL: bool = false;
    }
    macro_rules! check_proven_identical {
        ($expect:expr, $lhs:ty, $rhs:ty) => {
            assert!($expect == Namespace::<$lhs, $rhs>::PROVEN_IDENTICAL)
        };
    }
    fn accept<A: NatExpr, B: NatExpr>() {
        // types that are provably the same
        check_proven_identical!(true, crate::Eval<If<crate::lit!(1), A, B>>, crate::Eval<A>);
        check_proven_identical!(true, crate::Eval<If<crate::lit!(0), A, B>>, crate::Eval<B>);
        check_proven_identical!(true, crate::Eval<Opaque<crate::lit!(0), A>>, crate::Eval<A>);

        // types that are not provably the same
        check_proven_identical!(false, crate::Eval<Opaque<B, A>>, crate::Eval<A>);
        check_proven_identical!(false, crate::Eval<Opaque<B, A>>, Opaque<A, A>);
        check_proven_identical!(
            false,
            crate::Eval<PopBit<PushBit<crate::lit!(0), A>>>,
            crate::lit!(0)
        );
    }
    accept::<crate::lit!(3), crate::lit!(7)>();
}