|
|
|
|
@ -1,5 +1,31 @@
|
|
|
|
|
use std::convert::Infallible;
|
|
|
|
|
|
|
|
|
|
/// Consumes an element of type `Infallible` and produces an element of any type `T`. This is
|
|
|
|
|
/// possible because `Infallible` has no elements and thus this function can never be called, so
|
|
|
|
|
/// the statement "for any given type `T`, whenever this function returns, it returns an element of
|
|
|
|
|
/// `T`" is vacuously true. In MLTT, this corresponds to a proof by contradiction.
|
|
|
|
|
///
|
|
|
|
|
/// ```
|
|
|
|
|
/// # use std::convert::Infallible;
|
|
|
|
|
/// # use libshire::convert::infallible_elim;
|
|
|
|
|
/// use std::io;
|
|
|
|
|
/// let x: Result<u32, Infallible> = Ok(123);
|
|
|
|
|
/// let y: Result<u32, io::Error> = x.map_err(infallible_elim);
|
|
|
|
|
/// ```
|
|
|
|
|
#[inline]
|
|
|
|
|
#[must_use]
|
|
|
|
|
pub const fn infallible_elim<T>(infallible: Infallible) -> T {
|
|
|
|
|
match infallible {}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
/// Converts an element of type `Infallible` to an element of the "never" type `!`. The never type
|
|
|
|
|
/// can be more useful than `Infallible` because it can be coerced to any other type and implements
|
|
|
|
|
/// many more traits than `Infallible` does.
|
|
|
|
|
#[inline]
|
|
|
|
|
pub const fn infallible_to_never(infallible: Infallible) -> ! {
|
|
|
|
|
infallible_elim(infallible)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
/// The bottom type ⊥ with no elements. Since it has no elements, having an element of `Bot` is an
|
|
|
|
|
/// inherent contradiction and it can therefore be converted to any other type. In MLTT, this
|
|
|
|
|
/// corresponds to a proof by contradiction.
|
|
|
|
|
@ -11,18 +37,18 @@ pub struct Bot(BotRepr);
|
|
|
|
|
impl Bot {
|
|
|
|
|
#[inline]
|
|
|
|
|
#[must_use]
|
|
|
|
|
pub fn elim<T>(self) -> T {
|
|
|
|
|
pub const fn elim<T>(self) -> T {
|
|
|
|
|
self.0.elim()
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[inline]
|
|
|
|
|
#[must_use]
|
|
|
|
|
pub fn elim_ref<T>(&self) -> T {
|
|
|
|
|
pub const fn elim_ref<T>(&self) -> T {
|
|
|
|
|
self.0.elim()
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[inline]
|
|
|
|
|
pub fn never(self) -> ! {
|
|
|
|
|
pub const fn never(self) -> ! {
|
|
|
|
|
self.elim()
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
@ -37,12 +63,14 @@ impl Clone for Bot {
|
|
|
|
|
impl Copy for Bot {}
|
|
|
|
|
|
|
|
|
|
impl From<Infallible> for Bot {
|
|
|
|
|
#[inline]
|
|
|
|
|
fn from(infallible: Infallible) -> Self {
|
|
|
|
|
infallible_elim(infallible)
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
impl From<Bot> for Infallible {
|
|
|
|
|
#[inline]
|
|
|
|
|
fn from(bot: Bot) -> Self {
|
|
|
|
|
bot.elim()
|
|
|
|
|
}
|
|
|
|
|
@ -52,17 +80,18 @@ enum BotRepr {}
|
|
|
|
|
|
|
|
|
|
impl BotRepr {
|
|
|
|
|
#[inline]
|
|
|
|
|
fn elim<T>(self) -> T {
|
|
|
|
|
const fn elim<T>(self) -> T {
|
|
|
|
|
match self {}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[inline]
|
|
|
|
|
fn elim_ref<T>(&self) -> T {
|
|
|
|
|
const fn elim_ref<T>(&self) -> T {
|
|
|
|
|
match *self {}
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
impl Clone for BotRepr {
|
|
|
|
|
#[inline]
|
|
|
|
|
fn clone(&self) -> Self {
|
|
|
|
|
self.elim_ref()
|
|
|
|
|
}
|
|
|
|
|
@ -72,11 +101,24 @@ impl Copy for BotRepr {}
|
|
|
|
|
|
|
|
|
|
#[inline]
|
|
|
|
|
#[must_use]
|
|
|
|
|
pub fn infallible_elim<T>(infallible: Infallible) -> T {
|
|
|
|
|
match infallible {}
|
|
|
|
|
pub fn clone<T: Clone>(x: &T) -> T {
|
|
|
|
|
x.clone()
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[inline]
|
|
|
|
|
pub fn infallible_to_never(infallible: Infallible) -> ! {
|
|
|
|
|
infallible_elim(infallible)
|
|
|
|
|
#[must_use]
|
|
|
|
|
pub fn clone_mut<T: Clone>(x: &mut T) -> T {
|
|
|
|
|
(&*x).clone()
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[inline]
|
|
|
|
|
#[must_use]
|
|
|
|
|
pub fn copy<T: Copy>(x: &T) -> T {
|
|
|
|
|
*x
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[inline]
|
|
|
|
|
#[must_use]
|
|
|
|
|
pub fn copy_mut<T: Copy>(x: &mut T) -> T {
|
|
|
|
|
*x
|
|
|
|
|
}
|
|
|
|
|
|