{-# 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,
  withSpecTransM,
  withCtxSpecTransM,
  askSpecTransM,
  unComputationResult,
  unComputationResult_,
  toSpecRepTuple,
  toSpecRepTupleGen,
  toSpecRepOMap,
  toSpecRepMap,
) where

import Cardano.Ledger.BaseTypes (NonNegativeInterval, UnitInterval, unboundRational)
import Cardano.Ledger.Binary (Sized (..))
import Cardano.Ledger.Compactible (Compactible (..), fromCompact)
import Control.DeepSeq (NFData)
import Control.Monad.Except (ExceptT, MonadError (..), mapExceptT, runExceptT)
import Control.Monad.Reader (MonadReader (..), Reader, ask, runReader, withReaderT)
import Data.Bifunctor (bimap)
import Data.Bitraversable (bimapM)
import Data.Foldable (Foldable (..))
import Data.Kind (Type)
import Data.List (nub, sortOn)
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 Data.Void (Void, absurd)
import Data.Word (Word16, Word32, Word64)
import GHC.Generics (Generic (..), K1 (..), M1 (..), U1 (..), V1, (:*:) (..), (:+:) (..))
import qualified MAlonzo.Code.Ledger.Core.Foreign.API as Agda
import Test.Cardano.Ledger.TreeDiff (Expr (..), ToExpr (..))

