package de.renew.formalism.bool;

import java.util.Iterator;
import java.util.Vector;

import de.renew.expression.CallExpression;
import de.renew.expression.ConstantExpression;
import de.renew.expression.EqualsExpression;
import de.renew.expression.Expression;
import de.renew.expression.Function;
import de.renew.expression.LocalVariable;
import de.renew.expression.TupleExpression;
import de.renew.expression.VariableExpression;
import de.renew.formalism.function.BasicFunction;
import de.renew.net.ConstantTokenSource;
import de.renew.net.Net;
import de.renew.net.NetElementID;
import de.renew.net.Place;
import de.renew.net.Transition;
import de.renew.net.inscription.arc.Arc;
import de.renew.net.inscription.transition.ExpressionInscription;
import de.renew.net.inscription.transition.GuardInscription;
import de.renew.net.inscription.transition.RangeEnumeratorInscription;
import de.renew.net.loading.NetLoader;
import de.renew.shadowcompiler.ShadowCompiler;
import de.renew.shadowcompiler.ShadowLookup;
import de.renew.shadowcompiler.ShadowPreprocessor;
import de.renew.simulatorontology.shadow.ShadowArc;
import de.renew.simulatorontology.shadow.ShadowInscription;
import de.renew.simulatorontology.shadow.ShadowNet;
import de.renew.simulatorontology.shadow.ShadowNetElement;
import de.renew.simulatorontology.shadow.ShadowPlace;
import de.renew.simulatorontology.shadow.ShadowTransition;
import de.renew.simulatorontology.shadow.SyntaxException;
import de.renew.util.StringUtil;
import de.renew.util.Types;
import de.renew.util.Value;


/**
 * This class compiles a SingleBoolNet.
 * Therefore it compiles all Places, Transitions and the whole Net.
 */
public class SingleBoolNetCompiler implements ShadowCompiler {
    private static final Value VALUE_0 = new Value(0);
    private static final Value VALUE_1 = new Value(1);
    private static final Expression EXPR_0 = new ConstantExpression(Types.UNTYPED, VALUE_0);
    private static final Expression EXPR_1 = new ConstantExpression(Types.UNTYPED, VALUE_1);
    private static final LocalVariable LOCAL_VAR_ACT = new LocalVariable("act");
    private static final VariableExpression LOC_VAR_EXPR_ACT =
        new VariableExpression(Types.UNTYPED, LOCAL_VAR_ACT);
    private int _placeNum;
    private int _transNum;
    private int _varNum;
    private ShadowLookup _lookup;

    @Override
    public void setLoopbackNetLoader(NetLoader loopbackNetLoader) {
        // Ignore. No nets are loaded from this compiler.
    }

    @Override
    public void setShadowLookup(ShadowLookup lookup) {
        this._lookup = lookup;
    }

    @Override
    public Net createNet(String name) {
        return new Net(name);
    }

    @Override
    public ShadowPreprocessor[] getRequiredPreprocessors() {
        return new ShadowPreprocessor[0];
    }

    /**
     * Compiles/determines the TransitionInscription between places
     *
     * @param shadowTransition the transition to compile
     * @param inPlaces the input Places
     * @param outPlaces the output Places
     * @return the logical transition Mode as String, possible Transitions: and, or, xor
     * @throws SyntaxException In Case there are >1 Inscriptions or Inscription is not of type and, or , xor
     */
    String compileTransitionInscriptions(
        ShadowTransition shadowTransition, Vector<Place> inPlaces, Vector<Place> outPlaces)
        throws SyntaxException
    {
        String mode = null;

        // Parse the inscriptions.
        for (Object elem : shadowTransition.elements()) {
            if (elem instanceof ShadowInscription) {
                String inscr = StringUtil.unspace(((ShadowInscription) elem).getInscription());
                if ("and".equals(inscr) || "or".equals(inscr) || "xor".equals(inscr)) {
                    if (mode != null) {
                        throw new SyntaxException("Too many inscriptions.")
                            .addObject(shadowTransition);
                    }
                    mode = inscr;
                } else {
                    throw new SyntaxException("Expected one of: and, or, xor.").addObject(elem);
                }
            } else if (elem instanceof ShadowArc arc) {
                Place place = _lookup.get(arc.getPlace());
                if (arc.getShadowArcType() == ShadowArc.BOTH) {
                    inPlaces.addElement(place);
                    outPlaces.addElement(place);
                } else if (arc.getShadowArcType() == ShadowArc.ORDINARY) {
                    if (arc.isPlaceToTransition()) {
                        inPlaces.addElement(place);
                    } else {
                        outPlaces.addElement(place);
                    }
                } else {
                    throw new SyntaxException("Unsupported arc type").addObject(arc);
                }
            } else {
                throw new SyntaxException("Unsupported transition inscription")
                    .addObject(shadowTransition).addObject(elem);
            }
        }

        return mode;
    }

    /**
     * Creates an anonymous LocalVariable in case the name is not known
     *
     * @return LocalVariable with continuous numerating as name
     */
    LocalVariable createAnonVariable() {
        return new LocalVariable(String.valueOf(_varNum++), false);
    }

