package ws.prova.reference;

/*
 * Copyright (C) 2002-2007 <a href="mailto:a.kozlenkov@city.ac.uk">Alex Kozlenkov</a>
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

import org.mandarax.kernel.*;
import org.mandarax.util.TermIterator;
import ws.prova.kernel.ProvaTerm;

import java.util.Collection;
import java.util.Iterator;
import java.util.List;
import java.util.Map;

/**
 * A generic Prova variable containing the actual Mandarax Term to allow substitution
 * <p>Title: Prova</p>
 * <p>Description: A generic Prova variable containing the actual Mandarax Term to allow substitution</p>
 * <p>Copyright: Copyright (C) 2002-2007</p>
 * <p>Company: City University, London, United Kingdom </p>
 *
 * @author Alex Kozlenkov
 * @version 2.0 <25 March 2007>
 */
public class ProvaTermImpl implements ProvaTerm {
	protected Term t;

	public ProvaTermImpl(Term t) {
		this.t = t;
	}

	/**
	 * Factory method to build a Prova term recursively
	 *
	 * @param vars
	 * @param t
	 */
	static public Term fold(final Map vars, final Term t) {
		if (t.isConstant()) {
			return new ProvaTermImpl(t);
		} else if (t.isVariable()) {
			if (!vars.containsKey(t)) {
				vars.put(t, new ProvaTermImpl(t));
			}
			return t;
		}
		final ComplexTerm ct0 = (ComplexTerm) t;
		final ComplexTerm ct = new ComplexTermImpl();
		ct.setFunction(ct0.getFunction());
		final Term t1 = ct0.getTerms()[1];
		final Term t1m = fold(vars, t1);
		ct.setTerm(t1m, 1);
		final Term t2 = ct0.getTerms()[0];
		final Term t2m = fold(vars, t2);
		ct.setTerm(t2m, 0);
//		if( t instanceof ProvaTerm ) {
//			fold(vars,((ProvaTerm) t).getTerm());
//			return t;
//		}
//		final ComplexTerm ct = (ComplexTerm) t;
//		final Term t1 = ct.getTerms()[1];
//		final Term t1m = fold(vars,t1);
//		ct.setTerm(t1m,1);
//		final Term t2 = ct.getTerms()[0];
//		final Term t2m = fold(vars,t2);
//		ct.setTerm(t2m,0);
		return new ProvaTermImpl(ct);
	}

	public String getName() {
		return t.isVariable() ? ((VariableTerm) t).getName() : null;
	}

	public void setName(String n) {
		if (t.isVariable()) {
			((VariableTerm) t).setName(n);
		}
	}

	public Object getObject() {
		return t.isConstant() ? ((ConstantTerm) t).getObject() : null;
	}

	public void setObject(Object obj) {
		if (t.isConstant()) {
			((ConstantTerm) t).setObject(obj);
		}
	}

	public void setType(Class t) {
		if (this.t.isVariable()) {
			((VariableTerm) this.t).setType(t);
		}
	}

	public TermIterator allSubterms() {
		return t.isCompound() ? ((ComplexTerm) t).allSubterms() : null;
	}

	public Term apply(Replacement r) {			
		return t.apply(r);
	}

	public boolean containsVariables() {
		return t.containsVariables();
	}

	public boolean containsVariable(VariableTerm var) {
		return t.containsVariable(var);
	}

	public Term[] getAllSubterms() {
		return t.isCompound() ? ((ComplexTerm) t).getAllSubterms() : null;
	}

	public void getAllSubtermsA(List result) {
		result.add(new ProvaTermImpl(t));
		if (t instanceof ComplexTerm) {
			Term[] tt = ((ComplexTerm) t).getTerms();
			for (int i = tt.length; i-- != 0;) {
				ProvaTerm pt = new ProvaTermImpl(tt[i]);
				pt.getAllSubtermsA(result);
			}
		}
	}

	public void getAllSubtermsA(List result, boolean left) {
		t.getAllSubtermsA(result, left);
	}

	public boolean getAllSubtermsB(List result, Iterator aux) {
		return t.getAllSubtermsB(result, aux);
	}

