module Test.Cardano.Ledger.Conformance.Utils where

import Cardano.Crypto.Hash (ByteString, Hash, hashToBytes)
import Cardano.Crypto.Util (bytesToNatural, naturalToBytes)
import qualified Data.ByteString.Base16 as B16
import qualified Lib as Agda
import Test.Cardano.Ledger.TreeDiff (Expr, ToExpr (..))

agdaHashToBytes :: Int -> Integer -> ByteString
agdaHashToBytes :: Int -> Integer -> ByteString
agdaHashToBytes Int
hashSize = ByteString -> ByteString
B16.encode forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Natural -> ByteString
naturalToBytes Int
hashSize 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
hashSize = forall a. ToExpr a => a -> Expr
toExpr forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer -> ByteString
agdaHashToBytes Int
hashSize

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

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