Safe Haskell | None |
---|---|
Language | Haskell98 |
Synopsis
- type Formula = F Identity
- type Term = T Identity
- type FormulaST s = F (State s)
- type TermST s = T (State s)
- type FormulaC = FormulaST [String]
- type TermC = TermST [String]
- forgetFC :: FormulaC -> Formula
- forgetTC :: TermC -> Term
- (.<=>.) :: Pointed c => F c -> F c -> F c
- (.=>.) :: Pointed c => F c -> F c -> F c
- (.<=.) :: Pointed c => F c -> F c -> F c
- (.|.) :: Pointed c => F c -> F c -> F c
- (.&.) :: Pointed c => F c -> F c -> F c
- (.<~>.) :: Pointed c => F c -> F c -> F c
- (.~|.) :: Pointed c => F c -> F c -> F c
- (.~&.) :: Pointed c => F c -> F c -> F c
- (.~.) :: Pointed c => F c -> F c
- (.=.) :: Pointed c => T c -> T c -> F c
- (.!=.) :: Pointed c => T c -> T c -> F c
- for_all :: Pointed c => [V] -> F c -> F c
- exists :: Pointed c => [V] -> F c -> F c
- pApp :: Pointed c => AtomicWord -> [T c] -> F c
- var :: Pointed c => V -> T c
- fApp :: Pointed c => AtomicWord -> [T c] -> T c
- numberLitTerm :: Pointed c => Rational -> T c
- distinctObjectTerm :: Pointed c => String -> T c
- data Formula0 term formula
- data Term0 term
- = Var V
- | NumberLitTerm Rational
- | DistinctObjectTerm String
- | FunApp AtomicWord [term]
- data BinOp
- data InfixPred
- data Quant
- type TPTP_Input = TPTP_Input_ Identity
- type TPTP_Input_C = TPTP_Input_ (State [String])
- forgetTIC :: TPTP_Input_C -> TPTP_Input
- data TPTP_Input_ c
- = AFormula {
- name :: AtomicWord
- role :: Role
- formula :: F c
- annotations :: Annotations
- | Comment String
- | Include FilePath [AtomicWord]
- = AFormula {
- data Annotations
- data UsefulInfo
- = NoUsefulInfo
- | UsefulInfo [GTerm]
- newtype Role = Role {}
- data GData
- data GTerm
- class FreeVars a where
- univquant_free_vars :: Formula -> Formula
- newtype AtomicWord = AtomicWord String
- newtype V = V String
- newtype F c = F {}
- newtype T c = T {}
- 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
- 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
- foldT :: Copointed t => (String -> r) -> (Rational -> r) -> (V -> r) -> (AtomicWord -> [T t] -> r) -> T t -> r
Basic undecorated formulae and terms
Formulae and terms decorated with state
fApp :: Pointed c => AtomicWord -> [T c] -> T c Source #
Function symbol application (constants are encoded as nullary functions)
distinctObjectTerm :: Pointed c => String -> T c Source #
Double-quoted string literal, called Distinct Object in TPTP's grammar
General decorated formulae and terms
data Formula0 term formula Source #
See http://haskell.org/haskellwiki/Indirect_composite 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 Formula
and the wrapped constructors above.
BinOp formula BinOp formula | Binary connective application |
InfixPred term InfixPred term | Infix predicate application (equalities, inequalities) |
PredApp AtomicWord [term] | Predicate application |
Quant Quant [V] formula | Quantified formula |
(:~:) formula | Negation |
Instances
Pretty F0Diff # | |
Defined in Codec.TPTP.Diff | |
(Pretty (WithEnclosing t), Pretty (WithEnclosing f)) => Pretty (WithEnclosing (Formula0 t f)) # | |
Defined in Codec.TPTP.Pretty pretty :: WithEnclosing (Formula0 t f) -> Doc # prettyList :: [WithEnclosing (Formula0 t f)] -> Doc # | |
Pretty (WithEnclosing F0Diff) # | |
Defined in Codec.TPTP.Diff pretty :: WithEnclosing F0Diff -> Doc # prettyList :: [WithEnclosing F0Diff] -> Doc # | |
(Eq formula, Eq term) => Eq (Formula0 term formula) Source # | |
(Data term, Data formula) => Data (Formula0 term formula) Source # | |
Defined in Codec.TPTP.Base gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Formula0 term formula -> c (Formula0 term formula) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Formula0 term formula) # toConstr :: Formula0 term formula -> Constr # dataTypeOf :: Formula0 term formula -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Formula0 term formula)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Formula0 term formula)) # gmapT :: (forall b. Data b => b -> b) -> Formula0 term formula -> Formula0 term formula # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Formula0 term formula -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Formula0 term formula -> r # gmapQ :: (forall d. Data d => d -> u) -> Formula0 term formula -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Formula0 term formula -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Formula0 term formula -> m (Formula0 term formula) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Formula0 term formula -> m (Formula0 term formula) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Formula0 term formula -> m (Formula0 term formula) # | |
(Ord formula, Ord term) => Ord (Formula0 term formula) Source # | |
Defined in Codec.TPTP.Base compare :: Formula0 term formula -> Formula0 term formula -> Ordering # (<) :: Formula0 term formula -> Formula0 term formula -> Bool # (<=) :: Formula0 term formula -> Formula0 term formula -> Bool # (>) :: Formula0 term formula -> Formula0 term formula -> Bool # (>=) :: Formula0 term formula -> Formula0 term formula -> Bool # max :: Formula0 term formula -> Formula0 term formula -> Formula0 term formula # min :: Formula0 term formula -> Formula0 term formula -> Formula0 term formula # | |
(Read formula, Read term) => Read (Formula0 term formula) Source # | |
(Show formula, Show term) => Show (Formula0 term formula) Source # | |
(Arbitrary a, Arbitrary b) => Arbitrary (Formula0 a b) Source # | |
Pretty (Formula0 Term Formula) # | |
(ToTPTP f, ToTPTP t) => ToTPTP (Formula0 t f) Source # | |
See http://haskell.org/haskellwiki/Indirect_composite for the point of the type parameters (they allow for future decorations). If you don't need decorations, you can just use Term
and the wrapped constructors above.
Var V | Variable |
NumberLitTerm Rational | Number literal |
DistinctObjectTerm String | Double-quoted item |
FunApp AtomicWord [term] | Function symbol application (constants are encoded as nullary functions) |
Instances
Pretty T0Diff # | |
Defined in Codec.TPTP.Diff | |
Eq term => Eq (Term0 term) Source # | |
Data term => Data (Term0 term) Source # | |
Defined in Codec.TPTP.Base gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Term0 term -> c (Term0 term) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Term0 term) # toConstr :: Term0 term -> Constr # dataTypeOf :: Term0 term -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Term0 term)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Term0 term)) # gmapT :: (forall b. Data b => b -> b) -> Term0 term -> Term0 term # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term0 term -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term0 term -> r # gmapQ :: (forall d. Data d => d -> u) -> Term0 term -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Term0 term -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term) # | |
Ord term => Ord (Term0 term) Source # | |
Read term => Read (Term0 term) Source # | |
Show term => Show (Term0 term) Source # | |
Arbitrary a => Arbitrary (Term0 a) Source # | |
Pretty (Term0 Term) # | |
Pretty (WithEnclosing t) => Pretty (WithEnclosing (Term0 t)) # | |
Defined in Codec.TPTP.Pretty pretty :: WithEnclosing (Term0 t) -> Doc # prettyList :: [WithEnclosing (Term0 t)] -> Doc # | |
Pretty (WithEnclosing T0Diff) # | |
Defined in Codec.TPTP.Diff pretty :: WithEnclosing T0Diff -> Doc # prettyList :: [WithEnclosing T0Diff] -> Doc # | |
ToTPTP t => ToTPTP (Term0 t) Source # | |
Binary formula connectives
(:<=>:) | Equivalence |
(:=>:) | Implication |
(:<=:) | Reverse Implication |
(:&:) | AND |
(:|:) | OR |
(:~&:) | NAND |
(:~|:) | NOR |
(:<~>:) | XOR |
Instances
Bounded BinOp Source # | |
Enum BinOp Source # | |
Eq BinOp Source # | |
Data BinOp Source # | |
Defined in Codec.TPTP.Base 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 # 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 :: (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 # | |
Ord BinOp Source # | |
Read BinOp Source # | |
Show BinOp Source # | |
Arbitrary BinOp Source # | |
Pretty BinOp # | |
Defined in Codec.TPTP.Pretty | |
ToTPTP BinOp Source # | |
Term -> Term -> Formula infix connectives
Instances
Quantifier specification
Instances
Bounded Quant Source # | |
Enum Quant Source # | |
Eq Quant Source # | |
Data Quant Source # | |
Defined in Codec.TPTP.Base gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Quant -> c Quant # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Quant # dataTypeOf :: Quant -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Quant) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quant) # gmapT :: (forall b. Data b => b -> b) -> Quant -> Quant # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r # gmapQ :: (forall d. Data d => d -> u) -> Quant -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Quant -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Quant -> m Quant # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Quant -> m Quant # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Quant -> m Quant # | |
Ord Quant Source # | |
Read Quant Source # | |
Show Quant Source # | |
Arbitrary Quant Source # | |
Pretty Quant # | |
Defined in Codec.TPTP.Pretty | |
ToTPTP Quant Source # | |
Formula Metadata
type TPTP_Input = TPTP_Input_ Identity Source #
A line of a TPTP file: Annotated formula, comment or include statement.
type TPTP_Input_C = TPTP_Input_ (State [String]) Source #
A line of a TPTP file: Annotated formula (with the comment string embbeded in the State monad ), comment or include statement
forgetTIC :: TPTP_Input_C -> TPTP_Input Source #
Forget comments in a line of a TPTP file decorated with comments
data TPTP_Input_ c Source #
Generalized TPTP_Input
AFormula | Annotated formulae |
| |
Comment String | |
Include FilePath [AtomicWord] |
Instances
data Annotations Source #
Annotations about the formulas origin
Instances
data UsefulInfo Source #
Misc annotations
Instances
Formula roles
Instances
Eq Role Source # | |
Data Role Source # | |
Defined in Codec.TPTP.Base gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Role -> c Role # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Role # dataTypeOf :: Role -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Role) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Role) # gmapT :: (forall b. Data b => b -> b) -> Role -> Role # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r # gmapQ :: (forall d. Data d => d -> u) -> Role -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Role -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Role -> m Role # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role # | |
Ord Role Source # | |
Read Role Source # | |
Show Role Source # | |
Arbitrary Role Source # | |
ToTPTP Role Source # | |
Metadata (the general_data rule in TPTP's grammar)
GWord AtomicWord | |
GApp AtomicWord [GTerm] | |
GVar V | |
GNumber Rational | |
GDistinctObject String | |
GFormulaData String Formula |
Instances
Eq GData Source # | |
Data GData Source # | |
Defined in Codec.TPTP.Base gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GData -> c GData # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GData # dataTypeOf :: GData -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GData) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GData) # gmapT :: (forall b. Data b => b -> b) -> GData -> GData # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GData -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GData -> r # gmapQ :: (forall d. Data d => d -> u) -> GData -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> GData -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> GData -> m GData # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GData -> m GData # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GData -> m GData # | |
Ord GData Source # | |
Read GData Source # | |
Show GData Source # | |
Arbitrary GData Source # | |
Pretty GData # | |
Defined in Codec.TPTP.Pretty | |
ToTPTP GData Source # | |
Metadata (the general_term rule in TPTP's grammar)
Instances
Eq GTerm Source # | |
Data GTerm Source # | |
Defined in Codec.TPTP.Base gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GTerm -> c GTerm # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GTerm # dataTypeOf :: GTerm -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GTerm) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GTerm) # gmapT :: (forall b. Data b => b -> b) -> GTerm -> GTerm # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GTerm -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GTerm -> r # gmapQ :: (forall d. Data d => d -> u) -> GTerm -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> GTerm -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> GTerm -> m GTerm # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GTerm -> m GTerm # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GTerm -> m GTerm # | |
Ord GTerm Source # | |
Read GTerm Source # | |
Show GTerm Source # | |
Arbitrary GTerm Source # | |
Pretty GTerm # | |
Defined in Codec.TPTP.Pretty | |
ToTPTP GTerm Source # | |
Gathering free Variables
univquant_free_vars :: Formula -> Formula Source #
Universally quantify all free variables in the formula
newtype AtomicWord Source #
TPTP constant symbol/predicate symbol/function symbol identifiers (they are output in single quotes unless they are lower_words).
Tip: Use the -XOverloadedStrings
compiler flag if you don't want to have to type AtomicWord to construct an AtomicWord
Instances
Variable names
Instances
Eq V Source # | |
Data V Source # | |
Defined in Codec.TPTP.Base gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> V -> c V # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c V # dataTypeOf :: V -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c V) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c V) # gmapT :: (forall b. Data b => b -> b) -> V -> V # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> V -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> V -> r # gmapQ :: (forall d. Data d => d -> u) -> V -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> V -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> V -> m V # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> V -> m V # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> V -> m V # | |
Ord V Source # | |
Read V Source # | |
Show V Source # | |
IsString V Source # | |
Defined in Codec.TPTP.Base fromString :: String -> V # | |
Semigroup V Source # | |
Monoid V Source # | |
Arbitrary V Source # | |
Pretty V # | |
Defined in Codec.TPTP.Pretty | |
ToTPTP V Source # | |
Fixed-point style decorated formulae and terms
Formulae whose subexpressions are wrapped in the given type constructor c
.
For example:
Instances
Arbitrary Formula Source # | |
Pretty F0Diff # | |
Defined in Codec.TPTP.Diff | |
FreeVars Formula Source # | |
Diffable Formula (F DiffResult) Source # | |
Defined in Codec.TPTP.Diff | |
Eq (c (Formula0 (T c) (F c))) => Eq (F c) Source # | |
(Typeable c, Data (c (Formula0 (T c) (F c)))) => Data (F c) Source # | |
Defined in Codec.TPTP.Base gfoldl :: (forall d b. Data d => c0 (d -> b) -> d -> c0 b) -> (forall g. g -> c0 g) -> F c -> c0 (F c) # gunfold :: (forall b r. Data b => c0 (b -> r) -> c0 r) -> (forall r. r -> c0 r) -> Constr -> c0 (F c) # dataTypeOf :: F c -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c0 (t d)) -> Maybe (c0 (F c)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c0 (t d e)) -> Maybe (c0 (F c)) # gmapT :: (forall b. Data b => b -> b) -> F c -> F c # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> F c -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> F c -> r # gmapQ :: (forall d. Data d => d -> u) -> F c -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> F c -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> F c -> m (F c) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> F c -> m (F c) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> F c -> m (F c) # | |
Ord (c (Formula0 (T c) (F c))) => Ord (F c) Source # | |
Read (c (Formula0 (T c) (F c))) => Read (F c) Source # | |
Show (c (Formula0 (T c) (F c))) => Show (F c) Source # | |
Show (F DiffResult) # | |
Defined in Codec.TPTP.Diff | |
Pretty (F Identity) # | |
Pretty (F DiffResult) # | |
Defined in Codec.TPTP.Diff pretty :: F DiffResult -> Doc # prettyList :: [F DiffResult] -> Doc # | |
Pretty (WithEnclosing (F DiffResult)) # | |
Defined in Codec.TPTP.Diff pretty :: WithEnclosing (F DiffResult) -> Doc # prettyList :: [WithEnclosing (F DiffResult)] -> Doc # | |
Pretty (WithEnclosing Formula) # | |
Defined in Codec.TPTP.Pretty pretty :: WithEnclosing Formula -> Doc # prettyList :: [WithEnclosing Formula] -> Doc # | |
Pretty (WithEnclosing F0Diff) # | |
Defined in Codec.TPTP.Diff pretty :: WithEnclosing F0Diff -> Doc # prettyList :: [WithEnclosing F0Diff] -> Doc # | |
ToTPTP (F Identity) Source # | |
Pretty (Formula0 Term Formula) # | |
Terms whose subterms are wrapped in the given type constructor c
Instances
Arbitrary Term Source # | |
Pretty F0Diff # | |
Defined in Codec.TPTP.Diff | |
Pretty T0Diff # | |
Defined in Codec.TPTP.Diff | |
FreeVars Term Source # | |
Diffable Term (T DiffResult) Source # | |
Defined in Codec.TPTP.Diff | |
Eq (c (Term0 (T c))) => Eq (T c) Source # | |
(Typeable c, Data (c (Term0 (T c)))) => Data (T c) Source # | |
Defined in Codec.TPTP.Base gfoldl :: (forall d b. Data d => c0 (d -> b) -> d -> c0 b) -> (forall g. g -> c0 g) -> T c -> c0 (T c) # gunfold :: (forall b r. Data b => c0 (b -> r) -> c0 r) -> (forall r. r -> c0 r) -> Constr -> c0 (T c) # dataTypeOf :: T c -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c0 (t d)) -> Maybe (c0 (T c)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c0 (t d e)) -> Maybe (c0 (T c)) # gmapT :: (forall b. Data b => b -> b) -> T c -> T c # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> T c -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> T c -> r # gmapQ :: (forall d. Data d => d -> u) -> T c -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> T c -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> T c -> m (T c) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> T c -> m (T c) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> T c -> m (T c) # | |
Ord (c (Term0 (T c))) => Ord (T c) Source # | |
Read (c (Term0 (T c))) => Read (T c) Source # | |
Show (c (Term0 (T c))) => Show (T c) Source # | |
Show (T DiffResult) # | |
Defined in Codec.TPTP.Diff | |
Pretty (T Identity) # | |
Pretty (T DiffResult) # | |
Defined in Codec.TPTP.Diff pretty :: T DiffResult -> Doc # prettyList :: [T DiffResult] -> Doc # | |
Pretty (Term0 Term) # | |
Pretty (WithEnclosing (T DiffResult)) # | |
Defined in Codec.TPTP.Diff pretty :: WithEnclosing (T DiffResult) -> Doc # prettyList :: [WithEnclosing (T DiffResult)] -> Doc # | |
Pretty (WithEnclosing Term) # | |
Defined in Codec.TPTP.Pretty pretty :: WithEnclosing Term -> Doc # prettyList :: [WithEnclosing Term] -> Doc # | |
Pretty (WithEnclosing F0Diff) # | |
Defined in Codec.TPTP.Diff pretty :: WithEnclosing F0Diff -> Doc # prettyList :: [WithEnclosing F0Diff] -> Doc # | |
Pretty (WithEnclosing T0Diff) # | |
Defined in Codec.TPTP.Diff pretty :: WithEnclosing T0Diff -> Doc # prettyList :: [WithEnclosing T0Diff] -> Doc # | |
ToTPTP (T Identity) Source # | |
Pretty (Formula0 Term Formula) # | |
Utility functions
foldFormula0 :: (f -> r) -> (Quant -> [V] -> f -> r) -> (f -> BinOp -> f -> r) -> (t -> InfixPred -> t -> r) -> (AtomicWord -> [t] -> r) -> Formula0 t f -> r Source #
foldTerm0 :: (String -> r) -> (Rational -> r) -> (V -> r) -> (AtomicWord -> [t] -> r) -> Term0 t -> r Source #
:: Copointed t | |
=> (F t -> r) | Handle negation |
-> (Quant -> [V] -> F t -> r) | Handle quantification |
-> (F t -> BinOp -> F t -> r) | Handle binary op |
-> (T t -> InfixPred -> T t -> r) | Handle equality/inequality |
-> (AtomicWord -> [T t] -> r) | Handle predicate symbol application |
-> F t -> r | Handle formula |
Eliminate formulae