Data.Logic.Classes.Pretty

Documentation

class Pretty x where

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.

Methods

pretty :: x -> Doc

Instances

Pretty Bool

Pretty String

Pretty BinOp

Pretty Prop

Pretty Function

Pretty FOL

Pretty TermType

Pretty PredName

Pretty FOLEQ

(PropositionalFormula (PropForm atom) atom, Pretty atom, HasFixity atom) => Pretty (PropForm atom)

(Pretty atom, HasFixity atom, Ord atom) => Pretty (Formula atom)

Pretty (Atom N)

(Pretty atom, HasFixity atom, Ord atom) => Pretty (Formula atom)

(Pretty p, Ord p) => Pretty (PredicateName p)

FirstOrderFormula (Formula a) a String => Pretty (Formula a)

(Variable v, Pretty v, Predicate p, Pretty p, Function f v, Pretty f) => Pretty (Predicate p (PTerm v f))

(Formula (NormalSentence v p f) (NormalSentence v p f), Variable v, Predicate p, Function f v, Combinable (NormalSentence v p f)) => Pretty (NormalSentence v p f)

(FirstOrderFormula (Sentence v p f) (Sentence v p f) v, Variable v, Predicate p, Function f v) => Pretty (Sentence v p f)

(Formula (Formula v p f) (Predicate p (PTerm v f)), Variable v, Predicate p, Function f v) => Pretty (Formula v p f)

(Formula (Formula v p f) (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f)), Pretty v, Show v, Variable v, Pretty p, Show p, Predicate p, Pretty f, Show f, Function f v) => Pretty (Formula v p f)

class HasFixity x where

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.

Methods

fixity :: x -> Fixity

Instances

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 Fixity

Constructors

Fixity Int FixityDirection

Instances

Eq Fixity

Data Fixity

Show Fixity

Typeable Fixity

data FixityDirection

Constructors

InfixL

InfixR

InfixN

Instances

Eq FixityDirection

Data FixityDirection

Show FixityDirection

Typeable FixityDirection

topFixity :: Fixity

This is used as the initial value for the parent fixity.

botFixity :: Fixity

This is used as the fixity for things that never need parenthesization, such as function application.