22{-# LANGUAGE DataKinds #-}
33{-# LANGUAGE FlexibleContexts #-}
44{-# LANGUAGE ImportQualifiedPost #-}
5+ {-# LANGUAGE OverloadedStrings #-}
56{-# LANGUAGE RankNTypes #-}
67{-# LANGUAGE RecordWildCards #-}
78{-# LANGUAGE ScopedTypeVariables #-}
@@ -36,6 +37,7 @@ import Test.Cardano.Ledger.Constrained.Conway.MiniTrace (
3637 ConstrainedGeneratorBundle (.. ),
3738 constrainedRatify ,
3839 )
40+ import Test.Cardano.Ledger.Conway.TreeDiff (tableDoc )
3941import Test.Cardano.Ledger.Imp.Common
4042
4143conformsToImplAccepted ::
@@ -59,13 +61,22 @@ conformsToImplAccepted impl agda = property $ do
5961 conjoin $
6062 zipWith
6163 ( \ ga sga ->
62- counterexample (prettify ratifyEnv ratifySt ga) $
63- impl ratifyEnv ratifySt ga == agda specEnv specSt sga
64+ let implRes = impl ratifyEnv ratifySt ga
65+ agdaRes = agda specEnv specSt sga
66+ in counterexample (prettify ratifyEnv ratifySt ga implRes agdaRes) $
67+ implRes == agdaRes
6468 )
6569 govActions
6670 specGovActions
6771 where
68- prettify ratifyEnv ratifySt ga = ansiDocToString $ Pretty. vsep $ [ansiExpr ratifyEnv, ansiExpr ratifySt, ansiExpr ga]
72+ prettify ratifyEnv ratifySt ga implRes agdaRes =
73+ ansiDocToString $
74+ Pretty. vsep $
75+ tableDoc Nothing [(" Impl:" , showAccepted implRes), (" Spec:" , showAccepted agdaRes)]
76+ : [ansiExpr ratifyEnv, ansiExpr ratifySt, ansiExpr ga]
77+
78+ showAccepted True = Pretty. brackets " ✓"
79+ showAccepted False = Pretty. brackets " ×"
6980
7081spec :: Spec
7182spec = describe " RATIFY" $ do
0 commit comments