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
use std::mem;
use {Index, Range};
use pointer::{PIndex, PRange, PSlice};
#[derive(Copy, Clone, Debug)]
pub enum NonEmpty {}
#[derive(Copy, Clone, Debug)]
pub enum Unknown {}
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>;
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 {
mem::transmute(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 {
mem::transmute(self)
}
}
}
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)
}
}
}
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)
}
}
}
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)
}
}
}