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

Ensure cyclic terms in the solution are fully reconciled, some tests and code cleanup

This commit is contained in:
Fedor Isakov 2015-03-24 11:49:06 +01:00
parent 690e2929bb
commit 80d16b592d
3 changed files with 84 additions and 60 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -16,8 +16,13 @@
package jetbrains.mps.unification;
import jetbrains.mps.unification.Unification.SuccessfulSubstitution;
import java.util.*;
import static jetbrains.mps.unification.Node.Kind.*;
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>
@ -44,9 +49,11 @@ public class UnionFindTermGraphUnifier {
private Map<Object, Data> myData = new IdentityHashMap<Object, Data>();
private int myUnreconciledRefs = 0;
public Substitution unify(Node a, Node b) {
if (!unifClosure(a, b)) {
return Unification.FAILED_SUBSTITUTION;
return FAILED_SUBSTITUTION;
}
return findSolution(a);
@ -62,16 +69,16 @@ public class UnionFindTermGraphUnifier {
Node zt = getSchema(t);
// a VAR always matches another node
if(zs.is(Node.Kind.VAR) || zt.is(Node.Kind.VAR)) {
if(zs.is(VAR) || zt.is(VAR)) {
union(s, t);
return true;
}
// dereference REF nodes
Node ds = zs.is(Node.Kind.REF) ? zs.get() : zs;
Node dt = zt.is(Node.Kind.REF) ? zt.get() : zt;
Node ds = zs.is(REF) ? zs.get() : zs;
Node dt = zt.is(REF) ? zt.get() : zt;
if (ds.is(Node.Kind.VAR)) {
if (ds.is(VAR)) {
if (s != find(ds)) {
union(s, find(ds));
}
@ -82,7 +89,7 @@ public class UnionFindTermGraphUnifier {
zs = ds;
}
if (dt.is(Node.Kind.VAR)) {
if (dt.is(VAR)) {
if (t != find(dt)) {
union(t, find(dt));
}
@ -98,14 +105,14 @@ public class UnionFindTermGraphUnifier {
return true;
}
if (zs.is(Node.Kind.FUN) && zt.is(Node.Kind.FUN))
if (zs.is(FUN) && zt.is(FUN))
{
if (!eq(zs.symbol(), zt.symbol())) {
return false; // symbol clash
}
// union REF nodes only to each other
if (s.is(Node.Kind.REF) == t.is(Node.Kind.REF)) {
if (s.is(REF) == t.is(REF)) {
union(s, t);
}
@ -132,7 +139,7 @@ public class UnionFindTermGraphUnifier {
if (ssize < tsize) {
Node tmp = t; t = s; s = tmp;
}
else if (ssize == tsize && s.is(Node.Kind.VAR) && t.is(Node.Kind.VAR)) {
else if (ssize == tsize && s.is(VAR) && t.is(VAR)) {
// ensure proper order of variables in the substitution
if(t.compareTo(s) < 0) {
Node tmp = t; t = s; s = tmp;
@ -146,8 +153,7 @@ public class UnionFindTermGraphUnifier {
Node zs = getSchema(s);
Node zt = getSchema(t);
if (zs.is(Node.Kind.VAR) ||
(zs.is(Node.Kind.REF) && zs.get().is(Node.Kind.VAR) && !zt.is(Node.Kind.VAR)))
if (zs.is(VAR) || (zs.is(REF) && zs.get().is(VAR) && !zt.is(VAR)))
{
setSchema(s, zt);
}
@ -177,7 +183,8 @@ public class UnionFindTermGraphUnifier {
}
private Substitution findSolution(Node s) {
return findSolution(s, Unification.EMPTY_SUBSTITUTION);
myUnreconciledRefs = 0;
return findSolution(s, EMPTY_SUBSTITUTION);
}
private Substitution findSolution(Node s, Substitution substitution) {
@ -187,10 +194,11 @@ public class UnionFindTermGraphUnifier {
return substitution; // not part of a cycle
}
if (isVisited(z)) {
return Unification.FAILED_SUBSTITUTION; // there exists a cycle
return FAILED_SUBSTITUTION; // there exists a cycle
}
if (z.is(Node.Kind.FUN)) {
int unreconciled = myUnreconciledRefs;
if (z.is(FUN)) {
setVisited(z, true);
for (Node c : z.children()) {
@ -208,15 +216,24 @@ public class UnionFindTermGraphUnifier {
return substitution;
}
if (isReferenced(z)) {
setReferenced(z, false);
myUnreconciledRefs--;
}
setAcyclic(z, true);
Unification.SuccessfulSubstitution success = new Unification.SuccessfulSubstitution(substitution);
SuccessfulSubstitution success = new SuccessfulSubstitution(substitution);
for (Node var : getVars(find(z))) {
if (var != z) {
Node val = z.is(Node.Kind.REF) ? z.get() : z;
if (myUnreconciledRefs != unreconciled) {
return FAILED_SUBSTITUTION; // there's an unreconciled outward reference
}
Node val = z.is(REF) ? z.get() : z;
// Keep the order of variables within a binding
if (val.is(Node.Kind.VAR) && val.compareTo(var) < 0) {
if (val.is(VAR) && val.compareTo(var) < 0) {
success.addBinding(val, var);
}
else {
@ -225,6 +242,11 @@ public class UnionFindTermGraphUnifier {
}
}
if (z.is(REF) && z.get().is(FUN)) {
setReferenced(z.get(), true);
myUnreconciledRefs++;
}
return success;
}
@ -256,10 +278,7 @@ public class UnionFindTermGraphUnifier {
}
private List<Node> getVars(Node n) {
if (!hasData(n)) {
return collectVars(n);
}
return getData(n).myVars;
return hasData(n) ? getData(n).myVars : singletonVar(n);
}
private void appendVars(Node n, List<Node> vars) {
@ -269,8 +288,7 @@ public class UnionFindTermGraphUnifier {
}
private boolean isAcyclic(Node n) {
if (!hasData(n)) return false;
return getData(n).myAcyclic;
return hasData(n) && getData(n).myAcyclic;
}
private void setAcyclic(Node n, boolean acyclic) {
@ -278,50 +296,58 @@ public class UnionFindTermGraphUnifier {
}
private boolean isVisited(Node n) {
if (!hasData(n)) return false;
return getData(n).myVisited;
return hasData(n) && getData(n).myVisited;
}
private void setVisited(Node n, boolean visited) {
getData(n).myVisited = visited;
}
private boolean isReferenced(Node n) {
return hasData(n) && getData(n).myReferenced;
}
private void setReferenced(Node n, boolean referenced) {
getData(n).myReferenced = referenced;
}
private boolean hasData(Node n) {
Object key = n.is(Node.Kind.VAR) ? String.valueOf(n.symbol()).intern() : n;
Object key = n.is(VAR) ? String.valueOf(n.symbol()).intern() : n;
return myData.containsKey(key);
}
private Data getData(Node n) {
Object key = n.is(Node.Kind.VAR) ? String.valueOf(n.symbol()).intern() : n;
Object key = n.is(VAR) ? String.valueOf(n.symbol()).intern() : n;
if (myData.containsKey(key)) return myData.get(key);
Data data = new Data(n);
myData.put(key, data);
return data;
}
private List<Node> collectVars(Node n) {
if (n.is(Node.Kind.VAR)) {
return Collections.singletonList(n);
}
return Collections.<Node>emptyList();
}
private boolean eq(Object a, Object b) {
private static boolean eq(Object a, Object b) {
return a == null ? b == null : a.equals(b);
}
private class Data {
private static List<Node> singletonVar(Node n) {
return n.is(VAR) ?
Collections.singletonList(n) :
Collections.<Node>emptyList();
}
private static class Data {
int mySize = 1;
boolean myAcyclic = false;
boolean myVisited = false;
List<Node> myVars;
boolean myReferenced = false;
List<Node> myVars;
Node myClass;
Node mySchema;
Data(Node n) {
myClass = n;
mySchema = n;
myVars = collectVars(n);
myVars = singletonVar(n);
}
}
}

3
reactor/tests/src/jetbrains/mps/unification/test/AssertStructurallyEquivalent.java
View File

@ -84,10 +84,11 @@ public class AssertStructurallyEquivalent {
private static class Signature {
private NodeWalker[] walkers;
private IdentityHashMap<Node, Integer> labels = new IdentityHashMap<Node, Integer>();
private int label = 1;
private StringBuilder signature = new StringBuilder();
private NodeWalker[] walkers;
protected void label(Node node) {
labels.put(node, label++);

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

@ -382,31 +382,15 @@ public class SolverTests {
}
@Test
public void testFail1() throws Exception {
public void testFailConflict() throws Exception {
assertUnificationFails(
term("a"),
term("b")
);
}
@Test
public void testFail2() throws Exception {
assertUnificationFails(
parse("a{b c}"),
parse("a{X}")
);
}
@Test
public void testFail3() throws Exception {
assertUnificationFails(
parse("node{name{X} child{abc}}"),
parse("node{name{foo} child{X}}")
);
}
@Test
public void testFail4() throws Exception {
assertUnificationFails(
parse("f{a{X} Y }"),
parse("f{Y a{b{X}}}")
@ -414,18 +398,31 @@ public class SolverTests {
}
@Test
public void testFail5() throws Exception {
public void testFailCard() throws Exception {
assertUnificationFails(
parse("f{X}"),
parse("X")
parse("a{b c}"),
parse("a{X}")
);
}
@Test
public void testFail6() throws Exception {
public void testFailRecursive() throws Exception {
assertUnificationFails(
parse("f{X}"),
parse("X")
);
assertUnificationFails(
parse("f{f{X}}"),
parse("f{X}")
);
assertUnificationFails(
parse("a{X c{X}}"),
parse("a{b{Y} Y }")
);
assertUnificationFails (
parse("a{@1 b{c{^1}} @2 c{b{^2}}}"),
parse("a{ b{Y} Y }")
);
}
}