| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Data.Logic.ATP.Pretty
Contents
- (<>) :: Monoid m => m -> m -> m
- class Pretty a where
- pPrintPrec :: PrettyLevel -> Rational -> a -> Doc
- pPrint :: a -> Doc
- module Text.PrettyPrint.HughesPJClass
- data Associativity
- type Precedence = forall a. Num a => a
- class HasFixity x where
- data Side
- testParen :: (Eq a, Ord a, Num a) => Side -> a -> a -> Associativity -> Bool
- assertEqual' :: (?loc :: CallStack, Eq a, Pretty a) => String -> a -> a -> Assertion
- 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
Documentation
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
Instances
data Associativity Source #
Instances
type Precedence = forall a. Num a => a Source #
Use the same precedence type as the pretty package
class HasFixity x where Source #
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).
Instances
| HasFixity Prop Source # | |
| HasFixity Atom Source # | |
| IsAtom atom => HasFixity (LFormula atom) Source # | |
| HasFixity a => HasFixity (JL a) Source # | |
| IsAtom atom => HasFixity (PFormula atom) Source # | |
| Num a => HasFixity (Knows a) Source # | |
| (IsFunction function, IsVariable v) => HasFixity (Term function v) Source # | |
| HasFixity (FOLAP predicate term) Source # | |
| (IsPredicate predicate, IsTerm term) => HasFixity (FOL predicate term) Source # | |
| IsQuantified (QFormula v atom) => HasFixity (QFormula v atom) Source # | |
What side of the parent formula are we rendering?
testParen :: (Eq a, Ord a, Num a) => Side -> a -> a -> Associativity -> Bool Source #
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
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 Source #