-- 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 all files in the TPTP (v 5.2.0) distribution's
--   <tt>Problems</tt> subtree which don't match the regex "^(thf|tff)(",
--   <tt>parse . toTPTP . parse == parse</tt></li>
--   </ul>
--   
--   Not yet implemented: The new <i>thf</i> and <i>tff</i> formula types.
@package logic-TPTP
@version 0.4.7.0

module Codec.TPTP.Base

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

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

-- | First-order formulae decorated with state
type FormulaST s = F (State s)

-- | Terms decorated with state
type TermST s = T (State s)

-- | First-order formulae decorated with comments
type FormulaC = FormulaST [String]

-- | Terms decorated with comments
type TermC = TermST [String]

-- | Forget comments in formulae decorated with comments
forgetFC :: FormulaC -> Formula

-- | Forget comments in terms decorated with comments
forgetTC :: TermC -> Term

-- | Equivalence
--   
--   Important special case:
--   
--   <pre>
--   &lt;math&gt; :: <a>Formula</a> -&gt; <a>Formula</a> -&gt; <a>Formula</a>
--   </pre>
(.<=>.) :: Pointed c => F c -> F c -> F c
infixl 2 .<=>.

-- | Implication
(.=>.) :: Pointed c => F c -> F c -> F c
infixl 2 .=>.

-- | Reverse implication
(.<=.) :: Pointed c => F c -> F c -> F c
infixl 2 .<=.

-- | Disjunction/OR
(.|.) :: Pointed c => F c -> F c -> F c
infixl 3 .|.

-- | Conjunction/AND
(.&.) :: Pointed c => F c -> F c -> F c
infixl 4 .&.

-- | XOR
(.<~>.) :: Pointed c => F c -> F c -> F c
infixl 2 .<~>.

-- | NOR
(.~|.) :: Pointed c => F c -> F c -> F c
infixl 3 .~|.

-- | NAND
(.~&.) :: Pointed c => F c -> F c -> F c
infixl 4 .~&.

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

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

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

-- | Universal quantification
for_all :: Pointed c => [V] -> F c -> F c

-- | Existential quantification
exists :: Pointed c => [V] -> F c -> F c

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

-- | Variable
var :: Pointed c => V -> T c

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

-- | Number literal
numberLitTerm :: Pointed c => Rational -> T c

-- | Double-quoted string literal, called <i>Distinct Object</i> in TPTP's
--   grammar
distinctObjectTerm :: Pointed 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 :: Rational -> Term0 term

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

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

-- | 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.
type TPTP_Input = TPTP_Input_ Identity

-- | A line of a TPTP file: Annotated formula (with the comment string
--   embbeded in the State monad ), comment or include statement
type TPTP_Input_C = TPTP_Input_ (State [String])

-- | Forget comments in a line of a TPTP file decorated with comments
forgetTIC :: TPTP_Input_C -> TPTP_Input

-- | Generalized TPTP_Input
data TPTP_Input_ c

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

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

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

-- | Formula roles
newtype 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 :: Rational -> 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

-- | Obtain the free variables from a formula or term
freeVars :: FreeVars a => a -> Set V

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

-- | Universally quantify all free variables in the formula
univquant_free_vars_FC :: FormulaC -> FormulaC

-- | 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

-- | 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 = <tt>IORef</tt></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))
unwrapF :: Copointed t => F t -> Formula0 (T t) (F t)
unwrapT :: Copointed 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) -> (Rational -> r) -> (V -> r) -> (AtomicWord -> [t] -> r) -> Term0 t -> r

