package code.term;

import code.instr.Instruction;
import code.symbols.*;
import code.stuff.Tracer;
import code.subst.Subst;
import code.term.visitor.*;

/**
 * This class implements a term. There is an overloaded constructor for each
 * kind of term:
 * <UL>
 * <LI> Variable
 * <LI> Primitive (int, char, etc.)
 * <LI> Algebraic
 * </UL>
 * Since the root of an algebraic type is an int, the second argument of an
 * algebraic type term is an array of terms, the arguments. This array has zero
 * length for a nullary symbol term.
 *
 * @author Sergio Antoy
 * @since June 17, 2003
 */

public class Term {

    /**
     * The implementation of this term.
     */
    TermImpl representation;

    public TermImpl getRepresentation() {
        return (representation instanceof TermImplRef)
               ? ((TermImplRef)representation).getRepresentation()
               : representation;
    }

    /** 
     * Terms made up by a nullary symbol must still use 
     * the binary constructor to discriminate with the
     * constructor that construct integer constants.
     * Therefore, an array of zero arguments.
     */
    public final static Term [] noArgs = {};
    

    // The overloaded constructors

    public Term(int root, Term[] argument) {
        representation = new TermImplUser(root, argument);
        Tracer.terms++;

    }

    public Term(Variable variable) {
        representation = variable;
        Tracer.terms++;
    }

    public Term(int value) {
        representation = new TermImplInt(value);
        Tracer.terms++;
    }

    public Term(float value) {
        representation = new TermImplFloat(value);
        Tracer.terms++;
    }

    public Term(char value) {
        representation = new TermImplChar(value);
        Tracer.terms++;
    }

    public Term(String value) {
        representation = new TermImplString(value);
        Tracer.terms++;
    }

    public Term(TermImpl representation) {
        this.representation = representation;
        Tracer.terms++;
    }

    public Term(Term referee) {
        representation = new TermImplRef(referee);
        // Tracer.terms++;
    }

    /**
     * Returns the root id of this term.
     *
     * @return The root value
     */
    public int getRoot() { return representation.getRoot(); }

    /**
     * Returns the root symbol of this term
     *
     * @return String
     */
    public String getRootSymbol() { return representation.getRootSymbol(); }


    /**
     * Returns the list of arguments for this term.
     *
     * @return The argument value
     */
    public Term[] getArgument() { return representation.getArgument(); }


    /**
     * Returns the number-th argument of this term.
     *
     * @param number
     * @return Term
     */
    public Term getArgument(byte number) {
        return representation.getArgument(number);
    }


    /**
     * Returns the kind of this term.
     *
     * @return The kind value
     */
    public byte getKind() { return representation.getKind(); }


    /**
     * Returns true if this term is in head normal form.
     *
     * @return boolean
     */
    public boolean isHNF() { return representation.isHNF(); }


    /**
     * Returns true if this term is in normal form.
     *
     * @return boolean
     */
    public boolean isNF() { return representation.isNF(); }


    /**
     * Returns the bytecode represented with objects
     * for rewritting this term.
     *
     * @return The code value
     */
    public Instruction[] getCode() { return representation.getCode(); }

    /**
     * Replaces the representation of this term
     * with the replacement.
     *
     * @param replacement The replacement
     */
    public void update(Term replacement) {
	Tracer.steps++;
        if (representation instanceof TermImplRef)
            ((TermImplRef)representation).update(replacement);
        else
            representation = replacement.representation;
    }

    
    /**
     * Returns a String representation of this term.
     * This method should be called on terms that have 
     * no occurrences of bound variables. Generally these
     * terms are the normal form results of computations.
     *
     * @return String The printable representation of this term.
     */
    public String toString() {
        return (String) representation.accept
	    (ToStringTermVisitor.singleton, null);
    }

    /**
     * Returns a String representation of this term.
     * This method should be called on terms that have 
     * occurrences of bound variables. Generally these
     * terms are the images of variables of the computed
     * answer of a computation.
     *
     * @return String The printable representation of this term.
     */
    public String toString(Subst substitution) {
	Term instance = cloneWithSubst(substitution);
	return instance.toString();
    }

    public Term eqSuccess(Term right) {
	if (this.getKind() == DataSymbol.Failure)
	    return this;
	else if (right.getKind() == DataSymbol.Failure)
	    return right;
	else
	    return (Term) representation.accept
		(EqSuccessTermVisitor.singleton, right.representation);
    }

    public Term eqBool(Term right) {
	if (this.getKind() == DataSymbol.Failure)
	    return this;
	else if (right.getKind() == DataSymbol.Failure)
	    return right;
	else
	    return (Term) representation.accept
		(EqBoolTermVisitor.singleton, right.representation);
    }

    public Term cloneWithSubst(Subst subst) {
	CloneWithSubstTermVisitor cloner = new CloneWithSubstTermVisitor();
        TermImpl tmp = (TermImpl) representation.accept(cloner, subst);
        if (tmp == representation) return this;
        else return new Term(tmp);
    }

    public Term cloneWithReplace(Term out, Term in) {
	CloneWithReplaceTerm cloner = new CloneWithReplaceTerm();
	return cloner.doit(this, out, in);
    }
}