diff --git a/reactor/API/src/jetbrains/mps/logic/reactor/evaluation/MatchRule.java b/reactor/API/src/jetbrains/mps/logic/reactor/evaluation/MatchRule.java index deacffb1..0d94ac37 100644 --- a/reactor/API/src/jetbrains/mps/logic/reactor/evaluation/MatchRule.java +++ b/reactor/API/src/jetbrains/mps/logic/reactor/evaluation/MatchRule.java @@ -17,6 +17,7 @@ package jetbrains.mps.logic.reactor.evaluation; +import jetbrains.mps.logic.reactor.logical.LogicalContext; import jetbrains.mps.logic.reactor.program.Rule; /** @@ -32,4 +33,5 @@ public interface MatchRule { Iterable matchHeadReplaced(); + LogicalContext logicalContext(); } diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Dispatcher.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Dispatcher.kt new file mode 100644 index 00000000..049bdc6a --- /dev/null +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Dispatcher.kt @@ -0,0 +1,85 @@ +/* + * Copyright 2014-2018 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.logic.reactor.core + +import com.github.andrewoma.dexx.collection.Maps +import com.github.andrewoma.dexx.collection.Map as PersMap +import jetbrains.mps.logic.reactor.evaluation.ConstraintOccurrence +import jetbrains.mps.logic.reactor.evaluation.MatchRule +import jetbrains.mps.logic.reactor.program.Rule + +/** + * @author Fedor Isakov + */ + +class Dispatcher (val ruleIndex: RuleIndex) { + + private val rule2matcher = HashMap() + + init { + ruleIndex.forEach { rule -> + val matcher = RuleMatcher(rule) + rule2matcher.put(rule, matcher); + } + } + + inner class DispatchFringe { + + private var rule2fringe: PersMap + + val allMatches = arrayListOf() + + constructor() { + this.rule2fringe = Maps.of() + rule2matcher.entries.forEach { e -> + this.rule2fringe = rule2fringe.put(e.key, e.value.fringe()) + } + } + + constructor(pred: DispatchFringe, matching: Iterable) { + this.rule2fringe = pred.rule2fringe + matching.forEach { fringe -> + this.rule2fringe = rule2fringe.put(fringe.rule(), fringe) + allMatches.addAll(fringe.matches()) + } + } + + fun matches() : Iterable = allMatches + + fun activated(active: ConstraintOccurrence): DispatchFringe { + return DispatchFringe(this, + ruleIndex.forOccurrence(active).mapNotNull { rule -> + rule2fringe[rule] + }.map { fringe -> + fringe.expand(active) + }) + } + + fun discarded(discarded: ConstraintOccurrence): DispatchFringe { + return DispatchFringe(this, + ruleIndex.forOccurrence(discarded).mapNotNull { rule -> + rule2fringe[rule] + }.map { fringe -> + fringe.cleanup(discarded) + }) + } + + } + + fun fringe() = DispatchFringe() + +} \ No newline at end of file diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Matcher.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Matcher.kt index 2a19661e..cea8d2c9 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Matcher.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Matcher.kt @@ -113,6 +113,7 @@ class Match(val rule: Rule, override fun matchHeadReplaced(): Iterable = discardedOccurrences + override fun logicalContext(): LogicalContext = logicalContext } /** Function term with arguments == constraints converted to terms. May contain variables. */ diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/RuleIndex.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/RuleIndex.kt index cdb01fbf..f362a08c 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/RuleIndex.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/RuleIndex.kt @@ -30,7 +30,7 @@ import java.util.* * @author Fedor Isakov */ -class RuleIndex : Iterable { +class RuleIndex(handlers: Iterable) : Iterable { private val primarySymbol2valueIndex = HashMap() @@ -38,7 +38,7 @@ class RuleIndex : Iterable { private val tag2rule = LinkedHashMap() - constructor(handlers: Iterable) { + init { for (h in handlers) { for (r in h.rules()) { tag2rule[r.tag()] = r @@ -68,7 +68,7 @@ class RuleIndex : Iterable { val symbol = c.symbol() if (symbol in primSymbols) { primarySymbol2valueIndex[symbol]?.update(r, c) - + } else { auxSymbol2valueIndex.getOrPut(symbol) { ValueIndex(symbol) }.update(r, c) } diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/RuleMatcher.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/RuleMatcher.kt new file mode 100644 index 00000000..e71b8917 --- /dev/null +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/RuleMatcher.kt @@ -0,0 +1,277 @@ +/* + * Copyright 2014-2018 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.logic.reactor.core + +import com.github.andrewoma.dexx.collection.Map as PersMap +import com.github.andrewoma.dexx.collection.List as PersList +import com.github.andrewoma.dexx.collection.ConsList +import com.github.andrewoma.dexx.collection.Maps +import com.github.andrewoma.dexx.collection.Vector as PersVector +import jetbrains.mps.logic.reactor.evaluation.ConstraintOccurrence +import jetbrains.mps.logic.reactor.evaluation.MatchRule +import jetbrains.mps.logic.reactor.logical.Logical +import jetbrains.mps.logic.reactor.logical.LogicalContext +import jetbrains.mps.logic.reactor.logical.LogicalOwner +import jetbrains.mps.logic.reactor.logical.MetaLogical +import jetbrains.mps.logic.reactor.program.Constraint +import jetbrains.mps.logic.reactor.program.Rule +import jetbrains.mps.logic.reactor.util.* +import jetbrains.mps.unification.Term +import java.util.* + +/** + * @author Fedor Isakov + */ + +private typealias Subst = PersMap, Any> + +private fun emptySubst() = Maps.of, Any>() + + +class RuleMatcher(val rule: Rule) { + + val head = rule.headKept().toCollection(ArrayList(4)).also { it.addAll(rule.headReplaced()) } + + val propagation = rule.headReplaced().count() == 0 + + fun fringe() = MatchFringe(cons(FringeNode(emptySubst())), emptySet(), 0) + + inner class MatchFringe(val nodes: ConsList, + val seen: IdHashSet, + val genId: Int) { + + fun rule(): Rule = rule + + fun matches(): Collection = + nodes.filter { rn -> + rn is ActiveFringeNode && rn.complete && rn.genId == genId }.map { rn -> + (rn as ActiveFringeNode).toMatchRule() } + + fun expand(occ: ConstraintOccurrence): MatchFringe { + if (seen.contains(occ)) { + // constraint occurrence is reactivated + // there are nodes having occ in their paths + // select complete (leaf) nodes and make them appear as if newly expanded + // *unless* propagation (implement propagation history feature) + if (propagation) return MatchFringe(nodes, seen, genId + 1) + + val newNodes = nodes.asSequence().mapNotNull { fn -> + if (fn is ActiveFringeNode && fn.complete) + fn.unrelatedOrCopy(occ, genId + 1) + else + fn + }.appendAllTo(emptyConsList()) + return MatchFringe(newNodes, seen, genId + 1) + + } else { + val newNodes = nodes.asSequence().flatMap { it.expand(occ, genId + 1) } + return MatchFringe(newNodes.appendAllTo(nodes), seen.add(occ), genId + 1) + } + } + + fun cleanup(occ: ConstraintOccurrence): MatchFringe { + val newNodes = nodes.asSequence().mapNotNull { it.unrelatedOrNull(occ) } + return MatchFringe(newNodes.toConsList(), seen.remove(occ), genId + 1) + } + } + + open inner class FringeNode(val subst: Subst, + val vacant: BitSet = bitSetOfOnes(head.size)) + { + /** + * Returns the additional nodes built from this node on adding the occurrence. + * If the occurrence is already in the path, return empty sequence. + */ + fun expand(occ: ConstraintOccurrence, genId: Int): Sequence { + val fringeNode = unrelatedOrNull(occ) + if (fringeNode == null) return emptySequence() + + return fringeNode.vacant.allSetBits().map { idx -> + idx to match(head[idx] !!, occ, subst) }.asSequence().mapNotNull { (idx, newSubst) -> + newSubst?.let { ActiveFringeNode(this, occ, idx, genId, it) } + } + } + + /** + * Returns this node if it doesn't have the occurrence in its path, null otherwise. + */ + open fun unrelatedOrNull(occ: ConstraintOccurrence): FringeNode? = this + + /** + * Matches constraint and occurrence. + * Recursively processes all arguments, including terms. + * Returns substitution of MetaLogical instances on success, null otherwise. + */ + protected fun match(cst: Constraint, + occ: ConstraintOccurrence, + subst: Subst): Subst? + { + if (cst.symbol() != occ.constraint().symbol()) return null + + var itsubst = subst + for ((cstarg, occarg) in cst.arguments().zip(occ.arguments())) { + itsubst = matchAny(cstarg, occarg, itsubst) ?: return null + } + + return itsubst + } + + /** + * Matches target against pattern. + * Recursively iterates terms. + * Respects substitutions for MetaLogical instances. + * Returns either new substitution on successful match, or null. + */ + private fun matchAny(ptn: Any?, + trg: Any?, + subst: Subst): Subst? = + when (ptn) { + is MetaLogical<*> -> + // recursion with existing substitution or new substitution + if (subst.containsKey(ptn)) subst[ptn].let { matchAny(it, trg, subst) } else subst.put(ptn, trg) + is Logical<*> -> + // match logical or its value + matchLogical(ptn.findRoot(), trg, subst) + is Term -> + // recursion into the term + matchTerm(ptn, trg, subst) + else -> + // compare two arbitrary values + if (ptn == trg) subst else null + } + + private fun matchTerm(ptn: Term, + trg: Any?, + subst: Subst): Subst? + { + if (trg == null) return null + + val trgval = resolve(trg) + if (!(trgval is Term)) return null + + if (ptn.`is`(Term.Kind.VAR)) return matchAny(ptn.get().symbol(), trgval, subst) + + var itsubst = matchAny(ptn.get().symbol(), trgval.symbol(), subst) ?: return null + for ((ptnarg, trgarg) in ptn.get().arguments().zip(trgval.arguments())) { + itsubst = matchAny (ptnarg, trgarg, itsubst) ?: return null + } + + return itsubst + } + + private fun matchLogical(ptn: Logical<*>, + trg: Any?, + subst: Subst): Subst? = + if (ptn.isBound) { + if (trg is Logical<*>) matchAny(ptn.value(), trg.findRoot().value(), subst) else null + + } else { + if (trg is Logical<*> && ptn === trg.findRoot()) subst else null // reference equality! + } + + 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 + else -> obj + } + + /** + * Folds the path to the root. + */ + inline protected fun fold(init: T, action: (T, ActiveFringeNode) -> T): T { + var rn = this + var curr = init + while (rn is ActiveFringeNode) { + curr = action(curr, rn) + rn = rn.parent + } + return curr + } + + /** + * Folds the path to the root. If an iteration yields null, fold is stopped and null is returned. + */ + inline protected fun foldUntilNull(init: T, action: (T?, ActiveFringeNode) -> T?): T? { + var rn = this + var curr: T? = init + while (rn is ActiveFringeNode) { + curr = action(curr, rn) + if (curr == null) return null + rn = rn.parent + } + return curr + } + } + + inner class ActiveFringeNode(val parent: FringeNode, + val occ: ConstraintOccurrence, + val idx: Int, + val genId: Int, + subst: Subst) : + FringeNode(subst, parent.vacant.clearBit(idx)) + { + val complete = vacant.cardinality() == 0 + + override fun unrelatedOrNull(occ: ConstraintOccurrence): ActiveFringeNode? = + foldUntilNull(this) { acc, rn -> if (rn.occ === occ) null else acc } + + /** + * Returns this node if it doesn't have the occurrence in its path, + * otherwise a copy of this node with the specified generation id. + */ + fun unrelatedOrCopy(occ: ConstraintOccurrence, copyGenId: Int): FringeNode? = + unrelatedOrNull(occ) ?: ActiveFringeNode(parent, occ, idx, copyGenId, subst) + + private fun matchedOccurrences(): Array = + fold(arrayOfNulls(head.size)) { arr, rn -> arr[rn.idx] = rn.occ; arr } + + fun toMatchRule(): MatchRule = object : MatchRule { + + val matched = matchedOccurrences() + + val headKept = ArrayList (matched.take(rule.headKept().count())) + + val headReplaced = ArrayList (matched.takeLast(rule.headReplaced().count())) + + private val logicalContext = object : LogicalContext { + + val meta2logical = HashMap, Logical<*>>() + + override fun variable(meta: MetaLogical): Logical = + (meta2logical[meta] ?: subst[meta]?.let { value -> + when (value) { + is Logical<*> -> value + is LogicalOwner -> value.logical() + else -> LogicalImpl(value) + } + } ?: meta.logical().also { logical -> meta2logical[meta] = logical }) as Logical + + } + + override fun rule(): Rule = rule + + override fun matchHeadKept(): MutableIterable = headKept + + override fun matchHeadReplaced(): MutableIterable = headReplaced + + override fun logicalContext(): LogicalContext = logicalContext + + } + } +} diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/util/BitSet.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/util/BitSet.kt new file mode 100644 index 00000000..c3c351e7 --- /dev/null +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/util/BitSet.kt @@ -0,0 +1,52 @@ +/* + * Copyright 2014-2018 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.logic.reactor.util + +import java.util.* + +/** + * @author Fedor Isakov + */ + +fun bitSetOfOnes(size: Int): BitSet = + BitSet(size).also { it.set(0, size) } + +fun BitSet.setBit(bit: Int): BitSet = + BitSet.valueOf(this.toLongArray()).also { it.set(bit) } + +fun BitSet.clearBit(bit: Int): BitSet = + BitSet.valueOf(this.toLongArray()).also { it.clear(bit) } + +fun BitSet.allSetBits(): Iterable = object : Iterable { + override fun iterator(): Iterator = object : Iterator { + var next = nextSetBit(0); + + override fun hasNext(): Boolean = next != -1; + + override fun next(): Int = + if (next != -1) { + val ret = next + next = nextSetBit(next + 1) + ret + } else { + throw NoSuchElementException() + } + } +} + + + diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/util/DexxCollections.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/util/DexxCollections.kt index 0671c89f..bdbfd677 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/util/DexxCollections.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/util/DexxCollections.kt @@ -35,6 +35,11 @@ fun consListOf(vararg args: E): ConsList { return builder.build() } +fun Sequence.appendAllTo(toList: ConsList): ConsList = + fold(toList) { list, e -> list.append(e) } + +fun Sequence.toConsList(): ConsList = appendAllTo(emptyConsList()) + fun ConsList.removeAt(idx: Int): ConsList { if (idx < 0) throw IllegalArgumentException("index < 0") val left = this.take(idx) diff --git a/reactor/Test/src/jetbrains/mps/unification/test/MockTerm.java b/reactor/Test/src/jetbrains/mps/unification/test/MockTerm.java index 76ce911c..ae6c4d88 100644 --- a/reactor/Test/src/jetbrains/mps/unification/test/MockTerm.java +++ b/reactor/Test/src/jetbrains/mps/unification/test/MockTerm.java @@ -16,7 +16,10 @@ 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 sun.rmi.log.LogOutputStream; import java.util.*; @@ -36,6 +39,14 @@ public abstract class MockTerm implements Term { return new MockVar(name); } + public static Term metaVar(Object symbol) { + return new MockMetaVar(symbol); + } + + public static Term logicalVar(Logical logical) { + return new MockLogicalVar(logical); + } + public static Term ref(Term term) { return new MockRef(term); } @@ -154,6 +165,92 @@ public abstract class MockTerm implements Term { } + public static class MockMetaVar extends MockTerm { + private final Object mySymbol; + + public MockMetaVar(Object symbol) { + this.mySymbol = symbol; + } + + @Override + public Object symbol() { + return mySymbol; + } + + @Override + public boolean is(Kind kind) { + return Kind.VAR == kind; + } + + @Override + public String toString() { + return String.valueOf(mySymbol); + } + + @Override + public int hashCode() { + return 43 + 17*mySymbol.hashCode(); + } + + @Override + public boolean equals(Object o) { + return ((MockMetaVar)o).mySymbol.equals(mySymbol); + } + } + + public static class MockLogicalVar extends MockTerm implements LogicalOwner { + private final Logical myLogical; + + public MockLogicalVar(Logical logical) { + this.myLogical = logical; + } + + @Override + public Logical logical() { + return myLogical; + } + + @Override + public Object symbol() { + return myLogical; + } + + @Override + public boolean is(Kind kind) { + if (myLogical.isBound()) { + return Kind.REF == kind; + + } else { + return Kind.VAR == kind; + } + } + + @Override + public Term get() { + if (myLogical.isBound()) { + return myLogical.findRoot().value(); + + } else { + return this; + } + } + + @Override + public String toString() { + return String.valueOf(myLogical); + } + + @Override + public int hashCode() { + return 31 + 19* myLogical.hashCode(); + } + + @Override + public boolean equals(Object o) { + return ((MockLogicalVar)o).myLogical.equals(myLogical); + } + } + public static class MockRef extends MockTerm { private Term term; diff --git a/reactor/Test/src/jetbrains/mps/unification/test/MockTermsParser.java b/reactor/Test/src/jetbrains/mps/unification/test/MockTermsParser.java index d0bd061e..7aa3e66e 100644 --- a/reactor/Test/src/jetbrains/mps/unification/test/MockTermsParser.java +++ b/reactor/Test/src/jetbrains/mps/unification/test/MockTermsParser.java @@ -33,7 +33,7 @@ public class MockTermsParser { return new RecursiveDescent().parse(str); } - public static Term parse(String str) { + public static Term parseTerm(String str) { List terms = new RecursiveDescent().parse(str); if (terms.size() != 1) { throw new IllegalArgumentException("expected single asTerm or asVar"); @@ -41,14 +41,6 @@ public class MockTermsParser { return terms.get(0); } - public static Term parseTerm(String str) { - return parse(str); - } - - public static Term parseVar(String str) { - return parse(str); - } - private static class RecursiveDescent { private Token lastToken; @@ -57,7 +49,7 @@ public class MockTermsParser { private LinkedList> argumentsStack = new LinkedList>(); private int lastLabel = -1; private Map termRefs = new HashMap(); - // initialized on the parse finished + // initialized on the parseTerm finished private LookupHelper lookupHelper = new LookupHelper(); private List parse(String toParse) { diff --git a/reactor/Test/test/TestController.kt b/reactor/Test/test/TestController.kt index ff0a7802..43efe42b 100644 --- a/reactor/Test/test/TestController.kt +++ b/reactor/Test/test/TestController.kt @@ -508,22 +508,29 @@ class TestController { val (X1,Y1,Z1) = metaLogical("X1", "Y1", "Z1") val (X2,Y2,Z2) = metaLogical("X2", "Y2", "Z2") val (X3,Y3,Z3) = metaLogical("X3", "Y3", "Z3") + var count = 0 programWithRules( rule("main", - headReplaced( constraint("main") ), body( statement({ z -> z.set(0) }, Z1), - constraint("foo", X1, Z1), - constraint("foo", Y1, Z1), - statement({ x, y -> eq(x, y) }, X1, Y1) ) + headReplaced( constraint("main") ), + body( + statement({ z -> z.set(0) }, Z1), + constraint("foo", X1, Z1), + constraint("foo", Y1, Z1), + statement({ x, y -> eq(x, y) }, X1, Y1) ) ), rule("capture_foo", headKept( constraint("foo", X2, Y2) ), - body( statement({ y, z -> z.set(y.get() + 1) }, Y2, Z2), - constraint("capture", Z2) ) + body( + statement({ z -> z.set(count++) }, Z2), + constraint("capture", Z2) ) ), rule("capture_foo_foo", headKept( constraint("foo", X3, Z3) ), - headReplaced( constraint("foo", Y3, Z3) ), guard( expression({ x, y -> is_eq(x, y) }, X3, Y3)), - body( constraint("replaced") ) + headReplaced( constraint("foo", Y3, Z3) ), + guard( + expression({ x, y -> is_eq(x, y) }, X3, Y3)), + body( + constraint("replaced") ) ) ).controller().evaluate(occurrence("main")).run { assertEquals(setOf( ConstraintSymbol("foo", 2), diff --git a/reactor/Test/test/TestMatcher.kt b/reactor/Test/test/TestMatcher.kt index 72857291..ce5bdee8 100644 --- a/reactor/Test/test/TestMatcher.kt +++ b/reactor/Test/test/TestMatcher.kt @@ -5,9 +5,8 @@ import jetbrains.mps.logic.reactor.program.Constraint import jetbrains.mps.logic.reactor.program.ConstraintSymbol import jetbrains.mps.unification.Term import jetbrains.mps.unification.Unification -import jetbrains.mps.unification.test.MockTermsParser.parse +import jetbrains.mps.unification.test.MockTermsParser.parseTerm import org.junit.Assert.* -import org.junit.Ignore import org.junit.Test /** @@ -386,28 +385,28 @@ class TestMatcher { programWithRules( rule("select_fg_x", headKept( - constraint("foo", parse("f{g}"), M) + constraint("foo", parseTerm("f{g}"), M) ), body( constraint("bar") )), rule("select_abX_x", headKept( - constraint("foo", parse("a{b X}"), M) + constraint("foo", parseTerm("a{b X}"), M) ), body( constraint("bar") )), rule("select_aYcde_x", headKept( - constraint("foo", parse("a{Y c{d e}}"), M) + constraint("foo", parseTerm("a{Y c{d e}}"), M) ), body( constraint("bar") )), rule("select_aYcdd_fg", headKept( - constraint("foo", parse("a{Y c{d d}}"), parse("f{g}")) + constraint("foo", parseTerm("a{Y c{d d}}"), parseTerm("f{g}")) ), body( constraint("bar") @@ -416,16 +415,16 @@ class TestMatcher { assertEquals( listOf(byTag("select_fg_x")), - forOccurrence(occurrence("foo", parse("f{g}"), parse("u"))).toList()) + forOccurrence(occurrence("foo", parseTerm("f{g}"), parseTerm("u"))).toList()) assertEquals( listOf(byTag("select_fg_x")), - forOccurrence(occurrence("foo", parse("f{Z}"), parse("u"))).toList()) + forOccurrence(occurrence("foo", parseTerm("f{Z}"), parseTerm("u"))).toList()) assertEquals( listOf(byTag("select_abX_x"), byTag("select_aYcde_x")), - forOccurrence(occurrence("foo", parse("a{b c{d Z}}"), parse("u"))).toList()) + forOccurrence(occurrence("foo", parseTerm("a{b c{d Z}}"), parseTerm("u"))).toList()) assertEquals( listOf(byTag("select_aYcdd_fg")), - forOccurrence(occurrence("foo", parse("a{d c{d d}}"), parse("f{g}"))).toList()) + forOccurrence(occurrence("foo", parseTerm("a{d c{d d}}"), parseTerm("f{g}"))).toList()) } } @@ -435,21 +434,21 @@ class TestMatcher { programWithRules( rule("select_abcde", headKept( - constraint("foo", parse("a{b{h} c{d e}}")) + constraint("foo", parseTerm("a{b{h} c{d e}}")) ), body( constraint("bar") )), rule("select_abcdf", headKept( - constraint("foo", parse("a{b{h} c{d f}}")) + constraint("foo", parseTerm("a{b{h} c{d f}}")) ), body( constraint("bar") )), rule("select_agcde", headKept( - constraint("foo", parse("a{g{h} c{d e}}")) + constraint("foo", parseTerm("a{g{h} c{d e}}")) ), body( constraint("bar") @@ -458,13 +457,13 @@ class TestMatcher { assertEquals( listOf(byTag("select_abcde")), - forOccurrence(occurrence("foo", parse("a{b{h} c{d e}}"))).toList()) + forOccurrence(occurrence("foo", parseTerm("a{b{h} c{d e}}"))).toList()) assertEquals( listOf(byTag("select_abcdf")), - forOccurrence(occurrence("foo", parse("a{b{h} c{d f}}"))).toList()) + forOccurrence(occurrence("foo", parseTerm("a{b{h} c{d f}}"))).toList()) assertEquals( listOf(byTag("select_agcde")), - forOccurrence(occurrence("foo", parse("a{g{h} c{d e}}"))).toList()) + forOccurrence(occurrence("foo", parseTerm("a{g{h} c{d e}}"))).toList()) } } @@ -478,8 +477,8 @@ class TestMatcher { val program = programWithRules( rule("foo2", headKept( - constraint("foo", b, parse("a{b}")), - constraint("foo", c, parse("a{c}")) + constraint("foo", b, parseTerm("a{b}")), + constraint("foo", c, parseTerm("a{c}")) ), body( constraint("done") @@ -487,13 +486,13 @@ class TestMatcher { ) ) - program.indices(occurrence("foo", x, parse("a{c}"))).run { - Matcher(first).matching(occurrence("foo", y, parse("a{b}")), second).let { matches -> + program.indices(occurrence("foo", x, parseTerm("a{c}"))).run { + Matcher(first).matching(occurrence("foo", y, parseTerm("a{b}")), second).let { matches -> assertEquals("foo2", matches.single().rule.tag()) } } - program.indices(occurrence("foo", x, parse("a{b}"))).run { - Matcher(first).matching(occurrence("foo", y, parse("a{c}")), second).let { matches -> + program.indices(occurrence("foo", x, parseTerm("a{b}"))).run { + Matcher(first).matching(occurrence("foo", y, parseTerm("a{c}")), second).let { matches -> assertEquals("foo2", matches.single().rule.tag()) } } @@ -508,9 +507,9 @@ class TestMatcher { val program = programWithRules( rule("expected", headKept( - constraint("foo", d, parse("a{d}")), - constraint("foo", b, parse("a{b}")), - constraint("foo", c, parse("a{c}")) + constraint("foo", d, parseTerm("a{d}")), + constraint("foo", b, parseTerm("a{b}")), + constraint("foo", c, parseTerm("a{c}")) ), body( constraint("done") @@ -521,17 +520,17 @@ class TestMatcher { val stored = ArrayList() program.indices(stored).run { val matcher = Matcher(first) - val occ1 = occurrence("foo", x, parse("a{c}")) + val occ1 = occurrence("foo", x, parseTerm("a{c}")) stored.add(occ1) matcher.matching(occ1, second).let { matches -> assertTrue(matches.isEmpty()) } - val occ2 = occurrence("foo", y, parse("a{b}")) + val occ2 = occurrence("foo", y, parseTerm("a{b}")) stored.add(occ2) matcher.matching(occ2, second).let { matches -> assertTrue(matches.isEmpty()) } - val occ3 = occurrence("foo", z, parse("a{d}")) + val occ3 = occurrence("foo", z, parseTerm("a{d}")) stored.add(occ3) matcher.matching(occ3, second).let { matches -> assertEquals("expected", matches.single().rule.tag()) diff --git a/reactor/Test/test/TestOccurrenceStore.kt b/reactor/Test/test/TestOccurrenceStore.kt index 2bc831a3..7e56f1a5 100644 --- a/reactor/Test/test/TestOccurrenceStore.kt +++ b/reactor/Test/test/TestOccurrenceStore.kt @@ -3,7 +3,7 @@ import jetbrains.mps.logic.reactor.logical.Logical import jetbrains.mps.logic.reactor.program.ConstraintSymbol.symbol import jetbrains.mps.logic.reactor.util.emptyConsList import jetbrains.mps.unification.Term -import jetbrains.mps.unification.test.MockTermsParser.parse +import jetbrains.mps.unification.test.MockTermsParser.parseTerm import org.junit.Test import org.junit.Assert.* import org.junit.Before @@ -93,10 +93,10 @@ class TestOccurrenceStore { assertEquals(listOf(cnst), occstore.forLogical(foo)) assertEquals(listOf(cnst), occstore.forSymbol(symbol("cnst", 1))) - foo.set(parse("a{b c d{e}}")) + foo.set(parseTerm("a{b c d{e}}")) assertEquals(listOf(cnst), occstore.forLogical(foo)) - assertEquals(listOf(cnst), occstore.forTerm(parse("a{b c d{e}}"))) + assertEquals(listOf(cnst), occstore.forTerm(parseTerm("a{b c d{e}}"))) foo.union(bar) assertEquals(listOf(cnst), occstore.forLogical(bar)) @@ -106,27 +106,27 @@ class TestOccurrenceStore { fun testEarlyGroundLogical() { val foo = logical("foo") - foo.set(parse("a{b c d{e}}")) + foo.set(parseTerm("a{b c d{e}}")) val cnst = occurrence("cnst", foo) occstore.store(cnst) assertEquals(listOf(cnst), occstore.forLogical(foo)) assertEquals(listOf(cnst), occstore.forSymbol(symbol("cnst", 1))) - assertEquals(listOf(cnst), occstore.forTerm(parse("a{b c d{e}}"))) + assertEquals(listOf(cnst), occstore.forTerm(parseTerm("a{b c d{e}}"))) } @Test fun testIndependentlyGroundLogical() { val foo = logical("foo") - val cnst = occurrence("cnst", parse("a{b c d{e}}")) + val cnst = occurrence("cnst", parseTerm("a{b c d{e}}")) occstore.store(cnst) - foo.set(parse("a{b c d{e}}")) + foo.set(parseTerm("a{b c d{e}}")) assertEquals(listOf(cnst), occstore.forSymbol(symbol("cnst", 1))) - assertEquals(listOf(cnst), occstore.forTerm(parse("a{b c d{e}}"))) + assertEquals(listOf(cnst), occstore.forTerm(parseTerm("a{b c d{e}}"))) assertEquals(listOf(cnst), occstore.forLogical(foo)) } @@ -141,13 +141,13 @@ class TestOccurrenceStore { @Test fun testTermIndex () { - val foo = occurrence("foo", parse("a{b c}")) + val foo = occurrence("foo", parseTerm("a{b c}")) occstore.store(foo) // TODO: more tests - assertEquals(listOf(foo), occstore.forTerm(parse("a{b c}"))) - assertEquals(listOf(foo), occstore.forTerm(parse("a{b Y}"))) - assertEquals(listOf(foo), occstore.forTerm(parse("Z"))) + assertEquals(listOf(foo), occstore.forTerm(parseTerm("a{b c}"))) + assertEquals(listOf(foo), occstore.forTerm(parseTerm("a{b Y}"))) + assertEquals(listOf(foo), occstore.forTerm(parseTerm("Z"))) } } diff --git a/reactor/Test/test/TestRuleMatcher.kt b/reactor/Test/test/TestRuleMatcher.kt new file mode 100644 index 00000000..bb78cf58 --- /dev/null +++ b/reactor/Test/test/TestRuleMatcher.kt @@ -0,0 +1,632 @@ +import jetbrains.mps.logic.reactor.core.Dispatcher +import jetbrains.mps.logic.reactor.core.RuleIndex +import jetbrains.mps.logic.reactor.core.RuleMatcher +import jetbrains.mps.logic.reactor.core.logical +import jetbrains.mps.logic.reactor.program.ConstraintSymbol.symbol +import jetbrains.mps.unification.Term +import jetbrains.mps.unification.test.MockTerm.* +import jetbrains.mps.unification.test.MockTermsParser.* +import org.junit.Assert.assertEquals +import org.junit.Test + +/* + * Copyright 2014-2018 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. + */ + +/** + * @author Fedor Isakov + */ + + +class TestRuleMatcher { + + infix fun A.shouldBe(that: B) = assertEquals(that, this) + + @Test + fun testExpand() { + with(programWithRules( + rule("main", + headReplaced( + constraint("foo"), + constraint("bar") + ), + body( + constraint("qux") + )))) + { + with(RuleMatcher(rules.first()).fringe()) { + + expand(occurrence("foo")) }.apply { + matches().size shouldBe 0 }.run { + + expand(occurrence("bar")) }.apply { + matches().size shouldBe 1 }.run { + + expand(occurrence("bazz")) }.apply { + matches().size shouldBe 0 }.run { + + } + } + } + + @Test + fun testSameOccurrence() { + with(programWithRules( + rule("rule1", + headReplaced( + constraint("foo"), + constraint("foo") + ), + body( + constraint("qux") + )))) + { + val foo = occurrence("foo") + with(RuleMatcher(rules.first()).fringe()) { + + expand(foo) }.apply { + matches().size shouldBe 0 }.run { + + expand(foo) }.apply { + matches().size shouldBe 0 }.run { + + expand(occurrence("foo")) }.apply { + matches().size shouldBe 2 }.run { + } + } + } + + @Test + fun testTermArgument() { + with(programWithRules( + rule("main", + headReplaced( + constraint("foo", parseTerm("f{g h}")), + constraint("bar", parseTerm("g")) + ), + body( + constraint("qux") + )))) + { + with(RuleMatcher(rules.first()).fringe()) { + + expand(occurrence("foo", parseTerm("f{g g}"))) }.apply { + matches().size shouldBe 0 }.run { + + expand(occurrence("bar", parseTerm("g"))) }.apply { + matches().size shouldBe 0 }.run { + + expand(occurrence("foo", parseTerm("f{g h}"))) }.apply { + matches().size shouldBe 1 }.run { + + } + } + } + + @Test + fun testTermRefArgument() { + with(programWithRules( + rule("main", + headReplaced( + constraint("foo", parseTerm("f{g h{k}}")) + ), + body( + constraint("qux") + )))) + { + with(RuleMatcher(rules.first()).fringe()) { + val termh = parseTerm("h{k}") + + expand(occurrence("foo", term("f", parseTerm("g"), ref(termh)))) }.apply { + matches().size shouldBe 1 + + } + } + } + + @Test + fun testShrink() { + with(programWithRules( + rule("main", + headReplaced( + constraint("foo"), + constraint("bar", "a"), + constraint("bazz") + ), + body( + constraint("qux") + )))) + { + val bara = occurrence("bar", "a") + with(RuleMatcher(rules.first()).fringe()) { + + expand(occurrence("foo")) }.apply { + matches().size shouldBe 0 }.run { + + expand(bara) }.run { + expand(occurrence("bar", "b")) }.apply { + matches().size shouldBe 0 }.run { + + cleanup(bara) }.apply { + matches().size shouldBe 0 }.run { + + expand(occurrence("bazz")) }.apply { + matches().size shouldBe 0 }.run { + + expand(bara) }.apply { + matches().size shouldBe 1 + + with(matches().first()) { + + matchHeadKept().count() shouldBe 0 + matchHeadReplaced().count() shouldBe 3 + matchHeadReplaced().first().constraint().symbol() shouldBe symbol("foo", 0) + + } + } + } + } + + + @Test + fun testMetaLogical() { + val (X, Y) = metaLogical("X", "Y") + with(programWithRules( + rule("main", + headReplaced( + constraint("foo", X), + constraint("bar", X, Y), + constraint("bazz", Y) + ), + body( + constraint("qux") + )))) + { + with(RuleMatcher(rules.first()).fringe()) { + + expand(occurrence("foo", "a")) }.run { + expand(occurrence("bazz", "b")) }.run { + expand(occurrence("bar", "a", "c")) }.apply { + matches().size shouldBe 0 }.run { + + expand(occurrence("bar", "d", "b")) }.apply { + matches().size shouldBe 0 }.run { + + expand(occurrence("bar", "a", "b")) }.apply { + matches().size shouldBe 1 + + with(matches().first()) { + + with(matchHeadReplaced().drop(2).first()) + { + constraint().symbol() shouldBe symbol("bazz", 1) + arguments().count() shouldBe 1 + arguments().first() shouldBe "b" + } + + with(logicalContext()) { + variable(X).findRoot().value() shouldBe "a" + variable(Y).findRoot().value() shouldBe "b" + } + + } + }.run { + expand(occurrence("foo", "d")) }.apply { + matches().size shouldBe 1 + + with(matches().first()) { + + with(matchHeadReplaced().drop(1).first()) + { + constraint().symbol() shouldBe symbol("bar", 2) + arguments().count() shouldBe 2 + arguments().toList() shouldBe listOf("d", "b") + } + + with(logicalContext()) { + variable(X).findRoot().value() shouldBe "d" + variable(Y).findRoot().value() shouldBe "b" + } + + } + } + } + } + + + @Test + fun testTermMetaLogical() { + val (X, Y) = metaLogical("X", "Y") + val yLogical = Y.logical() + with(programWithRules( + rule("rule1", + headReplaced( + constraint("foo", term("f", metaVar(X)) ), + constraint("bar", parseTerm("g{h}")) + ), + body( + constraint("qux") + )))) + { + with(RuleMatcher(rules.first()).fringe()) { + expand(occurrence("foo", parseTerm("f{g{h}}"))) }.apply { + matches().size shouldBe 0 + }.run { + expand(occurrence("bar", parseTerm("g{h}"))) }.apply { + matches().size shouldBe 1 + + with(matches().first()) { + with(logicalContext()) { + variable(X).findRoot().value() shouldBe parseTerm("g{h}") + } + } + } + } + } + + @Test + fun testTermRefLogicalMetaLogical() { + val (X, Y) = metaLogical("X", "Y") + val yLogical = Y.logical() + with(programWithRules( + rule("rule1", + headReplaced( + constraint("bar", parseTerm("h{k}"), metaVar(X)), + constraint("foo", term("f", metaVar(X), term("g"))) + ), + body( + constraint("qux") + )))) + { + with(RuleMatcher(rules.first()).fringe()) { + expand(occurrence("bar", parseTerm("h{k}"), parseTerm("h{k}"))) }.apply { + matches().size shouldBe 0 }.run { + + yLogical.set(parseTerm("h{k}")) + val termh = logicalVar(yLogical) + + expand(occurrence("foo", term("f", ref(termh), term("g")))) }.apply { + matches().size shouldBe 1 + } + } + } + + + @Test + fun testTermRefLogicalMetaLogical2() { + val (X, Y) = metaLogical("X", "Y") + val yLogical = Y.logical() + with(programWithRules( + rule("rule1", + headReplaced( + constraint("foo", term("f", term("g", metaVar(X), term("h")))) + ), + body( + constraint("qux") + )))) + { + with(RuleMatcher(rules.first()).fringe()) { + + expand(occurrence("foo", term("f", ref(logicalVar(yLogical)), term("h")))) }.apply { + matches().size shouldBe 0 }.run { + + yLogical.set(parseTerm("g{k h}")) + expand(occurrence("foo", term("f", ref(logicalVar(yLogical)), term("h")))) }.apply { + matches().size shouldBe 1 }.run { + + } + } + } + + + @Test + fun testTermLogical() { + val (X, Y) = metaLogical("X", "Y") + val yLogical = Y.logical() + with(programWithRules( + rule("rule1", + headReplaced( + constraint("foo", term("f", term("k", metaVar(X)))), + constraint("bar", parseTerm("g{h}")), + constraint("bazz", term("k", metaVar(X))) + ), + body( + constraint("qux") + )))) + { + with(RuleMatcher(rules.first()).fringe()) { + expand(occurrence("bazz", term("k", logicalVar(yLogical)))) }.apply { + matches().size shouldBe 0 + yLogical.findRoot().value() shouldBe null + }.run { + expand(occurrence("foo", parseTerm("f{k{h}}"))) }.apply { + matches().size shouldBe 0 + + yLogical.set(parseTerm("h")) }.run { + expand(occurrence("bar", parseTerm("g{h}"))) }.apply { + matches().size shouldBe 0 + + yLogical.findRoot().set(parseTerm("h")) + }.run { + expand(occurrence("bazz", term("k", logicalVar(yLogical)))) }.apply { + matches().size shouldBe 1 + + with(matches().first()) { + rule().tag() shouldBe "rule1" + + with(logicalContext()) { + variable(X).findRoot().value() shouldBe parseTerm("h") + } + } + } + } + } + + + @Test + fun testDispatcher() { + with(programWithRules( + rule("main", + headReplaced( + constraint("foo"), + constraint("bar") + ), + body( + constraint("qux") + )))) + { + with(Dispatcher(RuleIndex(handlers)).fringe()) { + + activated(occurrence("foo")) }.apply { + matches().count() shouldBe 0 }.run { + + activated(occurrence("bar")) }.apply { + matches().count() shouldBe 1 + + with(matches().first()) { + + rule().tag() shouldBe "main" + matchHeadKept().count() shouldBe 0 + matchHeadReplaced().count() shouldBe 2 + + } + } + } + } + + + @Test + fun testDispatcherManyRules() { + val X = metaLogical("X") + with(programWithRules( + rule("rule1", + headKept( + constraint("foo"), + constraint("bar", X) + ), + body( + constraint("qux") + )), + rule("rule2", + headReplaced( + constraint("foo"), + constraint("bar", X), + constraint("bazz") + ), + body( + constraint("qux") + )))) + { + with(Dispatcher(RuleIndex(handlers)).fringe()) { + + activated(occurrence("foo")) }.apply { + matches().count() shouldBe 0 }.run { + + activated(occurrence("bar", "a")) }.apply { + matches().count() shouldBe 1 + + with(matches().first()) { + + rule().tag() shouldBe "rule1" + + } + }.run { + activated(occurrence("bazz")) }.apply { + matches().count() shouldBe 1 + + with(matches().first()) { + + rule().tag() shouldBe "rule2" + logicalContext().variable(X).value() shouldBe "a" + + } + }.run { + activated(occurrence("bar", "b")) }.apply { + matches().count() shouldBe 2 + + with(matches().drop(1).first()) { + + rule().tag() shouldBe "rule2" + logicalContext().variable(X).value() shouldBe "b" + + } + } + } + } + + + @Test + fun testDispatcherRulesOrder() { + with(programWithRules( + rule("rule1", + headKept( + constraint("foo"), + constraint("bar"), + constraint("bazz") + ), + body( + constraint("qux") + )), + rule("rule2", + headReplaced( + constraint("foo"), + constraint("bar") + ), + body( + constraint("qux") + )), + rule("rule3", + headReplaced( + constraint("foo"), + constraint("bar"), + constraint("bazz"), + constraint("blin") + ), + body( + constraint("qux") + )))) + { + with(Dispatcher(RuleIndex(handlers)).fringe()) { + + activated(occurrence("blin")) }.apply { + matches().count() shouldBe 0 }.run { + + activated(occurrence("bar")) }.apply { + matches().count() shouldBe 0 }.run { + + activated(occurrence("bazz")) }.apply { + matches().count() shouldBe 0 }.run { + + activated(occurrence("foo")) }.apply { + matches().count() shouldBe 3 }.run { + + matches().map { it.rule().tag() }.toList() shouldBe listOf("rule1", "rule2", "rule3") + } + } + } + + @Test + fun testDispatcherIncremental() { + with(programWithRules( + rule("rule1", + headKept( + constraint("foo"), + constraint("bar"), + constraint("bazz") + ), + body( + constraint("qux") + )), + rule("rule2", + headReplaced( + constraint("foo"), + constraint("bar") + ), + body( + constraint("qux") + )), + rule("rule3", + headReplaced( + constraint("foo"), + constraint("bar"), + constraint("bazz"), + constraint("blin") + ), + body( + constraint("qux") + )))) + { + with(Dispatcher(RuleIndex(handlers)).fringe()) { + + activated(occurrence("foo")) }.apply { + matches().count() shouldBe 0 }.run { + + activated(occurrence("bar")) }.apply { + matches().count() shouldBe 1 + matches().first().rule().tag() shouldBe "rule2" }.run { + + activated(occurrence("bazz")) }.apply { + matches().count() shouldBe 1 + matches().first().rule().tag() shouldBe "rule1" }.run { + + activated(occurrence("blin")) }.apply { + matches().count() shouldBe 1 + matches().first().rule().tag() shouldBe "rule3" + } + } + } + + @Test + fun testDispatcherIncrementalDiscard() { + with(programWithRules( + rule("rule1", + headKept( + constraint("foo"), + constraint("bar"), + constraint("bazz") + ), + body( + constraint("qux") + )), + rule("rule2", + headReplaced( + constraint("foo"), + constraint("bar") + ), + body( + constraint("qux") + )), + rule("rule3", + headReplaced( + constraint("foo"), + constraint("bar"), + constraint("bazz"), + constraint("blin") + ), + body( + constraint("qux") + )))) + { + val bar = occurrence("bar") + with(Dispatcher(RuleIndex(handlers)).fringe()) { + + activated(occurrence("foo")) }.apply { + matches().count() shouldBe 0 }.run { + + activated(bar) }.apply { + matches().count() shouldBe 1 + matches().first().rule().tag() shouldBe "rule2" }.run { + + activated(occurrence("bazz")) }.apply { + matches().count() shouldBe 1 + matches().first().rule().tag() shouldBe "rule1" }.run { + + discarded(bar) }.apply { + matches().count() shouldBe 0 }.run { + + activated(occurrence("blin")) }.apply { + matches().count() shouldBe 0 + }.run { + activated(bar) }.apply { + matches().count() shouldBe 3 + matches().map { it.rule().tag() }.toList() shouldBe listOf("rule1", "rule2", "rule3") + } + } + } + + + + +} \ No newline at end of file diff --git a/reactor/Test/test/TestTermTrie.kt b/reactor/Test/test/TestTermTrie.kt index 550711f3..33841e33 100644 --- a/reactor/Test/test/TestTermTrie.kt +++ b/reactor/Test/test/TestTermTrie.kt @@ -1,9 +1,6 @@ import jetbrains.mps.logic.reactor.core.TermTrie -import jetbrains.mps.unification.Term -import jetbrains.mps.unification.test.MockTerm import jetbrains.mps.unification.test.MockTerm.* -import jetbrains.mps.unification.test.MockTermsParser -import jetbrains.mps.unification.test.MockTermsParser.parse +import jetbrains.mps.unification.test.MockTermsParser.parseTerm import org.junit.Test import org.junit.Assert.* @@ -16,10 +13,10 @@ class TestTermTrie { @Test fun testPut() { - val t1 = parse("a{b c}") - val t2 = parse("a{d e}") - val t3 = parse("f{g h{i k{l m{o p} n}}}") - val t4 = parse("f{g h{i q }}") + val t1 = parseTerm("a{b c}") + val t2 = parseTerm("a{d e}") + val t3 = parseTerm("f{g h{i k{l m{o p} n}}}") + val t4 = parseTerm("f{g h{i q }}") val trie1 = TermTrie().runs( { put(t1, "foo") }, @@ -35,7 +32,7 @@ class TestTermTrie { assertEquals(setOf("foo", "bar", "qux", "blah", "bazz"), trie2.allValues().toSet()) assertEquals(setOf("bar", "bazz"), trie2.lookupValues(t2).toSet()) - assertEquals(setOf(), trie2.lookupValues(parse("a{d f}")).toSet()) + assertEquals(setOf(), trie2.lookupValues(parseTerm("a{d f}")).toSet()) assertEquals(setOf("qux"), trie2.lookupValues(t3).toSet()) assertEquals(setOf("blah"), trie2.lookupValues(t4).toSet()) @@ -47,10 +44,10 @@ class TestTermTrie { @Test fun testRemove() { - val t1 = parse("a{b c}") - val t2 = parse("a{d e}") - val t3 = parse("f{g h{i k{l m{o p} n}}}") - val t4 = parse("f{g h{i q }}") + val t1 = parseTerm("a{b c}") + val t2 = parseTerm("a{d e}") + val t3 = parseTerm("f{g h{i k{l m{o p} n}}}") + val t4 = parseTerm("f{g h{i q }}") val trie1 = TermTrie().runs( { put(t1, "foo") }, @@ -80,8 +77,8 @@ class TestTermTrie { @Test fun testRemovePut() { - val t1 = parse("a{b c}") - val t2 = parse("a{b d}") + val t1 = parseTerm("a{b c}") + val t2 = parseTerm("a{b d}") val trie1 = TermTrie().runs( { put(t1, "foo") }, @@ -112,11 +109,11 @@ class TestTermTrie { @Test fun testUnif () { - val t1 = parse("f{g{a b} a}") - val t2 = parse("f{g{a X} c}") - val t3 = parse("f{g{b c} X}") - val t4 = parse("f{g{X b} X}") - val t5 = parse("f{X Y}") + val t1 = parseTerm("f{g{a b} a}") + val t2 = parseTerm("f{g{a X} c}") + val t3 = parseTerm("f{g{b c} X}") + val t4 = parseTerm("f{g{X b} X}") + val t5 = parseTerm("f{X Y}") val tt = TermTrie().runs( { put(t1, "t1") }, @@ -126,64 +123,64 @@ class TestTermTrie { { put(t5, "t5") } ) - assertEquals(setOf("t3", "t5"), tt.lookupValues(parse("f{g{b c} a}")).toSet()) - assertEquals(setOf("t3", "t4", "t5"), tt.lookupValues(parse("f{g{b X} a}")).toSet()) - assertEquals(setOf("t1", "t3", "t4", "t5"), tt.lookupValues(parse("f{g{X Y} a}")).toSet()) + assertEquals(setOf("t3", "t5"), tt.lookupValues(parseTerm("f{g{b c} a}")).toSet()) + assertEquals(setOf("t3", "t4", "t5"), tt.lookupValues(parseTerm("f{g{b X} a}")).toSet()) + assertEquals(setOf("t1", "t3", "t4", "t5"), tt.lookupValues(parseTerm("f{g{X Y} a}")).toSet()) val tt2 = tt.remove(t4, "t4") - assertEquals(setOf("t3", "t5"), tt2.lookupValues(parse("f{g{b X} a}")).toSet()) - assertEquals(setOf("t1", "t3", "t5"), tt2.lookupValues(parse("f{g{X Y} a}")).toSet()) + assertEquals(setOf("t3", "t5"), tt2.lookupValues(parseTerm("f{g{b X} a}")).toSet()) + assertEquals(setOf("t1", "t3", "t5"), tt2.lookupValues(parseTerm("f{g{X Y} a}")).toSet()) } @Test fun testQuirks() { - val t1 = parse("a{b c}") - val t2 = parse("b{c d}") + val t1 = parseTerm("a{b c}") + val t2 = parseTerm("b{c d}") val trie1 = TermTrie().runs ( { put(t1, "foo") }, { put(t2, "bar") } ) - assertEquals(setOf("foo"), trie1.lookupValues(parse("a{b c d}")).toSet()) - assertEquals(setOf("bar"), trie1.lookupValues(parse("b{c d e}")).toSet()) - assertEquals(setOf(), trie1.lookupValues(parse("a{b}")).toSet()) - assertEquals(setOf(), trie1.lookupValues(parse("b{c}")).toSet()) + assertEquals(setOf("foo"), trie1.lookupValues(parseTerm("a{b c d}")).toSet()) + assertEquals(setOf("bar"), trie1.lookupValues(parseTerm("b{c d e}")).toSet()) + assertEquals(setOf(), trie1.lookupValues(parseTerm("a{b}")).toSet()) + assertEquals(setOf(), trie1.lookupValues(parseTerm("b{c}")).toSet()) } @Test fun testWildcard() { - val t1 = parse("a{X c}") - val t2 = parse("b{c Y}") + val t1 = parseTerm("a{X c}") + val t2 = parseTerm("b{c Y}") val trie1 = TermTrie().runs( { put(t1, "foo") }, { put(t2, "bar") } ) - assertEquals(setOf("foo"), trie1.lookupValues(parse("a{b c}")).toSet()) - assertEquals(setOf("foo"), trie1.lookupValues(parse("a{b c d}")).toSet()) - assertEquals(setOf("foo"), trie1.lookupValues(parse("a{Z c}")).toSet()) - assertEquals(setOf("bar"), trie1.lookupValues(parse("b{c d e}")).toSet()) - assertEquals(setOf("bar"), trie1.lookupValues(parse("b{c d}")).toSet()) - assertEquals(setOf("bar"), trie1.lookupValues(parse("b{c Z}")).toSet()) - assertEquals(setOf(), trie1.lookupValues(parse("a{b}")).toSet()) + assertEquals(setOf("foo"), trie1.lookupValues(parseTerm("a{b c}")).toSet()) + assertEquals(setOf("foo"), trie1.lookupValues(parseTerm("a{b c d}")).toSet()) + assertEquals(setOf("foo"), trie1.lookupValues(parseTerm("a{Z c}")).toSet()) + assertEquals(setOf("bar"), trie1.lookupValues(parseTerm("b{c d e}")).toSet()) + assertEquals(setOf("bar"), trie1.lookupValues(parseTerm("b{c d}")).toSet()) + assertEquals(setOf("bar"), trie1.lookupValues(parseTerm("b{c Z}")).toSet()) + assertEquals(setOf(), trie1.lookupValues(parseTerm("a{b}")).toSet()) // invariant violated: fixed term arity -// assertEquals(setOf(), trie1.lookupValues(parse("a{Z}")).toSet()) -// assertEquals(setOf(), trie1.lookupValues(parse("b{c}")).toSet()) -// assertEquals(setOf(), trie1.lookupValues(parse("b{Z}")).toSet()) +// assertEquals(setOf(), trie1.lookupValues(parseTerm("a{Z}")).toSet()) +// assertEquals(setOf(), trie1.lookupValues(parseTerm("b{c}")).toSet()) +// assertEquals(setOf(), trie1.lookupValues(parseTerm("b{Z}")).toSet()) } @Test fun testVariable() { - val t1 = parse("a{b c}") - val t2 = parse("b{c d}") - val t3 = parse("f{g h{i k{l m{o p} n}}}") - val t4 = parse("f{g h{i q }}") + val t1 = parseTerm("a{b c}") + val t2 = parseTerm("b{c d}") + val t3 = parseTerm("f{g h{i k{l m{o p} n}}}") + val t4 = parseTerm("f{g h{i q }}") val trie1 = TermTrie().runs( { put(t1, "foo") }, @@ -192,22 +189,22 @@ class TestTermTrie { { put(t4, "blah") } ) - assertEquals(setOf("foo"), trie1.lookupValues(parse("a{X c}")).toSet()) - assertEquals(setOf("foo"), trie1.lookupValues(parse("a{b Y}")).toSet()) - assertEquals(setOf("foo"), trie1.lookupValues(parse("a{X Y}")).toSet()) - assertEquals(setOf("foo", "bar", "qux", "blah"), trie1.lookupValues(parse("Z")).toSet()) - assertEquals(setOf("qux"), trie1.lookupValues(parse("f{X h{i k{l Y Z}}}")).toSet()) - assertEquals(setOf("qux", "blah"), trie1.lookupValues(parse("f{g h{i X}}")).toSet()) + assertEquals(setOf("foo"), trie1.lookupValues(parseTerm("a{X c}")).toSet()) + assertEquals(setOf("foo"), trie1.lookupValues(parseTerm("a{b Y}")).toSet()) + assertEquals(setOf("foo"), trie1.lookupValues(parseTerm("a{X Y}")).toSet()) + assertEquals(setOf("foo", "bar", "qux", "blah"), trie1.lookupValues(parseTerm("Z")).toSet()) + assertEquals(setOf("qux"), trie1.lookupValues(parseTerm("f{X h{i k{l Y Z}}}")).toSet()) + assertEquals(setOf("qux", "blah"), trie1.lookupValues(parseTerm("f{g h{i X}}")).toSet()) } @Test fun testWildcardVariable() { - val t1 = parse("a{X c{d e}}") - val t2 = parse("a{b Y}") - val t3 = parse("a{X Y}") - val t4 = parse("f{g h{Z k{l m{o p} n}}}") - val t5 = parse("f{Z h{i q }}") + val t1 = parseTerm("a{X c{d e}}") + val t2 = parseTerm("a{b Y}") + val t3 = parseTerm("a{X Y}") + val t4 = parseTerm("f{g h{Z k{l m{o p} n}}}") + val t5 = parseTerm("f{Z h{i q }}") val trie1 = TermTrie().runs( { put(t1, "foo") }, @@ -217,26 +214,26 @@ class TestTermTrie { { put(t5, "blah") } ) - assertEquals(setOf("foo", "bar", "bazz"), trie1.lookupValues(parse("a{X c{d e}}")).toSet()) - assertEquals(setOf("foo", "bar", "bazz"), trie1.lookupValues(parse("a{b Y}")).toSet()) - assertEquals(setOf("foo", "bazz"), trie1.lookupValues(parse("a{c Y}")).toSet()) - assertEquals(setOf("foo", "bar", "bazz"), trie1.lookupValues(parse("a{X Y}")).toSet()) - assertEquals(setOf("foo", "bar", "bazz", "qux", "blah"), trie1.lookupValues(parse("Z")).toSet()) - assertEquals(setOf("qux"), trie1.lookupValues(parse("f{X h{i k{l Y Y}}}")).toSet()) - assertEquals(setOf("qux"), trie1.lookupValues(parse("f{X h{j Y}}")).toSet()) - assertEquals(setOf("qux", "blah"), trie1.lookupValues(parse("f{g h{i X}}")).toSet()) - assertEquals(setOf("qux", "blah"), trie1.lookupValues(parse("f{X h{i Y}}")).toSet()) - assertEquals(setOf("qux", "blah"), trie1.lookupValues(parse("f{X Y}")).toSet()) - assertEquals(setOf("blah"), trie1.lookupValues(parse("f{j h{X q}}")).toSet()) + assertEquals(setOf("foo", "bar", "bazz"), trie1.lookupValues(parseTerm("a{X c{d e}}")).toSet()) + assertEquals(setOf("foo", "bar", "bazz"), trie1.lookupValues(parseTerm("a{b Y}")).toSet()) + assertEquals(setOf("foo", "bazz"), trie1.lookupValues(parseTerm("a{c Y}")).toSet()) + assertEquals(setOf("foo", "bar", "bazz"), trie1.lookupValues(parseTerm("a{X Y}")).toSet()) + assertEquals(setOf("foo", "bar", "bazz", "qux", "blah"), trie1.lookupValues(parseTerm("Z")).toSet()) + assertEquals(setOf("qux"), trie1.lookupValues(parseTerm("f{X h{i k{l Y Y}}}")).toSet()) + assertEquals(setOf("qux"), trie1.lookupValues(parseTerm("f{X h{j Y}}")).toSet()) + assertEquals(setOf("qux", "blah"), trie1.lookupValues(parseTerm("f{g h{i X}}")).toSet()) + assertEquals(setOf("qux", "blah"), trie1.lookupValues(parseTerm("f{X h{i Y}}")).toSet()) + assertEquals(setOf("qux", "blah"), trie1.lookupValues(parseTerm("f{X Y}")).toSet()) + assertEquals(setOf("blah"), trie1.lookupValues(parseTerm("f{j h{X q}}")).toSet()) } @Test fun testValuesOrder() { - val t1 = parse("a{X c}") - val t2 = parse("a{b Y}") - val t3 = parse("a{c Y}") - val t4 = parse("a{X Y}") + val t1 = parseTerm("a{X c}") + val t2 = parseTerm("a{b Y}") + val t3 = parseTerm("a{c Y}") + val t4 = parseTerm("a{X Y}") val trie1 = TermTrie().runs( { put(t1, "foo") }, @@ -246,15 +243,15 @@ class TestTermTrie { ) // value order/cardinality no longer maintained - assertEquals(setOf("foo", "bar", "qux"), trie1.lookupValues(parse("a{b X}")).toSet()) - assertEquals(setOf("foo", "bar", "bazz", "qux"), trie1.lookupValues(parse("a{X c}")).toSet()) - assertEquals(setOf("foo", "bazz", "qux"), trie1.lookupValues(parse("a{c c}")).toSet()) + assertEquals(setOf("foo", "bar", "qux"), trie1.lookupValues(parseTerm("a{b X}")).toSet()) + assertEquals(setOf("foo", "bar", "bazz", "qux"), trie1.lookupValues(parseTerm("a{X c}")).toSet()) + assertEquals(setOf("foo", "bazz", "qux"), trie1.lookupValues(parseTerm("a{c c}")).toSet()) val trie2 = trie1.remove(t2, "bar") val trie3 = trie2.put(t2, "blah") - assertEquals(setOf("foo", "qux", "blah"), trie3.lookupValues(parse("a{b X}")).toSet()) - assertEquals(setOf("foo", "bazz", "qux", "blah"), trie3.lookupValues(parse("a{X c}")).toSet()) + assertEquals(setOf("foo", "qux", "blah"), trie3.lookupValues(parseTerm("a{b X}")).toSet()) + assertEquals(setOf("foo", "bazz", "qux", "blah"), trie3.lookupValues(parseTerm("a{X c}")).toSet()) } @Test @@ -262,28 +259,28 @@ class TestTermTrie { val varRef = MockRef(MockVar("TAIL")) val pattern = MockFun("g", MockFun("h"), MockFun("f", varRef, MockFun("nil"))) val trie1 = TermTrie().runs( - { put(parse("g {h f {a nil}}"), "bar") }, - { put(parse("g {h f {a f {b nil}}}"), "bazz") }, + { put(parseTerm("g {h f {a nil}}"), "bar") }, + { put(parseTerm("g {h f {a f {b nil}}}"), "bazz") }, { put(pattern, "foo") }, - { put(parse("g {h foo {nil}}"), "qux") } + { put(parseTerm("g {h foo {nil}}"), "qux") } ) - assertEquals(listOf("qux"), trie1.lookupValues(parse("g {h foo {nil}}")).toList()) + assertEquals(listOf("qux"), trie1.lookupValues(parseTerm("g {h foo {nil}}")).toList()) - val key = MockFun("g", MockFun("h"), parse("f {c nil}")) + val key = MockFun("g", MockFun("h"), parseTerm("f {c nil}")) assertEquals(listOf("foo"), trie1.lookupValues(key).toList()) } @Test fun testRefList() { val trie = TermTrie().runs( - { put(parse("f{X Y}"), "foo") }, - { put(parse("f{a Z}"), "bar") }, - { put(parse("f{a f{b W}}"), "bazz") } + { put(parseTerm("f{X Y}"), "foo") }, + { put(parseTerm("f{a Z}"), "bar") }, + { put(parseTerm("f{a f{b W}}"), "bazz") } ) - val f = parse("f {b nil}") - val key = MockFun("f", parse("a"), MockRef(MockRef(f))) + val f = parseTerm("f {b nil}") + val key = MockFun("f", parseTerm("a"), MockRef(MockRef(f))) assertEquals(setOf("foo", "bar", "bazz"), trie.lookupValues(key).toSet()) } @@ -291,22 +288,22 @@ class TestTermTrie { @Test fun testCyclicTerm() { val trie = TermTrie().runs( - { put(parse("cst{ @1 n{ a{b c} d{^1} } }"), "foo") }, - { put(parse("cst{ n{ @2 a{b ^2} d{e} } }"), "bar") } + { put(parseTerm("cst{ @1 n{ a{b c} d{^1} } }"), "foo") }, + { put(parseTerm("cst{ n{ @2 a{b ^2} d{e} } }"), "bar") } ) - assertEquals(setOf("foo", "bar"), trie.lookupValues(parse("cst{ N }")).toSet()) - assertEquals(setOf("foo", "bar"), trie.lookupValues(parse("cst{ n{ X Y } }")).toSet()) - assertEquals(setOf("foo", "bar"), trie.lookupValues(parse("cst{ n{ X d{Z} } }")).toSet()) - assertEquals(setOf("foo", "bar"), trie.lookupValues(parse("cst{ n{ a{b W} V } }")).toSet()) - assertEquals(listOf("bar"), trie.lookupValues(parse("cst{ n{ @1 a{b ^1} V } }"))) - assertEquals(listOf("foo"), trie.lookupValues(parse("cst{ @1 n{ a{b S} d{^1} } }"))) + assertEquals(setOf("foo", "bar"), trie.lookupValues(parseTerm("cst{ N }")).toSet()) + assertEquals(setOf("foo", "bar"), trie.lookupValues(parseTerm("cst{ n{ X Y } }")).toSet()) + assertEquals(setOf("foo", "bar"), trie.lookupValues(parseTerm("cst{ n{ X d{Z} } }")).toSet()) + assertEquals(setOf("foo", "bar"), trie.lookupValues(parseTerm("cst{ n{ a{b W} V } }")).toSet()) + assertEquals(listOf("bar"), trie.lookupValues(parseTerm("cst{ n{ @1 a{b ^1} V } }"))) + assertEquals(listOf("foo"), trie.lookupValues(parseTerm("cst{ @1 n{ a{b S} d{^1} } }"))) val trie2 = trie.runs( - { remove(parse("cst{ n{ @2 a{b ^2} d{e} } }"), "bar") } + { remove(parseTerm("cst{ n{ @2 a{b ^2} d{e} } }"), "bar") } ) - assertEquals(emptyList(), trie2.lookupValues(parse("cst{ n{ @1 a{b ^1} V } }"))) - assertEquals(listOf("foo"), trie2.lookupValues(parse("cst{ @1 n{ a{b S} d{^1} } }"))) + assertEquals(emptyList(), trie2.lookupValues(parseTerm("cst{ n{ @1 a{b ^1} V } }"))) + assertEquals(listOf("foo"), trie2.lookupValues(parseTerm("cst{ @1 n{ a{b S} d{^1} } }"))) } diff --git a/reactor/Test/test/jetbrains/mps/unification/test/ParserTests.java b/reactor/Test/test/jetbrains/mps/unification/test/ParserTests.java index 8c615022..e08aac83 100644 --- a/reactor/Test/test/jetbrains/mps/unification/test/ParserTests.java +++ b/reactor/Test/test/jetbrains/mps/unification/test/ParserTests.java @@ -43,51 +43,51 @@ public class ParserTests { @Test public void testSingle() { - assertEquals(parse("a"), term("a")); - assertEquals(parseTerm("a").symbol(), term("a").symbol()); - 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()); - assertEquals(parse("a{b c}"), term("a", term("b"), term("c"))); - assertEquals(parse("a{b X}"), term("a", term("b"), var("X"))); - assertEquals(parse("a{X b}"), term("a", var("X"), term("b"))); - assertEquals(parse("a{X Y}"), term("a", var("X"), var("Y"))); + assertEquals(MockTermsParser.parseTerm("a"), MockTermsParser.parseTerm("a")); + assertEquals(parseTerm("a").symbol(), MockTermsParser.parseTerm("a").symbol()); + assertEquals(parseTerm("X").symbol(), var("X").symbol()); + assertEquals(MockTermsParser.parseTerm("X"), var("X")); + assertEquals(MockTermsParser.parseTerm("a{b}"), term("a", MockTermsParser.parseTerm("b"))); + assertEquals(parseTerm("a{b}").symbol(), term("a", MockTermsParser.parseTerm("b")).symbol()); + assertEquals(MockTermsParser.parseTerm("a{b c}"), term("a", MockTermsParser.parseTerm("b"), MockTermsParser.parseTerm("c"))); + assertEquals(MockTermsParser.parseTerm("a{b X}"), term("a", MockTermsParser.parseTerm("b"), var("X"))); + assertEquals(MockTermsParser.parseTerm("a{X b}"), term("a", var("X"), MockTermsParser.parseTerm("b"))); + assertEquals(MockTermsParser.parseTerm("a{X Y}"), term("a", var("X"), var("Y"))); } @Test public void testMuti() { - assertEqualsAll(parseAll("a b"), term("a"), term("b")); + assertEqualsAll(parseAll("a b"), MockTermsParser.parseTerm("a"), MockTermsParser.parseTerm("b")); assertEqualsAll(parseAll("X Y"), var("X"), var("Y")); - assertEqualsAll(parseAll("a{b} a{b}"), term("a", term("b")), term("a", term("b"))); + assertEqualsAll(parseAll("a{b} a{b}"), term("a", MockTermsParser.parseTerm("b")), term("a", MockTermsParser.parseTerm("b"))); } @Test public void testWhitespace() { - assertEquals(parse(" a"), term("a")); - assertEquals(parse(" Y "), var("Y")); - assertEquals(parse("a{ b }"), term("a", term("b"))); - assertEquals(parse("a{ b c }"), term("a", term("b"), term("c"))); - assertEquals(parse("a{b X} "), term("a", term("b"), var("X"))); - assertEquals(parse("a {X b}"), term("a", var("X"), term("b"))); - assertEquals(parse(" a{X Y } "), term("a", var("X"), var("Y"))); + assertEquals(MockTermsParser.parseTerm(" a"), MockTermsParser.parseTerm("a")); + assertEquals(MockTermsParser.parseTerm(" Y "), var("Y")); + assertEquals(MockTermsParser.parseTerm("a{ b }"), term("a", MockTermsParser.parseTerm("b"))); + assertEquals(MockTermsParser.parseTerm("a{ b c }"), term("a", MockTermsParser.parseTerm("b"), MockTermsParser.parseTerm("c"))); + assertEquals(MockTermsParser.parseTerm("a{b X} "), term("a", MockTermsParser.parseTerm("b"), var("X"))); + assertEquals(MockTermsParser.parseTerm("a {X b}"), term("a", var("X"), MockTermsParser.parseTerm("b"))); + assertEquals(MockTermsParser.parseTerm(" a{X Y } "), term("a", var("X"), var("Y"))); } @Test public void testDeep() { - assertEquals(parse("a{b{c{d{e f g}}}}"), + assertEquals(MockTermsParser.parseTerm("a{b{c{d{e f g}}}}"), term("a", term("b", term("c", term("d", - term("e"), term("f"), term("g")))))); + MockTermsParser.parseTerm("e"), MockTermsParser.parseTerm("f"), MockTermsParser.parseTerm("g")))))); - assertEquals(parse("a{X b{c{d{Z e W f g} Y}}}"), + assertEquals(MockTermsParser.parseTerm("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("Z"), MockTermsParser.parseTerm("e"), var("W"), MockTermsParser.parseTerm("f"), MockTermsParser.parseTerm("g")), var("Y"))))); } @@ -96,23 +96,23 @@ public class ParserTests { LazyTermLookup termLookup = new LazyTermLookup(); Term a = termLookup.term = term("a", ref(termLookup)); assertEquivalent( - parse("@1a{^1}"), + MockTermsParser.parseTerm("@1a{^1}"), a); - Term b = term("b"); + Term b = MockTermsParser.parseTerm("b"); assertEquivalent( - parse("a{@1b ^1}"), + MockTermsParser.parseTerm("a{@1b ^1}"), term("a", b, ref(b))); - Term c = term("c"); + Term c = MockTermsParser.parseTerm("c"); assertEquivalent( - parse("a{^1 @1c}"), + MockTermsParser.parseTerm("a{^1 @1c}"), term("a", ref(c), c)); - Term b1 = term("b"); - Term b2 = term("b"); + Term b1 = MockTermsParser.parseTerm("b"); + Term b2 = MockTermsParser.parseTerm("b"); assertEquivalent( - parse("a{@2b ^1 ^2 @1b}"), + MockTermsParser.parseTerm("a{@2b ^1 ^2 @1b}"), term("a", b2, ref(b1), ref(b2), b1)); } @@ -121,78 +121,78 @@ public class ParserTests { Term x = var("X"); assertEquivalent( - parse("^X"), + MockTermsParser.parseTerm("^X"), ref(x)); assertEquivalent( - parse("a{^X}"), + MockTermsParser.parseTerm("a{^X}"), term("a", ref(x))); } @Test(expected = ComparisonFailure.class) public void testNotEquivalent1() throws Exception { - Term d = term("d"); - assertEquivalent(parse("a{^1 @1c}"), + Term d = MockTermsParser.parseTerm("d"); + assertEquivalent(MockTermsParser.parseTerm("a{^1 @1c}"), term("a", ref(d), d)); } @Test(expected = MockTermsParser.ParseException.class) public void testUnclosedFail() { - parse("a{b "); + MockTermsParser.parseTerm("a{b "); } @Test(expected = MockTermsParser.ParseException.class) public void testUnclosedFail2() { - parse("a{X b"); + MockTermsParser.parseTerm("a{X b"); } @Test(expected = MockTermsParser.ParseException.class) public void testUnclosedFail3() { - parse("a{{X b}"); + MockTermsParser.parseTerm("a{{X b}"); } @Test(expected = MockTermsParser.ParseException.class) public void testDoubleClosed() { - parse("a{X b}}"); + MockTermsParser.parseTerm("a{X b}}"); } @Test(expected = IllegalArgumentException.class) public void testFailMulti1() { - parse(" a Y"); + MockTermsParser.parseTerm(" a Y"); } @Test(expected = IllegalArgumentException.class) public void testFailMulti2() { - parse("a b"); + MockTermsParser.parseTerm("a b"); } @Test(expected = MockTermsParser.ParseException.class) public void testEmptyFail() { - parse(""); + MockTermsParser.parseTerm(""); } @Test(expected = MockTermsParser.ParseException.class) public void testEmptyChildrenFail() { - parse("a{}"); + MockTermsParser.parseTerm("a{}"); } @Test(expected = MockTermsParser.ParseException.class) public void testWrongStartFail() { - parse("{a}"); + MockTermsParser.parseTerm("{a}"); } @Test(expected = MockTermsParser.ParseException.class) public void testVarHasChilrenFail() { - parse("X{a}"); + MockTermsParser.parseTerm("X{a}"); } @Test(expected = MockTermsParser.ParseException.class) public void testExtraSymbolFail() { - parse("a}"); + MockTermsParser.parseTerm("a}"); } @Test(expected = MockTermsParser.ParseException.class) public void testNonExistingRefFail() { - parse("a{b ^1}"); + MockTermsParser.parseTerm("a{b ^1}"); } } diff --git a/reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java b/reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java index db74a08d..eed9f766 100644 --- a/reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java +++ b/reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java @@ -19,9 +19,7 @@ package jetbrains.mps.unification.test; import jetbrains.mps.unification.Term; import jetbrains.mps.unification.TermWrapper; import org.jetbrains.annotations.NotNull; -import org.junit.Ignore; import org.junit.Test; -import org.omg.CORBA.UNKNOWN; import java.util.Collection; import java.util.Collections; @@ -39,10 +37,10 @@ public class SolverTests { @Test public void test1() throws Exception { assertUnifiesWithBindings( - term("a"), + MockTermsParser.parseTerm("a"), var("X"), - bind(var("X"), term("a")) + bind(var("X"), MockTermsParser.parseTerm("a")) ); assertUnifiesWithBindings( var("Y"), @@ -51,8 +49,8 @@ public class SolverTests { bind(var("X"), var("Y")) ); assertUnifiesWithBindings( - parse("a{Y}"), - parse("a{X}"), + MockTermsParser.parseTerm("a{Y}"), + MockTermsParser.parseTerm("a{X}"), bind(var("X"), var("Y")) ); @@ -61,56 +59,56 @@ public class SolverTests { @Test public void test2() throws Exception { assertUnifiesWithBindings( - parse("a{b c}"), - parse("a{X Y}"), + MockTermsParser.parseTerm("a{b c}"), + MockTermsParser.parseTerm("a{X Y}"), - bind(var("X"), term("b")), - bind(var("Y"), term("c")) + bind(var("X"), MockTermsParser.parseTerm("b")), + bind(var("Y"), MockTermsParser.parseTerm("c")) ); assertUnifiesWithBindings( - parse("a{b Y}"), - parse("a{X c}"), + MockTermsParser.parseTerm("a{b Y}"), + MockTermsParser.parseTerm("a{X c}"), - bind(var("X"), term("b")), - bind(var("Y"), term("c")) + bind(var("X"), MockTermsParser.parseTerm("b")), + bind(var("Y"), MockTermsParser.parseTerm("c")) ); assertUnifiesWithBindings( - parse("a{b{c} X Y Z}"), - parse("a{X Y Z b{c}}"), + MockTermsParser.parseTerm("a{b{c} X Y Z}"), + MockTermsParser.parseTerm("a{X Y Z b{c}}"), - bind(var("X"), parse("b{c}")), - bind(var("Y"), parse("b{c}")), - bind(var("Z"), parse("b{c}")) + bind(var("X"), MockTermsParser.parseTerm("b{c}")), + bind(var("Y"), MockTermsParser.parseTerm("b{c}")), + bind(var("Z"), MockTermsParser.parseTerm("b{c}")) ); assertUnifiesWithBindings( - parse("a{b{c} Z Y X}"), - parse("a{Z Y X b{W}}"), + MockTermsParser.parseTerm("a{b{c} Z Y X}"), + MockTermsParser.parseTerm("a{Z Y X b{W}}"), - bind(var("X"), parse("b{c}")), - bind(var("Y"), parse("b{c}")), - bind(var("Z"), parse("b{c}")), - bind(var("W"), parse("c")) + bind(var("X"), MockTermsParser.parseTerm("b{c}")), + bind(var("Y"), MockTermsParser.parseTerm("b{c}")), + bind(var("Z"), MockTermsParser.parseTerm("b{c}")), + bind(var("W"), MockTermsParser.parseTerm("c")) ); } @Test public void test3() throws Exception { assertUnifiesWithBindings( - parse("a{b{X} c{Y}}"), - parse("a{V W}"), + MockTermsParser.parseTerm("a{b{X} c{Y}}"), + MockTermsParser.parseTerm("a{V W}"), bind(var("V"), parseTerm("b{X}")), bind(var("W"), parseTerm("c{Y}")) ); assertUnifiesWithBindings( - parse("a{X}"), - parse("a{Y}"), + MockTermsParser.parseTerm("a{X}"), + MockTermsParser.parseTerm("a{Y}"), bind(var("X"), var("Y")) ); assertUnifiesWithBindings( - parse("a{b{X} c{Y}}"), - parse("a{b{V} c{W}}"), + MockTermsParser.parseTerm("a{b{X} c{Y}}"), + MockTermsParser.parseTerm("a{b{V} c{W}}"), bind(var("V"), var("X")), bind(var("W"), var("Y")) @@ -120,8 +118,8 @@ public class SolverTests { @Test public void test4() throws Exception { assertUnifiesWithBindings( - parse("a{b{X} c{Y}}"), - parse("a{Y Z}"), + MockTermsParser.parseTerm("a{b{X} c{Y}}"), + MockTermsParser.parseTerm("a{Y Z}"), bind(var("Y"), parseTerm("b{X}")), bind(var("Z"), parseTerm("c{Y}")) @@ -135,7 +133,7 @@ public class SolverTests { parseTerm("a{Y b{X}}"), bind(var("Y"), parseTerm("b{c}")), - bind(var("X"), term("c")) + bind(var("X"), MockTermsParser.parseTerm("c")) ); } @@ -146,7 +144,7 @@ public class SolverTests { parseTerm("a{Y c{b{d}}}"), bind(var("Y"), parseTerm("b{X}")), - bind(var("X"), term("d")) + bind(var("X"), MockTermsParser.parseTerm("d")) ); } @@ -211,8 +209,8 @@ public class SolverTests { @Test public void test12() throws Exception { assertUnifiesWithBindings( - parse("node{name{foo} child{X}}"), - parse("node{name{foo} child{Y}}"), + MockTermsParser.parseTerm("node{name{foo} child{X}}"), + MockTermsParser.parseTerm("node{name{foo} child{Y}}"), bind(var("X"), var("Y")) ); @@ -221,8 +219,8 @@ public class SolverTests { @Test public void test13() throws Exception { assertUnifiesWithBindings( - parse("node{name{foo} child{node{name{bar}}}}"), - parse("node{name{foo} child{X}}"), + MockTermsParser.parseTerm("node{name{foo} child{node{name{bar}}}}"), + MockTermsParser.parseTerm("node{name{foo} child{X}}"), bind(var("X"), parseTerm("node{name{bar}}")) ); @@ -231,8 +229,8 @@ public class SolverTests { @Test public void test14() throws Exception { assertUnifiesWithBindings( - parse("f{X g{a}}"), - parse("f{g{Y} g{Y}}"), + MockTermsParser.parseTerm("f{X g{a}}"), + MockTermsParser.parseTerm("f{g{Y} g{Y}}"), bind(var("X"), parseTerm("g{Y}")), bind(var("Y"), parseTerm("a")) @@ -242,10 +240,10 @@ public class SolverTests { @Test public void test15() throws Exception { assertUnifiesWithBindingsAsymm( - parse("h{X1 f{Y0 Y0} Y1}"), - parse("h{f{X0 X0} Y1 X1}"), + MockTermsParser.parseTerm("h{X1 f{Y0 Y0} Y1}"), + MockTermsParser.parseTerm("h{f{X0 X0} Y1 X1}"), - bind(var("X0"), parseVar("Y0")), + bind(var("X0"), parseTerm("Y0")), bind(var("X1"), parseTerm("f{Y0 Y0}")), bind(var("Y1"), parseTerm("f{Y0 Y0}")) ); @@ -258,12 +256,12 @@ public class SolverTests { // substitution instead of the "triangular" form used here. assertUnifiesWithBindingsAsymm( - parse("h{X1 X2 X3 X4 X5 X6 X7 X8 X9 " + + MockTermsParser.parseTerm("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} " + + MockTermsParser.parseTerm("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("X0"), parseTerm("Y0")), bind(var("X1"), parseTerm("f{Y0 Y0}")), bind(var("X2"), parseTerm("f{Y1 Y1}")), bind(var("X3"), parseTerm("f{Y2 Y2}")), @@ -288,63 +286,63 @@ public class SolverTests { @Test public void testCyclicVar() throws Exception { assertUnifiesWithBindings( - parse("@1 a{b ^1}"), - parse("X"), + MockTermsParser.parseTerm("@1 a{b ^1}"), + MockTermsParser.parseTerm("X"), - bind(var("X"), parse("@1 a{b ^1}")) + bind(var("X"), MockTermsParser.parseTerm("@1 a{b ^1}")) ); assertUnifiesWithBindings( - parse("@1 a{^1 b c}"), - parse("X"), + MockTermsParser.parseTerm("@1 a{^1 b c}"), + MockTermsParser.parseTerm("X"), - bind(var("X"), parse("@1 a{^1 b c}")) + bind(var("X"), MockTermsParser.parseTerm("@1 a{^1 b c}")) ); assertUnifiesWithBindings( - parse("a{X c{X} }"), - parse("a{b{Y} c{@1 b{@2 c{b{^2}}}}}"), + MockTermsParser.parseTerm("a{X c{X} }"), + MockTermsParser.parseTerm("a{b{Y} c{@1 b{@2 c{b{^2}}}}}"), - bind(var("X"), parse("b{Y}")), - bind(var("Y"), parse("@1 c{b{^1}}")) + bind(var("X"), MockTermsParser.parseTerm("b{Y}")), + bind(var("Y"), MockTermsParser.parseTerm("@1 c{b{^1}}")) ); } @Test public void testVarRef() throws Exception { assertUnifiesWithBindings( - parse("^X"), - parse("Y"), + MockTermsParser.parseTerm("^X"), + MockTermsParser.parseTerm("Y"), bind(var("X"), var("Y")) ); assertUnifiesWithBindings( - parse("a{b ^X}"), - parse("a{b c{d}}"), + MockTermsParser.parseTerm("a{b ^X}"), + MockTermsParser.parseTerm("a{b c{d}}"), - bind(var("X"), parse("c{d}")) + bind(var("X"), MockTermsParser.parseTerm("c{d}")) ); assertUnifiesWithBindings( - parse("a{b c{X} ^X}"), - parse("a{b c{d} d}"), + MockTermsParser.parseTerm("a{b c{X} ^X}"), + MockTermsParser.parseTerm("a{b c{d} d}"), - bind(var("X"), parse("d")) + bind(var("X"), MockTermsParser.parseTerm("d")) ); assertUnifiesWithBindings( - parse("a{b{d} c{X} ^X}"), - parse("a{b{^X} c{d} d}"), + MockTermsParser.parseTerm("a{b{d} c{X} ^X}"), + MockTermsParser.parseTerm("a{b{^X} c{d} d}"), - bind(var("X"), parse("d")) + bind(var("X"), MockTermsParser.parseTerm("d")) ); assertUnifiesWithBindings( - parse("a{b{d} c{X}}"), - parse("a{b{^X} c{d}}"), + MockTermsParser.parseTerm("a{b{d} c{X}}"), + MockTermsParser.parseTerm("a{b{^X} c{d}}"), - bind(var("X"), parse("d")) + bind(var("X"), MockTermsParser.parseTerm("d")) ); } @Test public void testUnifyExternalRef() throws Exception { - Term termRef = ref(parse("f {a f{b f{c d}}}")); + Term termRef = ref(MockTermsParser.parseTerm("f {a f{b f{c d}}}")); Term varRef = ref(var("TAIL")); Term a = term("g", termRef); @@ -354,14 +352,14 @@ public class SolverTests { a, b, - bind(var("HEAD"), parse("a")), - bind(var("TAIL"), parse("f{b f{c d}}")) + bind(var("HEAD"), MockTermsParser.parseTerm("a")), + bind(var("TAIL"), MockTermsParser.parseTerm("f{b f{c d}}")) ); } @Test public void testUnifyExternalRef2() throws Exception { - Term list = parse("f {a f{b f{c d}}}"); + Term list = MockTermsParser.parseTerm("f {a f{b f{c d}}}"); Term termRef = ref(list); Term varRef = ref(var("TAIL")); @@ -375,15 +373,15 @@ public class SolverTests { aa, bb, - bind(var("LIST"), parse("f {a f{b f{c d}}}")), - bind(var("HEAD"), parse("a")), - bind(var("TAIL"), parse("f{b f{c d}}")) + bind(var("LIST"), MockTermsParser.parseTerm("f {a f{b f{c d}}}")), + bind(var("HEAD"), MockTermsParser.parseTerm("a")), + bind(var("TAIL"), MockTermsParser.parseTerm("f{b f{c d}}")) ); } @Test public void testUnifyExternalRef3() throws Exception { - Term empty = parse("f {nil}"); + Term empty = MockTermsParser.parseTerm("f {nil}"); Term varRef = ref(var("TAIL")); Term aa = term("g", empty); @@ -393,16 +391,16 @@ public class SolverTests { aa, bb, - bind(var("TAIL"), parse("nil")) + bind(var("TAIL"), MockTermsParser.parseTerm("nil")) ); } @Test public void testWrapper() throws Exception { - Term t1 = parse("a{b c{X}}"); - Term t2 = parse("a{X c{Y}}"); - Term p1 = parse("a{META c{d}}"); - Term p2 = parse("a{b c{META}}"); + Term t1 = MockTermsParser.parseTerm("a{b c{X}}"); + Term t2 = MockTermsParser.parseTerm("a{X c{Y}}"); + Term p1 = MockTermsParser.parseTerm("a{META c{d}}"); + Term p2 = MockTermsParser.parseTerm("a{b c{META}}"); class Wrapper implements Term { Term wrapped; @@ -431,34 +429,34 @@ public class SolverTests { }; assertUnifiesWithBindings(t1, p1, - bind(var("META"), parse("b")), - bind(var("X"), parse("d")) + bind(var("META"), MockTermsParser.parseTerm("b")), + bind(var("X"), MockTermsParser.parseTerm("d")) ); assertUnificationFails(t1, p1, wrapper); assertUnifiesWithBindings(t1, p2, wrapper, - bind(var("X"), parse("META")) + bind(var("X"), MockTermsParser.parseTerm("META")) ); assertUnifiesWithBindings(t2, p2, wrapper, - bind(var("X"), parse("b")), - bind(var("Y"), parse("META")) + bind(var("X"), MockTermsParser.parseTerm("b")), + bind(var("Y"), MockTermsParser.parseTerm("META")) ); } @Test public void testFailConflict() throws Exception { assertUnificationFails( - term("a"), - term("b"), + MockTermsParser.parseTerm("a"), + MockTermsParser.parseTerm("b"), SYMBOL_CLASH, "a", "b" ); assertUnificationFails( - parse("node{name{X} child{abc}}"), - parse("node{name{foo} child{X}}"), + MockTermsParser.parseTerm("node{name{X} child{abc}}"), + MockTermsParser.parseTerm("node{name{foo} child{X}}"), SYMBOL_CLASH, "abc", @@ -469,76 +467,76 @@ public class SolverTests { @Test public void testFailCard() throws Exception { assertUnificationFails( - parse("a{b c}"), - parse("a{X}") + MockTermsParser.parseTerm("a{b c}"), + MockTermsParser.parseTerm("a{X}") ); } @Test public void testFailCyclic() throws Exception { assertUnificationFails( - term("g", ref(parse("f {h X}"))), + term("g", ref(MockTermsParser.parseTerm("f {h X}"))), term("g", var("X")), CYCLE_DETECTED ); assertUnificationFails( - parse("t {@1 f {h X} g {f {h X}}}"), - parse("t {Y g {X}}"), + MockTermsParser.parseTerm("t {@1 f {h X} g {f {h X}}}"), + MockTermsParser.parseTerm("t {Y g {X}}"), CYCLE_DETECTED ); assertUnificationFails( - parse("a{b X}"), - parse("X"), + MockTermsParser.parseTerm("a{b X}"), + MockTermsParser.parseTerm("X"), CYCLE_DETECTED ); assertUnificationFails( - parse("f{X}"), - parse("X"), + MockTermsParser.parseTerm("f{X}"), + MockTermsParser.parseTerm("X"), CYCLE_DETECTED ); assertUnificationFails( - parse("X"), - parse("f{X}"), + MockTermsParser.parseTerm("X"), + MockTermsParser.parseTerm("f{X}"), CYCLE_DETECTED ); assertUnificationFails( - parse("f{f{X}}"), - parse("f{X}"), + MockTermsParser.parseTerm("f{f{X}}"), + MockTermsParser.parseTerm("f{X}"), CYCLE_DETECTED ); assertUnificationFails( - parse("f{a{X} Y }"), - parse("f{Y a{b{X}}}"), + MockTermsParser.parseTerm("f{a{X} Y }"), + MockTermsParser.parseTerm("f{Y a{b{X}}}"), CYCLE_DETECTED ); assertUnificationFails( - parse("a{X c{X}}"), - parse("a{b{Y} Y }"), + MockTermsParser.parseTerm("a{X c{X}}"), + MockTermsParser.parseTerm("a{b{Y} Y }"), CYCLE_DETECTED ); assertUnificationFails( - parse("a{ b{c{b{c{b{c{^2}}}}}} @2 b{c{b{c{^2}}}}}"), - parse("a{ b{Y} b{Y} }"), + MockTermsParser.parseTerm("a{ b{c{b{c{b{c{^2}}}}}} @2 b{c{b{c{^2}}}}}"), + MockTermsParser.parseTerm("a{ b{Y} b{Y} }"), CYCLE_DETECTED ); assertUnificationFails( - parse("t {@1 f {h X} g {f {h X}}}"), - parse("t {Y g {X}}"), + MockTermsParser.parseTerm("t {@1 f {h X} g {f {h X}}}"), + MockTermsParser.parseTerm("t {Y g {X}}"), CYCLE_DETECTED ); assertUnificationFails( - parse("t {@1 f {h X} g {^1}}"), - parse("t {Y g {X}}"), + MockTermsParser.parseTerm("t {@1 f {h X} g {^1}}"), + MockTermsParser.parseTerm("t {Y g {X}}"), CYCLE_DETECTED );