unify

unify.js

var Unifier = (function(){
  
  function Unifier(){
    this.bindTable = {};
  }

  /*******************************************************************************
   * Unify two terms.
   *
   * Examples:
   *
   *   a         = a               → a
   *   (a b)     = (a b)           → (a b)
   *   (a z)     = (a a)           → (a a)
   *   (z Z)     = (a a)           → (Z Z)
   *   (A B C z) = (a b c (a b c)) → (A B C (A B C))
   *   (Z Y)     = (Z Y)           → (Z Y)
   *   (Z Y a X) = (Z Y a a)       → (Z Y X X)
   *
   * Seems to work. OK for first attempt but doesn't infinite loop…
   */
  Unifier.prototype.unify = function(a,b){
    var unifier = this;
    if(a.isArray() && b.isArray()){
      if(a.length == b.length){
        return a.zipWith(b,function(x,y){
          return unifier.unify(x,y);
        });
      } else {
        return new UnificationException(UnificationException.LengthMismatch,
                                        {a:a,b:b});
      }
    } else if(!a.isArray() && !b.isArray()) {
      var aref = unifier.lookup(a);
      var bref = unifier.lookup(b);
      if(aref || bref){
        if(aref && bref){
          if(aref !== bref) {
            throw new UnificationException(UnificationException.RefMismatch,
                                           {a:a,b:b});
          }
          return aref;
        } else {
          var ref = aref || bref;
          var term = aref? b : a;
          if(term.isConstant() && ref.isConstant() &&
             term.constant != ref.constant){
            throw new UnificationException(UnificationException.BindingMismatch,
                                           {a:a,b:b,ref:ref});
          }
          unifier.bind(aref? b : a,ref);
          return ref;
        }
      } else {
        var ref = new Unifier.Ref();
        unifier.bind(a,ref);
        unifier.bind(b,ref);
        return ref;
      }
    } else if(a.isArray() || b.isArray()) {
      var array = a.isArray()? a : b;
      var term = a.isArray()? b : a;
      if(term.isConstant()) {
        throw new UnificationException(UnificationException.TypeMismatch,
                                       {a:a,b:b});
      } else {
        var result = unifier.unify(array,array);
        var ref = new Unifier.Ref();
        unifier.bind(new Constant(result),ref);
        unifier.bind(term,ref);
        return ref;
      }
    } else {
      throw new UnificationException(UnificationException.TypeMismatch,
                                     {a:a,b:b});
    }
  };

  /*****************************************************************************
   * Lookup a term in the term table.
   */
  Unifier.prototype.lookup = function(term){
    return this.bindTable[term.term];
  };

  /*****************************************************************************
   * Bind a term to a reference in the term table.
   */
  Unifier.prototype.bind = function(term,ref){
    this.bindTable[term.term] = ref;
    if(term.isConstant()){
      ref.constant = term.term;
      delete ref.free;
    }
    else if(!ref.constant && !ref.free){ ref.free = term.term;}
  };

  Unifier.prototype.isBound = function(term){
    return !!this.bindTable[term];
  };

  /*****************************************************************************
   * A ref that variables refer to, that may contain constants.
   */
  var Ref = Unifier.Ref = function(a){
  };

  /*****************************************************************************
   * Is this a constant?
   */
  Ref.prototype.isConstant = function(){
    return !!this.constant;
  };

  /*****************************************************************************
   * Render the current contents of the ref.
   */
  Ref.prototype.toString = function(){
    return this.constant || this.free;
  };

  /*****************************************************************************
   * A unification exception.
   */
  var UnificationException = Unifier.UnificationException = function(reason,info){
    this.info = info;
    this.reason = reason;
  };

  /*****************************************************************************
   * Exception enum.
   */
  UnificationException.LengthMismatch = 0;
  UnificationException.Unknown        = 1;
  UnificationException.TypeMismatch   = 2;
  UnificationException.RefMismatch    = 3;
  UnificationException.RefMismatch    = 4;

  /*****************************************************************************
   * Printing for use to a console at the moment. Includes some simple
   * formatting.
   */
  UnificationException.prototype.toString = function(){
    return [
      "Couldn't unify ",
      this.info.a.toString(),
      " with ",
      this.info.b.toString(),
      " reason: " +
        UnificationException.showReason(this.reason,this.info)
    ].join("\n");
  };

  /*****************************************************************************
   * Pretty print a unification problem.
   */
  UnificationException.showReason = function(reason,info){
    switch(reason){
    case UnificationException.LengthMismatch: return "Length mismatch.";
    case UnificationException.RefMismatch:
      return "Ref mismatch.";
    case UnificationException.BindingMismatch:
      return "Binding mismatch. Already bound to: " + info.ref;
    case UnificationException.Unknown:
      return "General mismatch (unhandled unification case).";
    case UnificationException.TypeMismatch: return "Term type mismatch.";
    default: return "Unknown unification exception.";
    }
  };

  /*****************************************************************************
   * A term for unification.
   */
  var Term = Unifier.Term = function(term,typ){
    this.term = term;
    this.typ = typ;
  };

  /*****************************************************************************
   * Is this a free variable?
   */
  Term.prototype.isFree = function(){
    return this.typ == 'free';
  };

  /*****************************************************************************
   * Is this a constant?
   */
  Term.prototype.isConstant = function(){
    return this.typ == 'constant';
  };

  /*****************************************************************************
   * Show this term.
   */
  Term.prototype.toString = function(){
    return this.term;
  };

  /*****************************************************************************
   * Create a free variable term.
   */
  var Free = Unifier.Free = function(term){
    return new Unifier.Term(term,'free');
  };

  /*****************************************************************************
   * Create a constant term.
   */
  var Constant = Unifier.Constant = function(term){
    return new Unifier.Term(term,'constant');
  };

  return Unifier;
})();

