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

Reporting the cause of failed unification, some code cleanup

This commit is contained in:
Fedor Isakov 2015-03-24 16:20:40 +01:00
parent 80d16b592d
commit 41077453e8
5 changed files with 115 additions and 56 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

51
reactor/code/src/jetbrains/mps/unification/Substitution.java
View File

@ -25,13 +25,38 @@ import java.util.Collections;
*
* @author Fedor Isakov
*/
public interface Substitution {
public class Substitution {
boolean isSuccessful();
private boolean mySuccessful;
Collection<Binding> bindings() ;
private FailureCause myFailureCause;
public class Binding {
public Substitution(boolean successful) {
mySuccessful = successful;
}
public Substitution(FailureCause failCause) {
myFailureCause = failCause;
mySuccessful = false;
}
public boolean isSuccessful() {
return mySuccessful;
}
public Collection<Binding> bindings() {
return Collections.emptyList();
}
public FailureCause failureCause() {
return myFailureCause;
}
public String toString() {
return myFailureCause != null ? "[" + myFailureCause + "]" : "[FAILED_SUBSTITUTION]";
}
public static class Binding {
private Node myVar;
private Node myNode;
@ -49,4 +74,22 @@ public interface Substitution {
}
}
public enum FailureCause {
CYCLE_DETECTED("cycle detected"),
UNRECONCILED_REF("unreconciled ref"),
SYMBOL_CLASH("symbol clash"),
UKNOWN("uknown");
private String myMessage;
FailureCause(String message) {
myMessage = message;
}
@Override
public String toString() {
return myMessage;
}
}
}

49
reactor/code/src/jetbrains/mps/unification/Unification.java
View File

@ -16,6 +16,8 @@
package jetbrains.mps.unification;
import jetbrains.mps.unification.Substitution.FailureCause;
import java.util.*;
/**
@ -32,53 +34,33 @@ public class Unification {
return dagUnifier.unify(a, b);
}
protected static final Substitution FAILED_SUBSTITUTION = new Substitution() {
@Override
public boolean isSuccessful() {
return false;
}
@Override
public Collection<Binding> bindings() {
return Collections.emptyList();
}
@Override
public String toString() {
return "[FAILED_SUBSTITUTION]";
}
};
protected static final Substitution EMPTY_SUBSTITUTION = new Substitution() {
@Override
public boolean isSuccessful() {
return true;
}
@Override
public Collection<Binding> bindings() {
return Collections.emptyList();
}
protected static Substitution failedSubstitution(FailureCause failCause) {
return new Substitution(failCause);
}
protected static final Substitution EMPTY_SUBSTITUTION = new Substitution(true) {
@Override
public String toString() {
return "[]";
}
};
protected static class SuccessfulSubstitution implements Substitution {
protected static final Substitution FAILED_SUBSTITUTION = new Substitution(FailureCause.UKNOWN) {
@Override
public String toString() {
return "[FAILED_SUBSTITUTION]";
}
};
protected static class SuccessfulSubstitution extends Substitution {
private LinkedList<Binding> myBindings;
protected SuccessfulSubstitution(Substitution substitution) {
super(true);
this.myBindings = new LinkedList<Binding>(substitution.bindings());
}
@Override
public boolean isSuccessful() {
return true;
}
@Override
public Collection<Binding> bindings() {
return Collections.unmodifiableCollection(myBindings);
@ -108,5 +90,4 @@ public class Unification {
}
}
}

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

@ -16,11 +16,13 @@
package jetbrains.mps.unification;
import jetbrains.mps.unification.Substitution.FailureCause;
import jetbrains.mps.unification.Unification.SuccessfulSubstitution;
import java.util.*;
import static jetbrains.mps.unification.Node.Kind.*;
import static jetbrains.mps.unification.Substitution.FailureCause.*;
import static jetbrains.mps.unification.Unification.*;
/**
@ -51,9 +53,11 @@ public class UnionFindTermGraphUnifier {
private int myUnreconciledRefs = 0;
private FailureCause myFailureCause = UKNOWN;
public Substitution unify(Node a, Node b) {
if (!unifClosure(a, b)) {
return FAILED_SUBSTITUTION;
return failedSubstitution(myFailureCause);
}
return findSolution(a);
@ -108,6 +112,7 @@ public class UnionFindTermGraphUnifier {
if (zs.is(FUN) && zt.is(FUN))
{
if (!eq(zs.symbol(), zt.symbol())) {
myFailureCause = SYMBOL_CLASH;
return false; // symbol clash
}
@ -119,7 +124,9 @@ public class UnionFindTermGraphUnifier {
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;
if (!unifClosure(scit.next(), tcit.next())) {
return false; // children mismatch
}
}
// fail if different children count
@ -127,7 +134,7 @@ public class UnionFindTermGraphUnifier {
}
else {
// something's wrong with the input
return false;
throw new IllegalStateException("invalid input");
}
}
@ -194,7 +201,7 @@ public class UnionFindTermGraphUnifier {
return substitution; // not part of a cycle
}
if (isVisited(z)) {
return FAILED_SUBSTITUTION; // there exists a cycle
return failedSubstitution(CYCLE_DETECTED); // there exists a cycle
}
int unreconciled = myUnreconciledRefs;
@ -227,7 +234,7 @@ public class UnionFindTermGraphUnifier {
for (Node var : getVars(find(z))) {
if (var != z) {
if (myUnreconciledRefs != unreconciled) {
return FAILED_SUBSTITUTION; // there's an unreconciled outward reference
return failedSubstitution(UNRECONCILED_REF); // there's an unreconciled outward reference
}
Node val = z.is(REF) ? z.get() : z;

7
reactor/tests/src/jetbrains/mps/unification/test/AssertUnification.java
View File

@ -94,4 +94,11 @@ public class AssertUnification {
assertFalse(subs.isSuccessful());
}
public static void assertUnificationFails(Node s, Node t, FailureCause failureCause) throws Exception {
Substitution subs = Unification.unify(s, t);
assertFalse(subs.isSuccessful());
assertSame(failureCause, subs.failureCause());
}
}

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

@ -16,12 +16,13 @@
package jetbrains.mps.unification.test;
import jetbrains.mps.unification.Node;
import org.junit.Test;
import static jetbrains.mps.unification.test.MockNode.*;
import static jetbrains.mps.unification.test.MockTreeParser.*;
import static jetbrains.mps.unification.Substitution.FailureCause.*;
import static jetbrains.mps.unification.test.AssertUnification.*;
import static jetbrains.mps.unification.test.MockNode.term;
import static jetbrains.mps.unification.test.MockNode.var;
import static jetbrains.mps.unification.test.MockTreeParser.*;
/**
* Created by fyodor on 09.06.2014.
@ -315,6 +316,13 @@ public class SolverTests {
bind(var("X"), parse("@1 a{b ^1}"))
);
assertUnifiesWithBindings(
parse("a{X c{X} }"),
parse("a{b{Y} c{@1 b{@2 c{b{^2}}}}}"),
bind(var("X"), parse("b{Y}")),
bind(var("Y"), parse("@1 c{b{^1}}"))
);
}
@Test
@ -385,15 +393,15 @@ public class SolverTests {
public void testFailConflict() throws Exception {
assertUnificationFails(
term("a"),
term("b")
term("b"),
SYMBOL_CLASH
);
assertUnificationFails(
parse("node{name{X} child{abc}}"),
parse("node{name{foo} child{X}}")
);
assertUnificationFails(
parse("f{a{X} Y }"),
parse("f{Y a{b{X}}}")
parse("node{name{foo} child{X}}"),
SYMBOL_CLASH
);
}
@ -409,20 +417,33 @@ public class SolverTests {
public void testFailRecursive() throws Exception {
assertUnificationFails(
parse("f{X}"),
parse("X")
parse("X"),
CYCLE_DETECTED
);
assertUnificationFails(
parse("f{f{X}}"),
parse("f{X}")
parse("f{X}"),
CYCLE_DETECTED
);
assertUnificationFails(
parse("f{a{X} Y }"),
parse("f{Y a{b{X}}}"),
CYCLE_DETECTED
);
assertUnificationFails(
parse("a{X c{X}}"),
parse("a{b{Y} Y }")
parse("a{b{Y} Y }"),
CYCLE_DETECTED
);
assertUnificationFails (
parse("a{@1 b{c{^1}} @2 c{b{^2}}}"),
parse("a{ b{Y} Y }")
parse("a{ b{Y} Y }"),
UNRECONCILED_REF
);
}
}