Skip to content

Commit

Permalink
Improved the error messages when a Spec fails.
Browse files Browse the repository at this point in the history
The function explainSpec no longer drops explanations on TypeSpec
Added guardTypeSpec, which catches errors earlier, so there is less noise.
function symbols like subset_ and member_ print a elided version of their set
arguments when they are large literals. Improves readabilty as irrelevant
information no longer overwhelms the user.
Add the constructor ExplainSpec to Specification
Assert now has type Assert :: Term fn Bool -> Pred fn
  • Loading branch information
TimSheard committed Nov 15, 2024
1 parent 8a090f2 commit 16f5cf0
Show file tree
Hide file tree
Showing 15 changed files with 430 additions and 193 deletions.
2 changes: 1 addition & 1 deletion eras/byron/chain/executable-spec/byron-spec-chain.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -62,5 +62,5 @@ test-suite chain-rules-test
tasty-hedgehog,
tasty-hunit,
byron-spec-chain,
byron-spec-ledger,
byron-spec-ledger >=1.0,
small-steps:{small-steps, testlib} >=1.1
Original file line number Diff line number Diff line change
Expand Up @@ -1687,6 +1687,7 @@ instance CoercibleLike (CompactForm Coin) Word64 where
, reify x' unCompactCoin (==. V x)
]
coerceSpec TrueSpec = TrueSpec
coerceSpec (ExplainSpec es x) = ExplainSpec es (coerceSpec x)

getCoerceSpec ::
forall (fn :: [Type] -> Type -> Type).
Expand Down Expand Up @@ -1762,6 +1763,8 @@ toDelta_ ::
toDelta_ = app toDeltaFn

instance (Typeable fn, Member (CoinFn fn) fn) => Functions (CoinFn fn) fn where
propagateSpecFun fn ctx (ExplainSpec [] s) = propagateSpecFun fn ctx s
propagateSpecFun fn ctx (ExplainSpec es s) = ExplainSpec es $ propagateSpecFun fn ctx s
propagateSpecFun _ _ TrueSpec = TrueSpec
propagateSpecFun _ _ (ErrorSpec err) = ErrorSpec err
propagateSpecFun fn (ListCtx pre HOLE suf) (SuspendedSpec x p) =
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ import Cardano.Ledger.UMap (CompactForm (..))
import qualified Cardano.Ledger.UMap as UMap
import Cardano.Ledger.UTxO (UTxO (..))
import Constrained hiding (Value)
import Constrained.Base (Pred (..), hasSize, rangeSize)
import Constrained.Base (Pred (..))
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,6 @@ import Cardano.Ledger.Shelley.LedgerState (
)
import Cardano.Ledger.UTxO (UTxO (..))
import Constrained hiding (Value)
import Constrained.Base (hasSize, rangeSize)
import Data.Kind (Type)
import Data.Map (Map)
import qualified Data.Set as Set
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,6 @@ import Cardano.Ledger.SafeHash ()
import Cardano.Ledger.Shelley.LedgerState
import Cardano.Ledger.UTxO (UTxO (..))
import Constrained hiding (Value)
import Constrained.Base (hasSize, rangeSize)
import Data.Map (Map)
import Test.Cardano.Ledger.Constrained.Conway ()
import Test.Cardano.Ledger.Constrained.Conway.Instances
Expand Down
3 changes: 3 additions & 0 deletions libs/constrained-generators/src/Constrained.hs
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ module Constrained (
MapSpec (..),
FoldSpec (..),
simplifySpec,
addToErrorSpec,
genFromSpecT,
genFromSpec,
genFromSpecWithSeed,
Expand Down Expand Up @@ -117,6 +118,8 @@ module Constrained (
cNothing_,
cJust_,
null_,
rangeSize,
hasSize,
injectFn,
app,
lit,
Expand Down
Loading

0 comments on commit 16f5cf0

Please sign in to comment.