-- | Eliminate formulae
foldF :: Copointed 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 t => (String -> r) -> (Rational -> r) -> (V -> r) -> (AtomicWord -> [T t] -> r) -> T t -> r
instance Data.Data.Data Codec.TPTP.Base.Annotations
instance GHC.Read.Read Codec.TPTP.Base.Annotations
instance GHC.Show.Show Codec.TPTP.Base.Annotations
instance GHC.Classes.Ord Codec.TPTP.Base.Annotations
instance GHC.Classes.Eq Codec.TPTP.Base.Annotations
instance Data.Data.Data Codec.TPTP.Base.UsefulInfo
instance GHC.Read.Read Codec.TPTP.Base.UsefulInfo
instance GHC.Show.Show Codec.TPTP.Base.UsefulInfo
instance GHC.Classes.Ord Codec.TPTP.Base.UsefulInfo
instance GHC.Classes.Eq Codec.TPTP.Base.UsefulInfo
instance Data.Data.Data Codec.TPTP.Base.GTerm
instance GHC.Read.Read Codec.TPTP.Base.GTerm
instance GHC.Show.Show Codec.TPTP.Base.GTerm
instance GHC.Classes.Ord Codec.TPTP.Base.GTerm
instance GHC.Classes.Eq Codec.TPTP.Base.GTerm
instance Data.Data.Data Codec.TPTP.Base.GData
instance GHC.Read.Read Codec.TPTP.Base.GData
instance GHC.Show.Show Codec.TPTP.Base.GData
instance GHC.Classes.Ord Codec.TPTP.Base.GData
instance GHC.Classes.Eq Codec.TPTP.Base.GData
instance (Data.Data.Data term, Data.Data.Data formula) => Data.Data.Data (Codec.TPTP.Base.Formula0 term formula)
instance (GHC.Read.Read formula, GHC.Read.Read term) => GHC.Read.Read (Codec.TPTP.Base.Formula0 term formula)
instance (GHC.Show.Show formula, GHC.Show.Show term) => GHC.Show.Show (Codec.TPTP.Base.Formula0 term formula)
instance (GHC.Classes.Ord formula, GHC.Classes.Ord term) => GHC.Classes.Ord (Codec.TPTP.Base.Formula0 term formula)
instance (GHC.Classes.Eq formula, GHC.Classes.Eq term) => GHC.Classes.Eq (Codec.TPTP.Base.Formula0 term formula)
instance Data.Data.Data term => Data.Data.Data (Codec.TPTP.Base.Term0 term)
instance GHC.Read.Read term => GHC.Read.Read (Codec.TPTP.Base.Term0 term)
instance GHC.Show.Show term => GHC.Show.Show (Codec.TPTP.Base.Term0 term)
instance GHC.Classes.Ord term => GHC.Classes.Ord (Codec.TPTP.Base.Term0 term)
instance GHC.Classes.Eq term => GHC.Classes.Eq (Codec.TPTP.Base.Term0 term)
instance Data.String.IsString Codec.TPTP.Base.V
instance GHC.Base.Monoid Codec.TPTP.Base.V
instance GHC.Base.Semigroup Codec.TPTP.Base.V
instance GHC.Read.Read Codec.TPTP.Base.V
instance Data.Data.Data Codec.TPTP.Base.V
instance GHC.Show.Show Codec.TPTP.Base.V
instance GHC.Classes.Ord Codec.TPTP.Base.V
instance GHC.Classes.Eq Codec.TPTP.Base.V
instance Data.String.IsString Codec.TPTP.Base.AtomicWord
instance GHC.Base.Monoid Codec.TPTP.Base.AtomicWord
instance GHC.Base.Semigroup Codec.TPTP.Base.AtomicWord
instance GHC.Read.Read Codec.TPTP.Base.AtomicWord
instance Data.Data.Data Codec.TPTP.Base.AtomicWord
instance GHC.Show.Show Codec.TPTP.Base.AtomicWord
instance GHC.Classes.Ord Codec.TPTP.Base.AtomicWord
instance GHC.Classes.Eq Codec.TPTP.Base.AtomicWord
instance Data.Data.Data Codec.TPTP.Base.Role
instance GHC.Read.Read Codec.TPTP.Base.Role
instance GHC.Show.Show Codec.TPTP.Base.Role
instance GHC.Classes.Ord Codec.TPTP.Base.Role
instance GHC.Classes.Eq Codec.TPTP.Base.Role
instance GHC.Enum.Bounded Codec.TPTP.Base.Quant
instance GHC.Enum.Enum Codec.TPTP.Base.Quant
instance Data.Data.Data Codec.TPTP.Base.Quant
instance GHC.Read.Read Codec.TPTP.Base.Quant
instance GHC.Show.Show Codec.TPTP.Base.Quant
instance GHC.Classes.Ord Codec.TPTP.Base.Quant
instance GHC.Classes.Eq Codec.TPTP.Base.Quant
instance GHC.Enum.Bounded Codec.TPTP.Base.InfixPred
instance GHC.Enum.Enum Codec.TPTP.Base.InfixPred
instance Data.Data.Data Codec.TPTP.Base.InfixPred
instance GHC.Read.Read Codec.TPTP.Base.InfixPred
instance GHC.Show.Show Codec.TPTP.Base.InfixPred
instance GHC.Classes.Ord Codec.TPTP.Base.InfixPred
instance GHC.Classes.Eq Codec.TPTP.Base.InfixPred
instance GHC.Enum.Bounded Codec.TPTP.Base.BinOp
instance GHC.Enum.Enum Codec.TPTP.Base.BinOp
instance Data.Data.Data Codec.TPTP.Base.BinOp
instance GHC.Read.Read Codec.TPTP.Base.BinOp
instance GHC.Show.Show Codec.TPTP.Base.BinOp
instance GHC.Classes.Ord Codec.TPTP.Base.BinOp
instance GHC.Classes.Eq Codec.TPTP.Base.BinOp
instance GHC.Classes.Eq (c (Codec.TPTP.Base.Formula0 (Codec.TPTP.Base.T c) (Codec.TPTP.Base.F c))) => GHC.Classes.Eq (Codec.TPTP.Base.TPTP_Input_ c)
instance GHC.Classes.Ord (c (Codec.TPTP.Base.Formula0 (Codec.TPTP.Base.T c) (Codec.TPTP.Base.F c))) => GHC.Classes.Ord (Codec.TPTP.Base.TPTP_Input_ c)
instance GHC.Show.Show (c (Codec.TPTP.Base.Formula0 (Codec.TPTP.Base.T c) (Codec.TPTP.Base.F c))) => GHC.Show.Show (Codec.TPTP.Base.TPTP_Input_ c)
instance GHC.Read.Read (c (Codec.TPTP.Base.Formula0 (Codec.TPTP.Base.T c) (Codec.TPTP.Base.F c))) => GHC.Read.Read (Codec.TPTP.Base.TPTP_Input_ c)
instance (Data.Typeable.Internal.Typeable c, Data.Data.Data (c (Codec.TPTP.Base.Formula0 (Codec.TPTP.Base.T c) (Codec.TPTP.Base.F c)))) => Data.Data.Data (Codec.TPTP.Base.TPTP_Input_ c)
instance GHC.Classes.Eq (c (Codec.TPTP.Base.Term0 (Codec.TPTP.Base.T c))) => GHC.Classes.Eq (Codec.TPTP.Base.T c)
instance GHC.Classes.Eq (c (Codec.TPTP.Base.Formula0 (Codec.TPTP.Base.T c) (Codec.TPTP.Base.F c))) => GHC.Classes.Eq (Codec.TPTP.Base.F c)
instance GHC.Classes.Ord (c (Codec.TPTP.Base.Term0 (Codec.TPTP.Base.T c))) => GHC.Classes.Ord (Codec.TPTP.Base.T c)
instance GHC.Classes.Ord (c (Codec.TPTP.Base.Formula0 (Codec.TPTP.Base.T c) (Codec.TPTP.Base.F c))) => GHC.Classes.Ord (Codec.TPTP.Base.F c)
instance GHC.Show.Show (c (Codec.TPTP.Base.Term0 (Codec.TPTP.Base.T c))) => GHC.Show.Show (Codec.TPTP.Base.T c)
instance GHC.Show.Show (c (Codec.TPTP.Base.Formula0 (Codec.TPTP.Base.T c) (Codec.TPTP.Base.F c))) => GHC.Show.Show (Codec.TPTP.Base.F c)
instance GHC.Read.Read (c (Codec.TPTP.Base.Term0 (Codec.TPTP.Base.T c))) => GHC.Read.Read (Codec.TPTP.Base.T c)
instance GHC.Read.Read (c (Codec.TPTP.Base.Formula0 (Codec.TPTP.Base.T c) (Codec.TPTP.Base.F c))) => GHC.Read.Read (Codec.TPTP.Base.F c)
instance (Data.Typeable.Internal.Typeable c, Data.Data.Data (c (Codec.TPTP.Base.Term0 (Codec.TPTP.Base.T c)))) => Data.Data.Data (Codec.TPTP.Base.T c)
instance (Data.Typeable.Internal.Typeable c, Data.Data.Data (c (Codec.TPTP.Base.Formula0 (Codec.TPTP.Base.T c) (Codec.TPTP.Base.F c)))) => Data.Data.Data (Codec.TPTP.Base.F c)
instance Codec.TPTP.Base.FreeVars Codec.TPTP.Base.Term
instance Test.QuickCheck.Arbitrary.Arbitrary Codec.TPTP.Base.Term
instance Test.QuickCheck.Arbitrary.Arbitrary Codec.TPTP.Base.TPTP_Input
instance Test.QuickCheck.Arbitrary.Arbitrary Codec.TPTP.Base.Annotations
instance Test.QuickCheck.Arbitrary.Arbitrary Codec.TPTP.Base.UsefulInfo
instance Test.QuickCheck.Arbitrary.Arbitrary Codec.TPTP.Base.GData
instance Test.QuickCheck.Arbitrary.Arbitrary Codec.TPTP.Base.GTerm
instance Codec.TPTP.Base.FreeVars Codec.TPTP.Base.Formula
instance Test.QuickCheck.Arbitrary.Arbitrary Codec.TPTP.Base.Formula
instance (Test.QuickCheck.Arbitrary.Arbitrary a, Test.QuickCheck.Arbitrary.Arbitrary b) => Test.QuickCheck.Arbitrary.Arbitrary (Codec.TPTP.Base.Formula0 a b)
instance Test.QuickCheck.Arbitrary.Arbitrary a => Test.QuickCheck.Arbitrary.Arbitrary (Codec.TPTP.Base.Term0 a)
instance Test.QuickCheck.Arbitrary.Arbitrary Codec.TPTP.Base.V
instance Test.QuickCheck.Arbitrary.Arbitrary Codec.TPTP.Base.AtomicWord
instance Test.QuickCheck.Arbitrary.Arbitrary Codec.TPTP.Base.Role
instance Test.QuickCheck.Arbitrary.Arbitrary Codec.TPTP.Base.Quant
instance Test.QuickCheck.Arbitrary.Arbitrary Codec.TPTP.Base.InfixPred
instance Test.QuickCheck.Arbitrary.Arbitrary Codec.TPTP.Base.BinOp

