Copyright	(c) 2015-2016 Galois Inc.
License	BSD3
Maintainer	cryptol@galois.com
Stability	provisional
Portability	portable
Safe Haskell	Safe
Language	Haskell2010

Cryptol.TypeCheck.Solver.Numeric.Interval

Description

An interval interpretation of types.

Synopsis

typeInterval :: Map TVar Interval -> Type -> Interval
tvarInterval :: Map TVar Interval -> TVar -> Interval
data IntervalUpdate
- = NoChange
- | InvalidInterval TVar
- | NewIntervals (Map TVar Interval)
updateInterval :: (TVar, Interval) -> Map TVar Interval -> IntervalUpdate
computePropIntervals :: Map TVar Interval -> [Prop] -> IntervalUpdate
propInterval :: Map TVar Interval -> Prop -> [(TVar, Interval)]
data Interval = Interval {
- iLower :: Nat'
- iUpper :: Maybe Nat'
}
ppIntervals :: Map TVar Interval -> Doc
ppInterval :: Interval -> Doc
iIsExact :: Interval -> Maybe Nat'
iIsFin :: Interval -> Bool
iIsPosFin :: Interval -> Bool
iOverlap :: Interval -> Interval -> Bool
iIntersect :: Interval -> Interval -> Maybe Interval
iAny :: Interval
iAnyFin :: Interval
iConst :: Nat' -> Interval
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

Documentation

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

Only meaningful for numeric types

tvarInterval :: Map TVar Interval -> TVar -> Interval Source #

data IntervalUpdate Source #

Constructors

NoChange
InvalidInterval TVar
NewIntervals (Map TVar Interval)

Instances

Show IntervalUpdate Source #
Instance details 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 Source #

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

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

What we learn about variables from a single prop.

data Interval Source #

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 Source #
Instance details Defined in Cryptol.TypeCheck.Solver.Numeric.Interval Methods (==) :: Interval -> Interval -> Bool # (/=) :: Interval -> Interval -> Bool #
Show Interval Source #
Instance details Defined in Cryptol.TypeCheck.Solver.Numeric.Interval Methods showsPrec :: Int -> Interval -> ShowS # show :: Interval -> String # showList :: [Interval] -> ShowS #

ppIntervals :: Map TVar Interval -> Doc Source #

ppInterval :: Interval -> Doc Source #

iIsExact :: Interval -> Maybe Nat' Source #

iIsFin :: Interval -> Bool Source #

iIsPosFin :: Interval -> Bool Source #

Finite positive number. [1 .. inf).

iOverlap :: Interval -> Interval -> Bool Source #

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

iIntersect :: Interval -> Interval -> Maybe Interval Source #

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 Source #

Any value

iAnyFin :: Interval Source #

Any finite value

iConst :: Nat' -> Interval Source #

Exactly this value

iAdd :: Interval -> Interval -> Interval Source #

iMul :: Interval -> Interval -> Interval Source #

iExp :: Interval -> Interval -> Interval Source #

iMin :: Interval -> Interval -> Interval Source #

iMax :: Interval -> Interval -> Interval Source #

iSub :: Interval -> Interval -> Interval Source #

iDiv :: Interval -> Interval -> Interval Source #

iMod :: Interval -> Interval -> Interval Source #

iCeilDiv :: Interval -> Interval -> Interval Source #

iCeilMod :: Interval -> Interval -> Interval Source #

iWidth :: Interval -> Interval Source #

iLenFromThenTo :: Interval -> Interval -> Interval -> Interval Source #