#ifndef __LAMBDA_HPP__
#define __LAMBDA_HPP__

#include <string>
#include <iostream>
using namespace std;

class LambdaExpression {
 public:
	virtual ~LambdaExpression() {}
	virtual void print() const = 0;
	virtual LambdaExpression* clone() = 0;
	virtual LambdaExpression* substitute(string var, LambdaExpression* s) = 0;
	virtual bool betaConversion(LambdaExpression*& e) = 0;
};

class Variable : public LambdaExpression {
 public:
	Variable(string name) 
		: _name(name) {
	}

	LambdaExpression* clone() {
		return new Variable(*this);
	}

	void print() const {
		cout << _name;
	}

	
	LambdaExpression* substitute(string var, LambdaExpression* s) {
		return var == _name ? s->clone() : clone();
	}

	bool betaConversion(LambdaExpression*& e) {
		e = clone();	
		return false;
	}

 private:
	string _name;
};

class Constant : public LambdaExpression {
  public:
	Constant(int value)
		: _value(value) {
	}

	LambdaExpression* clone() {
		return new Constant(*this);
	}

	void print() const {
		cout << _value;
	}

	LambdaExpression* substitute(string var, LambdaExpression* s) {
		return clone();
	}
	

	bool betaConversion(LambdaExpression*& e) {
		e = clone();	
		return false;
	}

  private:
	int _value;
};


class BinaryOperator : public LambdaExpression {
 public:
	BinaryOperator(LambdaExpression* op1, LambdaExpression* op2) 
		: _op1(op1), _op2(op2) {
	}

	BinaryOperator(const BinaryOperator& o)
		: _op1(o._op1->clone()), _op2(o._op2->clone()) {
	}

	~BinaryOperator() {
		delete _op1;
		delete _op2;
	}

 protected:
	LambdaExpression *_op1, *_op2;  
};

class Plus : public BinaryOperator {
 public:
	Plus(LambdaExpression* op1, LambdaExpression* op2) 
		: BinaryOperator(op1, op2) {
	}

	LambdaExpression* clone() {
		return new Plus(*this);
	}

	void print() const {
		_op1->print();
		cout << " + ";
		_op2->print();
	}

	LambdaExpression* substitute(string var, LambdaExpression* s) {
		return new Plus(_op1->substitute(var, s), _op2->substitute(var, s));
	}

	bool betaConversion(LambdaExpression*& e) {
		e = clone();	
		return false;
	}
};


class LambdaAbstraction : public LambdaExpression {
 public:
	LambdaAbstraction(string var, LambdaExpression* op) 
		: _var(var), _op(op) {
	}

	LambdaAbstraction(const LambdaAbstraction& l) 
		: _var(l._var), _op(l._op->clone()) {
	}

	~LambdaAbstraction() {
		delete _op;
	}

	void print() const {
		cout << "(%" << _var << ". ";
		_op->print();
		cout << ")";
	}

	LambdaExpression* apply(LambdaExpression* s) {
		return _op->substitute(_var, s);
	}

	LambdaExpression* substitute(string var, LambdaExpression* s) {
		return new LambdaAbstraction(_var, _op->substitute(var, s));
	}

	LambdaExpression* clone() {
		return new LambdaAbstraction(*this);
	}

	bool betaConversion(LambdaExpression*& e) {
		LambdaExpression* t;
		bool r = _op->betaConversion(t); 
		e = new LambdaAbstraction(_var, t);
		return r;
	}

 private:
	string _var;
	LambdaExpression* _op;	
};



class Application : public BinaryOperator {
 public:
	Application(LambdaExpression* op1, LambdaExpression* op2) 
		: BinaryOperator(op1, op2) {
	}
	
	void print() const {
		cout << "(";
		_op1->print();
		cout << " ";
		_op2->print();
		cout << ")";
	}

	LambdaExpression* substitute(string var, LambdaExpression* s) {
		return new Application(_op1->substitute(var, s), _op2->substitute(var, s));
	}

	bool betaConversion(LambdaExpression*& e) {
		LambdaAbstraction* la = dynamic_cast<LambdaAbstraction*>(_op1);
		if (la == 0)  {
			LambdaExpression *e1, *e2;
			bool r1 = _op1->betaConversion(e1);
			bool r2 = _op2->betaConversion(e2);
			e = new Application(e1, e2);
			return r1 || r2;
		}
		else {
			e = la->apply(_op2);
			return true;
		}
	}
	
	LambdaExpression* clone() {
		return new Application(*this);
	}
};
		

#endif
