cryptol-2.6.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

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

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