Domain.Logic.Formula

Documentation

type LogicAlg b a = (b -> a, a -> a -> a, a -> a -> a, a -> a -> a, a -> a -> a, a -> a, a, a)

The type LogicAlg is the algebra for the data type Logic | Used in the fold for Logic.

type SLogic = Logic ShowString

For simple use, we assume the variables to be strings

data Logic a

The data type Logic is the abstract syntax for the domain | of logic expressions.

Constructors

Var a

(Logic a) :->: (Logic a) infixr 3

(Logic a) :<->: (Logic a) infixr 2

(Logic a) :&&: (Logic a) infixr 5

(Logic a) :||: (Logic a) infixr 4

Not (Logic a)

T

F

Instances

Functor Logic

Defined in Domain.Logic.Formula

Methods

fmap :: (a -> b) -> Logic a -> Logic b

(<$) :: a -> Logic b -> Logic a

Foldable Logic

Defined in Domain.Logic.Formula

Methods

fold :: Monoid m => Logic m -> m

foldMap :: Monoid m => (a -> m) -> Logic a -> m

foldr :: (a -> b -> b) -> b -> Logic a -> b

foldr' :: (a -> b -> b) -> b -> Logic a -> b

foldl :: (b -> a -> b) -> b -> Logic a -> b

foldl' :: (b -> a -> b) -> b -> Logic a -> b

foldr1 :: (a -> a -> a) -> Logic a -> a

foldl1 :: (a -> a -> a) -> Logic a -> a

toList :: Logic a -> [a]

null :: Logic a -> Bool

length :: Logic a -> Int

elem :: Eq a => a -> Logic a -> Bool

maximum :: Ord a => Logic a -> a

minimum :: Ord a => Logic a -> a

sum :: Num a => Logic a -> a

product :: Num a => Logic a -> a

Traversable Logic

Defined in Domain.Logic.Formula

Methods

traverse :: Applicative f => (a -> f b) -> Logic a -> f (Logic b)

sequenceA :: Applicative f => Logic (f a) -> f (Logic a)

mapM :: Monad m => (a -> m b) -> Logic a -> m (Logic b)

sequence :: Monad m => Logic (m a) -> m (Logic a)

Arbitrary SLogic

Defined in Domain.Logic.Generator

Methods

arbitrary :: Gen SLogic

shrink :: SLogic -> [SLogic]

CoArbitrary SLogic

Defined in Domain.Logic.Generator

Methods

coarbitrary :: SLogic -> Gen b -> Gen b

Container Logic

Defined in Domain.Logic.Formula

Methods

singleton :: a -> Logic a

getSingleton :: Logic a -> Maybe a

Eq a => Eq (Logic a)

Defined in Domain.Logic.Formula

Methods

(==) :: Logic a -> Logic a -> Bool

(/=) :: Logic a -> Logic a -> Bool

Ord a => Ord (Logic a)

Defined in Domain.Logic.Formula

Methods

compare :: Logic a -> Logic a -> Ordering

(<) :: Logic a -> Logic a -> Bool

(<=) :: Logic a -> Logic a -> Bool

(>) :: Logic a -> Logic a -> Bool

(>=) :: Logic a -> Logic a -> Bool

max :: Logic a -> Logic a -> Logic a

min :: Logic a -> Logic a -> Logic a

Show a => Show (Logic a)

Defined in Domain.Logic.Formula

Methods

showsPrec :: Int -> Logic a -> ShowS

show :: Logic a -> String

showList :: [Logic a] -> ShowS

Different (Logic a)

Defined in Domain.Logic.Formula

Methods

different :: (Logic a, Logic a)

IsTerm a => IsTerm (Logic a)

Defined in Domain.Logic.Formula

Methods

toTerm :: Logic a -> Term

toTermList :: [Logic a] -> Term

fromTerm :: MonadPlus m => Term -> m (Logic a)

fromTermList :: MonadPlus m => Term -> m [Logic a]

ToLatex a => ToLatex (Logic a)

Defined in Domain.Logic.Formula

Methods

toLatex :: Logic a -> Latex

toLatexPrec :: Int -> Logic a -> Latex

toLatexList :: [Logic a] -> Latex

BoolValue (Logic a)

Defined in Domain.Logic.Formula

Methods

true :: Logic a

false :: Logic a

fromBool :: Bool -> Logic a

isTrue :: Logic a -> Bool

isFalse :: Logic a -> Bool

Boolean (Logic a)

Defined in Domain.Logic.Formula

Methods

(<&&>) :: Logic a -> Logic a -> Logic a

(<||>) :: Logic a -> Logic a -> Logic a

complement :: Logic a -> Logic a

Uniplate (Logic a)

Defined in Domain.Logic.Formula

Methods

uniplate :: Logic a -> (Str (Logic a), Str (Logic a) -> Logic a)

descend :: (Logic a -> Logic a) -> Logic a -> Logic a

descendM :: Monad m => (Logic a -> m (Logic a)) -> Logic a -> m (Logic a)

CoBoolean (Logic a)

Defined in Domain.Logic.Formula

Methods

isAnd :: Logic a -> Maybe (Logic a, Logic a)

isOr :: Logic a -> Maybe (Logic a, Logic a)

isComplement :: Logic a -> Maybe (Logic a)

foldLogic :: LogicAlg b a -> Logic b -> a

foldLogic is the standard fold for Logic.

ppLogic :: Show a => Logic a -> String

Pretty-printer for propositions

ppLogicPrio :: Show a => Int -> Logic a -> String

catLogic :: Logic (Logic a) -> Logic a

The monadic join for logic

evalLogic :: (a -> Bool) -> Logic a -> Bool

evalLogic takes a function that gives a logic value to a variable, | and a Logic expression, and evaluates the boolean expression.

eqLogic :: Eq a => Logic a -> Logic a -> Bool

eqLogic determines whether or not two Logic expression are logically | equal, by evaluating the logic expressions on all valuations.

tautology :: Eq a => Logic a -> Bool

isNot :: Logic a -> Bool

isAtomic :: Logic a -> Bool

A Logic expression is atomic if it is a variable or a constant True or False.

isDNF :: Logic a -> Bool

Functions isDNF, and isCNF determine whether or not a Logix expression | is in disjunctive normal form, or conjunctive normal form, respectively.

isCNF :: Logic a -> Bool

Functions isDNF, and isCNF determine whether or not a Logix expression | is in disjunctive normal form, or conjunctive normal form, respectively.

countEquivalences :: Logic a -> Int

Count the number of equivalences

varsLogic :: Eq a => Logic a -> [a]

Function varsLogic returns the variables that appear in a Logic expression.

trueSymbol :: Symbol

falseSymbol :: Symbol

notSymbol :: Symbol

impliesSymbol :: Symbol

equivalentSymbol :: Symbol

andSymbol :: Symbol

orSymbol :: Symbol

module Domain.Algebra.Boolean