// pattern matching and type arithmetic in C++
// see https://en.wikipedia.org/wiki/Peano_axioms
// see https://en.wikipedia.org/wiki/Successor_function

// compile and test: "c++ peano.cpp -o peano && ./peano"

//
// zero is our first natural number
//

struct zero {};

//
// all other natural numbers are either a successor of zero
// or a successor of another successor
//

template<class> // let's forget that type (see ::sum below)
struct successor {};

//
// sum = first + second
//

// non-empty declaration: this is the end of the recursion
// (second is zero)
template<class first, class second>
struct sum {
    using type = first;
};

// recursive specialization
// the pattern "successor<second>" isn't matching zero
// and is giving us the type of the predecessor we
// forgot in the declaration of ::successor
template<class first, class second>
struct sum<first, successor<second>> {
    // second is decremented by pattern matching
    using recursion = typename sum<first, second>::type;
    // and the result is incremented
    using type = successor<recursion>;
};

//
// product = multiplicand * multiplier
//

// non-empty declaration: this is the end of the recursion
// (multiplier is zero)
template<class multiplicand, class multiplier>
struct product {
    using type = zero;
};

// recursive specialization when multiplier isn't zero
template<class multiplicand, class multiplier>
struct product<multiplicand, successor<multiplier>> {
    using recursion = typename product<multiplicand, multiplier>::type;
    using type = typename sum<multiplicand, recursion>::type;
};

//
// difference = minuend - subtrahend
//

// empty declaration: compilation error if the result is negative
template<class minuend, class subtrahend>
struct difference {
};

// end of the recursion
template<class minuend>
struct difference<minuend, zero> {
    using type = minuend;
};

// recursive specialization
template<class minuend, class subtrahend>
struct difference<successor<minuend>, successor<subtrahend>> {
    using recursion = difference<minuend, subtrahend>;
    using type = typename recursion::type;
};

//
// quotient, remainder = dividend / divisor
//

namespace impl {

    // NOTE: for the division, we decrement divisor and
    // increment _remainder until divisor is zero, at
    // this point we increment the result, swap _remainder
    // with divisor to restore its value, until dividend is
    // zero and _remainder is the final remainder

    // empty declaration: compilation error when dividing by zero
    template<class dividend, class divisor, class _remainder>
    struct quotient {
    };

    // specialization when the dividend is zero, this is the end
    // of the recursion when the remainder isn't zero
    template<class divisor, class _remainder>
    struct quotient<zero, divisor, _remainder> {
        using type = zero;
        using remainder = _remainder;
    };

    // specialization when both dividend and divisor are zero,
    // the result is incremented and this is the end of the
    // recursion when the remainder is zero
    template<class _remainder>
    struct quotient<zero, zero, successor<_remainder>> {
        using type = successor<zero>;
        using remainder = zero;
    };

    // recursive specialization when divisor is zero
    // the result is incremented and divisor is restored
    // from _remainder
    template<class dividend, class _remainder>
    struct quotient<dividend, zero, successor<_remainder>> {
        using recursion = quotient<dividend, successor<_remainder>, zero>;
        using type = successor<typename recursion::type>;
        using remainder = typename recursion::remainder;
    };

    // recursive specialization
    template<class dividend, class divisor, class _remainder>
    struct quotient<successor<dividend>, successor<divisor>, _remainder> {
        using recursion = quotient<dividend, divisor, successor<_remainder>>;
        using type = typename recursion::type;
        using remainder = typename recursion::remainder;
    };

} // namespace impl

// let's hide the third parameter
template<class dividend, class divisor>
using quotient = impl::quotient<dividend, divisor, zero>;

//
// natural_to_peano: convert from unsigned integer
//

template<unsigned natural>
struct natural_to_peano {
    using recursion = typename natural_to_peano<natural - 1u>::type;
    using type = successor<recursion>;
};

template<>
struct natural_to_peano<0u> {
    using type = zero;
};

//
// peano_to_natural: convert to unsigned integer
//

template<class>
struct peano_to_natural {
    enum : unsigned { value = 0u };
};

template<class type>
struct peano_to_natural<successor<type>> {
    enum : unsigned {
        recursion = peano_to_natural<type>::value,
        value = recursion + 1u
    };
};

//
// now let's test!
//

#include <cstdio>

int main () {
    using four = natural_to_peano<4u>::type;
    using six = natural_to_peano<6u>::type;
    using ten = sum<six, four>::type;
    using fourty = product<ten, four>::type;
    using thirty_four = difference<fourty, six>::type;

    // output: thirty_four = 34
    printf("thirty_four = %u\n",
        peano_to_natural<thirty_four>::value);

 	// compilation error
    // using negative_difference = difference<four, six>::type;

    using fourty_over_ten = quotient<fourty, ten>;
    using thirty_four_over_ten = quotient<thirty_four, ten>;

    // compilation errors:
    // using divide_by_zero = quotient<four, zero>;
    // printf("divide_by_zero = %u, %u\n",
    // 	peano_to_natural<typename divide_by_zero::type>::value,
    // 	peano_to_natural<typename divide_by_zero::remainder>::value);

    // output: fourty_over_ten = 4, 0
    printf("fourty_over_ten = %u, %u\n",
        peano_to_natural<typename fourty_over_ten::type>::value,
        peano_to_natural<typename fourty_over_ten::remainder>::value);

    // output: thirty_four_over_ten = 3, 4
    printf("thirty_four_over_ten = %u, %u\n",
        peano_to_natural<typename thirty_four_over_ten::type>::value,
        peano_to_natural<typename thirty_four_over_ten::remainder>::value);

    return 0;
}