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


-- | Import, export and other utilities 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 concisely 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 each problem in the TPTP library (v 3.7.0.0) which doesn'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.1

module Codec.TPTP.Base

-- | Basic (undecorated) first-order formulae
newtype Formula
FF :: (Formula0 Term Formula) -> Formula

-- | Basic (undecorated) terms
newtype Term
TT :: (Term0 Term) -> Term
(.<=>.) :: Formula -> Formula -> Formula
(.<~>.) :: Formula -> Formula -> Formula
(.=>.) :: Formula -> Formula -> Formula
(.<=.) :: Formula -> Formula -> Formula
(.~|.) :: Formula -> Formula -> Formula
(.|.) :: Formula -> Formula -> Formula
(.~&.) :: Formula -> Formula -> Formula
(.&.) :: Formula -> Formula -> Formula
(.~.) :: Formula -> Formula
(.=.) :: Term -> Term -> Formula
(.!=.) :: Term -> Term -> Formula
for_all :: [String] -> Formula -> Formula
exists :: [String] -> Formula -> Formula
pApp :: AtomicWord -> [Term] -> Formula
var :: String -> Term
fApp :: AtomicWord -> [Term] -> Term
numberLitTerm :: Double -> Term
distinctObjectTerm :: String -> Term

-- | 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>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 -> [String] -> 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 :: String -> Term0 term

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

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

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

-- | Binary formula connectives
data BinOp

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

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

-- | Implication (reverse)
(:<=:) :: 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 -> SourceInfo -> UsefulInfo -> TPTP_Input
name :: TPTP_Input -> AtomicWord
role :: TPTP_Input -> Role
formula :: TPTP_Input -> Formula
sourceInfo :: TPTP_Input -> SourceInfo
usefulInfo :: TPTP_Input -> UsefulInfo
Comment :: String -> TPTP_Input
Include :: FilePath -> [AtomicWord] -> TPTP_Input

-- | Annotations about the formulas origin
data SourceInfo
NoSourceInfo :: SourceInfo
SourceInfo :: GTerm -> SourceInfo

-- | 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 :: String -> 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 FormulaOrTerm a
elimFormulaOrTerm :: (FormulaOrTerm a) => (Formula -> r) -> (Term -> r) -> a -> r

-- | Get the free variables
free_vars :: (FormulaOrTerm a) => a -> Set String

-- | Universally quantify all free variables in the formula
univquant_free_vars :: Formula -> Formula
free_vars0 :: (Data d) => d -> Set String

-- | Tip: Use the <tt>-XOverloadedStrings</tt> compiler flag if you don't
--   want to type <i>AtomicWord</i> to construct an <a>AtomicWord</a>
newtype AtomicWord
AtomicWord :: String -> AtomicWord

-- | For a given type constructor <tt>f</tt>, make the fixed point type
--   <tt>Y</tt> satisfying:
--   
--   <pre>
--   Y = f (Term0 Y)
--   </pre>
--   
--   (modulo newtype wrapping). See for example diffFormula.
newtype TermFix f
TermFix :: f (Term0 (TermFix f)) -> TermFix f
runTermFix :: TermFix f -> f (Term0 (TermFix f))

