package aima.logic;
import aima.util.Expression;

/**
 * The Unify class provides methods for the unification of 
 * expressions and the substitution of values for variables in expressions.
 * This code is adapted from LISP code which contained the following comment:
 *
 * <pre>
 *   Unification and Substitutions (aka Binding Lists)
 *
 *   This code is borrowed from "Paradigms of AI Programming: Case Studies
 *   in Common Lisp", by Peter Norvig, published by Morgan Kaufmann, 1992.
 *   The complete code from that book is available for ftp at mkp.com in
 *   the directory "pub/Norvig".  Note that it uses the term "bindings"
 *   rather than "substitution" or "theta".  The meaning is the same.
 * </pre>
 *
 * @author Michael S. Braverman
 * @author Peter Norvig
 * @see Variable
 * @see Bindings
 * @see Expression
 */

// In the current documentation, we show the original LISP code corresponding
// to each JAVA method so that they may be more easily compared

public class Unify {
  /**
   * Parses the input <code>String</code> into an expression which may be 
   * processed by the various unify methods.  In particular, tokens in the 
   * input that are prefixed appropriately are converted into
   * <code>Variable</code> objects.
   *
   * @return An expression suitable as input to the various Unify methods
   * @param exprStr An expression to parse.
   * @exception Exception May be thrown if the expression <code>String</code>
   * does not parse properly.
   * @see #unify
   * @see #unifier
   * @see Variable#getPrefix
   */
  static public Object parse(String exprStr) throws Exception {
    return parseVariables(Expression.parse(exprStr));
  }

  /**
   * Processes a (compound or atomic) expression to create a new expression
   * in which all atoms, whose print names have an appropriate prefix 
   * character, are replaced with <code>Variable</code> objects.
   *
   * @return An expression suitable as input to the various Unify methods
   * @param obj An expression to process.
   * @see #unify
   * @see #unifier
   * @see Expression
   * @see Variable#getPrefix
   */
  static public Object parseVariables(Object obj) {
    if (Expression.isAtomic(obj)) {
      if ((obj instanceof String) &&
	  (((String)obj).charAt(0) == Variable.getPrefix())) {
	return new Variable(((String)obj).substring(1));
      } else {
	return obj;
      }
    } else {
      return Expression.reuse(parseVariables(Expression.car(obj)),
			      parseVariables(Expression.cdr(obj)),
			      obj);
    }
  }

  /**
   * Returns something that unifies with both x and y (or fail).
   *
   * @return An expression that unifies with both x and y, or the
   * <code>Bindings</code> object that represents failure.
   * @param x An expression (atomic or compound) to unify.
   * @param y An expression (atomic or compound) to unify.
   * @see Bindings#getFailure
   * @see Expression
   * @see #unify
   */

  /* Original LISP:
   * (defun unifier (x y)
   *   "Return something that unifies with both x and y (or fail)."
   *   (subst-bindings (unify x y) x))
   */
  static public Object unifier(Object x, Object y) {
    // note: I reversed the order of the parameters to substBindings
    return substBindings(x,unify(x,y));
  }


  /**
   * Determines if the given expressions match and
   * returns a <code>Bindings</code> object that would make them equal.
   *
   * <p>
   * By default, the <code>Bindings</code> object returned is
   * in terms of a <code>ListBindings</code> implementation.
   * If you want to explicitly specify the <code>Bindings</code>
   * implementation to use, use the alternative version of <code>unify</code>
   * where you should pass in an empty <code>Bindings</code> object
   * of the desired implementation type.  For instance:
   * <pre>
   *     Unify.unify(x,y,HashBindings.getEmpty());
   * </pre>
   * would return the results of the unification in a 
   * <code>HashBindings</code> <code>Bindings</code> implementation.
   *
   * @return A <code>Bindings</code> object that would make the
   * input parameters match, or the <code>Bindings</code> object that
   * represents failure if they do not match.
   * @param x An expression (atomic or compound) to unify.
   * @param y An expression (atomic or compound) to unify.
   * @see Bindings
   * @see ListBindings
   * @see HashBindings
   * @see Variable
   * @see Expression
   */
  /*
   * (defun unify (x y &optional (bindings +no-bindings+))
   *   "See if x and y match with given bindings.  If they do,
   *    return a binding list that would make them equal [p 303]."
   *   (cond ((eq bindings +fail+) +fail+)
   *    ((eql x y) bindings)
   *    ((variable? x) (unify-var x y bindings))
   *    ((variable? y) (unify-var y x bindings))
   *    ((and (consp x) (consp y))
   *    (unify (rest x) (rest y) 
   *           (unify (first x) (first y) bindings)))
   *    (t +fail+)))
   */
  static public Bindings unify(Object x, Object y) {
    return unify(x,y,ListBindings.getEmpty());
  }

