-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Generate Haskell code from a type. Library extracted from djinn package.
--   
--   Djinn uses an theorem prover for intuitionistic propositional logic to
--   generate a Haskell expression when given a type. This is a library
--   extracted from Djinn sources.
@package djinn-lib
@version 0.0.1.2

module Djinn.LJTFormula
newtype Symbol
Symbol :: String -> Symbol
data Formula
Conj :: [Formula] -> Formula
Disj :: [(ConsDesc, Formula)] -> Formula
(:->) :: Formula -> Formula -> Formula
PVar :: Symbol -> Formula
(<->) :: Formula -> Formula -> Formula
(&) :: Formula -> Formula -> Formula
(|:) :: Formula -> Formula -> Formula
fnot :: Formula -> Formula
false :: Formula
true :: Formula
data ConsDesc
ConsDesc :: String -> Int -> ConsDesc
data Term
Var :: Symbol -> Term
Lam :: Symbol -> Term -> Term
Apply :: Term -> Term -> Term
Ctuple :: Int -> Term
Csplit :: Int -> Term
Cinj :: ConsDesc -> Int -> Term
Ccases :: [ConsDesc] -> Term
Xsel :: Int -> Int -> Term -> Term
applys :: Term -> [Term] -> Term
freeVars :: Term -> [Symbol]
instance Eq Symbol
instance Ord Symbol
instance Eq ConsDesc
instance Ord ConsDesc
instance Show ConsDesc
instance Eq Formula
instance Ord Formula
instance Eq Term
instance Ord Term
instance Show Term
instance Show Formula
instance Show Symbol

module Djinn.LJT
provable :: Formula -> Bool
prove :: MoreSolutions -> [(Symbol, Formula)] -> Formula -> [Proof]
type Proof = Term
type MoreSolutions = Bool
instance Eq AtomF
instance Eq NestImp
instance Show Antecedent
instance Show AtomImp
instance Show NestImp
instance Show AtomF
instance MonadPlus P
instance Alternative P
instance Functor P
instance Monad P
instance Applicative P

module Djinn.HTypes
data HKind
KStar :: HKind
KArrow :: HKind -> HKind -> HKind
KVar :: Int -> HKind
data HType
HTApp :: HType -> HType -> HType
HTVar :: HSymbol -> HType
HTCon :: HSymbol -> HType
HTTuple :: [HType] -> HType
HTArrow :: HType -> HType -> HType
HTUnion :: [(HSymbol, [HType])] -> HType
HTAbstract :: HSymbol -> HKind -> HType
type HSymbol = String
hTypeToFormula :: [(HSymbol, ([HSymbol], HType, a))] -> HType -> Formula
pHSymbol :: Bool -> ReadP HSymbol
pHType :: ReadP HType
pHDataType :: ReadP HType
pHTAtom :: ReadP HType
pHKind :: ReadP HKind
prHSymbolOp :: HSymbol -> String
htNot :: HSymbol -> HType
isHTUnion :: HType -> Bool
getHTVars :: HType -> [HSymbol]
substHT :: [(HSymbol, HType)] -> HType -> HType
data HClause
HClause :: HSymbol -> [HPat] -> HExpr -> HClause
data HPat
HPVar :: HSymbol -> HPat
HPCon :: HSymbol -> HPat
HPTuple :: [HPat] -> HPat
HPAt :: HSymbol -> HPat -> HPat
HPApply :: HPat -> HPat -> HPat
data HExpr
HELam :: [HPat] -> HExpr -> HExpr
HEApply :: HExpr -> HExpr -> HExpr
HECon :: HSymbol -> HExpr
HEVar :: HSymbol -> HExpr
HETuple :: [HExpr] -> HExpr
HECase :: HExpr -> [(HPat, HExpr)] -> HExpr
hPrClause :: HClause -> String
hPrExpr :: HExpr -> String
termToHExpr :: Term -> HExpr
termToHClause :: HSymbol -> Term -> HClause
getBinderVars :: HClause -> [HSymbol]
instance Eq HKind
instance Show HKind
instance Eq HType
instance Show HPat
instance Eq HPat
instance Show HExpr
instance Eq HExpr
instance Show HClause
instance Eq HClause
instance Read HType
instance Show HType

module Djinn.HCheck
htCheckEnv :: [(HSymbol, ([HSymbol], HType, a))] -> Either String [(HSymbol, ([HSymbol], HType, HKind))]
htCheckType :: [(HSymbol, ([HSymbol], HType, HKind))] -> HType -> Either String ()