    /**
     * Creates a PlaceVariable and stores it in the variables set
     *
     * @param variables VariableSet with all PlaceVariables
     * @param prefix Determines whether it is an in or Out-Place
     * @param place the Place to store
     * @return the created Place Variable
     */
    LocalVariable createPlaceVariable(LocalVariableSet variables, String prefix, Place place) {
        String name = place.getName();
        if (name == null) {
            return createAnonVariable();
        }
        return variables.create(prefix + name);
    }

    /**
     * Compiles a Place and insert its inscriptions ("0", "1", "false", "true")
     *
     * @param net The net in which the place is
     * @param shadowPlace the Place to compile
     * @throws SyntaxException in case the inscription is not of type bool (0,1,false,true)
     */
    void compile(Net net, ShadowPlace shadowPlace) throws SyntaxException {
        // Determine the name.
        String pname = shadowPlace.getName();
        if (pname == null) {
            _placeNum++;
            pname = "P" + _placeNum;
        }

        // Create the new place;
        Place place = new Place(net, pname, new NetElementID(shadowPlace.getID()));
        place.setTrace(shadowPlace.getTrace());
        _lookup.set(shadowPlace, place);

        // Insert the inscriptions.
        for (Object elem : shadowPlace.elements()) {
            if (elem instanceof ShadowInscription) {
                Object token;
                String inscr = StringUtil.unspace(((ShadowInscription) elem).getInscription());
                if ("0".equals(inscr) || "false".equals(inscr)) {
                    token = VALUE_0;
                } else if ("1".equals(inscr) || "true".equals(inscr)) {
                    token = VALUE_1;
                } else {
                    throw new SyntaxException("Expected one of: 0, 1, true, false.")
                        .addObject(elem);
                }
                place.add(new ConstantTokenSource(token));
            } else if (!(elem instanceof ShadowArc)) {
                throw new SyntaxException("Unsupported place inscription: " + elem.getClass())
                    .addObject(shadowPlace).addObject(elem);
            }
        }
    }

