public final class TermLabelSV extends AbstractSV implements SchemaVariable, TermLabel
Modifier | Constructor and Description |
---|---|
protected |
TermLabelSV(Name name) |
Modifier and Type | Method and Description |
---|---|
int |
arity()
the arity of this operator
|
boolean |
bindVarsAt(int n)
Tells whether the operator binds variables at the n-th subterm.
|
java.lang.Object |
getChild(int i)
Retrieves the i-th parameter object of this term label.
|
int |
getChildCount()
Gets the number of parameters of this term label.
|
boolean |
isRigid()
Tells whether the operator is rigid.
|
Name |
name()
returns the name of this element
|
java.lang.String |
proofToString()
Creates a parseable string representation of the declaration of the
schema variable.
|
java.lang.String |
toString() |
boolean |
validTopLevel(Term term) |
void |
validTopLevelException(Term term)
Checks whether the top level structure of the given @link Term
is syntactically valid, given the assumption that the top level
operator of the term is the same as this Operator.
|
protected ImmutableArray<java.lang.Boolean> |
whereToBind() |
isStrict, toString
additionalValidTopLevel, argSort, argSorts, sort, sort
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
isStrict
argSort, argSorts, sort
arity, bindVarsAt, isRigid, sort, validTopLevelException
isProofRelevant, removeIrrelevantLabels, removeIrrelevantLabels
protected TermLabelSV(Name name)
public java.lang.String proofToString()
SchemaVariable
proofToString
in interface SchemaVariable
public java.lang.String toString()
public boolean validTopLevel(Term term)
validTopLevel
in interface Operator
Term
is valid, i.e. its parameters and types are correct.public java.lang.Object getChild(int i)
TermLabel
A term label may have structure, i.e. can be parameterized.
public int getChildCount()
TermLabel
getChildCount
in interface TermLabel
protected final ImmutableArray<java.lang.Boolean> whereToBind()
public final Name name()
Named
public final int arity()
Operator
public final boolean bindVarsAt(int n)
Operator
bindVarsAt
in interface Operator
public final boolean isRigid()
Operator
public void validTopLevelException(Term term) throws TermCreationException
Operator
validTopLevelException
in interface Operator
TermCreationException
- if a construction error was recogniseCopyright © 2003-2019 The KeY-Project.