package ws.prova;

import ws.prova.reference.FactImpl;
import ws.prova.reference.IProvaKnowledgeBase;
import ws.prova.reference.RBSLARobinsonsUnificationAlgorithm;
import ws.prova.util.DefaultLogicFactorySupport;
import org.mandarax.kernel.*;
import org.mandarax.reference.TmpClause;
import org.mandarax.reference.Resolution;
import org.mandarax.util.ClauseIterator;

import edu.emory.mathcs.backport.java.util.concurrent.ConcurrentHashMap;
import edu.emory.mathcs.backport.java.util.concurrent.ConcurrentMap;

import java.util.Collection;
import java.util.List;
import java.util.ArrayList;
import java.util.Iterator;
import java.util.ListIterator;

public class Updater {

	reagent reagent;

	private IProvaKnowledgeBase kb;

	private ConcurrentMap join_record = new ConcurrentHashMap(); 
	
	final static SimplePredicate state = HelperPredicates.state();
	final static SimplePredicate derive = HelperPredicates.derive();
	final UnificationAlgorithm unificationAlgorithm = new
			RBSLARobinsonsUnificationAlgorithm();

	public Updater(reagent reagent, IProvaKnowledgeBase kb) {
		this.reagent = reagent;
		this.kb = kb;
	}

	/**
     * Dynamically assert a new fact.
	 * Both meta/spec state predicates and regular derive predicates are supported.
	 *
	 * @param r Parameters including only one: ComplexTerm to be asserted
	 * @param reagent
	 * @return Always <code>true</code>
	 */
	boolean prova_assert(Object[] r, reagent reagent) {
		 ComplexTerm ct = (ComplexTerm) r[0];
		 String key = (String) ((ConstantTerm) ct.getTerms()[1]).getObject();
		 if (key.equals("meta") || key.equals("spec")) {
			  kb.add(DefaultLogicFactorySupport.fact(reagent.state, ct));
		 } else {
			  kb.add(DefaultLogicFactorySupport.fact(kb.poly(key, reagent.derive), key, ct));
		 }
		 return true;
	}

	/**
	 * Dynamically assert a new fact before all other facts.
	 * Both meta/spec state predicates and regular derive predicates are supported.
	 *
	 * @param r Parameters including only one: ComplexTerm to be asserted
	 * @param reagent
	 * @return Always <code>true</code>
	 */
	boolean prova_asserta(Object[] r, reagent reagent) {
		ComplexTerm ct = (ComplexTerm) r[0];
		String key = (String) ((ConstantTerm) ct.getTerms()[1]).getObject();
		if (key.equals("meta") || key.equals("spec")) {
			kb.add(DefaultLogicFactorySupport.fact(reagent.state, ct));
			kb.moveToTop(DefaultLogicFactorySupport.fact(reagent.state, ct));
		} else {
			kb.add(DefaultLogicFactorySupport.fact(kb.poly(key, reagent.derive), key, ct));
			kb.moveToTop(DefaultLogicFactorySupport.fact(kb.poly(key, reagent.derive), key, ct));
		}
		return true;
	}

	/**
	 * Dynamically insert a new fact.
	 * If a fact or a rule with header subsumed by the supplied fact exists in the KB,
	 * the method does nothing and returns <code>true</code>.
	 * Both meta/spec state predicates and regular derive predicates are supported.
	 *
	 * @param r Parameters including only one: ComplexTerm to be asserted
	 * @param reagent
	 * @return Always <code>true</code>
	 */
	synchronized boolean prova_update_fact(Object[] r, reagent reagent) throws ClauseSetException {
		if (r.length == 1) {
			retractall(r[0]);
			prova_assert(r, reagent);
			return true;
		} else if (r.length == 2) {
			// The first parameter is supposed to be a fact to be removed
			retractall(r[0]);
			prova_assert(new Object[]{r[1]}, reagent);
		}
		return true;
	}

	/**
	 * Retract one fact or a rule with a header that is subsumed by the pattern of the supplied fact.
	 * This method does not remove any rules.
	 *
	 * @param f Fact a fact holding a pattern of a fact to be removed
	 */
	protected synchronized boolean remove_fact(Fact f) throws ClauseSetException {
//		System.out.println("Pattern to retract: "+f);
		List lit = new ArrayList(1);
		lit.add(f);
		TmpClause nextClause = new TmpClause();
		nextClause.negativeLiterals = lit;
		nextClause.positiveLiterals = new ArrayList();
		ClauseIterator e = kb.clauses(nextClause, null);
		while (e.hasNext()) {
			Object o = e.next();
			if (o instanceof Fact) {
				Fact cs = (Fact) o;
				if (Resolution.subsumes(f, cs, unificationAlgorithm)) {
					kb.remove(cs);
					return true;
				}
			} else if (o instanceof Rule) {
				Rule r = (Rule) o;
				if (Resolution.subsumes(f, r.getHead(), unificationAlgorithm)) {
					kb.remove(r);
					return true;
				}
			}
		}
		return false;
	}

