diff --git a/reactor/.idea/misc.xml b/reactor/.idea/misc.xml index 49cd2039..15f63515 100644 --- a/reactor/.idea/misc.xml +++ b/reactor/.idea/misc.xml @@ -24,5 +24,4 @@ - - + \ No newline at end of file diff --git a/reactor/code/code.iml b/reactor/code/code.iml index d5c07432..c90834f2 100644 --- a/reactor/code/code.iml +++ b/reactor/code/code.iml @@ -8,5 +8,4 @@ - - + \ No newline at end of file diff --git a/reactor/code/src/jetbrains/mps/unification/Node.java b/reactor/code/src/jetbrains/mps/unification/Node.java index 6092033e..c18d4a8c 100644 --- a/reactor/code/src/jetbrains/mps/unification/Node.java +++ b/reactor/code/src/jetbrains/mps/unification/Node.java @@ -21,7 +21,7 @@ import java.util.Collection; /** * 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 reference must point to either a function term or a variable. * * A term must implement {@link java.lang.Comparable}, but this is only really used for * comparing the variables. @@ -32,18 +32,6 @@ import java.util.Collection; */ public interface Node extends Comparable { - @Deprecated - boolean isTerm(); - - @Deprecated - Term asTerm(); - - @Deprecated - boolean isVar(); - - @Deprecated - Var asVar(); - Object symbol(); Collection children(); diff --git a/reactor/code/src/jetbrains/mps/unification/Term.java b/reactor/code/src/jetbrains/mps/unification/Term.java deleted file mode 100644 index 679dc8f4..00000000 --- a/reactor/code/src/jetbrains/mps/unification/Term.java +++ /dev/null @@ -1,34 +0,0 @@ -/* - * Copyright 2014 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.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(); - - Collection children(); - -} diff --git a/reactor/code/src/jetbrains/mps/unification/Unification.java b/reactor/code/src/jetbrains/mps/unification/Unification.java index fb22cbbc..01f4530a 100644 --- a/reactor/code/src/jetbrains/mps/unification/Unification.java +++ b/reactor/code/src/jetbrains/mps/unification/Unification.java @@ -98,7 +98,7 @@ public class Unification { protected void addBinding(Node v, Node n) { Binding bng; if (n.is(Node.Kind.VAR) && n.compareTo(n) < 0) { - bng = new Binding((Var)n, v); + bng = new Binding(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 index a3695484..4ed00562 100644 --- a/reactor/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java +++ b/reactor/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java @@ -24,7 +24,8 @@ import java.util.*; * * 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. + * solutions binding variables to cyclic terms. Variables can also be passed by reference without altering the + * intuitive behaviour of the algorithm. * * If successful, the returned {@link Substitution} contains * the variable bindings. @@ -67,11 +68,35 @@ public class UnionFindTermGraphUnifier { } // dereference REF nodes - zs = zs.is(Node.Kind.REF) ? zs.get() : zs; - zt = zt.is(Node.Kind.REF) ? zt.get() : zt; + Node ds = zs.is(Node.Kind.REF) ? zs.get() : zs; + Node dt = zt.is(Node.Kind.REF) ? zt.get() : zt; + + if (ds.is(Node.Kind.VAR)) { + if (s != find(ds)) { + union(s, find(ds)); + } + union(s, t); + return true; + } + else { + zs = ds; + } + + if (dt.is(Node.Kind.VAR)) { + if (t != find(dt)) { + 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 (find(zs) == find(zt)) { + return true; + } if (zs.is(Node.Kind.FUN) && zt.is(Node.Kind.FUN)) { @@ -103,7 +128,7 @@ public class UnionFindTermGraphUnifier { int ssize = getSize(s); int tsize = getSize(t); - // keep the order + // keep the order: the smaller class gets inserted under the bigger one if (ssize < tsize) { Node tmp = t; t = s; s = tmp; } @@ -118,9 +143,15 @@ public class UnionFindTermGraphUnifier { setSize(s, ssize + tsize); appendVars(s, getVars(t)); - if (getSchema(s).is(Node.Kind.VAR)) { - setSchema(s, getSchema(t)); + + 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))) + { + setSchema(s, zt); } + setRepresentative(t, s); } @@ -164,6 +195,7 @@ public class UnionFindTermGraphUnifier { for (Node c : z.children()) { substitution = findSolution(c, substitution); + if (!substitution.isSuccessful()) { break; } @@ -181,7 +213,15 @@ public class UnionFindTermGraphUnifier { Unification.SuccessfulSubstitution success = new Unification.SuccessfulSubstitution(substitution); for (Node var : getVars(find(z))) { if (var != z) { - success.addBinding(var, z.is(Node.Kind.REF) ? z.get() : z); + Node val = z.is(Node.Kind.REF) ? z.get() : z; + + // Keep the order of variables within a binding + if (val.is(Node.Kind.VAR) && val.compareTo(var) < 0) { + success.addBinding(val, var); + } + else { + success.addBinding(var, val); + } } } diff --git a/reactor/code/src/jetbrains/mps/unification/Var.java b/reactor/code/src/jetbrains/mps/unification/Var.java deleted file mode 100644 index 729f76f0..00000000 --- a/reactor/code/src/jetbrains/mps/unification/Var.java +++ /dev/null @@ -1,33 +0,0 @@ -/* - * Copyright 2014 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; - -/** - * A variable node. Has a name and must implement {@link java.lang.Comparable}. - * - * @deprecated soon to be removed - * @author Fedor Isakov - */ -@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 index eaea6dae..1ff68c20 100644 --- a/reactor/tests/src/jetbrains/mps/unification/test/AssertStructurallyEquivalent.java +++ b/reactor/tests/src/jetbrains/mps/unification/test/AssertStructurallyEquivalent.java @@ -57,10 +57,20 @@ public class AssertStructurallyEquivalent { }, 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(); + if (ref.get().is(Node.Kind.FUN)) { + Integer label = signature.getLabel(ref.get()); + assertNotNull("not found label for '"+ref.get() + "'", label); + signature.appendSignature("^").append(label); + return Collections.emptyList(); + } + else if (ref.get().is(Node.Kind.VAR)) { + signature.appendSignature("^").append(ref.get().symbol()); + return Collections.emptyList(); + } + else { + throw new UnsupportedOperationException(); + } + } }) ); diff --git a/reactor/tests/src/jetbrains/mps/unification/test/AssertUnification.java b/reactor/tests/src/jetbrains/mps/unification/test/AssertUnification.java index b5380ec2..3f9fc4b8 100644 --- a/reactor/tests/src/jetbrains/mps/unification/test/AssertUnification.java +++ b/reactor/tests/src/jetbrains/mps/unification/test/AssertUnification.java @@ -20,7 +20,6 @@ import jetbrains.mps.unification.Substitution; import static jetbrains.mps.unification.Substitution.*; import jetbrains.mps.unification.Unification; import jetbrains.mps.unification.Node; -import jetbrains.mps.unification.Var; import java.util.*; diff --git a/reactor/tests/src/jetbrains/mps/unification/test/MockNode.java b/reactor/tests/src/jetbrains/mps/unification/test/MockNode.java index 52ec28c9..284b8268 100644 --- a/reactor/tests/src/jetbrains/mps/unification/test/MockNode.java +++ b/reactor/tests/src/jetbrains/mps/unification/test/MockNode.java @@ -17,8 +17,6 @@ package jetbrains.mps.unification.test; import jetbrains.mps.unification.Node; -import jetbrains.mps.unification.Term; -import jetbrains.mps.unification.Var; import java.util.*; @@ -50,26 +48,6 @@ public abstract class MockNode implements Node { 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; @@ -142,18 +120,13 @@ public abstract class MockNode implements Node { } } - public static class MockVar extends MockNode implements Var { + public static class MockVar extends MockNode { private String myName; public MockVar(String name) { myName = name; } - @Override - public String name() { - return myName; - } - @Override public Object symbol() { return myName; diff --git a/reactor/tests/src/jetbrains/mps/unification/test/MockTreeParser.java b/reactor/tests/src/jetbrains/mps/unification/test/MockTreeParser.java index fea21202..90bd80fa 100644 --- a/reactor/tests/src/jetbrains/mps/unification/test/MockTreeParser.java +++ b/reactor/tests/src/jetbrains/mps/unification/test/MockTreeParser.java @@ -17,8 +17,6 @@ package jetbrains.mps.unification.test; import jetbrains.mps.unification.Node; -import jetbrains.mps.unification.Node; -import jetbrains.mps.unification.Var; import java.util.*; import java.util.regex.Matcher; @@ -47,15 +45,15 @@ public class MockTreeParser { return (Node) parse(str); } - public static Var parseVar(String str) { - return (Var) parse(str); + public static Node parseVar(String str) { + return parse(str); } private static class RecursiveDescent { private Token lastToken; private LinkedList termsStack = new LinkedList(); - private LinkedList termsLabelsStack = new LinkedList(); + private LinkedList termLabelsStack = new LinkedList(); private LinkedList> childrenStack = new LinkedList>(); private int lastLabel = -1; private Map termRefs = new HashMap(); @@ -98,7 +96,7 @@ public class MockTreeParser { childrenStack.push(new ArrayList()); break; case END: - checkLastTokenOneOf(Token.TERM, Token.VAR, Token.RBRACE); + checkLastTokenOneOf(Token.TERM, Token.VAR, Token.VARREF, Token.RBRACE); if (lastToken == Token.TERM) { emptyTerm(); } @@ -116,12 +114,19 @@ public class MockTreeParser { } addVar(value); break; + case VARREF: + checkLastTokenNotOneOf(Token.LABEL); + if (lastToken == Token.TERM) { + emptyTerm(); + } + addVarRef(value.substring(1)); + break; case LBRACE: checkLastTokenOneOf(Token.TERM); beginChildren(); break; case RBRACE: - checkLastTokenOneOf(Token.TERM, Token.VAR, Token.REF, Token.RBRACE); + checkLastTokenOneOf(Token.TERM, Token.VAR, Token.VARREF, Token.REF, Token.RBRACE); if (lastToken == Token.TERM) { emptyTerm(); } @@ -187,13 +192,13 @@ public class MockTreeParser { private void beginTerm(String name) { termsStack.push(name); - termsLabelsStack.push(lastLabel >= 0 ? lastLabel : null); + termLabelsStack.push(lastLabel >= 0 ? lastLabel : null); lastLabel = -1; } private void emptyTerm() { String name = termsStack.pop(); - Integer label = termsLabelsStack.pop(); + Integer label = termLabelsStack.pop(); Node newTerm = term(name); childrenStack.peek().add(newTerm); if (label != null) { @@ -208,7 +213,7 @@ public class MockTreeParser { private void endChildren() { List children = childrenStack.pop(); String name = termsStack.pop(); - Integer label = termsLabelsStack.pop(); + Integer label = termLabelsStack.pop(); Node newTerm = term(name, children.toArray(new Node[children.size()])); childrenStack.peek().add(newTerm); if (label != null) { @@ -220,6 +225,10 @@ public class MockTreeParser { childrenStack.peek().add(var(name)); } + private void addVarRef(String name) { + childrenStack.peek().add(ref(var(name))); + } + private void addRef(String ref) { final int label = Integer.parseInt(ref.substring(1)); if (termRefs.containsKey(label)) { @@ -241,7 +250,8 @@ public class MockTreeParser { RBRACE(Pattern.compile("\\}")), WHITESPACE(Pattern.compile("\\s+")), LABEL(Pattern.compile("@[0-9]+")), - REF(Pattern.compile("\\^[0-9]+")); + REF(Pattern.compile("\\^[0-9]+")), + VARREF(Pattern.compile("\\^[A-Z][a-zA-Z0-9_]*")); private Pattern pattern; diff --git a/reactor/tests/src/jetbrains/mps/unification/test/ParserTests.java b/reactor/tests/src/jetbrains/mps/unification/test/ParserTests.java index 220ba106..3f4dbc66 100644 --- a/reactor/tests/src/jetbrains/mps/unification/test/ParserTests.java +++ b/reactor/tests/src/jetbrains/mps/unification/test/ParserTests.java @@ -95,23 +95,40 @@ public class ParserTests { public void testRef() throws Exception { LazyTermLookup termLookup = new LazyTermLookup(); Node a = termLookup.term = term("a", ref(termLookup)); - assertEquivalent(parse("@1a{^1}"), + assertEquivalent( + parse("@1a{^1}"), a); Node b = term("b"); - assertEquivalent(parse("a{@1b ^1}"), + assertEquivalent( + parse("a{@1b ^1}"), term("a", b, ref(b))); Node c = term("c"); - assertEquivalent(parse("a{^1 @1c}"), + 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}"), + assertEquivalent( + parse("a{@2b ^1 ^2 @1b}"), term("a", b2, ref(b1), ref(b2), b1)); } + @Test + public void testVarRef() throws Exception { + Node x = var("X"); + + assertEquivalent( + parse("^X"), + ref(x)); + assertEquivalent( + parse("a{^X}"), + term("a", ref(x))); + + } + @Test(expected = ComparisonFailure.class) public void testNotEquivalent1() throws Exception { Node d = term("d"); diff --git a/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java b/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java index fd258eff..094b2dc9 100644 --- a/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java +++ b/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java @@ -16,6 +16,7 @@ package jetbrains.mps.unification.test; +import jetbrains.mps.unification.Node; import org.junit.Test; import static jetbrains.mps.unification.test.MockNode.*; @@ -316,6 +317,42 @@ public class SolverTests { ); } + @Test + public void testVarRef() throws Exception { + + assertUnifiesWithBindings( + parse("^X"), + parse("Y"), + + bind(var("X"), var("Y")) + ); + assertUnifiesWithBindings( + parse("a{b ^X}"), + parse("a{b c{d}}"), + + bind(var("X"), parse("c{d}")) + ); + assertUnifiesWithBindings( + parse("a{b c{X} ^X}"), + parse("a{b c{d} d}"), + + bind(var("X"), parse("d")) + ); + assertUnifiesWithBindings( + parse("a{b{d} c{X} ^X}"), + parse("a{b{^X} c{d} d}"), + + bind(var("X"), parse("d")) + ); + assertUnifiesWithBindings( + parse("a{b{d} c{X}}"), + parse("a{b{^X} c{d}}"), + + bind(var("X"), parse("d")) + ); + + } + @Test public void testCyclic_TermRewriting() throws Exception { // The original problem is to unify two cyclic terms: