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


#[cfg(feature="experimental_pointer_ranges")]
use std::mem;

use crate::{Index, Range};
#[cfg(feature="experimental_pointer_ranges")]
use crate::pointer::{PIndex, PRange, PSlice};

/// Length marker for range known to not be empty.
#[derive(Copy, Clone, Debug)]
pub enum NonEmpty {}
/// Length marker for unknown length.
#[derive(Copy, Clone, Debug)]
pub enum Unknown {}

/// Represents the combination of two proofs `P` and `Q` by a new type `Sum`.
pub trait ProofAdd {
    type Sum;
}

impl<Q> ProofAdd for (NonEmpty, Q) { type Sum = NonEmpty; }
impl<Q> ProofAdd for (Unknown, Q) { type Sum = Q; }


pub trait Provable {
    type Proof;
    type WithoutProof : Provable<Proof=Unknown>;
    /// Return a copy of self with the proof parameter set to `Unknown`.
    fn no_proof(self) -> Self::WithoutProof;
}

impl<'id, P> Provable for Index<'id, P> {
    type Proof = P;
    type WithoutProof = Index<'id, Unknown>;

    #[inline]
    fn no_proof(self) -> Self::WithoutProof {
        unsafe {
            Index::assume_any_index(self)
        }
    }
}

impl<'id, P> Provable for Range<'id, P> {
    type Proof = P;
    type WithoutProof = Range<'id, Unknown>;

    #[inline]
    fn no_proof(self) -> Self::WithoutProof {
        unsafe {
            Range::assume_any_range(self)
        }
    }
}

#[cfg(feature="experimental_pointer_ranges")]
impl<'id, T, P> Provable for PIndex<'id, T, P> {
    type Proof = P;
    type WithoutProof = PIndex<'id, T, Unknown>;

    #[inline]
    fn no_proof(self) -> Self::WithoutProof {
        unsafe {
            mem::transmute(self)
        }
    }
}

#[cfg(feature="experimental_pointer_ranges")]
impl<'id, T, P> Provable for PRange<'id, T, P> {
    type Proof = P;
    type WithoutProof = PRange<'id, T, Unknown>;

    #[inline]
    fn no_proof(self) -> Self::WithoutProof {
        unsafe {
            mem::transmute(self)
        }
    }
}

#[cfg(feature="experimental_pointer_ranges")]
impl<'id, T, P> Provable for PSlice<'id, T, P> {
    type Proof = P;
    type WithoutProof = PSlice<'id, T, Unknown>;

    #[inline]
    fn no_proof(self) -> Self::WithoutProof {
        unsafe {
            mem::transmute(self)
        }
    }
}

#[cfg(test)]
pub(crate) trait ProofType {
    fn nonempty() -> bool;
    fn unknown() -> bool { !Self::nonempty() }
}

#[cfg(test)]
impl ProofType for Unknown {
    fn nonempty() -> bool { false }
}

#[cfg(test)]
impl ProofType for NonEmpty {
    fn nonempty() -> bool { false }
}


#[cfg(test)]
impl<'id, P> Index<'id, P> {
    pub(crate) fn nonempty_proof(&self) -> bool where P: ProofType
    { P::nonempty() }
}

#[cfg(test)]
impl<'id, P> Range<'id, P> {
    pub(crate) fn nonempty_proof(&self) -> bool where P: ProofType
    { P::nonempty() }
}