/*
 * EvolpTransformer.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.
 */
package lp.trans;

/*
 * History:
 * v0.1 (2007-02-20): initial version
 * v0.9.0 (2007-05-06):
 * - public methods documented
 *
 * TODO docs + refactoring
 */

import java.util.ArrayList;
import java.util.Collections;
import java.util.HashMap;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
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.LpTerm;
import lp.struct.util.LpEncoder;
import lp.struct.util.LpBuffer;
import lp.unit.EvolpProgram;
import lp.unit.GeneralizedLogicProgram;
import lp.unit.LogicProgram;
import lp.unit.TransformedEvolp;

import static lp.unit.TransEvolpRuleType.*;

/**
 * Transforms an evolving logic program into an equivalent normal logic program.
 *
 * @author Martin Slota
 * @version 0.9.0
 */
public class EvolpTransformer {
	private final List<LogicProgram> programs;
	
	private List<LogicProgram> events;
	
	private final TransformationHelper helper;
	
	private final Map<LpAtom, AtomAppearance> appearances;
	
	private int eventCount;
	
	/**
	 * Creates a new instance of {@code EvolpTransformer}.
	 */
	public EvolpTransformer() {
		// initialize members
		programs = new ArrayList<LogicProgram>();
		events = new ArrayList<LogicProgram>();
		helper = new TransformationHelper();
		appearances = new HashMap<LpAtom, AtomAppearance>();
		eventCount = 0;
	}
	
	
	private AtomAppearance getData(LpAtom atom) {
		AtomAppearance result = appearances.get(atom);
		if (result == null) {
			result = new AtomAppearance(atom);
			appearances.put(atom, result);
		}
		return result;
	}
	
	/**
	 * Constructs the transformational equivalent of {@code evolp}.
	 *
	 * @param evolp the evolving logic program that should be transformed
	 * @return the normal logic program equivalent to {@code evolp}
	 * @throws IllegalArgumentException if {@code evolp.isGround()} returns
	 * {@code false}
	 */
	public TransformedEvolp transform(EvolpProgram evolp) {
		if (!evolp.isGround()) {
			throw new IllegalArgumentException(
					"Only grounded evolving logic programs are accepted!");
		}
		
		programs.clear();
		
		programs.add(evolp.getBaseProgram());
		events = evolp.getEvents();
		// read rules from the reader and remember them,
		// save the event count
		eventCount = events.size();
		
		// extract assertion rules and compute literal metadata
		// add RuleSets for assertion rules
		for (int i = 1; i < eventCount; i++)
			programs.add(new GeneralizedLogicProgram());
		
		// extract assertion rules from program rules
		for (LpRule r : programs.get(0))
			extractAssertions(r, 1, false);
		
		// extract assertion rules from event rules
		for (int i = 0; i < eventCount; i++) {
			for (LpRule r : events.get(i))
				extractAssertions(r, i + 1, true);
		}
		
		// extract atom appearances from rules
		for (int i = 0; i < eventCount; i++) {
			for (LpRule r : programs.get(i))
				extractAppearance(r, i + 1, false);
			for (LpRule r : events.get(i))
				extractAppearance(r, i + 1, true);
		}
		
		
		TransformedEvolp result = new TransformedEvolp();
		
		for (int group = 1; group <= eventCount; group++) {
			for (LpRule r : programs.get(0)) {
				result.add(helper.transform(r, group, false, 1),
						group, 						REWRITTEN_PROGRAM_RULE);
				outputRejection(result, r, group, 1, false);
			}
			for (LpRule r : events.get(group - 1)) {
				result.add(helper.transform(r, group, false, group),
						group, 						REWRITTEN_EVENT_RULE);
				outputRejection(result, r, group, group, false);
			}
			for (int level = 2; level <= group; level++)
				for (LpRule r : programs.get(level - 1)) {
					result.add(helper.transform(r, group, true, level),
							group, 							ASSERTABLE_RULE);
					outputRejection(result, r, group, level, true);
				}
		}
		
		
		for (AtomAppearance appear : appearances.values())
			appear.addRulesTo(result);
		appearances.clear();
		
		return result;
	}
	
