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

module Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecTranslate (..),
  SpecNormalize (..),
  OpaqueErrorString (..),
  SpecTransM,
  runSpecTransM,
  askCtx,
  withCtx,
  unComputationResult,
  unComputationResult_,
  toSpecRep_,
) where

import Cardano.Ledger.BaseTypes (Inject (..), NonNegativeInterval, UnitInterval, unboundRational)
import Cardano.Ledger.Binary (Sized (..))
import Cardano.Ledger.Compactible (Compactible (..), fromCompact)
import Control.DeepSeq (NFData)
import Control.Monad.Except (ExceptT, MonadError (..), runExceptT)
import Control.Monad.Reader (MonadReader (..), Reader, asks, runReader)
import Data.Bitraversable (bimapM)
import Data.Foldable (Foldable (..))
import Data.Kind (Type)
import Data.List.NonEmpty (NonEmpty)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe.Strict (StrictMaybe (..), strictMaybeToMaybe)
import Data.OMap.Strict (OMap)
import qualified Data.OMap.Strict as OMap
import Data.OSet.Strict (OSet)
import Data.Sequence (Seq)
import Data.Sequence.Strict (StrictSeq)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Text (Text)
import qualified Data.Text as T
import Data.Void (Void, absurd)
import Data.Word (Word16, Word32, Word64)
import GHC.Generics (Generic (..), K1 (..), M1 (..), U1 (..), V1, (:*:) (..), (:+:) (..))
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.TreeDiff (Expr (..), ToExpr (..))

newtype SpecTransM ctx a
  = SpecTransM (ExceptT Text (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 Text, MonadReader ctx)

runSpecTransM :: ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM :: forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM ctx
ctx (SpecTransM ExceptT Text (Reader ctx) a
m) = Reader ctx (Either Text a) -> ctx -> Either Text a
forall r a. Reader r a -> r -> a
runReader (ExceptT Text (Reader ctx) a -> Reader ctx (Either Text a)
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)

instance SpecTranslate ctx () where
  type SpecRep () = ()

  toSpecRep :: () -> SpecTransM ctx (SpecRep ())
toSpecRep = () -> SpecTransM ctx ()
() -> SpecTransM ctx (SpecRep ())
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance SpecTranslate ctx Bool where
  type SpecRep Bool = Bool

  toSpecRep :: Bool -> SpecTransM ctx (SpecRep Bool)
toSpecRep = Bool -> SpecTransM ctx Bool
Bool -> SpecTransM ctx (SpecRep Bool)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance SpecTranslate ctx Integer where
  type SpecRep Integer = Integer

  toSpecRep :: Integer -> SpecTransM ctx (SpecRep Integer)
toSpecRep = Integer -> SpecTransM ctx Integer
Integer -> SpecTransM ctx (SpecRep Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance SpecTranslate ctx Void where
  type SpecRep Void = Void

  toSpecRep :: Void -> SpecTransM ctx (SpecRep Void)
toSpecRep = Void -> SpecTransM ctx Void
Void -> SpecTransM ctx (SpecRep Void)
forall a. Void -> a
absurd

instance SpecTranslate ctx Word16 where
  type SpecRep Word16 = Integer

  toSpecRep :: Word16 -> SpecTransM ctx (SpecRep Word16)
toSpecRep = Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM ctx Integer)
-> (Word16 -> Integer) -> Word16 -> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger

instance SpecTranslate ctx Word32 where
  type SpecRep Word32 = Integer

  toSpecRep :: Word32 -> SpecTransM ctx (SpecRep Word32)
toSpecRep = Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM ctx Integer)
-> (Word32 -> Integer) -> Word32 -> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger

instance SpecTranslate ctx Word64 where
  type SpecRep Word64 = Integer

  toSpecRep :: Word64 -> SpecTransM ctx (SpecRep Word64)
toSpecRep = Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM ctx Integer)
-> (Word64 -> Integer) -> Word64 -> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> Integer
forall a. Integral a => a -> Integer
toInteger

instance
  ( SpecTranslate ctx a
  , SpecTranslate ctx b
  ) =>
  SpecTranslate ctx (a, b)
  where
  type SpecRep (a, b) = (SpecRep a, SpecRep b)

  toSpecRep :: (a, b) -> SpecTransM ctx (SpecRep (a, b))
