package code.space;

import code.term.*;
import code.symbols.*;
import code.subst.*;
import code.instr.*;
import code.stuff.*;
import code.lang.*;
import code.table.*;

import java.util.Stack;
import java.util.EmptyStackException;
import java.util.Enumeration;
import java.util.Vector;
import java.text.DecimalFormat;

public class Computation implements Client {

    public Computation(int taskIndex, Term term, Subst subst, Client client) {
        this.result = term;
        this.subst = subst;
        this.client = client;
        this.taskCase = new TaskIF[]{new NFTask(result), new HNFTask(), new PATask()};

        this.task = taskCase[taskIndex];
        if (Tracer.computation)
            Logger.logln("-C- " + debug() + " creating " + term);
    }

    // ------------------------------------------------------------------
    // A computation may have children (sub) computations

    private Computation[] child;

    public void setChildren(Computation[] child) {
        this.child = child;
        task = taskCase[PARALLEL];
    }

    // ------------------------------------------------------------------
    // A computation has a result and a stack of pre-narrexes

    private Term result;

    public Term getResult() {
        return result;
    }

    private Stack <Term> stack = new Stack <Term>();

    public Term getTerm() {
        if (stack.size() <= 0)
            return null;
        return stack.peek();
    }

    private void update(Term reduct) {
        Term term = getTerm();
        if (Tracer.computation)
            Logger.logln("-C- " + debug() + " replacing " + term + 
			 " with " + reduct);
        term.update(reduct);
    }

    public void push(Term term) {
        if (Tracer.computation)
            Logger.logln("-C- " + debug() + " pushing " + term);
        stack.push(term);
        // stackDebug();
    }

    public void pop() {
        if (Tracer.computation) {
            Term term = stack.peek();
            Logger.logln("-C- " + debug() + " popping " + term);
        }
        stack.pop();
        // stackDebug();
    }

    public void stackDebug() {
        for (int i = 0; i < stack.size(); i++) {
            Logger.logln("Stack " + i + "  " + stack.elementAt(i));
        }
    }

    // ------------------------------------------------------------------
    // A computation has a state

    public static final int ACTIVE = 0;
    public static final int WAITING = ACTIVE + 1;
    public static final int ABANDONED = WAITING + 1;
    public static final int SUCCESS = ABANDONED + 1;
    public static final int FAILED = SUCCESS + 1;
    public static final int RESIDUATING = FAILED + 1;
    public static final int FLOUNDER = RESIDUATING + 1;
    public static final int PAUSED = FLOUNDER + 1; //For debugging
    public static final String[] stateName =
            {"active", "waiting", "abandoned", "success", "failed", "residuating", "flounder", "paused"};
    /**
     * This better be private so state changes go thru a method. The method ensures that any appropriate action is
     * taken.
     */
    private int state = ACTIVE;

    public int getState() {
        return state;
    }

    public void selfSetState(int state) {
        this.state = state;
        if (Tracer.computation)
            Logger.logln("-C- " + debug() + " changing state to " + stateName[state]);
        switch (state) {
            case SUCCESS:
            case FAILED:
            case RESIDUATING:
                client.doneChild(this);
                break;
            case ABANDONED:
                if (child != null)
                    for (int i = 0; i < child.length; i++)
                        child[i].forcedSetState(ABANDONED);
                client.doneChild(this);
                break;
            case ACTIVE:
            case WAITING:
            case PAUSED:
                break;
            default :
                throw new RuntimeException("Missing case in Computation.setState");
        }
    }

    public void forcedSetState(int state) {
        if (Tracer.computation)
            Logger.logln("-C- " + debug() + " forcing state " + stateName[state] + " from " + stateName[this.state]);
        if (this.state == ABANDONED)
            return;
        this.state = state;
        switch (state) {
            case FLOUNDER:
                // This happen when a top-level computation residuates
                // Then, recursively abandon every (residuating) child
            case ABANDONED:
                if (child != null)
                    for (int i = 0; i < child.length; i++)
                        child[i].forcedSetState(ABANDONED);
                break;
            default :
                throw new RuntimeException("Missing case in Computation.forcedSetState");
        }
    }

    // ------------------------------------------------------------------
    // A computation has an id (for tracing)

    protected static int idCounter = 0;
    public final int id = ++idCounter;

    public static final DecimalFormat i3 = new DecimalFormat("000");

    public String getIdString() {
        return client.getIdString() + "." + i3.format(id);
    }

    public String debug() {
        String string = task.type() + " " + getIdString() + " { " + subst + "}";
        return string;
    }

    // ------------------------------------------------------------------
    // A computation has a substitution

    private Subst subst;

    public Subst getSubst() {
        return subst;
    }

    public Term getBinding(Variable variable) {
        return subst.getBinding(variable);
    }

    public void setBinding(Variable variable, Term binding) {
	subst = new VarSubst(variable, binding, subst);
    }

    // ------------------------------------------------------------------
    // A computation has a client

    public final Client client;

    public Computation getTop() {
        Computation tmp = this;
        for (; ;) {
            Client client = tmp.client;
            if (client instanceof Computation)
                tmp = (Computation) client;
            else
                break;
        }
        return tmp;
    }

    public void doneChild(Computation child) {
        task.doneChild(child);
    }

    // ------------------------------------------------------------------
    // A computation has a task

    private interface TaskIF {
        String type();

        void step();

        void doneChild(Computation child);
    }

    private class NFTask implements TaskIF {
        private EnumTerm xenum;

        public NFTask(Term term) {
            xenum = new EnumTerm(term);
        }

        public String type() {
            return "NF";
        }

        public void step() {
            if (xenum.hasMoreElements()) {
                try {
                    Term tmp = (Term) xenum.nextElement();
                    push(tmp);
                    task = taskCase[HEADNORMAL];
                    return;
                } catch (EnumTerm.FailureException ex) {
                    // the stack should be empty at this point
                    result.update(SuccessModule.termFail);
                    selfSetState(FAILED);
                    return;
                }
            }
            if (state != FAILED)
                selfSetState(SUCCESS);
        }

        public void doneChild(Computation child) {
            throw new IllegalStateException("No doneChild for NF task");
        }
    }

    private class HNFTask implements TaskIF {
        public String type() {
            return "HN";
        }

        public void step() {

            try {
                Term term = stack.peek();
                if (term.isHNF())
                    pop();
                else {
		    if (Tracer.instruction) {
			int root = term.getRoot();
			Symbol symbol = MapTable.getSymbol(root);
			Logger.logln(getIdString() + 
				     ": -------- executing " +
				     symbol.moduleName + "." +
				     symbol.symbolName);
		    }
                    execute(term.getCode());
		}
            } catch (EmptyStackException ex) {
                task = taskCase[NORMAL];
            }
        }

        public void doneChild(Computation child) {
            throw new IllegalStateException("No doneChild for HNF task");
        }
    }

    private class PATask implements TaskIF {
        public String type() {
            return "PA";
        }

        public void step() {
            selfSetState(WAITING);
            child[0].selfSetState(ACTIVE);
        }

        public void doneChild(Computation xchild) {
            int childState = xchild.getState();
            switch (childState) {
                case ABANDONED:
                    selfSetState(ABANDONED);
                    break;
                case FAILED:
                    // REVISE CODE BELOW ???
                case SUCCESS:
                    Term result = xchild.getResult();
                    byte kind = result.getKind();
                    if (kind == DataSymbol.UnboundVariable) {
                        // either left or right operand is a variable
                        // bind and restart
                        Variable variable = (Variable) result.getRepresentation();
                        Term instance = SuccessModule.successTerm;
                        if (Tracer.computation)
                            Logger.logln("-C- " + debug() + " narrowing " + instance + " on variable " + variable);
                        Computation top = getTop();
                        Client client = top.client;
                        Term topLevel = top.getResult();
                        // Map map = new Map(variable, instance);
                        // Subst newSubst = new VarSubst(map, subst);
			Subst newSubst = 
			    new VarSubst(variable, instance, subst);
                        Term newTerm = topLevel.cloneWithSubst(newSubst);

			ComputationFactory.create(newTerm, newSubst, client);

                        // variable.restartResiduating();
                        selfSetState(Computation.ABANDONED);
                    } else if (kind == DataSymbol.Failure) {
                        // either left or right operand failed
                        // fail and abandon other operand
                        update(SuccessModule.termFail);
                        pop();
                        task = taskCase[HEADNORMAL];
                        selfSetState(ACTIVE);
                        // end other child if WAITING
                        if (xchild == child[0])
                            child[1].forcedSetState(ABANDONED);
                        else
                            child[0].forcedSetState(ABANDONED);
                    } else if (xchild == child[0]) {
                        // left operand succeeds, evaluate right operand
                        child[1].selfSetState(ACTIVE);
                    } else {
                        // right operand succeeds
                        if (child[0].getState() == RESIDUATING) {
                            // left operand residuates, this computation residuates
                            selfSetState(RESIDUATING);
                        } else {
                            // both left and right operands succeed
                            // this computation succeeds
                            update(SuccessModule.successTerm);
                            pop();
                            task = taskCase[HEADNORMAL];
                            selfSetState(ACTIVE);
                        }
                    }
                    break;
                case RESIDUATING:
                    if (xchild == child[0])
                        child[1].selfSetState(ACTIVE);
                    else
                        selfSetState(childState);
                    break;
                default :
                    throw new IllegalStateException("Unexpected child state " + stateName[childState] + " in PA");
            }
        }
    }

    public static final int NORMAL = 0;
    public static final int HEADNORMAL = NORMAL + 1;
    public static final int PARALLEL = HEADNORMAL + 1;

    public final TaskIF[] taskCase;
    private TaskIF task;

    public void step() {
        task.step();
    }

    public void execute(Instruction[] instruction) {
        int length = instruction.length;
        Tracer.instructions += length;
        for (int i = 0; i < length; i++)
            instruction[i].execute(Computation.this);
    }

}
