--------------------------------------------------------------------------------------------
--
--   Copyright   :  (C) 2022 Nathan Waivio
--   License     :  BSD3
--   Maintainer  :  Nathan Waivio <nathan.waivio@gmail.com>
--   Stability   :  Stable
--   Portability :  Portable
--
-- | Library implementing standard 'Posit-3.2' numbers, as defined by
--   the Posit Working Group 23 June 2018.
-- 
-- 
---------------------------------------------------------------------------------------------


{-# LANGUAGE TypeFamilyDependencies #-} -- For the associated bidirectional type family that the Posit library is based on
{-# LANGUAGE DataKinds #-}  -- For our ES kind and the constructors Z, I, II, III, IV, V, for exponent size type
{-# LANGUAGE TypeApplications #-}  -- The most excellent syntax @Int256
{-# LANGUAGE AllowAmbiguousTypes #-} -- The Haskell/GHC Type checker seems to have trouble things in the PositC class
{-# LANGUAGE ScopedTypeVariables #-} -- To reduce some code duplication
{-# LANGUAGE FlexibleContexts #-} -- To reduce some code duplication by claiming the type family provides some constraints, that GHC can't do without fully evaluating the type family
{-# LANGUAGE CPP #-} -- To remove Storable instances to remove noise when performing analysis of Core
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}  -- Turn off noise
{-# OPTIONS_GHC -Wno-type-defaults #-}  -- Turn off noise

-- ----
--  |Posit Class, implementing:
--
--   * PositC
--   * Orphan Instances of Storable for Word128, Int128, Int256
-- ----

module Posit.Internal.PositC
(PositC(..),
 ES(..)
 ) where

import Prelude hiding (exponent,significand)

-- Imports for Storable Instance of Data.DoubleWord
import Foreign.Storable (Storable, sizeOf, alignment, peek, poke)  -- Used for Storable Instances of Data.DoubleWord
import Foreign.Ptr (Ptr, plusPtr, castPtr)  -- Used for dealing with Pointers for the Data.DoubleWord Storable Instance

-- Machine Integers and Operations
{-@ embed Int128 * as int @-}
{-@ embed Int256 * as int @-}
import Data.Int (Int8,Int16,Int32,Int64)  -- Import standard Int sizes
import Data.DoubleWord (Word128,Int128,Int256,fromHiAndLo,hiWord,loWord) -- Import large Int sizes
import Data.Word (Word64)
import Data.Bits ((.|.), shiftL, shift, testBit, (.&.), shiftR)

-- Import Naturals and Rationals
{-@ embed Natural * as int @-}
import GHC.Natural (Natural) -- Import the Natural Numbers ℕ (u+2115)
{-@ embed Ratio * as int @-}
import Data.Ratio (Rational, (%))  -- Import the Rational Numbers ℚ (u+211A), ℚ can get arbitrarily close to Real numbers ℝ (u+211D)


-- | The Exponent Size 'ES' kind, the constructor for the Type is a Roman Numeral.
data ES = Z
        | I
        | II
        | III
        | IV
        | V


-- | The 'Posit' class is an approximation of ℝ, it is like a sampling on the Projective Real line ℙ(ℝ) with Maybe ℚ as the internal type.
-- The 'es' is an index that controlls the log2 word size of the Posit's
-- fininte precision representation.
class PositC (es :: ES) where
  -- | Type of the Finite Precision Representation, in our case Int8, Int16, Int32, Int64, Int128, Int256. The 'es' of kind 'ES' will determine a result of 'r' such that you can determine the 'es' by the 'r'
  type IntN es = r | r -> es
 
 
  -- | Transform to/from the Infinite Precision Representation
  encode :: Maybe Rational -> IntN es  -- ^ Maybe you have some Rational Number and you want to encode it as some integer with a finite integer log2 word size.
  decode :: IntN es -> Maybe Rational  -- ^ You have an integer with a finite integer log2 word size decode it and Maybe it is Rational
 
  -- | Exponent Size based on the Posit Exponent kind ES
  exponentSize :: Natural  -- ^ The exponent size, 'es' is a Natural number
 
  -- | Various other size definitions used in the Posit format with their default definitions
  nBytes :: Natural  -- ^ 'nBytes' the number of bytes of the Posit Representation
  nBytes = Natural
2forall a b. (Num a, Integral b) => a -> b -> a
^(forall (es :: ES). PositC es => Natural
exponentSize @es)
 
  nBits :: Natural  -- ^ 'nBits' the number of bits of the Posit Representation
  nBits = Natural
8 forall a. Num a => a -> a -> a
* (forall (es :: ES). PositC es => Natural
nBytes @es)
 
  signBitSize :: Natural  -- ^ 'signBitSize' the size of the sign bit
  signBitSize = Natural
1
 
  uSeed :: Natural  -- ^ 'uSeed' scaling factor for the regime of the Posit Representation
  uSeed = Natural
2forall a b. (Num a, Integral b) => a -> b -> a
^(forall (es :: ES). PositC es => Natural
nBytes @es)
 
  -- | Integer Representation of common bounds
  unReal :: IntN es  -- ^ 'unReal' is something that is not Real, the integer value that is not a Real number
 
  mostPosVal :: IntN es
  leastPosVal :: IntN es
  leastNegVal :: IntN es
  mostNegVal :: IntN es
 
  -- Rational Value of common bounds
  maxPosRat :: Rational
  maxPosRat = Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^((forall (es :: ES). PositC es => Natural
nBytes @es) forall a. Num a => a -> a -> a
* ((forall (es :: ES). PositC es => Natural
nBits @es) forall a. Num a => a -> a -> a
- Natural
2)) forall a. Integral a => a -> a -> Ratio a
% Integer
1
  minPosRat :: Rational
  minPosRat = forall a. Fractional a => a -> a
recip (forall (es :: ES). PositC es => Rational
maxPosRat @es)
  maxNegRat :: Rational
  maxNegRat = forall a. Num a => a -> a
negate (forall (es :: ES). PositC es => Rational
minPosRat @es)
  minNegRat :: Rational
  minNegRat = forall a. Num a => a -> a
negate (forall (es :: ES). PositC es => Rational
maxPosRat @es)
 
  -- Functions to support encode and decode
 
  -- log base uSeed
  -- After calculating the regime the rational should be in the range [1,uSeed), it starts with (0,rational)
  log_uSeed :: (Integer, Rational) -> (Integer, Rational)
  log_uSeed (Integer
regime,Rational
r)
    | Rational
r forall a. Ord a => a -> a -> Bool
< Rational
1 = forall (es :: ES).
PositC es =>
(Integer, Rational) -> (Integer, Rational)
log_uSeed @es (Integer
regimeforall a. Num a => a -> a -> a
-Integer
1,Rational
r forall a. Num a => a -> a -> a
* forall a. Fractional a => Rational -> a
fromRational (forall a. Integral a => a -> Integer
toInteger (forall (es :: ES). PositC es => Natural
uSeed @es) forall a. Integral a => a -> a -> Ratio a
% Integer
1))
    | Rational
r forall a. Ord a => a -> a -> Bool
>= forall a. Fractional a => Rational -> a
fromRational (forall a. Integral a => a -> Integer
toInteger (forall (es :: ES). PositC es => Natural
uSeed @es) forall a. Integral a => a -> a -> Ratio a
% Integer
1) = forall (es :: ES).
PositC es =>
(Integer, Rational) -> (Integer, Rational)
log_uSeed @es (Integer
regimeforall a. Num a => a -> a -> a
+Integer
1,Rational
r forall a. Num a => a -> a -> a
* forall a. Fractional a => Rational -> a
fromRational (Integer
1 forall a. Integral a => a -> a -> Ratio a
% forall a. Integral a => a -> Integer
toInteger (forall (es :: ES). PositC es => Natural
uSeed @es)))
    | Bool
otherwise = (Integer
regime,Rational
r)
 
  getRegime :: Rational -> (Integer, Rational)
  getRegime Rational
r = forall (es :: ES).
PositC es =>
(Integer, Rational) -> (Integer, Rational)
log_uSeed @es (Integer
0,Rational
r)
 
  posit2TupPosit :: Rational -> (Bool, Integer, Natural, Rational)
  posit2TupPosit Rational
r =
    let (Bool
sgn,Rational
r') = Rational -> (Bool, Rational)
getSign Rational
r -- returns the sign and a positive rational
        (Integer
regime,Rational
r'') = forall (es :: ES). PositC es => Rational -> (Integer, Rational)
getRegime @es Rational
r' -- returns the regime and a rational between uSeed^-1 to uSeed^1
        (Natural
exponent,Rational
significand) = Rational -> (Natural, Rational)
getExponent Rational
r'' -- returns the exponent and a rational between [1,2), the significand
    in (Bool
sgn,Integer
regime,Natural
exponent,Rational
significand)
 
  buildIntRep :: Rational -> IntN es
  mkIntRep :: Integer -> Natural -> Rational -> IntN es
  formRegime :: Integer -> (IntN es, Integer)
  formExponent :: Natural -> Integer -> (IntN es, Integer)
  formFraction :: Rational -> Integer -> IntN es
 
  tupPosit2Posit :: (Bool,Integer,Natural,Rational) -> Maybe Rational
  tupPosit2Posit (Bool
sgn,Integer
regime,Natural
exponent,Rational
rat) = -- s = isNeg posit == True
    let pow2 :: Rational
pow2 = forall a. Real a => a -> Rational
toRational (forall (es :: ES). PositC es => Natural
uSeed @es)forall a b. (Fractional a, Integral b) => a -> b -> a
^^Integer
regime forall a. Num a => a -> a -> a
* Rational
2forall a b. (Num a, Integral b) => a -> b -> a
^Natural
exponent
        scale :: Rational
scale = if Bool
sgn
                then forall a. Num a => a -> a
negate Rational
pow2
                else Rational
pow2
    in forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Rational
scale forall a. Num a => a -> a -> a
* Rational
rat
 
  regime2Integer :: IntN es -> (Integer, Int)
  findRegimeFormat :: IntN es -> Bool
  countRegimeBits :: Bool -> IntN es -> Int
  exponent2Nat :: Int -> IntN es -> Natural
  fraction2Posit :: Int -> IntN es -> Rational
 
  -- prints out the IntN es value in 0b... format
  displayBin :: IntN es -> String
  -- decimal Precision
  decimalPrec :: Int
  decimalPrec = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ Natural
2 forall a. Num a => a -> a -> a
* (forall (es :: ES). PositC es => Natural
nBytes @es) forall a. Num a => a -> a -> a
+ Natural
1



instance PositC Z where
  type IntN Z = Int8
  exponentSize :: Natural
exponentSize = Natural
0
 
  -- Posit Integer Rep of various values
  unReal :: IntN 'Z
unReal = forall a. Bounded a => a
minBound @Int8
 
  mostPosVal :: IntN 'Z
mostPosVal = forall a. Bounded a => a
maxBound @Int8
  leastPosVal :: IntN 'Z
leastPosVal = Int8
1
  leastNegVal :: IntN 'Z
leastNegVal = -Int8
1
  mostNegVal :: IntN 'Z
mostNegVal = forall a. Num a => a -> a
negate forall (es :: ES). PositC es => IntN es
mostPosVal
 
  encode :: Maybe Rational -> IntN 'Z
encode Maybe Rational
Nothing = forall (es :: ES). PositC es => IntN es
unReal @Z
  encode (Just Rational
0) = Int8
0
  encode (Just Rational
r)
    | Rational
r forall a. Ord a => a -> a -> Bool
> forall (es :: ES). PositC es => Rational
maxPosRat @Z = forall (es :: ES). PositC es => IntN es
mostPosVal @Z
    | Rational
r forall a. Ord a => a -> a -> Bool
< forall (es :: ES). PositC es => Rational
minNegRat @Z = forall (es :: ES). PositC es => IntN es
mostNegVal @Z
    | Rational
r forall a. Ord a => a -> a -> Bool
> Rational
0 Bool -> Bool -> Bool
&& Rational
r forall a. Ord a => a -> a -> Bool
< forall (es :: ES). PositC es => Rational
minPosRat @Z = forall (es :: ES). PositC es => IntN es
leastPosVal @Z
    | Rational
r forall a. Ord a => a -> a -> Bool
< Rational
0 Bool -> Bool -> Bool
&& Rational
r forall a. Ord a => a -> a -> Bool
> forall (es :: ES). PositC es => Rational
maxNegRat @Z = forall (es :: ES). PositC es => IntN es
leastNegVal @Z
    | Bool
otherwise = forall (es :: ES). PositC es => Rational -> IntN es
buildIntRep @Z Rational
r
 
  buildIntRep :: Rational -> IntN 'Z
buildIntRep Rational
r =
    let (Bool
signBit,Integer
regime,Natural
exponent,Rational
significand) = forall (es :: ES).
PositC es =>
Rational -> (Bool, Integer, Natural, Rational)
posit2TupPosit @Z Rational
r
        intRep :: IntN 'Z
intRep = forall (es :: ES).
PositC es =>
Integer -> Natural -> Rational -> IntN es
mkIntRep @Z Integer
regime Natural
exponent Rational
significand
    in if Bool
signBit
       then forall a. Num a => a -> a
negate IntN 'Z
intRep
       else IntN 'Z
intRep
 
  mkIntRep :: Integer -> Natural -> Rational -> IntN 'Z
mkIntRep Integer
regime Natural
exponent Rational
significand =
    let (IntN 'Z
regime', Integer
offset) = forall (es :: ES). PositC es => Integer -> (IntN es, Integer)
formRegime @Z Integer
regime  -- offset is the number of binary digits remaining after the regime is formed
        (IntN 'Z
exponent', Integer
offset') = forall (es :: ES).
PositC es =>
Natural -> Integer -> (IntN es, Integer)
formExponent @Z Natural
exponent Integer
offset  -- offset' is the number of binary digits remaining after the exponent is formed
        fraction :: IntN 'Z
fraction = forall (es :: ES). PositC es => Rational -> Integer -> IntN es
formFraction @Z Rational
significand Integer
offset'
    in IntN 'Z
regime' forall a. Bits a => a -> a -> a
.|. IntN 'Z
exponent' forall a. Bits a => a -> a -> a
.|. IntN 'Z
fraction
 
  formRegime :: Integer -> (IntN 'Z, Integer)
formRegime Integer
power
    | Integer
0 forall a. Ord a => a -> a -> Bool
<= Integer
power =
      let offset :: Integer
offset = (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @Z forall a. Num a => a -> a -> a
- Natural
1) forall a. Num a => a -> a -> a
-     Integer
power forall a. Num a => a -> a -> a
- Integer
1)
      in (forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
power forall a. Num a => a -> a -> a
+ Integer
1) forall a. Num a => a -> a -> a
- Integer
1) forall a. Bits a => a -> Int -> a
`shiftL` forall a. Num a => Integer -> a
fromInteger Integer
offset, Integer
offset forall a. Num a => a -> a -> a
- Integer
1)
    | Bool
otherwise =
      let offset :: Integer
offset = (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @Z forall a. Num a => a -> a -> a
- Natural
1) forall a. Num a => a -> a -> a
- forall a. Num a => a -> a
abs Integer
power forall a. Num a => a -> a -> a
- Integer
1)
      in (Int8
1 forall a. Bits a => a -> Int -> a
`shiftL` forall a. Num a => Integer -> a
fromInteger Integer
offset, Integer
offset)
 
  formExponent :: Natural -> Integer -> (IntN 'Z, Integer)
formExponent Natural
power Integer
offset =
    let offset' :: Integer
offset' = Integer
offset forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
exponentSize @Z)
    in (forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
power forall a. Bits a => a -> Int -> a
`shift` forall a. Num a => Integer -> a
fromInteger Integer
offset', Integer
offset')
 
  formFraction :: Rational -> Integer -> IntN 'Z
formFraction Rational
r Integer
offset =
    let numFractionBits :: Integer
numFractionBits = Integer
offset
        fractionSize :: Rational
fractionSize = Rational
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
numFractionBits
        normFraction :: Integer
normFraction = forall a b. (RealFrac a, Integral b) => a -> b
round forall a b. (a -> b) -> a -> b
$ (Rational
r forall a. Num a => a -> a -> a
- Rational
1) forall a. Num a => a -> a -> a
* Rational
fractionSize  -- "posit - 1" is changing it from the significand to the fraction: [1,2) -> [0,1)
    in if Integer
numFractionBits forall a. Ord a => a -> a -> Bool
>= Integer
1
       then forall a. Num a => Integer -> a
fromInteger Integer
normFraction
       else Int8
0
 
  decode :: IntN 'Z -> Maybe Rational
decode IntN 'Z
int
    | IntN 'Z
int forall a. Eq a => a -> a -> Bool
== forall (es :: ES). PositC es => IntN es
unReal @Z = forall a. Maybe a
Nothing
    | IntN 'Z
int forall a. Eq a => a -> a -> Bool
== Int8
0 = forall a. a -> Maybe a
Just Rational
0
    | Bool
otherwise =
      let sgn :: Bool
sgn = IntN 'Z
int forall a. Ord a => a -> a -> Bool
< Int8
0
          int' :: Int8
int' = if Bool
sgn
                 then forall a. Num a => a -> a
negate IntN 'Z
int
                 else IntN 'Z
int
          (Integer
regime,Int
nR) = forall (es :: ES). PositC es => IntN es -> (Integer, Int)
regime2Integer @Z Int8
int'
          exponent :: Natural
exponent = forall (es :: ES). PositC es => Int -> IntN es -> Natural
exponent2Nat @Z Int
nR Int8
int'  -- if no e or some bits missing, then they are considered zero
          rat :: Rational
rat = forall (es :: ES). PositC es => Int -> IntN es -> Rational
fraction2Posit @Z Int
nR Int8
int'  -- if no fraction or some bits missing, then the missing bits are zero, making the significand p=1
      in forall (es :: ES).
PositC es =>
(Bool, Integer, Natural, Rational) -> Maybe Rational
tupPosit2Posit @Z (Bool
sgn,Integer
regime,Natural
exponent,Rational
rat)
 
  regime2Integer :: IntN 'Z -> (Integer, Int)
regime2Integer IntN 'Z
posit =
    let regimeFormat :: Bool
regimeFormat = forall (es :: ES). PositC es => IntN es -> Bool
findRegimeFormat @Z IntN 'Z
posit
        regimeCount :: Int
regimeCount = forall (es :: ES). PositC es => Bool -> IntN es -> Int
countRegimeBits @Z Bool
regimeFormat IntN 'Z
posit
        regime :: Integer
regime = Bool -> Int -> Integer
calcRegimeInt Bool
regimeFormat Int
regimeCount
    in (Integer
regime, Int
regimeCount forall a. Num a => a -> a -> a
+ Int
1) -- a rational representation of the regime and the regimeCount plus rBar which is the numBitsRegime
 
  -- will return the format of the regime, either HI or LO; it could get refactored in the future
  -- True means a 1 is the first bit in the regime
  findRegimeFormat :: IntN 'Z -> Bool
findRegimeFormat IntN 'Z
posit = forall a. Bits a => a -> Int -> Bool
testBit IntN 'Z
posit (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @Z) forall a. Num a => a -> a -> a
- Int
1 forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @Z))
 
  countRegimeBits :: Bool -> IntN 'Z -> Int
countRegimeBits Bool
format IntN 'Z
posit = Int -> Int -> Int
go (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @Z) forall a. Num a => a -> a -> a
- Int
1 forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @Z)) Int
0
    where
      go :: Int -> Int -> Int
go (-1) Int
acc = Int
acc
      go Int
index Int
acc
        | Bool -> Bool -> Bool
xnor Bool
format (forall a. Bits a => a -> Int -> Bool
testBit IntN 'Z
posit Int
index)  = Int -> Int -> Int
go (Int
index forall a. Num a => a -> a -> a
- Int
1) (Int
acc forall a. Num a => a -> a -> a
+ Int
1)
        | Bool
otherwise = Int
acc
 
  -- knowing the number of the regime bits, and the sign bit we can extract
  -- the exponent.  We mask to the left of the exponent to remove the sign and regime, and
  -- then shift to the right to remove the fraction.
  exponent2Nat :: Int -> IntN 'Z -> Natural
exponent2Nat Int
numBitsRegime IntN 'Z
posit =
    let bitsRemaining :: Int
bitsRemaining = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @Z) forall a. Num a => a -> a -> a
- Int
numBitsRegime forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @Z)
        signNRegimeMask :: Int8
signNRegimeMask = Int8
2forall a b. (Num a, Integral b) => a -> b -> a
^Int
bitsRemaining forall a. Num a => a -> a -> a
- Int8
1
        int :: Int8
int = IntN 'Z
posit forall a. Bits a => a -> a -> a
.&. Int8
signNRegimeMask
        nBitsToTheRight :: Int
nBitsToTheRight = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @Z) forall a. Num a => a -> a -> a
- Int
numBitsRegime forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @Z) forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
exponentSize @Z)
    in if Int
