language-sally-0.1.0.0: AST and pretty printer for Sally

CopyrightBenjamin Jones <bjones@galois.com> 2016-2017
LicenseBSD3
Maintainerbjones@galois.com
Stabilityexperimental
Portabilityunknown
Safe HaskellSafe
LanguageHaskell2010

Language.Sally.Expr

Contents

Description

Better constructors for Sally expresssions and predicates than the raw ones defined in Language.Sally.Types.

Synopsis

better constructors

boolExpr :: Bool -> SallyExpr Source #

Create a constant boolean expression.

boolPred :: Bool -> SallyPred Source #

Create a constant boolean predicate.

intExpr :: Integral a => a -> SallyExpr Source #

Create a constant integer expression.

zeroExpr :: SallyExpr Source #

Create an expression for zero as an integer in Sally.

oneExpr :: SallyExpr Source #

Create an expression for one as an integer in Sally.

realExpr :: Real a => a -> SallyExpr Source #

Create a constant real expression.

addExpr :: SallyExpr -> SallyExpr -> SallyExpr Source #

Better constructor for adding expressions TODO maintain normal form

multExpr :: SallyExpr -> SallyExpr -> SallyExpr Source #

Better constructor for multiplying expressions; checks that one of the operands is a constant.

divExpr :: SallyExpr -> SallyExpr -> SallyExpr Source #

Better constructor for dividing expressions; checks that the denominator is a constant.

notExpr :: SallyExpr -> SallyExpr Source #

Create the expression that is the boolean negation of the given one.

eqExpr :: SallyExpr -> SallyExpr -> SallyExpr Source #

Create the expression equating two given expressions.

neqExpr :: SallyExpr -> SallyExpr -> SallyExpr Source #

Create the expression representing non-equality.

ltExpr :: SallyExpr -> SallyExpr -> SallyExpr Source #

a ltExpr b represents the expression a < b.

leqExpr :: SallyExpr -> SallyExpr -> SallyExpr Source #

a leqExpr b represents the expression a <= b.

gtExpr :: SallyExpr -> SallyExpr -> SallyExpr Source #

a gtExpr b represents the expression a > b.

geqExpr :: SallyExpr -> SallyExpr -> SallyExpr Source #

a geqExpr b represents the expression a >= b.

muxExpr :: SallyExpr -> SallyExpr -> SallyExpr -> SallyExpr Source #

Create an if-then-else expression: mux b x y represents the statement "if b then x else y".

andExprs :: [SallyExpr] -> SallyExpr Source #

Form the conjunction of the given expressions (which should be predicates, but this is not checked).

andPreds :: [SallyPred] -> SallyPred Source #

And over multiple predicates, doing some small inline simplification

orExprs :: [SallyExpr] -> SallyExpr Source #

Form the disjunction of the given expressions (which should be predicates, but this is not checked).

varExpr :: SallyVar -> SallyExpr Source #

Create a variable expression.

varExpr' :: Name -> SallyExpr Source #

Create a variable expression from a name.

xorExpr :: SallyExpr -> SallyExpr -> SallyExpr Source #

Create the XOR of two Sally expressions.

complex expression builders

minExpr :: [SallyExpr] -> Maybe SallyExpr -> SallyExpr Source #

Given a non-empty finite list of expressions, build an expression to compute their minimum. The second argument is a special value which, if present causes expressions in the list with this value to be ignored in the calculation. If the input list contains only the special value, then the special value itself is returned.

countExpr :: SallyExpr -> [SallyExpr] -> SallyExpr Source #

Build a Sally expression representing the number of times a particular item appears in a list of expressions.

expression rewriting

constFold :: SallyExpr -> SallyExpr Source #

A basic top-down recursive constant folding function.

simplifyAnds :: SallyPred -> SallyPred Source #

Top-down rewriting of and terms including constant folding and constructor reduction.

simplifyOrs :: SallyPred -> SallyPred Source #

Top-down rewriting of or terms including constant folding and constructor reduction.

flattenAnds :: Seq SallyPred -> Seq SallyPred Source #

Recursively flatten a tree of and expressions into an and sequence.

flattenOrs :: Seq SallyPred -> Seq SallyPred Source #

Recursively flatten a tree of or expressions into an or sequence.