{-# LANGUAGE CPP, NoMonomorphismRestriction
  , StandaloneDeriving
  , TypeSynonymInstances, FlexibleInstances, FlexibleContexts
  , UndecidableInstances, DeriveDataTypeable, GeneralizedNewtypeDeriving
  , ScopedTypeVariables
  #-}

module Codec.TPTP.Base where

import Codec.TPTP.QuickCheck
import Control.Applicative
import Control.Monad
import Control.Monad.Identity
import Control.Monad.Writer (Writer, runWriter)
import Data.Data
import Data.Function
import Data.Monoid hiding(All)
import Data.Semigroup (Semigroup)
import Data.Set as S hiding(fold)
import Data.String
import Prelude --hiding(concat,foldl,foldl1,foldr,foldr1)
import Test.QuickCheck hiding ((.&.))
import Data.Pointed
import Data.Copointed

-- * Basic undecorated formulae and terms

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

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

-- * Formulae and terms decorated with state

-- | First-order formulae decorated with state
type FormulaW s = F (Writer s)

-- | Terms decorated with state
type TermW s = T (Writer s)

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

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

-- | Forget comments in formulae decorated with comments
forgetFC :: FormulaC -> Formula
forgetFC :: FormulaC -> Formula
forgetFC (F Writer [String] (Formula0 (T (Writer [String])) FormulaC)
f) = Identity (Formula0 (T Identity) Formula) -> Formula
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F (Identity (Formula0 (T Identity) Formula) -> Formula)
-> (Formula0 (T Identity) Formula
    -> Identity (Formula0 (T Identity) Formula))
-> Formula0 (T Identity) Formula
-> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula0 (T Identity) Formula
-> Identity (Formula0 (T Identity) Formula)
forall a. a -> Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Formula0 (T Identity) Formula -> Formula)
-> Formula0 (T Identity) Formula -> Formula
forall a b. (a -> b) -> a -> b
$
  case (Formula0 (T (Writer [String])) FormulaC, [String])
-> Formula0 (T (Writer [String])) FormulaC
forall a b. (a, b) -> a
fst ((Formula0 (T (Writer [String])) FormulaC, [String])
 -> Formula0 (T (Writer [String])) FormulaC)
-> (Formula0 (T (Writer [String])) FormulaC, [String])
-> Formula0 (T (Writer [String])) FormulaC
forall a b. (a -> b) -> a -> b
$ Writer [String] (Formula0 (T (Writer [String])) FormulaC)
-> (Formula0 (T (Writer [String])) FormulaC, [String])
forall w a. Writer w a -> (a, w)
runWriter Writer [String] (Formula0 (T (Writer [String])) FormulaC)
f of
    BinOp FormulaC
f1 BinOp
op FormulaC
f2       -> Formula -> BinOp -> Formula -> Formula0 (T Identity) Formula
forall term formula.
formula -> BinOp -> formula -> Formula0 term formula
BinOp (FormulaC -> Formula
forgetFC FormulaC
f1) BinOp
op (FormulaC -> Formula
forgetFC FormulaC
f2)
    InfixPred T (Writer [String])
t1 InfixPred
pred_ T (Writer [String])
t2 -> T Identity
-> InfixPred -> T Identity -> Formula0 (T Identity) Formula
forall term formula.
term -> InfixPred -> term -> Formula0 term formula
InfixPred (T (Writer [String]) -> T Identity
forgetTC T (Writer [String])
t1) InfixPred
pred_ (T (Writer [String]) -> T Identity
forgetTC T (Writer [String])
t2)
    PredApp AtomicWord
aw [T (Writer [String])]
ts        -> AtomicWord -> [T Identity] -> Formula0 (T Identity) Formula
forall term formula. AtomicWord -> [term] -> Formula0 term formula
PredApp AtomicWord
aw ((T (Writer [String]) -> T Identity)
-> [T (Writer [String])] -> [T Identity]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap T (Writer [String]) -> T Identity
forgetTC [T (Writer [String])]
ts)
    Quant Quant
quant [V]
vs FormulaC
f_     -> Quant -> [V] -> Formula -> Formula0 (T Identity) Formula
forall term formula.
Quant -> [V] -> formula -> Formula0 term formula
Quant Quant
quant [V]
vs (FormulaC -> Formula
forgetFC FormulaC
f_)
    (:~:) FormulaC
f_              -> Formula -> Formula0 (T Identity) Formula
forall term formula. formula -> Formula0 term formula
(:~:) (FormulaC -> Formula
forgetFC FormulaC
f_)

-- | Forget comments in terms decorated with comments
forgetTC :: TermC -> Term
forgetTC :: T (Writer [String]) -> T Identity
forgetTC (T Writer [String] (Term0 (T (Writer [String])))
t) = Identity (Term0 (T Identity)) -> T Identity
forall (c :: * -> *). c (Term0 (T c)) -> T c
T (Identity (Term0 (T Identity)) -> T Identity)
-> (Term0 (T Identity) -> Identity (Term0 (T Identity)))
-> Term0 (T Identity)
-> T Identity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term0 (T Identity) -> Identity (Term0 (T Identity))
forall a. a -> Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term0 (T Identity) -> T Identity)
-> Term0 (T Identity) -> T Identity
forall a b. (a -> b) -> a -> b
$
  case (Term0 (T (Writer [String])), [String])
-> Term0 (T (Writer [String]))
forall a b. (a, b) -> a
fst ((Term0 (T (Writer [String])), [String])
 -> Term0 (T (Writer [String])))
-> (Term0 (T (Writer [String])), [String])
-> Term0 (T (Writer [String]))
forall a b. (a -> b) -> a -> b
$ Writer [String] (Term0 (T (Writer [String])))
-> (Term0 (T (Writer [String])), [String])
forall w a. Writer w a -> (a, w)
runWriter Writer [String] (Term0 (T (Writer [String])))
t of
    Var V
v -> V -> Term0 (T Identity)
forall term. V -> Term0 term
Var V
v
    NumberLitTerm Rational
d -> Rational -> Term0 (T Identity)
forall term. Rational -> Term0 term
NumberLitTerm Rational
d
    DistinctObjectTerm String
s -> String -> Term0 (T Identity)
forall term. String -> Term0 term
DistinctObjectTerm String
s
    FunApp AtomicWord
aw [T (Writer [String])]
ts -> AtomicWord -> [T Identity] -> Term0 (T Identity)
forall term. AtomicWord -> [term] -> Term0 term
FunApp AtomicWord
aw ((T (Writer [String]) -> T Identity)
-> [T (Writer [String])] -> [T Identity]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap T (Writer [String]) -> T Identity
forgetTC [T (Writer [String])]
ts)


-- | Equivalence
--
-- Important special case:
--
-- @\(\.\<\=\>\.\) :: 'Formula' -> 'Formula' -> 'Formula'@
(.<=>.) :: Pointed c => (F c) -> (F c) -> F c
F c
x .<=>. :: forall (c :: * -> *). Pointed c => F c -> F c -> F c
.<=>. F c
y = (c (Formula0 (T c) (F c)) -> F c
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F (c (Formula0 (T c) (F c)) -> F c)
-> (Formula0 (T c) (F c) -> c (Formula0 (T c) (F c)))
-> Formula0 (T c) (F c)
-> F c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula0 (T c) (F c) -> c (Formula0 (T c) (F c))
forall a. a -> c a
forall (p :: * -> *) a. Pointed p => a -> p a
point) (Formula0 (T c) (F c) -> F c) -> Formula0 (T c) (F c) -> F c
forall a b. (a -> b) -> a -> b
$ F c -> BinOp -> F c -> Formula0 (T c) (F c)
forall term formula.
formula -> BinOp -> formula -> Formula0 term formula
BinOp  F c
x BinOp
(:<=>:) F c
y


-- | Implication
(.=>.) :: Pointed c => (F c) -> (F c) -> F c
F c
x .=>. :: forall (c :: * -> *). Pointed c => F c -> F c -> F c
.=>.  F c
y = (c (Formula0 (T c) (F c)) -> F c
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F (c (Formula0 (T c) (F c)) -> F c)
-> (Formula0 (T c) (F c) -> c (Formula0 (T c) (F c)))
-> Formula0 (T c) (F c)
-> F c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula0 (T c) (F c) -> c (Formula0 (T c) (F c))
forall a. a -> c a
forall (p :: * -> *) a. Pointed p => a -> p a
point) (Formula0 (T c) (F c) -> F c) -> Formula0 (T c) (F c) -> F c
forall a b. (a -> b) -> a -> b
$ F c -> BinOp -> F c -> Formula0 (T c) (F c)
forall term formula.
formula -> BinOp -> formula -> Formula0 term formula
BinOp  F c
x BinOp
(:=>:)  F c
y

-- | Reverse implication
(.<=.) :: Pointed c => (F c) -> (F c) -> F c
F c
x .<=. :: forall (c :: * -> *). Pointed c => F c -> F c -> F c
.<=.  F c
y = (c (Formula0 (T c) (F c)) -> F c
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F (c (Formula0 (T c) (F c)) -> F c)
-> (Formula0 (T c) (F c) -> c (Formula0 (T c) (F c)))
-> Formula0 (T c) (F c)
-> F c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula0 (T c) (F c) -> c (Formula0 (T c) (F c))
forall a. a -> c a
forall (p :: * -> *) a. Pointed p => a -> p a
point) (Formula0 (T c) (F c) -> F c) -> Formula0 (T c) (F c) -> F c
forall a b. (a -> b) -> a -> b
$ F c -> BinOp -> F c -> Formula0 (T c) (F c)
forall term formula.
formula -> BinOp -> formula -> Formula0 term formula
BinOp  F c
x BinOp
(:<=:)  F c
y

-- | Disjunction/OR
(.|.) :: Pointed c => (F c) -> (F c) -> F c
F c
x .|. :: forall (c :: * -> *). Pointed c => F c -> F c -> F c
.|.   F c
y = (c (Formula0 (T c) (F c)) -> F c
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F (c (Formula0 (T c) (F c)) -> F c)
-> (Formula0 (T c) (F c) -> c (Formula0 (T c) (F c)))
-> Formula0 (T c) (F c)
-> F c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula0 (T c) (F c) -> c (Formula0 (T c) (F c))
forall a. a -> c a
forall (p :: * -> *) a. Pointed p => a -> p a
point) (Formula0 (T c) (F c) -> F c) -> Formula0 (T c) (F c) -> F c
forall a b. (a -> b) -> a -> b
$ F c -> BinOp -> F c -> Formula0 (T c) (F c)
forall term formula.
formula -> BinOp -> formula -> Formula0 term formula
BinOp  F c
x BinOp
(:|:)   F c
y

-- | Conjunction/AND
(.&.) :: Pointed c => (F c) -> (F c) -> F c
F c
x .&. :: forall (c :: * -> *). Pointed c => F c -> F c -> F c
.&.   F c
y = (c (Formula0 (T c) (F c)) -> F c
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F (c (Formula0 (T c) (F c)) -> F c)
-> (Formula0 (T c) (F c) -> c (Formula0 (T c) (F c)))
-> Formula0 (T c) (F c)
-> F c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula0 (T c) (F c) -> c (Formula0 (T c) (F c))
forall a. a -> c a
forall (p :: * -> *) a. Pointed p => a -> p a
point) (Formula0 (T c) (F c) -> F c) -> Formula0 (T c) (F c) -> F c
forall a b. (a -> b) -> a -> b
$ F c -> BinOp -> F c -> Formula0 (T c) (F c)
forall term formula.
formula -> BinOp -> formula -> Formula0 term formula
BinOp  F c
x BinOp
(:&:)   F c
y

-- | XOR
(.<~>.) :: Pointed c => (F c) -> (F c) -> F c
F c
x .<~>. :: forall (c :: * -> *). Pointed c => F c -> F c -> F c
.<~>. F c
y = (c (Formula0 (T c) (F c)) -> F c
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F (c (Formula0 (T c) (F c)) -> F c)
-> (Formula0 (T c) (F c) -> c (Formula0 (T c) (F c)))
-> Formula0 (T c) (F c)
-> F c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula0 (T c) (F c) -> c (Formula0 (T c) (F c))
forall a. a -> c a
forall (p :: * -> *) a. Pointed p => a -> p a
point) (Formula0 (T c) (F c) -> F c) -> Formula0 (T c) (F c) -> F c
forall a b. (a -> b) -> a -> b
$ F c -> BinOp -> F c -> Formula0 (T c) (F c)
forall term formula.
formula -> BinOp -> formula -> Formula0 term formula
BinOp  F c
x BinOp
(:<~>:) F c
y

-- | NOR
(.~|.) :: Pointed c => (F c) -> (F c) -> F c
F c
x .~|. :: forall (c :: * -> *). Pointed c => F c -> F c -> F c
.~|.  F c
y = (c (Formula0 (T c) (F c)) -> F c
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F (c (Formula0 (T c) (F c)) -> F c)
-> (Formula0 (T c) (F c) -> c (Formula0 (T c) (F c)))
-> Formula0 (T c) (F c)
-> F c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula0 (T c) (F c) -> c (Formula0 (T c) (F c))
forall a. a -> c a
forall (p :: * -> *) a. Pointed p => a -> p a
point) (Formula0 (T c) (F c) -> F c) -> Formula0 (T c) (F c) -> F c
forall a b. (a -> b) -> a -> b
$ F c -> BinOp -> F c -> Formula0 (T c) (F c)
forall term formula.
formula -> BinOp -> formula -> Formula0 term formula
BinOp  F c
x BinOp
(:~|:)  F c
y



-- | NAND
(.~&.) :: Pointed c => (F c) -> (F c) -> F c
F c
x .~&. :: forall (c :: * -> *). Pointed c => F c -> F c -> F c
.~&.  F c
y = (c (Formula0 (T c) (F c)) -> F c
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F (c (Formula0 (T c) (F c)) -> F c)
-> (Formula0 (T c) (F c) -> c (Formula0 (T c) (F c)))
-> Formula0 (T c) (F c)
-> F c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula0 (T c) (F c) -> c (Formula0 (T c) (F c))
forall a. a -> c a
forall (p :: * -> *) a. Pointed p => a -> p a
point) (Formula0 (T c) (F c) -> F c) -> Formula0 (T c) (F c) -> F c
forall a b. (a -> b) -> a -> b
$ F c -> BinOp -> F c -> Formula0 (T c) (F c)
forall term formula.
formula -> BinOp -> formula -> Formula0 term formula
BinOp  F c
x BinOp
(:~&:)  F c
y


-- | Negation
(.~.) :: Pointed c => (F c) -> F c
.~. :: forall (c :: * -> *). Pointed c => F c -> F c
(.~.) F c
x = (c (Formula0 (T c) (F c)) -> F c
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F (c (Formula0 (T c) (F c)) -> F c)
-> (Formula0 (T c) (F c) -> c (Formula0 (T c) (F c)))
-> Formula0 (T c) (F c)
-> F c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula0 (T c) (F c) -> c (Formula0 (T c) (F c))
forall a. a -> c a
forall (p :: * -> *) a. Pointed p => a -> p a
point) (Formula0 (T c) (F c) -> F c) -> Formula0 (T c) (F c) -> F c
forall a b. (a -> b) -> a -> b
$ F c -> Formula0 (T c) (F c)
forall term formula. formula -> Formula0 term formula
(:~:) F c
x

-- | Equality
(.=.) :: Pointed c => (T c) -> (T c) -> F c
T c
x .=. :: forall (c :: * -> *). Pointed c => T c -> T c -> F c
.=. T c
y   = (c (Formula0 (T c) (F c)) -> F c
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F (c (Formula0 (T c) (F c)) -> F c)
-> (Formula0 (T c) (F c) -> c (Formula0 (T c) (F c)))
-> Formula0 (T c) (F c)
-> F c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula0 (T c) (F c) -> c (Formula0 (T c) (F c))
forall a. a -> c a
forall (p :: * -> *) a. Pointed p => a -> p a
point) (Formula0 (T c) (F c) -> F c) -> Formula0 (T c) (F c) -> F c
forall a b. (a -> b) -> a -> b
$ T c -> InfixPred -> T c -> Formula0 (T c) (F c)
forall term formula.
term -> InfixPred -> term -> Formula0 term formula
InfixPred T c
x InfixPred
(:=:)   T c
y