bitsRemaining forall a. Ord a => a -> a -> Bool
<=Int
0
       then Natural
0
       else if Int
nBitsToTheRight forall a. Ord a => a -> a -> Bool
< Int
0
            then forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ Int8
int forall a. Bits a => a -> Int -> a
`shiftL` forall a. Num a => a -> a
negate Int
nBitsToTheRight
            else forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ Int8
int forall a. Bits a => a -> Int -> a
`shiftR` Int
nBitsToTheRight
 
  -- knowing the number of the regime bits, sign bit, and the number of the
  -- exponent bits we can extract the fraction.  We mask to the left of the fraction to
  -- remove the sign, regime, and exponent. If there is no fraction then the value is 1.
  fraction2Posit :: Int -> IntN 'Z -> Rational
fraction2Posit Int
numBitsRegime IntN 'Z
posit =
    let offset :: Integer
offset = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ (forall (es :: ES). PositC es => Natural
signBitSize @Z) forall a. Num a => a -> a -> a
+ forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
numBitsRegime forall a. Num a => a -> a -> a
+ (forall (es :: ES). PositC es => Natural
exponentSize @Z)
        fractionSize :: Integer
fractionSize = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @Z) forall a. Num a => a -> a -> a
- Integer
offset
        fractionBits :: Int8
fractionBits = IntN 'Z
posit forall a. Bits a => a -> a -> a
.&. (Int8
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
fractionSize forall a. Num a => a -> a -> a
- Int8
1)
    in if Integer
fractionSize forall a. Ord a => a -> a -> Bool
>= Integer
1
       then (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
fractionSize forall a. Num a => a -> a -> a
+ forall a. Integral a => a -> Integer
toInteger Int8
fractionBits) forall a. Integral a => a -> a -> Ratio a
% Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
fractionSize
       else Integer
1 forall a. Integral a => a -> a -> Ratio a
% Integer
1
 
  displayBin :: IntN 'Z -> String
displayBin IntN 'Z
int = String
"0b" forall a. [a] -> [a] -> [a]
++ Int -> String
go (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @Z) forall a. Num a => a -> a -> a
- Int
1)
    where
      go :: Int -> String
      go :: Int -> String
go Int
0 = if forall a. Bits a => a -> Int -> Bool
testBit IntN 'Z
int Int
0
             then String
"1"
             else String
"0"
      go Int
idx = if forall a. Bits a => a -> Int -> Bool
testBit IntN 'Z
int Int
idx
               then String
"1" forall a. [a] -> [a] -> [a]
++ Int -> String
go (Int
idx forall a. Num a => a -> a -> a
- Int
1)
               else String
"0" forall a. [a] -> [a] -> [a]
++ Int -> String
go (Int
idx forall a. Num a => a -> a -> a
-Int
1)



instance PositC I where
  type IntN I = Int16
  exponentSize :: Natural
exponentSize = Natural
1
 
  -- Posit Integer Rep of various values
  unReal :: IntN 'I
unReal = forall a. Bounded a => a
minBound @Int16
 
  mostPosVal :: IntN 'I
mostPosVal = forall a. Bounded a => a
maxBound @Int16
  leastPosVal :: IntN 'I
leastPosVal = Int16
1
  leastNegVal :: IntN 'I
leastNegVal = -Int16
1
  mostNegVal :: IntN 'I
mostNegVal = forall a. Num a => a -> a
negate forall (es :: ES). PositC es => IntN es
mostPosVal
 
  encode :: Maybe Rational -> IntN 'I
encode Maybe Rational
Nothing = forall (es :: ES). PositC es => IntN es
unReal @I
  encode (Just Rational
0) = Int16
0
  encode (Just Rational
r)
    | Rational
r forall a. Ord a => a -> a -> Bool
> forall (es :: ES). PositC es => Rational
maxPosRat @I = forall (es :: ES). PositC es => IntN es
mostPosVal @I
    | Rational
