| java.lang.Object
 de.uka.ilkd.key.pp.NotationInfo
| NotationInfo | | public class NotationInfo (Code) | |
Stores the mapping from operators to
Notation s. Each
Notation represents the concrete syntax for some
de.uka.ilkd.key.logic.op.Operator . The
LogicPrinter asks the NotationInfo to find out which Notation to use for a given term.
The Notation associated with an operator might change. New Notations can
be added.
Support for infix notations in case of function symbols like
+, -, *, /, <, >,
etc. is added by class
de.uka.ilkd.key.pp.PresentationFeatures (that has
historical reasons)
The next lines describe a general rule how to determine priorities and
associativities:
One thing we need to know from the pretty printer:
Given a term t containg s as proper subterm.
Then s is printed in parentheses when the priority of the
top level symbol of s is strict less than the associativity of the
position where s occurs. For example:
Let the priority of AND be 30 and the associativities for each
of its subterms be 40; ORs priority is 20 and the associativites are
both 30 then
- formula (p & q) | r is pretty printed as p & q | r
as the priority of & is 30 which is (greater or) equal than the
associativity of ORs left subterm which is 30.
- In contrast the formula p & (q | r) is pretty printed as
p & (q | r) as the priority of OR is 20 which is less than
the associativity of ANDs left subterm, which is 40.
A general rule to determine the correct priority and associativity is to use:
Grammar rules whose derivation delivers a syntactical correct logic term should follow
a standard numbering scheme, which is used as indicator for priorities and associativites,
e.g.
by simply reading the grammar rule
term60 ::= term70 (IMP term70)?
we get the priority of IMP, which is 60. The associativities
of IMPs subterms are not much more difficult to determine, namely
the left subterm has associativity 70 and in this case its the same
for the right subterm (70).
There are exceptional cases for
- infix function symbols that are left associative e.g.
-, +
term90 ::= term100 (PLUS term100)*
then the associative for the right subterm is increased by 1,
i.e. here we have a priority of 90 for PLUS as infix operator,
a left associativity of 100 and a right associativity of 101
- update and substituition terms: for them their associativity is
determined dynamically by the pretty printer depending if it is applied on a
formula or term. In principal there should be two different
rules in the parser as then we could reuse the general rule from above, but
there are technical reasons which causes this exception.
- some very few rules do not follow the usual parser design
e.g. like
R_PRIO ::= SubRule_ASS1 | SubRule_ASS2
where
SubRule_ASS2 ::= OP SubRule_ASS1
Most of these few rules could in general be rewritten to fit the usual scheme
e.g. as
R_PRIO ::= (OP)? SubRule_ASS1
using the priorities and associativities of the so rewritten rules
(instead of rewriting them actually) is a way to cope with them.
|
| Constructor Summary | |
| public | NotationInfo()
Create a new NotationInfo. |
| Method Summary | |
| public void | createCharLitNotation(Operator op)
Registers a character literal notation for a given operator. | | public void | createConstantNotation(String internalName, String token)
Used for OCL Simplification. | | public void | createInfixNotation(Operator op, String token)
| | public void | createInfixNotation(Operator op, String token, int prio, int lass, int rass)
| | final public static NotationInfo | createInstance()
Factory method: creates a new NotationInfo instance. | | public void | createNumLitNotation(Operator op)
Registers a number literal notation for a given operator. | | public void | createOCLCollOpBoundVarNotation(String token)
Used for OCL Simplification. | | public void | createOCLCollOpNotation(String token)
Used for OCL Simplification. | | public void | createOCLCollectionNotation(String internalName, String token)
Used for OCL Simplification. | | public void | createOCLDotOpNotation(String token)
Used for OCL Simplification. | | public void | createOCLIfNotation(String token)
Used for OCL Simplification. | | public void | createOCLInfixNotation(String internalName, String token, int prio, int assLeft, int assRight)
Used for OCL Simplification. | | public void | createOCLInvariantNotation(String token)
Used for OCL Simplification. | | public void | createOCLIterateNotation(String token)
Used for OCL Simplification. | | public void | createOCLListOfInvariantsNotation(String token)
Used for OCL Simplification. | | public void | createOCLPrefixNotation(String internalName, String token, int prio, int ass)
Used for OCL Simplification. | | public void | createOCLWrapperNotation(String token)
Used for OCL Simplification. | | public void | createPrefixNotation(Operator op, String token)
| | public void | createStringLitNotation(Operator op, Operator eps)
| | public AbbrevMap | getAbbrevMap()
| | public Notation | getNotation(Operator op, Services services)
Get the Notation for a given Operator. | | public void | setAbbrevMap(AbbrevMap am)
| | public void | setBackToDefault()
Set all notations back to default. |
| NotationInfo | | public NotationInfo()(Code) | | Create a new NotationInfo. Do not call this constructor
directly. Use the factory method
createInstance instead.
|
| createCharLitNotation | | public void createCharLitNotation(Operator op)(Code) | | Registers a character literal notation for a given operator.
This is done for the `C' operator which marks character literals.
A term C(3(2(#))) gets printed simply as
the character corresponding to the unicode value 23 (really 23
and not 32, see integer literals)
Parameters:
op - the operator |
| createConstantNotation | | public void createConstantNotation(String internalName, String token)(Code) | | Used for OCL Simplification.
Syntax for self, true, false, Set{}, etc.
|
| createInfixNotation | | public void createInfixNotation(Operator op, String token)(Code) | | Registers an infix notation for a given operator
Parameters:
op - the operator
Parameters:
token - the string representing the operator |
| createInfixNotation | | public void createInfixNotation(Operator op, String token, int prio, int lass, int rass)(Code) | | Registers an infix notation for a given operator
with given priority and associativity
Parameters:
op - the operator
Parameters:
token - the string representing the operator |
| createInstance | | final public static NotationInfo createInstance()(Code) | | Factory method: creates a new NotationInfo instance. The
actual implementation depends on system properties or service
entries.
|
| createNumLitNotation | | public void createNumLitNotation(Operator op)(Code) | | Registers a number literal notation for a given operator.
This is done for the `Z' operator which marks number literals.
A term Z(3(2(#))) gets printed simply as
23.
Parameters:
op - the operator |
| createOCLCollOpBoundVarNotation | | public void createOCLCollOpBoundVarNotation(String token)(Code) | | Used for OCL Simplification.
Syntax for forAll(), exists(), etc.
|
| createOCLCollOpNotation | | public void createOCLCollOpNotation(String token)(Code) | | Used for OCL Simplification.
Syntax for size(), includes(), etc.
|
| createOCLCollectionNotation | | public void createOCLCollectionNotation(String internalName, String token)(Code) | | Used for OCL Simplification.
Syntax for Set{...}, Bag{...}, and Sequence{...}.
|
| createOCLDotOpNotation | | public void createOCLDotOpNotation(String token)(Code) | | Used for OCL Simplification.
Syntax for supertypes(), oclIsNew(), etc.
|
| createOCLIfNotation | | public void createOCLIfNotation(String token)(Code) | | Used for OCL Simplification.
Syntax for if-then-else-endif.
|
| createOCLInfixNotation | | public void createOCLInfixNotation(String internalName, String token, int prio, int assLeft, int assRight)(Code) | | Used for OCL Simplification.
Syntax for "and", "or", "+", "<", etc.
|
| createOCLInvariantNotation | | public void createOCLInvariantNotation(String token)(Code) | | Used for OCL Simplification.
|
| createOCLIterateNotation | | public void createOCLIterateNotation(String token)(Code) | | Used for OCL Simplification.
Syntax for iterate().
|
| createOCLListOfInvariantsNotation | | public void createOCLListOfInvariantsNotation(String token)(Code) | | Used for OCL Simplification.
|
| createOCLPrefixNotation | | public void createOCLPrefixNotation(String internalName, String token, int prio, int ass)(Code) | | Used for OCL Simplification.
Syntax for "not" and "-".
|
| createOCLWrapperNotation | | public void createOCLWrapperNotation(String token)(Code) | | Used for OCL Simplification.
|
| createPrefixNotation | | public void createPrefixNotation(Operator op, String token)(Code) | | Registers a prefix notation for a given operator
Parameters:
op - the operator
Parameters:
token - the string representing the operator |
| getNotation | | public Notation getNotation(Operator op, Services services)(Code) | | Get the Notation for a given Operator.
If no notation is registered, a Function notation is returned.
|
| setBackToDefault | | public void setBackToDefault()(Code) | | Set all notations back to default.
|
|
|