Copyright	(c) Evgenii Kotelnikov 2019-2021
License	GPL-3
Maintainer	evgeny.kotelnikov@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

ATP.Pretty.FOL

Contents

Orphan instances

Description

Pretty-printers for formulas, theorems and proofs.

Synopsis

class Pretty a where
- pretty :: a -> Doc
- prettyList :: [a] -> Doc
pprint :: Pretty a => a -> IO ()
hprint :: Pretty a => Handle -> a -> IO ()

Documentation

class Pretty a where #

The member prettyList is only used to define the instance Pretty a => Pretty [a]. In normal circumstances only the pretty function is used.

Minimal complete definition

pretty

Methods

pretty :: a -> Doc #

prettyList :: [a] -> Doc #

Instances

Instances details

Pretty Bool
Instance details Defined in Text.PrettyPrint.ANSI.Leijen.Internal Methods pretty :: Bool -> Doc # prettyList :: [Bool] -> Doc #
Pretty Char
Instance details Defined in Text.PrettyPrint.ANSI.Leijen.Internal Methods pretty :: Char -> Doc # prettyList :: [Char] -> Doc #
Pretty Double
Instance details Defined in Text.PrettyPrint.ANSI.Leijen.Internal Methods pretty :: Double -> Doc # prettyList :: [Double] -> Doc #
Pretty Float
Instance details Defined in Text.PrettyPrint.ANSI.Leijen.Internal Methods pretty :: Float -> Doc # prettyList :: [Float] -> Doc #
Pretty Int
Instance details Defined in Text.PrettyPrint.ANSI.Leijen.Internal Methods pretty :: Int -> Doc # prettyList :: [Int] -> Doc #
Pretty Integer
Instance details Defined in Text.PrettyPrint.ANSI.Leijen.Internal Methods pretty :: Integer -> Doc # prettyList :: [Integer] -> Doc #
Pretty ()
Instance details Defined in Text.PrettyPrint.ANSI.Leijen.Internal Methods pretty :: () -> Doc # prettyList :: [()] -> Doc #
Pretty Doc
Instance details Defined in Text.PrettyPrint.ANSI.Leijen.Internal Methods pretty :: Doc -> Doc # prettyList :: [Doc] -> Doc #
Pretty Error Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: Error -> Doc # prettyList :: [Error] -> Doc #
Pretty Theorem Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: Theorem -> Doc # prettyList :: [Theorem] -> Doc #
Pretty LogicalExpression Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: LogicalExpression -> Doc # prettyList :: [LogicalExpression] -> Doc #
Pretty Formula Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: Formula -> Doc # prettyList :: [Formula] -> Doc #
Pretty Connective Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: Connective -> Doc # prettyList :: [Connective] -> Doc #
Pretty Quantifier Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: Quantifier -> Doc # prettyList :: [Quantifier] -> Doc #
Pretty Clauses Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: Clauses -> Doc # prettyList :: [Clauses] -> Doc #
Pretty Clause Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: Clause -> Doc # prettyList :: [Clause] -> Doc #
Pretty Literal Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: Literal -> Doc # prettyList :: [Literal] -> Doc #
Pretty PredicateSymbol Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: PredicateSymbol -> Doc # prettyList :: [PredicateSymbol] -> Doc #
Pretty Term Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: Term -> Doc # prettyList :: [Term] -> Doc #
Pretty FunctionSymbol Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: FunctionSymbol -> Doc # prettyList :: [FunctionSymbol] -> Doc #
Pretty Solution Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: Solution -> Doc # prettyList :: [Solution] -> Doc #
Pretty RuleName Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: RuleName -> Doc # prettyList :: [RuleName] -> Doc #
Pretty a => Pretty [a]
Instance details Defined in Text.PrettyPrint.ANSI.Leijen.Internal Methods pretty :: [a] -> Doc # prettyList :: [[a]] -> Doc #
Pretty a => Pretty (Maybe a)
Instance details Defined in Text.PrettyPrint.ANSI.Leijen.Internal Methods pretty :: Maybe a -> Doc # prettyList :: [Maybe a] -> Doc #
Pretty a => Pretty (Partial a) Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: Partial a -> Doc # prettyList :: [Partial a] -> Doc #
Pretty (Signed Literal) Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: Signed Literal -> Doc # prettyList :: [Signed Literal] -> Doc #
(Ord l, Pretty l) => Pretty (Refutation l) Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: Refutation l -> Doc # prettyList :: [Refutation l] -> Doc #
(Ord l, Pretty l) => Pretty (Derivation l) Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: Derivation l -> Doc # prettyList :: [Derivation l] -> Doc #
Pretty l => Pretty (Sequent l) Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: Sequent l -> Doc # prettyList :: [Sequent l] -> Doc #
Pretty l => Pretty (Inference l) Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: Inference l -> Doc # prettyList :: [Inference l] -> Doc #
Pretty l => Pretty (Rule l) Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: Rule l -> Doc # prettyList :: [Rule l] -> Doc #
(Pretty a, Pretty b) => Pretty (a, b)
Instance details Defined in Text.PrettyPrint.ANSI.Leijen.Internal Methods pretty :: (a, b) -> Doc # prettyList :: [(a, b)] -> Doc #
(Pretty a, Pretty b, Pretty c) => Pretty (a, b, c)
Instance details Defined in Text.PrettyPrint.ANSI.Leijen.Internal Methods pretty :: (a, b, c) -> Doc # prettyList :: [(a, b, c)] -> Doc #

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