r forall a. Ord a => a -> a -> Bool
< forall (es :: ES). PositC es => Rational
minNegRat @I = forall (es :: ES). PositC es => IntN es
mostNegVal @I
    | Rational
r forall a. Ord a => a -> a -> Bool
> Rational
0 Bool -> Bool -> Bool
&& Rational
r forall a. Ord a => a -> a -> Bool
< forall (es :: ES). PositC es => Rational
minPosRat @I = forall (es :: ES). PositC es => IntN es
leastPosVal @I
    | Rational
r forall a. Ord a => a -> a -> Bool
< Rational
0 Bool -> Bool -> Bool
&& Rational
r forall a. Ord a => a -> a -> Bool
> forall (es :: ES). PositC es => Rational
maxNegRat @I = forall (es :: ES). PositC es => IntN es
leastNegVal @I
    | Bool
otherwise = forall (es :: ES). PositC es => Rational -> IntN es
buildIntRep @I Rational
r
 
  buildIntRep :: Rational -> IntN 'I
buildIntRep Rational
r =
    let (Bool
signBit,Integer
regime,Natural
exponent,Rational
significand) = forall (es :: ES).
PositC es =>
Rational -> (Bool, Integer, Natural, Rational)
posit2TupPosit @I Rational
r
        intRep :: IntN 'I
intRep = forall (es :: ES).
PositC es =>
Integer -> Natural -> Rational -> IntN es
mkIntRep @I Integer
regime Natural
exponent Rational
significand
    in if Bool
signBit
       then forall a. Num a => a -> a
negate IntN 'I
intRep
       else IntN 'I
intRep
 
  mkIntRep :: Integer -> Natural -> Rational -> IntN 'I
mkIntRep Integer
regime Natural
exponent Rational
significand =
    let (IntN 'I
regime', Integer
offset) = forall (es :: ES). PositC es => Integer -> (IntN es, Integer)
formRegime @I Integer
regime  -- offset is the number of binary digits remaining after the regime is formed
        (IntN 'I
exponent', Integer
offset') = forall (es :: ES).
PositC es =>
Natural -> Integer -> (IntN es, Integer)
formExponent @I Natural
exponent Integer
offset  -- offset' is the number of binary digits remaining after the exponent is formed
        fraction :: IntN 'I
fraction = forall (es :: ES). PositC es => Rational -> Integer -> IntN es
formFraction @I Rational
significand Integer
offset'
    in IntN 'I
regime' forall a. Bits a => a -> a -> a
.|. IntN 'I
exponent' forall a. Bits a => a -> a -> a
.|. IntN 'I
fraction
 
  formRegime :: Integer -> (IntN 'I, Integer)
formRegime Integer
power
    | Integer
0 forall a. Ord a => a -> a -> Bool
<= Integer
power =
      let offset :: Integer
offset = (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @I forall a. Num a => a -> a -> a
- Natural
1) forall a. Num a => a -> a -> a
-     Integer
power forall a. Num a => a -> a -> a
- Integer
1)
      in (forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
power forall a. Num a => a -> a -> a
+ Integer
1) forall a. Num a => a -> a -> a
- Integer
1) forall a. Bits a => a -> Int -> a
`shiftL` forall a. Num a => Integer -> a
fromInteger Integer
offset, Integer
offset forall a. Num a => a -> a -> a
- Integer
1)
    | Bool
otherwise =
      let offset :: Integer
offset = (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @I forall a. Num a => a -> a -> a
- Natural
1) forall a. Num a => a -> a -> a
- forall a. Num a => a -> a
abs Integer
power forall a. Num a => a -> a -> a
- Integer
1)
      in (Int16
1 forall a. Bits a => a -> Int -> a
`shiftL` forall a. Num a => Integer -> a
fromInteger Integer
offset, Integer
offset)
 
  formExponent :: Natural -> Integer -> (IntN 'I, Integer)
formExponent Natural
power Integer
offset =
    let offset' :: Integer
offset' = Integer
offset forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
exponentSize @I)
    in (forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
power forall a. Bits a => a -> Int -> a
`shift` forall a. Num a => Integer -> a
fromInteger Integer
offset', Integer
offset')
 
  formFraction :: Rational -> Integer -> IntN 'I
formFraction Rational
r Integer
offset =
    let numFractionBits :: Integer
numFractionBits = Integer
offset
        fractionSize :: Rational
fractionSize = Rational
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
numFractionBits
        normFraction :: Integer
normFraction = forall a b. (RealFrac a, Integral b) => a -> b
round forall a b. (a -> b) -> a -> b
$ (Rational
r forall a. Num a => a -> a -> a
- Rational
1) forall a. Num a => a -> a -> a
* Rational
fractionSize  -- "posit - 1" is changing it from the significand to the fraction: [1,2) -> [0,1)
    in if Integer
numFractionBits forall a. Ord a => a -> a -> Bool
>= Integer
1
       then forall a. Num a => Integer -> a
fromInteger Integer
normFraction
       else Int16
0
 
  decode :: IntN 'I -> Maybe Rational
decode IntN 'I
int
    | IntN 'I
int forall a. Eq a => a -> a -> Bool
== forall (es :: ES). PositC es => IntN es
unReal @I = forall a. Maybe a
Nothing
    | IntN 'I
int forall a. Eq a => a -> a -> Bool
== Int16
0 = forall a. a -> Maybe a
Just Rational
0
    | Bool
otherwise =
      let sgn :: Bool
sgn = IntN 'I
int forall a. Ord a => a -> a -> Bool
< Int16
0
          int' :: Int16
int' = if Bool
sgn
                 then forall a. Num a => a -> a
negate IntN 'I
int
                 else IntN 'I
int
          (Integer
regime,Int
nR) = forall (es :: ES). PositC es => IntN es -> (Integer, Int)
regime2Integer @I Int16
int'
          exponent :: Natural
exponent = forall (es :: ES). PositC es => Int -> IntN es -> Natural
exponent2Nat @I Int
nR Int16
int'  -- if no e or some bits missing, then they are considered zero
          rat :: Rational
rat = forall (es :: ES). PositC es => Int -> IntN es -> Rational
fraction2Posit @I Int
nR Int16
int'  -- if no fraction or some bits missing, then the missing bits are zero, making the significand p=1
      in forall (es :: ES).
PositC es =>
(Bool, Integer, Natural, Rational) -> Maybe Rational
tupPosit2Posit @I (Bool
sgn,Integer
regime,Natural
exponent,Rational
rat)
 
  regime2Integer :: IntN 'I -> (Integer, Int)
regime2Integer IntN 'I
posit =
    let regimeFormat :: Bool
regimeFormat = forall (es :: ES). PositC es => IntN es -> Bool
findRegimeFormat @I IntN 'I
posit
        regimeCount :: Int
regimeCount = forall (es :: ES). PositC es => Bool -> IntN es -> Int
countRegimeBits @I Bool
regimeFormat IntN 'I
posit
        regime :: Integer
regime = Bool -> Int -> Integer
calcRegimeInt Bool
regimeFormat Int
regimeCount
    in (Integer
regime, Int
regimeCount forall a. Num a => a -> a -> a
+ Int
1) -- a rational representation of the regime and the regimeCount plus rBar which is the numBitsRegime
 
  -- will return the format of the regime, either HI or LO; it could get refactored in the future
  -- True means a 1 is the first bit in the regime
  findRegimeFormat :: IntN 'I -> Bool
findRegimeFormat IntN 'I
posit = forall a. Bits a => a -> Int -> Bool
testBit IntN 'I
posit (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @I) forall a. Num a => a -> a -> a
- Int
1 forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @I))
 
  countRegimeBits :: Bool -> IntN 'I -> Int
countRegimeBits Bool
format IntN 'I
posit = Int -> Int -> Int
go (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @I) forall a. Num a => a -> a -> a
- Int
1 forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @I)) Int
0
    where
      go :: Int -> Int -> Int
go (-1) Int
acc = Int
acc
      go Int
index Int
acc
        | Bool -> Bool -> Bool
xnor Bool
format (forall a. Bits a => a -> Int -> Bool
testBit IntN 'I
posit Int
index)  = Int -> Int -> Int
go (Int
index forall a. Num a => a -> a -> a
- Int
1) (Int
acc forall a. Num a => a -> a -> a
+ Int
1)
        | Bool
otherwise = Int
acc
 
  -- knowing the number of the regime bits, and the sign bit we can extract
  -- the exponent.  We mask to the left of the exponent to remove the sign and regime, and
  -- then shift to the right to remove the fraction.
  exponent2Nat :: Int -> IntN 'I -> Natural
exponent2Nat Int
numBitsRegime IntN 'I
posit =
    let bitsRemaining :: Int
bitsRemaining = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @I) forall a. Num a => a -> a -> a
- Int
numBitsRegime forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @I)
        signNRegimeMask :: Int16
signNRegimeMask = Int16
2forall a b. (Num a, Integral b) => a -> b -> a
^Int
bitsRemaining forall a. Num a => a -> a -> a
- Int16
1
        int :: Int16
int = IntN 'I
posit forall a. Bits a => a -> a -> a
.&. Int16
signNRegimeMask
        nBitsToTheRight :: Int
nBitsToTheRight = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @I) forall a. Num a => a -> a -> a
- Int
numBitsRegime forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @I) forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
exponentSize @I)
    in if Int
bitsRemaining forall a. Ord a => a -> a -> Bool
<=Int
0
       then Natural
0
       else if Int
nBitsToTheRight forall a. Ord a => a -> a -> Bool
< Int
0
            then forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ Int16
int forall a. Bits a => a -> Int -> a
`shiftL` forall a. Num a => a -> a
negate Int
nBitsToTheRight
            else forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ Int16
int forall a. Bits a => a -> Int -> a
`shiftR` Int
nBitsToTheRight
 
  -- knowing the number of the regime bits, sign bit, and the number of the
  -- exponent bits we can extract the fraction.  We mask to the left of the fraction to
  -- remove the sign, regime, and exponent. If there is no fraction then the value is 1.
  fraction2Posit :: Int -> IntN 'I -> Rational
fraction2Posit Int
numBitsRegime IntN 'I
posit =
    let offset :: Integer
offset = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ (forall (es :: ES). PositC es => Natural
signBitSize @I) forall a. Num a => a -> a -> a
+ forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
numBitsRegime forall a. Num a => a -> a -> a
+ (forall (es :: ES). PositC es => Natural
exponentSize @I)
        fractionSize :: Integer
fractionSize = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @I) forall a. Num a => a -> a -> a
- Integer
offset
        fractionBits :: Int16
fractionBits = IntN 'I
posit forall a. Bits a => a -> a -> a
.&. (Int16
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
fractionSize forall a. Num a => a -> a -> a
- Int16
1)
    in if Integer
fractionSize forall a. Ord a => a -> a -> Bool
>= Integer
1
       then (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
fractionSize forall a. Num a => a -> a -> a
+ forall a. Integral a => a -> Integer
toInteger Int16
fractionBits) forall a. Integral a => a -> a -> Ratio a
% Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
fractionSize
       else Integer
1 forall a. Integral a => a -> a -> Ratio a
% Integer
1
 
  displayBin :: IntN 'I -> String
displayBin IntN 'I
int = String
"0b" forall a. [a] -> [a] -> [a]
++ Int -> String
go (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @I) forall a. Num a => a -> a -> a
- Int
1)
    where
      go :: Int -> String
      go :: Int -> String
go Int
0 = if forall a. Bits a => a -> Int -> Bool
testBit IntN 'I
int Int
0
             then String
"1"
             else String
"0"
      go Int
idx = if forall a. Bits a => a -> Int -> Bool
testBit IntN 'I
int Int
idx
               then String
"1" forall a. [a] -> [a] -> [a]
++ Int -> String
go (Int
idx forall a. Num a => a -> a -> a
- Int
1)
               else String
"0" forall a. [a] -> [a] -> [a]
++ Int -> String
go (Int
idx forall a. Num a => a -> a -> a
-Int
1)



instance PositC II where
  type IntN II = Int32
  exponentSize :: Natural
exponentSize = Natural
2
 
  -- Posit Integer Rep of various values
  unReal :: IntN 'II
unReal = forall a. Bounded a => a
minBound @Int32
 
  mostPosVal :: IntN 'II
mostPosVal = forall a. Bounded a => a
maxBound @Int32
  leastPosVal :: IntN 'II
leastPosVal = Int32
1
  leastNegVal :: IntN 'II
leastNegVal = -Int32
1
  mostNegVal :: IntN 'II
mostNegVal = forall a. Num a => a -> a
negate forall (es :: ES). PositC es => IntN es
mostPosVal
 
  encode :: Maybe Rational -> IntN 'II
