indexing/
proof.rs

1use core::{fmt, marker::PhantomData};
2
3/// `Id<'id>` is _invariant_ w.r.t. `'id`.
4///
5/// This means that the inference engine is not allowed to
6/// grow or shrink `'id` to unify with any other lifetime.
7#[derive(Copy, Clone, Default, Ord, PartialOrd, Eq, PartialEq, Hash)]
8pub(crate) struct Id<'id> {
9    id: PhantomData<&'id mut &'id ()>,
10}
11
12unsafe impl<'id> Sync for Id<'id> {}
13unsafe impl<'id> Send for Id<'id> {}
14
15impl<'id> fmt::Debug for Id<'id> {
16    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
17        f.debug_struct("Id<'id>").finish()
18    }
19}
20
21/// Length marker for range/index known to not be empty.
22#[derive(Copy, Clone, Debug, Ord, PartialOrd, Eq, PartialEq, Hash)]
23pub enum NonEmpty {}
24
25/// Length marker for range/index of unknown length (may be empty).
26#[derive(Copy, Clone, Debug, Ord, PartialOrd, Eq, PartialEq, Hash)]
27pub enum Unknown {}
28
29/// Represents the combination of two proofs `P` and `Q` by a new type `Sum`.
30pub trait ProofAdd {
31    type Sum;
32}
33
34impl<Q> ProofAdd for (NonEmpty, Q) {
35    type Sum = NonEmpty;
36}
37impl<Q> ProofAdd for (Unknown, Q) {
38    type Sum = Q;
39}
indexing/proof.rs

indexing/
proof.rs
