{-# 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)