{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Utilities that avoid repetition when declaring instances for types
-- that are not amenable to @deriving@, and in particular, types with
-- existential quantification.
--
-- For existentials that only quantify one type variable, this module's
-- functionality is mostly superseded by the @some@ Hackage package. However,
-- this library involves many existentials that quantify multiple variables.
-- That can be shoehorned into @some@ with some encoding, but I believe this
-- module's weight is preferable to the overhead of using that encoding in our
-- existential data types' declarations.
module Test.Ouroboros.Consensus.ChainGenerator.Some (
    -- * 'Show'
    runShowsPrec
  , showArg
  , showCtor
  , showCtorProxy
    -- * 'Read'
  , Read.readPrec
  , readArg
  , readCtor
  , runReadPrec
    -- * 'Eq'
  , Forgotten
  , forgotten
  ) where

import           Data.Kind (Constraint, Type)
import           Data.Void (Void)
import qualified GHC.Read as Read
import           GHC.TypeLits (Symbol)
import qualified GHC.TypeLits as TE
import           Ouroboros.Consensus.Util.RedundantConstraints
import qualified Text.ParserCombinators.ReadPrec as Read
import qualified Text.Read.Lex as Read

-----

type family AbsError (s :: Symbol) (a :: Type) :: Void where
    AbsError s a = TE.TypeError (
                TE.Text "You have accidentaly applied `"
        TE.:<>: TE.Text s
        TE.:<>: TE.Text "' to a non-concrete type: "
        TE.:<>: TE.ShowType a
      )

type family NoFun (s :: Symbol) (a :: Type) (absError :: Void) :: Constraint where
    NoFun s (a -> b) abs = TE.TypeError (
                TE.Text "You have accidentaly applied `"
        TE.:<>: TE.Text s
        TE.:<>: TE.Text "' to a function type: "
        TE.:<>: TE.ShowType (a -> b)
      )
    NoFun s t        abs = ()

-----

newtype ShowBuilder a = ShowBuilder ShowS

infixl 1 `showArg`

-- | The context is satisfied by any type @a@ that is manifestly apart from @->@
runShowsPrec ::
     forall a. NoFun "runShowsPrec" a (AbsError "runShowsPrec" a)
  => Int -> ShowBuilder a -> ShowS
runShowsPrec :: forall a.
NoFun "runShowsPrec" a (AbsError "runShowsPrec" a) =>
Int -> ShowBuilder a -> ShowS
runShowsPrec Int
p (ShowBuilder ShowS
x) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) ShowS
x
  where
    ()
_ = Proxy (NoFun "runShowsPrec" a (TypeError ...)) -> ()
forall (c :: Constraint) (proxy :: Constraint -> *).
c =>
proxy c -> ()
keepRedundantConstraint (forall {k} (t :: k). Proxy t
forall (t :: Constraint). Proxy t
Proxy @(NoFun "runShowsPrec" a (AbsError "runShowsPrec" a)))

showCtor :: a -> String -> ShowBuilder a
showCtor :: forall a. a -> String -> ShowBuilder a
showCtor a
a String
s =
    Proxy a -> String -> ShowBuilder a
forall (proxy :: * -> *) a. proxy a -> String -> ShowBuilder a
showCtorProxy (a -> Proxy a
forall a. a -> Proxy a
toProxy a
a) String
s
  where
    toProxy :: a -> Proxy a
    toProxy :: forall a. a -> Proxy a
toProxy = Proxy a -> a -> Proxy a
forall a b. a -> b -> a
const Proxy a
forall {k} (t :: k). Proxy t
Proxy

showCtorProxy :: proxy a -> String -> ShowBuilder a
showCtorProxy :: forall (proxy :: * -> *) a. proxy a -> String -> ShowBuilder a
showCtorProxy proxy a
_a String
s = ShowS -> ShowBuilder a
forall a. ShowS -> ShowBuilder a
ShowBuilder (ShowS -> ShowBuilder a) -> ShowS -> ShowBuilder a
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
s

showArg :: Show a => ShowBuilder (a -> b) -> a -> ShowBuilder b
ShowBuilder ShowS
l showArg :: forall a b. Show a => ShowBuilder (a -> b) -> a -> ShowBuilder b
`showArg` a
r = ShowS -> ShowBuilder b
forall a. ShowS -> ShowBuilder a
ShowBuilder (ShowS -> ShowBuilder b) -> ShowS -> ShowBuilder b
forall a b. (a -> b) -> a -> b
$ ShowS
l ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  String -> ShowS
showString String
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 a
r

-----

