{-# 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 (Assertion -> (SomeException -> Assertion) -> Assertion
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
Exc.catch (IO a -> Assertion
forall (f :: * -> *) a. Functor f => f a -> f ()
void IO a
x) SomeException -> Assertion
forall {a}. SomeException -> IO a
handler)
  where
    -- handler :: Exc.ErrorCall -> IO ()
    handler :: SomeException -> IO a
handler (Exc.SomeException e
zs) = String -> IO a
forall a. HasCallStack => String -> IO a
assertFailure ([String] -> String
unlines [String
msg, e -> String
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 <- Typed (Env era) -> Typed (Env era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env era) -> Typed (Env era))
-> Typed (Env era) -> Typed (Env era)
forall a b. (a -> b) -> a -> b
$ Subst era -> Env era -> Typed (Env era)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst Env era
forall era. Env era
emptyEnv
  [(String, Bool, Pred era)]
testTriples <- (Pred era -> Typed (String, Bool, Pred era))
-> [Pred era] -> Typed [(String, Bool, Pred era)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env era -> Pred era -> Typed (String, Bool, Pred era)
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 = ((String, Bool, Pred era) -> Bool)
-> [(String, Bool, Pred era)] -> [(String, Bool, Pred era)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(String
_, Bool
b, Pred era
_) -> Bool -> Bool
not Bool
b) [(String, Bool, Pred era)]
testTriples
  if [(String, Bool, Pred era)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, Bool, Pred era)]
bad
    then (Env era, Maybe String) -> Typed (Env era, Maybe String)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Env era
env, Maybe String
forall a. Maybe a
Nothing)
    else (Env era, Maybe String) -> Typed (Env era, Maybe String)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Env era
env, String -> Maybe String
forall a. a -> Maybe a
Just (String
"Some conditions fail\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(String, Bool, Pred era)] -> Subst era -> String
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 (((String, Bool, Pred era) -> String)
-> [(String, Bool, Pred era)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Bool, Pred era) -> String
forall {a} {b} {c}. (a, b, c) -> a
getString [(String, Bool, Pred era)]
cs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Map String (SubstElem era) -> String
forall a. Show a => a -> String
show Map String (SubstElem era)
restricted
  where
    names :: HashSet (Name era)
names = (HashSet (Name era) -> Pred era -> HashSet (Name era))
-> HashSet (Name era) -> [Pred era] -> HashSet (Name era)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' HashSet (Name era) -> Pred era -> HashSet (Name era)
forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred HashSet (Name era)
forall a. HashSet a
HashSet.empty (((String, Bool, Pred era) -> Pred era)
-> [(String, Bool, Pred era)] -> [Pred era]
forall a b. (a -> b) -> [a] -> [b]
map (String, Bool, Pred era) -> Pred era
forall {a} {b} {c}. (a, b, c) -> c
getPred [(String, Bool, Pred era)]
cs)
    restricted :: Map String (SubstElem era)
restricted = (String -> SubstElem era -> Bool)
-> Map String (SubstElem era) -> Map String (SubstElem era)
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) = Name era -> HashSet (Name era) -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HashSet.member (V era t -> Name era
forall era t. V era t -> Name era
Name (String -> Rep era t -> Access era s t -> V era t
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