cryptol-2.8.0: Cryptol: The Language of Cryptography
Copyright(c) 2015-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell2010

Cryptol.TypeCheck.Solver.Numeric.Interval

Description

An interval interpretation of types.

Synopsis

Documentation

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

Only meaningful for numeric types

data IntervalUpdate Source #

Instances

Instances details
Show IntervalUpdate Source # 
Instance details

Defined in Cryptol.TypeCheck.Solver.Numeric.Interval

Methods

showsPrec :: Int -> IntervalUpdate -> ShowS

show :: IntervalUpdate -> String

showList :: [IntervalUpdate] -> ShowS

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

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