logic-classes-1.5.3: Framework for propositional and first order logic, theorem proving

Safe HaskellNone
LanguageHaskell98

Data.Logic.Classes.Pretty

Synopsis

Documentation

class Pretty x where Source

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 Source

Instances

class HasFixity x where Source

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 Source

Instances

data Fixity :: *

Constructors

Fixity Int FixityDirection 

Instances

data FixityDirection :: *

Constructors

InfixL 
InfixR 
InfixN 

Instances

Eq FixityDirection 
Data FixityDirection 
Ord FixityDirection 
Show FixityDirection 
Generic FixityDirection 
type Rep FixityDirection = D1 D1FixityDirection ((:+:) (C1 C1_0FixityDirection U1) ((:+:) (C1 C1_1FixityDirection U1) (C1 C1_2FixityDirection U1))) 

topFixity :: Fixity Source

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

botFixity :: Fixity Source

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