package at.ac.tuwien.kr.alpha.common.terms;

import at.ac.tuwien.kr.alpha.grounder.Substitution;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;

/**
 * Common representation of Terms. Terms are constructed such that each term is represented by a unique object, hence term equality can be checked by object
 * reference comparison. Each concrete subclass of a Term must implement a factory-like method to obtain instances.
 *
 * We use {@link Comparable} to establish the following ordering among terms:
 * <ol>
 * <li>Constant terms according to their corresponding object and its type
 * <ol>
 * <li>{@link ConstantTerm<Integer>} ordered by value of the integers</li>
 * <li>{@link ConstantTerm<String>} and symbolic, lexicographically ordered on the symbol</li>
 * <li>{@link ConstantTerm<String>} lexicographically
 * <li>{@link ConstantTerm} for all other types, where {@link Comparable#compareTo(Object)} is used as ordering whenever possible (i.e. two terms' objects have
 * the same type). For two terms with objects of different type, the result is the lexicographic ordering of the type names.</li>
 * </ol>
 * </li>
 * <li>Function terms (ordered by arity, functor name, and then on their argument terms).</li>
 * <li>Variable terms (lexicographically ordered on their variable names)</li>
 * </ol>
 *
 * Copyright (c) 2016-2017, the Alpha Team.
 */
public abstract class Term implements Comparable<Term> {
	public abstract boolean isGround();

	public abstract List<VariableTerm> getOccurringVariables();

	/**
	 * Applies a substitution, result may be nonground.
	 * 
	 * @param substitution the variable substitution to apply.
	 * @return the non-substitute term where all variable substitutions have been applied.
	 */
	public abstract Term substitute(Substitution substitution);

	private static int priority(Term term) {
		final Class<?> clazz = term.getClass();
		if (clazz.equals(ConstantTerm.class)) {
			return 1;
		} else if (clazz.equals(FunctionTerm.class)) {
			return 2;
		} else if (clazz.equals(VariableTerm.class)) {
			return 3;
		}
		throw new UnsupportedOperationException("Can only compare constant term, function terms and variable terms among each other.");
	}

	@Override
	public int compareTo(Term o) {
		return o == null ? 1 : Integer.compare(priority(this), priority(o));
	}

	/**
	 * Rename all variables occurring in this Term by prefixing their name.
	 * 
	 * @param renamePrefix the name to prefix all occurring variables.
	 * @return the term with all variables renamed.
	 */
	public abstract Term renameVariables(String renamePrefix);

	public abstract Term normalizeVariables(String renamePrefix, RenameCounter counter);

	public static class RenameCounter {
		int counter;
		final HashMap<VariableTerm, VariableTerm> renamedVariables;

		public RenameCounter(int startingValue) {
			counter = startingValue;
			renamedVariables = new HashMap<>();
		}
	}

	public static List<Term> renameTerms(List<Term> terms, String prefix, int counterStartingValue) {
		List<Term> renamedTerms = new ArrayList<>(terms.size());
		Term.RenameCounter renameCounter = new Term.RenameCounter(counterStartingValue);
		for (Term term : terms) {
			renamedTerms.add(term.normalizeVariables(prefix, renameCounter));
		}
		return renamedTerms;
	}

	@Override
	public abstract boolean equals(Object o);

	@Override
	public abstract int hashCode();
	
}

@@ -42,61 +42,8 @@
 s;%0A%0A
-import at.ac.tuwien.kr.alpha.grounder.Substitution;%0A%0A
 impo
@@ -116,16 +116,86 @@
 .List;%0A%0A
+import at.ac.tuwien.kr.alpha.grounder.Substitution;%0A%0A//@formatter:off%0A
 /**%0A * C
@@ -307,16 +307,19 @@
 t, hence
+%0A *
  term eq
@@ -349,19 +349,16 @@
 y object
-%0A *
  referen
@@ -421,16 +421,19 @@
 lement a
+%0A *
  factory
@@ -546,32 +546,33 @@
 g terms:%0A * 
+%09
 %3Col%3E%0A * 
 %3Cli%3EConstant
@@ -555,24 +555,26 @@
  * %09%3Col%3E%0A * 
+%09%09
 %3Cli%3EConstant
@@ -636,24 +636,27 @@
 type%0A * 
+%09%09%09
 %3Col%3E%0A * 
 %3Cli%3E%7B@li
@@ -643,24 +643,28 @@
  %09%09%09%3Col%3E%0A * 
+%09%09%09%09
 %3Cli%3E%7B@link C
@@ -718,32 +718,36 @@
 ntegers%3C/li%3E%0A * 
+%09%09%09%09
 %3Cli%3E%7B@link Const
@@ -821,24 +821,28 @@
 bol%3C/li%3E%0A * 
+%09%09%09%09
 %3Cli%3E%7B@link C
@@ -879,24 +879,28 @@
 phically%0A * 
+%09%09%09%09
 %3Cli%3E%7B@link C
@@ -1004,17 +1004,24 @@
 whenever
- 
+%0A * %09%09%09%09
 possible
@@ -1050,19 +1050,16 @@
 cts have
-%0A *
  the sam
@@ -1113,16 +1113,24 @@
 t type, 
+%0A *%09 %09%09%09
 the resu
@@ -1181,32 +1181,35 @@
  names.%3C/li%3E%0A * 
+%09%09%09
 %3C/ol%3E%0A * %3C/li%3E%0A 
@@ -1201,16 +1201,18 @@
 /ol%3E%0A * 
+%09%09
 %3C/li%3E%0A *
@@ -1208,24 +1208,26 @@
  %09%09%3C/li%3E%0A * 
+%09%09
 %3Cli%3EFunction
@@ -1309,16 +1309,18 @@
 /li%3E%0A * 
+%09%09
 %3Cli%3EVari
@@ -1427,10 +1427,10 @@
 6-20
-17
+20
 , th
@@ -1447,16 +1447,32 @@
 am.%0A */%0A
+//@formatter:on%0A
 public a
@@ -3472,12 +3472,11 @@
 Code();%0A
-%09
 %0A%7D%0A

improve javadoc formatting