| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.Cardano.Ledger.Conformance
Synopsis
- class (ForAllExecTypes HasSpec rule era, ForAllExecTypes ToExpr rule era, ForAllExecTypes NFData rule era, KnownSymbol rule, STS (EraRule rule era), BaseM (EraRule rule era) ~ ShelleyBase, SpecTranslate (ExecContext rule era) (PredicateFailure (EraRule rule era)), Inject (ExecEnvironment rule era) (Environment (EraRule rule era)), Inject (ExecState rule era) (State (EraRule rule era)), Inject (ExecSignal rule era) (Signal (EraRule rule era))) ⇒ ExecSpecRule (rule ∷ Symbol) era where
- type ExecContext rule era
- type ExecEnvironment rule era
- type ExecState rule era
- type ExecSignal rule era
- environmentSpec ∷ HasCallStack ⇒ ExecContext rule era → Specification (ExecEnvironment rule era)
- stateSpec ∷ HasCallStack ⇒ ExecContext rule era → ExecEnvironment rule era → Specification (ExecState rule era)
- signalSpec ∷ HasCallStack ⇒ ExecContext rule era → ExecEnvironment rule era → ExecState rule era → Specification (ExecSignal rule era)
- classOf ∷ ExecSignal rule era → Maybe String
- genExecContext ∷ HasCallStack ⇒ Gen (ExecContext rule era)
- runAgdaRule ∷ HasCallStack ⇒ SpecRep (ExecEnvironment rule era) → SpecRep (ExecState rule era) → SpecRep (ExecSignal rule era) → Either OpaqueErrorString (SpecRep (ExecState rule era))
- translateInputs ∷ HasCallStack ⇒ ExecEnvironment rule era → ExecState rule era → ExecSignal rule era → ExecContext rule era → ImpTestM era (SpecRep (ExecEnvironment rule era), SpecRep (ExecState rule era), SpecRep (ExecSignal rule era))
- testConformance ∷ (ShelleyEraImp era, SpecTranslate (ExecContext rule era) (State (EraRule rule era)), ForAllExecSpecRep NFData rule era, ForAllExecSpecRep ToExpr rule era, NFData (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (ExecState rule era)), Inject (State (EraRule rule era)) (ExecState rule era), SpecTranslate (ExecContext rule era) (ExecState rule era), FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (SpecRep (ExecState rule era)), Inject (ExecEnvironment rule era) (Environment (EraRule rule era)), Inject (ExecState rule era) (State (EraRule rule era)), Inject (ExecSignal rule era) (Signal (EraRule rule era)), EncCBOR (ExecContext rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), ToExpr (ExecContext rule era), ToExpr (PredicateFailure (EraRule rule era)), NFData (PredicateFailure (EraRule rule era)), HasCallStack) ⇒ ExecContext rule era → ExecEnvironment rule era → ExecState rule era → ExecSignal rule era → Property
- extraInfo ∷ HasCallStack ⇒ Globals → ExecContext rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → Either OpaqueErrorString (State (EraRule rule era), [Event (EraRule rule era)]) → Doc AnsiStyle
- class SpecTranslate ctx a where
- type SpecRep a ∷ Type
- toSpecRep ∷ a → SpecTransM ctx (SpecRep a)
- type ForAllExecSpecRep (c ∷ Type → Constraint) rule era = (c (SpecRep (ExecEnvironment rule era)), c (SpecRep (ExecState rule era)), c (SpecRep (ExecSignal rule era)))
- type ForAllExecTypes (c ∷ Type → Constraint) rule era = (c (ExecEnvironment rule era), c (ExecState rule era), c (ExecSignal rule era))
- class FixupSpecRep a where
- fixup ∷ a → a
- newtype OpaqueErrorString = OpaqueErrorString (NonEmpty Text)
- type SpecTranslationError = Text
- data SpecTransM ctx a
- integerToHash ∷ ∀ h a. HashAlgorithm h ⇒ Integer → Maybe (Hash h a)
- runSpecTransM ∷ ctx → SpecTransM ctx a → Either SpecTranslationError a
- unComputationResult ∷ ComputationResult Text a → Either OpaqueErrorString a
- unComputationResult_ ∷ ComputationResult Void a → Either e a
- defaultTestConformance ∷ ∀ era rule. (HasCallStack, ShelleyEraImp era, ExecSpecRule rule era, ForAllExecSpecRep NFData rule era, ForAllExecSpecRep ToExpr rule era, NFData (PredicateFailure (EraRule rule era)), Eq (SpecRep (ExecState rule era)), Inject (State (EraRule rule era)) (ExecState rule era), SpecTranslate (ExecContext rule era) (ExecState rule era), FixupSpecRep (SpecRep (ExecState rule era)), EncCBOR (ExecContext rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), ToExpr (ExecContext rule era), ToExpr (PredicateFailure (EraRule rule era))) ⇒ ExecContext rule era → ExecEnvironment rule era → ExecState rule era → ExecSignal rule era → Property
- conformsToImpl ∷ ∀ (rule ∷ Symbol) era. (ShelleyEraImp era, ExecSpecRule rule era, ForAllExecSpecRep NFData rule era, ForAllExecSpecRep ToExpr rule era, NFData (SpecRep (PredicateFailure (EraRule rule era))), NFData (ExecContext rule era), ToExpr (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (ExecContext rule era), SpecTranslate (ExecContext rule era) (State (EraRule rule era)), Eq (SpecRep (PredicateFailure (EraRule rule era))), Inject (State (EraRule rule era)) (ExecState rule era), Eq (SpecRep (ExecState rule era)), SpecTranslate (ExecContext rule era) (ExecState rule era), FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (SpecRep (ExecState rule era)), EncCBOR (ExecContext rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), HasCallStack, NFData (PredicateFailure (EraRule rule era)), ToExpr (PredicateFailure (EraRule rule era))) ⇒ Property
- generatesWithin ∷ ∀ a. (NFData a, ToExpr a, Typeable a, HasCallStack) ⇒ Gen a → Int → Spec
- inputsGenerateWithin ∷ ∀ (rule ∷ Symbol) era. ExecSpecRule rule era ⇒ Int → Spec
- runConformance ∷ ∀ (rule ∷ Symbol) era. (ExecSpecRule rule era, ForAllExecSpecRep NFData rule era, ForAllExecSpecRep ToExpr rule era, FixupSpecRep (SpecRep (ExecState rule era)), Inject (State (EraRule rule era)) (ExecState rule era), SpecTranslate (ExecContext rule era) (ExecState rule era), ToExpr (ExecContext rule era), HasCallStack, NFData (PredicateFailure (EraRule rule era))) ⇒ ExecContext rule era → ExecEnvironment rule era → ExecState rule era → ExecSignal rule era → ImpTestM era (Either (NonEmpty (PredicateFailure (EraRule rule era))) (SpecRep (ExecState rule era)), Either OpaqueErrorString (SpecRep (ExecState rule era)), Either (NonEmpty (PredicateFailure (EraRule rule era))) (State (EraRule rule era), [Event (EraRule rule era)]))
- checkConformance ∷ ∀ rule era. (Era era, ToExpr (SpecRep (ExecState rule era)), Eq (SpecRep (ExecState rule era)), EncCBOR (ExecContext rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), HasCallStack) ⇒ ExecContext rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → Either OpaqueErrorString (SpecRep (ExecState rule era)) → Either OpaqueErrorString (SpecRep (ExecState rule era)) → ImpTestM era ()
- translateWithContext ∷ SpecTranslate ctx a ⇒ ctx → a → ImpTestM era (SpecRep a)
- diffConformance ∷ ToExpr a ⇒ a → a → Doc AnsiStyle
- showOpaqueErrorString ∷ ToExpr a ⇒ a → OpaqueErrorString
- toTestRep ∷ (SpecTranslate ctx a, FixupSpecRep (SpecRep a)) ⇒ a → SpecTransM ctx (SpecRep a)
- askCtx ∷ ∀ b ctx. Inject ctx b ⇒ SpecTransM ctx b
- hashToInteger ∷ Hash a b → Integer
- withCtx ∷ ctx → SpecTransM ctx a → SpecTransM ctx' a
- agdaHashToBytes ∷ Int → Integer → ByteString
- agdaHashToExpr ∷ Int → Integer → Expr
Documentation
class (ForAllExecTypes HasSpec rule era, ForAllExecTypes ToExpr rule era, ForAllExecTypes NFData rule era, KnownSymbol rule, STS (EraRule rule era), BaseM (EraRule rule era) ~ ShelleyBase, SpecTranslate (ExecContext rule era) (PredicateFailure (EraRule rule era)), Inject (ExecEnvironment rule era) (Environment (EraRule rule era)), Inject (ExecState rule era) (State (EraRule rule era)), Inject (ExecSignal rule era) (Signal (EraRule rule era))) ⇒ ExecSpecRule (rule ∷ Symbol) era where Source #
Minimal complete definition
Associated Types
type ExecContext rule era Source #
type ExecContext rule era = ()
type ExecEnvironment rule era Source #
type ExecEnvironment rule era = Environment (EraRule rule era)
type ExecState rule era Source #
type ExecSignal rule era Source #
type ExecSignal rule era = Signal (EraRule rule era)
Methods
environmentSpec ∷ HasCallStack ⇒ ExecContext rule era → Specification (ExecEnvironment rule era) Source #
stateSpec ∷ HasCallStack ⇒ ExecContext rule era → ExecEnvironment rule era → Specification (ExecState rule era) Source #
signalSpec ∷ HasCallStack ⇒ ExecContext rule era → ExecEnvironment rule era → ExecState rule era → Specification (ExecSignal rule era) Source #
classOf ∷ ExecSignal rule era → Maybe String Source #
genExecContext ∷ HasCallStack ⇒ Gen (ExecContext rule era) Source #
default genExecContext ∷ Arbitrary (ExecContext rule era) ⇒ Gen (ExecContext rule era) Source #
runAgdaRule ∷ HasCallStack ⇒ SpecRep (ExecEnvironment rule era) → SpecRep (ExecState rule era) → SpecRep (ExecSignal rule era) → Either OpaqueErrorString (SpecRep (ExecState rule era)) Source #
translateInputs ∷ HasCallStack ⇒ ExecEnvironment rule era → ExecState rule era → ExecSignal rule era → ExecContext rule era → ImpTestM era (SpecRep (ExecEnvironment rule era), SpecRep (ExecState rule era), SpecRep (ExecSignal rule era)) Source #
default translateInputs ∷ (ForAllExecTypes (SpecTranslate (ExecContext rule era)) rule era, ForAllExecSpecRep ToExpr rule era) ⇒ ExecEnvironment rule era → ExecState rule era → ExecSignal rule era → ExecContext rule era → ImpTestM era (SpecRep (ExecEnvironment rule era), SpecRep (ExecState rule era), SpecRep (ExecSignal rule era)) Source #
testConformance ∷ (ShelleyEraImp era, SpecTranslate (ExecContext rule era) (State (EraRule rule era)), ForAllExecSpecRep NFData rule era, ForAllExecSpecRep ToExpr rule era, NFData (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (ExecState rule era)), Inject (State (EraRule rule era)) (ExecState rule era), SpecTranslate (ExecContext rule era) (ExecState rule era), FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (SpecRep (ExecState rule era)), Inject (ExecEnvironment rule era) (Environment (EraRule rule era)), Inject (ExecState rule era) (State (EraRule rule era)), Inject (ExecSignal rule era) (Signal (EraRule rule era)), EncCBOR (ExecContext rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), ToExpr (ExecContext rule era), ToExpr (PredicateFailure (EraRule rule era)), NFData (PredicateFailure (EraRule rule era)), HasCallStack) ⇒ ExecContext rule era → ExecEnvironment rule era → ExecState rule era → ExecSignal rule era → Property Source #
extraInfo ∷ HasCallStack ⇒ Globals → ExecContext rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → Either OpaqueErrorString (State (EraRule rule era), [Event (EraRule rule era)]) → Doc AnsiStyle Source #
Instances
class SpecTranslate ctx a where Source #
Methods
toSpecRep ∷ a → SpecTransM ctx (SpecRep a) Source #
Instances
type ForAllExecSpecRep (c ∷ Type → Constraint) rule era = (c (SpecRep (ExecEnvironment rule era)), c (SpecRep (ExecState rule era)), c (SpecRep (ExecSignal rule era))) Source #
type ForAllExecTypes (c ∷ Type → Constraint) rule era = (c (ExecEnvironment rule era), c (ExecState rule era), c (ExecSignal rule era)) Source #
class FixupSpecRep a where Source #
Minimal complete definition
Nothing
Instances
newtype OpaqueErrorString Source #
OpaqueErrorString behaves like unit in comparisons, but contains an error string that can be displayed.
Constructors
| OpaqueErrorString (NonEmpty Text) |
Instances
type SpecTranslationError = Text Source #
data SpecTransM ctx a Source #
Instances
integerToHash ∷ ∀ h a. HashAlgorithm h ⇒ Integer → Maybe (Hash h a) Source #
runSpecTransM ∷ ctx → SpecTransM ctx a → Either SpecTranslationError a Source #
unComputationResult_ ∷ ComputationResult Void a → Either e a Source #
defaultTestConformance ∷ ∀ era rule. (HasCallStack, ShelleyEraImp era, ExecSpecRule rule era, ForAllExecSpecRep NFData rule era, ForAllExecSpecRep ToExpr rule era, NFData (PredicateFailure (EraRule rule era)), Eq (SpecRep (ExecState rule era)), Inject (State (EraRule rule era)) (ExecState rule era), SpecTranslate (ExecContext rule era) (ExecState rule era), FixupSpecRep (SpecRep (ExecState rule era)), EncCBOR (ExecContext rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), ToExpr (ExecContext rule era), ToExpr (PredicateFailure (EraRule rule era))) ⇒ ExecContext rule era → ExecEnvironment rule era → ExecState rule era → ExecSignal rule era → Property Source #
conformsToImpl ∷ ∀ (rule ∷ Symbol) era. (ShelleyEraImp era, ExecSpecRule rule era, ForAllExecSpecRep NFData rule era, ForAllExecSpecRep ToExpr rule era, NFData (SpecRep (PredicateFailure (EraRule rule era))), NFData (ExecContext rule era), ToExpr (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (ExecContext rule era), SpecTranslate (ExecContext rule era) (State (EraRule rule era)), Eq (SpecRep (PredicateFailure (EraRule rule era))), Inject (State (EraRule rule era)) (ExecState rule era), Eq (SpecRep (ExecState rule era)), SpecTranslate (ExecContext rule era) (ExecState rule era), FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (SpecRep (ExecState rule era)), EncCBOR (ExecContext rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), HasCallStack, NFData (PredicateFailure (EraRule rule era)), ToExpr (PredicateFailure (EraRule rule era))) ⇒ Property Source #
generatesWithin ∷ ∀ a. (NFData a, ToExpr a, Typeable a, HasCallStack) ⇒ Gen a → Int → Spec Source #
inputsGenerateWithin ∷ ∀ (rule ∷ Symbol) era. ExecSpecRule rule era ⇒ Int → Spec Source #
runConformance ∷ ∀ (rule ∷ Symbol) era. (ExecSpecRule rule era, ForAllExecSpecRep NFData rule era, ForAllExecSpecRep ToExpr rule era, FixupSpecRep (SpecRep (ExecState rule era)), Inject (State (EraRule rule era)) (ExecState rule era), SpecTranslate (ExecContext rule era) (ExecState rule era), ToExpr (ExecContext rule era), HasCallStack, NFData (PredicateFailure (EraRule rule era))) ⇒ ExecContext rule era → ExecEnvironment rule era → ExecState rule era → ExecSignal rule era → ImpTestM era (Either (NonEmpty (PredicateFailure (EraRule rule era))) (SpecRep (ExecState rule era)), Either OpaqueErrorString (SpecRep (ExecState rule era)), Either (NonEmpty (PredicateFailure (EraRule rule era))) (State (EraRule rule era), [Event (EraRule rule era)])) Source #
checkConformance ∷ ∀ rule era. (Era era, ToExpr (SpecRep (ExecState rule era)), Eq (SpecRep (ExecState rule era)), EncCBOR (ExecContext rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), HasCallStack) ⇒ ExecContext rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → Either OpaqueErrorString (SpecRep (ExecState rule era)) → Either OpaqueErrorString (SpecRep (ExecState rule era)) → ImpTestM era () Source #
translateWithContext ∷ SpecTranslate ctx a ⇒ ctx → a → ImpTestM era (SpecRep a) Source #
Translate a Haskell type a whose translation context is ctx into its Agda type, in the ImpTest monad.
showOpaqueErrorString ∷ ToExpr a ⇒ a → OpaqueErrorString Source #
toTestRep ∷ (SpecTranslate ctx a, FixupSpecRep (SpecRep a)) ⇒ a → SpecTransM ctx (SpecRep a) Source #
askCtx ∷ ∀ b ctx. Inject ctx b ⇒ SpecTransM ctx b Source #
hashToInteger ∷ Hash a b → Integer Source #
withCtx ∷ ctx → SpecTransM ctx a → SpecTransM ctx' a Source #
agdaHashToBytes ∷ Int → Integer → ByteString Source #