-- | Inequality
(.!=.) :: Pointed c => (T c) -> (T c) -> F c
T c
x .!=. :: forall (c :: * -> *). Pointed c => T c -> T c -> F c
.!=. T c
y  = (c (Formula0 (T c) (F c)) -> F c
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F (c (Formula0 (T c) (F c)) -> F c)
-> (Formula0 (T c) (F c) -> c (Formula0 (T c) (F c)))
-> Formula0 (T c) (F c)
-> F c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula0 (T c) (F c) -> c (Formula0 (T c) (F c))
forall a. a -> c a
forall (p :: * -> *) a. Pointed p => a -> p a
point) (Formula0 (T c) (F c) -> F c) -> Formula0 (T c) (F c) -> F c
forall a b. (a -> b) -> a -> b
$ T c -> InfixPred -> T c -> Formula0 (T c) (F c)
forall term formula.
term -> InfixPred -> term -> Formula0 term formula
InfixPred T c
x InfixPred
(:!=:) T c
y

-- | Universal quantification
for_all :: Pointed c => [V] -> (F c) -> F c
for_all :: forall (c :: * -> *). Pointed c => [V] -> F c -> F c
for_all [V]
vars F c
x = (c (Formula0 (T c) (F c)) -> F c
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F (c (Formula0 (T c) (F c)) -> F c)
-> (Formula0 (T c) (F c) -> c (Formula0 (T c) (F c)))
-> Formula0 (T c) (F c)
-> F c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula0 (T c) (F c) -> c (Formula0 (T c) (F c))
forall a. a -> c a
forall (p :: * -> *) a. Pointed p => a -> p a
point) (Formula0 (T c) (F c) -> F c) -> Formula0 (T c) (F c) -> F c
forall a b. (a -> b) -> a -> b
$ Quant -> [V] -> F c -> Formula0 (T c) (F c)
forall term formula.
Quant -> [V] -> formula -> Formula0 term formula
Quant Quant
All [V]
vars F c
x

-- | Existential quantification
exists :: Pointed c => [V] -> (F c) -> F c
exists :: forall (c :: * -> *). Pointed c => [V] -> F c -> F c
exists [V]
vars F c
x = (c (Formula0 (T c) (F c)) -> F c
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F (c (Formula0 (T c) (F c)) -> F c)
-> (Formula0 (T c) (F c) -> c (Formula0 (T c) (F c)))
-> Formula0 (T c) (F c)
-> F c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula0 (T c) (F c) -> c (Formula0 (T c) (F c))
forall a. a -> c a
forall (p :: * -> *) a. Pointed p => a -> p a
point) (Formula0 (T c) (F c) -> F c) -> Formula0 (T c) (F c) -> F c
forall a b. (a -> b) -> a -> b
$ Quant -> [V] -> F c -> Formula0 (T c) (F c)
forall term formula.
Quant -> [V] -> formula -> Formula0 term formula
Quant Quant
Exists [V]
vars F c
x

-- | Predicate symbol application
pApp :: Pointed c => AtomicWord -> [T c] -> F c
pApp :: forall (c :: * -> *). Pointed c => AtomicWord -> [T c] -> F c
pApp AtomicWord
x [T c]
args = (c (Formula0 (T c) (F c)) -> F c
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F (c (Formula0 (T c) (F c)) -> F c)
-> (Formula0 (T c) (F c) -> c (Formula0 (T c) (F c)))
-> Formula0 (T c) (F c)
-> F c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula0 (T c) (F c) -> c (Formula0 (T c) (F c))
forall a. a -> c a
forall (p :: * -> *) a. Pointed p => a -> p a
point) (Formula0 (T c) (F c) -> F c) -> Formula0 (T c) (F c) -> F c
forall a b. (a -> b) -> a -> b
$ AtomicWord -> [T c] -> Formula0 (T c) (F c)
forall term formula. AtomicWord -> [term] -> Formula0 term formula
PredApp AtomicWord
x [T c]
args

-- | Variable
var :: Pointed c => V -> T c
var :: forall (c :: * -> *). Pointed c => V -> T c
var = (c (Term0 (T c)) -> T c
forall (c :: * -> *). c (Term0 (T c)) -> T c
T (c (Term0 (T c)) -> T c)
-> (Term0 (T c) -> c (Term0 (T c))) -> Term0 (T c) -> T c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term0 (T c) -> c (Term0 (T c))
forall a. a -> c a
forall (p :: * -> *) a. Pointed p => a -> p a
point) (Term0 (T c) -> T c) -> (V -> Term0 (T c)) -> V -> T c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. V -> Term0 (T c)
forall term. V -> Term0 term
Var

-- | Function symbol application (constants are encoded as nullary functions)
fApp :: Pointed c => AtomicWord -> [T c] -> T c
fApp :: forall (c :: * -> *). Pointed c => AtomicWord -> [T c] -> T c
fApp AtomicWord
x [T c]
args = (c (Term0 (T c)) -> T c
forall (c :: * -> *). c (Term0 (T c)) -> T c
T (c (Term0 (T c)) -> T c)
-> (Term0 (T c) -> c (Term0 (T c))) -> Term0 (T c) -> T c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term0 (T c) -> c (Term0 (T c))
forall a. a -> c a
forall (p :: * -> *) a. Pointed p => a -> p a
point) (Term0 (T c) -> T c) -> Term0 (T c) -> T c
forall a b. (a -> b) -> a -> b
$ AtomicWord -> [T c] -> Term0 (T c)
forall term. AtomicWord -> [term] -> Term0 term
FunApp AtomicWord
x [T c]
args

-- | Number literal
numberLitTerm :: Pointed c => Rational -> T c
numberLitTerm :: forall (c :: * -> *). Pointed c => Rational -> T c
numberLitTerm = (c (Term0 (T c)) -> T c
forall (c :: * -> *). c (Term0 (T c)) -> T c
T (c (Term0 (T c)) -> T c)
-> (Term0 (T c) -> c (Term0 (T c))) -> Term0 (T c) -> T c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term0 (T c) -> c (Term0 (T c))
forall a. a -> c a
forall (p :: * -> *) a. Pointed p => a -> p a
point) (Term0 (T c) -> T c)
-> (Rational -> Term0 (T c)) -> Rational -> T c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Term0 (T c)
forall term. Rational -> Term0 term
NumberLitTerm

-- | Double-quoted string literal, called /Distinct Object/ in TPTP's grammar
distinctObjectTerm :: Pointed c => String -> T c
distinctObjectTerm :: forall (c :: * -> *). Pointed c => String -> T c
distinctObjectTerm = (c (Term0 (T c)) -> T c
forall (c :: * -> *). c (Term0 (T c)) -> T c
T (c (Term0 (T c)) -> T c)
-> (Term0 (T c) -> c (Term0 (T c))) -> Term0 (T c) -> T c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term0 (T c) -> c (Term0 (T c))
forall a. a -> c a
forall (p :: * -> *) a. Pointed p => a -> p a
point) (Term0 (T c) -> T c) -> (String -> Term0 (T c)) -> String -> T c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Term0 (T c)
forall term. String -> Term0 term
DistinctObjectTerm

infixl 2  .<=>. ,  .=>. ,  .<=. ,  .<~>.
infixl 3  .|. ,  .~|.
infixl 4  .&. ,  .~&.
infixl 5  .=. ,  .!=.

-- * General decorated formulae and terms

-- | 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.
data Formula0 term formula =
              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
              deriving (Formula0 term formula -> Formula0 term formula -> Bool
(Formula0 term formula -> Formula0 term formula -> Bool)
-> (Formula0 term formula -> Formula0 term formula -> Bool)
-> Eq (Formula0 term formula)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall term formula.
(Eq term, Eq formula) =>
Formula0 term formula -> Formula0 term formula -> Bool
$c== :: forall term formula.
(Eq term, Eq formula) =>
Formula0 term formula -> Formula0 term formula -> Bool
== :: Formula0 term formula -> Formula0 term formula -> Bool
$c/= :: forall term formula.
(Eq term, Eq formula) =>
Formula0 term formula -> Formula0 term formula -> Bool
/= :: Formula0 term formula -> Formula0 term formula -> Bool
Eq,Eq (Formula0 term formula)
Eq (Formula0 term formula) =>
(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)
-> (Formula0 term formula
    -> Formula0 term formula -> Formula0 term formula)
-> (Formula0 term formula
    -> Formula0 term formula -> Formula0 term formula)
-> Ord (Formula0 term formula)
Formula0 term formula -> Formula0 term formula -> Bool
Formula0 term formula -> Formula0 term formula -> Ordering
Formula0 term formula
-> Formula0 term formula -> Formula0 term formula
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall term formula.
(Ord term, Ord formula) =>
Eq (Formula0 term formula)
forall term formula.
(Ord term, Ord formula) =>
Formula0 term formula -> Formula0 term formula -> Bool
forall term formula.
(Ord term, Ord formula) =>
Formula0 term formula -> Formula0 term formula -> Ordering
forall term formula.
(Ord term, Ord formula) =>
Formula0 term formula
-> Formula0 term formula -> Formula0 term formula
$ccompare :: forall term formula.
(Ord term, Ord formula) =>
Formula0 term formula -> Formula0 term formula -> Ordering
compare :: Formula0 term formula -> Formula0 term formula -> Ordering
$c< :: forall term formula.
(Ord term, Ord formula) =>
Formula0 term formula -> Formula0 term formula -> Bool
< :: Formula0 term formula -> Formula0 term formula -> Bool
$c<= :: forall term formula.
(Ord term, Ord formula) =>
Formula0 term formula -> Formula0 term formula -> Bool
<= :: Formula0 term formula -> Formula0 term formula -> Bool
$c> :: forall term formula.
(Ord term, Ord formula) =>
Formula0 term formula -> Formula0 term formula -> Bool
> :: Formula0 term formula -> Formula0 term formula -> Bool
$c>= :: forall term formula.
(Ord term, Ord formula) =>
Formula0 term formula -> Formula0 term formula -> Bool
>= :: Formula0 term formula -> Formula0 term formula -> Bool
$cmax :: forall term formula.
(Ord term, Ord formula) =>
Formula0 term formula
-> Formula0 term formula -> Formula0 term formula
max :: Formula0 term formula
-> Formula0 term formula -> Formula0 term formula
$cmin :: forall term formula.
(Ord term, Ord formula) =>
Formula0 term formula
-> Formula0 term formula -> Formula0 term formula
min :: Formula0 term formula
-> Formula0 term formula -> Formula0 term formula
Ord,Int -> Formula0 term formula -> ShowS
[Formula0 term formula] -> ShowS
Formula0 term formula -> String
(Int -> Formula0 term formula -> ShowS)
-> (Formula0 term formula -> String)
-> ([Formula0 term formula] -> ShowS)
-> Show (Formula0 term formula)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall term formula.
(Show term, Show formula) =>
Int -> Formula0 term formula -> ShowS
forall term formula.
(Show term, Show formula) =>
[Formula0 term formula] -> ShowS
forall term formula.
(Show term, Show formula) =>
Formula0 term formula -> String
$cshowsPrec :: forall term formula.
(Show term, Show formula) =>
Int -> Formula0 term formula -> ShowS
showsPrec :: Int -> Formula0 term formula -> ShowS
$cshow :: forall term formula.
(Show term, Show formula) =>
Formula0 term formula -> String
show :: Formula0 term formula -> String
$cshowList :: forall term formula.
(Show term, Show formula) =>
[Formula0 term formula] -> ShowS
showList :: [Formula0 term formula] -> ShowS
Show,ReadPrec [Formula0 term formula]
ReadPrec (Formula0 term formula)
Int -> ReadS (Formula0 term formula)
ReadS [Formula0 term formula]
(Int -> ReadS (Formula0 term formula))
-> ReadS [Formula0 term formula]
-> ReadPrec (Formula0 term formula)
-> ReadPrec [Formula0 term formula]
-> Read (Formula0 term formula)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall term formula.
(Read term, Read formula) =>
ReadPrec [Formula0 term formula]
forall term formula.
(Read term, Read formula) =>
ReadPrec (Formula0 term formula)
forall term formula.
(Read term, Read formula) =>
Int -> ReadS (Formula0 term formula)
forall term formula.
(Read term, Read formula) =>
ReadS [Formula0 term formula]
$creadsPrec :: forall term formula.
(Read term, Read formula) =>
Int -> ReadS (Formula0 term formula)
readsPrec :: Int -> ReadS (Formula0 term formula)
$creadList :: forall term formula.
(Read term, Read formula) =>
ReadS [Formula0 term formula]
readList :: ReadS [Formula0 term formula]
$creadPrec :: forall term formula.
(Read term, Read formula) =>
ReadPrec (Formula0 term formula)
readPrec :: ReadPrec (Formula0 term formula)
$creadListPrec :: forall term formula.
(Read term, Read formula) =>
ReadPrec [Formula0 term formula]
readListPrec :: ReadPrec [Formula0 term formula]
Read,Typeable (Formula0 term formula)
Typeable (Formula0 term formula) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> Formula0 term formula
 -> c (Formula0 term formula))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Formula0 term formula))
-> (Formula0 term formula -> Constr)
-> (Formula0 term formula -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Formula0 term formula)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Formula0 term formula)))
-> ((forall b. Data b => b -> b)
    -> Formula0 term formula -> Formula0 term formula)
-> (forall r r'.
    (r -> r' -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> Formula0 term formula
    -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> Formula0 term formula
    -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> Formula0 term formula -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Formula0 term formula -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> Formula0 term formula -> m (Formula0 term formula))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> Formula0 term formula -> m (Formula0 term formula))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> Formula0 term formula -> m (Formula0 term formula))