Pretty print to the standard output.

hprint :: Pretty a => Handle -> a -> IO () Source #

Pretty print to an IO handle.

Orphan instances

Pretty Error Source #
Instance details Methods pretty :: Error -> Doc # prettyList :: [Error] -> Doc #
Pretty Theorem Source #
Instance details Methods pretty :: Theorem -> Doc # prettyList :: [Theorem] -> Doc #
Pretty LogicalExpression Source #
Instance details Methods pretty :: LogicalExpression -> Doc # prettyList :: [LogicalExpression] -> Doc #
Pretty Formula Source #
Instance details Methods pretty :: Formula -> Doc # prettyList :: [Formula] -> Doc #
Pretty Connective Source #
Instance details Methods pretty :: Connective -> Doc # prettyList :: [Connective] -> Doc #
Pretty Quantifier Source #
Instance details Methods pretty :: Quantifier -> Doc # prettyList :: [Quantifier] -> Doc #
Pretty Clauses Source #
Instance details Methods pretty :: Clauses -> Doc # prettyList :: [Clauses] -> Doc #
Pretty Clause Source #
Instance details Methods pretty :: Clause -> Doc # prettyList :: [Clause] -> Doc #
Pretty Literal Source #
Instance details Methods pretty :: Literal -> Doc # prettyList :: [Literal] -> Doc #
Pretty PredicateSymbol Source #
Instance details Methods pretty :: PredicateSymbol -> Doc # prettyList :: [PredicateSymbol] -> Doc #
Pretty Term Source #
Instance details Methods pretty :: Term -> Doc # prettyList :: [Term] -> Doc #
Pretty FunctionSymbol Source #
Instance details Methods pretty :: FunctionSymbol -> Doc # prettyList :: [FunctionSymbol] -> Doc #
Pretty Solution Source #
Instance details Methods pretty :: Solution -> Doc # prettyList :: [Solution] -> Doc #
Pretty RuleName Source #
Instance details Methods pretty :: RuleName -> Doc # prettyList :: [RuleName] -> Doc #
Pretty a => Pretty (Partial a) Source #
Instance details Methods pretty :: Partial a -> Doc # prettyList :: [Partial a] -> Doc #
Pretty (Signed Literal) Source #
Instance details Methods pretty :: Signed Literal -> Doc # prettyList :: [Signed Literal] -> Doc #
(Ord l, Pretty l) => Pretty (Refutation l) Source #
Instance details Methods pretty :: Refutation l -> Doc # prettyList :: [Refutation l] -> Doc #
(Ord l, Pretty l) => Pretty (Derivation l) Source #
Instance details Methods pretty :: Derivation l -> Doc # prettyList :: [Derivation l] -> Doc #
Pretty l => Pretty (Sequent l) Source #
Instance details Methods pretty :: Sequent l -> Doc # prettyList :: [Sequent l] -> Doc #
Pretty l => Pretty (Inference l) Source #
Instance details Methods pretty :: Inference l -> Doc # prettyList :: [Inference l] -> Doc #
Pretty l => Pretty (Rule l) Source #
Instance details Methods pretty :: Rule l -> Doc # prettyList :: [Rule l] -> Doc #