deptypes 0.2.1

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

use core::marker::PhantomData;
use core::mem::ManuallyDrop;
use crate::bool::choose;
use crate::guard::Guard;
use crate::term::Value;
use crate::var::Var;
use crate::transmutable::{coerce, Equiv};
use crate::term::ValueEq;
use crate::{bool::{False, True}, term::Term};

#[repr(C)]
pub union DResult<B: Term<Type = bool>, T, F> {
    phantom: PhantomData<Value<B>>,
    t: ManuallyDrop<T>,
    f: ManuallyDrop<F>,
}

impl<B: Term<Type = bool>, T, F> Drop for DResult<B, T, F> {
    #[inline(always)]
    fn drop(&mut self) {
        link_error!("DResult types are linear types that cannot be allowed to be dropped, instead use into() or into_result() so that the proper destructor is run");
    }
}

impl<T, F> DResult<True, T, F> {
    pub fn into(mut self) -> T {
        let r = unsafe {ManuallyDrop::take(&mut self.t)};
        core::mem::forget(self);
        r
    }

    pub fn new(t: T) -> Self {
        DResult {t: ManuallyDrop::new(t)}
    }
}

impl<T, F> DResult<False, T, F> {
    pub fn into(mut self) -> F {
        let r = unsafe {ManuallyDrop::take(&mut self.f)};
        core::mem::forget(self);
        r
    }

    pub fn new(f: F) -> Self {
        DResult {f: ManuallyDrop::new(f)}
    }
}

impl<B: Term<Type = bool>, T, F> DResult<B, T, F> {
    pub fn equiv<B1: Term<Type = bool>>(_: ValueEq<B, B1>) -> Equiv<DResult<B, T, F>, DResult<B1, T, F>> {
        unsafe {Equiv::axiom()}
    }
}

impl<'a, T, F> DResult<Var<'a, bool>, T, F> {
    pub fn from(guard: Guard<'a>, x: Result<T, F>) -> (Self, Result<ValueEq<Var<'a, bool>, True>, ValueEq<Var<'a, bool>, False>>) {
        match x {
            Ok(t) => {
                let eq = Var::erase(guard);
                let r = DResult::<True, _, _>::new(t);
                let r = coerce(r, DResult::equiv(eq));
                (r, Ok(-eq))
            }
            Err(f) => {
                let eq = Var::erase(guard);
                let r = DResult::<False, _, _>::new(f);
                let r = coerce(r, DResult::equiv(eq));
                (r, Err(-eq))
            }
        }
    }
}

impl<B: Term<Type = bool>, T, F> DResult<B, T, F> {
    pub fn into_result(r: DResult<B, T, F>, b: Value<B>) -> Result<T, F> {
        match choose(b) {
            Ok(eq) => {
                let r = coerce(r, DResult::equiv(eq));
                Ok(r.into())
            },
            Err(eq) => {
                let r = coerce(r, DResult::equiv(eq));
                Err(r.into())
            }
        }
    }
}