User:Kevin Reid/unification.emaker

From Erights

The idea is to implement unification variables in E: a single object which acts as promise and resolver, and a procedure which makes two values equal by resolving variables if possible. I never finished this program.

def makeProxy := <elib:ref.makeProxy>
def [varResolverSealer, varResolverUnsealer] := <elib:sealing.makeBrand>("unifiable")
def makeVariable() {
  def resolutionBox
  def buffer
  def ref
  def resolver {
    to resolve(target) {
      bind resolutionBox := &target
      bind buffer := target
    }
  }
  def handler {
    to handleSend(v, a) { return E.send(buffer, v, a) }
    to handleSendOnly(v, a) { return E.sendOnly(buffer, v, a) }
    to handleOptSealedDispatch(brand) {
      if (brand == varResolverSealer.getBrand()) {
        return varResolverSealer.seal([ref, resolver])
      }
    }
  }
  bind ref := makeProxy(handler, resolutionBox, false)
  return ref
}

def makeSame(a, b) {

}

def _unify(a, b, unifications, sofar) {
  def ka := __equalizer.makeTraversalKey(a)
  def kb := __equalizer.makeTraversalKey(b)
  def k := [ka, kb]
  if (ka == kb || sofar.maps(k)) {
    # ok
  } else if (varResolverUnsealer.amplify(a) =~ [[==a, resolver]]) {
    unifications.pushfn { resolver.resolve(b) }]
  } else if (varResolverUnsealer.amplify(b) =~ [[==b, resolver]]) {
    [fn { resolver.resolve(a) }]
  } else if (a == b) {
    []
  } else if (Ref.isSelfless(a) && a.__optUncall() =~ [ar, av, aa]) {
    accum [] ...
  } else {
    return Ref.broken(`can't make $a and $b the same`)
  }
}