  /** 
   * Determines if the given expressions match subject to the variable
   * bindings given in the initial <code>Bindings</code> object and returns a
   * <code>Bindings</code> object that would make them equal.
   *
   * @return A <code>Bindings</code> object that would make the
   * input parameters match, or the <code>Bindings</code> object that
   * represents failure if they do not match.
   * @param x An expression (atomic or compound) to unify.
   * @param y An expression (atomic or compound) to unify.
   * @param theBindings An initial set of bindings to begin with.
   * @see Bindings
   * @see Variable
   * @see Expression 
   */
  static public Bindings unify(Object x, Object y,
			       Bindings theBindings) {
    if (theBindings.isFailure()) {
      return theBindings;
    } else if (Expression.eql(x,y)) {
      return theBindings;
    } else if (x instanceof Variable) {
      return unifyVar((Variable) x,y,theBindings);
    } else if (y instanceof Variable) {
      return unifyVar((Variable) y,x,theBindings);
    } else if (Expression.isTrueCompound(x) &&
	        Expression.isTrueCompound(y)) {
      return unify(Expression.rest(x),Expression.rest(y),
		  unify(Expression.first(x),Expression.first(y),theBindings));
    } else {
      return theBindings.getFailure();
    }
  }



  /** 
   * Determines if the given <code>Variable</code> occurs anywhere inside
   * the given expression, subject to the bindings contained in the given 
   * <code>Bindings</code> object.
   *
   * @return true iff <code>var</code> is contained is <code>x</code> subject
   * to <code>theBindings</code>
   * @param var <code>Variable</code> for which to search.
   * @param x An expression (atomic or compound) to search.
   * @param theBindings An set of bindings on the variables in <code>x</code>
   * @see Bindings
   * @see Variable
   * @see Expression 
   */
  /*
    (defun occurs-in? (var x bindings)
     "Does var occur anywhere inside x?"
     (cond ((eq var x) t)
        ((and (variable? x) (get-binding x bindings))
         (occurs-in? var (lookup x bindings) bindings))
        ((consp x) (or (occurs-in? var (first x) bindings)
                       (occurs-in? var (rest x) bindings)))
        (t nil)))
  */
  static public boolean occursIn(Variable var, Object x, 
				 Bindings theBindings) {
    if (var == x) {
      return true;
    } else if ((x instanceof Variable) &&
	         theBindings.isBound((Variable) x)) {
      return occursIn(var, theBindings.getBinding((Variable) x), 
			 theBindings);
    } else if (Expression.isTrueCompound(x)) {
      return (occursIn(var, Expression.first(x), theBindings) ||
	       occursIn(var, Expression.rest(x),  theBindings));
    } else {
      return false;
    }
  }
  
  /** 
   * Creates an isomorphic expression to the given expression in which all
   * the variables have been replaced with new ones.  If a variable appears
   * more than once in the expression, then it is given the same replacement
   * at each position in which it occurs.
   *
   * @return An isomorphic expression with new <code>Variables</code>.
   * @param x An expression (atomic or compound) to process.
   * @see Variable
   * @see Expression 
   */
  /*
   * (defun rename-variables (x)
   *   "Replace all variables in x with new ones."
   *   (sublis (mapcar #'(lambda (var) (make-binding var (new-variable var)))
   *    (variables-in x))
   *  x))
   */
  static public Object renameVariables(Object x) {
    // I didn't want to reimplement sublis right now, so instead I build
    // a map from existing variables to new variables, and then just use
    // substBindings to rename the variables in the Object passed.
    Bindings b = buildNewVarMap(x, HashBindings.getEmpty());
    return substBindings(x, b);
  }

  /** 
   * Creates a new expression in which the values of the variables indicated
   * in the given <code>Bindings</code> object are substituted into the given
   * (compound or atomic) expression.
   *
   * <p>
   * Note: The order of the parameters might be different than what you
   * may be used to seeing if you are familiar with the LISP version of this
   * function (but they are more in line with all the other methods in the
   * <code>Unify</code> class).
   *
   * @return An expression where the <code>Variable</code> values have been
   * substituted in place of the <code>Variable</code>s themselves.
   * @param x An expression (atomic or compound) to process.
   * @param theBindings The variable bindings.
   * @see Bindings
   * @see Variable
   * @see Expression 
   */
  /*
   * (defun subst-bindings (bindings x)
   *   "Substitute the value of variables in bindings into x,
   *    taking recursively bound variables into account."
   *    (cond ((eq bindings +fail+) +fail+)
   *          ((eq bindings +no-bindings+) x)
   *          ((and (variable? x) (get-binding x bindings))
   *           (subst-bindings bindings (lookup x bindings)))
   *          ((atom x) x)
   *          (t (reuse-cons (subst-bindings bindings (car x))
   *                         (subst-bindings bindings (cdr x))
   *                         x))))
   */
  // Note: swapped the order of the bindings and object to make more sense
  // (i.e., to people who have never heard of sublis):
  static public Object substBindings(Object x, Bindings theBindings) {
    if (theBindings.isFailure()) {
      return theBindings;
    } else if (theBindings.isEmpty()) {
      return x;
    } else if ((x instanceof Variable) && 
	        theBindings.isBound((Variable) x)) {
      return substBindings(theBindings.getBinding((Variable) x),
			   theBindings);
    } else if (Expression.isAtomic(x)) {
      return x;
    } else {
      return Expression.reuse(substBindings(Expression.first(x),theBindings),
      			      substBindings(Expression.rest(x),theBindings),
			      x);

    } 
  }

