diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/OccurrenceMatcher.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/OccurrenceMatcher.kt index 968de7ca..b5d60fae 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/OccurrenceMatcher.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/OccurrenceMatcher.kt @@ -34,7 +34,7 @@ interface OccurrenceMatcher { fun matches(cst: Constraint, occ: ConstraintOccurrence): Boolean - fun match(left: Any?, right: Any?): Boolean + fun match(left: Any, right: Any): Boolean } diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/OccurrenceMatcherImpl.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/OccurrenceMatcherImpl.kt index 4189e7d9..6968fd9d 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/OccurrenceMatcherImpl.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/OccurrenceMatcherImpl.kt @@ -26,12 +26,24 @@ import jetbrains.mps.logic.reactor.logical.MetaLogical import jetbrains.mps.logic.reactor.program.Constraint import jetbrains.mps.logic.reactor.util.assoc import jetbrains.mps.unification.Term +import java.lang.NullPointerException internal class OccurrenceMatcherImpl(val contextSubst: Subst? = null) : OccurrenceMatcher { - private var matchSubst : Subst? = null + private companion object { + // to be used instead of null for resolved logical w/o value + val NO_VALUE = object {} + } - override fun subst(): Subst = matchSubst ?: (contextSubst ?: emptySubst()) + private var _matchSubst : Subst? = null + + private var matchSubst : Subst + get() = _matchSubst ?: if (contextSubst != null) contextSubst else emptySubst() + set(value) { + this._matchSubst = value + } + + override fun subst(): Subst = matchSubst /** * Matches constraint and occurrence. @@ -43,6 +55,8 @@ internal class OccurrenceMatcherImpl(val contextSubst: Subst? = null) : Occurren if (cst.symbol() != occ.constraint().symbol()) return false return zipWhileTrue(cst.arguments(), occ.arguments()) { cstarg, occarg -> + if (cstarg == null) throw NullPointerException("constraint argument can't be null") + if (occarg == null) return false ptnMatchAny(cstarg, occarg) } } @@ -50,7 +64,7 @@ internal class OccurrenceMatcherImpl(val contextSubst: Subst? = null) : Occurren /** * Returns true for matching left and right parameters, false otherwise. */ - override fun match(left: Any?, right: Any?): Boolean { + override fun match(left: Any, right: Any): Boolean { return matchAny(left, right) } @@ -58,20 +72,16 @@ internal class OccurrenceMatcherImpl(val contextSubst: Subst? = null) : Occurren * Matches target against pattern. * Recursively iterates terms. * Respects substitutions for MetaLogical instances. - * Returns either new substitution on successful match, or null. + * Returns true on successful match, otherwise false. */ - private fun ptnMatchAny(ptn: Any?, trg: Any?): Boolean = + private fun ptnMatchAny(ptn: Any, trg: Any): Boolean = when (ptn) { is MetaLogical<*> -> { // recursion with existing substitution or new substitution - if (matchSubst == null) { - this.matchSubst = if (contextSubst != null) contextSubst else emptySubst() - } - - if (matchSubst!!.containsKey(ptn)) - matchSubst!![ptn].let { matchAny(it, trg) } + if (matchSubst.containsKey(ptn)) + matchSubst[ptn]?.let { matchAny(it, trg) } ?: false else - matchSubst!!.assoc(ptn, trg!!).also { matchSubst = it }.run { true } + matchSubst.assoc(ptn, trg).also { this.matchSubst = it }.run { true } } is Term -> when { @@ -80,15 +90,14 @@ internal class OccurrenceMatcherImpl(val contextSubst: Subst? = null) : Occurren } else -> when { - trg is Logical<*> -> ptnMatchAny(ptn, resolve(trg)) - else -> - // compare two arbitrary values + trg is Logical<*> -> ptnMatchAny(ptn, resolve(trg)) + else -> // compare two arbitrary values (ptn == trg) } } - private fun matchAny(left: Any?, right: Any?): Boolean = + private fun matchAny(left: Any, right: Any): Boolean = when (left) { is Logical<*> -> // match logical or its value @@ -100,15 +109,13 @@ internal class OccurrenceMatcherImpl(val contextSubst: Subst? = null) : Occurren } else -> when { - right is Logical<*> -> matchAny(left, resolve(right)) + right is Logical<*> -> matchAny(left, resolve(right)) else -> // compare two arbitrary values (left == right) } } - private fun ptnMatchTerm(ptn: Term, trg: Any?): Boolean { - if (trg == null) return false - + private fun ptnMatchTerm(ptn: Term, trg: Any): Boolean { val trgval = resolve(trg) if (!(trgval is Term)) return false @@ -124,9 +131,7 @@ internal class OccurrenceMatcherImpl(val contextSubst: Subst? = null) : Occurren } } - private fun matchTerm(left: Term, right: Any?): Boolean { - if (right == null) return false - + private fun matchTerm(left: Term, right: Any): Boolean { val rval = resolve(right) if (!(rval is Term)) return false @@ -140,12 +145,11 @@ internal class OccurrenceMatcherImpl(val contextSubst: Subst? = null) : Occurren } } - private fun matchLogical(left: Logical<*>, right: Any?): Boolean = + private fun matchLogical(left: Logical<*>, right: Any): Boolean = when { right is Logical<*> -> when { - left.isBound -> matchAny(left.findRoot().value(), - right.findRoot().value()) + left.isBound -> matchAny(left.findRoot().value(), resolve(right)) left.findRoot() === right.findRoot() -> true // reference equality else -> false } @@ -153,11 +157,11 @@ internal class OccurrenceMatcherImpl(val contextSubst: Subst? = null) : Occurren else -> false } - private fun resolve(obj: Any?): Any? = + private fun resolve(obj: Any): Any = when (obj) { is LogicalOwner -> if (obj.logical().isBound) resolve(obj.logical()) else obj - is Logical<*> -> resolve(obj.findRoot().value()) - is Term -> if (obj.`is`(Term.Kind.REF)) resolve(obj.get()) else obj + is Logical<*> -> if (obj.isBound) resolve(obj.findRoot().value()) else NO_VALUE + is Term -> if (obj.`is`(Term.Kind.REF)) resolve(obj.get()) else obj else -> obj } diff --git a/reactor/Core/src/jetbrains/mps/unification/Term.java b/reactor/Core/src/jetbrains/mps/unification/Term.java index 931a299e..340689c6 100644 --- a/reactor/Core/src/jetbrains/mps/unification/Term.java +++ b/reactor/Core/src/jetbrains/mps/unification/Term.java @@ -16,6 +16,8 @@ package jetbrains.mps.unification; +import org.jetbrains.annotations.NotNull; + import java.util.Collection; /** @@ -32,9 +34,11 @@ public interface Term extends Comparable { /** * A symbol corresponding to the function/constant name or the variable name. + * Must not be null. * TODO: what is the meaning of symbol in case of a reference term? * NOTE: two variable terms are treated as the same term if their symbols match. */ + @NotNull Object symbol(); /** diff --git a/reactor/Test/src/jetbrains/mps/unification/test/MockTerm.java b/reactor/Test/src/jetbrains/mps/unification/test/MockTerm.java index 681e4530..44d1c73d 100644 --- a/reactor/Test/src/jetbrains/mps/unification/test/MockTerm.java +++ b/reactor/Test/src/jetbrains/mps/unification/test/MockTerm.java @@ -19,6 +19,7 @@ package jetbrains.mps.unification.test; import jetbrains.mps.logic.reactor.logical.Logical; import jetbrains.mps.logic.reactor.logical.LogicalOwner; import jetbrains.mps.unification.Term; +import org.jetbrains.annotations.NotNull; import java.util.Arrays; import java.util.Collection; @@ -61,6 +62,7 @@ public abstract class MockTerm implements Term { Term lookupTerm(); } + @NotNull @Override public Object symbol() { return null; @@ -90,6 +92,7 @@ public abstract class MockTerm implements Term { this.myArgs = Arrays.asList(arguments); } + @NotNull @Override public Object symbol() { return mySymbol; @@ -140,6 +143,7 @@ public abstract class MockTerm implements Term { myName = name; } + @NotNull @Override public Object symbol() { return myName; @@ -174,6 +178,7 @@ public abstract class MockTerm implements Term { this.mySymbol = symbol; } + @NotNull @Override public Object symbol() { return mySymbol; @@ -212,6 +217,7 @@ public abstract class MockTerm implements Term { return myLogical; } + @NotNull @Override public Object symbol() { return myLogical; @@ -266,6 +272,7 @@ public abstract class MockTerm implements Term { this.termLookup = termLookup; } + @NotNull @Override public Object symbol() { return "^"; diff --git a/reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java b/reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java index 685ea827..01d4b750 100644 --- a/reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java +++ b/reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java @@ -414,6 +414,7 @@ public class SolverTests { this.wrapped = term; } + @NotNull @Override public Object symbol() { return wrapped;