#!/usr/bin/python
# -*- encoding: utf8 -*-
'''
Created on 2018/02/28

@author: Timothée BERNARD (timothee.bernard@ens-lyon.org)
'''

# The code is mainly based on three classes (all subclasses of class Term): Variable, Application and Lambda

# What to do:
# A. Define the properties freeVariableNames and boundVariableNames
# B. Define the methods renameVariable and renameBoundVariable
# C. Define the method respectConvention (only in class Term; you will propably need newVariableName; at the end, use respectConventionAux for the recursion part)
# E. Define the method replace and the property isBetaRedex
# F. Define the method topLeftBetaReduction
# G. Define the method normalise (only in class Term)
# I. Define a class Constant (subclass of Term; it should be even simpler than Variable)
# J. Define a term for each of the following word: "Marie", "see", "John"
# K. Compute the meaning of "Marie sees John" and "John sees Marie"
# L. Define a term for each of the following word: "eat", "a", "all", "cake", "kid" (and maybe redefine the previous ones)
# M. Compute the meaning of "a/all kid(s) eats a/all cake(s)"

# Help on the set structure:
# Create an empty set: set()
# Create a singleton set (containing x): set([x])
# Set intersection: s1.intersection(s2)
# Set union: s1.union(s2)

variable = 0;
application = 1;
abstraction = 2;

# Abstract class
class Term:
	# Returns an alpha-equivalent term that respects the convention on variables
	def respectConvention(self, otherNames=set()):
		pass;
	
	# Tries to normalise the term (using a different strategy)
	def normalise(self):
		pass;
	
	# Returns the simplified string version (with less parentheses)
	def short(self):
		return self.shortAux(0);

# Returns a variable name similar to name one but not in others
def newVariableName(name, others):
	tmpName = name + '\'';
	while tmpName in others:
		tmpName = tmpName + '\'';
	
	return tmpName;

class Variable(Term):
	def __init__(self, name):
		self.name = name;
		
		self.type = variable;
		
		self.freeVariableNames = "à implémenter"; # The set of the names of the free variables that appear in the term
		self.boundVariableNames = "à implémenter"; # The set of the names of the bound variables that appear in the term
		
		self.isBetaRedex = "à implémenter"; # Whether the term is a beta-redex
	
	# Returns the term with all occurrences of the variable named oldName replaced with a variable named newName
	def renameVariable(self, oldName, newName):
		pass;
	
	# Returns the term with all bound occurrences of the variable named oldName (including the bounders) replaced with a variable named newName
	def renameBoundVariable(self, oldName, newName):
		pass;
	
	def respectConventionAux(self, variableNames):
		pass;
	
	# Returns the term obtained by replacing the variable x with t
	def replace(self, x, t):
		pass;
	
	# Returns the term obtained by performing the topmost leftmost beta-reduction in the term, in addition to a boolean indicating whether there was one to perform
	def topLeftBetaReduction(self):
		pass;
	
	# Full string version
	def __str__(self):
		return self.name;
	
	# Used to get the simplified string version (with less parentheses)
	def shortAux(self, level):
		return self.name;

class App(Term):
	def __init__(self, M, N):
		self.M = M;
		self.N = N;
		
		self.type = application;
		
		self.freeVariableNames = "à implémenter"; # The set of the names of the free variables that appear in the term
		self.boundVariableNames = "à implémenter"; # The set of the names of the bound variables that appear in the term
		
		self.isBetaRedex = "à implémenter"; # Whether the term is a beta-redex
	
	# Returns the term with all occurrences of the variable named oldName replaced with a variable named newName
	def renameVariable(self, oldName, newName):
		pass;
	
	# Returns the term with all bound occurrences of the variable named oldName (including the bounders) replaced with a variable named newName
	def renameBoundVariable(self, oldName, newName):
		pass;
	
	def respectConventionAux(self, variableNames):
		pass;
	
	# Returns the term obtained by replacing the variable x with t
	def replace(self, x, t):
		pass;
	
	# Returns the term obtained by performing the topmost leftmost beta-reduction in the term, in addition to a boolean indicating whether there was one to perform
	def topLeftBetaReduction(self):
		pass;
	
	# Full string version
	def __str__(self):
		return "(" + str(self.M) + str(self.N) + ")";
	
	# Used to get the simplified string version (with less parentheses)
	def shortAux(self, level):
		if(level <= 1):
			return self.M.shortAux(1) + self.N.shortAux(2);
		else:
			return "(" + self.M.shortAux(1) + self.N.shortAux(2) + ")";

class Lambda(Term):
	def __init__(self, x, M):
		self.var = x;
		self.body = M;
		
		self.type = abstraction;
		
		self.freeVariableNames = "à implémenter"; # The set of the names of the free variables that appear in the term
		self.boundVariableNames = "à implémenter"; # The set of the names of the bound variables that appear in the term
		
		self.isBetaRedex = "à implémenter"; # Whether the term is a beta-redex
	
	# Returns the term with all occurrences of the variable named oldName replaced with a variable named newName
	def renameVariable(self, oldName, newName):
		pass;
	
	# Returns the term with all bound occurrences of the variable named oldName (including the bounders) replaced with a variable named newName
	def renameBoundVariable(self, oldName, newName):
		pass;
	
	def respectConventionAux(self, variableNames):
		pass;
	
	# Returns the term obtained by replacing the variable x with t
	def replace(self, x, t):
		pass;
	
	# Returns the term obtained by performing the topmost leftmost beta-reduction in the term, in addition to a boolean indicating whether there was one to perform
	def topLeftBetaReduction(self):
		pass;
	
	# Full string version
	def __str__(self):
		return "(λ" + str(self.var) + "." + str(self.body) + ")";
	
	# Used to get the simplified string version (with less parentheses)
	def shortAux(self, level):
		if(level == 0):
			if(self.body.type == abstraction):
				return "λ" + self.var.shortAux(1) + self.body.shortAux(3);
			else:
				return "λ" + self.var.shortAux(1) + "." + self.body.shortAux(1);
		elif(level == 3):
			if(self.body.type == abstraction):
				return self.var.shortAux(1) + self.body.shortAux(3);
			else:
				return self.var.shortAux(1) + "." + self.body.shortAux(1);
		else:
			if(self.body.type == abstraction):
				return "(λ" + self.var.shortAux(1) + self.body.shortAux(3) + ")";
			else:
				return "(λ" + self.var.shortAux(1) + "." + self.body.shortAux(1) + ")";

varX = Variable("x");
varY = Variable("y");
varZ = Variable("z");
varF = Variable("f");
varM = Variable("m");
varN = Variable("n");
varP = Variable("p");

def test(t):
	print "string:", t;
	print "short string:", t.short();
	print "free variables:", t.freeVariableNames;
	print "bound variables:", t.boundVariableNames;
	print "respectConvention:", t.respectConvention()#.short();
	print "normalise:", t.normalise()#.short();
	print;

t1 = Lambda(varX, App(varX, varY));
test(t1);

t2 = App(t1, varZ)
test(t2);

t3 = App(Lambda(varX, App(varX, App(varY, varZ))), Lambda(varZ, varY));
test(t3);

t4 = Lambda(varX,  App(varX, varX))
t5 = App(t4, t4);
test(t5);

t6 = App(Lambda(varX, Lambda(varY, App(varX, varY))), varY);
test(t6);

t7 = App(varY, t6);
test(t7);

t8 = Lambda(varX, App(Lambda(varZ, Lambda(varX, varY)), varX));
test(t8);