/*
 * EvolpPrettyPrinter.java
 *
 * Copyright (C) 2006 - 2007 Martin Slota
 *
 * This program is free software; you can redistribute it and/or modify it under
 * the terms of the GNU General Public License as published by the Free Software
 * Foundation; either version 2 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 Public License for more
 * details.
 *
 * You should have received a copy of the GNU General Public License along with
 * this program; if not, write to the Free Software Foundation, Inc., 51
 * Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA.
 */

/*
 * History:
 * v1.0.0 (2007-05-04):
 * - no version information kept before :P
 */

package lp.struct.util;

import java.io.StringWriter;
import java.io.Writer;
import java.util.Set;
import java.util.Stack;
import lp.struct.LpAtom;
import lp.struct.LpCompoundTerm;
import lp.struct.LpConstant;
import lp.struct.LpFunction;
import lp.struct.LpLiteral;
import lp.struct.LpPredicate;
import lp.struct.LpRule;
import lp.struct.LpStructureUnit;
import lp.struct.LpVariable;

/**
 * Transforms a logic program (or its components} represented by objects
 * implementing the {@link LpStructureUnit} interface into a human-readable
 * (standard) textual representation. In addition to the functionality of
 * {@link LpPrettyPrinter}, it also handles rules that appear as arguments of
 * predicate or function symbols correctly. Such rules do not end with a dot 
 * their the arrow separating their head from their body is never ommited and
 * they can be enclosed in parenthesis to prevent ambiguity.
 *
 * For example, an atom with the predicate {@code p/2}, the rule {@code a <- b.}
 * as the first argument and the term {@code f(X)} as the second argument will
 * be written as {@code p((a <- b), f(X))}.
 *
 * @author Martin Slota
 * @version 1.0.0
 */
public class EvolpPrettyPrinter<W extends Writer> extends LpPrettyPrinter<W> {
	/**
	 * A convenience method that creates a new {@link LpBuffer} that uses a new
	 * {@link EvolpPrettyPrinter} instance to write {@link LpStructureUnit}s.It
	 * will use the string "<-" to separate the head and body of a rule. The
	 * output will also contain extra spaces to enhance readability.
	 *
	 * @return as specified above
	 * @see LpBuffer
	 */
	public static LpBuffer getBuffer() {
		return new LpBuffer(new EvolpPrettyPrinter<StringWriter>(
				new StringWriter()));
	}
	
	/**
	 * A convenience method that creates a new {@link LpBuffer} that uses a new
	 * {@link EvolpPrettyPrinter} instance to write {@link LpStructureUnit}s. It
	 * will use the string {@code arrow} to separate the head and body of a
	 * rule. If {@code withSpaces} is {@code true}, then the output will also
	 * contain extra spaces to enhance readability.
	 *
	 * @param arrow the string to separate the head and body of a rule
	 * @param withSpaces determines whether extra spaces should be added to
	 * places where they can make the output more readable
	 * @return as specified above
	 * @see LpBuffer
	 */
	public static LpBuffer getBuffer(String arrow, boolean withSpaces) {
		return new LpBuffer(new EvolpPrettyPrinter<StringWriter>(
				new StringWriter(), arrow, withSpaces));
	}
	
	/**
	 * Is set to {@code true} when a rule or a compound term is being appended.
	 * In such a case the class remembers a "position" inside the structure so
	 * that it can treat inner and outer rules differently and put the inner
	 * rules in parenthesis where appropriate.
	 */
	protected boolean trackPosition;
	
	/**
	 * If {@code trackPosition} is {@code true}, this stack holds the numbers of
	 * remaining inner terms of function and predicate symbols. The first number
	 * relates to the inner-most symbol, the last number relates to the
	 * outer-most symbol.
	 */
	protected final Stack<MutableInteger> innerTermsLeft;
	
	/**
	 * Creates a new instance of {@code EvolpPrettyPrinter}. It will use the
	 * string "<-" to separate the head and body of a rule. The output will also
	 * contain extra spaces to enhance readability.
	 *
	 * @param out the underlying writer into which everything will be written
	 */
	public EvolpPrettyPrinter(W out) {
		this(out, "<-", true);
	}
	
	/**
	 * Creates a new instance of {@code EvolpPrettyPrinter}. It will use the
	 * string {@code arrow} to separate the head and body of a rule. If
	 * {@code withSpaces} is {@code true}, then the output will also contain
	 * extra spaces to enhance readability.
	 *
	 * @param out the underlying writer into which everything will be written
	 * @param arrow the string to separate the head and body of a rule
	 * @param withSpaces determines whether extra spaces should be added to
	 * places where they can make the output more readable
	 * @throws IllegalArgumentException if {@code arrow} is {@code null}
	 */
	public EvolpPrettyPrinter(W out, String arrow, boolean withSpaces) {
		super(out, arrow, withSpaces);
		innerTermsLeft = new Stack<MutableInteger>();
	}
	
	/**
	 * Writes a textual representation of {@code unit} to this
	 * {@code LpPrinter}. The string is constructed in the {@code #visit()}
	 * methods.
	 *
	 * @param unit the {@code LpStructureUnit} that should be represented
	 * as a string and appended to the underlying {@code Writer}
	 * @throws IllegalArgumentException if {@code unit} is {@code null}
	 * @throws IOException (wrapped in an {@link lp.util.ExceptionAdapter}) in
	 * case an I/O exception occurs while writing to the underlying
	 * {@code Writer}
	 */
	@Override
	public void write(LpStructureUnit unit) {
		if (unit == null)
			throw new IllegalArgumentException(
					"The object to be written must not be null!");
		trackPosition = (unit instanceof LpRule
				|| unit instanceof LpCompoundTerm
				|| unit instanceof LpAtom);
		unit.accept(this);
		assert innerTermsLeft.isEmpty();
	}
	