module Codec.TPTP.Export

-- | Convenient wrapper for <a>toTPTP</a>
toTPTP' :: forall a. ToTPTP a => a -> String
class ToTPTP a

-- | Convert to TPTP
toTPTP :: ToTPTP a => a -> ShowS
isLowerWord :: [Char] -> Bool
instance Codec.TPTP.Export.ToTPTP a => Codec.TPTP.Export.ToTPTP (Data.Functor.Identity.Identity a)
instance Codec.TPTP.Export.ToTPTP (Codec.TPTP.Base.F Data.Functor.Identity.Identity)
instance Codec.TPTP.Export.ToTPTP (Codec.TPTP.Base.T Data.Functor.Identity.Identity)
instance Codec.TPTP.Export.ToTPTP [Codec.TPTP.Base.TPTP_Input]
instance Codec.TPTP.Export.ToTPTP Codec.TPTP.Base.TPTP_Input
instance Codec.TPTP.Export.ToTPTP Codec.TPTP.Base.Role
instance Codec.TPTP.Export.ToTPTP Codec.TPTP.Base.Quant
instance Codec.TPTP.Export.ToTPTP Codec.TPTP.Base.InfixPred
instance Codec.TPTP.Export.ToTPTP Codec.TPTP.Base.BinOp
instance (Codec.TPTP.Export.ToTPTP f, Codec.TPTP.Export.ToTPTP t) => Codec.TPTP.Export.ToTPTP (Codec.TPTP.Base.Formula0 t f)
instance Codec.TPTP.Export.ToTPTP t => Codec.TPTP.Export.ToTPTP (Codec.TPTP.Base.Term0 t)
instance Codec.TPTP.Export.ToTPTP Codec.TPTP.Base.Annotations
instance Codec.TPTP.Export.ToTPTP Codec.TPTP.Base.UsefulInfo
instance Codec.TPTP.Export.ToTPTP Codec.TPTP.Base.GTerm
instance Codec.TPTP.Export.ToTPTP Codec.TPTP.Base.AtomicWord
instance Codec.TPTP.Export.ToTPTP Codec.TPTP.Base.GData
instance Codec.TPTP.Export.ToTPTP Codec.TPTP.Base.V


