Packages

class Matcher extends Logger

Matches a goal term against a template term.

  • Input: terms template and goal
  • Output: substitution solution such that template ^ solution == goal, where Term.^ is the method applying the substitution.

Full code example see below.

Source
Matcher.scala
Examples:

  1. In normed vector spaces you might have the template term ||x - y|| and would like to match the goal term ||(a - b) - c|| with it.
    The matcher will give you the substitution solution = [x := (a - b), y := c]. This is a special case of (typed!) unification. In general, unification seeks a solution substitution such that template solution == goal solution, i.e. the substitution applied on *both* sides. Thus the template usually contains variables intended for substitution ("matching"), but the goal does not. Still, the goal term may contain free variables as in the example above, they will then be part of the solution substitution - but only in the RHS of the substitutions. No equality relation is taken into account except alpha-conversion of bound variables and solution rules.

    2. ,

  2. scala // Construct the goal and template terms // val namespace = DPath(URI("http://example.com")) val module = namespace ? "myModule" val norm = OMID(module ? "norm") val minus = OMID(module ? "minus") // "||(x - y) - z||" val goal = OMA( norm, List( OMA( minus, List( OMA(minus, List(OMV("x"), OMV("y"))), OMV("z") ) ) ) ) // "||a - b||" val template = OMA( norm, List(OMA( minus, List(OMV("a"), OMV("b")) )) ) // Empty rule set because we don't use any logic foundation // specific typing rules (e.g. the rule in LF for function // application) val matcher = new Matcher(ctrl, new MutableRuleSet) val matchResult = matcher( Context(VarDecl(LocalName("x"), LocalName("y"), LocalName("z"))), goal, Context(VarDecl(LocalName("a"), LocalName("b"))), template ) // MatchSuccess(a:=(http://example.com?myModule?minus x y), b:=z,true)

Note

The class can be reused for multiple matches using the same RuleSet but is not thread-safe.

,

Beware of situations where the template and goal term share some variables. E.g. take template term = "a", goal term = "a - a". Intuitively, this should be a match with the substitution [a := a - a], but this class cannot handle this. The following code will lead to a MatchFail: scala val matchResult = matcher( Context(VarDecl(LocalName("a"))), OMA(minus, List(OMV("a"), OMV("a"))), Context(VarDecl(LocalName("a"))), OMV("a") ) As a solution you might want to first make your template variables fresh: scala val matchResult = matcher( Context(VarDecl(LocalName("a"))), OMA(minus, List(OMV("a"), OMV("a"))), Context(VarDecl(LocalName("b"))), OMV("b") ) // MatchSuccess(b:=(http://example.com?myModule?minus a a),true) println(matchResult)

Linear Supertypes
Logger, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Matcher
  2. Logger
  3. AnyRef
  4. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new Matcher(controller: Controller, rules: RuleSet)

    controller

    needed for lookups when type checking the matches

    rules

    Simplification and other equality-related rules to take into account. Especially, you most probably want to specify the equality of your meta-theory (e.g. LF), e.g., by calling scala val ctx = Context(mPathToATheory) new Matcher(ctrl, RuleSet.collectRules(ctrl, ctx))

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 apply(goalContext: Context, queryVars: Context)(doit: ((Term, Term) ⇒ Boolean) ⇒ Boolean): MatchResult

    A more general matching function that allows for multiple calls to the equality predicate (in the same context), e.g., to handle \forall queryVars.

    A more general matching function that allows for multiple calls to the equality predicate (in the same context), e.g., to handle \forall queryVars. q_1 = g_1 \wedge ... \wedge q_n = g_n.

    doit

    a function that takes an equality predicate (for matching) and returns true if the match is possible e.g., basic matching is obtained as apply(queryVars){eq => eq(goal, query)}

  5. def apply(goalContext: Context, goal: Term, queryVars: Context, query: Term): MatchResult

    The core matching function for API users.

    The core matching function for API users.

    goalContext

    the global context

    goal

    the term to be matched, relative to goalContext

    queryVars

    the variables to solve within the template query

    query

    the template term to match against, relative to goalContext ++ queryVars

    returns

    MatchSuccess(subs, true) if goal == query ^ subs for goalContext |- subs:queryVars -> .

  6. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  7. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()
  8. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  9. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  10. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  11. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  12. def getSolution: Substitution

    returns

    the solution if a match was found this does not provide maps for template variables that did not occur in the template

  13. def getUnsolvedVariables: List[LocalName]
  14. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  15. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  16. def log(e: Error): Unit

    logs an error - always logged

    logs an error - always logged

    Attributes
    protected
    Definition Classes
    Logger
  17. def log(s: ⇒ String, subgroup: Option[String] = None): Unit

    logs a message with this logger's logprefix

    logs a message with this logger's logprefix

    Attributes
    protected
    Definition Classes
    Logger
  18. def logError(s: ⇒ String): Unit

    log as an error message

    log as an error message

    Attributes
    protected
    Definition Classes
    Logger
  19. def logGroup[A](a: ⇒ A): A

    wraps around a group to create nested logging

    wraps around a group to create nested logging

    Attributes
    protected
    Definition Classes
    Logger
  20. def logPrefix: String
    Definition Classes
    Matcher → Logger
  21. def logTemp(s: ⇒ String): Unit

    temporary logging - always logged

    temporary logging - always logged

    Attributes
    protected
    Definition Classes
    Logger
  22. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  23. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  24. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  25. def report: Report
    Definition Classes
    Matcher → Logger
  26. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  27. def toString(): String
    Definition Classes
    AnyRef → Any
  28. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  29. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  30. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()

Inherited from Logger

Inherited from AnyRef

Inherited from Any

Ungrouped