-> Data (Formula0 term formula)
Formula0 term formula -> Constr
Formula0 term formula -> DataType
(forall b. Data b => b -> b)
-> Formula0 term formula -> Formula0 term formula
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> Formula0 term formula -> u
forall u.
(forall d. Data d => d -> u) -> Formula0 term formula -> [u]
forall term formula.
(Data term, Data formula) =>
Typeable (Formula0 term formula)
forall term formula.
(Data term, Data formula) =>
Formula0 term formula -> Constr
forall term formula.
(Data term, Data formula) =>
Formula0 term formula -> DataType
forall term formula.
(Data term, Data formula) =>
(forall b. Data b => b -> b)
-> Formula0 term formula -> Formula0 term formula
forall term formula u.
(Data term, Data formula) =>
Int -> (forall d. Data d => d -> u) -> Formula0 term formula -> u
forall term formula u.
(Data term, Data formula) =>
(forall d. Data d => d -> u) -> Formula0 term formula -> [u]
forall term formula r r'.
(Data term, Data formula) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Formula0 term formula -> r
forall term formula r r'.
(Data term, Data formula) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Formula0 term formula -> r
forall term formula (m :: * -> *).
(Data term, Data formula, Monad m) =>
(forall d. Data d => d -> m d)
-> Formula0 term formula -> m (Formula0 term formula)
forall term formula (m :: * -> *).
(Data term, Data formula, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Formula0 term formula -> m (Formula0 term formula)
forall term formula (c :: * -> *).
(Data term, Data formula) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Formula0 term formula)
forall term formula (c :: * -> *).
(Data term, Data formula) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> Formula0 term formula
-> c (Formula0 term formula)
forall term formula (t :: * -> *) (c :: * -> *).
(Data term, Data formula, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Formula0 term formula))
forall term formula (t :: * -> * -> *) (c :: * -> *).
(Data term, Data formula, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Formula0 term formula))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Formula0 term formula -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Formula0 term formula -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> Formula0 term formula -> m (Formula0 term formula)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> Formula0 term formula -> m (Formula0 term formula)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Formula0 term formula)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> Formula0 term formula
-> c (Formula0 term formula)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Formula0 term formula))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Formula0 term formula))
$cgfoldl :: forall term formula (c :: * -> *).
(Data term, Data formula) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> Formula0 term formula
-> c (Formula0 term formula)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> Formula0 term formula
-> c (Formula0 term formula)
$cgunfold :: forall term formula (c :: * -> *).
(Data term, Data formula) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Formula0 term formula)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Formula0 term formula)
$ctoConstr :: forall term formula.
(Data term, Data formula) =>
Formula0 term formula -> Constr
toConstr :: Formula0 term formula -> Constr
$cdataTypeOf :: forall term formula.
(Data term, Data formula) =>
Formula0 term formula -> DataType
dataTypeOf :: Formula0 term formula -> DataType
$cdataCast1 :: forall term formula (t :: * -> *) (c :: * -> *).
(Data term, Data formula, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Formula0 term formula))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Formula0 term formula))
$cdataCast2 :: forall term formula (t :: * -> * -> *) (c :: * -> *).
(Data term, Data formula, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Formula0 term formula))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Formula0 term formula))
$cgmapT :: forall term formula.
(Data term, Data formula) =>
(forall b. Data b => b -> b)
-> Formula0 term formula -> Formula0 term formula
gmapT :: (forall b. Data b => b -> b)
-> Formula0 term formula -> Formula0 term formula
$cgmapQl :: forall term formula r r'.
(Data term, Data formula) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Formula0 term formula -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Formula0 term formula -> r
$cgmapQr :: forall term formula r r'.
(Data term, Data formula) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Formula0 term formula -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Formula0 term formula -> r
$cgmapQ :: forall term formula u.
(Data term, Data formula) =>
(forall d. Data d => d -> u) -> Formula0 term formula -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> Formula0 term formula -> [u]
$cgmapQi :: forall term formula u.
(Data term, Data formula) =>
Int -> (forall d. Data d => d -> u) -> Formula0 term formula -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> Formula0 term formula -> u
$cgmapM :: forall term formula (m :: * -> *).
(Data term, Data formula, Monad m) =>
(forall d. Data d => d -> m d)
-> Formula0 term formula -> m (Formula0 term formula)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> Formula0 term formula -> m (Formula0 term formula)
$cgmapMp :: forall term formula (m :: * -> *).
(Data term, Data formula, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Formula0 term formula -> m (Formula0 term formula)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> Formula0 term formula -> m (Formula0 term formula)
$cgmapMo :: forall term formula (m :: * -> *).
(Data term, Data formula, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Formula0 term formula -> m (Formula0 term formula)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> Formula0 term formula -> m (Formula0 term formula)
Data,Typeable)


-- | 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.
data Term0 term =
            Var V -- ^ Variable
          | NumberLitTerm Rational -- ^ Number literal
          | DistinctObjectTerm String -- ^ Double-quoted item
          | FunApp AtomicWord [term] -- ^ Function symbol application (constants are encoded as nullary functions)
            deriving (Term0 term -> Term0 term -> Bool
(Term0 term -> Term0 term -> Bool)
-> (Term0 term -> Term0 term -> Bool) -> Eq (Term0 term)
forall term. Eq term => Term0 term -> Term0 term -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall term. Eq term => Term0 term -> Term0 term -> Bool
== :: Term0 term -> Term0 term -> Bool
$c/= :: forall term. Eq term => Term0 term -> Term0 term -> Bool
/= :: Term0 term -> Term0 term -> Bool
Eq,Eq (Term0 term)
Eq (Term0 term) =>
(Term0 term -> Term0 term -> Ordering)
-> (Term0 term -> Term0 term -> Bool)
-> (Term0 term -> Term0 term -> Bool)
-> (Term0 term -> Term0 term -> Bool)
-> (Term0 term -> Term0 term -> Bool)
-> (Term0 term -> Term0 term -> Term0 term)
-> (Term0 term -> Term0 term -> Term0 term)
-> Ord (Term0 term)
Term0 term -> Term0 term -> Bool
Term0 term -> Term0 term -> Ordering
Term0 term -> Term0 term -> Term0 term
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall term. Ord term => Eq (Term0 term)
forall term. Ord term => Term0 term -> Term0 term -> Bool
forall term. Ord term => Term0 term -> Term0 term -> Ordering
forall term. Ord term => Term0 term -> Term0 term -> Term0 term
$ccompare :: forall term. Ord term => Term0 term -> Term0 term -> Ordering
compare :: Term0 term -> Term0 term -> Ordering
$c< :: forall term. Ord term => Term0 term -> Term0 term -> Bool
< :: Term0 term -> Term0 term -> Bool
$c<= :: forall term. Ord term => Term0 term -> Term0 term -> Bool
<= :: Term0 term -> Term0 term -> Bool
$c> :: forall term. Ord term => Term0 term -> Term0 term -> Bool
> :: Term0 term -> Term0 term -> Bool
$c>= :: forall term. Ord term => Term0 term -> Term0 term -> Bool
>= :: Term0 term -> Term0 term -> Bool
$cmax :: forall term. Ord term => Term0 term -> Term0 term -> Term0 term
max :: Term0 term -> Term0 term -> Term0 term
$cmin :: forall term. Ord term => Term0 term -> Term0 term -> Term0 term
min :: Term0 term -> Term0 term -> Term0 term
Ord,Int -> Term0 term -> ShowS
[Term0 term] -> ShowS
Term0 term -> String
(Int -> Term0 term -> ShowS)
-> (Term0 term -> String)
-> ([Term0 term] -> ShowS)
-> Show (Term0 term)
forall term. Show term => Int -> Term0 term -> ShowS
forall term. Show term => [Term0 term] -> ShowS
forall term. Show term => Term0 term -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall term. Show term => Int -> Term0 term -> ShowS
showsPrec :: Int -> Term0 term -> ShowS
$cshow :: forall term. Show term => Term0 term -> String
show :: Term0 term -> String
$cshowList :: forall term. Show term => [Term0 term] -> ShowS
showList :: [Term0 term] -> ShowS
Show,ReadPrec [Term0 term]
ReadPrec (Term0 term)
Int -> ReadS (Term0 term)
ReadS [Term0 term]
(Int -> ReadS (Term0 term))
-> ReadS [Term0 term]
-> ReadPrec (Term0 term)
-> ReadPrec [Term0 term]
-> Read (Term0 term)
forall term. Read term => ReadPrec [Term0 term]
forall term. Read term => ReadPrec (Term0 term)
forall term. Read term => Int -> ReadS (Term0 term)
forall term. Read term => ReadS [Term0 term]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: forall term. Read term => Int -> ReadS (Term0 term)
readsPrec :: Int -> ReadS (Term0 term)
$creadList :: forall term. Read term => ReadS [Term0 term]
readList :: ReadS [Term0 term]
$creadPrec :: forall term. Read term => ReadPrec (Term0 term)
readPrec :: ReadPrec (Term0 term)
$creadListPrec :: forall term. Read term => ReadPrec [Term0 term]
readListPrec :: ReadPrec [Term0 term]
Read,Typeable (Term0 term)
Typeable (Term0 term) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Term0 term -> c (Term0 term))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Term0 term))
-> (Term0 term -> Constr)
-> (Term0 term -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Term0 term)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Term0 term)))
-> ((forall b. Data b => b -> b) -> Term0 term -> Term0 term)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Term0 term -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Term0 term -> r)
-> (forall u. (forall d. Data d => d -> u) -> Term0 term -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Term0 term -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term))
-> Data (Term0 term)
Term0 term -> Constr
Term0 term -> DataType
(forall b. Data b => b -> b) -> Term0 term -> Term0 term
forall term. Data term => Typeable (Term0 term)
forall term. Data term => Term0 term -> Constr
forall term. Data term => Term0 term -> DataType
forall term.
Data term =>
(forall b. Data b => b -> b) -> Term0 term -> Term0 term
forall term u.
Data term =>
Int -> (forall d. Data d => d -> u) -> Term0 term -> u
forall term u.
Data term =>
(forall d. Data d => d -> u) -> Term0 term -> [u]
forall term r r'.
Data term =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Term0 term -> r
forall term r r'.
Data term =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Term0 term -> r
forall term (m :: * -> *).
(Data term, Monad m) =>
(forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term)
forall term (m :: * -> *).
(Data term, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term)
forall term (c :: * -> *).
Data term =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Term0 term)
forall term (c :: * -> *).
Data term =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term0 term -> c (Term0 term)
forall term (t :: * -> *) (c :: * -> *).
(Data term, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Term0 term))
forall term (t :: * -> * -> *) (c :: * -> *).
(Data term, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Term0 term))
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Term0 term -> u
forall u. (forall d. Data d => d -> u) -> Term0 term -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Term0 term -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Term0 term -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Term0 term)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term0 term -> c (Term0 term)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Term0 term))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Term0 term))
$cgfoldl :: forall term (c :: * -> *).
Data term =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term0 term -> c (Term0 term)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term0 term -> c (Term0 term)
$cgunfold :: forall term (c :: * -> *).
Data term =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Term0 term)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Term0 term)
$ctoConstr :: forall term. Data term => Term0 term -> Constr
toConstr :: Term0 term -> Constr
$cdataTypeOf :: forall term. Data term => Term0 term -> DataType
dataTypeOf :: Term0 term -> DataType
$cdataCast1 :: forall term (t :: * -> *) (c :: * -> *).
(Data term, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Term0 term))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Term0 term))
$cdataCast2 :: forall term (t :: * -> * -> *) (c :: * -> *).
(Data term, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Term0 term))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Term0 term))
$cgmapT :: forall term.
Data term =>
(forall b. Data b => b -> b) -> Term0 term -> Term0 term
gmapT :: (forall b. Data b => b -> b) -> Term0 term -> Term0 term
$cgmapQl :: forall term r r'.
Data term =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Term0 term -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Term0 term -> r
$cgmapQr :: forall term r r'.
Data term =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Term0 term -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Term0 term -> r
$cgmapQ :: forall term u.
Data term =>
(forall d. Data d => d -> u) -> Term0 term -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Term0 term -> [u]
$cgmapQi :: forall term u.
Data term =>
Int -> (forall d. Data d => d -> u) -> Term0 term -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Term0 term -> u
$cgmapM :: forall term (m :: * -> *).
(Data term, Monad m) =>
(forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term)
$cgmapMp :: forall term (m :: * -> *).
(Data term, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term)
$cgmapMo :: forall term (m :: * -> *).
(Data term, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term)
Data,Typeable)






-- | Binary formula connectives
data BinOp =
    -- Please don't change the constructor names (the Show instance is significant)
               (:<=>:)  -- ^ Equivalence
            |  (:=>:)  -- ^ Implication
            |  (:<=:)  -- ^ Reverse Implication
            |  (:&:)  -- ^ AND
            |  (:|:)  -- ^ OR
            |  (:~&:)  -- ^ NAND
            |  (:~|:)  -- ^ NOR
            |  (:<~>:)  -- ^ XOR
              deriving (BinOp -> BinOp -> Bool
(BinOp -> BinOp -> Bool) -> (BinOp -> BinOp -> Bool) -> Eq BinOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BinOp -> BinOp -> Bool
== :: BinOp -> BinOp -> Bool
$c/= :: BinOp -> BinOp -> Bool
/= :: BinOp -> BinOp -> Bool
Eq,Eq BinOp
Eq BinOp =>
(BinOp -> BinOp -> Ordering)
-> (BinOp -> BinOp -> Bool)
-> (BinOp -> BinOp -> Bool)
-> (BinOp -> BinOp -> Bool)
-> (BinOp -> BinOp -> Bool)
-> (BinOp -> BinOp -> BinOp)
-> (BinOp -> BinOp -> BinOp)
-> Ord BinOp
BinOp -> BinOp -> Bool
BinOp -> BinOp -> Ordering
BinOp -> BinOp -> BinOp
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: BinOp -> BinOp -> Ordering
compare :: BinOp -> BinOp -> Ordering
$c< :: BinOp -> BinOp -> Bool
< :: BinOp -> BinOp -> Bool
$c<= :: BinOp -> BinOp -> Bool
<= :: BinOp -> BinOp -> Bool
$c> :: BinOp -> BinOp -> Bool
> :: BinOp -> BinOp -> Bool
$c>= :: BinOp -> BinOp -> Bool
>= :: BinOp -> BinOp -> Bool
$cmax :: BinOp -> BinOp -> BinOp
max :: BinOp -> BinOp -> BinOp
$cmin :: BinOp -> BinOp -> BinOp
min :: BinOp -> BinOp -> BinOp
Ord,Int -> BinOp -> ShowS
[BinOp] -> ShowS
BinOp -> String
(Int -> BinOp -> ShowS)
-> (BinOp -> String) -> ([BinOp] -> ShowS) -> Show BinOp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BinOp -> ShowS
showsPrec :: Int -> BinOp -> ShowS
$cshow :: BinOp -> String
show :: BinOp -> String
$cshowList :: [BinOp] -> ShowS
showList :: [BinOp] -> ShowS
Show,ReadPrec [BinOp]
ReadPrec BinOp
Int -> ReadS BinOp
ReadS [BinOp]
(Int -> ReadS BinOp)
-> ReadS [BinOp]
-> ReadPrec BinOp
-> ReadPrec [BinOp]
-> Read BinOp
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS BinOp
readsPrec :: Int -> ReadS BinOp
$creadList :: ReadS [BinOp]
readList :: ReadS [BinOp]
$creadPrec :: ReadPrec BinOp
readPrec :: ReadPrec BinOp
$creadListPrec :: ReadPrec [BinOp]
readListPrec :: ReadPrec [BinOp]
Read,Typeable BinOp
Typeable BinOp =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> BinOp -> c BinOp)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c BinOp)
-> (BinOp -> Constr)
-> (BinOp -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c BinOp))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BinOp))
-> ((forall b. Data b => b -> b) -> BinOp -> BinOp)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r)
-> (forall u. (forall d. Data d => d -> u) -> BinOp -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> BinOp -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> BinOp -> m BinOp)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BinOp -> m BinOp)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BinOp -> m BinOp)
-> Data BinOp
BinOp -> Constr
BinOp -> DataType
(forall b. Data b => b -> b) -> BinOp -> BinOp
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> BinOp -> u
forall u. (forall d. Data d => d -> u) -> BinOp -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BinOp -> m BinOp
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BinOp -> m BinOp
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BinOp
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BinOp -> c BinOp
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BinOp)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BinOp)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BinOp -> c BinOp
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BinOp -> c BinOp
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BinOp
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BinOp
$ctoConstr :: BinOp -> Constr
toConstr :: BinOp -> Constr
$cdataTypeOf :: BinOp -> DataType
dataTypeOf :: BinOp -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BinOp)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BinOp)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BinOp)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BinOp)
$cgmapT :: (forall b. Data b => b -> b) -> BinOp -> BinOp
gmapT :: (forall b. Data b => b -> b) -> BinOp -> BinOp
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> BinOp -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> BinOp -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BinOp -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BinOp -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BinOp -> m BinOp
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BinOp -> m BinOp
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BinOp -> m BinOp
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BinOp -> m BinOp
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BinOp -> m BinOp
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BinOp -> m BinOp
Data,Typeable,Int -> BinOp
BinOp -> Int
BinOp -> [BinOp]
BinOp -> BinOp
BinOp -> BinOp -> [BinOp]
BinOp -> BinOp -> BinOp -> [BinOp]
(BinOp -> BinOp)
-> (BinOp -> BinOp)
-> (Int -> BinOp)
-> (BinOp -> Int)
-> (BinOp -> [BinOp])
-> (BinOp -> BinOp -> [BinOp])
-> (BinOp -> BinOp -> [BinOp])
-> (BinOp -> BinOp -> BinOp -> [BinOp])
-> Enum BinOp
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: BinOp -> BinOp
succ :: BinOp -> BinOp
$cpred :: BinOp -> BinOp
pred :: BinOp -> BinOp
$ctoEnum :: Int -> BinOp
toEnum :: Int -> BinOp
$cfromEnum :: BinOp -> Int
fromEnum :: BinOp -> Int
$cenumFrom :: BinOp -> [BinOp]
enumFrom :: BinOp -> [BinOp]
$cenumFromThen :: BinOp -> BinOp -> [BinOp]
enumFromThen :: BinOp -> BinOp -> [BinOp]
$cenumFromTo :: BinOp -> BinOp -> [BinOp]
enumFromTo :: BinOp -> BinOp -> [BinOp]
$cenumFromThenTo :: BinOp -> BinOp -> BinOp -> [BinOp]
enumFromThenTo :: BinOp -> BinOp -> BinOp -> [BinOp]
Enum,BinOp
BinOp -> BinOp -> Bounded BinOp
forall a. a -> a -> Bounded a
$cminBound :: BinOp
minBound :: BinOp
$cmaxBound :: BinOp
maxBound :: BinOp
Bounded)

-- | /Term -> Term -> Formula/ infix connectives
data InfixPred =
    -- Please don't change the constructor names (the Show instance is significant)
    (:=:) | (:!=:)
            deriving (InfixPred -> InfixPred -> Bool
(InfixPred -> InfixPred -> Bool)
-> (InfixPred -> InfixPred -> Bool) -> Eq InfixPred
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: InfixPred -> InfixPred -> Bool
== :: InfixPred -> InfixPred -> Bool
$c/= :: InfixPred -> InfixPred -> Bool
/= :: InfixPred -> InfixPred -> Bool
Eq,Eq InfixPred
Eq InfixPred =>
(InfixPred -> InfixPred -> Ordering)
-> (InfixPred -> InfixPred -> Bool)
-> (InfixPred -> InfixPred -> Bool)
-> (InfixPred -> InfixPred -> Bool)
-> (InfixPred -> InfixPred -> Bool)
-> (InfixPred -> InfixPred -> InfixPred)
-> (InfixPred -> InfixPred -> InfixPred)
-> Ord InfixPred
InfixPred -> InfixPred -> Bool
InfixPred -> InfixPred -> Ordering
InfixPred -> InfixPred -> InfixPred
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: InfixPred -> InfixPred -> Ordering
compare :: InfixPred -> InfixPred -> Ordering
$c< :: InfixPred -> InfixPred -> Bool
< :: InfixPred -> InfixPred -> Bool
$c<= :: InfixPred -> InfixPred -> Bool
<= :: InfixPred -> InfixPred -> Bool
$c> :: InfixPred -> InfixPred -> Bool
> :: InfixPred -> InfixPred -> Bool
$c>= :: InfixPred -> InfixPred -> Bool
>= :: InfixPred -> InfixPred -> Bool
$cmax :: InfixPred -> InfixPred -> InfixPred
max :: InfixPred -> InfixPred -> InfixPred
$cmin :: InfixPred -> InfixPred -> InfixPred
min :: InfixPred -> InfixPred -> InfixPred
Ord,Int -> InfixPred -> ShowS
[InfixPred] -> ShowS
InfixPred -> String
(Int -> InfixPred -> ShowS)
-> (InfixPred -> String)
-> ([InfixPred] -> ShowS)
-> Show InfixPred
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> InfixPred -> ShowS
showsPrec :: Int -> InfixPred -> ShowS
$cshow :: InfixPred -> String
show :: InfixPred -> String
$cshowList :: [InfixPred] -> ShowS
showList :: [InfixPred] -> ShowS
Show,ReadPrec [InfixPred]
ReadPrec InfixPred
Int -> ReadS InfixPred
ReadS [InfixPred]
(Int -> ReadS InfixPred)
-> ReadS [InfixPred]
-> ReadPrec InfixPred
-> ReadPrec [InfixPred]
-> Read InfixPred
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS InfixPred
readsPrec :: Int -> ReadS InfixPred
$creadList :: ReadS [InfixPred]
readList :: ReadS [InfixPred]
$creadPrec :: ReadPrec InfixPred
readPrec :: ReadPrec InfixPred
$creadListPrec :: ReadPrec [InfixPred]
readListPrec :: ReadPrec [InfixPred]
Read,Typeable InfixPred
Typeable InfixPred =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> InfixPred -> c InfixPred)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c InfixPred)
-> (InfixPred -> Constr)
-> (InfixPred -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c InfixPred))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InfixPred))
-> ((forall b. Data b => b -> b) -> InfixPred -> InfixPred)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> InfixPred -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> InfixPred -> r)
-> (forall u. (forall d. Data d => d -> u) -> InfixPred -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> InfixPred -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> InfixPred -> m InfixPred)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> InfixPred -> m InfixPred)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> InfixPred -> m InfixPred)
-> Data InfixPred
InfixPred -> Constr
InfixPred -> DataType
(forall b. Data b => b -> b) -> InfixPred -> InfixPred
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> InfixPred -> u
forall u. (forall d. Data d => d -> u) -> InfixPred -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> InfixPred -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> InfixPred -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> InfixPred -> m InfixPred
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> InfixPred -> m InfixPred
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c InfixPred
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> InfixPred -> c InfixPred
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c InfixPred)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InfixPred)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> InfixPred -> c InfixPred
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> InfixPred -> c InfixPred
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c InfixPred
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c InfixPred
$ctoConstr :: InfixPred -> Constr
toConstr :: InfixPred -> Constr
$cdataTypeOf :: InfixPred -> DataType
dataTypeOf :: InfixPred -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c InfixPred)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c InfixPred)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InfixPred)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InfixPred)
$cgmapT :: (forall b. Data b => b -> b) -> InfixPred -> InfixPred
gmapT :: (forall b. Data b => b -> b) -> InfixPred -> InfixPred
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> InfixPred -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> InfixPred -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> InfixPred -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> InfixPred -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> InfixPred -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> InfixPred -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> InfixPred -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> InfixPred -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> InfixPred -> m InfixPred
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> InfixPred -> m InfixPred
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> InfixPred -> m InfixPred
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> InfixPred -> m InfixPred
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> InfixPred -> m InfixPred
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> InfixPred -> m InfixPred
Data,Typeable,Int -> InfixPred
InfixPred -> Int
InfixPred -> [InfixPred]
InfixPred -> InfixPred
InfixPred -> InfixPred -> [InfixPred]
InfixPred -> InfixPred -> InfixPred -> [InfixPred]
(InfixPred -> InfixPred)
-> (InfixPred -> InfixPred)
-> (Int -> InfixPred)
-> (InfixPred -> Int)
-> (InfixPred -> [InfixPred])
-> (InfixPred -> InfixPred -> [InfixPred])
-> (InfixPred -> InfixPred -> [InfixPred])
-> (InfixPred -> InfixPred -> InfixPred -> [InfixPred])
-> Enum InfixPred
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: InfixPred -> InfixPred
succ :: InfixPred -> InfixPred
$cpred :: InfixPred -> InfixPred
pred :: InfixPred -> InfixPred
$ctoEnum :: Int -> InfixPred
toEnum :: Int -> InfixPred
$cfromEnum :: InfixPred -> Int
fromEnum :: InfixPred -> Int
$cenumFrom :: InfixPred -> [InfixPred]
enumFrom :: InfixPred -> [InfixPred]
$cenumFromThen :: InfixPred -> InfixPred -> [InfixPred]
enumFromThen :: InfixPred -> InfixPred -> [InfixPred]
$cenumFromTo :: InfixPred -> InfixPred -> [InfixPred]
enumFromTo :: InfixPred -> InfixPred -> [InfixPred]
$cenumFromThenTo :: InfixPred -> InfixPred -> InfixPred -> [InfixPred]
enumFromThenTo :: InfixPred -> InfixPred -> InfixPred -> [InfixPred]
Enum,InfixPred
InfixPred -> InfixPred -> Bounded InfixPred
forall a. a -> a -> Bounded a
$cminBound :: InfixPred
minBound :: InfixPred
$cmaxBound :: InfixPred
maxBound :: InfixPred
Bounded)

-- | Quantifier specification
data Quant = All | Exists
              deriving (Quant -> Quant -> Bool
(Quant -> Quant -> Bool) -> (Quant -> Quant -> Bool) -> Eq Quant
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Quant -> Quant -> Bool
== :: Quant -> Quant -> Bool
$c/= :: Quant -> Quant -> Bool
/= :: Quant -> Quant -> Bool
Eq,Eq Quant
Eq Quant =>
(Quant -> Quant -> Ordering)
-> (Quant -> Quant -> Bool)
-> (Quant -> Quant -> Bool)
-> (Quant -> Quant -> Bool)
-> (Quant -> Quant -> Bool)
-> (Quant -> Quant -> Quant)
-> (Quant -> Quant -> Quant)
-> Ord Quant
Quant -> Quant -> Bool
Quant -> Quant -> Ordering
Quant -> Quant -> Quant
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Quant -> Quant -> Ordering
compare :: Quant -> Quant -> Ordering
$c< :: Quant -> Quant -> Bool
< :: Quant -> Quant -> Bool
$c<= :: Quant -> Quant -> Bool
<= :: Quant -> Quant -> Bool
$c> :: Quant -> Quant -> Bool
> :: Quant -> Quant -> Bool
$c>= :: Quant -> Quant -> Bool
>= :: Quant -> Quant -> Bool
$cmax :: Quant -> Quant -> Quant
max :: Quant -> Quant -> Quant
$cmin :: Quant -> Quant -> Quant
min :: Quant -> Quant -> Quant
Ord,Int -> Quant -> ShowS
[Quant] -> ShowS
Quant -> String
(Int -> Quant -> ShowS)
-> (Quant -> String) -> ([Quant] -> ShowS) -> Show Quant
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Quant -> ShowS
showsPrec :: Int -> Quant -> ShowS
$cshow :: Quant -> String
show :: Quant -> String
$cshowList :: [Quant] -> ShowS
showList :: [Quant] -> ShowS
Show,ReadPrec [Quant]
ReadPrec Quant
Int -> ReadS Quant
ReadS [Quant]
(Int -> ReadS Quant)
-> ReadS [Quant]
-> ReadPrec Quant
-> ReadPrec [Quant]
-> Read Quant
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS Quant
readsPrec :: Int -> ReadS Quant
$creadList :: ReadS [Quant]
readList :: ReadS [Quant]
$creadPrec :: ReadPrec Quant
readPrec :: ReadPrec Quant
$creadListPrec :: ReadPrec [Quant]
readListPrec :: ReadPrec [Quant]
Read,Typeable Quant
Typeable Quant =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Quant -> c Quant)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Quant)
-> (Quant -> Constr)
-> (Quant -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Quant))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quant))
-> ((forall b. Data b => b -> b) -> Quant -> Quant)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r)
-> (forall u. (forall d. Data d => d -> u) -> Quant -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Quant -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Quant -> m Quant)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Quant -> m Quant)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Quant -> m Quant)
-> Data Quant
Quant -> Constr
Quant -> DataType
(forall b. Data b => b -> b) -> Quant -> Quant
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Quant -> u
forall u. (forall d. Data d => d -> u) -> Quant -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Quant -> m Quant
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quant -> m Quant
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Quant
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Quant -> c Quant
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Quant)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quant)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Quant -> c Quant
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Quant -> c Quant
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Quant
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Quant
$ctoConstr :: Quant -> Constr
toConstr :: Quant -> Constr
$cdataTypeOf :: Quant -> DataType
dataTypeOf :: Quant -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Quant)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Quant)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quant)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quant)
$cgmapT :: (forall b. Data b => b -> b) -> Quant -> Quant
gmapT :: (forall b. Data b => b -> b) -> Quant -> Quant
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Quant -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Quant -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Quant -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Quant -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Quant -> m Quant
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Quant -> m Quant
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quant -> m Quant
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quant -> m Quant
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quant -> m Quant
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quant -> m Quant
Data,Typeable,Int -> Quant
Quant -> Int
Quant -> [Quant]
Quant -> Quant
Quant -> Quant -> [Quant]
Quant -> Quant -> Quant -> [Quant]
(Quant -> Quant)
-> (Quant -> Quant)
-> (Int -> Quant)
-> (Quant -> Int)
-> (Quant -> [Quant])
-> (Quant -> Quant -> [Quant])
-> (Quant -> Quant -> [Quant])
-> (Quant -> Quant -> Quant -> [Quant])
-> Enum Quant
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Quant -> Quant
succ :: Quant -> Quant
$cpred :: Quant -> Quant
pred :: Quant -> Quant
$ctoEnum :: Int -> Quant
toEnum :: Int -> Quant
$cfromEnum :: Quant -> Int
fromEnum :: Quant -> Int
$cenumFrom :: Quant -> [Quant]
enumFrom :: Quant -> [Quant]
$cenumFromThen :: Quant -> Quant -> [Quant]
enumFromThen :: Quant -> Quant -> [Quant]
$cenumFromTo :: Quant -> Quant -> [Quant]
enumFromTo :: Quant -> Quant -> [Quant]
$cenumFromThenTo :: Quant -> Quant -> Quant -> [Quant]
enumFromThenTo :: Quant -> Quant -> Quant -> [Quant]
Enum,Quant
Quant -> Quant -> Bounded Quant
forall a. a -> a -> Bounded a
$cminBound :: Quant
minBound :: Quant
$cmaxBound :: Quant
maxBound :: Quant
Bounded)

-- * Formula Metadata

-- | A line of a TPTP file: Annotated formula, comment or include statement.
type TPTP_Input = TPTP_Input_ Identity
{-
    -- | Annotated formulae
    AFormula {
      name :: AtomicWord
    , role :: Role
    , formula :: Formula
    , annotations :: Annotations
    }
    | Comment String
    | Include FilePath [AtomicWord]

    deriving (Eq,Ord,Show,Read,Data,Typeable)
-}

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

-- | Forget comments in a line of a TPTP file decorated with comments
forgetTIC :: TPTP_Input_C -> TPTP_Input
forgetTIC :: TPTP_Input_C -> TPTP_Input
forgetTIC tic :: TPTP_Input_C
tic@(AFormula {}) = TPTP_Input_C
tic { formula = forgetFC (formula tic) }
forgetTIC (Comment String
s) = String -> TPTP_Input
forall (c :: * -> *). String -> TPTP_Input_ c
Comment String
s
forgetTIC (Include String
p [AtomicWord]
aws) = String -> [AtomicWord] -> TPTP_Input
forall (c :: * -> *). String -> [AtomicWord] -> TPTP_Input_ c
Include String
p [AtomicWord]
aws

-- | Generalized TPTP_Input
data TPTP_Input_ c =
   -- | Annotated formulae
   AFormula {
     forall (c :: * -> *). TPTP_Input_ c -> AtomicWord
name :: AtomicWord
   , forall (c :: * -> *). TPTP_Input_ c -> Role
role :: Role
   , forall (c :: * -> *). TPTP_Input_ c -> F c
formula :: F c
   , forall (c :: * -> *). TPTP_Input_ c -> Annotations
annotations :: Annotations
   }
   | Comment String
   | Include FilePath [AtomicWord]


deriving instance Eq (c (Formula0 (T c) (F c))) => Eq (TPTP_Input_ c)
deriving instance Ord (c (Formula0 (T c) (F c))) => Ord (TPTP_Input_ c)
deriving instance Show (c (Formula0 (T c) (F c))) => Show (TPTP_Input_ c)
deriving instance Read (c (Formula0 (T c) (F c))) => Read (TPTP_Input_ c)

deriving instance (Typeable c, Data (c (Formula0 (T c) (F c)))) => Data (TPTP_Input_ c)
deriving instance Typeable TPTP_Input_

-- | Annotations about the formulas origin
data Annotations = NoAnnotations | Annotations GTerm UsefulInfo
                  deriving (Annotations -> Annotations -> Bool
(Annotations -> Annotations -> Bool)
-> (Annotations -> Annotations -> Bool) -> Eq Annotations
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Annotations -> Annotations -> Bool
== :: Annotations -> Annotations -> Bool
$c/= :: Annotations -> Annotations -> Bool
/= :: Annotations -> Annotations -> Bool
Eq,Eq Annotations
Eq Annotations =>
(Annotations -> Annotations -> Ordering)
-> (Annotations -> Annotations -> Bool)
-> (Annotations -> Annotations -> Bool)
-> (Annotations -> Annotations -> Bool)
-> (Annotations -> Annotations -> Bool)
-> (Annotations -> Annotations -> Annotations)
-> (Annotations -> Annotations -> Annotations)
-> Ord Annotations
Annotations -> Annotations -> Bool
Annotations -> Annotations -> Ordering
Annotations -> Annotations -> Annotations
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Annotations -> Annotations -> Ordering
compare :: Annotations -> Annotations -> Ordering
$c< :: Annotations -> Annotations -> Bool
< :: Annotations -> Annotations -> Bool
$c<= :: Annotations -> Annotations -> Bool
<= :: Annotations -> Annotations -> Bool
$c> :: Annotations -> Annotations -> Bool
> :: Annotations -> Annotations -> Bool
$c>= :: Annotations -> Annotations -> Bool
>= :: Annotations -> Annotations -> Bool
$cmax :: Annotations -> Annotations -> Annotations
max :: Annotations -> Annotations -> Annotations
$cmin :: Annotations -> Annotations -> Annotations
min :: Annotations -> Annotations -> Annotations
Ord,Int -> Annotations -> ShowS
[Annotations] -> ShowS
Annotations -> String
(Int -> Annotations -> ShowS)
-> (Annotations -> String)
-> ([Annotations] -> ShowS)
-> Show Annotations
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Annotations -> ShowS
showsPrec :: Int -> Annotations -> ShowS
$cshow :: Annotations -> String
show :: Annotations -> String
$cshowList :: [Annotations] -> ShowS
showList :: [Annotations] -> ShowS
Show,ReadPrec [Annotations]
ReadPrec Annotations
Int -> ReadS Annotations
ReadS [Annotations]
(Int -> ReadS Annotations)
-> ReadS [Annotations]
-> ReadPrec Annotations
-> ReadPrec [Annotations]
-> Read Annotations
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS Annotations
readsPrec :: Int -> ReadS Annotations
$creadList :: ReadS [Annotations]
readList :: ReadS [Annotations]
$creadPrec :: ReadPrec Annotations
readPrec :: ReadPrec Annotations
$creadListPrec :: ReadPrec [Annotations]
readListPrec :: ReadPrec [Annotations]
Read,Typeable Annotations
Typeable Annotations =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Annotations -> c Annotations)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Annotations)
-> (Annotations -> Constr)
-> (Annotations -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Annotations))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c Annotations))
-> ((forall b. Data b => b -> b) -> Annotations -> Annotations)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Annotations -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Annotations -> r)
-> (forall u. (forall d. Data d => d -> u) -> Annotations -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Annotations -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Annotations -> m Annotations)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Annotations -> m Annotations)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Annotations -> m Annotations)
-> Data Annotations
Annotations -> Constr
Annotations -> DataType
(forall b. Data b => b -> b) -> Annotations -> Annotations
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Annotations -> u
forall u. (forall d. Data d => d -> u) -> Annotations -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Annotations -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Annotations -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Annotations -> m Annotations
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Annotations -> m Annotations
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Annotations
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Annotations -> c Annotations
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Annotations)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Annotations)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Annotations -> c Annotations
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Annotations -> c Annotations
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Annotations
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Annotations
$ctoConstr :: Annotations -> Constr
toConstr :: Annotations -> Constr
$cdataTypeOf :: Annotations -> DataType
dataTypeOf :: Annotations -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Annotations)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Annotations)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Annotations)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Annotations)
$cgmapT :: (forall b. Data b => b -> b) -> Annotations -> Annotations
gmapT :: (forall b. Data b => b -> b) -> Annotations -> Annotations
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Annotations -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Annotations -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Annotations -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Annotations -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Annotations -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Annotations -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Annotations -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Annotations -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Annotations -> m Annotations
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Annotations -> m Annotations
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Annotations -> m Annotations
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Annotations -> m Annotations
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Annotations -> m Annotations
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Annotations -> m Annotations
Data,Typeable)

-- | Misc annotations
data UsefulInfo = NoUsefulInfo | UsefulInfo [GTerm]
                  deriving (UsefulInfo -> UsefulInfo -> Bool
(UsefulInfo -> UsefulInfo -> Bool)
-> (UsefulInfo -> UsefulInfo -> Bool) -> Eq UsefulInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UsefulInfo -> UsefulInfo -> Bool
== :: UsefulInfo -> UsefulInfo -> Bool
$c/= :: UsefulInfo -> UsefulInfo -> Bool
/= :: UsefulInfo -> UsefulInfo -> Bool
Eq,Eq UsefulInfo
Eq UsefulInfo =>
(UsefulInfo -> UsefulInfo -> Ordering)
-> (UsefulInfo -> UsefulInfo -> Bool)
-> (UsefulInfo -> UsefulInfo -> Bool)
-> (UsefulInfo -> UsefulInfo -> Bool)
-> (UsefulInfo -> UsefulInfo -> Bool)
-> (UsefulInfo -> UsefulInfo -> UsefulInfo)
-> (UsefulInfo -> UsefulInfo -> UsefulInfo)
-> Ord UsefulInfo
UsefulInfo -> UsefulInfo -> Bool
UsefulInfo -> UsefulInfo -> Ordering
UsefulInfo -> UsefulInfo -> UsefulInfo
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: UsefulInfo -> UsefulInfo -> Ordering
compare :: UsefulInfo -> UsefulInfo -> Ordering
$c< :: UsefulInfo -> UsefulInfo -> Bool
< :: UsefulInfo -> UsefulInfo -> Bool
$c<= :: UsefulInfo -> UsefulInfo -> Bool
<= :: UsefulInfo -> UsefulInfo -> Bool
$c> :: UsefulInfo -> UsefulInfo -> Bool
> :: UsefulInfo -> UsefulInfo -> Bool
$c>= :: UsefulInfo -> UsefulInfo -> Bool
>= :: UsefulInfo -> UsefulInfo -> Bool
$cmax :: UsefulInfo -> UsefulInfo -> UsefulInfo
max :: UsefulInfo -> UsefulInfo -> UsefulInfo
$cmin :: UsefulInfo -> UsefulInfo -> UsefulInfo
min :: UsefulInfo -> UsefulInfo -> UsefulInfo
Ord,Int -> UsefulInfo -> ShowS
[UsefulInfo] -> ShowS
UsefulInfo -> String
(Int -> UsefulInfo -> ShowS)
-> (UsefulInfo -> String)
-> ([UsefulInfo] -> ShowS)
-> Show UsefulInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UsefulInfo -> ShowS
showsPrec :: Int -> UsefulInfo -> ShowS
$cshow :: UsefulInfo -> String
show :: UsefulInfo -> String
$cshowList :: [UsefulInfo] -> ShowS
showList :: [UsefulInfo] -> ShowS
Show,ReadPrec [UsefulInfo]
ReadPrec UsefulInfo
Int -> ReadS UsefulInfo
ReadS [UsefulInfo]
(Int -> ReadS UsefulInfo)
-> ReadS [UsefulInfo]
-> ReadPrec UsefulInfo
-> ReadPrec [UsefulInfo]
-> Read UsefulInfo
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS UsefulInfo
readsPrec :: Int -> ReadS UsefulInfo
$creadList :: ReadS [UsefulInfo]
readList :: ReadS [UsefulInfo]
$creadPrec :: ReadPrec UsefulInfo
readPrec :: ReadPrec UsefulInfo
$creadListPrec :: ReadPrec [UsefulInfo]
readListPrec :: ReadPrec [UsefulInfo]
Read,Typeable UsefulInfo
Typeable UsefulInfo =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> UsefulInfo -> c UsefulInfo)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c UsefulInfo)
-> (UsefulInfo -> Constr)
-> (UsefulInfo -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c UsefulInfo))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c UsefulInfo))
-> ((forall b. Data b => b -> b) -> UsefulInfo -> UsefulInfo)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> UsefulInfo -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> UsefulInfo -> r)
-> (forall u. (forall d. Data d => d -> u) -> UsefulInfo -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> UsefulInfo -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> UsefulInfo -> m UsefulInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> UsefulInfo -> m UsefulInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> UsefulInfo -> m UsefulInfo)
-> Data UsefulInfo
UsefulInfo -> Constr
UsefulInfo -> DataType
(forall b. Data b => b -> b) -> UsefulInfo -> UsefulInfo
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> UsefulInfo -> u
forall u. (forall d. Data d => d -> u) -> UsefulInfo -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UsefulInfo -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UsefulInfo -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UsefulInfo -> m UsefulInfo
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UsefulInfo -> m UsefulInfo
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UsefulInfo
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UsefulInfo -> c UsefulInfo
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UsefulInfo)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UsefulInfo)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UsefulInfo -> c UsefulInfo
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UsefulInfo -> c UsefulInfo
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UsefulInfo
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UsefulInfo
$ctoConstr :: UsefulInfo -> Constr
toConstr :: UsefulInfo -> Constr
$cdataTypeOf :: UsefulInfo -> DataType
dataTypeOf :: UsefulInfo -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UsefulInfo)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UsefulInfo)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UsefulInfo)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UsefulInfo)
$cgmapT :: (forall b. Data b => b -> b) -> UsefulInfo -> UsefulInfo
gmapT :: (forall b. Data b => b -> b) -> UsefulInfo -> UsefulInfo
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UsefulInfo -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UsefulInfo -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UsefulInfo -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UsefulInfo -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> UsefulInfo -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> UsefulInfo -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UsefulInfo -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UsefulInfo -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UsefulInfo -> m UsefulInfo
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UsefulInfo -> m UsefulInfo
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UsefulInfo -> m UsefulInfo
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UsefulInfo -> m UsefulInfo
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UsefulInfo -> m UsefulInfo
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UsefulInfo -> m UsefulInfo
Data,Typeable)

-- | Formula roles
newtype Role = Role { Role -> String
unrole :: String }
            deriving (Role -> Role -> Bool
(Role -> Role -> Bool) -> (Role -> Role -> Bool) -> Eq Role
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Role -> Role -> Bool
== :: Role -> Role -> Bool
$c/= :: Role -> Role -> Bool
/= :: Role -> Role -> Bool
Eq,Eq Role
Eq Role =>
(Role -> Role -> Ordering)
-> (Role -> Role -> Bool)
-> (Role -> Role -> Bool)
-> (Role -> Role -> Bool)
-> (Role -> Role -> Bool)
-> (Role -> Role -> Role)
-> (Role -> Role -> Role)
-> Ord Role
Role -> Role -> Bool
Role -> Role -> Ordering
Role -> Role -> Role
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Role -> Role -> Ordering
compare :: Role -> Role -> Ordering
$c< :: Role -> Role -> Bool
< :: Role -> Role -> Bool
$c<= :: Role -> Role -> Bool
<= :: Role -> Role -> Bool
$c> :: Role -> Role -> Bool
> :: Role -> Role -> Bool
$c>= :: Role -> Role -> Bool
>= :: Role -> Role -> Bool
$cmax :: Role -> Role -> Role
max :: Role -> Role -> Role
$cmin :: Role -> Role -> Role
min :: Role -> Role -> Role
Ord,Int -> Role -> ShowS
[Role] -> ShowS
Role -> String
(Int -> Role -> ShowS)
-> (Role -> String) -> ([Role] -> ShowS) -> Show Role
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Role -> ShowS
showsPrec :: Int -> Role -> ShowS
$cshow :: Role -> String
show :: Role -> String
$cshowList :: [Role] -> ShowS
showList :: [Role] -> ShowS
Show,ReadPrec [Role]
ReadPrec Role
Int -> ReadS Role
ReadS [Role]
(Int -> ReadS Role)
-> ReadS [Role] -> ReadPrec Role -> ReadPrec [Role] -> Read Role
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS Role
readsPrec :: Int -> ReadS Role
$creadList :: ReadS [Role]
readList :: ReadS [Role]
$creadPrec :: ReadPrec Role
readPrec :: ReadPrec Role
$creadListPrec :: ReadPrec [Role]
readListPrec :: ReadPrec [Role]
Read,Typeable Role
Typeable Role =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Role -> c Role)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Role)
-> (Role -> Constr)
-> (Role -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Role))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Role))
-> ((forall b. Data b => b -> b) -> Role -> Role)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r)
-> (forall u. (forall d. Data d => d -> u) -> Role -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Role -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Role -> m Role)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Role -> m Role)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Role -> m Role)
-> Data Role
Role -> Constr
Role -> DataType
(forall b. Data b => b -> b) -> Role -> Role
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Role -> u
forall u. (forall d. Data d => d -> u) -> Role -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Role -> m Role
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Role -> m Role
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Role
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Role -> c Role
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Role)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Role)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Role -> c Role
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Role -> c Role
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Role
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Role
$ctoConstr :: Role -> Constr
toConstr :: Role -> Constr
$cdataTypeOf :: Role -> DataType
dataTypeOf :: Role -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Role)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Role)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Role)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Role)
$cgmapT :: (forall b. Data b => b -> b) -> Role -> Role
gmapT :: (forall b. Data b => b -> b) -> Role -> Role
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Role -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Role -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Role -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Role -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Role -> m Role
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Role -> m Role
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Role -> m Role
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Role -> m Role
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Role -> m Role
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Role -> m Role
Data,Typeable)


-- | Metadata (the /general_data/ rule in TPTP's grammar)
data GData = GWord AtomicWord
                 | GApp AtomicWord [GTerm]
                 | GVar V
                 | GNumber Rational
                 | GDistinctObject String
                 | GFormulaData String Formula
                 | GFormulaTerm String Term
                   deriving (GData -> GData -> Bool
(GData -> GData -> Bool) -> (GData -> GData -> Bool) -> Eq GData
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: GData -> GData -> Bool
== :: GData -> GData -> Bool
$c/= :: GData -> GData -> Bool
/= :: GData -> GData -> Bool
Eq,Eq GData
Eq GData =>
(GData -> GData -> Ordering)
-> (GData -> GData -> Bool)
-> (GData -> GData -> Bool)
-> (GData -> GData -> Bool)
-> (GData -> GData -> Bool)
-> (GData -> GData -> GData)
-> (GData -> GData -> GData)
-> Ord GData
GData -> GData -> Bool
GData -> GData -> Ordering
GData -> GData -> GData
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: GData -> GData -> Ordering
compare :: GData -> GData -> Ordering
$c< :: GData -> GData -> Bool
< :: GData -> GData -> Bool
$c<= :: GData -> GData -> Bool
<= :: GData -> GData -> Bool
$c> :: GData -> GData -> Bool
> :: GData -> GData -> Bool
$c>= :: GData -> GData -> Bool
>= :: GData -> GData -> Bool
$cmax :: GData -> GData -> GData
max :: GData -> GData -> GData
$cmin :: GData -> GData -> GData
min :: GData -> GData -> GData
Ord,Int -> GData -> ShowS
[GData] -> ShowS
GData -> String
(Int -> GData -> ShowS)
-> (GData -> String) -> ([GData] -> ShowS) -> Show GData
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GData -> ShowS
showsPrec :: Int -> GData -> ShowS
$cshow :: GData -> String
show :: GData -> String
$cshowList :: [GData] -> ShowS
showList :: [GData] -> ShowS
Show,ReadPrec [GData]
ReadPrec GData
Int -> ReadS GData
ReadS [GData]
(Int -> ReadS GData)
-> ReadS [GData]
-> ReadPrec GData
-> ReadPrec [GData]
-> Read GData
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS GData
readsPrec :: Int -> ReadS GData
$creadList :: ReadS [GData]
readList :: ReadS [GData]
$creadPrec :: ReadPrec GData
readPrec :: ReadPrec GData
$creadListPrec :: ReadPrec [GData]
readListPrec :: ReadPrec [GData]
Read,Typeable GData
Typeable GData =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> GData -> c GData)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c GData)
-> (GData -> Constr)
-> (GData -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c GData))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GData))
-> ((forall b. Data b => b -> b) -> GData -> GData)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GData -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GData -> r)
-> (forall u. (forall d. Data d => d -> u) -> GData -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> GData -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> GData -> m GData)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> GData -> m GData)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> GData -> m GData)
-> Data GData
GData -> Constr
GData -> DataType
(forall b. Data b => b -> b) -> GData -> GData
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> GData -> u
forall u. (forall d. Data d => d -> u) -> GData -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GData -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GData -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> GData -> m GData
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GData -> m GData
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c GData
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> GData -> c GData
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c GData)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GData)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> GData -> c GData
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> GData -> c GData
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c GData
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c GData
$ctoConstr :: GData -> Constr
toConstr :: GData -> Constr
$cdataTypeOf :: GData -> DataType
dataTypeOf :: GData -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c GData)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c GData)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GData)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GData)
$cgmapT :: (forall b. Data b => b -> b) -> GData -> GData
gmapT :: (forall b. Data b => b -> b) -> GData -> GData
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GData -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GData -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GData -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GData -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> GData -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> GData -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> GData -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> GData -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> GData -> m GData
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> GData -> m GData
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GData -> m GData
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GData -> m GData
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GData -> m GData
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GData -> m GData
Data,Typeable)