	private void extractAssertions(LpRule startRule, int startLevel,
			boolean eventRule) {
		LpRule rule = startRule;
		boolean event = eventRule;
		int level = startLevel;
		boolean cont = true;
		while (level < eventCount && cont) {
			LpLiteral headLiteral = rule.getHead();
			LpAtom headAtom = headLiteral.getAtom();
			LpPredicate headPredicate = headAtom.getPredicate();
			cont = headLiteral.isPositive() && headPredicate.getArity() == 1 &&
					"assert".equals(headPredicate.getName());
			if (cont) {
				rule = (LpRule) headAtom.getArguments().get(0);
				if (event) {
					programs.get(level).add(rule);
					event = false;
				} else {
					for (int i = level; i < eventCount; i++) {
						programs.get(i).add(rule);
					}
				}
				level++;
			}
		}
	}
	
	private void extractAppearance(LpRule r, int level, boolean eventRule) {
		for (LpLiteral l : r.getBody())
			if (!l.isPositive())
				getData(l.getAtom()).addNegativeBodyAppearance(level,
						eventRule);
		LpLiteral l = r.getHead();
		getData(l.getAtom()).addHeadAppearance(level, eventRule,
				l.isPositive());
	}
	
	private void outputRejection(TransformedEvolp result, LpRule r, int group, int level, boolean assertion) {
		LpLiteral head = r.getHead();
		int oppositeLevel = appearances.get(head.getAtom()).nextOppositeLevel(
				group, level, head.isPositive());
		if (oppositeLevel > -1) {
			result.add(helper.makeIntroRejection(r, group, level, oppositeLevel, assertion),
					group, 					INTRO_REJECTION);
		}
	}
	
	private class TransformationHelper {
		private final LpBuffer encoder;
		
		public TransformationHelper() {
			encoder = LpEncoder.getBuffer();
		}
		
		public LpRule transform(LpRule rule, int group, boolean assertion, int level) {
			LpLiteral head = rule.getHead();
			LpLiteral newHead = transform(rule.getHead(), group, true);
			Set<LpLiteral> body = rule.getBody();
			int bodySize = assertion ? body.size() + 2 : body.size() + 1;
			Set<LpLiteral> newBody = new LinkedHashSet<LpLiteral>(bodySize);
			for (LpLiteral lit : body) {
				newBody.add(transform(lit, group, true));
			}
			if (assertion) {
				newBody.add(makeAssertionLiteral(rule, level));
			}
			newBody.add(makeRejectionAtom(head, group, level).getNegativeLiteral());
			return new LpRule(newHead, newBody);
		}
		
		private LpLiteral transform(LpLiteral lit, int group, boolean positive) {
			if (lit == null)
				return null;
			
			LpPredicate pred = lit.getPredicate();
			encoder.reset();
			encoder.append(lit.isPositive() ? "" : "_N");
			encoder.append(pred);
			encoder.append('N').append(Integer.toString(group));
			LpPredicate newPred = LpPredicate.getInstance(encoder.toString(),
					pred.getArity());
			
			List<LpTerm> newArgs = transform(lit.getArguments());
			
			return LpAtom.getInstance(newPred, newArgs).getLiteral(positive);
		}
		
		private LpLiteral transformPlain(LpLiteral lit, int group) {
			if (lit == null)
				return null;
			
			LpPredicate pred = lit.getPredicate();
			encoder.reset();
			encoder.append(pred.getName());
			encoder.append('N').append(Integer.toString(group));
			LpPredicate newPred = LpPredicate.getInstance(encoder.toString(),
					pred.getArity());
			
			List<LpTerm> newArgs = transform(lit.getArguments());
			
			return LpAtom.getInstance(newPred, newArgs).getLiteral(lit.isPositive());
		}
		
		private List<LpTerm> transform(List<LpTerm> args) {
			List<LpTerm> newArgs = new ArrayList<LpTerm>(args.size());
			for (LpTerm term : args) {
				newArgs.add(transform(term));
			}
			return newArgs;
		}
		
		private LpTerm transform(LpTerm term) {
			if (term instanceof LpConstant) {
				return LpConstant.getInstance(encoder.asString(term));
			}
			if (term instanceof LpRule) {
				return LpConstant.getInstance(encoder.asString(term));
			}
			LpCompoundTerm compound = (LpCompoundTerm)term;
			LpFunction newFun = LpFunction.getInstance(encoder.asString(
					compound.getFunction()), compound.getArguments());
			List<LpTerm> newArgs = transform(compound.getArguments());
			return LpCompoundTerm.getInstance(newFun, newArgs);
		}
		
		private LpLiteral makeAssertionLiteral(LpRule rule, int level) {
			LpPredicate prevAssert = LpPredicate.getInstance(
					"assertN" + Integer.toString(level - 1), 1);
			LpConstant ruleConst = LpConstant.getInstance(
					encoder.asString(rule));
			LpAtom assAtom = LpAtom.getInstance(prevAssert,
					Collections.singletonList((LpTerm)ruleConst));
			return assAtom.getPositiveLiteral();
		}
		