  /** 
   * Unifies the given <code>Variable</code> with the given expression,
   * using (and maybe extending) the given <code>Bindings</code> object.
   *
   * @return A <code>Bindings</code> object that would make the
   * variable match the expression, or the <code>Bindings</code> object that
   * represents failure if they do not match.
   * @param var A <code>Variable</code> to unify.
   * @param x An expression (atomic or compound) to unify.
   * @param theBindings An initial set of bindings to begin with.
   * @see Bindings
   * @see Variable
   * @see Expression 
   */
  /*
   * (defun unify-var (var x bindings)
   *   "Unify var with x, using (and maybe extending) bindings [p 303]."
   *   (cond ((get-binding var bindings)
   *          (unify (lookup var bindings) x bindings))
   *         ((and (variable? x) (get-binding x bindings))
   *          (unify var (lookup x bindings) bindings))
   *         ((occurs-in? var x bindings)
   *          +fail+)
   *         (t (extend-bindings var x bindings))))
   */
  static private Bindings unifyVar(Variable var,Object x,
				  Bindings theBindings) {
    if (theBindings.isBound(var)) {
      return unify(theBindings.getBinding(var), x, theBindings);
    } else if ((x instanceof Variable) &&
	       theBindings.isBound((Variable) x)) {
      return unify(var, theBindings.getBinding((Variable) x), theBindings);
    } else if (occursIn(var,x,theBindings)) {
      return theBindings.getFailure();
    } else {
      return theBindings.extendBindings(var,x);
    }
  }

  /** 
   * Searches the given (compound or atomic) expression to find all the
   * <code>Variable</code>s it contains and returns a <code>Bindings</code>
   * object mapping from each <code>Variable</code> in the expression to 
   * a new, previously non-existant, <code>Variable</code>.
   *
   * @return A <code>Bindings</code> map from old to new 
   * <code>Variable</code>s.
   * @param x An expression (atomic or compound) to process.
   * @param varMap A mapping from old to new <code>Variable</code>s to extend.
   * @see Bindings
   * @see Variable
   * @see Expression 
   */
  private static Bindings buildNewVarMap(Object x, Bindings varMap) {
    if (x instanceof Variable) {
      if (!varMap.isBound((Variable) x)) {
	return varMap.extendBindings((Variable) x, 
				     new Variable((Variable) x));
      } else {
	return varMap;
      }
    } else if (Expression.isTrueCompound(x)) {
      return buildNewVarMap(Expression.first(x),
			    buildNewVarMap(Expression.rest(x),
					   varMap));
    } else {
      return varMap;
    }
  }

  /**
   * Placeholder to keep Unify objects from being created.
   */
  private Unify() {
    // This keeps Unify objects from being created.
  }

  /**
   * Used in testing out the functionality of this class.
   * @param obj1 An expression to unify.
   * @param obj2 An expression to unify.
   */
  static private void testIt(Object obj1, Object obj2) {
    System.out.println("unify("+obj1+","+obj2+") ="+
		       unify(obj1,obj2));
    System.out.println("unifier("+obj1+","+obj2+") ="+
		       unifier(obj1,obj2));
    System.out.println("-----");
  }
  /**
   * Tests out the functionality of this class.
   * @param args Ignored.
   * @exception Exception Thrown in case of an internal parsing error.
   */
  static public void main(String [] args) throws Exception {
    Object x  = parse("(a b)");
    Object y  = parse("(a b)");
    Object v1 = parse("?x");
    Object v2 = parse("?x");
    Variable vy = new Variable("y");

    Object z1 = parse("(a . c)");
    Object z2 = new Expression("a",new Variable("x"));
    Object z3 = new Expression(vy,vy);
    Object z4 = renameVariables(z3);
    Object z5 = parse("(?x y z)");
    Object z6 = parse("(z y ?x)");
    Object z7 = parse("(?y ?y z)");
    Object z8 = parse("(?y ?y ?x)");
    testIt(v1,v2);
    testIt(x,y);
    testIt(x,z1);
    testIt(x,z2);
    testIt(x,z3);
    testIt(z3,z3);
    testIt(z3,z4);
    testIt(z4,z5);
    testIt(z5,z6);
    testIt(z6,z7);
    testIt(z7,z8);
  }
}