Skip to content

Instantly share code, notes, and snippets.

@philopon
Last active May 29, 2019 12:27
Show Gist options
  • Save philopon/b59a4adff7bd12800ba41faca7f572af to your computer and use it in GitHub Desktop.
Save philopon/b59a4adff7bd12800ba41faca7f572af to your computer and use it in GitHub Desktop.
#![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());
}
$ 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment