package code.instr;

import code.space.Client;
import code.space.Computation;
import code.space.ComputationFactory;
import code.space.Space;
import code.stuff.Logger;
import code.stuff.Tracer;
import code.subst.Subst;
import code.subst.VarSubst;
import code.term.Term;
import code.term.Variable;

import java.util.Vector;

/**
 * Narrow the top term of the pre-term stack.
 * 
 * @author Sergio Antoy
 * @since June 17, 2003
 */

public class Narrow implements Instruction {
    private Narrow() {}
    public final static Narrow singleton = new Narrow();

    public void execute(Computation computation) {
        Computation top = computation.getTop();
        Client client = top.client;
        Term topLevel = top.getResult();
        Variable variable = (Variable) Space.instance.current.getRepresentation();
        Term term = computation.getTerm();
        Subst subst = computation.getSubst();

        if (Tracer.computation)
            Logger.logln("-C- " + computation.debug() + 
			 " narrowing " + term + " on variable " + variable);

	while (! Space.instance.preTerm.empty()) {
            Term instance = (Term) Space.instance.preTerm.pop();
	    // TODO: move this to the tracer
            if (Tracer.instruction) {
                Logger.logln(computation.getIdString() + 
			     ": Narrow: " + variable + " -> " + instance);
            }
            Subst newSubst = new VarSubst(variable, instance, subst);
	    // TODO: Maybe it should count this as a ND step
	    Tracer.steps++;
            Term newTerm = topLevel.cloneWithSubst(newSubst);
            if (Tracer.reduction) {
                Logger.logln(computation.getIdString() + " NAR " +
			     topLevel + " => " + newTerm);
            }

            ComputationFactory.create(newTerm, newSubst, client);
            // variable.restartResiduating();
        }
        computation.selfSetState(Computation.ABANDONED);
    }

    public String printAsTxtLoadable() { return "Narrow"; }
}