Cryptol.TypeCheck.Solver.Numeric.Interval

An interval interpretation of types.

Documentation

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

Only meaningful for numeric types

tvarInterval :: Map TVar Interval -> TVar -> Interval

data IntervalUpdate

Constructors

NoChange

InvalidInterval TVar

NewIntervals (Map TVar Interval)

Instances

Show IntervalUpdate

Defined in Cryptol.TypeCheck.Solver.Numeric.Interval

Methods

showsPrec :: Int -> IntervalUpdate -> ShowS

show :: IntervalUpdate -> String

showList :: [IntervalUpdate] -> ShowS

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, then all *natural* numbers.

Instances

Eq Interval

Defined in Cryptol.TypeCheck.Solver.Numeric.Interval

Methods

(==) :: Interval -> Interval -> Bool

(/=) :: Interval -> Interval -> Bool

Show Interval

Defined in Cryptol.TypeCheck.Solver.Numeric.Interval

Methods

showsPrec :: Int -> Interval -> ShowS

show :: Interval -> String

showList :: [Interval] -> ShowS

ppIntervals :: Map TVar Interval -> Doc

ppInterval :: Interval -> Doc

iIsExact :: Interval -> Maybe Nat'

iIsFin :: Interval -> Bool

iIsPosFin :: Interval -> Bool

Finite positive number. [1 .. inf).

iOverlap :: 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

iCeilDiv :: Interval -> Interval -> Interval

iCeilMod :: Interval -> Interval -> Interval

iWidth :: Interval -> Interval

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