    /**
     * Compiles a given Transition
     * Uses compileTransitionInscription-Method to determine the mode  (and, or, xor) and get in and out-Places
     *
     * @param net The Net
     * @param shadowTransition the Transition to compile
     * @throws SyntaxException Forwards syntax Exceptions from sub methods
     */
    void compile(Net net, ShadowTransition shadowTransition) throws SyntaxException {
        // Determine the name.
        String tname = shadowTransition.getName();
        if (tname == null) {
            _transNum++;
            tname = "T" + _transNum;
        }

        // Create the new transition;
        Transition transition =
            new Transition(net, tname, new NetElementID(shadowTransition.getID()));
        transition.setTrace(shadowTransition.getTrace());
        _lookup.set(shadowTransition, transition);

        // Vectors of Place objects.
        Vector<Place> inPlaces = new Vector<>();
        Vector<Place> outPlaces = new Vector<>();
        String mode = compileTransitionInscriptions(shadowTransition, inPlaces, outPlaces);
        if (mode == null) {
            mode = "and";
        }

        // Keep track of all local variables that are created.
        LocalVariableSet variables = new LocalVariableSet();

        // Handle all input arcs.
        if ("and".equals(mode)) {
            for (int i = 0; i < inPlaces.size(); i++) {
                Place place = inPlaces.elementAt(i);
                Arc arc = new Arc(
                    place, transition, Arc.Type.IN, LOC_VAR_EXPR_ACT,
                    ConstantExpression.DOUBLE_ZERO_EXPRESSION);
                arc.setTrace(shadowTransition.getTrace());
                transition.add(arc);
            }
        }

        if ("or".equals(mode) || "xor".equals(mode)) {
            Expression sum = EXPR_0;
            for (int i = 0; i < inPlaces.size(); i++) {
                Place place = inPlaces.elementAt(i);
                Expression expr = new VariableExpression(
                    Types.UNTYPED, createPlaceVariable(variables, "in", place));
                Arc arc = new Arc(
                    place, transition, Arc.Type.IN, expr,
                    ConstantExpression.DOUBLE_ZERO_EXPRESSION);
                arc.setTrace(shadowTransition.getTrace());
                transition.add(arc);
                sum = new CallExpression(
                    Types.UNTYPED, new TupleExpression(new Expression[] { sum, expr }),
                    BasicFunction.PLUS);
            }

            if ("or".equals(mode)) {
                Function func = arg -> {
                    if (VALUE_0.equals(arg)) {
                        return VALUE_0;
                    } else {
                        return VALUE_1;
                    }
                };

                Expression assignExpr = new EqualsExpression(
                    Types.UNTYPED, LOC_VAR_EXPR_ACT, new CallExpression(Types.UNTYPED, sum, func));
                transition.add(new ExpressionInscription(assignExpr));
            } else {
                Expression assignExpr = new EqualsExpression(Types.UNTYPED, LOC_VAR_EXPR_ACT, sum);
                transition.add(new ExpressionInscription(assignExpr));

                Expression compareExpr = new CallExpression(
                    Types.UNTYPED, new TupleExpression(new Expression[] { sum, EXPR_1 }),
                    BasicFunction.LESSEQUAL);
                transition.add(new GuardInscription(compareExpr));
            }
        }

        // Handle all output arcs.
        if ("and".equals(mode)) {
            for (int i = 0; i < outPlaces.size(); i++) {
                Place place = outPlaces.elementAt(i);
                Arc arc = new Arc(
                    place, transition, Arc.Type.OUT, LOC_VAR_EXPR_ACT,
                    ConstantExpression.DOUBLE_ZERO_EXPRESSION);
                arc.setTrace(shadowTransition.getTrace());
                transition.add(arc);
            }
        }

        if ("or".equals(mode)) {
            Expression sum = EXPR_0;
            for (int i = 0; i < outPlaces.size(); i++) {
                Place place = outPlaces.elementAt(i);
                Expression expr = new VariableExpression(
                    Types.UNTYPED, createPlaceVariable(variables, "out", place));
                Arc arc = new Arc(
                    place, transition, Arc.Type.OUT, expr,
                    ConstantExpression.DOUBLE_ZERO_EXPRESSION);
                arc.setTrace(shadowTransition.getTrace());
                transition.add(arc);
                RangeEnumeratorInscription range =
                    new RangeEnumeratorInscription(expr, 0, 1, false, transition);
                transition.add(range);
                sum = new CallExpression(
                    Types.UNTYPED, new TupleExpression(new Expression[] { sum, expr }),
                    BasicFunction.PLUS);
                Expression compareExpr = new CallExpression(
                    Types.UNTYPED, new TupleExpression(new Expression[] { expr, LOC_VAR_EXPR_ACT }),
                    BasicFunction.LESSEQUAL);
                transition.add(new GuardInscription(compareExpr));
            }

            Expression globalCompareExpr = new CallExpression(
                Types.UNTYPED, new TupleExpression(new Expression[] { sum, LOC_VAR_EXPR_ACT }),
                BasicFunction.GREATEREQUAL);
            transition.add(new GuardInscription(globalCompareExpr));
        }

        if ("xor".equals(mode)) {
            Expression choiceExpr = new VariableExpression(Types.UNTYPED, createAnonVariable());
            for (int i = 0; i < outPlaces.size(); i++) {
                Place place = outPlaces.elementAt(i);

                final Value iPlusOne = new Value(i + 1);
                Function func = arg -> {
                    if (iPlusOne.equals(arg)) {
                        return VALUE_1;
                    } else {
                        return VALUE_0;
                    }
                };

                Arc arc = new Arc(
                    place, transition, Arc.Type.OUT,
                    new EqualsExpression(
                        Types.UNTYPED,
                        new VariableExpression(
                            Types.UNTYPED, createPlaceVariable(variables, "out", place)),
                        new CallExpression(Types.UNTYPED, choiceExpr, func)),
                    ConstantExpression.DOUBLE_ZERO_EXPRESSION);
                arc.setTrace(shadowTransition.getTrace());
                transition.add(arc);
            }

            RangeEnumeratorInscription range =
                new RangeEnumeratorInscription(choiceExpr, 0, outPlaces.size(), false, transition);
            transition.add(range);

            Expression compareExpr = new CallExpression(
                Types.UNTYPED,
                new TupleExpression(
                    new Expression[] {
                        new CallExpression(
                            Types.UNTYPED,
                            new TupleExpression(new Expression[] { LOC_VAR_EXPR_ACT, EXPR_0 }),
                            BasicFunction.EQUAL),
                        new CallExpression(
                            Types.UNTYPED,
                            new TupleExpression(new Expression[] { choiceExpr, EXPR_0 }),
                            BasicFunction.EQUAL) }),
                BasicFunction.EQUAL);
            transition.add(new GuardInscription(compareExpr));
        }
    }

    @Override
    public void compile(ShadowNet shadowNet) throws SyntaxException {
        Net net = new Net(shadowNet.getName());

        Iterator<ShadowNetElement> iterator = shadowNet.elements().iterator();
        while (iterator.hasNext()) {
            Object elem = iterator.next();
            if (elem instanceof ShadowPlace) {
                compile(net, (ShadowPlace) elem);
            }
        }

        iterator = shadowNet.elements().iterator();
        while (iterator.hasNext()) {
            Object elem = iterator.next();
            if (elem instanceof ShadowTransition) {
                compile(net, (ShadowTransition) elem);
            }
        }

        _lookup.setNet(shadowNet.getName(), net);
    }

    @Override
    public String checkDeclarationNode(String inscription, boolean special, ShadowNet shadowNet) {
        return "unknown";
    }

    @Override
    public String checkArcInscription(String inscription, boolean special, ShadowNet shadowNet) {
        return "unknown";
    }

    @Override
    public String checkTransitionInscription(String inscr, boolean special, ShadowNet shadowNet) {
        return "unknown";
    }

    @Override
    public String checkPlaceInscription(String inscription, boolean special, ShadowNet shadowNet) {
        return "unknown";
    }
}