logic-TPTP-0.4.4.0: Import, export etc. for TPTP, a syntax for first-order logic

Codec.TPTP.Base

Synopsis

# Basic undecorated formulae and terms

Basic (undecorated) first-order formulae

type Term = T Identity Source #

Basic (undecorated) terms

# Formulae and terms decorated with state

type FormulaST s = F (State s) Source #

First-order formulae decorated with state

type TermST s = T (State s) Source #

Terms decorated with state

type TermC = TermST [String] Source #

(.<=>.) :: Pointed c => F c -> F c -> F c infixl 2 Source #

Equivalence

Important special case:

$$\.\<\=\>\.$$ :: Formula -> Formula -> Formula

(.=>.) :: Pointed c => F c -> F c -> F c infixl 2 Source #

Implication

(.<=.) :: Pointed c => F c -> F c -> F c infixl 2 Source #

Reverse implication

(.|.) :: Pointed c => F c -> F c -> F c infixl 3 Source #

Disjunction/OR

(.&.) :: Pointed c => F c -> F c -> F c infixl 4 Source #

Conjunction/AND

(.<~>.) :: Pointed c => F c -> F c -> F c infixl 2 Source #

XOR

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

NOR

(.~&.) :: Pointed c => F c -> F c -> F c infixl 4 Source #

NAND

(.~.) :: Pointed c => F c -> F c Source #

Negation

(.=.) :: Pointed c => T c -> T c -> F c infixl 5 Source #

Equality

(.!=.) :: Pointed c => T c -> T c -> F c infixl 5 Source #

Inequality

for_all :: Pointed c => [V] -> F c -> F c Source #

Universal quantification

exists :: Pointed c => [V] -> F c -> F c Source #

Existential quantification

pApp :: Pointed c => AtomicWord -> [T c] -> F c Source #

Predicate symbol application

var :: Pointed c => V -> T c Source #

Variable

fApp :: Pointed c => AtomicWord -> [T c] -> T c Source #

Function symbol application (constants are encoded as nullary functions)

numberLitTerm :: Pointed c => Rational -> T c Source #

Number literal

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.

Constructors

 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

data Term0 term 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.

Constructors

 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

data BinOp Source #

Binary formula connectives

Constructors

 (:<=>:) Equivalence (:=>:) Implication (:<=:) Reverse Implication (:&:) AND (:|:) OR (:~&:) NAND (:~|:) NOR (:<~>:) XOR

Instances

 Source # Methods Source # Methodssucc :: BinOp -> BinOp #pred :: BinOp -> BinOp #toEnum :: Int -> BinOp #enumFrom :: BinOp -> [BinOp] #enumFromThen :: BinOp -> BinOp -> [BinOp] #enumFromTo :: BinOp -> BinOp -> [BinOp] #enumFromThenTo :: BinOp -> BinOp -> BinOp -> [BinOp] # Source # Methods(==) :: BinOp -> BinOp -> Bool #(/=) :: BinOp -> BinOp -> Bool # Source # Methodsgfoldl :: (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 #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 # Source # Methods(<) :: BinOp -> BinOp -> Bool #(<=) :: BinOp -> BinOp -> Bool #(>) :: BinOp -> BinOp -> Bool #(>=) :: BinOp -> BinOp -> Bool #max :: BinOp -> BinOp -> BinOp #min :: BinOp -> BinOp -> BinOp # Source # Methods Source # MethodsshowsPrec :: Int -> BinOp -> ShowS #show :: BinOp -> String #showList :: [BinOp] -> ShowS # Source # Methodsshrink :: BinOp -> [BinOp] # Source # Methods

data InfixPred Source #

Term -> Term -> Formula infix connectives

Constructors

 (:=:) (:!=:)