encode Maybe Rational
Nothing = forall (es :: ES). PositC es => IntN es
unReal @II
  encode (Just Rational
0) = Int32
0
  encode (Just Rational
r)
    | Rational
r forall a. Ord a => a -> a -> Bool
> forall (es :: ES). PositC es => Rational
maxPosRat @II = forall (es :: ES). PositC es => IntN es
mostPosVal @II
    | Rational
r forall a. Ord a => a -> a -> Bool
< forall (es :: ES). PositC es => Rational
minNegRat @II = forall (es :: ES). PositC es => IntN es
mostNegVal @II
    | Rational
r forall a. Ord a => a -> a -> Bool
> Rational
0 Bool -> Bool -> Bool
&& Rational
r forall a. Ord a => a -> a -> Bool
< forall (es :: ES). PositC es => Rational
minPosRat @II = forall (es :: ES). PositC es => IntN es
leastPosVal @II
    | Rational
r forall a. Ord a => a -> a -> Bool
< Rational
0 Bool -> Bool -> Bool
&& Rational
r forall a. Ord a => a -> a -> Bool
> forall (es :: ES). PositC es => Rational
maxNegRat @II = forall (es :: ES). PositC es => IntN es
leastNegVal @II
    | Bool
otherwise = forall (es :: ES). PositC es => Rational -> IntN es
buildIntRep @II Rational
r
 
  buildIntRep :: Rational -> IntN 'II
buildIntRep Rational
r =
    let (Bool
signBit,Integer
regime,Natural
exponent,Rational
significand) = forall (es :: ES).
PositC es =>
Rational -> (Bool, Integer, Natural, Rational)
posit2TupPosit @II Rational
r
        intRep :: IntN 'II
intRep = forall (es :: ES).
PositC es =>
Integer -> Natural -> Rational -> IntN es
mkIntRep @II Integer
regime Natural
exponent Rational
significand
    in if Bool
signBit
       then forall a. Num a => a -> a
negate IntN 'II
intRep
       else IntN 'II
intRep
 
  mkIntRep :: Integer -> Natural -> Rational -> IntN 'II
mkIntRep Integer
regime Natural
exponent Rational
significand =
    let (IntN 'II
regime', Integer
offset) = forall (es :: ES). PositC es => Integer -> (IntN es, Integer)
formRegime @II Integer
regime  -- offset is the number of binary digits remaining after the regime is formed
        (IntN 'II
exponent', Integer
offset') = forall (es :: ES).
PositC es =>
Natural -> Integer -> (IntN es, Integer)
formExponent @II Natural
exponent Integer
offset  -- offset' is the number of binary digits remaining after the exponent is formed
        fraction :: IntN 'II
fraction = forall (es :: ES). PositC es => Rational -> Integer -> IntN es
formFraction @II Rational
significand Integer
offset'
    in IntN 'II
regime' forall a. Bits a => a -> a -> a
.|. IntN 'II
exponent' forall a. Bits a => a -> a -> a
.|. IntN 'II
fraction
 
  formRegime :: Integer -> (IntN 'II, Integer)
formRegime Integer
power
    | Integer
0 forall a. Ord a => a -> a -> Bool
<= Integer
power =
      let offset :: Integer
offset = (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @II forall a. Num a => a -> a -> a
- Natural
1) forall a. Num a => a -> a -> a
-     Integer
power forall a. Num a => a -> a -> a
- Integer
1)
      in (forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
power forall a. Num a => a -> a -> a
+ Integer
1) forall a. Num a => a -> a -> a
- Integer
1) forall a. Bits a => a -> Int -> a
`shiftL` forall a. Num a => Integer -> a
fromInteger Integer
offset, Integer
offset forall a. Num a => a -> a -> a
- Integer
1)
    | Bool
otherwise =
      let offset :: Integer
offset = (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @II forall a. Num a => a -> a -> a
- Natural
1) forall a. Num a => a -> a -> a
- forall a. Num a => a -> a
abs Integer
power forall a. Num a => a -> a -> a
- Integer
1)
      in (Int32
1 forall a. Bits a => a -> Int -> a
`shiftL` forall a. Num a => Integer -> a
fromInteger Integer
offset, Integer
offset)
 
  formExponent :: Natural -> Integer -> (IntN 'II, Integer)
formExponent Natural
power Integer
offset =
    let offset' :: Integer
offset' = Integer
offset forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
exponentSize @II)
    in (forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
power forall a. Bits a => a -> Int -> a
`shift` forall a. Num a => Integer -> a
fromInteger Integer
offset', Integer
offset')
 
  formFraction :: Rational -> Integer -> IntN 'II
formFraction Rational
r Integer
offset =
    let numFractionBits :: Integer
numFractionBits = Integer
offset
        fractionSize :: Rational
fractionSize = Rational
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
numFractionBits
        normFraction :: Integer
normFraction = forall a b. (RealFrac a, Integral b) => a -> b
round forall a b. (a -> b) -> a -> b
$ (Rational
r forall a. Num a => a -> a -> a
- Rational
1) forall a. Num a => a -> a -> a
* Rational
fractionSize  -- "posit - 1" is changing it from the significand to the fraction: [1,2) -> [0,1)
    in if Integer
numFractionBits forall a. Ord a => a -> a -> Bool
>= Integer
1
       then forall a. Num a => Integer -> a
fromInteger Integer
normFraction
       else Int32
0
 
  decode :: IntN 'II -> Maybe Rational
decode IntN 'II
int
    | IntN 'II
int forall a. Eq a => a -> a -> Bool
== forall (es :: ES). PositC es => IntN es
unReal @II = forall a. Maybe a
Nothing
    | IntN 'II
int forall a. Eq a => a -> a -> Bool
== Int32
0 = forall a. a -> Maybe a
Just Rational
0
    | Bool
otherwise =
      let sgn :: Bool
sgn = IntN 'II
int forall a. Ord a => a -> a -> Bool
< Int32
0
          int' :: Int32
int' = if Bool
sgn
                 then forall a. Num a => a -> a
negate IntN 'II
int
                 else IntN 'II
int
          (Integer
regime,Int
nR) = forall (es :: ES). PositC es => IntN es -> (Integer, Int)
regime2Integer @II Int32
int'
          exponent :: Natural
exponent = forall (es :: ES). PositC es => Int -> IntN es -> Natural
exponent2Nat @II Int
nR Int32
int'  -- if no e or some bits missing, then they are considered zero
          rat :: Rational
rat = forall (es :: ES). PositC es => Int -> IntN es -> Rational
fraction2Posit @II Int
nR Int32
int'  -- if no fraction or some bits missing, then the missing bits are zero, making the significand p=1
      in forall (es :: ES).
PositC es =>
(Bool, Integer, Natural, Rational) -> Maybe Rational
tupPosit2Posit @II (Bool
sgn,Integer
regime,Natural
exponent,Rational
rat)
 
  regime2Integer :: IntN 'II -> (Integer, Int)
regime2Integer IntN 'II
posit =
    let regimeFormat :: Bool
regimeFormat = forall (es :: ES). PositC es => IntN es -> Bool
findRegimeFormat @II IntN 'II
posit
        regimeCount :: Int
regimeCount = forall (es :: ES). PositC es => Bool -> IntN es -> Int
countRegimeBits @II Bool
regimeFormat IntN 'II
posit
        regime :: Integer
regime = Bool -> Int -> Integer
calcRegimeInt Bool
regimeFormat Int
regimeCount
    in (Integer
regime, Int
regimeCount forall a. Num a => a -> a -> a
+ Int
1) -- a rational representation of the regime and the regimeCount plus rBar which is the numBitsRegime
 
  -- will return the format of the regime, either HI or LO; it could get refactored in the future
  -- True means a 1 is the first bit in the regime
  findRegimeFormat :: IntN 'II -> Bool
findRegimeFormat IntN 'II
posit = forall a. Bits a => a -> Int -> Bool
testBit IntN 'II
posit (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @II) forall a. Num a => a -> a -> a
- Int
1 forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @II))
 
  countRegimeBits :: Bool -> IntN 'II -> Int
countRegimeBits Bool
format IntN 'II
posit = Int -> Int -> Int
go (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @II) forall a. Num a => a -> a -> a
- Int
1 forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @II)) Int
0
    where
      go :: Int -> Int -> Int
go (-1) Int
acc = Int
acc
      go Int
index Int
acc
        | Bool -> Bool -> Bool
xnor Bool
format (forall a. Bits a => a -> Int -> Bool
testBit IntN 'II
posit Int
index)  = Int -> Int -> Int
go (Int
index forall a. Num a => a -> a -> a
- Int
1) (Int
acc forall a. Num a => a -> a -> a
+ Int
1)
        | Bool
otherwise = Int
acc
 
  -- knowing the number of the regime bits, and the sign bit we can extract
  -- the exponent.  We mask to the left of the exponent to remove the sign and regime, and
  -- then shift to the right to remove the fraction.
  exponent2Nat :: Int -> IntN 'II -> Natural
exponent2Nat Int
numBitsRegime IntN 'II
posit =
    let bitsRemaining :: Int
bitsRemaining = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @II) forall a. Num a => a -> a -> a
- Int
numBitsRegime forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @II)
        signNRegimeMask :: Int32
signNRegimeMask = Int32
2forall a b. (Num a, Integral b) => a -> b -> a
^Int
bitsRemaining forall a. Num a => a -> a -> a
- Int32
1
        int :: Int32
int = IntN 'II
posit forall a. Bits a => a -> a -> a
.&. Int32
signNRegimeMask
        nBitsToTheRight :: Int
nBitsToTheRight = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @II) forall a. Num a => a -> a -> a
- Int
numBitsRegime forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @II) forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
exponentSize @II)
    in if Int
bitsRemaining forall a. Ord a => a -> a -> Bool
<=Int
0
       then Natural
0
       else if Int
nBitsToTheRight forall a. Ord a => a -> a -> Bool
< Int
0
            then forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ Int32
int forall a. Bits a => a -> Int -> a
`shiftL` forall a. Num a => a -> a
negate Int
nBitsToTheRight
            else forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ Int32
int forall a. Bits a => a -> Int -> a
`shiftR` Int
nBitsToTheRight
 
  -- knowing the number of the regime bits, sign bit, and the number of the
  -- exponent bits we can extract the fraction.  We mask to the left of the fraction to
  -- remove the sign, regime, and exponent. If there is no fraction then the value is 1.
  fraction2Posit :: Int -> IntN 'II -> Rational
fraction2Posit Int
numBitsRegime IntN 'II
posit =
    let offset :: Integer
offset = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ (forall (es :: ES). PositC es => Natural
signBitSize @II) forall a. Num a => a -> a -> a
+ forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
numBitsRegime forall a. Num a => a -> a -> a
+ (forall (es :: ES). PositC es => Natural
exponentSize @II)
        fractionSize :: Integer
fractionSize = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @II) forall a. Num a => a -> a -> a
- Integer
offset
        fractionBits :: Int32
fractionBits = IntN 'II
posit forall a. Bits a => a -> a -> a
.&. (Int32
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
fractionSize forall a. Num a => a -> a -> a
- Int32
1)
    in if Integer
fractionSize forall a. Ord a => a -> a -> Bool
>= Integer
1
       then (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
fractionSize forall a. Num a => a -> a -> a
+ forall a. Integral a => a -> Integer
toInteger Int32
fractionBits) forall a. Integral a => a -> a -> Ratio a
% Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
fractionSize
       else Integer
1 forall a. Integral a => a -> a -> Ratio a
% Integer
1
 
  displayBin :: IntN 'II -> String
displayBin IntN 'II
int = String
"0b" forall a. [a] -> [a] -> [a]
++ Int -> String
go (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @II) forall a. Num a => a -> a -> a
- Int
1)
    where
      go :: Int -> String
      go :: Int -> String
go Int
0 = if forall a. Bits a => a -> Int -> Bool
testBit IntN 'II
int Int
0
             then String
"1"
             else String
"0"
      go Int
idx = if forall a. Bits a => a -> Int -> Bool
testBit IntN 'II
int Int
idx
               then String
"1" forall a. [a] -> [a] -> [a]
++ Int -> String
go (Int
idx forall a. Num a => a -> a -> a
- Int
1)
               else String
"0" forall a. [a] -> [a] -> [a]
++ Int -> String
go (Int
idx forall a. Num a => a -> a -> a
-Int
1)



instance PositC III where
  type IntN III = Int64
  exponentSize :: Natural
