import java.util.*;

public class FirstOrderLogic {
	/** A test example for FirstOrderLogic */
	public static void main(String[] args) {
		String ruleList = "a(X,Y)|-p(X,Y);a(X,Y)|-p(X,Z)|-a(Z,Y);p(a,b);p(b,c)";
		System.out.println("facts : "+ruleList);
		String newFacts = unitResolution(ruleList.split(";"));
		System.out.println("inference : "+newFacts);
	}	
	/** Example : negate("p(x)") => "-p(x)" */
	public static String negate(String pTerm) {
		if (pTerm.startsWith("-"))
			return pTerm.substring(1);
		else 
			return "-"+pTerm;
	}
	/**@param pRules Example : "a(X,Y)|-p(X,Y);a(X,Y)|-p(X,Z)|-a(Z,Y);p(a,b);p(b,c)".split(";")
	  *@return Example : "a(a,b);a(b,c);a(a,c);" */
	public static String unitResolution(String[] pRules) {
		Vector rules = new Vector(Arrays.asList(pRules));
		for (int ri=0; ri<rules.size(); ri++) {
			String rule1 = (String) rules.get(ri);	 
			if (rule1.indexOf("|")>0) continue; 	 									// it's not a unit rule
			String negTerm1 = negate(rule1);		 									// negate the unit rule
			String negTag   = STR.head(negTerm1, "(");
			for (int rj=0; rj<rules.size(); rj++) {
				String rule2 = (String) rules.get(rj); 									// ex : unify e(a) with b(a),-d(a),-e(a) => b(a),-d(a)
				String[] terms2 = rule2.split("\\|");									// terms2 = {-e(X)}
				for (int ti=0; ti<terms2.length; ti++) {
					String tag = STR.head(terms2[ti], "(");
					if (!tag.equals(negTag)) continue;
					String unify = unify(negTerm1, terms2[ti]);							// unify e(a), -e(X)
					if (unify == null) continue;
					String bindRule  = STR.expand(rule2, unify);   						// b(X),-d(X),-e(X) => b(a),-d(a),-e(a)
					String unifyRule = STR.replace("|"+bindRule+"|", "|"+negTerm1+"|", "|"); // ,b(a),-d(a),-e(a), => ,b(a),-d(a)
					unifyRule = STR.trim(unifyRule, '|'); 								// ,b(a),-d(a), => b(a),-d(a)
					if (rules.indexOf(unifyRule) < 0) {
						rules.add(unifyRule);
						System.out.println(rule1+"  "+rule2+"\r\n ["+unify+"] => "+unifyRule);
					}
				}
			}
		}
		StringBuffer facts = new StringBuffer();
		for (int ri=pRules.length; ri<rules.size(); ri++) {
			String rule = (String) rules.get(ri);
			if (rule.indexOf("|") < 0)
				facts.append(rule+";");
		}
		return facts.toString();
	}
	
	/** add rule into rules */
	public static void addRule(String rule, Vector rules) {
	}
	
	/** Example : type("X") => "var";  type("a") => "value"; */
	public static String type(String pToken) {
		if (Character.isUpperCase(pToken.charAt(0))) return "var"; else return "value";
	}
	
	/** Example : unify("p(X,Y)", "p(a,b)") => "X=a|Y=b" */
	public static String unify(String term1, String term2) {
		StringBuffer rzUnify = new StringBuffer();
		String body1 = STR.innerText(term1, "(", ")");
		String body2 = STR.innerText(term2, "(", ")");
		String[] params1 = body1.split(",");
		String[] params2 = body2.split(",");
		if (params1.length != params2.length) return null;
		for (int i=0; i<params1.length; i++) {
			String type1 = type(params1[i]);
			String type2 = type(params2[i]);
			if (type2.equals("var") && type1.equals("value"))	// ex : parent(john,johnson)/parent(X, johnson) => X/john
				rzUnify.append("|"+params2[i]+"="+params1[i]);
			if (type1.equals("value")&&type2.equals("value"))	// ex : parent(X,mary)/parent(X,bob) => fail
				if (!params1[i].equals(params2[i]))
					return null;
		}
		if (rzUnify.length() == 0) return null;
		return rzUnify.substring(1);
	}	
}