Safe Haskell | None |
---|
Documentation
The intent of this class is to be similar to Show, but only one way, with no corresponding Read class. It doesn't really belong here in logic-classes. To put something in a pretty printing class implies that there is only one way to pretty print it, which is not an assumption made by Text.PrettyPrint. But in practice this is often good enough.
A class used to do proper parenthesization of formulas. If we
nest a higher precedence formula inside a lower one parentheses can
be omitted. Because |
has lower precedence than &
, the formula
a | (b & c)
appears as a | b & c
, while (a | b) & c
appears
unchanged. (Name Precedence chosen because Fixity was taken.)
The second field of Fixity is the FixityDirection, which can be
left, right, or non. A left associative operator like /
is
grouped left to right, so parenthese can be omitted from (a b)
c
but not from a (b c)
. It is a syntax error to omit
parentheses when formatting a non-associative operator.
The Haskell FixityDirection type is concerned with how to interpret
a formula formatted in a certain way, but here we are concerned
with how to format a formula given its interpretation. As such,
one case the Haskell type does not capture is whether the operator
follows the associative law, so we can omit parentheses in an
expression such as a & b & c
.
HasFixity String | |
HasFixity Prop | |
HasFixity FOL | |
HasFixity FOLEQ | |
(PropositionalFormula (PropForm atom) atom, HasFixity atom) => HasFixity (PropForm atom) | |
(Pretty atom, HasFixity atom, Ord atom) => HasFixity (Formula atom) | |
HasFixity (Atom N) | |
(Pretty atom, HasFixity atom, Ord atom) => HasFixity (Formula atom) | |
HasFixity (Formula FOLEQ) | |
HasFixity (Predicate p term) | |
(Formula (NormalSentence v p f) (NormalSentence v p f), Combinable (NormalSentence v p f), Predicate p, Function f v, Variable v) => HasFixity (NormalSentence v p f) | |
(Formula (Sentence v p f) (Sentence v p f), Predicate p, Function f v, Variable v) => HasFixity (Sentence v p f) | |
(Formula (Formula v p f) (Predicate p (PTerm v f)), Predicate p, Variable v, Function f v, HasFixity (Predicate p (PTerm v f))) => HasFixity (Formula v p f) | |
(Predicate p, Function f v) => HasFixity (Formula v p f) |
data FixityDirection