{-# 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 Cardano.Ledger.Crypto (Crypto (..), StandardCrypto)
import qualified Data.ByteString.Base16 as B16
import Data.Data (Proxy (..))
import qualified Lib as Agda
import Test.Cardano.Ledger.TreeDiff (Expr, ToExpr (..))

standardHashSize :: Int
standardHashSize :: Int
standardHashSize = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall h (proxy :: * -> *). HashAlgorithm h => proxy h -> Word
sizeHash forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @(HASH StandardCrypto)

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

agdaHashToExpr :: Int -> Integer -> Expr
agdaHashToExpr :: Int -> Integer -> Expr
agdaHashToExpr Int
hs = forall a. ToExpr a => a -> Expr
toExpr 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 = forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Natural
bytesToNatural forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall h a. HashAlgorithm h => ByteString -> Maybe (Hash h a)
hashFromBytes forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Natural -> ByteString
naturalToBytes (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall h (proxy :: * -> *). HashAlgorithm h => proxy h -> Word
sizeHash forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @h) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => Integer -> a
fromInteger

computationResultToEither :: Agda.ComputationResult e a -> Either e a
computationResultToEither :: forall e a. ComputationResult e a -> Either e a
computationResultToEither (Agda.Success a
x) = forall a b. b -> Either a b
Right a
x
computationResultToEither (Agda.Failure e
e) = forall a b. a -> Either a b
Left e
e