{-# 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 Lib 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 -> 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 Text a
runSpecTransM ctx
ctx (SpecTransM ExceptT Text (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 Text (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 Text a
runSpecTransM ctx
ctx SpecTransM ctx a
m of
    Right a
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
    Left Text
e -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError Text
e

-- | OpaqueErrorString behaves like unit in comparisons, but contains an
-- error string that can be displayed.
newtype OpaqueErrorString = OpaqueErrorString (NonEmpty Text)
  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, Int -> OpaqueErrorString -> ShowS
[OpaqueErrorString] -> ShowS
OpaqueErrorString -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OpaqueErrorString] -> ShowS
$cshowList :: [OpaqueErrorString] -> ShowS
show :: OpaqueErrorString -> String
$cshow :: OpaqueErrorString -> String
showsPrec :: Int -> OpaqueErrorString -> ShowS
$cshowsPrec :: Int -> OpaqueErrorString -> ShowS
Show, NonEmpty OpaqueErrorString -> OpaqueErrorString
OpaqueErrorString -> OpaqueErrorString -> 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
stimes :: forall b. Integral b => b -> OpaqueErrorString -> OpaqueErrorString
$cstimes :: forall b. Integral b => b -> OpaqueErrorString -> OpaqueErrorString
sconcat :: NonEmpty OpaqueErrorString -> OpaqueErrorString
$csconcat :: NonEmpty OpaqueErrorString -> OpaqueErrorString
<> :: OpaqueErrorString -> OpaqueErrorString -> OpaqueErrorString
$c<> :: OpaqueErrorString -> 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 Text
x) = String -> [Expr] -> Expr
App (Text -> String
T.unpack forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> Text
T.unlines forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty Text
x) []

instance NFData OpaqueErrorString

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

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

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