	public boolean getAllSubtermsB(List result, Iterator aux, boolean left) {
		return t.getAllSubtermsB(result, aux, left);
	}

	public Class getType() {
		return t.getType();
	}

	public boolean isCompound() {
		return t.isCompound();
	}

	public boolean isConstant() {
		return t.isConstant();
	}

	public boolean isVariable() {
		return t.isVariable();
	}

	public Object resolve(Session session) throws UnsupportedOperationException, IllegalArgumentException {
		return t.resolve(session);
	}

	public boolean sameAs(Term t) {
		return this.t.sameAs(t);
	}

    public boolean isExecutable() {
        return t.isExecutable();
    }

	public Function getFunction() {
		return t.isCompound() ? ((ComplexTerm) t).getFunction() : null;
	}

	public void setFunction(Function f) {
		if (t.isCompound()) {
			((ComplexTerm) t).setFunction(f);
		}
	}

	public Term[] getTerms() {
		return t.isCompound() ? ((ComplexTerm) t).getTerms() : null;
	}

	public void setTerm(Term t, int i) {
		if (t.isCompound()) {
			((ComplexTerm) t).setTerm(t, i);
		}
	}

	public TermIterator terms() {
		return t.isCompound() ? ((ComplexTerm) t).terms() : null;
	}

	public Term getTerm() {
		return t;
	}

	public void setTerm(Term t) {
		this.t = t;
	}

	public static boolean unify(final Map vars1, final Term ipt1, final Map vars2, final Term ipt2) {
		ProvaTerm pt1 = (ipt1 instanceof VariableTermImpl) ? ((ProvaTerm) vars1.get(ipt1)) : (ProvaTerm) ipt1;
		ProvaTerm pt2 = (ipt2 instanceof VariableTermImpl) ? ((ProvaTerm) vars2.get(ipt2)) : (ProvaTerm) ipt2;
		Term t1, t2;
		if (pt1 != null) {
			t1 = pt1.getTerm();
		} else {
			pt1 = (ProvaTerm) vars2.get(ipt1);
			t1 = pt1.getTerm();
		}
		if (pt2 != null) {
			t2 = pt2.getTerm();
		} else {
			pt2 = (ProvaTerm) vars1.get(ipt2);
			t2 = pt2.getTerm();
		}
		if (t1.isCompound()) {
			ComplexTerm ct1 = (ComplexTerm) t1;
			if (t2.isCompound()) {
				ComplexTerm ct2 = (ComplexTerm) t2;
				return unify(vars1, (Term) ct1.getTerms()[1], vars2, (Term) ct2.getTerms()[1]) &
						unify(vars1, (Term) ct1.getTerms()[0], vars2, (Term) ct2.getTerms()[0]);
			}
			if (t2.isConstant()) {
				return false;
			}
			VariableTerm vt2 = (VariableTerm) t2;
			if (vt2.getType() == ws.prova.RList.class || vt2.getType() == Object.class) {
				if (ct1.containsVariable(vt2))
					return false;
				pt2.setTerm(t1);
				return true;
			}
			return false;
		}
		if (t1.isConstant()) {
			if (t2.isCompound()) {
				return false;
			}
			if (t2.isConstant()) {
				return t2.sameAs(t1);
			}
			Class cl = t2.getType();
			if (cl == Object.class || cl.isInstance(((ConstantTerm) t1).getObject())) {
				pt2.setTerm(t1);
				return true;
			} else
				return false;
		}
		// t1 is a variable term
		VariableTerm vt1 = (VariableTerm) t1;
		Class cl = t1.getType();
		if (t2.isConstant()) {
			if (cl == Object.class || cl.isInstance(((ConstantTerm) t2).getObject())) {
				pt1.setTerm(t2);
				return true;
			} else
				return false;
		}
		if (t2.isCompound()) {
			ComplexTerm ct2 = (ComplexTerm) t2;
			if (cl == ws.prova.RList.class || cl == Object.class) {
				if (ct2.containsVariable(vt1))
					return false;
				pt1.setTerm(t2);
				return true;
			} else
				return false;
		}
		// t2 is also a variable term
		VariableTerm vt2 = (VariableTerm) t2;
		Class cl1 = vt1.getType();
		Class cl2 = vt2.getType();
		if (cl2 == cl1 || cl2.isAssignableFrom(cl1)) {
			if (t2 == ipt2)
				vars2.put(ipt2, pt1);
			else
				variableForVariable(vars1, vars2, t2, pt1);
			return true;
		}
		if (cl1.isAssignableFrom(cl2)) {
			if (t2 == ipt2)
				vars1.put(ipt1, pt2);
			else
				variableForVariable(vars1, vars2, t1, pt2);
			return true;
		}
		return false;
	}

