Data.Logic.ATP.Pretty

Documentation

(<>) :: Monoid m => m -> m -> m infixr 6

An infix synonym for mappend.

Since: 4.5.0.0

class Pretty a where

Pretty printing class. The precedence level is used in a similar way as in the Show class. Minimal complete definition is either pPrintPrec or pPrint.

Minimal complete definition

pPrintPrec | pPrint

Methods

pPrintPrec :: PrettyLevel -> Rational -> a -> Doc

pPrint :: a -> Doc

Instances

Pretty Bool

Pretty Char

Pretty Double

Pretty Float

Pretty Int

Pretty Integer

Pretty Ordering

Pretty ()

Pretty FName

Pretty V

Pretty Predicate

Pretty Depth

Pretty Prop

Pretty Atom

Pretty Function

Pretty K

Pretty a => Pretty [a]

Pretty a => Pretty (Maybe a)

IsAtom atom => Pretty (LFormula atom)

Pretty a => Pretty (JL a)

Pretty atom => Pretty (TruthTable atom)

IsAtom atom => Pretty (PFormula atom)

(Num a, Show a) => Pretty (Knows a)

(Pretty a, Pretty b) => Pretty (Either a b)

(Pretty a, Pretty b) => Pretty (a, b)

IsTerm (Term function v) => Pretty (Term function v)

(IsPredicate predicate, IsTerm term) => Pretty (FOLAP predicate term)

(HasApply (FOL predicate term), HasEquate (FOL predicate term), IsTerm term) => Pretty (FOL predicate term)

(HasApply atom, IsTerm term, (~) * term (TermOf atom), (~) * v (TVarOf term)) => Pretty (QFormula v atom)

(Pretty a, Pretty b, Pretty c) => Pretty (a, b, c)

(Pretty a, Pretty b, Pretty c, Pretty d) => Pretty (a, b, c, d)

(Pretty a, Pretty b, Pretty c, Pretty d, Pretty e) => Pretty (a, b, c, d, e)

(Pretty a, Pretty b, Pretty c, Pretty d, Pretty e, Pretty f) => Pretty (a, b, c, d, e, f)

(Pretty a, Pretty b, Pretty c, Pretty d, Pretty e, Pretty f, Pretty g) => Pretty (a, b, c, d, e, f, g)

(Pretty a, Pretty b, Pretty c, Pretty d, Pretty e, Pretty f, Pretty g, Pretty h) => Pretty (a, b, c, d, e, f, g, h)

module Text.PrettyPrint.HughesPJClass

data Associativity

Constructors

InfixL

InfixR

InfixN

InfixA

Instances

Show Associativity

type Precedence = forall a. Num a => a

Use the same precedence type as the pretty package

class HasFixity x where

A class to extract the fixity of a formula so they can be properly parenthesized.

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. Hopefully, we can generate formulas so that an associative operator with left associative fixity direction appears as (a+b)+c rather than a+(b+c).

Minimal complete definition

Nothing

Methods

precedence :: x -> Precedence

associativity :: x -> Associativity

Instances

HasFixity Prop

HasFixity Atom

IsAtom atom => HasFixity (LFormula atom)

HasFixity a => HasFixity (JL a)

IsAtom atom => HasFixity (PFormula atom)

Num a => HasFixity (Knows a)

(IsFunction function, IsVariable v) => HasFixity (Term function v)

HasFixity (FOLAP predicate term)

(IsPredicate predicate, IsTerm term) => HasFixity (FOL predicate term)

IsQuantified (QFormula v atom) => HasFixity (QFormula v atom)

data Side

What side of the parent formula are we rendering?

Constructors

Top

LHS

RHS

Unary

Instances

Show Side

testParen :: (Eq a, Ord a, Num a) => Side -> a -> a -> Associativity -> Bool

Decide whether to parenthesize based on which side of the parent binary operator we are rendering, the parent operator's precedence, and the precedence and associativity of the operator we are rendering. testParen :: Side -> Precedence -> Precedence -> Associativity -> Bool

assertEqual'

Arguments

:: (?loc :: CallStack, Eq a, Pretty a)

=> String

The message prefix

-> a

The expected value

-> a

The actual value

-> Assertion

Version of assertEqual that uses the pretty printer instead of show.

testEquals :: String -> ExpQ

leafPrec :: Num a => a

boolPrec :: Num a => a

notPrec :: Num a => a

atomPrec :: Num a => a

andPrec :: Num a => a

orPrec :: Num a => a

impPrec :: Num a => a

iffPrec :: Num a => a

quantPrec :: Num a => a

eqPrec :: Num a => a

pAppPrec :: Num a => a