Packages

trait Matcher extends (Expression, Expression) ⇒ RenUSubst

Matcher(shape, input) matches second argument input against the pattern shape of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape, i.e., gives a single-sided matcher.

The following notation is used to indicate that u is the unifier computed for matching input t against shape s:

s = t | u

That is u is the result of calling Matcher.apply(s,t).

Examples: 

  1. val s = Matcher("p()&q()".asFormula, "x<=0 & x^2>=0".asFormula)
// gives {p() ~> x<=0, q() ~> x^2>=0}
println(s)
    2. , 

  2. val s = Matcher("[a;++b;]p()".asFormula, "[x:=x+1; ++ {x'=-x}]y<=0".asFormula)
// gives {a ~> x:=x+1, b ~> {x'=-x}, p() ~> y<=0}
println(s)
    3. , 

  3. val s = Matcher("[a;++b;]p(||)".asFormula, "[x:=x+1; ++ {x'=-x}]x>=0".asFormula)
// gives {a ~> x:=x+1, b ~> {x'=-x}, p(||) ~> x>=0}
println(s)
    4. , 

  4. // will throw UnificationException
val s = Matcher("[a;++b;]p(||)".asFormula, "[x:=x+1;{x'=-x}]x>=0".asFormula)
See also

UnificationException

UnificationMatch

SchematicUnificationMatch

Linear Supertypes
(Expression, Expression) ⇒ RenUSubst, AnyRef, Any
Known Subclasses
BaseMatcher, FreshUnificationMatch, InsistentMatcher, LinearMatcher, NonSubstUnificationMatch, RestrictedBiDiUnificationMatch, RestrictedBiDiUnificationMatch, SchematicComposedUnificationMatch, SchematicUnificationMatch, UnificationMatch, UnificationMatchBase, UnificationMatchUSubstAboveURen, UniformMatcher, UniformMatcher, UniformMatching
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Matcher
  2. Function2
  3. AnyRef
  4. 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

    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.

    See also

    SubstitutionPair

Abstract Value Members

  1. abstract def apply(shape: Sequent, input: 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.

    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

  2. abstract def apply(shape: DifferentialProgram, input: 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.

    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

  3. abstract def apply(shape: Program, input: 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.

    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

  4. abstract def apply(shape: Formula, input: 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.

    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

  5. abstract def apply(shape: Term, input: 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.

    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

  6. abstract def apply(shape: Expression, input: 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
    Matcher → Function2
  7. abstract def unifiable(shape: Sequent, input: Sequent): Option[Subst]

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

  8. abstract def unifiable(shape: Expression, input: Expression): Option[Subst]

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

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
  5. def SubstRepl(what: Expression, repl: Expression): SubstRepl

    Create a (generalized) substitution pair.

    Create a (generalized) substitution pair.

    Attributes
    protected
    See also

    SubstitutionPair

  6. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  7. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  8. def curried: (Expression) ⇒ (Expression) ⇒ RenUSubst
    Definition Classes
    Function2
    Annotations
    @unspecialized()
  9. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  10. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  11. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  12. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  13. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  14. val id: List[SubstRepl]

    Identity substitution {} that does not change anything.

    Identity substitution {} that does not change anything.

    Attributes
    protected
  15. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  16. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  17. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  18. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  19. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  20. def toString(): String
    Definition Classes
    Function2 → AnyRef → Any
  21. def tupled: ((Expression, Expression)) ⇒ RenUSubst
    Definition Classes
    Function2
    Annotations
    @unspecialized()
  22. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  23. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  24. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from (Expression, Expression) ⇒ RenUSubst

Inherited from AnyRef

Inherited from Any

Ungrouped