Safe Haskell	Safe-Inferred

Language.Boogie.Intervals

Description

Lattice of integer intervals

Synopsis

Documentation

class Eq a => Lattice a whereSource

Lattice type class

Methods

top Source

Arguments

:: a

Top

bot Source

Arguments

:: a

Bottom

(<:)Source

Arguments

:: a
-> a
-> Bool	Partial order

join Source

Arguments

:: a
-> a
-> a	Least upper bound

meet Source

Arguments

:: a
-> a
-> a	Greatest lower bound

Instances

Lattice Interval

data Extended Source

Integers extended with infinity

Constructors

NegInf
Finite Integer
Inf

Instances

Eq Extended
Num Extended
Ord Extended
Show Extended

extDiv :: (Ratio Integer -> Integer) -> Extended -> Extended -> Maybe Extended Source

extDiv r a b : result of dividing a by b, rounded with r in the finite case; dividing infinty by infinity yields Nothing.

data Interval Source

Integer intervals

Constructors

Interval
Fields lower :: Extended upper :: Extended

Instances

Eq Interval
Num Interval
Show Interval
Lattice Interval

isBottom :: Interval -> Bool Source

Is interval empty?

isBounded :: Interval -> Bool Source

Are both bounds of the interval finite?

positives :: Interval Source

All positive integers

negatives :: Interval Source

All negative integers

nonNegatives :: Interval Source

All positive integers and 0

nonPositives :: Interval Source

All netaive integers and 0

mapBounds :: (Extended -> Extended -> t) -> Interval -> Interval -> [t]Source

Apply function to all pairs of bounds coming from two different intervals

(//) :: Interval -> Interval -> Interval Source

Division on integer intervals