Skip to content

Simplify implementation #5

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
mgeier wants to merge 4 commits into
base: main
Choose a base branch
from
Open

Simplify implementation #5

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
4c66b40
Add type definition for each operator
mgeier Jan 18, 2024
ca3f3cc
rustfmt
mgeier Jan 18, 2024
77150a8
Simplify impls
mgeier Jan 18, 2024
d12ff3c
Remove check for 0/0
mgeier Jan 18, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
204 changes: 80 additions & 124 deletions src/main.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ use std::marker::PhantomData;
fn main() {
println!(
"{}",
<(
Sub::<
encode!(
***********************
***********************
Expand All @@ -14,8 +14,8 @@ fn main() {
**************
**************
**************
)
) as Sub>::Diff::VALUE
),
>::VALUE
);
}

Expand Down Expand Up @@ -57,146 +57,116 @@ where

// Addition

trait Add {
type Sum;
trait AddImpl {
type Output;
}

impl Add for (Zero, Zero) {
type Sum = Zero;
}
type Add<L, R> = <(L, R) as AddImpl>::Output;

impl<T> Add for (Succ<T>, Zero) {
type Sum = Succ<T>;
impl<T> AddImpl for (Zero, T) {
type Output = T;
}

impl<T> Add for (Zero, Succ<T>) {
type Sum = Succ<T>;
}

impl<T, U> Add for (Succ<T>, Succ<U>)
impl<T, U> AddImpl for (Succ<T>, U)
where
(T, Succ<Succ<U>>): Add,
(T, Succ<U>): AddImpl,
{
type Sum = <(T, Succ<Succ<U>>) as Add>::Sum;
type Output = Add<T, Succ<U>>;
}

// Subtraction

trait Sub {
type Diff;
trait SubImpl {
type Output;
}

impl Sub for (Zero, Zero) {
type Diff = Zero;
}
type Sub<L, R> = <(L, R) as SubImpl>::Output;

impl<T> Sub for (Succ<T>, Zero) {
type Diff = Succ<T>;
impl<T> SubImpl for (T, Zero) {
type Output = T;
}

impl<T> Sub for (Zero, Succ<T>) {
type Diff = Zero;
impl<T> SubImpl for (Zero, Succ<T>) {
type Output = Zero;
}

impl<T, U> Sub for (Succ<T>, Succ<U>)
impl<T, U> SubImpl for (Succ<T>, Succ<U>)
where
(T, U): Sub,
(T, U): SubImpl,
{
type Diff = <(T, U) as Sub>::Diff;
type Output = Sub<T, U>;
}

// Multiplication

trait Mul {
type Product;
trait MulImpl {
type Output;
}

impl<T> Mul for (T, Zero) {
type Product = Zero;
}
type Mul<L, R> = <(L, R) as MulImpl>::Output;

// Implementing for (Zero, T) would overlap with the previous impl, so we do
// (Zero, Succ<T>) to avoid the (Zero, Zero) case that overlaps
impl<T> Mul for (Zero, Succ<T>) {
type Product = Zero;
impl<T> MulImpl for (Zero, T) {
type Output = Zero;
}

impl<T, U> Mul for (Succ<T>, Succ<U>)
impl<T, U> MulImpl for (Succ<T>, U)
where
(T, Succ<U>): Mul,
(Succ<U>, <(T, Succ<U>) as Mul>::Product): Add,
(T, U): MulImpl,
(U, Mul<T, U>): AddImpl,
{
// x * y = y + (x - 1) * y
type Product = <(Succ<U>, <(T, Succ<U>) as Mul>::Product) as Add>::Sum;
type Output = Add<U, Mul<T, U>>;
}

// Division

trait GreaterThanEq {
type Greater;
trait GreaterThanEqImpl {
type Output;
}

impl GreaterThanEq for (Zero, Zero) {
type Greater = Succ<Zero>;
}
type GreaterThanEq<L, R> = <(L, R) as GreaterThanEqImpl>::Output;

impl<T> GreaterThanEq for (Zero, Succ<T>) {
type Greater = Zero;
impl<T> GreaterThanEqImpl for (Zero, Succ<T>) {
type Output = Zero;
}

impl<T> GreaterThanEq for (Succ<T>, Zero) {
type Greater = Succ<Zero>;
impl<T> GreaterThanEqImpl for (T, Zero) {
type Output = Succ<Zero>;
}

impl<T, U> GreaterThanEq for (Succ<T>, Succ<U>)
impl<T, U> GreaterThanEqImpl for (Succ<T>, Succ<U>)
where
(T, U): GreaterThanEq,
(T, U): GreaterThanEqImpl,
{
type Greater = <(T, U) as GreaterThanEq>::Greater;
type Output = GreaterThanEq<T, U>;
}

trait Div {
type Quotient;
trait DivImpl {
type Output;
}

// Instead of implementing for (T, Succ<Zero>), implement for (Succ<T>, Succ<Zero>)
// to avoid overlapping with the next impl on (Zero, Succ<Zero>)
impl<T> Div for (Succ<T>, Succ<Zero>) {
type Quotient = Succ<T>;
}
type Div<L, R> = <(L, R) as DivImpl>::Output;

impl<T> Div for (Zero, T) {
type Quotient = Zero;
impl<T> DivImpl for (Zero, Succ<T>) {
type Output = Zero;
}

type RawQuotient<T, U> = <(
Succ<Zero>,
<(<(Succ<T>, Succ<Succ<U>>) as Sub>::Diff, Succ<Succ<U>>) as Div>::Quotient,
) as Add>::Sum;
type RawQuotient<T, U> = Add<Succ<Zero>, Div<Sub<Succ<T>, Succ<U>>, Succ<U>>>;

impl<T, U> Div for (Succ<T>, Succ<Succ<U>>)
impl<T, U> DivImpl for (Succ<T>, Succ<U>)
where
(T, Succ<U>): Sub,
(<(T, Succ<U>) as Sub>::Diff, Succ<Succ<U>>): Div,
(
Succ<Zero>,
<(<(T, Succ<U>) as Sub>::Diff, Succ<Succ<U>>) as Div>::Quotient,
): Add,
(T, U): SubImpl,
(Sub<T, U>, Succ<U>): DivImpl,
(Succ<Zero>, Div<Sub<T, U>, Succ<U>>): AddImpl,
(
<(Succ<T>, Succ<Succ<U>>) as GreaterThanEq>::Greater,
<(
Succ<Zero>,
<(<(T, Succ<U>) as Sub>::Diff, Succ<Succ<U>>) as Div>::Quotient,
) as Add>::Sum,
): Mul,
(Succ<T>, Succ<Succ<U>>): GreaterThanEq,
GreaterThanEq<T, U>,
Add<Succ<Zero>, Div<Sub<T, U>, Succ<U>>>,
): MulImpl,
(T, U): GreaterThanEqImpl,
{
// If x < y, return 0. We can do this by multiplying the "RawQuotient" by
// the bool->int value of this condition.
type Quotient = <(
<(Succ<T>, Succ<Succ<U>>) as GreaterThanEq>::Greater,
RawQuotient<T, U>,
) as Mul>::Product;
type Output = Mul<GreaterThanEq<Succ<T>, Succ<U>>, RawQuotient<T, U>>;
}

#[cfg(test)]
Expand All @@ -205,62 +175,48 @@ mod tests {

#[test]
fn addition() {
assert_eq!(<(encode!(), encode!()) as Add>::Sum::VALUE, 0);
assert_eq!(<(encode!(*), encode!()) as Add>::Sum::VALUE, 1);
assert_eq!(<(encode!(), encode!(*)) as Add>::Sum::VALUE, 1);
assert_eq!(<(encode!(**), encode!(***)) as Add>::Sum::VALUE, 5);
assert_eq!(Add::<encode!(), encode!()>::VALUE, 0);
assert_eq!(Add::<encode!(*), encode!()>::VALUE, 1);
assert_eq!(Add::<encode!(), encode!(*)>::VALUE, 1);
assert_eq!(Add::<encode!(**), encode!(***)>::VALUE, 5);
}

#[test]
fn subtraction() {
assert_eq!(<(encode!(), encode!()) as Sub>::Diff::VALUE, 0);
assert_eq!(<(encode!(*), encode!()) as Sub>::Diff::VALUE, 1);
assert_eq!(Sub::<encode!(), encode!()>::VALUE, 0);
assert_eq!(Sub::<encode!(*), encode!()>::VALUE, 1);
// Subtraction is saturating to make division easier
assert_eq!(<(encode!(), encode!(*)) as Sub>::Diff::VALUE, 0);
assert_eq!(<(encode!(***), encode!(**)) as Sub>::Diff::VALUE, 1);
assert_eq!(Sub::<encode!(), encode!(*)>::VALUE, 0);
assert_eq!(Sub::<encode!(***), encode!(**)>::VALUE, 1);
}

#[test]
fn multiplication() {
assert_eq!(<(encode!(), encode!()) as Mul>::Product::VALUE, 0);
assert_eq!(<(encode!(*), encode!()) as Mul>::Product::VALUE, 0);
assert_eq!(<(encode!(), encode!(*)) as Mul>::Product::VALUE, 0);
assert_eq!(<(encode!(*), encode!(*)) as Mul>::Product::VALUE, 1);
assert_eq!(<(encode!(**), encode!(***)) as Mul>::Product::VALUE, 6);
assert_eq!(Mul::<encode!(), encode!()>::VALUE, 0);
assert_eq!(Mul::<encode!(*), encode!()>::VALUE, 0);
assert_eq!(Mul::<encode!(), encode!(*)>::VALUE, 0);
assert_eq!(Mul::<encode!(*), encode!(*)>::VALUE, 1);
assert_eq!(Mul::<encode!(**), encode!(***)>::VALUE, 6);
}

#[test]
fn greater_than_eq() {
assert_eq!(<(encode!(), encode!()) as GreaterThanEq>::Greater::VALUE, 1);
assert_eq!(
<(encode!(*), encode!()) as GreaterThanEq>::Greater::VALUE,
1
);
assert_eq!(
<(encode!(), encode!(*)) as GreaterThanEq>::Greater::VALUE,
0
);
assert_eq!(
<(encode!(**), encode!(**)) as GreaterThanEq>::Greater::VALUE,
1
);
assert_eq!(
<(encode!(***), encode!(**)) as GreaterThanEq>::Greater::VALUE,
1
);
assert_eq!(GreaterThanEq::<encode!(), encode!()>::VALUE, 1);
assert_eq!(GreaterThanEq::<encode!(*), encode!()>::VALUE, 1);
assert_eq!(GreaterThanEq::<encode!(), encode!(*)>::VALUE, 0);
assert_eq!(GreaterThanEq::<encode!(**), encode!(**)>::VALUE, 1);
assert_eq!(GreaterThanEq::<encode!(***), encode!(**)>::VALUE, 1);
}

#[test]
fn division() {
// We define 0 / 0 as 0
assert_eq!(<(encode!(), encode!()) as Div>::Quotient::VALUE, 0);
// Gives a compiler error! We can't divide by 0! Such power.
// assert_eq!(<(church!(*), church!()) as Div>::Quotient::VALUE, 0);
assert_eq!(<(encode!(), encode!(*)) as Div>::Quotient::VALUE, 0);
assert_eq!(<(encode!(*), encode!(*)) as Div>::Quotient::VALUE, 1);
assert_eq!(<(encode!(**), encode!(***)) as Div>::Quotient::VALUE, 0);
assert_eq!(<(encode!(***), encode!(**)) as Div>::Quotient::VALUE, 1);
assert_eq!(<(encode!(******), encode!(**)) as Div>::Quotient::VALUE, 3);
assert_eq!(<(encode!(*******), encode!(**)) as Div>::Quotient::VALUE, 3);
// assert_eq!(Div::<encode!(*), encode!()>::VALUE, 0);
assert_eq!(Div::<encode!(), encode!(*)>::VALUE, 0);
assert_eq!(Div::<encode!(*), encode!(*)>::VALUE, 1);
assert_eq!(Div::<encode!(**), encode!(***)>::VALUE, 0);
assert_eq!(Div::<encode!(***), encode!(**)>::VALUE, 1);
assert_eq!(Div::<encode!(******), encode!(**)>::VALUE, 3);
assert_eq!(Div::<encode!(*******), encode!(**)>::VALUE, 3);
}
}