Packages

trait BaseMatcher extends Matcher with Logging

Basic matcher infrastructure that simply forwards all unification functionality to BaseMatcher.unify(). Only apply() functions wrap exceptions in context while unify() functions simply pass it upwards.

Linear Supertypes
Logging, LazyLogging, LoggerHolder, Matcher, (Expression, Expression) ⇒ RenUSubst, AnyRef, Any
Known Subclasses
FreshUnificationMatch, LinearMatcher, NonSubstUnificationMatch, RestrictedBiDiUnificationMatch, RestrictedBiDiUnificationMatch, SchematicComposedUnificationMatch, SchematicUnificationMatch, UnificationMatch, UnificationMatchBase, UniformMatcher, UniformMatcher, UniformMatching
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. BaseMatcher
  2. Logging
  3. LazyLogging
  4. LoggerHolder
  5. Matcher
  6. Function2
  7. AnyRef
  8. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. type Subst = RenUSubst

    The (generalized) substitutions used for unification purposes

    The (generalized) substitutions used for unification purposes

    Definition Classes
    Matcher
    See also

    RenUSubst

  2. type SubstRepl = (Expression, Expression)

    A (generalized) substitution pair, which is either like a SubstitutionPair for uniform substitution or a pair of Variable for uniform renaming.

    A (generalized) substitution pair, which is either like a SubstitutionPair for uniform substitution or a pair of Variable for uniform renaming.

    Definition Classes
    Matcher
    See also

    SubstitutionPair

Abstract Value Members

  1. abstract def unify(shape: Sequent, input: Sequent): List[SubstRepl]

    unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Attributes
    protected
    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

  2. abstract def unify(shape: Program, input: Program): List[SubstRepl]

    unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Attributes
    protected
    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

  3. abstract def unify(shape: Formula, input: Formula): List[SubstRepl]

    unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Attributes
    protected
    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

  4. abstract def unify(shape: Term, input: Term): List[SubstRepl]

    unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Attributes
    protected
    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

  5. abstract def unifyODE(shape: DifferentialProgram, input: DifferentialProgram): List[SubstRepl]

    unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Attributes
    protected
    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

Concrete Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. def Subst(subs: List[SubstRepl]): Subst

    Create a (generalized) substitution from the given representation subs.

    Create a (generalized) substitution from the given representation subs.

    Attributes
    protected
    Definition Classes
    Matcher
  5. def SubstRepl(what: Expression, repl: Expression): SubstRepl

    Create a (generalized) substitution pair.

    Create a (generalized) substitution pair.

    Attributes
    protected
    Definition Classes
    Matcher
    See also

    SubstitutionPair

  6. def apply(e1: Sequent, e2: Sequent): Subst

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Definition Classes
    BaseMatcher → Matcher
    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

  7. def apply(e1: DifferentialProgram, e2: DifferentialProgram): Subst

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Definition Classes
    BaseMatcher → Matcher
    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

  8. def apply(e1: Program, e2: Program): Subst

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Definition Classes
    BaseMatcher → Matcher
    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

  9. def apply(e1: Formula, e2: Formula): Subst

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Definition Classes
    BaseMatcher → Matcher
    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

  10. def apply(e1: Term, e2: Term): Subst

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Definition Classes
    BaseMatcher → Matcher
    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

  11. def apply(e1: Expression, e2: Expression): Subst

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Definition Classes
    BaseMatcher → Matcher → Function2
  12. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  13. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  14. def curried: (Expression) ⇒ (Expression) ⇒ RenUSubst
    Definition Classes
    Function2
    Annotations
    @unspecialized()
  15. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  16. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  17. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  18. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  19. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  20. val id: List[SubstRepl]

    Identity substitution {} that does not change anything.

    Identity substitution {} that does not change anything.

    Attributes
    protected
    Definition Classes
    Matcher
  21. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  22. def join(s: List[SubstRepl], t: List[SubstRepl]): List[SubstRepl]

    Union of renaming substitution representations: join(s, t) gives the representation of s performed together with t, if compatible.

    Union of renaming substitution representations: join(s, t) gives the representation of s performed together with t, if compatible.

    s \cup t = {p(.)~>F | (p(.)~>F) \in s}  ++  {(p(.)~>F) | (p(.)~>F) \in t}
if s and t are compatible, so do not map the same p(.) or f(.) or a to different replacements
    returns

    a substitution that has the same effect as applying both substitutions s and t simultaneously. Similar to returning s++t but skipping duplicates and checking compatibility in passing.

    Attributes
    protected
  23. lazy val logger: Logger
    Attributes
    protected
    Definition Classes
    LazyLogging → LoggerHolder
  24. final val loggerName: String
    Attributes
    protected
    Definition Classes
    LoggerHolder
  25. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  26. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  27. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  28. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  29. def toString(): String
    Definition Classes
    Function2 → AnyRef → Any
  30. def tupled: ((Expression, Expression)) ⇒ RenUSubst
    Definition Classes
    Function2
    Annotations
    @unspecialized()
  31. def unifiable(shape: Sequent, input: Sequent): Option[Subst]

    unifiable(shape, input) Compute some unifier matching input against the pattern shape if unifiable else None

    unifiable(shape, input) Compute some unifier matching input against the pattern shape if unifiable else None

    Definition Classes
    BaseMatcher → Matcher
  32. def unifiable(shape: Expression, input: Expression): Option[Subst]

    unifiable(shape, input) Compute some unifier matching input against the pattern shape if unifiable else None

    unifiable(shape, input) Compute some unifier matching input against the pattern shape if unifiable else None

    Definition Classes
    BaseMatcher → Matcher
  33. def unifier(e1: Sequent, e2: Sequent, us: List[SubstRepl]): Subst

    Create the unifier us (which was formed for e1 and e2, just for the record).

    Create the unifier us (which was formed for e1 and e2, just for the record).

    Attributes
    protected
  34. def unifier(e1: Expression, e2: Expression, us: List[SubstRepl]): Subst

    Create the unifier us (which was formed for e1 and e2, just for the record).

    Create the unifier us (which was formed for e1 and e2, just for the record).

    Attributes
    protected
  35. def unifier(shape: Expression, input: Expression): List[SubstRepl]

    Construct the base unifier that forces shape and input to unify unless equal already

    Construct the base unifier that forces shape and input to unify unless equal already

    returns

    {shape~>input} unless shape=input in which case it's {}.

    Attributes
    protected
  36. def unify(shape: Expression, input: Expression): List[SubstRepl]
    Attributes
    protected
  37. def ununifiable(shape: Sequent, input: Sequent): Nothing

    Indicates that input cannot be matched against the pattern shape by raising a UnificationException.

    Indicates that input cannot be matched against the pattern shape by raising a UnificationException.

    Attributes
    protected
    Exceptions thrown

    UnificationException always.

  38. def ununifiable(shape: Expression, input: Expression): Nothing

    Indicates that input cannot be matched against the pattern shape by raising a UnificationException.

    Indicates that input cannot be matched against the pattern shape by raising a UnificationException.

    Attributes
    protected
    Exceptions thrown

    UnificationException always.

  39. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  40. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  41. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from Logging

Inherited from LazyLogging

Inherited from LoggerHolder

Inherited from Matcher

Inherited from (Expression, Expression) ⇒ RenUSubst

Inherited from AnyRef

Inherited from Any

Ungrouped