{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeOperators #-}

module Test.Cardano.Ledger.Constrained.Monad (
  Typed (..),
  LiftT (..),
  failT,
  explain,
  mergeExplain,
  HasConstraint (..),
  Id (..),
  errorTyped,
  monadTyped,
  requireAll,
  generateWithSeed,
) where

import GHC.Stack
import Test.QuickCheck.Gen
import Test.QuickCheck.Random

generateWithSeed :: Int -> Gen a -> IO a
generateWithSeed :: forall a. Int -> Gen a -> IO a
generateWithSeed Int
n (MkGen QCGen -> Int -> a
g) =
  do
    let r :: QCGen
r = Int -> QCGen
mkQCGen Int
n
    forall (m :: * -> *) a. Monad m => a -> m a
return (QCGen -> Int -> a
g QCGen
r Int
30)

-- =================================================

newtype Typed x = Typed {forall x. Typed x -> Either [String] x
runTyped :: Either [String] x}
  deriving (forall a b. a -> Typed b -> Typed a
forall a b. (a -> b) -> Typed a -> Typed 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 -> Typed b -> Typed a
$c<$ :: forall a b. a -> Typed b -> Typed a
fmap :: forall a b. (a -> b) -> Typed a -> Typed b
$cfmap :: forall a b. (a -> b) -> Typed a -> Typed b
Functor, Functor Typed
forall a. a -> Typed a
forall a b. Typed a -> Typed b -> Typed a
forall a b. Typed a -> Typed b -> Typed b
forall a b. Typed (a -> b) -> Typed a -> Typed b
forall a b c. (a -> b -> c) -> Typed a -> Typed b -> Typed 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. Typed a -> Typed b -> Typed a
$c<* :: forall a b. Typed a -> Typed b -> Typed a
*> :: forall a b. Typed a -> Typed b -> Typed b
$c*> :: forall a b. Typed a -> Typed b -> Typed b
liftA2 :: forall a b c. (a -> b -> c) -> Typed a -> Typed b -> Typed c
$cliftA2 :: forall a b c. (a -> b -> c) -> Typed a -> Typed b -> Typed c
<*> :: forall a b. Typed (a -> b) -> Typed a -> Typed b
$c<*> :: forall a b. Typed (a -> b) -> Typed a -> Typed b
pure :: forall a. a -> Typed a
$cpure :: forall a. a -> Typed a
Applicative, Applicative Typed
forall a. a -> Typed a
forall a b. Typed a -> Typed b -> Typed b
forall a b. Typed a -> (a -> Typed b) -> Typed 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 -> Typed a
$creturn :: forall a. a -> Typed a
>> :: forall a b. Typed a -> Typed b -> Typed b
$c>> :: forall a b. Typed a -> Typed b -> Typed b
>>= :: forall a b. Typed a -> (a -> Typed b) -> Typed b
$c>>= :: forall a b. Typed a -> (a -> Typed b) -> Typed b
Monad)

instance MonadFail Typed where
  fail :: forall a. String -> Typed a
fail String
err = forall a. [String] -> Typed a
failT [String
err]

failT :: [String] -> Typed a
failT :: forall a. [String] -> Typed a
failT [String]
ss = forall x. Either [String] x -> Typed x
Typed (forall a b. a -> Either a b
Left [String]
ss)

class LiftT x where
  liftT :: x -> Typed x
  dropT :: Typed x -> x

-- ==================================

explain :: String -> Typed a -> Typed a
explain :: forall a. String -> Typed a -> Typed a
explain String
s (Typed (Left [String]
ss)) = forall x. Either [String] x -> Typed x
Typed (forall a b. a -> Either a b
Left (String
s forall a. a -> [a] -> [a]
: [String]
ss))
explain String
_ (Typed (Right a
x)) = forall x. Either [String] x -> Typed x
Typed (forall a b. b -> Either a b
Right a
x)

mergeExplain :: (Monoid x, LiftT x) => String -> x -> x -> x
mergeExplain :: forall x. (Monoid x, LiftT x) => String -> x -> x -> x
mergeExplain String
message x
x x
y = forall x. LiftT x => Typed x -> x
dropT (forall a. String -> Typed a -> Typed a
explain String
message (forall x. LiftT x => x -> Typed x
liftT (x
x forall a. Semigroup a => a -> a -> a
<> x
y)))

requireAll :: [(Bool, [String])] -> Typed a -> Typed a
requireAll :: forall a. [(Bool, [String])] -> Typed a -> Typed a
requireAll [(Bool, [String])]
xs Typed a
answer = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Bool, [String])]
bad then Typed a
answer else forall a. [String] -> Typed a
failT (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
msgs)
  where
    bad :: [(Bool, [String])]
bad = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Bool, [String])]
xs
    msgs :: [[String]]
msgs = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Bool, [String])]
bad

-- ======================================================
-- converting from a (Typed t) to something else

-- The projection from (newtype Typed t = Typed {runTyped :: Either [String] x})
-- runTyped :: Typed t => Either [String] x

-- | Pushes the (Left msgs) into a call to 'error'
errorTyped :: HasCallStack => Typed t -> t
errorTyped :: forall t. HasCallStack => Typed t -> t
errorTyped Typed t
t = case forall x. Typed x -> Either [String] x
runTyped Typed t
t of
  Right t
x -> t
x
  Left [String]
xs -> forall a. HasCallStack => String -> a
error ([String] -> String
unlines (String
"\nSolver-time error" forall a. a -> [a] -> [a]
: [String]
xs))

-- | Pushes the (Left msgs) into a call to 'error', then injects into a Monad
monadTyped :: (HasCallStack, Monad m) => Typed t -> m t
monadTyped :: forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped Typed t
t = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! forall t. HasCallStack => Typed t -> t
errorTyped Typed t
t

-- ================================================================
-- Computing runtime evidence of a constraint.

newtype Id x = Id x

-- | runTime evidence that the index 'i' of an indexed type '(s i)'
--   is constrained by the class 'c'. If one has an un-indexed type
--   't' one can always use (Id t) instead. Eg
--   With (Id x) <- hasOrd repT (Id t)
data HasConstraint c t where
  With :: c t => s t -> HasConstraint c (s t)