Now allowing REF nodes to point to variables too, adapted the algorithm, removed obsolete interfaces, created more tests
This commit is contained in:
Fedor Isakov
parent
09e0fd00b7
commit
004480ca70
|
|
@ -24,5 +24,4 @@
|
|||
<component name="ProjectRootManager" version="2" languageLevel="JDK_1_6" assert-keyword="true" jdk-15="true" project-jdk-name="1.6" project-jdk-type="JavaSDK">
|
||||
<output url="file://$PROJECT_DIR$/out" />
|
||||
</component>
|
||||
</project>
|
||||
|
||||
</project>
|
||||
|
|
@ -8,5 +8,4 @@
|
|||
<orderEntry type="inheritedJdk" />
|
||||
<orderEntry type="sourceFolder" forTests="false" />
|
||||
</component>
|
||||
</module>
|
||||
|
||||
</module>
|
||||
|
|
@ -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<Node> {
|
||||
|
||||
@Deprecated
|
||||
boolean isTerm();
|
||||
|
||||
@Deprecated
|
||||
Term asTerm();
|
||||
|
||||
@Deprecated
|
||||
boolean isVar();
|
||||
|
||||
@Deprecated
|
||||
Var asVar();
|
||||
|
||||
Object symbol();
|
||||
|
||||
Collection<? extends Node> children();
|
||||
|
|
|
|||
|
|
@ -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<? extends Node> children();
|
||||
|
||||
}
|
||||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
||||
}
|
||||
|
|
@ -57,10 +57,20 @@ public class AssertStructurallyEquivalent {
|
|||
}, new NodeVisitor<Node>(Node.Kind.REF) {
|
||||
@Override
|
||||
public Collection<? extends Node> 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();
|
||||
}
|
||||
|
||||
}
|
||||
})
|
||||
);
|
||||
|
|
|
|||
|
|
@ -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.*;
|
||||
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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<String> termsStack = new LinkedList<String>();
|
||||
private LinkedList<Integer> termsLabelsStack = new LinkedList<Integer>();
|
||||
private LinkedList<Integer> termLabelsStack = new LinkedList<Integer>();
|
||||
private LinkedList<List<Node>> childrenStack = new LinkedList<List<Node>>();
|
||||
private int lastLabel = -1;
|
||||
private Map<Integer, Node> termRefs = new HashMap<Integer, Node>();
|
||||
|
|
@ -98,7 +96,7 @@ public class MockTreeParser {
|
|||
childrenStack.push(new ArrayList<Node>());
|
||||
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<Node> 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;
|
||||
|
||||
|
|
|
|||
|
|
@ -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");
|
||||
|
|
|
|||
|
|
@ -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:
|
||||
|
|
|
|||
Loading…
Reference in New Issue