Instances

 Source # Methods Source # MethodsenumFrom :: InfixPred -> [InfixPred] # Source # Methods Source # Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> InfixPred -> c InfixPred #gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c InfixPred #dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c InfixPred) #dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InfixPred) #gmapT :: (forall b. Data b => b -> b) -> InfixPred -> InfixPred #gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> InfixPred -> r #gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> InfixPred -> r #gmapQ :: (forall d. Data d => d -> u) -> InfixPred -> [u] #gmapQi :: Int -> (forall d. Data d => d -> u) -> InfixPred -> u #gmapM :: Monad m => (forall d. Data d => d -> m d) -> InfixPred -> m InfixPred #gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> InfixPred -> m InfixPred #gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> InfixPred -> m InfixPred # Source # Methods Source # Methods Source # MethodsshowList :: [InfixPred] -> ShowS # Source # Methodsshrink :: InfixPred -> [InfixPred] # Source # Methods

data Quant Source #

Quantifier specification

Constructors

 All Exists

Instances

 Source # Methods Source # Methodssucc :: Quant -> Quant #pred :: Quant -> Quant #toEnum :: Int -> Quant #enumFrom :: Quant -> [Quant] #enumFromThen :: Quant -> Quant -> [Quant] #enumFromTo :: Quant -> Quant -> [Quant] #enumFromThenTo :: Quant -> Quant -> Quant -> [Quant] # Source # Methods(==) :: Quant -> Quant -> Bool #(/=) :: Quant -> Quant -> Bool # Source # Methodsgfoldl :: (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 #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 # Source # Methods(<) :: Quant -> Quant -> Bool #(<=) :: Quant -> Quant -> Bool #(>) :: Quant -> Quant -> Bool #(>=) :: Quant -> Quant -> Bool #max :: Quant -> Quant -> Quant #min :: Quant -> Quant -> Quant # Source # Methods Source # MethodsshowsPrec :: Int -> Quant -> ShowS #show :: Quant -> String #showList :: [Quant] -> ShowS # Source # Methodsshrink :: Quant -> [Quant] # Source # Methods

A line of a TPTP file: Annotated formula, comment or include statement.

A line of a TPTP file: Annotated formula (with the comment string embbeded in the State monad ), comment or include statement

Forget comments in a line of a TPTP file decorated with comments

data TPTP_Input_ c Source #

Generalized TPTP_Input

Constructors

 AFormula Annotated formulae Fieldsname :: AtomicWord role :: Role formula :: F c annotations :: Annotations Comment String Include FilePath [AtomicWord]

Instances

 Source # Methodsshrink :: TPTP_Input -> [TPTP_Input] # Source # Methods Eq (c (Formula0 (T c) (F c))) => Eq (TPTP_Input_ c) Source # Methods(==) :: TPTP_Input_ c -> TPTP_Input_ c -> Bool #(/=) :: TPTP_Input_ c -> TPTP_Input_ c -> Bool # (Typeable (* -> *) c, Data (c (Formula0 (T c) (F c)))) => Data (TPTP_Input_ c) Source # Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TPTP_Input_ c -> c (TPTP_Input_ c) #gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TPTP_Input_ c) #dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (TPTP_Input_ c)) #dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TPTP_Input_ c)) #gmapT :: (forall b. Data b => b -> b) -> TPTP_Input_ c -> TPTP_Input_ c #gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TPTP_Input_ c -> r #gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TPTP_Input_ c -> r #gmapQ :: (forall d. Data d => d -> u) -> TPTP_Input_ c -> [u] #gmapQi :: Int -> (forall d. Data d => d -> u) -> TPTP_Input_ c -> u #gmapM :: Monad m => (forall d. Data d => d -> m d) -> TPTP_Input_ c -> m (TPTP_Input_ c) #gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TPTP_Input_ c -> m (TPTP_Input_ c) #gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TPTP_Input_ c -> m (TPTP_Input_ c) # Ord (c (Formula0 (T c) (F c))) => Ord (TPTP_Input_ c) Source # Methodscompare :: TPTP_Input_ c -> TPTP_Input_ c -> Ordering #(<) :: TPTP_Input_ c -> TPTP_Input_ c -> Bool #(<=) :: TPTP_Input_ c -> TPTP_Input_ c -> Bool #(>) :: TPTP_Input_ c -> TPTP_Input_ c -> Bool #(>=) :: TPTP_Input_ c -> TPTP_Input_ c -> Bool #max :: TPTP_Input_ c -> TPTP_Input_ c -> TPTP_Input_ c #min :: TPTP_Input_ c -> TPTP_Input_ c -> TPTP_Input_ c # Read (c (Formula0 (T c) (F c))) => Read (TPTP_Input_ c) Source # Methods Show (c (Formula0 (T c) (F c))) => Show (TPTP_Input_ c) Source # MethodsshowsPrec :: Int -> TPTP_Input_ c -> ShowS #show :: TPTP_Input_ c -> String #showList :: [TPTP_Input_ c] -> ShowS # Source # MethodstoTPTP :: [TPTP_Input] -> ShowS Source #

Constructors

 NoAnnotations Annotations GTerm UsefulInfo

Instances

 Source # Methods Source # Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Annotations -> c Annotations #gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Annotations #dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Annotations) #dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Annotations) #gmapT :: (forall b. Data b => b -> b) -> Annotations -> Annotations #gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Annotations -> r #gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Annotations -> r #gmapQ :: (forall d. Data d => d -> u) -> Annotations -> [u] #gmapQi :: Int -> (forall d. Data d => d -> u) -> Annotations -> u #gmapM :: Monad m => (forall d. Data d => d -> m d) -> Annotations -> m Annotations #gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Annotations -> m Annotations #gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Annotations -> m Annotations # Source # Methods Source # Methods Source # MethodsshowList :: [Annotations] -> ShowS # Source # Methods Source # Methods

Misc annotations

Constructors

 NoUsefulInfo UsefulInfo [GTerm]

Instances

 Source # Methods Source # Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UsefulInfo -> c UsefulInfo #gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UsefulInfo #dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c UsefulInfo) #dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UsefulInfo) #gmapT :: (forall b. Data b => b -> b) -> UsefulInfo -> UsefulInfo #gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UsefulInfo -> r #gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UsefulInfo -> r #gmapQ :: (forall d. Data d => d -> u) -> UsefulInfo -> [u] #gmapQi :: Int -> (forall d. Data d => d -> u) -> UsefulInfo -> u #gmapM :: Monad m => (forall d. Data d => d -> m d) -> UsefulInfo -> m UsefulInfo #gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UsefulInfo -> m UsefulInfo #gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UsefulInfo -> m UsefulInfo # Source # Methods Source # Methods Source # MethodsshowList :: [UsefulInfo] -> ShowS # Source # Methodsshrink :: UsefulInfo -> [UsefulInfo] # Source # Methods

newtype Role Source #

Formula roles

Constructors

 Role Fieldsunrole :: String

Instances

 Source # Methods(==) :: Role -> Role -> Bool #(/=) :: Role -> Role -> Bool # Source # Methodsgfoldl :: (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 #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 # Source # Methodscompare :: Role -> Role -> Ordering #(<) :: Role -> Role -> Bool #(<=) :: Role -> Role -> Bool #(>) :: Role -> Role -> Bool #(>=) :: Role -> Role -> Bool #max :: Role -> Role -> Role #min :: Role -> Role -> Role # Source # Methods Source # MethodsshowsPrec :: Int -> Role -> ShowS #show :: Role -> String #showList :: [Role] -> ShowS # Source # Methodsshrink :: Role -> [Role] # Source # Methods

data GData Source #

