autoproof-0.0.0.0: Propositional logic library
Copyright(c) Artem Mavrin 2021
LicenseBSD3
Maintainerartemvmavrin@gmail.com
Stabilityexperimental
PortabilityPOSIX
Safe HaskellSafe
LanguageHaskell2010

AutoProof.Internal.Formula.Types

Description

Defines the Formula type, its constructors, and its instances.

Synopsis

Formula type

data Formula a where Source #

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\).

Bundled Patterns

pattern Lit :: Bool -> Formula a

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 Var :: a -> Formula a

Propositional variable. (Var x) represents a propositional variable \(x\).

pattern Not :: Formula a -> Formula a

Negation. (Not p) represents the formula \(\lnot p\).

pattern Imp :: Formula a -> Formula a -> Formula a

Implication. (Imp p q) represents the formula \(p \rightarrow q\).

pattern Or :: Formula a -> Formula a -> Formula a

Disjunction. (Or p q) represents the formula \(p \lor q\).

pattern And :: Formula a -> Formula a -> Formula a

Conjunction. (And p q) represents the formula \(p \land q\).

pattern Iff :: Formula a -> Formula a -> Formula a

Equivalence. (Iff p q) represents the formula \(p \leftrightarrow q\).

Instances

Instances details
Eq a => Eq (Formula a) Source #

Syntactic equality.

Instance details

Defined in AutoProof.Internal.Formula.Types

Methods

(==) :: Formula a -> Formula a -> Bool #

(/=) :: Formula a -> Formula a -> Bool #

Ord a => Ord (Formula a) Source #

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 details

Defined in AutoProof.Internal.Formula.Types

Methods

compare :: Formula a -> Formula a -> Ordering #

(<) :: Formula a -> Formula a -> Bool #

(<=) :: Formula a -> Formula a -> Bool #

(>) :: Formula a -> Formula a -> Bool #

(>=) :: Formula a -> Formula a -> Bool #

max :: Formula a -> Formula a -> Formula a #

min :: Formula a -> Formula a -> Formula a #

Read a => Read (Formula a) Source # 
Instance details

Defined in AutoProof.Internal.Formula.Types

Methods

readsPrec :: Int -> ReadS (Formula a) #

readList :: ReadS [Formula a] #

readPrec :: ReadPrec (Formula a) #

readListPrec :: ReadPrec [Formula a] #

Show a => Show (Formula a) Source # 
Instance details

Defined in AutoProof.Internal.Formula.Types

Methods

showsPrec :: Int -> Formula a -> ShowS #

show :: Formula a -> String #

showList :: [Formula a] -> ShowS #

AST (Formula a) Source # 
Instance details

Defined in AutoProof.Internal.Formula.Types

Associated Types

type Root (Formula a) Source #

Methods

root :: Formula a -> Root (Formula a) Source #

children :: Formula a -> [Formula a] Source #

metadata :: Formula a -> ASTMetadata Source #

height :: Formula a -> Int Source #

size :: Formula a -> Int Source #

PrettyPrintable a => PrettyPrintable (Formula a) Source # 
Instance details

Defined in AutoProof.Internal.Formula.Types

Methods

pretty :: Formula a -> String Source #

prettys :: Formula a -> ShowS Source #

type Root (Formula a) Source # 
Instance details

Defined in AutoProof.Internal.Formula.Types

type Root (Formula a) = Maybe a

Pretty-printing

prettyFormula :: PrettyPrintable a => Formula a -> String Source #

Get a pretty-printed representation of a propositional formula.

Examples

Expand
>>> prettyFormula $ Imp (Var "a") (Or (Var "b") (Lit False))
"a → (b ∨ ⊥)"