{-# LANGUAGE BangPatterns #-}

module Test.Cardano.Ledger.Constrained.Utils (
  testIO,
  checkForSoundness,
  explainBad,
) where

import Cardano.Ledger.Conway.Core (Era)
import qualified Control.Exception as Exc
import Control.Monad (void)
import qualified Data.HashSet as HashSet
import qualified Data.List as List
import qualified Data.Map.Strict as Map
import Test.Cardano.Ledger.Constrained.Ast (
  Pred,
  Subst (..),
  SubstElem (..),
  makeTest,
  substToEnv,
  varsOfPred,
 )
import Test.Cardano.Ledger.Constrained.Env (Env, Name (..), V (..), emptyEnv)
import Test.Cardano.Ledger.Constrained.Monad (Typed, monadTyped)
import Test.Tasty (TestTree)
import Test.Tasty.HUnit (assertFailure, testCase)

testIO :: String -> IO a -> TestTree
testIO :: forall a. String -> IO a -> TestTree
testIO String
msg IO a
x = String -> Assertion -> TestTree
testCase String
msg (forall e a. Exception e => IO a -> (e -> IO a) -> IO a
Exc.catch (forall (f :: * -> *) a. Functor f => f a -> f ()
void IO a
x) forall {a}. SomeException -> IO a
handler)
  where
    -- handler :: Exc.ErrorCall -> IO ()
    handler :: SomeException -> IO a
handler (Exc.SomeException e
zs) = forall a. HasCallStack => String -> IO a
assertFailure ([String] -> String
unlines [String
msg, forall a. Show a => a -> String
show e
zs])

checkForSoundness :: Era era => [Pred era] -> Subst era -> Typed (Env era, Maybe String)
checkForSoundness :: forall era.
Era era =>
[Pred era] -> Subst era -> Typed (Env era, Maybe String)
checkForSoundness [Pred era]
preds Subst era
subst = do
  !Env era
env <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst forall era. Env era
emptyEnv
  [(String, Bool, Pred era)]
testTriples <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall era. Env era -> Pred era -> Typed (String, Bool, Pred era)
makeTest Env era
env) [Pred era]
preds
  let bad :: [(String, Bool, Pred era)]
bad = forall a. (a -> Bool) -> [a] -> [a]
filter (\(String
_, Bool
b, Pred era
_) -> Bool -> Bool
not Bool
b) [(String, Bool, Pred era)]
testTriples
  if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, Bool, Pred era)]
bad
    then forall (f :: * -> *) a. Applicative f => a -> f a
pure (Env era
env, forall a. Maybe a
Nothing)
    else forall (f :: * -> *) a. Applicative f => a -> f a
pure (Env era
env, forall a. a -> Maybe a
Just (String
"Some conditions fail\n" forall a. [a] -> [a] -> [a]
++ forall era.
Era era =>
[(String, Bool, Pred era)] -> Subst era -> String
explainBad [(String, Bool, Pred era)]
bad Subst era
subst))

explainBad :: Era era => [(String, Bool, Pred era)] -> Subst era -> String
explainBad :: forall era.
Era era =>
[(String, Bool, Pred era)] -> Subst era -> String
explainBad [(String, Bool, Pred era)]
cs (Subst Map String (SubstElem era)
subst) = [String] -> String
unlines (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {c}. (a, b, c) -> a
getString [(String, Bool, Pred era)]
cs) forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Map String (SubstElem era)
restricted
  where
    names :: HashSet (Name era)
names = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred forall a. HashSet a
HashSet.empty (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {c}. (a, b, c) -> c
getPred [(String, Bool, Pred era)]
cs)
    restricted :: Map String (SubstElem era)
restricted = forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey String -> SubstElem era -> Bool
ok Map String (SubstElem era)
subst
    ok :: String -> SubstElem era -> Bool
ok String
key (SubstElem Rep era t
rep Term era t
_term Access era s t
access) = forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HashSet.member (forall era t. V era t -> Name era
Name (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
key Rep era t
rep Access era s t
access)) HashSet (Name era)
names
    getString :: (a, b, c) -> a
getString (a
s, b
_, c
_) = a
s
    getPred :: (a, b, c) -> c
getPred (a
_, b
_, c
pr) = c
pr