newtype ReadBuilder a = ReadBuilder (Read.ReadPrec a)
  deriving (Functor ReadBuilder
Functor ReadBuilder =>
(forall a. a -> ReadBuilder a)
-> (forall a b.
    ReadBuilder (a -> b) -> ReadBuilder a -> ReadBuilder b)
-> (forall a b c.
    (a -> b -> c) -> ReadBuilder a -> ReadBuilder b -> ReadBuilder c)
-> (forall a b. ReadBuilder a -> ReadBuilder b -> ReadBuilder b)
-> (forall a b. ReadBuilder a -> ReadBuilder b -> ReadBuilder a)
-> Applicative ReadBuilder
forall a. a -> ReadBuilder a
forall a b. ReadBuilder a -> ReadBuilder b -> ReadBuilder a
forall a b. ReadBuilder a -> ReadBuilder b -> ReadBuilder b
forall a b. ReadBuilder (a -> b) -> ReadBuilder a -> ReadBuilder b
forall a b c.
(a -> b -> c) -> ReadBuilder a -> ReadBuilder b -> ReadBuilder 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 a. a -> ReadBuilder a
pure :: forall a. a -> ReadBuilder a
$c<*> :: forall a b. ReadBuilder (a -> b) -> ReadBuilder a -> ReadBuilder b
<*> :: forall a b. ReadBuilder (a -> b) -> ReadBuilder a -> ReadBuilder b
$cliftA2 :: forall a b c.
(a -> b -> c) -> ReadBuilder a -> ReadBuilder b -> ReadBuilder c
liftA2 :: forall a b c.
(a -> b -> c) -> ReadBuilder a -> ReadBuilder b -> ReadBuilder c
$c*> :: forall a b. ReadBuilder a -> ReadBuilder b -> ReadBuilder b
*> :: forall a b. ReadBuilder a -> ReadBuilder b -> ReadBuilder b
$c<* :: forall a b. ReadBuilder a -> ReadBuilder b -> ReadBuilder a
<* :: forall a b. ReadBuilder a -> ReadBuilder b -> ReadBuilder a
Applicative, (forall a b. (a -> b) -> ReadBuilder a -> ReadBuilder b)
-> (forall a b. a -> ReadBuilder b -> ReadBuilder a)
-> Functor ReadBuilder
forall a b. a -> ReadBuilder b -> ReadBuilder a
forall a b. (a -> b) -> ReadBuilder a -> ReadBuilder b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> ReadBuilder a -> ReadBuilder b
fmap :: forall a b. (a -> b) -> ReadBuilder a -> ReadBuilder b
$c<$ :: forall a b. a -> ReadBuilder b -> ReadBuilder a
<$ :: forall a b. a -> ReadBuilder b -> ReadBuilder a
Functor)

-- | The context is satisfied by any type @a@ that is manifestly apart from @->@
runReadPrec ::
     forall a. NoFun "runReadPrec" a (AbsError "runReadPrec" a)
  => ReadBuilder a -> Read.ReadPrec a
runReadPrec :: forall a.
NoFun "runReadPrec" a (AbsError "runReadPrec" a) =>
ReadBuilder a -> ReadPrec a
runReadPrec (ReadBuilder ReadPrec a
x) = ReadPrec a -> ReadPrec a
forall a. ReadPrec a -> ReadPrec a
Read.parens (ReadPrec a -> ReadPrec a) -> ReadPrec a -> ReadPrec a
forall a b. (a -> b) -> a -> b
$ Int -> ReadPrec a -> ReadPrec a
forall a. Int -> ReadPrec a -> ReadPrec a
Read.prec Int
10 ReadPrec a
x
  where
    ()
_ = Proxy (NoFun "runReadPrec" a (TypeError ...)) -> ()
forall (c :: Constraint) (proxy :: Constraint -> *).
c =>
proxy c -> ()
keepRedundantConstraint (forall {k} (t :: k). Proxy t
forall (t :: Constraint). Proxy t
Proxy @(NoFun "runReadPrec" a (AbsError "runReadPrec" a)))

readCtor :: a -> String -> ReadBuilder a
readCtor :: forall a. a -> String -> ReadBuilder a
readCtor a
a String
s = ReadPrec a -> ReadBuilder a
forall a. ReadPrec a -> ReadBuilder a
ReadBuilder (ReadPrec a -> ReadBuilder a) -> ReadPrec a -> ReadBuilder a
forall a b. (a -> b) -> a -> b
$ a
a a -> ReadPrec () -> ReadPrec a
forall a b. a -> ReadPrec b -> ReadPrec a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Lexeme -> ReadPrec ()
Read.expectP (String -> Lexeme
Read.Ident String
s)

readArg :: Read a => ReadBuilder a
readArg :: forall a. Read a => ReadBuilder a
readArg = ReadPrec a -> ReadBuilder a
forall a. ReadPrec a -> ReadBuilder a
ReadBuilder (ReadPrec a -> ReadBuilder a) -> ReadPrec a -> ReadBuilder a
forall a b. (a -> b) -> a -> b
$ ReadPrec a -> ReadPrec a
forall a. ReadPrec a -> ReadPrec a
Read.step ReadPrec a
forall a. Read a => ReadPrec a
Read.readPrec

-----

-- | An opaque type that only allows for 'Eq' and human inspection
newtype Forgotten a = Forgotten a
  deriving (Forgotten a -> Forgotten a -> Bool
(Forgotten a -> Forgotten a -> Bool)
-> (Forgotten a -> Forgotten a -> Bool) -> Eq (Forgotten a)
forall a. Eq a => Forgotten a -> Forgotten a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Forgotten a -> Forgotten a -> Bool
== :: Forgotten a -> Forgotten a -> Bool
$c/= :: forall a. Eq a => Forgotten a -> Forgotten a -> Bool
/= :: Forgotten a -> Forgotten a -> Bool
Eq, Int -> Forgotten a -> ShowS
[Forgotten a] -> ShowS
Forgotten a -> String
(Int -> Forgotten a -> ShowS)
-> (Forgotten a -> String)
-> ([Forgotten a] -> ShowS)
-> Show (Forgotten a)
forall a. Show a => Int -> Forgotten a -> ShowS
forall a. Show a => [Forgotten a] -> ShowS
forall a. Show a => Forgotten a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Forgotten a -> ShowS
showsPrec :: Int -> Forgotten a -> ShowS
$cshow :: forall a. Show a => Forgotten a -> String
show :: Forgotten a -> String
$cshowList :: forall a. Show a => [Forgotten a] -> ShowS
showList :: [Forgotten a] -> ShowS
Show)

forgotten :: a -> Forgotten a
forgotten :: forall a. a -> Forgotten a
forgotten = a -> Forgotten a
forall a. a -> Forgotten a
Forgotten