toSpecRep (a
x, b
y) = (,) (SpecRep a -> SpecRep b -> (SpecRep a, SpecRep b))
-> SpecTransM ctx (SpecRep a)
-> SpecTransM ctx (SpecRep b -> (SpecRep a, SpecRep b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
x SpecTransM ctx (SpecRep b -> (SpecRep a, SpecRep b))
-> SpecTransM ctx (SpecRep b)
-> SpecTransM ctx (SpecRep a, SpecRep b)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> SpecTransM ctx (SpecRep b)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep b
y

instance SpecTranslate ctx a => SpecTranslate ctx [a] where
  type SpecRep [a] = [SpecRep a]

  toSpecRep :: [a] -> SpecTransM ctx (SpecRep [a])
toSpecRep = (a -> SpecTransM ctx (SpecRep a))
-> [a] -> SpecTransM ctx [SpecRep a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep

instance SpecTranslate ctx a => SpecTranslate ctx (StrictMaybe a) where
  type SpecRep (StrictMaybe a) = Maybe (SpecRep a)

  toSpecRep :: StrictMaybe a -> SpecTransM ctx (SpecRep (StrictMaybe a))
toSpecRep = Maybe a -> SpecTransM ctx (Maybe (SpecRep a))
Maybe a -> SpecTransM ctx (SpecRep (Maybe a))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Maybe a -> SpecTransM ctx (Maybe (SpecRep a)))
-> (StrictMaybe a -> Maybe a)
-> StrictMaybe a
-> SpecTransM ctx (Maybe (SpecRep a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictMaybe a -> Maybe a
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe

instance SpecTranslate ctx a => SpecTranslate ctx (Maybe a) where
  type SpecRep (Maybe a) = Maybe (SpecRep a)

  toSpecRep :: Maybe a -> SpecTransM ctx (SpecRep (Maybe a))
toSpecRep = (a -> SpecTransM ctx (SpecRep a))
-> Maybe a -> SpecTransM ctx (Maybe (SpecRep a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep

instance SpecTranslate ctx a => SpecTranslate ctx (StrictSeq a) where
  type SpecRep (StrictSeq a) = [SpecRep a]

  toSpecRep :: StrictSeq a -> SpecTransM ctx (SpecRep (StrictSeq a))
toSpecRep = (a -> SpecTransM ctx (SpecRep a))
-> [a] -> SpecTransM ctx [SpecRep a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ([a] -> SpecTransM ctx [SpecRep a])
-> (StrictSeq a -> [a])
-> StrictSeq a
-> SpecTransM ctx [SpecRep a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictSeq a -> [a]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

instance SpecTranslate ctx a => SpecTranslate ctx (Seq a) where
  type SpecRep (Seq a) = [SpecRep a]

  toSpecRep :: Seq a -> SpecTransM ctx (SpecRep (Seq a))
toSpecRep = (a -> SpecTransM ctx (SpecRep a))
-> [a] -> SpecTransM ctx [SpecRep a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ([a] -> SpecTransM ctx [SpecRep a])
-> (Seq a -> [a]) -> Seq a -> SpecTransM ctx [SpecRep a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Seq a -> [a]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

instance SpecTranslate ctx a => SpecTranslate ctx (OSet a) where
  type SpecRep (OSet a) = [SpecRep a]

  toSpecRep :: OSet a -> SpecTransM ctx (SpecRep (OSet a))
toSpecRep = (a -> SpecTransM ctx (SpecRep a))
-> [a] -> SpecTransM ctx [SpecRep a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ([a] -> SpecTransM ctx [SpecRep a])
-> (OSet a -> [a]) -> OSet a -> SpecTransM ctx [SpecRep a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OSet a -> [a]
forall a. OSet a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

instance
  ( SpecTranslate ctx k
  , SpecTranslate ctx v
  , Ord k
  ) =>
  SpecTranslate ctx (OMap k v)
  where
  type SpecRep (OMap k v) = [(SpecRep k, SpecRep v)]

  toSpecRep :: OMap k v -> SpecTransM ctx (SpecRep (OMap k v))
toSpecRep = ((k, v) -> SpecTransM ctx (SpecRep k, SpecRep v))
-> [(k, v)] -> SpecTransM ctx [(SpecRep k, SpecRep v)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((k -> SpecTransM ctx (SpecRep k))
-> (v -> SpecTransM ctx (SpecRep v))
-> (k, v)
-> SpecTransM ctx (SpecRep k, SpecRep v)
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bimapM k -> SpecTransM ctx (SpecRep k)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep v -> SpecTransM ctx (SpecRep v)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep) ([(k, v)] -> SpecTransM ctx [(SpecRep k, SpecRep v)])
-> (OMap k v -> [(k, v)])
-> OMap k v
-> SpecTransM ctx [(SpecRep k, SpecRep v)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OMap k v -> [(k, v)]
forall k v. Ord k => OMap k v -> [(k, v)]
OMap.assocList

instance (SpecTranslate ctx a, Compactible a) => SpecTranslate ctx (CompactForm a) where
  type SpecRep (CompactForm a) = SpecRep a

  toSpecRep :: CompactForm a -> SpecTransM ctx (SpecRep (CompactForm a))
toSpecRep = a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (a -> SpecTransM ctx (SpecRep a))
-> (CompactForm a -> a)
-> CompactForm a
-> SpecTransM ctx (SpecRep a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompactForm a -> a
forall a. Compactible a => CompactForm a -> a
fromCompact

instance SpecTranslate ctx a => SpecTranslate ctx (Sized a) where
  type SpecRep (Sized a) = SpecRep a

  toSpecRep :: Sized a -> SpecTransM ctx (SpecRep (Sized a))
toSpecRep (Sized a
x Int64
_) = a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
x

instance SpecTranslate ctx a => SpecTranslate ctx (Set a) where
  type SpecRep (Set a) = Agda.HSSet (SpecRep a)

  toSpecRep :: Set a -> SpecTransM ctx (SpecRep (Set a))
toSpecRep = ([SpecRep a] -> HSSet (SpecRep a))
-> SpecTransM ctx [SpecRep a] -> SpecTransM ctx (HSSet (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] -> HSSet (SpecRep a)
forall a. [a] -> HSSet a
Agda.MkHSSet (SpecTransM ctx [SpecRep a] -> SpecTransM ctx (HSSet (SpecRep a)))
-> (Set a -> SpecTransM ctx [SpecRep a])
-> Set a
-> SpecTransM ctx (HSSet (SpecRep a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> SpecTransM ctx (SpecRep a))
-> [a] -> SpecTransM ctx [SpecRep a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ([a] -> SpecTransM ctx [SpecRep a])
-> (Set a -> [a]) -> Set a -> SpecTransM ctx [SpecRep a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set a -> [a]
forall a. Set a -> [a]
Set.toList

instance SpecTranslate ctx UnitInterval where
  type SpecRep UnitInterval = Agda.Rational

  toSpecRep :: UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
toSpecRep = Rational -> SpecTransM ctx Rational
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rational -> SpecTransM ctx Rational)
-> (UnitInterval -> Rational)
-> UnitInterval
-> SpecTransM ctx Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnitInterval -> Rational
forall r. BoundedRational r => r -> Rational
unboundRational

instance SpecTranslate ctx NonNegativeInterval where
  type SpecRep NonNegativeInterval = Agda.Rational

  toSpecRep :: NonNegativeInterval -> SpecTransM ctx (SpecRep NonNegativeInterval)
toSpecRep = Rational -> SpecTransM ctx Rational
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rational -> SpecTransM ctx Rational)
-> (NonNegativeInterval -> Rational)
-> NonNegativeInterval
-> SpecTransM ctx Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonNegativeInterval -> Rational
forall r. BoundedRational r => r -> Rational
unboundRational

instance
  ( SpecTranslate ctx k
  , SpecTranslate ctx v
  ) =>
  SpecTranslate ctx (Map k v)
  where
  type SpecRep (Map k v) = Agda.HSMap (SpecRep k) (SpecRep v)

  toSpecRep :: Map k v -> SpecTransM ctx (SpecRep (Map k v))
toSpecRep = ([(SpecRep k, SpecRep v)] -> HSMap (SpecRep k) (SpecRep v))
-> SpecTransM ctx [(SpecRep k, SpecRep v)]
-> SpecTransM ctx (HSMap (SpecRep k) (SpecRep v))
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 k, SpecRep v)] -> HSMap (SpecRep k) (SpecRep v)
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap (SpecTransM ctx [(SpecRep k, SpecRep v)]
 -> SpecTransM ctx (HSMap (SpecRep k) (SpecRep v)))
-> (Map k v -> SpecTransM ctx [(SpecRep k, SpecRep v)])
-> Map k v
-> SpecTransM ctx (HSMap (SpecRep k) (SpecRep v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((k, v) -> SpecTransM ctx (SpecRep k, SpecRep v))
-> [(k, v)] -> SpecTransM ctx [(SpecRep k, SpecRep v)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((k -> SpecTransM ctx (SpecRep k))
-> (v -> SpecTransM ctx (SpecRep v))
-> (k, v)
-> SpecTransM ctx (SpecRep k, SpecRep v)
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bimapM k -> SpecTransM ctx (SpecRep k)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep v -> SpecTransM ctx (SpecRep v)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep) ([(k, v)] -> SpecTransM ctx [(SpecRep k, SpecRep v)])
-> (Map k v -> [(k, v)])
-> Map k v
-> SpecTransM ctx [(SpecRep k, SpecRep v)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map k v -> [(k, v)]
forall k a. Map k a -> [(k, a)]
Map.toList

class GSpecNormalize f where
  genericSpecNormalize :: f a -> f a

instance GSpecNormalize U1 where
  genericSpecNormalize :: forall a. U1 a -> U1 a
genericSpecNormalize U1 a
U1 = U1 a
forall k (p :: k). U1 p
U1

instance GSpecNormalize V1 where
  genericSpecNormalize :: forall a. V1 a -> V1 a
genericSpecNormalize = \case {}

instance (GSpecNormalize f, GSpecNormalize g) => GSpecNormalize (f :*: g) where
  genericSpecNormalize :: forall a. (:*:) f g a -> (:*:) f g a
genericSpecNormalize (f a
f :*: g a
g) = f a -> f a
forall a. f a -> f a
forall (f :: * -> *) a. GSpecNormalize f => f a -> f a
genericSpecNormalize 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. GSpecNormalize f => f a -> f a
genericSpecNormalize g a
g

instance (GSpecNormalize f, GSpecNormalize g) => GSpecNormalize (f :+: g) where
  genericSpecNormalize :: forall a. (:+:) f g a -> (:+:) f g a
genericSpecNormalize (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. GSpecNormalize f => f a -> f a
genericSpecNormalize f a
f
  genericSpecNormalize (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. GSpecNormalize f => f a -> f a
genericSpecNormalize g a
f

instance GSpecNormalize a => GSpecNormalize (M1 i c a) where
  genericSpecNormalize :: forall a. M1 i c a a -> M1 i c a a
genericSpecNormalize (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. GSpecNormalize f => f a -> f a
genericSpecNormalize a a
x

instance SpecNormalize a => GSpecNormalize (K1 i a) where
  genericSpecNormalize :: forall a. K1 i a a -> K1 i a a
genericSpecNormalize (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. SpecNormalize a => a -> a
specNormalize a
x

class SpecNormalize a where
  specNormalize :: a -> a
  default specNormalize :: (Generic a, GSpecNormalize (Rep a)) => a -> a
  specNormalize = 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. GSpecNormalize f => f a -> f a
genericSpecNormalize (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

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 Text a
forall ctx a. ctx -> SpecTransM ctx a -> Either Text 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 Text
e -> Text -> SpecTransM ctx' a
forall a. Text -> SpecTransM ctx' a
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. 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 Text
x) = String -> [Expr] -> Expr
App String
"OpaqueErrorString" [NonEmpty Text -> Expr
forall a. ToExpr a => a -> Expr
toExpr NonEmpty Text
x]

instance NFData OpaqueErrorString

unComputationResult :: Agda.ComputationResult Text a -> Either Text a
unComputationResult :: forall a. ComputationResult Text a -> Either Text a
unComputationResult (Agda.Success a
x) = a -> Either Text a
forall a b. b -> Either a b
Right a
x
unComputationResult (Agda.Failure Text
e) = Text -> Either Text a
forall a b. a -> Either a b
Left 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) = a -> Either e a
forall a b. b -> Either a b
Right a
x
unComputationResult_ (Agda.Failure Void
x) = case Void
x of {}

toSpecRep_ ::
  SpecTranslate () a =>
  a ->
  SpecRep a
toSpecRep_ :: forall a. SpecTranslate () a => a -> SpecRep a
toSpecRep_ a
x = case () -> SpecTransM () (SpecRep a) -> Either Text (SpecRep a)
forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM () (SpecTransM () (SpecRep a) -> Either Text (SpecRep a))
-> SpecTransM () (SpecRep a) -> Either Text (SpecRep a)
forall a b. (a -> b) -> a -> b
$ a -> SpecTransM () (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
x of
  Right SpecRep a
res -> SpecRep a
res
  Left Text
v -> String -> SpecRep a
forall a. HasCallStack => String -> a
error (String -> SpecRep a) -> String -> SpecRep a
forall a b. (a -> b) -> a -> b
$ String
"Failed to translate:\n" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Text -> String
T.unpack Text
v