-- | 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 GHC.Read.Read Codec.TPTP.Pretty.Enclosing
instance Data.Data.Data Codec.TPTP.Pretty.Enclosing
instance GHC.Show.Show Codec.TPTP.Pretty.Enclosing
instance GHC.Classes.Ord Codec.TPTP.Pretty.Enclosing
instance GHC.Classes.Eq Codec.TPTP.Pretty.Enclosing
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty (Codec.TPTP.Base.F Data.Functor.Identity.Identity)
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty (Codec.TPTP.Base.T Data.Functor.Identity.Identity)
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty a => Text.PrettyPrint.ANSI.Leijen.Internal.Pretty (Data.Functor.Identity.Identity a)
instance (Text.PrettyPrint.ANSI.Leijen.Internal.Pretty (Codec.TPTP.Pretty.WithEnclosing t), Text.PrettyPrint.ANSI.Leijen.Internal.Pretty (Codec.TPTP.Pretty.WithEnclosing f)) => Text.PrettyPrint.ANSI.Leijen.Internal.Pretty (Codec.TPTP.Pretty.WithEnclosing (Codec.TPTP.Base.Formula0 t f))
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty (Codec.TPTP.Pretty.WithEnclosing t) => Text.PrettyPrint.ANSI.Leijen.Internal.Pretty (Codec.TPTP.Pretty.WithEnclosing (Codec.TPTP.Base.Term0 t))
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty (Codec.TPTP.Base.Formula0 Codec.TPTP.Base.Term Codec.TPTP.Base.Formula)
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty (Codec.TPTP.Base.Term0 Codec.TPTP.Base.Term)
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty (Codec.TPTP.Pretty.WithEnclosing Codec.TPTP.Base.Formula)
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty (Codec.TPTP.Pretty.WithEnclosing Codec.TPTP.Base.Term)
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty Codec.TPTP.Base.TPTP_Input
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty Codec.TPTP.Base.Quant
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty Codec.TPTP.Base.BinOp
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty Codec.TPTP.Base.InfixPred
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty Codec.TPTP.Base.Annotations
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty Codec.TPTP.Base.UsefulInfo
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty Codec.TPTP.Base.GData
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty Codec.TPTP.Base.AtomicWord
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty Codec.TPTP.Base.GTerm
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty Codec.TPTP.Base.V

