#ifndef __LAMBDA_HPP__
#define __LAMBDA_HPP__

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

class LambdaExpression {
 public:
	virtual ~LambdaExpression() {}

	// ispisuje lambda izraz na standardni izlaz
	virtual void print() const = 0;

	// Kreira kopiju lambda izraza
	virtual LambdaExpression* clone() = 0;

	// Kreira nov lambda izraz dobijen zamenom svih pojavljivanja promenljive var izrazom s
	virtual LambdaExpression* substitute(string var, LambdaExpression* s) = 0;

	// Vrsi jedan korak beta redukcije. 
	// Rezultat je novi lambda izraz koji se vraca preko argumenta e. 
	// Vraca true ukoliko je rezultat redukcije e razlicit od polaznog izraza
	virtual bool betaReduction(LambdaExpression*& e) = 0;

	// Proverava da li dati izraz sadrzi slobodno pojavljivanje date promenljive
	virtual bool containsFreeVariable(const string& var) = 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 betaReduction(LambdaExpression*& e) {
		e = clone();	
		return false;
	}

	bool containsFreeVariable(const string& var) {
		return var == _name;
	}

 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 betaReduction(LambdaExpression*& e) {
		e = clone();	
		return false;
	}

	bool containsFreeVariable(const string& var) {
		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;
	}

	bool containsFreeVariable(const string& var) {
		return _op1->containsFreeVariable(var) || _op2->containsFreeVariable(var);
	}

 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 betaReduction(LambdaExpression*& e) {
		e = clone();	
		return false;
	}
};


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

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

	~Abstraction() {
		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) {
		if (s->containsFreeVariable(_var)) {
			string freshVar = _var + "'";
			LambdaExpression* renamed = new Abstraction(freshVar , _op->substitute(_var, new Variable(freshVar)));
			LambdaExpression* result = renamed->substitute(var, s);
			delete renamed;
			return result;
		} else {
			return new Abstraction(_var, _op->substitute(var, s));
		}
	}

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

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

	bool containsFreeVariable(const string& var) {
		return var != _var && _op->containsFreeVariable(var);
	}

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

#endif
