Introduced unification of cyclic terms, redesigned the algorithm, refactored the API, wrote a bunch of tests
This commit is contained in:
Fedor Isakov
parent
83eb1ca827
commit
28387e683b
|
|
@ -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<Node> {
|
||||
|
||||
@Deprecated
|
||||
boolean isTerm();
|
||||
|
||||
@Deprecated
|
||||
Term asTerm();
|
||||
|
||||
@Deprecated
|
||||
boolean isVar();
|
||||
|
||||
@Deprecated
|
||||
Var asVar();
|
||||
|
||||
Object symbol();
|
||||
|
||||
Collection<? extends Node> children();
|
||||
|
||||
Node get();
|
||||
|
||||
boolean is(Kind kind);
|
||||
|
||||
enum Kind {
|
||||
FUN,
|
||||
VAR,
|
||||
REF
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -32,15 +32,15 @@ public interface Substitution {
|
|||
Collection<Binding> 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;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -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.<sup>1</sup> No recursive terms are allowed, meaning the "occurrs check"
|
||||
* is performed on the input. If successful, the returned {@link Substitution} contains
|
||||
* the variable bindings.
|
||||
* <p/>
|
||||
* The variables are sorted using {@link java.lang.Comparable} to ensure uniqueness of bindings
|
||||
* whereas the substituted term is also a variable.
|
||||
* <p/>
|
||||
* <blockquote>
|
||||
* 1. <i>Baader, Franz, and Wayne Snyder. "Unification Theory." Handbook of automated reasoning 1 (2001): 445-532.</i>
|
||||
* </blockquote>
|
||||
* 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<Object, Data> myData = new HashMap<Object, Data>();
|
||||
|
||||
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<? extends Node> scit = zs.asTerm().children().iterator();
|
||||
Iterator<? extends Node> 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<Node> path = new ArrayList<Node>();
|
||||
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<Var> getVars(Node n) {
|
||||
if (!hasData(n)) {
|
||||
return n.isTerm() ? Collections.<Var>emptyList() : Collections.singletonList(n.asVar());
|
||||
}
|
||||
return getData(n).myVars;
|
||||
}
|
||||
|
||||
private void appendVars(Node n, List<Var> vars) {
|
||||
List<Var> newVars = new ArrayList<Var>(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<Var> myVars;
|
||||
|
||||
Node myClass;
|
||||
Node mySchema;
|
||||
Data(Node n) {
|
||||
myClass = n;
|
||||
mySchema = n;
|
||||
myVars = n.isTerm() ? Collections.<Var>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<Binding> myBindings;
|
||||
|
||||
private SuccessfulSubstitution(Substitution substitution) {
|
||||
protected SuccessfulSubstitution(Substitution substitution) {
|
||||
this.myBindings = new LinkedList<Binding>(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);
|
||||
|
|
|
|||
|
|
@ -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.<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 bindind variables to cyclic terms.
|
||||
*
|
||||
* If successful, the returned {@link Substitution} contains
|
||||
* the variable bindings.
|
||||
* <p/>
|
||||
* The variables are sorted using {@link java.lang.Comparable} to ensure uniqueness of bindings
|
||||
* whereas the substituted term is also a variable.
|
||||
* <p/>
|
||||
* <blockquote>
|
||||
* 1. <i>Baader, Franz, and Wayne Snyder. "Unification Theory." Handbook of automated reasoning 1 (2001): 445-532.</i>
|
||||
* 2. <i>Baader, Franz, and Tobias Nipkow. Term rewriting and all that. Cambridge University Press, 1999.</i>
|
||||
* </blockquote>
|
||||
*
|
||||
* @author Fedor Isakov
|
||||
*/
|
||||
public class UnionFindTermGraphUnifier {
|
||||
|
||||
private Map<Object, Data> myData = new HashMap<Object, Data>();
|
||||
|
||||
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<? extends Node> scit = zs.children().iterator();
|
||||
Iterator<? extends Node> 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<Node> path = new ArrayList<Node>();
|
||||
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<Var> getVars(Node n) {
|
||||
if (!hasData(n)) {
|
||||
return n.is(Node.Kind.VAR) ? Collections.singletonList((Var)n) : Collections.<Var>emptyList();
|
||||
}
|
||||
return getData(n).myVars;
|
||||
}
|
||||
|
||||
private void appendVars(Node n, List<Var> vars) {
|
||||
List<Var> newVars = new ArrayList<Var>(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<Var> myVars;
|
||||
|
||||
Node myClass;
|
||||
Node mySchema;
|
||||
Data(Node n) {
|
||||
myClass = n;
|
||||
mySchema = n;
|
||||
myVars = n.is(Node.Kind.VAR) ? Collections.singletonList((Var)n) : Collections.<Var>emptyList();
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -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<Var> {
|
||||
@Deprecated
|
||||
public interface Var extends Node {
|
||||
|
||||
Object symbol();
|
||||
|
||||
@Deprecated
|
||||
String name();
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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>(Node.Kind.FUN) {
|
||||
@Override
|
||||
public Collection<? extends Node> visit(Node term) throws Exception {
|
||||
signature.label(term);
|
||||
return term.children();
|
||||
}
|
||||
}),
|
||||
// second pass
|
||||
new NodeWalker(
|
||||
new NodeVisitor<Node>(Node.Kind.FUN) {
|
||||
@Override
|
||||
public Collection<? extends Node> visit(Node term) throws Exception {
|
||||
signature.appendSignature("@").append(signature.getLabel(term)).append(term.symbol());
|
||||
return term.children();
|
||||
}
|
||||
},
|
||||
new NodeVisitor<Node>(Node.Kind.VAR) {
|
||||
@Override
|
||||
public Collection<? extends Node> visit(Node var) throws Exception {
|
||||
signature.appendSignature("$").append(var.symbol());
|
||||
return Collections.emptyList();
|
||||
}
|
||||
}, 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();
|
||||
}
|
||||
})
|
||||
);
|
||||
|
||||
String signa = signature.getSignature(a);
|
||||
String signb = signature.getSignature(b);
|
||||
|
||||
assertEquals(signa, signb);
|
||||
}
|
||||
|
||||
|
||||
private static class Signature {
|
||||
|
||||
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++);
|
||||
}
|
||||
|
||||
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 <T extends Node> {
|
||||
|
||||
private Node.Kind kind;
|
||||
|
||||
public NodeVisitor(Node.Kind kind) {
|
||||
this.kind = kind;
|
||||
}
|
||||
|
||||
public Node.Kind applicableTo() {
|
||||
return kind;
|
||||
}
|
||||
|
||||
public abstract Collection<? extends Node> visit(T t) throws Exception ;
|
||||
|
||||
}
|
||||
|
||||
private static class NodeWalker {
|
||||
|
||||
private Map<Node.Kind, NodeVisitor<? extends Node>> visitorMap = new HashMap<Node.Kind, NodeVisitor<? extends Node>>();
|
||||
|
||||
public NodeWalker(NodeVisitor<? extends Node>... visitors) {
|
||||
for (NodeVisitor<? extends Node> visitor : visitors) {
|
||||
visitorMap.put(visitor.applicableTo(), visitor);
|
||||
}
|
||||
}
|
||||
|
||||
public void walk(Node node) throws Exception {
|
||||
Collection<? extends Node> children = switchClass(node);
|
||||
for (Node child : children) {
|
||||
walk(child);
|
||||
}
|
||||
}
|
||||
|
||||
private Collection<? extends Node> switchClass(Node node) throws Exception {
|
||||
for (Map.Entry<Node.Kind, NodeVisitor<? extends Node>> e : visitorMap.entrySet()) {
|
||||
if (node.is(e.getKey())) {
|
||||
NodeVisitor<Node> value = (NodeVisitor<Node>) e.getValue();
|
||||
return value.visit(node);
|
||||
}
|
||||
}
|
||||
return Collections.emptyList();
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -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> BINDING_COMPARATOR = new Comparator<Binding>() {
|
||||
@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<Binding> expected, Collection<Binding> actual) throws Exception {
|
||||
Iterator<Binding> expIt = expected.iterator();
|
||||
Iterator<Binding> actIt = actual.iterator();
|
||||
|
||||
Map<Var, Node> expMap = new HashMap<Var, Node>();
|
||||
Map<Var, Node> actMap = new HashMap<Var, Node>();
|
||||
ArrayList<Binding> expectedCopy = new ArrayList<Binding>(expected);
|
||||
Collections.sort(expectedCopy, BINDING_COMPARATOR);
|
||||
Iterator<Binding> expIt = expectedCopy.iterator();
|
||||
ArrayList<Binding> actualCopy = new ArrayList<Binding>(actual);
|
||||
Collections.sort(actualCopy, BINDING_COMPARATOR);
|
||||
Iterator<Binding> 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());
|
||||
|
|
|
|||
|
|
@ -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<? extends Node> 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<Node> 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() : "^<NULL>";
|
||||
}
|
||||
|
||||
@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;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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<String> termsStack = new LinkedList<String>();
|
||||
private LinkedList<Integer> termsLabelsStack = 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>();
|
||||
// initialized on the parse finished
|
||||
private LookupHelper lookupHelper = new LookupHelper();
|
||||
|
||||
private List<Node> parse(String toParse) {
|
||||
parseNextToken(Token.START, null);
|
||||
loop(toParse);
|
||||
parseNextToken(Token.END, null);
|
||||
checkFinalState();
|
||||
checkAllRefsExist();
|
||||
lookupHelper.setTermRefs(Collections.unmodifiableMap(new HashMap<Integer, Node>(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<Integer, Node> 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<Node> 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<Integer, Node> termRefs;
|
||||
|
||||
private void setTermRefs (Map<Integer, Node> 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);
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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}");
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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}")
|
||||
);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue