Notation.CastFunction, Notation.CharLiteral, Notation.Constant, Notation.ElementaryUpdateNotation, Notation.ElementOfNotation, Notation.FunctionNotation, Notation.HeapConstructorNotation, Notation.IfThenElse, Notation.Infix, Notation.LabelNotation, Notation.ModalityNotation, Notation.ModalSVNotation, Notation.NumLiteral, Notation.ObserverNotation, Notation.ParallelUpdateNotation, Notation.Postfix, Notation.Prefix, Notation.Quantifier, Notation.SchemaVariableNotation, Notation.SelectNotation, Notation.SeqConcatNotation, Notation.SeqGetNotation, Notation.SeqSingletonNotation, Notation.SingletonNotation, Notation.StoreNotation, Notation.Subst, Notation.UpdateApplicationNotation, Notation.VariableNotation
Modifier and Type | Field and Description |
---|---|
private Function |
charLiteral |
private Function |
seqConcat |
private Function |
seqSingleton |
Constructor and Description |
---|
SeqConcatNotation(Function seqConcat,
Function seqSingleton,
Function charLiteral) |
Modifier and Type | Method and Description |
---|---|
private boolean |
isCharLiteralSequence(Term t) |
private boolean |
isCharLiteralSequenceHelp(Term t) |
void |
print(Term t,
LogicPrinter sp)
Print a term to a
LogicPrinter . |
private java.lang.String |
printStringTerm(Term t) |
getPriority, printContinuingBlock
private final Function seqSingleton
private final Function seqConcat
private final Function charLiteral
private java.lang.String printStringTerm(Term t)
public void print(Term t, LogicPrinter sp) throws java.io.IOException
Notation
LogicPrinter
. Concrete subclasses override
this to call one of the printXYZTerm
of
LogicPrinter
, which do the layout.private boolean isCharLiteralSequence(Term t)
private boolean isCharLiteralSequenceHelp(Term t)