-- | Metadata (the /general_term/ rule in TPTP's grammar)
data GTerm = ColonSep GData GTerm
           | GTerm GData
           | GList [GTerm]
             deriving (GTerm -> GTerm -> Bool
(GTerm -> GTerm -> Bool) -> (GTerm -> GTerm -> Bool) -> Eq GTerm
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: GTerm -> GTerm -> Bool
== :: GTerm -> GTerm -> Bool
$c/= :: GTerm -> GTerm -> Bool
/= :: GTerm -> GTerm -> Bool
Eq,Eq GTerm
Eq GTerm =>
(GTerm -> GTerm -> Ordering)
-> (GTerm -> GTerm -> Bool)
-> (GTerm -> GTerm -> Bool)
-> (GTerm -> GTerm -> Bool)
-> (GTerm -> GTerm -> Bool)
-> (GTerm -> GTerm -> GTerm)
-> (GTerm -> GTerm -> GTerm)
-> Ord GTerm
GTerm -> GTerm -> Bool
GTerm -> GTerm -> Ordering
GTerm -> GTerm -> GTerm
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: GTerm -> GTerm -> Ordering
compare :: GTerm -> GTerm -> Ordering
$c< :: GTerm -> GTerm -> Bool
< :: GTerm -> GTerm -> Bool
$c<= :: GTerm -> GTerm -> Bool
<= :: GTerm -> GTerm -> Bool
$c> :: GTerm -> GTerm -> Bool
> :: GTerm -> GTerm -> Bool
$c>= :: GTerm -> GTerm -> Bool
>= :: GTerm -> GTerm -> Bool
$cmax :: GTerm -> GTerm -> GTerm
max :: GTerm -> GTerm -> GTerm
$cmin :: GTerm -> GTerm -> GTerm
min :: GTerm -> GTerm -> GTerm
Ord,Int -> GTerm -> ShowS
[GTerm] -> ShowS
GTerm -> String
(Int -> GTerm -> ShowS)
-> (GTerm -> String) -> ([GTerm] -> ShowS) -> Show GTerm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GTerm -> ShowS
showsPrec :: Int -> GTerm -> ShowS
$cshow :: GTerm -> String
show :: GTerm -> String
$cshowList :: [GTerm] -> ShowS
showList :: [GTerm] -> ShowS
Show,ReadPrec [GTerm]
ReadPrec GTerm
Int -> ReadS GTerm
ReadS [GTerm]
(Int -> ReadS GTerm)
-> ReadS [GTerm]
-> ReadPrec GTerm
-> ReadPrec [GTerm]
-> Read GTerm
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS GTerm
readsPrec :: Int -> ReadS GTerm
$creadList :: ReadS [GTerm]
readList :: ReadS [GTerm]
$creadPrec :: ReadPrec GTerm
readPrec :: ReadPrec GTerm
$creadListPrec :: ReadPrec [GTerm]
readListPrec :: ReadPrec [GTerm]
Read,Typeable GTerm
Typeable GTerm =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> GTerm -> c GTerm)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c GTerm)
-> (GTerm -> Constr)
-> (GTerm -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c GTerm))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GTerm))
-> ((forall b. Data b => b -> b) -> GTerm -> GTerm)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GTerm -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GTerm -> r)
-> (forall u. (forall d. Data d => d -> u) -> GTerm -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> GTerm -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> GTerm -> m GTerm)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> GTerm -> m GTerm)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> GTerm -> m GTerm)
-> Data GTerm
GTerm -> Constr
GTerm -> DataType
(forall b. Data b => b -> b) -> GTerm -> GTerm
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> GTerm -> u
forall u. (forall d. Data d => d -> u) -> GTerm -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GTerm -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GTerm -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> GTerm -> m GTerm
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GTerm -> m GTerm
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c GTerm
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> GTerm -> c GTerm
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c GTerm)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GTerm)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> GTerm -> c GTerm
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> GTerm -> c GTerm
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c GTerm
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c GTerm
$ctoConstr :: GTerm -> Constr
toConstr :: GTerm -> Constr
$cdataTypeOf :: GTerm -> DataType
dataTypeOf :: GTerm -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c GTerm)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c GTerm)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GTerm)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GTerm)
$cgmapT :: (forall b. Data b => b -> b) -> GTerm -> GTerm
gmapT :: (forall b. Data b => b -> b) -> GTerm -> GTerm
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GTerm -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GTerm -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GTerm -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GTerm -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> GTerm -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> GTerm -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> GTerm -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> GTerm -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> GTerm -> m GTerm
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> GTerm -> m GTerm
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GTerm -> m GTerm
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GTerm -> m GTerm
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GTerm -> m GTerm
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GTerm -> m GTerm
Data,Typeable)




-- * Gathering free Variables

-- class FormulaOrTerm c a where
--     elimFormulaOrTerm :: (F c -> r) -> (T c -> r) -> a -> r

-- instance FormulaOrTerm Identity Formula where
--     elimFormulaOrTerm k _ x = k x

-- instance FormulaOrTerm Identity Term where
--     elimFormulaOrTerm _ k x = k x

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

-- | Universally quantify all free variables in the formula
univquant_free_vars :: Formula -> Formula
univquant_free_vars :: Formula -> Formula
univquant_free_vars Formula
cnf =
    case Set V -> [V]
forall a. Set a -> [a]
S.toList (Formula -> Set V
forall a. FreeVars a => a -> Set V
freeVars Formula
cnf) of
      [] -> Formula
cnf
      [V]
vars -> [V] -> Formula -> Formula
forall (c :: * -> *). Pointed c => [V] -> F c -> F c
for_all [V]
vars Formula
cnf

-- | Universally quantify all free variables in the formula
univquant_free_vars_FC :: FormulaC -> FormulaC
univquant_free_vars_FC :: FormulaC -> FormulaC
univquant_free_vars_FC FormulaC
cnf =
    case Set V -> [V]
forall a. Set a -> [a]
S.toList (Formula -> Set V
forall a. FreeVars a => a -> Set V
freeVars (FormulaC -> Formula
forgetFC FormulaC
cnf)) of
      [] -> FormulaC
cnf
      [V]
vars -> [V] -> FormulaC -> FormulaC
forall (c :: * -> *). Pointed c => [V] -> F c -> F c
for_all [V]
vars FormulaC
cnf

instance FreeVars Formula where
    freeVars :: Formula -> Set V
freeVars = (Formula -> Set V)
-> (Quant -> [V] -> Formula -> Set V)
-> (Formula -> BinOp -> Formula -> Set V)
-> (T Identity -> InfixPred -> T Identity -> Set V)
-> (AtomicWord -> [T Identity] -> Set V)
-> Formula
-> Set V
forall (t :: * -> *) r.
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
foldF
               Formula -> Set V
forall a. FreeVars a => a -> Set V
freeVars
               (\Quant
_ [V]
vars Formula
x -> Set V -> Set V -> Set V
forall a. Ord a => Set a -> Set a -> Set a
S.difference (Formula -> Set V
forall a. FreeVars a => a -> Set V
freeVars Formula
x) ([V] -> Set V
forall a. Ord a => [a] -> Set a
S.fromList [V]
vars))
               (\Formula
x BinOp
_ Formula
y -> (Set V -> Set V -> Set V
forall a. Monoid a => a -> a -> a
mappend (Set V -> Set V -> Set V)
-> (Formula -> Set V) -> Formula -> Formula -> Set V
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Formula -> Set V
forall a. FreeVars a => a -> Set V
freeVars) Formula
x Formula
y)
               (\T Identity
x InfixPred
_ T Identity
y -> (Set V -> Set V -> Set V
forall a. Monoid a => a -> a -> a
mappend (Set V -> Set V -> Set V)
-> (T Identity -> Set V) -> T Identity -> T Identity -> Set V
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` T Identity -> Set V
forall a. FreeVars a => a -> Set V
freeVars) T Identity
x T Identity
y)
               (\AtomicWord
_ [T Identity]
args -> [Set V] -> Set V
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ((T Identity -> Set V) -> [T Identity] -> [Set V]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap T Identity -> Set V
forall a. FreeVars a => a -> Set V
freeVars [T Identity]
args))

instance FreeVars Term where
    freeVars :: T Identity -> Set V
freeVars = (String -> Set V)
-> (Rational -> Set V)
-> (V -> Set V)
-> (AtomicWord -> [T Identity] -> Set V)
-> T Identity
-> Set V
forall (t :: * -> *) r.
Copointed t =>
(String -> r)
-> (Rational -> r)
-> (V -> r)
-> (AtomicWord -> [T t] -> r)
-> T t
-> r
foldT
               (Set V -> String -> Set V
forall a b. a -> b -> a
const Set V
forall a. Monoid a => a
mempty)
               (Set V -> Rational -> Set V
forall a b. a -> b -> a
const Set V
forall a. Monoid a => a
mempty)
               V -> Set V
forall a. a -> Set a
S.singleton
               (\AtomicWord
_ [T Identity]
args -> [Set V] -> Set V
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ((T Identity -> Set V) -> [T Identity] -> [Set V]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap T Identity -> Set V
forall a. FreeVars a => a -> Set V
freeVars [T Identity]
args))


--- Have the Arbitrary instances in this module to avoid orphan instances

instance Arbitrary TPTP_Input
    where arbitrary :: Gen TPTP_Input
arbitrary = [(Int, Gen TPTP_Input)] -> Gen TPTP_Input
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [(Int
10,
                                    do
                                      AtomicWord
x1 <- String -> AtomicWord
AtomicWord (String -> AtomicWord) -> Gen String -> Gen AtomicWord
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen String
arbLowerWord
                                      Role
x2 <- Gen Role
forall a. Arbitrary a => Gen a
arbitrary
                                      Formula
x3 <- Gen Formula
forall a. Arbitrary a => Gen a
arbitrary
                                      Annotations
x4 <- Gen Annotations
forall a. Arbitrary a => Gen a
arbitrary
                                      TPTP_Input -> Gen TPTP_Input
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (AtomicWord -> Role -> Formula -> Annotations -> TPTP_Input
forall (c :: * -> *).
AtomicWord -> Role -> F c -> Annotations -> TPTP_Input_ c
AFormula AtomicWord
x1 Role
x2 Formula
x3 Annotations
x4))

                                  , (Int
1,
                                    do
                                      String
x1 <- Gen String
arbPrintable
                                      TPTP_Input -> Gen TPTP_Input
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> TPTP_Input
forall (c :: * -> *). String -> TPTP_Input_ c
Comment (String
"% "String -> ShowS
forall a. [a] -> [a] -> [a]
++String
x1))
                                  )

                                  , (Int
1, String -> [AtomicWord] -> TPTP_Input
forall (c :: * -> *). String -> [AtomicWord] -> TPTP_Input_ c
Include (String -> [AtomicWord] -> TPTP_Input)
-> Gen String -> Gen ([AtomicWord] -> TPTP_Input)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Gen String
arbLowerWord Gen ([AtomicWord] -> TPTP_Input)
-> Gen [AtomicWord] -> Gen TPTP_Input
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
`ap`
                                         Gen AtomicWord -> Gen [AtomicWord]
forall a. Gen a -> Gen [a]
listOf Gen AtomicWord
forall a. Arbitrary a => Gen a
arbitrary)
                                ]

instance Arbitrary Formula
    where arbitrary :: Gen Formula
arbitrary = (Formula0 (T Identity) Formula -> Formula)
-> Gen (Formula0 (T Identity) Formula) -> Gen Formula
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Identity (Formula0 (T Identity) Formula) -> Formula
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F (Identity (Formula0 (T Identity) Formula) -> Formula)
-> (Formula0 (T Identity) Formula
    -> Identity (Formula0 (T Identity) Formula))
-> Formula0 (T Identity) Formula
-> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula0 (T Identity) Formula
-> Identity (Formula0 (T Identity) Formula)
forall a. a -> Identity a
forall (p :: * -> *) a. Pointed p => a -> p a
point) Gen (Formula0 (T Identity) Formula)
forall a. Arbitrary a => Gen a
arbitrary

instance Arbitrary Term
    where arbitrary :: Gen (T Identity)
arbitrary = (Term0 (T Identity) -> T Identity)
-> Gen (Term0 (T Identity)) -> Gen (T Identity)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Identity (Term0 (T Identity)) -> T Identity
forall (c :: * -> *). c (Term0 (T c)) -> T c
T (Identity (Term0 (T Identity)) -> T Identity)
-> (Term0 (T Identity) -> Identity (Term0 (T Identity)))
-> Term0 (T Identity)
-> T Identity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term0 (T Identity) -> Identity (Term0 (T Identity))
forall a. a -> Identity a
forall (p :: * -> *) a. Pointed p => a -> p a
point) Gen (Term0 (T Identity))
forall a. Arbitrary a => Gen a
arbitrary

instance Arbitrary Annotations
    where arbitrary :: Gen Annotations
arbitrary = [Gen Annotations] -> Gen Annotations
forall a. HasCallStack => [Gen a] -> Gen a
oneof [
                              Annotations -> Gen Annotations
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return Annotations
NoAnnotations
                            , GTerm -> UsefulInfo -> Annotations
Annotations (GTerm -> UsefulInfo -> Annotations)
-> Gen GTerm -> Gen (UsefulInfo -> Annotations)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Gen GTerm
forall a. Arbitrary a => Gen a
arbitrary Gen (UsefulInfo -> Annotations)
-> Gen UsefulInfo -> Gen Annotations
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
`ap` Gen UsefulInfo
forall a. Arbitrary a => Gen a
arbitrary
                      ]

instance Arbitrary UsefulInfo
    where arbitrary :: Gen UsefulInfo
arbitrary = [Gen UsefulInfo] -> Gen UsefulInfo
forall a. HasCallStack => [Gen a] -> Gen a
oneof [
                              UsefulInfo -> Gen UsefulInfo
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return UsefulInfo
NoUsefulInfo
                             , do
                                [GTerm]
x1 <- Gen [GTerm]
forall a. Arbitrary a => Gen a
arbitrary
                                UsefulInfo -> Gen UsefulInfo
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return ([GTerm] -> UsefulInfo
UsefulInfo [GTerm]
x1)
                      ]

instance Arbitrary Role
    where arbitrary :: Gen Role
arbitrary = String -> Role
Role (String -> Role) -> Gen String -> Gen Role
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Gen String
arbLowerWord


instance (Arbitrary a, Arbitrary b) => Arbitrary (Formula0 a b)


    where arbitrary :: Gen (Formula0 a b)
arbitrary = (Int -> Gen (Formula0 a b)) -> Gen (Formula0 a b)
forall a. (Int -> Gen a) -> Gen a
sized Int -> Gen (Formula0 a b)
forall {formula} {term}.
(Arbitrary formula, Arbitrary term) =>
Int -> Gen (Formula0 term formula)
go

           where
            go :: Int -> Gen (Formula0 term formula)
go Int
0 = (AtomicWord -> [term] -> Formula0 term formula)
-> [term] -> AtomicWord -> Formula0 term formula
forall a b c. (a -> b -> c) -> b -> a -> c
flip AtomicWord -> [term] -> Formula0 term formula
forall term formula. AtomicWord -> [term] -> Formula0 term formula
PredApp [] (AtomicWord -> Formula0 term formula)
-> Gen AtomicWord -> Gen (Formula0 term formula)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Gen AtomicWord
forall a. Arbitrary a => Gen a
arbitrary

            go Int
i =
                [Gen (Formula0 term formula)] -> Gen (Formula0 term formula)
forall a. HasCallStack => [Gen a] -> Gen a
oneof [ do
                                  Int
ileft <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0,Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
                                  formula
x1 <- Int -> Gen formula -> Gen formula
forall a. HasCallStack => Int -> Gen a -> Gen a
resize Int
ileft Gen formula
forall a. Arbitrary a => Gen a
arbitrary
                                  BinOp
x2 <- Gen BinOp
forall a. Arbitrary a => Gen a
arbitrary
                                  formula
x3 <- Int -> Gen formula -> Gen formula
forall a. HasCallStack => Int -> Gen a -> Gen a
resize (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
ileft) Gen formula
forall a. Arbitrary a => Gen a
arbitrary
                                  Formula0 term formula -> Gen (Formula0 term formula)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (formula -> BinOp -> formula -> Formula0 term formula
forall term formula.
formula -> BinOp -> formula -> Formula0 term formula
BinOp formula
x1 BinOp
x2 formula
x3)

                      , do
                                  term
x1 <- Gen term
forall a. Arbitrary a => Gen a
arbitrary
                                  InfixPred
x2 <- Gen InfixPred
forall a. Arbitrary a => Gen a
arbitrary
                                  term
x3 <- Gen term
forall a. Arbitrary a => Gen a
arbitrary
                                  Formula0 term formula -> Gen (Formula0 term formula)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (term -> InfixPred -> term -> Formula0 term formula
forall term formula.
term -> InfixPred -> term -> Formula0 term formula
InfixPred term
x1 InfixPred
x2 term
x3)

                      , do
                                  AtomicWord
x1 <- Gen AtomicWord
forall a. Arbitrary a => Gen a
arbitrary
                                  [term]
x2 <- (Int -> Gen [term]) -> Gen [term]
forall a. (Int -> Gen a) -> Gen a
argsFreq Int -> Gen [term]
forall a. Arbitrary a => Int -> Gen [a]
vector
                                  Formula0 term formula -> Gen (Formula0 term formula)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (AtomicWord -> [term] -> Formula0 term formula
forall term formula. AtomicWord -> [term] -> Formula0 term formula
PredApp AtomicWord
x1 [term]
x2)

                      , do
                               Quant
x1 <- Gen Quant
forall a. Arbitrary a => Gen a
arbitrary
                               [V]
x2 <- (V -> [V] -> [V]) -> Gen V -> Gen [V] -> Gen [V]
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (:) Gen V
forall a. Arbitrary a => Gen a
arbitrary ((Int -> Gen [V]) -> Gen [V]
forall a. (Int -> Gen a) -> Gen a
argsFreq (\Int
nargs -> Int -> Gen V -> Gen [V]
forall a. Int -> Gen a -> Gen [a]
vectorOf Int
nargs Gen V
forall a. Arbitrary a => Gen a
arbitrary))
                               formula
x3 <- Int -> Gen formula -> Gen formula
forall a. HasCallStack => Int -> Gen a -> Gen a
resize (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Gen formula
forall a. Arbitrary a => Gen a
arbitrary
                               Formula0 term formula -> Gen (Formula0 term formula)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Quant -> [V] -> formula -> Formula0 term formula
forall term formula.
Quant -> [V] -> formula -> Formula0 term formula
Quant Quant
x1 [V]
x2 formula
x3)

                      , do
                                  formula
x1 <- Int -> Gen formula -> Gen formula
forall a. HasCallStack => Int -> Gen a -> Gen a
resize (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Gen formula
forall a. Arbitrary a => Gen a
arbitrary
                                  Formula0 term formula -> Gen (Formula0 term formula)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (formula -> Formula0 term formula
forall term formula. formula -> Formula0 term formula
(:~:) formula
x1)
                      ]

instance Arbitrary BinOp
    where arbitrary :: Gen BinOp
arbitrary = [BinOp] -> Gen BinOp
forall a. HasCallStack => [a] -> Gen a
elements

                             [ BinOp
(:<=>:)
                             , BinOp
(:=>:)
                             , BinOp
(:<=:)
                             , BinOp
(:&:)
                             , BinOp
(:|:)
                             , BinOp
(:~&:)
                             , BinOp
(:~|:)
                             , BinOp
(:<~>:)
                             ]

instance Arbitrary InfixPred
    where arbitrary :: Gen InfixPred
arbitrary = [InfixPred] -> Gen InfixPred
forall a. HasCallStack => [a] -> Gen a
elements [ InfixPred
(:=:),InfixPred
(:!=:) ]

instance Arbitrary Quant
    where arbitrary :: Gen Quant
arbitrary = [Quant] -> Gen Quant
forall a. HasCallStack => [a] -> Gen a
elements [Quant
All,Quant
Exists]

instance Arbitrary a => Arbitrary (Term0 a)
    where arbitrary :: Gen (Term0 a)
arbitrary = (Int -> Gen (Term0 a)) -> Gen (Term0 a)
forall a. (Int -> Gen a) -> Gen a
sized Int -> Gen (Term0 a)
forall {term}. Arbitrary term => Int -> Gen (Term0 term)
go
           where


            go :: Int -> Gen (Term0 term)
go Int
0 = [(Int, Gen (Term0 term))] -> Gen (Term0 term)
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [ (Int
2,V -> Term0 term
forall term. V -> Term0 term
Var (V -> Term0 term) -> Gen V -> Gen (Term0 term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen V
forall a. Arbitrary a => Gen a
arbitrary), (Int
1,AtomicWord -> [term] -> Term0 term
forall term. AtomicWord -> [term] -> Term0 term
FunApp (AtomicWord -> [term] -> Term0 term)
-> Gen AtomicWord -> Gen ([term] -> Term0 term)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Gen AtomicWord
forall a. Arbitrary a => Gen a
arbitrary Gen ([term] -> Term0 term) -> Gen [term] -> Gen (Term0 term)
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
`ap` [term] -> Gen [term]
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return[] ) ]

            go Int
i = [Gen (Term0 term)] -> Gen (Term0 term)
forall a. HasCallStack => [Gen a] -> Gen a
oneof [
                             do
                              V
x1 <- Gen V
forall a. Arbitrary a => Gen a
arbitrary
                              Term0 term -> Gen (Term0 term)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Term0 term
forall term. V -> Term0 term
Var V
x1)

                           , (Rational -> Term0 term) -> Gen (Term0 term)
forall a a1. (Arbitrary a, Num a) => (a -> a1) -> Gen a1
arbNum Rational -> Term0 term
forall term. Rational -> Term0 term
NumberLitTerm


                           , do
                              String
x1 <- Gen String
arbPrintable
                              Term0 term -> Gen (Term0 term)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Term0 term
forall term. String -> Term0 term
DistinctObjectTerm String
x1)

                           , do
                              AtomicWord
x1 <- Gen AtomicWord
forall a. Arbitrary a => Gen a
arbitrary
                              [term]
args <- (Int -> Gen [term]) -> Gen [term]
forall a. (Int -> Gen a) -> Gen a
argsFreq
                                (\Int
nargs -> do
                                   [Int]
parti <- Int -> Int -> Gen [Int]
arbPartition Int
nargs (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
                                   (Int -> Gen term) -> [Int] -> Gen [term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Int -> Gen term -> Gen term) -> Gen term -> Int -> Gen term
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Gen term -> Gen term
forall a. HasCallStack => Int -> Gen a -> Gen a
resize Gen term
forall a. Arbitrary a => Gen a
arbitrary) [Int]
parti
                                )

                              Term0 term -> Gen (Term0 term)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (AtomicWord -> [term] -> Term0 term
forall term. AtomicWord -> [term] -> Term0 term
FunApp AtomicWord
x1 [term]
args)
                           ]

instance Arbitrary GData
    where arbitrary :: Gen GData
arbitrary = (Int -> Gen GData) -> Gen GData
forall a. (Int -> Gen a) -> Gen a
sized Int -> Gen GData
go

                  where
                       go :: Int -> Gen GData
go Int
0 = [Gen GData] -> Gen GData
forall a. HasCallStack => [Gen a] -> Gen a
oneof [ (AtomicWord -> GData) -> Gen AtomicWord -> Gen GData
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AtomicWord -> GData
GWord Gen AtomicWord
forall a. Arbitrary a => Gen a
arbitrary
                                    , (V -> GData) -> Gen V -> Gen GData
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap V -> GData
GVar Gen V
forall a. Arbitrary a => Gen a
arbitrary
                                    ]

                       go Int
i =
                           [Gen GData] -> Gen GData
forall a. HasCallStack => [Gen a] -> Gen a
oneof
                           [
                            AtomicWord -> GData
GWord (AtomicWord -> GData) -> Gen AtomicWord -> Gen GData
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen AtomicWord
forall a. Arbitrary a => Gen a
arbitrary

                           ,do
                              String
x1 <- Gen String
arbLowerWord
                              [GTerm]
args <- (Int -> Gen [GTerm]) -> Gen [GTerm]
forall a. (Int -> Gen a) -> Gen a
argsFreq
                                         (\Int
nargs -> do
                                            [Int]
parti <- Int -> Int -> Gen [Int]
arbPartition Int
nargs (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
                                            (Int -> Gen GTerm) -> [Int] -> Gen [GTerm]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Int -> Gen GTerm -> Gen GTerm) -> Gen GTerm -> Int -> Gen GTerm
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Gen GTerm -> Gen GTerm
forall a. HasCallStack => Int -> Gen a -> Gen a
resize Gen GTerm
forall a. Arbitrary a => Gen a
arbitrary) [Int]
parti
                                         ) Gen [GTerm] -> ([GTerm] -> Bool) -> Gen [GTerm]
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` ([GTerm] -> [GTerm] -> Bool
forall a. Eq a => a -> a -> Bool
(/=) [])

                              GData -> Gen GData
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (AtomicWord -> [GTerm] -> GData
GApp (String -> AtomicWord
AtomicWord String
x1) [GTerm]
args)

                           ,V -> GData
GVar (V -> GData) -> Gen V -> Gen GData
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen V
forall a. Arbitrary a => Gen a
arbitrary
                           ,(Rational -> GData) -> Gen GData
forall a a1. (Arbitrary a, Num a) => (a -> a1) -> Gen a1
arbNum Rational -> GData
GNumber

                           ,String -> GData
GDistinctObject (String -> GData) -> Gen String -> Gen GData
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen String
arbPrintable
                           ,[Gen GData] -> Gen GData
forall a. HasCallStack => [Gen a] -> Gen a
oneof
                            [ String -> Formula -> GData
GFormulaData String
"$fof" (Formula -> GData) -> Gen Formula -> Gen GData
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (Int -> Gen Formula) -> Gen Formula
forall a. (Int -> Gen a) -> Gen a
sized (\Int
n -> Int -> Gen Formula -> Gen Formula
forall a. HasCallStack => Int -> Gen a -> Gen a
resize (Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) Gen Formula
forall a. Arbitrary a => Gen a
arbitrary)
                            , String -> Formula -> GData
GFormulaData String
"$cnf" (Formula -> GData) -> Gen Formula -> Gen GData
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (Int -> Gen Formula) -> Gen Formula
forall a. (Int -> Gen a) -> Gen a
sized (\Int
n -> Int -> Gen Formula -> Gen Formula
forall a. HasCallStack => Int -> Gen a -> Gen a
resize (Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) Gen Formula
arbCNF)
                            , String -> T Identity -> GData
GFormulaTerm String
"$fot" (T Identity -> GData) -> Gen (T Identity) -> Gen GData
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (Int -> Gen (T Identity)) -> Gen (T Identity)
forall a. (Int -> Gen a) -> Gen a
sized (\Int
n -> Int -> Gen (T Identity) -> Gen (T Identity)
forall a. HasCallStack => Int -> Gen a -> Gen a
resize (Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) Gen (T Identity)
forall a. Arbitrary a => Gen a
arbitrary)
                            ]
                           ]

arbCNF :: Gen Formula
arbCNF :: Gen Formula
arbCNF = do
    ([Formula]
xs :: [Formula]) <- Gen Formula -> Gen [Formula]
forall a. Gen a -> Gen [a]
forall (f :: * -> *) a. Arbitrary1 f => Gen a -> Gen (f a)
liftArbitrary Gen Formula
arbLiteral Gen [Formula] -> ([Formula] -> Bool) -> Gen [Formula]
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (Bool -> Bool
not (Bool -> Bool) -> ([Formula] -> Bool) -> [Formula] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Formula] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Prelude.null)
    Formula -> Gen Formula
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Formula -> Gen Formula) -> Formula -> Gen Formula
forall a b. (a -> b) -> a -> b
$ (Formula -> Formula -> Formula) -> [Formula] -> Formula
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Formula -> Formula -> Formula
forall (c :: * -> *). Pointed c => F c -> F c -> F c
(.|.) [Formula]
xs


