Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr

Simplification of expressions. The result of simplifying an expression e, is a new expression e', which satisfies the property:

if e is well-defined then e and e' will evaluate to the same type.

Documentation

crySimpExpr :: Expr -> Expr

Simplify an expression, if possible.

crySimpExprMaybe :: Expr -> Maybe Expr

Perform simplification from the leaves up. Returns Nothing if there were no changes.

data Sign

Constructors

Pos

Neg

Instances

Show Sign

Methods

showsPrec :: Int -> Sign -> ShowS

show :: Sign -> String

showList :: [Sign] -> ShowS

otherSign :: Sign -> Sign

signed :: Sign -> Integer -> Integer

splitSum :: Expr -> [(Sign, Expr)]

normSum :: Expr -> Expr

crySimpExprStep :: Expr -> Maybe Expr

crySimpExprStep1 :: Expr -> Maybe Expr

Make a simplification step, assuming the expression is well-formed.