| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.Cardano.Ledger.Conformance.ExecSpecRule.Core
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
- 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 ()
- 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
- translateWithContext ∷ SpecTranslate ctx a ⇒ ctx → a → ImpTestM era (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))
- diffConformance ∷ ToExpr a ⇒ a → a → Doc AnsiStyle
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
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 #
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 #
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.
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 #