Safe Haskell | None |
---|---|
Language | Haskell2010 |
- theoryBoolOpToIf :: Ord a => Theory a -> Theory a
- formulaBoolOpToIf :: Ord a => Expr a -> Expr a
- hasBoolType :: Ord a => Expr a -> Bool
- boolOpToIf :: (Ord a, TransformBi (Expr a) (f a)) => f a -> f a
- ifToBoolOp :: TransformBi (Expr a) (f a) => f a -> f a
- data BoolNames a = BoolNames {
- boolName :: a
- trueName :: a
- falseName :: a
- isTrueName :: a
- isFalseName :: a
- freshBoolNames :: Name a => Fresh (BoolNames a)
- boolGbl :: BoolNames a -> Bool -> Global a
- boolExpr :: BoolNames a -> Bool -> Expr a
- removeBuiltinBoolFrom :: forall f a. (TransformBi (Type a) (f a), TransformBi (Pattern a) (f a), TransformBi (Head a) (f a)) => BoolNames a -> f a -> f a
- removeBuiltinBoolWith :: Ord a => BoolNames a -> Theory a -> Theory a
- removeBuiltinBool :: Name a => Theory a -> Fresh (Theory a)
Documentation
theoryBoolOpToIf :: Ord a => Theory a -> Theory a Source
Transforms boolean operators to if, but not in expression contexts.
formulaBoolOpToIf :: Ord a => Expr a -> Expr a Source
hasBoolType :: Ord a => Expr a -> Bool Source
boolOpToIf :: (Ord a, TransformBi (Expr a) (f a)) => f a -> f a Source
Transforms and
, or
, =>
, not
and =
and distinct
on Bool
into ite
(i.e. match
)
ifToBoolOp :: TransformBi (Expr a) (f a) => f a -> f a Source
Transforms ite
(match
) on boolean literals in the branches
into the corresponding builtin boolean function.
Names to replace the builtin boolean type with
BoolNames | |
|
freshBoolNames :: Name a => Fresh (BoolNames a) Source
removeBuiltinBoolFrom :: forall f a. (TransformBi (Type a) (f a), TransformBi (Pattern a) (f a), TransformBi (Head a) (f a)) => BoolNames a -> f a -> f a Source