exponentSize = Natural
3
 
  -- Posit Integer Rep of various values
  unReal :: IntN 'III
unReal = forall a. Bounded a => a
minBound @Int64
 
  mostPosVal :: IntN 'III
mostPosVal = forall a. Bounded a => a
maxBound @Int64
  leastPosVal :: IntN 'III
leastPosVal = Int64
1
  leastNegVal :: IntN 'III
leastNegVal = -Int64
1
  mostNegVal :: IntN 'III
mostNegVal = forall a. Num a => a -> a
negate forall (es :: ES). PositC es => IntN es
mostPosVal
 
  encode :: Maybe Rational -> IntN 'III
encode Maybe Rational
Nothing = forall (es :: ES). PositC es => IntN es
unReal @III
  encode (Just Rational
0) = Int64
0
  encode (Just Rational
r)
    | Rational
r forall a. Ord a => a -> a -> Bool
> forall (es :: ES). PositC es => Rational
maxPosRat @III = forall (es :: ES). PositC es => IntN es
mostPosVal @III
    | Rational
r forall a. Ord a => a -> a -> Bool
< forall (es :: ES). PositC es => Rational
minNegRat @III = forall (es :: ES). PositC es => IntN es
mostNegVal @III
    | Rational
r forall a. Ord a => a -> a -> Bool
> Rational
0 Bool -> Bool -> Bool
&& Rational
r forall a. Ord a => a -> a -> Bool
< forall (es :: ES). PositC es => Rational
minPosRat @III = forall (es :: ES). PositC es => IntN es
leastPosVal @III
    | Rational
r forall a. Ord a => a -> a -> Bool
< Rational
0 Bool -> Bool -> Bool
&& Rational
r forall a. Ord a => a -> a -> Bool
> forall (es :: ES). PositC es => Rational
maxNegRat @III = forall (es :: ES). PositC es => IntN es
leastNegVal @III
    | Bool
otherwise = forall (es :: ES). PositC es => Rational -> IntN es
buildIntRep @III Rational
r
 
  buildIntRep :: Rational -> IntN 'III
buildIntRep Rational
r =
    let (Bool
signBit,Integer
regime,Natural
exponent,Rational
significand) = forall (es :: ES).
PositC es =>
Rational -> (Bool, Integer, Natural, Rational)
posit2TupPosit @III Rational
r
        intRep :: IntN 'III
intRep = forall (es :: ES).
PositC es =>
Integer -> Natural -> Rational -> IntN es
mkIntRep @III Integer
regime Natural
exponent Rational
significand
    in if Bool
signBit
       then forall a. Num a => a -> a
negate IntN 'III
intRep
       else IntN 'III
intRep
 
  mkIntRep :: Integer -> Natural -> Rational -> IntN 'III
mkIntRep Integer
regime Natural
exponent Rational
significand =
    let (IntN 'III
regime', Integer
offset) = forall (es :: ES). PositC es => Integer -> (IntN es, Integer)
formRegime @III Integer
regime  -- offset is the number of binary digits remaining after the regime is formed
        (IntN 'III
exponent', Integer
offset') = forall (es :: ES).
PositC es =>
Natural -> Integer -> (IntN es, Integer)
formExponent @III Natural
exponent Integer
offset  -- offset' is the number of binary digits remaining after the exponent is formed
        fraction :: IntN 'III
fraction = forall (es :: ES). PositC es => Rational -> Integer -> IntN es
formFraction @III Rational
significand Integer
offset'
    in IntN 'III
regime' forall a. Bits a => a -> a -> a
.|. IntN 'III
exponent' forall a. Bits a => a -> a -> a
.|. IntN 'III
fraction
 
  formRegime :: Integer -> (IntN 'III, Integer)
formRegime Integer
power
    | Integer
0 forall a. Ord a => a -> a -> Bool
<= Integer
power =
      let offset :: Integer
offset = (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @III forall a. Num a => a -> a -> a
- Natural
1) forall a. Num a => a -> a -> a
-     Integer
power forall a. Num a => a -> a -> a
- Integer
1)
      in (forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
power forall a. Num a => a -> a -> a
+ Integer
1) forall a. Num a => a -> a -> a
- Integer
1) forall a. Bits a => a -> Int -> a
`shiftL` forall a. Num a => Integer -> a
fromInteger Integer
offset, Integer
offset forall a. Num a => a -> a -> a
- Integer
1)
    | Bool
otherwise =
      let offset :: Integer
offset = (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @III forall a. Num a => a -> a -> a
- Natural
1) forall a. Num a => a -> a -> a
- forall a. Num a => a -> a
abs Integer
power forall a. Num a => a -> a -> a
- Integer
1)
      in (Int64
1 forall a. Bits a => a -> Int -> a
`shiftL` forall a. Num a => Integer -> a
fromInteger Integer
offset, Integer
offset)
 
  formExponent :: Natural -> Integer -> (IntN 'III, Integer)
formExponent Natural
power Integer
offset =
    let offset' :: Integer
offset' = Integer
offset forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
exponentSize @III)
    in (forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
power forall a. Bits a => a -> Int -> a
`shift` forall a. Num a => Integer -> a
fromInteger Integer
offset', Integer
offset')
 
  formFraction :: Rational -> Integer -> IntN 'III
formFraction Rational
r Integer
offset =
    let numFractionBits :: Integer
numFractionBits = Integer
offset
        fractionSize :: Rational
fractionSize = Rational
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
numFractionBits
        normFraction :: Integer
normFraction = forall a b. (RealFrac a, Integral b) => a -> b
round forall a b. (a -> b) -> a -> b
$ (Rational
r forall a. Num a => a -> a -> a
- Rational
1) forall a. Num a => a -> a -> a
* Rational
fractionSize  -- "posit - 1" is changing it from the significand to the fraction: [1,2) -> [0,1)
    in if Integer
numFractionBits forall a. Ord a => a -> a -> Bool
>= Integer
1
       then forall a. Num a => Integer -> a
fromInteger Integer
normFraction
       else Int64
0
 
  decode :: IntN 'III -> Maybe Rational
decode IntN 'III
int
    | IntN 'III
int forall a. Eq a => a -> a -> Bool
== forall (es :: ES). PositC es => IntN es
unReal @III = forall a. Maybe a
Nothing
    | IntN 'III
int forall a. Eq a => a -> a -> Bool
== Int64
0 = forall a. a -> Maybe a
Just Rational
0
    | Bool
otherwise =
      let sgn :: Bool
sgn = IntN 'III
int forall a. Ord a => a -> a -> Bool
< Int64
0
          int' :: Int64
int' = if Bool
sgn
                 then forall a. Num a => a -> a
negate IntN 'III
int
                 else IntN 'III
int
          (Integer
regime,Int
nR) = forall (es :: ES). PositC es => IntN es -> (Integer, Int)
regime2Integer @III Int64
int'
          exponent :: Natural
exponent = forall (es :: ES). PositC es => Int -> IntN es -> Natural
exponent2Nat @III Int
nR Int64
int'  -- if no e or some bits missing, then they are considered zero
          rat :: Rational
rat = forall (es :: ES). PositC es => Int -> IntN es -> Rational
fraction2Posit @III Int
nR Int64
int'  -- if no fraction or some bits missing, then the missing bits are zero, making the significand p=1
      in forall (es :: ES).
PositC es =>
(Bool, Integer, Natural, Rational) -> Maybe Rational
tupPosit2Posit @III (Bool
sgn,Integer
regime,Natural
exponent,Rational
rat)
 
  regime2Integer :: IntN 'III -> (Integer, Int)
regime2Integer IntN 'III
posit =
    let regimeFormat :: Bool
regimeFormat = forall (es :: ES). PositC es => IntN es -> Bool
findRegimeFormat @III IntN 'III
posit
        regimeCount :: Int
regimeCount = forall (es :: ES). PositC es => Bool -> IntN es -> Int
countRegimeBits @III Bool
regimeFormat IntN 'III
posit
        regime :: Integer
regime = Bool -> Int -> Integer
calcRegimeInt Bool
regimeFormat Int
regimeCount
    in (Integer
regime, Int
regimeCount forall a. Num a => a -> a -> a
+ Int
1) -- a rational representation of the regime and the regimeCount plus rBar which is the numBitsRegime
 
  -- will return the format of the regime, either HI or LO; it could get refactored in the future
  -- True means a 1 is the first bit in the regime
  findRegimeFormat :: IntN 'III -> Bool
findRegimeFormat IntN 'III
posit = forall a. Bits a => a -> Int -> Bool
testBit IntN 'III
posit (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @III) forall a. Num a => a -> a -> a
- Int
1 forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @III))
 
  countRegimeBits :: Bool -> IntN 'III -> Int
countRegimeBits Bool
format IntN 'III
posit = Int -> Int -> Int
go (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @III) forall a. Num a => a -> a -> a
- Int
1 forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @III)) Int
0
    where
      go :: Int -> Int -> Int
go (-1) Int
acc = Int
acc
      go Int
index Int
acc
        | Bool -> Bool -> Bool
xnor Bool
format (forall a. Bits a => a -> Int -> Bool
testBit IntN 'III
posit Int
index)  = Int -> Int -> Int
go (Int
index forall a. Num a => a -> a -> a
- Int
1) (Int
acc forall a. Num a => a -> a -> a
+ Int
1)
        | Bool
otherwise = Int
acc
 
  -- knowing the number of the regime bits, and the sign bit we can extract
  -- the exponent.  We mask to the left of the exponent to remove the sign and regime, and
  -- then shift to the right to remove the fraction.
  exponent2Nat :: Int -> IntN 'III -> Natural
exponent2Nat Int
numBitsRegime IntN 'III
posit =
    let bitsRemaining :: Int
bitsRemaining = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @III) forall a. Num a => a -> a -> a
- Int
numBitsRegime forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @III)
        signNRegimeMask :: Int64
signNRegimeMask = Int64
2forall a b. (Num a, Integral b) => a -> b -> a
^Int
bitsRemaining forall a. Num a => a -> a -> a
- Int64
1
        int :: Int64
int = IntN 'III
posit forall a. Bits a => a -> a -> a
.&. Int64
signNRegimeMask
        nBitsToTheRight :: Int
nBitsToTheRight = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @III) forall a. Num a => a -> a -> a
- Int
numBitsRegime forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @III) forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
exponentSize @III)
    in if Int
bitsRemaining forall a. Ord a => a -> a -> Bool
<=Int
0
       then Natural
0
       else if Int
nBitsToTheRight forall a. Ord a => a -> a -> Bool
< Int
0
            then forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ Int64
int forall a. Bits a => a -> Int -> a
`shiftL` forall a. Num a => a -> a
negate Int
nBitsToTheRight
            else forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ Int64
int forall a. Bits a => a -> Int -> a
`shiftR` Int
nBitsToTheRight
 
  -- knowing the number of the regime bits, sign bit, and the number of the
  -- exponent bits we can extract the fraction.  We mask to the left of the fraction to
  -- remove the sign, regime, and exponent. If there is no fraction then the value is 1.
  fraction2Posit :: Int -> IntN 'III -> Rational
fraction2Posit Int
numBitsRegime IntN 'III
posit =
    let offset :: Integer
offset = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ (forall (es :: ES). PositC es => Natural
signBitSize @III) forall a. Num a => a -> a -> a
+ forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
numBitsRegime forall a. Num a => a -> a -> a
+ (forall (es :: ES). PositC es => Natural
exponentSize @III)
        fractionSize :: Integer
fractionSize = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @III) forall a. Num a => a -> a -> a
- Integer
offset
        fractionBits :: Int64
fractionBits = IntN 'III
posit forall a. Bits a => a -> a -> a
.&. (Int64
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
fractionSize forall a. Num a => a -> a -> a
- Int64
1)
    in if Integer
fractionSize forall a. Ord a => a -> a -> Bool
>= Integer
1
       then (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
fractionSize forall a. Num a => a -> a -> a
+ forall a. Integral a => a -> Integer
toInteger Int64
fractionBits) forall a. Integral a => a -> a -> Ratio a
% Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
fractionSize
       else Integer
1 forall a. Integral a => a -> a -> Ratio a
% Integer
1
 
  displayBin :: IntN 'III -> String
displayBin IntN 'III
int = String
"0b" forall a. [a] -> [a] -> [a]
++ Int -> String
go (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @III) forall a. Num a => a -> a -> a
- Int
1)
    where
      go :: Int -> String
      go :: Int -> String
go Int
0 = if forall a. Bits a => a -> Int -> Bool
testBit IntN 'III
int Int
0
             then String
