/*
    * #%L
    * prolobjectlink-jpi-jtrolog
    * %%
    * Copyright (C) 2012 - 2018 WorkLogic Project
    * %%
    * This program 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.1 of the
   * License, or (at your option) any later version.
   * 
   * This program 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 General Lesser Public License for more details.
   * 
   * You should have received a copy of the GNU General Lesser Public
   * License along with this program.  If not, see
   * <http://www.gnu.org/licenses/lgpl-2.1.html>.
   * #L%
   */
  package jTrolog.engine;
  
  import jTrolog.errors.PrologException;
  import jTrolog.lib.BasicLibrary;
  import jTrolog.parser.Parser;
  import jTrolog.terms.Double;
  import jTrolog.terms.EvaluableTerm;
  import jTrolog.terms.Number;
  import jTrolog.terms.Struct;
  import jTrolog.terms.StructAtom;
  import jTrolog.terms.Term;
  import jTrolog.terms.Var;
  import jTrolog.terms.WrapStruct;
  import jTrolog.terms.WrapVar;
  import jTrolog.terms.Wrapper;
  
  import java.util.Collection;
  import java.util.HashMap;
  import java.util.Iterator;
  import java.util.NoSuchElementException;
  
  /**
   * Keeps track of what variables are bound to what Terms and at which
   * ChoicePoint this connection was made.
   * 
   * now, the BindingsTable never receives anything that is not Wrapped. All
   * Structs sent in are wrapped as a mfck. the unifyBranch is now possible to run
   * without generating new objects when the getArg is called.
   * 
   * all the methods that add vars and get vars from the bidnings table is now
   * given both Var and context (and link term and its context) a problem is that
   * the stackMap needs to be subsumed into the bindings table since it needs to
   * retract the links done by a current owner. I don't think I can remove the
   * current owner as a separate map since it provides a rollback function. What I
   * can do is stringToStructList WrapVars for it only and then move these into
   * and out of the bindingsMap
   * 
   * @author janerist@stud.ntnu.no
   * @author ivar.orstavik@hist.no
   */
  @SuppressWarnings({ "rawtypes", "unchecked" })
  public class BindingsTable {
  
  	private int currentExecCtx = 0;
  
  	private LinkTable links = new LinkTable();
  
  	int uniqueExecutionCtxID = 1;
  	int[] firstInCtx = new int[10000];
  	private GarbageCan gc = new GarbageCan(links);
  
  	public int getUniqueExecutionCtxID() {
  		if (links.getWidth() == uniqueExecutionCtxID)
  			links.doubleWidth(uniqueExecutionCtxID * 2);
  		return uniqueExecutionCtxID++;
  	}
  
  	public void expandLinkTable(int newSize) {
  		gc.doubleTrashCanWidth(newSize);
  	}
  
  	final void collectGarbage(final int execCtx) {
  		uniqueExecutionCtxID = firstInCtx[execCtx];
  		currentExecCtx = execCtx;
  		gc.collectGarbageLinks(execCtx);
  	}
  
  	final void collectGarbageSmall() {
  		uniqueExecutionCtxID--;
  		gc.collectGarbageLinks(currentExecCtx);
  	}
  
  	final void setCurrentExecCtx(final int execCtx) {
  		currentExecCtx = execCtx;
  		if (execCtx >= firstInCtx.length)
  			firstInCtx = LinkTable.expandArray(firstInCtx, execCtx * 2);
  		firstInCtx[execCtx] = uniqueExecutionCtxID;
  	}
 
 	// todo 1. perhaps it would be smart to keep track of the left and right
 	// terms/ctxs that the unification process works on.
 	// todo if this is done, then whenever a unification fails, one could
 	// display exactly what two terms did not match.
 	// todo but this is perhaps better done in the Engine, since one here might
 	// like to view the entire terms..
 	public boolean unify(Term t0, Term t1) {
 		int oneCtx = t0 instanceof Wrapper ? ((Wrapper) t0).getContext() : 0;
 		int twoCtx = t1 instanceof Wrapper ? ((Wrapper) t1).getContext() : 0;
 		return unifyBranch(unWrap(t0), unWrap(t1), oneCtx, twoCtx);
 	}
 
 	// ca. 500
 
 	/**
 	 * @param one
 	 * @param two
 	 * @param oneCtx
 	 * @param twoCtx
 	 * @return true if the two terms are unified, false otherwise
 	 */
 	boolean unifyBranch(Term one, Term two, int oneCtx, int twoCtx) {
 		while (one.type == Term.VAR) {
 			Var vOne = (Var) one;
 			// if the two varaiables are equal, then return true
 			if (oneCtx == twoCtx && vOne.equals(two)) // if (oneCtx == twoCtx &&
 														// two instanceof Var &&
 														// vOne.nrInStruct ==
 														// ((Var)
 														// two).nrInStruct )
 				return true;
 			// else, if the left variable is not bound, bind it
 			final int vNr = vOne.nrInStruct;
 			Term link = links.getTerm(vNr, oneCtx);
 			if (link == null)
 				return setLink(vNr, oneCtx, two, twoCtx);
 			// else, Var one is bound. If it is bound to a Var, then the loop
 			// will continue updating the on Var, else it will continue down the
 			// method
 			oneCtx = links.getCtx(vNr, oneCtx);
 			one = link;
 		}
 		while (two.type == Term.VAR) {
 			final int vNr = ((Var) two).nrInStruct;
 			Term link = links.getTerm(vNr, twoCtx);
 			if (link == null)
 				return setLink(vNr, twoCtx, one, oneCtx); // var two is unbound,
 															// bind it against
 															// one
 			twoCtx = links.getCtx(vNr, twoCtx);
 			two = link;
 		}
 		// from now on, neither branch is a Var
 		if (one.type >= Term.STRUCT && two.type >= Term.STRUCT) {
 			Struct a = (Struct) one;
 			Struct b = (Struct) two;
 			if (a.predicateIndicator != b.predicateIndicator)
 				return false;
 			for (int c = 0; c < a.arity; c++)
 				if (!unifyBranch(a.getArg(c), b.getArg(c), oneCtx, twoCtx))
 					return false;
 			return true;
 		}
 		return one.type == Term.NUMBER && two.type == Term.NUMBER && BasicLibrary.number_equality_2((Number) one, (Number) two);
 	}
 
 	// ca. 500
 
 	// this method calls an almost entirely iterative method
 	boolean unifyBranchTwo(Term one, Term two, int oneCtx, int twoCtx) {
 		return unifyTrees(one.pos, two.pos, one.prePost, one.tree, two.tree, two.prePost, oneCtx, twoCtx);
 	}
 
 	private boolean unifyTrees(int i, int j, int[] prePostA, Term[] treeA, Term[] treeB, int[] prePostB, int oneCtx, int twoCtx) {
 		bb: for (int stopValue = prePostA[i]; i < prePostA.length && prePostA[i] <= stopValue; i++, j++) {
 			Term one = treeA[i], two = treeB[j];
 			int tmpCtx1 = oneCtx;
 			int tmpCtx2 = twoCtx;
 			boolean mustMakeNewStackLevel = false;
 
 			if (one.type == Term.VAR) {// instanceof Var){
 				while (one.type == Term.VAR) {// instanceof Var) {
 					Var vOne = (Var) one;
 					// if the two varaiables are equal, then return true
 					if (tmpCtx1 == twoCtx && vOne.equals(two))
 						continue bb;
 					// else, if the left variable is not bound, bind it
 					Term link = links.getTerm(vOne.nrInStruct, tmpCtx1);
 					if (link == null) {
 						if (!setLink(vOne.nrInStruct, tmpCtx1, two, twoCtx))
 							return false;
 						if (two.type == Term.STRUCT)// instanceof Struct &&
 													// ((Struct) two).arity >0)
 													// //we must increment j to
 													// skip two's children
 							for (int postStop = prePostB[j]; j < prePostB.length - 1 && prePostB[j + 1] < postStop; j++)
 								;
 						continue bb;
 					}
 					// else, Var one is bound. If it is bound to a Var, then the
 					// loop will continue updating the on Var, else it will
 					// continue down the method
 					tmpCtx1 = links.getCtx(vOne.nrInStruct, tmpCtx1);
 					one = link;
 				}
 				if (one.type == Term.STRUCT)// instanceof Struct && ((Struct)
 											// one).arity > 0) //todo we don't
 											// need to mustMakeNewStackLevel
 											// when the node har no children.
 					mustMakeNewStackLevel = true;
 			}
 
 			if (two.type == Term.VAR) {// instanceof Var){
 				while (two.type == Term.VAR) {// instanceof Var){
 					Var vTwo = (Var) two;
 					Term link = links.getTerm(vTwo.nrInStruct, tmpCtx2);
 					if (link == null) {
 						if (!setLink(vTwo.nrInStruct, tmpCtx2, one, tmpCtx1))
 							return false; // var two is unbound, bind it against
 											// on
 						if (one.type == Term.STRUCT)// instanceof Struct &&
 													// ((Struct) one).arity >0)
 													// //we must increment i to
 													// skip one's children
 							for (int postStop = prePostA[i]; i < prePostA.length - 1 && prePostA[i + 1] < postStop; i++)
 								;
 						continue bb;
 					}
 					tmpCtx2 = links.getCtx(vTwo.nrInStruct, tmpCtx2);
 					two = link;
 				}
 				if (two.type == Term.STRUCT)// instanceof Struct && ((Struct)
 											// two).arity > 0)
 					mustMakeNewStackLevel = true;
 			}
 
 			// todo we need to mustMakeNewStackLevel here because the ctx id
 			// changes,
 			// todo the prePost and values arrays changes.
 			// todo however these values only become relevant for the next
 			// check, so Atoms and Numbers do NOT mustMakeNewStackLevel
 			if (mustMakeNewStackLevel) {
 				if (!unifyBranch(one, two, tmpCtx1, tmpCtx2))
 					return false;
 				// we must increment i to skip one's and/or two's children
 				if (one.type == Term.STRUCT)// instanceof Struct && ((Struct)
 											// one).arity >0)
 					for (int postStop = prePostA[i]; i < prePostA.length - 1 && prePostA[i + 1] < postStop; i++)
 						;
 				if (two.type == Term.STRUCT)// instanceof Struct && ((Struct)
 											// two).arity >0)
 					for (int postStop = prePostB[j]; j < prePostB.length - 1 && prePostB[j + 1] < postStop; j++)
 						;
 			} else if (one.type >= Term.STRUCT && two.type >= Term.STRUCT) {// instanceof
 																			// Struct
 																			// &&
 																			// two
 																			// instanceof
 																			// Struct)
 																			// {
 				if (((Struct) one).predicateIndicator != ((Struct) two).predicateIndicator)
 					return false;
 			} else if (one.type == Term.NUMBER && two.type == Term.NUMBER) {// instanceof
 																			// Number
 																			// &&
 																			// two
 																			// instanceof
 																			// Number){
 				if (!BasicLibrary.number_equality_2((Number) one, (Number) two))
 					return false;
 			} else
 				return false;
 		}
 		return true;
 	}
 
 	@SuppressWarnings("unused")
 	private static int leftMostChildsPost(int i, int[] aPrePostArr) {
 		int temp;
 		int min = aPrePostArr[i];
 		while (i++ < aPrePostArr.length && min > (temp = aPrePostArr[i]))
 			min = temp;
 		return min;
 	}
 
 	public Term wrapWithID(Term t) {
 		return wrapWithID(t, getUniqueExecutionCtxID());
 	}
 
 	public static Term wrapWithID(Term t, int renameVarID) {
 		if (t instanceof Wrapper)
 			return t;
 		if (t instanceof Var)
 			return new WrapVar((Var) t, renameVarID);
 		if (t instanceof Struct && !(t instanceof StructAtom))
 			return new WrapStruct((Struct) t, renameVarID);
 		return t;
 	}
 
 	public static Term unWrap(Term l) {
 		return l instanceof Wrapper ? ((Wrapper) l).getBasis() : l;
 	}
 
 	/**
 	 * Adds a link. The key of the link is an ID calculated from the Variable
 	 * (its position in the root parent Struct) and its context The link is
 	 * stored in three different maps: 1. a map of the link to the Term it is
 	 * linked to 2. a map of the link to the context number of the Term it is
 	 * linked to 3. to facilitate garbage collection of unused links, a map
 	 * linking the context in which the binding takes place to a list of links
 	 * that are bound at this execution context is also updated
 	 * 
 	 * @param vNr
 	 * @param vCtx
 	 * @param link
 	 * @param linkCtx
 	 * @return true always
 	 */
 	private boolean setLink(final int vNr, final int vCtx, final Term link, final int linkCtx) {
 		// Most applications can probably turn off
 		// checkForInternalOccurencesOfVarInTerm without any consequenses by
 		// commenting out the if clause below.
 		// Removing this will likely result in approx 20% speed-up. But do so
 		// only when you know your application do not need this check.
 //	---->	if (checkForInternalOccurencesOfVarInTerm(vNr, vCtx, link, linkCtx))
 //	---->		return false;
 		links.put(vNr, vCtx, link, linkCtx);
 		gc.addToTrashCan(vNr, vCtx, currentExecCtx);
 		return true;
 	}
 
 	/**
 	 * todo don't search, sort? this now only gets in the original terms and the
 	 * context int as values
 	 * 
 	 * @param varBeingChecked
 	 * @param beingCheckedsContext
 	 * @param t
 	 * @param tCtx
 	 */
 	@SuppressWarnings("unused")
 	private boolean checkForInternalOccurencesOfVarInTerm(int varBeingChecked, int beingCheckedsContext, Term t, int tCtx) {
 		while (t.type == Term.VAR) {
 			final int vNr = ((Var) t).nrInStruct;
 			if (beingCheckedsContext == tCtx && varBeingChecked == vNr)
 				return true;
 			Term link = links.getTerm(vNr, tCtx);
 			if (link == null || link.type == Term.NUMBER || link.type == Term.ATOM)
 				return false;
 			t = link;
 			tCtx = links.getCtx(vNr, tCtx);
 			// if the Var was linked to a Var, the loop will run once more
 			// else t is a Struct and 'if (t instanceof Struct)' below will kick
 			// into action
 		}
 		if (t.type == Term.STRUCT) {
 			Var[] varList = ((Struct) t).getVarList();
 			if (varList == null)
 				return false;
 			boolean sameCtx = beingCheckedsContext == tCtx;
 			for (int i = 0; i < varList.length; i++) {
 				Var v = varList[i];
 				if (sameCtx && varBeingChecked == v.nrInStruct)
 					return true;
 				Term link = links.getTerm(v.nrInStruct, tCtx);
 				if (link == null || link.type == Term.NUMBER || link.type == Term.ATOM)
 					continue;
 				int linkCtx = links.getCtx(v.nrInStruct, tCtx);
 				return checkForInternalOccurencesOfVarInTerm(varBeingChecked, beingCheckedsContext, link, linkCtx);
 			}
 		}
 		return false;
 	}
 
 	/**
 	 * 
 	 * @param owner
 	 * @return // * @deprecated no longer supported. should be implemented anew
 	 *         if needed in f.ex. GUI or debugger.
 	 */
 	int[][] getKeysForCp(int owner) {
 		return gc.getGarbageLinks(owner);
 	}
 
 	/**
 	 * @param prolog
 	 * @param expression
 	 * @return result of the evaluation as a Number
 	 * @throws jTrolog.errors.PrologException
 	 *             instantiation error if one of the Variables to be evaluated
 	 *             is not instantiated type_error(Evaluable, other) if a part in
 	 *             the evaluable Term is not evaluable
 	 * @throws Throwable
 	 *             any other exception that might be thrown by parts of the
 	 *             expression to be evaluated
 	 */
 	public Number evalExpression(Prolog prolog, EvaluableTerm expression) throws PrologException, Throwable {
 		if (expression instanceof Number)
 			return (Number) expression;
 
 		Term child = null;
 		try {
 			Struct struct = (Struct) expression;
 			// chp 9 defines separate behavior for _evaluation_ of float/1
 			// (casting of Int) that should only accept Numbers,
 			// as opposed to the execution of float/1 that accepts Term.
 			if (struct.predicateIndicator == Parser.floatSignature) {
 				child = resolve(struct.getArg(0));
 				Number result = evalExpression(prolog, (EvaluableTerm) child);
 				return new Double(result.doubleValue());
 			}
 
 			PrimitiveInfo prim = prolog.getPrimitiveExp(struct);
 			if (prim == null)
 				throw new PrologException("type_error(Evaluable, " + struct.predicateIndicator + ")");
 
 			// we have an expression that might be evaluable
 			Object[] primitive_args = new Object[struct.arity + 1];
 			primitive_args[0] = this;
 			for (int i = 0; i < primitive_args.length - 1; i++) {
 				child = resolve(struct.getArg(i));
 				primitive_args[i + 1] = evalExpression(prolog, (EvaluableTerm) child);
 			}
 			return (Number) prim.method.invoke(prim.source, primitive_args);
 		} catch (ClassCastException e) {
 			if (child instanceof Var)
 				throw new PrologException("instantiation_error");
 			throw new PrologException("type_error(Evaluable, " + child + ")");
 		}
 	}
 
 	Object[] resolveArgs(Struct unresolved, int ctx) {
 		Object[] primitive_args = new Object[unresolved.arity + 1];
 		primitive_args[0] = this;
 		for (int i = 0; i < unresolved.arity; i++) {
 			final Term arg = unresolved.getArg(i);
 			Term link = resolveFaster(arg, ctx);
 			if (secondOutOfFasterResolve == Integer.MAX_VALUE)
 				primitive_args[i + 1] = wrapWithID(arg, ctx);
 			else
 				primitive_args[i + 1] = wrapWithID(link, secondOutOfFasterResolve);
 		}
 		return primitive_args;
 	}
 
 	public Term resolve(Term term) {
 		if (term instanceof WrapVar) {
 			final WrapVar wrapVar = ((WrapVar) term);
 			Term link = resolveFaster(wrapVar.getBasis(), wrapVar.getContext());
 			return secondOutOfFasterResolve == Integer.MAX_VALUE ? term : wrapWithID(link, secondOutOfFasterResolve);
 		}
 		return term;
 	}
 
 	int secondOutOfFasterResolve;
 
 	public Term resolveFaster(Term term, int ctx) {
 		secondOutOfFasterResolve = Integer.MAX_VALUE;
 		while (term instanceof Var) {
 			int vNr = ((Var) term).nrInStruct;
 			Term link = links.getTerm(vNr, ctx);
 			if (link == null)
 				break;
 			term = link;
 			ctx = secondOutOfFasterResolve = links.getCtx(vNr, ctx);
 		}
 		return term;
 	}
 
 	public Iterator structListIterator(Struct origin, boolean skipLastEmptyList) throws PrologException {
 		if (origin.equals(Term.emptyList))
 			return Term.iterator;
 		if (origin.predicateIndicator != Parser.listSignature)
 			throw new PrologException("type_error(list, " + origin + ")");
 		return new StructListIterator(origin, skipLastEmptyList);
 	}
 
 	public Struct createStructList(Collection complete) {
 		if (complete.isEmpty())
 			return Term.emptyList;
 		Struct res = (WrapStruct) wrapWithID(Parser.createListContainingAnyVars(complete.size() - 1));
 		Iterator toBeLinked = complete.iterator();
 		try {
 			for (Iterator it = structListIterator(res, true); it.hasNext();) {
 				Var child = (Var) it.next();
 				Term link = (Term) toBeLinked.next();
 				unify(child, link);
 			}
 		} catch (PrologException e) {
 			throw new RuntimeException("error in iterating a Struct list");
 		}
 		return res;
 	}
 
 	private class StructListIterator implements Iterator {
 
 		Iterator currentListIterator;
 		Term cache;
 		boolean includeLastEmptyList;
 
 		StructListIterator(Struct origin, boolean skipLastEmptyList) {
 			this.includeLastEmptyList = !skipLastEmptyList;
 			currentListIterator = Struct.iterator(origin);
 		}
 
 		public boolean hasNext() {
 			if (cache != null)
 				return true;
 			if (!currentListIterator.hasNext())
 				return false;
 			cache = (Term) currentListIterator.next();
 			cache = resolve(cache);
 
 			if (currentListIterator.hasNext())
 				return true;
 
 			if (cache.equals(Term.emptyList)) {
 				if (includeLastEmptyList)
 					return true;
 				cache = null;
 				return false;
 			}
 
 			if (!(cache instanceof Struct && ((Struct) cache).predicateIndicator == Parser.listSignature))
 				return true;
 
 			currentListIterator = Struct.iterator((Struct) cache);
 			cache = null;
 			return hasNext();
 		}
 
 		public Object next() {
 			if (cache == null)
 				hasNext();
 			if (cache == null)
 				throw new NoSuchElementException();
 			Term temp = cache;
 			cache = null;
 			return temp;
 		}
 
 		public void remove() {
 			throw new UnsupportedOperationException();
 		}
 	}
 
 	// todo override toString();
 
 	/**
 	 * See 7.1.6.1 Variants of a term in the ISO spec this method resolves all
 	 * the terms children. Not sure if this is in line with the spec.
 	 * 
 	 * @param original
 	 *            such as - f(X,Y,X) - g(A,B) - P + Q
 	 * @return a variant of the original such as - f(_1, _2, _1) - g(_1, _2) -
 	 *         _1 + _2
 	 */
 	public Term variant(Term original) {
 		return new Copier(original).getFlatVariant();
 	}
 
 	public Term flatCopy(Term original, int keepCtx) {
 		return new Copier(BindingsTable.wrapWithID(original, keepCtx), keepCtx).getFlatCopy();
 	}
 
 	private class Copier {
 		HashMap varTable = new HashMap();
 		Term original;
 		Term copy;
 		private int keepOriginals = -1;
 
 		public Copier(Term root) {
 			original = root;
 		}
 
 		public Copier(Term root, int ctxToKeep) {
 			original = root;
 			keepOriginals = ctxToKeep;
 		}
 
 		private Term copyRecursive(Term original) {
 			if (original instanceof StructAtom || original instanceof Number)
 				return original;
 			if (original instanceof Var) {
 				Term link = resolve(original);
 				if (link != original)
 					return copyRecursive(link);
 				if (link instanceof Wrapper && ((Wrapper) link).getContext() == keepOriginals)
 					return ((Wrapper) link).getBasis();
 				Var copyVar = (Var) varTable.get(link);
 				if (copyVar == null)
 					varTable.put(link, copyVar = new Var("_", varTable.size() + 1));
 				return copyVar;
 			}
 			Struct sOrig = (Struct) original;
 			Term[] clonedElements = new Term[sOrig.arity];
 			for (int i = 0; i < clonedElements.length; i++)
 				clonedElements[i] = copyRecursive(sOrig.getArg(i));
 			return new Struct(sOrig.name, clonedElements, sOrig.getOperatorType());
 		}
 
 		public Term getFlatVariant() {
 			if (copy != null)
 				return copy;
 			return copy = copyRecursive(this.original);
 		}
 
 		public Term getFlatCopy() {
 			if (copy != null)
 				return copy;
 			return copy = copyRecursive(this.original);
 		}
 
 	}
 }