Safe Haskell	Safe-Inferred
Language	Haskell2010

PropaFP.Expression

Synopsis

data BinOp
- = Add
- | Sub
- | Mul
- | Div
- | Min
- | Max
- | Pow
- | Mod
data UnOp
- = Sqrt
- | Negate
- | Abs
- | Sin
- | Cos
data RoundingMode
- = RNE
- | RTP
- | RTN
- | RTZ
- | RNA
data E
- = EBinOp BinOp E E
- | EUnOp UnOp E
- | Lit Rational
- | Var String
- | PowI E Integer
- | Float32 RoundingMode E
- | Float64 RoundingMode E
- | Float RoundingMode E
- | Pi
- | RoundToInteger RoundingMode E
data ESafe
- = EStrict E
- | ENonStrict E
data Comp
- = Gt
- | Ge
- | Lt
- | Le
- | Eq
data Conn
- = And
- | Or
- | Impl
data F
- = FComp Comp E E
- | FConn Conn F F
- | FNot F
- | FTrue
- | FFalse
lengthF :: F -> Integer
lengthE :: E -> Integer
newtype Name = Name String
flipStrictness :: ESafe -> ESafe
negateSafeE :: ESafe -> ESafe
extractSafeE :: ESafe -> E
fmapESafe :: (E -> E) -> ESafe -> ESafe
fToECNF :: F -> [[ESafe]]
fToEDNF :: F -> [[ESafe]]
fToFDNF :: F -> [[F]]
eSafeToF :: ESafe -> F
eSafeDisjToF :: [ESafe] -> F
eSafeCNFToF :: [[ESafe]] -> F
eSafeCNFToDNF :: [[ESafe]] -> [[ESafe]]
simplifyE :: E -> E
simplifyF :: F -> F
simplifyEDoubleList :: [[E]] -> [[E]]
simplifyFDNF :: [[F]] -> [[F]]
fDNFToFDNFWithoutEq :: [[F]] -> [[F]] -> [[F]]
fDNFToEDNF :: [[F]] -> [[ESafe]]
simplifyFDoubleList :: [[F]] -> [[F]]
simplifyESafeDoubleList :: [[ESafe]] -> [[ESafe]]
computeE :: E -> [(String, Rational)] -> CN Double
computeQualifiedEs :: [([E], E)] -> [(String, Rational)] -> [CN Double]
computeEDisjunction :: [E] -> [(String, Rational)] -> [CN Double]
computeECNF :: [[E]] -> [(String, Rational)] -> [[CN Double]]
prettyShowESafeCNF :: [[ESafe]] -> String
prettyShowESafeDNF :: [[ESafe]] -> String
prettyShowFSafeDNF :: [[F]] -> String
prettyShowVC :: F -> TypedVarMap -> String
latexShowE :: E -> String
latexShowF :: F -> Integer -> String
latexShowComp :: Comp -> String
latexShowConn :: Conn -> String
prettyShowE :: E -> String
prettyShowECNF :: [[E]] -> String
prettyShowF :: F -> Integer -> String
prettyShowComp :: Comp -> String
prettyShowConn :: Conn -> String
extractVariablesE :: E -> [String]
extractVariablesF :: F -> [String]
extractVariablesECNF :: [[E]] -> [String]
hasVarsE :: E -> Bool
hasVarsF :: F -> Bool
hasFloatE :: E -> Bool
hasFloatF :: F -> Bool
substVarEWithLit :: E -> String -> Rational -> E
substVarFWithLit :: F -> String -> Rational -> F
substVarEWithE :: String -> E -> E -> E
substVarFWithE :: String -> F -> E -> F
transformImplications :: F -> F
removeVariableFreeComparisons :: F -> F
hasMinMaxAbsE :: E -> Bool
hasMinMaxAbsF :: F -> Bool
replaceEInE :: E -> E -> E -> E
replaceEInF :: F -> E -> E -> F
normalizeBoolean :: F -> F

Documentation

data BinOp Source #

Constructors

Add
Sub
Mul
Div
Min
Max
Pow
Mod

Instances

Instances details

