/*
 * DlpGrounder.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:
 * v0.1 (2007-02-08): initial version
 * v0.2 (2007-02-08):
 * - implementation and tests
 * v0.2.1 (2007-02-11):
 * - changed to reflect the new LpAtom class
 * v0.2.2 (2007-02-12):
 * - changed because of changes in LpParser
 * v0.2.3 (2007-02-14):
 * - some changes because of LparseOutputFilter got merged with LparseWrapper
 * - some changes because of LpPrettyPrinter now has withSpaces instead of space
 *   string
 * v0.2.4 (2007-02-17):
 * - a bug in TaggedDlpParser fixed (didn't parse correctly lparse output for an
 *   empty initial program)
 * - setLparsePath and a default constructor added
 * v1.0.0 (2007-05-05):
 * - functionality that is common for this class and for LpGrounder was moved 
 *   to the Grounder class
 *
 * PENDING analyze and rewrite lparse messages into nicer messages (or write
 * jlparse :o)
 */

package lp.trans;

import java.io.Writer;
import java.util.Iterator;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Set;

import lp.parse.LpParser;
import static lp.parse.LpTokenType.*;

import lp.struct.LpAtom;
import lp.struct.LpLiteral;
import lp.struct.LpPredicate;
import lp.struct.LpRule;
import lp.struct.LpTerm;
import lp.struct.util.LpPrettyPrinter;

import lp.unit.GeneralizedLogicProgram;
import lp.unit.DynamicLogicProgram;
import lp.unit.LogicProgram;

import lp.wrap.LparseMessage;
import lp.wrap.LparseWrapper;

/**
 * Creates a grounded version of a {@link DynamicLogicProgram}. This means that
 * the resulting DLP {@code output} has the same answer sets as the original
 * DLP and {@code output.isGround()} returns {@code true}.
 *
 * The transformation is performed using {@link LparseWrapper} and can executed
 * by calling the {@link #ground(Object)} method.
 *
 * Lparse warnings (see {@link LparseWrapper#getWarnings()}) issued during the
 * grounding process are translated into {@link GrounderMessage}s and can be
 * retrieved through the {@link #getWarnings()} method.
 *
 * @author Martin Slota
 * @version 1.0.0
 * @see LparseWrapper
 */
public class DlpGrounder extends Grounder<DynamicLogicProgram> {
	/**
	 * Contains the length of the dynamic logic program that is being grounded.
	 * Is needed by {@link #parseOutput(String)} which doesn't have access to 
	 * the input program. Therefore, it is set in 
	 * {@link #printProgram(DynamicLogicProgram, Writer)}.
	 */
	private int programCount;
	
	/**
	 * This printer is used to dump rules in the original dynamic logic program
	 * into a single logic program. A literal is added to the body of each rule
	 * in order to remember which level of the DLP the rule comes from.
	 */
	private final DlpTagger<Writer> printer;
	
	/**
	 * Parses lparse's output and gets rid of the tagging literals again.
	 */
	private final DlpDetagger parser;
	
	/**
	 * Creates a new instance of {@code DlpGrounder} that creates its own
	 * {@link LparseWrapper} instance using its default constructors.
	 */
	public DlpGrounder() {
		this(new LparseWrapper());
	}
	
	/**
	 * Creates a new instance of {@code DlpGrounder} that uses the given object
	 * to invoke lparse and process its output.
	 *
	 * @param wrapper the object used to execute lparse, parse its warnings
	 * and/or errors and create corresponding LparseMessage objects
	 */
	public DlpGrounder(LparseWrapper wrapper) {
		super(wrapper);
		printer = new DlpTagger<Writer>(null);
		parser = new DlpDetagger();
	}
	
	/**
	 * {@inheritDoc}
	 */
	protected void printProgram(DynamicLogicProgram inputProgram,
			Writer writer) {
		programCount = inputProgram.size();
		// prepare the tagged program
		printer.reset();
		printer.setOut(writer);
		Iterator<LogicProgram> iter = inputProgram.iterator();
		if (iter.hasNext()) {
			for (LpRule r : iter.next()) {
				printer.append(r);
				printer.append('\n');
			}
			while (iter.hasNext()) {
				printer.incTagNumber();
				for (LpRule r : iter.next()) {
					printer.append(r);
					printer.append('\n');
				}
			}
		}
		// add a fact for each tagging literal that was previously used
		// this is necessary, otherwise lparse may decide that the rule's body
		// is not satisfiable and delete the rule completely
		printer.appendTagFacts();
		printer.close();
	}

