| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.Cardano.Ledger.Conformance
Synopsis
- newtype OpaqueErrorString = OpaqueErrorString (NonEmpty Text)
- 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
- 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
- showOpaqueErrorString ∷ ToExpr a ⇒ a → OpaqueErrorString
- unComputationResult ∷ ComputationResult Text a → Either OpaqueErrorString a
- unComputationResult_ ∷ ComputationResult Void a → Either e 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 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
- 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
- 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
- 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)]))
- 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
- translateWithContext ∷ SpecTranslate ctx a ⇒ ctx → a → ImpTestM era (SpecRep a)
- standardHashSize ∷ Int
- agdaHashToBytes ∷ Int → Integer → ByteString
- agdaHashToExpr ∷ Int → Integer → Expr
- hashToInteger ∷ Hash a b → Integer
- integerToHash ∷ ∀ h a. HashAlgorithm h ⇒ Integer → Maybe (Hash h a)
Documentation
newtype OpaqueErrorString Source #
OpaqueErrorString behaves like unit in comparisons, but contains an error string that can be displayed.
Constructors
| OpaqueErrorString (NonEmpty Text) |
Instances
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 #
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 #
showOpaqueErrorString ∷ ToExpr a ⇒ a → OpaqueErrorString Source #
unComputationResult_ ∷ ComputationResult Void a → Either e 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 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
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 #
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 #
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 #
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 #
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 #
integerToHash ∷ ∀ h a. HashAlgorithm h ⇒ Integer → Maybe (Hash h a) Source #