de.uka.ilkd.key.rule.match.vm

Class TacletMatchProgram

java.lang.Object

de.uka.ilkd.key.rule.match.vm.TacletMatchProgram

public class TacletMatchProgram
extends java.lang.Object

Instances of this class represent programs for matching a term against a given pattern. The programs are specialised for a certain pattern. To create such a program use the static method createProgram(Term) and provide as argument the pattern for which you want to get a matcher. The program is executed by invoking match(Term, MatchConditions, Services).

Field Summary

Fields

Modifier and Type	Field and Description
static TacletMatchProgram	EMPTY_PROGRAM the skip program (matches anything)
private MatchInstruction[]	instruction the instructions of the program

Constructor Summary

Constructors

Modifier	Constructor and Description
private	TacletMatchProgram(MatchInstruction[] instruction) creates an instance of the matcher consisting of the instruction

Method Summary

Modifier and Type	Method and Description
static TacletMatchProgram	createProgram(Term pattern) creates a matcher for the given pattern
private static void	createProgram(Term pattern, java.util.ArrayList<MatchInstruction> program) creates a matching program for the given pattern.
static MatchSchemaVariableInstruction<? extends SchemaVariable>	getMatchInstructionForSV(SchemaVariable op) returns the instruction for the specified variable
MatchConditions	match(Term p_toMatch, MatchConditions p_matchCond, Services services) executes the program and tries to match the provided term; additional restrictions are provided via match conditions.

Methods inherited from class java.lang.Object

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

Field Detail

EMPTY_PROGRAM

public static final TacletMatchProgram EMPTY_PROGRAM

the skip program (matches anything)

instruction

private final MatchInstruction[] instruction

the instructions of the program

Constructor Detail

TacletMatchProgram

private TacletMatchProgram(MatchInstruction[] instruction)

creates an instance of the matcher consisting of the instruction

Method Detail

createProgram

public static TacletMatchProgram createProgram(Term pattern)

creates a matcher for the given pattern

Parameters:

pattern - the Term specifying the pattern

Returns:

the specialized matcher for the given pattern

getMatchInstructionForSV

public static MatchSchemaVariableInstruction<? extends SchemaVariable> getMatchInstructionForSV(SchemaVariable op)

returns the instruction for the specified variable

Parameters:

sv - the SchemaVariable for which to get the instruction

Returns:

the instruction for the specified variable

createProgram

private static void createProgram(Term pattern,
                                  java.util.ArrayList<MatchInstruction> program)

creates a matching program for the given pattern. It appends the necessary match instruction to the given list of instructions

Parameters:

pattern - the Term used as pattern for which to create a matcher

program - the list of MatchInstruction to which the instructions for matching pattern are added.

match

public MatchConditions match(Term p_toMatch,
                             MatchConditions p_matchCond,
                             Services services)

executes the program and tries to match the provided term; additional restrictions are provided via match conditions. The returned conditions are either null if no match is possible or MatchConditions which extends the given conditions by additional constraints (e.g., instantiations of schemavariables) such that they describe the found match

Parameters:

p_toMatch - the Term to match

p_matchCond - the initial MatchConditions which have to be satisfied in addition to those generated by this match

services - the Services

Returns:

null if no match was found or the match result