public final class NotationInfo
extends java.lang.Object
Stores the mapping from operators to Notation
s. Each
Notation
represents the concrete syntax for some
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.
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
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
-, +
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
R_PRIO ::= SubRule_ASS1 | SubRule_ASS2where
SubRule_ASS2 ::= OP SubRule_ASS1Most of these few rules could in general be rewritten to fit the usual scheme e.g. as
R_PRIO ::= (OP)? SubRule_ASS1using the priorities and associativities of the so rewritten rules (instead of rewriting them actually) is a way to cope with them.
Modifier and Type | Field and Description |
---|---|
static boolean |
DEFAULT_HIDE_PACKAGE_PREFIX |
static boolean |
DEFAULT_PRETTY_SYNTAX |
static boolean |
DEFAULT_UNICODE_ENABLED
Whether the very fancy notation is enabled
in which Unicode characters for logical operators
are printed.
|
private boolean |
hidePackagePrefix |
private java.util.HashMap<java.lang.Object,Notation> |
notationTable
This maps operators and classes of operators to
Notation s. |
private boolean |
prettySyntax |
(package private) static int |
PRIORITY_AND |
(package private) static int |
PRIORITY_ARITH_STRONG |
(package private) static int |
PRIORITY_ARITH_WEAK |
(package private) static int |
PRIORITY_ATOM |
(package private) static int |
PRIORITY_BELOW_ARITH_STRONG |
(package private) static int |
PRIORITY_BELOW_ARITH_WEAK |
(package private) static int |
PRIORITY_BOTTOM |
(package private) static int |
PRIORITY_CAST |
(package private) static int |
PRIORITY_COMPARISON |
(package private) static int |
PRIORITY_EQUAL |
(package private) static int |
PRIORITY_EQUIVALENCE |
(package private) static int |
PRIORITY_IMP |
(package private) static int |
PRIORITY_LABEL |
(package private) static int |
PRIORITY_MODALITY |
(package private) static int |
PRIORITY_NEGATION |
(package private) static int |
PRIORITY_OR |
(package private) static int |
PRIORITY_POST_MODALITY |
(package private) static int |
PRIORITY_QUANTIFIER |
(package private) static int |
PRIORITY_TOP |
private AbbrevMap |
scm
Maps terms to abbreviations and reverse.
|
private boolean |
unicodeEnabled |
Constructor and Description |
---|
NotationInfo() |
Modifier and Type | Method and Description |
---|---|
private java.util.HashMap<java.lang.Object,Notation> |
createDefaultNotation()
Register the standard set of notations (that can be defined without
a services object).
|
private java.util.HashMap<java.lang.Object,Notation> |
createPrettyNotation(Services services)
Adds notations that can only be defined when a services object is
available.
|
private java.util.HashMap<java.lang.Object,Notation> |
createUnicodeNotation(Services services)
Add notations with Unicode symbols.
|
AbbrevMap |
getAbbrevMap() |
(package private) Notation |
getNotation(java.lang.Class<?> c) |
(package private) Notation |
getNotation(Operator op)
Get the Notation for a given Operator.
|
java.util.Map<java.lang.Object,Notation> |
getNotationTable() |
boolean |
isHidePackagePrefix() |
boolean |
isPrettySyntax() |
boolean |
isUnicodeEnabled() |
void |
refresh(Services services) |
void |
refresh(Services services,
boolean usePrettyPrinting,
boolean useUnicodeSymbols) |
void |
setAbbrevMap(AbbrevMap am) |
void |
setHidePackagePrefix(boolean b) |
static final int PRIORITY_TOP
static final int PRIORITY_EQUIVALENCE
static final int PRIORITY_IMP
static final int PRIORITY_OR
static final int PRIORITY_AND
static final int PRIORITY_NEGATION
static final int PRIORITY_QUANTIFIER
static final int PRIORITY_MODALITY
static final int PRIORITY_POST_MODALITY
static final int PRIORITY_EQUAL
static final int PRIORITY_COMPARISON
static final int PRIORITY_ARITH_WEAK
static final int PRIORITY_BELOW_ARITH_WEAK
static final int PRIORITY_ARITH_STRONG
static final int PRIORITY_BELOW_ARITH_STRONG
static final int PRIORITY_CAST
static final int PRIORITY_ATOM
static final int PRIORITY_BOTTOM
static final int PRIORITY_LABEL
public static boolean DEFAULT_PRETTY_SYNTAX
public static boolean DEFAULT_UNICODE_ENABLED
public static boolean DEFAULT_HIDE_PACKAGE_PREFIX
private java.util.HashMap<java.lang.Object,Notation> notationTable
Notation
s. The idea is that we first look whether the operator has
a Notation registered. Otherwise, we see if there is one for the
class of the operator.private AbbrevMap scm
private boolean prettySyntax
private boolean unicodeEnabled
private boolean hidePackagePrefix
private java.util.HashMap<java.lang.Object,Notation> createDefaultNotation()
private java.util.HashMap<java.lang.Object,Notation> createPrettyNotation(Services services)
private java.util.HashMap<java.lang.Object,Notation> createUnicodeNotation(Services services)
services
- public void refresh(Services services)
public void refresh(Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols)
public AbbrevMap getAbbrevMap()
public void setAbbrevMap(AbbrevMap am)
Notation getNotation(java.lang.Class<?> c)
Notation getNotation(Operator op)
public boolean isPrettySyntax()
public boolean isUnicodeEnabled()
public boolean isHidePackagePrefix()
public void setHidePackagePrefix(boolean b)
public java.util.Map<java.lang.Object,Notation> getNotationTable()