de.uka.ilkd.key.pp

Class Notation

java.lang.Object

de.uka.ilkd.key.pp.Notation

Direct Known Subclasses:

CharListNotation, 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.SeqConcatNotation, Notation.SeqGetNotation, Notation.SeqSingletonNotation, Notation.SingletonNotation, Notation.Subst, Notation.UpdateApplicationNotation, Notation.VariableNotation

public abstract class Notation
extends java.lang.Object

Encapsulate the concrete syntax used to print a term. The 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.

Nested Class Summary

Nested Classes

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.

Field Summary

Fields

Modifier and Type	Field and Description
private int	priority The priority of this operator in the given concrete syntax.

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	Notation(int priority) Create a Notation with a given priority.

Method Summary

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.

Methods inherited from class java.lang.Object

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

Field Detail

priority

private final int priority

The priority of this operator in the given concrete syntax. This is used to determine whether parentheses are required around a subterm.

Constructor Detail

Notation

protected Notation(int priority)

Create a Notation with a given priority.

Method Detail

getPriority

public final int getPriority()

get the priority of the term

print

public abstract void print(Term t,
                           LogicPrinter sp)
                    throws java.io.IOException

Print a term to a LogicPrinter. Concrete subclasses override this to call one of the printXYZTerm of LogicPrinter, which do the layout.

Throws:

java.io.IOException

printContinuingBlock

public void printContinuingBlock(Term t,
                                 LogicPrinter sp)
                          throws java.io.IOException

Print a term without beginning a new block. See LogicPrinter.printTermContinuingBlock(Term)for the idea behind this. The standard implementation just delegates to print(Term,LogicPrinter)

Throws:

java.io.IOException