-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Import, export etc. for TPTP, a syntax for first-order logic
--   
--   For information about the TPTP format, see
--   <a>http://www.cs.miami.edu/~tptp/</a>.
--   
--   Components:
--   
--   <ul>
--   <li>Parser (<a>parse</a>)</li>
--   <li>Exporter (<a>toTPTP</a>)</li>
--   <li>Pretty-printer (<a>pretty</a>)</li>
--   <li>QuickCheck instances (generation of random formulae)</li>
--   <li><a>diff</a> : Get a "formula" which represents the differences
--   between two given formulae (equal subexpressions are truncated; so are
--   the subexpressions of subexpressions whose heads already differ)</li>
--   </ul>
--   
--   Tests passed:
--   
--   <ul>
--   <li>For randomly generated formulae, <tt>parse . toTPTP ==
--   id</tt></li>
--   <li>For the <tt>.p</tt> files in the TPTP (v 3.7.0.0) distribution's
--   <tt>PROBLEMS</tt> subtree which don't contain the string "thf(",
--   <tt>parse . toTPTP . parse == parse</tt></li>
--   </ul>
--   
--   Not yet implemented: The new <i>thf</i> formula type.
@package logic-TPTP
@version 0.2.0

module Codec.TPTP.Base

-- | Basic (undecorated) first-order formulae
type Formula = F Identity

-- | Basic (undecorated) terms
type Term = T Identity

-- | Equivalence
--   
--   Don't let the type context of these wrapper function confuse you :) --
--   the important special case is just:
--   
--   <pre>
--   (.&lt;=&gt;.) :: <a>Formula</a> -&gt; <a>Formula</a> -&gt; <a>Formula</a>
--   </pre>
(.<=>.) :: (Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) => (F c) -> (F c) -> F c

-- | Implication
(.=>.) :: (Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) => (F c) -> (F c) -> F c

-- | Reverse implication
(.<=.) :: (Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) => (F c) -> (F c) -> F c

-- | Disjunction/OR
(.|.) :: (Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) => (F c) -> (F c) -> F c

-- | Conjunction/AND
(.&.) :: (Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) => (F c) -> (F c) -> F c

-- | XOR
(.<~>.) :: (Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) => (F c) -> (F c) -> F c

-- | NOR
(.~|.) :: (Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) => (F c) -> (F c) -> F c

-- | NAND
(.~&.) :: (Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) => (F c) -> (F c) -> F c

-- | Negation
(.~.) :: (Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) => (F c) -> F c

-- | Equality
(.=.) :: (Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) => (T c) -> (T c) -> F c

-- | Inequality
(.!=.) :: (Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) => (T c) -> (T c) -> F c

-- | Universal quantification
for_all :: (Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) => [V] -> (F c) -> F c

-- | Existential quantification
exists :: (Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) => [V] -> (F c) -> F c

-- | Predicate symbol application
pApp :: (Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) => AtomicWord -> [T c] -> F c

-- | Variable
var :: (Pointed (Term0 (T c)) (c (Term0 (T c)))) => V -> T c

-- | Function symbol application (constants are encoded as nullary
--   functions)
fApp :: (Pointed (Term0 (T c)) (c (Term0 (T c)))) => AtomicWord -> [T c] -> T c

-- | Number literal
numberLitTerm :: (Pointed (Term0 (T c)) (c (Term0 (T c)))) => Double -> T c

-- | Double-quoted string literal, called <i>Distinct Object</i> in TPTP's
--   grammar
distinctObjectTerm :: (Pointed (Term0 (T c)) (c (Term0 (T c)))) => String -> T c

-- | See <a>http://haskell.org/haskellwiki/Indirect_composite</a> for the
--   point of the type parameters (they allow for future decorations, e.g.
--   monadic subformulae). If you don't need decorations, you can just use
--   <a>Formula</a> and the wrapped constructors above.
data Formula0 term formula

-- | Binary connective application
BinOp :: formula -> BinOp -> formula -> Formula0 term formula

-- | Infix predicate application (equalities, inequalities)
InfixPred :: term -> InfixPred -> term -> Formula0 term formula

-- | Predicate application
PredApp :: AtomicWord -> [term] -> Formula0 term formula

-- | Quantified formula
Quant :: Quant -> [V] -> formula -> Formula0 term formula

-- | Negation
(:~:) :: formula -> Formula0 term formula