arbLiteral :: Gen Formula
arbLiteral :: Gen Formula
arbLiteral = [Gen Formula] -> Gen Formula
forall a. HasCallStack => [Gen a] -> Gen a
oneof
    [
      do
            Bool
p <- Gen Bool
forall a. Arbitrary a => Gen a
arbitrary
            Formula
x <- Gen Formula
arbAtomicFormula
            Formula -> Gen Formula
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Formula -> Gen Formula) -> Formula -> Gen Formula
forall a b. (a -> b) -> a -> b
$ if Bool
p then Formula
x else Formula -> Formula
forall (c :: * -> *). Pointed c => F c -> F c
(.~.) Formula
x
    , do
            T Identity
x1 <- Gen (T Identity)
forall a. Arbitrary a => Gen a
arbitrary
            T Identity
x2 <- Gen (T Identity)
forall a. Arbitrary a => Gen a
arbitrary
            Formula -> Gen Formula
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Formula -> Gen Formula) -> Formula -> Gen Formula
forall a b. (a -> b) -> a -> b
$ Identity (Formula0 (T Identity) Formula) -> Formula
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F (Identity (Formula0 (T Identity) Formula) -> Formula)
-> Identity (Formula0 (T Identity) Formula) -> Formula
forall a b. (a -> b) -> a -> b
$ Formula0 (T Identity) Formula
-> Identity (Formula0 (T Identity) Formula)
forall a. a -> Identity a
forall (p :: * -> *) a. Pointed p => a -> p a
point (Formula0 (T Identity) Formula
 -> Identity (Formula0 (T Identity) Formula))
-> Formula0 (T Identity) Formula
-> Identity (Formula0 (T Identity) Formula)
forall a b. (a -> b) -> a -> b
$ T Identity
-> InfixPred -> T Identity -> Formula0 (T Identity) Formula
forall term formula.
term -> InfixPred -> term -> Formula0 term formula
InfixPred T Identity
x1 InfixPred
(:!=:) T Identity
x2
    ]


arbAtomicFormula :: Gen Formula
arbAtomicFormula :: Gen Formula
arbAtomicFormula = (Formula0 (T Identity) Formula -> Formula)
-> Gen (Formula0 (T Identity) Formula) -> Gen Formula
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Identity (Formula0 (T Identity) Formula) -> Formula
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F (Identity (Formula0 (T Identity) Formula) -> Formula)
-> (Formula0 (T Identity) Formula
    -> Identity (Formula0 (T Identity) Formula))
-> Formula0 (T Identity) Formula
-> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula0 (T Identity) Formula
-> Identity (Formula0 (T Identity) Formula)
forall a. a -> Identity a
forall (p :: * -> *) a. Pointed p => a -> p a
point) (Gen (Formula0 (T Identity) Formula) -> Gen Formula)
-> Gen (Formula0 (T Identity) Formula) -> Gen Formula
forall a b. (a -> b) -> a -> b
$ do
    AtomicWord
x1 <- Gen AtomicWord
forall a. Arbitrary a => Gen a
arbitrary
    [T Identity]
x2 <- (Int -> Gen [T Identity]) -> Gen [T Identity]
forall a. (Int -> Gen a) -> Gen a
argsFreq Int -> Gen [T Identity]
forall a. Arbitrary a => Int -> Gen [a]
vector
    Formula0 (T Identity) Formula
-> Gen (Formula0 (T Identity) Formula)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (AtomicWord -> [T Identity] -> Formula0 (T Identity) Formula
forall term formula. AtomicWord -> [term] -> Formula0 term formula
PredApp AtomicWord
x1 [T Identity]
x2)


instance Arbitrary GTerm
    where arbitrary :: Gen GTerm
arbitrary = (Int -> Gen GTerm) -> Gen GTerm
forall a. (Int -> Gen a) -> Gen a
sized Int -> Gen GTerm
go

              where
                go :: Int -> Gen GTerm
go Int
0 = (GData -> GTerm) -> Gen GData -> Gen GTerm
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap GData -> GTerm
GTerm Gen GData
forall a. Arbitrary a => Gen a
arbitrary

                go Int
i =
                    [Gen GTerm] -> Gen GTerm
