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

New rule matching algorithm

This commit is contained in:
Fedor Isakov 2018-07-30 15:08:36 +02:00
parent 1609b5838d
commit 74402a8a1c
16 changed files with 1467 additions and 323 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
reactor/API/src/jetbrains/mps/logic/reactor/evaluation/MatchRule.java
View File

@ -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<ConstraintOccurrence> matchHeadReplaced();
LogicalContext logicalContext();
}

85
reactor/Core/src/jetbrains/mps/logic/reactor/core/Dispatcher.kt Normal file
View File

@ -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<Rule, RuleMatcher>()
init {
ruleIndex.forEach { rule ->
val matcher = RuleMatcher(rule)
rule2matcher.put(rule, matcher);
}
}
inner class DispatchFringe {
private var rule2fringe: PersMap<Rule, RuleMatcher.MatchFringe>
val allMatches = arrayListOf<MatchRule>()
constructor() {
this.rule2fringe = Maps.of()
rule2matcher.entries.forEach { e ->
this.rule2fringe = rule2fringe.put(e.key, e.value.fringe())
}
}
constructor(pred: DispatchFringe, matching: Iterable<RuleMatcher.MatchFringe>) {
this.rule2fringe = pred.rule2fringe
matching.forEach { fringe ->
this.rule2fringe = rule2fringe.put(fringe.rule(), fringe)
allMatches.addAll(fringe.matches())
}
}
fun matches() : Iterable<MatchRule> = 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()
}

1
reactor/Core/src/jetbrains/mps/logic/reactor/core/Matcher.kt
View File

@ -113,6 +113,7 @@ class Match(val rule: Rule,
override fun matchHeadReplaced(): Iterable<ConstraintOccurrence> = discardedOccurrences
override fun logicalContext(): LogicalContext = logicalContext
}
/** Function term with arguments == constraints converted to terms. May contain variables. */

6
reactor/Core/src/jetbrains/mps/logic/reactor/core/RuleIndex.kt
View File

