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

Class MatchTermLabelInstruction

java.lang.Object

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

All Implemented Interfaces:

MatchInstruction

public class MatchTermLabelInstruction
extends java.lang.Object
implements MatchInstruction

This match instruction implements the matching logic for term labels.

Field Summary

Fields

Modifier and Type	Field and Description
private ImmutableArray<TermLabel>	labels

Constructor Summary

Constructors

Constructor and Description
MatchTermLabelInstruction(ImmutableArray<TermLabel> labels)

Method Summary

Modifier and Type	Method and Description
private MatchConditions	match(TermLabelSV sv, Term instantiationCandidate, MatchConditions matchCond, Services services)
MatchConditions	match(TermNavigator termPosition, MatchConditions matchConditions, Services services)

Methods inherited from class java.lang.Object

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

Field Detail

labels

private final ImmutableArray<TermLabel> labels

Constructor Detail

MatchTermLabelInstruction

public MatchTermLabelInstruction(ImmutableArray<TermLabel> labels)

Method Detail

match

private MatchConditions match(TermLabelSV sv,
                              Term instantiationCandidate,
                              MatchConditions matchCond,
                              Services services)

match

public MatchConditions match(TermNavigator termPosition,
                             MatchConditions matchConditions,
                             Services services)

Specified by:

match in interface MatchInstruction