newtype SpecTransM era ctx a
  = SpecTransM (ExceptT Text (Reader ctx) a)
  deriving ((forall a b.
 (a -> b) -> SpecTransM era ctx a -> SpecTransM era ctx b)
-> (forall a b. a -> SpecTransM era ctx b -> SpecTransM era ctx a)
-> Functor (SpecTransM era ctx)
forall a b. a -> SpecTransM era ctx b -> SpecTransM era ctx a
forall a b.
(a -> b) -> SpecTransM era ctx a -> SpecTransM era ctx b
forall era ctx a b.
a -> SpecTransM era ctx b -> SpecTransM era ctx a
forall era ctx a b.
(a -> b) -> SpecTransM era ctx a -> SpecTransM era 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 era ctx a b.
(a -> b) -> SpecTransM era ctx a -> SpecTransM era ctx b
fmap :: forall a b.
(a -> b) -> SpecTransM era ctx a -> SpecTransM era ctx b
$c<$ :: forall era ctx a b.
a -> SpecTransM era ctx b -> SpecTransM era ctx a
<$ :: forall a b. a -> SpecTransM era ctx b -> SpecTransM era ctx a
Functor, Functor (SpecTransM era ctx)
Functor (SpecTransM era ctx) =>
(forall a. a -> SpecTransM era ctx a)
-> (forall a b.
    SpecTransM era ctx (a -> b)
    -> SpecTransM era ctx a -> SpecTransM era ctx b)
-> (forall a b c.
    (a -> b -> c)
    -> SpecTransM era ctx a
    -> SpecTransM era ctx b
    -> SpecTransM era ctx c)
-> (forall a b.
    SpecTransM era ctx a
    -> SpecTransM era ctx b -> SpecTransM era ctx b)
-> (forall a b.
    SpecTransM era ctx a
    -> SpecTransM era ctx b -> SpecTransM era ctx a)
-> Applicative (SpecTransM era ctx)
forall a. a -> SpecTransM era ctx a
forall era ctx. Functor (SpecTransM era ctx)
forall a b.
SpecTransM era ctx a
-> SpecTransM era ctx b -> SpecTransM era ctx a
forall a b.
SpecTransM era ctx a
-> SpecTransM era ctx b -> SpecTransM era ctx b
forall a b.
SpecTransM era ctx (a -> b)
-> SpecTransM era ctx a -> SpecTransM era ctx b
forall era ctx a. a -> SpecTransM era ctx a
forall a b c.
(a -> b -> c)
-> SpecTransM era ctx a
-> SpecTransM era ctx b
-> SpecTransM era ctx c
forall era ctx a b.
SpecTransM era ctx a
-> SpecTransM era ctx b -> SpecTransM era ctx a
forall era ctx a b.
SpecTransM era ctx a
-> SpecTransM era ctx b -> SpecTransM era ctx b
forall era ctx a b.
SpecTransM era ctx (a -> b)
-> SpecTransM era ctx a -> SpecTransM era ctx b
forall era ctx a b c.
(a -> b -> c)
-> SpecTransM era ctx a
-> SpecTransM era ctx b
-> SpecTransM era 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 era ctx a. a -> SpecTransM era ctx a
pure :: forall a. a -> SpecTransM era ctx a
$c<*> :: forall era ctx a b.
SpecTransM era ctx (a -> b)
-> SpecTransM era ctx a -> SpecTransM era ctx b
<*> :: forall a b.
SpecTransM era ctx (a -> b)
-> SpecTransM era ctx a -> SpecTransM era ctx b
$cliftA2 :: forall era ctx a b c.
(a -> b -> c)
-> SpecTransM era ctx a
-> SpecTransM era ctx b
-> SpecTransM era ctx c
liftA2 :: forall a b c.
(a -> b -> c)
-> SpecTransM era ctx a
-> SpecTransM era ctx b
-> SpecTransM era ctx c
$c*> :: forall era ctx a b.
SpecTransM era ctx a
-> SpecTransM era ctx b -> SpecTransM era ctx b
*> :: forall a b.
SpecTransM era ctx a
-> SpecTransM era ctx b -> SpecTransM era ctx b
$c<* :: forall era ctx a b.
SpecTransM era ctx a
-> SpecTransM era ctx b -> SpecTransM era ctx a
<* :: forall a b.
SpecTransM era ctx a
-> SpecTransM era ctx b -> SpecTransM era ctx a
Applicative, Applicative (SpecTransM era ctx)
Applicative (SpecTransM era ctx) =>
(forall a b.
 SpecTransM era ctx a
 -> (a -> SpecTransM era ctx b) -> SpecTransM era ctx b)
-> (forall a b.
    SpecTransM era ctx a
    -> SpecTransM era ctx b -> SpecTransM era ctx b)
-> (forall a. a -> SpecTransM era ctx a)
-> Monad (SpecTransM era ctx)
forall a. a -> SpecTransM era ctx a
forall era ctx. Applicative (SpecTransM era ctx)
forall a b.
SpecTransM era ctx a
-> SpecTransM era ctx b -> SpecTransM era ctx b
forall a b.
SpecTransM era ctx a
-> (a -> SpecTransM era ctx b) -> SpecTransM era ctx b
forall era ctx a. a -> SpecTransM era ctx a
forall era ctx a b.
SpecTransM era ctx a
-> SpecTransM era ctx b -> SpecTransM era ctx b
forall era ctx a b.
SpecTransM era ctx a
-> (a -> SpecTransM era ctx b) -> SpecTransM era 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 era ctx a b.
SpecTransM era ctx a
-> (a -> SpecTransM era ctx b) -> SpecTransM era ctx b
>>= :: forall a b.
SpecTransM era ctx a
-> (a -> SpecTransM era ctx b) -> SpecTransM era ctx b
$c>> :: forall era ctx a b.
SpecTransM era ctx a
-> SpecTransM era ctx b -> SpecTransM era ctx b
>> :: forall a b.
SpecTransM era ctx a
-> SpecTransM era ctx b -> SpecTransM era ctx b
$creturn :: forall era ctx a. a -> SpecTransM era ctx a
return :: forall a. a -> SpecTransM era ctx a
Monad, MonadError Text, MonadReader ctx)

runSpecTransM :: forall era ctx a. ctx -> SpecTransM era ctx a -> Either Text a
runSpecTransM :: forall era ctx a. ctx -> SpecTransM era 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