Arbitrary BinOp Source #
Instance details Defined in PropaFP.Expression Methods arbitrary :: Gen BinOp # shrink :: BinOp -> [BinOp] #
Show BinOp Source #
Instance details Defined in PropaFP.Expression Methods showsPrec :: Int -> BinOp -> ShowS # show :: BinOp -> String # showList :: [BinOp] -> ShowS #
Eq BinOp Source #
Instance details Defined in PropaFP.Expression Methods (==) :: BinOp -> BinOp -> Bool # (/=) :: BinOp -> BinOp -> Bool #
Ord BinOp Source #
Instance details Defined in PropaFP.Expression Methods compare :: BinOp -> BinOp -> Ordering # (<) :: BinOp -> BinOp -> Bool # (<=) :: BinOp -> BinOp -> Bool # (>) :: BinOp -> BinOp -> Bool # (>=) :: BinOp -> BinOp -> Bool # max :: BinOp -> BinOp -> BinOp # min :: BinOp -> BinOp -> BinOp #

data UnOp Source #

Constructors

Sqrt
Negate
Abs
Sin
Cos

Instances

Instances details

Arbitrary UnOp Source #
Instance details Defined in PropaFP.Expression Methods arbitrary :: Gen UnOp # shrink :: UnOp -> [UnOp] #
Show UnOp Source #
Instance details Defined in PropaFP.Expression Methods showsPrec :: Int -> UnOp -> ShowS # show :: UnOp -> String # showList :: [UnOp] -> ShowS #
Eq UnOp Source #
Instance details Defined in PropaFP.Expression Methods (==) :: UnOp -> UnOp -> Bool # (/=) :: UnOp -> UnOp -> Bool #
Ord UnOp Source #
Instance details Defined in PropaFP.Expression Methods compare :: UnOp -> UnOp -> Ordering # (<) :: UnOp -> UnOp -> Bool # (<=) :: UnOp -> UnOp -> Bool # (>) :: UnOp -> UnOp -> Bool # (>=) :: UnOp -> UnOp -> Bool # max :: UnOp -> UnOp -> UnOp # min :: UnOp -> UnOp -> UnOp #

data RoundingMode Source #

Constructors

RNE
RTP
RTN
RTZ
RNA

Instances

Instances details

Arbitrary RoundingMode Source #
Instance details Defined in PropaFP.Expression Methods arbitrary :: Gen RoundingMode # shrink :: RoundingMode -> [RoundingMode] #
Show RoundingMode Source #
Instance details Defined in PropaFP.Expression Methods showsPrec :: Int -> RoundingMode -> ShowS # show :: RoundingMode -> String # showList :: [RoundingMode] -> ShowS #
Eq RoundingMode Source #
Instance details Defined in PropaFP.Expression Methods (==) :: RoundingMode -> RoundingMode -> Bool # (/=) :: RoundingMode -> RoundingMode -> Bool #
Ord RoundingMode Source #
Instance details Defined in PropaFP.Expression Methods compare :: RoundingMode -> RoundingMode -> Ordering # (<) :: RoundingMode -> RoundingMode -> Bool # (<=) :: RoundingMode -> RoundingMode -> Bool # (>) :: RoundingMode -> RoundingMode -> Bool # (>=) :: RoundingMode -> RoundingMode -> Bool # max :: RoundingMode -> RoundingMode -> RoundingMode # min :: RoundingMode -> RoundingMode -> RoundingMode #

data E Source #

The E type represents the inequality: expression :: E >= 0 TODO: Add rounding operator with certain epsilon/floating-point type

Constructors

EBinOp BinOp E E
EUnOp UnOp E
Lit Rational
Var String
PowI E Integer
Float32 RoundingMode E
Float64 RoundingMode E
Float RoundingMode E
Pi
RoundToInteger RoundingMode E

Instances

Instances details

Arbitrary E Source #
Instance details Defined in PropaFP.Expression Methods arbitrary :: Gen E # shrink :: E -> [E] #
Show E Source #
Instance details Defined in PropaFP.Expression Methods showsPrec :: Int -> E -> ShowS # show :: E -> String # showList :: [E] -> ShowS #
Eq E Source #
Instance details Defined in PropaFP.Expression Methods (==) :: E -> E -> Bool # (/=) :: E -> E -> Bool #
Ord E Source #
Instance details Defined in PropaFP.Expression Methods compare :: E -> E -> Ordering # (<) :: E -> E -> Bool # (<=) :: E -> E -> Bool # (>) :: E -> E -> Bool # (>=) :: E -> E -> Bool # max :: E -> E -> E # min :: E -> E -> E #