	/**
	 * {@inheritDoc}
	 */
	protected GrounderMessage makeGrounderMessage(LparseMessage message,
			DynamicLogicProgram inputProgram) {
		// rule index
		int rIndex = message.getLineNumber() - 1;
		LpRule rule = null;
		// program index
		int pIndex = 0;
		if (inputProgram.size() > 0) {
			int pCount = inputProgram.size();
			int pRuleCount = inputProgram.get(0).size();
			// increment program index until we find the right program
			while (pIndex < pCount && rIndex >= pRuleCount) {
				rIndex -= pRuleCount;
				pIndex++;
				pRuleCount = inputProgram.get(pIndex).size();
			}
			if (pIndex < pCount) {
				rule = inputProgram.get(pIndex).get(rIndex);
			}
		}
		return new GrounderMessage(message.getMessage(), rule,
				message.isWarning(), message);
	}

	/**
	 * {@inheritDoc}
	 */
	protected DynamicLogicProgram parseOutput(String program) {
		// prepare the resulting DynamicLogicProgram
		DynamicLogicProgram result = new DynamicLogicProgram(programCount);
		for (int i = 0; i < programCount; i++)
			result.add(new GeneralizedLogicProgram());
		
		// prepare the parser to parse the output of lparse
		parser.setInput(program);
		
		// add the parsed rules to the result
		try {
			while (parser.hasMoreTokens()) {
				LpRule r = parser.parseRule();
				if (r != null)
					result.get(parser.getTagNumber()).add(r);
			}
		} finally {
			parser.close();
		}
		
		return result;
	}
	
	/**
	 * A special {@link lp.struct.LpStructureUnit} printer that:
	 * <ol>
	 *   <li>gets rid of negation in rule heads by prepending a "p_" or "n_"</li>
	 *   <li>adds a tagging literal to body of every rule. This literal is of
	 *   the form "tag#" where # is some non-negative number. It indicates which
	 *   program of the sequence the rule came from</li>
	 * </ol>
	 *
	 * @author Martin Slota
	 * @version 1.0.0
	 */
	private static class DlpTagger<W extends Writer> extends LpPrettyPrinter<W> {
		/**
		 * Contains the current tag number used for adding the tagging literals.
		 */
		private int tagNumber;
		
		/**
		 * Indicates whether a rule's head or a body literal is being processed.
		 */
		private boolean visitingHead;
		
		/**
		 * Creates a new instance of {@code TaggingPrettyPrinter}.
		 */
		public DlpTagger(W out) {
			super(out, ":-", false);
			reset();
		}
		
		public void reset() {
			tagNumber = 0;
		}
		
		/**
		 * Increments the tag number used for adding the tagging literals.
		 * Initially it is 0.
		 */
		public void incTagNumber() {
			tagNumber++;
		}
		
		/**
		 * Appends a textual form of a {@link LpRule} instance to this character
		 * sequence. Shouldn't be called directly,
		 * {@link #append(LpStructureUnit)} should be used instead.
		 *
		 * In case it has a negative literal in its head, it is output as a
		 * positive literal, but "n_" is prepended to the predicate's name. In
		 * case the head is a positive literal, "p_" is prepended to its head.
		 *
		 * Polarity of body literals is not changed but the "p_" is always
		 * prepended to their predicate names to recognize them from the tagging
		 * literal (lparse changes the order of literals so this couldn't be
		 * used). A tagging literal of the form "tag#" is added to each rule's
		 * body. The # is substituted with the current tag number.
		 *
		 * @param rule the {@code LpRule} instance whose textual
		 * representation should be appended to this character sequence
		 * @see lp.struct.util.LpPrinter
		 * @see lp.struct.LpStructureUnitVisitor#visit(LpRule)
		 * @throws NullPointerException if {@code rule} is {@code null}
		 */
		@Override
		public void visit(LpRule rule) {
			LpLiteral head = rule.getHead();
			Set<LpLiteral> body = rule.getBody();
			if (head != null) {
				visitingHead = true;
				visit(head);
				append(SPACE_STRING);
			}
			append(ARROW_STRING);
			append(SPACE_STRING);
			for (LpLiteral l : body) {
				visit(l);
				append(',');
				append(SPACE_STRING);
			}
			append("tag").append(Integer.toString(tagNumber));
			append('.');
		}
		
		/**
		 * Appends a textual form of a {@link LpLiteral} instance to this
		 * character sequence. Shouldn't be called directly,
		 * {@link #append(LpStructureUnit)} should be used instead.
		 *
		 * The behaviour of this method depends on the context of the given
		 * literal&#8212;whether it is a body literal or a head literal. See
		 * {@link #visit(LpRule)}.
		 *
		 * @param lit the {@code LpLiteral} instance whose textual
		 * representation should be appended to this character sequence
		 * @see lp.struct.util.LpPrinter
		 * @see lp.struct.LpStructureUnitVisitor#visit(LpLiteral)
		 * @throws NullPointerException if {@code lit} is {@code null}
		 */
		@Override
		public void visit(LpLiteral lit) {
			if (visitingHead) {
				append(lit.isPositive() ? "p_" : "n_");
				visitingHead = false;
			} else {
				if (!lit.isPositive()) {
					append("not ");
				}
				append("p_");
			}
			visit(lit.getAtom());
		}
		
