ideas-math-types-1.1: Common types for mathematical domain reasoners

Maintainer bastiaan.heeren@ou.nl provisional portable (depends on ghc) None Haskell2010

Domain.Logic.Formula

Description

Synopsis

# Documentation

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

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

For simple use, we assume the variables to be strings

data Logic a Source #

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
 Source # Instance detailsDefined in Domain.Logic.Formula Methodsfmap :: (a -> b) -> Logic a -> Logic b #(<\$) :: a -> Logic b -> Logic a # Source # Instance detailsDefined in Domain.Logic.Formula Methodsfold :: 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 # Source # Instance detailsDefined in Domain.Logic.Formula Methodstraverse :: 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) # Source # Instance detailsDefined in Domain.Logic.Generator Methodsshrink :: SLogic -> [SLogic] # Source # Instance detailsDefined in Domain.Logic.Generator Methodscoarbitrary :: SLogic -> Gen b -> Gen b # Source # Instance detailsDefined in Domain.Logic.Formula Methodssingleton :: a -> Logic a #getSingleton :: Logic a -> Maybe a # Eq a => Eq (Logic a) Source # Instance detailsDefined in Domain.Logic.Formula Methods(==) :: Logic a -> Logic a -> Bool #(/=) :: Logic a -> Logic a -> Bool # Ord a => Ord (Logic a) Source # Instance detailsDefined in Domain.Logic.Formula Methodscompare :: 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) Source # Instance detailsDefined in Domain.Logic.Formula MethodsshowsPrec :: Int -> Logic a -> ShowS #show :: Logic a -> String #showList :: [Logic a] -> ShowS # Source # Instance detailsDefined in Domain.Logic.Formula Methodsdifferent :: (Logic a, Logic a) # IsTerm a => IsTerm (Logic a) Source # Instance detailsDefined in Domain.Logic.Formula MethodstoTerm :: 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) Source # Instance detailsDefined in Domain.Logic.Formula MethodstoLatex :: Logic a -> Latex #toLatexPrec :: Int -> Logic a -> Latex #toLatexList :: [Logic a] -> Latex # Source # Instance detailsDefined in Domain.Logic.Formula Methodstrue :: Logic a #false :: Logic a #fromBool :: Bool -> Logic a #isTrue :: Logic a -> Bool #isFalse :: Logic a -> Bool # Boolean (Logic a) Source # Instance detailsDefined in Domain.Logic.Formula Methods(<&&>) :: Logic a -> Logic a -> Logic a #(<||>) :: Logic a -> Logic a -> Logic a #complement :: Logic a -> Logic a # Source # Instance detailsDefined in Domain.Logic.Formula Methodsuniplate :: 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) # Source # Instance detailsDefined in Domain.Logic.Formula MethodsisAnd :: Logic a -> Maybe (Logic a, Logic a) Source #isOr :: Logic a -> Maybe (Logic a, Logic a) Source #isComplement :: Logic a -> Maybe (Logic a) Source #

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

foldLogic is the standard fold for Logic.

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

Pretty-printer for propositions

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

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

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 Source #

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 Source #

isAtomic :: Logic a -> Bool Source #

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

isDNF :: Logic a -> Bool Source #

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 Source #

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

Count the number of equivalences

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

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