Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Logic.ATP

Synopsis

module Data.Logic.ATP.Lib
module Data.Logic.ATP.Pretty
module Data.Logic.ATP.Formulas
data Lit = L {
- lname :: String
}
class IsFormula lit => IsLiteral lit where
- naiveNegate :: lit -> lit
- foldNegation :: (lit -> r) -> (lit -> r) -> lit -> r
- foldLiteral' :: (lit -> r) -> (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
class IsLiteral formula => JustLiteral formula
data LFormula atom
negate :: IsLiteral formula => formula -> formula
negative :: IsLiteral formula => formula -> Bool
(.~.) :: IsLiteral formula => formula -> formula
(¬) :: IsLiteral formula => formula -> formula
negated :: IsLiteral formula => formula -> Bool
positive :: IsLiteral formula => formula -> Bool
foldLiteral :: JustLiteral lit => (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
onatomsLiteral :: JustLiteral lit => (AtomOf lit -> AtomOf lit) -> lit -> lit
overatomsLiteral :: JustLiteral lit => (AtomOf lit -> r -> r) -> lit -> r -> r
zipLiterals' :: (IsLiteral lit1, IsLiteral lit2) => (lit1 -> lit2 -> Maybe r) -> (lit1 -> lit2 -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (AtomOf lit1 -> AtomOf lit2 -> Maybe r) -> lit1 -> lit2 -> Maybe r
zipLiterals :: (JustLiteral lit1, JustLiteral lit2) => (lit1 -> lit2 -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (AtomOf lit1 -> AtomOf lit2 -> Maybe r) -> lit1 -> lit2 -> Maybe r
convertLiteral :: (JustLiteral lit1, IsLiteral lit2) => (AtomOf lit1 -> AtomOf lit2) -> lit1 -> lit2
convertToLiteral :: (IsLiteral formula, JustLiteral lit) => (formula -> lit) -> (AtomOf formula -> AtomOf lit) -> formula -> lit
precedenceLiteral :: JustLiteral lit => lit -> Precedence
associativityLiteral :: JustLiteral lit => lit -> Associativity
prettyLiteral :: JustLiteral lit => PrettyLevel -> Rational -> lit -> Doc
showLiteral :: JustLiteral lit => lit -> String
data Prop = P {
- pname :: String
}
class IsLiteral formula => IsPropositional formula where
- (.|.) :: formula -> formula -> formula
- (.&.) :: formula -> formula -> formula
- (.<=>.) :: formula -> formula -> formula
- (.=>.) :: formula -> formula -> formula
- foldPropositional' :: (formula -> r) -> (formula -> BinOp -> formula -> r) -> (formula -> r) -> (Bool -> r) -> (AtomOf formula -> r) -> formula -> r
- foldCombination :: (formula -> r) -> (formula -> formula -> r) -> (formula -> formula -> r) -> (formula -> formula -> r) -> (formula -> formula -> r) -> formula -> r
data BinOp
- = (:<=>:)
- | (:=>:)
- | (:&:)
- | (:|:)
class IsPropositional formula => JustPropositional formula
data TruthTable a = TruthTable [a] [TruthTableRow]
data PFormula atom
(==>) :: IsPropositional formula => formula -> formula -> formula
(⇒) :: IsPropositional formula => formula -> formula -> formula
(→) :: IsPropositional formula => formula -> formula -> formula
binop :: IsPropositional formula => formula -> BinOp -> formula -> formula
(⊃) :: IsPropositional formula => formula -> formula -> formula
(⇔) :: IsPropositional formula => formula -> formula -> formula
(<=>) :: IsPropositional formula => formula -> formula -> formula
(↔) :: IsPropositional formula => formula -> formula -> formula
(<==>) :: IsPropositional formula => formula -> formula -> formula
(∧) :: IsPropositional formula => formula -> formula -> formula
(·) :: IsPropositional formula => formula -> formula -> formula
(∨) :: IsPropositional formula => formula -> formula -> formula
foldPropositional :: JustPropositional pf => (pf -> BinOp -> pf -> r) -> (pf -> r) -> (Bool -> r) -> (AtomOf pf -> r) -> pf -> r
zipPropositional :: (JustPropositional pf1, JustPropositional pf2) => (pf1 -> BinOp -> pf1 -> pf2 -> BinOp -> pf2 -> Maybe r) -> (pf1 -> pf2 -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (AtomOf pf1 -> AtomOf pf2 -> Maybe r) -> pf1 -> pf2 -> Maybe r
convertPropositional :: (JustPropositional pf1, IsPropositional pf2) => (AtomOf pf1 -> AtomOf pf2) -> pf1 -> pf2
convertToPropositional :: (IsPropositional formula, JustPropositional pf) => (formula -> pf) -> (AtomOf formula -> AtomOf pf) -> formula -> pf
precedencePropositional :: JustPropositional pf => pf -> Precedence
associativityPropositional :: JustPropositional pf => pf -> Associativity
prettyPropositional :: forall pf. JustPropositional pf => Side -> PrettyLevel -> Rational -> pf -> Doc
showPropositional :: JustPropositional pf => Side -> Int -> pf -> ShowS
onatomsPropositional :: JustPropositional pf => (AtomOf pf -> AtomOf pf) -> pf -> pf
overatomsPropositional :: JustPropositional pf => (AtomOf pf -> r -> r) -> pf -> r -> r
eval :: JustPropositional pf => pf -> (AtomOf pf -> Bool) -> Bool
atoms :: IsFormula formula => formula -> Set (AtomOf formula)
onallvaluations :: Ord atom => (r -> r -> r) -> ((atom -> Bool) -> r) -> (atom -> Bool) -> Set atom -> r
truthTable :: JustPropositional pf => pf -> TruthTable (AtomOf pf)
tautology :: JustPropositional pf => pf -> Bool
unsatisfiable :: JustPropositional pf => pf -> Bool
satisfiable :: JustPropositional pf => pf -> Bool
psubst :: JustPropositional formula => Map (AtomOf formula) formula -> formula -> formula
dual :: JustPropositional pf => pf -> pf
psimplify :: IsPropositional formula => formula -> formula
psimplify1 :: IsPropositional formula => formula -> formula
nenf :: IsPropositional formula => formula -> formula
list_conj :: (Foldable t, IsFormula formula, IsPropositional formula) => t formula -> formula
list_disj :: (Foldable t, IsFormula formula, IsPropositional formula) => t formula -> formula
mk_lits :: (JustPropositional pf, Ord pf) => Set pf -> (AtomOf pf -> Bool) -> pf
allsatvaluations :: Ord atom => ((atom -> Bool) -> Bool) -> (atom -> Bool) -> Set atom -> [atom -> Bool]
dnfSet :: (JustPropositional pf, Ord pf) => pf -> pf
purednf :: (JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpdnf :: (JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
rawdnf :: IsPropositional formula => formula -> formula
dnf :: forall pf. (JustPropositional pf, Ord pf) => pf -> pf
purecnf :: (JustPropositional pf, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpcnf :: (JustPropositional pf, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
cnf' :: forall pf. (JustPropositional pf, Ord pf) => pf -> pf
cnf_ :: (IsPropositional pf, Ord pf, JustLiteral lit) => (AtomOf lit -> AtomOf pf) -> Set (Set lit) -> pf
trivial :: (Ord lit, IsLiteral lit) => Set lit -> Bool
testProp :: Test
data Knows a
mk_knows :: (IsPropositional formula, AtomOf formula ~ Knows a) => String -> a -> formula
mk_knows2 :: (IsPropositional formula, AtomOf formula ~ Knows a) => String -> a -> a -> formula
prime :: (IsPropositional formula, Ord formula, AtomOf formula ~ Knows Integer) => Integer -> formula
ramsey :: (IsPropositional pf, AtomOf pf ~ Knows Integer, Ord pf) => Integer -> Integer -> Integer -> pf
testPropExamples :: Test
module Data.Logic.ATP.DefCNF
module Data.Logic.ATP.DP
module Data.Logic.ATP.Term
module Data.Logic.ATP.Apply
module Data.Logic.ATP.Equate
module Data.Logic.ATP.Quantified
module Data.Logic.ATP.Parser
module Data.Logic.ATP.FOL
module Data.Logic.ATP.Skolem
module Data.Logic.ATP.Herbrand
module Data.Logic.ATP.Unif
tab :: (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Pretty formula, HasSkolem function, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => Maybe Depth -> formula -> Failing ((K, Map v term), Depth)
prawitz :: forall formula atom term function v. (IsFirstOrder formula, Ord formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => formula -> Int
testTableaux :: Test
module Data.Logic.ATP.Resolution
module Data.Logic.ATP.Prolog
module Data.Logic.ATP.Meson
module Data.Logic.ATP.Equal
data Mode
- = PageMode
- | ZigZagMode
- | LeftMode
- | OneLineMode
data Style = Style {
- mode :: Mode
- lineLength :: Int
- ribbonsPerLine :: Float
}
data TextDetails
- = Chr !Char
- | Str String
- | PStr String
data Doc
class Pretty a where
- pPrintPrec :: PrettyLevel -> Rational -> a -> Doc
- pPrint :: a -> Doc
- pPrintList :: PrettyLevel -> [a] -> Doc
newtype PrettyLevel = PrettyLevel Int
text :: String -> Doc
first :: Doc -> Doc -> Doc
empty :: Doc
char :: Char -> Doc
parens :: Doc -> Doc
(<+>) :: Doc -> Doc -> Doc
isEmpty :: Doc -> Bool
space :: Doc
integer :: Integer -> Doc
float :: Float -> Doc
braces :: Doc -> Doc
brackets :: Doc -> Doc
semi :: Doc
comma :: Doc
colon :: Doc
ptext :: String -> Doc
sizedText :: Int -> String -> Doc
zeroWidthText :: String -> Doc
equals :: Doc
lparen :: Doc
rparen :: Doc
lbrack :: Doc
rbrack :: Doc
lbrace :: Doc
rbrace :: Doc
int :: Int -> Doc
double :: Double -> Doc
rational :: Rational -> Doc
quotes :: Doc -> Doc
doubleQuotes :: Doc -> Doc
maybeParens :: Bool -> Doc -> Doc
maybeBrackets :: Bool -> Doc -> Doc
maybeBraces :: Bool -> Doc -> Doc
maybeQuotes :: Bool -> Doc -> Doc
maybeDoubleQuotes :: Bool -> Doc -> Doc
reduceDoc :: Doc -> RDoc
hcat :: [Doc] -> Doc
hsep :: [Doc] -> Doc
vcat :: [Doc] -> Doc
nest :: Int -> Doc -> Doc
hang :: Doc -> Int -> Doc -> Doc
punctuate :: Doc -> [Doc] -> [Doc]
($$) :: Doc -> Doc -> Doc
($+$) :: Doc -> Doc -> Doc
sep :: [Doc] -> Doc
cat :: [Doc] -> Doc
fcat :: [Doc] -> Doc
fsep :: [Doc] -> Doc
style :: Style
render :: Doc -> String
renderStyle :: Style -> Doc -> String
fullRender :: Mode -> Int -> Float -> (TextDetails -> a -> a) -> a -> Doc -> a
prettyNormal :: PrettyLevel
prettyShow :: Pretty a => a -> String
prettyParen :: Bool -> Doc -> Doc
module Test.HUnit

Documentation

module Data.Logic.ATP.Lib

module Data.Logic.ATP.Pretty

module Data.Logic.ATP.Formulas

data Lit Source #

Constructors

L
Fields lname :: String

Instances

Instances details

Eq Lit Source #
Instance details Defined in Data.Logic.ATP.Lit Methods (==) :: Lit -> Lit -> Bool # (/=) :: Lit -> Lit -> Bool #
Ord Lit Source #
Instance details Defined in Data.Logic.ATP.Lit Methods compare :: Lit -> Lit -> Ordering # (<) :: Lit -> Lit -> Bool # (<=) :: Lit -> Lit -> Bool # (>) :: Lit -> Lit -> Bool # (>=) :: Lit -> Lit -> Bool # max :: Lit -> Lit -> Lit # min :: Lit -> Lit -> Lit #

class IsFormula lit => IsLiteral lit where Source #

The class of formulas that can be negated. Literals are the building blocks of the clause and implicative normal forms. They support negation and must include true and false elements.

Methods

naiveNegate :: lit -> lit Source #

Negate a formula in a naive fashion, the operators below prevent double negation.

foldNegation Source #

Arguments

:: (lit -> r)	called for normal formulas
-> (lit -> r)	called for negated formulas
-> lit
-> r

Test whether a lit is negated or normal

foldLiteral' Source #

Arguments

:: (lit -> r)	Called for higher order formulas (non-literal)
-> (lit -> r)	Called for negated formulas
-> (Bool -> r)	Called for true and false formulas
-> (AtomOf lit -> r)	Called for atomic formulas
-> lit
-> r

This is the internal fold for literals, foldLiteral below should normally be used, but its argument must be an instance of JustLiteral.

Instances

Instances details

(IsFormula (LFormula atom), Eq atom, Ord atom) => IsLiteral (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit Methods naiveNegate :: LFormula atom -> LFormula atom Source # foldNegation :: (LFormula atom -> r) -> (LFormula atom -> r) -> LFormula atom -> r Source # foldLiteral' :: (LFormula atom -> r) -> (LFormula atom -> r) -> (Bool -> r) -> (AtomOf (LFormula atom) -> r) -> LFormula atom -> r Source #
(IsFormula (JL a), IsLiteral a) => IsLiteral (JL a) Source #
Instance details Defined in Data.Logic.ATP.LitWrapper Methods naiveNegate :: JL a -> JL a Source # foldNegation :: (JL a -> r) -> (JL a -> r) -> JL a -> r Source # foldLiteral' :: (JL a -> r) -> (JL a -> r) -> (Bool -> r) -> (AtomOf (JL a) -> r) -> JL a -> r Source #
IsAtom atom => IsLiteral (PFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Prop Methods naiveNegate :: PFormula atom -> PFormula atom Source # foldNegation :: (PFormula atom -> r) -> (PFormula atom -> r) -> PFormula atom -> r Source # foldLiteral' :: (PFormula atom -> r) -> (PFormula atom -> r) -> (Bool -> r) -> (AtomOf (PFormula atom) -> r) -> PFormula atom -> r Source #
(HasApply atom, v ~ TVarOf (TermOf atom)) => IsLiteral (QFormula v atom) Source #
Instance details Defined in Data.Logic.ATP.Quantified Methods naiveNegate :: QFormula v atom -> QFormula v atom Source # foldNegation :: (QFormula v atom -> r) -> (QFormula v atom -> r) -> QFormula v atom -> r Source # foldLiteral' :: (QFormula v atom -> r) -> (QFormula v atom -> r) -> (Bool -> r) -> (AtomOf (QFormula v atom) -> r) -> QFormula v atom -> r Source #

class IsLiteral formula => JustLiteral formula Source #

Class that indicates that a formula type *only* contains IsLiteral features - no combinations or quantifiers.

Instances

Instances details

IsAtom atom => JustLiteral (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit
(IsFormula (JL a), IsLiteral a) => JustLiteral (JL a) Source #
Instance details Defined in Data.Logic.ATP.LitWrapper

data LFormula atom Source #

Example of a JustLiteral type.

Instances

Instances details

IsAtom atom => IsFormula (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit Associated Types type AtomOf (LFormula atom) Source # Methods true :: LFormula atom Source # false :: LFormula atom Source # asBool :: LFormula atom -> Maybe Bool Source # atomic :: AtomOf (LFormula atom) -> LFormula atom Source # overatoms :: (AtomOf (LFormula atom) -> r -> r) -> LFormula atom -> r -> r Source # onatoms :: (AtomOf (LFormula atom) -> AtomOf (LFormula atom)) -> LFormula atom -> LFormula atom Source #
(IsFormula (LFormula atom), Eq atom, Ord atom) => IsLiteral (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit Methods naiveNegate :: LFormula atom -> LFormula atom Source # foldNegation :: (LFormula atom -> r) -> (LFormula atom -> r) -> LFormula atom -> r Source # foldLiteral' :: (LFormula atom -> r) -> (LFormula atom -> r) -> (Bool -> r) -> (AtomOf (LFormula atom) -> r) -> LFormula atom -> r Source #
IsAtom atom => JustLiteral (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit
IsAtom atom => HasFixity (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit Methods precedence :: LFormula atom -> Precedence Source # associativity :: LFormula atom -> Associativity Source #
Data atom => Data (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LFormula atom -> c (LFormula atom) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (LFormula atom) # toConstr :: LFormula atom -> Constr # dataTypeOf :: LFormula atom -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (LFormula atom)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (LFormula atom)) # gmapT :: (forall b. Data b => b -> b) -> LFormula atom -> LFormula atom # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LFormula atom -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LFormula atom -> r # gmapQ :: (forall d. Data d => d -> u) -> LFormula atom -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LFormula atom -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LFormula atom -> m (LFormula atom) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LFormula atom -> m (LFormula atom) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LFormula atom -> m (LFormula atom) #
Read atom => Read (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit Methods readsPrec :: Int -> ReadS (LFormula atom) # readList :: ReadS [LFormula atom] # readPrec :: ReadPrec (LFormula atom) # readListPrec :: ReadPrec [LFormula atom] #
Show atom => Show (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit Methods showsPrec :: Int -> LFormula atom -> ShowS # show :: LFormula atom -> String # showList :: [LFormula atom] -> ShowS #
Eq atom => Eq (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit Methods (==) :: LFormula atom -> LFormula atom -> Bool # (/=) :: LFormula atom -> LFormula atom -> Bool #
Ord atom => Ord (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit Methods compare :: LFormula atom -> LFormula atom -> Ordering # (<) :: LFormula atom -> LFormula atom -> Bool # (<=) :: LFormula atom -> LFormula atom -> Bool # (>) :: LFormula atom -> LFormula atom -> Bool # (>=) :: LFormula atom -> LFormula atom -> Bool # max :: LFormula atom -> LFormula atom -> LFormula atom # min :: LFormula atom -> LFormula atom -> LFormula atom #
IsAtom atom => Pretty (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit Methods pPrintPrec :: PrettyLevel -> Rational -> LFormula atom -> Doc # pPrint :: LFormula atom -> Doc # pPrintList :: PrettyLevel -> [LFormula atom] -> Doc #
type AtomOf (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit type AtomOf (LFormula atom) = atom

negate :: IsLiteral formula => formula -> formula Source #

Negate the formula, avoiding double negation

negative :: IsLiteral formula => formula -> Bool Source #

Some operations on IsLiteral formulas

(.~.) :: IsLiteral formula => formula -> formula infix 6 Source #

Negate the formula, avoiding double negation

(¬) :: IsLiteral formula => formula -> formula infix 6 Source #

Negate the formula, avoiding double negation

negated :: IsLiteral formula => formula -> Bool Source #

Is this formula negated at the top level?

positive :: IsLiteral formula => formula -> Bool Source #

foldLiteral :: JustLiteral lit => (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r Source #

onatomsLiteral :: JustLiteral lit => (AtomOf lit -> AtomOf lit) -> lit -> lit Source #

Implementation of onatoms for JustLiteral types.

overatomsLiteral :: JustLiteral lit => (AtomOf lit -> r -> r) -> lit -> r -> r Source #

implementation of overatoms for JustLiteral types.

zipLiterals' :: (IsLiteral lit1, IsLiteral lit2) => (lit1 -> lit2 -> Maybe r) -> (lit1 -> lit2 -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (AtomOf lit1 -> AtomOf lit2 -> Maybe r) -> lit1 -> lit2 -> Maybe r Source #

Combine two literals (internal version).

zipLiterals :: (JustLiteral lit1, JustLiteral lit2) => (lit1 -> lit2 -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (AtomOf lit1 -> AtomOf lit2 -> Maybe r) -> lit1 -> lit2 -> Maybe r Source #

Combine two literals.

convertLiteral :: (JustLiteral lit1, IsLiteral lit2) => (AtomOf lit1 -> AtomOf lit2) -> lit1 -> lit2 Source #

Convert a JustLiteral instance to any IsLiteral instance.

convertToLiteral :: (IsLiteral formula, JustLiteral lit) => (formula -> lit) -> (AtomOf formula -> AtomOf lit) -> formula -> lit Source #

Convert any formula to a literal, passing non-IsLiteral structures to the first argument (typically a call to error.)

precedenceLiteral :: JustLiteral lit => lit -> Precedence Source #

associativityLiteral :: JustLiteral lit => lit -> Associativity Source #

prettyLiteral :: JustLiteral lit => PrettyLevel -> Rational -> lit -> Doc Source #

Implementation of pPrint for -- JustLiteral types.

showLiteral :: JustLiteral lit => lit -> String Source #

data Prop Source #

An instance of IsPredicate.

Constructors

P
Fields pname :: String

Instances

Instances details

IsAtom Prop Source #
Instance details Defined in Data.Logic.ATP.Prop
HasFixity Prop Source #
Instance details Defined in Data.Logic.ATP.Prop Methods precedence :: Prop -> Precedence Source # associativity :: Prop -> Associativity Source #
IsString Prop Source #
Instance details Defined in Data.Logic.ATP.Prop Methods fromString :: String -> Prop #
Show Prop Source #
Instance details Defined in Data.Logic.ATP.Prop Methods showsPrec :: Int -> Prop -> ShowS # show :: Prop -> String # showList :: [Prop] -> ShowS #
Eq Prop Source #
Instance details Defined in Data.Logic.ATP.Prop Methods (==) :: Prop -> Prop -> Bool # (/=) :: Prop -> Prop -> Bool #
Ord Prop Source #
Instance details Defined in Data.Logic.ATP.Prop Methods compare :: Prop -> Prop -> Ordering # (<) :: Prop -> Prop -> Bool # (<=) :: Prop -> Prop -> Bool # (>) :: Prop -> Prop -> Bool # (>=) :: Prop -> Prop -> Bool # max :: Prop -> Prop -> Prop # min :: Prop -> Prop -> Prop #
Pretty Prop Source #
Instance details Defined in Data.Logic.ATP.Prop Methods pPrintPrec :: PrettyLevel -> Rational -> Prop -> Doc # pPrint :: Prop -> Doc # pPrintList :: PrettyLevel -> [Prop] -> Doc #

class IsLiteral formula => IsPropositional formula where Source #

A type class for propositional logic. If the type we are writing an instance for is a zero-order (aka propositional) logic type there will generally by a type or a type parameter corresponding to atom. For first order or predicate logic types, it is generally easiest to just use the formula type itself as the atom type, and raise errors in the implementation if a non-atomic formula somehow appears where an atomic formula is expected (i.e. as an argument to atomic or to the third argument of foldPropositional.)

Methods

(.|.) :: formula -> formula -> formula infixl 4 Source #

Disjunction/OR

(.&.) :: formula -> formula -> formula infixl 5 Source #

Conjunction/AND. x .&. y = (.~.) ((.~.) x .|. (.~.) y)

(.<=>.) :: formula -> formula -> formula infixl 2 Source #

Equivalence. x .=. y = (x .=>. y) .&. (y .=>. x)

(.=>.) :: formula -> formula -> formula infixr 3 Source #

Implication. x .=>. y = ((.~.) x .|. y)

foldPropositional' Source #

Arguments

:: (formula -> r)	fold on some higher order formula
-> (formula -> BinOp -> formula -> r)	fold on a binary operation formula. Functions of this type can be constructed using `binop`.
-> (formula -> r)	fold on a negated formula
-> (Bool -> r)	fold on a boolean formula
-> (AtomOf formula -> r)	fold on an atomic formula
-> formula
-> r

A fold function that distributes different sorts of formula to its parameter functions, one to handle binary operators, one for negations, and one for atomic formulas. See examples of its use to implement the polymorphic functions below.

foldCombination :: (formula -> r) -> (formula -> formula -> r) -> (formula -> formula -> r) -> (formula -> formula -> r) -> (formula -> formula -> r) -> formula -> r Source #

An alternative fold function for binary combinations of formulas

Instances

Instances details

IsAtom atom => IsPropositional (PFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Prop Methods (.\|.) :: PFormula atom -> PFormula atom -> PFormula atom Source # (.&.) :: PFormula atom -> PFormula atom -> PFormula atom Source # (.<=>.) :: PFormula atom -> PFormula atom -> PFormula atom Source # (.=>.) :: PFormula atom -> PFormula atom -> PFormula atom Source # foldPropositional' :: (PFormula atom -> r) -> (PFormula atom -> BinOp -> PFormula atom -> r) -> (PFormula atom -> r) -> (Bool -> r) -> (AtomOf (PFormula atom) -> r) -> PFormula atom -> r Source # foldCombination :: (PFormula atom -> r) -> (PFormula atom -> PFormula atom -> r) -> (PFormula atom -> PFormula atom -> r) -> (PFormula atom -> PFormula atom -> r) -> (PFormula atom -> PFormula atom -> r) -> PFormula atom -> r Source #
(IsFormula (QFormula v atom), HasApply atom, v ~ TVarOf (TermOf atom)) => IsPropositional (QFormula v atom) Source #
Instance details Defined in Data.Logic.ATP.Quantified Methods (.\|.) :: QFormula v atom -> QFormula v atom -> QFormula v atom Source # (.&.) :: QFormula v atom -> QFormula v atom -> QFormula v atom Source # (.<=>.) :: QFormula v atom -> QFormula v atom -> QFormula v atom Source # (.=>.) :: QFormula v atom -> QFormula v atom -> QFormula v atom Source # foldPropositional' :: (QFormula v atom -> r) -> (QFormula v atom -> BinOp -> QFormula v atom -> r) -> (QFormula v atom -> r) -> (Bool -> r) -> (AtomOf (QFormula v atom) -> r) -> QFormula v atom -> r Source # foldCombination :: (QFormula v atom -> r) -> (QFormula v atom -> QFormula v atom -> r) -> (QFormula v atom -> QFormula v atom -> r) -> (QFormula v atom -> QFormula v atom -> r) -> (QFormula v atom -> QFormula v atom -> r) -> QFormula v atom -> r Source #

data BinOp Source #

This type is used to construct the first argument of foldPropositional.

Constructors

(:<=>:)
(:=>:)
(:&:)
(:\|:)

Instances

Instances details

Data BinOp Source #
Instance details Defined in Data.Logic.ATP.Prop Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BinOp -> c BinOp # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BinOp # toConstr :: BinOp -> Constr # dataTypeOf :: BinOp -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BinOp) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BinOp) # gmapT :: (forall b. Data b => b -> b) -> BinOp -> BinOp # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r # gmapQ :: (forall d. Data d => d -> u) -> BinOp -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BinOp -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BinOp -> m BinOp # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BinOp -> m BinOp # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BinOp -> m BinOp #
Bounded BinOp Source #
Instance details Defined in Data.Logic.ATP.Prop Methods minBound :: BinOp # maxBound :: BinOp #
Enum BinOp Source #
Instance details Defined in Data.Logic.ATP.Prop Methods succ :: BinOp -> BinOp # pred :: BinOp -> BinOp # toEnum :: Int -> BinOp # fromEnum :: BinOp -> Int # enumFrom :: BinOp -> [BinOp] # enumFromThen :: BinOp -> BinOp -> [BinOp] # enumFromTo :: BinOp -> BinOp -> [BinOp] # enumFromThenTo :: BinOp -> BinOp -> BinOp -> [BinOp] #
Show BinOp Source #
Instance details Defined in Data.Logic.ATP.Prop Methods showsPrec :: Int -> BinOp -> ShowS # show :: BinOp -> String # showList :: [BinOp] -> ShowS #
Eq BinOp Source #
Instance details Defined in Data.Logic.ATP.Prop Methods (==) :: BinOp -> BinOp -> Bool # (/=) :: BinOp -> BinOp -> Bool #
Ord BinOp Source #
Instance details Defined in Data.Logic.ATP.Prop Methods compare :: BinOp -> BinOp -> Ordering # (<) :: BinOp -> BinOp -> Bool # (<=) :: BinOp -> BinOp -> Bool # (>) :: BinOp -> BinOp -> Bool # (>=) :: BinOp -> BinOp -> Bool # max :: BinOp -> BinOp -> BinOp # min :: BinOp -> BinOp -> BinOp #

class IsPropositional formula => JustPropositional formula Source #

Class that indicates a formula type *only* supports Propositional features - it has no way to represent quantifiers.

Instances

Instances details

IsAtom atom => JustPropositional (PFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Prop

data TruthTable a Source #

Constructors

TruthTable [a] [TruthTableRow]

Instances

Instances details

Show a => Show (TruthTable a) Source #
Instance details Defined in Data.Logic.ATP.Prop Methods showsPrec :: Int -> TruthTable a -> ShowS # show :: TruthTable a -> String # showList :: [TruthTable a] -> ShowS #
Eq a => Eq (TruthTable a) Source #
Instance details Defined in Data.Logic.ATP.Prop Methods (==) :: TruthTable a -> TruthTable a -> Bool # (/=) :: TruthTable a -> TruthTable a -> Bool #
Pretty atom => Pretty (TruthTable atom) Source #
Instance details Defined in Data.Logic.ATP.Prop Methods pPrintPrec :: PrettyLevel -> Rational -> TruthTable atom -> Doc # pPrint :: TruthTable atom -> Doc # pPrintList :: PrettyLevel -> [TruthTable atom] -> Doc #

data PFormula atom Source #

An instance of IsPropositional.

Instances

Instances details

IsAtom atom => IsFormula (PFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Prop Associated Types type AtomOf (PFormula atom) Source # Methods true :: PFormula atom Source # false :: PFormula atom Source # asBool :: PFormula atom -> Maybe Bool Source # atomic :: AtomOf (PFormula atom) -> PFormula atom Source # overatoms :: (AtomOf (PFormula atom) -> r -> r) -> PFormula atom -> r -> r Source # onatoms :: (AtomOf (PFormula atom) -> AtomOf (PFormula atom)) -> PFormula atom -> PFormula atom Source #
IsAtom atom => IsLiteral (PFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Prop Methods naiveNegate :: PFormula atom -> PFormula atom Source # foldNegation :: (PFormula atom -> r) -> (PFormula atom -> r) -> PFormula atom -> r Source # foldLiteral' :: (PFormula atom -> r) -> (PFormula atom -> r) -> (Bool -> r) -> (AtomOf (PFormula atom) -> r) -> PFormula atom -> r Source #
IsAtom atom => HasFixity (PFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Prop Methods precedence :: PFormula atom -> Precedence Source # associativity :: PFormula atom -> Associativity Source #
IsAtom atom => IsPropositional (PFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Prop Methods (.\|.) :: PFormula atom -> PFormula atom -> PFormula atom Source # (.&.) :: PFormula atom -> PFormula atom -> PFormula atom Source # (.<=>.) :: PFormula atom -> PFormula atom -> PFormula atom Source # (.=>.) :: PFormula atom -> PFormula atom -> PFormula atom Source # foldPropositional' :: (PFormula atom -> r) -> (PFormula atom -> BinOp -> PFormula atom -> r) -> (PFormula atom -> r) -> (Bool -> r) -> (AtomOf (PFormula atom) -> r) -> PFormula atom -> r Source # foldCombination :: (PFormula atom -> r) -> (PFormula atom -> PFormula atom -> r) -> (PFormula atom -> PFormula atom -> r) -> (PFormula atom -> PFormula atom -> r) -> (PFormula atom -> PFormula atom -> r) -> PFormula atom -> r Source #
IsAtom atom => JustPropositional (PFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Prop
Data atom => Data (PFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Prop Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PFormula atom -> c (PFormula atom) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (PFormula atom) # toConstr :: PFormula atom -> Constr # dataTypeOf :: PFormula atom -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (PFormula atom)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (PFormula atom)) # gmapT :: (forall b. Data b => b -> b) -> PFormula atom -> PFormula atom # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PFormula atom -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PFormula atom -> r # gmapQ :: (forall d. Data d => d -> u) -> PFormula atom -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> PFormula atom -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> PFormula atom -> m (PFormula atom) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PFormula atom -> m (PFormula atom) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PFormula atom -> m (PFormula atom) #
Read atom => Read (PFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Prop Methods readsPrec :: Int -> ReadS (PFormula atom) # readList :: ReadS [PFormula atom] # readPrec :: ReadPrec (PFormula atom) # readListPrec :: ReadPrec [PFormula atom] #
(IsPropositional (PFormula atom), Show atom) => Show (PFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Prop Methods showsPrec :: Int -> PFormula atom -> ShowS # show :: PFormula atom -> String # showList :: [PFormula atom] -> ShowS #
Eq atom => Eq (PFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Prop Methods (==) :: PFormula atom -> PFormula atom -> Bool # (/=) :: PFormula atom -> PFormula atom -> Bool #
Ord atom => Ord (PFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Prop Methods compare :: PFormula atom -> PFormula atom -> Ordering # (<) :: PFormula atom -> PFormula atom -> Bool # (<=) :: PFormula atom -> PFormula atom -> Bool # (>) :: PFormula atom -> PFormula atom -> Bool # (>=) :: PFormula atom -> PFormula atom -> Bool # max :: PFormula atom -> PFormula atom -> PFormula atom # min :: PFormula atom -> PFormula atom -> PFormula atom #
IsAtom atom => Pretty (PFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Prop Methods pPrintPrec :: PrettyLevel -> Rational -> PFormula atom -> Doc # pPrint :: PFormula atom -> Doc # pPrintList :: PrettyLevel -> [PFormula atom] -> Doc #
type AtomOf (PFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Prop type AtomOf (PFormula atom) = atom

(==>) :: IsPropositional formula => formula -> formula -> formula infixr 3 Source #

Implication synonyms. Note that if the -XUnicodeSyntax option is turned on the operator ⇒ can not be declared/used as a function - it becomes a reserved special character used in type signatures.

(⇒) :: IsPropositional formula => formula -> formula -> formula infixr 3 Source #

Implication synonyms. Note that if the -XUnicodeSyntax option is turned on the operator ⇒ can not be declared/used as a function - it becomes a reserved special character used in type signatures.

(→) :: IsPropositional formula => formula -> formula -> formula infixr 3 Source #

Implication synonyms. Note that if the -XUnicodeSyntax option is turned on the operator ⇒ can not be declared/used as a function - it becomes a reserved special character used in type signatures.

binop :: IsPropositional formula => formula -> BinOp -> formula -> formula Source #

Combine formulas with a BinOp, for use building the first argument of foldPropositional.

(⊃) :: IsPropositional formula => formula -> formula -> formula infixr 3 Source #

Implication synonyms. Note that if the -XUnicodeSyntax option is turned on the operator ⇒ can not be declared/used as a function - it becomes a reserved special character used in type signatures.

(⇔) :: IsPropositional formula => formula -> formula -> formula infixl 2 Source #

If-and-only-if synonyms

(<=>) :: IsPropositional formula => formula -> formula -> formula infixl 2 Source #

If-and-only-if synonyms

(↔) :: IsPropositional formula => formula -> formula -> formula infixl 2 Source #

If-and-only-if synonyms

(<==>) :: IsPropositional formula => formula -> formula -> formula infixl 2 Source #

If-and-only-if synonyms

(∧) :: IsPropositional formula => formula -> formula -> formula infixl 5 Source #

And/conjunction synonyms

(·) :: IsPropositional formula => formula -> formula -> formula infixl 5 Source #

And/conjunction synonyms

(∨) :: IsPropositional formula => formula -> formula -> formula infixl 4 Source #

Or/disjunction synonyms

foldPropositional Source #

Arguments

:: JustPropositional pf
=> (pf -> BinOp -> pf -> r)	fold on a binary operation formula
-> (pf -> r)	fold on a negated formula
-> (Bool -> r)	fold on a boolean formula
-> (AtomOf pf -> r)	fold on an atomic formula
-> pf
-> r

Deconstruct a JustPropositional formula.

zipPropositional Source #

Arguments

:: (JustPropositional pf1, JustPropositional pf2)
=> (pf1 -> BinOp -> pf1 -> pf2 -> BinOp -> pf2 -> Maybe r)	Combine two binary operation formulas
-> (pf1 -> pf2 -> Maybe r)	Combine two negated formulas
-> (Bool -> Bool -> Maybe r)	Combine two boolean formulas
-> (AtomOf pf1 -> AtomOf pf2 -> Maybe r)	Combine two atomic formulas
-> pf1
-> pf2
-> Maybe r	Result is Nothing if the formulas don't unify

Combine two JustPropositional formulas if they are similar.

convertPropositional Source #

Arguments

:: (JustPropositional pf1, IsPropositional pf2)
=> (AtomOf pf1 -> AtomOf pf2)	Convert an atomic formula
-> pf1
-> pf2

Convert any instance of JustPropositional to any IsPropositional formula.

convertToPropositional Source #

Arguments

:: (IsPropositional formula, JustPropositional pf)
=> (formula -> pf)	Convert a higher order formula
-> (AtomOf formula -> AtomOf pf)	Convert an atomic formula
-> formula
-> pf

Convert any instance of IsPropositional to a JustPropositional formula. Typically the ho (higher order) argument calls error if it encounters something it can't handle.

precedencePropositional :: JustPropositional pf => pf -> Precedence Source #

Implementation of precedence for any JustPropostional type.

associativityPropositional :: JustPropositional pf => pf -> Associativity Source #

prettyPropositional :: forall pf. JustPropositional pf => Side -> PrettyLevel -> Rational -> pf -> Doc Source #

Implementation of pPrint for any JustPropostional type.

showPropositional :: JustPropositional pf => Side -> Int -> pf -> ShowS Source #

Implementation of show for any JustPropositional type. For clarity, show methods fully parenthesize

onatomsPropositional :: JustPropositional pf => (AtomOf pf -> AtomOf pf) -> pf -> pf Source #

Implementation of onatoms for any JustPropositional type.

overatomsPropositional :: JustPropositional pf => (AtomOf pf -> r -> r) -> pf -> r -> r Source #

Implementation of overatoms for any JustPropositional type.

eval :: JustPropositional pf => pf -> (AtomOf pf -> Bool) -> Bool Source #

Interpretation of formulas.

atoms :: IsFormula formula => formula -> Set (AtomOf formula) Source #

Return the set of propositional variables in a formula.

onallvaluations :: Ord atom => (r -> r -> r) -> ((atom -> Bool) -> r) -> (atom -> Bool) -> Set atom -> r Source #

truthTable :: JustPropositional pf => pf -> TruthTable (AtomOf pf) Source #

Code to print out truth tables.

tautology :: JustPropositional pf => pf -> Bool Source #

Recognizing tautologies.

unsatisfiable :: JustPropositional pf => pf -> Bool Source #

Related concepts.

satisfiable :: JustPropositional pf => pf -> Bool Source #

psubst :: JustPropositional formula => Map (AtomOf formula) formula -> formula -> formula Source #

Substitution operation.

dual :: JustPropositional pf => pf -> pf Source #

Dualization.

psimplify :: IsPropositional formula => formula -> formula Source #

Routine simplification.

psimplify1 :: IsPropositional formula => formula -> formula Source #

nenf :: IsPropositional formula => formula -> formula Source #

list_conj :: (Foldable t, IsFormula formula, IsPropositional formula) => t formula -> formula Source #

Disjunctive normal form (DNF) via truth tables.

list_disj :: (Foldable t, IsFormula formula, IsPropositional formula) => t formula -> formula Source #

mk_lits :: (JustPropositional pf, Ord pf) => Set pf -> (AtomOf pf -> Bool) -> pf Source #

allsatvaluations :: Ord atom => ((atom -> Bool) -> Bool) -> (atom -> Bool) -> Set atom -> [atom -> Bool] Source #

dnfSet :: (JustPropositional pf, Ord pf) => pf -> pf Source #

purednf :: (JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit) Source #

simpdnf :: (JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit) Source #

With subsumption checking, done very naively (quadratic).

rawdnf :: IsPropositional formula => formula -> formula Source #

dnf :: forall pf. (JustPropositional pf, Ord pf) => pf -> pf Source #

Mapping back to a formula.

purecnf :: (JustPropositional pf, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit) Source #

Conjunctive normal form (CNF) by essentially the same code. (p. 60)

simpcnf :: (JustPropositional pf, JustLiteral lit, Ord lit) => (AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit) Source #

cnf' :: forall pf. (JustPropositional pf, Ord pf) => pf -> pf Source #

cnf_ :: (IsPropositional pf, Ord pf, JustLiteral lit) => (AtomOf lit -> AtomOf pf) -> Set (Set lit) -> pf Source #

trivial :: (Ord lit, IsLiteral lit) => Set lit -> Bool Source #

Filtering out trivial disjuncts (in this guise, contradictory).

testProp :: Test Source #

data Knows a Source #

Instances

Instances details

NumAtom (Knows Integer) Source #
Instance details Defined in Data.Logic.ATP.DP Methods ma :: Integer -> Knows Integer Source # ai :: Knows Integer -> Integer Source #
IsAtom (Knows Integer) Source #
Instance details Defined in Data.Logic.ATP.PropExamples
Num a => HasFixity (Knows a) Source #
Instance details Defined in Data.Logic.ATP.PropExamples Methods precedence :: Knows a -> Precedence Source # associativity :: Knows a -> Associativity Source #
Show a => Show (Knows a) Source #
Instance details Defined in Data.Logic.ATP.PropExamples Methods showsPrec :: Int -> Knows a -> ShowS # show :: Knows a -> String # showList :: [Knows a] -> ShowS #
Eq a => Eq (Knows a) Source #
Instance details Defined in Data.Logic.ATP.PropExamples Methods (==) :: Knows a -> Knows a -> Bool # (/=) :: Knows a -> Knows a -> Bool #
Ord a => Ord (Knows a) Source #
Instance details Defined in Data.Logic.ATP.PropExamples Methods compare :: Knows a -> Knows a -> Ordering # (<) :: Knows a -> Knows a -> Bool # (<=) :: Knows a -> Knows a -> Bool # (>) :: Knows a -> Knows a -> Bool # (>=) :: Knows a -> Knows a -> Bool # max :: Knows a -> Knows a -> Knows a # min :: Knows a -> Knows a -> Knows a #
(Num a, Show a) => Pretty (Knows a) Source #
Instance details Defined in Data.Logic.ATP.PropExamples Methods pPrintPrec :: PrettyLevel -> Rational -> Knows a -> Doc # pPrint :: Knows a -> Doc # pPrintList :: PrettyLevel -> [Knows a] -> Doc #

mk_knows :: (IsPropositional formula, AtomOf formula ~ Knows a) => String -> a -> formula Source #

mk_knows2 :: (IsPropositional formula, AtomOf formula ~ Knows a) => String -> a -> a -> formula Source #

prime :: (IsPropositional formula, Ord formula, AtomOf formula ~ Knows Integer) => Integer -> formula Source #

ramsey :: (IsPropositional pf, AtomOf pf ~ Knows Integer, Ord pf) => Integer -> Integer -> Integer -> pf Source #

Generate assertion equivalent to R(s,t) <= n for the Ramsey number R(s,t)

testPropExamples :: Test Source #

module Data.Logic.ATP.DefCNF

module Data.Logic.ATP.DP

module Data.Logic.ATP.Term

module Data.Logic.ATP.Apply

module Data.Logic.ATP.Equate

module Data.Logic.ATP.Quantified

module Data.Logic.ATP.Parser

module Data.Logic.ATP.FOL

module Data.Logic.ATP.Skolem

module Data.Logic.ATP.Herbrand

module Data.Logic.ATP.Unif

tab :: (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Pretty formula, HasSkolem function, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => Maybe Depth -> formula -> Failing ((K, Map v term), Depth) Source #

prawitz :: forall formula atom term function v. (IsFirstOrder formula, Ord formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => formula -> Int Source #

testTableaux :: Test Source #

module Data.Logic.ATP.Resolution

module Data.Logic.ATP.Prolog

module Data.Logic.ATP.Meson

module Data.Logic.ATP.Equal

data Mode #

Rendering mode.

Constructors

PageMode	Normal rendering (`lineLength` and `ribbonsPerLine` respected').
ZigZagMode	With zig-zag cuts.
LeftMode	No indentation, infinitely long lines (`lineLength` ignored), but explicit new lines, i.e., `text "one" $$ text "two"`, are respected.
OneLineMode	All on one line, `lineLength` ignored and explicit new lines (`$$`) are turned into spaces.

Instances

Instances details

Generic Mode
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Associated Types type Rep Mode :: Type -> Type # Methods from :: Mode -> Rep Mode x # to :: Rep Mode x -> Mode #
Show Mode
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Methods showsPrec :: Int -> Mode -> ShowS # show :: Mode -> String # showList :: [Mode] -> ShowS #
Eq Mode
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Methods (==) :: Mode -> Mode -> Bool # (/=) :: Mode -> Mode -> Bool #
type Rep Mode
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ type Rep Mode = D1 ('MetaData "Mode" "Text.PrettyPrint.Annotated.HughesPJ" "pretty-1.1.3.6" 'False) ((C1 ('MetaCons "PageMode" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ZigZagMode" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "LeftMode" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OneLineMode" 'PrefixI 'False) (U1 :: Type -> Type)))

data Style #

A rendering style. Allows us to specify constraints to choose among the many different rendering options.

Constructors

Style

Fields

mode :: Mode
The rendering mode.
lineLength :: Int
Maximum length of a line, in characters.
ribbonsPerLine :: Float
Ratio of line length to ribbon length. A ribbon refers to the characters on a line excluding indentation. So a lineLength of 100, with a ribbonsPerLine of 2.0 would only allow up to 50 characters of ribbon to be displayed on a line, while allowing it to be indented up to 50 characters.

Instances

Instances details

Generic Style
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Associated Types type Rep Style :: Type -> Type # Methods from :: Style -> Rep Style x # to :: Rep Style x -> Style #
Show Style
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Methods showsPrec :: Int -> Style -> ShowS # show :: Style -> String # showList :: [Style] -> ShowS #
Eq Style
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Methods (==) :: Style -> Style -> Bool # (/=) :: Style -> Style -> Bool #
type Rep Style
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ type Rep Style = D1 ('MetaData "Style" "Text.PrettyPrint.Annotated.HughesPJ" "pretty-1.1.3.6" 'False) (C1 ('MetaCons "Style" 'PrefixI 'True) (S1 ('MetaSel ('Just "mode") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Mode) :: (S1 ('MetaSel ('Just "lineLength") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :: S1 ('MetaSel ('Just "ribbonsPerLine") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Float))))

data TextDetails #

A TextDetails represents a fragment of text that will be output at some point in a Doc.

Constructors

Chr !Char	A single Char fragment
Str String	A whole String fragment
PStr String	Used to represent a Fast String fragment but now deprecated and identical to the Str constructor.

Instances

Instances details

Generic TextDetails
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Associated Types type Rep TextDetails :: Type -> Type # Methods from :: TextDetails -> Rep TextDetails x # to :: Rep TextDetails x -> TextDetails #
Show TextDetails
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Methods showsPrec :: Int -> TextDetails -> ShowS # show :: TextDetails -> String # showList :: [TextDetails] -> ShowS #
NFData TextDetails
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Methods rnf :: TextDetails -> () #
Eq TextDetails
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Methods (==) :: TextDetails -> TextDetails -> Bool # (/=) :: TextDetails -> TextDetails -> Bool #
type Rep TextDetails
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ type Rep TextDetails = D1 ('MetaData "TextDetails" "Text.PrettyPrint.Annotated.HughesPJ" "pretty-1.1.3.6" 'False) (C1 ('MetaCons "Chr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedUnpack) (Rec0 Char)) :+: (C1 ('MetaCons "Str" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "PStr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))))

data Doc #

The abstract type of documents. A Doc represents a set of layouts. A Doc with no occurrences of Union or NoDoc represents just one layout.

Instances

Instances details

IsString Doc
Instance details Defined in Text.PrettyPrint.HughesPJ Methods fromString :: String -> Doc #
Monoid Doc
Instance details Defined in Text.PrettyPrint.HughesPJ Methods mempty :: Doc # mappend :: Doc -> Doc -> Doc # mconcat :: [Doc] -> Doc #
Semigroup Doc
Instance details Defined in Text.PrettyPrint.HughesPJ Methods (<>) :: Doc -> Doc -> Doc # sconcat :: NonEmpty Doc -> Doc # stimes :: Integral b => b -> Doc -> Doc #
Generic Doc
Instance details Defined in Text.PrettyPrint.HughesPJ Associated Types type Rep Doc :: Type -> Type # Methods from :: Doc -> Rep Doc x # to :: Rep Doc x -> Doc #
Show Doc
Instance details Defined in Text.PrettyPrint.HughesPJ Methods showsPrec :: Int -> Doc -> ShowS # show :: Doc -> String # showList :: [Doc] -> ShowS #
NFData Doc
Instance details Defined in Text.PrettyPrint.HughesPJ Methods rnf :: Doc -> () #
Eq Doc
Instance details Defined in Text.PrettyPrint.HughesPJ Methods (==) :: Doc -> Doc -> Bool # (/=) :: Doc -> Doc -> Bool #
type Rep Doc
Instance details Defined in Text.PrettyPrint.HughesPJ type Rep Doc = D1 ('MetaData "Doc" "Text.PrettyPrint.HughesPJ" "pretty-1.1.3.6" 'True) (C1 ('MetaCons "Doc" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Doc ()))))

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

Instances details

Pretty Predicate Source #
Instance details Defined in Data.Logic.ATP.Apply Methods pPrintPrec :: PrettyLevel -> Rational -> Predicate -> Doc # pPrint :: Predicate -> Doc # pPrintList :: PrettyLevel -> [Predicate] -> Doc #
Pretty Atom Source #
Instance details Defined in Data.Logic.ATP.DefCNF Methods pPrintPrec :: PrettyLevel -> Rational -> Atom -> Doc # pPrint :: Atom -> Doc # pPrintList :: PrettyLevel -> [Atom] -> Doc #
Pretty Depth Source #
Instance details Defined in Data.Logic.ATP.Lib Methods pPrintPrec :: PrettyLevel -> Rational -> Depth -> Doc # pPrint :: Depth -> Doc # pPrintList :: PrettyLevel -> [Depth] -> Doc #
Pretty Prop Source #
Instance details Defined in Data.Logic.ATP.Prop Methods pPrintPrec :: PrettyLevel -> Rational -> Prop -> Doc # pPrint :: Prop -> Doc # pPrintList :: PrettyLevel -> [Prop] -> Doc #
Pretty Function Source #
Instance details Defined in Data.Logic.ATP.Skolem Methods pPrintPrec :: PrettyLevel -> Rational -> Function -> Doc # pPrint :: Function -> Doc # pPrintList :: PrettyLevel -> [Function] -> Doc #
Pretty K Source #
Instance details Defined in Data.Logic.ATP.Tableaux Methods pPrintPrec :: PrettyLevel -> Rational -> K -> Doc # pPrint :: K -> Doc # pPrintList :: PrettyLevel -> [K] -> Doc #
Pretty FName Source #
Instance details Defined in Data.Logic.ATP.Term Methods pPrintPrec :: PrettyLevel -> Rational -> FName -> Doc # pPrint :: FName -> Doc # pPrintList :: PrettyLevel -> [FName] -> Doc #
Pretty V Source #
Instance details Defined in Data.Logic.ATP.Term Methods pPrintPrec :: PrettyLevel -> Rational -> V -> Doc # pPrint :: V -> Doc # pPrintList :: PrettyLevel -> [V] -> Doc #
Pretty Ordering
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> Ordering -> Doc # pPrint :: Ordering -> Doc # pPrintList :: PrettyLevel -> [Ordering] -> Doc #
Pretty Message Source #
Instance details Defined in Data.Logic.ATP.Parser Methods pPrintPrec :: PrettyLevel -> Rational -> Message -> Doc # pPrint :: Message -> Doc # pPrintList :: PrettyLevel -> [Message] -> Doc #
Pretty ParseError Source #
Instance details Defined in Data.Logic.ATP.Parser Methods pPrintPrec :: PrettyLevel -> Rational -> ParseError -> Doc # pPrint :: ParseError -> Doc # pPrintList :: PrettyLevel -> [ParseError] -> Doc #
Pretty Integer
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> Integer -> Doc # pPrint :: Integer -> Doc # pPrintList :: PrettyLevel -> [Integer] -> Doc #
Pretty ()
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> () -> Doc # pPrint :: () -> Doc # pPrintList :: PrettyLevel -> [()] -> Doc #
Pretty Bool
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> Bool -> Doc # pPrint :: Bool -> Doc # pPrintList :: PrettyLevel -> [Bool] -> Doc #
Pretty Char
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> Char -> Doc # pPrint :: Char -> Doc # pPrintList :: PrettyLevel -> [Char] -> Doc #
Pretty Double
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> Double -> Doc # pPrint :: Double -> Doc # pPrintList :: PrettyLevel -> [Double] -> Doc #
Pretty Float
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> Float -> Doc # pPrint :: Float -> Doc # pPrintList :: PrettyLevel -> [Float] -> Doc #
Pretty Int
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> Int -> Doc # pPrint :: Int -> Doc # pPrintList :: PrettyLevel -> [Int] -> Doc #
Pretty a => Pretty (Failing a) Source #
Instance details Defined in Data.Logic.ATP.Lib Methods pPrintPrec :: PrettyLevel -> Rational -> Failing a -> Doc # pPrint :: Failing a -> Doc # pPrintList :: PrettyLevel -> [Failing a] -> Doc #
IsAtom atom => Pretty (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit Methods pPrintPrec :: PrettyLevel -> Rational -> LFormula atom -> Doc # pPrint :: LFormula atom -> Doc # pPrintList :: PrettyLevel -> [LFormula atom] -> Doc #
Pretty a => Pretty (JL a) Source #
Instance details Defined in Data.Logic.ATP.LitWrapper Methods pPrintPrec :: PrettyLevel -> Rational -> JL a -> Doc # pPrint :: JL a -> Doc # pPrintList :: PrettyLevel -> [JL a] -> Doc #
IsAtom atom => Pretty (PFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Prop Methods pPrintPrec :: PrettyLevel -> Rational -> PFormula atom -> Doc # pPrint :: PFormula atom -> Doc # pPrintList :: PrettyLevel -> [PFormula atom] -> Doc #
Pretty atom => Pretty (TruthTable atom) Source #
Instance details Defined in Data.Logic.ATP.Prop Methods pPrintPrec :: PrettyLevel -> Rational -> TruthTable atom -> Doc # pPrint :: TruthTable atom -> Doc # pPrintList :: PrettyLevel -> [TruthTable atom] -> Doc #
(Num a, Show a) => Pretty (Knows a) Source #
Instance details Defined in Data.Logic.ATP.PropExamples Methods pPrintPrec :: PrettyLevel -> Rational -> Knows a -> Doc # pPrint :: Knows a -> Doc # pPrintList :: PrettyLevel -> [Knows a] -> Doc #
Pretty a => Pretty (Set a) Source #
Instance details Defined in Data.Logic.ATP.Pretty Methods pPrintPrec :: PrettyLevel -> Rational -> Set a -> Doc # pPrint :: Set a -> Doc # pPrintList :: PrettyLevel -> [Set a] -> Doc #
Pretty a => Pretty (Maybe a)
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> Maybe a -> Doc # pPrint :: Maybe a -> Doc # pPrintList :: PrettyLevel -> [Maybe a] -> Doc #
Pretty a => Pretty [a]
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> [a] -> Doc # pPrint :: [a] -> Doc # pPrintList :: PrettyLevel -> [[a]] -> Doc #
(IsPredicate predicate, IsTerm term) => Pretty (FOLAP predicate term) Source #
Instance details Defined in Data.Logic.ATP.Apply Methods pPrintPrec :: PrettyLevel -> Rational -> FOLAP predicate term -> Doc # pPrint :: FOLAP predicate term -> Doc # pPrintList :: PrettyLevel -> [FOLAP predicate term] -> Doc #
(HasApply (FOL predicate term), HasEquate (FOL predicate term), IsTerm term) => Pretty (FOL predicate term) Source #
Instance details Defined in Data.Logic.ATP.Equate Methods pPrintPrec :: PrettyLevel -> Rational -> FOL predicate term -> Doc # pPrint :: FOL predicate term -> Doc # pPrintList :: PrettyLevel -> [FOL predicate term] -> Doc #
(HasApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => Pretty (QFormula v atom) Source #
Instance details Defined in Data.Logic.ATP.Quantified Methods pPrintPrec :: PrettyLevel -> Rational -> QFormula v atom -> Doc # pPrint :: QFormula v atom -> Doc # pPrintList :: PrettyLevel -> [QFormula v atom] -> Doc #
IsTerm (Term function v) => Pretty (Term function v) Source #
Instance details Defined in Data.Logic.ATP.Term Methods pPrintPrec :: PrettyLevel -> Rational -> Term function v -> Doc # pPrint :: Term function v -> Doc # pPrintList :: PrettyLevel -> [Term function v] -> Doc #
(Pretty a, Pretty b) => Pretty (Either a b)
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> Either a b -> Doc # pPrint :: Either a b -> Doc # pPrintList :: PrettyLevel -> [Either a b] -> Doc #
(Pretty v, Pretty term) => Pretty (Map v term) Source #
Instance details Defined in Data.Logic.ATP.Pretty Methods pPrintPrec :: PrettyLevel -> Rational -> Map v term -> Doc # pPrint :: Map v term -> Doc # pPrintList :: PrettyLevel -> [Map v term] -> Doc #
(Pretty a, Pretty b) => Pretty (a, b)
Instance details Defined in Text.PrettyPrint.HughesPJClass 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)
Instance details Defined in Text.PrettyPrint.HughesPJClass 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)
Instance details Defined in Text.PrettyPrint.HughesPJClass 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)
Instance details Defined in Text.PrettyPrint.HughesPJClass 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)
Instance details Defined in Text.PrettyPrint.HughesPJClass 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)
Instance details Defined in Text.PrettyPrint.HughesPJClass 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)
Instance details Defined in Text.PrettyPrint.HughesPJClass 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 #

newtype PrettyLevel #

Level of detail in the pretty printed output. Level 0 is the least detail.

Constructors

PrettyLevel Int

Instances

Instances details

Show PrettyLevel
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods showsPrec :: Int -> PrettyLevel -> ShowS # show :: PrettyLevel -> String # showList :: [PrettyLevel] -> ShowS #
Eq PrettyLevel
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods (==) :: PrettyLevel -> PrettyLevel -> Bool # (/=) :: PrettyLevel -> PrettyLevel -> Bool #
Ord PrettyLevel
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods compare :: PrettyLevel -> PrettyLevel -> Ordering # (<) :: PrettyLevel -> PrettyLevel -> Bool # (<=) :: PrettyLevel -> PrettyLevel -> Bool # (>) :: PrettyLevel -> PrettyLevel -> Bool # (>=) :: PrettyLevel -> PrettyLevel -> Bool # max :: PrettyLevel -> PrettyLevel -> PrettyLevel # min :: PrettyLevel -> PrettyLevel -> PrettyLevel #

text :: String -> Doc #

A document of height 1 containing a literal string. text satisfies the following laws:

```
text s <> text t = text (s++t)
```
text "" <> x = x, if x non-empty

The side condition on the last law is necessary because text "" has height 1, while empty has no height.

first :: Doc -> Doc -> Doc #

first returns its first argument if it is non-empty, otherwise its second.

empty :: Doc #

The empty document, with no height and no width. empty is the identity for <>, <+>, $$ and $+$ , and anywhere in the argument list for sep, hcat, hsep, vcat, fcat etc.

char :: Char -> Doc #

A document of height and width 1, containing a literal character.

parens #

Arguments

:: Doc
-> Doc	Wrap document in `(...)`

(<+>) :: Doc -> Doc -> Doc infixl 6 #

Beside, separated by space, unless one of the arguments is empty. <+> is associative, with identity empty.

isEmpty :: Doc -> Bool #

Returns True if the document is empty

space #

Arguments

:: Doc

A space character

integer #

Arguments

:: Integer
-> Doc	integer n = text (show n)

float #

Arguments

:: Float
-> Doc	float n = text (show n)

braces #

Arguments

:: Doc
-> Doc	Wrap document in `{...}`

brackets #

Arguments

:: Doc
-> Doc	Wrap document in `[...]`

semi #

Arguments

:: Doc

A ';' character

comma #

Arguments

:: Doc

A ',' character

colon #

Arguments

:: Doc

A : character

ptext :: String -> Doc #

Same as text. Used to be used for Bytestrings.

sizedText :: Int -> String -> Doc #

Some text with any width. (text s = sizedText (length s) s)

zeroWidthText :: String -> Doc #

Some text, but without any width. Use for non-printing text such as a HTML or Latex tags

equals #

Arguments

:: Doc

A '=' character

lparen #

Arguments

:: Doc

A '(' character

rparen #

Arguments

:: Doc

A ')' character

lbrack #

Arguments

:: Doc

A '[' character

rbrack #

Arguments

:: Doc

A ']' character

lbrace #

Arguments

:: Doc

A '{' character

rbrace #

Arguments

:: Doc

A '}' character

int #

Arguments

:: Int
-> Doc	int n = text (show n)

double #

Arguments

:: Double
-> Doc	double n = text (show n)

rational #

Arguments

:: Rational
-> Doc	rational n = text (show n)

quotes #

Arguments

:: Doc
-> Doc	Wrap document in `'...'`

doubleQuotes #

Arguments

:: Doc
-> Doc	Wrap document in `"..."`

maybeParens :: Bool -> Doc -> Doc #

Apply parens to Doc if boolean is true.

maybeBrackets :: Bool -> Doc -> Doc #

Apply brackets to Doc if boolean is true.

maybeBraces :: Bool -> Doc -> Doc #

Apply braces to Doc if boolean is true.

maybeQuotes :: Bool -> Doc -> Doc #

Apply quotes to Doc if boolean is true.

maybeDoubleQuotes :: Bool -> Doc -> Doc #

Apply doubleQuotes to Doc if boolean is true.

reduceDoc :: Doc -> RDoc #

Perform some simplification of a built up GDoc.

hcat :: [Doc] -> Doc #

List version of <>.

hsep :: [Doc] -> Doc #

List version of <+>.

vcat :: [Doc] -> Doc #

List version of $$.

nest :: Int -> Doc -> Doc #

Nest (or indent) a document by a given number of positions (which may also be negative). nest satisfies the laws:

```
nest 0 x = x
```
```
nest k (nest k' x) = nest (k+k') x
```
```
nest k (x <> y) = nest k x <> nest k y
```
```
nest k (x $$ y) = nest k x $$ nest k y
```
```
nest k empty = empty
```
x <> nest k y = x <> y, if x non-empty

The side condition on the last law is needed because empty is a left identity for <>.

hang :: Doc -> Int -> Doc -> Doc #

hang d1 n d2 = sep [d1, nest n d2]

punctuate :: Doc -> [Doc] -> [Doc] #

punctuate p [d1, ... dn] = [d1 <> p, d2 <> p, ... dn-1 <> p, dn]

($$) :: Doc -> Doc -> Doc infixl 5 #

Above, except that if the last line of the first argument stops at least one position before the first line of the second begins, these two lines are overlapped. For example:

   text "hi" $$ nest 5 (text "there")

lays out as

   hi   there

rather than

   hi
        there

$$ is associative, with identity empty, and also satisfies

(x $$ y) <> z = x $$ (y <> z), if y non-empty.

($+$) :: Doc -> Doc -> Doc infixl 5 #

Above, with no overlapping. $+$ is associative, with identity empty.

sep :: [Doc] -> Doc #

Either hsep or vcat.

cat :: [Doc] -> Doc #

Either hcat or vcat.

fcat :: [Doc] -> Doc #

"Paragraph fill" version of cat.

fsep :: [Doc] -> Doc #

"Paragraph fill" version of sep.

style :: Style #

The default style (mode=PageMode, lineLength=100, ribbonsPerLine=1.5).

render :: Doc -> String #

Render the Doc to a String using the default Style (see style).

renderStyle :: Style -> Doc -> String #

Render the Doc to a String using the given Style.

fullRender #

Arguments

:: Mode	Rendering mode.
-> Int	Line length.
-> Float	Ribbons per line.
-> (TextDetails -> a -> a)	What to do with text.
-> a	What to do at the end.
-> Doc	The document.
-> a	Result.

The general rendering interface. Please refer to the Style and Mode types for a description of rendering mode, line length and ribbons.

prettyNormal :: PrettyLevel #

The "normal" (Level 0) of detail.

prettyShow :: Pretty a => a -> String #

Pretty print a value with the prettyNormal level.

prettyParen :: Bool -> Doc -> Doc #

Parenthesize an value if the boolean is true.

module Test.HUnit