{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Test.Cardano.Ledger.Conformance.SpecTranslate.Core (
  SpecTranslationError,
  SpecTranslate (..),
  FixupSpecRep (..),
  OpaqueErrorString (..),
  SpecTransM,
  runSpecTransM,
  askCtx,
  withCtx,
  toTestRep,
  showOpaqueErrorString,
  unComputationResult,
  unComputationResult_,
) where

import Cardano.Ledger.BaseTypes (Inject (..))
import Constrained.Base ()
import Control.DeepSeq (NFData)
import Control.Monad.Except (ExceptT, MonadError (..), runExceptT)
import Control.Monad.Reader (MonadReader (..), Reader, asks, runReader)
import Data.Foldable (Foldable (..))
import Data.Kind (Type)
import Data.List.NonEmpty (NonEmpty)
import Data.Text (Text)
import qualified Data.Text as T
import Data.Void (Void)
import GHC.Generics (Generic (..), K1 (..), M1 (..), U1 (..), V1, (:*:) (..), (:+:) (..))
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.TreeDiff (Expr (..), ToExpr (..), showExpr)

type SpecTranslationError = Text

newtype SpecTransM ctx a
  = SpecTransM (ExceptT SpecTranslationError (Reader ctx) a)
  deriving ((forall a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b)
-> (forall a b. a -> SpecTransM ctx b -> SpecTransM ctx a)
-> Functor (SpecTransM ctx)
forall a b. a -> SpecTransM ctx b -> SpecTransM ctx a
forall a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall ctx a b. a -> SpecTransM ctx b -> SpecTransM ctx a
forall ctx a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall ctx a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
fmap :: forall a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
$c<$ :: forall ctx a b. a -> SpecTransM ctx b -> SpecTransM ctx a
<$ :: forall a b. a -> SpecTransM ctx b -> SpecTransM ctx a
Functor, Functor (SpecTransM ctx)
Functor (SpecTransM ctx) =>
(forall a. a -> SpecTransM ctx a)
-> (forall a b.
    SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b)
-> (forall a b c.
    (a -> b -> c)
    -> SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx c)
-> (forall a b.
    SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx b)
-> (forall a b.
    SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx a)
-> Applicative (SpecTransM ctx)
forall ctx. Functor (SpecTransM ctx)
forall a. a -> SpecTransM ctx a
forall ctx a. a -> SpecTransM ctx a
forall a b.
SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx a
forall a b.
SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx b
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall ctx a b.
SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx a
forall ctx a b.
SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx b
forall ctx a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall a b c.
(a -> b -> c)
-> SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx c
forall ctx a b c.
(a -> b -> c)
-> SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall ctx a. a -> SpecTransM ctx a
pure :: forall a. a -> SpecTransM ctx a
$c<*> :: forall ctx a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
<*> :: forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
$cliftA2 :: forall ctx a b c.
(a -> b -> c)
-> SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx c
liftA2 :: forall a b c.
(a -> b -> c)
-> SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx c
$c*> :: forall ctx a b.
SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx b
*> :: forall a b.
SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx b
$c<* :: forall ctx a b.
SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx a
<* :: forall a b.
SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx a
Applicative, Applicative (SpecTransM ctx)
Applicative (SpecTransM ctx) =>
(forall a b.
 SpecTransM ctx a -> (a -> SpecTransM ctx b) -> SpecTransM ctx b)
-> (forall a b.
    SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx b)
-> (forall a. a -> SpecTransM ctx a)
-> Monad (SpecTransM ctx)
forall ctx. Applicative (SpecTransM ctx)
forall a. a -> SpecTransM ctx a
forall ctx a. a -> SpecTransM ctx a
forall a b.
SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx b
forall a b.
SpecTransM ctx a -> (a -> SpecTransM ctx b) -> SpecTransM ctx b
forall ctx a b.
SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx b
forall ctx a b.
SpecTransM ctx a -> (a -> SpecTransM ctx b) -> SpecTransM ctx b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall ctx a b.
SpecTransM ctx a -> (a -> SpecTransM ctx b) -> SpecTransM ctx b
>>= :: forall a b.
SpecTransM ctx a -> (a -> SpecTransM ctx b) -> SpecTransM ctx b
$c>> :: forall ctx a b.
SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx b
>> :: forall a b.
SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx b
$creturn :: forall ctx a. a -> SpecTransM ctx a
return :: forall a. a -> SpecTransM ctx a
Monad, MonadError SpecTranslationError, MonadReader ctx)

runSpecTransM :: ctx -> SpecTransM ctx a -> Either SpecTranslationError a
runSpecTransM :: forall ctx a.
ctx -> SpecTransM ctx a -> Either SpecTranslationError a
runSpecTransM ctx
ctx (SpecTransM ExceptT SpecTranslationError (Reader ctx) a
m) = Reader ctx (Either SpecTranslationError a)
-> ctx -> Either SpecTranslationError a
forall r a. Reader r a -> r -> a
runReader (ExceptT SpecTranslationError (Reader ctx) a
-> Reader ctx (Either SpecTranslationError a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT SpecTranslationError (Reader ctx) a
m) ctx
ctx

class SpecTranslate ctx a where
  type SpecRep a :: Type

  toSpecRep :: a -> SpecTransM ctx (SpecRep a)

class GFixupSpecRep f where
  genericFixupSpecRep :: f a -> f a

instance GFixupSpecRep U1 where
  genericFixupSpecRep :: forall a. U1 a -> U1 a
genericFixupSpecRep U1 a
U1 = U1 a
forall k (p :: k). U1 p
U1

instance GFixupSpecRep V1 where
  genericFixupSpecRep :: forall a. V1 a -> V1 a
genericFixupSpecRep = \case {}

instance (GFixupSpecRep f, GFixupSpecRep g) => GFixupSpecRep (f :*: g) where
  genericFixupSpecRep :: forall a. (:*:) f g a -> (:*:) f g a
genericFixupSpecRep (f a
f :*: g a
g) = f a -> f a
forall a. f a -> f a
forall (f :: * -> *) a. GFixupSpecRep f => f a -> f a
genericFixupSpecRep f a
f f a -> g a -> (:*:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a -> g a
forall a. g a -> g a
forall (f :: * -> *) a. GFixupSpecRep f => f a -> f a
genericFixupSpecRep g a
g

instance (GFixupSpecRep f, GFixupSpecRep g) => GFixupSpecRep (f :+: g) where
  genericFixupSpecRep :: forall a. (:+:) f g a -> (:+:) f g a
genericFixupSpecRep (L1 f a
f) = f a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (f a -> (:+:) f g a) -> f a -> (:+:) f g a
forall a b. (a -> b) -> a -> b
$ f a -> f a
forall a. f a -> f a
forall (f :: * -> *) a. GFixupSpecRep f => f a -> f a
genericFixupSpecRep f a
f
  genericFixupSpecRep (R1 g a
f) = g a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (g a -> (:+:) f g a) -> g a -> (:+:) f g a
forall a b. (a -> b) -> a -> b
$ g a -> g a
forall a. g a -> g a
forall (f :: * -> *) a. GFixupSpecRep f => f a -> f a
genericFixupSpecRep g a
f

instance GFixupSpecRep a => GFixupSpecRep (M1 i c a) where
  genericFixupSpecRep :: forall a. M1 i c a a -> M1 i c a a
genericFixupSpecRep (M1 a a
x) = a a -> M1 i c a a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (a a -> M1 i c a a) -> a a -> M1 i c a a
forall a b. (a -> b) -> a -> b
$ a a -> a a
forall a. a a -> a a
forall (f :: * -> *) a. GFixupSpecRep f => f a -> f a
genericFixupSpecRep a a
x

instance FixupSpecRep a => GFixupSpecRep (K1 i a) where
  genericFixupSpecRep :: forall a. K1 i a a -> K1 i a a
genericFixupSpecRep (K1 a
x) = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (a -> K1 i a a) -> a -> K1 i a a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. FixupSpecRep a => a -> a
fixup a
x

class FixupSpecRep a where
  fixup :: a -> a
  default fixup :: (Generic a, GFixupSpecRep (Rep a)) => a -> a
  fixup = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> (a -> Rep a Any) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep a Any -> Rep a Any
forall a. Rep a a -> Rep a a
forall (f :: * -> *) a. GFixupSpecRep f => f a -> f a
genericFixupSpecRep (Rep a Any -> Rep a Any) -> (a -> Rep a Any) -> a -> Rep a Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from

toTestRep :: (SpecTranslate ctx a, FixupSpecRep (SpecRep a)) => a -> SpecTransM ctx (SpecRep a)
toTestRep :: forall ctx a.
(SpecTranslate ctx a, FixupSpecRep (SpecRep a)) =>
a -> SpecTransM ctx (SpecRep a)
toTestRep = (SpecRep a -> SpecRep a)
-> SpecTransM ctx (SpecRep a) -> SpecTransM ctx (SpecRep a)
forall a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SpecRep a -> SpecRep a
forall a. FixupSpecRep a => a -> a
fixup (SpecTransM ctx (SpecRep a) -> SpecTransM ctx (SpecRep a))
-> (a -> SpecTransM ctx (SpecRep a))
-> a
-> SpecTransM ctx (SpecRep a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep

askCtx :: forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx :: forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx = (ctx -> b) -> SpecTransM ctx b
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ctx -> b
forall t s. Inject t s => t -> s
inject

withCtx :: ctx -> SpecTransM ctx a -> SpecTransM ctx' a
withCtx :: forall ctx a ctx'. ctx -> SpecTransM ctx a -> SpecTransM ctx' a
withCtx ctx
ctx SpecTransM ctx a
m = do
  case ctx -> SpecTransM ctx a -> Either SpecTranslationError a
forall ctx a.
ctx -> SpecTransM ctx a -> Either SpecTranslationError a
runSpecTransM ctx
ctx SpecTransM ctx a
m of
    Right a
x -> a -> SpecTransM ctx' a
forall a. a -> SpecTransM ctx' a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
    Left SpecTranslationError
e -> SpecTranslationError -> SpecTransM ctx' a
forall a. SpecTranslationError -> SpecTransM ctx' a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError SpecTranslationError
e

-- | OpaqueErrorString behaves like unit in comparisons, but contains an
-- error string that can be displayed.
newtype OpaqueErrorString = OpaqueErrorString (NonEmpty Text)
  deriving ((forall x. OpaqueErrorString -> Rep OpaqueErrorString x)
-> (forall x. Rep OpaqueErrorString x -> OpaqueErrorString)
-> Generic OpaqueErrorString
forall x. Rep OpaqueErrorString x -> OpaqueErrorString
forall x. OpaqueErrorString -> Rep OpaqueErrorString x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. OpaqueErrorString -> Rep OpaqueErrorString x
from :: forall x. OpaqueErrorString -> Rep OpaqueErrorString x
$cto :: forall x. Rep OpaqueErrorString x -> OpaqueErrorString
to :: forall x. Rep OpaqueErrorString x -> OpaqueErrorString
Generic, Int -> OpaqueErrorString -> ShowS
[OpaqueErrorString] -> ShowS
OpaqueErrorString -> String
(Int -> OpaqueErrorString -> ShowS)
-> (OpaqueErrorString -> String)
-> ([OpaqueErrorString] -> ShowS)
-> Show OpaqueErrorString
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> OpaqueErrorString -> ShowS
showsPrec :: Int -> OpaqueErrorString -> ShowS
$cshow :: OpaqueErrorString -> String
show :: OpaqueErrorString -> String
$cshowList :: [OpaqueErrorString] -> ShowS
showList :: [OpaqueErrorString] -> ShowS
Show, NonEmpty OpaqueErrorString -> OpaqueErrorString
OpaqueErrorString -> OpaqueErrorString -> OpaqueErrorString
(OpaqueErrorString -> OpaqueErrorString -> OpaqueErrorString)
-> (NonEmpty OpaqueErrorString -> OpaqueErrorString)
-> (forall b.
    Integral b =>
    b -> OpaqueErrorString -> OpaqueErrorString)
-> Semigroup OpaqueErrorString
forall b. Integral b => b -> OpaqueErrorString -> OpaqueErrorString
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
$c<> :: OpaqueErrorString -> OpaqueErrorString -> OpaqueErrorString
<> :: OpaqueErrorString -> OpaqueErrorString -> OpaqueErrorString
$csconcat :: NonEmpty OpaqueErrorString -> OpaqueErrorString
sconcat :: NonEmpty OpaqueErrorString -> OpaqueErrorString
$cstimes :: forall b. Integral b => b -> OpaqueErrorString -> OpaqueErrorString
stimes :: forall b. Integral b => b -> OpaqueErrorString -> OpaqueErrorString
Semigroup)

-- | This implementation violates referential transparency. Do not rely on it
-- unless you know what you're doing.
instance Eq OpaqueErrorString where
  OpaqueErrorString
_ == :: OpaqueErrorString -> OpaqueErrorString -> Bool
== OpaqueErrorString
_ = Bool
True

instance ToExpr OpaqueErrorString where
  toExpr :: OpaqueErrorString -> Expr
toExpr (OpaqueErrorString NonEmpty SpecTranslationError
x) = String -> [Expr] -> Expr
App (SpecTranslationError -> String
T.unpack (SpecTranslationError -> String)
-> ([SpecTranslationError] -> SpecTranslationError)
-> [SpecTranslationError]
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SpecTranslationError] -> SpecTranslationError
T.unlines ([SpecTranslationError] -> String)
-> [SpecTranslationError] -> String
forall a b. (a -> b) -> a -> b
$ NonEmpty SpecTranslationError -> [SpecTranslationError]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty SpecTranslationError
x) []

instance NFData OpaqueErrorString

showOpaqueErrorString :: ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString :: forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString = NonEmpty SpecTranslationError -> OpaqueErrorString
OpaqueErrorString (NonEmpty SpecTranslationError -> OpaqueErrorString)
-> (a -> NonEmpty SpecTranslationError) -> a -> OpaqueErrorString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecTranslationError -> NonEmpty SpecTranslationError
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SpecTranslationError -> NonEmpty SpecTranslationError)
-> (a -> SpecTranslationError)
-> a
-> NonEmpty SpecTranslationError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> SpecTranslationError
T.pack (String -> SpecTranslationError)
-> (a -> String) -> a -> SpecTranslationError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> String
forall a. ToExpr a => a -> String
showExpr

unComputationResult :: Agda.ComputationResult Text a -> Either OpaqueErrorString a
unComputationResult :: forall a.
ComputationResult SpecTranslationError a
-> Either OpaqueErrorString a
unComputationResult (Agda.Success a
x) = a -> Either OpaqueErrorString a
forall a b. b -> Either a b
Right a
x
unComputationResult (Agda.Failure SpecTranslationError
e) = OpaqueErrorString -> Either OpaqueErrorString a
forall a b. a -> Either a b
Left (NonEmpty SpecTranslationError -> OpaqueErrorString
OpaqueErrorString (NonEmpty SpecTranslationError -> OpaqueErrorString)
-> NonEmpty SpecTranslationError -> OpaqueErrorString
forall a b. (a -> b) -> a -> b
$ SpecTranslationError -> NonEmpty SpecTranslationError
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SpecTranslationError
e)

unComputationResult_ :: Agda.ComputationResult Void a -> Either e a
unComputationResult_ :: forall a e. ComputationResult Void a -> Either e a
unComputationResult_ (Agda.Success a
x) = a -> Either e a
forall a b. b -> Either a b
Right a
x
unComputationResult_ (Agda.Failure Void
x) = case Void
x of {}