Kevin Reid at 14:21, 8 March 2011

2011-03-08T14:21:59Z

New page

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.

<pre><nowiki>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`)
}
}
</nowiki></pre>

User:Kevin Reid/unification.emaker - Revision history

Kevin Reid at 14:21, 8 March 2011