// 	An illustration of an extreme static type system
// 			x/0 is a type error
//
// The present code implements a type system which assigns a distinct
// type to every number. The compiler can infer these specific types for
// results of arithmetic expressions. This can help the compiler catch
// _all_ the errors. In particular, an expression whose evaluation
// includes a division by zero is flagged by the _compiler_ as mistyped.
// This static type system is as specific as it can ever be.
// 
// The present code also shows C++ compiler as a term-rewriting engine --
// an interpreter of untyped lambda-calculus over type identifiers.
//
// The code defines rules of the type arithmetics (addition, subtraction,
// and division) of integers represented as types. It then computes
// and prints out the result of an expression (3*x+1)/(x-1) for x=4.
// To be precise, the program prints out the value corresponding to the
// type of that expression.
// See a web site
//	http://pobox.com/~oleg/ftp/Computation/type-arithmetics.html
// for more details.
// 
// This code is self-contained. You can run it as
// 	g++ lambda-interp.cc -o lambda-interp
// 	./lambda-interp
//
// Or, to specify your own value of x, for example, 3,
// 	g++ -DARG1=3 lambda-interp.cc -o lambda-interp
// 	./lambda-interp
// To include a statement that attempts to _eventually_ perform division
// by zero, compile the code as:
// 	g++ -DARG1=1 lambda-interp.cc -o lambda-interp
// 
// The compiler finds a type error in that statement. Therefore, the
// compilation fails, and no object file (let alone executable) is
// produced.
//
// This code was compiled with egcs-2.91.66 and g++ 2.95.2
// on FreeBSD 3.2-4.0 and Linux 2.2.x
// Any C++ compiler that is able to perform a partial template instantiation
// will do.
// 
// $Id: lambda-interp.cc,v 2.5 2000/08/26 00:23:47 oleg Exp oleg $	

#include <stdio.h>


// Three base types of our static type system 
class Zero {
  public: enum { value = 0 };
  int eval(void) const { return value; }
};

template<class T> class Succ {
  public: enum { value = T::value + 1 };
  int eval(void) const { return value; }
};

template<class T> class Neg {
  public: enum { value = - T::value };
  int eval(void) const { return value; }
};


// The following classes define type inference rules for an addition operation
// Note that these classes have no members -- they merely specify
// inference rules for our (type) term re-writing

template<typename T1, typename T2>
struct Add {			// Traits class
};

				// (a+1) + (b+1) ==> a + (b + 1 + 1)
template<typename T1, typename T2>
struct Add<Succ<T1>, Succ<T2> > {
  typedef typename Add<T1, Succ<Succ<T2> > >::sum sum;
};

template<typename T>
struct Add<Zero,T> {		// 0 + a ==> a
  typedef T sum;
};

template<typename T>
struct Add<Neg<Zero>,T> {
  typedef T sum;
};

template<typename T>
struct Add<T, Zero> {
  typedef T sum;
};

template<typename T>
struct Add<T, Neg<Zero> > {
  typedef T sum;
};

struct Add<Zero, Zero> {	// 0 + 0 ==> 0
  typedef Zero sum;
};

				// (a+1) + (- (b + 1 + 1)) ==> a + (- (b + 1))
template<typename T1, typename T2>
struct Add<Succ<T1>, Neg<Succ<Succ<T2> > > > {
  typedef typename Add<T1, Neg<Succ<T2> > >::sum sum;
};

				// (a+1) + (- (0 + 1)) ==> a + 0
template<typename T>
struct Add<Succ<T>, Neg<Succ<Zero > > > {
  typedef typename Add<T,Zero>::sum sum;
};

				// (- a) + (- b) ==> - (a + b)
template<typename T1, typename T2>
struct Add<Neg<T1>, Neg<T2> > {
  typedef typename Add<T1, T2>::sum sum_abs;
  typedef Neg<sum_abs> sum;
};

				// (- a) + b ==> b + (- a)
