/*
 * EvolpSolver.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-06):
 * - no version information kept before :P
 *
 * PENDING create a junit test
 */

package lp.trans;

import java.io.BufferedReader;
import java.io.File;
import java.io.FileReader;
import java.io.IOException;
import java.io.Reader;
import java.io.StringReader;
import java.util.List;

import lp.parse.EvolpParser;

import lp.struct.LpAtom;
import lp.struct.LpPredicate;
import lp.struct.LpTerm;

import lp.unit.StableModel;

import lp.wrap.LparseWrapper;
import lp.wrap.SmodelsWrapper;

import static lp.parse.LpTokenType.*;

import lp.unit.EvolutionStableModel;
import lp.util.ExceptionAdapter;

/**
 * A class that computes evolution stable models of an evoluving logic program
 * given its transformational equivalent.
 *
 * @author Martin Slota
 * @version 1.0.0
 */
public class EvolpSolver extends Solver<EvolutionStableModel> {
	/**
	 * Parser used to convert the string representation of a model into object
	 * representations of the atoms in the model.
	 */
	private final TransEvolpParser parser;
	
	/**
	 * Contains the length of the resulting evolution stable model.
	 */
	private int modelLength;
	
	/**
	 * Creates a new instance of {@code EvolpSolver}. It will also create new
	 * instances of {@link LparseWrapper} and {@link SmodelsWrapper}. They are
	 * used them to compute the stable models of transformational equivalents of
	 * evolving logic programs passed in through the
	 * {@link #solve(LogicProgram, Consumer)} method.
	 */
	public EvolpSolver() {
		this(new LparseWrapper(), new SmodelsWrapper());
	}
	
	/**
	 * Creates a new instance of {@code EvolpSolver}. It will use the given
	 * instances of {@link LparseWrapper} and {@link SmodelsWrapper} classes and
	 * use them to compute the stable models of transformational equivalents of
	 * evolving logic programs passed in through the
	 * {@link #solve(LogicProgram, Consumer)} method.
	 *
	 * @param lparseWrapper the object used to execute lparse
	 * @param smodelsWrapper the object used to execute smodels
	 */
	public EvolpSolver(LparseWrapper lparseWrapper,
			SmodelsWrapper smodelsWrapper) {
		super(lparseWrapper, smodelsWrapper);
		parser = new TransEvolpParser();
	}
	
	/**
	 * Sets the desired length of computed evolution stable models.
	 */
	public void setModelLength(int modelLength) {
		this.modelLength = modelLength;
	}
	
	/**
	 * {@inheritDoc}
	 */
	protected EvolutionStableModel parseModel(String modelString) {
		EvolutionStableModel result = new EvolutionStableModel();
		for (int i = 0; i < modelLength; i++)
			result.add(new StableModel());
		parser.setInput(modelString);
		while (parser.hasMoreTokens()) {
			LpAtom a = parser.parseAtom();
			if (a != null) {
				int group = parser.getGroup();
				result.get(group - 1).add(a);
			}
		}
		parser.close();
		return result;
	}
	
	/**
	 * Special parser that recognizes the indexation of atoms in the normal
	 * logic program that was constructed by the transformation from an evolving
	 * logic program.
	 */
	private class TransEvolpParser extends EvolpParser {
		/**
		 * Contains the index of the last atom that was parsed.
		 */
		private int group;
		
		/**
		 * Used internally to remember whether we are parsing a top-level atom
		 * or some atom that is part of an inner rule.
		 */
		private boolean topLevel = true;
		
		/**
		 * {@inheritDoc}
		 */
		@Override
		public void setInput(CharSequence input) {
			if (input == null)
				throw new IllegalArgumentException(
						"The source string cannot be null!");
			setInput(new StringReader(input.toString()));
		}
		
		/**
		 * {@inheritDoc}
		 */
		@Override
		public void setInput(File file) {
			if (file == null)
				throw new IllegalArgumentException(
						"The source file cannot be null!");
			try {
				setInput(new BufferedReader(new FileReader(file)));
			} catch (IOException e) {
				throw new ExceptionAdapter(e);
			}
		}
		
		/**
		 * {@inheritDoc}
		 */
		@Override
		public void setInput(Reader input) {
			super.setInput(new Decoder(input));
		}
		
