| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.Cardano.Ledger.Conformance
Synopsis
- class FixupSpecRep a where
- fixup ∷ a → a
- class SpecTranslate ctx a where
- type SpecRep a ∷ Type
- toSpecRep ∷ a → SpecTransM ctx (SpecRep a)
- data SpecTransM ctx a
- type SpecTranslationError = Text
- newtype OpaqueErrorString = OpaqueErrorString String
- runSpecTransM ∷ ctx → SpecTransM ctx a → Either SpecTranslationError a
- toTestRep ∷ (SpecTranslate ctx a, FixupSpecRep (SpecRep a)) ⇒ a → SpecTransM ctx (SpecRep a)
- askCtx ∷ ∀ b ctx. Inject ctx b ⇒ SpecTransM ctx b
- withCtx ∷ ctx → SpecTransM ctx a → SpecTransM ctx' a
- 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 (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (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), HasCallStack) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → Property
- extraInfo ∷ HasCallStack ⇒ ExecContext fn rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → Doc AnsiStyle
- checkConformance ∷ ∀ rule era fn. (Era era, ToExpr (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (SpecRep (ExecState fn rule era)), Eq (SpecRep (PredicateFailure (EraRule 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 (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (ExecState fn rule era)) → Either (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (ExecState fn rule era)) → ImpTestM era ()
- defaultTestConformance ∷ ∀ fn era rule. (ShelleyEraImp era, ExecSpecRule fn 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)), 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), HasCallStack) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → Property
- runConformance ∷ ∀ (rule ∷ Symbol) (fn ∷ [Type] → Type → Type) era. (ExecSpecRule fn rule era, NFData (SpecRep (PredicateFailure (EraRule rule era))), ForAllExecSpecRep NFData fn rule era, ForAllExecSpecRep ToExpr fn rule era, FixupSpecRep (SpecRep (PredicateFailure (EraRule 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) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → ImpTestM era (Either (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (ExecState fn rule era)), Either (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (ExecState fn rule era)))
- 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) ⇒ 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
- translateWithContext ∷ SpecTranslate ctx a ⇒ ctx → a → ImpTestM era (SpecRep a)
- agdaHashToBytes ∷ Int → Integer → ByteString
- agdaHashToExpr ∷ Int → Integer → Expr
- hashToInteger ∷ Hash a b → Integer
- computationResultToEither ∷ ComputationResult e a → Either e a
Documentation
class FixupSpecRep a where Source #
Minimal complete definition
Nothing
Instances
class SpecTranslate ctx a where Source #
Methods
toSpecRep ∷ a → SpecTransM ctx (SpecRep a) Source #
Instances
data SpecTransM ctx a Source #
Instances
type SpecTranslationError = Text Source #
newtype OpaqueErrorString Source #
OpaqueErrorString behaves like unit in comparisons, but contains an error string that can be displayed.
Constructors
| OpaqueErrorString String |
Instances
runSpecTransM ∷ ctx → SpecTransM ctx a → Either SpecTranslationError a Source #
toTestRep ∷ (SpecTranslate ctx a, FixupSpecRep (SpecRep a)) ⇒ a → SpecTransM ctx (SpecRep a) Source #
askCtx ∷ ∀ b ctx. Inject ctx b ⇒ SpecTransM ctx b Source #
withCtx ∷ ctx → SpecTransM ctx a → SpecTransM ctx' a Source #
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 (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (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), HasCallStack) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → Property Source #
extraInfo ∷ HasCallStack ⇒ ExecContext fn rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → Doc AnsiStyle Source #
Instances
checkConformance ∷ ∀ rule era fn. (Era era, ToExpr (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (SpecRep (ExecState fn rule era)), Eq (SpecRep (PredicateFailure (EraRule 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 (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (ExecState fn rule era)) → Either (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (ExecState fn rule era)) → ImpTestM era () Source #
defaultTestConformance ∷ ∀ fn era rule. (ShelleyEraImp era, ExecSpecRule fn 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)), 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), HasCallStack) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → Property Source #
runConformance ∷ ∀ (rule ∷ Symbol) (fn ∷ [Type] → Type → Type) era. (ExecSpecRule fn rule era, NFData (SpecRep (PredicateFailure (EraRule rule era))), ForAllExecSpecRep NFData fn rule era, ForAllExecSpecRep ToExpr fn rule era, FixupSpecRep (SpecRep (PredicateFailure (EraRule 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) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → ImpTestM era (Either (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (ExecState fn rule era)), Either (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (ExecState fn rule era))) Source #
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) ⇒ 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 #
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.
agdaHashToBytes ∷ Int → Integer → ByteString Source #
hashToInteger ∷ Hash a b → Integer Source #
computationResultToEither ∷ ComputationResult e a → Either e a Source #