data ESafe Source #

Constructors

EStrict E
ENonStrict E

Instances

Instances details

Arbitrary ESafe Source #
Instance details Defined in PropaFP.Expression Methods arbitrary :: Gen ESafe # shrink :: ESafe -> [ESafe] #
Show ESafe Source #
Instance details Defined in PropaFP.Expression Methods showsPrec :: Int -> ESafe -> ShowS # show :: ESafe -> String # showList :: [ESafe] -> ShowS #
Eq ESafe Source #
Instance details Defined in PropaFP.Expression Methods (==) :: ESafe -> ESafe -> Bool # (/=) :: ESafe -> ESafe -> Bool #
Ord ESafe Source #
Instance details Defined in PropaFP.Expression Methods compare :: ESafe -> ESafe -> Ordering # (<) :: ESafe -> ESafe -> Bool # (<=) :: ESafe -> ESafe -> Bool # (>) :: ESafe -> ESafe -> Bool # (>=) :: ESafe -> ESafe -> Bool # max :: ESafe -> ESafe -> ESafe # min :: ESafe -> ESafe -> ESafe #

data Comp Source #

Constructors

Gt
Ge
Lt
Le
Eq

Instances

Instances details

Arbitrary Comp Source #
Instance details Defined in PropaFP.Expression Methods arbitrary :: Gen Comp # shrink :: Comp -> [Comp] #
Show Comp Source #
Instance details Defined in PropaFP.Expression Methods showsPrec :: Int -> Comp -> ShowS # show :: Comp -> String # showList :: [Comp] -> ShowS #
Eq Comp Source #
Instance details Defined in PropaFP.Expression Methods (==) :: Comp -> Comp -> Bool # (/=) :: Comp -> Comp -> Bool #
Ord Comp Source #
Instance details Defined in PropaFP.Expression Methods compare :: Comp -> Comp -> Ordering # (<) :: Comp -> Comp -> Bool # (<=) :: Comp -> Comp -> Bool # (>) :: Comp -> Comp -> Bool # (>=) :: Comp -> Comp -> Bool # max :: Comp -> Comp -> Comp # min :: Comp -> Comp -> Comp #

data Conn Source #

Constructors

And
Or
Impl

Instances

Instances details

Arbitrary Conn Source #
Instance details Defined in PropaFP.Expression Methods arbitrary :: Gen Conn # shrink :: Conn -> [Conn] #
Show Conn Source #
Instance details Defined in PropaFP.Expression Methods showsPrec :: Int -> Conn -> ShowS # show :: Conn -> String # showList :: [Conn] -> ShowS #
Eq Conn Source #
Instance details Defined in PropaFP.Expression Methods (==) :: Conn -> Conn -> Bool # (/=) :: Conn -> Conn -> Bool #
Ord Conn Source #
Instance details Defined in PropaFP.Expression Methods compare :: Conn -> Conn -> Ordering # (<) :: Conn -> Conn -> Bool # (<=) :: Conn -> Conn -> Bool # (>) :: Conn -> Conn -> Bool # (>=) :: Conn -> Conn -> Bool # max :: Conn -> Conn -> Conn # min :: Conn -> Conn -> Conn #

data F Source #

The F type is used to specify comparisons between E types and logical connectives between F types

Constructors

FComp Comp E E
FConn Conn F F
FNot F
FTrue
FFalse

Instances

Instances details

Arbitrary F Source #
Instance details Defined in PropaFP.Expression Methods arbitrary :: Gen F # shrink :: F -> [F] #
Show F Source #
Instance details Defined in PropaFP.Expression Methods showsPrec :: Int -> F -> ShowS # show :: F -> String # showList :: [F] -> ShowS #
Eq F Source #
Instance details Defined in PropaFP.Expression Methods (==) :: F -> F -> Bool # (/=) :: F -> F -> Bool #
Ord F Source #
Instance details Defined in PropaFP.Expression Methods compare :: F -> F -> Ordering # (<) :: F -> F -> Bool # (<=) :: F -> F -> Bool # (>) :: F -> F -> Bool # (>=) :: F -> F -> Bool # max :: F -> F -> F # min :: F -> F -> F #

