cryptol-2.4.0: Cryptol: The Language of Cryptography

Copyright | (c) 2015-2016 Galois Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe
Language | Haskell98

Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr

Description

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.

Synopsis

- crySimpExpr :: Expr -> Expr
- crySimpExprMaybe :: Expr -> Maybe Expr
- data Sign
  - = Pos
  - | Neg
- otherSign :: Sign -> Sign
- signed :: Sign -> Integer -> Integer
- splitSum :: Expr -> [(Sign, Expr)]
- normSum :: Expr -> Expr
- crySimpExprStep :: Expr -> Maybe Expr
- crySimpExprStep1 :: Expr -> Maybe Expr

# Documentation

crySimpExpr :: Expr -> Expr Source #

Simplify an expression, if possible.

crySimpExprMaybe :: Expr -> Maybe Expr Source #

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

data Sign Source #

Constructors

Pos |
Neg |

Instances

Show Sign Source # |
Methods showsPrec :: Int -> Sign -> ShowS # show :: Sign -> String # showList :: [Sign] -> ShowS #

otherSign :: Sign -> Sign Source #

signed :: Sign -> Integer -> Integer Source #

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

normSum :: Expr -> Expr Source #

crySimpExprStep :: Expr -> Maybe Expr Source #

crySimpExprStep1 :: Expr -> Maybe Expr Source #

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