Remove Bot type in favour of Empty trait
This commit is contained in:
1 parent
6aebb1f104
commit
62dae93140
2 files changed
+39
-75
No files matched your search
+6
-63
@@ -26,79 +26,22 @@ pub const fn infallible_to_never(infallible: Infallible) -> ! {
|
|||||||
infallible_elim(infallible)
|
infallible_elim(infallible)
|
||||||
}
|
}
|
||||||
|
|
||||||
/// The bottom type ⊥ with no elements. Since it has no elements, having an element of `Bot` is an
|
pub trait Empty: Sized {
|
||||||
/// inherent contradiction and it can therefore be converted to any other type. In MLTT, this
|
fn elim<T>(self) -> T;
|
||||||
/// corresponds to a proof by contradiction.
|
|
||||||
///
|
|
||||||
/// `Bot` serves the same purpose as `std::convert::Infallible` and the currently unstable "never"
|
|
||||||
/// type `!`, but provides more convenience methods than the former.
|
|
||||||
pub struct Bot(BotRepr);
|
|
||||||
|
|
||||||
impl Bot {
|
|
||||||
#[inline]
|
|
||||||
#[must_use]
|
|
||||||
pub const fn elim<T>(self) -> T {
|
|
||||||
self.0.elim()
|
|
||||||
}
|
|
||||||
|
|
||||||
#[inline]
|
#[inline]
|
||||||
#[must_use]
|
fn never(self) -> ! {
|
||||||
pub const fn elim_ref<T>(&self) -> T {
|
|
||||||
self.0.elim()
|
|
||||||
}
|
|
||||||
|
|
||||||
#[inline]
|
|
||||||
pub const fn never(self) -> ! {
|
|
||||||
self.elim()
|
self.elim()
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl Clone for Bot {
|
impl Empty for Infallible {
|
||||||
#[inline]
|
#[inline]
|
||||||
fn clone(&self) -> Self {
|
fn elim<T>(self) -> T {
|
||||||
self.elim_ref()
|
infallible_elim(self)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
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()
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
enum BotRepr {}
|
|
||||||
|
|
||||||
impl BotRepr {
|
|
||||||
#[inline]
|
|
||||||
const fn elim<T>(self) -> T {
|
|
||||||
match self {}
|
|
||||||
}
|
|
||||||
|
|
||||||
#[inline]
|
|
||||||
const fn elim_ref<T>(&self) -> T {
|
|
||||||
match *self {}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl Clone for BotRepr {
|
|
||||||
#[inline]
|
|
||||||
fn clone(&self) -> Self {
|
|
||||||
self.elim_ref()
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl Copy for BotRepr {}
|
|
||||||
|
|
||||||
#[inline]
|
#[inline]
|
||||||
#[must_use]
|
#[must_use]
|
||||||
pub fn clone<T: Clone>(x: &T) -> T {
|
pub fn clone<T: Clone>(x: &T) -> T {
|
||||||
|
|||||||
+33
-12
@@ -1,7 +1,12 @@
|
|||||||
use std::{convert::identity, hint, ops::{Deref, DerefMut}};
|
use std::{
|
||||||
|
convert::identity,
|
||||||
|
hint,
|
||||||
|
ops::{Deref, DerefMut}
|
||||||
|
};
|
||||||
|
|
||||||
use Either::{Inl, Inr};
|
use Either::{Inl, Inr};
|
||||||
use crate::convert::{clone, clone_mut, copy, copy_mut};
|
use crate::convert::{clone, clone_mut, copy, copy_mut, Empty};
|
||||||
|
|
||||||
pub enum Either<L, R> {
|
pub enum Either<L, R> {
|
||||||
Inl(L),
|
Inl(L),
|
||||||
Inr(R),
|
Inr(R),
|
||||||
@@ -174,6 +179,24 @@ impl<L, R> Either<L, R> {
|
|||||||
self.fold(Inr, Inl)
|
self.fold(Inr, Inl)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[inline]
|
||||||
|
#[must_use]
|
||||||
|
pub fn elim_l(self) -> R
|
||||||
|
where
|
||||||
|
L: Empty,
|
||||||
|
{
|
||||||
|
self.fold_l(<L as Empty>::elim)
|
||||||
|
}
|
||||||
|
|
||||||
|
#[inline]
|
||||||
|
#[must_use]
|
||||||
|
pub fn elim_r(self) -> L
|
||||||
|
where
|
||||||
|
R: Empty,
|
||||||
|
{
|
||||||
|
self.fold_r(<R as Empty>::elim)
|
||||||
|
}
|
||||||
|
|
||||||
#[inline]
|
#[inline]
|
||||||
#[must_use]
|
#[must_use]
|
||||||
pub fn some_l(self) -> Option<L> {
|
pub fn some_l(self) -> Option<L> {
|
||||||
@@ -489,19 +512,17 @@ impl<T> Either<T, T> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<L, R> Clone for Either<L, R>
|
impl<L: Empty, R: Empty> Empty for Either<L, R> {
|
||||||
where
|
fn elim<T>(self) -> T {
|
||||||
L: Clone,
|
self.fold(<L as Empty>::elim, <R as Empty>::elim)
|
||||||
R: Clone,
|
}
|
||||||
{
|
}
|
||||||
|
|
||||||
|
impl<L: Clone, R: Clone> Clone for Either<L, R> {
|
||||||
#[inline]
|
#[inline]
|
||||||
fn clone(&self) -> Self {
|
fn clone(&self) -> Self {
|
||||||
self.as_ref().map(<L as Clone>::clone, <R as Clone>::clone)
|
self.as_ref().map(<L as Clone>::clone, <R as Clone>::clone)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<L, R> Copy for Either<L, R>
|
impl<L: Copy, R: Copy> Copy for Either<L, R> {}
|
||||||
where
|
|
||||||
L: Copy,
|
|
||||||
R: Copy,
|
|
||||||
{}
|
|
||||||
Reference in new issue
Block a user