{-# 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 (..),
  SpecTransM,
  runSpecTransM,
  askCtx,
  withCtx,
  toTestRep,
  OpaqueErrorString (..),
) 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.Kind (Type)
import Data.Text (Text)
import GHC.Generics (Generic (..), K1 (..), M1 (..), U1 (..), V1, (:*:) (..), (:+:) (..))
import Test.Cardano.Ledger.TreeDiff (Expr (..), ToExpr (..))

-- | OpaqueErrorString behaves like unit in comparisons, but contains an
-- error string that can be displayed.
newtype OpaqueErrorString = OpaqueErrorString String
  deriving (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
$cto :: forall x. Rep OpaqueErrorString x -> OpaqueErrorString
$cfrom :: forall x. OpaqueErrorString -> Rep OpaqueErrorString x
Generic)

instance Eq OpaqueErrorString where
  OpaqueErrorString
_ == :: OpaqueErrorString -> OpaqueErrorString -> Bool
== OpaqueErrorString
_ = Bool
True

instance ToExpr OpaqueErrorString where
  -- Using `toExpr` on a `String` displays escape codes in place of unicode
  -- characters (e.g. "≡" becomes "\8802")
  -- TODO figure out a less hacky way to solve this problem
  toExpr :: OpaqueErrorString -> Expr
toExpr (OpaqueErrorString String
x) = String -> [Expr] -> Expr
App String
x []

instance NFData OpaqueErrorString

type SpecTranslationError = Text

newtype SpecTransM ctx a
  = SpecTransM (ExceptT SpecTranslationError (Reader ctx) a)
  deriving (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
<$ :: forall a b. a -> SpecTransM ctx b -> SpecTransM ctx a
$c<$ :: forall ctx a b. a -> SpecTransM ctx b -> SpecTransM ctx a
fmap :: forall a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
$cfmap :: forall ctx a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
Functor, 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
<* :: forall a b.
SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx a
$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 b
$c*> :: forall ctx a b.
SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx b
liftA2 :: forall a b c.
(a -> b -> c)
-> SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx c
$cliftA2 :: forall ctx a b c.
(a -> b -> c)
-> SpecTransM ctx a -> SpecTransM ctx b -> SpecTransM ctx c
<*> :: forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
$c<*> :: forall ctx a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
pure :: forall a. a -> SpecTransM ctx a
$cpure :: forall ctx a. a -> SpecTransM ctx a
Applicative, 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
return :: forall a. a -> SpecTransM ctx a
$creturn :: forall ctx a. a -> SpecTransM ctx a
>> :: 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 b
>>= :: forall a b.
SpecTransM ctx a -> (a -> SpecTransM ctx b) -> SpecTransM ctx b
$c>>= :: forall ctx a b.
SpecTransM ctx a -> (a -> SpecTransM ctx b) -> SpecTransM ctx b
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) = forall r a. Reader r a -> r -> a
runReader (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 = 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) = forall (f :: * -> *) a. GFixupSpecRep f => f a -> f a
genericFixupSpecRep f a
f forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: 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) = forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. GFixupSpecRep f => f a -> f a
genericFixupSpecRep f a
f
  genericFixupSpecRep (R1 g a
f) = forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 forall a b. (a -> b) -> a -> b
$ 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) = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall a b. (a -> b) -> a -> b
$ 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) = forall k i c (p :: k). c -> K1 i c p
K1 forall a b. (a -> b) -> a -> b
$ 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 = forall a x. Generic a => Rep a x -> a
to forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. GFixupSpecRep f => f a -> f a
genericFixupSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. FixupSpecRep a => a -> a
fixup forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks 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 forall ctx a.
ctx -> SpecTransM ctx a -> Either SpecTranslationError a
runSpecTransM ctx
ctx SpecTransM ctx a
m of
    Right a
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
    Left SpecTranslationError
e -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError SpecTranslationError
e