////////////////////////////////////////////////////////////////////////////////
// Fundamental functions to make JavaScript not suck as hard.

/*******************************************************************************
 * Is an object an array? The answer is no.
 */
Object.prototype.isArray = function(){
  return false;
};

/*******************************************************************************
 * Is an array an array? The answer is “oui, monsieur!”
 */
Array.prototype.isArray = function(){
  return true;
};

/*******************************************************************************
 * Fold-right over an array.
 */
Array.prototype.foldr = function(cons,accum){
  var len = this.length;
  for(var i = 0; i < len; i++){
    accum = cons(this[i],accum);
  }
  return accum;
};

/*******************************************************************************
 * Zip two lists together.
 */
Array.prototype.zip = function(xs){
  var len = Math.max(xs.length,this.length);
  var accum = [];
  for(var i = 0; i < len; i++){
    accum.push([this[i],xs[i]]);
  }
  return accum;
};

/*******************************************************************************
 * Zip two lists with a cons function.
 */
Array.prototype.zipWith = function(xs,cons){
  var len = Math.max(xs.length,this.length);
  var accum = [];
  for(var i = 0; i < len; i++){
    accum.push(cons(this[i],xs[i]));
  }
  return accum;
};

var F = Unifier.Free;
var C = Unifier.Constant;

console.log((new Unifier).unify(F('a'),F('a')));
console.log((new Unifier).unify(F('a'),F('z')));
console.log((new Unifier).unify([F('a'),F('b')],[F('a'),F('b')]));
console.log((new Unifier).unify([F('a'),F('z')],[F('a'),F('a')]));
console.log(
  JSON.stringify(
    (new Unifier).unify([C('A'),C('B'),C('C'),F('z')],
                        [F('a'),F('b'),F('c'),[F('a'),F('b'),F('c')]])));

console.log((new Unifier).unify([C('Z'),C('Y')],[C('Z'),C('Y')]));
console.log((new Unifier).unify([C('Z'),C('Y'),F('a'),C('X')],
                                [C('Z'),C('Y'),F('a'),F('a')]));

// should infinite loop but doesn't continue resolving
// x = (x)
console.log(
  JSON.stringify(
    (new Unifier).unify([F('x')],
                        [[F('x')]])));

// this one should fail
// console.log((new Unifier).unify([F('z'),C('Z')],[C('H'),F('z')]));