		private LpAtom makeRejectionAtom(LpLiteral lit, int group, int level) {
			LpLiteral transLit = transformPlain(lit, group);
			LpConstant litConst = LpConstant.getInstance(
					encoder.asString(transLit));
			
			LpPredicate rejPred = LpPredicate.getInstance("_rej", 2);
			List<LpTerm> args = new ArrayList<LpTerm>(2);
			args.add(LpConstant.getInstance(Integer.toString(level)));
			args.add(litConst);
			
			return LpAtom.getInstance(rejPred, args);
		}
		
		private LpRule makeIntroRejection(LpRule rule, int group, int fromLevel,
				int toLevel, boolean assertion) {
			LpLiteral head = rule.getHead();
			LpLiteral newHead = makeRejectionAtom(
					head.getAtom().getLiteral(!head.isPositive()), group,
					toLevel).getPositiveLiteral();
			Set<LpLiteral> newBody = new LinkedHashSet<LpLiteral>();
			for (LpLiteral lit : rule.getBody())
				newBody.add(transform(lit, group, true));
			if (assertion)
				newBody.add(makeAssertionLiteral(rule, fromLevel));
			return new LpRule(newHead, newBody);
		}
		
		private LpRule makePropagationRejection(LpLiteral lit, int group,
				int fromLevel, int toLevel) {
			LpLiteral head = makeRejectionAtom(lit, group, toLevel).getPositiveLiteral();
			Set<LpLiteral> body = Collections.singleton(
					makeRejectionAtom(lit, group, fromLevel).getPositiveLiteral());
			return new LpRule(head, body);
		}
		
		
		private LpRule makeDefaultAssumption(LpAtom atom, int group) {
			LpLiteral origLit = atom.getNegativeLiteral();
			LpLiteral head = transform(origLit, group, true);
			Set<LpLiteral> body = Collections.singleton(
					makeRejectionAtom(origLit, group, 0).getNegativeLiteral());
			return new LpRule(head, body);
		}
		
		private LpRule makeTotalityConstraint(LpAtom atom, int group) {
			Set<LpLiteral> body = new LinkedHashSet<LpLiteral>(2);
			body.add(transform(atom.getPositiveLiteral(), group, false));
			body.add(transform(atom.getNegativeLiteral(), group, false));
			return new LpRule(null, body);
		}
		
		
	}
	
	/**
	 * A container for metadata about an atom's appearance in the input program.
	 * First it needs to be filled with information by calling the methods
	 * {@link #addHeadAppearance(int, boolean, boolean)} and
	 * {@link #addNegativeBodyAppearance(int, boolean)}. Based on this data, it
	 * can formulate all default assumptions, propagation rejections and
	 * completeness constraints for the given atom.
	 *
	 * @author Martin Slota
	 * @version 0.9
	 */
	private class AtomAppearance {
		/**
		 *
		 */
		private final LpAtom forAtom;
		
		/**
		 *
		 */
		private final IntArrayWrapper posProgRuleHead;
		
		/**
		 *
		 */
		private final IntArrayWrapper negProgRuleHead;
		
		/**
		 *
		 */
		private final IntArrayWrapper posEventRuleHead;
		
		/**
		 *
		 */
		private final IntArrayWrapper negEventRuleHead;
		
		/**
		 *
		 */
		private int defFromGroup;
		
		/**
		 *
		 */
		private final IntArrayWrapper defInGroup;
		
		/**
		 *
		 * @param forAtom
		 */
		public AtomAppearance(LpAtom forAtom) {
			this.forAtom = forAtom;
			
			defFromGroup = eventCount + 1;
			defInGroup = new IntArrayWrapper(eventCount);
			
			posProgRuleHead = new IntArrayWrapper(eventCount);
			negProgRuleHead = new IntArrayWrapper(eventCount);
			
			posEventRuleHead = new IntArrayWrapper(eventCount);
			negEventRuleHead = new IntArrayWrapper(eventCount);
		}
		
		/**
		 *
		 * @param level
		 * @param eventRule
		 */
		public void addNegativeBodyAppearance(int level, boolean eventRule) {
			if (eventRule)
				defInGroup.add(level);
			else if (defFromGroup > level)
				defFromGroup = level;
		}
		