	/**
	 * Dynamically retract one fact or rule with header subsumed by the specified pattern.
	 * Both meta/spec state predicates and regular derive predicates are supported.
	 * If at least one fact is not found, the method returns Boolean.FALSE.
	 *
	 * @param r Object[] Parameters including only one: ComplexTerm to be retracted
	 * @return true if a fact was retracted
	 */
	boolean retract(Object[] r) throws ClauseSetException {
		ComplexTerm ct = (ComplexTerm) r[0];
		String key = (String) ((ConstantTerm) ct.getTerms()[1]).getObject();
		boolean removed = false;
		if (key.equals("meta") || key.equals("spec")) {
			removed = remove_fact(DefaultLogicFactorySupport.fact(state, ct));
		} else {
			removed = remove_fact(DefaultLogicFactorySupport.fact(kb.poly(key, derive), key, ct));
		}
		return removed;
	}

	/**
	 * Dynamically retract all facts or rules with headers subsumed by the specified pattern.
	 * Both meta/spec state predicates and regular derive predicates are supported.
	 *
	 * @param r The pattern as either
	 *          <br> a <code>ComplexTerm</code> for the facts to be retracted
	 *          <br> or a <code>String</code> representing the rulebase source for which all facts and rules are to be retracted
	 */
	void retractall(Object r) throws ClauseSetException {
		if (r instanceof String) {
			removeall_facts((String) r);
			return;
		}
		ComplexTerm ct = (ComplexTerm) r;
		String key = (String) ((ConstantTerm) ct.getTerms()[1]).getObject();
		if (key.equals("meta") || key.equals("spec")) {
			removeall_facts(DefaultLogicFactorySupport.fact(state, ct));
		} else {
			removeall_facts(DefaultLogicFactorySupport.fact(kb.poly(key, derive), key, ct));
		}
	}

	/**
	 * Retract all facts or rules subsumed by a fact serving as a pattern.
	 *
	 * @param f Fact a fact holding a pattern of facts to be removed
	 */
	public synchronized void removeall_facts(Fact f) throws ClauseSetException {
//		System.out.println("Pattern to retract: "+f);
		List lit = new ArrayList(1);
		lit.add(f);
		TmpClause nextClause = new TmpClause();
		nextClause.negativeLiterals = lit;
		nextClause.positiveLiterals = new ArrayList();
		ClauseIterator e = kb.clauses(nextClause, null);
		while (e.hasNext()) {
			Object o = e.next();
			if (o instanceof Fact) {
				Fact cs = (Fact) o;
				if (Resolution.subsumes(f, cs, unificationAlgorithm)) {
					kb.remove(cs);
				}
			} else if (o instanceof Rule) {
				Rule r = (Rule) o;
				if (Resolution.subsumes(f, r.getHead(), unificationAlgorithm)) {
					kb.remove(r);
				}
			}
		}
	}

	/**
	 * Retract all facts or rules having a src representing the source of the consulted rulebase.
	 *
	 * @param src The source of the consulted rulebase
	 */
	public synchronized void removeall_facts(String src) {
		List list = kb.getClauseSets();
		for (Iterator e = list.iterator(); e.hasNext();) {
			Object o = e.next();
			if (o instanceof Fact) {
				Fact f = (Fact) o;
				if (f.getProperty("src") != null && f.getProperty("src").equals(src)) {
					kb.remove(f);
				}
			} else if (o instanceof Rule) {
				Rule r = (Rule) o;
				if (r.getProperty("src") != null && r.getProperty("src").equals(src)) {
					kb.remove(r);
				}
			}
		}
	}

	/**
	 * Dynamically insert a new fact.
	 * If a fact or a rule with header subsumed by the supplied fact exists in the KB,
	 * the method does nothing and returns <code>true</code>.
	 * Both meta/spec state predicates and regular derive predicates are supported.
	 *
	 * @param r Parameters including only one: ComplexTerm to be asserted
	 * @return Always <code>true</code>
	 */
	synchronized boolean prova_insert(Object[] r) throws ClauseSetException {
		ComplexTerm ct = (ComplexTerm) r[0];
		String key = (String) ((ConstantTerm) ct.getTerms()[1]).getObject();
		Fact f = null;
		if (key.equals("meta") || key.equals("spec")) {
			f = DefaultLogicFactorySupport.fact(state, ct);
		} else {
			f = DefaultLogicFactorySupport.fact(kb.poly(key, derive), key, ct);
		}
		List lit = new ArrayList(1);
		lit.add(f);
		TmpClause nextClause = new TmpClause();
		nextClause.negativeLiterals = lit;
		nextClause.positiveLiterals = new ArrayList();
		ClauseIterator e = kb.clauses(nextClause, null);
		while (e.hasNext()) {
			Object o = e.next();
			if (o instanceof Fact) {
				Fact cs = (Fact) o;
				if (Resolution.subsumes(f, cs, unificationAlgorithm)) {
					return true;
				}
			} else if (o instanceof Rule) {
				Rule rule = (Rule) o;
				if (Resolution.subsumes(f, rule.getHead(), unificationAlgorithm)) {
					return true;
				}
			}
		}
		kb.add(f);
		return true;
	}