"1"
             else String
"0"
      go Int
idx = if forall a. Bits a => a -> Int -> Bool
testBit IntN 'III
int Int
idx
               then String
"1" forall a. [a] -> [a] -> [a]
++ Int -> String
go (Int
idx forall a. Num a => a -> a -> a
- Int
1)
               else String
"0" forall a. [a] -> [a] -> [a]
++ Int -> String
go (Int
idx forall a. Num a => a -> a -> a
-Int
1)



instance PositC IV where
  type IntN IV = Int128
  exponentSize :: Natural
exponentSize = Natural
4
 
  -- Posit Integer Rep of various values
  unReal :: IntN 'IV
unReal = forall a. Bounded a => a
minBound @Int128
 
  mostPosVal :: IntN 'IV
mostPosVal = forall a. Bounded a => a
maxBound @Int128
  leastPosVal :: IntN 'IV
leastPosVal = Int128
1
  leastNegVal :: IntN 'IV
leastNegVal = -Int128
1
  mostNegVal :: IntN 'IV
mostNegVal = forall a. Num a => a -> a
negate forall (es :: ES). PositC es => IntN es
mostPosVal
 
  encode :: Maybe Rational -> IntN 'IV
encode Maybe Rational
Nothing = forall (es :: ES). PositC es => IntN es
unReal @IV
  encode (Just Rational
0) = Int128
0
  encode (Just Rational
r)
    | Rational
r forall a. Ord a => a -> a -> Bool
> forall (es :: ES). PositC es => Rational
maxPosRat @IV = forall (es :: ES). PositC es => IntN es
mostPosVal @IV
    | Rational
r forall a. Ord a => a -> a -> Bool
< forall (es :: ES). PositC es => Rational
minNegRat @IV = forall (es :: ES). PositC es => IntN es
mostNegVal @IV
    | Rational
r forall a. Ord a => a -> a -> Bool
> Rational
0 Bool -> Bool -> Bool
&& Rational
r forall a. Ord a => a -> a -> Bool
< forall (es :: ES). PositC es => Rational
minPosRat @IV = forall (es :: ES). PositC es => IntN es
leastPosVal @IV
    | Rational
r forall a. Ord a => a -> a -> Bool
< Rational
0 Bool -> Bool -> Bool
&& Rational
r forall a. Ord a => a -> a -> Bool
> forall (es :: ES). PositC es => Rational
maxNegRat @IV = forall (es :: ES). PositC es => IntN es
leastNegVal @IV
    | Bool
otherwise = forall (es :: ES). PositC es => Rational -> IntN es
buildIntRep @IV Rational
r
 
  buildIntRep :: Rational -> IntN 'IV
buildIntRep Rational
r =
    let (Bool
signBit,Integer
regime,Natural
exponent,Rational
significand) = forall (es :: ES).
PositC es =>
Rational -> (Bool, Integer, Natural, Rational)
posit2TupPosit @IV Rational
r
        intRep :: IntN 'IV
intRep = forall (es :: ES).
PositC es =>
Integer -> Natural -> Rational -> IntN es
mkIntRep @IV Integer
regime Natural
exponent Rational
significand
    in if Bool
signBit
       then forall a. Num a => a -> a
negate IntN 'IV
intRep
       else IntN 'IV
intRep
 
  mkIntRep :: Integer -> Natural -> Rational -> IntN 'IV
mkIntRep Integer
regime Natural
exponent Rational
significand =
    let (IntN 'IV
regime', Integer
offset) = forall (es :: ES). PositC es => Integer -> (IntN es, Integer)
formRegime @IV Integer
regime  -- offset is the number of binary digits remaining after the regime is formed
        (IntN 'IV
exponent', Integer
offset') = forall (es :: ES).
PositC es =>
Natural -> Integer -> (IntN es, Integer)
formExponent @IV Natural
exponent Integer
offset  -- offset' is the number of binary digits remaining after the exponent is formed
        fraction :: IntN 'IV
fraction = forall (es :: ES). PositC es => Rational -> Integer -> IntN es
formFraction @IV Rational
significand Integer
offset'
    in IntN 'IV
regime' forall a. Bits a => a -> a -> a
.|. IntN 'IV
exponent' forall a. Bits a => a -> a -> a
.|. IntN 'IV
fraction
 
  formRegime :: Integer -> (IntN 'IV, Integer)
formRegime Integer
power
    | Integer
0 forall a. Ord a => a -> a -> Bool
<= Integer
power =
      let offset :: Integer
offset = (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @IV forall a. Num a => a -> a -> a
- Natural
1) forall a. Num a => a -> a -> a
-     Integer
power forall a. Num a => a -> a -> a
- Integer
1)
      in (forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
power forall a. Num a => a -> a -> a
+ Integer
1) forall a. Num a => a -> a -> a
- Integer
1) forall a. Bits a => a -> Int -> a
`shiftL` forall a. Num a => Integer -> a
fromInteger Integer
offset, Integer
offset forall a. Num a => a -> a -> a
- Integer
1)
    | Bool
otherwise =
      let offset :: Integer
offset = (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @IV forall a. Num a => a -> a -> a
- Natural
1) forall a. Num a => a -> a -> a
- forall a. Num a => a -> a
abs Integer
power forall a. Num a => a -> a -> a
- Integer
1)
      in (Int128
1 forall a. Bits a => a -> Int -> a
`shiftL` forall a. Num a => Integer -> a
fromInteger Integer
offset, Integer
offset)
 
  formExponent :: Natural -> Integer -> (IntN 'IV, Integer)
formExponent Natural
power Integer
offset =
    let offset' :: Integer
offset' = Integer
offset forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
exponentSize @IV)
    in (forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
power forall a. Bits a => a -> Int -> a
`shift` forall a. Num a => Integer -> a
fromInteger Integer
offset', Integer
offset')
 
  formFraction :: Rational -> Integer -> IntN 'IV
formFraction Rational
r Integer
offset =
    let numFractionBits :: Integer
numFractionBits = Integer
offset
        fractionSize :: Rational
fractionSize = Rational
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
numFractionBits
        normFraction :: Integer
normFraction = forall a b. (RealFrac a, Integral b) => a -> b
round forall a b. (a -> b) -> a -> b
$ (Rational
r forall a. Num a => a -> a -> a
- Rational
1) forall a. Num a => a -> a -> a
* Rational
fractionSize  -- "posit - 1" is changing it from the significand to the fraction: [1,2) -> [0,1)
    in if Integer
numFractionBits forall a. Ord a => a -> a -> Bool
>= Integer
1
       then forall a. Num a => Integer -> a
fromInteger Integer
normFraction
       else Int128
0
 
  decode :: IntN 'IV -> Maybe Rational
decode IntN 'IV
int
    | IntN 'IV
int forall a. Eq a => a -> a -> Bool
== forall (es :: ES). PositC es => IntN es
unReal @IV = forall a. Maybe a
Nothing
    | IntN 'IV
int forall a. Eq a => a -> a -> Bool
== Int128
0 = forall a. a -> Maybe a
Just Rational
0
    | Bool
otherwise =
      let sgn :: Bool
sgn = IntN 'IV
int forall a. Ord a => a -> a -> Bool
< Int128
0
          int' :: Int128
int' = if Bool
sgn
                 then forall a. Num a => a -> a
negate IntN 'IV
int
                 else IntN 'IV
int
          (Integer
regime,Int
nR) = forall (es :: ES). PositC es => IntN es -> (Integer, Int)
regime2Integer @IV Int128
int'
          exponent :: Natural
exponent = forall (es :: ES). PositC es => Int -> IntN es -> Natural
exponent2Nat @IV Int
nR Int128
int'  -- if no e or some bits missing, then they are considered zero
          rat :: Rational
rat = forall (es :: ES). PositC es => Int -> IntN es -> Rational
fraction2Posit @IV Int
nR Int128
int'  -- if no fraction or some bits missing, then the missing bits are zero, making the significand p=1
      in forall (es :: ES).
PositC es =>
(Bool, Integer, Natural, Rational) -> Maybe Rational
tupPosit2Posit @IV (Bool
sgn,Integer
regime,Natural
exponent,Rational
rat)
 
  regime2Integer :: IntN 'IV -> (Integer, Int)
regime2Integer IntN 'IV
posit =
    let regimeFormat :: Bool
regimeFormat = forall (es :: ES). PositC es => IntN es -> Bool
findRegimeFormat @IV IntN 'IV
posit
        regimeCount :: Int
regimeCount = forall (es :: ES). PositC es => Bool -> IntN es -> Int
countRegimeBits @IV Bool
regimeFormat IntN 'IV
posit
        regime :: Integer
regime = Bool -> Int -> Integer
calcRegimeInt Bool
regimeFormat Int
regimeCount
    in (Integer
regime, Int
regimeCount forall a. Num a => a -> a -> a
+ Int
1) -- a rational representation of the regime and the regimeCount plus rBar which is the numBitsRegime
 
  -- will return the format of the regime, either HI or LO; it could get refactored in the future
  -- True means a 1 is the first bit in the regime
  findRegimeFormat :: IntN 'IV -> Bool
findRegimeFormat IntN 'IV
posit = forall a. Bits a => a -> Int -> Bool
testBit IntN 'IV
posit (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @IV) forall a. Num a => a -> a -> a
- Int
1 forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @IV))
 
  countRegimeBits :: Bool -> IntN 'IV -> Int
countRegimeBits Bool
format IntN 'IV
posit = Int -> Int -> Int
go (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @IV) forall a. Num a => a -> a -> a
- Int
1 forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @IV)) Int
0
    where
      go :: Int -> Int -> Int
go (-1) Int
acc = Int
acc
      go Int
index Int
acc
        | Bool -> Bool -> Bool
xnor Bool
format (forall a. Bits a => a -> Int -> Bool
testBit IntN 'IV
posit Int
index)  = Int -> Int -> Int
go (Int
index forall a. Num a => a -> a -> a
- Int
1) (Int
acc forall a. Num a => a -> a -> a
+ Int
1)
        | Bool
otherwise = Int
acc
 
  -- knowing the number of the regime bits, and the sign bit we can extract
  -- the exponent.  We mask to the left of the exponent to remove the sign and regime, and
  -- then shift to the right to remove the fraction.
  exponent2Nat :: Int -> IntN 'IV -> Natural
exponent2Nat Int
numBitsRegime IntN 'IV
posit =
    let bitsRemaining :: Int
bitsRemaining = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @IV) forall a. Num a => a -> a -> a
- Int
numBitsRegime forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @IV)
        signNRegimeMask :: Int128
signNRegimeMask = Int128
2forall a b. (Num a, Integral b) => a -> b -> a
^Int
bitsRemaining forall a. Num a => a -> a -> a
- Int128
1
        int :: Int128
int = IntN 'IV
posit forall a. Bits a => a -> a -> a
.&. Int128
signNRegimeMask
        nBitsToTheRight :: Int
nBitsToTheRight = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @IV) forall a. Num a => a -> a -> a
- Int
numBitsRegime forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @IV) forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
exponentSize @IV)
    in if Int
bitsRemaining forall a. Ord a => a -> a -> Bool
<=Int
0
       then Natural
0
       else if Int
nBitsToTheRight forall a. Ord a => a -> a -> Bool
< Int
0
            then forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ Int128
int forall a. Bits a => a -> Int -> a
`shiftL` forall a. Num a => a -> a
negate Int
nBitsToTheRight
            else forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ Int128
int forall a. Bits a => a -> Int -> a
`shiftR` Int
nBitsToTheRight
 
  -- knowing the number of the regime bits, sign bit, and the number of the
  -- exponent bits we can extract the fraction.  We mask to the left of the fraction to
  -- remove the sign, regime, and exponent. If there is no fraction then the value is 1.
  fraction2Posit :: Int -> IntN 'IV -> Rational
fraction2Posit Int
numBitsRegime IntN 'IV
posit =
    let offset :: Integer
offset = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ (forall (es :: ES). PositC es => Natural
signBitSize @IV) forall a. Num a => a -> a -> a
+ forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
numBitsRegime forall a. Num a => a -> a -> a
+ (forall (es :: ES). PositC es => Natural
exponentSize @IV)
        fractionSize :: Integer
fractionSize = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @IV) forall a. Num a => a -> a -> a
- Integer
offset
        fractionBits :: Int128
fractionBits = IntN 'IV
posit forall a. Bits a => a -> a -> a
.&. (Int128
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
fractionSize forall a. Num a => a -> a -> a
- Int128
1)
    in if Integer
