djinn-lib-0.0.1.4: Generate Haskell code from a type. Library extracted from djinn package.
Safe HaskellSafe-Inferred
LanguageHaskell98

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 #