		/**
		 * Parses an atom in a normal way but cuts off the indexation suffix
		 * "N([0-9]+)" and stores $1. It can be later retrieved by calling the
		 * {@link #getGroup()} method.
		 */
		@Override
		public LpAtom parseAtom() {
			if (topLevel) {
				expect(LOWERCASE_WORD);
				String name = getLexer().getLexem();
				int posN = name.lastIndexOf('N');
				group = Integer.parseInt(name.substring(posN + 1));
				name = name.substring(0, name.lastIndexOf('N'));
				
				topLevel = false;
				nextToken();
				List<LpTerm> arguments = parseArguments();
				topLevel = true;
				
				LpPredicate pred = LpPredicate.getInstance(name, arguments);
				return LpAtom.getInstance(pred, arguments);
			} else {
				return super.parseAtom();
			}
		}
		
		/**
		 * Returns the index of the last atom that was parsed.
		 */
		public int getGroup() {
			return group;
		}
	}
	
	/**
	 * A filtering reader that decodes logic programming constructs previously
	 * encoded by {@link lp.struct.util.LpEncoder}. Decoding means replacing
	 * each occurence of
	 * <ul>
	 * <li>'L' with '('</li>
	 * <li>'R' with ')'</li>
	 * <li>'C' with ','</li>
	 * <li>'A' with "<-"</li>
	 * <li>'D' with '.'</li>
	 * <li>'_N' with "not "</li>
	 * <li>"_l" with 'L',</li>
	 * <li>"_r" with 'R',</li>
	 * <li>"_c" with 'C',</li>
	 * <li>"_a" with 'A' and</li>
	 * <li>"_d" with 'D'.</li>
	 * </ul>
	 */
	private static class Decoder extends Reader {
		/**
		 * The underlying {@code Reader}.
		 */
		private final Reader in;
		
		/**
		 * A small buffer used in case a single character in the original input
		 * corresponds to more characters after the decoding filter is applied.
		 */
		private final char[] buffer;
		
		/**
		 * Position in the buffer.
		 */
		private int top;
		
		/**
		 * Creates a new instance of {@code Decoder} that filters the contents
		 * of {@code in}.
		 *
		 * @param in the underlying {@code Reader}
		 */
		public Decoder(Reader in) {
			this.in = in;
			buffer = new char[3];
			top = -1;
		}
		
		/**
		 * Returns the next character after applying the filter to the original
		 * input.
		 *
		 * @return the next character or -1 if the end has been reached
		 * @throws IOException if an I/O error occurs while reading from the
		 * underlying {@code Reader}
		 */
		@Override
		public int read() throws IOException {
			int c;
			if (top > -1) {
				c = buffer[top];
				top--;
			} else {
				c = in.read();
				switch (c) {
					case '_':
						c = in.read();
						if (c == 'N') {
							c = 'n';
							buffer[2] = 'o';
							buffer[1] = 't';
							buffer[0] = ' ';
							top = 2;
						} else {
							c = Character.toUpperCase(c);
						}
						break;
					case 'L': c = '('; break;
					case 'R': c = ')'; break;
					case 'C': c = ','; break;
					case 'A': buffer[0] = '-'; top = 0; c = '<'; break;
					case 'D': c = '.'; break;
				}
			}
			System.out.print((char)c);
			return c;
		}
		
		/**
		 * Reads to a character buffer.
		 *
		 * @param cbuf destination buffer
		 * @param off offset at which to start storing characters
		 * @param len maximum number of characters to read
		 * @return the number of characters read, or -1 if the end of the stream
		 * has been reached
		 * @throws IOException if an I/O error occurs while reading from the
		 * underlying {@code Reader}
		 */
		public int read(char[] cbuf, int off, int len) throws IOException {
			int c = read();
			if (c == -1)
				return -1;
			int pos = off;
			int maxPos = off + len - 1;
			while (c != -1 && pos <= maxPos) {
				cbuf[pos] = (char)c;
				pos++;
				c = read();
			}
			return (pos - off);
		}
		
		/**
		 * Closes the underlying {@code Reader}.
		 *
		 * @throws IOException if an I/O error occurs
		 */
		public void close() throws IOException {
			in.close();
		}
	}
}