{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeFamilies #-}

-- |
-- Module      : AutoProof.Internal.Formula.Types
-- Copyright   : (c) Artem Mavrin, 2021
-- License     : BSD3
-- Maintainer  : artemvmavrin@gmail.com
-- Stability   : experimental
-- Portability : POSIX
--
-- Defines the 'Formula' type, its constructors, and its instances.
module AutoProof.Internal.Formula.Types
  ( -- * Formula type
    Formula (Lit, Var, Not, Imp, Or, And, Iff),

    -- * Pretty-printing
    prettyFormula,
  )
where

import AutoProof.Internal.AST
  ( AST (Root, children, metadata, root),
    ASTMetadata,
    atomicASTConstructor,
    binaryASTConstructor,
    unaryASTConstructor,
  )
import AutoProof.Internal.Utils.PrettyPrintable
  ( PrettyPrintable (pretty, prettys),
  )
import AutoProof.Internal.Utils.PrettyPrintable.Symbols
  ( andS,
    falseS,
    iffS,
    impS,
    notS,
    orS,
    trueS,
  )

-- | Formulas of propositional logic are built inductively from atomic
-- propositions
--
-- * truth \(\top\),
-- * falsity \(\bot\), and
-- * propositional variables \(a, b, c, \ldots\)
--
-- using the unary connective
--
-- * negation \(\lnot\)
--
-- and the binary connectives
--
-- * implication \(\rightarrow\),
-- * disjunction \(\lor\),
-- * conjunction \(\land\), and
-- * equivalence \(\leftrightarrow\).
data Formula a
  = Lit_ !ASTMetadata Bool
  | Var_ !ASTMetadata a
  | Not_ !ASTMetadata !(Formula a)
  | Imp_ !ASTMetadata !(Formula a) !(Formula a)
  | Or_ !ASTMetadata !(Formula a) !(Formula a)
  | And_ !ASTMetadata !(Formula a) !(Formula a)
  | Iff_ !ASTMetadata !(Formula a) !(Formula a)

-- Smart constructors and pattern matching synonyms

-- | Propositional literal/constant. @('Lit' 'True')@ is \(\top\) (i.e., truth,
-- tautology, or top), and @('Lit' 'False')@ is \(\bot\) (i.e., falsity,
-- contradiction, or bottom).
pattern Lit :: Bool -> Formula a
pattern $bLit :: Bool -> Formula a
$mLit :: forall r a. Formula a -> (Bool -> r) -> (Void# -> r) -> r
Lit x <-
  Lit_ _ x
  where
    Lit = (ASTMetadata -> Bool -> Formula a) -> Bool -> Formula a
forall a t. (ASTMetadata -> a -> t) -> a -> t
atomicASTConstructor ASTMetadata -> Bool -> Formula a
forall a. ASTMetadata -> Bool -> Formula a
Lit_

-- | Propositional variable. @('Var' x)@ represents a propositional variable
-- \(x\).
pattern Var :: a -> Formula a
pattern $bVar :: a -> Formula a
$mVar :: forall r a. Formula a -> (a -> r) -> (Void# -> r) -> r
Var x <-
  Var_ _ x
  where
    Var = (ASTMetadata -> a -> Formula a) -> a -> Formula a
forall a t. (ASTMetadata -> a -> t) -> a -> t
atomicASTConstructor ASTMetadata -> a -> Formula a
forall a. ASTMetadata -> a -> Formula a
Var_

-- | Negation. @('Not' p)@ represents the formula \(\lnot p\).
pattern Not :: Formula a -> Formula a
pattern $bNot :: Formula a -> Formula a
$mNot :: forall r a. Formula a -> (Formula a -> r) -> (Void# -> r) -> r
Not a <-
  Not_ _ a
  where
    Not = (ASTMetadata -> Formula a -> Formula a) -> Formula a -> Formula a
forall t. AST t => (ASTMetadata -> t -> t) -> t -> t
unaryASTConstructor ASTMetadata -> Formula a -> Formula a
forall a. ASTMetadata -> Formula a -> Formula a
Not_

-- | Implication. @('Imp' p q)@ represents the formula \(p \rightarrow q\).
pattern Imp :: Formula a -> Formula a -> Formula a
pattern $bImp :: Formula a -> Formula a -> Formula a
$mImp :: forall r a.
Formula a -> (Formula a -> Formula a -> r) -> (Void# -> r) -> r
Imp a b <-
  Imp_ _ a b
  where
    Imp = (ASTMetadata -> Formula a -> Formula a -> Formula a)
-> Formula a -> Formula a -> Formula a
forall t. AST t => (ASTMetadata -> t -> t -> t) -> t -> t -> t
binaryASTConstructor ASTMetadata -> Formula a -> Formula a -> Formula a
forall a. ASTMetadata -> Formula a -> Formula a -> Formula a
Imp_

-- | Disjunction. @('Or' p q)@ represents the formula \(p \lor q\).
pattern Or :: Formula a -> Formula a -> Formula a
pattern $bOr :: Formula a -> Formula a -> Formula a
$mOr :: forall r a.
Formula a -> (Formula a -> Formula a -> r) -> (Void# -> r) -> r
Or a b <-
  Or_ _ a b
  where
    Or = (ASTMetadata -> Formula a -> Formula a -> Formula a)
-> Formula a -> Formula a -> Formula a
forall t. AST t => (ASTMetadata -> t -> t -> t) -> t -> t -> t
binaryASTConstructor ASTMetadata -> Formula a -> Formula a -> Formula a
forall a. ASTMetadata -> Formula a -> Formula a -> Formula a
Or_

-- | Conjunction. @('And' p q)@ represents the formula \(p \land q\).
pattern And :: Formula a -> Formula a -> Formula a
pattern $bAnd :: Formula a -> Formula a -> Formula a
$mAnd :: forall r a.
Formula a -> (Formula a -> Formula a -> r) -> (Void# -> r) -> r
And a b <-
  And_ _ a b
  where
    And = (ASTMetadata -> Formula a -> Formula a -> Formula a)
-> Formula a -> Formula a -> Formula a
forall t. AST t => (ASTMetadata -> t -> t -> t) -> t -> t -> t
binaryASTConstructor ASTMetadata -> Formula a -> Formula a -> Formula a
forall a. ASTMetadata -> Formula a -> Formula a -> Formula a
And_

-- | Equivalence. @('Iff' p q)@ represents the formula \(p \leftrightarrow q\).
pattern Iff :: Formula a -> Formula a -> Formula a
pattern $bIff :: Formula a -> Formula a -> Formula a
$mIff :: forall r a.
Formula a -> (Formula a -> Formula a -> r) -> (Void# -> r) -> r
Iff a b <-
  Iff_ _ a b
  where
    Iff = (ASTMetadata -> Formula a -> Formula a -> Formula a)
-> Formula a -> Formula a -> Formula a
forall t. AST t => (ASTMetadata -> t -> t -> t) -> t -> t -> t
binaryASTConstructor ASTMetadata -> Formula a -> Formula a -> Formula a
forall a. ASTMetadata -> Formula a -> Formula a -> Formula a
Iff_

{-# COMPLETE Lit, Var, Not, Imp, Or, And, Iff #-}

instance AST (Formula a) where
  type Root (Formula a) = Maybe a

  root :: Formula a -> Root (Formula a)
root (Var x :: a
x) = a -> Maybe a
forall a. a -> Maybe a
Just a
x
  root _ = Root (Formula a)
forall a. Maybe a
Nothing

  children :: Formula a -> [Formula a]
children (Lit _) = []
  children (Var _) = []
  children (Not a :: Formula a
a) = [Formula a
a]
  children (Imp a :: Formula a
a b :: Formula a
b) = [Formula a
a, Formula a
b]
  children (Or a :: Formula a
a b :: Formula a
b) = [Formula a
a, Formula a
b]
  children (And a :: Formula a
a b :: Formula a
b) = [Formula a
a, Formula a
b]
  children (Iff a :: Formula a
a b :: Formula a
b) = [Formula a
a, Formula a
b]

  metadata :: Formula a -> ASTMetadata
metadata (Lit_ m :: ASTMetadata
m _) = ASTMetadata
m
  metadata (Var_ m :: ASTMetadata
m _) = ASTMetadata
m
  metadata (Not_ m :: ASTMetadata
m _) = ASTMetadata
m
  metadata (Imp_ m :: ASTMetadata
m _ _) = ASTMetadata
m
  metadata (Or_ m :: ASTMetadata
m _ _) = ASTMetadata
m
  metadata (And_ m :: ASTMetadata
m _ _) = ASTMetadata
m
  metadata (Iff_ m :: ASTMetadata
m _ _) = ASTMetadata
m

-- Instance declarations

instance Show a => Show (Formula a) where
  showsPrec :: Int -> Formula a -> ShowS
showsPrec d :: Int
d = Bool -> Formula a -> ShowS
f (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec)
    where
      appPrec :: Int
appPrec = 10

      f :: Bool -> Formula a -> ShowS
f b :: Bool
b a :: Formula a
a = Bool -> ShowS -> ShowS
showParen Bool
b (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Formula a -> ShowS
g Formula a
a

      g :: Formula a -> ShowS
g (Lit False) = String -> ShowS
showString "Lit False"
      g (Lit True) = String -> ShowS
showString "Lit True"
      g (Var x :: a
x) = String -> ShowS
showString "Var " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) a
x
      g (Not p :: Formula a
p) = String -> ShowS
showString "Not " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Formula a -> ShowS
f Bool
True Formula a
p
      g (Imp p :: Formula a
p q :: Formula a
q) = String -> Formula a -> Formula a -> ShowS
h "Imp " Formula a
p Formula a
q
      g (Or p :: Formula a
p q :: Formula a
q) = String -> Formula a -> Formula a -> ShowS
h "Or " Formula a
p Formula a
q
      g (And p :: Formula a
p q :: Formula a
q) = String -> Formula a -> Formula a -> ShowS
h "And " Formula a
p Formula a
q
      g (Iff p :: Formula a
p q :: Formula a
q) = String -> Formula a -> Formula a -> ShowS
h "Iff " Formula a
p Formula a
q

      h :: String -> Formula a -> Formula a -> ShowS
h c :: String
c p :: Formula a
p q :: Formula a
q = String -> ShowS
showString String
c ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Formula a -> ShowS
f Bool
True Formula a
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Formula a -> ShowS
f Bool
True Formula a
q

instance Read a => Read (Formula a) where
  readsPrec :: Int -> ReadS (Formula a)
readsPrec d :: Int
d = Bool -> ReadS (Formula a)
f (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec)
    where
      appPrec :: Int
appPrec = 10

      f :: Bool -> ReadS (Formula a)
f b :: Bool
b s :: String
s = (ReadS (Formula a) -> [(Formula a, String)])
-> [ReadS (Formula a)] -> [(Formula a, String)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((ReadS (Formula a) -> ReadS (Formula a)
forall a b. (a -> b) -> a -> b
$ String
s) (ReadS (Formula a) -> [(Formula a, String)])
-> (ReadS (Formula a) -> ReadS (Formula a))
-> ReadS (Formula a)
-> [(Formula a, String)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> ReadS (Formula a) -> ReadS (Formula a)
forall a. Bool -> ReadS a -> ReadS a
readParen Bool
b) [ReadS (Formula a)]
readers
      readers :: [ReadS (Formula a)]
readers =
        [ ReadS (Formula a)
readLit,
          ReadS (Formula a)
readVar,
          ReadS (Formula a)
readNot,
          ReadS (Formula a)
readImp,
          ReadS (Formula a)
readOr,
          ReadS (Formula a)
readAnd,
          ReadS (Formula a)
readIff
        ]
      readLit :: ReadS (Formula a)
readLit s :: String
s = [(Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
b, String
r) | ("Lit", t :: String
t) <- ReadS String
lex String
s, (b :: Bool
b, r :: String
r) <- Int -> ReadS Bool
forall a. Read a => Int -> ReadS a
readsPrec (Int
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) String
t]
      readVar :: ReadS (Formula a)
readVar s :: String
s = [(a -> Formula a
forall a. a -> Formula a
Var a
x, String
r) | ("Var", t :: String
t) <- ReadS String
lex String
s, (x :: a
x, r :: String
r) <- Int -> ReadS a
forall a. Read a => Int -> ReadS a
readsPrec (Int
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) String
t]
      readNot :: ReadS (Formula a)
readNot = (Formula a -> Formula a) -> String -> ReadS (Formula a)
parseUnary Formula a -> Formula a
forall a. Formula a -> Formula a
Not "Not"
      readImp :: ReadS (Formula a)
readImp = (Formula a -> Formula a -> Formula a)
-> String -> ReadS (Formula a)
parseBinary Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp "Imp"
      readOr :: ReadS (Formula a)
readOr = (Formula a -> Formula a -> Formula a)
-> String -> ReadS (Formula a)
parseBinary Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Or "Or"
      readAnd :: ReadS (Formula a)
readAnd = (Formula a -> Formula a -> Formula a)
-> String -> ReadS (Formula a)
parseBinary Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
And "And"
      readIff :: ReadS (Formula a)
readIff = (Formula a -> Formula a -> Formula a)
-> String -> ReadS (Formula a)
parseBinary Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Iff "Iff"

      parseUnary :: (Formula a -> Formula a) -> String -> ReadS (Formula a)
parseUnary c :: Formula a -> Formula a
c n :: String
n s :: String
s = [(Formula a -> Formula a
c Formula a
a, String
u) | (n' :: String
n', t :: String
t) <- ReadS String
lex String
s, String
n String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
n', (a :: Formula a
a, u :: String
u) <- Bool -> ReadS (Formula a)
f Bool
True String
t]
      parseBinary :: (Formula a -> Formula a -> Formula a)
-> String -> ReadS (Formula a)
parseBinary c :: Formula a -> Formula a -> Formula a
c n :: String
n s :: String
s = [(Formula a -> Formula a -> Formula a
c Formula a
a Formula a
b, String
v) | (n' :: String
n', t :: String
t) <- ReadS String
lex String
s, String
n String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
n', (a :: Formula a
a, u :: String
u) <- Bool -> ReadS (Formula a)
f Bool
True String
t, (b :: Formula a
b, v :: String
v) <- Bool -> ReadS (Formula a)
f Bool
True String
u]

-- | Syntactic equality.
instance Eq a => Eq (Formula a) where
  (Lit a :: Bool
a) == :: Formula a -> Formula a -> Bool
== (Lit b :: Bool
b) = Bool
a Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b
  (Var a :: a
a) == (Var b :: a
b) = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b
  (Not a :: Formula a
a) == (Not b :: Formula a
b) = Formula a
a Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
b
  (Imp a :: Formula a
a c :: Formula a
c) == (Imp b :: Formula a
b d :: Formula a
d) = Formula a
a Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
b Bool -> Bool -> Bool
&& Formula a
c Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
d
  (Or a :: Formula a
a c :: Formula a
c) == (Or b :: Formula a
b d :: Formula a
d) = Formula a
a Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
b Bool -> Bool -> Bool
&& Formula a
c Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
d
  (And a :: Formula a
a c :: Formula a
c) == (And b :: Formula a
b d :: Formula a
d) = Formula a
a Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
b Bool -> Bool -> Bool
&& Formula a
c Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
d
  (Iff a :: Formula a
a c :: Formula a
c) == (Iff b :: Formula a
b d :: Formula a
d) = Formula a
a Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
b Bool -> Bool -> Bool
&& Formula a
c Formula a -> Formula a -> Bool
forall a. Eq a => a -> a -> Bool
== Formula a
d
  _ == _ = Bool
False

-- | First compare heights, then compare sizes, then resolve using the
-- convention @Lit < Var < Not < Imp < Or < And < Iff@ (on equality, compare
-- children from left to right).
instance Ord a => Ord (Formula a) where
  compare :: Formula a -> Formula a -> Ordering
compare a :: Formula a
a b :: Formula a
b = case ASTMetadata -> ASTMetadata -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Formula a -> ASTMetadata
forall t. AST t => t -> ASTMetadata
metadata Formula a
a) (Formula a -> ASTMetadata
forall t. AST t => t -> ASTMetadata
metadata Formula a
b) of
    EQ -> case Formula a
a of
      Lit c :: Bool
c -> case Formula a
b of
        Lit d :: Bool
d -> Bool -> Bool -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Bool
c Bool
d
        _ -> Ordering
LT
      Var c :: a
c -> case Formula a
b of
        Lit {} -> Ordering
GT
        Var d :: a
d -> a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
c a
d
        _ -> Ordering
LT
      Not c :: Formula a
c -> case Formula a
b of
        Lit {} -> Ordering
GT
        Var {} -> Ordering
GT
        Not d :: Formula a
d -> Formula a -> Formula a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Formula a
c Formula a
d
        _ -> Ordering
LT
      Imp c :: Formula a
c e :: Formula a
e -> case Formula a
b of
        Iff {} -> Ordering
LT
        And {} -> Ordering
LT
        Or {} -> Ordering
LT
        Imp d :: Formula a
d f :: Formula a
f -> case Formula a -> Formula a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Formula a
c Formula a
d of
          EQ -> Formula a -> Formula a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Formula a
e Formula a
f
          y :: Ordering
y -> Ordering
y
        _ -> Ordering
GT
      Or c :: Formula a
c e :: Formula a
e -> case Formula a
b of
        Iff {} -> Ordering
LT
        And {} -> Ordering
LT
        Or d :: Formula a
d f :: Formula a
f -> case Formula a -> Formula a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Formula a
c Formula a
d of
          EQ -> Formula a -> Formula a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Formula a
e Formula a
f
          y :: Ordering
y -> Ordering
y
        _ -> Ordering
GT
      And c :: Formula a
c e :: Formula a
e -> case Formula a
b of
        Iff {} -> Ordering
LT
        And d :: Formula a
d f :: Formula a
f -> case Formula a -> Formula a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Formula a
c Formula a
d of
          EQ -> Formula a -> Formula a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Formula a
e Formula a
f
          y :: Ordering
y -> Ordering
y
        _ -> Ordering
GT
      Iff c :: Formula a
c e :: Formula a
e -> case Formula a
b of
        Iff d :: Formula a
d f :: Formula a
f -> case Formula a -> Formula a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Formula a
c Formula a
d of
          EQ -> Formula a -> Formula a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Formula a
e Formula a
f
          y :: Ordering
y -> Ordering
y
        _ -> Ordering
GT
    x :: Ordering
x -> Ordering
x

instance PrettyPrintable a => PrettyPrintable (Formula a) where
  prettys :: Formula a -> ShowS
prettys = Bool -> Formula a -> ShowS
forall a. PrettyPrintable a => Bool -> Formula a -> ShowS
f Bool
False
    where
      f :: Bool -> Formula a -> ShowS
f _ p :: Formula a
p@(Lit _) = Formula a -> ShowS
g Formula a
p
      f _ p :: Formula a
p@(Var _) = Formula a -> ShowS
g Formula a
p
      f _ p :: Formula a
p@Not {} = Formula a -> ShowS
g Formula a
p
      f b :: Bool
b p :: Formula a
p = Bool -> ShowS -> ShowS
showParen Bool
b (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Formula a -> ShowS
g Formula a
p

      g :: Formula a -> ShowS
g (Lit False) = String -> ShowS
showString String
falseS
      g (Lit True) = String -> ShowS
showString String
trueS
      g (Var x :: a
x) = a -> ShowS
forall a. PrettyPrintable a => a -> ShowS
prettys a
x
      g (Not p :: Formula a
p) = String -> ShowS
showString String
notS ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Formula a -> ShowS
f Bool
True Formula a
p
      g (Imp p :: Formula a
p q :: Formula a
q) = Bool -> Formula a -> ShowS
f Bool
True Formula a
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
padded String
impS ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Formula a -> ShowS
f Bool
True Formula a
q
      g (Or p :: Formula a
p q :: Formula a
q) = Bool -> Formula a -> ShowS
f Bool
True Formula a
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
padded String
orS ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Formula a -> ShowS
f Bool
True Formula a
q
      g (And p :: Formula a
p q :: Formula a
q) = Bool -> Formula a -> ShowS
f Bool
True Formula a
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
padded String
andS ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Formula a -> ShowS
f Bool
True Formula a
q
      g (Iff p :: Formula a
p q :: Formula a
q) = Bool -> Formula a -> ShowS
f Bool
True Formula a
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
padded String
iffS ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Formula a -> ShowS
f Bool
True Formula a
q

      -- Pad a symbol with one space character on each side
      padded :: String -> ShowS
      padded :: String -> ShowS
padded s :: String
s = String -> ShowS
showString (' ' Char -> ShowS
forall a. a -> [a] -> [a]
: String
s) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " "

-- | Get a pretty-printed representation of a propositional formula.
--
-- ==== __Examples__
--
-- >>> prettyFormula $ Imp (Var "a") (Or (Var "b") (Lit False))
-- "a → (b ∨ ⊥)"
prettyFormula :: PrettyPrintable a => Formula a -> String
prettyFormula :: Formula a -> String
prettyFormula = Formula a -> String
forall a. PrettyPrintable a => a -> String
pretty