@ -30,7 +30,7 @@ import java.util.*
* @author Fedor Isakov
*/
class RuleIndex : Iterable<Rule> {
class RuleIndex(handlers: Iterable<Handler>) : Iterable<Rule> {
private val primarySymbol2valueIndex = HashMap<ConstraintSymbol, ValueIndex>()
@ -38,7 +38,7 @@ class RuleIndex : Iterable<Rule> {
private val tag2rule = LinkedHashMap<String, Rule>()
constructor(handlers: Iterable<Handler>) {
init {
for (h in handlers) {
for (r in h.rules()) {
tag2rule[r.tag()] = r
@ -68,7 +68,7 @@ class RuleIndex : Iterable<Rule> {
val symbol = c.symbol()
if (symbol in primSymbols) {
primarySymbol2valueIndex[symbol]?.update(r, c)
} else {
auxSymbol2valueIndex.getOrPut(symbol) { ValueIndex(symbol) }.update(r, c)
}

277
reactor/Core/src/jetbrains/mps/logic/reactor/core/RuleMatcher.kt Normal file
View File

@ -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<MetaLogical<*>, Any>
private fun emptySubst() = Maps.of<MetaLogical<*>, 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<FringeNode>,
val seen: IdHashSet<ConstraintOccurrence>,
val genId: Int) {
fun rule(): Rule = rule
fun matches(): Collection<MatchRule> =
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<ActiveFringeNode> {
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 <T> 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 <T> 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<ConstraintOccurrence?> =
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<MetaLogical<*>, Logical<*>>()
override fun <V : Any> variable(meta: MetaLogical<V>): Logical<V> =
(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<V>
}
override fun rule(): Rule = rule
override fun matchHeadKept(): MutableIterable<ConstraintOccurrence?> = headKept
override fun matchHeadReplaced(): MutableIterable<ConstraintOccurrence?> = headReplaced
override fun logicalContext(): LogicalContext = logicalContext
}
}
}

52
reactor/Core/src/jetbrains/mps/logic/reactor/util/BitSet.kt Normal file
View File

@ -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<Int> = object : Iterable<Int> {
override fun iterator(): Iterator<Int> = object : Iterator<Int> {
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()
}
}
}

5
reactor/Core/src/jetbrains/mps/logic/reactor/util/DexxCollections.kt
View File

@ -35,6 +35,11 @@ fun <E> consListOf(vararg args: E): ConsList<E> {
return builder.build()
}
fun <E> Sequence<E>.appendAllTo(toList: ConsList<E>): ConsList<E> =
fold(toList) { list, e -> list.append(e) }
fun <E> Sequence<E>.toConsList(): ConsList<E> = appendAllTo(emptyConsList())
fun <E> ConsList<E>.removeAt(idx: Int): ConsList<E> {
if (idx < 0) throw IllegalArgumentException("index < 0")
val left = this.take(idx)

97
reactor/Test/src/jetbrains/mps/unification/test/MockTerm.java
View File

@ -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<? extends Term> 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<? extends Term> myLogical;
public MockLogicalVar(Logical<? extends Term> 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;

12
reactor/Test/src/jetbrains/mps/unification/test/MockTermsParser.java
View File

@ -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<Term> 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<List<Term>> argumentsStack = new LinkedList<List<Term>>();
private int lastLabel = -1;
private Map<Integer, Term> termRefs = new HashMap<Integer, Term>();
// initialized on the parse finished
// initialized on the parseTerm finished
private LookupHelper lookupHelper = new LookupHelper();
private List<Term> parse(String toParse) {

23
reactor/Test/test/TestController.kt
View File

@ -508,22 +508,29 @@ class TestController {
val (X1,Y1,Z1) = metaLogical<Int>("X1", "Y1", "Z1")
val (X2,Y2,Z2) = metaLogical<Int>("X2", "Y2", "Z2")
val (X3,Y3,Z3) = metaLogical<Int>("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),

55
reactor/Test/test/TestMatcher.kt
View File

@ -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<ConstraintOccurrence>()
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())

24
reactor/Test/test/TestOccurrenceStore.kt
View File

@ -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<Term>("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<Term>("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")))
}
}

632
reactor/Test/test/TestRuleMatcher.kt Normal file
View File

@ -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, B> 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<String>("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<Term>("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<Term>("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<Term>("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<Term>("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<String>("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")
}
}
}
}

195
reactor/Test/test/TestTermTrie.kt
View File

@ -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<Any>().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<Any>(), trie2.lookupValues(parse("a{d f}")).toSet())
assertEquals(setOf<Any>(), 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<Any>().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<Any>().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<String>().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<Any>().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<Any>(), trie1.lookupValues(parse("a{b}")).toSet())
assertEquals(setOf<Any>(), 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<Any>(), trie1.lookupValues(parseTerm("a{b}")).toSet())
assertEquals(setOf<Any>(), 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<Any>().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<Any>(), 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<Any>(), trie1.lookupValues(parseTerm("a{b}")).toSet())
// invariant violated: fixed term arity
// assertEquals(setOf<Any>(), trie1.lookupValues(parse("a{Z}")).toSet())
// assertEquals(setOf<Any>(), trie1.lookupValues(parse("b{c}")).toSet())
// assertEquals(setOf<Any>(), trie1.lookupValues(parse("b{Z}")).toSet())
// assertEquals(setOf<Any>(), trie1.lookupValues(parseTerm("a{Z}")).toSet())
// assertEquals(setOf<Any>(), trie1.lookupValues(parseTerm("b{c}")).toSet())
// assertEquals(setOf<Any>(), 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<Any>().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<Any>().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<Any>().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<Any>().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<Any>().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<Any>().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<String>(), 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<String>(), trie2.lookupValues(parseTerm("cst{ n{ @1 a{b ^1} V } }")))
assertEquals(listOf("foo"), trie2.lookupValues(parseTerm("cst{ @1 n{ a{b S} d{^1} } }")))
}

94
reactor/Test/test/jetbrains/mps/unification/test/ParserTests.java
View File

@ -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}");
}
}

230
reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java
View File

@ -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
);