forall a. HasCallStack => [Gen a] -> Gen a
oneof [
                            do
                                  Int
ileft <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose(Int
0,Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
                                  GData
x1 <- Int -> Gen GData -> Gen GData
forall a. HasCallStack => Int -> Gen a -> Gen a
resize Int
ileft Gen GData
forall a. Arbitrary a => Gen a
arbitrary
                                  GTerm
x2 <- Int -> Gen GTerm -> Gen GTerm
forall a. HasCallStack => Int -> Gen a -> Gen a
resize (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
ileft) Gen GTerm
forall a. Arbitrary a => Gen a
arbitrary
                                  GTerm -> Gen GTerm
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (GData -> GTerm -> GTerm
ColonSep GData
x1 GTerm
x2)

                          , do
                                  GData
x1 <- Gen GData
forall a. Arbitrary a => Gen a
arbitrary
                                  GTerm -> Gen GTerm
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (GData -> GTerm
GTerm GData
x1)

                          , do
                                  [GTerm]
args <- (Int -> Gen [GTerm]) -> Gen [GTerm]
forall a. (Int -> Gen a) -> Gen a
argsFreq
                                           (\Int
nargs -> do
                                              [Int]
parti <- Int -> Int -> Gen [Int]
arbPartition Int
nargs (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
                                              (Int -> Gen GTerm) -> [Int] -> Gen [GTerm]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Int -> Gen GTerm -> Gen GTerm) -> Gen GTerm -> Int -> Gen GTerm
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Gen GTerm -> Gen GTerm
forall a. HasCallStack => Int -> Gen a -> Gen a
resize Gen GTerm
forall a. Arbitrary a => Gen a
arbitrary) [Int]
parti
                                           ) Gen [GTerm] -> ([GTerm] -> Bool) -> Gen [GTerm]
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` ([GTerm] -> [GTerm] -> Bool
forall a. Eq a => a -> a -> Bool
/= [])

                                  GTerm -> Gen GTerm
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return ([GTerm] -> GTerm
GList [GTerm]
args)
                       ]

-- | TPTP constant symbol\/predicate symbol\/function symbol identifiers (they are output in single quotes unless they are /lower_word/s).
--
-- Tip: Use the @-XOverloadedStrings@ compiler flag if you don't want to have to type /AtomicWord/ to construct an 'AtomicWord'
newtype AtomicWord = AtomicWord String
    deriving (AtomicWord -> AtomicWord -> Bool
(AtomicWord -> AtomicWord -> Bool)
-> (AtomicWord -> AtomicWord -> Bool) -> Eq AtomicWord
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AtomicWord -> AtomicWord -> Bool
== :: AtomicWord -> AtomicWord -> Bool
$c/= :: AtomicWord -> AtomicWord -> Bool
/= :: AtomicWord -> AtomicWord -> Bool
Eq,Eq AtomicWord
Eq AtomicWord =>
(AtomicWord -> AtomicWord -> Ordering)
-> (AtomicWord -> AtomicWord -> Bool)
-> (AtomicWord -> AtomicWord -> Bool)
-> (AtomicWord -> AtomicWord -> Bool)
-> (AtomicWord -> AtomicWord -> Bool)
-> (AtomicWord -> AtomicWord -> AtomicWord)
-> (AtomicWord -> AtomicWord -> AtomicWord)
-> Ord AtomicWord
AtomicWord -> AtomicWord -> Bool
AtomicWord -> AtomicWord -> Ordering
AtomicWord -> AtomicWord -> AtomicWord
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: AtomicWord -> AtomicWord -> Ordering
compare :: AtomicWord -> AtomicWord -> Ordering
$c< :: AtomicWord -> AtomicWord -> Bool
< :: AtomicWord -> AtomicWord -> Bool
$c<= :: AtomicWord -> AtomicWord -> Bool
<= :: AtomicWord -> AtomicWord -> Bool
$c> :: AtomicWord -> AtomicWord -> Bool
> :: AtomicWord -> AtomicWord -> Bool
$c>= :: AtomicWord -> AtomicWord -> Bool
>= :: AtomicWord -> AtomicWord -> Bool
$cmax :: AtomicWord -> AtomicWord -> AtomicWord
max :: AtomicWord -> AtomicWord -> AtomicWord
$cmin :: AtomicWord -> AtomicWord -> AtomicWord
min :: AtomicWord -> AtomicWord -> AtomicWord
Ord,Int -> AtomicWord -> ShowS
[AtomicWord] -> ShowS
AtomicWord -> String
(Int -> AtomicWord -> ShowS)
-> (AtomicWord -> String)
-> ([AtomicWord] -> ShowS)
-> Show AtomicWord
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AtomicWord -> ShowS
showsPrec :: Int -> AtomicWord -> ShowS
$cshow :: AtomicWord -> String
show :: AtomicWord -> String
$cshowList :: [AtomicWord] -> ShowS
showList :: [AtomicWord] -> ShowS
Show,Typeable AtomicWord
Typeable AtomicWord =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> AtomicWord -> c AtomicWord)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c AtomicWord)
-> (AtomicWord -> Constr)
-> (AtomicWord -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c AtomicWord))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c AtomicWord))
-> ((forall b. Data b => b -> b) -> AtomicWord -> AtomicWord)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> AtomicWord -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> AtomicWord -> r)
-> (forall u. (forall d. Data d => d -> u) -> AtomicWord -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> AtomicWord -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord)
-> Data AtomicWord
AtomicWord -> Constr
AtomicWord -> DataType
(forall b. Data b => b -> b) -> AtomicWord -> AtomicWord
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> AtomicWord -> u
forall u. (forall d. Data d => d -> u) -> AtomicWord -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AtomicWord -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AtomicWord -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AtomicWord
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AtomicWord -> c AtomicWord
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AtomicWord)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AtomicWord)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AtomicWord -> c AtomicWord
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AtomicWord -> c AtomicWord
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AtomicWord
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AtomicWord
$ctoConstr :: AtomicWord -> Constr
toConstr :: AtomicWord -> Constr
$cdataTypeOf :: AtomicWord -> DataType
dataTypeOf :: AtomicWord -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AtomicWord)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AtomicWord)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AtomicWord)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AtomicWord)
$cgmapT :: (forall b. Data b => b -> b) -> AtomicWord -> AtomicWord
gmapT :: (forall b. Data b => b -> b) -> AtomicWord -> AtomicWord
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AtomicWord -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AtomicWord -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AtomicWord -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AtomicWord -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> AtomicWord -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> AtomicWord -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> AtomicWord -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> AtomicWord -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord
Data,Typeable,ReadPrec [AtomicWord]
ReadPrec AtomicWord
Int -> ReadS AtomicWord
ReadS [AtomicWord]
(Int -> ReadS AtomicWord)
-> ReadS [AtomicWord]
-> ReadPrec AtomicWord
-> ReadPrec [AtomicWord]
-> Read AtomicWord
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS AtomicWord
readsPrec :: Int -> ReadS AtomicWord
$creadList :: ReadS [AtomicWord]
readList :: ReadS [AtomicWord]
$creadPrec :: ReadPrec AtomicWord
readPrec :: ReadPrec AtomicWord
$creadListPrec :: ReadPrec [AtomicWord]
readListPrec :: ReadPrec [AtomicWord]
Read,NonEmpty AtomicWord -> AtomicWord
AtomicWord -> AtomicWord -> AtomicWord
(AtomicWord -> AtomicWord -> AtomicWord)
-> (NonEmpty AtomicWord -> AtomicWord)
-> (forall b. Integral b => b -> AtomicWord -> AtomicWord)
-> Semigroup AtomicWord
forall b. Integral b => b -> AtomicWord -> AtomicWord
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
$c<> :: AtomicWord -> AtomicWord -> AtomicWord
<> :: AtomicWord -> AtomicWord -> AtomicWord
$csconcat :: NonEmpty AtomicWord -> AtomicWord
sconcat :: NonEmpty AtomicWord -> AtomicWord
$cstimes :: forall b. Integral b => b -> AtomicWord -> AtomicWord
stimes :: forall b. Integral b => b -> AtomicWord -> AtomicWord
Semigroup,Semigroup AtomicWord
AtomicWord
Semigroup AtomicWord =>
AtomicWord
-> (AtomicWord -> AtomicWord -> AtomicWord)
-> ([AtomicWord] -> AtomicWord)
-> Monoid AtomicWord
[AtomicWord] -> AtomicWord
AtomicWord -> AtomicWord -> AtomicWord
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: AtomicWord
mempty :: AtomicWord
$cmappend :: AtomicWord -> AtomicWord -> AtomicWord
mappend :: AtomicWord -> AtomicWord -> AtomicWord
$cmconcat :: [AtomicWord] -> AtomicWord
mconcat :: [AtomicWord] -> AtomicWord
Monoid,String -> AtomicWord
(String -> AtomicWord) -> IsString AtomicWord
forall a. (String -> a) -> IsString a
$cfromString :: String -> AtomicWord
fromString :: String -> AtomicWord
IsString)

instance Arbitrary AtomicWord where
    arbitrary :: Gen AtomicWord
arbitrary = [(Int, Gen AtomicWord)] -> Gen AtomicWord
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [  (Int
5, String -> AtomicWord
AtomicWord (String -> AtomicWord) -> Gen String -> Gen AtomicWord
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen String
arbLowerWord)
                            ,(Int
1, String -> AtomicWord
AtomicWord (String -> AtomicWord) -> Gen String -> Gen AtomicWord
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen String
arbPrintable)
                          ]

-- | Variable names
newtype V = V String
    deriving (V -> V -> Bool
(V -> V -> Bool) -> (V -> V -> Bool) -> Eq V
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: V -> V -> Bool
== :: V -> V -> Bool
$c/= :: V -> V -> Bool
/= :: V -> V -> Bool
Eq,Eq V
Eq V =>
(V -> V -> Ordering)
-> (V -> V -> Bool)
-> (V -> V -> Bool)
-> (V -> V -> Bool)
-> (V -> V -> Bool)
-> (V -> V -> V)
-> (V -> V -> V)
-> Ord V
V -> V -> Bool
V -> V -> Ordering
V -> V -> V
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: V -> V -> Ordering
compare :: V -> V -> Ordering
$c< :: V -> V -> Bool
< :: V -> V -> Bool
$c<= :: V -> V -> Bool
<= :: V -> V -> Bool
$c> :: V -> V -> Bool
> :: V -> V -> Bool
$c>= :: V -> V -> Bool
>= :: V -> V -> Bool
$cmax :: V -> V -> V
max :: V -> V -> V
$cmin :: V -> V -> V
min :: V -> V -> V
Ord,Int -> V -> ShowS
[V] -> ShowS
V -> String
(Int -> V -> ShowS) -> (V -> String) -> ([V] -> ShowS) -> Show V
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> V -> ShowS
showsPrec :: Int -> V -> ShowS
$cshow :: V -> String
show :: V -> String
$cshowList :: [V] -> ShowS
showList :: [V] -> ShowS
Show,Typeable V
Typeable V =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> V -> c V)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c V)
-> (V -> Constr)
-> (V -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c V))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c V))
-> ((forall b. Data b => b -> b) -> V -> V)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> V -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> V -> r)
-> (forall u. (forall d. Data d => d -> u) -> V -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> V -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> V -> m V)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> V -> m V)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> V -> m V)
-> Data V
V -> Constr
V -> DataType
(forall b. Data b => b -> b) -> V -> V
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> V -> u
forall u. (forall d. Data d => d -> u) -> V -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> V -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> V -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> V -> m V
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> V -> m V
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c V
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> V -> c V
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c V)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c V)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> V -> c V
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> V -> c V
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c V
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c V
$ctoConstr :: V -> Constr
toConstr :: V -> Constr
$cdataTypeOf :: V -> DataType
dataTypeOf :: V -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c V)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c V)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c V)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c V)
$cgmapT :: (forall b. Data b => b -> b) -> V -> V
gmapT :: (forall b. Data b => b -> b) -> V -> V
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> V -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> V -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> V -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> V -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> V -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> V -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> V -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> V -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> V -> m V
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> V -> m V
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> V -> m V
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> V -> m V
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> V -> m V
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> V -> m V
Data,Typeable,ReadPrec [V]
ReadPrec V
Int -> ReadS V
ReadS [V]
(Int -> ReadS V)
-> ReadS [V] -> ReadPrec V -> ReadPrec [V] -> Read V
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS V
readsPrec :: Int -> ReadS V
$creadList :: ReadS [V]
readList :: ReadS [V]
$creadPrec :: ReadPrec V
readPrec :: ReadPrec V
$creadListPrec :: ReadPrec [V]
readListPrec :: ReadPrec [V]
Read,NonEmpty V -> V
V -> V -> V
(V -> V -> V)
-> (NonEmpty V -> V)
-> (forall b. Integral b => b -> V -> V)
-> Semigroup V
forall b. Integral b => b -> V -> V
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
$c<> :: V -> V -> V
<> :: V -> V -> V
$csconcat :: NonEmpty V -> V
sconcat :: NonEmpty V -> V
$cstimes :: forall b. Integral b => b -> V -> V
stimes :: forall b. Integral b => b -> V -> V
Semigroup,Semigroup V
V
Semigroup V => V -> (V -> V -> V) -> ([V] -> V) -> Monoid V
[V] -> V
V -> V -> V
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: V
mempty :: V
$cmappend :: V -> V -> V
mappend :: V -> V -> V
$cmconcat :: [V] -> V
mconcat :: [V] -> V
Monoid,String -> V
(String -> V) -> IsString V
forall a. (String -> a) -> IsString a
$cfromString :: String -> V
fromString :: String -> V
IsString)

instance Arbitrary V where
    arbitrary :: Gen V
arbitrary = String -> V
V (String -> V) -> Gen String -> Gen V
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen String
arbVar

-- * Fixed-point style decorated formulae and terms

-- | 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
newtype F c = F { forall (c :: * -> *). F c -> c (Formula0 (T c) (F c))
runF :: c (Formula0 (T c) (F c)) }

-- | Terms whose subterms are wrapped in the given type constructor @c@
newtype T c = T { forall (c :: * -> *). T c -> c (Term0 (T c))
runT :: c (Term0 (T c)) }

#define DI(X) deriving instance (X (c (Term0 (T c)))) => X (T c); deriving instance (X (c (Formula0 (T c) (F c)))) => X (F c)

DI(Eq)
DI(Ord)
DI(Show)
DI(Read)

deriving instance Typeable F
deriving instance Typeable T

deriving instance (Typeable c, Data (c (Term0 (T c)))) => Data (T c)
deriving instance (Typeable c, Data (c (Formula0 (T c) (F c)))) => Data (F c)

-- * Utility functions

unwrapF ::
            (Copointed t) =>
            F t -> Formula0 (T t) (F t)
unwrapF :: forall (t :: * -> *). Copointed t => F t -> Formula0 (T t) (F t)
unwrapF (F t (Formula0 (T t) (F t))
x) = t (Formula0 (T t) (F t)) -> Formula0 (T t) (F t)
forall a. t a -> a
forall (p :: * -> *) a. Copointed p => p a -> a
copoint t (Formula0 (T t) (F t))
x
unwrapT ::
            (Copointed t) =>
            T t -> Term0 (T t)
unwrapT :: forall (t :: * -> *). Copointed t => T t -> Term0 (T t)
unwrapT (T t (Term0 (T t))
x) = t (Term0 (T t)) -> Term0 (T t)
forall a. t a -> a
forall (p :: * -> *) a. Copointed p => p a -> a
copoint t (Term0 (T t))
x

foldFormula0 ::
                  (f -> r)
                -> (Quant -> [V] -> f -> r)
                -> (f -> BinOp -> f -> r)
                -> (t -> InfixPred -> t -> r)
                -> (AtomicWord -> [t] -> r)
                -> Formula0 t f
                -> r
foldFormula0 :: forall f r t.
(f -> r)
-> (Quant -> [V] -> f -> r)
-> (f -> BinOp -> f -> r)
-> (t -> InfixPred -> t -> r)
-> (AtomicWord -> [t] -> r)
-> Formula0 t f
-> r
foldFormula0 f -> r
kneg Quant -> [V] -> f -> r
kquant f -> BinOp -> f -> r
kbinop t -> InfixPred -> t -> r
kinfix AtomicWord -> [t] -> r
kpredapp Formula0 t f
f =
    case Formula0 t f
f of
      (:~:) f
x -> f -> r
kneg f
x
      Quant Quant
x [V]
y f
z -> Quant -> [V] -> f -> r
kquant Quant
x [V]
y f
z
      BinOp f
x BinOp
y f
z -> f -> BinOp -> f -> r
kbinop f
x BinOp
y f
z
      InfixPred t
x InfixPred
y t
z -> t -> InfixPred -> t -> r
kinfix t
x InfixPred
y t
z
      PredApp AtomicWord
x [t]
y -> AtomicWord -> [t] -> r
kpredapp AtomicWord
x [t]
y

foldTerm0 ::
               (String -> r)
             -> (Rational -> r)
             -> (V -> r)
             -> (AtomicWord -> [t] -> r)
             -> Term0 t
             -> r
foldTerm0 :: forall r t.
(String -> r)
-> (Rational -> r)
-> (V -> r)
-> (AtomicWord -> [t] -> r)
-> Term0 t
-> r
foldTerm0 String -> r
kdistinct Rational -> r
knum V -> r
kvar AtomicWord -> [t] -> r
kfunapp Term0 t
t =
    case Term0 t
t of
      DistinctObjectTerm String
x -> String -> r
kdistinct String
x
      NumberLitTerm Rational
x -> Rational -> r
knum Rational
x
      Var V
x -> V -> r
kvar V
x
      FunApp AtomicWord
x [t]
y -> AtomicWord -> [t] -> r
kfunapp AtomicWord
x [t]
y


-- | Eliminate formulae
foldF ::
         (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

foldF :: forall (t :: * -> *) r.
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
foldF F t -> r
kneg Quant -> [V] -> F t -> r
kquant F t -> BinOp -> F t -> r
kbinop T t -> InfixPred -> T t -> r
kinfix AtomicWord -> [T t] -> r
kpredapp F t
f = (F t -> r)
-> (Quant -> [V] -> F t -> r)
-> (F t -> BinOp -> F t -> r)
-> (T t -> InfixPred -> T t -> r)
-> (AtomicWord -> [T t] -> r)
-> Formula0 (T t) (F t)
-> r
forall f r t.
(f -> r)
-> (Quant -> [V] -> f -> r)
-> (f -> BinOp -> f -> r)
-> (t -> InfixPred -> t -> r)
-> (AtomicWord -> [t] -> r)
-> Formula0 t f
-> r
foldFormula0 F t -> r
kneg Quant -> [V] -> F t -> r
kquant F t -> BinOp -> F t -> r
kbinop T t -> InfixPred -> T t -> r
kinfix AtomicWord -> [T t] -> r
kpredapp (F t -> Formula0 (T t) (F t)
forall (t :: * -> *). Copointed t => F t -> Formula0 (T t) (F t)
unwrapF F t
f)

-- | Eliminate terms
foldT ::
         (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
foldT :: forall (t :: * -> *) r.
Copointed t =>
(String -> r)
-> (Rational -> r)
-> (V -> r)
-> (AtomicWord -> [T t] -> r)
-> T t
-> r
foldT String -> r
kdistinct Rational -> r
knum V -> r
kvar AtomicWord -> [T t] -> r
kfunapp T t
t = (String -> r)
-> (Rational -> r)
-> (V -> r)
-> (AtomicWord -> [T t] -> r)
-> Term0 (T t)
-> r
forall r t.
(String -> r)
-> (Rational -> r)
-> (V -> r)
-> (AtomicWord -> [t] -> r)
-> Term0 t
-> r
foldTerm0 String -> r
kdistinct Rational -> r
knum V -> r
kvar AtomicWord -> [T t] -> r
kfunapp (T t -> Term0 (T t)
forall (t :: * -> *). Copointed t => T t -> Term0 (T t)
unwrapT T t
t)