package de.renew.expression;

import de.renew.unify.ICalculationChecker;
import de.renew.unify.IStateRecorder;
import de.renew.unify.Impossible;
import de.renew.unify.Notifiable;
import de.renew.unify.Unify;
import de.renew.unify.Variable;


/**
 * An {@code InvertibleExpression} is an expression that represents a function call that is invertible, meaning that
 * the called function has an inverse function, so that unification of its argument's value and the return value
 * can happen in both directions.
 */
public class InvertibleExpression extends ExpressionWithTypeField {
    /**
     * The {@code Expression} whose value will be used as the argument of {@link #_forwardFunction}.
     * Multiple arguments are modelled by an expression that returns
     * a tuple that is processed by a function.
     */
    private final Expression _argument;
    /**
     * The {@code Function} that is applied to the value of {@link #_argument} upon evaluation.
     */
    private final Function _forwardFunction;
    /**
     * The inverse {@code Function} of {@link #_forwardFunction}. This means that for all values of {@link #_argument},
     * {@code value==backwardFunction(forwardFunction(value))} is {@code true}.
     */
    private final Function _backwardFunction;

    /**
     * Constructs a new {@code InvertibleExpression} based on a {@code Class}, the argument {@code Expression}, a
     * {@code Function} and its inverse {@code Function}.
     *
     * @param targetType the type of the {@code GuardExpression}'s value
     * @param argument the {@code Expression} on whose value {@code forwardFunction} is called during evaluation
     * @param forwardFunction the {@code Function} that will be called on the value of {@code argument}
     * @param backwardFunction the inverse {@code Function} of {@code forwardFunction}
     */
    public InvertibleExpression(
        Class<?> targetType, Expression argument, Function forwardFunction,
        Function backwardFunction)
    {
        super(targetType);
        _argument = argument;
        _forwardFunction = forwardFunction;
        _backwardFunction = backwardFunction;
    }

    @Override
    public boolean isInvertible() {
        return _argument.isInvertible();
    }

    /**
    * Gets the {@code Expression} that evaluates to the forward function's argument.
    * @return the {@code Expression} that evaluates to the forward function's argument
    */
    public Expression getArgument() {
        return _argument;
    }

    @Override
    public Object startEvaluation(
        VariableMapper mapper, IStateRecorder recorder, ICalculationChecker checker)
        throws Impossible
    {
        final Variable source =
            new Variable(_argument.startEvaluation(mapper, recorder, checker), recorder);
        final Variable target = new Variable();

        if (checker != null) {
            checker.addEarlyVariable(source, recorder);
        }

        Notifiable sourceListener = new Notifiable() {
            @Override
            public void boundNotify(IStateRecorder irecorder) throws Impossible {
                if (Unify.isBound(source)) {
                    Unify.unify(target, _forwardFunction.function(source.getValue()), irecorder);
                }
            }
        };
        source.addListener(sourceListener, recorder);

        Notifiable targetListener = new Notifiable() {
            @Override
            public void boundNotify(IStateRecorder irecorder) throws Impossible {
                if (Unify.isBound(target)) {
                    Unify.unify(source, _backwardFunction.function(target.getValue()), irecorder);
                }
            }
        };
        target.addListener(targetListener, recorder);

        return target.getValue();
    }

    @Override
    public Object registerCalculation(
        VariableMapper mapper, IStateRecorder recorder, ICalculationChecker checker)
        throws Impossible
    {
        Variable source =
            new Variable(_argument.registerCalculation(mapper, recorder, checker), recorder);
        Variable target = new Variable();

        checker.addLateVariable(source, recorder);
        checker.addCalculated(getType(), target, source.getValue(), recorder);

        return target.getValue();
    }

    @Override
    public String toString() {
        return "InvertibleExpr(" + de.renew.util.Types.typeToString(getType()) + ": "
            + _forwardFunction + ", " + _backwardFunction + ", " + _argument + ")";
    }
}