lengthF :: F -> Integer Source #

lengthE :: E -> Integer Source #

newtype Name Source #

Constructors

Name String

Instances

Instances details

Arbitrary Name Source #
Instance details Defined in PropaFP.Expression Methods arbitrary :: Gen Name # shrink :: Name -> [Name] #
Show Name Source #
Instance details Defined in PropaFP.Expression Methods showsPrec :: Int -> Name -> ShowS # show :: Name -> String # showList :: [Name] -> ShowS #

flipStrictness :: ESafe -> ESafe Source #

negateSafeE :: ESafe -> ESafe Source #

Equivalent to E * -1 Example: ENonStrict e == e >= 0. negateSafeE (ENonStrict e) == e == -e 0 == (EStrict (EUnOp Negate e))

extractSafeE :: ESafe -> E Source #

fmapESafe :: (E -> E) -> ESafe -> ESafe Source #

fToECNF :: F -> [[ESafe]] Source #

fToEDNF :: F -> [[ESafe]] Source #

fToFDNF :: F -> [[F]] Source #

eSafeToF :: ESafe -> F Source #

eSafeDisjToF :: [ESafe] -> F Source #

eSafeCNFToF :: [[ESafe]] -> F Source #

eSafeCNFToDNF :: [[ESafe]] -> [[ESafe]] Source #

simplifyE :: E -> E Source #

Add bounds for any Float expressions addRoundingBounds :: E -> [[E]] addRoundingBounds (Float e significand) = [[exactExpression - machineEpsilon], [exactExpression + machineEpsilon]] where exactExpression = addRoundingBounds e machineEpsilon = 2^(-23) addRoundingBounds e = e

Various rules to simplify expressions

simplifyF :: F -> F Source #

simplifyEDoubleList :: [[E]] -> [[E]] Source #

simplifyFDNF :: [[F]] -> [[F]] Source #

fDNFToFDNFWithoutEq :: [[F]] -> [[F]] -> [[F]] Source #

fDNFToEDNF :: [[F]] -> [[ESafe]] Source #

simplifyFDoubleList :: [[F]] -> [[F]] Source #

simplifyESafeDoubleList :: [[ESafe]] -> [[ESafe]] Source #

computeE :: E -> [(String, Rational)] -> CN Double Source #

compute the value of E with Vars at specified points

computeQualifiedEs :: [([E], E)] -> [(String, Rational)] -> [CN Double] Source #

Given a list of qualified Es and points for all Vars, compute a list of valid values.

A value is the computed result of the second element of the tuple and is valid if all the expressions in the list at the first element of the tuple compute to be above 0.

computeEDisjunction :: [E] -> [(String, Rational)] -> [CN Double] Source #

computeECNF :: [[E]] -> [(String, Rational)] -> [[CN Double]] Source #

prettyShowESafeCNF :: [[ESafe]] -> String Source #

prettyShowESafeDNF :: [[ESafe]] -> String Source #

prettyShowFSafeDNF :: [[F]] -> String Source #

prettyShowVC :: F -> TypedVarMap -> String Source #

latexShowE :: E -> String Source #

latexShowF :: F -> Integer -> String Source #

latexShowComp :: Comp -> String Source #

latexShowConn :: Conn -> String Source #

prettyShowE :: E -> String Source #

Show an expression in a human-readable format Rationals are converted into doubles

prettyShowECNF :: [[E]] -> String Source #

Show a conjunction of expressions in a human-readable format This is shown as an AND with each disjunction tabbed in with an OR If there is only one term in a disjunction, the expression is shown without an OR

prettyShowF :: F -> Integer -> String Source #

prettyShowComp :: Comp -> String Source #

prettyShowConn :: Conn -> String Source #

extractVariablesE :: E -> [String] Source #

Extract all variables in an expression Will not return duplicationes

extractVariablesF :: F -> [String] Source #

Extract all variables in an expression Will not return duplicationes

extractVariablesECNF :: [[E]] -> [String] Source #

hasVarsE :: E -> Bool Source #

hasVarsF :: F -> Bool Source #

hasFloatE :: E -> Bool Source #

hasFloatF :: F -> Bool Source #