template<typename T1, typename T2>
struct Add<Neg<T1>, T2 > {
  typedef typename Add<T2, Neg<T1> >::sum sum;
};


// Negation, addition, and subtraction operations themselves
// (appropriately typed!)

template <typename T> Neg<Succ<T> >
neg(Succ<T>) { return Neg<Succ<T> > (); }
Zero neg(Zero t) { return t; }

template <typename T1, typename T2>
typename Add<T1,T2>::sum add(T1, T2)
{
  typename Add<T1,T2>::sum c;
  return c;
}

template <typename T1, typename T2>
typename Add<T1,Neg<T2> >::sum sub(T1, T2)
{
  typename Add<T1,Neg<T2> >::sum c;
  return c;
}


// The following classes define type inference rules for a division operation

template<typename T1, typename T2>
struct Div {			// Traits class
};

				// a / (- b) ==> - (a/b)
template<typename T1, typename T2>
struct Div<T1, Neg<T2> > {
  typedef typename Div<T1, T2>::ratio ratio_abs;
  typedef Neg<ratio_abs> ratio;
};

				// (- a) / b ==> - (a/b)
template<typename T1, typename T2>
struct Div<Neg<T1>, T2 > {
  typedef typename Div<T1, T2>::ratio ratio_abs;
  typedef Neg<ratio_abs> ratio;
};

				// (- a) / (- b) ==> a/b
template<typename T1, typename T2>
struct Div<Neg<T1>, Neg<T2> > {
  typedef typename Div<T1, T2>::ratio ratio;
};

				// a / 1 ==> a
template<typename T>
struct Div<T, Succ<Zero> > {
  typedef T ratio;
};


// "Perform" division by repeated subtractions of the Divisor from
// the Dividend, until the result becomes Zero or Negative.
// Ratio counts the number of the subtractions performed.

template<typename Dividend, typename Divisor, typename Ratio>
struct DivEval {                     // Traits class
};

template<typename Divisor, typename Ratio>
struct DivEval<Zero, Divisor, Ratio>  {
  typedef Ratio value;
};

template<typename T, typename Divisor, typename Ratio>
struct DivEval<Neg<T>, Divisor, Ratio> {
  typedef typename Add<Ratio, Neg<Succ<Zero> > >::sum value;
};

template<typename Dividend, typename Divisor, typename Ratio>
struct DivEval<Succ<Dividend>, Divisor, Ratio> {
  typedef typename Add< Succ<Dividend>, Neg<Divisor> >::sum new_dividend;
  typedef typename DivEval< new_dividend, Divisor, Succ<Ratio> >::value value;
};

template<typename T1, typename T2>
struct Div<T1, Succ<T2> > {
  typedef typename DivEval<T1, Succ<T2>, Zero>::value ratio;
};

// Division operation itself (appropriately typed!)

template <typename T1, typename T2>
typename Div<T1,T2>::ratio div(T1, T2)
{
  typename Div<T1,T2>::ratio c;
  return c;
}

// An example of complex, "user-defined functions"
// (or, user-defined type constructors to be precise).
// In this example, we will be computing (3*x+1)/(x-1), with the help of a
// "temporary type variables"

#if 0
	// The following is a type constructor that computes (3*x+1)
	// It corresponds to the following sequence in the value arithemtics:
	// val y = x + x;
	// val z = y + x;
	// return z + 1;
template<typename x> struct Foo {
  typedef typename Add<x,x>::sum y;
  typedef typename Add<y,x>::sum z;
  typedef typename Add<z,Succ<Zero> >::sum result;
};
#endif

#if 1
	// The following is a type constructor that computes (3*x+1)
	// It is set to emulate an expression:
	//	let y = x + x in let z = y + x in z + 1
template<typename x> struct Foo {
  template<typename y> struct body {
    template<typename z> struct body2 {
      typedef typename Add<z,Succ<Zero> >::sum result;
    };
    typedef typename body2<typename Add<y,x>::sum>::result result;
  };
  typedef typename body<typename Add<x,x>::sum>::result result;
};
#endif

