cryptol-3.0.0: Cryptol: The Language of Cryptography

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
- ppIntervalsWithNames :: NameMap -> 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

Instances details

Show IntervalUpdate Source # |
Instance details Defined in Cryptol.TypeCheck.Solver.Numeric.Interval Methods showsPrec :: Int -> IntervalUpdate -> ShowS Source # show :: IntervalUpdate -> String Source # showList :: [IntervalUpdate] -> ShowS Source #

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

Instances details

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

ppIntervals :: Map TVar Interval -> Doc Source #

ppIntervalsWithNames :: NameMap -> 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 #