| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.Cardano.Ledger.Conformance.ExecSpecRule.Core
Synopsis
- class (ForAllExecTypes (HasSpec fn) fn rule era, ForAllExecTypes ToExpr fn rule era, ForAllExecTypes NFData fn rule era, KnownSymbol rule, STS (EraRule rule era), BaseM (EraRule rule era) ~ ShelleyBase, SpecTranslate (ExecContext fn rule era) (PredicateFailure (EraRule rule era)), Inject (ExecEnvironment fn rule era) (Environment (EraRule rule era)), Inject (ExecState fn rule era) (State (EraRule rule era)), Inject (ExecSignal fn rule era) (Signal (EraRule rule era))) ⇒ ExecSpecRule fn (rule ∷ Symbol) era where
- type ExecContext fn rule era
- type ExecEnvironment fn rule era
- type ExecState fn rule era
- type ExecSignal fn rule era
- environmentSpec ∷ HasCallStack ⇒ ExecContext fn rule era → Specification fn (ExecEnvironment fn rule era)
- stateSpec ∷ HasCallStack ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → Specification fn (ExecState fn rule era)
- signalSpec ∷ HasCallStack ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → Specification fn (ExecSignal fn rule era)
- classOf ∷ ExecSignal fn rule era → Maybe String
- genExecContext ∷ HasCallStack ⇒ Gen (ExecContext fn rule era)
- runAgdaRule ∷ HasCallStack ⇒ SpecRep (ExecEnvironment fn rule era) → SpecRep (ExecState fn rule era) → SpecRep (ExecSignal fn rule era) → Either OpaqueErrorString (SpecRep (ExecState fn rule era))
- translateInputs ∷ HasCallStack ⇒ ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → ExecContext fn rule era → ImpTestM era (SpecRep (ExecEnvironment fn rule era), SpecRep (ExecState fn rule era), SpecRep (ExecSignal fn rule era))
- testConformance ∷ (ShelleyEraImp era, SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)), ForAllExecSpecRep NFData fn rule era, ForAllExecSpecRep ToExpr fn rule era, NFData (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (ExecState fn rule era)), Inject (State (EraRule rule era)) (ExecState fn rule era), SpecTranslate (ExecContext fn rule era) (ExecState fn rule era), FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (SpecRep (ExecState fn rule era)), Inject (ExecEnvironment fn rule era) (Environment (EraRule rule era)), Inject (ExecState fn rule era) (State (EraRule rule era)), Inject (ExecSignal fn rule era) (Signal (EraRule rule era)), EncCBOR (ExecContext fn rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), ToExpr (ExecContext fn rule era), ToExpr (PredicateFailure (EraRule rule era)), NFData (PredicateFailure (EraRule rule era)), HasCallStack) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → Property
- extraInfo ∷ HasCallStack ⇒ Globals → ExecContext fn 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) fn era. (ShelleyEraImp era, ExecSpecRule fn rule era, ForAllExecSpecRep NFData fn rule era, ForAllExecSpecRep ToExpr fn rule era, NFData (SpecRep (PredicateFailure (EraRule rule era))), NFData (ExecContext fn rule era), ToExpr (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (ExecContext fn rule era), SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)), Eq (SpecRep (PredicateFailure (EraRule rule era))), Inject (State (EraRule rule era)) (ExecState fn rule era), Eq (SpecRep (ExecState fn rule era)), SpecTranslate (ExecContext fn rule era) (ExecState fn rule era), FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (SpecRep (ExecState fn rule era)), EncCBOR (ExecContext fn 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 ∷ ∀ (fn ∷ [Type] → Type → Type) (rule ∷ Symbol) era. ExecSpecRule fn rule era ⇒ Int → Spec
- runConformance ∷ ∀ (rule ∷ Symbol) (fn ∷ [Type] → Type → Type) era. (ExecSpecRule fn rule era, ForAllExecSpecRep NFData fn rule era, ForAllExecSpecRep ToExpr fn rule era, FixupSpecRep (SpecRep (ExecState fn rule era)), Inject (State (EraRule rule era)) (ExecState fn rule era), SpecTranslate (ExecContext fn rule era) (ExecState fn rule era), ToExpr (ExecContext fn rule era), HasCallStack, NFData (PredicateFailure (EraRule rule era))) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → ImpTestM era (Either (NonEmpty (PredicateFailure (EraRule rule era))) (SpecRep (ExecState fn rule era)), Either OpaqueErrorString (SpecRep (ExecState fn rule era)), Either (NonEmpty (PredicateFailure (EraRule rule era))) (State (EraRule rule era), [Event (EraRule rule era)]))
- checkConformance ∷ ∀ rule era fn. (Era era, ToExpr (SpecRep (ExecState fn rule era)), Eq (SpecRep (ExecState fn rule era)), EncCBOR (ExecContext fn rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), HasCallStack) ⇒ ExecContext fn rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → Either OpaqueErrorString (SpecRep (ExecState fn rule era)) → Either OpaqueErrorString (SpecRep (ExecState fn rule era)) → ImpTestM era ()
- defaultTestConformance ∷ ∀ fn era rule. (HasCallStack, ShelleyEraImp era, ExecSpecRule fn rule era, ForAllExecSpecRep NFData fn rule era, ForAllExecSpecRep ToExpr fn rule era, NFData (PredicateFailure (EraRule rule era)), Eq (SpecRep (ExecState fn rule era)), Inject (State (EraRule rule era)) (ExecState fn rule era), SpecTranslate (ExecContext fn rule era) (ExecState fn rule era), FixupSpecRep (SpecRep (ExecState fn rule era)), EncCBOR (ExecContext fn rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), ToExpr (ExecContext fn rule era), ToExpr (PredicateFailure (EraRule rule era))) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → Property
- translateWithContext ∷ SpecTranslate ctx a ⇒ ctx → a → ImpTestM era (SpecRep a)
- type ForAllExecSpecRep (c ∷ Type → Constraint) fn rule era = (c (SpecRep (ExecEnvironment fn rule era)), c (SpecRep (ExecState fn rule era)), c (SpecRep (ExecSignal fn rule era)))
- type ForAllExecTypes (c ∷ Type → Constraint) fn rule era = (c (ExecEnvironment fn rule era), c (ExecState fn rule era), c (ExecSignal fn rule era))
- diffConformance ∷ ToExpr a ⇒ a → a → Doc AnsiStyle
Documentation
class (ForAllExecTypes (HasSpec fn) fn rule era, ForAllExecTypes ToExpr fn rule era, ForAllExecTypes NFData fn rule era, KnownSymbol rule, STS (EraRule rule era), BaseM (EraRule rule era) ~ ShelleyBase, SpecTranslate (ExecContext fn rule era) (PredicateFailure (EraRule rule era)), Inject (ExecEnvironment fn rule era) (Environment (EraRule rule era)), Inject (ExecState fn rule era) (State (EraRule rule era)), Inject (ExecSignal fn rule era) (Signal (EraRule rule era))) ⇒ ExecSpecRule fn (rule ∷ Symbol) era where Source #
Minimal complete definition
Associated Types
type ExecContext fn rule era Source #
type ExecContext fn rule era = ()
type ExecEnvironment fn rule era Source #
type ExecEnvironment fn rule era = Environment (EraRule rule era)
type ExecState fn rule era Source #
type ExecSignal fn rule era Source #
type ExecSignal fn rule era = Signal (EraRule rule era)
Methods
environmentSpec ∷ HasCallStack ⇒ ExecContext fn rule era → Specification fn (ExecEnvironment fn rule era) Source #
stateSpec ∷ HasCallStack ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → Specification fn (ExecState fn rule era) Source #
signalSpec ∷ HasCallStack ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → Specification fn (ExecSignal fn rule era) Source #
classOf ∷ ExecSignal fn rule era → Maybe String Source #
genExecContext ∷ HasCallStack ⇒ Gen (ExecContext fn rule era) Source #
default genExecContext ∷ Arbitrary (ExecContext fn rule era) ⇒ Gen (ExecContext fn rule era) Source #
runAgdaRule ∷ HasCallStack ⇒ SpecRep (ExecEnvironment fn rule era) → SpecRep (ExecState fn rule era) → SpecRep (ExecSignal fn rule era) → Either OpaqueErrorString (SpecRep (ExecState fn rule era)) Source #
translateInputs ∷ HasCallStack ⇒ ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → ExecContext fn rule era → ImpTestM era (SpecRep (ExecEnvironment fn rule era), SpecRep (ExecState fn rule era), SpecRep (ExecSignal fn rule era)) Source #
default translateInputs ∷ (ForAllExecTypes (SpecTranslate (ExecContext fn rule era)) fn rule era, ForAllExecSpecRep ToExpr fn rule era) ⇒ ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → ExecContext fn rule era → ImpTestM era (SpecRep (ExecEnvironment fn rule era), SpecRep (ExecState fn rule era), SpecRep (ExecSignal fn rule era)) Source #
testConformance ∷ (ShelleyEraImp era, SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)), ForAllExecSpecRep NFData fn rule era, ForAllExecSpecRep ToExpr fn rule era, NFData (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (ExecState fn rule era)), Inject (State (EraRule rule era)) (ExecState fn rule era), SpecTranslate (ExecContext fn rule era) (ExecState fn rule era), FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (SpecRep (ExecState fn rule era)), Inject (ExecEnvironment fn rule era) (Environment (EraRule rule era)), Inject (ExecState fn rule era) (State (EraRule rule era)), Inject (ExecSignal fn rule era) (Signal (EraRule rule era)), EncCBOR (ExecContext fn rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), ToExpr (ExecContext fn rule era), ToExpr (PredicateFailure (EraRule rule era)), NFData (PredicateFailure (EraRule rule era)), HasCallStack) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → Property Source #
extraInfo ∷ HasCallStack ⇒ Globals → ExecContext fn 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) fn era. (ShelleyEraImp era, ExecSpecRule fn rule era, ForAllExecSpecRep NFData fn rule era, ForAllExecSpecRep ToExpr fn rule era, NFData (SpecRep (PredicateFailure (EraRule rule era))), NFData (ExecContext fn rule era), ToExpr (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (ExecContext fn rule era), SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)), Eq (SpecRep (PredicateFailure (EraRule rule era))), Inject (State (EraRule rule era)) (ExecState fn rule era), Eq (SpecRep (ExecState fn rule era)), SpecTranslate (ExecContext fn rule era) (ExecState fn rule era), FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (SpecRep (ExecState fn rule era)), EncCBOR (ExecContext fn 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 ∷ ∀ (fn ∷ [Type] → Type → Type) (rule ∷ Symbol) era. ExecSpecRule fn rule era ⇒ Int → Spec Source #
runConformance ∷ ∀ (rule ∷ Symbol) (fn ∷ [Type] → Type → Type) era. (ExecSpecRule fn rule era, ForAllExecSpecRep NFData fn rule era, ForAllExecSpecRep ToExpr fn rule era, FixupSpecRep (SpecRep (ExecState fn rule era)), Inject (State (EraRule rule era)) (ExecState fn rule era), SpecTranslate (ExecContext fn rule era) (ExecState fn rule era), ToExpr (ExecContext fn rule era), HasCallStack, NFData (PredicateFailure (EraRule rule era))) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → ImpTestM era (Either (NonEmpty (PredicateFailure (EraRule rule era))) (SpecRep (ExecState fn rule era)), Either OpaqueErrorString (SpecRep (ExecState fn rule era)), Either (NonEmpty (PredicateFailure (EraRule rule era))) (State (EraRule rule era), [Event (EraRule rule era)])) Source #
checkConformance ∷ ∀ rule era fn. (Era era, ToExpr (SpecRep (ExecState fn rule era)), Eq (SpecRep (ExecState fn rule era)), EncCBOR (ExecContext fn rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), HasCallStack) ⇒ ExecContext fn rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → Either OpaqueErrorString (SpecRep (ExecState fn rule era)) → Either OpaqueErrorString (SpecRep (ExecState fn rule era)) → ImpTestM era () Source #
defaultTestConformance ∷ ∀ fn era rule. (HasCallStack, ShelleyEraImp era, ExecSpecRule fn rule era, ForAllExecSpecRep NFData fn rule era, ForAllExecSpecRep ToExpr fn rule era, NFData (PredicateFailure (EraRule rule era)), Eq (SpecRep (ExecState fn rule era)), Inject (State (EraRule rule era)) (ExecState fn rule era), SpecTranslate (ExecContext fn rule era) (ExecState fn rule era), FixupSpecRep (SpecRep (ExecState fn rule era)), EncCBOR (ExecContext fn rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), ToExpr (ExecContext fn rule era), ToExpr (PredicateFailure (EraRule rule era))) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn 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) fn rule era = (c (SpecRep (ExecEnvironment fn rule era)), c (SpecRep (ExecState fn rule era)), c (SpecRep (ExecSignal fn rule era))) Source #
type ForAllExecTypes (c ∷ Type → Constraint) fn rule era = (c (ExecEnvironment fn rule era), c (ExecState fn rule era), c (ExecSignal fn rule era)) Source #