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

Instances details

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

data Formula Source #

Constructors

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

#### Instances

Instances details

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

(<->) :: 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

Instances details

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

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

Instances details

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

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

freeVars :: Term -> [Symbol] Source #