public abstract class Notation
extends java.lang.Object
NotationInfo
class associates a Notation with every Operator
. The various inner classes of this class
represent different kinds of concrete syntax, like prefix, infix, postfix,
function style, attribute style, etc.Modifier and Type | Class and Description |
---|---|
static class |
Notation.CastFunction
The standard concrete syntax for casts.
|
(package private) static class |
Notation.CharLiteral
The standard concrete syntax for the character literal indicator `C'.
|
static class |
Notation.Constant
The standard concrete syntax for constants like true and false.
|
static class |
Notation.ElementaryUpdateNotation
The standard concrete syntax for elementary updates.
|
static class |
Notation.ElementOfNotation
The standard concrete syntax for the element of operator.
|
static class |
Notation.FunctionNotation
The standard concrete syntax for function and predicate terms.
|
static class |
Notation.HeapConstructorNotation
The standard concrete syntax for heap constructors.
|
static class |
Notation.IfThenElse
The standard concrete syntax for conditional terms
if (phi) (t1) (t2) . |
static class |
Notation.Infix
The standard concrete syntax for infix operators.
|
static class |
Notation.LabelNotation |
static class |
Notation.ModalityNotation
The standard concrete syntax for DL modalities box and diamond.
|
static class |
Notation.ModalSVNotation
The concrete syntax for DL modalities represented with a
SchemaVariable.
|
(package private) static class |
Notation.NumLiteral
The standard concrete syntax for the number literal indicator `Z'.
|
(package private) static class |
Notation.ObserverNotation
The standard concrete syntax for observer function terms.
|
static class |
Notation.ParallelUpdateNotation
The standard concrete syntax for parallel updates
|
static class |
Notation.Postfix
The standard concrete syntax for length.
|
static class |
Notation.Prefix
The standard concrete syntax for prefix operators.
|
static class |
Notation.Quantifier
The standard concrete syntax for quantifiers.
|
static class |
Notation.SchemaVariableNotation |
static class |
Notation.SelectNotation
The standard concrete syntax for select.
|
static class |
Notation.SeqConcatNotation |
static class |
Notation.SeqGetNotation |
static class |
Notation.SeqSingletonNotation
The standard concrete syntax for sequence singletons.
|
static class |
Notation.SingletonNotation
The standard concrete syntax for singleton sets.
|
static class |
Notation.StoreNotation
The standard concrete syntax for store.
|
static class |
Notation.Subst
The standard concrete syntax for substitution terms.
|
static class |
Notation.UpdateApplicationNotation
The standard concrete syntax for update application.
|
static class |
Notation.VariableNotation
The standard concrete syntax for all kinds of variables.
|
Modifier and Type | Field and Description |
---|---|
private int |
priority
The priority of this operator in the given concrete syntax.
|
Modifier | Constructor and Description |
---|---|
protected |
Notation(int priority)
Create a Notation with a given priority.
|
Modifier and Type | Method and Description |
---|---|
int |
getPriority()
get the priority of the term
|
abstract void |
print(Term t,
LogicPrinter sp)
Print a term to a
LogicPrinter . |
void |
printContinuingBlock(Term t,
LogicPrinter sp)
Print a term without beginning a new block.
|
private final int priority
protected Notation(int priority)
public final int getPriority()
public abstract void print(Term t, LogicPrinter sp) throws java.io.IOException
LogicPrinter
. Concrete subclasses override
this to call one of the printXYZTerm
of
LogicPrinter
, which do the layout.java.io.IOException
public void printContinuingBlock(Term t, LogicPrinter sp) throws java.io.IOException
LogicPrinter.printTermContinuingBlock(Term)
for the idea
behind this. The standard implementation just delegates to
print(Term,LogicPrinter)
java.io.IOException