{-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-}
module RetroClash.BCD
    ( Digit, toDigit
    , BCD
    , fromBCD
    , BCDSize
    , toBCD
    , ShiftAdd, initBCD, stepBCD
    , prop_BCD
    ) where

import Clash.Prelude hiding (shift, add)
import RetroClash.Utils

type Digit = Index 10
type BCD n = Vec n Digit

toDigit :: Unsigned 4 -> Digit
toDigit :: Unsigned 4 -> Digit
toDigit = Unsigned 4 -> Digit
forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce

fromBCD :: BCD n -> Integer
fromBCD :: forall (n :: Nat). BCD n -> Integer
fromBCD = (Integer -> Digit -> Integer) -> Integer -> Vec n Digit -> Integer
forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
foldl (\Integer
x Digit
d -> Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
10 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Digit -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Digit
d) Integer
0

type BCDSize n = CLog 10 (2 ^ n)
type ShiftAdd n = (Vec (BCDSize n) (Unsigned 4), Unsigned n)

{-# INLINE initBCD #-}
initBCD :: (KnownNat n) => Unsigned n -> ShiftAdd n
initBCD :: forall (n :: Nat). KnownNat n => Unsigned n -> ShiftAdd n
initBCD = (,) (Unsigned 4 -> Vec (CLog 10 (2 ^ n)) (Unsigned 4)
forall (n :: Nat) a. KnownNat n => a -> Vec n a
repeat Unsigned 4
0)

stepBCD :: (KnownNat n) => ShiftAdd n -> ShiftAdd n
stepBCD :: forall (n :: Nat). KnownNat n => ShiftAdd n -> ShiftAdd n
stepBCD = (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
-> (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
forall (n :: Nat). KnownNat n => ShiftAdd n -> ShiftAdd n
shift ((Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
 -> (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n))
-> ((Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
    -> (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n))
-> (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
-> (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
-> (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
forall (n :: Nat). ShiftAdd n -> ShiftAdd n
add
  where
    shift :: (KnownNat n) => ShiftAdd n -> ShiftAdd n
    shift :: forall (n :: Nat). KnownNat n => ShiftAdd n -> ShiftAdd n
shift = (BitVector
   (BitSize (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n))
 -> BitVector
      (BitSize (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)))
-> (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
-> (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
forall a.
BitPack a =>
(BitVector (BitSize a) -> BitVector (BitSize a)) -> a -> a
bitwise (BitVector
  (BitSize (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n))
-> Int
-> BitVector
     (BitSize (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n))
forall a. Bits a => a -> Int -> a
`shiftL` Int
1)

    add :: ShiftAdd n -> ShiftAdd n
    add :: forall (n :: Nat). ShiftAdd n -> ShiftAdd n
add (Vec (BCDSize n) (Unsigned 4)
digits, Unsigned n
buf) = ((Unsigned 4 -> Unsigned 4)
-> Vec (BCDSize n) (Unsigned 4) -> Vec (BCDSize n) (Unsigned 4)
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map Unsigned 4 -> Unsigned 4
forall {a}. (Ord a, Num a) => a -> a
add3 Vec (BCDSize n) (Unsigned 4)
digits, Unsigned n
buf)
      where
        add3 :: a -> a
add3 a
d = if a
d a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
5 then a
d a -> a -> a
forall a. Num a => a -> a -> a
+ a
3 else a
d

{-# INLINE toBCD #-}
toBCD :: forall n. (KnownNat n) => Unsigned n -> BCD (BCDSize n)
toBCD :: forall (n :: Nat). KnownNat n => Unsigned n -> BCD (BCDSize n)
toBCD = (Unsigned 4 -> Digit)
-> Vec (CLog 10 (2 ^ n)) (Unsigned 4)
-> Vec (CLog 10 (2 ^ n)) Digit
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map Unsigned 4 -> Digit
toDigit (Vec (CLog 10 (2 ^ n)) (Unsigned 4) -> Vec (CLog 10 (2 ^ n)) Digit)
-> (Unsigned n -> Vec (CLog 10 (2 ^ n)) (Unsigned 4))
-> Unsigned n
-> Vec (CLog 10 (2 ^ n)) Digit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
-> Vec (CLog 10 (2 ^ n)) (Unsigned 4)
forall a b. (a, b) -> a
fst ((Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
 -> Vec (CLog 10 (2 ^ n)) (Unsigned 4))
-> (Unsigned n -> (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n))
-> Unsigned n
-> Vec (CLog 10 (2 ^ n)) (Unsigned 4)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vec (n + 1) (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
-> (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
forall (n :: Nat) a. Vec (n + 1) a -> a
last (Vec (n + 1) (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
 -> (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n))
-> (Unsigned n
    -> Vec (n + 1) (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n))
-> Unsigned n
-> (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat (n + 1)
-> ((Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
    -> (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n))
-> (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
-> Vec (n + 1) (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
forall (n :: Nat) a. SNat n -> (a -> a) -> a -> Vec n a
iterate (forall (n :: Nat). KnownNat n => SNat n
SNat @(n + 1)) (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
-> (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
forall (n :: Nat). KnownNat n => ShiftAdd n -> ShiftAdd n
stepBCD ((Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
 -> Vec (n + 1) (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n))
-> (Unsigned n -> (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n))
-> Unsigned n
-> Vec (n + 1) (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unsigned n -> (Vec (CLog 10 (2 ^ n)) (Unsigned 4), Unsigned n)
forall (n :: Nat). KnownNat n => Unsigned n -> ShiftAdd n
initBCD

roundtrip :: (KnownNat n) => Unsigned n -> Unsigned n
roundtrip :: forall (n :: Nat). KnownNat n => Unsigned n -> Unsigned n
roundtrip = Integer -> Unsigned n
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Unsigned n)
-> (Unsigned n -> Integer) -> Unsigned n -> Unsigned n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BCD (CLog 10 (2 ^ n)) -> Integer
forall (n :: Nat). BCD n -> Integer
fromBCD (BCD (CLog 10 (2 ^ n)) -> Integer)
-> (Unsigned n -> BCD (CLog 10 (2 ^ n))) -> Unsigned n -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Digit -> Digit) -> BCD (CLog 10 (2 ^ n)) -> BCD (CLog 10 (2 ^ n))
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map Digit -> Digit
forall a b. (BitPack a, BitPack b, BitSize a ~ BitSize b) => a -> b
bitCoerce (BCD (CLog 10 (2 ^ n)) -> BCD (CLog 10 (2 ^ n)))
-> (Unsigned n -> BCD (CLog 10 (2 ^ n)))
-> Unsigned n
-> BCD (CLog 10 (2 ^ n))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unsigned n -> BCD (CLog 10 (2 ^ n))
forall (n :: Nat). KnownNat n => Unsigned n -> BCD (BCDSize n)
toBCD

prop_BCD :: (KnownNat n) => Unsigned n -> Bool
prop_BCD :: forall (n :: Nat). KnownNat n => Unsigned n -> Bool
prop_BCD Unsigned n
x = Unsigned n
x Unsigned n -> Unsigned n -> Bool
forall a. Eq a => a -> a -> Bool
== Unsigned n -> Unsigned n
forall (n :: Nat). KnownNat n => Unsigned n -> Unsigned n
roundtrip Unsigned n
x