| java.lang.Object
 de.uka.ilkd.key.logic.op.TermSymbol
de.uka.ilkd.key.logic.op.SchemaVariableAdapter
de.uka.ilkd.key.logic.op.SortedSchemaVariable
All known Subclasses: de.uka.ilkd.key.logic.op.AbstractTermSV, de.uka.ilkd.key.logic.op.VariableSV, de.uka.ilkd.key.logic.op.SkolemTermSV, de.uka.ilkd.key.logic.op.ProgramSV,
| SortedSchemaVariable | | abstract public class SortedSchemaVariable extends SchemaVariableAdapter implements ParsableVariable,QuantifiableVariable,Location(Code) | | This class represents the root of a schema variable hierarchy to be express
termstructures that match on logical terms. Schema variables are used in
Taclets where they act as placeholders for other TermSymbols. The TermSymbols
a SchemaVariable is allowed to match is specified by their type and sort. If
a match fits these conditions can be checked using the method
isCompatible(TermSymbol t)
|
| SortedSchemaVariable | | protected SortedSchemaVariable(Name name, Class matchType, Sort sort, boolean listSV)(Code) | | creates a new SchemaVariable. That is used as placeholder for TermSymbols
of a certain type.
Parameters:
name - the Name of the SchemaVariable
Parameters:
matchType - Class representing the type of symbols that can be matched
Parameters:
sort - the Sort of the SchemaVariable and the matched type
Parameters:
listSV - a boolean which is true iff the schemavariable is allowed tomatch a list of syntactical elements |
| addInstantiation | | protected MatchConditions addInstantiation(ProgramElement pe, MatchConditions matchCond, Services services)(Code) | | tries to add the pair (this,pe) to the match conditions. If
possible the resulting match conditions are returned, otherwise
null. Such an addition can fail, e.g. if already a pair
(this,x) exists where x<>pe
|
| addInstantiation | | protected MatchConditions addInstantiation(Term term, MatchConditions matchCond, Services services)(Code) | | tries to add the pair (this,term) to the match conditions. If
successful the resulting conditions are returned, otherwise null. Failure
is possible e.g. if this schemavariable has been already matched to a
term t2 which is not unifiable with the given term.
|
| isStrict | | public boolean isStrict()(Code) | | true if the schemavariable has the strict modifier which forcesthe instantiation to have exact the same sort as theschemavariable (or if the sv is of generic sort - theinstantiation of the generic sort) |
| match | | public MatchConditions match(SVSubstitute subst, MatchConditions mc, Services services)(Code) | | checks if this schemavariable matches element subst with
respect to the given conditions and returns the resulting match
conditions (or null if the match is not possible)
Parameters:
subst - the SVSubstitute to be matched
Parameters:
mc - the MatchConditions posing restrictions on the variables to bematched
Parameters:
services - the Services with additional information about the context(e.g. type hierarchy) the resulting MatchConditions |
|
|