/*
 * EvolpVarTransformer.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.5.0 (2007-05-06):
 * - no version information kept before :P
 */

package lp.trans;

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

/**
 * Transforms an evolving logic program into an equivalent dynamic logic
 * program.
 *
 * @author Martin Slota
 * @version 0.5.0
 */
public class EvolpVarTransformer {
	private final List<LogicProgram> programs;
	
	private List<LogicProgram> events;
	
	private int eventCount;
	
	private final DlpGrounder grounder;
	
	private final TransformationHelper helper;
	
	/**
	 * Creates a new instance of {@code EvolpVarTransformer}.
	 */
	public EvolpVarTransformer() {
		// initialize members
		programs = new ArrayList<LogicProgram>();
		events = new ArrayList<LogicProgram>();
		eventCount = 0;
		grounder = new DlpGrounder();
		helper = new TransformationHelper();
	}
	
	/**
	 * Sets the path to lparse binary that is used to invoke lparse.
	 *
	 * @param lparsePath path to the lparse binary
	 * @throws IllegalArgumentException if {@code lparsePath} is {@code null} or
	 * an empty string
	 */
	public void setLparsePath(String lparsePath) {
		grounder.setLparsePath(lparsePath);
	}
	
	/**
	 * Constructs a dynamic logic program that is equivalent to the evolving
	 * logic program {@code evolp}.
	 *
	 * @param evolp the evolving logic program that should be transformed
	 * @return the dynamic logic program equivalent to {@code evolp}
	 */
	public DynamicLogicProgram transform(EvolpProgram evolp) {
		programs.clear();
		programs.add(evolp.getBaseProgram());
		events = evolp.getEvents();
		
		// save the event count
		eventCount = events.size();
		
		DynamicLogicProgram dlp = new DynamicLogicProgram();
		for (int group = 1; group <= eventCount; group++) {
			dlp.add(new GeneralizedLogicProgram());
		}
		
		helper.reset();
		for (int group = 1; group <= eventCount; group++) {
			for (int level = 0; level < group; level++) {
				LogicProgram current = dlp.get(level);
				for (LpRule r : programs.get(level)) {
					current.add(helper.transform(r, group, level));
				}
			}
			LogicProgram current = dlp.get(group - 1);
			for (LpRule r : events.get(group - 1)) {
				current.add(helper.transform(r, group, 0));
			}
			if (!dlp.isGround())
				dlp = grounder.ground(dlp);
			
			
			LogicProgram newProg = new GeneralizedLogicProgram();
			String assertName = "assertN" + group;
			for (int level = 0; level < group; level++) {
				for (LpRule r : dlp.get(level)) {
					LpPredicate headPred = r.getHead().getPredicate();
					if (assertName.equals(headPred.getName()) &&
							headPred.getArity() == 1) {
						newProg.add(helper.decode(
								(LpConstant)r.getHead().getArguments().get(0)));
					}
				}
			}
			programs.add(newProg);
		}
		
		return dlp;
	}
	
	/* PENDING create a test case from this
	public static void main(String [] args) {
		String source =
				"assert(assert(p(X) <- d(X)) <-) <- d(X). d(0)." +
				"newEvents.d(1)." +
				"newEvents.assert(assert(a(X) <- p(X)) <- )." +
				"newEvents.assert(d(2) <-)." +
				"newEvents." +
				"newEvents.";
		source =
				"a :- not b.\n" +
				"b :- not a.\n" +
				"assert(X) :- p(X)." +
				"newEvents.\n assert(d <-)." +
				"newEvents.\n p(f <-)." +
				"c :- a.\n" +
				"not c :- a. newEvents.";
		source =
				"a <- not b." +
				"b <- not a." +
				"assert(c <-) <- a." +
				"assert(not c <-) <- a." +
				"newEvents." +
				"newEvents.";
		source =
				"assert(assert(p(X) <- d(X), not g(h(i))) <-) <- d(X). d(0)." +
				"newEvents.d(1)." +
				"newEvents.assert(assert(a(X) <- d(X), p(X)) <- )." +
				"newEvents.assert(d(2) <-)." +
				"newEvents." +
				"newEvents.g(h(i)).";
		EvolpParser parser = new EvolpParser();
		parser.setInput(source);
		EvolpProgram evolp = parser.parseEvolp();
		
		EvolpVarTransformer transformer = new EvolpVarTransformer();
		LogicProgram transformed = new DlpTransformer().transform(transformer.transform(evolp));
		
		EvolpSolver solver = new EvolpSolver();
		solver.setModelLength(evolp.getEvents().size());
	

		solver.solve(transformed, new Consumer<EvolutionStableModel>() {
			public void beforeConsuming() {
				//
			}
			
			public void afterConsuming() {
				//
			}
			
			public void consume(EvolutionStableModel model) {
				System.out.println(model);
			}
		});
		
		// extract the rules that could be asserted in the next program
		// transform the group-th DLP
		// add transformed rules to transformed EVOLP
		for (LpRule r : transformed)
			System.out.println(r);
	}*/
	
	private class TransformationHelper {
		private final LpBuffer encoder;
		
		private final HashMap<LpConstant, LpRule> decoder;
		
		public TransformationHelper() {
			encoder = LpEncoder.getBuffer();
			decoder = new HashMap<LpConstant, LpRule>();
		}
		
		public void reset() {
			decoder.clear();
		}
		
		public LpRule decode(LpConstant encoded) {
			return decoder.get(encoded);
		}
		
		public LpRule transform(LpRule rule, int group, int assertLevel) {
			LpLiteral newHead = transform(rule.getHead(), group);
			Set<LpLiteral> body = rule.getBody();
			boolean assertion = (assertLevel > 0);
			int bodySize = assertion ? body.size() + 1 : body.size();
			Set<LpLiteral> newBody = new LinkedHashSet<LpLiteral>(bodySize);
			for (LpLiteral lit : body) {
				newBody.add(transform(lit, group));
			}
			if (assertion) {
				LpPredicate prevAssert = LpPredicate.getInstance(
						"assertN" + Integer.toString(assertLevel), 1);
				LpConstant ruleConst = LpConstant.getInstance(
						encoder.asString(rule));
				LpAtom assAtom = LpAtom.getInstance(prevAssert,
						Collections.singletonList((LpTerm)ruleConst));
				LpLiteral assGuard = assAtom.getPositiveLiteral();
				newBody.add(assGuard);
			}
			return new LpRule(newHead, newBody);
		}
		
		private LpLiteral transform(LpLiteral lit, int group) {
			if (lit == null)
				return null;
			
			LpPredicate pred = lit.getPredicate();
			encoder.reset();
			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(
					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 LpVariable) {
				return term;
			}
			if (term instanceof LpConstant) {
				return LpConstant.getInstance(encoder.asString(term));
			}
			if (term instanceof LpRule) {
				LpConstant ruleConst = LpConstant.getInstance(encoder.asString(term));
				decoder.put(ruleConst, (LpRule)term);
				return ruleConst;
			}
			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);
		}
	}
}