de.uka.ilkd.key.rule.match.legacy

Class ElementMatcher.SortDependingFunctionMatcher

java.lang.Object

de.uka.ilkd.key.rule.match.legacy.ElementMatcher<SortDependingFunction>

de.uka.ilkd.key.rule.match.legacy.ElementMatcher.SortDependingFunctionMatcher

Enclosing class:

ElementMatcher<T extends Operator>

private static class ElementMatcher.SortDependingFunctionMatcher
extends ElementMatcher<SortDependingFunction>

Constructor Summary

Constructors

Modifier	Constructor and Description
private	SortDependingFunctionMatcher()

Method Summary

Modifier and Type	Method and Description
MatchConditions	match(SortDependingFunction op, SVSubstitute subst, MatchConditions mc, Services services) Taking this sortdepending function as template to be matched against op, the necessary conditions are returned or null if not unifiable (matchable).
private static MatchConditions	matchSorts(Sort s1, Sort s2, MatchConditions mc, Services services) tries to match sort s1 to fit sort s2

Methods inherited from class de.uka.ilkd.key.rule.match.legacy.ElementMatcher

getElementMatcherFor

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

SortDependingFunctionMatcher

private SortDependingFunctionMatcher()

Method Detail

matchSorts

private static MatchConditions matchSorts(Sort s1,
                                          Sort s2,
                                          MatchConditions mc,
                                          Services services)

tries to match sort s1 to fit sort s2

Parameters:

s1 - Sort tried to matched (maybe concrete or (contain) generic)

s2 - concrete Sort

mc - the MatchConditions up to now

Returns:

null if failed the resulting match conditions otherwise

match

public MatchConditions match(SortDependingFunction op,
                             SVSubstitute subst,
                             MatchConditions mc,
                             Services services)

Taking this sortdepending function as template to be matched against op, the necessary conditions are returned or null if not unifiable (matchable). A sortdepending function is matched successfully against another sortdepending function if the sorts can be matched and they are of same kind.

Specified by:

match in class ElementMatcher<SortDependingFunction>