-- | 'IsQuantified' is a subclass of 'IsPropositional' of formula
-- types that support existential and universal quantification.

{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE UndecidableInstances #-}

module Data.Logic.ATP.Quantified
    ( Quant((:!:), (:?:))
    , IsQuantified(VarOf, quant, foldQuantified)
    , for_all, (∀)
    , exists, (∃)
    , precedenceQuantified
    , associativityQuantified
    , prettyQuantified
    , showQuantified
    , zipQuantified
    , convertQuantified
    , onatomsQuantified
    , overatomsQuantified
    -- * Concrete instance of a quantified formula type
    , QFormula(F, T, Atom, Not, And, Or, Imp, Iff, Forall, Exists)
    ) where

import Data.Data (Data)
import Data.Logic.ATP.Apply (HasApply(TermOf))
import Data.Logic.ATP.Formulas (fromBool, IsAtom, IsFormula(..), onatoms, prettyBool)
import Data.Logic.ATP.Lit ((.~.), IsLiteral(foldLiteral'), IsLiteral(..))
import Data.Logic.ATP.Pretty as Pretty
    ((<>), Associativity(InfixN, InfixR, InfixA), Doc, HasFixity(precedence, associativity),
     Precedence, Side(Top, LHS, RHS, Unary), testParen, text,
     andPrec, orPrec, impPrec, iffPrec, notPrec, leafPrec, quantPrec)
import Data.Logic.ATP.Prop (BinOp(..), binop, IsPropositional((.&.), (.|.), (.=>.), (.<=>.), foldPropositional', foldCombination))
import Data.Logic.ATP.Term (IsTerm(TVarOf), IsVariable)
import Data.Typeable (Typeable)
import Prelude hiding (pred)
import Text.PrettyPrint (fsep)
import Text.PrettyPrint.HughesPJClass (maybeParens, Pretty(pPrint, pPrintPrec), PrettyLevel, prettyNormal)

-------------------------
-- QUANTIFIED FORMULAS --
-------------------------

-- | The two types of quantification
data Quant
    = (:!:) -- ^ for_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, 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 -> 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)

-- | Class of quantified formulas.
class (IsPropositional formula, IsVariable (VarOf formula)) => IsQuantified formula where
    type (VarOf formula) -- A type function mapping formula to the associated variable
    quant :: Quant -> VarOf formula -> formula -> formula
    foldQuantified :: (Quant -> VarOf formula -> formula -> r)
                   -> (formula -> BinOp -> formula-> r)
                   -> (formula -> r)
                   -> (Bool -> r)
                   -> (AtomOf formula -> r)
                   -> formula -> r

for_all :: IsQuantified formula => VarOf formula -> formula -> formula
for_all :: forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all = Quant -> VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
Quant -> VarOf formula -> formula -> formula
quant Quant
(:!:)
exists :: IsQuantified formula => VarOf formula -> formula -> formula
exists :: forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists = Quant -> VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
Quant -> VarOf formula -> formula -> formula
quant Quant
(:?:)

-- | ∀ can't be a function when -XUnicodeSyntax is enabled.
(∀) :: IsQuantified formula => VarOf formula -> formula -> formula
infixr 1 ∀
∀ :: forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∀) = VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all
(∃) :: IsQuantified formula => VarOf formula -> formula -> formula
infixr 1 ∃
∃ :: forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
(∃) = VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists

precedenceQuantified :: forall formula. IsQuantified formula => formula -> Precedence
precedenceQuantified :: forall formula. IsQuantified formula => formula -> Precedence
precedenceQuantified = (Quant -> VarOf formula -> formula -> a)
-> (formula -> BinOp -> formula -> a)
-> (formula -> a)
-> (Bool -> a)
-> (AtomOf formula -> a)
-> formula
-> a
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified Quant -> VarOf formula -> formula -> a
forall {a} {p} {p} {p}. Num a => p -> p -> p -> a
qu formula -> BinOp -> formula -> a
forall {a} {p} {p}. Num a => p -> BinOp -> p -> a
co formula -> a
forall {a} {p}. Num a => p -> a
ne Bool -> a
forall {a} {p}. Num a => p -> a
tf AtomOf formula -> a
at
    where
      qu :: p -> p -> p -> a
qu p
_ p
_ p
_ = a
Precedence
quantPrec
      co :: p -> BinOp -> p -> a
co p
_ BinOp
(:&:) p
_ = a
Precedence
andPrec
      co p
_ BinOp
(:|:) p
_ = a
Precedence
orPrec
      co p
_ BinOp
(:=>:) p
_ = a
Precedence
impPrec
      co p
_ BinOp
(:<=>:) p
_ = a
Precedence
iffPrec
      ne :: p -> a
ne p
_ = a
Precedence
notPrec
      tf :: p -> a
tf p
_ = a
Precedence
leafPrec
      at :: AtomOf formula -> a
at = (AtomOf formula -> a
AtomOf formula -> Precedence
forall {a}. Num a => AtomOf formula -> a
forall x. HasFixity x => x -> Precedence
precedence :: Num a => AtomOf formula -> a)

associativityQuantified :: forall formula. IsQuantified formula => formula -> Associativity
associativityQuantified :: forall formula. IsQuantified formula => formula -> Associativity
associativityQuantified = (Quant -> VarOf formula -> formula -> Associativity)
-> (formula -> BinOp -> formula -> Associativity)
-> (formula -> Associativity)
-> (Bool -> Associativity)
-> (AtomOf formula -> Associativity)
-> formula
-> Associativity
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified Quant -> VarOf formula -> formula -> Associativity
forall {p} {p} {p}. p -> p -> p -> Associativity
qu formula -> BinOp -> formula -> Associativity
forall {p} {p}. p -> BinOp -> p -> Associativity
co formula -> Associativity
forall {p}. p -> Associativity
ne Bool -> Associativity
forall {p}. p -> Associativity
tf AtomOf formula -> Associativity
at
    where
      qu :: p -> p -> p -> Associativity
qu p
_ p
_ p
_ = Associativity
Pretty.InfixR
      ne :: p -> Associativity
ne p
_ = Associativity
Pretty.InfixA
      co :: p -> BinOp -> p -> Associativity
co p
_ BinOp
(:&:) p
_ = Associativity
Pretty.InfixA
      co p
_ BinOp
(:|:) p
_ = Associativity
Pretty.InfixA
      co p
_ BinOp
(:=>:) p
_ = Associativity
Pretty.InfixR
      co p
_ BinOp
(:<=>:) p
_ = Associativity
Pretty.InfixA
      tf :: p -> Associativity
tf p
_ = Associativity
Pretty.InfixN
      at :: AtomOf formula -> Associativity
at = AtomOf formula -> Associativity
forall x. HasFixity x => x -> Associativity
associativity

-- | Implementation of 'Pretty' for 'IsQuantified' types.
prettyQuantified :: forall fof v. (IsQuantified fof, v ~ VarOf fof) =>
                    Side -> PrettyLevel -> Rational -> fof -> Doc
prettyQuantified :: forall fof v.
(IsQuantified fof, v ~ VarOf fof) =>
Side -> PrettyLevel -> Rational -> fof -> Doc
prettyQuantified Side
side PrettyLevel
l Rational
r fof
fm =
    Bool -> Doc -> Doc
maybeParens (PrettyLevel
l PrettyLevel -> PrettyLevel -> Bool
forall a. Ord a => a -> a -> Bool
> PrettyLevel
prettyNormal Bool -> Bool -> Bool
|| Side -> Rational -> Rational -> Associativity -> Bool
forall a.
(Eq a, Ord a, Num a) =>
Side -> a -> a -> Associativity -> Bool
testParen Side
side Rational
r (fof -> Precedence
forall x. HasFixity x => x -> Precedence
precedence fof
fm) (fof -> Associativity
forall x. HasFixity x => x -> Associativity
associativity fof
fm)) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (Quant -> VarOf fof -> fof -> Doc)
-> (fof -> BinOp -> fof -> Doc)
-> (fof -> Doc)
-> (Bool -> Doc)
-> (AtomOf fof -> Doc)
-> fof
-> Doc
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf fof -> fof -> r)
-> (fof -> BinOp -> fof -> r)
-> (fof -> r)
-> (Bool -> r)
-> (AtomOf fof -> r)
-> fof
-> r
foldQuantified (\Quant
op VarOf fof
v fof
p -> Quant -> [v] -> fof -> Doc
qu Quant
op [v
VarOf fof
v] fof
p) fof -> BinOp -> fof -> Doc
co fof -> Doc
ne Bool -> Doc
tf AtomOf fof -> Doc
at fof
fm
    -- maybeParens (r > precedence fm) $ foldQuantified (\op v p -> qu op [v] p) co ne tf at fm
    where
      -- Collect similarly quantified variables
      qu :: Quant -> [v] -> fof -> Doc
      qu :: Quant -> [v] -> fof -> Doc
qu Quant
op [v]
vs fof
p' = (Quant -> VarOf fof -> fof -> Doc)
-> (fof -> BinOp -> fof -> Doc)
-> (fof -> Doc)
-> (Bool -> Doc)
-> (AtomOf fof -> Doc)
-> fof
-> Doc
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf fof -> fof -> r)
-> (fof -> BinOp -> fof -> r)
-> (fof -> r)
-> (Bool -> r)
-> (AtomOf fof -> r)
-> fof
-> r
foldQuantified (Quant -> [v] -> fof -> Quant -> v -> fof -> Doc
qu' Quant
op [v]
vs fof
p') (\fof
_ BinOp
_ fof
_ -> Quant -> [v] -> fof -> Doc
qu'' Quant
op [v]
vs fof
p') (\fof
_ -> Quant -> [v] -> fof -> Doc
qu'' Quant
op [v]
vs fof
p')
                                                      (\Bool
_ -> Quant -> [v] -> fof -> Doc
qu'' Quant
op [v]
vs fof
p') (\AtomOf fof
_ -> Quant -> [v] -> fof -> Doc
qu'' Quant
op [v]
vs fof
p') fof
p'
      qu' :: Quant -> [v] -> fof -> Quant -> v -> fof -> Doc
      qu' :: Quant -> [v] -> fof -> Quant -> v -> fof -> Doc
qu' Quant
op [v]
vs fof
_ Quant
op' v
v fof
p' | Quant
op Quant -> Quant -> Bool
forall a. Eq a => a -> a -> Bool
== Quant
op' = Quant -> [v] -> fof -> Doc
qu Quant
op (v
v v -> [v] -> [v]
forall a. a -> [a] -> [a]
: [v]
vs) fof
p'
      qu' Quant
op [v]
vs fof
p Quant
_ v
_ fof
_ = Quant -> [v] -> fof -> Doc
qu'' Quant
op [v]
vs fof
p
      qu'' :: Quant -> [v] -> fof -> Doc
      qu'' :: Quant -> [v] -> fof -> Doc
qu'' Quant
_op [] fof
p = Side -> PrettyLevel -> Rational -> fof -> Doc
forall fof v.
(IsQuantified fof, v ~ VarOf fof) =>
Side -> PrettyLevel -> Rational -> fof -> Doc
prettyQuantified Side
Unary PrettyLevel
l Rational
r fof
p
      qu'' Quant
op [v]
vs fof
p = String -> Doc
text (case Quant
op of Quant
(:!:) -> String
"∀"; Quant
(:?:) -> String
"∃") Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>
                     [Doc] -> Doc
fsep ((v -> Doc) -> [v] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map v -> Doc
forall a. Pretty a => a -> Doc
pPrint ([v] -> [v]
forall a. [a] -> [a]
reverse [v]
vs)) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>
                     String -> Doc
text String
". " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Side -> PrettyLevel -> Rational -> fof -> Doc
forall fof v.
(IsQuantified fof, v ~ VarOf fof) =>
Side -> PrettyLevel -> Rational -> fof -> Doc
prettyQuantified Side
Unary PrettyLevel
l (fof -> Precedence
forall x. HasFixity x => x -> Precedence
precedence fof
fm Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ Rational
1) fof
p
      co :: fof -> BinOp -> fof -> Doc
      co :: fof -> BinOp -> fof -> Doc
co fof
p BinOp
(:&:) fof
q = Side -> PrettyLevel -> Rational -> fof -> Doc
forall fof v.
(IsQuantified fof, v ~ VarOf fof) =>
Side -> PrettyLevel -> Rational -> fof -> Doc
prettyQuantified Side
LHS PrettyLevel
l (fof -> Precedence
forall x. HasFixity x => x -> Precedence
precedence fof
fm) fof
p Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
"∧" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>  Side -> PrettyLevel -> Rational -> fof -> Doc
forall fof v.
(IsQuantified fof, v ~ VarOf fof) =>
Side -> PrettyLevel -> Rational -> fof -> Doc
prettyQuantified Side
RHS PrettyLevel
l (fof -> Precedence
forall x. HasFixity x => x -> Precedence
precedence fof
fm) fof
q
      co fof
p BinOp
(:|:) fof
q = Side -> PrettyLevel -> Rational -> fof -> Doc
forall fof v.
(IsQuantified fof, v ~ VarOf fof) =>
Side -> PrettyLevel -> Rational -> fof -> Doc
prettyQuantified Side
LHS PrettyLevel
l (fof -> Precedence
forall x. HasFixity x => x -> Precedence
precedence fof
fm) fof
p Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
"∨" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Side -> PrettyLevel -> Rational -> fof -> Doc
forall fof v.
(IsQuantified fof, v ~ VarOf fof) =>
Side -> PrettyLevel -> Rational -> fof -> Doc
prettyQuantified Side
RHS PrettyLevel
l (fof -> Precedence
forall x. HasFixity x => x -> Precedence
precedence fof
fm) fof
q
      co fof
p BinOp
(:=>:) fof
q = Side -> PrettyLevel -> Rational -> fof -> Doc
forall fof v.
(IsQuantified fof, v ~ VarOf fof) =>
Side -> PrettyLevel -> Rational -> fof -> Doc
prettyQuantified Side
LHS PrettyLevel
l (fof -> Precedence
forall x. HasFixity x => x -> Precedence
precedence fof
fm) fof
p Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
"⇒" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Side -> PrettyLevel -> Rational -> fof -> Doc
forall fof v.
(IsQuantified fof, v ~ VarOf fof) =>
Side -> PrettyLevel -> Rational -> fof -> Doc
prettyQuantified Side
RHS PrettyLevel
l (fof -> Precedence
forall x. HasFixity x => x -> Precedence
precedence fof
fm) fof
q
      co fof
p BinOp
(:<=>:) fof
q = Side -> PrettyLevel -> Rational -> fof -> Doc
forall fof v.
(IsQuantified fof, v ~ VarOf fof) =>
Side -> PrettyLevel -> Rational -> fof -> Doc
prettyQuantified Side
LHS PrettyLevel
l (fof -> Precedence
forall x. HasFixity x => x -> Precedence
precedence fof
fm) fof
p Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
"⇔" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Side -> PrettyLevel -> Rational -> fof -> Doc
forall fof v.
(IsQuantified fof, v ~ VarOf fof) =>
Side -> PrettyLevel -> Rational -> fof -> Doc
prettyQuantified Side
RHS PrettyLevel
l (fof -> Precedence
forall x. HasFixity x => x -> Precedence
precedence fof
fm) fof
q
      ne :: fof -> Doc
ne fof
p = String -> Doc
text String
"¬" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Side -> PrettyLevel -> Rational -> fof -> Doc
forall fof v.
(IsQuantified fof, v ~ VarOf fof) =>
Side -> PrettyLevel -> Rational -> fof -> Doc
prettyQuantified Side
Unary PrettyLevel
l (fof -> Precedence
forall x. HasFixity x => x -> Precedence
precedence fof
fm) fof
p
      tf :: Bool -> Doc
tf Bool
x = Bool -> Doc
prettyBool Bool
x
      at :: AtomOf fof -> Doc
at AtomOf fof
x = PrettyLevel -> Rational -> AtomOf fof -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
l Rational
r AtomOf fof
x -- maybeParens (d > PrettyLevel atomPrec) $ pPrint x

-- | Implementation of 'showsPrec' for 'IsQuantified' types.
showQuantified :: IsQuantified formula => Side -> Int -> formula -> ShowS
showQuantified :: forall formula.
IsQuantified formula =>
Side -> Int -> formula -> ShowS
showQuantified Side
side Int
r formula
fm =
    Bool -> ShowS -> ShowS
showParen (Side -> Int -> Int -> Associativity -> Bool
forall a.
(Eq a, Ord a, Num a) =>
Side -> a -> a -> Associativity -> Bool
testParen Side
side Int
r (formula -> Precedence
forall x. HasFixity x => x -> Precedence
precedence formula
fm) (formula -> Associativity
forall x. HasFixity x => x -> Associativity
associativity formula
fm)) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ (Quant -> VarOf formula -> formula -> ShowS)
-> (formula -> BinOp -> formula -> ShowS)
-> (formula -> ShowS)
-> (Bool -> ShowS)
-> (AtomOf formula -> ShowS)
-> formula
-> ShowS
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified Quant -> VarOf formula -> formula -> ShowS
qu formula -> BinOp -> formula -> ShowS
co formula -> ShowS
ne Bool -> ShowS
tf AtomOf formula -> ShowS
at formula
fm
    where
      qu :: Quant -> VarOf formula -> formula -> ShowS
qu Quant
(:!:) VarOf formula
x formula
p = String -> ShowS
showString String
"for_all " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString (VarOf formula -> String
forall a. Show a => a -> String
show VarOf formula
x) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Side -> Int -> formula -> ShowS
forall formula.
IsQuantified formula =>
Side -> Int -> formula -> ShowS
showQuantified Side
Unary (formula -> Precedence
forall x. HasFixity x => x -> Precedence
precedence formula
fm Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) formula
p
      qu Quant
(:?:) VarOf formula
x formula
p = String -> ShowS
showString String
"exists " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString (VarOf formula -> String
forall a. Show a => a -> String
show VarOf formula
x) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Side -> Int -> formula -> ShowS
forall formula.
IsQuantified formula =>
Side -> Int -> formula -> ShowS
showQuantified Side
Unary (formula -> Precedence
forall x. HasFixity x => x -> Precedence
precedence formula
fm Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) formula
p
      co :: formula -> BinOp -> formula -> ShowS
co formula
p BinOp
(:&:) formula
q = Side -> Int -> formula -> ShowS
forall formula.
IsQuantified formula =>
Side -> Int -> formula -> ShowS
showQuantified Side
LHS (formula -> Precedence
forall x. HasFixity x => x -> Precedence
precedence formula
fm) formula
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" .&. " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Side -> Int -> formula -> ShowS
forall formula.
IsQuantified formula =>
Side -> Int -> formula -> ShowS
showQuantified Side
RHS (formula -> Precedence
forall x. HasFixity x => x -> Precedence
precedence formula
fm) formula
q
      co formula
p BinOp
(:|:) formula
q = Side -> Int -> formula -> ShowS
forall formula.
IsQuantified formula =>
Side -> Int -> formula -> ShowS
showQuantified Side
LHS (formula -> Precedence
forall x. HasFixity x => x -> Precedence
precedence formula
fm) formula
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" .|. " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Side -> Int -> formula -> ShowS
forall formula.
IsQuantified formula =>
Side -> Int -> formula -> ShowS
showQuantified Side
RHS (formula -> Precedence
forall x. HasFixity x => x -> Precedence
precedence formula
fm) formula
q
      co formula
p BinOp
(:=>:) formula
q = Side -> Int -> formula -> ShowS
forall formula.
IsQuantified formula =>
Side -> Int -> formula -> ShowS
showQuantified Side
LHS (formula -> Precedence
forall x. HasFixity x => x -> Precedence
precedence formula
fm) formula
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" .=>. " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Side -> Int -> formula -> ShowS
forall formula.
IsQuantified formula =>
Side -> Int -> formula -> ShowS
showQuantified Side
RHS (formula -> Precedence
forall x. HasFixity x => x -> Precedence
precedence formula
fm) formula
q
      co formula
p BinOp
(:<=>:) formula
q = Side -> Int -> formula -> ShowS
forall formula.
IsQuantified formula =>
Side -> Int -> formula -> ShowS
showQuantified Side
LHS (formula -> Precedence
forall x. HasFixity x => x -> Precedence
precedence formula
fm) formula
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" .<=>. " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Side -> Int -> formula -> ShowS
forall formula.
IsQuantified formula =>
Side -> Int -> formula -> ShowS
showQuantified Side
RHS (formula -> Precedence
forall x. HasFixity x => x -> Precedence
precedence formula
fm) formula
q
      ne :: formula -> ShowS
ne formula
p = String -> ShowS
showString String
"(.~.) " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Side -> Int -> formula -> ShowS
forall formula.
IsQuantified formula =>
Side -> Int -> formula -> ShowS
showQuantified Side
Unary (Int -> Int
forall a. Enum a => a -> a
succ (formula -> Precedence
forall x. HasFixity x => x -> Precedence
precedence formula
fm)) formula
p
      tf :: Bool -> ShowS
tf Bool
x = Int -> Bool -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (formula -> Precedence
forall x. HasFixity x => x -> Precedence
precedence formula
fm) Bool
x
      at :: AtomOf formula -> ShowS
at AtomOf formula
x = Int -> AtomOf formula -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (formula -> Precedence
forall x. HasFixity x => x -> Precedence
precedence formula
fm) AtomOf formula
x

-- | Combine two formulas if they are similar.
zipQuantified :: IsQuantified formula =>
                 (Quant -> VarOf formula -> formula -> Quant -> VarOf formula -> formula -> Maybe r)
              -> (formula -> BinOp -> formula -> formula -> BinOp -> formula -> Maybe r)
              -> (formula -> formula -> Maybe r)
              -> (Bool -> Bool -> Maybe r)
              -> ((AtomOf formula) -> (AtomOf formula) -> Maybe r)
              -> formula -> formula -> Maybe r
zipQuantified :: forall formula r.
IsQuantified formula =>
(Quant
 -> VarOf formula
 -> formula
 -> Quant
 -> VarOf formula
 -> formula
 -> Maybe r)
-> (formula
    -> BinOp -> formula -> formula -> BinOp -> formula -> Maybe r)
-> (formula -> formula -> Maybe r)
-> (Bool -> Bool -> Maybe r)
-> (AtomOf formula -> AtomOf formula -> Maybe r)
-> formula
-> formula
-> Maybe r
zipQuantified Quant
-> VarOf formula
-> formula
-> Quant
-> VarOf formula
-> formula
-> Maybe r
qu formula
-> BinOp -> formula -> formula -> BinOp -> formula -> Maybe r
co formula -> formula -> Maybe r
ne Bool -> Bool -> Maybe r
tf AtomOf formula -> AtomOf formula -> Maybe r
at formula
fm1 formula
fm2 =
    (Quant -> VarOf formula -> formula -> Maybe r)
-> (formula -> BinOp -> formula -> Maybe r)
-> (formula -> Maybe r)
-> (Bool -> Maybe r)
-> (AtomOf formula -> Maybe r)
-> formula
-> Maybe r
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified Quant -> VarOf formula -> formula -> Maybe r
qu' formula -> BinOp -> formula -> Maybe r
co' formula -> Maybe r
ne' Bool -> Maybe r
tf' AtomOf formula -> Maybe r
at' formula
fm1
    where
      qu' :: Quant -> VarOf formula -> formula -> Maybe r
qu' Quant
op1 VarOf formula
v1 formula
p1 = (Quant -> VarOf formula -> formula -> Maybe r)
-> (formula -> BinOp -> formula -> Maybe r)
-> (formula -> Maybe r)
-> (Bool -> Maybe r)
-> (AtomOf formula -> Maybe r)
-> formula
-> Maybe r
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified (Quant
-> VarOf formula
-> formula
-> Quant
-> VarOf formula
-> formula
-> Maybe r
qu Quant
op1 VarOf formula
v1 formula
p1)       (\ formula
_ BinOp
_ formula
_ -> Maybe r
forall a. Maybe a
Nothing) (\ formula
_ -> Maybe r
forall a. Maybe a
Nothing) (\ Bool
_ -> Maybe r
forall a. Maybe a
Nothing) (\ AtomOf formula
_ -> Maybe r
forall a. Maybe a
Nothing) formula
fm2
      co' :: formula -> BinOp -> formula -> Maybe r
co' formula
l1 BinOp
op1 formula
r1 = (Quant -> VarOf formula -> formula -> Maybe r)
-> (formula -> BinOp -> formula -> Maybe r)
-> (formula -> Maybe r)
-> (Bool -> Maybe r)
-> (AtomOf formula -> Maybe r)
-> formula
-> Maybe r
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified (\ Quant
_ VarOf formula
_ formula
_ -> Maybe r
forall a. Maybe a
Nothing) (formula
-> BinOp -> formula -> formula -> BinOp -> formula -> Maybe r
co formula
l1 BinOp
op1 formula
r1)       (\ formula
_ -> Maybe r
forall a. Maybe a
Nothing) (\ Bool
_ -> Maybe r
forall a. Maybe a
Nothing) (\ AtomOf formula
_ -> Maybe r
forall a. Maybe a
Nothing) formula
fm2
      ne' :: formula -> Maybe r
ne' formula
x1 =        (Quant -> VarOf formula -> formula -> Maybe r)
-> (formula -> BinOp -> formula -> Maybe r)
-> (formula -> Maybe r)
-> (Bool -> Maybe r)
-> (AtomOf formula -> Maybe r)
-> formula
-> Maybe r
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified (\ Quant
_ VarOf formula
_ formula
_ -> Maybe r
forall a. Maybe a
Nothing) (\ formula
_ BinOp
_ formula
_ -> Maybe r
forall a. Maybe a
Nothing) (formula -> formula -> Maybe r
ne formula
x1)          (\ Bool
_ -> Maybe r
forall a. Maybe a
Nothing) (\ AtomOf formula
_ -> Maybe r
forall a. Maybe a
Nothing) formula
fm2
      tf' :: Bool -> Maybe r
tf' Bool
x1 =        (Quant -> VarOf formula -> formula -> Maybe r)
-> (formula -> BinOp -> formula -> Maybe r)
-> (formula -> Maybe r)
-> (Bool -> Maybe r)
-> (AtomOf formula -> Maybe r)
-> formula
-> Maybe r
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified (\ Quant
_ VarOf formula
_ formula
_ -> Maybe r
forall a. Maybe a
Nothing) (\ formula
_ BinOp
_ formula
_ -> Maybe r
forall a. Maybe a
Nothing) (\ formula
_ -> Maybe r
forall a. Maybe a
Nothing) (Bool -> Bool -> Maybe r
tf Bool
x1)          (\ AtomOf formula
_ -> Maybe r
forall a. Maybe a
Nothing) formula
fm2
      at' :: AtomOf formula -> Maybe r
at' AtomOf formula
atom1 =     (Quant -> VarOf formula -> formula -> Maybe r)
-> (formula -> BinOp -> formula -> Maybe r)
-> (formula -> Maybe r)
-> (Bool -> Maybe r)
-> (AtomOf formula -> Maybe r)
-> formula
-> Maybe r
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified (\ Quant
_ VarOf formula
_ formula
_ -> Maybe r
forall a. Maybe a
Nothing) (\ formula
_ BinOp
_ formula
_ -> Maybe r
forall a. Maybe a
Nothing) (\ formula
_ -> Maybe r
forall a. Maybe a
Nothing) (\ Bool
_ -> Maybe r
forall a. Maybe a
Nothing) (AtomOf formula -> AtomOf formula -> Maybe r
at AtomOf formula
atom1)       formula
fm2

-- | Convert any instance of IsQuantified to any other by
-- specifying the result type.
convertQuantified :: forall f1 f2.
                     (IsQuantified f1, IsQuantified f2) =>
                     (AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
convertQuantified :: forall f1 f2.
(IsQuantified f1, IsQuantified f2) =>
(AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
convertQuantified AtomOf f1 -> AtomOf f2
ca VarOf f1 -> VarOf f2
cv f1
f1 =
    (Quant -> VarOf f1 -> f1 -> f2)
-> (f1 -> BinOp -> f1 -> f2)
-> (f1 -> f2)
-> (Bool -> f2)
-> (AtomOf f1 -> f2)
-> f1
-> f2
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf f1 -> f1 -> r)
-> (f1 -> BinOp -> f1 -> r)
-> (f1 -> r)
-> (Bool -> r)
-> (AtomOf f1 -> r)
-> f1
-> r
foldQuantified Quant -> VarOf f1 -> f1 -> f2
qu f1 -> BinOp -> f1 -> f2
co f1 -> f2
ne Bool -> f2
tf AtomOf f1 -> f2
at f1
f1
    where
      qu :: Quant -> VarOf f1 -> f1 -> f2
      qu :: Quant -> VarOf f1 -> f1 -> f2
qu Quant
(:!:) VarOf f1
x f1
p = VarOf f2 -> f2 -> f2
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all (VarOf f1 -> VarOf f2
cv VarOf f1
x :: VarOf f2) ((AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
forall f1 f2.
(IsQuantified f1, IsQuantified f2) =>
(AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
convertQuantified AtomOf f1 -> AtomOf f2
ca VarOf f1 -> VarOf f2
cv f1
p :: f2)
      qu Quant
(:?:) VarOf f1
x f1
p = VarOf f2 -> f2 -> f2
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists (VarOf f1 -> VarOf f2
cv VarOf f1
x :: VarOf f2) ((AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
forall f1 f2.
(IsQuantified f1, IsQuantified f2) =>
(AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
convertQuantified AtomOf f1 -> AtomOf f2
ca VarOf f1 -> VarOf f2
cv f1
p :: f2)
      co :: f1 -> BinOp -> f1 -> f2
co f1
p BinOp
(:&:) f1
q = (AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
forall f1 f2.
(IsQuantified f1, IsQuantified f2) =>
(AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
convertQuantified AtomOf f1 -> AtomOf f2
ca VarOf f1 -> VarOf f2
cv f1
p f2 -> f2 -> f2
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
forall f1 f2.
(IsQuantified f1, IsQuantified f2) =>
(AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
convertQuantified AtomOf f1 -> AtomOf f2
ca VarOf f1 -> VarOf f2
cv f1
q
      co f1
p BinOp
(:|:) f1
q = (AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
forall f1 f2.
(IsQuantified f1, IsQuantified f2) =>
(AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
convertQuantified AtomOf f1 -> AtomOf f2
ca VarOf f1 -> VarOf f2
cv f1
p f2 -> f2 -> f2
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
forall f1 f2.
(IsQuantified f1, IsQuantified f2) =>
(AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
convertQuantified AtomOf f1 -> AtomOf f2
ca VarOf f1 -> VarOf f2
cv f1
q
      co f1
p BinOp
(:=>:) f1
q = (AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
forall f1 f2.
(IsQuantified f1, IsQuantified f2) =>
(AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
convertQuantified AtomOf f1 -> AtomOf f2
ca VarOf f1 -> VarOf f2
cv f1
p f2 -> f2 -> f2
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
forall f1 f2.
(IsQuantified f1, IsQuantified f2) =>
(AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
convertQuantified AtomOf f1 -> AtomOf f2
ca VarOf f1 -> VarOf f2
cv f1
q
      co f1
p BinOp
(:<=>:) f1
q = (AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
forall f1 f2.
(IsQuantified f1, IsQuantified f2) =>
(AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
convertQuantified AtomOf f1 -> AtomOf f2
ca VarOf f1 -> VarOf f2
cv f1
p f2 -> f2 -> f2
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
forall f1 f2.
(IsQuantified f1, IsQuantified f2) =>
(AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
convertQuantified AtomOf f1 -> AtomOf f2
ca VarOf f1 -> VarOf f2
cv f1
q
      ne :: f1 -> f2
ne f1
p = f2 -> f2
forall formula. IsLiteral formula => formula -> formula
(.~.) ((AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
forall f1 f2.
(IsQuantified f1, IsQuantified f2) =>
(AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
convertQuantified AtomOf f1 -> AtomOf f2
ca VarOf f1 -> VarOf f2
cv f1
p)
      tf :: Bool -> f2
      tf :: Bool -> f2
tf = Bool -> f2
forall formula. IsFormula formula => Bool -> formula
fromBool
      at :: AtomOf f1 -> f2
      at :: AtomOf f1 -> f2
at = AtomOf f2 -> f2
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (AtomOf f2 -> f2) -> (AtomOf f1 -> AtomOf f2) -> AtomOf f1 -> f2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AtomOf f1 -> AtomOf f2
ca

onatomsQuantified :: IsQuantified formula => (AtomOf formula -> AtomOf formula) -> formula -> formula
onatomsQuantified :: forall formula.
IsQuantified formula =>
(AtomOf formula -> AtomOf formula) -> formula -> formula
onatomsQuantified AtomOf formula -> AtomOf formula
f formula
fm =
    (Quant -> VarOf formula -> formula -> formula)
-> (formula -> BinOp -> formula -> formula)
-> (formula -> formula)
-> (Bool -> formula)
-> (AtomOf formula -> formula)
-> formula
-> formula
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified Quant -> VarOf formula -> formula -> formula
qu formula -> BinOp -> formula -> formula
co formula -> formula
ne Bool -> formula
forall formula. IsFormula formula => Bool -> formula
tf AtomOf formula -> formula
at formula
fm
    where
      qu :: Quant -> VarOf formula -> formula -> formula
qu Quant
op VarOf formula
v formula
p = Quant -> VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
Quant -> VarOf formula -> formula -> formula
quant Quant
op VarOf formula
v ((AtomOf formula -> AtomOf formula) -> formula -> formula
forall formula.
IsQuantified formula =>
(AtomOf formula -> AtomOf formula) -> formula -> formula
onatomsQuantified AtomOf formula -> AtomOf formula
f formula
p)
      ne :: formula -> formula
ne formula
p = formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) ((AtomOf formula -> AtomOf formula) -> formula -> formula
forall formula.
IsQuantified formula =>
(AtomOf formula -> AtomOf formula) -> formula -> formula
onatomsQuantified AtomOf formula -> AtomOf formula
f formula
p)
      co :: formula -> BinOp -> formula -> formula
co formula
p BinOp
op formula
q = formula -> BinOp -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> BinOp -> formula -> formula
binop ((AtomOf formula -> AtomOf formula) -> formula -> formula
forall formula.
IsQuantified formula =>
(AtomOf formula -> AtomOf formula) -> formula -> formula
onatomsQuantified AtomOf formula -> AtomOf formula
f formula
p) BinOp
op ((AtomOf formula -> AtomOf formula) -> formula -> formula
forall formula.
IsQuantified formula =>
(AtomOf formula -> AtomOf formula) -> formula -> formula
onatomsQuantified AtomOf formula -> AtomOf formula
f formula
q)
      tf :: Bool -> formula
tf Bool
flag = Bool -> formula
forall formula. IsFormula formula => Bool -> formula
fromBool Bool
flag
      at :: AtomOf formula -> formula
at AtomOf formula
x = AtomOf formula -> formula
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (AtomOf formula -> AtomOf formula
f AtomOf formula
x)

overatomsQuantified :: IsQuantified fof => (AtomOf fof -> r -> r) -> fof -> r -> r
overatomsQuantified :: forall fof r.
IsQuantified fof =>
(AtomOf fof -> r -> r) -> fof -> r -> r
overatomsQuantified AtomOf fof -> r -> r
f fof
fof r
r0 =
    (Quant -> VarOf fof -> fof -> r)
-> (fof -> BinOp -> fof -> r)
-> (fof -> r)
-> (Bool -> r)
-> (AtomOf fof -> r)
-> fof
-> r
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf fof -> fof -> r)
-> (fof -> BinOp -> fof -> r)
-> (fof -> r)
-> (Bool -> r)
-> (AtomOf fof -> r)
-> fof
-> r
foldQuantified Quant -> VarOf fof -> fof -> r
qu fof -> BinOp -> fof -> r
co fof -> r
ne (r -> Bool -> r
forall a b. a -> b -> a
const r
r0) ((AtomOf fof -> r -> r) -> r -> AtomOf fof -> r
forall a b c. (a -> b -> c) -> b -> a -> c
flip AtomOf fof -> r -> r
f r
r0) fof
fof
    where
      qu :: Quant -> VarOf fof -> fof -> r
qu Quant
_ VarOf fof
_ fof
fof' = (AtomOf fof -> r -> r) -> fof -> r -> r
forall fof r.
IsQuantified fof =>
(AtomOf fof -> r -> r) -> fof -> r -> r
overatomsQuantified AtomOf fof -> r -> r
f fof
fof' r
r0
      ne :: fof -> r
ne fof
fof' = (AtomOf fof -> r -> r) -> fof -> r -> r
forall fof r.
IsQuantified fof =>
(AtomOf fof -> r -> r) -> fof -> r -> r
overatomsQuantified AtomOf fof -> r -> r
f fof
fof' r
r0
      co :: fof -> BinOp -> fof -> r
co fof
p BinOp
_ fof
q = (AtomOf fof -> r -> r) -> fof -> r -> r
forall fof r.
IsQuantified fof =>
(AtomOf fof -> r -> r) -> fof -> r -> r
overatomsQuantified AtomOf fof -> r -> r
f fof
p ((AtomOf fof -> r -> r) -> fof -> r -> r
forall fof r.
IsQuantified fof =>
(AtomOf fof -> r -> r) -> fof -> r -> r
overatomsQuantified AtomOf fof -> r -> r
f fof
q r
r0)

data QFormula v atom
    = F
    | T
    | Atom atom
    | Not (QFormula v atom)
    | And (QFormula v atom) (QFormula v atom)
    | Or (QFormula v atom) (QFormula v atom)
    | Imp (QFormula v atom) (QFormula v atom)
    | Iff (QFormula v atom) (QFormula v atom)
    | Forall v (QFormula v atom)
    | Exists v (QFormula v atom)
    deriving (QFormula v atom -> QFormula v atom -> Bool
(QFormula v atom -> QFormula v atom -> Bool)
-> (QFormula v atom -> QFormula v atom -> Bool)
-> Eq (QFormula v atom)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall v atom.
(Eq atom, Eq v) =>
QFormula v atom -> QFormula v atom -> Bool
$c== :: forall v atom.
(Eq atom, Eq v) =>
QFormula v atom -> QFormula v atom -> Bool
== :: QFormula v atom -> QFormula v atom -> Bool
$c/= :: forall v atom.
(Eq atom, Eq v) =>
QFormula v atom -> QFormula v atom -> Bool
/= :: QFormula v atom -> QFormula v atom -> Bool
Eq, Eq (QFormula v atom)
Eq (QFormula v atom) =>
(QFormula v atom -> QFormula v atom -> Ordering)
-> (QFormula v atom -> QFormula v atom -> Bool)
-> (QFormula v atom -> QFormula v atom -> Bool)
-> (QFormula v atom -> QFormula v atom -> Bool)
-> (QFormula v atom -> QFormula v atom -> Bool)
-> (QFormula v atom -> QFormula v atom -> QFormula v atom)
-> (QFormula v atom -> QFormula v atom -> QFormula v atom)
-> Ord (QFormula v atom)
QFormula v atom -> QFormula v atom -> Bool
QFormula v atom -> QFormula v atom -> Ordering
QFormula v atom -> QFormula v atom -> QFormula v atom
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 v atom. (Ord atom, Ord v) => Eq (QFormula v atom)
forall v atom.
(Ord atom, Ord v) =>
QFormula v atom -> QFormula v atom -> Bool
forall v atom.
(Ord atom, Ord v) =>
QFormula v atom -> QFormula v atom -> Ordering
forall v atom.
(Ord atom, Ord v) =>
QFormula v atom -> QFormula v atom -> QFormula v atom
$ccompare :: forall v atom.
(Ord atom, Ord v) =>
QFormula v atom -> QFormula v atom -> Ordering
compare :: QFormula v atom -> QFormula v atom -> Ordering
$c< :: forall v atom.
(Ord atom, Ord v) =>
QFormula v atom -> QFormula v atom -> Bool
< :: QFormula v atom -> QFormula v atom -> Bool
$c<= :: forall v atom.
(Ord atom, Ord v) =>
QFormula v atom -> QFormula v atom -> Bool
<= :: QFormula v atom -> QFormula v atom -> Bool
$c> :: forall v atom.
(Ord atom, Ord v) =>
QFormula v atom -> QFormula v atom -> Bool
> :: QFormula v atom -> QFormula v atom -> Bool
$c>= :: forall v atom.
(Ord atom, Ord v) =>
QFormula v atom -> QFormula v atom -> Bool
>= :: QFormula v atom -> QFormula v atom -> Bool
$cmax :: forall v atom.
(Ord atom, Ord v) =>
QFormula v atom -> QFormula v atom -> QFormula v atom
max :: QFormula v atom -> QFormula v atom -> QFormula v atom
$cmin :: forall v atom.
(Ord atom, Ord v) =>
QFormula v atom -> QFormula v atom -> QFormula v atom
min :: QFormula v atom -> QFormula v atom -> QFormula v atom
Ord, Typeable (QFormula v atom)
Typeable (QFormula v atom) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> QFormula v atom -> c (QFormula v atom))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (QFormula v atom))
-> (QFormula v atom -> Constr)
-> (QFormula v atom -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (QFormula v atom)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (QFormula v atom)))
-> ((forall b. Data b => b -> b)
    -> QFormula v atom -> QFormula v atom)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> QFormula v atom -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> QFormula v atom -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> QFormula v atom -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> QFormula v atom -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> QFormula v atom -> m (QFormula v atom))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> QFormula v atom -> m (QFormula v atom))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> QFormula v atom -> m (QFormula v atom))
-> Data (QFormula v atom)
QFormula v atom -> Constr
QFormula v atom -> DataType
(forall b. Data b => b -> b) -> QFormula v atom -> QFormula v atom
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) -> QFormula v atom -> u
forall u. (forall d. Data d => d -> u) -> QFormula v atom -> [u]
forall v atom. (Data atom, Data v) => Typeable (QFormula v atom)
forall v atom. (Data atom, Data v) => QFormula v atom -> Constr
forall v atom. (Data atom, Data v) => QFormula v atom -> DataType
forall v atom.
(Data atom, Data v) =>
(forall b. Data b => b -> b) -> QFormula v atom -> QFormula v atom
forall v atom u.
(Data atom, Data v) =>
Int -> (forall d. Data d => d -> u) -> QFormula v atom -> u
forall v atom u.
(Data atom, Data v) =>
(forall d. Data d => d -> u) -> QFormula v atom -> [u]
forall v atom r r'.
(Data atom, Data v) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QFormula v atom -> r
forall v atom r r'.
(Data atom, Data v) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QFormula v atom -> r
forall v atom (m :: * -> *).
(Data atom, Data v, Monad m) =>
(forall d. Data d => d -> m d)
-> QFormula v atom -> m (QFormula v atom)
forall v atom (m :: * -> *).
(Data atom, Data v, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> QFormula v atom -> m (QFormula v atom)
forall v atom (c :: * -> *).
(Data atom, Data v) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (QFormula v atom)
forall v atom (c :: * -> *).
(Data atom, Data v) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QFormula v atom -> c (QFormula v atom)
forall v atom (t :: * -> *) (c :: * -> *).
(Data atom, Data v, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (QFormula v atom))
forall v atom (t :: * -> * -> *) (c :: * -> *).
(Data atom, Data v, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (QFormula v atom))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QFormula v atom -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QFormula v atom -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> QFormula v atom -> m (QFormula v atom)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> QFormula v atom -> m (QFormula v atom)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (QFormula v atom)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QFormula v atom -> c (QFormula v atom)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (QFormula v atom))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (QFormula v atom))
$cgfoldl :: forall v atom (c :: * -> *).
(Data atom, Data v) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QFormula v atom -> c (QFormula v atom)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QFormula v atom -> c (QFormula v atom)
$cgunfold :: forall v atom (c :: * -> *).
(Data atom, Data v) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (QFormula v atom)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (QFormula v atom)
$ctoConstr :: forall v atom. (Data atom, Data v) => QFormula v atom -> Constr
toConstr :: QFormula v atom -> Constr
$cdataTypeOf :: forall v atom. (Data atom, Data v) => QFormula v atom -> DataType
dataTypeOf :: QFormula v atom -> DataType
$cdataCast1 :: forall v atom (t :: * -> *) (c :: * -> *).
(Data atom, Data v, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (QFormula v atom))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (QFormula v atom))
$cdataCast2 :: forall v atom (t :: * -> * -> *) (c :: * -> *).
(Data atom, Data v, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (QFormula v atom))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (QFormula v atom))
$cgmapT :: forall v atom.
(Data atom, Data v) =>
(forall b. Data b => b -> b) -> QFormula v atom -> QFormula v atom
gmapT :: (forall b. Data b => b -> b) -> QFormula v atom -> QFormula v atom
$cgmapQl :: forall v atom r r'.
(Data atom, Data v) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QFormula v atom -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QFormula v atom -> r
$cgmapQr :: forall v atom r r'.
(Data atom, Data v) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QFormula v atom -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QFormula v atom -> r
$cgmapQ :: forall v atom u.
(Data atom, Data v) =>
(forall d. Data d => d -> u) -> QFormula v atom -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> QFormula v atom -> [u]
$cgmapQi :: forall v atom u.
(Data atom, Data v) =>
Int -> (forall d. Data d => d -> u) -> QFormula v atom -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> QFormula v atom -> u
$cgmapM :: forall v atom (m :: * -> *).
(Data atom, Data v, Monad m) =>
(forall d. Data d => d -> m d)
-> QFormula v atom -> m (QFormula v atom)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> QFormula v atom -> m (QFormula v atom)
$cgmapMp :: forall v atom (m :: * -> *).
(Data atom, Data v, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> QFormula v atom -> m (QFormula v atom)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> QFormula v atom -> m (QFormula v atom)
$cgmapMo :: forall v atom (m :: * -> *).
(Data atom, Data v, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> QFormula v atom -> m (QFormula v atom)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> QFormula v atom -> m (QFormula v atom)
Data, Typeable, ReadPrec [QFormula v atom]
ReadPrec (QFormula v atom)
Int -> ReadS (QFormula v atom)
ReadS [QFormula v atom]
(Int -> ReadS (QFormula v atom))
-> ReadS [QFormula v atom]
-> ReadPrec (QFormula v atom)
-> ReadPrec [QFormula v atom]
-> Read (QFormula v atom)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall v atom. (Read atom, Read v) => ReadPrec [QFormula v atom]
forall v atom. (Read atom, Read v) => ReadPrec (QFormula v atom)
forall v atom.
(Read atom, Read v) =>
Int -> ReadS (QFormula v atom)
forall v atom. (Read atom, Read v) => ReadS [QFormula v atom]
$creadsPrec :: forall v atom.
(Read atom, Read v) =>
Int -> ReadS (QFormula v atom)
readsPrec :: Int -> ReadS (QFormula v atom)
$creadList :: forall v atom. (Read atom, Read v) => ReadS [QFormula v atom]
readList :: ReadS [QFormula v atom]
$creadPrec :: forall v atom. (Read atom, Read v) => ReadPrec (QFormula v atom)
readPrec :: ReadPrec (QFormula v atom)
$creadListPrec :: forall v atom. (Read atom, Read v) => ReadPrec [QFormula v atom]
readListPrec :: ReadPrec [QFormula v atom]
Read)

instance (HasApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => Pretty (QFormula v atom) where
    pPrintPrec :: PrettyLevel -> Rational -> QFormula v atom -> Doc
pPrintPrec = Side -> PrettyLevel -> Rational -> QFormula v atom -> Doc
forall fof v.
(IsQuantified fof, v ~ VarOf fof) =>
Side -> PrettyLevel -> Rational -> fof -> Doc
prettyQuantified Side
Top

-- The IsFormula instance for QFormula
instance (HasApply atom, v ~ TVarOf (TermOf atom)) => IsFormula (QFormula v atom) where
    type AtomOf (QFormula v atom) = atom
    asBool :: QFormula v atom -> Maybe Bool
asBool QFormula v atom
T = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
    asBool QFormula v atom
F = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
    asBool QFormula v atom
_ = Maybe Bool
forall a. Maybe a
Nothing
    true :: QFormula v atom
true = QFormula v atom
forall v atom. QFormula v atom
T
    false :: QFormula v atom
false = QFormula v atom
forall v atom. QFormula v atom
F
    atomic :: AtomOf (QFormula v atom) -> QFormula v atom
atomic = atom -> QFormula v atom
AtomOf (QFormula v atom) -> QFormula v atom
forall v atom. atom -> QFormula v atom
Atom
    overatoms :: forall r.
(AtomOf (QFormula v atom) -> r -> r) -> QFormula v atom -> r -> r
overatoms = (AtomOf (QFormula v atom) -> r -> r) -> QFormula v atom -> r -> r
forall fof r.
IsQuantified fof =>
(AtomOf fof -> r -> r) -> fof -> r -> r
overatomsQuantified
    onatoms :: (AtomOf (QFormula v atom) -> AtomOf (QFormula v atom))
-> QFormula v atom -> QFormula v atom
onatoms = (AtomOf (QFormula v atom) -> AtomOf (QFormula v atom))
-> QFormula v atom -> QFormula v atom
forall formula.
IsQuantified formula =>
(AtomOf formula -> AtomOf formula) -> formula -> formula
onatomsQuantified

instance (IsFormula (QFormula v atom), HasApply atom, v ~ TVarOf (TermOf atom)) => IsPropositional (QFormula v atom) where
    .|. :: QFormula v atom -> QFormula v atom -> QFormula v atom
(.|.) = QFormula v atom -> QFormula v atom -> QFormula v atom
forall v atom.
QFormula v atom -> QFormula v atom -> QFormula v atom
Or
    .&. :: QFormula v atom -> QFormula v atom -> QFormula v atom
(.&.) = QFormula v atom -> QFormula v atom -> QFormula v atom
forall v atom.
QFormula v atom -> QFormula v atom -> QFormula v atom
And
    .=>. :: QFormula v atom -> QFormula v atom -> QFormula v atom
(.=>.) = QFormula v atom -> QFormula v atom -> QFormula v atom
forall v atom.
QFormula v atom -> QFormula v atom -> QFormula v atom
Imp
    .<=>. :: QFormula v atom -> QFormula v atom -> QFormula v atom
(.<=>.) = QFormula v atom -> QFormula v atom -> QFormula v atom
forall v atom.
QFormula v atom -> QFormula v atom -> QFormula v atom
Iff
    foldPropositional' :: forall r.
(QFormula v atom -> r)
-> (QFormula v atom -> BinOp -> QFormula v atom -> r)
-> (QFormula v atom -> r)
-> (Bool -> r)
-> (AtomOf (QFormula v atom) -> r)
-> QFormula v atom
-> r
foldPropositional' QFormula v atom -> r
ho QFormula v atom -> BinOp -> QFormula v atom -> r
co QFormula v atom -> r
ne Bool -> r
tf AtomOf (QFormula v atom) -> r
at QFormula v atom
fm =
        case QFormula v atom
fm of
          And QFormula v atom
p QFormula v atom
q -> QFormula v atom -> BinOp -> QFormula v atom -> r
co QFormula v atom
p BinOp
(:&:) QFormula v atom
q
          Or QFormula v atom
p QFormula v atom
q -> QFormula v atom -> BinOp -> QFormula v atom -> r
co QFormula v atom
p BinOp
(:|:) QFormula v atom
q
          Imp QFormula v atom
p QFormula v atom
q -> QFormula v atom -> BinOp -> QFormula v atom -> r
co QFormula v atom
p BinOp
(:=>:) QFormula v atom
q
          Iff QFormula v atom
p QFormula v atom
q -> QFormula v atom -> BinOp -> QFormula v atom -> r
co QFormula v atom
p BinOp
(:<=>:) QFormula v atom
q
          QFormula v atom
_ -> (QFormula v atom -> r)
-> (QFormula v atom -> r)
-> (Bool -> r)
-> (AtomOf (QFormula v atom) -> r)
-> QFormula v atom
-> r
forall lit r.
IsLiteral lit =>
(lit -> r)
-> (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
forall r.
(QFormula v atom -> r)
-> (QFormula v atom -> r)
-> (Bool -> r)
-> (AtomOf (QFormula v atom) -> r)
-> QFormula v atom
-> r
foldLiteral' QFormula v atom -> r
ho QFormula v atom -> r
ne Bool -> r
tf AtomOf (QFormula v atom) -> r
at QFormula v atom
fm
    foldCombination :: forall r.
(QFormula v atom -> r)
-> (QFormula v atom -> QFormula v atom -> r)
-> (QFormula v atom -> QFormula v atom -> r)
-> (QFormula v atom -> QFormula v atom -> r)
-> (QFormula v atom -> QFormula v atom -> r)
-> QFormula v atom
-> r
foldCombination QFormula v atom -> r
other QFormula v atom -> QFormula v atom -> r
dj QFormula v atom -> QFormula v atom -> r
cj QFormula v atom -> QFormula v atom -> r
imp QFormula v atom -> QFormula v atom -> r
iff QFormula v atom
fm =
        case QFormula v atom
fm of
          Or QFormula v atom
a QFormula v atom
b -> QFormula v atom
a QFormula v atom -> QFormula v atom -> r
`dj` QFormula v atom
b
          And QFormula v atom
a QFormula v atom
b -> QFormula v atom
a QFormula v atom -> QFormula v atom -> r
`cj` QFormula v atom
b
          Imp QFormula v atom
a QFormula v atom
b -> QFormula v atom
a QFormula v atom -> QFormula v atom -> r
`imp` QFormula v atom
b
          Iff QFormula v atom
a QFormula v atom
b -> QFormula v atom
a QFormula v atom -> QFormula v atom -> r
`iff` QFormula v atom
b
          QFormula v atom
_ -> QFormula v atom -> r
other QFormula v atom
fm

instance (IsPropositional (QFormula v atom), IsVariable v, IsAtom atom) => IsQuantified (QFormula v atom) where
    type VarOf (QFormula v atom) = v
    quant :: Quant
-> VarOf (QFormula v atom) -> QFormula v atom -> QFormula v atom
quant Quant
(:!:) = v -> QFormula v atom -> QFormula v atom
VarOf (QFormula v atom) -> QFormula v atom -> QFormula v atom
forall v atom. v -> QFormula v atom -> QFormula v atom
Forall
    quant Quant
(:?:) = v -> QFormula v atom -> QFormula v atom
VarOf (QFormula v atom) -> QFormula v atom -> QFormula v atom
forall v atom. v -> QFormula v atom -> QFormula v atom
Exists
    foldQuantified :: forall r.
(Quant -> VarOf (QFormula v atom) -> QFormula v atom -> r)
-> (QFormula v atom -> BinOp -> QFormula v atom -> r)
-> (QFormula v atom -> r)
-> (Bool -> r)
-> (AtomOf (QFormula v atom) -> r)
-> QFormula v atom
-> r
foldQuantified Quant -> VarOf (QFormula v atom) -> QFormula v atom -> r
qu QFormula v atom -> BinOp -> QFormula v atom -> r
_co QFormula v atom -> r
_ne Bool -> r
_tf AtomOf (QFormula v atom) -> r
_at (Forall v
v QFormula v atom
fm) = Quant -> VarOf (QFormula v atom) -> QFormula v atom -> r
qu Quant
(:!:) v
VarOf (QFormula v atom)
v QFormula v atom
fm
    foldQuantified Quant -> VarOf (QFormula v atom) -> QFormula v atom -> r
qu QFormula v atom -> BinOp -> QFormula v atom -> r
_co QFormula v atom -> r
_ne Bool -> r
_tf AtomOf (QFormula v atom) -> r
_at (Exists v
v QFormula v atom
fm) = Quant -> VarOf (QFormula v atom) -> QFormula v atom -> r
qu Quant
(:?:) v
VarOf (QFormula v atom)
v QFormula v atom
fm
    foldQuantified Quant -> VarOf (QFormula v atom) -> QFormula v atom -> r
_qu QFormula v atom -> BinOp -> QFormula v atom -> r
co QFormula v atom -> r
ne Bool -> r
tf AtomOf (QFormula v atom) -> r
at QFormula v atom
fm =
        (QFormula v atom -> r)
-> (QFormula v atom -> BinOp -> QFormula v atom -> r)
-> (QFormula v atom -> r)
-> (Bool -> r)
-> (AtomOf (QFormula v atom) -> r)
-> QFormula v atom
-> r
forall formula r.
IsPropositional formula =>
(formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(QFormula v atom -> r)
-> (QFormula v atom -> BinOp -> QFormula v atom -> r)
-> (QFormula v atom -> r)
-> (Bool -> r)
-> (AtomOf (QFormula v atom) -> r)
-> QFormula v atom
-> r
foldPropositional' (\QFormula v atom
_ -> String -> r
forall a. HasCallStack => String -> a
error String
"IsQuantified QFormula") QFormula v atom -> BinOp -> QFormula v atom -> r
co QFormula v atom -> r
ne Bool -> r
tf AtomOf (QFormula v atom) -> r
at QFormula v atom
fm

-- Build a Haskell expression for this formula
instance IsQuantified (QFormula v atom) => Show (QFormula v atom) where
    showsPrec :: Int -> QFormula v atom -> ShowS
showsPrec = Side -> Int -> QFormula v atom -> ShowS
forall formula.
IsQuantified formula =>
Side -> Int -> formula -> ShowS
showQuantified Side
Top

-- Precedence information for QFormula
instance IsQuantified (QFormula v atom) => HasFixity (QFormula v atom) where
    precedence :: QFormula v atom -> Precedence
precedence = QFormula v atom -> a
QFormula v atom -> Precedence
forall formula. IsQuantified formula => formula -> Precedence
precedenceQuantified
    associativity :: QFormula v atom -> Associativity
associativity = QFormula v atom -> Associativity
forall formula. IsQuantified formula => formula -> Associativity
associativityQuantified

instance (HasApply atom, v ~ TVarOf (TermOf atom)) => IsLiteral (QFormula v atom) where
    naiveNegate :: QFormula v atom -> QFormula v atom
naiveNegate = QFormula v atom -> QFormula v atom
forall v atom. QFormula v atom -> QFormula v atom
Not
    foldNegation :: forall r.
(QFormula v atom -> r)
-> (QFormula v atom -> r) -> QFormula v atom -> r
foldNegation QFormula v atom -> r
normal QFormula v atom -> r
inverted (Not QFormula v atom
x) = (QFormula v atom -> r)
-> (QFormula v atom -> r) -> QFormula v atom -> r
forall lit r. IsLiteral lit => (lit -> r) -> (lit -> r) -> lit -> r
forall r.
(QFormula v atom -> r)
-> (QFormula v atom -> r) -> QFormula v atom -> r
foldNegation QFormula v atom -> r
inverted QFormula v atom -> r
normal QFormula v atom
x
    foldNegation QFormula v atom -> r
normal QFormula v atom -> r
_ QFormula v atom
x = QFormula v atom -> r
normal QFormula v atom
x
    foldLiteral' :: forall r.
(QFormula v atom -> r)
-> (QFormula v atom -> r)
-> (Bool -> r)
-> (AtomOf (QFormula v atom) -> r)
-> QFormula v atom
-> r
foldLiteral' QFormula v atom -> r
ho QFormula v atom -> r
ne Bool -> r
tf AtomOf (QFormula v atom) -> r
at QFormula v atom
fm =
        case QFormula v atom
fm of
          QFormula v atom
T -> Bool -> r
tf Bool
True
          QFormula v atom
F -> Bool -> r
tf Bool
False
          Atom atom
a -> AtomOf (QFormula v atom) -> r
at atom
AtomOf (QFormula v atom)
a
          Not QFormula v atom
p -> QFormula v atom -> r
ne QFormula v atom
p
          QFormula v atom
_ -> QFormula v atom -> r
ho QFormula v atom
fm