Safe Haskell	None
Language	Haskell2010

What4.Serialize.Normalize

Description

Normalization and equivalence checking for expressions

Synopsis

normSymFn :: forall sym (st :: Type -> Type) fs t (args :: Ctx BaseType) (ret :: BaseType). sym ~ ExprBuilder t st fs => sym -> ExprSymFn t args ret -> Assignment (Expr t) args -> IO (Expr t ret)
normExpr :: forall sym (st :: Type -> Type) fs t (tp :: BaseType). sym ~ ExprBuilder t st fs => sym -> Expr t tp -> IO (Expr t tp)
testEquivSymFn :: forall sym (st :: Type -> Type) fs t (args :: Ctx BaseType) (ret :: BaseType) (args' :: Ctx BaseType) (ret' :: BaseType). sym ~ ExprBuilder t st fs => sym -> SymFn sym args ret -> SymFn sym args' ret' -> IO ExprEquivResult
testEquivExpr :: forall sym (st :: Type -> Type) fs t (tp :: BaseType) (tp' :: BaseType). sym ~ ExprBuilder t st fs => sym -> Expr t tp -> Expr t tp' -> IO ExprEquivResult
data ExprEquivResult
- = ExprEquivalent
- | ExprNormEquivalent
- | ExprUnequal

Documentation

normSymFn :: forall sym (st :: Type -> Type) fs t (args :: Ctx BaseType) (ret :: BaseType). sym ~ ExprBuilder t st fs => sym -> ExprSymFn t args ret -> Assignment (Expr t) args -> IO (Expr t ret) Source #

Apply some normalizations to make function call arguments more readable. Examples include:

Avoid wrapping single literals in a SemiRingLiteral and just represent them as a bare integer literals
Attempt to reduce function calls with constant arguments where possible

normExpr :: forall sym (st :: Type -> Type) fs t (tp :: BaseType). sym ~ ExprBuilder t st fs => sym -> Expr t tp -> IO (Expr t tp) Source #

testEquivSymFn :: forall sym (st :: Type -> Type) fs t (args :: Ctx BaseType) (ret :: BaseType) (args' :: Ctx BaseType) (ret' :: BaseType). sym ~ ExprBuilder t st fs => sym -> SymFn sym args ret -> SymFn sym args' ret' -> IO ExprEquivResult Source #

testEquivExpr :: forall sym (st :: Type -> Type) fs t (tp :: BaseType) (tp' :: BaseType). sym ~ ExprBuilder t st fs => sym -> Expr t tp -> Expr t tp' -> IO ExprEquivResult Source #

Constructors