Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Types.SMTPrint

Documentation

class ToHornSMT a where Source #

Methods

toHornSMT :: a -> Doc Source #

Instances

Instances details

ToHornSMT Pred Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods toHornSMT :: Pred -> Doc Source #
ToHornSMT Tag Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods toHornSMT :: Tag -> Doc Source #
ToHornSMT QualParam Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods toHornSMT :: QualParam -> Doc Source #
ToHornSMT Qualifier Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods toHornSMT :: Qualifier -> Doc Source #
ToHornSMT Rewrite Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods toHornSMT :: Rewrite -> Doc Source #
ToHornSMT Symbol Source #
Instance details Defined in Language.Fixpoint.Types.SMTPrint Methods toHornSMT :: Symbol -> Doc Source #
ToHornSMT Expr Source #
Instance details Defined in Language.Fixpoint.Types.SMTPrint Methods toHornSMT :: Expr -> Doc Source #
ToHornSMT KVar Source #
Instance details Defined in Language.Fixpoint.Types.SMTPrint Methods toHornSMT :: KVar -> Doc Source #
ToHornSMT Subst Source #
Instance details Defined in Language.Fixpoint.Types.SMTPrint Methods toHornSMT :: Subst -> Doc Source #
ToHornSMT DataCtor Source #
Instance details Defined in Language.Fixpoint.Types.SMTPrint Methods toHornSMT :: DataCtor -> Doc Source #
ToHornSMT DataDecl Source #
Instance details Defined in Language.Fixpoint.Types.SMTPrint Methods toHornSMT :: DataDecl -> Doc Source #
ToHornSMT DataField Source #
Instance details Defined in Language.Fixpoint.Types.SMTPrint Methods toHornSMT :: DataField -> Doc Source #
ToHornSMT FTycon Source #
Instance details Defined in Language.Fixpoint.Types.SMTPrint Methods toHornSMT :: FTycon -> Doc Source #
ToHornSMT Sort Source #
Instance details Defined in Language.Fixpoint.Types.SMTPrint Methods toHornSMT :: Sort -> Doc Source #
ToHornSMT (Bind a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods toHornSMT :: Bind a -> Doc Source #
ToHornSMT (Cstr a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods toHornSMT :: Cstr a -> Doc Source #
ToHornSMT (Query a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods toHornSMT :: Query a -> Doc Source #
ToHornSMT (Var a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods toHornSMT :: Var a -> Doc Source #
ToHornSMT a => ToHornSMT (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.SMTPrint Methods toHornSMT :: Located a -> Doc Source #
ToHornSMT a => ToHornSMT [a] Source #
Instance details Defined in Language.Fixpoint.Types.SMTPrint Methods toHornSMT :: [a] -> Doc Source #
ToHornSMT a => ToHornSMT (Symbol, a) Source #
Instance details Defined in Language.Fixpoint.Types.SMTPrint Methods toHornSMT :: (Symbol, a) -> Doc Source #

toHornWithBinders :: (ToHornSMT a, ToHornSMT t) => Doc -> [(Symbol, t)] -> a -> Doc Source #

toHornMany :: [Doc] -> Doc Source #

toHornAnd :: (a -> Doc) -> [a] -> Doc Source #

toHornSort :: Sort -> Doc Source #

toHornAbsApp :: Sort -> Doc Source #

toHornFApp :: [Sort] -> Doc Source #

toHornExpr :: Expr -> Doc Source #

toHornOp :: ToHornSMT a => Doc -> [a] -> Doc Source #