-- | See <a>http://haskell.org/haskellwiki/Indirect_composite</a> for the
--   point of the type parameters (they allow for future decorations). If
--   you don't need decorations, you can just use <a>Term</a> and the
--   wrapped constructors above.
data Term0 term

-- | Variable
Var :: V -> Term0 term

-- | Number literal
NumberLitTerm :: Double -> Term0 term

-- | Double-quoted item
DistinctObjectTerm :: String -> Term0 term

-- | Function symbol application (constants are encoded as nullary
--   functions)
FunApp :: AtomicWord -> [term] -> Term0 term

-- | Formulae whose subexpressions are wrapped in the given type
--   constructor <tt>c</tt>.
--   
--   For example:
--   
--   <ul>
--   <li><tt>c = <a>Identity</a></tt>: Plain formulae</li>
--   <li><tt>c = <a>Maybe</a></tt>: Formulae that may contain "holes"</li>
--   <li><tt>c = IORef</tt>: (Mutable) formulae with mutable
--   subexpressions</li>
--   </ul>
newtype F c
F :: c (Formula0 (T c) (F c)) -> F c
runF :: F c -> c (Formula0 (T c) (F c))

-- | Terms whose subterms are wrapped in the given type constructor
--   <tt>c</tt>
newtype T c
T :: c (Term0 (T c)) -> T c
runT :: T c -> c (Term0 (T c))

-- | Binary formula connectives
data BinOp

-- | Equivalence
(:<=>:) :: BinOp

-- | Implication
(:=>:) :: BinOp

-- | Reverse Implication
(:<=:) :: BinOp

-- | AND
(:&:) :: BinOp

-- | OR
(:|:) :: BinOp

-- | NAND
(:~&:) :: BinOp

-- | NOR
(:~|:) :: BinOp

-- | XOR
(:<~>:) :: BinOp

-- | <i>Term -&gt; Term -&gt; Formula</i> infix connectives
data InfixPred
(:=:) :: InfixPred
(:!=:) :: InfixPred

-- | Quantifier specification
data Quant
All :: Quant
Exists :: Quant

-- | A line of a TPTP file: Annotated formula, comment or include
--   statement.
data TPTP_Input

-- | Annotated formulae
AFormula :: AtomicWord -> Role -> Formula -> Annotations -> TPTP_Input
name :: TPTP_Input -> AtomicWord
role :: TPTP_Input -> Role
formula :: TPTP_Input -> Formula
annotations :: TPTP_Input -> Annotations
Comment :: String -> TPTP_Input
Include :: FilePath -> [AtomicWord] -> TPTP_Input

-- | Annotations about the formulas origin
data Annotations
NoAnnotations :: Annotations
Annotations :: GTerm -> UsefulInfo -> Annotations

-- | Misc annotations
data UsefulInfo
NoUsefulInfo :: UsefulInfo
UsefulInfo :: [GTerm] -> UsefulInfo

-- | Formula roles
data Role
Role :: String -> Role
unrole :: Role -> String

