Cryptol.TypeCheck.Solver.Interval

This module defines intervals and interval arithmetic.

Documentation

data Interval

Representation of intervals. Intervals always include the lower bound. Intervals include the upper bound if: * either the upper bound is finite, or * the upper bound is Inf and isFinite == False.

Invariant: if the upper bound is finite, then `isFinite == True`.

[x,y]     Interval (Nat x) (Nat y) True
[x,inf]   Interval (Nat x) Inf     False
[x,inf)   Interval (Nat x) Inf     True

Constructors

Interval

Fields

lowerBound :: Nat'

Lower bound

upperBound :: Nat'

Upper bound

isFinite :: Bool

Do we know this to be a finite value. Note that for [inf,inf] this field is False (i.e., this field is not talking about the size of the interval, but, rather, about if it contains infinity).

Instances

Show Interval

anything :: Interval

Any possible value.

iConst :: Nat' -> Interval

iAdd :: Interval -> Interval -> Interval

iMul :: Interval -> Interval -> Interval

iExp :: Interval -> Interval -> Interval

iMin :: Interval -> Interval -> Interval

iMax :: Interval -> Interval -> Interval

iLg2 :: Interval -> Interval

iWidth :: Interval -> Interval

iSub :: Interval -> Interval -> Interval

iDiv :: Interval -> Interval -> Interval

iMod :: Interval -> Interval -> Interval

iLenFromThen :: Interval -> Interval -> Interval -> Interval

iLenFromTo :: Interval -> Interval -> Interval

iLenFromThenTo :: Interval -> Interval -> Interval -> Interval

iLeq :: Interval -> Interval -> Bool

The first interval is definiately smaller

iLt :: Interval -> Interval -> Bool

The first interval is definiately smaller

iDisjoint :: Interval -> Interval -> Bool

The two intervals do not overlap.