deptypes/
result.rs

1use core::marker::PhantomData;
2use core::mem::ManuallyDrop;
3use crate::bool::choose;
4use crate::guard::Guard;
5use crate::term::Value;
6use crate::var::Var;
7use crate::transmutable::{coerce, Equiv};
8use crate::term::ValueEq;
9use crate::{bool::{False, True}, term::Term};
10
11#[repr(C)]
12pub union DResult<B: Term<Type = bool>, T, F> {
13    phantom: PhantomData<Value<B>>,
14    t: ManuallyDrop<T>,
15    f: ManuallyDrop<F>,
16}
17
18impl<B: Term<Type = bool>, T, F> Drop for DResult<B, T, F> {
19    #[inline(always)]
20    fn drop(&mut self) {
21        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");
22    }
23}
24
25impl<T, F> DResult<True, T, F> {
26    pub fn into(mut self) -> T {
27        let r = unsafe {ManuallyDrop::take(&mut self.t)};
28        core::mem::forget(self);
29        r
30    }
31
32    pub fn new(t: T) -> Self {
33        DResult {t: ManuallyDrop::new(t)}
34    }
35}
36
37impl<T, F> DResult<False, T, F> {
38    pub fn into(mut self) -> F {
39        let r = unsafe {ManuallyDrop::take(&mut self.f)};
40        core::mem::forget(self);
41        r
42    }
43
44    pub fn new(f: F) -> Self {
45        DResult {f: ManuallyDrop::new(f)}
46    }
47}
48
49impl<B: Term<Type = bool>, T, F> DResult<B, T, F> {
50    pub fn equiv<B1: Term<Type = bool>>(_: ValueEq<B, B1>) -> Equiv<DResult<B, T, F>, DResult<B1, T, F>> {
51        unsafe {Equiv::axiom()}
52    }
53}
54
55impl<'a, T, F> DResult<Var<'a, bool>, T, F> {
56    pub fn from(guard: Guard<'a>, x: Result<T, F>) -> (Self, Result<ValueEq<Var<'a, bool>, True>, ValueEq<Var<'a, bool>, False>>) {
57        match x {
58            Ok(t) => {
59                let eq = Var::erase(guard);
60                let r = DResult::<True, _, _>::new(t);
61                let r = coerce(r, DResult::equiv(eq));
62                (r, Ok(-eq))
63            }
64            Err(f) => {
65                let eq = Var::erase(guard);
66                let r = DResult::<False, _, _>::new(f);
67                let r = coerce(r, DResult::equiv(eq));
68                (r, Err(-eq))
69            }
70        }
71    }
72}
73
74impl<B: Term<Type = bool>, T, F> DResult<B, T, F> {
75    pub fn into_result(r: DResult<B, T, F>, b: Value<B>) -> Result<T, F> {
76        match choose(b) {
77            Ok(eq) => {
78                let r = coerce(r, DResult::equiv(eq));
79                Ok(r.into())
80            },
81            Err(eq) => {
82                let r = coerce(r, DResult::equiv(eq));
83                Err(r.into())
84            }
85        }
86    }
87}
deptypes/result.rs

deptypes/
result.rs