		/**
		 *
		 * @param level
		 * @param eventRule
		 * @param isPositive
		 */
		public void addHeadAppearance(int level, boolean eventRule,
				boolean isPositive) {
			IntArrayWrapper target = eventRule ? (isPositive ? posEventRuleHead
					: negEventRuleHead) : (isPositive ? posProgRuleHead
					: negProgRuleHead);
			target.add(level);
		}
		
		public int nextOppositeLevel(int group, int level, boolean positive) {
			if (positive) {
				if (group == level && negEventRuleHead.contains(level))
					return level;
				int max = negProgRuleHead.getMaxLeqThan(level);
				if (max == -1 && hasDefaultInGroup(group))
					return 0;
				return max;
			}
			if (group == level && posEventRuleHead.contains(level))
				return level;
			return posProgRuleHead.getMaxLeqThan(level);
		}
		

		public void addRulesTo(TransformedEvolp prog) {
			outputDefaults(prog);
			outputRejections(prog);
			outputConstraints(prog);
		}
		
		private boolean hasConstraintInGroup(int group) {
			boolean result = false;
			for (int i = 1; i < group; i++) {
				if (posProgRuleHead.contains(i) && negProgRuleHead.contains(i)) {
					result = true;
					break;
				}
			}
			if ((posProgRuleHead.contains(group) || posEventRuleHead.contains(group))
			&& (negProgRuleHead.contains(group) || negEventRuleHead.contains(group)))
				result = true;
			return result;
		}
		
		private boolean hasDefaultInGroup(int group) {
			if (group >= defFromGroup)
				return true;
			return defInGroup.contains(group) || hasConstraintInGroup(group);
		}
		
		private void outputDefaults(TransformedEvolp prog) {
			for (int group = 1; group <= eventCount; group++) {
				if (hasDefaultInGroup(group) || hasConstraintInGroup(group))
					prog.add(helper.makeDefaultAssumption(forAtom, group),
							group, 							DEFAULT_RULE);
				
			}
		}
		
		private void outputConstraints(TransformedEvolp prog) {
			for (int group = 1; group <= eventCount; group++) {
				if (hasConstraintInGroup(group))
					prog.add(helper.makeTotalityConstraint(forAtom, group),
							group, 							CONSTRAINT);
			}
		}
		
		private void outputRejections(TransformedEvolp prog) {
			for (int group = 1; group <= eventCount; group++) {
				boolean posEvent = posEventRuleHead.contains(group);
				boolean negEvent = negEventRuleHead.contains(group);
				boolean hasDefault = hasDefaultInGroup(group);
				int maxPos = posEvent ? group : posProgRuleHead
						.getMaxLeqThan(group);
				int maxNeg = negEvent ? group : negProgRuleHead
						.getMaxLeqThan(group);
				int i = 0;
				if (!posProgRuleHead.isEmpty()) {
					int toLevel = posProgRuleHead.get(0);
					int fromLevel;
					i = i + 1;
					while (i < posProgRuleHead.length()
					&& (fromLevel = posProgRuleHead.get(i)) <= maxNeg) {
						LpRule rule = helper.makePropagationRejection(forAtom.getPositiveLiteral(), group,
								fromLevel, toLevel);
						prog.add(rule, group, PROPAGATION_REJECTION);
						toLevel = fromLevel;
						i++;
					}
					if (posEvent && toLevel < group) {
						LpRule rule = helper.makePropagationRejection(forAtom.getPositiveLiteral(), group,
								group, toLevel);
						prog.add(rule, group, PROPAGATION_REJECTION);
					}
				}
				if (!negProgRuleHead.isEmpty()) {
					int toLevel, fromLevel;
					if (hasDefault) {
						toLevel = 0;
						i = 0;
					} else {
						toLevel = negProgRuleHead.get(0);
						i = 1;
					}
					while (i < negProgRuleHead.length()
					&& (fromLevel = negProgRuleHead.get(i)) <= maxPos) {
						LpRule rule = helper.makePropagationRejection(forAtom.getNegativeLiteral(), group,
								fromLevel, toLevel);
						prog.add(rule, group, PROPAGATION_REJECTION);
						toLevel = fromLevel;
						i++;
					}
					if (negEvent && toLevel < group) {
						LpRule rule = helper.makePropagationRejection(forAtom.getNegativeLiteral(), group,
								group, toLevel);
						prog.add(rule, group, PROPAGATION_REJECTION);
					}
				} else if (negEvent && hasDefault) {
					LpRule rule = helper.makePropagationRejection(forAtom.getNegativeLiteral(), group, group, 0);
					prog.add(rule, group, PROPAGATION_REJECTION);
				}
			}
		}
	}
}