withSpecTransM :: (ctx -> ctx') -> SpecTransM era ctx' a -> SpecTransM era ctx a
withSpecTransM :: forall ctx ctx' era a.
(ctx -> ctx') -> SpecTransM era ctx' a -> SpecTransM era ctx a
withSpecTransM ctx -> ctx'
f (SpecTransM ExceptT Text (Reader ctx') a
m) = ExceptT Text (Reader ctx) a -> SpecTransM era ctx a
forall era ctx a.
ExceptT Text (Reader ctx) a -> SpecTransM era ctx a
SpecTransM ((ReaderT ctx' Identity (Either Text a)
 -> Reader ctx (Either Text a))
-> ExceptT Text (Reader ctx') a -> ExceptT Text (Reader ctx) a
forall (m :: * -> *) e a (n :: * -> *) e' b.
(m (Either e a) -> n (Either e' b))
-> ExceptT e m a -> ExceptT e' n b
mapExceptT ((ctx -> ctx')
-> ReaderT ctx' Identity (Either Text a)
-> Reader ctx (Either Text a)
forall r' r (m :: * -> *) a.
(r' -> r) -> ReaderT r m a -> ReaderT r' m a
withReaderT ctx -> ctx'
f) ExceptT Text (Reader ctx') a
m)

withCtxSpecTransM :: ctx -> SpecTransM era ctx a -> SpecTransM era ctx' a
withCtxSpecTransM :: forall ctx era a ctx'.
ctx -> SpecTransM era ctx a -> SpecTransM era ctx' a
withCtxSpecTransM ctx
ctx = (ctx' -> ctx) -> SpecTransM era ctx a -> SpecTransM era ctx' a
forall ctx ctx' era a.
(ctx -> ctx') -> SpecTransM era ctx' a -> SpecTransM era ctx a
withSpecTransM (ctx -> ctx' -> ctx
forall a b. a -> b -> a
const ctx
ctx)

askSpecTransM :: SpecTransM era ctx ctx
askSpecTransM :: forall era ctx. SpecTransM era ctx ctx
askSpecTransM = SpecTransM era ctx ctx
forall r (m :: * -> *). MonadReader r m => m r
ask

class SpecTranslate era a where
  type SpecRep era a :: Type

  type SpecContext era a :: Type
  type SpecContext era a = ()

  toSpecRep :: a -> SpecTransM era (SpecContext era a) (SpecRep era a)

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

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

instance SpecTranslate era Bool where
  type SpecRep era Bool = Bool

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

instance SpecTranslate era Integer where
  type SpecRep era Integer = Integer

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

instance SpecTranslate era Void where
  type SpecRep era Void = Void

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

instance SpecTranslate era Word16 where
  type SpecRep era Word16 = Integer

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

instance SpecTranslate era Word32 where
  type SpecRep era Word32 = Integer

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

instance SpecTranslate era Word64 where
  type SpecRep era Word64 = Integer

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

toSpecRepTupleGen ::
  forall era a b c d ctx.
  (a -> SpecTransM era ctx c) ->
  (b -> SpecTransM era ctx d) ->
  (a, b) ->
  SpecTransM era ctx (c, d)
toSpecRepTupleGen :: forall era a b c d ctx.
(a -> SpecTransM era ctx c)
-> (b -> SpecTransM era ctx d)
-> (a, b)
-> SpecTransM era ctx (c, d)
toSpecRepTupleGen a -> SpecTransM era ctx c
f b -> SpecTransM era ctx d
g (a
a, b
b) = (,) (c -> d -> (c, d))
-> SpecTransM era ctx c -> SpecTransM era ctx (d -> (c, d))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> SpecTransM era ctx c
f a
a SpecTransM era ctx (d -> (c, d))
-> SpecTransM era ctx d -> SpecTransM era ctx (c, d)
forall a b.
SpecTransM era ctx (a -> b)
-> SpecTransM era ctx a -> SpecTransM era ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> SpecTransM era ctx d
g b
b

toSpecRepTuple ::
  forall era a b ctx.
  (SpecTranslate era a, SpecTranslate era b, SpecContext era a ~ ctx, SpecContext era b ~ ctx) =>
  (a, b) -> SpecTransM era ctx (SpecRep era a, SpecRep era b)
toSpecRepTuple :: forall era a b ctx.
(SpecTranslate era a, SpecTranslate era b, SpecContext era a ~ ctx,
 SpecContext era b ~ ctx) =>
(a, b) -> SpecTransM era ctx (SpecRep era a, SpecRep era b)
toSpecRepTuple = (a -> SpecTransM era ctx (SpecRep era a))
-> (b -> SpecTransM era ctx (SpecRep era b))
-> (a, b)
-> SpecTransM era ctx (SpecRep era a, SpecRep era b)
forall era a b c d ctx.
(a -> SpecTransM era ctx c)
-> (b -> SpecTransM era ctx d)
-> (a, b)
-> SpecTransM era ctx (c, d)
toSpecRepTupleGen a -> SpecTransM era ctx (SpecRep era a)
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep b -> SpecTransM era ctx (SpecRep era b)
b -> SpecTransM era (SpecContext era b) (SpecRep era b)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep

instance SpecTranslate era a => SpecTranslate era [a] where
  type SpecRep era [a] = [SpecRep era a]
  type SpecContext era [a] = SpecContext era a

  toSpecRep :: [a] -> SpecTransM era (SpecContext era [a]) (SpecRep era [a])
toSpecRep = (a -> SpecTransM era (SpecContext era a) (SpecRep era a))
-> [a] -> SpecTransM era (SpecContext era a) [SpecRep era 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 era (SpecContext era a) (SpecRep era a)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep

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

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

instance SpecTranslate era a => SpecTranslate era (Maybe a) where
  type SpecRep era (Maybe a) = Maybe (SpecRep era a)
  type SpecContext era (Maybe a) = SpecContext era a

  toSpecRep :: Maybe a
-> SpecTransM
     era (SpecContext era (Maybe a)) (SpecRep era (Maybe a))
toSpecRep = (a -> SpecTransM era (SpecContext era a) (SpecRep era a))
-> Maybe a
-> SpecTransM era (SpecContext era a) (Maybe (SpecRep era 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 era (SpecContext era a) (SpecRep era a)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep

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

  toSpecRep :: StrictSeq a
-> SpecTransM
     era (SpecContext era (StrictSeq a)) (SpecRep era (StrictSeq a))
toSpecRep = (a -> SpecTransM era (SpecContext era a) (SpecRep era a))
-> [a] -> SpecTransM era (SpecContext era a) [SpecRep era 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 era (SpecContext era a) (SpecRep era a)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep ([a] -> SpecTransM era (SpecContext era a) [SpecRep era a])
-> (StrictSeq a -> [a])
-> StrictSeq a
-> SpecTransM era (SpecContext era a) [SpecRep era 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 era a => SpecTranslate era (Seq a) where
  type SpecRep era (Seq a) = [SpecRep era a]
  type SpecContext era (Seq a) = SpecContext era a

  toSpecRep :: Seq a
-> SpecTransM era (SpecContext era (Seq a)) (SpecRep era (Seq a))
toSpecRep = (a -> SpecTransM era (SpecContext era a) (SpecRep era a))
-> [a] -> SpecTransM era (SpecContext era a) [SpecRep era 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 era (SpecContext era a) (SpecRep era a)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep ([a] -> SpecTransM era (SpecContext era a) [SpecRep era a])
-> (Seq a -> [a])
-> Seq a
-> SpecTransM era (SpecContext era a) [SpecRep era 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 era a => SpecTranslate era (OSet a) where
  type SpecRep era (OSet a) = [SpecRep era a]
  type SpecContext era (OSet a) = SpecContext era a

  toSpecRep :: OSet a
-> SpecTransM era (SpecContext era (OSet a)) (SpecRep era (OSet a))
toSpecRep = (a -> SpecTransM era (SpecContext era a) (SpecRep era a))
-> [a] -> SpecTransM era (SpecContext era a) [SpecRep era 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 era (SpecContext era a) (SpecRep era a)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep ([a] -> SpecTransM era (SpecContext era a) [SpecRep era a])
-> (OSet a -> [a])
-> OSet a
-> SpecTransM era (SpecContext era a) [SpecRep era 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

toSpecRepOMap ::
  forall era k v ctx.
  (Ord k, SpecTranslate era k, SpecTranslate era v, SpecContext era k ~ ctx, SpecContext era v ~ ctx) =>
  OMap k v -> SpecTransM era ctx [(SpecRep era k, SpecRep era v)]
toSpecRepOMap :: forall era k v ctx.
(Ord k, SpecTranslate era k, SpecTranslate era v,
 SpecContext era k ~ ctx, SpecContext era v ~ ctx) =>
OMap k v -> SpecTransM era ctx [(SpecRep era k, SpecRep era v)]
toSpecRepOMap = ((k, v) -> SpecTransM era ctx (SpecRep era k, SpecRep era v))
-> [(k, v)] -> SpecTransM era ctx [(SpecRep era k, SpecRep era 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 era ctx (SpecRep era k))
-> (v -> SpecTransM era ctx (SpecRep era v))
-> (k, v)
-> SpecTransM era ctx (SpecRep era k, SpecRep era 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 era ctx (SpecRep era k)
k -> SpecTransM era (SpecContext era k) (SpecRep era k)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep v -> SpecTransM era ctx (SpecRep era v)
v -> SpecTransM era (SpecContext era v) (SpecRep era v)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep) ([(k, v)] -> SpecTransM era ctx [(SpecRep era k, SpecRep era v)])
-> (OMap k v -> [(k, v)])
-> OMap k v
-> SpecTransM era ctx [(SpecRep era k, SpecRep era 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 era a, Compactible a) => SpecTranslate era (CompactForm a) where
  type SpecRep era (CompactForm a) = SpecRep era a
  type SpecContext era (CompactForm a) = SpecContext era a

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

instance SpecTranslate era a => SpecTranslate era (Sized a) where
  type SpecRep era (Sized a) = SpecRep era a
  type SpecContext era (Sized a) = SpecContext era a

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

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

  toSpecRep :: Set a
-> SpecTransM era (SpecContext era (Set a)) (SpecRep era (Set a))
toSpecRep = ([SpecRep era a] -> HSSet (SpecRep era a))
-> SpecTransM era (SpecContext era a) [SpecRep era a]
-> SpecTransM era (SpecContext era a) (HSSet (SpecRep era a))
forall a b.
(a -> b)
-> SpecTransM era (SpecContext era a) a
-> SpecTransM era (SpecContext era a) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [SpecRep era a] -> HSSet (SpecRep era a)
forall a. [a] -> HSSet a
Agda.MkHSSet (SpecTransM era (SpecContext era a) [SpecRep era a]
 -> SpecTransM era (SpecContext era a) (HSSet (SpecRep era a)))
-> (Set a -> SpecTransM era (SpecContext era a) [SpecRep era a])
-> Set a
-> SpecTransM era (SpecContext era a) (HSSet (SpecRep era a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> SpecTransM era (SpecContext era a) (SpecRep era a))
-> [a] -> SpecTransM era (SpecContext era a) [SpecRep era 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 era (SpecContext era a) (SpecRep era a)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep ([a] -> SpecTransM era (SpecContext era a) [SpecRep era a])
-> (Set a -> [a])
-> Set a
-> SpecTransM era (SpecContext era a) [SpecRep era a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set a -> [a]
forall a. Set a -> [a]
Set.toList

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

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

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

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

toSpecRepMap ::
  forall era k v ctx.
  (SpecTranslate era k, SpecTranslate era v, SpecContext era k ~ ctx, SpecContext era v ~ ctx) =>
  Map k v -> SpecTransM era ctx (Agda.HSMap (SpecRep era k) (SpecRep era v))
toSpecRepMap :: forall era k v ctx.
(SpecTranslate era k, SpecTranslate era v, SpecContext era k ~ ctx,
 SpecContext era v ~ ctx) =>
Map k v
-> SpecTransM era ctx (HSMap (SpecRep era k) (SpecRep era v))
toSpecRepMap =
  ([(SpecRep era k, SpecRep era v)]
 -> HSMap (SpecRep era k) (SpecRep era v))
-> SpecTransM era ctx [(SpecRep era k, SpecRep era v)]
-> SpecTransM era ctx (HSMap (SpecRep era k) (SpecRep era v))
forall a b.
(a -> b) -> SpecTransM era ctx a -> SpecTransM era ctx b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(SpecRep era k, SpecRep era v)]
-> HSMap (SpecRep era k) (SpecRep era v)
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap
    (SpecTransM era ctx [(SpecRep era k, SpecRep era v)]
 -> SpecTransM era ctx (HSMap (SpecRep era k) (SpecRep era v)))
-> (Map k v -> SpecTransM era ctx [(SpecRep era k, SpecRep era v)])
-> Map k v
-> SpecTransM era ctx (HSMap (SpecRep era k) (SpecRep era v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((k, v) -> SpecTransM era ctx (SpecRep era k, SpecRep era v))
-> [(k, v)] -> SpecTransM era ctx [(SpecRep era k, SpecRep era 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 era ctx (SpecRep era k))
-> (v -> SpecTransM era ctx (SpecRep era v))
-> (k, v)
-> SpecTransM era ctx (SpecRep era k, SpecRep era 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 era ctx (SpecRep era k)
k -> SpecTransM era (SpecContext era k) (SpecRep era k)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep v -> SpecTransM era ctx (SpecRep era v)
v -> SpecTransM era (SpecContext era v) (SpecRep era v)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep)
    ([(k, v)] -> SpecTransM era ctx [(SpecRep era k, SpecRep era v)])
-> (Map k v -> [(k, v)])
-> Map k v
-> SpecTransM era ctx [(SpecRep era k, SpecRep era 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 (ZonkAny 0) -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a (ZonkAny 0) -> a) -> (a -> Rep a (ZonkAny 0)) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep a (ZonkAny 0) -> Rep a (ZonkAny 0)
forall a. Rep a a -> Rep a a
forall (f :: * -> *) a. GSpecNormalize f => f a -> f a
genericSpecNormalize (Rep a (ZonkAny 0) -> Rep a (ZonkAny 0))
-> (a -> Rep a (ZonkAny 0)) -> a -> Rep a (ZonkAny 0)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a (ZonkAny 0)
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from

instance SpecNormalize Void

instance SpecNormalize Text where
  specNormalize :: Text -> Text
specNormalize = Text -> Text
forall a. a -> a
id

instance SpecNormalize OpaqueErrorString

instance SpecNormalize Char where
  specNormalize :: Char -> Char
specNormalize = Char -> Char
forall a. a -> a
id

instance SpecNormalize Integer where
  specNormalize :: Integer -> Integer
specNormalize = Integer -> Integer
forall a. a -> a
id

instance SpecNormalize Bool

instance SpecNormalize ()

instance SpecNormalize a => SpecNormalize [a]

instance SpecNormalize a => SpecNormalize (NonEmpty a)

instance
  ( Eq v
  , Ord k
  , SpecNormalize k
  , SpecNormalize v
  ) =>
  SpecNormalize (Agda.HSMap k v)
  where
  specNormalize :: HSMap k v -> HSMap k v
specNormalize (Agda.MkHSMap [(k, v)]
l) = [(k, v)] -> HSMap k v
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(k, v)] -> HSMap k v)
-> ([(k, v)] -> [(k, v)]) -> [(k, v)] -> HSMap k v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((k, v) -> k) -> [(k, v)] -> [(k, v)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (k, v) -> k
forall a b. (a, b) -> a
fst ([(k, v)] -> HSMap k v) -> [(k, v)] -> HSMap k v
forall a b. (a -> b) -> a -> b
$ (k -> k) -> (v -> v) -> (k, v) -> (k, v)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap k -> k
forall a. SpecNormalize a => a -> a
specNormalize v -> v
forall a. SpecNormalize a => a -> a
specNormalize ((k, v) -> (k, v)) -> [(k, v)] -> [(k, v)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(k, v)] -> [(k, v)]
forall a. Eq a => [a] -> [a]
nub [(k, v)]
l

instance (Ord a, SpecNormalize a) => SpecNormalize (Agda.HSSet a) where
  specNormalize :: HSSet a -> HSSet a
specNormalize (Agda.MkHSSet [a]
l) = [a] -> HSSet a
forall a. [a] -> HSSet a
Agda.MkHSSet ([a] -> HSSet a) -> ([a] -> [a]) -> [a] -> HSSet a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set a -> [a]
forall a. Set a -> [a]
Set.toList (Set a -> [a]) -> ([a] -> Set a) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList ([a] -> HSSet a) -> [a] -> HSSet a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. SpecNormalize a => a -> a
specNormalize (a -> a) -> [a] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
l

instance (SpecNormalize a, SpecNormalize b) => SpecNormalize (a, b)

instance SpecNormalize a => SpecNormalize (Maybe a)

instance (SpecNormalize a, SpecNormalize b) => SpecNormalize (Either a b)

instance SpecNormalize Agda.Rational where
  specNormalize :: Rational -> Rational
specNormalize = Rational -> Rational
forall a. a -> a
id

-- | 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 {}