diff --git a/reactor/code/src/jetbrains/mps/unification/Node.java b/reactor/code/src/jetbrains/mps/unification/Node.java index b37f1b19..f9494f81 100644 --- a/reactor/code/src/jetbrains/mps/unification/Node.java +++ b/reactor/code/src/jetbrains/mps/unification/Node.java @@ -16,19 +16,45 @@ package jetbrains.mps.unification; +import java.util.Collection; + /** - * Represents a node in a term DAG. A node can be either a an instance of - * {@link Term} or {@link Var}. + * Represents a node in a term graph. The graph may contain cycles. A node in a term + * graph can be of three kinds: a variable, a function (possibly constant) and a reference. + * A reference must point to a function term. + * + * A term must implement {@link java.lang.Comparable}, but this is only really used for + * comparing the variables. + * + * Soon to be renamed to Term. * * @author Fedor Isakov */ -public interface Node { +public interface Node extends Comparable { + @Deprecated boolean isTerm(); + @Deprecated Term asTerm(); + @Deprecated boolean isVar(); + @Deprecated Var asVar(); + + Object symbol(); + + Collection children(); + + Node get(); + + boolean is(Kind kind); + + enum Kind { + FUN, + VAR, + REF + } } diff --git a/reactor/code/src/jetbrains/mps/unification/Substitution.java b/reactor/code/src/jetbrains/mps/unification/Substitution.java index fe221dbd..1e16b58c 100644 --- a/reactor/code/src/jetbrains/mps/unification/Substitution.java +++ b/reactor/code/src/jetbrains/mps/unification/Substitution.java @@ -32,15 +32,15 @@ public interface Substitution { Collection bindings() ; public class Binding { - private Var myVar; + private Node myVar; private Node myNode; - public Binding(Var myVar, Node myNode) { + public Binding(Node myVar, Node myNode) { this.myVar = myVar; this.myNode = myNode; } - public Var var() { + public Node var() { return myVar; } diff --git a/reactor/code/src/jetbrains/mps/unification/Term.java b/reactor/code/src/jetbrains/mps/unification/Term.java index e727eb1f..679dc8f4 100644 --- a/reactor/code/src/jetbrains/mps/unification/Term.java +++ b/reactor/code/src/jetbrains/mps/unification/Term.java @@ -21,8 +21,10 @@ import java.util.Collection; /** * A term node. Has a symbol object and a read-only collection of children nodes. * + * @deprecated soon to be removed * @author Fedor Isakov */ +@Deprecated public interface Term extends Node { Object symbol(); diff --git a/reactor/code/src/jetbrains/mps/unification/Unification.java b/reactor/code/src/jetbrains/mps/unification/Unification.java index beaddf53..fb22cbbc 100644 --- a/reactor/code/src/jetbrains/mps/unification/Unification.java +++ b/reactor/code/src/jetbrains/mps/unification/Unification.java @@ -19,233 +19,20 @@ package jetbrains.mps.unification; import java.util.*; /** - * This is an implementation of the "near linear" algorithm for solving syntactic unification - * as described in the paper linked below.1 No recursive terms are allowed, meaning the "occurrs check" - * is performed on the input. If successful, the returned {@link Substitution} contains - * the variable bindings. - *

- * The variables are sorted using {@link java.lang.Comparable} to ensure uniqueness of bindings - * whereas the substituted term is also a variable. - *

- *

- * 1. Baader, Franz, and Wayne Snyder. "Unification Theory." Handbook of automated reasoning 1 (2001): 445-532. - *
+ * This is the main entry point to the unification solver. Presently @{link UnionFindTermGraphUnifier} is used + * for finding the solution. * * @author Fedor Isakov */ public class Unification { public static Substitution unify(Node a, Node b) { - DagUnifier dagUnifier = new DagUnifier(); + UnionFindTermGraphUnifier dagUnifier = new UnionFindTermGraphUnifier(); - if (!dagUnifier.unifClosure(a, b)) return FAILED_SUBSTITUTION; - - return dagUnifier.findSolution(a); + return dagUnifier.unify(a, b); } - private static class DagUnifier { - - private Map myData = new HashMap(); - - private boolean unifClosure(Node s, Node t) { - s = find(s); - t = find(t); - - if (s == t) return true; - - Node zs = getSchema(s); - Node zt = getSchema(t); - - if (zs.isTerm() && zt.isTerm()) { - if (eq(zs.asTerm().symbol(), zt.asTerm().symbol())) { - union(s, t); - Iterator scit = zs.asTerm().children().iterator(); - Iterator tcit = zt.asTerm().children().iterator(); - while(scit.hasNext() && tcit.hasNext()) { - if (!unifClosure(scit.next(), tcit.next())) return false; - } - if (scit.hasNext() != tcit.hasNext()) { - return false; // children lists are of different size - } - } - else { - return false; // symbol clash - } - } - else { - union(s, t); - } - - return true; - } - - private void union(Node s, Node t) { - Integer ssize = getSize(s); - Integer tsize = getSize(t); - - // keep the order - if (ssize < tsize) { - Node tmp = t; t = s; s = tmp; - } - else if (ssize == tsize && s.isVar() && t.isVar()) { - // ensure proper order of variables in the substitution - if(s.asVar().compareTo(t.asVar()) < 0) { - Node tmp = t; t = s; s = tmp; - } - } - - // union s and t classes by moving t under s - - setSize(s, ssize + tsize); - appendVars(s, getVars(t)); - if (getSchema(s).isVar()) { - setSchema(s, getSchema(t)); - } - setRepresentative(t, s); - } - - private Node find(Node s) { - Node node = getRepresentative(s); - if (node == s) return s; - - // find representative and compress paths - - List path = new ArrayList(); - path.add(node); - for (Node t; (t = getRepresentative(node)) != node; ) { - path.add(t); - node = t; - } - for (Node p : path) { - setRepresentative(p, node); - } - - return node; - } - - private Substitution findSolution(Node s) { - return findSolution(s, EMPTY_SUBSTITUTION); - } - - private Substitution findSolution(Node s, Substitution substitution) { - Node z = getSchema(find(s)); - - if (isAcyclic(z)) return substitution; // not part of a cycle - if (isVisited(z)) return FAILED_SUBSTITUTION; // there exists a cycle - - if (z.isTerm()) { - setVisited(z, true); - - for (Node c : z.asTerm().children()) { - substitution = findSolution(c, substitution); - if (!substitution.isSuccessful()) return substitution; - } - - setVisited(z, false); - } - - setAcyclic(z, true); - - SuccessfulSubstitution success = new SuccessfulSubstitution(substitution); - for (Var var : getVars(find(z))) { - if (var != z) { - success.addBinding(var, z); - } - } - - return success; - } - - private int getSize(Node n) { - if (!hasData(n)) return 1; - return getData(n).mySize; - } - - private void setSize(Node n, int size) { - getData(n).mySize = size; - } - - private Node getRepresentative(Node n) { - if (!hasData(n)) return n; - return getData(n).myClass; - } - - private void setRepresentative(Node n, Node rep) { - getData(n).myClass = rep; - } - - private Node getSchema(Node n) { - if (!hasData(n)) return n; - return getData(n).mySchema; - } - - private void setSchema(Node n, Node schema) { - getData(n).mySchema = schema; - } - - private List getVars(Node n) { - if (!hasData(n)) { - return n.isTerm() ? Collections.emptyList() : Collections.singletonList(n.asVar()); - } - return getData(n).myVars; - } - - private void appendVars(Node n, List vars) { - List newVars = new ArrayList(getVars(n)); - newVars.addAll(vars); - getData(n).myVars = newVars; - } - - private boolean isAcyclic(Node n) { - if (!hasData(n)) return false; - return getData(n).myAcyclic; - } - - private void setAcyclic(Node n, boolean acyclic) { - getData(n).myAcyclic = acyclic; - } - - private boolean isVisited(Node n) { - if (!hasData(n)) return false; - return getData(n).myVisited; - } - - private void setVisited(Node n, boolean visited) { - getData(n).myVisited = visited; - } - - private boolean hasData(Node n) { - return myData.containsKey(n); - } - - private Data getData(Node n) { - if (myData.containsKey(n)) return myData.get(n); - Data data = new Data(n); - myData.put(n, data); - return data; - } - - private boolean eq(Object a, Object b) { - return a == null ? b == null : a.equals(b); - } - - private static class Data { - int mySize = 1; - boolean myAcyclic = false; - boolean myVisited = false; - List myVars; - - Node myClass; - Node mySchema; - Data(Node n) { - myClass = n; - mySchema = n; - myVars = n.isTerm() ? Collections.emptyList() : Collections.singletonList(n.asVar()); - } - } - } - - private static final Substitution FAILED_SUBSTITUTION = new Substitution() { + protected static final Substitution FAILED_SUBSTITUTION = new Substitution() { @Override public boolean isSuccessful() { return false; @@ -262,7 +49,7 @@ public class Unification { } }; - private static final Substitution EMPTY_SUBSTITUTION = new Substitution() { + protected static final Substitution EMPTY_SUBSTITUTION = new Substitution() { @Override public boolean isSuccessful() { return true; @@ -279,11 +66,11 @@ public class Unification { } }; - private static class SuccessfulSubstitution implements Substitution { + protected static class SuccessfulSubstitution implements Substitution { private LinkedList myBindings; - private SuccessfulSubstitution(Substitution substitution) { + protected SuccessfulSubstitution(Substitution substitution) { this.myBindings = new LinkedList(substitution.bindings()); } @@ -308,10 +95,10 @@ public class Unification { return sb.append("]").toString(); } - private void addBinding(Var v, Node n) { + protected void addBinding(Node v, Node n) { Binding bng; - if (n.isVar() && n.asVar().compareTo(v) < 0) { - bng = new Binding(n.asVar(), v); + if (n.is(Node.Kind.VAR) && n.compareTo(n) < 0) { + bng = new Binding((Var)n, v); } else { bng = new Binding(v, n); diff --git a/reactor/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java b/reactor/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java new file mode 100644 index 00000000..e3b8bab0 --- /dev/null +++ b/reactor/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java @@ -0,0 +1,278 @@ +/* + * Copyright 2015 JetBrains s.r.o. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package jetbrains.mps.unification; + +import java.util.*; + +/** + * 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.1 2 + * + * 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 bindind variables to cyclic terms. + * + * If successful, the returned {@link Substitution} contains + * the variable bindings. + *

+ * The variables are sorted using {@link java.lang.Comparable} to ensure uniqueness of bindings + * whereas the substituted term is also a variable. + *

+ *

+ * 1. Baader, Franz, and Wayne Snyder. "Unification Theory." Handbook of automated reasoning 1 (2001): 445-532. + * 2. Baader, Franz, and Tobias Nipkow. Term rewriting and all that. Cambridge University Press, 1999. + *
+ * + * @author Fedor Isakov + */ +public class UnionFindTermGraphUnifier { + + private Map myData = new HashMap(); + + public Substitution unify(Node a, Node b) { + if (!unifClosure(a, b)) { + return Unification.FAILED_SUBSTITUTION; + } + + return findSolution(a); + } + + private boolean unifClosure(Node s, Node t) { + s = find(s); + t = find(t); + + if (s == t) return true; + + Node zs = getSchema(s); + Node zt = getSchema(t); + + // a VAR always matches another node + if(zs.is(Node.Kind.VAR) || zt.is(Node.Kind.VAR)) { + union(s, t); + return true; + } + + // dereference REF nodes + zs = zs.is(Node.Kind.REF) ? zs.get() : zs; + zt = zt.is(Node.Kind.REF) ? zt.get() : zt; + + // use find 2nd time to account for dereferenced nodes + if (find(zs) == find(zt)) return true; + + if (zs.is(Node.Kind.FUN) && zt.is(Node.Kind.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)) { + union(s, t); + } + + Iterator scit = zs.children().iterator(); + Iterator tcit = zt.children().iterator(); + while (scit.hasNext() && tcit.hasNext()) { + if (!unifClosure(scit.next(), tcit.next())) return false; + } + + // fail if different children count + return scit.hasNext() == tcit.hasNext(); + } + else { + // something's wrong with the input + return false; + } + } + + private void union(Node s, Node t) { + int ssize = getSize(s); + int tsize = getSize(t); + + // keep the order + if (ssize < tsize) { + Node tmp = t; t = s; s = tmp; + } + else if (ssize == tsize && s.is(Node.Kind.VAR) && t.is(Node.Kind.VAR)) { + // ensure proper order of variables in the substitution + if(s.compareTo(t) < 0) { + Node tmp = t; t = s; s = tmp; + } + } + + // union s and t classes by moving t under s + + setSize(s, ssize + tsize); + appendVars(s, getVars(t)); + if (getSchema(s).is(Node.Kind.VAR)) { + setSchema(s, getSchema(t)); + } + setRepresentative(t, s); + } + + private Node find(Node s) { + Node node = getRepresentative(s); + if (node == s) { + return s; + } + + // find representative and compress paths + + List path = new ArrayList(); + path.add(node); + for (Node t; (t = getRepresentative(node)) != node; ) { + path.add(t); + node = t; + } + for (Node p : path) { + setRepresentative(p, node); + } + + return node; + } + + private Substitution findSolution(Node s) { + return findSolution(s, Unification.EMPTY_SUBSTITUTION); + } + + private Substitution findSolution(Node s, Substitution substitution) { + Node z = getSchema(find(s)); + + if (isAcyclic(z)) { + return substitution; // not part of a cycle + } + if (isVisited(z)) { + return Unification.FAILED_SUBSTITUTION; // there exists a cycle + } + + if (z.is(Node.Kind.FUN)) { + setVisited(z, true); + + for (Node c : z.children()) { + substitution = findSolution(c, substitution); + if (!substitution.isSuccessful()) { + break; + } + } + + setVisited(z, false); + } + + if (!substitution.isSuccessful()) { + return substitution; + } + + setAcyclic(z, true); + + Unification.SuccessfulSubstitution success = new Unification.SuccessfulSubstitution(substitution); + for (Var var : getVars(find(z))) { + if (var != z) { + success.addBinding(var, z.is(Node.Kind.REF) ? z.get() : z); + } + } + + return success; + } + + private int getSize(Node n) { + if (!hasData(n)) return 1; + return getData(n).mySize; + } + + private void setSize(Node n, int size) { + getData(n).mySize = size; + } + + private Node getRepresentative(Node n) { + if (!hasData(n)) return n; + return getData(n).myClass; + } + + private void setRepresentative(Node n, Node rep) { + getData(n).myClass = rep; + } + + private Node getSchema(Node n) { + if (!hasData(n)) return n; + return getData(n).mySchema; + } + + private void setSchema(Node n, Node schema) { + getData(n).mySchema = schema; + } + + private List getVars(Node n) { + if (!hasData(n)) { + return n.is(Node.Kind.VAR) ? Collections.singletonList((Var)n) : Collections.emptyList(); + } + return getData(n).myVars; + } + + private void appendVars(Node n, List vars) { + List newVars = new ArrayList(getVars(n)); + newVars.addAll(vars); + getData(n).myVars = newVars; + } + + private boolean isAcyclic(Node n) { + if (!hasData(n)) return false; + return getData(n).myAcyclic; + } + + private void setAcyclic(Node n, boolean acyclic) { + getData(n).myAcyclic = acyclic; + } + + private boolean isVisited(Node n) { + if (!hasData(n)) return false; + return getData(n).myVisited; + } + + private void setVisited(Node n, boolean visited) { + getData(n).myVisited = visited; + } + + private boolean hasData(Node n) { + return myData.containsKey(n); + } + + private Data getData(Node n) { + if (myData.containsKey(n)) return myData.get(n); + Data data = new Data(n); + myData.put(n, data); + return data; + } + + private boolean eq(Object a, Object b) { + return a == null ? b == null : a.equals(b); + } + + private static class Data { + int mySize = 1; + boolean myAcyclic = false; + boolean myVisited = false; + List myVars; + + Node myClass; + Node mySchema; + Data(Node n) { + myClass = n; + mySchema = n; + myVars = n.is(Node.Kind.VAR) ? Collections.singletonList((Var)n) : Collections.emptyList(); + } + } +} diff --git a/reactor/code/src/jetbrains/mps/unification/Var.java b/reactor/code/src/jetbrains/mps/unification/Var.java index 8ef1514d..729f76f0 100644 --- a/reactor/code/src/jetbrains/mps/unification/Var.java +++ b/reactor/code/src/jetbrains/mps/unification/Var.java @@ -19,10 +19,15 @@ package jetbrains.mps.unification; /** * A variable node. Has a name and must implement {@link java.lang.Comparable}. * + * @deprecated soon to be removed * @author Fedor Isakov */ -public interface Var extends Node, Comparable { +@Deprecated +public interface Var extends Node { + Object symbol(); + + @Deprecated String name(); } diff --git a/reactor/tests/src/jetbrains/mps/unification/test/AssertStructurallyEquivalent.java b/reactor/tests/src/jetbrains/mps/unification/test/AssertStructurallyEquivalent.java new file mode 100644 index 00000000..eaea6dae --- /dev/null +++ b/reactor/tests/src/jetbrains/mps/unification/test/AssertStructurallyEquivalent.java @@ -0,0 +1,158 @@ +/* + * Copyright 2015 JetBrains s.r.o. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package jetbrains.mps.unification.test; + +import jetbrains.mps.unification.Node; +import static org.junit.Assert.*; + +import java.util.*; + +/** + * @author Fedor Isakov + */ +public class AssertStructurallyEquivalent { + + public static void assertEquivalent(Node a, Node b) throws Exception { + + final Signature signature = new Signature(); + signature.setWalkers( + // first pass + new NodeWalker( + new NodeVisitor(Node.Kind.FUN) { + @Override + public Collection visit(Node term) throws Exception { + signature.label(term); + return term.children(); + } + }), + // second pass + new NodeWalker( + new NodeVisitor(Node.Kind.FUN) { + @Override + public Collection visit(Node term) throws Exception { + signature.appendSignature("@").append(signature.getLabel(term)).append(term.symbol()); + return term.children(); + } + }, + new NodeVisitor(Node.Kind.VAR) { + @Override + public Collection visit(Node var) throws Exception { + signature.appendSignature("$").append(var.symbol()); + return Collections.emptyList(); + } + }, new NodeVisitor(Node.Kind.REF) { + @Override + public Collection visit(Node ref) throws Exception { + Integer label = signature.getLabel(ref.get()); + assertNotNull("not found label for '"+ref.get() + "'", label); + signature.appendSignature("^").append(label); + return Collections.emptyList(); + } + }) + ); + + String signa = signature.getSignature(a); + String signb = signature.getSignature(b); + + assertEquals(signa, signb); + } + + + private static class Signature { + + private IdentityHashMap labels = new IdentityHashMap(); + private int label = 1; + private StringBuilder signature = new StringBuilder(); + private NodeWalker[] walkers; + + protected void label(Node node) { + labels.put(node, label++); + } + + protected Integer getLabel(Node node) { + return labels.get(node); + } + + protected StringBuilder appendSignature(String str) { + return signature.append(str); + } + + public String getSignature (Node node) throws Exception { + reset(); + for (NodeWalker walker : walkers) { + walker.walk(node); + } + return signature.toString(); + } + + protected void reset() { + labels.clear(); + this.label = 1; + signature.setLength(0); + } + + protected void setWalkers(NodeWalker ... walkers) { + this.walkers = walkers; + } + } + + private static abstract class NodeVisitor { + + private Node.Kind kind; + + public NodeVisitor(Node.Kind kind) { + this.kind = kind; + } + + public Node.Kind applicableTo() { + return kind; + } + + public abstract Collection visit(T t) throws Exception ; + + } + + private static class NodeWalker { + + private Map> visitorMap = new HashMap>(); + + public NodeWalker(NodeVisitor... visitors) { + for (NodeVisitor visitor : visitors) { + visitorMap.put(visitor.applicableTo(), visitor); + } + } + + public void walk(Node node) throws Exception { + Collection children = switchClass(node); + for (Node child : children) { + walk(child); + } + } + + private Collection switchClass(Node node) throws Exception { + for (Map.Entry> e : visitorMap.entrySet()) { + if (node.is(e.getKey())) { + NodeVisitor value = (NodeVisitor) e.getValue(); + return value.visit(node); + } + } + return Collections.emptyList(); + } + + } + +} diff --git a/reactor/tests/src/jetbrains/mps/unification/test/AssertUnification.java b/reactor/tests/src/jetbrains/mps/unification/test/AssertUnification.java index e25a4e57..b5380ec2 100644 --- a/reactor/tests/src/jetbrains/mps/unification/test/AssertUnification.java +++ b/reactor/tests/src/jetbrains/mps/unification/test/AssertUnification.java @@ -24,6 +24,7 @@ import jetbrains.mps.unification.Var; import java.util.*; +import static jetbrains.mps.unification.test.AssertStructurallyEquivalent.assertEquivalent; import static org.junit.Assert.*; @@ -32,27 +33,32 @@ import static org.junit.Assert.*; */ public class AssertUnification { - public static Binding bind(Var v, Node n) { + public static final Comparator BINDING_COMPARATOR = new Comparator() { + @Override + public int compare(Binding a, Binding b) { + return a.var().compareTo(b.var()); + } + }; + + public static Binding bind(Node v, Node n) { return new Binding(v, n); } public static void assertSameBindings(Collection expected, Collection actual) throws Exception { - Iterator expIt = expected.iterator(); - Iterator actIt = actual.iterator(); - - Map expMap = new HashMap(); - Map actMap = new HashMap(); + ArrayList expectedCopy = new ArrayList(expected); + Collections.sort(expectedCopy, BINDING_COMPARATOR); + Iterator expIt = expectedCopy.iterator(); + ArrayList actualCopy = new ArrayList(actual); + Collections.sort(actualCopy, BINDING_COMPARATOR); + Iterator actIt = actualCopy.iterator(); while(expIt.hasNext() && actIt.hasNext()) { Binding expb = expIt.next(); Binding actb = actIt.next(); - expMap.put(expb.var(), expb.node()); - actMap.put(actb.var(), actb.node()); + assertEquals(expb.var(), actb.var()); + assertEquivalent(expb.node(), actb.node()); } - - assertEquals(expMap, actMap); - if(expIt.hasNext() || actIt.hasNext()) throw new Exception("mismatched number of bindings"); } @@ -72,7 +78,18 @@ public class AssertUnification { assertSameBindings(subs.bindings(), subs2.bindings()); } - public static void assertUnifificationFails(Node s, Node t) throws Exception { + public static void assertUnifiesWithBindingsAsymm(Node s, Node t, Substitution.Binding ... bindings) throws Exception{ + Substitution subs = Unification.unify(s, t); + + assertTrue(subs.isSuccessful()); + assertSameBindings( + Arrays.asList( + bindings + ), + subs.bindings()); + } + + public static void assertUnificationFails(Node s, Node t) throws Exception { Substitution subs = Unification.unify(s, t); assertFalse(subs.isSuccessful()); diff --git a/reactor/tests/src/jetbrains/mps/unification/test/MockNode.java b/reactor/tests/src/jetbrains/mps/unification/test/MockNode.java index 3d022c8a..52ec28c9 100644 --- a/reactor/tests/src/jetbrains/mps/unification/test/MockNode.java +++ b/reactor/tests/src/jetbrains/mps/unification/test/MockNode.java @@ -30,15 +30,67 @@ public abstract class MockNode implements Node { public MockNode() { } - public static Term term(Object sym, Node ... children) { + public static Node term(Object sym, Node ... children) { return new MockTerm(sym, children); } - public static Var var(String name) { + public static Node var(String name) { return new MockVar(name); } - public static class MockTerm extends MockNode implements Term { + public static Node ref(Node term) { + return new MockRef(term); + } + + public static Node ref(TermLookup termLookup) { + return new MockRef(termLookup); + } + + interface TermLookup { + Node lookupTerm(); + } + + @Override + public boolean isTerm() { + return is(Kind.FUN); + } + + @Override + public Term asTerm() { + return (Term) this; + } + + @Override + public boolean isVar() { + return is(Kind.VAR); + } + + @Override + public Var asVar() { + return (Var) this; + } + + @Override + public Object symbol() { + return null; + } + + @Override + public Collection children() { + return null; + } + + @Override + public Node get() { + return this; + } + + @Override + public int compareTo(Node node) { + return String.valueOf(symbol()).compareTo(String.valueOf(node.symbol())); + } + + public static class MockTerm extends MockNode { private List myChildren; private Object mySymbol; @@ -47,26 +99,6 @@ public abstract class MockNode implements Node { this.myChildren = Arrays.asList(children); } - @Override - public boolean isTerm() { - return true; - } - - @Override - public boolean isVar() { - return false; - } - - @Override - public Term asTerm() { - return this; - } - - @Override - public Var asVar() { - throw new IllegalStateException(); - } - @Override public Object symbol() { return mySymbol; @@ -77,6 +109,11 @@ public abstract class MockNode implements Node { return Collections.unmodifiableList(myChildren); } + @Override + public boolean is(Kind kind) { + return Kind.FUN == kind; + } + @Override public String toString() { StringBuilder sb = new StringBuilder(String.valueOf(mySymbol)); @@ -118,23 +155,13 @@ public abstract class MockNode implements Node { } @Override - public boolean isTerm() { - return false; + public Object symbol() { + return myName; } @Override - public boolean isVar() { - return true; - } - - @Override - public Term asTerm() { - throw new IllegalStateException(); - } - - @Override - public Var asVar() { - return this; + public boolean is(Kind kind) { + return Kind.VAR == kind; } @Override @@ -152,9 +179,53 @@ public abstract class MockNode implements Node { return ((MockVar)o).myName.equals(myName); } + } + + public static class MockRef extends MockNode { + + private Node term; + private TermLookup termLookup; + + public MockRef(Node term) { + this.term = term; + } + + public MockRef(TermLookup termLookup) { + this.termLookup = termLookup; + } + @Override - public int compareTo(Var var) { - return ((String)myName).compareTo((String)((MockVar)var).myName); + public final Node get() { + if (term == null && termLookup != null) { + term = termLookup.lookupTerm(); + termLookup = null; + } + return term; + } + + @Override + public boolean is(Kind kind) { + return Kind.REF == kind; + } + + @Override + public String toString() { + Node t = get(); + return t != null ? "^"+ t.symbol() : "^"; + } + + @Override + public boolean equals(Object that) { + if (that == this) return true; + if (that == null || getClass() != that.getClass()) return false; + + return get() == ((MockNode) that).get(); + } + + @Override + public int hashCode() { + Node t = get(); + return t != null ? System.identityHashCode(t) : 0; } } } diff --git a/reactor/tests/src/jetbrains/mps/unification/test/MockTreeParser.java b/reactor/tests/src/jetbrains/mps/unification/test/MockTreeParser.java index ccbde7ca..fea21202 100644 --- a/reactor/tests/src/jetbrains/mps/unification/test/MockTreeParser.java +++ b/reactor/tests/src/jetbrains/mps/unification/test/MockTreeParser.java @@ -17,7 +17,7 @@ package jetbrains.mps.unification.test; import jetbrains.mps.unification.Node; -import jetbrains.mps.unification.Term; +import jetbrains.mps.unification.Node; import jetbrains.mps.unification.Var; import java.util.*; @@ -43,8 +43,8 @@ public class MockTreeParser { return nodes.get(0); } - public static Term parseTerm(String str) { - return (Term) parse(str); + public static Node parseTerm(String str) { + return (Node) parse(str); } public static Var parseVar(String str) { @@ -55,13 +55,20 @@ public class MockTreeParser { private Token lastToken; private LinkedList termsStack = new LinkedList(); + private LinkedList termsLabelsStack = new LinkedList(); private LinkedList> childrenStack = new LinkedList>(); + private int lastLabel = -1; + private Map termRefs = new HashMap(); + // initialized on the parse finished + private LookupHelper lookupHelper = new LookupHelper(); private List parse(String toParse) { parseNextToken(Token.START, null); loop(toParse); parseNextToken(Token.END, null); checkFinalState(); + checkAllRefsExist(); + lookupHelper.setTermRefs(Collections.unmodifiableMap(new HashMap(termRefs))); return Collections.unmodifiableList(childrenStack.pop()); } @@ -80,7 +87,7 @@ public class MockTreeParser { // see if the last matching succeeded assert matcher != null; if (!matcher.lookingAt() && !matcher.hitEnd()) { - throw new ParseException("unexpected input"); + throw new ParseException("unexpected input: '"+toParse+"'"); } } while (!matcher.hitEnd()); } @@ -103,6 +110,7 @@ public class MockTreeParser { beginTerm(value); break; case VAR: + checkLastTokenNotOneOf(Token.LABEL); if (lastToken == Token.TERM) { emptyTerm(); } @@ -113,7 +121,7 @@ public class MockTreeParser { beginChildren(); break; case RBRACE: - checkLastTokenOneOf(Token.TERM, Token.VAR, Token.RBRACE); + checkLastTokenOneOf(Token.TERM, Token.VAR, Token.REF, Token.RBRACE); if (lastToken == Token.TERM) { emptyTerm(); } @@ -122,15 +130,39 @@ public class MockTreeParser { break; case WHITESPACE: return; // ignore + case LABEL: + checkLastTokenNotOneOf(Token.LABEL); + if (lastToken == Token.TERM) { + emptyTerm(); + } + lastLabel = Integer.parseInt(value.substring(1)); + break; + case REF: + checkLastTokenNotOneOf(Token.LABEL); + if (lastToken == Token.TERM) { + emptyTerm(); + } + addRef(value); + break; } this.lastToken = token; } private void checkLastTokenOneOf(Token ... tokens) { + if (lastToken == Token.WHITESPACE) return; for (Token token : tokens) { if (token == lastToken) return; } - throw new ParseException("parse error"); + throw new ParseException("parse error: unexpected token '"+lastToken+"'"); + } + + private void checkLastTokenNotOneOf(Token ... tokens) { + if (lastToken == Token.WHITESPACE) return; + for (Token token : tokens) { + if (token == lastToken) { + throw new ParseException("parse error: unexpected token '"+lastToken+"'"); + } + } } private void checkFinalState() { @@ -145,13 +177,28 @@ public class MockTreeParser { } } + private void checkAllRefsExist() { + for (Map.Entry e: termRefs.entrySet()) { + if (e.getValue() == null) { + throw new ParseException("non-existing label '" + e.getKey() + "'"); + } + } + } + private void beginTerm(String name) { termsStack.push(name); + termsLabelsStack.push(lastLabel >= 0 ? lastLabel : null); + lastLabel = -1; } private void emptyTerm() { - String term = termsStack.pop(); - childrenStack.peek().add(term(term)); + String name = termsStack.pop(); + Integer label = termsLabelsStack.pop(); + Node newTerm = term(name); + childrenStack.peek().add(newTerm); + if (label != null) { + termRefs.put(label, newTerm); + } } private void beginChildren(){ @@ -159,14 +206,30 @@ public class MockTreeParser { } private void endChildren() { - String term = termsStack.pop(); List children = childrenStack.pop(); - childrenStack.peek().add(term(term, children.toArray(new Node[children.size()]))); + String name = termsStack.pop(); + Integer label = termsLabelsStack.pop(); + Node newTerm = term(name, children.toArray(new Node[children.size()])); + childrenStack.peek().add(newTerm); + if (label != null) { + termRefs.put(label, newTerm); + } } private void addVar(String name) { childrenStack.peek().add(var(name)); } + + private void addRef(String ref) { + final int label = Integer.parseInt(ref.substring(1)); + if (termRefs.containsKey(label)) { + childrenStack.peek().add(ref(termRefs.get(label))); + } + else { + termRefs.put(label, null); + childrenStack.peek().add(ref(lookupHelper.lookup(label))); + } + } } private static enum Token { @@ -176,7 +239,9 @@ public class MockTreeParser { VAR(Pattern.compile("[A-Z][a-zA-Z0-9_]*")), LBRACE(Pattern.compile("\\{")), RBRACE(Pattern.compile("\\}")), - WHITESPACE(Pattern.compile("\\s+")); + WHITESPACE(Pattern.compile("\\s+")), + LABEL(Pattern.compile("@[0-9]+")), + REF(Pattern.compile("\\^[0-9]+")); private Pattern pattern; @@ -190,6 +255,30 @@ public class MockTreeParser { super(s); } } + + private static class LookupHelper { + private Map termRefs; + + private void setTermRefs (Map termRefs) { + this.termRefs = termRefs; + } + + public TermLookup lookup(final int label) { + return new TermLookup() { + @Override + public Node lookupTerm() { + if (termRefs == null) { + throw new IllegalStateException("call to uninitialized lookup"); + } + if (!termRefs.containsKey(label)) { + throw new IllegalStateException("non-existing label '" + label + "'"); + } + return termRefs.get(label); + } + }; + } + + } } diff --git a/reactor/tests/src/jetbrains/mps/unification/test/ParserTests.java b/reactor/tests/src/jetbrains/mps/unification/test/ParserTests.java index e022913d..220ba106 100644 --- a/reactor/tests/src/jetbrains/mps/unification/test/ParserTests.java +++ b/reactor/tests/src/jetbrains/mps/unification/test/ParserTests.java @@ -16,6 +16,8 @@ package jetbrains.mps.unification.test; +import jetbrains.mps.unification.Node; +import org.junit.ComparisonFailure; import org.junit.Test; import static org.junit.Assert.*; @@ -23,17 +25,27 @@ import static org.junit.Assert.*; import static jetbrains.mps.unification.test.MockNode.*; import static jetbrains.mps.unification.test.MockTreeParser.*; import static jetbrains.mps.unification.test.AssertAll.*; +import static jetbrains.mps.unification.test.AssertStructurallyEquivalent.*; /** * Created by fyodor on 10.06.2014. */ public class ParserTests { + private static class LazyTermLookup implements TermLookup{ + private Node term; + + @Override + public Node lookupTerm() { + return term; + } + } + @Test public void testSingle() { assertEquals(parse("a"), term("a")); assertEquals(parseTerm("a").symbol(), term("a").symbol()); - assertEquals(parseVar("X").name(), var("X").name()); + assertEquals(parseVar("X").symbol(), var("X").symbol()); assertEquals(parse("X"), var("X")); assertEquals(parse("a{b}"), term("a", term("b"))); assertEquals(parseTerm("a{b}").symbol(), term("a", term("b")).symbol()); @@ -66,31 +78,75 @@ public class ParserTests { assertEquals(parse("a{b{c{d{e f g}}}}"), term("a", term("b", - term("c", - term("d", - term("e"), term("f"), term("g")))))); + term("c", + term("d", + term("e"), term("f"), term("g")))))); assertEquals(parse("a{X b{c{d{Z e W f g} Y}}}"), term("a", var("X"), term("b", - term("c", - term("d", - var("Z"), term("e"), var("W"), term("f"), term("g")), - var("Y"))))); + term("c", + term("d", + var("Z"), term("e"), var("W"), term("f"), term("g")), + var("Y"))))); + } + + @Test + public void testRef() throws Exception { + LazyTermLookup termLookup = new LazyTermLookup(); + Node a = termLookup.term = term("a", ref(termLookup)); + assertEquivalent(parse("@1a{^1}"), + a); + + Node b = term("b"); + assertEquivalent(parse("a{@1b ^1}"), + term("a", b, ref(b))); + + Node c = term("c"); + assertEquivalent(parse("a{^1 @1c}"), + term("a", ref(c), c)); + + Node b1 = term("b"); + Node b2 = term("b"); + assertEquivalent(parse("a{@2b ^1 ^2 @1b}"), + term("a", b2, ref(b1), ref(b2), b1)); + } + + @Test(expected = ComparisonFailure.class) + public void testNotEquivalent1() throws Exception { + Node d = term("d"); + assertEquivalent(parse("a{^1 @1c}"), + term("a", ref(d), d)); + } + + @Test(expected = ComparisonFailure.class) + public void testNotEquivalent2() throws Exception { + Node b1 = term("b"); + Node b2 = term("b"); + assertEquivalent(parse("a{@2b ^1 @1b ^2}"), + term("a", b2, ref(b2), b1, ref(b1))); + } + + @Test(expected = ComparisonFailure.class) + public void testNotEquivalent3() throws Exception { + Node b1 = term("b"); + Node b2 = term("b"); + assertEquivalent(parse("a{@2b ^1 ^2 @1b}"), + term("a", b2, ref(b2), ref(b1), b1)); } @Test(expected = MockTreeParser.ParseException.class) - public void testUclosedFail() { + public void testUnclosedFail() { parse("a{b "); } @Test(expected = MockTreeParser.ParseException.class) - public void testUclosedFail2() { + public void testUnclosedFail2() { parse("a{X b"); } @Test(expected = MockTreeParser.ParseException.class) - public void testUclosedFail3() { + public void testUnclosedFail3() { parse("a{{X b}"); } @@ -133,4 +189,9 @@ public class ParserTests { public void testExtraSymbolFail() { parse("a}"); } + + @Test(expected = MockTreeParser.ParseException.class) + public void testNonExistingRefFail() { + parse("a{b ^1}"); + } } diff --git a/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java b/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java index 70c17c18..fd258eff 100644 --- a/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java +++ b/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java @@ -213,9 +213,140 @@ public class SolverTests { ); } + @Test + public void test14() throws Exception { + assertUnifiesWithBindings( + parse("f{X g{a}}"), + parse("f{g{Y} g{Y}}"), + + bind(var("X"), parseTerm("g{Y}")), + bind(var("Y"), parseTerm("a")) + ); + } + + @Test + public void test15() throws Exception { + assertUnifiesWithBindingsAsymm( + parse("h{X1 f{Y0 Y0} Y1}"), + parse("h{f{X0 X0} Y1 X1}"), + + bind(var("X0"), parseVar("Y0")), + bind(var("X1"), parseTerm("f{Y0 Y0}")), + bind(var("Y1"), parseTerm("f{Y0 Y0}")) + ); + } + + @Test + public void test16() throws Exception { + // this test illustrates why the used algorithm is superior to recursive descent: + // the latter would have an exponential complexity because of "functional" form of + // substitution instead of the "triangular" form used here. + + assertUnifiesWithBindingsAsymm( + parse("h{X1 X2 X3 X4 X5 X6 X7 X8 X9 " + + "f{Y0 Y0} f{Y1 Y1} f{Y2 Y2} f{Y3 Y3} f{Y4 Y4} f{Y5 Y5} f{Y6 Y6} f{Y7 Y7} f{Y8 Y8} Y9}"), + parse("h{f{X0 X0} f{X1 X1} f{X2 X2} f{X3 X3} f{X4 X4} f{X5 X5} f{X6 X6} f{X7 X7} f{X8 X8} " + + "Y1 Y2 Y3 Y4 Y5 Y6 Y7 Y8 Y9 X9}"), + + bind(var("X0"), parseVar("Y0")), + bind(var("X1"), parseTerm("f{Y0 Y0}")), + bind(var("X2"), parseTerm("f{Y1 Y1}")), + bind(var("X3"), parseTerm("f{Y2 Y2}")), + bind(var("X4"), parseTerm("f{Y3 Y3}")), + bind(var("X5"), parseTerm("f{Y4 Y4}")), + bind(var("X6"), parseTerm("f{Y5 Y5}")), + bind(var("X7"), parseTerm("f{Y6 Y6}")), + bind(var("X8"), parseTerm("f{Y7 Y7}")), + bind(var("X9"), parseTerm("f{Y8 Y8}")), + bind(var("Y1"), parseTerm("f{Y0 Y0}")), + bind(var("Y2"), parseTerm("f{Y1 Y1}")), + bind(var("Y3"), parseTerm("f{Y2 Y2}")), + bind(var("Y4"), parseTerm("f{Y3 Y3}")), + bind(var("Y5"), parseTerm("f{Y4 Y4}")), + bind(var("Y6"), parseTerm("f{Y5 Y5}")), + bind(var("Y7"), parseTerm("f{Y6 Y6}")), + bind(var("Y8"), parseTerm("f{Y7 Y7}")), + bind(var("Y9"), parseTerm("f{Y8 Y8}")) + ); + } + + @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}") + ); + } + + @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"), + + bind(var("X"), parse("@1 a{b ^1}")) + ); + assertUnifiesWithBindings( + parse("@1 a{^1 b c}"), + parse("X"), + + 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}")) + ); + } + + @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 testFail1() throws Exception { - assertUnifificationFails( + assertUnificationFails( term("a"), term("b") ); @@ -223,7 +354,7 @@ public class SolverTests { @Test public void testFail2() throws Exception { - assertUnifificationFails( + assertUnificationFails( parse("a{b c}"), parse("a{X}") ); @@ -231,10 +362,33 @@ public class SolverTests { @Test public void testFail3() throws Exception { - assertUnifificationFails( + 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}}}") + ); + } + + @Test + public void testFail5() throws Exception { + assertUnificationFails( + parse("f{X}"), + parse("X") + ); + } + + @Test + public void testFail6() throws Exception { + assertUnificationFails( + parse("f{f{X}}"), + parse("f{X}") + ); + } }