package code.space;

import code.term.*;
import code.lang.*;
import code.table.*;
import code.symbols.*;

import java.util.*;

/**
 * This class provides an enumerator of the maximal
 * operation-rooted subterms of a term.
 *
 * @author Sergio Antoy
 * @since July 21, 2003
 */

public class EnumTerm {

    public class FailureException extends Exception {}
    private static int closureId;

    private class Tagger {
        private int currArg = 0;
        private Term[] todo;

        private Tagger(Term[] todo) {
            this.todo = todo;
        }
    }

    private Stack stack = new Stack();
    private Object current;
    private boolean more;

    /**
     * Constructs an enumerator of the argument's elements.
     *
     * @param term The term whose maximal operation-rooted
     *             subterms will be enumerated.
     */
    public EnumTerm(Term term) {
	closureId = ModuleTable.getId
	    (SystemModule.moduleName,SystemModule.closureName);
        stack.push(new Tagger(new Term[]{term}));
        try {
            doit();
        } catch (FailureException ex) {
            throw new RuntimeException("Unexpected FailureException");
        }
    }

    /**
     * Tests if this enumeration contains more elements.
     *
     * @return true if and only if this enumeration object
     *         contains at least one more element to provide;
     *         false otherwise.
     */
    public boolean hasMoreElements() {
        return more;
    }

    /**
     * Returns the next element of this enumeration if
     * this enumeration object has at least one more element to provide.
     *
     * @return the next element of this enumeration.
     * @throws NoSuchElementException if no more elements exist.
     */
    public Object nextElement() throws FailureException {
        if (more) {
            Object tmp = current;
            doit();
            return tmp;
        } else
            throw new NoSuchElementException();
    }

    /**
     * This method maintains the values that the interface
     * methods return.  It should be called by the constructor and
     * after an element of the iteration is returned.
     * <p/>
     * Execute a pre-order, left-to-right traversal.
     */
    private void doit() throws FailureException {
        while (!stack.isEmpty()) {
	    more = false;
            Tagger tagger = (Tagger) stack.peek();
            Term[] tmp = tagger.todo;
            int length = tmp.length;
            if (tagger.currArg == length) {
                stack.pop();
            } else {
                Term term = (Term) tmp[tagger.currArg];
                // If term is a HNF, then forget it forever
                // and move on to its arguments.
                // Otherwise, return it, but leave it there
                // so that its arguments will be processed later
                // All this is done by advancing currArg.
		switch (term.getKind()) {
		case DataSymbol.Operation:
		    current = term;
		    more = true;
		    return;
		case DataSymbol.UnboundVariable:
		    tagger.currArg++;
		    break;
		case DataSymbol.Failure:
		    throw new FailureException();
		default:    
		    // term is a HNF, look into the arguments
		    tagger.currArg++;
		    int root = term.getRoot();
		    if (root == closureId) {
			// Must avoid returning the argument's root
			// One cannot have a closure of a closure
			stack.push(new Tagger(term.getArgument((byte) 0).getArgument()));
		    } else {
			stack.push(new Tagger(term.getArgument()));
		    }
		    break;
		}
	    }
	}
	more = false;
    }
}