	/**
	 * Substitute a variable for a variable in the variables Maps for goal and target of unification
	 *
	 * @param vars1
	 * @param vars2
	 * @param t2
	 * @param pt1
	 */
	private static void variableForVariable(final Map vars1, final Map vars2, final Term t2, final ProvaTerm pt1) {
		for (Iterator kit1 = vars1.keySet().iterator(); kit1.hasNext();) {
			VariableTerm v1 = (VariableTerm) kit1.next();
			if (((ProvaTerm) vars1.get(v1)).getTerm() == t2) {
				vars1.put(v1, pt1);
			}
		}
		for (Iterator kit2 = vars2.keySet().iterator(); kit2.hasNext();) {
			VariableTerm v2 = (VariableTerm) kit2.next();
			if (((ProvaTerm) vars2.get(v2)).getTerm() == t2) {
				vars2.put(v2, pt1);
			}
		}
	}

	public static void assignSubstitutions(final Map vars1, final Map vars2, final List subst, final List substLocal, boolean isRule) {
		for (Iterator kit1 = vars1.keySet().iterator(); kit1.hasNext();) {
			VariableTerm vt1 = (VariableTerm) kit1.next();
			Term repvt1 = ((ProvaTerm) vars1.get(vt1)).getTerm();
			if (repvt1 != vt1) {
				Term sub = repvt1;
				if (repvt1.isCompound()) {
					sub = unfold(repvt1, vars1, vars2);
//					sub = repvt1;
				}
				subst.add(new Replacement(vt1, sub));
			}
		}
		if (!isRule)
			return;
		for (Iterator kit2 = vars2.keySet().iterator(); kit2.hasNext();) {
			VariableTerm vt2 = (VariableTerm) kit2.next();
			Term repvt2 = ((ProvaTerm) vars2.get(vt2)).getTerm();
			if (repvt2 != vt2) {
				Term sub = repvt2;
				if (repvt2.isCompound()) {
					sub = unfold(repvt2, vars1, vars2);
//					sub = repvt2;
				}
				substLocal.add(new Replacement(vt2, sub));
			}
		}
	}

	private static Term unfold(final Term t, Map vars1, Map vars2) {
		if (!(t instanceof ProvaTerm)) {
			if (t.isCompound()) {
				ComplexTerm ct = (ComplexTerm) t;
				ct.setTerm(unfold((Term) ct.getTerms()[1], vars1, vars2), 1);
				ct.setTerm(unfold((Term) ct.getTerms()[0], vars1, vars2), 0);
				return ct;
			}
			if (t.isVariable()) {
				final Term t1 = (Term) vars1.get(t);
				if (vars1.containsKey(t) && !t1.isVariable() && t1 != t) {
					return unfold((Term) t1, vars1, vars2);
				}
				final Term t2 = (Term) vars2.get(t);
				if (vars2.containsKey(t) && !t2.isVariable() && t2 != t) {
					return unfold((Term) vars2.get(t), vars1, vars2);
				}
			}
			return t;
		}
		final ProvaTerm pt = (ProvaTerm) t;
		if (pt.isCompound()) {
			ComplexTerm ct = (ComplexTerm) pt.getTerm();
			ct.setTerm(unfold((Term) ct.getTerms()[1], vars1, vars2), 1);
			ct.setTerm(unfold((Term) ct.getTerms()[0], vars1, vars2), 0);
			return ct;
		}
		return pt.getTerm();
	}

	public Term applyMinimally(Collection r, Map complexReplacements) {
		// TODO Auto-generated method stub
		return null;
	}
}
