cryptol-2.2.6: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2015 Galois, Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe
Language | Haskell98

Cryptol.TypeCheck.Solver.Interval

Description

This module defines intervals and interval arithmetic.

Synopsis

- data Interval = Interval {
  - lowerBound :: Nat'
  - upperBound :: Nat'
  - isFinite :: Bool
  }
- anything :: Interval
- iConst :: Nat' -> Interval
- iAdd :: Interval -> Interval -> Interval
- iMul :: Interval -> Interval -> Interval
- iExp :: Interval -> Interval -> Interval
- iMin :: Interval -> Interval -> Interval
- iMax :: Interval -> Interval -> Interval
- iLg2 :: Interval -> Interval
- iWidth :: Interval -> Interval
- iSub :: Interval -> Interval -> Interval
- iDiv :: Interval -> Interval -> Interval
- iMod :: Interval -> Interval -> Interval
- iLenFromThen :: Interval -> Interval -> Interval -> Interval
- iLenFromTo :: Interval -> Interval -> Interval
- iLenFromThenTo :: Interval -> Interval -> Interval -> Interval
- iLeq :: Interval -> Interval -> Bool
- iLt :: Interval -> Interval -> Bool
- iDisjoint :: Interval -> Interval -> Bool

# 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

Show Interval Source |

anything :: Interval Source

Any possible value.

iConst :: Nat' -> Interval Source

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

iLg2 :: Interval -> Interval Source

iWidth :: Interval -> Interval Source

iSub :: Interval -> Interval -> Interval Source

iDiv :: Interval -> Interval -> Interval Source

iMod :: Interval -> Interval -> Interval Source

iLenFromThen :: Interval -> Interval -> Interval -> Interval Source

iLenFromTo :: Interval -> Interval -> Interval Source

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

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.