fractionSize forall a. Ord a => a -> a -> Bool
>= Integer
1
       then (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
fractionSize forall a. Num a => a -> a -> a
+ forall a. Integral a => a -> Integer
toInteger Int128
fractionBits) forall a. Integral a => a -> a -> Ratio a
% Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
fractionSize
       else Integer
1 forall a. Integral a => a -> a -> Ratio a
% Integer
1
 
  displayBin :: IntN 'IV -> String
displayBin IntN 'IV
int = String
"0b" forall a. [a] -> [a] -> [a]
++ Int -> String
go (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @IV) forall a. Num a => a -> a -> a
- Int
1)
    where
      go :: Int -> String
      go :: Int -> String
go Int
0 = if forall a. Bits a => a -> Int -> Bool
testBit IntN 'IV
int Int
0
             then String
"1"
             else String
"0"
      go Int
idx = if forall a. Bits a => a -> Int -> Bool
testBit IntN 'IV
int Int
idx
               then String
"1" forall a. [a] -> [a] -> [a]
++ Int -> String
go (Int
idx forall a. Num a => a -> a -> a
- Int
1)
               else String
"0" forall a. [a] -> [a] -> [a]
++ Int -> String
go (Int
idx forall a. Num a => a -> a -> a
-Int
1)



instance PositC V where
  type IntN V = Int256
  exponentSize :: Natural
exponentSize = Natural
5
 
  -- Posit Integer Rep of various values
  unReal :: IntN 'V
unReal = forall a. Bounded a => a
minBound @Int256
 
  mostPosVal :: IntN 'V
mostPosVal = forall a. Bounded a => a
maxBound @Int256
  leastPosVal :: IntN 'V
leastPosVal = Int256
1
  leastNegVal :: IntN 'V
leastNegVal = -Int256
1
  mostNegVal :: IntN 'V
mostNegVal = forall a. Num a => a -> a
negate forall (es :: ES). PositC es => IntN es
mostPosVal
 
  encode :: Maybe Rational -> IntN 'V
encode Maybe Rational
Nothing = forall (es :: ES). PositC es => IntN es
unReal @V
  encode (Just Rational
0) = Int256
0
  encode (Just Rational
r)
    | Rational
r forall a. Ord a => a -> a -> Bool
> forall (es :: ES). PositC es => Rational
maxPosRat @V = forall (es :: ES). PositC es => IntN es
mostPosVal @V
    | Rational
r forall a. Ord a => a -> a -> Bool
< forall (es :: ES). PositC es => Rational
minNegRat @V = forall (es :: ES). PositC es => IntN es
mostNegVal @V
    | Rational
r forall a. Ord a => a -> a -> Bool
> Rational
0 Bool -> Bool -> Bool
&& Rational
r forall a. Ord a => a -> a -> Bool
< forall (es :: ES). PositC es => Rational
minPosRat @V = forall (es :: ES). PositC es => IntN es
leastPosVal @V
    | Rational
r forall a. Ord a => a -> a -> Bool
< Rational
0 Bool -> Bool -> Bool
&& Rational
r forall a. Ord a => a -> a -> Bool
> forall (es :: ES). PositC es => Rational
maxNegRat @V = forall (es :: ES). PositC es => IntN es
leastNegVal @V
    | Bool
otherwise = forall (es :: ES). PositC es => Rational -> IntN es
buildIntRep @V Rational
r
 
  buildIntRep :: Rational -> IntN 'V
buildIntRep Rational
r =
    let (Bool
signBit,Integer
regime,Natural
exponent,Rational
significand) = forall (es :: ES).
PositC es =>
Rational -> (Bool, Integer, Natural, Rational)
posit2TupPosit @V Rational
r
        intRep :: IntN 'V
intRep = forall (es :: ES).
PositC es =>
Integer -> Natural -> Rational -> IntN es
mkIntRep @V Integer
regime Natural
exponent Rational
significand
    in if Bool
signBit
       then forall a. Num a => a -> a
negate IntN 'V
intRep
       else IntN 'V
intRep
 
  mkIntRep :: Integer -> Natural -> Rational -> IntN 'V
mkIntRep Integer
regime Natural
exponent Rational
significand =
    let (IntN 'V
regime', Integer
offset) = forall (es :: ES). PositC es => Integer -> (IntN es, Integer)
formRegime @V Integer
regime  -- offset is the number of binary digits remaining after the regime is formed
        (IntN 'V
exponent', Integer
offset') = forall (es :: ES).
PositC es =>
Natural -> Integer -> (IntN es, Integer)
formExponent @V Natural
exponent Integer
offset  -- offset' is the number of binary digits remaining after the exponent is formed
        fraction :: IntN 'V
fraction = forall (es :: ES). PositC es => Rational -> Integer -> IntN es
formFraction @V Rational
significand Integer
offset'
    in IntN 'V
regime' forall a. Bits a => a -> a -> a
.|. IntN 'V
exponent' forall a. Bits a => a -> a -> a
.|. IntN 'V
fraction
 
  formRegime :: Integer -> (IntN 'V, Integer)
formRegime Integer
power
    | Integer
0 forall a. Ord a => a -> a -> Bool
<= Integer
power =
      let offset :: Integer
offset = (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @V forall a. Num a => a -> a -> a
- Natural
1) forall a. Num a => a -> a -> a
-     Integer
power forall a. Num a => a -> a -> a
- Integer
1)
      in (forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
power forall a. Num a => a -> a -> a
+ Integer
1) forall a. Num a => a -> a -> a
- Integer
1) forall a. Bits a => a -> Int -> a
`shiftL` forall a. Num a => Integer -> a
fromInteger Integer
offset, Integer
offset forall a. Num a => a -> a -> a
- Integer
1)
    | Bool
otherwise =
      let offset :: Integer
offset = (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @V forall a. Num a => a -> a -> a
- Natural
1) forall a. Num a => a -> a -> a
- forall a. Num a => a -> a
abs Integer
power forall a. Num a => a -> a -> a
- Integer
1)
      in (Int256
1 forall a. Bits a => a -> Int -> a
`shiftL` forall a. Num a => Integer -> a
fromInteger Integer
offset, Integer
offset)
 
  formExponent :: Natural -> Integer -> (IntN 'V, Integer)
formExponent Natural
power Integer
offset =
    let offset' :: Integer
offset' = Integer
offset forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
exponentSize @V)
    in (forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
power forall a. Bits a => a -> Int -> a
`shift` forall a. Num a => Integer -> a
fromInteger Integer
offset', Integer
offset')
 
  formFraction :: Rational -> Integer -> IntN 'V
formFraction Rational
r Integer
offset =
    let numFractionBits :: Integer
numFractionBits = Integer
offset
        fractionSize :: Rational
fractionSize = Rational
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
numFractionBits
        normFraction :: Integer
normFraction = forall a b. (RealFrac a, Integral b) => a -> b
round forall a b. (a -> b) -> a -> b
$ (Rational
r forall a. Num a => a -> a -> a
- Rational
1) forall a. Num a => a -> a -> a
* Rational
fractionSize  -- "posit - 1" is changing it from the significand to the fraction: [1,2) -> [0,1)
    in if Integer
numFractionBits forall a. Ord a => a -> a -> Bool
>= Integer
1
       then forall a. Num a => Integer -> a
fromInteger Integer
normFraction
       else Int256
0
 
  decode :: IntN 'V -> Maybe Rational
decode IntN 'V
int
    | IntN 'V
int forall a. Eq a => a -> a -> Bool
== forall (es :: ES). PositC es => IntN es
unReal @V = forall a. Maybe a
Nothing
    | IntN 'V
int forall a. Eq a => a -> a -> Bool
== Int256
0 = forall a. a -> Maybe a
Just Rational
0
    | Bool
otherwise =
      let sgn :: Bool
sgn = IntN 'V
int forall a. Ord a => a -> a -> Bool
< Int256
0
          int' :: Int256
int' = if Bool
sgn
                 then forall a. Num a => a -> a
negate IntN 'V
int
                 else IntN 'V
int
          (Integer
regime,Int
nR) = forall (es :: ES). PositC es => IntN es -> (Integer, Int)
regime2Integer @V Int256
int'
          exponent :: Natural
exponent = forall (es :: ES). PositC es => Int -> IntN es -> Natural
exponent2Nat @V Int
nR Int256
int'  -- if no e or some bits missing, then they are considered zero
          rat :: Rational
rat = forall (es :: ES). PositC es => Int -> IntN es -> Rational
fraction2Posit @V Int
nR Int256
int'  -- if no fraction or some bits missing, then the missing bits are zero, making the significand p=1
      in forall (es :: ES).
PositC es =>
(Bool, Integer, Natural, Rational) -> Maybe Rational
tupPosit2Posit @V (Bool
sgn,Integer
regime,Natural
exponent,Rational
rat)
 
  regime2Integer :: IntN 'V -> (Integer, Int)
regime2Integer IntN 'V
posit =
    let regimeFormat :: Bool
regimeFormat = forall (es :: ES). PositC es => IntN es -> Bool
findRegimeFormat @V IntN 'V
posit
        regimeCount :: Int
regimeCount = forall (es :: ES). PositC es => Bool -> IntN es -> Int
countRegimeBits @V Bool
regimeFormat IntN 'V
posit
        regime :: Integer
regime = Bool -> Int -> Integer
calcRegimeInt Bool
regimeFormat Int
regimeCount
    in (Integer
regime, Int
regimeCount forall a. Num a => a -> a -> a
+ Int
1) -- a rational representation of the regime and the regimeCount plus rBar which is the numBitsRegime
 
  -- will return the format of the regime, either HI or LO; it could get refactored in the future
  -- True means a 1 is the first bit in the regime
  findRegimeFormat :: IntN 'V -> Bool
findRegimeFormat IntN 'V
posit = forall a. Bits a => a -> Int -> Bool
testBit IntN 'V
posit (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @V) forall a. Num a => a -> a -> a
- Int
1 forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @V))
 
  countRegimeBits :: Bool -> IntN 'V -> Int
countRegimeBits Bool
format IntN 'V
posit = Int -> Int -> Int
go (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @V) forall a. Num a => a -> a -> a
- Int
1 forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @V)) Int
0
    where
      go :: Int -> Int -> Int
go (-1) Int
acc = Int
acc
      go Int
index Int
acc
        | Bool -> Bool -> Bool
xnor Bool
format (forall a. Bits a => a -> Int -> Bool
testBit IntN 'V
posit Int
index)  = Int -> Int -> Int
go (Int
index forall a. Num a => a -> a -> a
- Int
1) (Int
acc forall a. Num a => a -> a -> a
+ Int
1)
        | Bool
otherwise = Int
acc
 
  -- knowing the number of the regime bits, and the sign bit we can extract
  -- the exponent.  We mask to the left of the exponent to remove the sign and regime, and
  -- then shift to the right to remove the fraction.
  exponent2Nat :: Int -> IntN 'V -> Natural
exponent2Nat Int
numBitsRegime IntN 'V
posit =
    let bitsRemaining :: Int
bitsRemaining = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @V) forall a. Num a => a -> a -> a
- Int
numBitsRegime forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @V)
        signNRegimeMask :: Int256
signNRegimeMask = Int256
2forall a b. (Num a, Integral b) => a -> b -> a
^Int
bitsRemaining forall a. Num a => a -> a -> a
- Int256
1
        int :: Int256
int = IntN 'V
posit forall a. Bits a => a -> a -> a
.&. Int256
signNRegimeMask
        nBitsToTheRight :: Int
nBitsToTheRight = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @V) forall a. Num a => a -> a -> a
- Int
numBitsRegime forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
signBitSize @V) forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
exponentSize @V)
    in if Int
bitsRemaining forall a. Ord a => a -> a -> Bool
<=Int
0
       then Natural
0
       else if Int
nBitsToTheRight forall a. Ord a => a -> a -> Bool
< Int
0
            then forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ Int256
int forall a. Bits a => a -> Int -> a
`shiftL` forall a. Num a => a -> a
negate Int
nBitsToTheRight
            else forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ Int256
int forall a. Bits a => a -> Int -> a
`shiftR` Int
nBitsToTheRight
 
  -- knowing the number of the regime bits, sign bit, and the number of the
  -- exponent bits we can extract the fraction.  We mask to the left of the fraction to
  -- remove the sign, regime, and exponent. If there is no fraction then the value is 1.
  fraction2Posit :: Int -> IntN 'V -> Rational
fraction2Posit Int
numBitsRegime IntN 'V
posit =
    let offset :: Integer
