Orbital library

orbital.logic.trs
Interface Substitution.Matcher

Enclosing interface:
Substitution

public static interface Substitution.Matcher

Interface for matching and replacing elementary terms within a substitution.

Instances of this interface provide the functionality of an elementary replacement x2→t2 of a substitution σ = [x1→t1,x2→t2,…,xn→tn]. The matcher is called by the Substitution to check whether a given term matches it, and can then be used to replace the matched term with another term, if required. Hence, the substitution is the inductive homomorphic continuation of its elementary replacements.

Author:
André Platzer
See Also:
Substitutions.createExactMatcher(Object, Object), Substitutions.createExactMatcher(Object), Substitutions.createSingleSidedMatcher(Object, Object), Substitutions.createSingleSidedMatcher(Object, Object, orbital.logic.functor.Predicate), Substitutions.createSingleSidedMatcher(Object)
Note:
in effect this is a local variant of substitution.

Method Summary
 boolean equals(java.lang.Object o)
          Whether this matcher equals another.
 int hashCode()
           
 boolean matches(java.lang.Object t)
          Attempts to match t against this.
 java.lang.Object pattern()
          Get the pattern descriptor.
 java.lang.Object replace(java.lang.Object t)
          Replace a matched term.
 

Method Detail

equals

boolean equals(java.lang.Object o)
Whether this matcher equals another. Two matchers are equal if they describe the same elementary replacements.

Note that it is usually safe to compare for type and pattern only, regardless of the substitute. But carefully avoid using "substitutions" with multiple replacements specified for a single pattern.

Overrides:
equals in class java.lang.Object

hashCode

int hashCode()
Overrides:
hashCode in class java.lang.Object

pattern

java.lang.Object pattern()
Get the pattern descriptor.

Returns:
an object that describes the pattern against which to match.

matches

boolean matches(java.lang.Object t)
Attempts to match t against this.

Returns:
whether t matches this Matcher, which is thus applicable, here.

replace

java.lang.Object replace(java.lang.Object t)
Replace a matched term.

Parameters:
t - the term matched per matches(Object).
Returns:
the substitute for t. Simply returns t if no replacement should occur at all.
Preconditions:
matches(t) ∧ "matches(t) was the last call to matches(Object)"

Orbital library
1.3.0: 11 Apr 2009

Copyright © 1996-2009 André Platzer
All Rights Reserved.