module Codec.TPTP.Diff
class Diffable a b | 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 :: forall t. DiffResult t -> Bool

-- | Less random generator for generating formulae suitable for testing
--   diff
diffGenF :: Gen Formula
diffGenT :: Gen Term
printSampleDiffs :: IO ()
instance GHC.Read.Read d => GHC.Read.Read (Codec.TPTP.Diff.DiffResult d)
instance Data.Data.Data d => Data.Data.Data (Codec.TPTP.Diff.DiffResult d)
instance GHC.Show.Show d => GHC.Show.Show (Codec.TPTP.Diff.DiffResult d)
instance GHC.Classes.Ord d => GHC.Classes.Ord (Codec.TPTP.Diff.DiffResult d)
instance GHC.Classes.Eq d => GHC.Classes.Eq (Codec.TPTP.Diff.DiffResult d)
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty (Codec.TPTP.Base.T Codec.TPTP.Diff.DiffResult)
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty (Codec.TPTP.Base.F Codec.TPTP.Diff.DiffResult)
instance Codec.TPTP.Diff.Diffable Codec.TPTP.Base.Formula (Codec.TPTP.Base.F Codec.TPTP.Diff.DiffResult)
instance Codec.TPTP.Diff.Diffable Codec.TPTP.Base.Term (Codec.TPTP.Base.T Codec.TPTP.Diff.DiffResult)
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty (Codec.TPTP.Pretty.WithEnclosing Codec.TPTP.Diff.F0Diff)
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty Codec.TPTP.Diff.F0Diff
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty (Codec.TPTP.Pretty.WithEnclosing Codec.TPTP.Diff.T0Diff)
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty Codec.TPTP.Diff.T0Diff
instance GHC.Show.Show (Codec.TPTP.Base.T Codec.TPTP.Diff.DiffResult)
instance GHC.Show.Show (Codec.TPTP.Base.F Codec.TPTP.Diff.DiffResult)
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty (Codec.TPTP.Pretty.WithEnclosing (Codec.TPTP.Base.T Codec.TPTP.Diff.DiffResult))
instance Text.PrettyPrint.ANSI.Leijen.Internal.Pretty (Codec.TPTP.Pretty.WithEnclosing (Codec.TPTP.Base.F Codec.TPTP.Diff.DiffResult))
instance GHC.Base.Functor Codec.TPTP.Diff.DiffResult

module Codec.TPTP.Import
parse :: String -> [TPTP_Input]
parseFile :: FilePath -> IO [TPTP_Input]
parseWithComment :: String -> [TPTP_Input_C]
parseWithCommentFile :: FilePath -> IO [TPTP_Input_C]
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 :: Integer -> Token
UnsignedInt :: Integer -> Token
Real :: Rational -> Token
CommentToken :: String -> Token
Slash :: Token

module Codec.TPTP