Metadata (the general_data rule in TPTP's grammar)

Constructors

 GWord AtomicWord GApp AtomicWord [GTerm] GVar V GNumber Rational GDistinctObject String GFormulaData String Formula

Instances

 Source # Methods(==) :: GData -> GData -> Bool #(/=) :: GData -> GData -> Bool # Source # Methodsgfoldl :: (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 #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 # Source # Methods(<) :: GData -> GData -> Bool #(<=) :: GData -> GData -> Bool #(>) :: GData -> GData -> Bool #(>=) :: GData -> GData -> Bool #max :: GData -> GData -> GData #min :: GData -> GData -> GData # Source # Methods Source # MethodsshowsPrec :: Int -> GData -> ShowS #show :: GData -> String #showList :: [GData] -> ShowS # Source # Methodsshrink :: GData -> [GData] # Source # Methods

data GTerm Source #

Metadata (the general_term rule in TPTP's grammar)

Constructors

 ColonSep GData GTerm GTerm GData GList [GTerm]

Instances

 Source # Methods(==) :: GTerm -> GTerm -> Bool #(/=) :: GTerm -> GTerm -> Bool # Source # Methodsgfoldl :: (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 #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 # Source # Methods(<) :: GTerm -> GTerm -> Bool #(<=) :: GTerm -> GTerm -> Bool #(>) :: GTerm -> GTerm -> Bool #(>=) :: GTerm -> GTerm -> Bool #max :: GTerm -> GTerm -> GTerm #min :: GTerm -> GTerm -> GTerm # Source # Methods Source # MethodsshowsPrec :: Int -> GTerm -> ShowS #show :: GTerm -> String #showList :: [GTerm] -> ShowS # Source # Methodsshrink :: GTerm -> [GTerm] # Source # Methods

# Gathering free Variables

class FreeVars a where Source #

Minimal complete definition

freeVars

Methods

freeVars :: a -> Set V Source #

Obtain the free variables from a formula or term

Instances

 Source # Methods Source # Methods

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

Constructors

 AtomicWord String

Instances

 Source # Methods Source # Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AtomicWord -> c AtomicWord #gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AtomicWord #dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c AtomicWord) #dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AtomicWord) #gmapT :: (forall b. Data b => b -> b) -> AtomicWord -> AtomicWord #gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AtomicWord -> r #gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AtomicWord -> r #gmapQ :: (forall d. Data d => d -> u) -> AtomicWord -> [u] #gmapQi :: Int -> (forall d. Data d => d -> u) -> AtomicWord -> u #gmapM :: Monad m => (forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord #gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord #gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord # Source # Methods Source # Methods Source # MethodsshowList :: [AtomicWord] -> ShowS # Source # Methods Source # Methodsmconcat :: [AtomicWord] -> AtomicWord # Source # Methodsshrink :: AtomicWord -> [AtomicWord] # Source # Methods

newtype V Source #

Variable names

Constructors

 V String

Instances

 Source # Methods(==) :: V -> V -> Bool #(/=) :: V -> V -> Bool # Source # Methodsgfoldl :: (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 #toConstr :: V -> Constr #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 # Source # Methodscompare :: V -> V -> Ordering #(<) :: V -> V -> Bool #(<=) :: V -> V -> Bool #(>) :: V -> V -> Bool #(>=) :: V -> V -> Bool #max :: V -> V -> V #min :: V -> V -> V # Source # MethodsreadList :: ReadS [V] # Source # MethodsshowsPrec :: Int -> V -> ShowS #show :: V -> String #showList :: [V] -> ShowS # Source # Methods Source # Methodsmempty :: V #mappend :: V -> V -> V #mconcat :: [V] -> V # Source # Methodsshrink :: V -> [V] # Source # Methods

# Fixed-point style decorated formulae and terms

newtype F c Source #

Formulae whose subexpressions are wrapped in the given type constructor c.

For example:

• c = Identity: Plain formulae
• c = Maybe: Formulae that may contain "holes"
• c = IORef: (Mutable) formulae with mutable subexpressions

Constructors

 F FieldsrunF :: c (Formula0 (T c) (F c))

Instances

newtype T c Source #

Terms whose subterms are wrapped in the given type constructor c

Constructors

 T FieldsrunT :: c (Term0 (T c))

Instances

# Utility functions

unwrapF :: Copointed t => F t -> Formula0 (T t) (F t) Source #

unwrapT :: Copointed t => T t -> Term0 (T t) Source #

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 #

Arguments

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

Arguments

 :: Copointed t => (String -> r) Handle string literal -> (Rational -> r) Handle number literal -> (V -> r) Handle variable -> (AtomicWord -> [T t] -> r) Handle function symbol application -> T t -> r Handle term

Eliminate terms