#if 0
		// The following evaluates "let var = exp in body;"
		// It was a great idea, but it doesn't work out:
		// the C preprocessor can't handle embedded commas
#define XY(X,Y) X##Y
#define MakeNameXY(FX,LINE) XY(FX,LINE)
#define MakeName(FX) MakeNameXY(FX,__LINE__)

#define LET(var,exp,body) \
  template <typename var> struct MakeName(__BODY__##var) { \
    typedef typename body result; }; \
  typedef typename MakeName(__BODY__##var) <typename exp>:: result result;


	// The following is a function that computes (3*x+1)
	// It is set to emulate an expression:
	//	let y = x + x in let y = y + x in y + 1;
	// even more closely
template<typename x> struct Foo {
  LET(y,Add<x,x>::sum,
      LET(y,Add<y,x>::sum,Add<y,Succ<Zero> >::sum));
};
#endif		// of the great unworkable idea

	// The following type constructor computes Foo(x)/(x-1)
template<typename x> struct Bar {
  typedef typename Foo<x>::result y;
  typedef typename Add<x,Neg<Succ<Zero> > >::sum d;
  typedef typename Div<y,d>::ratio result;
};



// The following is a converter from a "value" to a "type"
// Use it in the context
// type_of(val).type or "typename type_of(val).type"
template<typename T> struct TypeOf {
  typedef T result;
  result type;
  TypeOf(T x) {}
};

template<typename T> TypeOf<T> type_of(T x) { return x; }


// The following "functions" that "convert a value to a type"
// aren't strictly necessary.
// if classes Foo and Bar contained the following
// template <typename x> struct Foo { ...; Foo(x _x) {} result type; };
// The one could write
// SHOWVAL( Foo(two).type )

template<typename TX>
typename Foo<TX>::result foo(TX)
{
  Foo<TX>::result type;
  return type;
}

template<typename TX>
typename Bar<TX>::result bar(TX)
{
  Bar<TX>::result type;
  return type;
}


	// Convert a natural number to a "unary" notation as a sequence of
	// Succ _type constructors_ applied to a Zero type constructor.
	// This function converts a value to a "type"
	// In a sense it is equivalent to a getInt function
	// that is present in some languages...
template<int N> struct Peanoizer {
  typedef Succ<typename Peanoizer<N-1>::result> result;
  result type;
};
struct Peanoizer<0> {
  typedef Zero result;
  result type;
};


// The root module

#define SHOWVAL(X) printf("The value of " #X " is: %d\n", X .eval())

// ARG1 is better defined as -DARG1 command-line option to the compiler
#if !defined(ARG1)
#define ARG1 4
#endif

int main()
{
  Succ<Succ<Zero> > two;
  Succ<Zero> one;

  printf("\nType arithmetics: computing bar(x) = (3*x+1)/(x-1)\n");
  SHOWVAL( bar(two) );
  SHOWVAL( bar(add(two,one)) );
  SHOWVAL( Peanoizer<ARG1>().type );
  SHOWVAL( bar( Peanoizer<ARG1>().type ) );
  // SHOWVAL( bar(add(one,one)) );
  // SHOWVAL( foo(two) );
  // SHOWVAL( bar(two) );
  // SHOWVAL( bar(add(two,one)) );


#if 0 
  // Old tests
  SHOWVAL( two );
  SHOWVAL( neg(two) ); 
  SHOWVAL( add(one,two) );
  SHOWVAL( add(neg(one),two) );
  SHOWVAL( add(neg(one),neg(two)) );
  SHOWVAL( add(two,neg(two)) );
  SHOWVAL( add(neg(two),neg(two)) );
  SHOWVAL( add(neg(two),two) );
  SHOWVAL( div(one,two) );
  SHOWVAL( div(two,one) );
  SHOWVAL( div(add(one,add(two,two)),add(div(two,two),one)) );
#if defined(TRYDIV0)
  SHOWVAL( div(add(two,two),add(div(two,two),neg(one))) );
#endif
#endif
}