Picologic.AST

Documentation

data Expr

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

Data Expr

Ord Expr

newtype Ident

Constructors

Ident String

Instances

Eq Ident

Data Ident

Ord Ident

Show Ident

newtype Solutions

Constructors

Solutions [[Expr]]

type Ctx = Map Ident Bool

variables :: Expr -> [Ident]

Variables in expression

eval :: Ctx -> Expr -> Bool

Evaluate expression.

cnf :: Expr -> Expr

Conjunctive normal form. (May result in exponential growth)

nnf :: Expr -> Expr

Negation normal form. (May result in exponential growth)

simp :: Expr -> Expr

Remove tautologies.

isConst :: Expr -> Bool

Test if expression is constant.

propConst :: Expr -> Expr

Propagate constants (to simplify expression).

subst :: Map Ident Expr -> Expr -> Expr

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

partEval :: Ctx -> Expr -> Expr

Partially evaluate expression.