	/**
	 * If {@link #trackPosition} is {@code true}, 1 one is subtracted from the
	 * topmost integer in {@link #innerTermsLeft}. Is called when a term is
	 * appended to keep track of how many inner terms are left.
	 */
	protected void registerTerm() {
		if (trackPosition && !innerTermsLeft.empty()) {
			MutableInteger peek = innerTermsLeft.peek();
			peek.decrement();
			if (peek.getValue() == 0)
				innerTermsLeft.pop();
		}
	}
	
	/**
	 * {@inheritDoc}
	 */
	@Override
	public void visit(LpConstant con) {
		super.visit(con);
		registerTerm();
	}
	
	/**
	 * {@inheritDoc}
	 */
	@Override
	public void visit(LpVariable var) {
		super.visit(var);
		registerTerm();
	}
	
	/**
	 * {@inheritDoc}
	 */
	@Override
	public void visit(LpFunction fun) {
		super.visit(fun);
		if (trackPosition) {
			int arity = fun.getArity();
			if (arity > 0)
				innerTermsLeft.push(new MutableInteger(fun.getArity()));
		}
	}
	
	/**
	 * {@inheritDoc}
	 */
	@Override
	public void visit(LpCompoundTerm term) {
		super.visit(term);
		registerTerm();
	}
	
	/**
	 * {@inheritDoc}
	 */
	@Override
	public void visit(LpPredicate pred) {
		super.visit(pred);
		if (trackPosition) {
			int arity = pred.getArity();
			if (arity > 0)
				innerTermsLeft.push(new MutableInteger(pred.getArity()));
		}
	}
	
	/**
	 * Takes care of writing an ordinary rule, just like {@link LpPrettyPrinter}
	 * does.
	 *
	 * @param rule the rule to write
	 * @throws NullPointerException if {@code rule} is {@code null}
	 * @throws IOException (wrapped in an {@link lp.util.ExceptionAdapter}) in
	 * case an I/O exception occurs while writing to the underlying 
	 * {@code Writer}
	 */
	protected void appendOuterRule(LpRule rule) {
		appendRuleNoDot(rule);
		dot();
	}
	
	/**
	 * Appends an inner rule, i.e. it is appended without the trailing dot, the
	 * separating arrow is never ommited and it is enclosed in parenthesis if 
	 * more terms follow after the rule and the body of the rule is non-empty.
	 *
	 * @param rule the rule to write
	 * @throws NullPointerException if {@code rule} is {@code null}
	 * @throws IOException (wrapped in an {@link lp.util.ExceptionAdapter}) in
	 * case an I/O exception occurs while writing to the underlying 
	 * {@code Writer}
	 */
	protected void appendInnerRule(LpRule rule) {
		MutableInteger peek = innerTermsLeft.peek();
		Set<LpLiteral> body = rule.getBody();
		
		boolean needParens =
				peek.getValue() > 1 && !body.isEmpty();
		
		if (needParens)
			beginParen();
		
		appendRuleNoDot(rule);
		if (body.isEmpty()) {
			space();
			arrow();
		}
		
		if (needParens)
			endParen();
	}
	
	/**
	 * Appends a natural textual form of a {@link LpRule} instance to this
	 * {@link LpPrinter}. Shouldn't be called directly,
	 * {@link #append(LpStructureUnit)} should be used instead.
	 *
	 * A natural form of a rule consists of the natural form of its head
	 * followed by special separator (set in the constructor) and natural forms
	 * of literals in its body, separated from each other by commas.
	 *
	 * If {@link LpRule#getHead()} is {@code null}, the natural form
	 * begins with the separator string (the head's natural form is left out).
	 * If {@link LpRule#getBody()} is {@code null} or has no
	 * members, the natural form only consists of the head's natural form.
	 *
	 * In case the rule is an outer rule (i.e. not inside a function or
	 * predicate symbol), it is ended with a dot. If it is an inner rule, the
	 * separator string is never omitted and the rule will be put into
	 * parenthesis if more terms follow in the argument list of the closest
	 * function or predicate symbol (without the parenthesis an ambiguity would
	 * arise).
	 *
	 * @param rule the {@code LpRule} instance whose natural textual
	 * representation should be appended to the underlying {@code Writer}
	 * @throws NullPointerException if {@code rule} is {@code null}
	 * @throws IOException (wrapped in an {@link lp.util.ExceptionAdapter}) in
	 * case an I/O exception occurs while writing to the underlying 
	 * {@code Writer}
	 * @see LpPrinter
	 * @see lp.struct.LpStructureUnitVisitor#visit(LpRule)
	 */
	@Override
	public void visit(LpRule rule) {
		if (innerTermsLeft.empty()) {
			appendOuterRule(rule);
		} else {
			appendInnerRule(rule);
			registerTerm();
		}
	}
	
	/**
	 * A wrapper class for a mutable integer.
	 */
	private static class MutableInteger {
		/**
		 * The integer value.
		 */
		private int value;
		
		/**
		 * Constructs a new instance that initially holds the value
		 * {@code initialValue}.
		 *
		 * @param initialValue the initial value for the new instance
		 */
		public MutableInteger(int initialValue) {
			value = initialValue;
		}
		
		/**
		 * Returns the current value.
		 *
		 * @return an integer with the current value
		 */
		public int getValue() {
			return value;
		}
		
		/**
		 * Subtracts 1 from the current value.
		 */
		public void decrement() {
			value--;
		}
	}
}