{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Test.Cardano.Ledger.Conformance.Utils where

import Cardano.Crypto.Hash (ByteString, Hash, HashAlgorithm, hashFromBytes, hashToBytes, sizeHash)
import Cardano.Crypto.Util (bytesToNatural, naturalToBytes)
import Data.Bifunctor (Bifunctor (..))
import Data.Bitraversable (bimapM)
import qualified Data.ByteString.Base16 as B16
import Data.Containers.ListUtils (nubOrdOn)
import Data.Data (Proxy (..))
import Data.Foldable (Foldable (..))
import Data.List (sortOn)
import MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.TreeDiff (Expr, ToExpr (..))

agdaHashToBytes :: Int -> Integer -> ByteString
agdaHashToBytes :: Int -> Integer -> ByteString
agdaHashToBytes Int
hs = ByteString -> ByteString
B16.encode (ByteString -> ByteString)
-> (Integer -> ByteString) -> Integer -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Natural -> ByteString
naturalToBytes Int
hs (Natural -> ByteString)
-> (Integer -> Natural) -> Integer -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Natural
forall a. Num a => Integer -> a
fromInteger

agdaHashToExpr :: Int -> Integer -> Expr
agdaHashToExpr :: Int -> Integer -> Expr
agdaHashToExpr Int
hs = ByteString -> Expr
forall a. ToExpr a => a -> Expr
toExpr (ByteString -> Expr) -> (Integer -> ByteString) -> Integer -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer -> ByteString
agdaHashToBytes Int
hs

hashToInteger :: Hash a b -> Integer
hashToInteger :: forall a b. Hash a b -> Integer
hashToInteger = Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (Natural -> Integer)
-> (Hash a b -> Natural) -> Hash a b -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Natural
bytesToNatural (ByteString -> Natural)
-> (Hash a b -> ByteString) -> Hash a b -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hash a b -> ByteString
forall h a. Hash h a -> ByteString
hashToBytes

integerToHash :: forall h a. HashAlgorithm h => Integer -> Maybe (Hash h a)
integerToHash :: forall h a. HashAlgorithm h => Integer -> Maybe (Hash h a)
integerToHash = ByteString -> Maybe (Hash h a)
forall h a. HashAlgorithm h => ByteString -> Maybe (Hash h a)
hashFromBytes (ByteString -> Maybe (Hash h a))
-> (Integer -> ByteString) -> Integer -> Maybe (Hash h a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Natural -> ByteString
naturalToBytes (Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word -> Int) -> (Proxy h -> Word) -> Proxy h -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy h -> Word
forall h (proxy :: * -> *). HashAlgorithm h => proxy h -> Word
sizeHash (Proxy h -> Int) -> Proxy h -> Int
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @h) (Natural -> ByteString)
-> (Integer -> Natural) -> Integer -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Natural
forall a. Num a => Integer -> a
fromInteger

-- HSMap utils

unionsHSMap :: Ord k => [Agda.HSMap k v] -> Agda.HSMap k v
unionsHSMap :: forall k v. Ord k => [HSMap k v] -> HSMap k v
unionsHSMap = [(k, v)] -> HSMap k v
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(k, v)] -> HSMap k v)
-> ([HSMap k v] -> [(k, v)]) -> [HSMap k v] -> HSMap k v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((k, v) -> k) -> [(k, v)] -> [(k, v)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (k, v) -> k
forall a b. (a, b) -> a
fst ([(k, v)] -> [(k, v)])
-> ([HSMap k v] -> [(k, v)]) -> [HSMap k v] -> [(k, v)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((k, v) -> k) -> [(k, v)] -> [(k, v)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOrdOn (k, v) -> k
forall a b. (a, b) -> a
fst ([(k, v)] -> [(k, v)])
-> ([HSMap k v] -> [(k, v)]) -> [HSMap k v] -> [(k, v)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HSMap k v -> [(k, v)] -> [(k, v)])
-> [(k, v)] -> [HSMap k v] -> [(k, v)]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr' (\(Agda.MkHSMap [(k, v)]
x) [(k, v)]
y -> [(k, v)]
x [(k, v)] -> [(k, v)] -> [(k, v)]
forall a. Semigroup a => a -> a -> a
<> [(k, v)]
y) []

unionHSMap :: Ord k => Agda.HSMap k v -> Agda.HSMap k v -> Agda.HSMap k v
unionHSMap :: forall k v. Ord k => HSMap k v -> HSMap k v -> HSMap k v
unionHSMap HSMap k v
x HSMap k v
y = [HSMap k v] -> HSMap k v
forall k v. Ord k => [HSMap k v] -> HSMap k v
unionsHSMap [HSMap k v
x, HSMap k v
y]

mapHSMapKey :: (k -> l) -> Agda.HSMap k v -> Agda.HSMap l v
mapHSMapKey :: forall k l v. (k -> l) -> HSMap k v -> HSMap l v
mapHSMapKey k -> l
f (Agda.MkHSMap [(k, v)]
l) = [(l, v)] -> HSMap l v
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(l, v)] -> HSMap l v) -> [(l, v)] -> HSMap l v
forall a b. (a -> b) -> a -> b
$ (k -> l) -> (k, v) -> (l, v)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first k -> l
f ((k, v) -> (l, v)) -> [(k, v)] -> [(l, v)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(k, v)]
l

bimapMHSMap :: Applicative m => (k -> m k') -> (v -> m v') -> Agda.HSMap k v -> m (Agda.HSMap k' v')
bimapMHSMap :: forall (m :: * -> *) k k' v v'.
Applicative m =>
(k -> m k') -> (v -> m v') -> HSMap k v -> m (HSMap k' v')
bimapMHSMap k -> m k'
f v -> m v'
g (Agda.MkHSMap [(k, v)]
m) = [(k', v')] -> HSMap k' v'
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(k', v')] -> HSMap k' v') -> m [(k', v')] -> m (HSMap k' v')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((k, v) -> m (k', v')) -> [(k, v)] -> m [(k', v')]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((k -> m k') -> (v -> m v') -> (k, v) -> m (k', v')
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bimapM k -> m k'
f v -> m v'
g) [(k, v)]
m