package coffee.liz.lambda.bind;

import coffee.liz.lambda.ast.Expression;
import coffee.liz.lambda.ast.Expression.IdentifierExpression;
import coffee.liz.lambda.ast.Expression.AbstractionExpression;
import coffee.liz.lambda.ast.Expression.ApplicationExpression;
import coffee.liz.lambda.ast.SourceSpan;
import coffee.liz.lambda.eval.Environment;

import java.util.Optional;
import coffee.liz.lambda.eval.Value;
import coffee.liz.lambda.eval.Value.Free;
import coffee.liz.lambda.eval.Value.Closure;
import lombok.Getter;

/**
 * Converts an integer to its Church numeral representation.
 *
 * <p>
 * Church numerals encode n as {@code λf.λx.f(f(...f(x)...))} with n
 * applications of f.
 */
@Getter
public class ToChurch implements ExternalBinding {
	private final String name = "ToChurch";

	/**
	 * Converts a free variable containing an integer string to a Church numeral.
	 *
	 * @param env
	 *            the current environment
	 * @param val
	 *            a Free value whose name is an integer string
	 * @return a Closure representing the Church numeral
	 */
	@Override
	public Value apply(final Environment env, final Value val) {
		final Free free = (Free) val;
		final int n = Integer.parseInt(free.name());

		Expression body = new IdentifierExpression(Optional.empty(), SourceSpan.UNKNOWN, "x");
		for (int i = 0; i < n; i++) {
			body = new ApplicationExpression(Optional.empty(), SourceSpan.UNKNOWN,
					new IdentifierExpression(Optional.empty(), SourceSpan.UNKNOWN, "f"), body);
		}

		return new Closure(env, "f", new AbstractionExpression(Optional.empty(), SourceSpan.UNKNOWN, "x", body));
	}
}