peano.rs

#![recursion_limit = "1280"]

use std::marker::PhantomData;

struct Zero;

struct Succ<T> {
    pred: PhantomData<T>,
}

trait KnownNat {
    fn as_i64() -> i64;
}

impl KnownNat for Zero {
    fn as_i64() -> i64 {
        0
    }
}

type N0 = Zero;
type N1 = Succ<N0>;
type N2 = Succ<N1>;
type N3 = Succ<N2>;
type N4 = Succ<N3>;
type N5 = Succ<N4>;

impl<T: KnownNat> KnownNat for Succ<T> {
    fn as_i64() -> i64 {
        T::as_i64() + 1
    }
}

trait Add_<Rhs> {
    type Output;
}

impl<Rhs> Add_<Rhs> for Zero {
    type Output = Rhs;
}

impl<T, Rhs> Add_<Rhs> for Succ<T>
where
    T: Add_<Rhs>,
{
    type Output = Succ<<T as Add_<Rhs>>::Output>;
}

trait Sub_<Rhs> {
    type Output;
}

impl<Lhs> Sub_<Zero> for Lhs {
    type Output = Lhs;
}

impl<T, Rhs> Sub_<Succ<Rhs>> for Succ<T>
where
    T: Sub_<Rhs>,
{
    type Output = <T as Sub_<Rhs>>::Output;
}

trait Mul_<Rhs> {
    type Output;
}

impl<Lhs> Mul_<Zero> for Lhs {
    type Output = Zero;
}

impl<T, Rhs> Mul_<Succ<Rhs>> for T
where
    T: Mul_<Rhs>,
    T::Output: Add_<T>,
{
    type Output = <<T as Mul_<Rhs>>::Output as Add_<T>>::Output;
}

type Add<L, R> = <L as Add_<R>>::Output;
type Sub<L, R> = <L as Sub_<R>>::Output;
type Mul<L, R> = <L as Mul_<R>>::Output;


fn main() {
    assert_eq!(N0::as_i64(), 0);
    assert_eq!(N3::as_i64(), 3);

    assert_eq!(<Add<N0, N2>>::as_i64(), 2);
    assert_eq!(<Add<N4, N2>>::as_i64(), 6);

    assert_eq!(<Sub<N3, N0>>::as_i64(), 3);
    assert_eq!(<Sub<N3, N1>>::as_i64(), 2);
    assert_eq!(<Sub<N5, N2>>::as_i64(), 3);

    assert_eq!(<Mul<N0, N4>>::as_i64(), 0);
    assert_eq!(<Mul<N2, N0>>::as_i64(), 0);
    assert_eq!(<Mul<N2, N5>>::as_i64(), 10);
    assert_eq!(<Mul<N5, N5>>::as_i64(), 25);

    assert_eq!(<Mul<Mul<Sub<N5, N1>, Add<N5, N3>>, N5>>::as_i64(), 160);
    println!("{}", <Mul<Mul<Sub<N5, N1>, Add<N5, N3>>, N5>>::as_i64());
}

xx.asm

$ cargo asm typed_test::main
typed_test::main:
 push    rbp
 mov     rbp, rsp
 sub     rsp, 80
 mov     qword, ptr, [rbp, -, 8], 160
 lea     rax, [rbp, -, 8]
 mov     qword, ptr, [rbp, -, 24], rax
 mov     rax, qword, ptr, [rip, +, __ZN4core3fmt3num3imp52_$LT$impl$u20$core..fmt..Display$u20$for$u20$i64$GT$3fmt17h06143d8b2239fee6E@GOTPCREL]
 mov     qword, ptr, [rbp, -, 16], rax
 lea     rax, [rip, +, l___unnamed_2]
 mov     qword, ptr, [rbp, -, 72], rax
 mov     qword, ptr, [rbp, -, 64], 2
 mov     qword, ptr, [rbp, -, 56], 0
 lea     rax, [rbp, -, 24]
 mov     qword, ptr, [rbp, -, 40], rax
 mov     qword, ptr, [rbp, -, 32], 1
 lea     rdi, [rbp, -, 72]
 call    std::io::stdio::_print
 add     rsp, 80
 pop     rbp
 ret