picologic-0.3.0: Utilities for symbolic predicate logic expressions

Safe HaskellSafe
LanguageHaskell2010

Picologic.AST

Synopsis

Documentation

data Expr Source #

Constructors

Var Ident

Variable

Neg Expr

Logical negation

Conj Expr Expr

Logical conjunction

Disj Expr Expr

Logical disjunction

Iff Expr Expr

Logical biconditional

Implies Expr Expr

Material implication

Top

Constant true

Bottom

Constant false

Instances

Eq Expr Source # 

Methods

(==) :: Expr -> Expr -> Bool #

(/=) :: Expr -> Expr -> Bool #

Data Expr Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Expr -> c Expr #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Expr #

toConstr :: Expr -> Constr #

dataTypeOf :: Expr -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Expr) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr) #

gmapT :: (forall b. Data b => b -> b) -> Expr -> Expr #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r #

gmapQ :: (forall d. Data d => d -> u) -> Expr -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Expr -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Expr -> m Expr #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr #

Ord Expr Source # 

Methods

compare :: Expr -> Expr -> Ordering #

(<) :: Expr -> Expr -> Bool #

(<=) :: Expr -> Expr -> Bool #

(>) :: Expr -> Expr -> Bool #

(>=) :: Expr -> Expr -> Bool #

max :: Expr -> Expr -> Expr #

min :: Expr -> Expr -> Expr #

newtype Ident Source #

Constructors

Ident String 

Instances

Eq Ident Source # 

Methods

(==) :: Ident -> Ident -> Bool #

(/=) :: Ident -> Ident -> Bool #

Data Ident Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Ident -> c Ident #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Ident #

toConstr :: Ident -> Constr #

dataTypeOf :: Ident -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Ident) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ident) #

gmapT :: (forall b. Data b => b -> b) -> Ident -> Ident #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r #

gmapQ :: (forall d. Data d => d -> u) -> Ident -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Ident -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Ident -> m Ident #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Ident -> m Ident #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Ident -> m Ident #

Ord Ident Source # 

Methods

compare :: Ident -> Ident -> Ordering #

(<) :: Ident -> Ident -> Bool #

(<=) :: Ident -> Ident -> Bool #

(>) :: Ident -> Ident -> Bool #

(>=) :: Ident -> Ident -> Bool #

max :: Ident -> Ident -> Ident #

min :: Ident -> Ident -> Ident #

Show Ident Source # 

Methods

showsPrec :: Int -> Ident -> ShowS #

show :: Ident -> String #

showList :: [Ident] -> ShowS #

newtype Solutions Source #

Constructors

Solutions [[Expr]] 

variables :: Expr -> [Ident] Source #

Variables in expression

eval :: Ctx -> Expr -> Bool Source #

Evaluate expression.

cnf :: Expr -> Expr Source #

Conjunctive normal form. (May result in exponential growth)

nnf :: Expr -> Expr Source #

Negation normal form. (May result in exponential growth)

simp :: Expr -> Expr Source #

Remove tautologies.

isConst :: Expr -> Bool Source #

Test if expression is constant.

propConst :: Expr -> Expr Source #

Propagate constants (to simplify expression).

subst :: Map Ident Expr -> Expr -> Expr Source #

Substitute expressions for variables. This doesn't resolve any potential variable name conflicts.

partEval :: Ctx -> Expr -> Expr Source #

Partially evaluate expression.