-- | For a given type constructor <tt>f</tt>, make the fixed point type
--   <tt>X</tt> satisfying:
--   
--   <pre>
--   X = f (Formula0 Y X) 
--   Y = f (Term0 Y)
--   </pre>
--   
--   (modulo newtype wrapping). See for example diffTerm.
newtype FormulaFix f
FormulaFix :: f (Formula0 (TermFix f) (FormulaFix f)) -> FormulaFix f
runFormulaFix :: FormulaFix f -> f (Formula0 (TermFix f) (FormulaFix f))
instance Typeable AtomicWord
instance Typeable GTerm
instance Typeable GData
instance Typeable Role
instance Typeable UsefulInfo
instance Typeable SourceInfo
instance Typeable TPTP_Input
instance Typeable Quant
instance Typeable InfixPred
instance Typeable BinOp
instance Typeable1 Term0
instance Typeable2 Formula0
instance Typeable Term
instance Typeable Formula
instance Eq AtomicWord
instance Ord AtomicWord
instance Show AtomicWord
instance Data AtomicWord
instance Read AtomicWord
instance Monoid AtomicWord
instance IsString AtomicWord
instance Eq GTerm
instance Ord GTerm
instance Show GTerm
instance Read GTerm
instance Data GTerm
instance Eq GData
instance Ord GData
instance Show GData
instance Read GData
instance Data GData
instance Eq Role
instance Ord Role
instance Show Role
instance Read Role
instance Data Role
instance Eq UsefulInfo
instance Ord UsefulInfo
instance Show UsefulInfo
instance Read UsefulInfo
instance Data UsefulInfo
instance Eq SourceInfo
instance Ord SourceInfo
instance Show SourceInfo
instance Read SourceInfo
instance Data SourceInfo
instance Eq TPTP_Input
instance Ord TPTP_Input
instance Show TPTP_Input
instance Read TPTP_Input
instance Data TPTP_Input
instance Eq Quant
instance Ord Quant
instance Show Quant
instance Read Quant
instance Data Quant
instance Enum Quant
instance Bounded Quant
instance Eq InfixPred
instance Ord InfixPred
instance Show InfixPred
instance Read InfixPred
instance Data InfixPred
instance Enum InfixPred
instance Bounded InfixPred
instance Eq BinOp
instance Ord BinOp
instance Show BinOp
instance Read BinOp
instance Data BinOp
instance Enum BinOp
instance Bounded BinOp
instance (Eq term) => Eq (Term0 term)
instance (Ord term) => Ord (Term0 term)
instance (Show term) => Show (Term0 term)
instance (Read term) => Read (Term0 term)
instance (Data term) => Data (Term0 term)
instance (Eq term, Eq formula) => Eq (Formula0 term formula)
instance (Ord term, Ord formula) => Ord (Formula0 term formula)
instance (Show term, Show formula) => Show (Formula0 term formula)
instance (Read term, Read formula) => Read (Formula0 term formula)
instance (Data term, Data formula) => Data (Formula0 term formula)
instance Eq Term
instance Ord Term
instance Show Term
instance Read Term
instance Data Term
instance Eq Formula
instance Ord Formula
instance Show Formula
instance Read Formula
instance Data Formula
instance Arbitrary AtomicWord
instance Arbitrary GTerm
instance Arbitrary GData
instance (Arbitrary a) => Arbitrary (Term0 a)
instance Arbitrary Quant
instance Arbitrary InfixPred
instance Arbitrary BinOp
instance (Arbitrary a, Arbitrary b) => Arbitrary (Formula0 a b)
instance Arbitrary Role
instance Arbitrary UsefulInfo
instance Arbitrary SourceInfo
instance Arbitrary Term
instance Arbitrary Formula
instance Arbitrary TPTP_Input
instance FormulaOrTerm Term
instance FormulaOrTerm 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 Term
instance ToTPTP Formula
instance ToTPTP GData
instance ToTPTP AtomicWord
instance ToTPTP GTerm
instance ToTPTP UsefulInfo
instance ToTPTP SourceInfo
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 Term
instance Pretty Formula
instance Eq Enclosing
instance Ord Enclosing
instance Show Enclosing
instance Data Enclosing
instance Read Enclosing
instance Pretty GTerm
instance Pretty AtomicWord
instance Pretty GData
instance Pretty UsefulInfo
instance Pretty SourceInfo
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 (TermFix DiffResult))
type F0Diff = DiffResult (Formula0 (TermFix DiffResult) (FormulaFix 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 (FormulaFix DiffResult)
instance Pretty (TermFix 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 (TermFix DiffResult)
instance Diffable Formula (FormulaFix DiffResult)
instance Functor DiffResult
instance Pretty F0Diff
instance Pretty T0Diff
instance Pretty (WithEnclosing (FormulaFix DiffResult))
instance Pretty (WithEnclosing (TermFix DiffResult))
instance Pretty (WithEnclosing F0Diff)
instance Pretty (WithEnclosing T0Diff)
instance Show (FormulaFix DiffResult)
instance Show (TermFix 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