djinn-lib-0.0.1.3: Generate Haskell code from a type. Library extracted from djinn package.

Safe Haskell | Safe
Language | Haskell98

Djinn.LJTFormula

# Documentation

newtype Symbol Source #

Constructors

Symbol String |

Instances

Eq Symbol Source # |
Instance details Defined in Djinn.LJTFormula Methods (==) :: Symbol -> Symbol -> Bool Source # (/=) :: Symbol -> Symbol -> Bool Source #
Ord Symbol Source # |
Instance details Defined in Djinn.LJTFormula Methods compare :: Symbol -> Symbol -> Ordering Source # (<) :: Symbol -> Symbol -> Bool Source # (<=) :: Symbol -> Symbol -> Bool Source # (>) :: Symbol -> Symbol -> Bool Source # (>=) :: Symbol -> Symbol -> Bool Source # max :: Symbol -> Symbol -> Symbol Source # min :: Symbol -> Symbol -> Symbol Source #
Show Symbol Source # |
Instance details Defined in Djinn.LJTFormula Methods showsPrec :: Int -> Symbol -> ShowS Source # show :: Symbol -> String Source # showList :: [Symbol] -> ShowS Source #

data Formula Source #

Constructors

Conj [Formula] |
Disj [(ConsDesc, Formula)] |
Formula :-> Formula infixr 2 |
PVar Symbol |

Instances

Eq Formula Source # |
Instance details Defined in Djinn.LJTFormula Methods (==) :: Formula -> Formula -> Bool Source # (/=) :: Formula -> Formula -> Bool Source #
Ord Formula Source # |
Instance details Defined in Djinn.LJTFormula Methods compare :: Formula -> Formula -> Ordering Source # (<) :: Formula -> Formula -> Bool Source # (<=) :: Formula -> Formula -> Bool Source # (>) :: Formula -> Formula -> Bool Source # (>=) :: Formula -> Formula -> Bool Source # max :: Formula -> Formula -> Formula Source # min :: Formula -> Formula -> Formula Source #
Show Formula Source # |
Instance details Defined in Djinn.LJTFormula Methods showsPrec :: Int -> Formula -> ShowS Source # show :: Formula -> String Source # showList :: [Formula] -> ShowS Source #

(<->) :: Formula -> Formula -> Formula infix 2 Source #

(&) :: Formula -> Formula -> Formula infixl 4 Source #

(|:) :: Formula -> Formula -> Formula infixl 3 Source #

fnot :: Formula -> Formula Source #

false :: Formula Source #

true :: Formula Source #

data ConsDesc Source #

Constructors

ConsDesc String Int |

Instances

Eq ConsDesc Source # |
Instance details Defined in Djinn.LJTFormula Methods (==) :: ConsDesc -> ConsDesc -> Bool Source # (/=) :: ConsDesc -> ConsDesc -> Bool Source #
Ord ConsDesc Source # |
Instance details Defined in Djinn.LJTFormula Methods compare :: ConsDesc -> ConsDesc -> Ordering Source # (<) :: ConsDesc -> ConsDesc -> Bool Source # (<=) :: ConsDesc -> ConsDesc -> Bool Source # (>) :: ConsDesc -> ConsDesc -> Bool Source # (>=) :: ConsDesc -> ConsDesc -> Bool Source # max :: ConsDesc -> ConsDesc -> ConsDesc Source # min :: ConsDesc -> ConsDesc -> ConsDesc Source #
Show ConsDesc Source # |
Instance details Defined in Djinn.LJTFormula Methods showsPrec :: Int -> ConsDesc -> ShowS Source # show :: ConsDesc -> String Source # showList :: [ConsDesc] -> ShowS Source #

data Term Source #

Constructors

Var Symbol |
Lam Symbol Term |
Apply Term Term |
Ctuple Int |
Csplit Int |
Cinj ConsDesc Int |
Ccases [ConsDesc] |
Xsel Int Int Term |

Instances

Eq Term Source # |
Instance details Defined in Djinn.LJTFormula Methods (==) :: Term -> Term -> Bool Source # (/=) :: Term -> Term -> Bool Source #
Ord Term Source # |
Instance details Defined in Djinn.LJTFormula Methods compare :: Term -> Term -> Ordering Source # (<) :: Term -> Term -> Bool Source # (<=) :: Term -> Term -> Bool Source # (>) :: Term -> Term -> Bool Source # (>=) :: Term -> Term -> Bool Source # max :: Term -> Term -> Term Source # min :: Term -> Term -> Term Source #
Show Term Source # |
Instance details Defined in Djinn.LJTFormula Methods showsPrec :: Int -> Term -> ShowS Source # show :: Term -> String Source # showList :: [Term] -> ShowS Source #

applys :: Term -> [Term] -> Term Source #

freeVars :: Term -> [Symbol] Source #