-- | Metadata (the <i>general_data</i> rule in TPTP's grammar)
data GData
GWord :: AtomicWord -> GData
GApp :: AtomicWord -> [GTerm] -> GData
GVar :: V -> GData
GNumber :: Double -> GData
GDistinctObject :: String -> GData
GFormulaData :: String -> Formula -> GData

-- | Metadata (the <i>general_term</i> rule in TPTP's grammar)
data GTerm
ColonSep :: GData -> GTerm -> GTerm
GTerm :: GData -> GTerm
GList :: [GTerm] -> GTerm
class FreeVars a
freeVars :: (FreeVars a) => a -> Set V

-- | Universally quantify all free variables in the formula
univquant_free_vars :: Formula -> Formula

-- | TPTP constant symbol/predicate symbol/function symbol identifiers
--   (they are output in single quotes unless they are <i>lower_word</i>s).
--   
--   Tip: Use the <tt>-XOverloadedStrings</tt> compiler flag if you don't
--   want to have to type <i>AtomicWord</i> to construct an
--   <a>AtomicWord</a>
newtype AtomicWord
AtomicWord :: String -> AtomicWord

-- | Variable names
newtype V
V :: String -> V

-- | This class is used in several utility functions involving <a>F</a> and
--   <a>T</a>.
--   
--   Conceptually <a>point</a> should be of type <tt>a -&gt; m a</tt>, but
--   we need the extra flexibility to make restricted monads like
--   <a>Set</a> instances.
--   
--   Note: We have <tt>instance (Monad m) =&gt; Pointed a (m a)</tt>, but
--   Haddock currently doesn't display this.
class Pointed a b | b -> a
point :: (Pointed a b) => a -> b

-- | This class is used in several utility functions involving <a>F</a> and
--   <a>T</a>.
--   
--   Conceptually <a>copoint</a> should be of type <tt>w a -&gt; a</tt>,
--   but let's keep the extra flexibility.
class Copointed a b | b -> a
copoint :: (Copointed a b) => b -> a
unwrapF :: (Copointed (Formula0 (T t) (F t)) (t (Formula0 (T t) (F t)))) => F t -> Formula0 (T t) (F t)
unwrapT :: (Copointed (Term0 (T t)) (t (Term0 (T t)))) => T t -> Term0 (T t)
foldFormula0 :: (f -> r) -> (Quant -> [V] -> f -> r) -> (f -> BinOp -> f -> r) -> (t -> InfixPred -> t -> r) -> (AtomicWord -> [t] -> r) -> Formula0 t f -> r
foldTerm0 :: (String -> r) -> (Double -> r) -> (V -> r) -> (AtomicWord -> [t] -> r) -> Term0 t -> r

-- | Eliminate formulae
foldF :: (Copointed (Formula0 (T t) (F t)) (t (Formula0 (T t) (F t)))) => (F t -> r) -> (Quant -> [V] -> F t -> r) -> (F t -> BinOp -> F t -> r) -> (T t -> InfixPred -> T t -> r) -> (AtomicWord -> [T t] -> r) -> (F t -> r)

-- | Eliminate terms
foldT :: (Copointed (Term0 (T t)) (t (Term0 (T t)))) => (String -> r) -> (Double -> r) -> (V -> r) -> (AtomicWord -> [T t] -> r) -> (T t -> r)
instance [overlap ok] Typeable V
instance [overlap ok] Typeable AtomicWord
instance [overlap ok] Typeable GTerm
instance [overlap ok] Typeable GData
instance [overlap ok] Typeable Role
instance [overlap ok] Typeable UsefulInfo
instance [overlap ok] Typeable Annotations
instance [overlap ok] Typeable TPTP_Input
instance [overlap ok] Typeable Quant
instance [overlap ok] Typeable InfixPred
instance [overlap ok] Typeable BinOp
instance [overlap ok] Typeable1 Term0
instance [overlap ok] Typeable2 Formula0
instance [overlap ok] (Typeable1 c, Data (c (Formula0 (T c) (F c)))) => Data (F c)
instance [overlap ok] (Typeable1 c, Data (c (Term0 (T c)))) => Data (T c)
instance [overlap ok] (Read (c (Formula0 (T c) (F c)))) => Read (F c)
instance [overlap ok] (Read (c (Term0 (T c)))) => Read (T c)
instance [overlap ok] (Show (c (Formula0 (T c) (F c)))) => Show (F c)
instance [overlap ok] (Show (c (Term0 (T c)))) => Show (T c)
instance [overlap ok] (Ord (c (Formula0 (T c) (F c)))) => Ord (F c)
instance [overlap ok] (Ord (c (Term0 (T c)))) => Ord (T c)
instance [overlap ok] (Eq (c (Formula0 (T c) (F c)))) => Eq (F c)
instance [overlap ok] (Eq (c (Term0 (T c)))) => Eq (T c)
instance [overlap ok] Typeable1 Identity
instance [overlap ok] (Data a) => Data (Identity a)
instance [overlap ok] (Read a) => Read (Identity a)
instance [overlap ok] (Show a) => Show (Identity a)
instance [overlap ok] (Ord a) => Ord (Identity a)
instance [overlap ok] (Eq a) => Eq (Identity a)
instance [overlap ok] Eq V
instance [overlap ok] Ord V
instance [overlap ok] Show V
instance [overlap ok] Data V
instance [overlap ok] Read V
instance [overlap ok] Monoid V
instance [overlap ok] IsString V
instance [overlap ok] Eq AtomicWord
instance [overlap ok] Ord AtomicWord
instance [overlap ok] Show AtomicWord
instance [overlap ok] Data AtomicWord
instance [overlap ok] Read AtomicWord
instance [overlap ok] Monoid AtomicWord
instance [overlap ok] IsString AtomicWord
instance [overlap ok] Eq GTerm
instance [overlap ok] Ord GTerm
instance [overlap ok] Show GTerm
instance [overlap ok] Read GTerm
instance [overlap ok] Data GTerm
instance [overlap ok] Eq GData
instance [overlap ok] Ord GData
instance [overlap ok] Show GData
instance [overlap ok] Read GData
instance [overlap ok] Data GData
instance [overlap ok] Eq Role
instance [overlap ok] Ord Role
instance [overlap ok] Show Role
instance [overlap ok] Read Role
instance [overlap ok] Data Role
instance [overlap ok] Eq UsefulInfo
instance [overlap ok] Ord UsefulInfo
instance [overlap ok] Show UsefulInfo
instance [overlap ok] Read UsefulInfo
instance [overlap ok] Data UsefulInfo
instance [overlap ok] Eq Annotations
instance [overlap ok] Ord Annotations
instance [overlap ok] Show Annotations
instance [overlap ok] Read Annotations
instance [overlap ok] Data Annotations
instance [overlap ok] Eq TPTP_Input
instance [overlap ok] Ord TPTP_Input
instance [overlap ok] Show TPTP_Input
instance [overlap ok] Read TPTP_Input
instance [overlap ok] Data TPTP_Input
instance [overlap ok] Eq Quant
instance [overlap ok] Ord Quant
instance [overlap ok] Show Quant
instance [overlap ok] Read Quant
instance [overlap ok] Data Quant
instance [overlap ok] Enum Quant
instance [overlap ok] Bounded Quant
instance [overlap ok] Eq InfixPred
instance [overlap ok] Ord InfixPred
instance [overlap ok] Show InfixPred
instance [overlap ok] Read InfixPred
instance [overlap ok] Data InfixPred
instance [overlap ok] Enum InfixPred
instance [overlap ok] Bounded InfixPred
instance [overlap ok] Eq BinOp
instance [overlap ok] Ord BinOp
instance [overlap ok] Show BinOp
instance [overlap ok] Read BinOp
instance [overlap ok] Data BinOp
instance [overlap ok] Enum BinOp
instance [overlap ok] Bounded BinOp
instance [overlap ok] (Eq term) => Eq (Term0 term)
instance [overlap ok] (Ord term) => Ord (Term0 term)
instance [overlap ok] (Show term) => Show (Term0 term)
instance [overlap ok] (Read term) => Read (Term0 term)
instance [overlap ok] (Data term) => Data (Term0 term)
instance [overlap ok] (Eq term, Eq formula) => Eq (Formula0 term formula)
instance [overlap ok] (Ord term, Ord formula) => Ord (Formula0 term formula)
instance [overlap ok] (Show term, Show formula) => Show (Formula0 term formula)
instance [overlap ok] (Read term, Read formula) => Read (Formula0 term formula)
instance [overlap ok] (Data term, Data formula) => Data (Formula0 term formula)
instance [overlap ok] Copointed a (Identity a)
instance [overlap ok] (Ord a) => Pointed a (Set a)
instance [overlap ok] (Monad m) => Pointed a (m a)
instance [overlap ok] (Typeable1 c) => Typeable (T c)
instance [overlap ok] (Typeable1 c) => Typeable (F c)
instance [overlap ok] Arbitrary V
instance [overlap ok] Arbitrary AtomicWord
instance [overlap ok] Arbitrary GTerm
instance [overlap ok] Arbitrary GData
instance [overlap ok] (Arbitrary a) => Arbitrary (Term0 a)
instance [overlap ok] Arbitrary Quant
instance [overlap ok] Arbitrary InfixPred
instance [overlap ok] Arbitrary BinOp
instance [overlap ok] (Arbitrary a, Arbitrary b) => Arbitrary (Formula0 a b)
instance [overlap ok] Arbitrary Role
instance [overlap ok] Arbitrary UsefulInfo
instance [overlap ok] Arbitrary Annotations
instance [overlap ok] Arbitrary Term
instance [overlap ok] Arbitrary Formula
instance [overlap ok] Arbitrary TPTP_Input
instance [overlap ok] FreeVars Term
instance [overlap ok] FreeVars Formula

module Codec.TPTP.Export

-- | Convenient wrapper for <a>toTPTP</a>
toTPTP' :: (ToTPTP a) => a -> String
class ToTPTP a
toTPTP :: (ToTPTP a) => a -> ShowS
isLowerWord :: [Char] -> Bool
instance ToTPTP (T Identity)
instance ToTPTP (F Identity)
instance (ToTPTP a) => ToTPTP (Identity a)
instance ToTPTP V
instance ToTPTP GData
instance ToTPTP AtomicWord
instance ToTPTP GTerm
instance ToTPTP UsefulInfo
instance ToTPTP Annotations
instance (ToTPTP t) => ToTPTP (Term0 t)
instance (ToTPTP f, ToTPTP t) => ToTPTP (Formula0 t f)
instance ToTPTP BinOp
instance ToTPTP InfixPred
instance ToTPTP Quant
instance ToTPTP Role
instance ToTPTP TPTP_Input
instance ToTPTP [TPTP_Input]


-- | Mainly just <a>Pretty</a> instances
module Codec.TPTP.Pretty
prettySimple :: (Pretty a) => a -> String

-- | Carries information about the enclosing operation (for the purpose of
--   printing stuff without parentheses if possible).
data WithEnclosing a
WithEnclosing :: Enclosing -> a -> WithEnclosing a
data Enclosing
EnclBinOp :: BinOp -> Enclosing
EnclQuant :: Enclosing
EnclNeg :: Enclosing
EnclInfixPred :: InfixPred -> Enclosing
EnclNothing :: Enclosing
instance Typeable Enclosing
instance (Pretty a) => Pretty (Identity a)
instance Pretty (T Identity)
instance Pretty (F Identity)
instance Eq Enclosing
instance Ord Enclosing
instance Show Enclosing
instance Data Enclosing
instance Read Enclosing
instance Pretty V
instance Pretty GTerm
instance Pretty AtomicWord
instance Pretty GData
instance Pretty UsefulInfo
instance Pretty Annotations
instance Pretty (WithEnclosing Term)
instance Pretty (WithEnclosing Formula)
instance Pretty (Term0 Term)
instance Pretty (Formula0 Term Formula)
instance (Pretty (WithEnclosing t)) => Pretty (WithEnclosing (Term0 t))
instance Pretty InfixPred
instance Pretty BinOp
instance (Pretty (WithEnclosing t), Pretty (WithEnclosing f)) => Pretty (WithEnclosing (Formula0 t f))
instance Pretty Quant
instance Pretty TPTP_Input

module Codec.TPTP.Diff
class Diffable a b
diff :: (Diffable a b) => a -> a -> b
data DiffResult d

-- | Both arguments are the same.
Same :: DiffResult d

-- | The arguments are recursive expressions of the same form, but their
--   subterms differ. Return a "decorated" term that shows where the
--   differences are
SameHead :: d -> DiffResult d

-- | The arguments differ and are not of similar form (don't recurse)
Differ :: d -> d -> DiffResult d
DontCare :: DiffResult d
type T0Diff = DiffResult (Term0 (T DiffResult))
type F0Diff = DiffResult (Formula0 (T DiffResult) (F DiffResult))
isSame :: DiffResult t -> Bool

-- | Less random generator for generating formulae suitable for testing
--   diff
diffGenF :: Gen Formula
diffGenT :: Gen Term
printSampleDiffs :: IO ()
instance Typeable1 DiffResult
instance Pretty (F DiffResult)
instance Pretty (T DiffResult)
instance (Eq d) => Eq (DiffResult d)
instance (Ord d) => Ord (DiffResult d)
instance (Show d) => Show (DiffResult d)
instance (Data d) => Data (DiffResult d)
instance (Read d) => Read (DiffResult d)
instance Diffable Term (T DiffResult)
instance Diffable Formula (F DiffResult)
instance Functor DiffResult
instance Pretty F0Diff
instance Pretty T0Diff
instance Pretty (WithEnclosing (F DiffResult))
instance Pretty (WithEnclosing (T DiffResult))
instance Pretty (WithEnclosing F0Diff)
instance Pretty (WithEnclosing T0Diff)
instance Show (F DiffResult)
instance Show (T DiffResult)

module Codec.TPTP.Import
parse :: String -> [TPTP_Input]
parseFile :: FilePath -> IO [TPTP_Input]
data Token
LP :: Token
RP :: Token
Comma :: Token
Dot :: Token
Lbrack :: Token
Rbrack :: Token
Oper :: String -> Token
SingleQuoted :: String -> Token
DoubleQuoted :: String -> Token
DollarWord :: String -> Token
DollarDollarWord :: String -> Token
UpperWord :: String -> Token
LowerWord :: String -> Token
Star :: Token
Plus :: Token
Rangle :: Token
SignedInt :: Int -> Token
UnsignedInt :: Int -> Token
Real :: Double -> Token
CommentToken :: String -> Token

module Codec.TPTP