cryptol-2.2.6: Cryptol: The Language of Cryptography

Copyright(c) 2013-2015 Galois, Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell98

Cryptol.TypeCheck.Solver.Interval

Description

This module defines intervals and interval arithmetic.

Synopsis

Documentation

data Interval Source

Representation of intervals. Intervals always include the lower bound. Intervals include the upper bound if: * either the upper bound is finite, or * the upper bound is Inf and isFinite == False.

Invariant: if the upper bound is finite, then `isFinite == True`.

[x,y]     Interval (Nat x) (Nat y) True
[x,inf]   Interval (Nat x) Inf     False
[x,inf)   Interval (Nat x) Inf     True

Constructors

Interval 

Fields

lowerBound :: Nat'

Lower bound

upperBound :: Nat'

Upper bound

isFinite :: Bool

Do we know this to be a finite value. Note that for [inf,inf] this field is False (i.e., this field is not talking about the size of the interval, but, rather, about if it contains infinity).

Instances

anything :: Interval Source

Any possible value.

iLeq :: Interval -> Interval -> Bool Source

The first interval is definiately smaller

iLt :: Interval -> Interval -> Bool Source

The first interval is definiately smaller

iDisjoint :: Interval -> Interval -> Bool Source

The two intervals do not overlap.