	public synchronized boolean increment_value(Object[] r) throws ClauseSetException {
		ComplexTerm ct = (ComplexTerm) r[0];
		String key = (String) ((ConstantTerm) ct.getTerms()[1]).getObject();
		ComplexTerm nt = DefaultLogicFactorySupport.cplx(reagent.flist, RListUtils.emptyRList, DefaultLogicFactorySupport.variable("_",Object.class));
		ComplexTerm ct0 = (ComplexTerm) ((ComplexTerm) ct.getTerms()[0]).getTerms()[0];
		ct0.setTerm(nt,0);
		Fact f = null;
		if (key.equals("meta") || key.equals("spec")) {
			f = DefaultLogicFactorySupport.fact(state, ct);
		} else {
			f = DefaultLogicFactorySupport.fact(kb.poly(key, derive), key, ct);
		}
		List lit = new ArrayList(1);
		lit.add(f);
		TmpClause nextClause = new TmpClause();
		nextClause.negativeLiterals = lit;
		nextClause.positiveLiterals = new ArrayList();
		ClauseIterator e = kb.clauses(nextClause, null);
		boolean term = e.hasNext();
		if( !term ) {
			nt.setTerm(DefaultLogicFactorySupport.cons(new Integer(1), Integer.class), 1);
			kb.add(f);
			return true;
		}
		Object o = e.next();
		if (o instanceof FactImpl) {
			FactImpl cs = (FactImpl) o;
			if (Resolution.subsumes(f, cs, unificationAlgorithm)) {
				ComplexTerm ct1 = (ComplexTerm) cs.getTerms()[1];
				ComplexTerm ct2 = (ComplexTerm) ((ComplexTerm) ((ComplexTerm) ct1.getTerms()[0]).getTerms()[0]).getTerms()[0];
				ConstantTerm value = (ConstantTerm) ct2.getTerms()[1];
				Number oldValue = (Number) value.getObject();
				if( oldValue instanceof Integer )
					value.setObject( new Integer(oldValue.intValue()+1) );
				else if( oldValue instanceof Long )
					value.setObject( new Long(oldValue.longValue()+1) );
				else if( oldValue instanceof Float )
					value.setObject( new Float(oldValue.floatValue()+1) );
				else if( oldValue instanceof Double )
					value.setObject( new Double(oldValue.doubleValue()+1) );
				return true;
			}
		} else if (o instanceof Rule) {
			Rule rule = (Rule) o;
			if (Resolution.subsumes(f, rule.getHead(), unificationAlgorithm)) {
				return true;
			}
		}
		return false;
	}

	public boolean init_join(Object[] r) {
		List waiting = new ArrayList();
		List data = new ArrayList();
		RListUtils.rlist2List( (ComplexTerm) r[2], data, 0);
		waiting.addAll(data);
		List complete = new ArrayList();
		// TODO: fail if the entry is already there for the given key
		// Key is XID+JoinID
		join_record.put(((String) r[0])+r[1], new List[]{waiting,complete});
		return true;
	}

	public synchronized Boolean join_test(Object[] r, final List bindings) {
		// Key is XID+JoinID
		List[] waitingAndComplete = (List[]) join_record.get(((String) r[1])+r[2]);
		for( ListIterator iter = waitingAndComplete[0].listIterator(); iter.hasNext(); ) {
			Term t = (Term) iter.next();
			Unification u = unificationAlgorithm.unify2( new Term[]{t} , new Term[]{(Term) r[3]}, false);
			if( u==Unification.noUnificationPossible )
				continue;
			iter.remove();
			waitingAndComplete[1].add(r[3]);
			if( waitingAndComplete[0].isEmpty() ) {
				join_record.remove(((String) r[1])+r[2]);
				Object[] retobj = new Object[5];
				retobj[0] = r[0];
				retobj[1] = r[1];
				retobj[2] = r[2];
				retobj[3] = r[3];
				retobj[4] = waitingAndComplete[1];
				bindings.add(retobj);
				return Boolean.TRUE;
			}
		}
		return Boolean.FALSE;
	}

}