offset = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ (forall (es :: ES). PositC es => Natural
signBitSize @V) forall a. Num a => a -> a -> a
+ forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
numBitsRegime forall a. Num a => a -> a -> a
+ (forall (es :: ES). PositC es => Natural
exponentSize @V)
        fractionSize :: Integer
fractionSize = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @V) forall a. Num a => a -> a -> a
- Integer
offset
        fractionBits :: Int256
fractionBits = IntN 'V
posit forall a. Bits a => a -> a -> a
.&. (Int256
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
fractionSize forall a. Num a => a -> a -> a
- Int256
1)
    in if Integer
fractionSize forall a. Ord a => a -> a -> Bool
>= Integer
1
       then (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
fractionSize forall a. Num a => a -> a -> a
+ forall a. Integral a => a -> Integer
toInteger Int256
fractionBits) forall a. Integral a => a -> a -> Ratio a
% Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
fractionSize
       else Integer
1 forall a. Integral a => a -> a -> Ratio a
% Integer
1
 
  displayBin :: IntN 'V -> String
displayBin IntN 'V
int = String
"0b" forall a. [a] -> [a] -> [a]
++ Int -> String
go (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (es :: ES). PositC es => Natural
nBits @V) forall a. Num a => a -> a -> a
- Int
1)
    where
      go :: Int -> String
      go :: Int -> String
go Int
0 = if forall a. Bits a => a -> Int -> Bool
testBit IntN 'V
int Int
0
             then String
"1"
             else String
"0"
      go Int
idx = if forall a. Bits a => a -> Int -> Bool
testBit IntN 'V
int Int
idx
               then String
"1" forall a. [a] -> [a] -> [a]
++ Int -> String
go (Int
idx forall a. Num a => a -> a -> a
- Int
1)
               else String
"0" forall a. [a] -> [a] -> [a]
++ Int -> String
go (Int
idx forall a. Num a => a -> a -> a
-Int
1)


-- =====================================================================
-- ===                Encode and Decode Helpers                      ===
-- =====================================================================


-- getSign finds the sign value and then returns the absolute value of the Posit
getSign :: Rational -> (Bool, Rational)
getSign :: Rational -> (Bool, Rational)
getSign Rational
r =
  let s :: Bool
s = Rational
r forall a. Ord a => a -> a -> Bool
<= Rational
0
      absPosit :: Rational
absPosit =
        if Bool
s
        then forall a. Num a => a -> a
negate Rational
r
        else Rational
r
  in (Bool
s,Rational
absPosit)  -- pretty much the same as 'abs')

-- Exponent should be an integer in the range of [0,uSeed), and also return the posit [1,2)
getExponent :: Rational -> (Natural, Rational)
getExponent :: Rational -> (Natural, Rational)
getExponent Rational
r = (Natural, Rational) -> (Natural, Rational)
log_2 (Natural
0,Rational
r)

log_2 :: (Natural, Rational) -> (Natural, Rational)
log_2 :: (Natural, Rational) -> (Natural, Rational)
log_2 (Natural
exponent,Rational
r) | Rational
r forall a. Ord a => a -> a -> Bool
<  Rational
1 = forall a. HasCallStack => String -> a
error String
"Should never happen, exponent should be a natural number, i.e. positive integer."
                   | Rational
r forall a. Ord a => a -> a -> Bool
>= (Integer
2 forall a. Integral a => a -> a -> Ratio a
% Integer
1) = (Natural, Rational) -> (Natural, Rational)
log_2 (Natural
exponentforall a. Num a => a -> a -> a
+Natural
1,Rational
r forall a. Num a => a -> a -> a
* (Integer
1 forall a. Integral a => a -> a -> Ratio a
% Integer
2))
                   | Bool
otherwise = (Natural
exponent,Rational
r)


calcRegimeInt :: Bool -> Int -> Integer
calcRegimeInt :: Bool -> Int -> Integer
calcRegimeInt Bool
format Int
count | Bool
format = forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
count forall a. Num a => a -> a -> a
- Int
1)
                           | Bool
otherwise = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall a. Num a => a -> a
negate Int
count


xnor :: Bool -> Bool -> Bool
xnor :: Bool -> Bool -> Bool
xnor Bool
a Bool
b = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ (Bool
a Bool -> Bool -> Bool
|| Bool
b) Bool -> Bool -> Bool
&& Bool -> Bool
not (Bool
b Bool -> Bool -> Bool
&& Bool
a)


#ifndef O_NO_ORPHANS
#ifndef O_NO_STORABLE
-- =====================================================================
-- ===                  Storable Instances                           ===
-- =====================================================================
--
-- Orphan Instance for Word128 using the DoubleWord type class
instance Storable Word128 where
  sizeOf :: Word128 -> Int
sizeOf Word128
_ = Int
16
  alignment :: Word128 -> Int
alignment Word128
_ = Int
16
  peek :: Ptr Word128 -> IO Word128
peek Ptr Word128
ptr = do
    Word64
hi <- forall a. Storable a => Ptr a -> IO a
peek forall a b. (a -> b) -> a -> b
$ Int -> Ptr Word64
offsetInt Int
0
    Word64
lo <- forall a. Storable a => Ptr a -> IO a
peek forall a b. (a -> b) -> a -> b
$ Int -> Ptr Word64
offsetWord Int
1
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall w. DoubleWord w => HiWord w -> LoWord w -> w
fromHiAndLo Word64
hi Word64
lo
      where
        offsetInt :: Int -> Ptr Word64
offsetInt Int
i = (forall a b. Ptr a -> Ptr b
castPtr Ptr Word128
ptr :: Ptr Word64) forall a b. Ptr a -> Int -> Ptr b
`plusPtr` (Int
iforall a. Num a => a -> a -> a
*Int
8)
        offsetWord :: Int -> Ptr Word64
offsetWord Int
i = (forall a b. Ptr a -> Ptr b
castPtr Ptr Word128
ptr :: Ptr Word64) forall a b. Ptr a -> Int -> Ptr b
`plusPtr` (Int
iforall a. Num a => a -> a -> a
*Int
8)
  poke :: Ptr Word128 -> Word128 -> IO ()
poke Ptr Word128
ptr Word128
int = do
    forall a. Storable a => Ptr a -> a -> IO ()
poke (Int -> Ptr Word64
offsetInt Int
0) (forall w. DoubleWord w => w -> HiWord w
hiWord Word128
int)
    forall a. Storable a => Ptr a -> a -> IO ()
poke (Int -> Ptr Word64
offsetWord Int
1) (forall w. DoubleWord w => w -> LoWord w
loWord Word128
int)
      where
        offsetInt :: Int -> Ptr Word64
offsetInt Int
i = (forall a b. Ptr a -> Ptr b
castPtr Ptr Word128
ptr :: Ptr Word64) forall a b. Ptr a -> Int -> Ptr b
`plusPtr` (Int
iforall a. Num a => a -> a -> a
*Int
8)
        offsetWord :: Int -> Ptr Word64
offsetWord Int
i = (forall a b. Ptr a -> Ptr b
castPtr Ptr Word128
ptr :: Ptr Word64) forall a b. Ptr a -> Int -> Ptr b
`plusPtr` (Int
iforall a. Num a => a -> a -> a
*Int
8)

-- Orphan Instance for Int128 using the DoubleWord type class
instance Storable Int128 where
  sizeOf :: Int128 -> Int
sizeOf Int128
_ = Int
16
  alignment :: Int128 -> Int
alignment Int128
_ = Int
16
  peek :: Ptr Int128 -> IO Int128
peek Ptr Int128
ptr = do
    Int64
hi <- forall a. Storable a => Ptr a -> IO a
peek forall a b. (a -> b) -> a -> b
$ Int -> Ptr Int64
offsetInt Int
0
    Word64
lo <- forall a. Storable a => Ptr a -> IO a
peek forall a b. (a -> b) -> a -> b
$ Int -> Ptr Word64
offsetWord Int
1
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall w. DoubleWord w => HiWord w -> LoWord w -> w
fromHiAndLo Int64
hi Word64
lo
      where
        offsetInt :: Int -> Ptr Int64
offsetInt Int
i = (forall a b. Ptr a -> Ptr b
castPtr Ptr Int128
ptr :: Ptr Int64) forall a b. Ptr a -> Int -> Ptr b
`plusPtr` (Int
iforall a. Num a => a -> a -> a
*Int
8)
        offsetWord :: Int -> Ptr Word64
offsetWord Int
i = (forall a b. Ptr a -> Ptr b
castPtr Ptr Int128
ptr :: Ptr Word64) forall a b. Ptr a -> Int -> Ptr b
`plusPtr` (Int
iforall a. Num a => a -> a -> a
*Int
8)
  poke :: Ptr Int128 -> Int128 -> IO ()
poke Ptr Int128
ptr Int128
int = do
    forall a. Storable a => Ptr a -> a -> IO ()
poke (Int -> Ptr Int64
offsetInt Int
0) (forall w. DoubleWord w => w -> HiWord w
hiWord Int128
int)
    forall a. Storable a => Ptr a -> a -> IO ()
poke (Int -> Ptr Word64
offsetWord Int
1) (forall w. DoubleWord w => w -> LoWord w
loWord Int128
int)
      where
        offsetInt :: Int -> Ptr Int64
offsetInt Int
i = (forall a b. Ptr a -> Ptr b
castPtr Ptr Int128
ptr :: Ptr Int64) forall a b. Ptr a -> Int -> Ptr b
`plusPtr` (Int
iforall a. Num a => a -> a -> a
*Int
8)
        offsetWord :: Int -> Ptr Word64
offsetWord Int
i = (forall a b. Ptr a -> Ptr b
castPtr Ptr Int128
ptr :: Ptr Word64) forall a b. Ptr a -> Int -> Ptr b
`plusPtr` (Int
iforall a. Num a => a -> a -> a
*Int
8)

-- Orphan Instance for Int256 using the DoubleWord type class
instance Storable Int256 where
  sizeOf :: Int256 -> Int
sizeOf Int256
_ = Int
32
  alignment :: Int256 -> Int
alignment Int256
_ = Int
32
  peek :: Ptr Int256 -> IO Int256
peek Ptr Int256
ptr = do
    Int128
hi <- forall a. Storable a => Ptr a -> IO a
peek forall a b. (a -> b) -> a -> b
$ Int -> Ptr Int128
offsetInt Int
0
    Word128
lo <- forall a. Storable a => Ptr a -> IO a
peek forall a b. (a -> b) -> a -> b
$ Int -> Ptr Word128
offsetWord Int
1
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall w. DoubleWord w => HiWord w -> LoWord w -> w
fromHiAndLo Int128
hi Word128
lo
      where
        offsetInt :: Int -> Ptr Int128
offsetInt Int
i = (forall a b. Ptr a -> Ptr b
castPtr Ptr Int256
ptr :: Ptr Int128) forall a b. Ptr a -> Int -> Ptr b
`plusPtr` (Int
iforall a. Num a => a -> a -> a
*Int
16)
        offsetWord :: Int -> Ptr Word128
offsetWord Int
i = (forall a b. Ptr a -> Ptr b
castPtr Ptr Int256
ptr :: Ptr Word128) forall a b. Ptr a -> Int -> Ptr b
`plusPtr` (Int
iforall a. Num a => a -> a -> a
*Int
16)
  poke :: Ptr Int256 -> Int256 -> IO ()
poke Ptr Int256
ptr Int256
int = do
    forall a. Storable a => Ptr a -> a -> IO ()
poke (Int -> Ptr Int128
offsetInt Int
0) (forall w. DoubleWord w => w -> HiWord w
hiWord Int256
int)
    forall a. Storable a => Ptr a -> a -> IO ()
poke (Int -> Ptr Word128
offsetWord Int
1) (forall w. DoubleWord w => w -> LoWord w
loWord Int256
int)
      where
        offsetInt :: Int -> Ptr Int128
offsetInt Int
i = (forall a b. Ptr a -> Ptr b
castPtr Ptr Int256
ptr :: Ptr Int128) forall a b. Ptr a -> Int -> Ptr b
`plusPtr` (Int
iforall a. Num a => a -> a -> a
*Int
16)
        offsetWord :: Int -> Ptr Word128
offsetWord Int
i = (forall a b. Ptr a -> Ptr b
castPtr Ptr Int256
ptr :: Ptr Word128) forall a b. Ptr a -> Int -> Ptr b
`plusPtr` (Int
iforall a. Num a => a -> a -> a
*Int
16)
--
#endif
#endif