twee-lib-2.1.3: An equational theorem prover

Safe HaskellNone
LanguageHaskell2010

Twee.Pretty

Contents

Description

Pretty-printing of terms and assorted other values.

Synopsis

Miscellaneous Pretty instances and utilities.

prettyPrint :: Pretty a => a -> IO () Source #

Print a value to the console.

pPrintEmpty :: Doc Source #

The empty document. Used to avoid name clashes with empty.

pPrintTuple :: [Doc] -> Doc Source #

Print a tuple of values.

pPrintSet :: [Doc] -> Doc Source #

Print a set of vlaues.

supply :: [String] -> [String] Source #

Generate a list of candidate names for pretty-printing.

Pretty-printing of terms.

class Pretty f => PrettyTerm f where Source #

A class for customising the printing of function symbols.

Methods

termStyle :: f -> TermStyle Source #

The style of the function symbol. Defaults to curried.

Instances

newtype TermStyle Source #

Defines how to print out a function symbol.

Constructors

TermStyle 

Fields

  • pPrintTerm :: forall a. Pretty a => PrettyLevel -> Rational -> Doc -> [a] -> Doc

    Renders a function application. Takes the following arguments in this order: Pretty-printing level, current precedence, pretty-printed function symbol and list of arguments to the function.

invisible :: TermStyle Source #

For operators like $ that should be printed as a blank space.

curried :: TermStyle Source #

For functions that should be printed curried.

uncurried :: TermStyle Source #

For functions that should be printed uncurried.

prefix :: TermStyle Source #

For prefix operators.

postfix :: TermStyle Source #

For postfix operators.

fixedArity :: Int -> TermStyle -> TermStyle Source #

A helper function that deals with under- and oversaturated applications.

implicitArguments :: Int -> TermStyle -> TermStyle Source #

A helper function that drops a certain number of arguments.

infixStyle :: Int -> TermStyle Source #

For infix operators.

tupleStyle :: TermStyle Source #

For tuples.

module Text.PrettyPrint.HughesPJClass

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 #

pPrintList :: PrettyLevel -> [a] -> Doc #

Instances

Pretty Bool 
Pretty Char 
Pretty Double 
Pretty Float 
Pretty Int 
Pretty Integer 
Pretty Ordering 
Pretty () 

Methods

pPrintPrec :: PrettyLevel -> Rational -> () -> Doc #

pPrint :: () -> Doc #

pPrintList :: PrettyLevel -> [()] -> Doc #

Pretty Id # 
Pretty a => Pretty [a] 

Methods

pPrintPrec :: PrettyLevel -> Rational -> [a] -> Doc #

pPrint :: [a] -> Doc #

pPrintList :: PrettyLevel -> [[a]] -> Doc #

Pretty a => Pretty (Maybe a) 
PrettyTerm f => Pretty (Model f) # 
PrettyTerm f => Pretty (Branch f) # 
PrettyTerm f => Pretty (Formula f) # 
PrettyTerm f => Pretty (Atom f) # 

Methods

pPrintPrec :: PrettyLevel -> Rational -> Atom f -> Doc #

pPrint :: Atom f -> Doc #

pPrintList :: PrettyLevel -> [Atom f] -> Doc #

Pretty f => Pretty (Extended f) # 
PrettyTerm f => Pretty (Equation f) # 
Function f => Pretty (Presentation f) # 
PrettyTerm f => Pretty (Axiom f) # 
PrettyTerm f => Pretty (Lemma f) # 
PrettyTerm f => Pretty (Derivation f) # 
Function f => Pretty (Proof f) # 
Function f => Pretty (Resulting f) # 
Function f => Pretty (Reduction f) # 
PrettyTerm f => Pretty (Rule f) # 

Methods

pPrintPrec :: PrettyLevel -> Rational -> Rule f -> Doc #

pPrint :: Rule f -> Doc #

pPrintList :: PrettyLevel -> [Rule f] -> Doc #

PrettyTerm f => Pretty (CriticalPair f) # 
Function f => Pretty (Active f) # 
Function f => Pretty (Message f) # 
(Pretty a, Pretty b) => Pretty (Either a b) 

Methods

pPrintPrec :: PrettyLevel -> Rational -> Either a b -> Doc #

pPrint :: Either a b -> Doc #

pPrintList :: PrettyLevel -> [Either a b] -> Doc #

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

Methods

pPrintPrec :: PrettyLevel -> Rational -> (a, b) -> Doc #

pPrint :: (a, b) -> Doc #

pPrintList :: PrettyLevel -> [(a, b)] -> Doc #

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

Methods

pPrintPrec :: PrettyLevel -> Rational -> (a, b, c) -> Doc #

pPrint :: (a, b, c) -> Doc #

pPrintList :: PrettyLevel -> [(a, b, c)] -> Doc #

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

Methods

pPrintPrec :: PrettyLevel -> Rational -> (a, b, c, d) -> Doc #

pPrint :: (a, b, c, d) -> Doc #

pPrintList :: PrettyLevel -> [(a, b, c, d)] -> Doc #

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

Methods

pPrintPrec :: PrettyLevel -> Rational -> (a, b, c, d, e) -> Doc #

pPrint :: (a, b, c, d, e) -> Doc #

pPrintList :: PrettyLevel -> [(a, b, c, d, e)] -> Doc #

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

Methods

pPrintPrec :: PrettyLevel -> Rational -> (a, b, c, d, e, f) -> Doc #

pPrint :: (a, b, c, d, e, f) -> Doc #

pPrintList :: PrettyLevel -> [(a, b, c, d, e, f)] -> Doc #

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

Methods

pPrintPrec :: PrettyLevel -> Rational -> (a, b, c, d, e, f, g) -> Doc #

pPrint :: (a, b, c, d, e, f, g) -> Doc #

pPrintList :: PrettyLevel -> [(a, b, c, d, e, f, g)] -> Doc #

(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) 

Methods

pPrintPrec :: PrettyLevel -> Rational -> (a, b, c, d, e, f, g, h) -> Doc #

pPrint :: (a, b, c, d, e, f, g, h) -> Doc #

pPrintList :: PrettyLevel -> [(a, b, c, d, e, f, g, h)] -> Doc #

Orphan instances

Pretty Doc Source # 
Pretty Var Source # 
(Eq a, Integral a, Pretty a) => Pretty (Ratio a) Source # 
Pretty a => Pretty (Set a) Source # 

Methods

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

pPrint :: Set a -> Doc #

pPrintList :: PrettyLevel -> [Set a] -> Doc #

Pretty f => Pretty (Fun f) Source # 

Methods

pPrintPrec :: PrettyLevel -> Rational -> Fun f -> Doc #

pPrint :: Fun f -> Doc #

pPrintList :: PrettyLevel -> [Fun f] -> Doc #

PrettyTerm f => Pretty (Term f) Source # 

Methods

pPrintPrec :: PrettyLevel -> Rational -> Term f -> Doc #

pPrint :: Term f -> Doc #

pPrintList :: PrettyLevel -> [Term f] -> Doc #

PrettyTerm f => Pretty (TermList f) Source # 
PrettyTerm f => Pretty (Subst f) Source # 
(Pretty k, Pretty v) => Pretty (Map k v) Source # 

Methods

pPrintPrec :: PrettyLevel -> Rational -> Map k v -> Doc #

pPrint :: Map k v -> Doc #

pPrintList :: PrettyLevel -> [Map k v] -> Doc #