		/**
		 * Appends facts with all tagging literals used until now to this
		 * character sequence.
		 */
		public void appendTagFacts() {
			for (int i = 0; i <= tagNumber; i++) {
				append("tag").append(Integer.toString(i)).append(".\n");
			}
		}
	}
	
	/**
	 * A special parser for parsing the grounded and tagged program. It filters
	 * out all tagging literals, both in rule bodies and in facts. It also
	 * eliminates the "p_" and "n_" prefixes from predicate names.
	 *
	 * @author Martin Slota
	 * @version 1.0.0
	 */
	private static class DlpDetagger extends LpParser {
		/**
		 * An internally used literal that indicates that a tag has been parsed.
		 * It is returned by {@link #parseLiteral()} and processed by 
		 * {@link #parseRule()}.
		 */
		private static final LpLiteral TAG = LpAtom.getInstance(
				LpPredicate.getInstance("tag", 0), null).getPositiveLiteral();
		
		/**
		 * The tag number of the last rule.
		 */
		private int tagNumber;
		
		/**
		 * Creates a new instance of {@code TaggedDlpParser}.
		 */
		public DlpDetagger() {
			super();
			tagNumber = 0;
		}
		
		/**
		 * {@inheritDoc}
		 */
		@Override
		public void setInput(CharSequence input) {
			super.setInput(input);
			tagNumber = 0;
		}
		
		/**
		 * Returns the tag number of the last rule.
		 */
		public int getTagNumber() {
			return tagNumber;
		}
		
		/**
		 * Parses and returns the next rule on input. Applies the changes
		 * described in class description.
		 *
		 * @return the parsed rule or {@code null} if no more rules follow
		 * @throws IOException (wrapped in an {@link lp.util.ExceptionAdapter})
		 * in case an I/O error occurs while tokenizing the input
		 * @throws LpParserException if the input is not parseable
		 */
		@Override
		public LpRule parseRule() {
			LpLiteral head;
			if (getLexer().getTokenType() == RULE_ARROW) {
				head = null;
			} else {
				head = parseLiteral();
			}
			
			while (hasMoreTokens() && head == TAG) {
				match(DOT);
				if (hasMoreTokens())
					head = parseLiteral();
			}
			
			if (!hasMoreTokens()) {
				return null;
			}
			
			Set<LpLiteral> body = null;
			
			if (getLexer().getTokenType() == RULE_ARROW) {
				nextToken();
				if (getLexer().getTokenType() == LOWERCASE_WORD) {
					body = new LinkedHashSet<LpLiteral>();
					LpLiteral l = parseLiteral();
					if (l != TAG)
						body.add(l);
					while (getLexer().getTokenType() == COMMA) {
						nextToken();
						l = parseLiteral();
						if (l != TAG)
							body.add(l);
					}
				}
			}
			
			match(DOT);
			
			return new LpRule(head, body);
		}
		
		/**
		 * Parses and returns the next literal on input. Applies the changes
		 * described in class description.
		 *
		 * @return the parsed literal or {@code null} if it was a tagging
		 * literal
		 * @throws IOException (wrapped in an {@link lp.util.ExceptionAdapter})
		 * in case an I/O error occurs while tokenizing the input
		 * @throws LpParserException if the input is not parseable
		 */
		@Override
		public LpLiteral parseLiteral() {
			boolean positive = true;
			if (getLexer().getTokenType() == LOWERCASE_WORD
					&& getLexer().getLexem().equals("not")) {
				positive = false;
				nextToken();
			}
			
			expect(LOWERCASE_WORD);
			String name = getLexer().getLexem();
			nextToken();
			if (name.startsWith("p_")) {
				name = name.substring(2);
			} else if (name.startsWith("n_")) {
				name = name.substring(2);
				positive = false;
			} else if (name.matches("tag[0-9]+")) {
				tagNumber = Integer.decode(name.substring(3));
				return TAG;
			} else if ("_false".equals(name)) {
				return null;
			} else {
				throw new IllegalArgumentException("Bad input program!");
			}
			
			List<LpTerm> arguments = parseArguments();
			
			LpPredicate pred = LpPredicate.getInstance(name, arguments);
			LpAtom atom = LpAtom.getInstance(pred, arguments);
			return atom.getLiteral(positive);
		}
	}
}