{-# 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
    a -> IO a
forall a. a -> IO a
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 -> b) -> Typed a -> Typed b)
-> (forall a b. a -> Typed b -> Typed a) -> Functor Typed
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
$cfmap :: forall a b. (a -> b) -> Typed a -> Typed b
fmap :: forall a b. (a -> b) -> Typed a -> Typed b
$c<$ :: forall a b. a -> Typed b -> Typed a
<$ :: forall a b. a -> Typed b -> Typed a
Functor, Functor Typed
Functor Typed =>
(forall a. a -> Typed a)
-> (forall a b. Typed (a -> b) -> Typed a -> Typed b)
-> (forall a b c. (a -> b -> c) -> Typed a -> Typed b -> Typed c)
-> (forall a b. Typed a -> Typed b -> Typed b)
-> (forall a b. Typed a -> Typed b -> Typed a)
-> Applicative 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
$cpure :: forall a. a -> Typed a
pure :: forall a. a -> Typed a
$c<*> :: forall a b. Typed (a -> b) -> Typed a -> Typed b
<*> :: forall a b. Typed (a -> b) -> Typed a -> Typed b
$cliftA2 :: forall a b c. (a -> b -> c) -> Typed a -> Typed b -> Typed c
liftA2 :: forall a b c. (a -> b -> c) -> Typed a -> Typed b -> Typed c
$c*> :: forall a b. Typed a -> Typed b -> Typed b
*> :: forall a b. Typed a -> Typed b -> Typed b
$c<* :: forall a b. Typed a -> Typed b -> Typed a
<* :: forall a b. Typed a -> Typed b -> Typed a
Applicative, Applicative Typed
Applicative Typed =>
(forall a b. Typed a -> (a -> Typed b) -> Typed b)
-> (forall a b. Typed a -> Typed b -> Typed b)
-> (forall a. a -> Typed a)
-> Monad 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
$c>>= :: forall a b. Typed a -> (a -> Typed b) -> Typed b
>>= :: forall a b. Typed a -> (a -> Typed b) -> Typed b
$c>> :: forall a b. Typed a -> Typed b -> Typed b
>> :: forall a b. Typed a -> Typed b -> Typed b
$creturn :: forall a. a -> Typed a
return :: forall a. a -> Typed a
Monad)

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

failT :: [String] -> Typed a
failT :: forall a. [String] -> Typed a
failT [String]
ss = Either [String] a -> Typed a
forall x. Either [String] x -> Typed x
Typed ([String] -> Either [String] a
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)) = Either [String] a -> Typed a
forall x. Either [String] x -> Typed x
Typed ([String] -> Either [String] a
forall a b. a -> Either a b
Left (String
s String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
ss))
explain String
_ (Typed (Right a
x)) = Either [String] a -> Typed a
forall x. Either [String] x -> Typed x
Typed (a -> Either [String] a
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 = Typed x -> x
forall x. LiftT x => Typed x -> x
dropT (String -> Typed x -> Typed x
forall a. String -> Typed a -> Typed a
explain String
message (x -> Typed x
forall x. LiftT x => x -> Typed x
liftT (x
x x -> 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 [(Bool, [String])] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Bool, [String])]
bad then Typed a
answer else [String] -> Typed a
forall a. [String] -> Typed a
failT ([[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
msgs)
  where
    bad :: [(Bool, [String])]
bad = ((Bool, [String]) -> Bool)
-> [(Bool, [String])] -> [(Bool, [String])]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((Bool, [String]) -> Bool) -> (Bool, [String]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool, [String]) -> Bool
forall a b. (a, b) -> a
fst) [(Bool, [String])]
xs
    msgs :: [[String]]
msgs = ((Bool, [String]) -> [String]) -> [(Bool, [String])] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map (Bool, [String]) -> [String]
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 Typed t -> Either [String] t
forall x. Typed x -> Either [String] x
runTyped Typed t
t of
  Right t
x -> t
x
  Left [String]
xs -> String -> t
forall a. HasCallStack => String -> a
error ([String] -> String
unlines (String
"\nSolver-time error" String -> [String] -> [String]
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 = t -> m t
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> m t) -> t -> m t
forall a b. (a -> b) -> a -> b
$! Typed t -> t
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)