natas_hw
/
mps-coderules
mirror of https://github.com/JetBrains/mps-coderules
0
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Fix and simplify the unification algorithm. Drop support for cyclic terms. Correctly report cycles.

This commit is contained in:
Fedor Isakov 2017-02-25 18:36:56 +01:00
parent c687908e1e
commit 6cac64b6bd
2 changed files with 95 additions and 216 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

143
reactor/unification/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java
View File

@ -29,11 +29,13 @@ import static jetbrains.mps.unification.Unification.*;
* This is an implementation of the "near linear" algorithm for solving syntactic unification
* as described in the paper linked below and also in the textbook of the same author.<sup>1</sup> <sup>2</sup>
*
* No recursive terms are allowed as a solution, meaning the "occurrs check" for variables
* is performed on the input. However, cyclic terms are allowed as input and can be unified, producing
* solutions binding variables to cyclic terms. Variables can also be passed by reference without altering the
* No recursive terms are allowed as a solution, meaning the "occurs check" for variables
* is performed on the input. Variables can also be passed by reference without altering the
* intuitive behaviour of the algorithm.
*
* The "REF" terms are an extension of the term algebra used in [1]. For the purposes of this algorithm, the "REF"
* terms are treated as pre-bound variables.
*
* If successful, the returned {@link Substitution} contains
* the variable bindings.
* <p/>
@ -68,46 +70,29 @@ public class UnionFindTermGraphUnifier {
s = find(s);
t = find(t);
if (s == t) return true;
if (s == t) {
return true;
}
InnerTerm zs = s.mySchema;
InnerTerm zt = t.mySchema;
while (zs.myOrigin.is(REF)) {
s = union(s, getRef(zs));
zs = s.mySchema;
}
while (zt.myOrigin.is(REF)) {
t = union(t, getRef(zt));
zt = t.mySchema;
}
// a VAR always matches another node
if(zs.myOrigin.is(VAR) || zt.myOrigin.is(VAR)) {
union(s, t);
return true;
}
// dereference REF nodes
InnerTerm ds = deref(zs);
InnerTerm dt = deref(zt);
if (ds.myOrigin.is(VAR)) {
union(s, find(ds));
union(s, t);
return true;
}
else
{
zs = ds;
}
if (dt.myOrigin.is(VAR)) {
union(t, find(dt));
union(t, s);
return true;
}
else
{
zt = dt;
}
// use find 2nd time to account for dereferenced nodes
if (find(zs) == find(zt)) {
return true;
}
if (zs.myOrigin.is(FUN) && zt.myOrigin.is(FUN))
{
if (!eq(zs.myOrigin.symbol(), zt.myOrigin.symbol())) {
@ -116,7 +101,7 @@ public class UnionFindTermGraphUnifier {
return false; // symbol clash
}
// union REF nodes only to each other
// union REF nodes only if they are the same node
if (s.myOrigin.is(REF) == t.myOrigin.is(REF)) {
union(s, t);
}
@ -138,7 +123,14 @@ public class UnionFindTermGraphUnifier {
}
}
private void union(InnerTerm s, InnerTerm t) {
private InnerTerm union(InnerTerm s, InnerTerm t) {
s = find(s);
t = find(t);
if (s == t) {
return s;
}
int ssize = s.mySize;
int tsize = t.mySize;
@ -154,19 +146,21 @@ public class UnionFindTermGraphUnifier {
}
// union s and t classes by moving t under s
s.mySize = ssize + tsize;
prependVars(s, t.myVars);
t.myClass = s;
// copy the schema
InnerTerm zs = s.mySchema;
InnerTerm zt = t.mySchema;
if (zs.myOrigin.is(VAR) ||
(zs.myOrigin.is(REF) && !zt.myOrigin.is(VAR)))
{
if (zs.myOrigin.is(REF)) {
s.mySchema = zt;
} else if (zs.myOrigin.is(VAR) && !(zt.myOrigin.is(VAR))) {
s.mySchema = zt;
}
t.myClass = s;
return s;
}
private InnerTerm find(InnerTerm term) {
@ -176,7 +170,6 @@ public class UnionFindTermGraphUnifier {
}
// find representative and compress paths
List<InnerTerm> path = new ArrayList<InnerTerm>(4);
path.add(term.myClass);
for (InnerTerm t; (t = term.myClass) != repr; ) {
@ -191,12 +184,7 @@ public class UnionFindTermGraphUnifier {
}
private Substitution findSolution(InnerTerm s) {
mySolutionQueue.add(s);
Substitution solution = EMPTY_SUBSTITUTION;
while(!mySolutionQueue.isEmpty() && solution.isSuccessful()) {
solution = findSolution(mySolutionQueue.removeFirst(), solution);
}
return solution;
return findSolution(s, EMPTY_SUBSTITUTION);
}
private Substitution findSolution(InnerTerm s, Substitution substitution) {
@ -213,49 +201,38 @@ public class UnionFindTermGraphUnifier {
z.myVisited = true;
for (Term c : z.myOrigin.arguments()) {
substitution = findSolution(toInner(c), substitution);
if (!substitution.isSuccessful()) {
if (!(substitution = findSolution(toInner(c), substitution)).isSuccessful()) {
break;
}
}
z.myVisited = false;
}
else if(z.myOrigin.is(REF)) {
InnerTerm trg = deref(z);
if (!trg.myAcyclic) {
mySolutionQueue.add(trg);
}
}
if (!substitution.isSuccessful()) {
return substitution;
}
if (substitution.isSuccessful()) {
z.myAcyclic = true;
z.myAcyclic = true;
// avoid unnecessary instantiation
SuccessfulSubstitution success =
(substitution instanceof SuccessfulSubstitution) ?
(SuccessfulSubstitution) substitution : new SuccessfulSubstitution(substitution);
// avoid unnecessary instantiation
SuccessfulSubstitution success =
(substitution instanceof SuccessfulSubstitution) ?
(SuccessfulSubstitution) substitution : new SuccessfulSubstitution(substitution);
for (InnerTerm var : find(z).myVars) {
if (var != z) {
// Keep the order of variables within a binding
if (z.myOrigin.is(VAR) && z.myOrigin.compareTo(var.myOrigin) < 0) {
success.addBinding(fromInner(z), fromInner(var));
for (InnerTerm var : find(z).myVars) {
if (var != z) {
InnerTerm trg = deref(z);
// Keep the order of variables within a binding
if (trg.myOrigin.is(VAR) && trg.myOrigin.compareTo(var.myOrigin) < 0) {
success.addBinding(fromInner(trg), fromInner(var));
}
else {
success.addBinding(fromInner(var), fromInner(trg));
} else {
success.addBinding(fromInner(var), fromInner(z));
}
}
}
substitution = success;
}
return success;
return substitution;
}
private void prependVars(InnerTerm t, List<InnerTerm> vars) {
@ -266,12 +243,11 @@ public class UnionFindTermGraphUnifier {
t.myVars = newVars;
}
private InnerTerm deref(InnerTerm zs) {
InnerTerm tmp = zs;
while (tmp.myOrigin.is(REF)) {
tmp = toInner(tmp.myOrigin.get());
private InnerTerm getRef(InnerTerm zs) {
if (zs.myOrigin.is(REF)) {
return toInner(zs.myOrigin.get());
}
return tmp;
return zs;
}
private InnerTerm toInner(Term term) {
@ -298,13 +274,8 @@ public class UnionFindTermGraphUnifier {
}
private TermWrapper wrapper = TermWrapper.ID;
private Map<Object, InnerTerm> myTermCache = new IdentityHashMap<Object, InnerTerm>();
private FailureCause myFailureCause = UKNOWN;
private LinkedList<InnerTerm> mySolutionQueue = new LinkedList<InnerTerm>();
private Object[] myFailureDetails = null;
private static boolean eq(Object a, Object b) {

168
reactor/unification/tests/test/jetbrains/mps/unification/test/SolverTests.java
View File

@ -19,7 +19,9 @@ package jetbrains.mps.unification.test;
import jetbrains.mps.unification.Term;
import jetbrains.mps.unification.TermWrapper;
import org.jetbrains.annotations.NotNull;
import org.junit.Ignore;
import org.junit.Test;
import org.omg.CORBA.UNKNOWN;
import java.util.Collection;
import java.util.Collections;
@ -283,103 +285,8 @@ public class SolverTests {
);
}
@Test
public void testCyclic() throws Exception {
assertUnifiesWithBindings(
parse("@1 a{b ^1}"),
parse("@2 a{b a{b ^2}}")
);
assertUnifiesWithBindings(
parse("@1 a{b ^1}"),
parse(" a{b @3 a{b ^3}}")
);
assertUnifiesWithBindings(
parse("@1 a{b ^1}"),
parse("@2 a{b ^2}")
);
// the following tests are not very strict, but they suffice to convey a message
// that cyclic terms can be safely unified
assertUnifiesWithBindings(
parse("a{@1 b{c{^2}} @2 b{c{^1}}}"),
parse("a{ b{Y} b{Y} }"),
// TODO: the innermost "b" must actually contain a ref to the top level
// FIXME: AssertStructurallyEquivalent
bind(var("Y"), parse("@1 c{b{c{b }}}"))
);
assertUnifiesWithBindings(
parse("a{@1 b{c{^1}} @2 c{b{^2}}}"),
parse("a{ b{Y} Y }"),
// TODO: the innermost "b" must actually contain a ref to the top level
// FIXME: AssertStructurallyEquivalent
bind(var("Y"), parse("c{b }"))
);
assertUnifiesWithBindings(
parse("a{@1 b{c{@3 b{c{^3}}}} @2 c{b{^2}}}"),
parse("a{ b{Y} Y }"),
// TODO: the innermost "c" must actually contain a ref to the top level
// FIXME: AssertStructurallyEquivalent
bind(var("Y"), parse("c{b{c }}"))
);
assertUnifiesWithBindings(
parse("@1 a{c{d} b{e{^1 f}}}"),
parse(" a{c{X} b{Y}}"),
bind(var("X"), parse("d")),
// TODO: the innermost "b" must actually contain a ref to the top level
// FIXME: AssertStructurallyEquivalent
bind(var("Y"), parse("e{a{c{d} b } f}"))
);
assertUnifiesWithBindings(
parse("@1 a{c{d} b{e{@2 a{c{d} b{e{^2 f}}} f}}}"),
parse(" a{c{X} b{Y}}"),
bind(var("X"), parse("d")),
// TODO: the innermost "e" must actually contain a ref to the top level
// FIXME: AssertStructurallyEquivalent
bind(var("Y"), parse("e{a{c{d} b{e{ f}}} f}"))
);
}
@Test
public void testCyclicExt() throws Exception {
Term left = parse("@1 j{^1}");
Term right = term("j", term("j", ref(left)));
assertUnifiesWithBindings(
left,
right
);
assertUnifiesWithBindings(
parse("a{@1 b{c{^1}} b{c{Z}} @2 c{b{^2}}}"),
parse("a{ Z b{Y} Y }"),
bind(var("Y"), parse("@2 c{Z}")),
bind(var("Z"), parse("@1 b{c{^1}}"))
);
assertUnifiesWithBindings(
parse("@1 a{c{d} b{e{Z f}} ^1}"),
parse(" a{c{X} b{Y} Z}"),
bind(var("X"), parse("d")),
bind(var("Y"), parse("e{Z f}")),
bind(var("Z"), parse("@1 a{c{d} b{e{Z f}} ^1}"))
);
}
@Test
public void testCyclicVar() throws Exception {
assertUnifiesWithBindings(
parse("@1 a{b ^1}"),
parse("@1 a{b X}"),
bind(var("X"), parse("@1 a{b ^1}"))
);
assertUnifiesWithBindings(
parse("@1 a{b ^1}"),
parse("X"),
@ -392,12 +299,6 @@ public class SolverTests {
bind(var("X"), parse("@1 a{^1 b c}"))
);
assertUnifiesWithBindings(
parse("@1 a{b ^1}"),
parse("@1 a{b a{b X}}"),
bind(var("X"), parse("@1 a{b ^1}"))
);
assertUnifiesWithBindings(
parse("a{X c{X} }"),
parse("a{b{Y} c{@1 b{@2 c{b{^2}}}}}"),
@ -441,35 +342,6 @@ public class SolverTests {
);
}
@Test
public void testCyclic_TermRewriting() throws Exception {
// The original problem is to unify two cyclic terms:
//
// +->f +--->f
// |_/ \ | / \
// X | f f<-+
// |_/ \ / \_|
// Y
//
// -- which would be equivalent to the following:
//
// "@1 f {^1 X}" "@2 f {f {^2 Y} @3 f {Y ^3}}"
//
// Unfortunately, although the algorithm can successfully unify these
// two terms, no solution exists that is not recursive. That is,
// we cannot produce a list of variable bindings that do not include a
// variable itself in the substitution. Thus, we resort to a simplified test.
assertUnifiesWithBindings(
parse("@1 f {^1 X}"),
parse("@2 f {f {^2 Y} @3 f {Z ^3}}"),
bind(var("X"), parse("@1 f{Z ^1}")),
bind(var("Y"), parse("@1 f{Z ^1}"))
);
}
@Test
public void testUnifyExternalRef() throws Exception {
Term termRef = ref(parse("f {a f{b f{c d}}}"));
@ -604,12 +476,36 @@ public class SolverTests {
@Test
public void testFailCyclic() throws Exception {
assertUnificationFails(
term("g", ref(parse("f {h X}"))),
term("g", var("X")),
CYCLE_DETECTED
);
assertUnificationFails(
parse("t {@1 f {h X} g {f {h X}}}"),
parse("t {Y g {X}}"),
CYCLE_DETECTED
);
assertUnificationFails(
parse("a{b X}"),
parse("X"),
CYCLE_DETECTED
);
assertUnificationFails(
parse("f{X}"),
parse("X"),
CYCLE_DETECTED
);
assertUnificationFails(
parse("X"),
parse("f{X}"),
CYCLE_DETECTED
);
assertUnificationFails(
parse("f{f{X}}"),
parse("f{X}"),
@ -632,6 +528,18 @@ public class SolverTests {
parse("a{ b{c{b{c{b{c{^2}}}}}} @2 b{c{b{c{^2}}}}}"),
parse("a{ b{Y} b{Y} }"),
CYCLE_DETECTED
);
assertUnificationFails(
parse("t {@1 f {h X} g {f {h X}}}"),
parse("t {Y g {X}}"),
CYCLE_DETECTED
);
assertUnificationFails(
parse("t {@1 f {h X} g {^1}}"),
parse("t {Y g {X}}"),
CYCLE_DETECTED
);
}