Cryptol.TypeCheck.Solver.Numeric.Interval

An interval interpretation of types.

Documentation

typeInterval :: Map TVar Interval -> Type -> Interval

Only meaningful for numeric types

data IntervalUpdate

Constructors

NoChange

InvalidInterval TVar

NewIntervals (Map TVar Interval)

Instances

Show IntervalUpdate

updateInterval :: (TVar, Interval) -> Map TVar Interval -> IntervalUpdate

computePropIntervals :: Map TVar Interval -> [Prop] -> IntervalUpdate

propInterval :: Map TVar Interval -> Prop -> [(TVar, Interval)]

What we learn about variables from a single prop.

data Interval

Constructors

Interval

Fields

iLower :: Nat'

lower bound (inclusive)

iUpper :: Maybe Nat'

upper bound (inclusive) If there is no upper bound, than all *natural* numbers.

Instances

Eq Interval

Show Interval

ppIntervals :: Map TVar Interval -> Doc

ppInterval :: Interval -> Doc

iIsExact :: Interval -> Maybe Nat'

iIsFin :: Interval -> Bool

iDisjoint :: Interval -> Interval -> Bool

Returns True when the intervals definitely overlap, and False otherwise.

iIntersect :: Interval -> Interval -> Maybe Interval

Intersect two intervals, yielding a new one that describes the space where they overlap. If the two intervals are disjoint, the result will be Nothing.

iAny :: Interval

Any value

iAnyFin :: Interval

Any finite value

iConst :: Nat' -> Interval

Exactly this value

iAdd :: Interval -> Interval -> Interval

iMul :: Interval -> Interval -> Interval

iExp :: Interval -> Interval -> Interval

iMin :: Interval -> Interval -> Interval

iMax :: Interval -> Interval -> Interval

iSub :: Interval -> Interval -> Interval

iDiv :: Interval -> Interval -> Interval

iMod :: Interval -> Interval -> Interval

iWidth :: Interval -> Interval

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

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