Safe Haskell	Safe-Inferred
Language	Haskell2010

What4.Serialize.Normalize

Description

Normalization and equivalence checking for expressions

Synopsis

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

Documentation

normSymFn :: forall sym st fs t args ret. 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 fs t tp. sym ~ ExprBuilder t st fs => sym -> Expr t tp -> IO (Expr t tp) Source #

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

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

Constructors