Copyright | (c) 2013-2015 Galois, Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell98 |
This module defines natural numbers with an additional infinity element, and various arithmetic operators on them.
- data Nat'
- fromNat :: Nat' -> Maybe Integer
- nAdd :: Nat' -> Nat' -> Nat'
- nMul :: Nat' -> Nat' -> Nat'
- nExp :: Nat' -> Nat' -> Nat'
- nMin :: Nat' -> Nat' -> Nat'
- nMax :: Nat' -> Nat' -> Nat'
- nSub :: Nat' -> Nat' -> Maybe Nat'
- nDiv :: Nat' -> Nat' -> Maybe Nat'
- nMod :: Nat' -> Nat' -> Maybe Nat'
- nLg2 :: Nat' -> Nat'
- nWidth :: Nat' -> Nat'
- nLenFromThen :: Nat' -> Nat' -> Nat' -> Maybe Nat'
- nLenFromThenTo :: Nat' -> Nat' -> Nat' -> Maybe Nat'
- genLog :: Integer -> Integer -> Maybe (Integer, Bool)
- widthInteger :: Integer -> Integer
Documentation
nMul :: Nat' -> Nat' -> Nat' Source
Some algerbaic properties of interest:
1 * x = x x * (y * z) = (x * y) * z 0 * x = 0 x * y = y * x x * (a + b) = x * a + x * b
nExp :: Nat' -> Nat' -> Nat' Source
Some algeibraic properties of interest:
x ^ 0 = 1 x ^ (n + 1) = x * (x ^ n) x ^ (m + n) = (x ^ m) * (x ^ n) x ^ (m * n) = (x ^ m) ^ n
nSub :: Nat' -> Nat' -> Maybe Nat' Source
nSub x y = Just z
iff z
is the unique value
such that Add y z = Just x
.
nWidth n
is number of bits needed to represent all numbers
from 0 to n, inclusive. nWidth x = nLg2 (x + 1)
.
genLog :: Integer -> Integer -> Maybe (Integer, Bool) Source
Compute the logarithm of a number in the given base, rounded down to the closest integer. The boolean indicates if we the result is exact (i.e., True means no rounding happened, False means we rounded down). The logarithm base is the second argument.
widthInteger :: Integer -> Integer Source
Compute the number of bits required to represent the given integer.